79 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
79 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
80 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
80 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
81 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
81 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
82 |
82 |
83 val defname = mk_defname fixes |
83 val defname = mk_defname fixes |
84 val FunctionConfig {partials, tailrec, default, ...} = config |
84 val FunctionConfig {partials, default, ...} = config |
85 val _ = |
|
86 if tailrec then Output.legacy_feature |
|
87 "'function (tailrec)' command. Use 'partial_function (tailrec)'." |
|
88 else () |
|
89 val _ = |
85 val _ = |
90 if is_some default then Output.legacy_feature |
86 if is_some default then Output.legacy_feature |
91 "'function (default)'. Use 'partial_function'." |
87 "'function (default)'. Use 'partial_function'." |
92 else () |
88 else () |
93 |
89 |
94 val ((goal_state, cont), lthy') = |
90 val ((goal_state, cont), lthy') = |
95 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
91 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
96 |
92 |
97 fun afterqed [[proof]] lthy = |
93 fun afterqed [[proof]] lthy = |
98 let |
94 let |
99 val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, |
95 val FunctionResult {fs, R, psimps, simple_pinducts, |
100 termination, domintros, cases, ...} = |
96 termination, domintros, cases, ...} = |
101 cont (Thm.close_derivation proof) |
97 cont (Thm.close_derivation proof) |
102 |
98 |
103 val fnames = map (fst o fst) fixes |
99 val fnames = map (fst o fst) fixes |
104 fun qualify n = Binding.name n |
100 fun qualify n = Binding.name n |
109 |
105 |
110 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
106 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
111 lthy |
107 lthy |
112 |> addsmps (conceal_partial o Binding.qualify false "partial") |
108 |> addsmps (conceal_partial o Binding.qualify false "partial") |
113 "psimps" conceal_partial psimp_attribs psimps |
109 "psimps" conceal_partial psimp_attribs psimps |
114 ||> (case trsimps of NONE => I | SOME thms => |
|
115 addsmps I "simps" I simp_attribs thms #> snd |
|
116 #> Spec_Rules.add Spec_Rules.Equational (fs, thms)) |
|
117 ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
110 ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
118 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
111 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
119 Attrib.internal (K (Rule_Cases.consumes 1)), |
112 Attrib.internal (K (Rule_Cases.consumes 1)), |
120 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
113 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
121 ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
114 ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |