equal
deleted
inserted
replaced
125 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
125 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
126 apply(simp add: atom_eqvt insert_eqvt) |
126 apply(simp add: atom_eqvt insert_eqvt) |
127 done |
127 done |
128 |
128 |
129 |
129 |
|
130 lemma Let1_rename: |
|
131 assumes "supp ([bn1 assn]lst. trm) \<sharp>* p" |
|
132 shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \<bullet> trm)" |
|
133 using assms |
|
134 apply - |
|
135 apply(drule supp_perm_eq[symmetric]) |
|
136 apply(simp only: permute_Abs) |
|
137 apply(simp only: tt1) |
|
138 apply(simp only: foo.eq_iff) |
|
139 apply(rule conjI) |
|
140 apply(rule refl) |
|
141 apply(rule uu1) |
|
142 done |
|
143 |
|
144 lemma Let1_rename_a: |
|
145 fixes c::"'a::fs" |
|
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)" |
|
148 using assms |
|
149 apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric]) |
|
150 apply(simp del: permute_Abs) |
|
151 apply(rule at_set_avoiding3) |
|
152 apply(simp_all only: finite_supp Abs_fresh_star finite_set) |
|
153 done |
130 |
154 |
131 lemma strong_exhaust1: |
155 lemma strong_exhaust1: |
132 fixes c::"'a::fs" |
156 fixes c::"'a::fs" |
133 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
157 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
134 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
158 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
156 apply(rule at_set_avoiding2) |
180 apply(rule at_set_avoiding2) |
157 apply(simp add: finite_supp) |
181 apply(simp add: finite_supp) |
158 apply(simp add: finite_supp) |
182 apply(simp add: finite_supp) |
159 apply(simp add: finite_supp) |
183 apply(simp add: finite_supp) |
160 apply(simp add: foo.fresh fresh_star_def) |
184 apply(simp add: foo.fresh fresh_star_def) |
161 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q") |
185 apply(drule Let1_rename_a) |
162 apply(erule exE) |
186 apply(erule exE) |
163 apply(erule conjE) |
187 apply(erule conjE) |
164 apply(rule assms(4)) |
188 apply(rule assms(4)) |
165 apply(perm_simp add: tt1) |
189 apply(simp only: set_eqvt tt1) |
166 apply(assumption) |
190 apply(assumption) |
167 apply(drule supp_perm_eq[symmetric]) |
|
168 apply(simp add: foo.eq_iff) |
|
169 apply(simp add: tt1 uu1) |
|
170 apply(rule at_set_avoiding2) |
|
171 apply(simp add: finite_supp) |
|
172 apply(simp add: finite_supp) |
|
173 apply(simp add: finite_supp) |
|
174 apply(simp add: Abs_fresh_star) |
|
175 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
191 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q") |
176 apply(erule exE) |
192 apply(erule exE) |
177 apply(erule conjE) |
193 apply(erule conjE) |
178 apply(rule assms(5)) |
194 apply(rule assms(5)) |
179 apply(simp add: set_eqvt) |
195 apply(simp add: set_eqvt) |