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 -> bclause list list list -> thm |
46 end |
46 end |
47 |
47 |
48 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
48 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
49 struct |
49 struct |
|
50 |
|
51 fun lookup xs x = the (AList.lookup (op=) xs x) |
50 |
52 |
51 |
53 |
52 (* defines the quotient types *) |
54 (* defines the quotient types *) |
53 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
55 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
54 let |
56 let |
377 |> ProofContext.export ctxt' ctxt |
379 |> ProofContext.export ctxt' ctxt |
378 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
380 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
379 end |
381 end |
380 |
382 |
381 |
383 |
382 (** proves strong exhauts theorems **) |
384 |
383 |
385 (*** proves strong exhauts theorems ***) |
384 |
386 |
385 (* fixme: move into nominal_library *) |
387 (* fixme: move into nominal_library *) |
386 fun abs_const bmode ty = |
388 fun abs_const bmode ty = |
387 let |
389 let |
388 val (const_name, binder_ty, abs_ty) = |
390 val (const_name, binder_ty, abs_ty) = |
627 |> incr_boundvars 1 |
629 |> incr_boundvars 1 |
628 |> add_c_prop (Bound 0) c_ty |
630 |> add_c_prop (Bound 0) c_ty |
629 |> HOLogic.mk_Trueprop |
631 |> HOLogic.mk_Trueprop |
630 |> mk_all (c_name, c_ty) |
632 |> mk_all (c_name, c_ty) |
631 |
633 |
632 fun prep_prem lthy c (c_name, c_ty) bclauses (params, prems, concl) = |
634 fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) = |
633 let |
635 let |
634 val tys = map snd params |
636 val tys = map snd params |
635 val binders = get_all_binders bclauses |
637 val binders = get_all_binders bclauses |
636 |
638 |
637 fun prep_binder (opt, i) = |
639 fun prep_binder (opt, i) = |
684 |> map (add_c_prop c c_ty) |
686 |> map (add_c_prop c c_ty) |
685 |> map HOLogic.mk_Trueprop |
687 |> map HOLogic.mk_Trueprop |
686 |
688 |
687 val prems' = prems |
689 val prems' = prems |
688 |> map strip_full_horn |
690 |> map strip_full_horn |
689 |> map2 (prep_prem lthy'' c (c_name, c_ty)) (flat bclausesss) |
691 |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss) |
690 |> map (Syntax.check_term lthy'') |
692 |
691 |
693 fun pat_tac ctxt thm = |
692 val _ = tracing ("induct:\n" ^ Syntax.string_of_term lthy'' (prop_of induct')) |
694 Subgoal.FOCUS (fn {params, context, ...} => |
693 val _ = tracing ("concls:\n" ^ commas (map (Syntax.string_of_term lthy'') concls)) |
695 let |
694 val _ = tracing ("prems':\n" ^ cat_lines (map (Syntax.string_of_term lthy'') prems')) |
696 val thy = ProofContext.theory_of context |
695 |
697 val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params |
|
698 val vs = Term.add_vars (prop_of thm) [] |
|
699 val vs_tys = map (Type.legacy_freeze_type o snd) vs |
|
700 val vs_ctrms = map (cterm_of thy o Var) vs |
|
701 val assigns = map (lookup ty_parms) vs_tys |
|
702 |
|
703 val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm |
|
704 in |
|
705 rtac thm' 1 |
|
706 end) ctxt |
|
707 THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss |
|
708 |
696 val thm = Goal.prove_multi lthy'' [] prems' concls |
709 val thm = Goal.prove_multi lthy'' [] prems' concls |
697 (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy'')) |
710 (fn {prems, context} => |
|
711 print_tac "start" |
|
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 |
|
715 THEN print_tac "after pat" |
|
716 THEN Skip_Proof.cheat_tac (ProofContext.theory_of context) |
|
717 ) |
698 in |
718 in |
699 @{thm TrueI} |
719 @{thm TrueI} |
700 end |
720 end |
701 |
721 |
702 |
722 |