clarified context;
authorwenzelm
Tue Jun 02 09:40:04 2015 +0200 (2015-06-02)
changeset 60359cb8828b859a1
parent 60358 aebfbcab1eb8
child 60360 f585b1f0b4c3
clarified context;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jun 02 09:16:19 2015 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Jun 02 09:40:04 2015 +0200
     1.3 @@ -120,8 +120,8 @@
     1.4  val perm_simproc =
     1.5    Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
     1.6  
     1.7 -fun projections rule =
     1.8 -  Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule
     1.9 +fun projections ctxt rule =
    1.10 +  Project_Rule.projections ctxt rule
    1.11    |> map (Drule.export_without_context #> Rule_Cases.save rule);
    1.12  
    1.13  val supp_prod = @{thm supp_prod};
    1.14 @@ -1114,7 +1114,9 @@
    1.15      val (_, thy9) = thy8 |>
    1.16        Sign.add_path big_name |>
    1.17        Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
    1.18 -      Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
    1.19 +      Global_Theory.add_thmss
    1.20 +        [((Binding.name "inducts", projections (Proof_Context.init_global thy8) dt_induct),
    1.21 +            [case_names_induct])] ||>
    1.22        Sign.parent_path ||>>
    1.23        Old_Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
    1.24        Old_Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
    1.25 @@ -1412,7 +1414,9 @@
    1.26        Sign.add_path big_name |>
    1.27        Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
    1.28        Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
    1.29 -      Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
    1.30 +      Global_Theory.add_thmss
    1.31 +        [((Binding.name "strong_inducts", projections (Proof_Context.init_global thy9) induct),
    1.32 +            [case_names_induct])];
    1.33  
    1.34      (**** recursion combinator ****)
    1.35  
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Jun 02 09:16:19 2015 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Jun 02 09:40:04 2015 +0200
     2.3 @@ -145,10 +145,11 @@
     2.4      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
     2.5      fun inst_fresh vars params i st =
     2.6     let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
     2.7 -       val thy = Thm.theory_of_thm st;
     2.8     in case subtract (op =) vars vars' of
     2.9       [x] =>
    2.10 -      Seq.single (Thm.instantiate ([], [(Thm.global_cterm_of thy x, Thm.global_cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    2.11 +      Seq.single
    2.12 +        (Thm.instantiate ([],
    2.13 +          [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st)
    2.14      | _ => error "fresh_fun_simp: Too many variables, please report."
    2.15     end
    2.16    in
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jun 02 09:16:19 2015 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jun 02 09:40:04 2015 +0200
     3.3 @@ -39,8 +39,8 @@
     3.4  fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
     3.5    [(perm_boolI_pi, pi)] perm_boolI;
     3.6  
     3.7 -fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
     3.8 -  (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     3.9 +fun mk_perm_bool_simproc names =
    3.10 +  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
    3.11      fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    3.12           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    3.13           then SOME perm_bool else NONE
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jun 02 09:16:19 2015 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jun 02 09:40:04 2015 +0200
     4.3 @@ -43,8 +43,8 @@
     4.4  fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
     4.5    [(perm_boolI_pi, pi)] perm_boolI;
     4.6  
     4.7 -fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
     4.8 -  (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     4.9 +fun mk_perm_bool_simproc names =
    4.10 +  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
    4.11      fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    4.12           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    4.13           then SOME perm_bool else NONE
     5.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Tue Jun 02 09:16:19 2015 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Jun 02 09:40:04 2015 +0200
     5.3 @@ -70,11 +70,6 @@
     5.4  val perm_aux_fold       = @{thm "perm_aux_fold"}; 
     5.5  val supports_fresh_rule = @{thm "supports_fresh"};
     5.6  
     5.7 -(* pulls out dynamically a thm via the proof state *)
     5.8 -fun dynamic_thms st name = Global_Theory.get_thms (Thm.theory_of_thm st) name;
     5.9 -fun dynamic_thm  st name = Global_Theory.get_thm  (Thm.theory_of_thm st) name;
    5.10 -
    5.11 -
    5.12  (* needed in the process of fully simplifying permutations *)
    5.13  val strong_congs = [@{thm "if_cong"}]
    5.14  (* needed to avoid warnings about overwritten congs *)
    5.15 @@ -146,7 +141,7 @@
    5.16      ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
    5.17      let
    5.18         val ctxt' = ctxt
    5.19 -         addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
    5.20 +         addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
    5.21           addsimprocs [perm_simproc_fun, perm_simproc_app]
    5.22           |> fold Simplifier.del_cong weak_congs
    5.23           |> fold Simplifier.add_cong strong_congs
    5.24 @@ -296,7 +291,6 @@
    5.25        case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of
    5.26            _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
    5.27            let
    5.28 -            val cert = Thm.global_cterm_of (Thm.theory_of_thm st);
    5.29              val ps = Logic.strip_params (Thm.term_of goal);
    5.30              val Ts = rev (map snd ps);
    5.31              val vs = collect_vars 0 x [];
    5.32 @@ -310,8 +304,8 @@
    5.33              val _ $ (_ $ S $ _) =
    5.34                Logic.strip_assums_concl (hd (Thm.prems_of supports_rule'));
    5.35              val supports_rule'' = Drule.cterm_instantiate
    5.36 -              [(cert (head_of S), cert s')] supports_rule'
    5.37 -            val fin_supp = dynamic_thms st ("fin_supp")
    5.38 +              [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_rule'
    5.39 +            val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
    5.40              val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    5.41            in
    5.42              (tactical ctxt ("guessing of the right supports-set",
    5.43 @@ -332,15 +326,14 @@
    5.44  fun fresh_guess_tac_i tactical ctxt i st =
    5.45      let 
    5.46          val goal = nth (cprems_of st) (i - 1)
    5.47 -        val fin_supp = dynamic_thms st ("fin_supp")
    5.48 -        val fresh_atm = dynamic_thms st ("fresh_atm")
    5.49 +        val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
    5.50 +        val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
    5.51          val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
    5.52          val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    5.53      in
    5.54        case Logic.strip_assums_concl (Thm.term_of goal) of
    5.55            _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => 
    5.56            let
    5.57 -            val cert = Thm.global_cterm_of (Thm.theory_of_thm st);
    5.58              val ps = Logic.strip_params (Thm.term_of goal);
    5.59              val Ts = rev (map snd ps);
    5.60              val vs = collect_vars 0 t [];
    5.61 @@ -354,7 +347,7 @@
    5.62              val _ $ (_ $ S $ _) =
    5.63                Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule'));
    5.64              val supports_fresh_rule'' = Drule.cterm_instantiate
    5.65 -              [(cert (head_of S), cert s')] supports_fresh_rule'
    5.66 +              [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_fresh_rule'
    5.67            in
    5.68              (tactical ctxt ("guessing of the right set that supports the goal", 
    5.69                        (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,