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