src/HOL/Nominal/nominal_datatype.ML
changeset 54742 7a86358a3c0b
parent 52788 da1fdbfebd39
child 54895 515630483010
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4  val at_fin_set_fresh = @{thm at_fin_set_fresh};
     1.5  val abs_fun_eq1 = @{thm abs_fun_eq1};
     1.6  
     1.7 -val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
     1.8 +fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
     1.9  
    1.10  fun mk_perm Ts t u =
    1.11    let
    1.12 @@ -595,10 +595,12 @@
    1.13          end))
    1.14          (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
    1.15  
    1.16 +    val ctxt6 = Proof_Context.init_global thy6;
    1.17 +
    1.18      val perm_defs = map snd typedefs;
    1.19 -    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
    1.20 +    val Abs_inverse_thms = map (collect_simp ctxt6 o #Abs_inverse o snd o fst) typedefs;
    1.21      val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
    1.22 -    val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
    1.23 +    val Rep_thms = map (collect_simp ctxt6 o #Rep o snd o fst) typedefs;
    1.24  
    1.25  
    1.26      (** prove that new types are in class pt_<name> **)
    1.27 @@ -616,7 +618,7 @@
    1.28              (Sign.intern_type thy name,
    1.29                map (inter_sort thy sort o snd) tvs, [pt_class])
    1.30              (fn ctxt => EVERY [Class.intro_classes_tac [],
    1.31 -              rewrite_goals_tac [perm_def],
    1.32 +              rewrite_goals_tac ctxt [perm_def],
    1.33                asm_full_simp_tac (ctxt addsimps [Rep_inverse]) 1,
    1.34                asm_full_simp_tac (ctxt addsimps
    1.35                  [Rep RS perm_closed RS Abs_inverse]) 1,
    1.36 @@ -645,7 +647,7 @@
    1.37              (Sign.intern_type thy name,
    1.38                map (inter_sort thy sort o snd) tvs, [cp_class])
    1.39              (fn ctxt => EVERY [Class.intro_classes_tac [],
    1.40 -              rewrite_goals_tac [perm_def],
    1.41 +              rewrite_goals_tac ctxt [perm_def],
    1.42                asm_full_simp_tac (ctxt addsimps
    1.43                  ((Rep RS perm_closed1 RS Abs_inverse) ::
    1.44                   (if atom1 = atom2 then []
    1.45 @@ -783,7 +785,7 @@
    1.46          new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
    1.47        (thy7, [], [], []);
    1.48  
    1.49 -    val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
    1.50 +    val abs_inject_thms = map (collect_simp ctxt6 o #Abs_inject o snd o fst) typedefs
    1.51      val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
    1.52  
    1.53      (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
    1.54 @@ -792,9 +794,9 @@
    1.55        let
    1.56          val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
    1.57          val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
    1.58 -      in Goal.prove_global_future thy8 [] [] eqn (fn _ => EVERY
    1.59 +      in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY
    1.60          [resolve_tac inj_thms 1,
    1.61 -         rewrite_goals_tac rewrites,
    1.62 +         rewrite_goals_tac ctxt rewrites,
    1.63           rtac refl 3,
    1.64           resolve_tac rep_intrs 2,
    1.65           REPEAT (resolve_tac Rep_thms 1)])
    1.66 @@ -1043,7 +1045,7 @@
    1.67        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    1.68        (fn {prems, context = ctxt} => EVERY
    1.69          [rtac indrule_lemma' 1,
    1.70 -         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
    1.71 +         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
    1.72           EVERY (map (fn (prem, r) => (EVERY
    1.73             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
    1.74              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
    1.75 @@ -2017,8 +2019,8 @@
    1.76          Goal.prove_global_future thy12 []
    1.77            (map (augment_sort thy12 fs_cp_sort) prems')
    1.78            (augment_sort thy12 fs_cp_sort concl')
    1.79 -          (fn {prems, ...} => EVERY
    1.80 -            [rewrite_goals_tac reccomb_defs,
    1.81 +          (fn {context = ctxt, prems} => EVERY
    1.82 +            [rewrite_goals_tac ctxt reccomb_defs,
    1.83               rtac @{thm the1_equality} 1,
    1.84               solve rec_unique_thms prems 1,
    1.85               resolve_tac rec_intrs 1,