You can also check out
src/bool/boolScript.sml
in the HOL4 distribution where quite a few theorems are proved
about the connectives and quantifiers. Those are forward proofs
since tactics don't yet exist at that stage of system build. So they
should be easy to adapt to your framework. One example:
(* ------------------------------------------------------------------------- *)
(* Skolemization: |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) *)
(* ------------------------------------------------------------------------- *)
val SKOLEM_THM = save_thm("SKOLEM_THM",
let val P = Term`P:'a -> 'b -> bool`
val x = Term`x:'a`
val y = Term`y:'b`
val f = Term`f:'a->'b`
val tm1 = Term`!x. ?y. ^P x y`
val tm2 = Term `?f. !x. ^P x (f x)`
val tm4 = Term`\x. @y. ^P x y`
val tm5 = Term`(\x. @y. ^P x y) x`
val th1 = ASSUME tm1
val th2 = ASSUME tm2
val th3 = SPEC x th1
val th4 = INST_TYPE [alpha |-> beta] SELECT_AX
val th5 = SPEC y (SPEC (Term`\y. ^P x y`) th4)
val th6 = BETA_CONV (fst(dest_imp(concl th5)))
val th7 = BETA_CONV (snd(dest_imp(concl th5)))
val th8 = MK_COMB (MK_COMB (REFL (Term`$==>`),th6),th7)
val th9 = EQ_MP th8 th5
val th10 = MP th9 (ASSUME(fst(dest_imp(concl th9))))
val th11 = CHOOSE (y,th3) th10
val th12 = SYM (BETA_CONV tm5)
val th13 = SUBST [Term`v:'b` |-> th12] (Term`^P x v`) th11
val th14 = DISCH tm1 (EXISTS (tm2,tm4) (GEN x th13))
val th15 = ASSUME (Term`!x. ^P x (f x)`)
val th16 = SPEC x th15
val th17 = GEN x (EXISTS(Term`?y. ^P x y`,Term`f (x:'a):'b`) th16)
val th18 = DISCH tm2 (CHOOSE (f,th2) th17)
val th19 = MP (MP (SPEC tm1 (SPEC tm2 IMP_ANTISYM_AX)) th18) th14
in
GEN P (SYM th19)
end);
Konrad.
On Tue, Apr 24, 2012 at 1:26 AM, Ramana Kumar <[email protected]> wrote:
> You might want to consider implementing import/export of OpenTheory proofs
> (http://www.gilith.com/research/opentheory/) to get access to some larger
> existing proofs. It would be interesting to see how they would look in the
> web interface.
>
> On Mon, Apr 23, 2012 at 3:32 AM, Cris Perdue <[email protected]> wrote:
>>
>> I would like to announce the Prooftoys visual proof assistant, a work in
>> progress, and invite experimental use of it, available at
>> http://prooftoys.org/.
>>
>> The Prooftoys logic is very close to Peter Andrews' Q0, including
>> essentially the same axioms and the same single fundamental rule of
>> inference, Rule R, which allows replacement of a term by an equal term. The
>> implementation builds up numerous derived rules of inference, which are
>> available in the same way as theorems and the primitive rule of inference
>> through the web-based user interface.
>>
>> Prooftoys and its user interface normally run entirely within the user's
>> web browser for interactivity and immediate access. It includes an
>> interactive proof editor, with ability to save and restore proofs to textual
>> format. It supports inference in the style of natural deduction, using
>> hypotheses.
>>
>> The system aims to make higher-order logic more accessible conceptually
>> and easier to use as a tool, bringing more people to understand and use it.
>>
>> The implementation is very much a work in progress in all dimensions, but
>> has been working well for experimental interactive use. It has a set of
>> axioms for real numbers and some rather primitive derived rules of inference
>> so it is possible to experiment with real numbers.
>>
>> More information is available on the Prooftoys web site.
>>
>> Best regards,
>> Cris Perdue
>>
>>
>>
>> ------------------------------------------------------------------------------
>> For Developers, A Lot Can Happen In A Second.
>> Boundary is the first to Know...and Tell You.
>> Monitor Your Applications in Ultra-Fine Resolution. Try it FREE!
>> http://p.sf.net/sfu/Boundary-d2dvs2
>>
>> _______________________________________________
>> hol-info mailing list
>> [email protected]
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
