88 val ((goal_state, cont), lthy') = |
88 val ((goal_state, cont), lthy') = |
89 Function_Mutual.prepare_function_mutual config defname fixes0 eqs lthy |
89 Function_Mutual.prepare_function_mutual config defname fixes0 eqs lthy |
90 |
90 |
91 fun afterqed [[proof]] lthy = |
91 fun afterqed [[proof]] lthy = |
92 let |
92 let |
93 val result = cont lthy (Thm.close_derivation proof) |
93 val result = cont lthy (Thm.close_derivation \<^here> proof) |
94 val FunctionResult {fs, R, dom, psimps, simple_pinducts, |
94 val FunctionResult {fs, R, dom, psimps, simple_pinducts, |
95 termination, domintros, cases, ...} = result |
95 termination, domintros, cases, ...} = result |
96 |
96 |
97 val pelims = Function_Elims.mk_partial_elim_rules lthy result |
97 val pelims = Function_Elims.mk_partial_elim_rules lthy result |
98 |
98 |
183 pinducts, defname, fnames, cases, dom, pelims, ...} = info |
183 pinducts, defname, fnames, cases, dom, pelims, ...} = info |
184 val domT = domain_type (fastype_of R) |
184 val domT = domain_type (fastype_of R) |
185 val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
185 val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
186 fun afterqed [[totality]] lthy = |
186 fun afterqed [[totality]] lthy = |
187 let |
187 let |
188 val totality = Thm.close_derivation totality |
188 val totality = Thm.close_derivation \<^here> totality |
189 val remove_domain_condition = |
189 val remove_domain_condition = |
190 full_simplify (put_simpset HOL_basic_ss lthy |
190 full_simplify (put_simpset HOL_basic_ss lthy |
191 addsimps [totality, @{thm True_implies_equals}]) |
191 addsimps [totality, @{thm True_implies_equals}]) |
192 val tsimps = map remove_domain_condition psimps |
192 val tsimps = map remove_domain_condition psimps |
193 val tinduct = map remove_domain_condition pinducts |
193 val tinduct = map remove_domain_condition pinducts |