26408

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


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 
*)


5 


6 
header {* FirstOrder Logic: propositional examples *}


7 


8 
theory Propositional_Cla


9 
imports FOLP


10 
begin


11 


12 


13 
text "commutative laws of & and  "

36319

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

26408

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


16 

36319

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

26408

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


19 


20 


21 
text "associative laws of & and  "

36319

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

26408

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


24 

36319

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

26408

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


27 


28 


29 
text "distributive laws of & and  "

36319

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

26408

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


32 

36319

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

26408

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


35 

36319

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

26408

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


38 


39 

36319

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

26408

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


42 


43 


44 
text "Laws involving implication"


45 

36319

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

26408

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


48 

36319

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

26408

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


51 

36319

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

26408

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


54 

36319

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

26408

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


57 

36319

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

26408

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


60 


61 


62 
text "Propositionsastypes"


63 


64 
(*The combinator K*)

36319

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

26408

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


67 


68 
(*The combinator S*)

36319

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

26408

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


71 


72 


73 
(*Converse is classical*)

36319

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

26408

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


76 

36319

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

26408

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


79 


80 


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


82 

36319

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

26408

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


85 

36319

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

26408

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


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


89 

36319

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

26408

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


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


93 

36319

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

26408

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


96 

36319

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

26408

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


99 

36319

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

26408

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


102 

36319

103 
schematic_lemma 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"


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


109 

36319

110 
schematic_lemma 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"


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


116 


117 
end
