47 thm foo.supports |
48 thm foo.supports |
48 thm foo.fsupp |
49 thm foo.fsupp |
49 thm foo.supp |
50 thm foo.supp |
50 thm foo.fresh |
51 thm foo.fresh |
51 |
52 |
52 (* |
53 lemma at_set_avoiding5: |
53 lemma ex_prop: |
54 assumes "finite xs" |
54 shows "\<exists>n::nat. Suc n = n" |
55 and "finite (supp c)" |
55 sorry |
56 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs" |
56 |
57 using assms |
57 lemma test: |
58 apply(erule_tac c="c" in at_set_avoiding) |
58 shows "True" |
59 apply(auto) |
|
60 done |
|
61 |
|
62 |
|
63 lemma Abs_rename_lst3: |
|
64 fixes x::"'a::fs" |
|
65 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
|
66 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" |
|
67 proof - |
|
68 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
|
69 by (simp add: fresh_star_Pair fresh_star_set) |
|
70 with list_renaming_perm |
|
71 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
|
72 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
|
73 apply(rule perm_supp_eq[symmetric]) |
|
74 using a ** |
|
75 unfolding fresh_star_Pair |
|
76 unfolding Abs_fresh_star_iff |
|
77 unfolding fresh_star_def |
|
78 by auto |
|
79 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
|
80 also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp |
|
81 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" . |
|
82 then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" |
|
83 using * ** by metis |
|
84 qed |
|
85 |
|
86 |
|
87 lemma |
|
88 fixes c::"'a::fs" |
|
89 assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
90 shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
59 apply - |
91 apply - |
60 ML_prf {* |
92 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
61 val (x, ctxt') = Obtain.result (K ( |
93 supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
62 EVERY [print_tac "test", |
94 defer |
63 etac exE 1, |
95 apply(rule at_set_avoiding5) |
64 print_tac "end"])) |
96 apply(simp add: foo.bn_finite) |
65 @{thms ex_prop} @{context}; |
97 apply(simp add: supp_Pair finite_supp) |
66 ProofContext.verbose := true; |
98 apply(erule exE) |
67 ProofContext.pretty_context ctxt' |
99 apply(perm_simp add: foo.permute_bn) |
68 |> Pretty.block |
100 apply(simp add: fresh_star_Pair) |
69 |> Pretty.writeln |
101 apply(erule conjE)+ |
70 *} |
102 thm Abs_rename_lst |
71 *) |
103 apply(insert Abs_rename_lst)[1] |
72 |
104 apply(drule_tac x="p" in meta_spec) |
73 |
105 apply(drule_tac x="bn assg1" in meta_spec) |
|
106 apply(drule_tac x="trm1" in meta_spec) |
|
107 apply(insert Abs_rename_lst)[1] |
|
108 apply(drule_tac x="p" in meta_spec) |
|
109 apply(drule_tac x="bn assg2" in meta_spec) |
|
110 apply(drule_tac x="trm2" in meta_spec) |
|
111 apply(drule meta_mp) |
|
112 apply(perm_simp add: foo.permute_bn) |
|
113 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
114 apply(drule meta_mp) |
|
115 apply(perm_simp add: foo.permute_bn) |
|
116 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
117 apply(erule exE)+ |
|
118 apply(rule a) |
|
119 apply(assumption) |
|
120 apply(simp only: foo.eq_iff) |
|
121 apply(perm_simp add: foo.permute_bn) |
|
122 apply(rule conjI) |
|
123 apply(rule refl) |
|
124 apply(rule conjI) |
|
125 apply(rule foo.perm_bn_alpha) |
|
126 apply(rule conjI) |
|
127 apply(perm_simp add: foo.permute_bn) |
|
128 apply(rule refl) |
|
129 apply(rule foo.perm_bn_alpha) |
|
130 done |
|
131 |
|
132 lemma |
|
133 fixes c::"'a::fs" |
|
134 assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
135 shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
136 apply - |
|
137 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
138 supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
139 defer |
|
140 apply(rule at_set_avoiding5) |
|
141 apply(simp add: foo.bn_finite) |
|
142 apply(simp add: supp_Pair finite_supp) |
|
143 apply(erule exE) |
|
144 apply(perm_simp add: foo.permute_bn) |
|
145 apply(simp add: fresh_star_Pair) |
|
146 apply(erule conjE)+ |
|
147 apply(insert Abs_rename_lst3)[1] |
|
148 apply(drule_tac x="p" in meta_spec) |
|
149 apply(drule_tac x="bn assg1" in meta_spec) |
|
150 apply(drule_tac x="trm1" in meta_spec) |
|
151 apply(insert Abs_rename_lst3)[1] |
|
152 apply(drule_tac x="p" in meta_spec) |
|
153 apply(drule_tac x="bn assg2" in meta_spec) |
|
154 apply(drule_tac x="trm2" in meta_spec) |
|
155 apply(drule meta_mp) |
|
156 apply(perm_simp add: foo.permute_bn) |
|
157 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
158 apply(drule meta_mp) |
|
159 apply(perm_simp add: foo.permute_bn) |
|
160 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
161 apply(erule exE)+ |
|
162 apply(erule conjE)+ |
|
163 apply(simp add: foo.permute_bn) |
|
164 apply(rule a) |
|
165 apply(assumption) |
|
166 apply(clarify) |
|
167 apply(simp (no_asm) only: foo.eq_iff) |
|
168 apply(rule conjI) |
|
169 apply(assumption) |
|
170 apply(rule conjI) |
|
171 apply(rule foo.perm_bn_alpha) |
|
172 apply(rule conjI) |
|
173 apply(assumption) |
|
174 apply(rule foo.perm_bn_alpha) |
|
175 done |
|
176 |
|
177 |
|
178 lemma |
|
179 fixes c::"'a::fs" |
|
180 assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
181 shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
182 apply - |
|
183 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
184 supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
185 defer |
|
186 apply(rule at_set_avoiding5) |
|
187 apply(simp add: foo.bn_finite) |
|
188 apply(simp add: supp_Pair finite_supp) |
|
189 apply(erule exE) |
|
190 apply(simp add: fresh_star_Pair) |
|
191 apply(erule conjE)+ |
|
192 apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt) |
|
193 apply(rule a) |
|
194 apply(assumption) |
|
195 apply(clarify) |
|
196 apply(simp (no_asm) only: foo.eq_iff) |
|
197 apply(rule conjI) |
|
198 apply(rule trans) |
|
199 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
200 apply(rule fresh_star_supp_conv) |
|
201 apply(simp (no_asm_use) add: fresh_star_def) |
|
202 apply(simp (no_asm_use) add: Abs_fresh_iff)[1] |
|
203 apply(rule ballI) |
|
204 apply(auto simp add: fresh_Pair)[1] |
|
205 apply(simp (no_asm_use) only: permute_Abs) |
|
206 apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt) |
|
207 apply(simp) |
|
208 apply(rule at_set_avoiding5) |
|
209 apply(simp add: multi_recs.bn_finite) |
|
210 apply(simp add: supp_Pair finite_supp) |
|
211 apply(rule finite_sets_supp) |
|
212 apply(simp add: multi_recs.bn_finite) |
|
213 done |
74 |
214 |
75 |
215 |
76 |
216 |
77 lemma test6: |
217 lemma test6: |
78 fixes c::"'a::fs" |
218 fixes c::"'a::fs" |
110 apply(simp) |
250 apply(simp) |
111 apply(simp add: finite_supp) |
251 apply(simp add: finite_supp) |
112 (* let1 case *) |
252 (* let1 case *) |
113 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
253 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
114 apply(erule exE) |
254 apply(erule exE) |
115 apply(rule assms(4)) |
255 apply(perm_simp add: foo.permute_bn) |
116 apply(perm_simp add: foo.permute_bn) |
256 apply(simp add: fresh_star_Pair) |
117 apply(simp add: fresh_star_Pair) |
257 apply(erule conjE)+ |
118 apply(erule conjE)+ |
|
119 apply(assumption) |
|
120 apply(simp only:) |
|
121 apply(simp only: foo.eq_iff) |
|
122 (* *) |
|
123 apply(insert Abs_rename_lst)[1] |
258 apply(insert Abs_rename_lst)[1] |
124 apply(drule_tac x="p" in meta_spec) |
259 apply(drule_tac x="p" in meta_spec) |
125 apply(drule_tac x="bn assg1" in meta_spec) |
260 apply(drule_tac x="bn assg1" in meta_spec) |
126 apply(drule_tac x="trm1" in meta_spec) |
261 apply(drule_tac x="trm1" in meta_spec) |
127 apply(insert Abs_rename_lst)[1] |
262 apply(insert Abs_rename_lst)[1] |
128 apply(drule_tac x="p" in meta_spec) |
263 apply(drule_tac x="p" in meta_spec) |
129 apply(drule_tac x="bn assg2" in meta_spec) |
264 apply(drule_tac x="bn assg2" in meta_spec) |
130 apply(drule_tac x="trm2" in meta_spec) |
265 apply(drule_tac x="trm2" in meta_spec) |
131 apply(drule meta_mp) |
266 apply(drule meta_mp) |
132 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
267 apply(perm_simp add: foo.permute_bn) |
133 apply(drule meta_mp) |
268 apply(simp add: fresh_star_Pair fresh_star_Un) |
134 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
269 apply(drule meta_mp) |
135 apply(erule exE)+ |
270 apply(perm_simp add: foo.permute_bn) |
136 apply(perm_simp add: foo.permute_bn) |
271 apply(simp add: fresh_star_Pair fresh_star_Un) |
137 apply(simp add: fresh_star_Pair) |
272 apply(erule exE)+ |
138 apply(erule conjE)+ |
|
139 apply(rule assms(4)) |
273 apply(rule assms(4)) |
140 apply(assumption) |
274 apply(assumption) |
141 apply(simp add: foo.eq_iff refl) |
275 apply(simp add: foo.eq_iff refl) |
142 apply(rule conjI) |
276 apply(rule conjI) |
|
277 apply(perm_simp add: foo.permute_bn) |
143 apply(rule refl) |
278 apply(rule refl) |
144 apply(rule conjI) |
279 apply(rule conjI) |
145 apply(rule foo.perm_bn_alpha) |
280 apply(rule foo.perm_bn_alpha) |
146 apply(rule conjI) |
281 apply(rule conjI) |
|
282 apply(perm_simp add: foo.permute_bn) |
147 apply(rule refl) |
283 apply(rule refl) |
148 apply(rule foo.perm_bn_alpha) |
284 apply(rule foo.perm_bn_alpha) |
149 apply(rule at_set_avoiding1) |
285 apply(rule at_set_avoiding1) |
150 apply(simp) |
286 apply(simp) |
151 apply(simp add: finite_supp) |
287 apply(simp add: finite_supp) |