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.
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
