70 end; |
70 end; |
71 |
71 |
72 fun mk_primcorec_assumption_tac ctxt discIs = |
72 fun mk_primcorec_assumption_tac ctxt discIs = |
73 SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
73 SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True |
74 not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
74 not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
75 SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' etac ctxt conjE ORELSE' |
75 SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' |
|
76 etac ctxt conjE ORELSE' |
76 eresolve_tac ctxt falseEs ORELSE' |
77 eresolve_tac ctxt falseEs ORELSE' |
77 resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE' |
78 resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE' |
78 dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE' |
79 dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE' |
79 etac ctxt notE THEN' assume_tac ctxt ORELSE' |
80 etac ctxt notE THEN' assume_tac ctxt ORELSE' |
80 etac ctxt disjE)))); |
81 etac ctxt disjE)))); |
135 HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE' |
136 HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE' |
136 eresolve_tac ctxt falseEs ORELSE' |
137 eresolve_tac ctxt falseEs ORELSE' |
137 resolve_tac ctxt split_connectI ORELSE' |
138 resolve_tac ctxt split_connectI ORELSE' |
138 Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' |
139 Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' |
139 Splitter.split_tac ctxt (split_if :: splits) ORELSE' |
140 Splitter.split_tac ctxt (split_if :: splits) ORELSE' |
140 eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE' |
141 eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' |
|
142 assume_tac ctxt ORELSE' |
141 etac ctxt notE THEN' assume_tac ctxt ORELSE' |
143 etac ctxt notE THEN' assume_tac ctxt ORELSE' |
142 (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def |
144 (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]]} @ |
145 sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ |
144 mapsx @ map_ident0s @ map_comps))) ORELSE' |
146 mapsx @ map_ident0s @ map_comps))) ORELSE' |
145 fo_rtac ctxt @{thm cong} ORELSE' |
147 fo_rtac ctxt @{thm cong} ORELSE' |
146 rtac ctxt @{thm ext} ORELSE' |
148 rtac ctxt @{thm ext} ORELSE' |
147 mk_primcorec_assumption_tac ctxt [])); |
149 mk_primcorec_assumption_tac ctxt [])); |
148 |
150 |
149 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
151 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
150 HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
152 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 ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o assume_tac ctxt) THEN |
153 (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' |
|
154 REPEAT_DETERM_N m o assume_tac ctxt) THEN |
152 unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl); |
155 unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl); |
153 |
156 |
154 fun inst_split_eq ctxt split = |
157 fun inst_split_eq ctxt split = |
155 (case Thm.prop_of split of |
158 (case Thm.prop_of split of |
156 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |
159 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |