equal
deleted
inserted
replaced
191 thus "h a = h b" by simp |
191 thus "h a = h b" by simp |
192 next |
192 next |
193 assume "a \<noteq> b" |
193 assume "a \<noteq> b" |
194 hence "atom a \<sharp> b" by (simp add: fresh_at_base) |
194 hence "atom a \<sharp> b" by (simp add: fresh_at_base) |
195 with a3 have "atom a \<sharp> h b" |
195 with a3 have "atom a \<sharp> h b" |
196 by (rule fresh_fun_app) |
196 by (rule fresh_fun_app) |
197 with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)" |
197 with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)" |
198 by (rule swap_fresh_fresh) |
198 by (rule swap_fresh_fresh) |
199 from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h" |
199 from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h" |
200 by (rule swap_fresh_fresh) |
200 by (rule swap_fresh_fresh) |
201 from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp |
201 from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp |
390 then have "P p" using zero by simp |
390 then have "P p" using zero by simp |
391 } |
391 } |
392 moreover |
392 moreover |
393 { assume "supp p \<noteq> {}" |
393 { assume "supp p \<noteq> {}" |
394 then obtain a where a0: "a \<in> supp p" by blast |
394 then obtain a where a0: "a \<in> supp p" by blast |
395 then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as |
395 then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" |
396 by (auto simp add: supp_atom supp_perm swap_atom) |
396 using as by (auto simp add: supp_atom supp_perm swap_atom) |
397 let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p" |
397 let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p" |
398 have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom) |
398 have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom) |
399 moreover |
399 moreover |
400 have "a \<notin> supp ?q" by (simp add: supp_perm) |
400 have "a \<notin> supp ?q" by (simp add: supp_perm) |
401 then have "supp ?q \<noteq> supp p" using a0 by auto |
401 then have "supp ?q \<noteq> supp p" using a0 by auto |
501 fixes S::"('a::fs set)" |
501 fixes S::"('a::fs set)" |
502 assumes fin: "finite S" |
502 assumes fin: "finite S" |
503 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
503 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
504 proof - |
504 proof - |
505 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
505 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
506 apply(rule supp_finite_atom_set[symmetric]) |
506 by (rule supp_finite_atom_set[symmetric]) |
507 apply(rule Union_of_fin_supp_sets[OF fin]) |
507 (rule Union_of_fin_supp_sets[OF fin]) |
508 done |
|
509 also have "\<dots> \<subseteq> supp S" |
508 also have "\<dots> \<subseteq> supp S" |
510 apply(rule supp_subset_fresh) |
509 by (rule supp_subset_fresh) |
511 apply(simp add: Union_fresh) |
510 (simp add: Union_fresh) |
512 done |
511 finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" . |
513 finally show ?thesis . |
|
514 qed |
512 qed |
515 |
513 |
516 lemma supp_of_fin_sets: |
514 lemma supp_of_fin_sets: |
517 fixes S::"('a::fs set)" |
515 fixes S::"('a::fs set)" |
518 assumes fin: "finite S" |
516 assumes fin: "finite S" |