equal
deleted
inserted
replaced
40 thm list -> Proof.context -> thm list |
40 thm list -> Proof.context -> thm list |
41 |
41 |
42 val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> |
42 val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> |
43 thm list -> thm list -> thm list -> thm list -> thm list |
43 thm list -> thm list -> thm list -> thm list -> thm list |
44 |
44 |
45 val prove_strong_induct: Proof.context -> thm -> thm list -> bclause list list list -> thm |
45 val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> |
|
46 thm list |
46 end |
47 end |
47 |
48 |
48 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
49 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
49 struct |
50 struct |
50 |
51 |
666 |> HOLogic.mk_Trueprop |
667 |> HOLogic.mk_Trueprop |
667 in |
668 in |
668 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
669 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
669 end |
670 end |
670 |
671 |
671 fun prove_strong_induct lthy induct exhausts bclausesss = |
672 fun prove_strong_induct lthy induct exhausts size_thms bclausesss = |
672 let |
673 let |
673 val ((insts, [induct']), lthy') = Variable.import true [induct] lthy |
674 val ((insts, [induct']), lthy') = Variable.import true [induct] lthy |
674 |
675 |
675 val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
676 val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
676 val c_ty = TFree (a, @{sort fs}) |
677 val c_ty = TFree (a, @{sort fs}) |
704 in |
705 in |
705 rtac thm' 1 |
706 rtac thm' 1 |
706 end) ctxt |
707 end) ctxt |
707 THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss |
708 THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss |
708 |
709 |
709 val thm = Goal.prove_multi lthy'' [] prems' concls |
710 val size_simp_tac = |
|
711 simp_tac (size_simpset addsimps (@{thms comp_def snd_conv} @ size_thms)) |
|
712 in |
|
713 Goal.prove_multi lthy'' [] prems' concls |
710 (fn {prems, context} => |
714 (fn {prems, context} => |
711 print_tac "start" |
715 Induction_Schema.induction_schema_tac context prems |
712 THEN Induction_Schema.induction_schema_tac context prems |
|
713 THEN print_tac "after induct schema" |
|
714 THEN RANGE (map (pat_tac context) exhausts) 1 |
716 THEN RANGE (map (pat_tac context) exhausts) 1 |
715 THEN print_tac "after pat" |
717 THEN prove_termination_ind context 1 |
716 THEN Skip_Proof.cheat_tac (ProofContext.theory_of context) |
718 THEN ALLGOALS size_simp_tac) |
717 ) |
719 |> ProofContext.export lthy'' lthy |
718 in |
|
719 @{thm TrueI} |
|
720 end |
720 end |
721 |
721 |
722 |
722 |
723 end (* structure *) |
723 end (* structure *) |
724 |
724 |