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 -> thm list -> tactic |
10 val mk_primcorec_assumption_tac: Proof.context -> thm list -> tactic |
11 val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
11 val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
12 thm list -> int list -> thm list -> tactic |
12 int list -> thm list -> tactic |
13 val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> thm list -> tactic |
13 val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> tactic |
14 val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic |
14 val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic |
15 val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> |
15 val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> |
16 tactic |
16 tactic |
17 val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
17 val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> |
18 thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic |
18 thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic |
81 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs = |
81 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs = |
82 HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN' |
82 HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN' |
83 (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN |
83 (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN |
84 unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); |
84 unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); |
85 |
85 |
86 (* TODO: do we need "collapses"? *) |
|
87 (* TODO: reduce code duplication with selector tactic above *) |
86 (* TODO: reduce code duplication with selector tactic above *) |
88 fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr = |
87 fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr = |
89 HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN |
88 HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN |
90 mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN |
89 mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN |
91 REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN |
90 REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN |
92 HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o |
91 HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o |
93 (rtac refl ORELSE' atac ORELSE' |
92 (rtac refl ORELSE' atac ORELSE' |
94 eresolve_tac (falseEs @ map (fn thm => thm RS trans) collapses) ORELSE' |
|
95 resolve_tac split_connectI ORELSE' |
93 resolve_tac split_connectI ORELSE' |
96 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
94 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
97 Splitter.split_tac (split_if :: splits) ORELSE' |
95 Splitter.split_tac (split_if :: splits) ORELSE' |
98 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
96 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
99 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))); |
97 (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))); |
100 |
98 |
101 fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs collapses splits split_asms ms ctr_thms = |
99 fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms = |
102 EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits |
100 EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) |
103 split_asms) ms ctr_thms); |
101 ms ctr_thms); |
104 |
102 |
105 fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses = |
103 fun mk_primcorec_code_of_raw_tac splits disc_excludes raw = |
106 HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o |
104 HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o |
107 (rtac refl ORELSE' |
105 (rtac refl ORELSE' |
108 (TRY o rtac sym) THEN' atac ORELSE' |
106 (TRY o rtac sym) THEN' atac ORELSE' |
109 resolve_tac split_connectI ORELSE' |
107 resolve_tac split_connectI ORELSE' |
110 Splitter.split_tac (split_if :: splits) ORELSE' |
108 Splitter.split_tac (split_if :: splits) ORELSE' |
111 etac notE THEN' atac ORELSE' |
109 etac notE THEN' atac ORELSE' |
112 dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE' |
110 (TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac)); |
113 eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses))); |
111 |
114 |
112 |
115 end; |
113 end; |