John, I feel my code isn't quite perfect enough to submit my Hilbert
geometry paper. Freek's miz3 code in the miz3 dox 1201.3601-1.pdf
solving the drinker's paradox on p 13--14 is perhaps designed to show
various features of miz3, but it is more than twice as long as needed:
Paste in these 4 commands and then the rest of this message:
hol_light> ocaml
#use "hol.ml";;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
let DRINKER = thm `;
let P be A->bool;
thus ?x. P x ==> !y. P y [22]
proof
(?x. ~P x) \/ ~(?x. ~P x) [1];
cases by 1;
suppose ?x. ~P x [2];
consider x such that ~P x [3] by 2;
take x;
assume P x [4];
F [5] by 3,4;
thus !y. P y [6] by 5;
end;
suppose ~(?x. ~P x) [10];
consider a being A such that T;
take a;
assume P a [11];
let y be A;
P y \/ ~P y [12];
cases by 12;
suppose P y [13];
thus P y by 13;
end;
suppose ~P y [14];
?x. ~P x [15] by 14;
F [16] by 10,15;
thus P y [17] by 16;
end;
end;
end`;;
(* Few of the above labels are needed. Here's a much shorter version. *)
horizon := 0;;
let DRINKER = thm `;
let P be A->bool;
thus ?x. P x ==> !y. P y
proof
(?x. ~P x) \/ ~(?x. ~P x);
cases by -;
suppose ?x. ~P x;
consider x such that ~P x by -;
P x ==> !y. P y by -;
qed by -;
suppose ~(?x. ~P x);
!y. P y by -;
qed by -;
end`;;
(* We can save one line by understanding that ~(!x. P x) <=> !y. P y: *)
let DRINKER = thm `;
let P be A->bool;
thus ?x. P x ==> !y. P y
proof
(!x. P x) \/ ~(!x. P x);
cases by -;
suppose (!x. P x);
qed by -;
suppose ~(!x. P x);
consider x such that ~P x by -;
P x ==> !y. P y by -;
qed by -;
end`;;
(* So I still don't know of an example where `take' is necessary. *)
--
Best,
Bill
------------------------------------------------------------------------------
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
