equal
deleted
inserted
replaced
140 else |
140 else |
141 let |
141 let |
142 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
142 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
143 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
143 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
144 |
144 |
145 val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) |
145 val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1) |
146 val {fs, simps, inducts, ...} = info |
146 val {fs, simps, inducts, ...} = info |
147 |
147 |
148 val raw_bn_induct = (the inducts) |
148 val raw_bn_induct = (the inducts) |
149 val raw_bn_eqs = the simps |
149 val raw_bn_eqs = the simps |
150 |
150 |
275 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
275 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
276 |
276 |
277 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
277 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
278 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
278 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
279 |
279 |
280 val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') |
280 val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy') |
281 |
281 |
282 val {fs, simps, inducts, ...} = info; |
282 val {fs, simps, inducts, ...} = info; |
283 |
283 |
284 val morphism = ProofContext.export_morphism lthy'' lthy |
284 val morphism = ProofContext.export_morphism lthy'' lthy |
285 val simps_exp = map (Morphism.thm morphism) (the simps) |
285 val simps_exp = map (Morphism.thm morphism) (the simps) |
340 val prod_simps = @{thms prod.inject HOL.simp_thms} |
340 val prod_simps = @{thms prod.inject HOL.simp_thms} |
341 |
341 |
342 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
342 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
343 Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy |
343 Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy |
344 |
344 |
345 val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy') |
345 val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy') |
346 |
346 |
347 val {fs, simps, ...} = info; |
347 val {fs, simps, ...} = info; |
348 |
348 |
349 val morphism = ProofContext.export_morphism lthy'' lthy |
349 val morphism = ProofContext.export_morphism lthy'' lthy |
350 val simps_exp = map (Morphism.thm morphism) (the simps) |
350 val simps_exp = map (Morphism.thm morphism) (the simps) |