--- a/Nominal-General/Nominal2_Base.thy Mon Apr 19 11:32:33 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy Mon Apr 19 11:38:43 2010 +0200
@@ -212,8 +212,8 @@
lemma swap_cancel:
"(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
-by (rule Rep_perm_ext)
- (simp add: Rep_perm_simps expand_fun_eq)
+ by (rule Rep_perm_ext)
+ (simp add: Rep_perm_simps expand_fun_eq)
lemma swap_self [simp]:
"(a \<rightleftharpoons> a) = 0"
@@ -302,7 +302,7 @@
begin
definition
- "p \<bullet> a = Rep_perm p a"
+ "p \<bullet> a = (Rep_perm p) a"
instance
apply(default)
@@ -351,8 +351,10 @@
end
-lemma permute_self: "p \<bullet> p = p"
-unfolding permute_perm_def by (simp add: diff_minus add_assoc)
+lemma permute_self:
+ shows "p \<bullet> p = p"
+ unfolding permute_perm_def
+ by (simp add: diff_minus add_assoc)
lemma permute_eqvt:
shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"
@@ -392,7 +394,7 @@
lemma permute_fun_app_eq:
shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
-unfolding permute_fun_def by simp
+ unfolding permute_fun_def by simp
subsection {* Permutations for booleans *}
@@ -429,29 +431,33 @@
fixes x::"'a::pt"
and p::"perm"
shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
- apply(auto simp add: permute_fun_def permute_bool_def mem_def)
+ unfolding permute_fun_def
+ unfolding permute_bool_def
+ apply(auto simp add: mem_def)
apply(rule_tac x="- p \<bullet> x" in exI)
apply(simp)
done
lemma permute_set_eq_image:
shows "p \<bullet> X = permute p ` X"
-unfolding permute_set_eq by auto
+ unfolding permute_set_eq by auto
lemma permute_set_eq_vimage:
shows "p \<bullet> X = permute (- p) -` X"
-unfolding permute_fun_def permute_bool_def
-unfolding vimage_def Collect_def mem_def ..
+ unfolding permute_fun_def permute_bool_def
+ unfolding vimage_def Collect_def mem_def ..
lemma swap_set_not_in:
assumes a: "a \<notin> S" "b \<notin> S"
shows "(a \<rightleftharpoons> b) \<bullet> S = S"
- using a by (auto simp add: permute_set_eq swap_atom)
+ unfolding permute_set_eq
+ using a by (auto simp add: swap_atom)
lemma swap_set_in:
assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
- using a by (auto simp add: permute_set_eq swap_atom)
+ unfolding permute_set_eq
+ using a by (auto simp add: swap_atom)
subsection {* Permutations for units *}
@@ -461,8 +467,8 @@
definition "p \<bullet> (u::unit) = u"
-instance proof
-qed (simp_all add: permute_unit_def)
+instance
+by (default) (simp_all add: permute_unit_def)
end
@@ -493,8 +499,8 @@
"p \<bullet> (Inl x) = Inl (p \<bullet> x)"
| "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
-instance proof
-qed (case_tac [!] x, simp_all)
+instance
+by (default) (case_tac [!] x, simp_all)
end
@@ -509,8 +515,8 @@
"p \<bullet> [] = []"
| "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
-instance proof
-qed (induct_tac [!] x, simp_all)
+instance
+by (default) (induct_tac [!] x, simp_all)
end
@@ -525,8 +531,8 @@
"p \<bullet> None = None"
| "p \<bullet> (Some x) = Some (p \<bullet> x)"
-instance proof
-qed (induct_tac [!] x, simp_all)
+instance
+by (default) (induct_tac [!] x, simp_all)
end
@@ -537,8 +543,8 @@
definition "p \<bullet> (c::char) = c"
-instance proof
-qed (simp_all add: permute_char_def)
+instance
+by (default) (simp_all add: permute_char_def)
end
@@ -547,8 +553,8 @@
definition "p \<bullet> (n::nat) = n"
-instance proof
-qed (simp_all add: permute_nat_def)
+instance
+by (default) (simp_all add: permute_nat_def)
end
@@ -557,8 +563,8 @@
definition "p \<bullet> (i::int) = i"
-instance proof
-qed (simp_all add: permute_int_def)
+instance
+by (default) (simp_all add: permute_int_def)
end
@@ -679,26 +685,28 @@
have "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}"
unfolding fresh_def supp_def by simp
also have "\<dots> \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> p \<bullet> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}"
- using bij_permute by (rule finite_Collect_bij [symmetric])
+ using bij_permute by (rule finite_Collect_bij[symmetric])
also have "\<dots> \<longleftrightarrow> finite {b. p \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> p \<bullet> x}"
by (simp only: permute_eqvt [of p] swap_eqvt)
also have "\<dots> \<longleftrightarrow> finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"
by (simp only: permute_eq_iff)
also have "\<dots> \<longleftrightarrow> a \<sharp> x"
unfolding fresh_def supp_def by simp
- finally show ?thesis .
+ finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
qed
lemma fresh_eqvt:
shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
- by (simp add: permute_bool_def fresh_permute_iff)
+ unfolding permute_bool_def
+ by (simp add: fresh_permute_iff)
lemma supp_eqvt:
fixes p :: "perm"
and x :: "'a::pt"
shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
unfolding supp_conv_fresh
- unfolding permute_fun_def Collect_def
+ unfolding Collect_def
+ unfolding permute_fun_def
by (simp add: Not_eqvt fresh_eqvt)
subsection {* supports *}
@@ -715,10 +723,10 @@
and a2: "finite S"
shows "(supp x) \<subseteq> S"
proof (rule ccontr)
- assume "\<not>(supp x \<subseteq> S)"
+ assume "\<not> (supp x \<subseteq> S)"
then obtain a where b1: "a \<in> supp x" and b2: "a \<notin> S" by auto
- from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" by (unfold supports_def) (auto)
- hence "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto
+ from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto
+ then have "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto
with a2 have "finite {b. (a \<rightleftharpoons> b)\<bullet>x \<noteq> x}" by (simp add: finite_subset)
then have "a \<notin> (supp x)" unfolding supp_def by simp
with b1 show False by simp
@@ -738,11 +746,12 @@
lemma supp_supports:
fixes x :: "'a::pt"
shows "(supp x) supports x"
-proof (unfold supports_def, intro strip)
+unfolding supports_def
+proof (intro strip)
fix a b
assume "a \<notin> (supp x) \<and> b \<notin> (supp x)"
then have "a \<sharp> x" and "b \<sharp> x" by (simp_all add: fresh_def)
- then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (rule swap_fresh_fresh)
+ then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
qed
lemma supp_is_least_supports:
@@ -837,7 +846,8 @@
lemma supports_perm:
shows "{a. p \<bullet> a \<noteq> a} supports p"
unfolding supports_def
- by (simp add: perm_swap_eq swap_eqvt)
+ unfolding perm_swap_eq
+ by (simp add: swap_eqvt)
lemma finite_perm_lemma:
shows "finite {a::atom. p \<bullet> a \<noteq> a}"
@@ -855,7 +865,8 @@
lemma fresh_perm:
shows "a \<sharp> p \<longleftrightarrow> p \<bullet> a = a"
-unfolding fresh_def by (simp add: supp_perm)
+ unfolding fresh_def
+ by (simp add: supp_perm)
lemma supp_swap:
shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})"
@@ -886,8 +897,9 @@
fixes p::perm
shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
unfolding fresh_def
- apply(auto simp add: supp_perm)
- apply(metis permute_minus_cancel)+
+ unfolding supp_perm
+ apply(simp)
+ apply(metis permute_minus_cancel)
done
lemma supp_minus_perm:
@@ -901,7 +913,7 @@
lemma plus_perm_eq:
fixes p q::"perm"
- assumes asm: "supp p \<inter> supp q = {}"
+ assumes asm: "supp p \<inter> supp q = {}"
shows "p + q = q + p"
unfolding expand_perm_eq
proof
@@ -1023,8 +1035,28 @@
section {* Support and freshness for applications *}
+lemma fresh_conv_MOST:
+ shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
+ unfolding fresh_def supp_def
+ unfolding MOST_iff_cofinite by simp
+
+lemma fresh_fun_app:
+ assumes "a \<sharp> f" and "a \<sharp> x"
+ shows "a \<sharp> f x"
+ using assms
+ unfolding fresh_conv_MOST
+ unfolding permute_fun_app_eq
+ by (elim MOST_rev_mp, simp)
+
lemma supp_fun_app:
shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
+ using fresh_fun_app
+ unfolding fresh_def
+ by auto
+
+(* alternative proof *)
+lemma
+ shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
proof (rule subsetCI)
fix a::"atom"
assume a: "a \<in> supp (f x)"
@@ -1042,25 +1074,19 @@
with a show "False" by simp
qed
-lemma fresh_fun_app:
- shows "a \<sharp> (f, x) \<Longrightarrow> a \<sharp> f x"
-unfolding fresh_def
-using supp_fun_app
-by (auto simp add: supp_Pair)
-
lemma fresh_fun_eqvt_app:
assumes a: "\<forall>p. p \<bullet> f = f"
shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
proof -
- from a have b: "supp f = {}"
+ from a have "supp f = {}"
unfolding supp_def by simp
- show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
+ then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
unfolding fresh_def
- using supp_fun_app b
+ using supp_fun_app
by auto
qed
-(* nominal infrastructure *)
+section {* library functions for the nominal infrastructure *}
use "nominal_library.ML"
end
--- a/Nominal-General/Nominal2_Supp.thy Mon Apr 19 11:32:33 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy Mon Apr 19 11:38:43 2010 +0200
@@ -141,20 +141,38 @@
using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
unfolding fresh_star_def fresh_def by blast
+lemma at_set_avoiding2:
+ assumes "finite xs"
+ and "finite (supp c)" "finite (supp x)"
+ and "xs \<sharp>* x"
+ shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+apply(auto simp add: fresh_star_def fresh_def)
+done
+
+lemma at_set_avoiding2_atom:
+ assumes "finite (supp c)" "finite (supp x)"
+ and b: "xa \<sharp> x"
+ shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
+proof -
+ have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+ obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+ using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
+ have c: "(p \<bullet> xa) \<sharp> c" using p1
+ unfolding fresh_star_def Ball_def
+ by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
+ hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+ then show ?thesis by blast
+qed
section {* The freshness lemma according to Andrew Pitts *}
-lemma fresh_conv_MOST:
- shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
- unfolding fresh_def supp_def MOST_iff_cofinite by simp
-
-lemma fresh_apply:
- assumes "a \<sharp> f" and "a \<sharp> x"
- shows "a \<sharp> f x"
- using assms unfolding fresh_conv_MOST
- unfolding permute_fun_app_eq [where f=f]
- by (elim MOST_rev_mp, simp)
-
lemma freshness_lemma:
fixes h :: "'a::at \<Rightarrow> 'b::pt"
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
@@ -173,7 +191,8 @@
next
assume "a \<noteq> b"
hence "atom a \<sharp> b" by (simp add: fresh_at_base)
- with a3 have "atom a \<sharp> h b" by (rule fresh_apply)
+ with a3 have "atom a \<sharp> h b"
+ by (rule fresh_fun_app)
with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
by (rule swap_fresh_fresh)
from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
@@ -358,7 +377,7 @@
using not_fresh_nat_of [unfolded fresh_def] by auto
-section {* Support for sets of atoms *}
+section {* Support for finite sets of atoms *}
lemma supp_finite_atom_set:
fixes S::"atom set"
@@ -447,36 +466,4 @@
qed
qed
-section {* at_set_avoiding2 *}
-
-lemma at_set_avoiding2:
- assumes "finite xs"
- and "finite (supp c)" "finite (supp x)"
- and "xs \<sharp>* x"
- shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
-using assms
-apply(erule_tac c="(c, x)" in at_set_avoiding)
-apply(simp add: supp_Pair)
-apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
-apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
-apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
-apply(auto simp add: fresh_star_def fresh_def)
-done
-
-lemma at_set_avoiding2_atom:
- assumes "finite (supp c)" "finite (supp x)"
- and b: "xa \<sharp> x"
- shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
-proof -
- have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
- obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
- using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
- have c: "(p \<bullet> xa) \<sharp> c" using p1
- unfolding fresh_star_def Ball_def
- by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
- hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
- then show ?thesis by blast
-qed
-
end