7 |
7 |
8 signature BNF_FP_REC_SUGAR_TACTICS = |
8 signature BNF_FP_REC_SUGAR_TACTICS = |
9 sig |
9 sig |
10 val mk_primcorec_assumption_tac: Proof.context -> tactic |
10 val mk_primcorec_assumption_tac: Proof.context -> tactic |
11 val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic |
11 val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic |
12 val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic |
12 val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> tactic |
13 val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic |
13 val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic |
14 val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int -> |
14 val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int -> |
15 thm list list list -> thm list -> thm list -> thm list -> tactic |
15 thm list list list -> thm list -> thm list -> thm list -> tactic |
16 val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic; |
16 val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic; |
17 val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> |
17 val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> |
72 HEADGOAL (rtac discI THEN' rtac f_ctr) THEN ALLGOALS atac; |
72 HEADGOAL (rtac discI THEN' rtac f_ctr) THEN ALLGOALS atac; |
73 |
73 |
74 fun mk_primcorec_sel_of_ctr_tac sel f_ctr = |
74 fun mk_primcorec_sel_of_ctr_tac sel f_ctr = |
75 HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel); |
75 HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel); |
76 |
76 |
77 fun mk_primcorec_code_of_ctr_case_tac ctxt m f_ctr = |
77 fun mk_primcorec_code_of_ctr_case_tac ctxt f_ctr = |
78 HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN |
78 HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN |
79 mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN |
79 mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN |
80 REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN |
80 REPEAT_DETERM (mk_primcorec_assumption_tac ctxt) THEN |
81 HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)); |
81 HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)); |
82 |
82 |
83 fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms = |
83 fun mk_primcorec_code_of_ctr_tac ctxt ctr_thms = |
84 EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms); |
84 EVERY (map (mk_primcorec_code_of_ctr_case_tac ctxt) ctr_thms); |
85 |
85 |
86 fun mk_primcorec_code_tac ctxt raw collapses = |
86 fun mk_primcorec_code_tac ctxt raw collapses = |
87 HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN |
87 HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN |
88 Method.intros_tac @{thms conjI impI} [] THEN |
88 Method.intros_tac @{thms conjI impI} [] THEN |
89 REPEAT (HEADGOAL (rtac refl ORELSE' (etac notE THEN' atac) ORELSE' |
89 REPEAT (HEADGOAL (rtac refl ORELSE' (etac notE THEN' atac) ORELSE' |