equal
deleted
inserted
replaced
170 apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1)) |
170 apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1)) |
171 apply(blast) |
171 apply(blast) |
172 apply(auto simp add: fresh_star_def)[1] |
172 apply(auto simp add: fresh_star_def)[1] |
173 apply(blast) |
173 apply(blast) |
174 apply(simp) |
174 apply(simp) |
175 apply(blast) |
|
176 apply(simp) |
|
177 apply(case_tac b) |
175 apply(case_tac b) |
178 apply(simp) |
176 apply(simp) |
179 apply(case_tac a) |
177 apply(case_tac a) |
180 apply(simp) |
178 apply(simp) |
181 apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2)) |
179 apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2)) |
190 apply(blast) |
188 apply(blast) |
191 apply(blast) |
189 apply(blast) |
192 apply(blast) |
190 apply(blast) |
193 using [[simproc del: alpha_lst]] |
191 using [[simproc del: alpha_lst]] |
194 apply(auto simp add: fresh_star_def)[1] |
192 apply(auto simp add: fresh_star_def)[1] |
195 apply(blast) |
193 apply(simp) |
196 apply(simp) |
|
197 apply(blast) |
|
198 --"compatibility" |
194 --"compatibility" |
199 apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
195 apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
200 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
196 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
201 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
197 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
202 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |
198 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |