85 apply(simp only: foo.eq_iff) |
85 apply(simp only: foo.eq_iff) |
86 apply(simp only: eqvts) |
86 apply(simp only: eqvts) |
87 apply simp |
87 apply simp |
88 done |
88 done |
89 |
89 |
|
90 lemma Let2_rename2: |
|
91 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(atom y) \<sharp> p" |
|
92 shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) y (p \<bullet> t1) t2" |
|
93 using assms |
|
94 apply - |
|
95 apply(drule supp_perm_eq[symmetric]) |
|
96 apply(simp only: foo.eq_iff) |
|
97 apply(simp only: eqvts) |
|
98 apply simp |
|
99 by (metis assms(2) atom_eqvt fresh_perm) |
|
100 |
90 lemma strong_exhaust1: |
101 lemma strong_exhaust1: |
91 fixes c::"'a::fs" |
102 fixes c::"'a::fs" |
92 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
103 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
93 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
104 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
94 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
105 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
95 and "\<And>assn1 trm1 assn2 trm2. |
106 and "\<And>assn1 trm1 assn2 trm2. |
96 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
107 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
97 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
108 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
98 shows "P" |
109 shows "P" |
99 apply(rule_tac y="y" in foo.exhaust(1)) |
110 apply(rule_tac y="y" in foo.exhaust(1)) |
100 apply(rule assms(1)) |
111 apply(rule assms(1)) |
101 apply(assumption) |
112 apply(assumption) |
102 apply(rule assms(2)) |
113 apply(rule assms(2)) |
140 apply(rule at_set_avoiding2) |
151 apply(rule at_set_avoiding2) |
141 apply(simp add: finite_supp) |
152 apply(simp add: finite_supp) |
142 apply(simp add: finite_supp) |
153 apply(simp add: finite_supp) |
143 apply(simp add: finite_supp) |
154 apply(simp add: finite_supp) |
144 apply(simp add: Abs_fresh_star) |
155 apply(simp add: Abs_fresh_star) |
145 thm foo.eq_iff |
156 apply(case_tac "name1 = name2") |
146 apply(subgoal_tac |
157 apply(subgoal_tac |
147 "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> supp ([[atom name1]]lst. trm1) \<sharp>* q") |
158 "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* c \<and> (supp (([[atom name1, atom name2]]lst. trm1), ([[atom name2]]lst. trm2))) \<sharp>* q") |
148 apply(subgoal_tac |
|
149 "\<exists>q. (q \<bullet> {atom name2}) \<sharp>* c \<and> supp ([[atom name2]]lst. trm2) \<sharp>* q") |
|
150 apply(erule exE)+ |
159 apply(erule exE)+ |
151 apply(erule conjE)+ |
160 apply(erule conjE)+ |
|
161 apply(perm_simp) |
152 apply(rule assms(5)) |
162 apply(rule assms(5)) |
153 apply(perm_simp) |
163 |
154 apply(simp (no_asm) add: fresh_star_insert) |
164 apply (simp add: fresh_star_def eqvts) |
155 apply(rule conjI) |
165 apply (simp only: supp_Pair) |
156 apply(simp add: fresh_star_def) |
166 apply (simp only: fresh_star_Un_elim) |
157 apply(rotate_tac 3) |
167 apply (subst Let2_rename) |
158 apply(simp add: fresh_star_def) |
168 apply assumption |
159 apply(simp) |
169 apply assumption |
160 apply(simp add: foo.eq_iff) |
170 apply (rule refl) |
161 apply(drule supp_perm_eq[symmetric])+ |
171 apply(rule at_set_avoiding2) |
162 apply(simp add: atom_eqvt) |
172 apply(simp add: finite_supp) |
163 apply(rule conjI) |
173 apply(simp add: finite_supp) |
164 oops |
174 apply(simp add: finite_supp) |
|
175 apply clarify |
|
176 apply (simp add: fresh_star_def) |
|
177 apply (simp add: fresh_def supp_Pair supp_Abs) |
|
178 apply(subgoal_tac |
|
179 "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> (supp ((([[atom name1, atom name2]]lst. trm1)), (atom name2))) \<sharp>* q") |
|
180 prefer 2 |
|
181 apply(rule at_set_avoiding2) |
|
182 apply(simp add: finite_supp) |
|
183 apply(simp add: finite_supp) |
|
184 apply(simp add: finite_supp) |
|
185 apply (simp add: fresh_star_def) |
|
186 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
|
187 apply(erule exE)+ |
|
188 apply(erule conjE)+ |
|
189 apply(perm_simp) |
|
190 apply(rule assms(5)) |
|
191 apply assumption |
|
192 apply clarify |
|
193 apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2) |
|
194 apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs) |
|
195 apply (simp add: fresh_star_def supp_atom) |
|
196 done |
165 |
197 |
166 |
198 |
167 end |
199 end |
168 |
200 |
169 |
201 |