clarified context;
authorwenzelm
Fri Mar 06 23:57:01 2015 +0100 (2015-03-06)
changeset 59643f3be9235503d
parent 59642 929984c529d3
child 59644 cc78fd8d955d
clarified context;
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/Countable.thy
src/HOL/NSA/transfer.ML
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Word/WordBitwise.thy
src/HOL/ex/SAT_Examples.thy
src/HOL/ex/SVC_Oracle.thy
     1.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Mar 06 23:56:43 2015 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Mar 06 23:57:01 2015 +0100
     1.3 @@ -121,8 +121,7 @@
     1.4  local
     1.5    fun solve_cont ctxt t =
     1.6      let
     1.7 -      val thy = Proof_Context.theory_of ctxt
     1.8 -      val tr = instantiate' [] [SOME (Thm.global_cterm_of thy t)] @{thm Eq_TrueI}
     1.9 +      val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
    1.10      in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
    1.11  in
    1.12    fun cont_proc thy =
     2.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:56:43 2015 +0100
     2.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:57:01 2015 +0100
     2.3 @@ -56,10 +56,9 @@
     2.4  
     2.5  fun remove_suc ctxt thms =
     2.6    let
     2.7 -    val thy = Proof_Context.theory_of ctxt;
     2.8      val vname = singleton (Name.variant_list (map fst
     2.9        (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    2.10 -    val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT));
    2.11 +    val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
    2.12      val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
    2.13      val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
    2.14      fun find_vars ct = (case Thm.term_of ct of
     3.1 --- a/src/HOL/Library/Countable.thy	Fri Mar 06 23:56:43 2015 +0100
     3.2 +++ b/src/HOL/Library/Countable.thy	Fri Mar 06 23:57:01 2015 +0100
     3.3 @@ -180,8 +180,7 @@
     3.4          val alist = pred_names ~~ induct_thms
     3.5          val induct_thm = the (AList.lookup (op =) alist pred_name)
     3.6          val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
     3.7 -        val thy = Proof_Context.theory_of ctxt
     3.8 -        val insts = vars |> map (fn (_, T) => try (Thm.global_cterm_of thy)
     3.9 +        val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
    3.10            (Const (@{const_name Countable.finite_item}, T)))
    3.11          val induct_thm' = Drule.instantiate' [] insts induct_thm
    3.12          val rules = @{thms finite_item.intros}
     4.1 --- a/src/HOL/NSA/transfer.ML	Fri Mar 06 23:56:43 2015 +0100
     4.2 +++ b/src/HOL/NSA/transfer.ML	Fri Mar 06 23:57:01 2015 +0100
     4.3 @@ -52,12 +52,11 @@
     4.4  
     4.5  fun transfer_thm_of ctxt ths t =
     4.6    let
     4.7 -    val thy = Proof_Context.theory_of ctxt;
     4.8      val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
     4.9      val meta = Local_Defs.meta_rewrite_rule ctxt;
    4.10      val ths' = map meta ths;
    4.11      val unfolds' = map meta unfolds and refolds' = map meta refolds;
    4.12 -    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.global_cterm_of thy t))
    4.13 +    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
    4.14      val u = unstar_term consts t'
    4.15      val tac =
    4.16        rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
     5.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Mar 06 23:56:43 2015 +0100
     5.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Mar 06 23:57:01 2015 +0100
     5.3 @@ -433,11 +433,11 @@
     5.4  
     5.5  val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
     5.6  val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
     5.7 -val ct1' = Thm.global_cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
     5.8 +val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
     5.9  
    5.10  val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
    5.11  val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
    5.12 -val ct2' = Thm.global_cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
    5.13 +val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
    5.14  *}
    5.15  
    5.16  end
     6.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Mar 06 23:56:43 2015 +0100
     6.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Mar 06 23:57:01 2015 +0100
     6.3 @@ -53,26 +53,24 @@
     6.4  val lazy_conj_simproc =
     6.5    Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     6.6      (fn ctxt => fn t =>
     6.7 -      let val thy = Proof_Context.theory_of ctxt in
     6.8 -        (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
     6.9 -          let
    6.10 -            val P_P' = Simplifier.rewrite ctxt (Thm.global_cterm_of thy P);
    6.11 -            val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
    6.12 -          in
    6.13 -            if isFalse P' then SOME (conj1_False OF [P_P'])
    6.14 -            else
    6.15 -              let
    6.16 -                val Q_Q' = Simplifier.rewrite ctxt (Thm.global_cterm_of thy Q);
    6.17 -                val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
    6.18 -              in
    6.19 -                if isFalse Q' then SOME (conj2_False OF [Q_Q'])
    6.20 -                else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
    6.21 -                else if P aconv P' andalso Q aconv Q' then NONE
    6.22 -                else SOME (conj_cong OF [P_P', Q_Q'])
    6.23 -              end
    6.24 -           end
    6.25 -        | _ => NONE)
    6.26 -      end);
    6.27 +      (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
    6.28 +        let
    6.29 +          val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P);
    6.30 +          val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
    6.31 +        in
    6.32 +          if isFalse P' then SOME (conj1_False OF [P_P'])
    6.33 +          else
    6.34 +            let
    6.35 +              val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q);
    6.36 +              val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
    6.37 +            in
    6.38 +              if isFalse Q' then SOME (conj2_False OF [Q_Q'])
    6.39 +              else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
    6.40 +              else if P aconv P' andalso Q aconv Q' then NONE
    6.41 +              else SOME (conj_cong OF [P_P', Q_Q'])
    6.42 +            end
    6.43 +         end
    6.44 +      | _ => NONE));
    6.45  
    6.46  fun string_eq_simp_tac ctxt =
    6.47    simp_tac (put_simpset HOL_basic_ss ctxt
    6.48 @@ -113,7 +111,6 @@
    6.49        (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
    6.50                     (s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) =>
    6.51          (let
    6.52 -          val thy = Proof_Context.theory_of ctxt;
    6.53            val (_::_::_::_::sT::_) = binder_types uT;
    6.54            val mi = maxidx_of_term t;
    6.55            fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) =
    6.56 @@ -141,7 +138,8 @@
    6.57              | mk_upds s = (Var (("s", mi + 1), sT), mi + 2);
    6.58  
    6.59            val ct =
    6.60 -            Thm.global_cterm_of thy (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
    6.61 +            Thm.cterm_of ctxt
    6.62 +              (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
    6.63            val basic_ss = #1 (Data.get (Context.Proof ctxt));
    6.64            val ctxt' = ctxt |> Config.put simp_depth_limit 100 |> put_simpset basic_ss;
    6.65            val thm = Simplifier.rewrite ctxt' ct;
     7.1 --- a/src/HOL/Word/WordBitwise.thy	Fri Mar 06 23:56:43 2015 +0100
     7.2 +++ b/src/HOL/Word/WordBitwise.thy	Fri Mar 06 23:57:01 2015 +0100
     7.3 @@ -550,7 +550,6 @@
     7.4  
     7.5  fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
     7.6    let
     7.7 -    val thy = Proof_Context.theory_of ctxt;
     7.8      val (f $ arg) = Thm.term_of ct;
     7.9      val n = (case arg of @{term nat} $ n => n | n => n)
    7.10        |> HOLogic.dest_number |> snd;
    7.11 @@ -560,7 +559,7 @@
    7.12          (replicate i @{term Suc});
    7.13      val _ = if arg = arg' then raise TERM ("", []) else ();
    7.14      fun propfn g = HOLogic.mk_eq (g arg, g arg')
    7.15 -      |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy;
    7.16 +      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
    7.17      val eq1 = Goal.prove_internal ctxt [] (propfn I)
    7.18        (K (simp_tac (put_simpset word_ss ctxt) 1));
    7.19    in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
     8.1 --- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 06 23:56:43 2015 +0100
     8.2 +++ b/src/HOL/ex/SAT_Examples.thy	Fri Mar 06 23:57:01 2015 +0100
     8.3 @@ -534,7 +534,7 @@
     8.4          | and_to_list fm acc = rev (fm :: acc)
     8.5        val clauses = and_to_list prop_fm []
     8.6        val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
     8.7 -      val cterms = map (Thm.global_cterm_of @{theory}) terms
     8.8 +      val cterms = map (Thm.cterm_of @{context}) terms
     8.9        val start = Timing.start ()
    8.10        val _ = SAT.rawsat_thm @{context} cterms
    8.11      in
     9.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Mar 06 23:56:43 2015 +0100
     9.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Mar 06 23:57:01 2015 +0100
     9.3 @@ -111,9 +111,8 @@
     9.4  
     9.5  fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
     9.6    let
     9.7 -    val thy = Thm.theory_of_cterm ct;
     9.8      val (abs_goal, _) = svc_abstract (Thm.term_of ct);
     9.9 -    val th = svc_oracle (Thm.global_cterm_of thy abs_goal);
    9.10 +    val th = svc_oracle (Thm.cterm_of ctxt abs_goal);
    9.11     in compose_tac ctxt (false, th, 0) i end
    9.12     handle TERM _ => no_tac);
    9.13  *}