# HG changeset patch # User wenzelm # Date 1634255092 -7200 # Node ID fc65e39ca170c7d3693bf6a7889c506a86142512 # Parent de4f151c2a3459706916453034734e77f59bc677 clarified context; diff -r de4f151c2a34 -r fc65e39ca170 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Oct 14 16:03:20 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Oct 15 01:44:52 2021 +0200 @@ -25,7 +25,7 @@ (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize); fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt)); fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt)); + (Conv.params_conv ~1 (fn ctxt' => Conv.prems_conv ~1 (atomize_conv ctxt')) ctxt)); fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []); @@ -131,10 +131,10 @@ let val prop = Thm.prop_of th; fun prove t = - Goal.prove ctxt [] [] t (fn _ => - EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1, - REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)), - REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))]) + Goal.prove ctxt [] [] t (fn {context = goal_ctxt, ...} => + EVERY [cut_facts_tac [th] 1, eresolve_tac goal_ctxt [rev_mp] 1, + REPEAT_DETERM (FIRSTGOAL (resolve_tac goal_ctxt monos)), + REPEAT_DETERM (resolve_tac goal_ctxt [impI] 1 THEN (assume_tac goal_ctxt 1 ORELSE tac))]) in Option.map prove (map_term f prop (the_default prop opt)) end; val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion; @@ -349,19 +349,19 @@ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z]))) ihyp; fun mk_pi th = - Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}] + Simplifier.simplify (put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}] addsimprocs [NominalDatatype.perm_simproc]) - (Simplifier.simplify (put_simpset eqvt_ss ctxt') - (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt') + (Simplifier.simplify (put_simpset eqvt_ss ctxt'') + (fold_rev (mk_perm_bool ctxt'' o Thm.cterm_of ctxt'') (rev pis' @ pis) th)); val (gprems1, gprems2) = split_list (map (fn (th, t) => if null (preds_of ps t) then (SOME th, mk_pi th) else - (map_thm ctxt' (split_conj (K o I) names) - (eresolve_tac ctxt' [conjunct1] 1) monos NONE th, - mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis'')) - (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))) + (map_thm ctxt'' (split_conj (K o I) names) + (eresolve_tac ctxt'' [conjunct1] 1) monos NONE th, + mk_pi (the (map_thm ctxt'' (inst_conj_all names ps (rev pis'')) + (inst_conj_all_tac ctxt'' (length pis'')) monos (SOME t) th)))) (gprems ~~ oprems)) |>> map_filter I; val vc_compat_ths' = map (fn th => let @@ -375,7 +375,7 @@ (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs) (fold_rev (NominalDatatype.mk_perm []) pis rhs))) (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps - (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt' [th'] 1) + (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt'' [th'] 1) in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end) vc_compat_ths; val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths'; @@ -588,15 +588,15 @@ (map (map (rulify_term thy #> rpair [])) vc_compat) end; -fun prove_eqvt s xatoms ctxt = (* FIXME ctxt should be called lthy *) +fun prove_eqvt s xatoms lthy = let - val thy = Proof_Context.theory_of ctxt; + val thy = Proof_Context.theory_of lthy; val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive_global ctxt (Sign.intern_const thy s); - val raw_induct = atomize_induct ctxt raw_induct; - val elims = map (atomize_induct ctxt) elims; - val intrs = map (atomize_intr ctxt) intrs; - val monos = Inductive.get_monos ctxt; + Inductive.the_inductive_global lthy (Sign.intern_const thy s); + val raw_induct = atomize_induct lthy raw_induct; + val elims = map (atomize_induct lthy) elims; + val intrs = map (atomize_intr lthy) intrs; + val monos = Inductive.get_monos lthy; val intrs' = Inductive.unpartition_rules intrs (map (fn (((s, ths), (_, k)), th) => (s, ths ~~ Inductive.infer_intro_vars thy th k ths)) @@ -617,43 +617,43 @@ atoms) end; val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; - val (([t], [pi]), ctxt') = ctxt |> + val (([t], [pi]), ctxt1) = lthy |> Variable.import_terms false [Thm.concl_of raw_induct] ||>> Variable.variant_fixes ["pi"]; - val eqvt_simpset = put_simpset HOL_basic_ss ctxt' addsimps - (NominalThmDecls.get_eqvt_thms ctxt' @ perm_pi_simp) addsimprocs + fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps + (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names, NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; val ps = map (fst o HOLogic.dest_imp) (HOLogic.dest_conj (HOLogic.dest_Trueprop t)); - fun eqvt_tac pi (intr, vs) st = + fun eqvt_tac ctxt pi (intr, vs) st = let fun eqvt_err s = - let val ([t], ctxt'') = Variable.import_terms true [Thm.prop_of intr] ctxt' + let val ([t], ctxt') = Variable.import_terms true [Thm.prop_of intr] ctxt in error ("Could not prove equivariance for introduction rule\n" ^ - Syntax.string_of_term ctxt'' t ^ "\n" ^ s) + Syntax.string_of_term ctxt' t ^ "\n" ^ s) end; val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} => let val prems' = map (fn th => the_default th (map_thm ctxt'' (split_conj (K I) names) (eresolve_tac ctxt'' [conjunct2] 1) monos NONE th)) prems; - val prems'' = map (fn th => Simplifier.simplify eqvt_simpset + val prems'' = map (fn th => Simplifier.simplify (eqvt_simpset ctxt'') (mk_perm_bool ctxt'' (Thm.cterm_of ctxt'' pi) th)) prems'; val intr' = infer_instantiate ctxt'' (map (#1 o dest_Var) vs ~~ map (Thm.cterm_of ctxt'' o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params) intr in (resolve_tac ctxt'' [intr'] THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1 - end) ctxt' 1 st + end) ctxt 1 st in case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of NONE => eqvt_err ("Rule does not match goal\n" ^ - Syntax.string_of_term ctxt' (hd (Thm.prems_of st))) + Syntax.string_of_term ctxt (hd (Thm.prems_of st))) | SOME (th, _) => Seq.single th end; val thss = map (fn atom => let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, []))) in map (fn th => zero_var_indexes (th RS mp)) - (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] + (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt1 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => let val (h, ts) = strip_comb p; @@ -662,13 +662,14 @@ HOLogic.mk_imp (p, list_comb (h, ts1 @ map (NominalDatatype.mk_perm [] pi') ts2)) end) ps))) - (fn _ => EVERY (resolve_tac ctxt' [raw_induct] 1 :: map (fn intr_vs => - full_simp_tac eqvt_simpset 1 THEN - eqvt_tac pi' intr_vs) intrs')) |> - singleton (Proof_Context.export ctxt' ctxt))) + (fn {context = ctxt'', ...} => + EVERY (resolve_tac ctxt'' [raw_induct] 1 :: map (fn intr_vs => + full_simp_tac (eqvt_simpset ctxt'') 1 THEN + eqvt_tac ctxt'' pi' intr_vs) intrs')) |> + singleton (Proof_Context.export ctxt1 lthy))) end) atoms in - ctxt |> + lthy |> Local_Theory.notes (map (fn (name, ths) => ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))