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 

36319

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

25991

17 
apply (rule impI)


18 
apply (rule disjE)


19 
prefer 3 apply (assumption)


20 
prefer 2 apply (assumption)


21 
apply assumption


22 
done


23 

36319

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

25991

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*)

36319

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

25991

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 

36319

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

25991

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 

36319

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

25991

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 

36319

60 
schematic_lemma

25991

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 

36319

74 
schematic_lemma

25991

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 

36319

83 
schematic_lemma

25991

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 *}

36319

94 
schematic_lemma

25991

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
