src/FOLP/IFOLP.thy
changeset 36319 8feb2c4bef1a
parent 35128 c1ad622e90e4
child 36452 d37c6eed8117
     1.1 --- a/src/FOLP/IFOLP.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -159,7 +159,7 @@
     1.4  
     1.5  (*** Sequent-style elimination rules for & --> and ALL ***)
     1.6  
     1.7 -lemma conjE:
     1.8 +schematic_lemma conjE:
     1.9    assumes "p:P&Q"
    1.10      and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
    1.11    shows "?a:R"
    1.12 @@ -168,7 +168,7 @@
    1.13    apply (rule conjunct2 [OF assms(1)])
    1.14    done
    1.15  
    1.16 -lemma impE:
    1.17 +schematic_lemma impE:
    1.18    assumes "p:P-->Q"
    1.19      and "q:P"
    1.20      and "!!x. x:Q ==> r(x):R"
    1.21 @@ -176,7 +176,7 @@
    1.22    apply (rule assms mp)+
    1.23    done
    1.24  
    1.25 -lemma allE:
    1.26 +schematic_lemma allE:
    1.27    assumes "p:ALL x. P(x)"
    1.28      and "!!y. y:P(x) ==> q(y):R"
    1.29    shows "?p:R"
    1.30 @@ -184,7 +184,7 @@
    1.31    done
    1.32  
    1.33  (*Duplicates the quantifier; for use with eresolve_tac*)
    1.34 -lemma all_dupE:
    1.35 +schematic_lemma all_dupE:
    1.36    assumes "p:ALL x. P(x)"
    1.37      and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
    1.38    shows "?p:R"
    1.39 @@ -194,21 +194,21 @@
    1.40  
    1.41  (*** Negation rules, which translate between ~P and P-->False ***)
    1.42  
    1.43 -lemma notI:
    1.44 +schematic_lemma notI:
    1.45    assumes "!!x. x:P ==> q(x):False"
    1.46    shows "?p:~P"
    1.47    unfolding not_def
    1.48    apply (assumption | rule assms impI)+
    1.49    done
    1.50  
    1.51 -lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
    1.52 +schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
    1.53    unfolding not_def
    1.54    apply (drule (1) mp)
    1.55    apply (erule FalseE)
    1.56    done
    1.57  
    1.58  (*This is useful with the special implication rules for each kind of P. *)
    1.59 -lemma not_to_imp:
    1.60 +schematic_lemma not_to_imp:
    1.61    assumes "p:~P"
    1.62      and "!!x. x:(P-->False) ==> q(x):Q"
    1.63    shows "?p:Q"
    1.64 @@ -217,13 +217,13 @@
    1.65  
    1.66  (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
    1.67     this implication, then apply impI to move P back into the assumptions.*)
    1.68 -lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
    1.69 +schematic_lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
    1.70    apply (assumption | rule mp)+
    1.71    done
    1.72  
    1.73  
    1.74  (*Contrapositive of an inference rule*)
    1.75 -lemma contrapos:
    1.76 +schematic_lemma contrapos:
    1.77    assumes major: "p:~Q"
    1.78      and minor: "!!y. y:P==>q(y):Q"
    1.79    shows "?a:~P"
    1.80 @@ -271,7 +271,7 @@
    1.81  
    1.82  (*** If-and-only-if ***)
    1.83  
    1.84 -lemma iffI:
    1.85 +schematic_lemma iffI:
    1.86    assumes "!!x. x:P ==> q(x):Q"
    1.87      and "!!x. x:Q ==> r(x):P"
    1.88    shows "?p:P<->Q"
    1.89 @@ -282,7 +282,7 @@
    1.90  
    1.91  (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
    1.92    
    1.93 -lemma iffE:
    1.94 +schematic_lemma iffE:
    1.95    assumes "p:P <-> Q"
    1.96      and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
    1.97    shows "?p:R"
    1.98 @@ -294,28 +294,28 @@
    1.99  
   1.100  (* Destruct rules for <-> similar to Modus Ponens *)
   1.101  
   1.102 -lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
   1.103 +schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
   1.104    unfolding iff_def
   1.105    apply (rule conjunct1 [THEN mp], assumption+)
   1.106    done
   1.107  
   1.108 -lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
   1.109 +schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
   1.110    unfolding iff_def
   1.111    apply (rule conjunct2 [THEN mp], assumption+)
   1.112    done
   1.113  
   1.114 -lemma iff_refl: "?p:P <-> P"
   1.115 +schematic_lemma iff_refl: "?p:P <-> P"
   1.116    apply (rule iffI)
   1.117     apply assumption+
   1.118    done
   1.119  
   1.120 -lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
   1.121 +schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
   1.122    apply (erule iffE)
   1.123    apply (rule iffI)
   1.124     apply (erule (1) mp)+
   1.125    done
   1.126  
   1.127 -lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
   1.128 +schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
   1.129    apply (rule iffI)
   1.130     apply (assumption | erule iffE | erule (1) impE)+
   1.131    done
   1.132 @@ -326,7 +326,7 @@
   1.133   do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   1.134  ***)
   1.135  
   1.136 -lemma ex1I:
   1.137 +schematic_lemma ex1I:
   1.138    assumes "p:P(a)"
   1.139      and "!!x u. u:P(x) ==> f(u) : x=a"
   1.140    shows "?p:EX! x. P(x)"
   1.141 @@ -334,7 +334,7 @@
   1.142    apply (assumption | rule assms exI conjI allI impI)+
   1.143    done
   1.144  
   1.145 -lemma ex1E:
   1.146 +schematic_lemma ex1E:
   1.147    assumes "p:EX! x. P(x)"
   1.148      and "!!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
   1.149    shows "?a : R"
   1.150 @@ -353,7 +353,7 @@
   1.151      REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
   1.152  *}
   1.153  
   1.154 -lemma conj_cong:
   1.155 +schematic_lemma conj_cong:
   1.156    assumes "p:P <-> P'"
   1.157      and "!!x. x:P' ==> q(x):Q <-> Q'"
   1.158    shows "?p:(P&Q) <-> (P'&Q')"
   1.159 @@ -362,12 +362,12 @@
   1.160      erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
   1.161    done
   1.162  
   1.163 -lemma disj_cong:
   1.164 +schematic_lemma disj_cong:
   1.165    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
   1.166    apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
   1.167    done
   1.168  
   1.169 -lemma imp_cong:
   1.170 +schematic_lemma imp_cong:
   1.171    assumes "p:P <-> P'"
   1.172      and "!!x. x:P' ==> q(x):Q <-> Q'"
   1.173    shows "?p:(P-->Q) <-> (P'-->Q')"
   1.174 @@ -376,24 +376,24 @@
   1.175      tactic {* iff_tac @{thms assms} 1 *})+
   1.176    done
   1.177  
   1.178 -lemma iff_cong:
   1.179 +schematic_lemma iff_cong:
   1.180    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   1.181    apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
   1.182    done
   1.183  
   1.184 -lemma not_cong:
   1.185 +schematic_lemma not_cong:
   1.186    "p:P <-> P' ==> ?p:~P <-> ~P'"
   1.187    apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
   1.188    done
   1.189  
   1.190 -lemma all_cong:
   1.191 +schematic_lemma all_cong:
   1.192    assumes "!!x. f(x):P(x) <-> Q(x)"
   1.193    shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   1.194    apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
   1.195      tactic {* iff_tac @{thms assms} 1 *})+
   1.196    done
   1.197  
   1.198 -lemma ex_cong:
   1.199 +schematic_lemma ex_cong:
   1.200    assumes "!!x. f(x):P(x) <-> Q(x)"
   1.201    shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
   1.202    apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
   1.203 @@ -413,7 +413,7 @@
   1.204  
   1.205  lemmas refl = ieqI
   1.206  
   1.207 -lemma subst:
   1.208 +schematic_lemma subst:
   1.209    assumes prem1: "p:a=b"
   1.210      and prem2: "q:P(a)"
   1.211    shows "?p : P(b)"
   1.212 @@ -423,17 +423,17 @@
   1.213    apply assumption
   1.214    done
   1.215  
   1.216 -lemma sym: "q:a=b ==> ?c:b=a"
   1.217 +schematic_lemma sym: "q:a=b ==> ?c:b=a"
   1.218    apply (erule subst)
   1.219    apply (rule refl)
   1.220    done
   1.221  
   1.222 -lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
   1.223 +schematic_lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
   1.224    apply (erule (1) subst)
   1.225    done
   1.226  
   1.227  (** ~ b=a ==> ~ a=b **)
   1.228 -lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
   1.229 +schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
   1.230    apply (erule contrapos)
   1.231    apply (erule sym)
   1.232    done
   1.233 @@ -442,7 +442,7 @@
   1.234  lemmas ssubst = sym [THEN subst, standard]
   1.235  
   1.236  (*A special case of ex1E that would otherwise need quantifier expansion*)
   1.237 -lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   1.238 +schematic_lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   1.239    apply (erule ex1E)
   1.240    apply (rule trans)
   1.241     apply (rule_tac [2] sym)
   1.242 @@ -451,17 +451,17 @@
   1.243  
   1.244  (** Polymorphic congruence rules **)
   1.245  
   1.246 -lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
   1.247 +schematic_lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
   1.248    apply (erule ssubst)
   1.249    apply (rule refl)
   1.250    done
   1.251  
   1.252 -lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
   1.253 +schematic_lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
   1.254    apply (erule ssubst)+
   1.255    apply (rule refl)
   1.256    done
   1.257  
   1.258 -lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
   1.259 +schematic_lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
   1.260    apply (erule ssubst)+
   1.261    apply (rule refl)
   1.262    done
   1.263 @@ -470,7 +470,7 @@
   1.264          a = b
   1.265          |   |
   1.266          c = d   *)
   1.267 -lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
   1.268 +schematic_lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
   1.269    apply (rule trans)
   1.270     apply (rule trans)
   1.271      apply (rule sym)
   1.272 @@ -478,7 +478,7 @@
   1.273    done
   1.274  
   1.275  (*Dual of box_equals: for proving equalities backwards*)
   1.276 -lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
   1.277 +schematic_lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
   1.278    apply (rule trans)
   1.279     apply (rule trans)
   1.280      apply (assumption | rule sym)+
   1.281 @@ -486,17 +486,17 @@
   1.282  
   1.283  (** Congruence rules for predicate letters **)
   1.284  
   1.285 -lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
   1.286 +schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
   1.287    apply (rule iffI)
   1.288     apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   1.289    done
   1.290  
   1.291 -lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   1.292 +schematic_lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   1.293    apply (rule iffI)
   1.294     apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   1.295    done
   1.296  
   1.297 -lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
   1.298 +schematic_lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
   1.299    apply (rule iffI)
   1.300     apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   1.301    done
   1.302 @@ -514,14 +514,14 @@
   1.303     R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   1.304      (preprint, University of St Andrews, 1991)  ***)
   1.305  
   1.306 -lemma conj_impE:
   1.307 +schematic_lemma conj_impE:
   1.308    assumes major: "p:(P&Q)-->S"
   1.309      and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
   1.310    shows "?p:R"
   1.311    apply (assumption | rule conjI impI major [THEN mp] minor)+
   1.312    done
   1.313  
   1.314 -lemma disj_impE:
   1.315 +schematic_lemma disj_impE:
   1.316    assumes major: "p:(P|Q)-->S"
   1.317      and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
   1.318    shows "?p:R"
   1.319 @@ -532,7 +532,7 @@
   1.320  
   1.321  (*Simplifies the implication.  Classical version is stronger.
   1.322    Still UNSAFE since Q must be provable -- backtracking needed.  *)
   1.323 -lemma imp_impE:
   1.324 +schematic_lemma imp_impE:
   1.325    assumes major: "p:(P-->Q)-->S"
   1.326      and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
   1.327      and r2: "!!x. x:S ==> r(x):R"
   1.328 @@ -542,7 +542,7 @@
   1.329  
   1.330  (*Simplifies the implication.  Classical version is stronger.
   1.331    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   1.332 -lemma not_impE:
   1.333 +schematic_lemma not_impE:
   1.334    assumes major: "p:~P --> S"
   1.335      and r1: "!!y. y:P ==> q(y):False"
   1.336      and r2: "!!y. y:S ==> r(y):R"
   1.337 @@ -551,7 +551,7 @@
   1.338    done
   1.339  
   1.340  (*Simplifies the implication.   UNSAFE.  *)
   1.341 -lemma iff_impE:
   1.342 +schematic_lemma iff_impE:
   1.343    assumes major: "p:(P<->Q)-->S"
   1.344      and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
   1.345      and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
   1.346 @@ -561,7 +561,7 @@
   1.347    done
   1.348  
   1.349  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   1.350 -lemma all_impE:
   1.351 +schematic_lemma all_impE:
   1.352    assumes major: "p:(ALL x. P(x))-->S"
   1.353      and r1: "!!x. q:P(x)"
   1.354      and r2: "!!y. y:S ==> r(y):R"
   1.355 @@ -570,7 +570,7 @@
   1.356    done
   1.357  
   1.358  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   1.359 -lemma ex_impE:
   1.360 +schematic_lemma ex_impE:
   1.361    assumes major: "p:(EX x. P(x))-->S"
   1.362      and r: "!!y. y:P(a)-->S ==> q(y):R"
   1.363    shows "?p:R"
   1.364 @@ -578,7 +578,7 @@
   1.365    done
   1.366  
   1.367  
   1.368 -lemma rev_cut_eq:
   1.369 +schematic_lemma rev_cut_eq:
   1.370    assumes "p:a=b"
   1.371      and "!!x. x:a=b ==> f(x):R"
   1.372    shows "?p:R"
   1.373 @@ -619,7 +619,7 @@
   1.374  
   1.375  (*** Rewrite rules ***)
   1.376  
   1.377 -lemma conj_rews:
   1.378 +schematic_lemma conj_rews:
   1.379    "?p1 : P & True <-> P"
   1.380    "?p2 : True & P <-> P"
   1.381    "?p3 : P & False <-> False"
   1.382 @@ -631,7 +631,7 @@
   1.383    apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
   1.384    done
   1.385  
   1.386 -lemma disj_rews:
   1.387 +schematic_lemma disj_rews:
   1.388    "?p1 : P | True <-> True"
   1.389    "?p2 : True | P <-> True"
   1.390    "?p3 : P | False <-> P"
   1.391 @@ -641,13 +641,13 @@
   1.392    apply (tactic {* IntPr.fast_tac 1 *})+
   1.393    done
   1.394  
   1.395 -lemma not_rews:
   1.396 +schematic_lemma not_rews:
   1.397    "?p1 : ~ False <-> True"
   1.398    "?p2 : ~ True <-> False"
   1.399    apply (tactic {* IntPr.fast_tac 1 *})+
   1.400    done
   1.401  
   1.402 -lemma imp_rews:
   1.403 +schematic_lemma imp_rews:
   1.404    "?p1 : (P --> False) <-> ~P"
   1.405    "?p2 : (P --> True) <-> True"
   1.406    "?p3 : (False --> P) <-> True"
   1.407 @@ -657,7 +657,7 @@
   1.408    apply (tactic {* IntPr.fast_tac 1 *})+
   1.409    done
   1.410  
   1.411 -lemma iff_rews:
   1.412 +schematic_lemma iff_rews:
   1.413    "?p1 : (True <-> P) <-> P"
   1.414    "?p2 : (P <-> True) <-> P"
   1.415    "?p3 : (P <-> P) <-> True"
   1.416 @@ -666,14 +666,14 @@
   1.417    apply (tactic {* IntPr.fast_tac 1 *})+
   1.418    done
   1.419  
   1.420 -lemma quant_rews:
   1.421 +schematic_lemma quant_rews:
   1.422    "?p1 : (ALL x. P) <-> P"
   1.423    "?p2 : (EX x. P) <-> P"
   1.424    apply (tactic {* IntPr.fast_tac 1 *})+
   1.425    done
   1.426  
   1.427  (*These are NOT supplied by default!*)
   1.428 -lemma distrib_rews1:
   1.429 +schematic_lemma distrib_rews1:
   1.430    "?p1 : ~(P|Q) <-> ~P & ~Q"
   1.431    "?p2 : P & (Q | R) <-> P&Q | P&R"
   1.432    "?p3 : (Q | R) & P <-> Q&P | R&P"
   1.433 @@ -681,7 +681,7 @@
   1.434    apply (tactic {* IntPr.fast_tac 1 *})+
   1.435    done
   1.436  
   1.437 -lemma distrib_rews2:
   1.438 +schematic_lemma distrib_rews2:
   1.439    "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
   1.440    "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
   1.441    "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
   1.442 @@ -691,11 +691,11 @@
   1.443  
   1.444  lemmas distrib_rews = distrib_rews1 distrib_rews2
   1.445  
   1.446 -lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
   1.447 +schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
   1.448    apply (tactic {* IntPr.fast_tac 1 *})
   1.449    done
   1.450  
   1.451 -lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
   1.452 +schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
   1.453    apply (tactic {* IntPr.fast_tac 1 *})
   1.454    done
   1.455