--- a/Nominal/Nominal2_Base.thy Mon Feb 28 16:47:13 2011 +0000
+++ b/Nominal/Nominal2_Base.thy Tue Mar 01 00:14:02 2011 +0000
@@ -80,6 +80,7 @@
shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
by (induct a, induct b, simp)
+
section {* Sort-Respecting Permutations *}
typedef perm =
@@ -150,9 +151,9 @@
instance perm :: size ..
+
subsection {* Permutations form a (multiplicative) group *}
-
instantiation perm :: group_add
begin
@@ -381,30 +382,6 @@
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)"
- unfolding permute_perm_def by simp
-
-lemma zero_perm_eqvt:
- shows "p \<bullet> (0::perm) = 0"
- unfolding permute_perm_def by simp
-
-lemma add_perm_eqvt:
- fixes p p1 p2 :: perm
- shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2"
- unfolding permute_perm_def
- by (simp add: perm_eq_iff)
-
-lemma swap_eqvt:
- shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"
- unfolding permute_perm_def
- by (auto simp add: swap_atom perm_eq_iff)
-
-lemma uminus_eqvt:
- fixes p q::"perm"
- shows "p \<bullet> (- q) = - (p \<bullet> q)"
- unfolding permute_perm_def
- by (simp add: diff_minus minus_add add_assoc)
subsection {* Permutations for functions *}
@@ -474,15 +451,8 @@
lemma permute_finite [simp]:
shows "finite (p \<bullet> X) = finite X"
-apply(simp add: permute_set_eq_image)
-apply(rule iffI)
-apply(drule finite_imageD)
-using inj_permute[where p="p"]
-apply(simp add: inj_on_def)
-apply(assumption)
-apply(rule finite_imageI)
-apply(assumption)
-done
+ unfolding permute_set_eq_vimage
+ using bij_permute by (rule finite_vimage_iff)
lemma swap_set_not_in:
assumes a: "a \<notin> S" "b \<notin> S"
@@ -522,7 +492,8 @@
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
unfolding permute_set_eq_image image_insert ..
-subsection {* Permutations for units *}
+
+subsection {* Permutations for @{typ unit} *}
instantiation unit :: pt
begin
@@ -566,7 +537,7 @@
end
-subsection {* Permutations for lists *}
+subsection {* Permutations for @{typ "'a list"} *}
instantiation list :: (pt) pt
begin
@@ -588,7 +559,7 @@
-subsection {* Permutations for options *}
+subsection {* Permutations for @{typ "'a option"} *}
instantiation option :: (pt) pt
begin
@@ -605,9 +576,7 @@
end
-subsection {* Permutations for fsets *}
-
-
+subsection {* Permutations for @{typ "'a fset"} *}
lemma permute_fset_rsp[quot_respect]:
shows "(op = ===> list_eq ===> list_eq) permute permute"
@@ -641,6 +610,7 @@
shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
by (lifting set_eqvt)
+
subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
instantiation char :: pt
@@ -720,13 +690,14 @@
proof qed (rule permute_int_def)
+section {* Infrastructure for Equivariance and Perm_simp *}
subsection {* Basic functions about permutations *}
use "nominal_basics.ML"
-subsection {* Equivariance infrastructure *}
+subsection {* Eqvt infrastructure *}
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
@@ -735,11 +706,8 @@
lemmas [eqvt] =
- (* permutations *)
- uminus_eqvt add_perm_eqvt swap_eqvt
-
- (* datatypes *)
- Pair_eqvt
+ (* pt types *)
+ permute_prod.simps
permute_list.simps
permute_option.simps
permute_sum.simps
@@ -785,6 +753,13 @@
{* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
{* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+
+subsubsection {* Equivariance for permutations and swapping *}
+
+lemma permute_eqvt:
+ shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"
+ unfolding permute_perm_def by simp
+
(* the normal version of this lemma would cause loops *)
lemma permute_eqvt_raw[eqvt_raw]:
shows "p \<bullet> permute \<equiv> permute"
@@ -793,6 +768,28 @@
apply(simp)
done
+lemma zero_perm_eqvt [eqvt]:
+ shows "p \<bullet> (0::perm) = 0"
+ unfolding permute_perm_def by simp
+
+lemma add_perm_eqvt [eqvt]:
+ fixes p p1 p2 :: perm
+ shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2"
+ unfolding permute_perm_def
+ by (simp add: perm_eq_iff)
+
+lemma swap_eqvt [eqvt]:
+ shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"
+ unfolding permute_perm_def
+ by (auto simp add: swap_atom perm_eq_iff)
+
+lemma uminus_eqvt [eqvt]:
+ fixes p q::"perm"
+ shows "p \<bullet> (- q) = - (p \<bullet> q)"
+ unfolding permute_perm_def
+ by (simp add: diff_minus minus_add add_assoc)
+
+
subsubsection {* Equivariance of Logical Operators *}
lemma eq_eqvt [eqvt]:
@@ -800,15 +797,15 @@
unfolding permute_eq_iff permute_bool_def ..
lemma Not_eqvt [eqvt]:
- shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
-by (simp add: permute_bool_def)
+ shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
+ by (simp add: permute_bool_def)
lemma conj_eqvt [eqvt]:
- shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ shows "p \<bullet> (A \<and> B) \<longleftrightarrow> (p \<bullet> A) \<and> (p \<bullet> B)"
by (simp add: permute_bool_def)
lemma imp_eqvt [eqvt]:
- shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+ shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)"
by (simp add: permute_bool_def)
declare imp_eqvt[folded induct_implies_def, eqvt]
@@ -839,8 +836,6 @@
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
@@ -865,7 +860,7 @@
unfolding permute_bool_def ..
lemma disj_eqvt [eqvt]:
- shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+ shows "p \<bullet> (A \<or> B) \<longleftrightarrow> (p \<bullet> A) \<or> (p \<bullet> B)"
by (simp add: permute_bool_def)
lemma all_eqvt2:
@@ -902,95 +897,142 @@
apply(rule theI'[OF unique])
done
-subsubsection {* Equivariance Set Operations *}
-
-lemma Bex_eqvt[eqvt]:
+subsubsection {* Equivariance set operations *}
+
+lemma Bex_eqvt [eqvt]:
shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
unfolding Bex_def
by (perm_simp) (rule refl)
-lemma Ball_eqvt[eqvt]:
+lemma Ball_eqvt [eqvt]:
shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
unfolding Ball_def
by (perm_simp) (rule refl)
-lemma UNIV_eqvt[eqvt]:
+lemma UNIV_eqvt [eqvt]:
shows "p \<bullet> UNIV = UNIV"
unfolding UNIV_def
by (perm_simp) (rule refl)
-lemma union_eqvt[eqvt]:
+lemma union_eqvt [eqvt]:
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
unfolding Un_def
by (perm_simp) (rule refl)
-lemma Diff_eqvt[eqvt]:
+lemma Diff_eqvt [eqvt]:
fixes A B :: "'a::pt set"
- shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+ shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
unfolding set_diff_eq
by (perm_simp) (rule refl)
-lemma Compl_eqvt[eqvt]:
+lemma Compl_eqvt [eqvt]:
fixes A :: "'a::pt set"
shows "p \<bullet> (- A) = - (p \<bullet> A)"
unfolding Compl_eq_Diff_UNIV
by (perm_simp) (rule refl)
-lemma subset_eqvt[eqvt]:
+lemma subset_eqvt [eqvt]:
shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
unfolding subset_eq
by (perm_simp) (rule refl)
-lemma psubset_eqvt[eqvt]:
+lemma psubset_eqvt [eqvt]:
shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
unfolding psubset_eq
by (perm_simp) (rule refl)
-lemma vimage_eqvt[eqvt]:
+lemma vimage_eqvt [eqvt]:
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
unfolding vimage_def
by (perm_simp) (rule refl)
-lemma Union_eqvt[eqvt]:
+lemma Union_eqvt [eqvt]:
shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
unfolding Union_eq
by (perm_simp) (rule refl)
+(* FIXME: eqvt attribute *)
lemma Sigma_eqvt:
shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
unfolding Sigma_def
unfolding UNION_eq_Union_image
by (perm_simp) (rule refl)
-lemma finite_permute_iff:
- shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
- unfolding permute_set_eq_vimage
- using bij_permute by (rule finite_vimage_iff)
-
-lemma finite_eqvt[eqvt]:
+lemma finite_eqvt [eqvt]:
shows "p \<bullet> finite A = finite (p \<bullet> A)"
- unfolding finite_permute_iff permute_bool_def ..
-
-
-subsubsection {* Product Operations *}
-
-lemma fst_eqvt[eqvt]:
+ unfolding permute_finite permute_bool_def ..
+
+subsubsection {* Equivariance for product operations *}
+
+lemma fst_eqvt [eqvt]:
"p \<bullet> (fst x) = fst (p \<bullet> x)"
by (cases x) simp
-lemma snd_eqvt[eqvt]:
+lemma snd_eqvt [eqvt]:
"p \<bullet> (snd x) = snd (p \<bullet> x)"
by (cases x) simp
-lemma split_eqvt[eqvt]:
+lemma split_eqvt [eqvt]:
shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
unfolding split_def
by (perm_simp) (rule refl)
-
-
-subsection {* Supp, Freshness and Supports *}
+subsubsection {* Equivariance for list operations *}
+
+lemma append_eqvt [eqvt]:
+ shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ by (induct xs) auto
+
+lemma rev_eqvt [eqvt]:
+ shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ by (induct xs) (simp_all add: append_eqvt)
+
+lemma map_eqvt [eqvt]:
+ shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+
+lemma removeAll_eqvt [eqvt]:
+ shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+ by (induct xs) (auto)
+
+lemma filter_eqvt [eqvt]:
+ shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt [eqvt]:
+ shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
+lemma length_eqvt [eqvt]:
+ shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
+
+subsubsection {* Equivariance for @{typ "'a fset"} *}
+
+lemma in_fset_eqvt [eqvt]:
+ shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
+unfolding in_fset
+by (perm_simp) (simp)
+
+lemma union_fset_eqvt [eqvt]:
+ shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
+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)"
+ by (lifting map_eqvt)
+
+
+section {* Supp, Freshness and Supports *}
context pt
begin
@@ -1096,7 +1138,7 @@
qed
-subsection {* supports *}
+section {* supports *}
definition
supports :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" (infixl "supports" 80)
@@ -1198,13 +1240,15 @@
"supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
+
section {* Finitely-supported types *}
class fs = pt +
assumes finite_supp: "finite (supp x)"
lemma pure_supp:
- shows "supp (x::'a::pure) = {}"
+ fixes x::"'a::pure"
+ shows "supp x = {}"
unfolding supp_def by (simp add: permute_pure)
lemma pure_fresh:
@@ -1306,9 +1350,6 @@
unfolding supp_conv_fresh
by (simp add: fresh_minus_perm)
-instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
-
lemma plus_perm_eq:
fixes p q::"perm"
assumes asm: "supp p \<inter> supp q = {}"
@@ -1367,6 +1408,10 @@
by blast
qed
+instance perm :: fs
+by default (simp add: supp_perm finite_perm_lemma)
+
+
section {* Finite Support instances for other types *}
@@ -1472,17 +1517,6 @@
shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
-
-subsubsection {* List Operations *}
-
-lemma append_eqvt[eqvt]:
- shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
- by (induct xs) auto
-
-lemma rev_eqvt[eqvt]:
- shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
- by (induct xs) (simp_all add: append_eqvt)
-
lemma supp_rev:
shows "supp (rev xs) = supp xs"
by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
@@ -1491,39 +1525,17 @@
shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
-lemma map_eqvt[eqvt]:
- shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
- by (induct xs) (simp_all, simp only: permute_fun_app_eq)
-
-lemma removeAll_eqvt[eqvt]:
- shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
- by (induct xs) (auto)
-
lemma supp_removeAll:
fixes x::"atom"
shows "supp (removeAll x xs) = supp xs - {x}"
by (induct xs)
(auto simp add: supp_Nil supp_Cons supp_atom)
-lemma filter_eqvt[eqvt]:
- shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
-apply(induct xs)
-apply(simp)
-apply(simp only: filter.simps permute_list.simps if_eqvt)
-apply(simp only: permute_fun_app_eq)
-done
-
-lemma distinct_eqvt[eqvt]:
- shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
-apply(induct xs)
-apply(simp add: permute_bool_def)
-apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
-done
-
-lemma length_eqvt[eqvt]:
- shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
-by (induct xs) (simp_all add: permute_pure)
-
+lemma supp_of_atom_list:
+ fixes as::"atom list"
+ shows "supp as = set as"
+by (induct as)
+ (simp_all add: supp_Nil supp_Cons supp_atom)
instance list :: (fs) fs
apply default
@@ -1531,12 +1543,6 @@
apply (simp_all add: supp_Nil supp_Cons finite_supp)
done
-lemma supp_of_atom_list:
- fixes as::"atom list"
- shows "supp as = set as"
-by (induct as)
- (simp_all add: supp_Nil supp_Cons supp_atom)
-
section {* Support and Freshness for Applications *}
@@ -1560,11 +1566,18 @@
by auto
-subsection {* Equivariance *}
+subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*}
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
@@ -1591,17 +1604,9 @@
lemma supp_fun_app_eqvt:
assumes a: "eqvt f"
shows "supp (f x) \<subseteq> supp x"
-proof -
- from a have "supp f = {}" by (simp add: supp_fun_eqvt)
- then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast
-qed
-
-
-
-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)"
+ using fresh_fun_eqvt_app[OF a]
+ unfolding fresh_def
+ by auto
lemma supp_eqvt_at:
assumes asm: "eqvt_at f x"
@@ -1699,6 +1704,7 @@
using assms
by (auto intro: fundef_ex1_eqvt)
+
section {* Support of Finite Sets of Finitely Supported Elements *}
text {* support and freshness for atom sets *}
@@ -1863,22 +1869,6 @@
shows "finite (supp S)"
by (induct S) (simp_all add: finite_supp)
-
-instance fset :: (fs) fs
- apply (default)
- apply (rule fset_finite_supp)
- done
-
-
-lemma in_fset_eqvt[eqvt]:
- shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset
-by (perm_simp) (simp)
-
-lemma union_fset_eqvt[eqvt]:
- shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
-by (induct S) (simp_all)
-
lemma supp_union_fset:
fixes S T::"'a::fs fset"
shows "supp (S |\<union>| T) = supp S \<union> supp T"
@@ -1890,9 +1880,11 @@
unfolding fresh_def
by (simp add: supp_union_fset)
-lemma map_fset_eqvt[eqvt]:
- shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
- by (lifting map_eqvt)
+instance fset :: (fs) fs
+ apply (default)
+ apply (rule fset_finite_supp)
+ done
+
section {* Freshness and Fresh-Star *}
@@ -2041,6 +2033,7 @@
by (perm_simp) (rule refl)
+
section {* Induction principle for permutations *}