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