src/FOLP/ex/Quantifiers_Cla.thy
changeset 58957 c9e744ea8a38
parent 36319 8feb2c4bef1a
child 60770 240563fbf41d
     1.1 --- a/src/FOLP/ex/Quantifiers_Cla.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOLP/ex/Quantifiers_Cla.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -11,91 +11,91 @@
     1.4  begin
     1.5  
     1.6  schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
     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 : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
    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  (*Converse is false*)
    1.16  schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
    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 : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
    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  schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
    1.26 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.27 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.28  
    1.29  
    1.30  text "Some harder ones"
    1.31  
    1.32  schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
    1.33 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.34 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.35  
    1.36  (*Converse is false*)
    1.37  schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
    1.38 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.39 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.40  
    1.41  
    1.42  text "Basic test of quantifier reasoning"
    1.43  (*TRUE*)
    1.44  schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    1.45 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.46 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.47  
    1.48  schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
    1.49 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.50 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.51  
    1.52  
    1.53  text "The following should fail, as they are false!"
    1.54  
    1.55  schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
    1.56 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    1.57 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
    1.58    oops
    1.59  
    1.60  schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
    1.61 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    1.62 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
    1.63    oops
    1.64  
    1.65  schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
    1.66 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    1.67 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
    1.68    oops
    1.69  
    1.70  schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
    1.71 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
    1.72 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
    1.73    oops
    1.74  
    1.75  
    1.76  text "Back to things that are provable..."
    1.77  
    1.78  schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
    1.79 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.80 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.81  
    1.82  
    1.83  (*An example of why exI should be delayed as long as possible*)
    1.84  schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
    1.85 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.86 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.87  
    1.88  schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
    1.89 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    1.90 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    1.91  
    1.92  schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
    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  
    1.97  text "Some slow ones"
    1.98  
    1.99  (*Principia Mathematica *11.53  *)
   1.100  schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
   1.101 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.102 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   1.103  
   1.104  (*Principia Mathematica *11.55  *)
   1.105  schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
   1.106 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   1.107 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   1.108  
   1.109  (*Principia Mathematica *11.61  *)
   1.110  schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
   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  end