26408

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


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
FirstOrder Logic: quantifier examples (intuitionistic and classical)


7 
Needs declarations of the theory "thy" and the tactic "tac"


8 
*)


9 


10 
theory Quantifiers_Cla


11 
imports FOLP


12 
begin


13 


14 
lemma "?p : (ALL x y. P(x,y)) > (ALL y x. P(x,y))"


15 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


16 


17 
lemma "?p : (EX x y. P(x,y)) > (EX y x. P(x,y))"


18 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


19 


20 


21 
(*Converse is false*)


22 
lemma "?p : (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)  Q(x))"


23 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


24 


25 
lemma "?p : (ALL x. P>Q(x)) <> (P> (ALL x. Q(x)))"


26 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


27 


28 


29 
lemma "?p : (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)"


30 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


31 


32 


33 
text "Some harder ones"


34 


35 
lemma "?p : (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))"


36 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


37 


38 
(*Converse is false*)


39 
lemma "?p : (EX x. P(x)&Q(x)) > (EX x. P(x)) & (EX x. Q(x))"


40 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


41 


42 


43 
text "Basic test of quantifier reasoning"


44 
(*TRUE*)


45 
lemma "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"


46 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


47 


48 
lemma "?p : (ALL x. Q(x)) > (EX x. Q(x))"


49 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


50 


51 


52 
text "The following should fail, as they are false!"


53 


54 
lemma "?p : (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))"


55 
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?


56 
oops


57 


58 
lemma "?p : (EX x. Q(x)) > (ALL x. Q(x))"


59 
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?


60 
oops


61 


62 
lemma "?p : P(?a) > (ALL x. P(x))"


63 
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?


64 
oops


65 


66 
lemma "?p : (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))"


67 
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?


68 
oops


69 


70 


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


72 


73 
lemma "?p : (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))"


74 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


75 


76 


77 
(*An example of why exI should be delayed as long as possible*)


78 
lemma "?p : (P > (EX x. Q(x))) & P > (EX x. Q(x))"


79 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


80 


81 
lemma "?p : (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)"


82 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


83 


84 
lemma "?p : (ALL x. Q(x)) > (EX x. Q(x))"


85 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


86 


87 


88 
text "Some slow ones"


89 


90 
(*Principia Mathematica *11.53 *)


91 
lemma "?p : (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))"


92 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


93 


94 
(*Principia Mathematica *11.55 *)


95 
lemma "?p : (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))"


96 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


97 


98 
(*Principia Mathematica *11.61 *)


99 
lemma "?p : (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))"


100 
by (tactic {* Cla.fast_tac FOLP_cs 1 *})


101 


102 
end
