25991

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


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1992 University of Cambridge


4 


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


6 
*)


7 


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


9 


10 
theory Intro


11 
imports FOLP


12 
begin


13 


14 
subsubsection {* Some simple backward proofs *}


15 


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


17 
apply (rule impI)


18 
apply (rule disjE)


19 
prefer 3 apply (assumption)


20 
prefer 2 apply (assumption)


21 
apply assumption


22 
done


23 


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


25 
apply (rule impI)


26 
apply (erule disjE)


27 
apply (drule conjunct1)


28 
apply (rule disjI1)


29 
apply (rule_tac [2] disjI2)


30 
apply assumption+


31 
done


32 


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


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


35 
apply (rule impI)


36 
apply (rule allI)


37 
apply (rule allI)


38 
apply (drule spec)


39 
apply (drule spec)


40 
apply assumption


41 
done


42 


43 


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


45 


46 
lemma "?p : (EX y. ALL x. J(y,x) <> ~J(x,x))


47 
> ~ (ALL x. EX y. ALL z. J(z,y) <> ~ J(z,x))"


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


49 
done


50 


51 


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


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


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


55 
done


56 


57 


58 
subsubsection {* Derivation of conjunction elimination rule *}


59 


60 
lemma


61 
assumes major: "p : P&Q"


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


63 
shows "?p : R"


64 
apply (rule minor)


65 
apply (rule major [THEN conjunct1])


66 
apply (rule major [THEN conjunct2])


67 
done


68 


69 


70 
subsection {* Derived rules involving definitions *}


71 


72 
text {* Derivation of negation introduction *}


73 


74 
lemma


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


76 
shows "?p : ~ P"


77 
apply (unfold not_def)


78 
apply (rule impI)


79 
apply (rule prems)


80 
apply assumption


81 
done


82 


83 
lemma


84 
assumes major: "p : ~P"


85 
and minor: "q : P"


86 
shows "?p : R"


87 
apply (rule FalseE)


88 
apply (rule mp)


89 
apply (rule major [unfolded not_def])


90 
apply (rule minor)


91 
done


92 


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


94 
lemma


95 
assumes major: "p : ~P"


96 
and minor: "q : P"


97 
shows "?p : R"


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


99 
done


100 


101 
end
