0

1 
(* Title: FOL/ex/intro


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Examples for the manual "Introduction to Isabelle"


7 


8 
Derives some inference rules, illustrating the use of definitions


9 


10 
To generate similar output to manual, execute these commands:


11 
Pretty.setmargin 72; print_depth 0;


12 
*)


13 


14 


15 
(**** Some simple backward proofs ****)


16 


17 
goal FOLP.thy "?p:PP > P";


18 
by (resolve_tac [impI] 1);


19 
by (resolve_tac [disjE] 1);


20 
by (assume_tac 3);


21 
by (assume_tac 2);


22 
by (assume_tac 1);


23 
val mythm = result();


24 


25 
goal FOLP.thy "?p:(P & Q)  R > (P  R)";


26 
by (resolve_tac [impI] 1);


27 
by (eresolve_tac [disjE] 1);


28 
by (dresolve_tac [conjunct1] 1);


29 
by (resolve_tac [disjI1] 1);


30 
by (resolve_tac [disjI2] 2);


31 
by (REPEAT (assume_tac 1));


32 
result();


33 


34 
(*Correct version, delaying use of "spec" until last*)


35 
goal FOLP.thy "?p:(ALL x y.P(x,y)) > (ALL z w.P(w,z))";


36 
by (resolve_tac [impI] 1);


37 
by (resolve_tac [allI] 1);


38 
by (resolve_tac [allI] 1);


39 
by (dresolve_tac [spec] 1);


40 
by (dresolve_tac [spec] 1);


41 
by (assume_tac 1);


42 
result();


43 


44 


45 
(**** Demonstration of fast_tac ****)


46 


47 
goal FOLP.thy "?p:(EX y. ALL x. J(y,x) <> ~J(x,x)) \


48 
\ > ~ (ALL x. EX y. ALL z. J(z,y) <> ~ J(z,x))";


49 
by (fast_tac FOLP_cs 1);


50 
result();


51 


52 
goal FOLP.thy "?p:ALL x. P(x,f(x)) <> \


53 
\ (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))";


54 
by (fast_tac FOLP_cs 1);


55 
result();


56 


57 


58 
(**** Derivation of conjunction elimination rule ****)


59 


60 
val [major,minor] = goal FOLP.thy "[ p:P&Q; !!x y.[ x:P; y:Q ] ==>f(x,y):R ] ==> ?p:R";


61 
by (resolve_tac [minor] 1);


62 
by (resolve_tac [major RS conjunct1] 1);


63 
by (resolve_tac [major RS conjunct2] 1);


64 
prth (topthm());


65 
result();


66 


67 


68 
(**** Derived rules involving definitions ****)


69 


70 
(** Derivation of negation introduction **)


71 


72 
val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";


73 
by (rewrite_goals_tac [not_def]);


74 
by (resolve_tac [impI] 1);


75 
by (resolve_tac prems 1);


76 
by (assume_tac 1);


77 
result();


78 


79 
val [major,minor] = goal FOLP.thy "[ p:~P; q:P ] ==> ?p:R";


80 
by (resolve_tac [FalseE] 1);


81 
by (resolve_tac [mp] 1);


82 
by (resolve_tac [rewrite_rule [not_def] major] 1);


83 
by (resolve_tac [minor] 1);


84 
result();


85 


86 
(*Alternative proof of above result*)


87 
val [major,minor] = goalw FOLP.thy [not_def]


88 
"[ p:~P; q:P ] ==> ?p:R";


89 
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);


90 
result();


91 


92 
writeln"Reached end of file.";
