nominal2: comparison Nominal-General/Nominal2

equal deleted inserted replaced

-:c7cdea70eacd
+:869d1183e082
 "sort_of a \<noteq> sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) = 0"
 by (rule Rep_perm_ext) (simp add: Rep_perm_simps)
 lemma swap_cancel:
 "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
 by (rule Rep_perm_ext)
 (simp add: Rep_perm_simps expand_fun_eq)
 lemma swap_self [simp]:
 "(a \<rightleftharpoons> a) = 0"
 by (rule Rep_perm_ext, simp add: Rep_perm_simps expand_fun_eq)
 instantiation atom :: pt
 begin
 definition
-"p \<bullet> a = Rep_perm p a"
+"p \<bullet> a = (Rep_perm p) a"
 instance
 apply(default)
 apply(simp_all add: permute_atom_def Rep_perm_simps)
 done
 apply (simp add: permute_perm_def diff_minus minus_add add_assoc)
 done
 end
-lemma permute_self: "p \<bullet> p = p"
+lemma permute_self:
-unfolding permute_perm_def by (simp add: diff_minus add_assoc)
+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
 end
 lemma permute_fun_app_eq:
 shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
 unfolding permute_fun_def by simp
 subsection {* Permutations for booleans *}
 instantiation bool :: pt
 lemma permute_set_eq:
 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
 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 ..
 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 *}
 instantiation unit :: pt
 begin
 definition "p \<bullet> (u::unit) = u"
-instance proof
+instance
-qed (simp_all add: permute_unit_def)
+by (default) (simp_all add: permute_unit_def)
 end
 subsection {* Permutations for products *}
 permute_sum
 where
 "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
 | "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
-instance proof
+instance
-qed (case_tac [!] x, simp_all)
+by (default) (case_tac [!] x, simp_all)
 end
 subsection {* Permutations for lists *}
 permute_list
 where
 "p \<bullet> [] = []"
 | "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
-instance proof
+instance
-qed (induct_tac [!] x, simp_all)
+by (default) (induct_tac [!] x, simp_all)
 end
 subsection {* Permutations for options *}
 permute_option
 where
 "p \<bullet> None = None"
 | "p \<bullet> (Some x) = Some (p \<bullet> x)"
-instance proof
+instance
-qed (induct_tac [!] x, simp_all)
+by (default) (induct_tac [!] x, simp_all)
 end
 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 instantiation char :: pt
 begin
 definition "p \<bullet> (c::char) = c"
-instance proof
+instance
-qed (simp_all add: permute_char_def)
+by (default) (simp_all add: permute_char_def)
 end
 instantiation nat :: pt
 begin
 definition "p \<bullet> (n::nat) = n"
-instance proof
+instance
-qed (simp_all add: permute_nat_def)
+by (default) (simp_all add: permute_nat_def)
 end
 instantiation int :: pt
 begin
 definition "p \<bullet> (i::int) = i"
-instance proof
+instance
-qed (simp_all add: permute_int_def)
+by (default) (simp_all add: permute_int_def)
 end
 section {* Pure types *}
 shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x"
 proof -
 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 *}
 definition
 and   x :: "'a::pt"
 assumes a1: "S supports x"
 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)
+from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto
-hence "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" 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
 qed
 qed
 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:
 fixes S :: "atom set"
 and   x :: "'a::pt"
 by (metis add_diff_cancel minus_perm_def)
 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}"
 using finite_Rep_perm [of p]
 unfolding permute_atom_def .
 apply (auto simp add: expand_perm_eq swap_atom)
 done
 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})"
 by (auto simp add: supp_perm swap_atom)
 lemma fresh_minus_perm:
 fixes p::perm
 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
 unfolding fresh_def
-apply(auto simp add: supp_perm)
+unfolding supp_perm
-apply(metis permute_minus_cancel)+
+apply(simp)
+apply(metis permute_minus_cancel)
 done
 lemma supp_minus_perm:
 fixes p::perm
 shows "supp (- p) = supp p"
 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 = {}"
+assumes asm: "supp p \<inter> supp q = {}"
 shows "p + q  = q + p"
 unfolding expand_perm_eq
 proof
 fix a::"atom"
 show "(p + q) \<bullet> a = (q + p) \<bullet> a"
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 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)"
 assume b: "a \<notin> supp f \<union> supp x"
 then have "a \<notin> supp (f x)" unfolding supp_def
 by (simp add: permute_fun_app_eq)
 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

changeset 1879	869d1183e082
parent 1833	2050b5723c04
child 1930	f189cf2c0987