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