26408

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


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
header {* FirstOrder Logic: propositional examples *}


8 


9 
theory Propositional_Int


10 
imports IFOLP


11 
begin


12 


13 


14 
text "commutative laws of & and  "


15 
lemma "?p : P & Q > Q & P"


16 
by (tactic {* IntPr.fast_tac 1 *})


17 


18 
lemma "?p : P  Q > Q  P"


19 
by (tactic {* IntPr.fast_tac 1 *})


20 


21 


22 
text "associative laws of & and  "


23 
lemma "?p : (P & Q) & R > P & (Q & R)"


24 
by (tactic {* IntPr.fast_tac 1 *})


25 


26 
lemma "?p : (P  Q)  R > P  (Q  R)"


27 
by (tactic {* IntPr.fast_tac 1 *})


28 


29 


30 
text "distributive laws of & and  "


31 
lemma "?p : (P & Q)  R > (P  R) & (Q  R)"


32 
by (tactic {* IntPr.fast_tac 1 *})


33 


34 
lemma "?p : (P  R) & (Q  R) > (P & Q)  R"


35 
by (tactic {* IntPr.fast_tac 1 *})


36 


37 
lemma "?p : (P  Q) & R > (P & R)  (Q & R)"


38 
by (tactic {* IntPr.fast_tac 1 *})


39 


40 


41 
lemma "?p : (P & R)  (Q & R) > (P  Q) & R"


42 
by (tactic {* IntPr.fast_tac 1 *})


43 


44 


45 
text "Laws involving implication"


46 


47 
lemma "?p : (P>R) & (Q>R) <> (PQ > R)"


48 
by (tactic {* IntPr.fast_tac 1 *})


49 


50 
lemma "?p : (P & Q > R) <> (P> (Q>R))"


51 
by (tactic {* IntPr.fast_tac 1 *})


52 


53 
lemma "?p : ((P>R)>R) > ((Q>R)>R) > (P&Q>R) > R"


54 
by (tactic {* IntPr.fast_tac 1 *})


55 


56 
lemma "?p : ~(P>R) > ~(Q>R) > ~(P&Q>R)"


57 
by (tactic {* IntPr.fast_tac 1 *})


58 


59 
lemma "?p : (P > Q & R) <> (P>Q) & (P>R)"


60 
by (tactic {* IntPr.fast_tac 1 *})


61 


62 


63 
text "Propositionsastypes"


64 


65 
(*The combinator K*)


66 
lemma "?p : P > (Q > P)"


67 
by (tactic {* IntPr.fast_tac 1 *})


68 


69 
(*The combinator S*)


70 
lemma "?p : (P>Q>R) > (P>Q) > (P>R)"


71 
by (tactic {* IntPr.fast_tac 1 *})


72 


73 


74 
(*Converse is classical*)


75 
lemma "?p : (P>Q)  (P>R) > (P > Q  R)"


76 
by (tactic {* IntPr.fast_tac 1 *})


77 


78 
lemma "?p : (P>Q) > (~Q > ~P)"


79 
by (tactic {* IntPr.fast_tac 1 *})


80 


81 


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


83 


84 
lemma stab_imp: "?p : (((Q>R)>R)>Q) > (((P>Q)>R)>R)>P>Q"


85 
by (tactic {* IntPr.fast_tac 1 *})


86 


87 
lemma stab_to_peirce: "?p : (((P > R) > R) > P) > (((Q > R) > R) > Q)


88 
> ((P > Q) > P) > P"


89 
by (tactic {* IntPr.fast_tac 1 *})


90 


91 
lemma peirce_imp1: "?p : (((Q > R) > Q) > Q)


92 
> (((P > Q) > R) > P > Q) > P > Q"


93 
by (tactic {* IntPr.fast_tac 1 *})


94 


95 
lemma peirce_imp2: "?p : (((P > R) > P) > P) > ((P > Q > R) > P) > P"


96 
by (tactic {* IntPr.fast_tac 1 *})


97 


98 
lemma mints: "?p : ((((P > Q) > P) > P) > Q) > Q"


99 
by (tactic {* IntPr.fast_tac 1 *})


100 


101 
lemma mints_solovev: "?p : (P > (Q > R) > Q) > ((P > Q) > R) > R"


102 
by (tactic {* IntPr.fast_tac 1 *})


103 


104 
lemma tatsuta: "?p : (((P7 > P1) > P10) > P4 > P5)


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


106 
> (P1 > P8) > P6 > P7


107 
> (((P3 > P2) > P9) > P4)


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


109 
by (tactic {* IntPr.fast_tac 1 *})


110 


111 
lemma tatsuta1: "?p : (((P8 > P2) > P9) > P3 > P10)


112 
> (((P3 > P2) > P9) > P4)


113 
> (((P6 > P1) > P2) > P9)


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


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


116 
by (tactic {* IntPr.fast_tac 1 *})


117 


118 
end
