nominal2: comparison Nominal/nominal_function

equal deleted inserted replaced

-:4af8a92396ce
+:c4f31f1564b7
 -> (term   (* f *)
 * term (* G(raph) *)
 * thm list (* GIntros *)
 * thm (* Ginduct *)
 * thm  (* goalstate *)
-* (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
+* (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
 ) * local_theory
 val inductive_def : (binding * typ) * mixfix -> term list -> local_theory
 -> (term * thm list * thm * thm) * local_theory
 end
 |> Thm.forall_intr (Thm.cterm_of ctxt y)
 val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 val exactly_one =
-ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
+ex1I |> Thm.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 ctxt addsimps [case_hyp RS sym])
 |> Thm.implies_intr (Thm.cprop_of case_hyp)
 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
 |> 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 (Thm.cterm_of ctxt h)]
+|> Thm.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 ctxt h ih_elim) clauses
 (* wrapper -- restores quantifiers in rule specifications *)
 fun inductive_def (binding as ((R, T), _)) intrs lthy =
 let
 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
 lthy
+|> Config.put Inductive.inductive_internals true
 |> Proof_Context.concealed
 |> Inductive.add_inductive_i
 {quiet_mode = true,
 verbose = ! trace,
 alt_name = Binding.empty,
 [binding] (* relation *)
 [] (* no parameters *)
 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
 [] (* no special monos *)
 ||> Proof_Context.restore_naming lthy
+||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals)
 val cert = Thm.cterm_of lthy
 fun requantify orig_intro thm =
 let
 val (qs, t) = dest_all_all orig_intro
 val simple_induct_rule =
 subset_induct_rule
 |> Thm.forall_intr (Thm.cterm_of ctxt D)
 |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
-|> atac 1 |> Seq.hd
+|> assume_tac ctxt 1 |> Seq.hd
 |> (curry op COMP) (acc_downward
-|> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
+|> (Thm.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)
 val (goalstate, values) = PROFILE "prove_stuff"
 (prove_stuff lthy globals G f R xclauses complete compat
 compat_store G_elim G_eqvt invariant) f_defthm
-fun mk_partial_rules provedgoal =
+fun mk_partial_rules newctxt provedgoal =
 let
-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
 |> Conjunction.elim
 |>> fst o Conjunction.elim
 |>> Conjunction.elim

branch	Nominal2-Isabelle2016
changeset 3243	c4f31f1564b7
parent 3239	67370521c09c
child 3245	017e33849f4d