0

1 
(* Title: FOL/ex/foundn


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover


7 
*)


8 


9 
writeln"File FOL/ex/foundn.";


10 


11 
goal IFOLP.thy "?p : A&B > (C>A&C)";


12 
by (resolve_tac [impI] 1);


13 
by (resolve_tac [impI] 1);


14 
by (resolve_tac [conjI] 1);


15 
by (assume_tac 2);


16 
by (resolve_tac [conjunct1] 1);


17 
by (assume_tac 1);


18 
result();


19 


20 
(*A form of conjelimination*)


21 
val prems =


22 
goal IFOLP.thy "p : A&B ==> (!!x y.[ x:A; y:B ] ==> f(x,y):C) ==> ?p:C";


23 
by (resolve_tac prems 1);


24 
by (resolve_tac [conjunct1] 1);


25 
by (resolve_tac prems 1);


26 
by (resolve_tac [conjunct2] 1);


27 
by (resolve_tac prems 1);


28 
result();


29 


30 


31 
val prems =


32 
goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B  ~B";


33 
by (resolve_tac prems 1);


34 
by (resolve_tac [notI] 1);


35 
by (res_inst_tac [ ("P", "~B") ] notE 1);


36 
by (resolve_tac [notI] 2);


37 
by (res_inst_tac [ ("P", "B  ~B") ] notE 2);


38 
by (assume_tac 2);


39 
by (resolve_tac [disjI1] 2);


40 
by (assume_tac 2);


41 
by (resolve_tac [notI] 1);


42 
by (res_inst_tac [ ("P", "B  ~B") ] notE 1);


43 
by (assume_tac 1);


44 
by (resolve_tac [disjI2] 1);


45 
by (assume_tac 1);


46 
result();


47 


48 


49 
val prems =


50 
goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B  ~B";


51 
by (resolve_tac prems 1);


52 
by (resolve_tac [notI] 1);


53 
by (resolve_tac [notE] 1);


54 
by (resolve_tac [notI] 2);


55 
by (eresolve_tac [notE] 2);


56 
by (eresolve_tac [disjI1] 2);


57 
by (resolve_tac [notI] 1);


58 
by (eresolve_tac [notE] 1);


59 
by (eresolve_tac [disjI2] 1);


60 
result();


61 


62 


63 
val prems =


64 
goal IFOLP.thy "[ p:A  ~A; q:~ ~A ] ==> ?p:A";


65 
by (resolve_tac [disjE] 1);


66 
by (resolve_tac prems 1);


67 
by (assume_tac 1);


68 
by (resolve_tac [FalseE] 1);


69 
by (res_inst_tac [ ("P", "~A") ] notE 1);


70 
by (resolve_tac prems 1);


71 
by (assume_tac 1);


72 
result();


73 


74 


75 
writeln"Examples with quantifiers";


76 


77 
val prems =


78 
goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)H(z)";


79 
by (resolve_tac [allI] 1);


80 
by (resolve_tac [disjI1] 1);


81 
by (resolve_tac (prems RL [spec]) 1);


82 
(*can use instead


83 
by (resolve_tac [spec] 1); by (resolve_tac prems 1); *)


84 
result();


85 


86 


87 
goal IFOLP.thy "?p : ALL x. EX y. x=y";


88 
by (resolve_tac [allI] 1);


89 
by (resolve_tac [exI] 1);


90 
by (resolve_tac [refl] 1);


91 
result();


92 


93 


94 
goal IFOLP.thy "?p : EX y. ALL x. x=y";


95 
by (resolve_tac [exI] 1);


96 
by (resolve_tac [allI] 1);


97 
by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";


98 
getgoal 1;


99 


100 


101 
(*Parallel lifting example. *)


102 
goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";


103 
by (resolve_tac [exI, allI] 1);


104 
by (resolve_tac [exI, allI] 1);


105 
by (resolve_tac [exI, allI] 1);


106 
by (resolve_tac [exI, allI] 1);


107 
by (resolve_tac [exI, allI] 1);


108 


109 


110 
val prems =


111 
goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";


112 
by (resolve_tac [conjE] 1);


113 
by (resolve_tac prems 1);


114 
by (resolve_tac [exE] 1);


115 
by (assume_tac 1);


116 
by (resolve_tac [exI] 1);


117 
by (resolve_tac [conjI] 1);


118 
by (assume_tac 1);


119 
by (assume_tac 1);


120 
result();


121 


122 


123 
(*A bigger demonstration of quantifiers  not in the paper*)


124 
goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


125 
by (resolve_tac [impI] 1);


126 
by (resolve_tac [allI] 1);


127 
by (resolve_tac [exE] 1 THEN assume_tac 1);


128 
by (resolve_tac [exI] 1);


129 
by (resolve_tac [allE] 1 THEN assume_tac 1);


130 
by (assume_tac 1);


131 
result();


132 


133 


134 
writeln"Reached end of file.";
