--- a/Nominal-General/Nominal2_Base.thy Sun Apr 18 18:01:22 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy Mon Apr 19 09:25:31 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