equal
deleted
inserted
replaced
75 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
75 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
76 apply (simp_all add: fresh_star_def)[12] |
76 apply (simp_all add: fresh_star_def)[12] |
77 apply(metis)+ |
77 apply(metis)+ |
78 -- "compatibility" |
78 -- "compatibility" |
79 apply(all_trivials) |
79 apply(all_trivials) |
|
80 using [[simproc del: alpha_lst]] |
80 apply(simp_all) |
81 apply(simp_all) |
81 apply(rule conjI) |
82 apply(rule conjI) |
82 apply(elim conjE) |
83 apply(elim conjE) |
83 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
84 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
84 apply(simp add: Abs_fresh_iff) |
85 apply(simp add: Abs_fresh_iff) |
278 apply(case_tac x) |
279 apply(case_tac x) |
279 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
280 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
280 apply (simp_all add: fresh_star_def)[12] |
281 apply (simp_all add: fresh_star_def)[12] |
281 apply(metis)+ |
282 apply(metis)+ |
282 -- "compatibility" |
283 -- "compatibility" |
|
284 using [[simproc del: alpha_lst]] |
283 apply(simp_all) |
285 apply(simp_all) |
284 apply(rule conjI) |
286 apply(rule conjI) |
285 apply(elim conjE) |
287 apply(elim conjE) |
286 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
288 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
287 apply(simp add: Abs_fresh_iff) |
289 apply(simp add: Abs_fresh_iff) |
477 apply(rule TrueI) |
479 apply(rule TrueI) |
478 -- "covered all cases" |
480 -- "covered all cases" |
479 apply(case_tac x) |
481 apply(case_tac x) |
480 apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust) |
482 apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust) |
481 apply (simp_all add: fresh_star_def fresh_Pair)[12] |
483 apply (simp_all add: fresh_star_def fresh_Pair)[12] |
482 apply(metis)+ |
484 apply(metis) |
483 apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)") |
|
484 apply(auto simp add: fresh_Pair)[1] |
|
485 apply(metis)+ |
|
486 apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)") |
|
487 apply(auto simp add: fresh_Pair)[1] |
|
488 apply(rule obtain_fresh) |
|
489 apply(auto)[1] |
|
490 apply(metis)+ |
|
491 -- "compatibility" |
|
492 apply(all_trivials) |
|
493 apply(simp) |
|
494 oops |
485 oops |
495 |
486 |
496 end |
487 end |
497 |
488 |
498 |
489 |