equal
deleted
inserted
replaced
88 apply simp_all |
88 apply simp_all |
89 apply(case_tac x) |
89 apply(case_tac x) |
90 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
90 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
91 apply(auto simp add: fresh_star_def) |
91 apply(auto simp add: fresh_star_def) |
92 apply(erule Abs1_eq_fdest) |
92 apply(erule Abs1_eq_fdest) |
93 defer |
93 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
94 apply simp_all |
94 apply (simp add: fresh_star_def) |
|
95 apply (rule fcb3) |
|
96 apply (simp add: fresh_star_def) |
95 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
97 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
96 apply (simp add: fresh_at_base) |
98 apply (simp add: fresh_at_base) |
97 apply assumption |
99 apply assumption |
98 apply (erule fresh_eqvt_at) |
100 apply (erule fresh_eqvt_at) |
99 apply (simp add: finite_supp) |
101 apply (simp add: finite_supp) |
102 apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)") |
104 apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)") |
103 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la") |
105 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la") |
104 apply (simp add: eqvt_at_def) |
106 apply (simp add: eqvt_at_def) |
105 apply (simp add: swap_fresh_fresh) |
107 apply (simp add: swap_fresh_fresh) |
106 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
108 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
107 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
109 apply simp |
108 apply (simp add: fresh_star_def) |
110 done |
109 apply (rule fcb3) |
|
110 apply (rule_tac x="x # la" in meta_spec) |
|
111 unfolding fresh_star_def |
|
112 --"Exactly the assumption just for the other argument" |
|
113 sorry |
|
114 |
111 |
115 termination |
112 termination |
116 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
113 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
117 |
114 |
118 end |
115 end |