# HG changeset patch # User wenzelm # Date 1365592238 -7200 # Node ID 0d142a78fb7c70f883eb5484e3da5cefb8773555 # Parent d721d21e63746812bb8313c07520b39b3ee1688e formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context; diff -r d721d21e6374 -r 0d142a78fb7c src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Wed Apr 10 12:31:35 2013 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Wed Apr 10 13:10:38 2013 +0200 @@ -74,7 +74,7 @@ val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1 - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy + val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy (* transfer thms so that they will know about the new cpo instance *) val cpo_thms' = map (Thm.transfer thy) cpo_thms fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') @@ -113,7 +113,7 @@ val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy + val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy val pcpo_thms' = map (Thm.transfer thy) pcpo_thms fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') val Rep_strict = make @{thm typedef_Rep_strict} diff -r d721d21e6374 -r 0d142a78fb7c src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Apr 10 12:31:35 2013 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Apr 10 13:10:38 2013 +0200 @@ -518,7 +518,7 @@ in thy' |> AxClass.prove_arity (qu_name,[],[cls_name]) - (if ak_name = ak_name' then proof1 else proof2) + (fn _ => if ak_name = ak_name' then proof1 else proof2) end) ak_names thy) ak_names thy12d; (* show that *) @@ -537,7 +537,7 @@ val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst"); val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst"); - fun pt_proof thm = + fun pt_proof thm ctxt = EVERY [Class.intro_classes_tac [], rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; @@ -592,7 +592,7 @@ val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) in - AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' + AxClass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy' end) ak_names thy) ak_names thy18; (* shows that *) @@ -607,7 +607,7 @@ let val cls_name = Sign.full_bname thy ("fs_"^ak_name); val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); - fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; + fun fs_proof thm ctxt = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; val fs_thm_unit = fs_unit_inst; val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); @@ -669,7 +669,7 @@ EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] end)) in - AxClass.prove_arity (name,[],[cls_name]) proof thy'' + AxClass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy'' end) ak_names thy') ak_names thy) ak_names thy24; (* shows that *) @@ -689,7 +689,7 @@ val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); - fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; + fun cp_proof thm ctxt = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; val cp_thm_unit = cp_unit_inst; val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); @@ -722,7 +722,7 @@ val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn]; val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in - AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy + AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy end) ak_names; fun discrete_fs_inst discrete_ty defn = @@ -733,7 +733,7 @@ val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn]; val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in - AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy + AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy end) ak_names; fun discrete_cp_inst discrete_ty defn = @@ -744,7 +744,7 @@ val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn]; val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in - AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy + AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy end) ak_names)) ak_names; in diff -r d721d21e6374 -r 0d142a78fb7c src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Apr 10 12:31:35 2013 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Apr 10 13:10:38 2013 +0200 @@ -278,9 +278,9 @@ Const ("Nominal.perm", T) $ pi $ Free (x, T2)) end) (perm_names_types ~~ perm_indnames)))) - (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, + (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, ALLGOALS (asm_full_simp_tac - (global_simpset_of thy2 addsimps [perm_fun_def]))])), + (simpset_of ctxt addsimps [perm_fun_def]))])), length new_type_names)); (**** prove [] \ t = t ****) @@ -299,8 +299,8 @@ Free (x, T))) (perm_names ~~ map body_type perm_types ~~ perm_indnames))))) - (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])), + (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (simpset_of ctxt))])), length new_type_names)) end) atoms; @@ -334,8 +334,8 @@ end) (perm_names ~~ map body_type perm_types ~~ perm_indnames))))) - (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))), + (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (simpset_of ctxt addsimps [pt2', pt2_ax]))]))), length new_type_names) end) atoms; @@ -370,8 +370,8 @@ end) (perm_names ~~ map body_type perm_types ~~ perm_indnames)))))) - (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))), + (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (simpset_of ctxt addsimps [pt3', pt3_rev', pt3_ax]))]))), length new_type_names) end) atoms; @@ -393,7 +393,7 @@ val permT2 = mk_permT (Type (name2, [])); val Ts = map body_type perm_types; val cp_inst = cp_inst_of thy name1 name2; - val simps = global_simpset_of thy addsimps (perm_fun_def :: + fun simps ctxt = simpset_of ctxt addsimps (perm_fun_def :: (if name1 <> name2 then let val dj = dj_thm_of thy name2 name1 in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end @@ -422,12 +422,12 @@ perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T))) end) (perm_names ~~ Ts ~~ perm_indnames))))) - (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac simps)])) + (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (simps ctxt))])) in fold (fn (s, tvs) => fn thy => AxClass.prove_arity (s, map (inter_sort thy sort o snd) tvs, [cp_class]) - (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) + (fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) (full_new_type_names' ~~ tyvars) thy |> Theory.checkpoint end; @@ -439,7 +439,7 @@ in fold (fn (s, tvs) => fn thy => AxClass.prove_arity (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name]) - (EVERY + (fn _ => EVERY [Class.intro_classes_tac [], resolve_tac perm_empty_thms 1, resolve_tac perm_append_thms 1, @@ -561,9 +561,9 @@ S $ (Const ("Nominal.perm", permT --> T --> T) $ Free ("pi", permT) $ Free (x, T))) end) (rep_set_names'' ~~ recTs' ~~ perm_indnames'))))) - (fn _ => EVERY + (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac rep_induct [] 1, - ALLGOALS (simp_tac (global_simpset_of thy4 addsimps + ALLGOALS (simp_tac (simpset_of ctxt addsimps (Thm.symmetric perm_fun_def :: abs_perm))), ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])), length new_type_names)); @@ -621,10 +621,10 @@ in AxClass.prove_arity (Sign.intern_type thy name, map (inter_sort thy sort o snd) tvs, [pt_class]) - (EVERY [Class.intro_classes_tac [], + (fn ctxt => EVERY [Class.intro_classes_tac [], rewrite_goals_tac [perm_def], - asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1, - asm_full_simp_tac (global_simpset_of thy addsimps + asm_full_simp_tac (simpset_of ctxt addsimps [Rep_inverse]) 1, + asm_full_simp_tac (simpset_of ctxt addsimps [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy @@ -651,9 +651,9 @@ AxClass.prove_arity (Sign.intern_type thy name, map (inter_sort thy sort o snd) tvs, [cp_class]) - (EVERY [Class.intro_classes_tac [], + (fn ctxt => EVERY [Class.intro_classes_tac [], rewrite_goals_tac [perm_def], - asm_full_simp_tac (global_simpset_of thy addsimps + asm_full_simp_tac (simpset_of ctxt addsimps ((Rep RS perm_closed1 RS Abs_inverse) :: (if atom1 = atom2 then [] else [Rep RS perm_closed2 RS Abs_inverse]))) 1, @@ -841,8 +841,8 @@ fun prove_distinct_thms _ [] = [] | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) = let - val dist_thm = Goal.prove_global_future thy8 [] [] t (fn _ => - simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1) + val dist_thm = Goal.prove_global_future thy8 [] [] t (fn {context = ctxt, ...} => + simp_tac (simpset_of ctxt addsimps (dist_lemma :: rep_thms)) 1) in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove_distinct_thms p ts @@ -889,8 +889,8 @@ (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms)) (HOLogic.mk_Trueprop (HOLogic.mk_eq (perm (list_comb (c, l_args)), list_comb (c, r_args))))) - (fn _ => EVERY - [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1, + (fn {context = ctxt, ...} => EVERY + [simp_tac (simpset_of ctxt addsimps (constr_rep_thm :: perm_defs)) 1, simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @ constr_defs @ perm_closed_thms)) 1, TRY (simp_tac (HOL_basic_ss addsimps @@ -945,8 +945,8 @@ (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)), foldr1 HOLogic.mk_conj eqs)))) - (fn _ => EVERY - [asm_full_simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: + (fn {context = ctxt, ...} => EVERY + [asm_full_simp_tac (simpset_of ctxt addsimps (constr_rep_thm :: rep_inject_thms')) 1, TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def :: alpha @ abs_perm @ abs_fresh @ rep_inject_thms @ @@ -1075,8 +1075,8 @@ Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $ (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T))) (indnames ~~ recTs))))) - (fn _ => Datatype_Aux.ind_tac dt_induct indnames 1 THEN - ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps + (fn {context = ctxt, ...} => Datatype_Aux.ind_tac dt_induct indnames 1 THEN + ALLGOALS (asm_full_simp_tac (simpset_of ctxt addsimps (abs_supp @ supp_atm @ Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @ flat supp_thms))))), @@ -1107,7 +1107,7 @@ val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort)); in fold (fn Type (s, Ts) => AxClass.prove_arity (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class]) - (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy + (fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy end) (atoms ~~ finite_supp_thms) ||> Theory.checkpoint; diff -r d721d21e6374 -r 0d142a78fb7c src/Pure/axclass.ML --- a/src/Pure/axclass.ML Wed Apr 10 12:31:35 2013 +0200 +++ b/src/Pure/axclass.ML Wed Apr 10 13:10:38 2013 +0200 @@ -26,8 +26,8 @@ val define_overloaded: binding -> string * term -> theory -> thm * theory val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory - val prove_classrel: class * class -> tactic -> theory -> theory - val prove_arity: string * sort list * sort -> tactic -> theory -> theory + val prove_classrel: class * class -> (Proof.context -> tactic) -> theory -> theory + val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory val define_class: binding * class list -> string list -> (Thm.binding * term list) list -> theory -> class * theory val axiomatize_class: binding * class list -> theory -> theory @@ -439,9 +439,11 @@ let val ctxt = Proof_Context.init_global thy; val (c1, c2) = cert_classrel thy raw_rel; - val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg => - cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ - quote (Syntax.string_of_classrel ctxt [c1, c2])); + val th = + Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (fn {context, ...} => tac context) + handle ERROR msg => + cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ + quote (Syntax.string_of_classrel ctxt [c1, c2])); in thy |> add_classrel th end; @@ -452,10 +454,12 @@ val arity = Proof_Context.cert_arity ctxt raw_arity; val names = map (prefix arity_prefix) (Logic.name_arities arity); val props = Logic.mk_arities arity; - val ths = Goal.prove_multi ctxt [] [] props - (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => - cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ - quote (Syntax.string_of_arity ctxt arity)); + val ths = + Goal.prove_multi ctxt [] [] props + (fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context) + handle ERROR msg => + cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ + quote (Syntax.string_of_arity ctxt arity)); in thy |> fold add_arity ths end;