John, thanks for writing the R^2 = Tarski-model code! I could not
have done it. You're the boss, so I'll use your new code. BTW did
you see that I proved your equation responding to Josef?
(x1^2 + x2^2 + x3^2 + x4^2) (y1^2 + y2^2 + y3^2 + y4^2)
= ...
Your other code works quite well, and I ported Bqaa, but I'm stuck on
C1. I assumed you had a typo
loadt "miz3/make.ml";;
and changed it to loadt "miz3/miz3.ml";;
So I paste in 3 commands
hol_light> ocaml
#use "hol.ml";;
#load "unix.cma";;
and then paste in the file below, JohnTarski.ml (I couldn't figure out
how to #use it), and everything compiles, where I got the C1 error
(`;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a b x y : point.
~(a = b) /\ Between (a,b,x) /\ Between (a,b,y) /\ b,x === b,y
==> y = x
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a b x y be point;
assume ~(a = b) [1];
assume Between (a,b,x) [2];
assume Between (a,b,y) [3];
assume b,x === b,y [4];
a,b === a,b /\ a,y === a,y /\ b,y === b,y by 0, EquivReflexive; then
a,b,y cong a,b,y by 0, cong; then
y,x === y,y by 0, 1, 2, 3, 4, A5; thus
y = x by 0, A3;
:: #8 #8#2
:: 8: syntax or type error hol
:: 2: inference time-out
end
;`,
(2, 1, 0)).
It's interesting that the one I couldn't get to work was the one with
your clever cong definition. Maybe it's my version 2.20++ (I asked my
syasadmin to install svn (crazy thing about rpm is (I think) that you
can't install anything without being root), and maybe this is a
complicated inference that Mizar can perform due to better automation.
And maybe I did something really stupid, I could believe that.
------------- JohnTarski.ml -------------
(* ------------------------------------------------------------------------- *)
(* Infix status for a couple of the geometric predicates. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
(* ------------------------------------------------------------------------- *)
(* Constant saying that three predicates satisfy the Tarski axioms. *)
(* ------------------------------------------------------------------------- *)
let TarskiModel = new_definition
`TarskiModel((===),(Between:point#point#point->bool),(cong)) <=>
(!a b. a,b === b,a) /\
(!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s) /\
(!a b c. a,b === c,c ==> a = b) /\
(!a q b c. ?x. Between(q,a,x) /\ a,x === b,c) /\
(!a b c x a' b' c' x'.
~(a = b) /\ a,b,c cong a',b',c' /\
Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x'
==> c,x === c',x') /\
(!a b. Between(a,b,a) ==> a = b) /\
(!a b p q z.
Between(a,p,z) /\ Between(b,q,z)
==> ?x. Between(p,x,b) /\ Between(q,x,a)) /\
(!a b c x y z.
a,b,c cong x,y,z <=>
a,b === x,y /\ a,c === x,z /\ b,c === y,z)`;;
let [A1;A2;A3;A4;A5;A6;A7;cong] =
map DISCH_ALL (CONJUNCTS(UNDISCH(fst(EQ_IMP_RULE(SPEC_ALL TarskiModel)))));;
(* ------------------------------------------------------------------------- *)
(* Now Mizarlight versions of the actual proofs. *)
(* ------------------------------------------------------------------------- *)
loadt "miz3/miz3.ml";;
let EquivReflexive = thm `;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a b. a,b === a,b
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a b be point;
b,a === a,b by 0,A1;
thus a,b === a,b by 0,A2;
end`;;
let EquivSymmetric = thm `;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a b c d. a,b === c,d ==> c,d === a,b
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a b c d be point;
assume a,b === c,d [1];
a,b === a,b by 0,EquivReflexive;
thus c,d === a,b by 0, 1, A2;
end`;;
let EquivTransitive = thm `;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a b p q r s : point. a,b === p,q /\ p,q === r,s ==> a,b === r,s
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a b p q r s be point;
assume a,b === p,q [1];
assume p,q === r,s [2];
p,q === a,b by 0, 1, EquivSymmetric;
thus a,b === r,s by 0, 2, A2;
end`;;
let Baaa_THM = thm `;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a b. Between (a,a,a) /\ a,a === b,b
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a b be point;
?x. Between (a,a,x) /\ a,x === b,b by 0,A4;
consider x such that Between (a,a,x) /\ a,x === b,b [1];
a = x by 0,1, A3;
thus Between (a,a,a) /\ a,a === b,b by 0,1;
end`;;
let Bqaa_THM = thm `;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a q. Between (q,a,a)
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a q be point;
?x. Between (q,a,x) /\ a,x === a,a by 0,A4;
consider x such that Between (q,a,x) /\ a,x === a,a [1];
a = x by 0,1, A3;
thus Between (q,a,a) by 0,1;
end`;;
let C1_THM = thm `;
!(===) (Between:point#point#point->bool) (cong).
TarskiModel((===),(Between:point#point#point->bool),(cong))
==> !a b x y : point.
~(a = b) /\ Between (a,b,x) /\ Between (a,b,y) /\ b,x === b,y
==> y = x
proof
let (===) be point#point->point#point->bool;
let (Between) be point#point#point->bool;
let (cong) be point#point#point->point#point#point->bool;
assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0];
let a b x y be point;
assume ~(a = b) [1];
assume Between (a,b,x) [2];
assume Between (a,b,y) [3];
assume b,x === b,y [4];
a,b === a,b /\ a,y === a,y /\ b,y === b,y by 0, EquivReflexive; then
a,b,y cong a,b,y by 0, cong; then
y,x === y,y by 0, 1, 2, 3, 4, A5; thus
y = x by 0, A3;
end`;;
------------------------------------------------------------------------------
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
