--- a/Nominal/Nominal2_Base.thy Wed May 04 15:27:04 2011 +0800
+++ b/Nominal/Nominal2_Base.thy Mon May 09 04:46:43 2011 +0100
@@ -761,7 +761,7 @@
unfolding permute_perm_def by simp
(* the normal version of this lemma would cause loops *)
-lemma permute_eqvt_raw[eqvt_raw]:
+lemma permute_eqvt_raw [eqvt_raw]:
shows "p \<bullet> permute \<equiv> permute"
apply(simp add: fun_eq_iff permute_fun_def)
apply(subst permute_eqvt)
@@ -827,26 +827,6 @@
unfolding Ex1_def
by (perm_simp) (rule refl)
-lemma mem_eqvt [eqvt]:
- shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_def
- by (simp add: permute_fun_app_eq)
-
-lemma Collect_eqvt [eqvt]:
- shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
-
-lemma inter_eqvt [eqvt]:
- shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def
- by (perm_simp) (rule refl)
-
-lemma image_eqvt [eqvt]:
- shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
- unfolding permute_set_eq_image
- unfolding permute_fun_def [where f=f]
- by (simp add: image_image)
-
lemma if_eqvt [eqvt]:
shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
by (simp add: permute_fun_def permute_bool_def)
@@ -897,7 +877,21 @@
apply(rule theI'[OF unique])
done
-subsubsection {* Equivariance set operations *}
+subsubsection {* Equivariance of Set operators *}
+
+lemma mem_eqvt [eqvt]:
+ shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ unfolding mem_def
+ by (rule permute_fun_app_eq)
+
+lemma Collect_eqvt [eqvt]:
+ shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ unfolding Collect_def permute_fun_def ..
+
+lemma inter_eqvt [eqvt]:
+ shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ unfolding Int_def
+ by (perm_simp) (rule refl)
lemma Bex_eqvt [eqvt]:
shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
@@ -909,6 +903,11 @@
unfolding Ball_def
by (perm_simp) (rule refl)
+lemma image_eqvt [eqvt]:
+ shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ unfolding image_def
+ by (perm_simp) (rule refl)
+
lemma UNIV_eqvt [eqvt]:
shows "p \<bullet> UNIV = UNIV"
unfolding UNIV_def
@@ -965,12 +964,12 @@
subsubsection {* Equivariance for product operations *}
lemma fst_eqvt [eqvt]:
- "p \<bullet> (fst x) = fst (p \<bullet> x)"
- by (cases x) simp
+ shows "p \<bullet> (fst x) = fst (p \<bullet> x)"
+ by (cases x) simp
lemma snd_eqvt [eqvt]:
- "p \<bullet> (snd x) = snd (p \<bullet> x)"
- by (cases x) simp
+ shows "p \<bullet> (snd x) = snd (p \<bullet> x)"
+ by (cases x) simp
lemma split_eqvt [eqvt]:
shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
@@ -1025,7 +1024,7 @@
lemma union_fset_eqvt [eqvt]:
shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
-by (induct S) (simp_all)
+ by (induct S) (simp_all)
lemma map_fset_eqvt [eqvt]:
shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
@@ -1336,7 +1335,7 @@
lemma plus_perm_eq:
fixes p q::"perm"
assumes asm: "supp p \<inter> supp q = {}"
- shows "p + q = q + p"
+ shows "p + q = q + p"
unfolding perm_eq_iff
proof
fix a::"atom"
@@ -1419,7 +1418,7 @@
instance prod :: (fs, fs) fs
apply default
-apply (induct_tac x)
+apply (case_tac x)
apply (simp add: supp_Pair finite_supp)
done
@@ -1444,7 +1443,7 @@
instance sum :: (fs, fs) fs
apply default
-apply (induct_tac x)
+apply (case_tac x)
apply (simp_all add: supp_Inl supp_Inr finite_supp)
done
@@ -1480,22 +1479,22 @@
shows "supp [] = {}"
by (simp add: supp_def)
+lemma fresh_Nil:
+ shows "a \<sharp> []"
+ by (simp add: fresh_def supp_Nil)
+
lemma supp_Cons:
shows "supp (x # xs) = supp x \<union> supp xs"
by (simp add: supp_def Collect_imp_eq Collect_neg_eq)
+lemma fresh_Cons:
+ shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs"
+ by (simp add: fresh_def supp_Cons)
+
lemma supp_append:
shows "supp (xs @ ys) = supp xs \<union> supp ys"
by (induct xs) (auto simp add: supp_Nil supp_Cons)
-lemma fresh_Nil:
- shows "a \<sharp> []"
- by (simp add: fresh_def supp_Nil)
-
-lemma fresh_Cons:
- shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs"
- by (simp add: fresh_def supp_Cons)
-
lemma fresh_append:
shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
@@ -1540,7 +1539,7 @@
using assms
unfolding fresh_conv_MOST
unfolding permute_fun_app_eq
- by (elim MOST_rev_mp, simp)
+ by (elim MOST_rev_mp) (simp)
lemma supp_fun_app:
shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
@@ -1554,13 +1553,11 @@
definition
"eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
-
text {* equivariance of a function at a given argument *}
definition
"eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
-
lemma eqvtI:
shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
unfolding eqvt_def
@@ -2031,6 +2028,19 @@
section {* Induction principle for permutations *}
+lemma smaller_supp:
+ assumes a: "a \<in> supp p"
+ shows "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p"
+proof -
+ have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subseteq> supp p"
+ unfolding supp_perm by (auto simp add: swap_atom)
+ moreover
+ have "a \<notin> supp ((p \<bullet> a \<rightleftharpoons> a) + p)" by (simp add: supp_perm)
+ then have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<noteq> supp p" using a by auto
+ ultimately
+ show "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p" by auto
+qed
+
lemma perm_struct_induct[consumes 1, case_names zero swap]:
assumes S: "supp p \<subseteq> S"
@@ -2054,11 +2064,7 @@
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 by (auto simp add: supp_atom supp_perm swap_atom)
let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
- have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
- moreover
- have "a \<notin> supp ?q" by (simp add: supp_perm)
- then have "supp ?q \<noteq> supp p" using a0 by auto
- ultimately have "supp ?q \<subset> supp p" using a2 by auto
+ have a2: "supp ?q \<subset> supp p" using a0 smaller_supp by simp
then have "P ?q" using ih by simp
moreover
have "supp ?q \<subseteq> S" using as a2 by simp
@@ -2139,6 +2145,7 @@
qed
qed
+text {* same lemma as above, but proved with a different induction principle *}
lemma supp_perm_eq_test:
assumes "(supp x) \<sharp>* p"
shows "p \<bullet> x = x"
@@ -2163,8 +2170,24 @@
lemma perm_supp_eq:
assumes a: "(supp p) \<sharp>* x"
shows "p \<bullet> x = x"
-by (rule supp_perm_eq)
- (simp add: fresh_star_supp_conv a)
+proof -
+ from assms have "supp p \<subseteq> {a. a \<sharp> x}"
+ unfolding supp_perm fresh_star_def fresh_def by auto
+ then show "p \<bullet> x = x"
+ proof (induct p rule: perm_struct_induct2)
+ case zero
+ show "0 \<bullet> x = x" by simp
+ next
+ case (swap a b)
+ then have "a \<sharp> x" "b \<sharp> x" by simp_all
+ then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+ next
+ case (plus p1 p2)
+ have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
+ then show "(p1 + p2) \<bullet> x = x" by simp
+ qed
+qed
+
lemma supp_perm_perm_eq:
assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
@@ -2562,7 +2585,7 @@
apply(simp)
done
-lemma fresh_at_base_permute_iff[simp]:
+lemma fresh_at_base_permute_iff [simp]:
fixes a::"'a::at_base"
shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
unfolding atom_eqvt[symmetric]