26408

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


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 


5 
FirstOrder Logic: quantifier examples (intuitionistic and classical)

35762

6 
Needs declarations of the theory "thy" and the tactic "tac".

26408

7 
*)


8 


9 
theory Quantifiers_Cla


10 
imports FOLP


11 
begin


12 

61337

13 
schematic_goal "?p : (ALL x y. P(x,y)) > (ALL y x. P(x,y))"

60770

14 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

15 

61337

16 
schematic_goal "?p : (EX x y. P(x,y)) > (EX y x. P(x,y))"

60770

17 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

18 


19 


20 
(*Converse is false*)

61337

21 
schematic_goal "?p : (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)  Q(x))"

60770

22 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

23 

61337

24 
schematic_goal "?p : (ALL x. P>Q(x)) <> (P> (ALL x. Q(x)))"

60770

25 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

26 


27 

61337

28 
schematic_goal "?p : (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)"

60770

29 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

30 


31 


32 
text "Some harder ones"


33 

61337

34 
schematic_goal "?p : (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))"

60770

35 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

36 


37 
(*Converse is false*)

61337

38 
schematic_goal "?p : (EX x. P(x)&Q(x)) > (EX x. P(x)) & (EX x. Q(x))"

60770

39 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

40 


41 


42 
text "Basic test of quantifier reasoning"


43 
(*TRUE*)

61337

44 
schematic_goal "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"

60770

45 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

46 

61337

47 
schematic_goal "?p : (ALL x. Q(x)) > (EX x. Q(x))"

60770

48 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

49 


50 


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


52 

61337

53 
schematic_goal "?p : (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))"

60770

54 
apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?

26408

55 
oops


56 

61337

57 
schematic_goal "?p : (EX x. Q(x)) > (ALL x. Q(x))"

60770

58 
apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?

26408

59 
oops


60 

61337

61 
schematic_goal "?p : P(?a) > (ALL x. P(x))"

60770

62 
apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?

26408

63 
oops


64 

61337

65 
schematic_goal "?p : (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))"

60770

66 
apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?

26408

67 
oops


68 


69 


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


71 

61337

72 
schematic_goal "?p : (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))"

60770

73 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

74 


75 


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

61337

77 
schematic_goal "?p : (P > (EX x. Q(x))) & P > (EX x. Q(x))"

60770

78 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

79 

61337

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

60770

81 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

82 

61337

83 
schematic_goal "?p : (ALL x. Q(x)) > (EX x. Q(x))"

60770

84 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

85 


86 


87 
text "Some slow ones"


88 


89 
(*Principia Mathematica *11.53 *)

61337

90 
schematic_goal "?p : (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))"

60770

91 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

92 


93 
(*Principia Mathematica *11.55 *)

61337

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

60770

95 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

96 


97 
(*Principia Mathematica *11.61 *)

61337

98 
schematic_goal "?p : (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))"

60770

99 
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)

26408

100 


101 
end
