equal
deleted
inserted
replaced
259 |
259 |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
261 |
261 |
262 val {fs, simps, inducts, ...} = info; |
262 val {fs, simps, inducts, ...} = info; |
263 |
263 |
264 val morphism = Proof_Context.export_morphism lthy'' lthy |
264 val morphism = |
|
265 Proof_Context.export_morphism lthy'' |
|
266 (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy) |
265 val simps_exp = map (Morphism.thm morphism) (the simps) |
267 val simps_exp = map (Morphism.thm morphism) (the simps) |
266 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
268 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
267 |
269 |
268 val (fvs', fv_bns') = chop (length fv_frees) fs |
270 val (fvs', fv_bns') = chop (length fv_frees) fs |
269 |
271 |
332 |
334 |
333 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
335 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
334 |
336 |
335 val {fs, simps, ...} = info; |
337 val {fs, simps, ...} = info; |
336 |
338 |
337 val morphism = Proof_Context.export_morphism lthy'' lthy |
339 val morphism = |
|
340 Proof_Context.export_morphism lthy'' |
|
341 (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy) |
338 val simps_exp = map (Morphism.thm morphism) (the simps) |
342 val simps_exp = map (Morphism.thm morphism) (the simps) |
339 in |
343 in |
340 (fs, simps_exp, lthy'') |
344 (fs, simps_exp, lthy'') |
341 end |
345 end |
342 |
346 |
353 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
357 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
354 |
358 |
355 val goals = |
359 val goals = |
356 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
360 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
357 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
361 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
358 |
362 in |
359 val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs) |
363 Goal.prove ctxt perm_indnames [] goals |
360 |
364 (fn {context = ctxt', ...} => |
361 val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames |
365 (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW |
362 THEN_ALL_NEW asm_simp_tac simpset) 1 |
366 asm_simp_tac |
363 in |
367 (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_zero} :: perm_defs))) 1) |
364 Goal.prove ctxt perm_indnames [] goals (K tac) |
|
365 |> Old_Datatype_Aux.split_conj_thm |
368 |> Old_Datatype_Aux.split_conj_thm |
366 end |
369 end |
367 |
370 |
368 |
371 |
369 fun prove_permute_plus induct perm_defs perm_fns ctxt = |
372 fun prove_permute_plus induct perm_defs perm_fns ctxt = |
377 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
380 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
378 |
381 |
379 val goals = |
382 val goals = |
380 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
383 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
381 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
384 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
382 |
385 in |
383 (* FIXME proper goal context *) |
386 Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals |
384 val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs) |
387 (fn {context = ctxt', ...} => |
385 |
388 (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW |
386 val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames |
389 asm_simp_tac |
387 THEN_ALL_NEW asm_simp_tac simpset) 1 |
390 (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_plus} :: perm_defs))) 1) |
388 in |
|
389 Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac) |
|
390 |> Old_Datatype_Aux.split_conj_thm |
391 |> Old_Datatype_Aux.split_conj_thm |
391 end |
392 end |
392 |
393 |
393 |
394 |
394 fun mk_perm_eq ty_perm_assoc cnstr = |
395 fun mk_perm_eq ty_perm_assoc cnstr = |