proper use of bind_thm(s);
authorwenzelm
Sat Nov 03 18:42:38 2001 +0100 (2001-11-03)
changeset 12038343a9888e875
parent 12037 0282eacef4e7
child 12039 ef2a6fdd3564
proper use of bind_thm(s);
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Sat Nov 03 18:42:00 2001 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sat Nov 03 18:42:38 2001 +0100
     1.3 @@ -9,11 +9,11 @@
     1.4  
     1.5  (* Elimination of True from asumptions: *)
     1.6  
     1.7 -val True_implies_equals = prove_goal IFOL.thy
     1.8 +bind_thm ("True_implies_equals", prove_goal IFOL.thy
     1.9   "(True ==> PROP P) == PROP P"
    1.10  (K [rtac equal_intr_rule 1, atac 2,
    1.11            METAHYPS (fn prems => resolve_tac prems 1) 1,
    1.12 -          rtac TrueI 1]);
    1.13 +          rtac TrueI 1]));
    1.14  
    1.15  
    1.16  (*** Rewrite rules ***)
    1.17 @@ -24,57 +24,57 @@
    1.18     (fn prems => [ (cut_facts_tac prems 1),
    1.19                    (IntPr.fast_tac 1) ]));
    1.20  
    1.21 -val conj_simps = map int_prove_fun
    1.22 +bind_thms ("conj_simps", map int_prove_fun
    1.23   ["P & True <-> P",      "True & P <-> P",
    1.24    "P & False <-> False", "False & P <-> False",
    1.25    "P & P <-> P", "P & P & Q <-> P & Q",
    1.26    "P & ~P <-> False",    "~P & P <-> False",
    1.27 -  "(P & Q) & R <-> P & (Q & R)"];
    1.28 +  "(P & Q) & R <-> P & (Q & R)"]);
    1.29  
    1.30 -val disj_simps = map int_prove_fun
    1.31 +bind_thms ("disj_simps", map int_prove_fun
    1.32   ["P | True <-> True",  "True | P <-> True",
    1.33    "P | False <-> P",    "False | P <-> P",
    1.34    "P | P <-> P", "P | P | Q <-> P | Q",
    1.35 -  "(P | Q) | R <-> P | (Q | R)"];
    1.36 +  "(P | Q) | R <-> P | (Q | R)"]);
    1.37  
    1.38 -val not_simps = map int_prove_fun
    1.39 +bind_thms ("not_simps", map int_prove_fun
    1.40   ["~(P|Q)  <-> ~P & ~Q",
    1.41 -  "~ False <-> True",   "~ True <-> False"];
    1.42 +  "~ False <-> True",   "~ True <-> False"]);
    1.43  
    1.44 -val imp_simps = map int_prove_fun
    1.45 +bind_thms ("imp_simps", map int_prove_fun
    1.46   ["(P --> False) <-> ~P",       "(P --> True) <-> True",
    1.47    "(False --> P) <-> True",     "(True --> P) <-> P",
    1.48 -  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
    1.49 +  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"]);
    1.50  
    1.51 -val iff_simps = map int_prove_fun
    1.52 +bind_thms ("iff_simps", map int_prove_fun
    1.53   ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    1.54    "(P <-> P) <-> True",
    1.55 -  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    1.56 +  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"]);
    1.57  
    1.58  (*The x=t versions are needed for the simplification procedures*)
    1.59 -val quant_simps = map int_prove_fun
    1.60 +bind_thms ("quant_simps", map int_prove_fun
    1.61   ["(ALL x. P) <-> P",
    1.62    "(ALL x. x=t --> P(x)) <-> P(t)",
    1.63    "(ALL x. t=x --> P(x)) <-> P(t)",
    1.64    "(EX x. P) <-> P",
    1.65    "(EX x. x=t & P(x)) <-> P(t)",
    1.66 -  "(EX x. t=x & P(x)) <-> P(t)"];
    1.67 +  "(EX x. t=x & P(x)) <-> P(t)"]);
    1.68  
    1.69  (*These are NOT supplied by default!*)
    1.70 -val distrib_simps  = map int_prove_fun
    1.71 +bind_thms ("distrib_simps", map int_prove_fun
    1.72   ["P & (Q | R) <-> P&Q | P&R",
    1.73    "(Q | R) & P <-> Q&P | R&P",
    1.74 -  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
    1.75 +  "(P | Q --> R) <-> (P --> R) & (Q --> R)"]);
    1.76  
    1.77  (** Conversion into rewrite rules **)
    1.78  
    1.79  fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    1.80  
    1.81 -val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    1.82 -val iff_reflection_F = P_iff_F RS iff_reflection;
    1.83 +bind_thm ("P_iff_F", int_prove_fun "~P ==> (P <-> False)");
    1.84 +bind_thm ("iff_reflection_F", P_iff_F RS iff_reflection);
    1.85  
    1.86 -val P_iff_T = int_prove_fun "P ==> (P <-> True)";
    1.87 -val iff_reflection_T = P_iff_T RS iff_reflection;
    1.88 +bind_thm ("P_iff_T", int_prove_fun "P ==> (P <-> True)");
    1.89 +bind_thm ("iff_reflection_T", P_iff_T RS iff_reflection);
    1.90  
    1.91  (*Make meta-equalities.  The operator below is Trueprop*)
    1.92  
    1.93 @@ -135,7 +135,7 @@
    1.94  
    1.95  (*Avoids duplication of subgoals after expand_if, when the true and false
    1.96    cases boil down to the same thing.*)
    1.97 -val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
    1.98 +bind_thm ("cases_simp", prove_fun "(P --> Q) & (~P --> Q) <-> Q");
    1.99  
   1.100  
   1.101  (*** Miniscoping: pushing quantifiers in
   1.102 @@ -145,32 +145,32 @@
   1.103  ***)
   1.104  
   1.105  (*existential miniscoping*)
   1.106 -val int_ex_simps = map int_prove_fun
   1.107 -                     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
   1.108 -                      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
   1.109 -                      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
   1.110 -                      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
   1.111 +bind_thms ("int_ex_simps", map int_prove_fun
   1.112 + ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
   1.113 +  "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
   1.114 +  "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
   1.115 +  "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"]);
   1.116  
   1.117  (*classical rules*)
   1.118 -val cla_ex_simps = map prove_fun
   1.119 -                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
   1.120 -                      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
   1.121 +bind_thms ("cla_ex_simps", map prove_fun
   1.122 + ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
   1.123 +  "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"]);
   1.124  
   1.125 -val ex_simps = int_ex_simps @ cla_ex_simps;
   1.126 +bind_thms ("ex_simps", int_ex_simps @ cla_ex_simps);
   1.127  
   1.128  (*universal miniscoping*)
   1.129 -val int_all_simps = map int_prove_fun
   1.130 -                      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
   1.131 -                       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
   1.132 -                       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
   1.133 -                       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
   1.134 +bind_thms ("int_all_simps", map int_prove_fun
   1.135 + ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
   1.136 +  "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
   1.137 +  "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
   1.138 +  "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"]);
   1.139  
   1.140  (*classical rules*)
   1.141 -val cla_all_simps = map prove_fun
   1.142 -                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
   1.143 -                       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
   1.144 +bind_thms ("cla_all_simps", map prove_fun
   1.145 + ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
   1.146 +  "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]);
   1.147  
   1.148 -val all_simps = int_all_simps @ cla_all_simps;
   1.149 +bind_thms ("all_simps", int_all_simps @ cla_all_simps);
   1.150  
   1.151  
   1.152  (*** Named rewrite rules proved for IFOL ***)
   1.153 @@ -183,11 +183,11 @@
   1.154  
   1.155  int_prove "conj_commute" "P&Q <-> Q&P";
   1.156  int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
   1.157 -val conj_comms = [conj_commute, conj_left_commute];
   1.158 +bind_thms ("conj_comms", [conj_commute, conj_left_commute]);
   1.159  
   1.160  int_prove "disj_commute" "P|Q <-> Q|P";
   1.161  int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
   1.162 -val disj_comms = [disj_commute, disj_left_commute];
   1.163 +bind_thms ("disj_comms", [disj_commute, disj_left_commute]);
   1.164  
   1.165  int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
   1.166  int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
   1.167 @@ -272,8 +272,8 @@
   1.168  
   1.169  (*** Case splitting ***)
   1.170  
   1.171 -val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
   1.172 -  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
   1.173 +bind_thm ("meta_eq_to_iff", prove_goal IFOL.thy "x==y ==> x<->y"
   1.174 +  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]));
   1.175  
   1.176  structure SplitterData =
   1.177    struct
   1.178 @@ -307,16 +307,16 @@
   1.179  open Induction;
   1.180  
   1.181  
   1.182 -val meta_simps =
   1.183 -   [triv_forall_equality,  (* prunes params *)
   1.184 -    True_implies_equals];  (* prune asms `True' *)
   1.185 +bind_thms ("meta_simps",
   1.186 + [triv_forall_equality,   (* prunes params *)
   1.187 +  True_implies_equals]);  (* prune asms `True' *)
   1.188  
   1.189 -val IFOL_simps =
   1.190 -    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
   1.191 -    imp_simps @ iff_simps @ quant_simps;
   1.192 +bind_thms ("IFOL_simps",
   1.193 + [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
   1.194 +  imp_simps @ iff_simps @ quant_simps);
   1.195  
   1.196 -val notFalseI = int_prove_fun "~False";
   1.197 -val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
   1.198 +bind_thm ("notFalseI", int_prove_fun "~False");
   1.199 +bind_thms ("triv_rls", [TrueI,refl,reflexive_thm,iff_refl,notFalseI]);
   1.200  
   1.201  fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
   1.202                                   atac, etac FalseE];
   1.203 @@ -339,14 +339,14 @@
   1.204    addsimprocs [defALL_regroup, defEX_regroup]    
   1.205    addcongs [imp_cong];
   1.206  
   1.207 -val cla_simps =
   1.208 -    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
   1.209 -     not_all, not_ex, cases_simp] @
   1.210 -    map prove_fun
   1.211 -     ["~(P&Q)  <-> ~P | ~Q",
   1.212 -      "P | ~P",             "~P | P",
   1.213 -      "~ ~ P <-> P",        "(~P --> P) <-> P",
   1.214 -      "(~P <-> ~Q) <-> (P<->Q)"];
   1.215 +bind_thms ("cla_simps",
   1.216 +  [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
   1.217 +   not_all, not_ex, cases_simp] @
   1.218 +  map prove_fun
   1.219 +   ["~(P&Q) <-> ~P | ~Q",
   1.220 +    "P | ~P",             "~P | P",
   1.221 +    "~ ~ P <-> P",        "(~P --> P) <-> P",
   1.222 +    "(~P <-> ~Q) <-> (P<->Q)"]);
   1.223  
   1.224  (*classical simprules too*)
   1.225  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
     2.1 --- a/src/HOL/simpdata.ML	Sat Nov 03 18:42:00 2001 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Sat Nov 03 18:42:38 2001 +0100
     2.3 @@ -17,19 +17,16 @@
     2.4  br refl 1;
     2.5  qed "eta_contract_eq";
     2.6  
     2.7 -local
     2.8  
     2.9 -  fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
    2.10 -
    2.11 -in
    2.12 +fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
    2.13  
    2.14  (*Make meta-equalities.  The operator below is Trueprop*)
    2.15  
    2.16  fun mk_meta_eq r = r RS eq_reflection;
    2.17  fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
    2.18  
    2.19 -val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
    2.20 -val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);
    2.21 +bind_thm ("Eq_TrueI", mk_meta_eq (prover  "P --> (P = True)"  RS mp));
    2.22 +bind_thm ("Eq_FalseI", mk_meta_eq(prover "~P --> (P = False)" RS mp));
    2.23  
    2.24  fun mk_eq th = case concl_of th of
    2.25          Const("==",_)$_$_       => th
    2.26 @@ -47,63 +44,56 @@
    2.27    handle THM _ =>
    2.28    error("Premises and conclusion of congruence rules must be =-equalities");
    2.29  
    2.30 -val not_not = prover "(~ ~ P) = P";
    2.31 +bind_thm ("not_not", prover "(~ ~ P) = P");
    2.32  
    2.33 -val simp_thms = [not_not] @ map prover
    2.34 - [ "(x=x) = True",
    2.35 -   "(~True) = False", "(~False) = True",
    2.36 -   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    2.37 -   "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    2.38 -   "(True --> P) = P", "(False --> P) = True",
    2.39 -   "(P --> True) = True", "(P --> P) = True",
    2.40 -   "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    2.41 -   "(P & True) = P", "(True & P) = P",
    2.42 -   "(P & False) = False", "(False & P) = False",
    2.43 -   "(P & P) = P", "(P & (P & Q)) = (P & Q)",
    2.44 -   "(P & ~P) = False",    "(~P & P) = False",
    2.45 -   "(P | True) = True", "(True | P) = True",
    2.46 -   "(P | False) = P", "(False | P) = P",
    2.47 -   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    2.48 -   "(P | ~P) = True",    "(~P | P) = True",
    2.49 -   "((~P) = (~Q)) = (P=Q)",
    2.50 -   "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
    2.51 +bind_thms ("simp_thms", [not_not] @ map prover
    2.52 + ["(x=x) = True",
    2.53 +  "(~True) = False", "(~False) = True",
    2.54 +  "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    2.55 +  "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    2.56 +  "(True --> P) = P", "(False --> P) = True",
    2.57 +  "(P --> True) = True", "(P --> P) = True",
    2.58 +  "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    2.59 +  "(P & True) = P", "(True & P) = P",
    2.60 +  "(P & False) = False", "(False & P) = False",
    2.61 +  "(P & P) = P", "(P & (P & Q)) = (P & Q)",
    2.62 +  "(P & ~P) = False",    "(~P & P) = False",
    2.63 +  "(P | True) = True", "(True | P) = True",
    2.64 +  "(P | False) = P", "(False | P) = P",
    2.65 +  "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    2.66 +  "(P | ~P) = True",    "(~P | P) = True",
    2.67 +  "((~P) = (~Q)) = (P=Q)",
    2.68 +  "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
    2.69  (* needed for the one-point-rule quantifier simplification procs*)
    2.70  (*essential for termination!!*)
    2.71 -   "(? x. x=t & P(x)) = P(t)",
    2.72 -   "(? x. t=x & P(x)) = P(t)",
    2.73 -   "(! x. x=t --> P(x)) = P(t)",
    2.74 -   "(! x. t=x --> P(x)) = P(t)" ];
    2.75 +  "(? x. x=t & P(x)) = P(t)",
    2.76 +  "(? x. t=x & P(x)) = P(t)",
    2.77 +  "(! x. x=t --> P(x)) = P(t)",
    2.78 +  "(! x. t=x --> P(x)) = P(t)"]);
    2.79  
    2.80 -val imp_cong = standard(impI RSN
    2.81 +bind_thm ("imp_cong", standard (impI RSN
    2.82      (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    2.83 -        (fn _=> [(Blast_tac 1)]) RS mp RS mp));
    2.84 +        (fn _=> [(Blast_tac 1)]) RS mp RS mp)));
    2.85  
    2.86  (*Miniscoping: pushing in existential quantifiers*)
    2.87 -val ex_simps = map prover
    2.88 -                ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
    2.89 -                 "(EX x. P & Q x)   = (P & (EX x. Q x))",
    2.90 -                 "(EX x. P x | Q)   = ((EX x. P x) | Q)",
    2.91 -                 "(EX x. P | Q x)   = (P | (EX x. Q x))",
    2.92 -                 "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
    2.93 -                 "(EX x. P --> Q x) = (P --> (EX x. Q x))"];
    2.94 +bind_thms ("ex_simps", map prover
    2.95 + ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
    2.96 +  "(EX x. P & Q x)   = (P & (EX x. Q x))",
    2.97 +  "(EX x. P x | Q)   = ((EX x. P x) | Q)",
    2.98 +  "(EX x. P | Q x)   = (P | (EX x. Q x))",
    2.99 +  "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
   2.100 +  "(EX x. P --> Q x) = (P --> (EX x. Q x))"]);
   2.101  
   2.102  (*Miniscoping: pushing in universal quantifiers*)
   2.103 -val all_simps = map prover
   2.104 -                ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
   2.105 -                 "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
   2.106 -                 "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
   2.107 -                 "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
   2.108 -                 "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
   2.109 -                 "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
   2.110 +bind_thms ("all_simps", map prover
   2.111 + ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
   2.112 +  "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
   2.113 +  "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
   2.114 +  "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
   2.115 +  "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
   2.116 +  "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]);
   2.117  
   2.118  
   2.119 -end;
   2.120 -
   2.121 -bind_thms ("ex_simps", ex_simps);
   2.122 -bind_thms ("all_simps", all_simps);
   2.123 -bind_thm ("not_not", not_not);
   2.124 -bind_thm ("imp_cong", imp_cong);
   2.125 -
   2.126  (* Elimination of True from asumptions: *)
   2.127  
   2.128  local fun rd s = read_cterm (sign_of (the_context())) (s, propT);
   2.129 @@ -117,18 +107,18 @@
   2.130  prove "eq_commute" "(a=b) = (b=a)";
   2.131  prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))";
   2.132  prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))";
   2.133 -val eq_ac = [eq_commute, eq_left_commute, eq_assoc];
   2.134 +bind_thms ("eq_ac", [eq_commute, eq_left_commute, eq_assoc]);
   2.135  
   2.136  prove "neq_commute" "(a~=b) = (b~=a)";
   2.137  
   2.138  prove "conj_commute" "(P&Q) = (Q&P)";
   2.139  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
   2.140 -val conj_comms = [conj_commute, conj_left_commute];
   2.141 +bind_thms ("conj_comms", [conj_commute, conj_left_commute]);
   2.142  prove "conj_assoc" "((P&Q)&R) = (P&(Q&R))";
   2.143  
   2.144  prove "disj_commute" "(P|Q) = (Q|P)";
   2.145  prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))";
   2.146 -val disj_comms = [disj_commute, disj_left_commute];
   2.147 +bind_thms ("disj_comms", [disj_commute, disj_left_commute]);
   2.148  prove "disj_assoc" "((P|Q)|R) = (P|(Q|R))";
   2.149  
   2.150  prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";