src/FOLP/ex/Propositional_Cla.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 58889 5b7a9633cfa8
     1.1 --- a/src/FOLP/ex/Propositional_Cla.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/FOLP/ex/Propositional_Cla.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -11,103 +11,103 @@
     1.4  
     1.5  
     1.6  text "commutative laws of & and | "
     1.7 -lemma "?p : P & Q  -->  Q & P"
     1.8 +schematic_lemma "?p : P & Q  -->  Q & P"
     1.9    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.10  
    1.11 -lemma "?p : P | Q  -->  Q | P"
    1.12 +schematic_lemma "?p : P | Q  -->  Q | P"
    1.13    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.14  
    1.15  
    1.16  text "associative laws of & and | "
    1.17 -lemma "?p : (P & Q) & R  -->  P & (Q & R)"
    1.18 +schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
    1.19    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.20  
    1.21 -lemma "?p : (P | Q) | R  -->  P | (Q | R)"
    1.22 +schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
    1.23    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.24  
    1.25  
    1.26  text "distributive laws of & and | "
    1.27 -lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
    1.28 +schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
    1.29    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.30  
    1.31 -lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
    1.32 +schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
    1.33    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.34  
    1.35 -lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
    1.36 +schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
    1.37    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.38  
    1.39  
    1.40 -lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
    1.41 +schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
    1.42    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.43  
    1.44  
    1.45  text "Laws involving implication"
    1.46  
    1.47 -lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
    1.48 +schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
    1.49    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.50  
    1.51 -lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
    1.52 +schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
    1.53    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.54  
    1.55 -lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
    1.56 +schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
    1.57    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.58  
    1.59 -lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
    1.60 +schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
    1.61    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.62  
    1.63 -lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
    1.64 +schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
    1.65    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.66  
    1.67  
    1.68  text "Propositions-as-types"
    1.69  
    1.70  (*The combinator K*)
    1.71 -lemma "?p : P --> (Q --> P)"
    1.72 +schematic_lemma "?p : P --> (Q --> P)"
    1.73    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.74  
    1.75  (*The combinator S*)
    1.76 -lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
    1.77 +schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
    1.78    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.79  
    1.80  
    1.81  (*Converse is classical*)
    1.82 -lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
    1.83 +schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
    1.84    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.85  
    1.86 -lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
    1.87 +schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
    1.88    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.89  
    1.90  
    1.91  text "Schwichtenberg's examples (via T. Nipkow)"
    1.92  
    1.93 -lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
    1.94 +schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
    1.95    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.96  
    1.97 -lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
    1.98 +schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
    1.99                --> ((P --> Q) --> P) --> P"
   1.100    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.101  
   1.102 -lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
   1.103 +schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
   1.104                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
   1.105    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.106    
   1.107 -lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
   1.108 +schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
   1.109    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.110  
   1.111 -lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
   1.112 +schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
   1.113    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.114  
   1.115 -lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
   1.116 +schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
   1.117    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.118  
   1.119 -lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
   1.120 +schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
   1.121            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
   1.122            --> (P1 --> P8) --> P6 --> P7  
   1.123            --> (((P3 --> P2) --> P9) --> P4)  
   1.124            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
   1.125    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.126  
   1.127 -lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
   1.128 +schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
   1.129       --> (((P3 --> P2) --> P9) --> P4)  
   1.130       --> (((P6 --> P1) --> P2) --> P9)  
   1.131       --> (((P7 --> P1) --> P10) --> P4 --> P5)