63 let val ks = 1 upto n in |
63 let val ks = 1 upto n in |
64 HEADGOAL (atac ORELSE' |
64 HEADGOAL (atac ORELSE' |
65 cut_tac nchotomy THEN' |
65 cut_tac nchotomy THEN' |
66 K (exhaust_inst_as_projs_tac ctxt frees) THEN' |
66 K (exhaust_inst_as_projs_tac ctxt frees) THEN' |
67 EVERY' (map (fn k => |
67 EVERY' (map (fn k => |
68 (if k < n then etac disjE else K all_tac) THEN' |
68 (if k < n then etac ctxt disjE else K all_tac) THEN' |
69 REPEAT o (dtac meta_mp THEN' atac ORELSE' |
69 REPEAT o (dtac ctxt meta_mp THEN' atac ORELSE' |
70 etac conjE THEN' dtac meta_mp THEN' atac ORELSE' |
70 etac ctxt conjE THEN' dtac ctxt meta_mp THEN' atac ORELSE' |
71 atac)) |
71 atac)) |
72 ks)) |
72 ks)) |
73 end; |
73 end; |
74 |
74 |
75 fun mk_primcorec_assumption_tac ctxt discIs = |
75 fun mk_primcorec_assumption_tac ctxt discIs = |
76 SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
76 SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
77 not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
77 not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
78 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
78 SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' atac ORELSE' etac ctxt conjE ORELSE' |
79 eresolve_tac ctxt falseEs ORELSE' |
79 eresolve_tac ctxt falseEs ORELSE' |
80 resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE' |
80 resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE' |
81 dresolve_tac ctxt discIs THEN' atac ORELSE' |
81 dresolve_tac ctxt discIs THEN' atac ORELSE' |
82 etac notE THEN' atac ORELSE' |
82 etac ctxt notE THEN' atac ORELSE' |
83 etac disjE)))); |
83 etac ctxt disjE)))); |
84 |
84 |
85 fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt); |
85 fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt); |
86 |
86 |
87 fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt); |
87 fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt); |
88 |
88 |
89 fun same_case_tac ctxt m = |
89 fun same_case_tac ctxt m = |
90 HEADGOAL (if m = 0 then rtac TrueI |
90 HEADGOAL (if m = 0 then rtac ctxt TrueI |
91 else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt); |
91 else REPEAT_DETERM_N (m - 1) o (rtac ctxt conjI THEN' case_atac ctxt) THEN' case_atac ctxt); |
92 |
92 |
93 fun different_case_tac ctxt m exclude = |
93 fun different_case_tac ctxt m exclude = |
94 HEADGOAL (if m = 0 then |
94 HEADGOAL (if m = 0 then |
95 mk_primcorec_assumption_tac ctxt [] |
95 mk_primcorec_assumption_tac ctxt [] |
96 else |
96 else |
97 dtac exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN' |
97 dtac ctxt exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN' |
98 mk_primcorec_assumption_tac ctxt []); |
98 mk_primcorec_assumption_tac ctxt []); |
99 |
99 |
100 fun cases_tac ctxt k m excludesss = |
100 fun cases_tac ctxt k m excludesss = |
101 let val n = length excludesss in |
101 let val n = length excludesss in |
102 EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
102 EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
103 | [exclude] => different_case_tac ctxt m exclude) |
103 | [exclude] => different_case_tac ctxt m exclude) |
104 (take k (nth excludesss (k - 1)))) |
104 (take k (nth excludesss (k - 1)))) |
105 end; |
105 end; |
106 |
106 |
107 fun prelude_tac ctxt defs thm = |
107 fun prelude_tac ctxt defs thm = |
108 unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets; |
108 unfold_thms_tac ctxt defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets; |
109 |
109 |
110 fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss = |
110 fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss = |
111 prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss; |
111 prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss; |
112 |
112 |
113 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss |
113 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss |
114 distinct_discs = |
114 distinct_discs = |
115 HEADGOAL (rtac iffI THEN' |
115 HEADGOAL (rtac ctxt iffI THEN' |
116 rtac fun_exhaust THEN' |
116 rtac ctxt fun_exhaust THEN' |
117 K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN' |
117 K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN' |
118 EVERY' (map (fn [] => etac FalseE |
118 EVERY' (map (fn [] => etac ctxt FalseE |
119 | fun_discs' as [fun_disc'] => |
119 | fun_discs' as [fun_disc'] => |
120 if eq_list Thm.eq_thm (fun_discs', fun_discs) then |
120 if eq_list Thm.eq_thm (fun_discs', fun_discs) then |
121 REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI) |
121 REPEAT_DETERM o etac ctxt conjI THEN' (atac ORELSE' rtac ctxt TrueI) |
122 else |
122 else |
123 rtac FalseE THEN' |
123 rtac ctxt FalseE THEN' |
124 (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT o atac ORELSE' |
124 (rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o atac ORELSE' |
125 cut_tac fun_disc') THEN' |
125 cut_tac fun_disc') THEN' |
126 dresolve_tac ctxt distinct_discs THEN' etac notE THEN' atac) |
126 dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' atac) |
127 fun_discss) THEN' |
127 fun_discss) THEN' |
128 (etac FalseE ORELSE' |
128 (etac ctxt FalseE ORELSE' |
129 resolve_tac ctxt (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac)); |
129 resolve_tac ctxt (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac)); |
130 |
130 |
131 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k |
131 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k |
132 m excludesss = |
132 m excludesss = |
133 prelude_tac ctxt defs (fun_sel RS trans) THEN |
133 prelude_tac ctxt defs (fun_sel RS trans) THEN |
134 cases_tac ctxt k m excludesss THEN |
134 cases_tac ctxt k m excludesss THEN |
135 HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' |
135 HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE' |
136 eresolve_tac ctxt falseEs ORELSE' |
136 eresolve_tac ctxt falseEs ORELSE' |
137 resolve_tac ctxt split_connectI ORELSE' |
137 resolve_tac ctxt split_connectI ORELSE' |
138 Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' |
138 Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' |
139 Splitter.split_tac ctxt (split_if :: splits) ORELSE' |
139 Splitter.split_tac ctxt (split_if :: splits) ORELSE' |
140 eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
140 eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
141 etac notE THEN' atac ORELSE' |
141 etac ctxt notE THEN' atac ORELSE' |
142 (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def |
142 (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def |
143 sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ |
143 sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ |
144 mapsx @ map_ident0s @ map_comps))) ORELSE' |
144 mapsx @ map_ident0s @ map_comps))) ORELSE' |
145 fo_rtac @{thm cong} ctxt ORELSE' |
145 fo_rtac ctxt @{thm cong} ORELSE' |
146 rtac @{thm ext} ORELSE' |
146 rtac ctxt @{thm ext} ORELSE' |
147 mk_primcorec_assumption_tac ctxt [])); |
147 mk_primcorec_assumption_tac ctxt [])); |
148 |
148 |
149 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
149 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
150 HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
150 HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
151 (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
151 (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
152 unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl); |
152 unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl); |
153 |
153 |
154 fun inst_split_eq ctxt split = |
154 fun inst_split_eq ctxt split = |
155 (case Thm.prop_of split of |
155 (case Thm.prop_of split of |
156 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |
156 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |
157 let |
157 let |