26408

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


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 
*)


5 

60770

6 
section \<open>FirstOrder Logic: propositional examples\<close>

26408

7 


8 
theory Propositional_Int


9 
imports IFOLP


10 
begin


11 


12 


13 
text "commutative laws of & and  "

61337

14 
schematic_goal "?p : P & Q > Q & P"

60770

15 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

16 

61337

17 
schematic_goal "?p : P  Q > Q  P"

60770

18 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

19 


20 


21 
text "associative laws of & and  "

61337

22 
schematic_goal "?p : (P & Q) & R > P & (Q & R)"

60770

23 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

24 

61337

25 
schematic_goal "?p : (P  Q)  R > P  (Q  R)"

60770

26 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

27 


28 


29 
text "distributive laws of & and  "

61337

30 
schematic_goal "?p : (P & Q)  R > (P  R) & (Q  R)"

60770

31 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

32 

61337

33 
schematic_goal "?p : (P  R) & (Q  R) > (P & Q)  R"

60770

34 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

35 

61337

36 
schematic_goal "?p : (P  Q) & R > (P & R)  (Q & R)"

60770

37 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

38 


39 

61337

40 
schematic_goal "?p : (P & R)  (Q & R) > (P  Q) & R"

60770

41 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

42 


43 


44 
text "Laws involving implication"


45 

61337

46 
schematic_goal "?p : (P>R) & (Q>R) <> (PQ > R)"

60770

47 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

48 

61337

49 
schematic_goal "?p : (P & Q > R) <> (P> (Q>R))"

60770

50 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

51 

61337

52 
schematic_goal "?p : ((P>R)>R) > ((Q>R)>R) > (P&Q>R) > R"

60770

53 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

54 

61337

55 
schematic_goal "?p : ~(P>R) > ~(Q>R) > ~(P&Q>R)"

60770

56 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

57 

61337

58 
schematic_goal "?p : (P > Q & R) <> (P>Q) & (P>R)"

60770

59 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

60 


61 


62 
text "Propositionsastypes"


63 


64 
(*The combinator K*)

61337

65 
schematic_goal "?p : P > (Q > P)"

60770

66 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

67 


68 
(*The combinator S*)

61337

69 
schematic_goal "?p : (P>Q>R) > (P>Q) > (P>R)"

60770

70 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

71 


72 


73 
(*Converse is classical*)

61337

74 
schematic_goal "?p : (P>Q)  (P>R) > (P > Q  R)"

60770

75 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

76 

61337

77 
schematic_goal "?p : (P>Q) > (~Q > ~P)"

60770

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

26408

79 


80 


81 
text "Schwichtenberg's examples (via T. Nipkow)"


82 

61337

83 
schematic_goal stab_imp: "?p : (((Q>R)>R)>Q) > (((P>Q)>R)>R)>P>Q"

60770

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

26408

85 

61337

86 
schematic_goal stab_to_peirce: "?p : (((P > R) > R) > P) > (((Q > R) > R) > Q)

26408

87 
> ((P > Q) > P) > P"

60770

88 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

89 

61337

90 
schematic_goal peirce_imp1: "?p : (((Q > R) > Q) > Q)

26408

91 
> (((P > Q) > R) > P > Q) > P > Q"

60770

92 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

93 

61337

94 
schematic_goal peirce_imp2: "?p : (((P > R) > P) > P) > ((P > Q > R) > P) > P"

60770

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

26408

96 

61337

97 
schematic_goal mints: "?p : ((((P > Q) > P) > P) > Q) > Q"

60770

98 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

99 

61337

100 
schematic_goal mints_solovev: "?p : (P > (Q > R) > Q) > ((P > Q) > R) > R"

60770

101 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

102 

61337

103 
schematic_goal tatsuta: "?p : (((P7 > P1) > P10) > P4 > P5)

26408

104 
> (((P8 > P2) > P9) > P3 > P10)


105 
> (P1 > P8) > P6 > P7


106 
> (((P3 > P2) > P9) > P4)


107 
> (P1 > P3) > (((P6 > P1) > P2) > P9) > P5"

60770

108 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

109 

61337

110 
schematic_goal tatsuta1: "?p : (((P8 > P2) > P9) > P3 > P10)

26408

111 
> (((P3 > P2) > P9) > P4)


112 
> (((P6 > P1) > P2) > P9)


113 
> (((P7 > P1) > P10) > P4 > P5)


114 
> (P1 > P3) > (P1 > P8) > P6 > P7 > P5"

60770

115 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)

26408

116 


117 
end
