diff -r eee5deb35aa8 -r d97e04126a3d Nominal/Nominal2_Base.thy
--- 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 *}