25991

1 
(* Title: FOLP/ex/Intro.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Derives some inference rules, illustrating the use of definitions.


7 
*)


8 


9 
header {* Examples for the manual ``Introduction to Isabelle'' *}


10 


11 
theory Intro


12 
imports FOLP


13 
begin


14 


15 
subsubsection {* Some simple backward proofs *}


16 


17 
lemma mythm: "?p : PP > P"


18 
apply (rule impI)


19 
apply (rule disjE)


20 
prefer 3 apply (assumption)


21 
prefer 2 apply (assumption)


22 
apply assumption


23 
done


24 


25 
lemma "?p : (P & Q)  R > (P  R)"


26 
apply (rule impI)


27 
apply (erule disjE)


28 
apply (drule conjunct1)


29 
apply (rule disjI1)


30 
apply (rule_tac [2] disjI2)


31 
apply assumption+


32 
done


33 


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


35 
lemma "?p : (ALL x y. P(x,y)) > (ALL z w. P(w,z))"


36 
apply (rule impI)


37 
apply (rule allI)


38 
apply (rule allI)


39 
apply (drule spec)


40 
apply (drule spec)


41 
apply assumption


42 
done


43 


44 


45 
subsubsection {* Demonstration of @{text "fast"} *}


46 


47 
lemma "?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 
apply (tactic {* fast_tac FOLP_cs 1 *})


50 
done


51 


52 


53 
lemma "?p : ALL x. P(x,f(x)) <>


54 
(EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"


55 
apply (tactic {* fast_tac FOLP_cs 1 *})


56 
done


57 


58 


59 
subsubsection {* Derivation of conjunction elimination rule *}


60 


61 
lemma


62 
assumes major: "p : P&Q"


63 
and minor: "!!x y. [ x : P; y : Q ] ==> f(x, y) : R"


64 
shows "?p : R"


65 
apply (rule minor)


66 
apply (rule major [THEN conjunct1])


67 
apply (rule major [THEN conjunct2])


68 
done


69 


70 


71 
subsection {* Derived rules involving definitions *}


72 


73 
text {* Derivation of negation introduction *}


74 


75 
lemma


76 
assumes "!!x. x : P ==> f(x) : False"


77 
shows "?p : ~ P"


78 
apply (unfold not_def)


79 
apply (rule impI)


80 
apply (rule prems)


81 
apply assumption


82 
done


83 


84 
lemma


85 
assumes major: "p : ~P"


86 
and minor: "q : P"


87 
shows "?p : R"


88 
apply (rule FalseE)


89 
apply (rule mp)


90 
apply (rule major [unfolded not_def])


91 
apply (rule minor)


92 
done


93 


94 
text {* Alternative proof of the result above *}


95 
lemma


96 
assumes major: "p : ~P"


97 
and minor: "q : P"


98 
shows "?p : R"


99 
apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])


100 
done


101 


102 
end
