nominal2: comparison Nominal/Nominal2

equal deleted inserted replaced

-:eee5deb35aa8
+:d97e04126a3d
 lemma atom_components_eq_iff:
 fixes a b :: atom
 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 =
 "{f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}"
 proof
 "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"
 by (simp add: fun_eq_iff Rep_perm_inject [symmetric])
 instance perm :: size ..
 subsection {* Permutations form a (multiplicative) group *}
 instantiation perm :: group_add
 begin
 definition
 lemma pemute_minus_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)"
-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 *}
 instantiation "fun" :: (pt, pt) pt
 begin
 unfolding permute_fun_def permute_bool_def
 unfolding vimage_def Collect_def mem_def ..
 lemma permute_finite [simp]:
 shows "finite (p \<bullet> X) = finite X"
-apply(simp add: permute_set_eq_image)
+unfolding permute_set_eq_vimage
-apply(rule iffI)
+using bij_permute by (rule finite_vimage_iff)
-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
 lemma swap_set_not_in:
 assumes a: "a \<notin> S" "b \<notin> S"
 shows "(a \<rightleftharpoons> b) \<bullet> S = S"
 unfolding permute_set_eq
 lemma insert_eqvt:
 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
 definition "p \<bullet> (u::unit) = u"
 instance
 by (default) (case_tac [!] x, simp_all)
 end
-subsection {* Permutations for lists *}
+subsection {* Permutations for @{typ "'a list"} *}
 instantiation list :: (pt) pt
 begin
 primrec
 shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
 by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
-subsection {* Permutations for options *}
+subsection {* Permutations for @{typ "'a option"} *}
 instantiation option :: (pt) pt
 begin
 primrec
 by (default) (induct_tac [!] x, simp_all)
 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"
 unfolding fun_rel_def
 by (simp add: set_eqvt[symmetric])
 lemma fset_eqvt:
 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
 begin
 instance int :: pure
 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} *}
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 lemmas [eqvt] =
-(* permutations *)
+(* pt types *)
-uminus_eqvt add_perm_eqvt swap_eqvt
+permute_prod.simps
-(* datatypes *)
-Pair_eqvt
 permute_list.simps
 permute_option.simps
 permute_sum.simps
 (* sets *)
 {* pushes permutations inside. *}
 method_setup perm_strict_simp =
 {* 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"
 apply(simp add: fun_eq_iff permute_fun_def)
 apply(subst permute_eqvt)
 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]:
 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
 unfolding permute_eq_iff permute_bool_def ..
 lemma Not_eqvt [eqvt]:
-shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
+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]
 lemma ex_eqvt [eqvt]:
 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 False_eqvt [eqvt]:
 shows "p \<bullet> False = False"
 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:
 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
 by (perm_simp add: permute_minus_cancel) (rule refl)
 apply(simp add: permute_bool_def unique)
 apply(simp add: permute_bool_def)
 apply(rule theI'[OF unique])
 done
-subsubsection {* Equivariance Set Operations *}
+subsubsection {* Equivariance set operations *}
-lemma Bex_eqvt[eqvt]:
+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:
+lemma finite_eqvt [eqvt]:
-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]:
 shows "p \<bullet> finite A = finite (p \<bullet> A)"
-unfolding finite_permute_iff permute_bool_def ..
+unfolding permute_finite permute_bool_def ..
+subsubsection {* Equivariance for product operations *}
-subsubsection {* Product Operations *}
+lemma fst_eqvt [eqvt]:
-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)
+subsubsection {* Equivariance for list operations *}
-subsection {* Supp, Freshness and Supports *}
+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
 definition
 then have "p \<bullet> - p \<bullet> a \<sharp> p \<bullet> x" by (simp only: fresh_permute_iff)
 then show "a \<sharp> p \<bullet> x" by simp
 qed
-subsection {* supports *}
+section {* supports *}
 definition
 supports :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" (infixl "supports" 80)
 where
 "S supports x \<equiv> \<forall>a b. (a \<notin> S \<and> b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x)"
 definition
 "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:
 fixes x::"'a::pure"
 shows "a \<sharp> x"
 lemma supp_minus_perm:
 fixes p::perm
 shows "supp (- p) = supp p"
 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 = {}"
 shows "p + q  = q + p"
 by blast
 then show "supp (p + q) = supp p \<union> supp q" using supp_plus_perm
 by blast
 qed
+instance perm :: fs
+by default (simp add: supp_perm finite_perm_lemma)
 section {* Finite Support instances for other types *}
 subsection {* Type @{typ "'a \<times> 'b"} is finitely-supported. *}
 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)
-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)
 lemma fresh_rev:
 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]:
+lemma supp_of_atom_list:
-shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+fixes as::"atom list"
-apply(induct xs)
+shows "supp as = set as"
-apply(simp)
+by (induct as)
-apply(simp only: filter.simps permute_list.simps if_eqvt)
+(simp_all add: supp_Nil supp_Cons supp_atom)
-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)
 instance list :: (fs) fs
 apply default
 apply (induct_tac x)
 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 *}
 lemma fresh_conv_MOST:
 using fresh_fun_app
 unfolding fresh_def
 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
 by simp
 qed
 lemma supp_fun_app_eqvt:
 assumes a: "eqvt f"
 shows "supp (f x) \<subseteq> supp x"
-proof -
+using fresh_fun_eqvt_app[OF a]
-from a have "supp f = {}" by (simp add: supp_fun_eqvt)
+unfolding fresh_def
-then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast
+by auto
-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)"
 lemma supp_eqvt_at:
 assumes asm: "eqvt_at f x"
 and     fin: "finite (supp x)"
 shows "supp (f x) \<subseteq> supp x"
 assumes ex1: "\<exists>!y. G x y"
 shows "eqvt_at f x"
 unfolding eqvt_at_def
 using assms
 by (auto intro: fundef_ex1_eqvt)
 section {* Support of Finite Sets of Finitely Supported Elements *}
 text {* support and freshness for atom sets *}
 lemma fset_finite_supp:
 fixes S::"('a::fs) fset"
 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"
 by (induct S) (auto)
 fixes S T::"'a::fs fset"
 shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
 unfolding fresh_def
 by (simp add: supp_union_fset)
-lemma map_fset_eqvt[eqvt]:
+instance fset :: (fs) fs
-shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+apply (default)
-by (lifting map_eqvt)
+apply (rule fset_finite_supp)
+done
 section {* Freshness and Fresh-Star *}
 lemma fresh_Unit_elim:
 shows "(a \<sharp> () \<Longrightarrow> PROP C) \<equiv> PROP C"
 lemma fresh_star_eqvt [eqvt]:
 shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
 unfolding fresh_star_def
 by (perm_simp) (rule refl)
 section {* Induction principle for permutations *}

changeset 2735	d97e04126a3d
parent 2733	5f6fefdbf055
child 2742	f1192e3474e0