2226 then obtain a :: 'a where "atom a \<notin> X" |
2226 then obtain a :: 'a where "atom a \<notin> X" |
2227 by auto |
2227 by auto |
2228 thus ?thesis .. |
2228 thus ?thesis .. |
2229 qed |
2229 qed |
2230 |
2230 |
|
2231 lemma obtain_fresh': |
|
2232 assumes fin: "finite (supp x)" |
|
2233 obtains a::"'a::at_base" where "atom a \<sharp> x" |
|
2234 using obtain_at_base[where X="supp x"] |
|
2235 by (auto simp add: fresh_def fin) |
|
2236 |
|
2237 lemma obtain_fresh: |
|
2238 fixes x::"'b::fs" |
|
2239 obtains a::"'a::at_base" where "atom a \<sharp> x" |
|
2240 by (rule obtain_fresh') (auto simp add: finite_supp) |
|
2241 |
2231 lemma supp_finite_set_at_base: |
2242 lemma supp_finite_set_at_base: |
2232 assumes a: "finite S" |
2243 assumes a: "finite S" |
2233 shows "supp S = atom ` S" |
2244 shows "supp S = atom ` S" |
2234 apply(simp add: supp_of_finite_sets[OF a]) |
2245 apply(simp add: supp_of_finite_sets[OF a]) |
2235 apply(simp add: supp_at_base) |
2246 apply(simp add: supp_at_base) |
2537 fixes P :: "'a::at \<Rightarrow> 'b::pure" |
2548 fixes P :: "'a::at \<Rightarrow> 'b::pure" |
2538 fixes f :: "'b \<Rightarrow> 'c::pure" |
2549 fixes f :: "'b \<Rightarrow> 'c::pure" |
2539 assumes P: "finite (supp P)" |
2550 assumes P: "finite (supp P)" |
2540 shows "(FRESH x. f (P x)) = f (FRESH x. P x)" |
2551 shows "(FRESH x. f (P x)) = f (FRESH x. P x)" |
2541 proof - |
2552 proof - |
2542 obtain a::'a where "atom a \<notin> supp P" |
2553 obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh') |
2543 using P by (rule obtain_at_base) |
|
2544 hence "atom a \<sharp> P" |
|
2545 by (simp add: fresh_def) |
|
2546 show "(FRESH x. f (P x)) = f (FRESH x. P x)" |
2554 show "(FRESH x. f (P x)) = f (FRESH x. P x)" |
2547 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
2555 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
2548 apply (cut_tac `atom a \<sharp> P`) |
2556 apply (cut_tac `atom a \<sharp> P`) |
2549 apply (simp add: fresh_conv_MOST) |
2557 apply (simp add: fresh_conv_MOST) |
2550 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
2558 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
2560 fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure" |
2568 fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure" |
2561 assumes P: "finite (supp P)" |
2569 assumes P: "finite (supp P)" |
2562 and Q: "finite (supp Q)" |
2570 and Q: "finite (supp Q)" |
2563 shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)" |
2571 shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)" |
2564 proof - |
2572 proof - |
2565 from assms have "finite (supp P \<union> supp Q)" by simp |
2573 from assms have "finite (supp (P, Q))" by (simp add: supp_Pair) |
2566 then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)" |
2574 then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh') |
2567 by (rule obtain_at_base) |
2575 then have "atom a \<sharp> P" and "atom a \<sharp> Q" by (simp_all add: fresh_Pair) |
2568 hence "atom a \<sharp> P" and "atom a \<sharp> Q" |
|
2569 by (simp_all add: fresh_def) |
|
2570 show ?thesis |
2576 show ?thesis |
2571 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
2577 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
2572 apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`) |
2578 apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`) |
2573 apply (simp add: fresh_conv_MOST) |
2579 apply (simp add: fresh_conv_MOST) |
2574 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
2580 apply (elim MOST_rev_mp, rule MOST_I, clarify) |