# HG changeset patch # User Christian Urban # Date 1436405566 -3600 # Node ID 67370521c09ce40a5040e866835386c8db92da09 # Parent b2e1a7b83e05d5f9f201297d9c828460bc271965 updated for Isabelle 2015 diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/Ex/Lambda.thy Thu Jul 09 02:32:46 2015 +0100 @@ -12,6 +12,16 @@ atom_decl name +thm obtain_atom + +lemma + "(\thesis. (finite X \ (\a. ((a \ X \ sort_of a = s) \ thesis)) \ thesis)) \ + (finite X \ (\ a. (a \ X \ sort_of a = s)))" +apply(auto) +done + + + ML {* trace := true *} nominal_datatype lam = @@ -19,6 +29,24 @@ | App "lam" "lam" | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) +nominal_datatype environment = + Ni + | En name closure environment +and closure = + Clos "lam" "environment" + +thm environment_closure.exhaust(1) + +nominal_function + env_lookup :: "environment => name => closure" +where + "env_lookup Ni x = Clos (Var x) Ni" +| "env_lookup (En v clos rest) x = (if (v = x) then clos else env_lookup rest x)" + apply (auto) + apply (simp add: env_lookup_graph_aux_def eqvt_def) + by (metis environment_closure.strong_exhaust(1)) + + lemma "Lam [x]. Var x = Lam [y]. Var y" proof - @@ -232,6 +260,16 @@ section {* free name function *} + +lemma fresh_removeAll_name: + fixes x::"name" + and xs:: "name list" + shows "atom x \ (removeAll y xs) \ (atom x \ xs \ x = y)" + apply (induct xs) + apply(auto simp add: fresh_def supp_Nil supp_Cons supp_at_base) + done + + text {* first returns an atom list *} nominal_function diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/Ex/TypeVarsTest.thy Thu Jul 09 02:32:46 2015 +0100 @@ -2,6 +2,37 @@ imports "../Nominal2" begin +atom_decl var + +ML {* trace := true *} +declare [[ML_print_depth = 1000]] + +nominal_datatype exp = + Var var + | App exp var + | LetA as::assn body::exp binds "bn as" in "body" "as" + | Lam x::var body::exp binds x in body + and assn = + ANil | ACons var exp assn + binder + bn + where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)" + +nominal_datatype ('ann::fs) exp2 = + Var var +| App "'ann exp2" var +| LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as +| Lam x::var body::"'ann exp2" binds x in body +and ('ann::fs) assn2 = + ANil +| ACons var "'ann exp2" 'ann "'ann assn2" +binder + bnn :: "('ann::fs) assn2 \ atom list" +where + "bnn ANil = []" +| "bnn (ACons x a t as) = (atom x) # (bnn as)" + + (* a nominal datatype with type variables and sorts *) @@ -54,7 +85,6 @@ - end diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/Nominal2.thy Thu Jul 09 02:32:46 2015 +0100 @@ -149,7 +149,7 @@ val bn_fun_strs = get_bn_fun_strs bn_funs val bn_fun_strs' = add_raws bn_fun_strs val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' - val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) + val bn_fun_full_env = map (apply2 (Long_Name.qualify thy_name)) (bn_fun_strs ~~ bn_fun_strs') val raw_dts = rawify_dts dts dts_env @@ -157,14 +157,14 @@ val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses val (raw_full_dt_names', thy1) = - Datatype.add_datatype Datatype.default_config raw_dts thy + Old_Datatype.add_datatype Old_Datatype_Aux.default_config raw_dts thy val lthy1 = Named_Target.theory_init thy1 - val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' + val dtinfos = map (Old_Datatype_Data.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' val {descr, ...} = hd dtinfos - val raw_tys = Datatype_Aux.get_rec_types descr + val raw_tys = Old_Datatype_Aux.get_rec_types descr val raw_ty_args = hd raw_tys |> snd o dest_Type |> map dest_TFree @@ -179,7 +179,7 @@ val raw_exhaust_thms = map #exhaust dtinfos val raw_size_trms = map HOLogic.size_const raw_tys val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd) - (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names'))) + (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names'))) val raw_result = RawDtInfo {raw_dt_names = raw_full_dt_names', @@ -303,7 +303,7 @@ val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux fun match_const cnst th = - (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = + (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o Thm.prop_of) th = fst (dest_Const cnst); fun find_matching_rsp cnst = hd (filter (fn th => match_const cnst th) raw_funs_rsp); @@ -398,7 +398,7 @@ val qperm_bns = map #qconst qperm_bns_info val _ = trace_msg (K "Lifting of theorems...") - val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def + val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_sel prod.case} val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, @@ -452,7 +452,7 @@ val qsupp_constrs = qfv_defs |> map (simplify (put_simpset HOL_basic_ss lthyC - addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) + addsimps (filter (is_qfv_thm o Thm.prop_of) qfv_supp_thms))) val transform_thm = @{lemma "x = y \ a \ x \ a \ y" by simp} val transform_thms = @@ -548,7 +548,7 @@ ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx'))) val (dts, spec_ctxt) = - Datatype.read_specs (map prep_spec dt_strs) thy + Old_Datatype.read_specs (map prep_spec dt_strs) thy fun augment ((tname, tvs, mx), constrs) = ((tname, map (apsnd (augment_sort thy)) tvs, mx), @@ -736,10 +736,9 @@ end (* Command Keyword *) -val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} +val _ = Outer_Syntax.local_theory @{command_keyword nominal_datatype} "declaration of nominal datatypes" (main_parser >> nominal_datatype2_cmd) *} - end diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/Nominal2_Abs.thy Thu Jul 09 02:32:46 2015 +0100 @@ -923,15 +923,15 @@ ML {* fun alpha_single_simproc thm _ ctxt ctrm = - let + let val thy = Proof_Context.theory_of ctxt - val _ $ (_ $ x) $ (_ $ y) = term_of ctrm + val _ $ (_ $ x) $ (_ $ y) = Thm.term_of ctrm val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) |> map Free |> HOLogic.mk_tuple - |> Thm.cterm_of thy - val cvrs_ty = ctyp_of_term cvrs + |> Thm.cterm_of ctxt + val cvrs_ty = Thm.ctyp_of_cterm cvrs val thm' = thm |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] in @@ -1050,7 +1050,6 @@ lemma [quot_respect]: shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv" unfolding rel_fun_def - unfolding rel_prod_def by auto lemma [quot_preserve]: @@ -1067,7 +1066,7 @@ lemma [eqvt]: shows "p \ prod_alpha A B x y = prod_alpha (p \ A) (p \ B) (p \ x) (p \ y)" unfolding prod_alpha_def - unfolding rel_prod_def + unfolding rel_prod_conv by (perm_simp) (rule refl) lemma [eqvt]: diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/Nominal2_Base.thy Thu Jul 09 02:32:46 2015 +0100 @@ -5,7 +5,7 @@ Nominal Isabelle. *) theory Nominal2_Base -imports Main +imports "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/FinFun" @@ -769,9 +769,8 @@ subsection {* Eqvt infrastructure *} text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw}. *} - + ML_file "nominal_thmdecls.ML" -setup "Nominal_ThmDecls.setup" lemmas [eqvt] = @@ -823,7 +822,7 @@ {* pushes permutations inside, raises an error if it cannot solve all permutations. *} simproc_setup perm_simproc ("p \ t") = {* fn _ => fn ctxt => fn ctrm => - case term_of (Thm.dest_arg ctrm) of + case Thm.term_of (Thm.dest_arg ctrm) of Free _ => NONE | Var _ => NONE | Const (@{const_name permute}, _) $ _ $ _ => NONE @@ -891,14 +890,14 @@ shows "p \ (A \ B) \ (p \ A) \ (p \ B)" by (simp add: permute_bool_def) -declare imp_eqvt[folded induct_implies_def, eqvt] +declare imp_eqvt[folded HOL.induct_implies_def, eqvt] lemma all_eqvt [eqvt]: shows "p \ (\x. P x) = (\x. (p \ P) x)" unfolding All_def by (perm_simp) (rule refl) -declare all_eqvt[folded induct_forall_def, eqvt] +declare all_eqvt[folded HOL.induct_forall_def, eqvt] lemma ex_eqvt [eqvt]: shows "p \ (\x. P x) = (\x. (p \ P) x)" @@ -1885,17 +1884,18 @@ simproc_setup fresh_fun_simproc ("a \ (f::'a::pt \'b::pt)") = {* fn _ => fn ctxt => fn ctrm => let - val _ $ _ $ f = term_of ctrm + val _ $ _ $ f = Thm.term_of ctrm in case (Term.add_frees f [], Term.add_vars f []) of ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) - | (x::_, []) => let - val thy = Proof_Context.theory_of ctxt - val argx = Free x - val absf = absfree x f - val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))] - val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)] - val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} + | (x::_, []) => + let + val argx = Free x + val absf = absfree x f + val cty_inst = + [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))] + val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)] + val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} in SOME(thm RS @{thm Eq_TrueI}) end @@ -2952,7 +2952,7 @@ simproc_setup fresh_ineq ("x \ (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => - case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => + case Thm.term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => let fun first_is_neg lhs rhs [] = NONE | first_is_neg lhs rhs (thm::thms) = @@ -2973,8 +2973,8 @@ member (op=) atms lhs andalso member (op=) atms rhs end) | _ => false) - |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) - |> map HOLogic.conj_elims + |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) + |> map (HOLogic.conj_elims ctxt) |> flat in case first_is_neg lhs rhs prems of @@ -3353,7 +3353,7 @@ simproc_setup Fresh_simproc ("Fresh (h::'a::at \ 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => let - val _ $ h = term_of ctrm + val _ $ h = Thm.term_of ctrm val cfresh = @{const_name fresh} val catom = @{const_name atom} diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_atoms.ML --- a/Nominal/nominal_atoms.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_atoms.ML Thu Jul 09 02:32:46 2015 +0100 @@ -28,14 +28,13 @@ fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = let - val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic"; val str = Sign.full_name thy name; (* typedef *) val set = atom_decl_set str; - val tac = rtac @{thm exists_eq_simple_sort} 1; - val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = - Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy; + fun tac _ = rtac @{thm exists_eq_simple_sort} 1; + val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = + Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy; (* definition of atom and permute *) val newT = #abs_type (fst info); @@ -77,7 +76,7 @@ (** outer syntax **) val _ = - Outer_Syntax.command @{command_spec "atom_decl"} + Outer_Syntax.command @{command_keyword atom_decl} "declaration of a concrete atom type" ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >> (Toplevel.theory o add_atom_decl)) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_dt_alpha.ML Thu Jul 09 02:32:46 2015 +0100 @@ -162,7 +162,7 @@ (* produces the introduction rule for an alpha rule *) fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = let - val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) @@ -205,7 +205,7 @@ fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = let - val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) @@ -315,14 +315,14 @@ HEADGOAL (DETERM o (rtac induct_thm) THEN_ALL_NEW - (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt]))) + (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm - |> map Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm + |> map Old_Datatype_Aux.split_conj_thm |> flat - |> filter_out (is_true o concl_of) + |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end @@ -365,11 +365,11 @@ in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm |> map (fn th => th RS mp) - |> map Datatype_Aux.split_conj_thm + |> map Old_Datatype_Aux.split_conj_thm |> flat - |> filter_out (is_true o concl_of) + |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end @@ -392,7 +392,7 @@ end fun distinct_tac ctxt cases_thms distinct_thms = - rtac notI THEN' eresolve_tac cases_thms + rtac notI THEN' eresolve_tac ctxt cases_thms THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = @@ -410,7 +410,7 @@ (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) end in - map (mk_alpha_distinct o prop_of) raw_distinct_thms + map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms end @@ -421,19 +421,19 @@ rewritten to ((Rel Const = Const) = True) *) fun mk_simp_rule thm = - case (prop_of thm) of + case Thm.prop_of thm of @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} | _ => thm fun alpha_eq_iff_tac ctxt dist_inj intros elims = SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' (rtac @{thm iffI} THEN' - RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), + RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) fun mk_alpha_eq_iff_goal thm = let - val prop = prop_of thm; + val prop = Thm.prop_of thm; val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); fun list_conj l = foldr1 HOLogic.mk_conj l; @@ -463,16 +463,16 @@ fun cases_tac intros ctxt = let - val prod_simps = @{thms split_conv prod_alpha_def rel_prod_def} + val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} - val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac + val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt val bound_tac = EVERY' [ rtac exi_zero, - resolve_tac @{thms alpha_refl}, + resolve_tac ctxt @{thms alpha_refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] in - resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] + resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] end fun raw_prove_refl ctxt alpha_result raw_dt_induct = @@ -502,13 +502,13 @@ let val prems' = map (transform_prem1 context pred_names) prems in - resolve_tac prems' 1 + resolve_tac ctxt prems' 1 end) ctxt - val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_def alphas} + val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} in EVERY' [ etac exi_neg, - resolve_tac @{thms alpha_sym_eqvt}, + resolve_tac ctxt @{thms alpha_sym_eqvt}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, trans_prem_tac pred_names ctxt] @@ -525,8 +525,10 @@ val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms fun tac ctxt = - resolve_tac alpha_intros THEN_ALL_NEW - FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] + resolve_tac ctxt alpha_intros THEN_ALL_NEW + FIRST' [assume_tac ctxt, + rtac @{thm sym} THEN' assume_tac ctxt, + prem_bound_tac alpha_names alpha_eqvt ctxt] in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt end @@ -536,18 +538,18 @@ (* applies cases rules and resolves them with the last premise *) fun ecases_tac cases = - Subgoal.FOCUS (fn {prems, ...} => - HEADGOAL (resolve_tac cases THEN' rtac (List.last prems))) + Subgoal.FOCUS (fn {context = ctxt, prems, ...} => + HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems))) fun aatac pred_names = - SUBPROOF (fn {prems, context, ...} => - HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems))) + SUBPROOF (fn {context = ctxt, prems, ...} => + HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) (* instantiates exI with the permutation p + q *) val perm_inst_tac = Subgoal.FOCUS (fn {params, ...} => let - val (p, q) = pairself snd (last2 params) + val (p, q) = apply2 snd (last2 params) val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} in @@ -556,16 +558,16 @@ fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let - val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_def} + val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} in - resolve_tac intros + resolve_tac ctxt intros THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' TRY o EVERY' (* if binders are present *) [ etac @{thm exE}, etac @{thm exE}, perm_inst_tac ctxt, - resolve_tac @{thms alpha_trans_eqvt}, - atac, + resolve_tac ctxt @{thms alpha_trans_eqvt}, + assume_tac ctxt, aatac pred_names ctxt, eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) @@ -630,9 +632,9 @@ fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in - Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) + Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' - RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) + RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) |> chop (length alpha_trms) end @@ -644,16 +646,16 @@ let val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result - val prems' = flat (map Datatype_Aux.split_conj_thm prems) + val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 context alpha_names) prems' in HEADGOAL (REPEAT_ALL_NEW (FIRST' [ rtac @{thm TrueI}, rtac @{thm conjI}, - resolve_tac prems', - resolve_tac prems'', - resolve_tac alpha_intros ])) + resolve_tac ctxt prems', + resolve_tac ctxt prems'', + resolve_tac ctxt alpha_intros ])) end) ctxt @@ -706,7 +708,7 @@ val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val simpset = - put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_def + put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv permute_prod_def prod.case prod.rec}) val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset @@ -720,12 +722,12 @@ fun raw_constr_rsp_tac ctxt alpha_intros simps = let val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def} - val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_def + val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps in asm_full_simp_tac pre_simpset - THEN' REPEAT o (resolve_tac @{thms allI impI}) - THEN' resolve_tac alpha_intros + THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) + THEN' resolve_tac ctxt alpha_intros THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset) end @@ -752,7 +754,7 @@ |> HOLogic.mk_Trueprop in map (fn constrs => - Goal.prove_multi ctxt [] [] (map prep_goal constrs) + Goal.prove_common ctxt NONE [] [] (map prep_goal constrs) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs end @@ -772,7 +774,7 @@ val AlphaResult {alpha_bn_trms, ...} = alpha_result fun mk_map thm = - thm |> `prop_of + thm |> `Thm.prop_of |>> List.last o snd o strip_comb |>> HOLogic.dest_Trueprop |>> head_of @@ -797,7 +799,7 @@ SUBPROOF (fn {prems, context, ...} => let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result - val prems' = flat (map Datatype_Aux.split_conj_thm prems) + val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems' in HEADGOAL @@ -806,9 +808,9 @@ (FIRST' [ rtac @{thm TrueI}, rtac @{thm conjI}, rtac @{thm refl}, - resolve_tac prems', - resolve_tac prems'', - resolve_tac alpha_intros ])) + resolve_tac ctxt prems', + resolve_tac ctxt prems'', + resolve_tac ctxt alpha_intros ])) end) ctxt fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_data.ML --- a/Nominal/nominal_dt_data.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_dt_data.ML Thu Jul 09 02:32:46 2015 +0100 @@ -25,7 +25,7 @@ val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list datatype user_data = UserData of - {dts : Datatype.spec list, + {dts : Old_Datatype.spec list, cn_names : string list, cn_tys : (string * string) list, bn_funs : (binding * typ * mixfix) list, @@ -34,7 +34,7 @@ datatype raw_dt_info = RawDtInfo of {raw_dt_names : string list, - raw_dts : Datatype.spec list, + raw_dts : Old_Datatype.spec list, raw_tys : typ list, raw_ty_args : (string * sort) list, raw_cns_info : cns_info list, @@ -111,7 +111,7 @@ datatype user_data = UserData of - {dts : Datatype.spec list, + {dts : Old_Datatype.spec list, cn_names : string list, cn_tys : (string * string) list, bn_funs : (binding * typ * mixfix) list, @@ -120,7 +120,7 @@ datatype raw_dt_info = RawDtInfo of {raw_dt_names : string list, - raw_dts : Datatype.spec list, + raw_dts : Old_Datatype.spec list, raw_tys : typ list, raw_ty_args : (string * sort) list, raw_cns_info : cns_info list, diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_dt_quot.ML Thu Jul 09 02:32:46 2015 +0100 @@ -58,7 +58,7 @@ fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = let val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms - val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, false, NONE))) qtys_descr qty_args1 + val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1 val qty_args3 = qty_args2 ~~ alpha_equivp_thms in fold_map Quotient_Type.add_quotient_type qty_args3 lthy @@ -113,9 +113,9 @@ map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |> Variable.exportT lthy3 lthy2 - fun tac _ = - Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac lifted_perm_laws)) + fun tac ctxt = + Class.intro_classes_tac ctxt [] THEN + (ALLGOALS (resolve_tac ctxt lifted_perm_laws)) in lthy2 |> Class.prove_instantiation_exit tac @@ -126,7 +126,7 @@ (* defines the size functions and proves size-class *) fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = let - val tac = K (Class.intro_classes_tac []) + fun tac ctxt = Class.intro_classes_tac ctxt [] in lthy |> Local_Theory.exit_global @@ -157,7 +157,7 @@ let fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) - val vars = Term.add_vars (prop_of thm) [] + val vars = Term.add_vars (Thm.prop_of thm) [] val vars' = map (Var o unraw_var_str) vars in Thm.certify_instantiate ([], (vars ~~ vars')) thm @@ -229,14 +229,14 @@ val tac = EVERY' [ rtac @{thm supports_finite}, - resolve_tac qsupports_thms, + resolve_tac ctxt' qsupports_thms, asm_simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms finite_supp supp_Pair finite_Un}) ] in Goal.prove ctxt' [] [] goals (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |> singleton (Proof_Context.export ctxt' ctxt) - |> Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm |> map zero_var_indexes end @@ -250,9 +250,9 @@ |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) - fun tac _ = - Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac qfsupp_thms)) + fun tac ctxt = + Class.intro_classes_tac ctxt [] THEN + (ALLGOALS (resolve_tac ctxt qfsupp_thms)) in lthy1 |> Class.prove_instantiation_exit tac @@ -303,7 +303,7 @@ val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} -val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def +val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_conv permute_prod_def prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps @@ -436,7 +436,7 @@ | Const (@{const_name "Abs_res"}, _) => true | _ => false in - thm |> prop_of + thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst @@ -538,8 +538,8 @@ val tac1 = if rec_flag - then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} - else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} + then resolve_tac ctxt @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} + else resolve_tac ctxt @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} val tac2 = EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss), @@ -559,10 +559,10 @@ let fun aux_tac prem bclauses = case (get_all_binders bclauses) of - [] => EVERY' [rtac prem, atac] + [] => EVERY' [rtac prem, assume_tac ctxt] | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => let - val parms = map (term_of o snd) params + val parms = map (Thm.term_of o snd) params val fthm = fresh_thm ctxt c parms binders bn_finite_thms val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} @@ -572,7 +572,7 @@ REPEAT o (etac @{thm conjE})]) [fthm] ctxt val abs_eq_thms = flat - (map (abs_eq_thm ctxt' fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses) + (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses) val ((_, eqs), ctxt'') = Obtain.result (fn ctxt'' => EVERY1 @@ -592,17 +592,17 @@ val tac1 = SOLVED' (EVERY' [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), - conj_tac (DETERM o resolve_tac fprops') ]) + conj_tac (DETERM o resolve_tac ctxt'' fprops') ]) (* for equalities between constructors *) val tac2 = SOLVED' (EVERY' [ rtac (@{thm ssubst} OF prems), rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms), rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs), - conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) + conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ]) (* proves goal "P" *) - val side_thm = Goal.prove ctxt'' [] [] (term_of concl) + val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl) (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |> singleton (Proof_Context.export ctxt'' ctxt) in @@ -622,7 +622,7 @@ val c = Free (c, TFree (a, @{sort fs})) val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) - |> map prop_of + |> map Thm.prop_of |> map Logic.strip_horn |> split_list @@ -707,7 +707,7 @@ val c = Free (c_name, c_ty) val (prems, concl) = induct' - |> prop_of + |> Thm.prop_of |> Logic.strip_horn val concls = concl @@ -721,13 +721,12 @@ |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss) fun pat_tac ctxt thm = - Subgoal.FOCUS (fn {params, context, ...} => + Subgoal.FOCUS (fn {params, context = ctxt', ...} => let - val thy = Proof_Context.theory_of context - val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params - val vs = Term.add_vars (prop_of thm) [] + val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params + val vs = Term.add_vars (Thm.prop_of thm) [] val vs_tys = map (Type.legacy_freeze_type o snd) vs - val vs_ctrms = map (cterm_of thy o Var) vs + val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs val assigns = map (lookup ty_parms) vs_tys val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm @@ -739,7 +738,7 @@ fun size_simp_tac ctxt = simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms)) in - Goal.prove_multi lthy'' [] prems' concls + Goal.prove_common lthy'' NONE [] prems' concls (fn {prems, context = ctxt} => Induction_Schema.induction_schema_tac ctxt prems THEN RANGE (map (pat_tac ctxt) exhausts) 1 diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Thu Jul 09 02:32:46 2015 +0100 @@ -125,7 +125,7 @@ val raw_bn_eqs = the simps val raw_bn_info = - prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs) + prep_bn_info lthy raw_dt_names raw_dts fs (map Thm.prop_of raw_bn_eqs) in (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) end @@ -166,7 +166,7 @@ binders |> map (bind_fn lthy args) |> split_list - |> pairself combine_fn + |> apply2 combine_fn end val t1 = map (mk_fv_body fv_map args) bodies @@ -199,7 +199,7 @@ fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = let - val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv = lookup fv_map ty val lhs = fv $ list_comb (constr, args) @@ -211,7 +211,7 @@ fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = let - val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv_bn = lookup fv_bn_map bn_trm val lhs = fv_bn $ list_comb (constr, args) @@ -287,7 +287,7 @@ fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) = let val p = Free ("p", @{typ perm}) - val arg_names = Datatype_Prop.make_tnames arg_tys + val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val perm_bn = lookup perm_bn_map bn_trm val lhs = perm_bn $ p $ list_comb (constr, args) @@ -347,7 +347,7 @@ fun prove_permute_zero induct perm_defs perm_fns ctxt = let val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types + val perm_indnames = Old_Datatype_Prop.make_tnames perm_types fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) @@ -358,11 +358,11 @@ val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs) - val tac = (Datatype_Aux.ind_tac induct perm_indnames + val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames THEN_ALL_NEW asm_simp_tac simpset) 1 in Goal.prove ctxt perm_indnames [] goals (K tac) - |> Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm end @@ -371,7 +371,7 @@ val p = Free ("p", @{typ perm}) val q = Free ("q", @{typ perm}) val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types + val perm_indnames = Old_Datatype_Prop.make_tnames perm_types fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) @@ -383,11 +383,11 @@ (* FIXME proper goal context *) val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs) - val tac = (Datatype_Aux.ind_tac induct perm_indnames + val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames THEN_ALL_NEW asm_simp_tac simpset) 1 in Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac) - |> Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm end @@ -403,7 +403,7 @@ fastype_of cnstr |> strip_type - val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) + val arg_names = Name.variant_list ["p"] (Old_Datatype_Prop.make_tnames arg_tys) val args = map Free (arg_names ~~ arg_tys) val lhs = lookup_perm p (ty, list_comb (cnstr, args)) @@ -430,8 +430,8 @@ val perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns) - fun tac _ (_, _, simps) = - Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) + fun tac ctxt (_, _, simps) = + Class.intro_classes_tac ctxt [] THEN ALLGOALS (resolve_tac ctxt simps) fun morphism phi (fvs, dfs, simps) = (map (Morphism.term phi) fvs, @@ -442,7 +442,7 @@ lthy |> Local_Theory.exit_global |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt}) - |> Primrec.add_primrec perm_fn_binds perm_eqs + |> BNF_LFP_Compat.primrec perm_fn_binds perm_eqs val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy' val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy' @@ -468,7 +468,7 @@ fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL (Object_Logic.full_atomize_tac ctxt - THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) + THEN' (DETERM o (Induct_Tacs.induct_tac ctxt insts (SOME ind_thms))) THEN_ALL_NEW subproof_tac const_names simps ctxt) fun mk_eqvt_goal pi const arg = @@ -491,13 +491,13 @@ |> map fastype_of |> map domain_type val (arg_names, ctxt'') = - Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' + Variable.variant_fixes (Old_Datatype_Prop.make_tnames arg_tys) ctxt' val args = map Free (arg_names ~~ arg_tys) val goals = map2 (mk_eqvt_goal p) consts args val insts = map (single o SOME) arg_names val const_names = map (fst o dest_Const) consts in - Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => + Goal.prove_common ctxt'' NONE [] [] goals (fn {context, ...} => prove_eqvt_tac insts ind_thms const_names simps context) |> Proof_Context.export ctxt'' ctxt end diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_eqvt.ML --- a/Nominal/nominal_eqvt.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_eqvt.ML Thu Jul 09 02:32:46 2015 +0100 @@ -32,8 +32,7 @@ fun eqvt_rel_single_case_tac ctxt pred_names pi intro = let - val thy = Proof_Context.theory_of ctxt - val cpi = Thm.cterm_of thy pi + val cpi = Thm.cterm_of ctxt pi val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} val eqvt_sconfig = eqvt_strict_config addexcls pred_names val simps1 = @@ -48,7 +47,7 @@ val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' val prems''' = map (simplify simps2 o simplify simps1) prems'' in - HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) + HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems''')) end) ctxt end @@ -92,7 +91,7 @@ val (([raw_concl], [raw_pi]), ctxt') = ctxt - |> Variable.import_terms false [concl_of raw_induct'] + |> Variable.import_terms false [Thm.concl_of raw_induct'] ||>> Variable.variant_fixes ["p"] val pi = Free (raw_pi, @{typ perm}) @@ -108,7 +107,7 @@ in Goal.prove ctxt' [] [] goal (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) - |> Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm |> Proof_Context.export ctxt' ctxt |> map (fn th => th RS mp) |> map zero_var_indexes @@ -140,7 +139,7 @@ end val _ = - Outer_Syntax.local_theory @{command_spec "equivariance"} + Outer_Syntax.local_theory @{command_keyword equivariance} "Proves equivariance for inductive predicate involving nominal datatypes." (Parse.const >> equivariance_cmd) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_function.ML Thu Jul 09 02:32:46 2015 +0100 @@ -27,9 +27,6 @@ (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> bool -> local_theory -> Proof.state - val setup : theory -> theory - val get_congs : Proof.context -> thm list - val get_info : Proof.context -> term -> nominal_info end @@ -106,10 +103,10 @@ val simp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, Code.add_default_eqn_attribute, - Nitpick_Simps.add] + Named_Theorems.add @{named_theorems nitpick_simp}] val psimp_attribs = map (Attrib.internal o K) - [Nitpick_Psimps.add] + [Named_Theorems.add @{named_theorems nitpick_psimp}] fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" @@ -159,19 +156,19 @@ val fnames = map (fst o fst) fixes fun qualify n = Binding.name n |> Binding.qualify true defname - val conceal_partial = if partials then I else Binding.conceal + val concealed_partial = if partials then I else Binding.concealed val addsmps = add_simps fnames post sort_cont val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy - |> addsmps (conceal_partial o Binding.qualify false "partial") - "psimps" conceal_partial psimp_attribs psimps - ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), + |> addsmps (concealed_partial o Binding.qualify false "partial") + "psimps" concealed_partial psimp_attribs psimps + ||>> Local_Theory.note ((concealed_partial (qualify "pinduct"), [Attrib.internal (K (Rule_Cases.case_names cnames)), Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) - ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) + ||>> Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination]) ||> (snd o Local_Theory.note ((qualify "cases", [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) ||> (case domintros of NONE => I | SOME thms => @@ -216,7 +213,7 @@ prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy in lthy' - |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] + |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd end @@ -225,31 +222,6 @@ fun nominal_function_cmd a b c int = gen_nominal_function int Specification.read_spec "_::type" a b c - -fun add_case_cong n thy = - let - val cong = #case_cong (Datatype.the_info thy n) - |> safe_mk_meta_eq - in - Context.theory_map - (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy - end - -val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) - - - -(* setup *) - -val setup = - Attrib.setup @{binding fundef_cong} - (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) - "declaration of congruence rule for function definitions" - #> setup_case_cong - #> Function_Common.Termination_Simps.setup - -val get_congs = Function_Ctx_Tree.get_function_congs - fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |> the_single |> snd @@ -275,7 +247,7 @@ (* nominal *) val _ = - Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_function"} + Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function} "define general recursive nominal functions" (nominal_function_parser nominal_default_config >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_function_common.ML --- a/Nominal/nominal_function_common.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_function_common.ML Thu Jul 09 02:32:46 2015 +0100 @@ -15,7 +15,7 @@ defname : string, (* contains no logical entities: invariant under morphisms: *) add_simps : (binding -> binding) -> string -> (binding -> binding) -> - Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + Token.src list -> thm list -> local_theory -> thm list * local_theory, case_names : string list, fs : term list, R : term, @@ -37,7 +37,7 @@ defname : string, (* contains no logical entities: invariant under morphisms: *) add_simps : (binding -> binding) -> string -> (binding -> binding) -> - Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + Token.src list -> thm list -> local_theory -> thm list * local_theory, case_names : string list, fs : term list, R : term, @@ -64,7 +64,7 @@ structure NominalFunctionData = Generic_Data ( type T = (term * nominal_info) Item_Net.T; - val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); + val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst); val extend = I; fun merge tabs : T = Item_Net.merge tabs; ) @@ -72,9 +72,9 @@ val get_function = NominalFunctionData.get o Context.Proof; -fun lift_morphism thy f = +fun lift_morphism ctxt f = let - fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) + fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t)) in Morphism.morphism "lift_morphism" {binding = [], @@ -85,12 +85,11 @@ fun import_function_data t ctxt = let - val thy = Proof_Context.theory_of ctxt - val ct = cterm_of thy t - val inst_morph = lift_morphism thy o Thm.instantiate + val ct = Thm.cterm_of ctxt t + val inst_morph = lift_morphism ctxt o Thm.instantiate fun match (trm, data) = - SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) + SOME (morph_function_data data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct)))) handle Pattern.MATCH => NONE in get_first match (Item_Net.retrieve (get_function ctxt) t) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_function_core.ML Thu Jul 09 02:32:46 2015 +0100 @@ -83,7 +83,7 @@ {no: int, qglr : ((string * typ) list * term list * term * term), cdata : clause_context, - tree: Function_Ctx_Tree.ctx_tree, + tree: Function_Context_Tree.ctx_tree, lGI: thm, RCs: rec_call_info list} @@ -109,7 +109,7 @@ ([], (fixes, assumes, arg) :: xs) | add_Ri _ _ _ _ = raise Match in - rev (Function_Ctx_Tree.traverse_tree add_Ri tree []) + rev (Function_Context_Tree.traverse_tree add_Ri tree []) end (* nominal *) @@ -147,14 +147,14 @@ (** building proof obligations *) fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = mk_eqvt_at (fvar, arg) - |> curry Logic.list_implies (map prop_of assms) + |> curry Logic.list_implies (map Thm.prop_of assms) |> fold_rev (Logic.all o Free) vs |> fold_rev absfree qs |> strip_abs_body fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = mk_inv inv (fvar, arg) - |> curry Logic.list_implies (map prop_of assms) + |> curry Logic.list_implies (map Thm.prop_of assms) |> fold_rev (Logic.all o Free) vs |> fold_rev absfree qs |> strip_abs_body @@ -207,17 +207,15 @@ val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs - val thy = Proof_Context.theory_of ctxt' - fun inst t = subst_bounds (rev qs, t) val gs = map inst pre_gs val lhs = inst pre_lhs val rhs = inst pre_rhs - val cqs = map (cterm_of thy) qs - val ags = map (Thm.assume o cterm_of thy) gs + val cqs = map (Thm.cterm_of ctxt') qs + val ags = map (Thm.assume o Thm.cterm_of ctxt') gs - val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) + val case_hyp = Thm.assume (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) in ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } @@ -245,7 +243,7 @@ val Globals {h, ...} = globals val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata - val cert = Thm.cterm_of (Proof_Context.theory_of ctxt) + val cert = Thm.cterm_of ctxt (* Instantiate the GIntro thm with "f" and import into the clause context. *) val lGI = GIntro_thm @@ -263,7 +261,7 @@ val h_assum = HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] [] |> abstract_over_list (rev qs) @@ -293,12 +291,12 @@ (* nominal *) (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) (* if j < i, then turn around *) -fun get_compat_thm thy cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj = +fun get_compat_thm ctxt cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj = let val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj - val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) + val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) in if j < i then let @@ -333,7 +331,7 @@ (* Generates the replacement lemma in fully quantified form. *) -fun mk_replacement_lemma thy h ih_elim clause = +fun mk_replacement_lemma ctxt h ih_elim clause = let val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause @@ -346,16 +344,16 @@ val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs val h_assums = map (fn RCInfo {h_assum, ...} => - Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs + Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs val (eql, _) = - Function_Ctx_Tree.rewrite_by_tree (Proof_Context.init_global thy) + Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree val replace_lemma = (eql RS meta_eq_to_obj_eq) - |> Thm.implies_intr (cprop_of case_hyp) - |> fold_rev (Thm.implies_intr o cprop_of) h_assums - |> fold_rev (Thm.implies_intr o cprop_of) ags + |> Thm.implies_intr (Thm.cprop_of case_hyp) + |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums + |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs |> Thm.close_derivation in @@ -364,7 +362,7 @@ (* nominal *) (* Generates the eqvt lemmas for each clause *) -fun mk_eqvt_lemma thy ih_eqvt clause = +fun mk_eqvt_lemma ctxt ih_eqvt clause = let val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause @@ -377,18 +375,18 @@ fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_eqvt_case) - |> fold_rev (Thm.implies_intr o cprop_of) CCas - |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs + |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas + |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs in map prep_eqvt RCs - |> map (fold_rev (Thm.implies_intr o cprop_of) ags) - |> map (Thm.implies_intr (cprop_of case_hyp)) + |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags) + |> map (Thm.implies_intr (Thm.cprop_of case_hyp)) |> map (fold_rev Thm.forall_intr cqs) |> map (Thm.close_derivation) end (* nominal *) -fun mk_invariant_lemma thy ih_inv clause = +fun mk_invariant_lemma ctxt ih_inv clause = let val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause @@ -401,19 +399,21 @@ fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_inv_case) - |> fold_rev (Thm.implies_intr o cprop_of) CCas - |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs + |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas + |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs in map prep_inv RCs - |> map (fold_rev (Thm.implies_intr o cprop_of) ags) - |> map (Thm.implies_intr (cprop_of case_hyp)) + |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags) + |> map (Thm.implies_intr (Thm.cprop_of case_hyp)) |> map (fold_rev Thm.forall_intr cqs) |> map (Thm.close_derivation) end (* nominal *) -fun mk_uniqueness_clause thy globals compat_store eqvts invs clausei clausej RLj = +fun mk_uniqueness_clause ctxt globals compat_store eqvts invs clausei clausej RLj = let + val thy = Proof_Context.theory_of ctxt + val Globals {h, y, x, fvar, ...} = globals val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ags = agsi, ...}, ...} = clausei @@ -425,10 +425,11 @@ val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' val Ghsj' = map - (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj + (fn RCInfo {h_assum, ...} => + Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj - val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) + val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj'] @@ -458,7 +459,7 @@ |> map (fold Thm.elim_implies [case_hypj']) |> map (fold Thm.elim_implies agsj') - val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj + val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) @@ -468,70 +469,71 @@ (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) - |> fold_rev (Thm.implies_intr o cprop_of) Ghsj' - |> fold_rev (Thm.implies_intr o cprop_of) agsj' + |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj' + |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) - |> Thm.implies_intr (cprop_of y_eq_rhsj'h) - |> Thm.implies_intr (cprop_of lhsi_eq_lhsj') - |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj') + |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h) + |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj') + |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj') end (* nominal *) -fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems - clausei = +fun mk_uniqueness_case ctxt + globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei = let + val thy = Proof_Context.theory_of ctxt + val Globals {x, y, ranT, fvar, ...} = globals val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs val ih_intro_case = - full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp]) + full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ih_intro fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) - |> fold_rev (Thm.implies_intr o cprop_of) CCas - |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs + |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas + |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val existence = fold (curry op COMP o prep_RC) RCs lGI - val P = cterm_of thy (mk_eq (y, rhsC)) - val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) + val P = Thm.cterm_of ctxt (mk_eq (y, rhsC)) + val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = - map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems + map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems fun elim_implies_eta A AB = - Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB + Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |> Seq.list_of |> the_single val uniqueness = G_cases - |> Thm.forall_elim (cterm_of thy lhs) - |> Thm.forall_elim (cterm_of thy y) + |> Thm.forall_elim (Thm.cterm_of ctxt lhs) + |> Thm.forall_elim (Thm.cterm_of ctxt y) |> Thm.forall_elim P |> Thm.elim_implies G_lhs_y |> fold elim_implies_eta unique_clauses - |> Thm.implies_intr (cprop_of G_lhs_y) - |> Thm.forall_intr (cterm_of thy y) + |> Thm.implies_intr (Thm.cprop_of G_lhs_y) + |> Thm.forall_intr (Thm.cterm_of ctxt y) - val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) + val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) val exactly_one = - ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] + ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)] |> curry (op COMP) existence |> curry (op COMP) uniqueness - |> simplify - (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym]) - |> Thm.implies_intr (cprop_of case_hyp) - |> fold_rev (Thm.implies_intr o cprop_of) ags + |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym]) + |> Thm.implies_intr (Thm.cprop_of case_hyp) + |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs val function_value = existence |> Thm.implies_intr ihyp - |> Thm.implies_intr (cprop_of case_hyp) - |> Thm.forall_intr (cterm_of thy x) - |> Thm.forall_elim (cterm_of thy lhs) + |> Thm.implies_intr (Thm.cprop_of case_hyp) + |> Thm.forall_intr (Thm.cterm_of ctxt x) + |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |> curry (op RS) refl in (exactly_one, function_value) @@ -539,57 +541,58 @@ (* nominal *) -fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = +fun prove_stuff ctxt + globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = let val Globals {h, domT, ranT, x, ...} = globals - val thy = Proof_Context.theory_of ctxt (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) - |> cterm_of thy + |> Thm.cterm_of ctxt val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) - |> instantiate' [] [NONE, SOME (cterm_of thy h)] + |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)] val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop})) val _ = trace_msg (K "Proving Replacement lemmas...") - val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses + val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses val _ = trace_msg (K "Proving Equivariance lemmas...") - val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses + val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses val _ = trace_msg (K "Proving Invariance lemmas...") - val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses + val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses val _ = trace_msg (K "Proving cases for unique existence...") val (ex1s, values) = - split_list (map (mk_uniqueness_case thy globals G f + split_list (map (mk_uniqueness_case ctxt globals G f ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses) val _ = trace_msg (K "Proving: Graph is a function") val graph_is_function = complete |> Thm.forall_elim_vars 0 |> fold (curry op COMP) ex1s - |> Thm.implies_intr (ihyp) - |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) - |> Thm.forall_intr (cterm_of thy x) + |> Thm.implies_intr ihyp + |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x))) + |> Thm.forall_intr (Thm.cterm_of ctxt x) |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) - |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) + |> (fn it => + fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it) val goalstate = - Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt + Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |> Thm.close_derivation |> Goal.protect 0 - |> fold_rev (Thm.implies_intr o cprop_of) compat - |> Thm.implies_intr (cprop_of complete) - |> Thm.implies_intr (cprop_of invariant) - |> Thm.implies_intr (cprop_of G_eqvt) + |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat + |> Thm.implies_intr (Thm.cprop_of complete) + |> Thm.implies_intr (Thm.cprop_of invariant) + |> Thm.implies_intr (Thm.cprop_of G_eqvt) in (goalstate, values) end @@ -599,7 +602,7 @@ let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = lthy - |> Local_Theory.conceal + |> Proof_Context.concealed |> Inductive.add_inductive_i {quiet_mode = true, verbose = ! trace, @@ -612,14 +615,14 @@ [] (* no parameters *) (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) [] (* no special monos *) - ||> Local_Theory.restore_naming lthy + ||> Proof_Context.restore_naming lthy - val cert = cterm_of (Proof_Context.theory_of lthy) + val cert = Thm.cterm_of lthy fun requantify orig_intro thm = let val (qs, t) = dest_all_all orig_intro val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) - val vars = Term.add_vars (prop_of thm) [] + val vars = Term.add_vars (Thm.prop_of thm) [] val varmap = AList.lookup (op =) (frees ~~ map fst vars) #> the_default ("",0) in @@ -640,7 +643,7 @@ let fun mk_h_assm (rcfix, rcassm, rcarg) = HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg)) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix in HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs) @@ -663,7 +666,7 @@ in Local_Theory.define ((Binding.name (function_name fname), mixfix), - ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy + ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy end (* nominal *) @@ -674,7 +677,7 @@ fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (curry Logic.mk_implies) gs |> fold_rev (Logic.all o Free) rcfix |> fold_rev mk_forall_rename (map fst oqs ~~ qs) @@ -691,7 +694,7 @@ fun fix_globals domT ranT fvar ctxt = let - val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes + val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt in (Globals {h = Free (h, domT --> ranT), @@ -708,11 +711,11 @@ ctxt') end -fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = +fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) = let fun inst_term t = subst_bound(f, abstract_over (fvar, t)) in - (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) + (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg) end @@ -721,23 +724,23 @@ * PROVING THE RULES **********************************************************) -fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = +fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function = let val Globals {domT, z, ...} = globals fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = let - val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) - val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) + val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) + val z_smaller = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) in ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |> (fn it => it COMP graph_is_function) |> Thm.implies_intr z_smaller - |> Thm.forall_intr (cterm_of thy z) + |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP valthm) |> Thm.implies_intr lhs_acc - |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff]) - |> fold_rev (Thm.implies_intr o cprop_of) ags + |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff]) + |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in @@ -751,34 +754,34 @@ val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} -fun mk_partial_induct_rule thy globals R complete_thm clauses = +fun mk_partial_induct_rule ctxt globals R complete_thm clauses = let val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R - val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) - val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) + val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x))) + val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a)) - val D_subset = cterm_of thy (Logic.all x + val D_subset = Thm.cterm_of ctxt (Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), HOLogic.mk_Trueprop (D $ z))))) - |> cterm_of thy + |> Thm.cterm_of ctxt (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (P $ Bound 0))) - |> cterm_of thy + |> Thm.cterm_of ctxt val aihyp = Thm.assume ihyp fun prove_case clause = let - val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, + val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, qglr = (oqs, _, _, _), ...} = clause val case_hyp_conv = K (case_hyp RS eq_reflection) @@ -786,23 +789,23 @@ val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D val sih = fconv_rule (Conv.binder_conv - (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp + (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp end fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih - |> Thm.forall_elim (cterm_of thy rcarg) + |> Thm.forall_elim (Thm.cterm_of ctxt rcarg) |> Thm.elim_implies llRI - |> fold_rev (Thm.implies_intr o cprop_of) CCas - |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs + |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas + |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) val step = HOLogic.mk_Trueprop (P $ lhs) - |> fold_rev (curry Logic.mk_implies o prop_of) P_recs + |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs |> fold_rev (curry Logic.mk_implies) gs |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - |> cterm_of thy + |> Thm.cterm_of ctxt val P_lhs = Thm.assume step |> fold Thm.forall_elim cqs @@ -810,12 +813,13 @@ |> fold Thm.elim_implies ags |> fold Thm.elim_implies P_recs - val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) + val res = + Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x)) |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |> Thm.symmetric (* P lhs == P x *) |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) - |> Thm.implies_intr (cprop_of case_hyp) - |> fold_rev (Thm.implies_intr o cprop_of) ags + |> Thm.implies_intr (Thm.cprop_of case_hyp) + |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs in (res, step) @@ -827,8 +831,8 @@ |> Thm.forall_elim_vars 0 |> fold (curry op COMP) cases (* P x *) |> Thm.implies_intr ihyp - |> Thm.implies_intr (cprop_of x_D) - |> Thm.forall_intr (cterm_of thy x) + |> Thm.implies_intr (Thm.cprop_of x_D) + |> Thm.forall_intr (Thm.cterm_of ctxt x) val subset_induct_rule = acc_subset_induct @@ -843,16 +847,16 @@ val simple_induct_rule = subset_induct_rule - |> Thm.forall_intr (cterm_of thy D) - |> Thm.forall_elim (cterm_of thy acc_R) - |> assume_tac 1 |> Seq.hd + |> Thm.forall_intr (Thm.cterm_of ctxt D) + |> Thm.forall_elim (Thm.cterm_of ctxt acc_R) + |> atac 1 |> Seq.hd |> (curry op COMP) (acc_downward - |> (instantiate' [SOME (ctyp_of thy domT)] - (map (SOME o cterm_of thy) [R, x, z])) - |> Thm.forall_intr (cterm_of thy z) - |> Thm.forall_intr (cterm_of thy x)) - |> Thm.forall_intr (cterm_of thy a) - |> Thm.forall_intr (cterm_of thy P) + |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] + (map (SOME o Thm.cterm_of ctxt) [R, x, z])) + |> Thm.forall_intr (Thm.cterm_of ctxt z) + |> Thm.forall_intr (Thm.cterm_of ctxt x)) + |> Thm.forall_intr (Thm.cterm_of ctxt a) + |> Thm.forall_intr (Thm.cterm_of ctxt P) in simple_induct_rule end @@ -861,16 +865,15 @@ (* FIXME: broken by design *) fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = let - val thy = Proof_Context.theory_of ctxt val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |> fold_rev (curry Logic.mk_implies) gs - |> cterm_of thy + |> Thm.cterm_of ctxt in Goal.init goal - |> (SINGLE (resolve_tac [accI] 1)) |> the - |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the + |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the + |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the |> (SINGLE (auto_tac ctxt)) |> the |> Goal.conclude |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) @@ -884,36 +887,36 @@ val wf_in_rel = @{thm Fun_Def.wf_in_rel} val in_rel_def = @{thm Fun_Def.in_rel_def} -fun mk_nest_term_case thy globals R' ihyp clause = +fun mk_nest_term_case ctxt globals R' ihyp clause = let val Globals {z, ...} = globals val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, qglr=(oqs, _, _, _), ...} = clause val ih_case = - full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp]) + full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ihyp fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = let val used = (u @ sub) - |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) + |> map (fn (ctx,thm) => Function_Context_Tree.export_thm ctxt ctx thm) val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) - |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) - |> Function_Ctx_Tree.export_term (fixes, assumes) - |> fold_rev (curry Logic.mk_implies o prop_of) ags + |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *) + |> Function_Context_Tree.export_term (fixes, assumes) + |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - |> cterm_of thy + |> Thm.cterm_of ctxt val thm = Thm.assume hyp |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags - |> Function_Ctx_Tree.import_thm thy (fixes, assumes) + |> Function_Context_Tree.import_thm ctxt (fixes, assumes) |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) - |> cterm_of thy |> Thm.assume + |> Thm.cterm_of ctxt |> Thm.assume val acc = thm COMP ih_case val z_acc_local = acc @@ -921,7 +924,7 @@ (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) val ethm = z_acc_local - |> Function_Ctx_Tree.export_thm thy (fixes, + |> Function_Context_Tree.export_thm ctxt (fixes, z_eq_arg :: case_hyp :: ags @ assumes) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) @@ -931,11 +934,11 @@ end | step _ _ _ _ = raise Match in - Function_Ctx_Tree.traverse_tree step tree + Function_Context_Tree.traverse_tree step tree end -fun mk_nest_term_rule thy globals R R_cases clauses = +fun mk_nest_term_rule ctxt globals R R_cases clauses = let val Globals { domT, x, z, ... } = globals val acc_R = mk_acc domT R @@ -948,42 +951,42 @@ val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R') - |> cterm_of thy (* "wf R'" *) + |> Thm.cterm_of ctxt (* "wf R'" *) (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), HOLogic.mk_Trueprop (acc_R $ Bound 0))) - |> cterm_of thy + |> Thm.cterm_of ctxt val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 - val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) + val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x)) - val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], []) + val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], []) in R_cases - |> Thm.forall_elim (cterm_of thy z) - |> Thm.forall_elim (cterm_of thy x) - |> Thm.forall_elim (cterm_of thy (acc_R $ z)) + |> Thm.forall_elim (Thm.cterm_of ctxt z) + |> Thm.forall_elim (Thm.cterm_of ctxt x) + |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z)) |> curry op COMP (Thm.assume R_z_x) |> fold_rev (curry op COMP) cases |> Thm.implies_intr R_z_x - |> Thm.forall_intr (cterm_of thy z) + |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP accI) |> Thm.implies_intr ihyp - |> Thm.forall_intr (cterm_of thy x) + |> Thm.forall_intr (Thm.cterm_of ctxt x) |> (fn it => Drule.compose (it, 2, wf_induct_rule)) |> curry op RS (Thm.assume wfR') |> forall_intr_vars |> (fn it => it COMP allI) |> fold Thm.implies_intr hyps |> Thm.implies_intr wfR' - |> Thm.forall_intr (cterm_of thy R') - |> Thm.forall_elim (cterm_of thy (inrel_R)) + |> Thm.forall_intr (Thm.cterm_of ctxt R') + |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R)) |> curry op RS wf_in_rel - |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def]) - |> Thm.forall_intr (cterm_of thy Rrel) + |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def]) + |> Thm.forall_intr (Thm.cterm_of ctxt Rrel) end @@ -1014,7 +1017,7 @@ val n = length abstract_qglrs fun build_tree (ClauseContext { ctxt, rhs, ...}) = - Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs + Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs val trees = map build_tree clauses val RCss = map find_calls trees @@ -1025,8 +1028,8 @@ val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy - val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss - val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees + val RCss = map (map (inst_RC lthy fvar f)) RCss + val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy @@ -1037,10 +1040,10 @@ val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses - val cert = cterm_of (Proof_Context.theory_of lthy) + val cert = Thm.cterm_of lthy val xclauses = PROFILE "xclauses" - (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees + (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss val complete = @@ -1062,7 +1065,8 @@ fun mk_partial_rules provedgoal = let - val newthy = theory_of_thm provedgoal (*FIXME*) + val newthy = Thm.theory_of_thm provedgoal (*FIXME*) + val newctxt = Proof_Context.init_global newthy (*FIXME*) val ((graph_is_function, complete_thm), graph_is_eqvt) = provedgoal @@ -1075,13 +1079,13 @@ val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) val psimps = PROFILE "Proving simplification rules" - (mk_psimps newthy globals R xclauses values f_iff) graph_is_function + (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function val simple_pinduct = PROFILE "Proving partial induction rule" - (mk_partial_induct_rule newthy globals R complete_thm) xclauses + (mk_partial_induct_rule newctxt globals R complete_thm) xclauses val total_intro = PROFILE "Proving nested termination rule" - (mk_nest_term_rule newthy globals R R_elim) xclauses + (mk_nest_term_rule newctxt globals R R_elim) xclauses val dom_intros = if domintros then SOME (PROFILE "Proving domain introduction rules" diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_induct.ML --- a/Nominal/nominal_induct.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_induct.ML Thu Jul 09 02:32:46 2015 +0100 @@ -57,7 +57,7 @@ end; val substs = map2 subst insts concls |> flat |> distinct (op =) - |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt))); + |> map (apply2 (Thm.cterm_of ctxt)); in (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) end; @@ -86,9 +86,6 @@ fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = let - val thy = Proof_Context.theory_of ctxt; - val cert = Thm.cterm_of thy; - val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs; @@ -99,7 +96,7 @@ fun rule_cases ctxt r = let val r' = if simp then Induct.simplified_rule ctxt r else r - in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; + in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end; in (fn i => fn st => rules @@ -110,7 +107,7 @@ (CONJUNCTS (ALLGOALS let val adefs = nth_list atomized_defs (j - 1); - val frees = fold (Term.add_frees o prop_of) adefs []; + val frees = fold (Term.add_frees o Thm.prop_of) adefs []; val xs = nth_list fixings (j - 1); val k = nth concls (j - 1) + more_consumes in @@ -131,7 +128,7 @@ (Tactic.rtac (rename_params_rule false [] rule') i THEN PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) THEN_ALL_NEW_CASES - ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) + ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt) else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt) end; @@ -176,9 +173,8 @@ Scan.lift (Args.mode Induct.no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- avoiding -- fixing -- rule_spec) >> - (fn (no_simp, (((x, y), z), w)) => fn ctxt => - RAW_METHOD_CASES (fn facts => - HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); + (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts => + HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)); end diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_inductive.ML --- a/Nominal/nominal_inductive.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_inductive.ML Thu Jul 09 02:32:46 2015 +0100 @@ -35,7 +35,7 @@ | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t - | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t + | real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of t = head_of t @@ -81,7 +81,7 @@ end fun induct_forall_const T = - Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool}) + Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool}) fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t) @@ -156,7 +156,7 @@ val all_elims = let fun spec' ct = - Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec} + Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec} in fold (fn ct => fn th => th RS spec' ct) end @@ -172,34 +172,33 @@ |> flag ? (all_elims [p]) |> flag ? (eqvt_srule context) in - asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms induct_forall_def})) 1 + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1 end) ctxt fun non_binder_tac prem intr_cvars Ps ctxt = - Subgoal.SUBPROOF (fn {context, params, prems, ...} => + Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} => let - val thy = Proof_Context.theory_of context val (prms, p, _) = split_last2 (map snd params) - val prm_tys = map (fastype_of o term_of) prms - val cperms = map (cterm_of thy o perm_const) prm_tys + val prm_tys = map (fastype_of o Thm.term_of) prms + val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms val prem' = prem |> cterm_instantiate (intr_cvars ~~ p_prms) |> eqvt_srule ctxt (* for inductive-premises*) - fun tac1 prm = helper_tac true prm p context + fun tac1 prm = helper_tac true prm p ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac p, - eqvt_stac context, - helper_tac false prm p context ] + eqvt_stac ctxt', + helper_tac false prm p ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in - EVERY1 [ eqvt_stac context, + EVERY1 [ eqvt_stac ctxt', rtac prem', RANGE (map (SUBGOAL o select) prems) ] end) ctxt @@ -232,9 +231,8 @@ fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => let - val thy = Proof_Context.theory_of ctxt val (prms, p, c) = split_last2 (map snd params) - val prm_trms = map term_of prms + val prm_trms = map Thm.term_of prms val prm_tys = map fastype_of prm_trms val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm @@ -243,7 +241,7 @@ val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) - val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm' + val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm' val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result (K (EVERY1 [etac @{thm exE}, @@ -256,7 +254,7 @@ val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt - val cperms = map (cterm_of thy o perm_const) prm_tys + val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms val prem' = prem |> cterm_instantiate (intr_cvars ~~ qp_prms) @@ -277,13 +275,13 @@ fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i - val side_thm = Goal.prove ctxt' [] [] (term_of concl) - (fn {context, ...} => - EVERY1 [ CONVERSION (expand_conv_bot context), - eqvt_stac context, + val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl) + (fn {context = ctxt'', ...} => + EVERY1 [ CONVERSION (expand_conv_bot ctxt''), + eqvt_stac ctxt'', rtac prem', RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) - |> singleton (Proof_Context.export ctxt' ctxt) + |> singleton (Proof_Context.export ctxt' ctxt) in rtac side_thm 1 end) ctxt @@ -310,23 +308,22 @@ fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = let - val thy = Proof_Context.theory_of ctxt val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt val (ind_prems, ind_concl) = raw_induct' - |> prop_of + |> Thm.prop_of |> Logic.strip_horn |>> map strip_full_horn val params = map (fn (x, _, _) => x) ind_prems val param_trms = (map o map) Free params - val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs + val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs val intr_vars = (map o map) fst intr_vars_tys val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms - val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys + val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys val (intr_prems, intr_concls) = intrs - |> map prop_of + |> map Thm.prop_of |> map2 subst_Vars intr_vars_substs |> map Logic.strip_horn |> split_list @@ -369,7 +366,7 @@ val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |> singleton (Proof_Context.export ctxt ctxt_outside) - |> Datatype_Aux.split_conj_thm + |> Old_Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms permute_zero induct_rulify})) @@ -417,7 +414,7 @@ let (* fixme hack *) val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt - val trms = map (term_of o snd) ctrms + val trms = map (Thm.term_of o snd) ctrms val ctxt'' = fold Variable.declare_term trms ctxt' in map (Syntax.read_term ctxt'') avoid_trms @@ -439,7 +436,7 @@ val main_parser = Parse.xname -- avoids_parser in val _ = - Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"} + Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} "prove strong induction theorem for inductive predicate involving nominal datatypes" (main_parser >> prove_strong_inductive_cmd) end diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_library.ML Thu Jul 09 02:32:46 2015 +0100 @@ -86,7 +86,7 @@ (* datatype operations *) type cns_info = (term * typ * typ list * bool list) list - val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list + val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list (* tactics for function package *) val size_ss: simpset @@ -333,10 +333,10 @@ let fun aux ((ty_name, vs), (cname, args)) = let - val vs_tys = map (Datatype_Aux.typ_of_dtyp descr) vs + val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs val ty = Type (ty_name, vs_tys) - val arg_tys = map (Datatype_Aux.typ_of_dtyp descr) args - val is_rec = map Datatype_Aux.is_rec_type args + val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args + val is_rec = map Old_Datatype_Aux.is_rec_type args in (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) end @@ -451,13 +451,13 @@ val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} in EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] + REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), + REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))] end fun map_thm ctxt f tac thm = let - val opt_goal_trm = map_term f (prop_of thm) + val opt_goal_trm = map_term f (Thm.prop_of thm) in case opt_goal_trm of NONE => thm @@ -495,7 +495,7 @@ fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; fun atomize_rule ctxt i thm = Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm -fun atomize_concl ctxt thm = atomize_rule ctxt (length (prems_of thm)) thm +fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm (* applies a tactic to a formula composed of conjunctions *) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_mutual.ML Thu Jul 09 02:32:46 2015 +0100 @@ -138,7 +138,7 @@ val ((f, (_, f_defthm)), lthy') = Local_Theory.define ((Binding.name fname, mixfix), - ((Binding.conceal (Binding.name (fname ^ "_def")), []), + ((Binding.concealed (Binding.name (fname ^ "_def")), []), Term.subst_bound (fsum, f_def))) lthy in (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, @@ -156,8 +156,6 @@ fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = let - val thy = Proof_Context.theory_of ctxt - val oqnames = map fst pre_qs val (qs, _) = Variable.variant_fixes oqnames ctxt |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs @@ -167,13 +165,13 @@ val args = map inst pre_args val rhs = inst pre_rhs - val cqs = map (cterm_of thy) qs - val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt + val cqs = map (Thm.cterm_of ctxt) qs + val (ags, ctxt') = fold_map Thm.assume_hyps (map (Thm.cterm_of ctxt) gs) ctxt val import = fold Thm.forall_elim cqs #> fold Thm.elim_implies ags - val export = fold_rev (Thm.implies_intr o cprop_of) ags + val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags #> fold_rev forall_intr_rename (oqnames ~~ cqs) in F ctxt' (f, qs, gs, args, rhs) import export @@ -242,8 +240,7 @@ fun mk_applied_form ctxt caTs thm = let - val thy = Proof_Context.theory_of ctxt - val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) + val xs = map_index (fn (i,T) => Thm.cterm_of ctxt (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) in fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |> Conv.fconv_rule (Thm.beta_conversion true) @@ -253,7 +250,7 @@ fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = let - val cert = cterm_of (Proof_Context.theory_of ctxt) + val cert = Thm.cterm_of ctxt val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => Free (Pname, cargTs ---> HOLogic.boolT)) @@ -314,7 +311,7 @@ (* extracting the acc-premises from the induction theorems *) val acc_prems = - map prop_of induct_thms + map Thm.prop_of induct_thms |> map2 forall_elim_list argss |> map (strip_qnt_body @{const_name Pure.all}) |> map (curry Logic.nth_prem 1) @@ -333,19 +330,21 @@ val induct_thm = case induct_thms of [thm] => thm - |> Drule.gen_all + |> Drule.gen_all (Variable.maxidx_of ctxt') |> Thm.permute_prems 0 1 - |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm) + |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm) | thms => thms - |> map Drule.gen_all + |> map (Drule.gen_all (Variable.maxidx_of ctxt')) |> map (Rule_Cases.add_consumes 1) |> snd o Rule_Cases.strict_mutual_rule ctxt' |> atomize_concl ctxt' - fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac + fun tac ctxt thm = + rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt in Goal.prove ctxt' (flat arg_namess) [] goal - (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms))) + (fn {context = ctxt'', ...} => + HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms))) |> singleton (Proof_Context.export ctxt' ctxt) |> split_conj_thm |> map (fn th => th RS mp) @@ -435,7 +434,7 @@ val G_name_aux = G_name ^ "_aux" val subst = [(G, Free (G_name_aux, G_type))] val GIntros_aux = GIntro_thms - |> map prop_of + |> map Thm.prop_of |> map (Term.subst_free subst) |> map (subst_all case_sum_exp) @@ -478,15 +477,16 @@ (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1))) fun aux_tac thm = - rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (simpset1 addsimps [inj_thm])) + rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW + asm_full_simp_tac (simpset1 addsimps [inj_thm]) val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms)))) - |> Drule.gen_all + |> Drule.gen_all (Variable.maxidx_of lthy''') val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) - |> Drule.gen_all + |> Drule.gen_all (Variable.maxidx_of lthy''') val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm])))) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_permeq.ML --- a/Nominal/nominal_permeq.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_permeq.ML Thu Jul 09 02:32:46 2015 +0100 @@ -101,8 +101,8 @@ fun trace_msg ctxt result = let - val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) - val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) + val lhs_str = Syntax.string_of_term ctxt (Thm.term_of (Thm.lhs_of result)) + val rhs_str = Syntax.string_of_term ctxt (Thm.term_of (Thm.rhs_of result)) in warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) end @@ -120,7 +120,7 @@ out the analysed term *) fun trace_info_conv ctxt ctrm = let - val trm = term_of ctrm + val trm = Thm.term_of ctrm val _ = case (head_of trm) of @{const "Trueprop"} => () | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) @@ -130,14 +130,14 @@ (* conversion for applications *) fun eqvt_apply_conv ctrm = - case (term_of ctrm) of + case Thm.term_of ctrm of Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => let val (perm, t) = Thm.dest_comb ctrm val (_, p) = Thm.dest_comb perm val (f, x) = Thm.dest_comb t - val a = ctyp_of_term x; - val b = ctyp_of_term t; + val a = Thm.ctyp_of_cterm x; + val b = Thm.ctyp_of_cterm t; val ty_insts = map SOME [b, a] val term_insts = map SOME [p, f, x] in @@ -147,7 +147,7 @@ (* conversion for lambdas *) fun eqvt_lambda_conv ctrm = - case (term_of ctrm) of + case Thm.term_of ctrm of Const (@{const_name "permute"}, _) $ _ $ (Abs _) => Conv.rewr_conv @{thm eqvt_lambda} ctrm | _ => Conv.no_conv ctrm @@ -166,7 +166,8 @@ (if strict_flag then error else warning) ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) - val _ = case (term_of ctrm) of + val _ = + case Thm.term_of ctrm of Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm | _ => () diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_termination.ML --- a/Nominal/nominal_termination.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_termination.ML Thu Jul 09 02:32:46 2015 +0100 @@ -26,7 +26,7 @@ val simp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, Code.add_default_eqn_attribute, - Nitpick_Simps.add] + Named_Theorems.add @{named_theorems nitpick_simp}] val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) @@ -107,7 +107,7 @@ (Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (false)) val _ = - Outer_Syntax.local_theory_to_proof @{command_spec "nominal_termination"} + Outer_Syntax.local_theory_to_proof @{command_keyword nominal_termination} "prove termination of a recursive nominal function" (option_parser -- Scan.option Parse.term >> (fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm)) diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_thmdecls.ML --- a/Nominal/nominal_thmdecls.ML Tue Jul 08 11:18:31 2014 +0100 +++ b/Nominal/nominal_thmdecls.ML Thu Jul 09 02:32:46 2015 +0100 @@ -62,7 +62,6 @@ val eqvt_del: attribute val eqvt_raw_add: attribute val eqvt_raw_del: attribute - val setup: theory -> theory val get_eqvts_thms: Proof.context -> thm list val get_eqvts_raw_thms: Proof.context -> thm list val eqvt_transform: Proof.context -> thm -> thm @@ -91,6 +90,11 @@ val eqvts = Item_Net.content o EqvtData.get val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get +val _ = + Theory.setup + (Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> + Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)) + val get_eqvts_thms = eqvts o Context.Proof val get_eqvts_raw_thms = eqvts_raw o Context.Proof @@ -109,9 +113,9 @@ fun error_msg () = error ("Theorem must be of the form \"?p \ c \ c\", with c a constant or fixed parameter:\n" ^ - Syntax.string_of_term (Context.proof_of context) (prop_of thm)) + Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)) in - case prop_of thm of + case Thm.prop_of thm of Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' => if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then c @@ -151,7 +155,7 @@ ( if Item_Net.member (EqvtData.get context) thm then warning ("Theorem already declared as equivariant:\n" ^ - Syntax.string_of_term (Context.proof_of context) (prop_of thm)) + Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)) else (); EqvtData.map (Item_Net.update thm) context ) @@ -162,7 +166,7 @@ EqvtData.map (Item_Net.remove thm) context else ( warning ("Cannot delete non-existing equivariance theorem:\n" ^ - Syntax.string_of_term (Context.proof_of context) (prop_of thm)); + Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)); context ) ) @@ -187,7 +191,7 @@ fun thm_4_of_1 ctxt thm = let - val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop + val (p, c) = thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt) val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt @@ -209,7 +213,7 @@ let val ss_thms = @{thms "permute_minus_cancel"(2)} in - EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac, + EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt, rtac @{thm "permute_boolI"}, dtac thm', full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] end @@ -218,7 +222,7 @@ fun thm_1_of_2 ctxt thm = let - val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop + val (prem, concl) = thm |> Thm.prop_of |> Logic.dest_implies |> apply2 HOLogic.dest_Trueprop (* since argument terms "?p \ ?x1" may actually be eta-expanded or tuples, we need the following function to find ?p *) fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p @@ -228,10 +232,9 @@ val p = concl |> dest_comb |> snd |> find_perm val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt - val certify = cterm_of (theory_of_thm thm) - val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm + val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm in - Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1) + Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1) |> singleton (Proof_Context.export ctxt' ctxt) end handle TERM _ => @@ -254,7 +257,7 @@ (* Transforms a theorem of the form (1) or (2) into the form (4). *) fun eqvt_transform ctxt thm = - (case prop_of thm of @{const "Trueprop"} $ _ => + (case Thm.prop_of thm of @{const "Trueprop"} $ _ => thm_4_of_1 ctxt thm | @{const Pure.imp} $ _ $ _ => thm_4_of_1 ctxt (thm_1_of_2 ctxt thm) @@ -268,7 +271,7 @@ (3)) and (4); transforms a theorem of the form (2) into theorems of the form (3) and (4). *) fun eqvt_and_raw_transform ctxt thm = - (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) => + (case Thm.prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) => let val th' = if fastype_of c_args = @{typ "bool"} @@ -310,15 +313,11 @@ val eqvt_add = eqvt_add_or_del add_thm add_raw_thm val eqvt_del = eqvt_add_or_del del_thm del_raw_thm - -(** setup function **) - -val setup = - Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) - "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \ c \ c" #> - Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) - "Declaration of raw equivariance lemmas - no transformation is performed" #> - Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> - Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw) +val _ = + Theory.setup + (Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) + "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \ c \ c" #> + Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) + "Declaration of raw equivariance lemmas - no transformation is performed") end;