On Fri, Aug 3, 2012 at 4:43 AM, Bill Richter
<rich...@math.northwestern.edu>wrote:
> Define a four-argument predicate
> Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds
> /\
> ...
> and use that as a hypothesis on all your theorems.
>
> Thanks, Ramana! The code below indicates that I can get rid of new_axiom
> following your suggestion. I should have seen this myself before, but I
> was bogged down in the set theory which I still don't know how to pull off,
> so I didn't even try. So thanks!
>
> I kept the new_type stuff, and made TarskiModel a 0-argument predicate,
> and proved the first 4 theorems of my Tarski axiomatic geometry
> http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
>
> EquivReflexive : thm = |- TarskiModel ==> (!a b. a,b === a,b)
> EquivSymmetric : thm =
> |- TarskiModel ==> (!a b c d. a,b === c,d ==> c,d === a,b)
> EquivTransitive : thm =
> |- TarskiModel
> ==> (!a b p q r s. a,b === p,q ==> p,q === r,s ==> a,b === r,s)
> Baaa_THM : thm =
> |- TarskiModel ==> (!a b. Between (a,a,a) /\ a,a === b,b)
>
> I'm not too happy about the extra clutter caused by the statement
> TarskiModel, the label TM I use to refer to it, and turning the axioms into
> theorems. But that's great that I can get rid of new_axiom at least, so
> thanks.
>
If HOL Light has record datatypes (not sure if it does), you can at least
hide all the arguments to TarskiModel inside a record. And put an overload
of TM for TarskiModel so you don't have to type/read the long name
everywhere. (Come to think of it, overloads may also not be available in
HOL Light...)
In HOL4 you could use both features I mention above.
In Isabelle, you could do the whole thing much more cleanly using what is
known as a "locale", where you fix some constants like ===, Between, H,
etc. and state some properties (the axioms) you want to hold of them in
this context, and then do your formalisation without the clutter, and at
the end it gives you the effect of having used the extra hypothesis on
every theorem.
(All these features could exist in all the theorem provers; they just
happen not to.)
Finally, if you go back to your old new_axiom way in HOL Light for
convenience, it may be possible to simulate locales by using OpenTheory
theory packages. But I can't really recommend that yet because the idea is
completely untested.
>
> I don't know how to get rid of new_type using H and your 4-arg predicate.
> I tried this, and I got the error message
> # Exception: Failure "term after binary operator expected":
>
> parse_as_infix("===",(12, "right"));;
> let A1_DEF = new_definition
> `A1axiom T === <=> !a b. T a /\ T b ==> a,b === b,a`;;
>
> I can appreciate this error message. I want to say that T is a set and a
> belongs to T (or T a = True, or T a), but I don't see how I can do that
> without some typing. What do I even want the type of a, b & T to be here?
>
> This seems to be a question of how to implement sets in HOL Light.
>
> --
> Best,
> Bill
>
> horizon := 0;;
> #load "unix.cma";;
> loadt "miz3/miz3.ml";;
>
> new_type("point",0);;
> new_constant("===",`:point#point->point#point->bool`);;
> new_constant("Between",`:point#point#point->bool`);;
>
> parse_as_infix("===",(12, "right"));;
>
> let A1_DEF = new_definition
> `A1axiom <=> !a b. a,b === b,a`;;
>
> let A2_DEF = new_definition
> `A2axiom <=> !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q ===
> r,s`;;
>
> let A3_DEF = new_definition
> `A3axiom <=> !a b c. a,b === c,c ==> a = b`;;
>
> let A4_DEF = new_definition
> `A4axiom <=> !a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;
>
> let TarskiModel_DEF = new_definition
> `TarskiModel <=> A1axiom /\ A2axiom /\ A3axiom /\ A4axiom`;;
>
> let A1 = thm `;
> TarskiModel ==> !a b. a,b === b,a
> by TarskiModel_DEF, A1_DEF`;;
>
> let A2 = thm `;
> TarskiModel ==> !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q ===
> r,s
> by TarskiModel_DEF, A2_DEF`;;
>
> let A3 = thm `;
> TarskiModel ==> !a b c. a,b === c,c ==> a = b
> by TarskiModel_DEF, A3_DEF`;;
>
> let A4 = thm `;
> TarskiModel ==> !a q b c. ?x. Between(q,a,x) /\ a,x === b,c
> by TarskiModel_DEF, A4_DEF`;;
>
>
> let EquivReflexive = thm `;
> TarskiModel ==> !a b. a,b === a,b
>
> proof
> assume TarskiModel [TM];
> let a b be point;
> b,a === a,b by A1, TM;
> qed by -, A2, TM`;;
>
>
> let EquivSymmetric = thm `;
> assume TarskiModel [TM];
> let a b c d be point;
> assume a,b === c,d [1];
> thus c,d === a,b
>
> proof
> a,b === a,b by EquivReflexive, TM;
> qed by -, 1, A2, TM`;;
>
>
> let EquivTransitive = thm `;
> assume TarskiModel [TM];
> let a b p q r s be point;
> assume a,b === p,q [H1];
> assume p,q === r,s [H2];
> thus a,b === r,s
>
> proof
> p,q === a,b by H1, EquivSymmetric, TM;
> qed by -, H2, A2, TM`;;
>
>
> let Baaa_THM = thm `;
> assume TarskiModel [TM];
> let a b be point;
> thus Between (a,a,a) /\ a,a === b,b
>
> proof
> consider x such that
> Between (a,a,x) /\ a,x === b,b [X1] by A4, TM;
> a = x by -, A3, TM;
> qed by -, X1`;;
>
>
>
>
>
>
>
>
> ------------------------------------------------------------------------------
> 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
> hol-info@lists.sourceforge.net
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
