certify wrt. dynamic context;
authorwenzelm
Sat Mar 29 19:14:09 2008 +0100 (2008-03-29)
changeset 2648749850ac120e3
parent 26486 b65a5272b360
child 26488 b497e3187ec7
certify wrt. dynamic context;
functional store_thm (wrt. thread data);
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Mar 29 19:14:08 2008 +0100
     1.2 +++ b/src/Pure/drule.ML	Sat Mar 29 19:14:09 2008 +0100
     1.3 @@ -160,9 +160,9 @@
     1.4    let val {T, thy, ...} = Thm.rep_ctyp cT
     1.5    in Thm.ctyp_of thy (f T) end;
     1.6  
     1.7 -val cert = cterm_of (Context.the_theory (Context.the_thread_data ()));
     1.8 +fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
     1.9  
    1.10 -val implies = cert Term.implies;
    1.11 +val implies = certify Term.implies;
    1.12  fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
    1.13  
    1.14  (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
    1.15 @@ -518,15 +518,19 @@
    1.16  
    1.17  (*** Meta-Rewriting Rules ***)
    1.18  
    1.19 -val read_prop = cert o SimpleSyntax.read_prop;
    1.20 +val read_prop = certify o SimpleSyntax.read_prop;
    1.21 +
    1.22 +fun store_thm name th =
    1.23 +  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
    1.24  
    1.25 -fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    1.26 -fun store_standard_thm name thm = store_thm name (standard thm);
    1.27 -fun store_thm_open name thm = hd (PureThy.smart_store_thms_open (name, [thm]));
    1.28 +fun store_thm_open name th =
    1.29 +  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
    1.30 +
    1.31 +fun store_standard_thm name th = store_thm name (standard th);
    1.32  fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
    1.33  
    1.34  val reflexive_thm =
    1.35 -  let val cx = cert (Var(("x",0),TVar(("'a",0),[])))
    1.36 +  let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
    1.37    in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
    1.38  
    1.39  val symmetric_thm =
    1.40 @@ -667,7 +671,7 @@
    1.41  val triv_forall_equality =
    1.42    let val V  = read_prop "V"
    1.43        and QV = read_prop "!!x::'a. V"
    1.44 -      and x  = cert (Free ("x", Term.aT []));
    1.45 +      and x  = certify (Free ("x", Term.aT []));
    1.46    in
    1.47      store_standard_thm_open "triv_forall_equality"
    1.48        (equal_intr (implies_intr QV (forall_elim x (assume QV)))
    1.49 @@ -743,10 +747,10 @@
    1.50      val phi = Free ("phi", propT);
    1.51      val psi = Free ("psi", aT --> propT);
    1.52  
    1.53 -    val cx = cert x;
    1.54 -    val cphi = cert phi;
    1.55 -    val lhs = cert (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0)));
    1.56 -    val rhs = cert (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0)));
    1.57 +    val cx = certify x;
    1.58 +    val cphi = certify phi;
    1.59 +    val lhs = certify (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0)));
    1.60 +    val rhs = certify (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0)));
    1.61    in
    1.62      Thm.equal_intr
    1.63        (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi)
    1.64 @@ -857,12 +861,12 @@
    1.65  (** protected propositions and embedded terms **)
    1.66  
    1.67  local
    1.68 -  val A = cert (Free ("A", propT));
    1.69 +  val A = certify (Free ("A", propT));
    1.70    val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ()));
    1.71    val prop_def = get_axiom "prop_def";
    1.72    val term_def = get_axiom "term_def";
    1.73  in
    1.74 -  val protect = Thm.capply (cert Logic.protectC);
    1.75 +  val protect = Thm.capply (certify Logic.protectC);
    1.76    val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
    1.77        (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
    1.78    val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
    1.79 @@ -900,7 +904,7 @@
    1.80  fun cterm_rule f = dest_term o f o mk_term;
    1.81  fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
    1.82  
    1.83 -val dummy_thm = mk_term (cert (Term.dummy_pattern propT));
    1.84 +val dummy_thm = mk_term (certify (Term.dummy_pattern propT));
    1.85  
    1.86  
    1.87