35762

1 
(* Title: LK/Quantifiers.thy

21426

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1992 University of Cambridge


4 


5 
Classical sequent calculus: examples with quantifiers.


6 
*)


7 


8 
theory Quantifiers


9 
imports LK


10 
begin


11 


12 
lemma " (ALL x. P) <> P"


13 
by fast


14 


15 
lemma " (ALL x y. P(x,y)) <> (ALL y x. P(x,y))"


16 
by fast


17 


18 
lemma "ALL u. P(u), ALL v. Q(v)  ALL u v. P(u) & Q(v)"


19 
by fast


20 


21 


22 
text "Permutation of existential quantifier."


23 


24 
lemma " (EX x y. P(x,y)) <> (EX y x. P(x,y))"


25 
by fast


26 


27 
lemma " (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))"


28 
by fast


29 


30 
(*Converse is invalid*)


31 
lemma " (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)Q(x))"


32 
by fast


33 


34 


35 
text "Pushing ALL into an implication."


36 


37 
lemma " (ALL x. P > Q(x)) <> (P > (ALL x. Q(x)))"


38 
by fast


39 


40 
lemma " (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)"


41 
by fast


42 


43 
lemma " (EX x. P) <> P"


44 
by fast


45 


46 


47 
text "Distribution of EX over disjunction."


48 


49 
lemma " (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))"


50 
by fast


51 


52 
(*Converse is invalid*)


53 
lemma " (EX x. P(x) & Q(x)) > (EX x. P(x)) & (EX x. Q(x))"


54 
by fast


55 


56 


57 
text "Harder examples: classical theorems."


58 


59 
lemma " (EX x. P>Q(x)) <> (P > (EX x. Q(x)))"


60 
by fast


61 


62 
lemma " (EX x. P(x)>Q) <> (ALL x. P(x)) > Q"


63 
by fast


64 


65 
lemma " (ALL x. P(x))  Q <> (ALL x. P(x)  Q)"


66 
by fast


67 


68 


69 
text "Basic test of quantifier reasoning"


70 


71 
lemma " (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"


72 
by fast


73 


74 
lemma " (ALL x. Q(x)) > (EX x. Q(x))"


75 
by fast


76 


77 


78 
text "The following are invalid!"


79 


80 
(*INVALID*)


81 
lemma " (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))"


82 
apply fast?


83 
apply (rule _)


84 
oops


85 


86 
(*INVALID*)


87 
lemma " (EX x. Q(x)) > (ALL x. Q(x))"


88 
apply fast?


89 
apply (rule _)


90 
oops


91 


92 
(*INVALID*)

36319

93 
schematic_lemma " P(?a) > (ALL x. P(x))"

21426

94 
apply fast?


95 
apply (rule _)


96 
oops


97 


98 
(*INVALID*)

36319

99 
schematic_lemma " (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))"

21426

100 
apply fast?


101 
apply (rule _)


102 
oops


103 


104 


105 
text "Back to things that are provable..."


106 


107 
lemma " (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))"


108 
by fast


109 


110 
(*An example of why exR should be delayed as long as possible*)


111 
lemma " (P> (EX x. Q(x))) & P> (EX x. Q(x))"


112 
by fast


113 


114 


115 
text "Solving for a Var"


116 

36319

117 
schematic_lemma " (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)"

21426

118 
by fast


119 


120 


121 
text "Principia Mathematica *11.53"


122 


123 
lemma " (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))"


124 
by fast


125 


126 


127 
text "Principia Mathematica *11.55"


128 


129 
lemma " (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))"


130 
by fast


131 


132 


133 
text "Principia Mathematica *11.61"


134 


135 
lemma " (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))"


136 
by fast


137 


138 


139 
(*21 August 88: loaded in 45.7 secs*)


140 
(*18 September 2005: loaded in 0.114 secs*)


141 


142 
end
