equal
deleted
inserted
replaced
147 HEADGOAL (rtac ctor_induct' THEN' inst_as_projs_tac ctxt) THEN |
147 HEADGOAL (rtac ctor_induct' THEN' inst_as_projs_tac ctxt) THEN |
148 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss |
148 EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss |
149 mss (unflat mss (1 upto n)) kkss) |
149 mss (unflat mss (1 upto n)) kkss) |
150 end; |
150 end; |
151 |
151 |
152 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = |
152 fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = |
153 hyp_subst_tac ctxt THEN' |
153 hyp_subst_tac ctxt THEN' |
154 CONVERSION (hhf_concl_conv |
154 CONVERSION (hhf_concl_conv |
155 (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN' |
155 (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN' |
156 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN' |
156 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN' |
157 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN' |
157 SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN' |
159 full_simp_tac |
159 full_simp_tac |
160 (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN' |
160 (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN' |
161 REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' |
161 REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' |
162 REPEAT o rtac refl); |
162 REPEAT o rtac refl); |
163 |
163 |
164 fun mk_coinduct_distinct_ctrs ctxt discs discs' = |
164 fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' = |
165 hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN' |
165 hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN' |
166 full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt); |
166 full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt); |
167 |
167 |
168 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs |
168 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs |
169 discss selss = |
169 discss selss = |
173 hyp_subst_tac ctxt] @ |
173 hyp_subst_tac ctxt] @ |
174 map4 (fn k => fn ctr_def => fn discs => fn sels => |
174 map4 (fn k => fn ctr_def => fn discs => fn sels => |
175 EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @ |
175 EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @ |
176 map2 (fn k' => fn discs' => |
176 map2 (fn k' => fn discs' => |
177 if k' = k then |
177 if k' = k then |
178 mk_coinduct_same_ctr ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels |
178 mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels |
179 else |
179 else |
180 mk_coinduct_distinct_ctrs ctxt discs discs') ks discss)) ks ctr_defs discss selss) |
180 mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss) |
181 end; |
181 end; |
182 |
182 |
183 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss |
183 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss |
184 discsss selsss = |
184 discsss selsss = |
185 HEADGOAL (rtac dtor_coinduct' THEN' |
185 HEADGOAL (rtac dtor_coinduct' THEN' |