Michael, your polymorphism worked! Following your advice, I coded up in miz3,
without new_type or new_axiom, my first 7 Tarski axiomatic geometry theorems of
http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
I'm stuck on the next result because I don't know how to rewrite my definition
parse_as_infix("cong",(12, "right"));;
let cong_DEF = new_definition
`a,b,c cong x,y,z <=>
a,b === x,y /\ a,c === x,z /\ b,c === y,z`;;
My problem, I think, is that cong is now a function of ===, which is now a
variable being passed around. Here's my miz3 code below, which I really
enjoyed writing, as it took quite a bit of fiddling to get right. Let me try
to explain why your polymorphism works on axiom A4, on which HOL-Light/miz3
prints out
val A4 : thm =
|- !(===) Between.
TarskiModel (===) Between
==> (!a q b c. ?x. Between (q,a,x) /\ a,x === b,c)
That says that === is a 2-ary predicate parsed-as-infix defined on ordered
pairs and Between is a predicate defined on ordered triples. Then TarskiModel
is a 2-ary predicate defined on any such === and Between, and the predicate is
true iff !a q b c. ?x. Between (q,a,x) /\ a,x === b,c, i.e. if Tarski's 4th
axiom holds for === and Between. I'm a bit puzzled here because in the
statement of A4, I wrote
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
To me, that means that all 7 arguments of === and Between have the same type,
the unspecified type 'a, but you can't see that in val A4 above. I had the
impression that HOL Light printed out less information in the theorem
statements than I'd put in because of its clever type-inference scheme, but
this looks like taking it too far. Maybe I don't know what 'a means.
--
Best,
Bill
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
parse_as_infix("===",(12, "right"));;
let A1_DEF = new_definition
`A1axiom (===) Between <=> !a b. a,b === b,a`;;
let A2_DEF = new_definition
`A2axiom (===) Between <=> !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q
=== r,s`;;
let A3_DEF = new_definition
`A3axiom (===) Between <=> !a b c. a,b === c,c ==> a = b`;;
let A4_DEF = new_definition
`A4axiom (===) Between <=> !a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;
let TarskiModel_DEF = new_definition
`TarskiModel (===) Between <=>
A1axiom (===) Between /\ A2axiom (===) Between /\ A3axiom (===) Between /\
A4axiom (===) Between`;;
let A1 = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
let a b be 'a;
thus TarskiModel (===) Between ==> a,b === b,a
by TarskiModel_DEF, A1_DEF`;;
let A2 = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
let a b p q r s be 'a;
thus TarskiModel (===) Between ==> a,b === p,q /\ a,b === r,s ==> p,q ===
r,s
by TarskiModel_DEF, A2_DEF`;;
let A3 = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
let a b c be 'a;
thus TarskiModel (===) Between ==> a,b === c,c ==> a = b
by TarskiModel_DEF, A3_DEF`;;
let A4 = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a q b c be 'a;
thus ?x. Between(q,a,x) /\ a,x === b,c
by TM, TarskiModel_DEF, A4_DEF`;;
let EquivReflexive = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus a,b === a,b
proof
b,a === a,b by A1, TM;
qed by -, A2, TM`;;
let EquivSymmetric = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b c d be 'a;
assume a,b === c,d [ab_cd];
thus c,d === a,b
proof
a,b === a,b by EquivReflexive, TM;
qed by -, ab_cd, A2, TM`;;
let EquivTransitive = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b p q r s be 'a;
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 `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus Between (a,a,a) /\ a,a === b,b
proof
consider x such that
Between (a,a,x) /\ a,x === b,b [useA4] by A4, TM;
a = x by -, A3, TM;
qed by -, useA4`;;
let Baaa_THM = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus Between (a,a,a) /\ a,a === b,b
proof
?x. Between(a,a,x) /\ a,x === b,b by A4, TM;
consider x such that
Between (a,a,x) /\ a,x === b,b [useA4] by -;
a = x by -, A3, TM;
qed by -, useA4`;;
let Baaa_THM = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus Between (a,a,a) /\ a,a === b,b
proof
consider x such that
Between (a,a,x) /\ a,x === b,b [useA4] by A4, TM;
a = x by -, A3, TM;
qed by -, useA4`;;
let Bqaa_THM = thm `;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a q be 'a;
thus Between(q,a,a)
proof
consider x such that Between(q,a,x) /\ a,x === a,a [useA4] by A4, TM;
a = x by -, A3, TM;
qed by -, useA4`;;
------------------------------------------------------------------------------
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
