Drule.store: proper binding;
authorwenzelm
Wed Oct 28 16:25:26 2009 +0100 (2009-10-28)
changeset 332771bdc3c732fdd
parent 33276 f2bc8bc6e73d
child 33278 ba9f52f56356
Drule.store: proper binding;
conceal internal bindings;
src/Pure/conjunction.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/conjunction.ML	Wed Oct 28 16:25:10 2009 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Wed Oct 28 16:25:26 2009 +0100
     1.3 @@ -83,15 +83,16 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
     1.8 -val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
     1.9 +val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
    1.10 +val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
    1.11  
    1.12 -val conjunctionI = Drule.store_standard_thm "conjunctionI"
    1.13 -  (Drule.implies_intr_list [A, B]
    1.14 -    (Thm.equal_elim
    1.15 -      (Thm.symmetric conjunction_def)
    1.16 -      (Thm.forall_intr C (Thm.implies_intr ABC
    1.17 -        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.18 +val conjunctionI =
    1.19 +  Drule.store_standard_thm (Binding.name "conjunctionI")
    1.20 +    (Drule.implies_intr_list [A, B]
    1.21 +      (Thm.equal_elim
    1.22 +        (Thm.symmetric conjunction_def)
    1.23 +        (Thm.forall_intr C (Thm.implies_intr ABC
    1.24 +          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.25  
    1.26  
    1.27  fun intr tha thb =
     2.1 --- a/src/Pure/drule.ML	Wed Oct 28 16:25:10 2009 +0100
     2.2 +++ b/src/Pure/drule.ML	Wed Oct 28 16:25:26 2009 +0100
     2.3 @@ -78,10 +78,10 @@
     2.4    val standard: thm -> thm
     2.5    val standard': thm -> thm
     2.6    val get_def: theory -> xstring -> thm
     2.7 -  val store_thm: bstring -> thm -> thm
     2.8 -  val store_standard_thm: bstring -> thm -> thm
     2.9 -  val store_thm_open: bstring -> thm -> thm
    2.10 -  val store_standard_thm_open: bstring -> thm -> thm
    2.11 +  val store_thm: binding -> thm -> thm
    2.12 +  val store_standard_thm: binding -> thm -> thm
    2.13 +  val store_thm_open: binding -> thm -> thm
    2.14 +  val store_standard_thm_open: binding -> thm -> thm
    2.15    val compose_single: thm * int * thm -> thm
    2.16    val imp_cong_rule: thm -> thm -> thm
    2.17    val arg_cong_rule: cterm -> thm -> thm
    2.18 @@ -455,27 +455,32 @@
    2.19  fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
    2.20  
    2.21  fun store_thm name th =
    2.22 -  Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
    2.23 +  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
    2.24  
    2.25  fun store_thm_open name th =
    2.26 -  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
    2.27 +  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
    2.28  
    2.29  fun store_standard_thm name th = store_thm name (standard th);
    2.30  fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
    2.31  
    2.32  val reflexive_thm =
    2.33    let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
    2.34 -  in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
    2.35 +  in store_standard_thm_open (Binding.name "reflexive") (Thm.reflexive cx) end;
    2.36  
    2.37  val symmetric_thm =
    2.38 -  let val xy = read_prop "x::'a == y::'a"
    2.39 -  in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end;
    2.40 +  let
    2.41 +    val xy = read_prop "x::'a == y::'a";
    2.42 +    val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
    2.43 +  in store_standard_thm_open (Binding.name "symmetric") thm end;
    2.44  
    2.45  val transitive_thm =
    2.46 -  let val xy = read_prop "x::'a == y::'a"
    2.47 -      val yz = read_prop "y::'a == z::'a"
    2.48 -      val xythm = Thm.assume xy and yzthm = Thm.assume yz
    2.49 -  in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    2.50 +  let
    2.51 +    val xy = read_prop "x::'a == y::'a";
    2.52 +    val yz = read_prop "y::'a == z::'a";
    2.53 +    val xythm = Thm.assume xy;
    2.54 +    val yzthm = Thm.assume yz;
    2.55 +    val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
    2.56 +  in store_standard_thm_open (Binding.name "transitive") thm end;
    2.57  
    2.58  fun symmetric_fun thm = thm RS symmetric_thm;
    2.59  
    2.60 @@ -485,7 +490,8 @@
    2.61    in equal_elim (eta_conversion (cprop_of eq')) eq' end;
    2.62  
    2.63  val equals_cong =
    2.64 -  store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a"));
    2.65 +  store_standard_thm_open (Binding.name "equals_cong")
    2.66 +    (Thm.reflexive (read_prop "x::'a == y::'a"));
    2.67  
    2.68  val imp_cong =
    2.69    let
    2.70 @@ -494,7 +500,7 @@
    2.71      val AC = read_prop "A ==> C"
    2.72      val A = read_prop "A"
    2.73    in
    2.74 -    store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr
    2.75 +    store_standard_thm_open (Binding.name "imp_cong") (implies_intr ABC (equal_intr
    2.76        (implies_intr AB (implies_intr A
    2.77          (equal_elim (implies_elim (assume ABC) (assume A))
    2.78            (implies_elim (assume AB) (assume A)))))
    2.79 @@ -510,11 +516,12 @@
    2.80      val A = read_prop "A"
    2.81      val B = read_prop "B"
    2.82    in
    2.83 -    store_standard_thm_open "swap_prems_eq" (equal_intr
    2.84 -      (implies_intr ABC (implies_intr B (implies_intr A
    2.85 -        (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
    2.86 -      (implies_intr BAC (implies_intr A (implies_intr B
    2.87 -        (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
    2.88 +    store_standard_thm_open (Binding.name "swap_prems_eq")
    2.89 +      (equal_intr
    2.90 +        (implies_intr ABC (implies_intr B (implies_intr A
    2.91 +          (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
    2.92 +        (implies_intr BAC (implies_intr A (implies_intr B
    2.93 +          (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
    2.94    end;
    2.95  
    2.96  val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
    2.97 @@ -577,37 +584,41 @@
    2.98  (*** Some useful meta-theorems ***)
    2.99  
   2.100  (*The rule V/V, obtains assumption solving for eresolve_tac*)
   2.101 -val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
   2.102 -val _ = store_thm_open "_" asm_rl;
   2.103 +val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi"));
   2.104 +val _ = store_thm_open (Binding.name "_") asm_rl;
   2.105  
   2.106  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   2.107  val cut_rl =
   2.108 -  store_standard_thm_open "cut_rl"
   2.109 +  store_standard_thm_open (Binding.name "cut_rl")
   2.110      (Thm.trivial (read_prop "?psi ==> ?theta"));
   2.111  
   2.112  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   2.113       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   2.114  val revcut_rl =
   2.115 -  let val V = read_prop "V"
   2.116 -      and VW = read_prop "V ==> W";
   2.117 +  let
   2.118 +    val V = read_prop "V";
   2.119 +    val VW = read_prop "V ==> W";
   2.120    in
   2.121 -    store_standard_thm_open "revcut_rl"
   2.122 +    store_standard_thm_open (Binding.name "revcut_rl")
   2.123        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   2.124    end;
   2.125  
   2.126  (*for deleting an unwanted assumption*)
   2.127  val thin_rl =
   2.128 -  let val V = read_prop "V"
   2.129 -      and W = read_prop "W";
   2.130 -  in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end;
   2.131 +  let
   2.132 +    val V = read_prop "V";
   2.133 +    val W = read_prop "W";
   2.134 +    val thm = implies_intr V (implies_intr W (assume W));
   2.135 +  in store_standard_thm_open (Binding.name "thin_rl") thm end;
   2.136  
   2.137  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   2.138  val triv_forall_equality =
   2.139 -  let val V  = read_prop "V"
   2.140 -      and QV = read_prop "!!x::'a. V"
   2.141 -      and x  = certify (Free ("x", Term.aT []));
   2.142 +  let
   2.143 +    val V = read_prop "V";
   2.144 +    val QV = read_prop "!!x::'a. V";
   2.145 +    val x = certify (Free ("x", Term.aT []));
   2.146    in
   2.147 -    store_standard_thm_open "triv_forall_equality"
   2.148 +    store_standard_thm_open (Binding.name "triv_forall_equality")
   2.149        (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   2.150          (implies_intr V  (forall_intr x (assume V))))
   2.151    end;
   2.152 @@ -617,10 +628,10 @@
   2.153  *)
   2.154  val distinct_prems_rl =
   2.155    let
   2.156 -    val AAB = read_prop "Phi ==> Phi ==> Psi"
   2.157 +    val AAB = read_prop "Phi ==> Phi ==> Psi";
   2.158      val A = read_prop "Phi";
   2.159    in
   2.160 -    store_standard_thm_open "distinct_prems_rl"
   2.161 +    store_standard_thm_open (Binding.name "distinct_prems_rl")
   2.162        (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
   2.163    end;
   2.164  
   2.165 @@ -629,15 +640,17 @@
   2.166     `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   2.167  *)
   2.168  val swap_prems_rl =
   2.169 -  let val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
   2.170 -      val major = assume cmajor;
   2.171 -      val cminor1 = read_prop "PhiA";
   2.172 -      val minor1 = assume cminor1;
   2.173 -      val cminor2 = read_prop "PhiB";
   2.174 -      val minor2 = assume cminor2;
   2.175 -  in store_standard_thm_open "swap_prems_rl"
   2.176 -       (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   2.177 -         (implies_elim (implies_elim major minor1) minor2))))
   2.178 +  let
   2.179 +    val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
   2.180 +    val major = assume cmajor;
   2.181 +    val cminor1 = read_prop "PhiA";
   2.182 +    val minor1 = assume cminor1;
   2.183 +    val cminor2 = read_prop "PhiB";
   2.184 +    val minor2 = assume cminor2;
   2.185 +  in
   2.186 +    store_standard_thm_open (Binding.name "swap_prems_rl")
   2.187 +      (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   2.188 +        (implies_elim (implies_elim major minor1) minor2))))
   2.189    end;
   2.190  
   2.191  (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
   2.192 @@ -645,29 +658,36 @@
   2.193     Introduction rule for == as a meta-theorem.
   2.194  *)
   2.195  val equal_intr_rule =
   2.196 -  let val PQ = read_prop "phi ==> psi"
   2.197 -      and QP = read_prop "psi ==> phi"
   2.198 +  let
   2.199 +    val PQ = read_prop "phi ==> psi";
   2.200 +    val QP = read_prop "psi ==> phi";
   2.201    in
   2.202 -    store_standard_thm_open "equal_intr_rule"
   2.203 +    store_standard_thm_open (Binding.name "equal_intr_rule")
   2.204        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   2.205    end;
   2.206  
   2.207  (* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
   2.208  val equal_elim_rule1 =
   2.209 -  let val eq = read_prop "phi::prop == psi::prop"
   2.210 -      and P = read_prop "phi"
   2.211 -  in store_standard_thm_open "equal_elim_rule1"
   2.212 -    (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
   2.213 +  let
   2.214 +    val eq = read_prop "phi::prop == psi::prop";
   2.215 +    val P = read_prop "phi";
   2.216 +  in
   2.217 +    store_standard_thm_open (Binding.name "equal_elim_rule1")
   2.218 +      (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
   2.219    end;
   2.220  
   2.221  (* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
   2.222  val equal_elim_rule2 =
   2.223 -  store_standard_thm_open "equal_elim_rule2" (symmetric_thm RS equal_elim_rule1);
   2.224 +  store_standard_thm_open (Binding.name "equal_elim_rule2")
   2.225 +    (symmetric_thm RS equal_elim_rule1);
   2.226  
   2.227  (* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
   2.228  val remdups_rl =
   2.229 -  let val P = read_prop "phi" and Q = read_prop "psi";
   2.230 -  in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
   2.231 +  let
   2.232 +    val P = read_prop "phi";
   2.233 +    val Q = read_prop "psi";
   2.234 +    val thm = implies_intr_list [P, P, Q] (Thm.assume Q);
   2.235 +  in store_standard_thm_open (Binding.name "remdups_rl") thm end;
   2.236  
   2.237  
   2.238  
   2.239 @@ -688,13 +708,18 @@
   2.240  
   2.241  val protect = Thm.capply (certify Logic.protectC);
   2.242  
   2.243 -val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard
   2.244 -    (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   2.245 +val protectI =
   2.246 +  store_thm (Binding.conceal (Binding.name "protectI"))
   2.247 +    (Thm.kind_rule Thm.internalK (standard
   2.248 +      (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   2.249  
   2.250 -val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard
   2.251 -    (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   2.252 +val protectD =
   2.253 +  store_thm (Binding.conceal (Binding.name "protectD"))
   2.254 +    (Thm.kind_rule Thm.internalK (standard
   2.255 +      (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   2.256  
   2.257 -val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
   2.258 +val protect_cong =
   2.259 +  store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
   2.260  
   2.261  fun implies_intr_protected asms th =
   2.262    let val asms' = map protect asms in
   2.263 @@ -707,8 +732,10 @@
   2.264  
   2.265  (* term *)
   2.266  
   2.267 -val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard
   2.268 -    (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
   2.269 +val termI =
   2.270 +  store_thm (Binding.conceal (Binding.name "termI"))
   2.271 +    (Thm.kind_rule Thm.internalK (standard
   2.272 +      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
   2.273  
   2.274  fun mk_term ct =
   2.275    let
   2.276 @@ -735,13 +762,17 @@
   2.277  
   2.278  (* sort_constraint *)
   2.279  
   2.280 -val sort_constraintI = store_thm "sort_constraintI" (Thm.kind_rule Thm.internalK (standard
   2.281 -  (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
   2.282 +val sort_constraintI =
   2.283 +  store_thm (Binding.conceal (Binding.name "sort_constraintI"))
   2.284 +    (Thm.kind_rule Thm.internalK (standard
   2.285 +      (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
   2.286  
   2.287 -val sort_constraint_eq = store_thm "sort_constraint_eq" (Thm.kind_rule Thm.internalK (standard
   2.288 -  (Thm.equal_intr
   2.289 -    (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
   2.290 -    (implies_intr_list [A, C] (Thm.assume A)))));
   2.291 +val sort_constraint_eq =
   2.292 +  store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
   2.293 +    (Thm.kind_rule Thm.internalK (standard
   2.294 +      (Thm.equal_intr
   2.295 +        (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
   2.296 +        (implies_intr_list [A, C] (Thm.assume A)))));
   2.297  
   2.298  end;
   2.299  
   2.300 @@ -773,7 +804,7 @@
   2.301          |> Thm.forall_intr cx
   2.302          |> Thm.implies_intr cphi
   2.303          |> Thm.implies_intr rhs)
   2.304 -    |> store_standard_thm_open "norm_hhf_eq"
   2.305 +    |> store_standard_thm_open (Binding.name "norm_hhf_eq")
   2.306    end;
   2.307  
   2.308  val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);