146 assumes "y = Let1 assn trm" |
146 assumes "y = Let1 assn trm" |
147 shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)" |
147 shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)" |
148 using assms |
148 using assms |
149 apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric]) |
149 apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric]) |
150 apply(simp del: permute_Abs) |
150 apply(simp del: permute_Abs) |
151 apply(rule at_set_avoiding3) |
151 sorry |
152 apply(simp_all only: finite_supp Abs_fresh_star finite_set) |
152 |
153 done |
153 lemma strong_exhaust1: |
|
154 fixes c::"'a::fs" |
|
155 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
|
156 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
157 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
|
158 and "\<exists>assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" |
|
159 and "\<exists>assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" |
|
160 and "\<exists>assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" |
|
161 and "\<exists>assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" |
|
162 shows "P" |
|
163 apply(rule_tac y="y" in foo.exhaust(1)) |
|
164 apply(rule assms(1)) |
|
165 apply(rule exI) |
|
166 apply(assumption) |
|
167 apply(rule assms(2)) |
|
168 apply(rule exI)+ |
|
169 apply(assumption) |
|
170 apply(rule assms(3)) |
|
171 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
172 apply(erule exE) |
|
173 apply(erule conjE) |
|
174 apply(rule assms(3)) |
|
175 apply(perm_simp) |
|
176 apply(assumption) |
|
177 apply(simp) |
|
178 apply(drule supp_perm_eq[symmetric]) |
|
179 apply(perm_simp) |
|
180 apply(simp) |
|
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: foo.fresh fresh_star_def) |
|
186 apply(drule Let1_rename_a) |
|
187 apply(erule exE) |
|
188 apply(erule conjE) |
|
189 apply(rule assms(4)) |
|
190 apply(simp only: set_eqvt tt1) |
|
191 apply(assumption) |
|
192 (* |
|
193 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
|
194 apply(erule exE) |
|
195 apply(erule conjE) |
|
196 *) |
|
197 thm assms(5) |
|
198 apply(rule assms(5)) |
|
199 prefer 2 |
|
200 apply(clarify) |
|
201 unfolding foo.eq_iff |
|
202 apply |
154 |
203 |
155 lemma strong_exhaust1: |
204 lemma strong_exhaust1: |
156 fixes c::"'a::fs" |
205 fixes c::"'a::fs" |
157 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
206 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
158 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
207 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
186 apply(erule exE) |
235 apply(erule exE) |
187 apply(erule conjE) |
236 apply(erule conjE) |
188 apply(rule assms(4)) |
237 apply(rule assms(4)) |
189 apply(simp only: set_eqvt tt1) |
238 apply(simp only: set_eqvt tt1) |
190 apply(assumption) |
239 apply(assumption) |
|
240 (* |
191 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
241 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
192 apply(erule exE) |
242 apply(erule exE) |
193 apply(erule conjE) |
243 apply(erule conjE) |
|
244 *) |
|
245 thm assms(5) |
194 apply(rule assms(5)) |
246 apply(rule assms(5)) |
|
247 prefer 2 |
|
248 apply(clarify) |
|
249 unfolding foo.eq_iff |
|
250 apply(rule conjI) |
|
251 prefer 2 |
|
252 apply(rule uu2) |
|
253 apply(simp only: tt2[symmetric]) |
|
254 prefer 2 |
|
255 apply(simp only: tt2[symmetric]) |
|
256 |
|
257 apply(simp_all only:)[2] |
195 apply(simp add: set_eqvt) |
258 apply(simp add: set_eqvt) |
196 apply(simp add: tt2) |
259 apply(simp add: tt2) |
197 apply(simp add: foo.eq_iff) |
260 apply(simp add: foo.eq_iff) |
198 apply(drule supp_perm_eq[symmetric]) |
261 apply(drule supp_perm_eq[symmetric]) |
199 apply(simp) |
262 apply(simp) |