nominal2: comparison Nominal/Nominal2

equal deleted inserted replaced

-:a44479bde681
+:017e33849f4d
 Nominal Isabelle.
 *)
 theory Nominal2_Base
 imports "~~/src/HOL/Library/Old_Datatype"
 "~~/src/HOL/Library/Infinite_Set"
-"~~/src/HOL/Quotient_Examples/FSet"
+"~~/src/HOL/Library/Multiset"
+"~~/src/HOL/Library/FSet"
 "~~/src/HOL/Library/FinFun"
 keywords
 "atom_decl" "equivariance" :: thy_decl
 begin
 declare [[typedef_overloaded]]
 section {* Atoms and Sorts *}
-text {* A simple implementation for atom_sorts is strings. *}
+text {* A simple implementation for @{text atom_sorts} is strings. *}
 (* types atom_sort = string *)
 text {* To deal with Church-like binding we use trees of
 strings as sorts. *}
 end
 lemma permute_multiset [simp]:
 fixes M N::"('a::pt) multiset"
 shows "(p \<bullet> {#}) = ({#} ::('a::pt) multiset)"
-and   "(p \<bullet> {# x #}) = {# p \<bullet> x #}"
+and   "(p \<bullet> add_mset x M) = add_mset (p \<bullet> x) (p \<bullet> M)"
 and   "(p \<bullet> (M + N)) = (p \<bullet> M) + (p \<bullet> N)"
 unfolding permute_multiset_def
 by (simp_all)
 subsection {* Permutations for @{typ "'a fset"} *}
-lemma permute_fset_rsp[quot_respect]:
-shows "(op = ===> list_eq ===> list_eq) permute permute"
-unfolding rel_fun_def
-by (simp add: set_eqvt[symmetric])
 instantiation fset :: (pt) pt
 begin
-quotient_definition
+context includes fset.lifting begin
-"permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+lift_definition
-is
+"permute_fset" :: "perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-"permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+is "permute :: perm \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
-by (simp add: set_eqvt[symmetric])
+end
+context includes fset.lifting begin
 instance
 proof
 fix x :: "'a fset" and p q :: "perm"
-show "0 \<bullet> x = x" by (descending) (simp)
+show "0 \<bullet> x = x" by transfer simp
-show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
+show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"  by transfer simp
 qed
 end
+end
+context includes fset.lifting
+begin
 lemma permute_fset [simp]:
 fixes S::"('a::pt) fset"
 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
-and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
+and   "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)"
-by (lifting permute_list.simps)
+apply (transfer, simp add: empty_eqvt)
+apply (transfer, simp add: insert_eqvt)
+done
 lemma fset_eqvt:
 shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
-by (lifting set_eqvt)
+by transfer simp
+end
 subsection {* Permutations for @{typ "('a, 'b) finfun"} *}
 instantiation finfun :: (pt, pt) pt
 instance int :: pure
 proof qed (rule permute_int_def)
-section {* Infrastructure for Equivariance and Perm_simp *}
+section {* Infrastructure for Equivariance and @{text Perm_simp} *}
 subsection {* Basic functions about permutations *}
 ML_file "nominal_basics.ML"
 permute_fset fset_eqvt
 (* multisets *)
 permute_multiset
-subsection {* perm_simp infrastructure *}
+subsection {* @{text perm_simp} infrastructure *}
 definition
 "unpermute p = permute (- p)"
 lemma eqvt_apply:
 lemma eqvt_bound:
 shows "p \<bullet> unpermute p x \<equiv> x"
 unfolding unpermute_def by simp
-text {* provides perm_simp methods *}
+text {* provides @{text perm_simp} methods *}
 ML_file "nominal_permeq.ML"
 method_setup perm_simp =
 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
 lemma Collect_eqvt [eqvt]:
 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
 unfolding permute_set_eq permute_fun_def
 by (auto simp: permute_bool_def)
-lemma inter_eqvt [eqvt]:
-shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-unfolding Int_def by simp
 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 simp
 lemma Ball_eqvt [eqvt]:
 lemma UNIV_eqvt [eqvt]:
 shows "p \<bullet> UNIV = UNIV"
 unfolding UNIV_def
 by (perm_simp) (rule refl)
+lemma inter_eqvt [eqvt]:
+shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+unfolding Int_def by simp
+lemma Inter_eqvt [eqvt]:
+shows "p \<bullet> \<Inter>S = \<Inter>(p \<bullet> S)"
+unfolding Inter_eq by simp
 lemma union_eqvt [eqvt]:
 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
 unfolding Un_def by simp
-lemma UNION_eqvt [eqvt]:
+lemma Union_eqvt [eqvt]:
-shows "p \<bullet> (UNION A f) = (UNION (p \<bullet> A) (p \<bullet> f))"
+shows "p \<bullet> \<Union>A = \<Union>(p \<bullet> A)"
-unfolding UNION_eq
+unfolding Union_eq
-by (perm_simp) (simp)
+by perm_simp rule
 lemma Diff_eqvt [eqvt]:
 fixes A B :: "'a::pt set"
 shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
 unfolding set_diff_eq by simp
 unfolding psubset_eq by simp
 lemma vimage_eqvt [eqvt]:
 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
 unfolding vimage_def by simp
-lemma Union_eqvt [eqvt]:
-shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
-unfolding Union_eq by simp
-lemma Inter_eqvt [eqvt]:
-shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
-unfolding Inter_eq by simp
-thm foldr.simps
 lemma foldr_eqvt[eqvt]:
 "p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)"
 apply(induct xs)
 apply(simp_all)
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
 unfolding Sigma_def
-unfolding SUP_def
 by (perm_simp) (rule refl)
 text {*
 In order to prove that lfp is equivariant we need two
 auxiliary classes which specify that (op <=) and
 instantiation "fun" :: (pt, inf_eqvt) inf_eqvt
 begin
 instance
 apply standard
-unfolding Inf_fun_def INF_def
+unfolding Inf_fun_def
 apply(perm_simp)
 apply(rule refl)
 done
 end
 by (cases x) (simp_all)
 subsubsection {* Equivariance for @{typ "'a fset"} *}
+context includes fset.lifting begin
 lemma in_fset_eqvt [eqvt]:
 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset by simp
+by transfer 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 inter_fset_eqvt [eqvt]:
 shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
-apply(descending)
+by transfer simp
-unfolding list_eq_def inter_list_def
-apply(simp)
-done
 lemma subset_fset_eqvt [eqvt]:
 shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
-apply(descending)
+by transfer simp
-unfolding sub_list_def
-apply(simp)
-done
 lemma map_fset_eqvt [eqvt]:
-shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+shows "p \<bullet> (f |`| S) = (p \<bullet> f) |`| (p \<bullet> S)"
-by (lifting map_eqvt)
+by transfer simp
+end
 subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *}
 lemma finfun_update_eqvt [eqvt]:
 shows "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)"
 end
 | (_, _) => NONE
 end
 *}
-subsection {* helper functions for nominal_functions *}
+subsection {* helper functions for @{text nominal_functions} *}
 lemma THE_defaultI2:
 assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
 shows "Q (THE_default d P)"
 by (iprover intro: assms THE_defaultI')
 then show "finite (\<Union>{supp x | x. x \<in># M})"
 by (simp only: image_Collect)
 qed
 lemma Union_supports_multiset:
-shows "\<Union>{supp x | x. x :# M} supports M"
+shows "\<Union>{supp x | x. x \<in># M} supports M"
 proof -
-have sw: "\<And>a b. ((\<And>x. x :# M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
+have sw: "\<And>a b. ((\<And>x. x \<in># M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
-unfolding permute_multiset_def
+unfolding permute_multiset_def by (induct M) simp_all
-apply(induct M)
+have "(\<Union>x\<in>set_mset M. supp x) supports M"
-apply(simp_all)
+by (auto intro!: sw swap_fresh_fresh simp add: fresh_def supports_def)
-done
+also have "(\<Union>x\<in>set_mset M. supp x) = (\<Union>{supp x | x. x \<in># M})"
-show "(\<Union>{supp x | x. x :# M}) supports M"
+by auto
-unfolding supports_def
+finally show "(\<Union>{supp x | x. x \<in># M}) supports M" .
-apply(clarify)
-apply(rule sw)
-apply(rule swap_fresh_fresh)
-apply(simp_all only: fresh_def)
-apply(auto)
-apply(metis neq0_conv)+
-done
 qed
 lemma Union_included_multiset:
 fixes M::"('a::fs multiset)"
 shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
 proof -
-have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
+have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>x \<in> set_mset M. supp x)" by auto
-also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
 also have "... = supp (set_mset M)"
 by (simp add: supp_of_finite_sets)
 also have " ... \<subseteq> supp M" by (rule supp_set_mset)
 finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
 qed
 lemma supp_of_multisets:
 fixes M::"('a::fs multiset)"
-shows "(supp M) = (\<Union>{supp x | x. x :# M})"
+shows "(supp M) = (\<Union>{supp x | x. x \<in># M})"
 apply(rule subset_antisym)
 apply(rule supp_is_subset)
 apply(rule Union_supports_multiset)
 apply(rule Union_finite_multiset)
 apply(rule Union_included_multiset)
 lemma fresh_empty_fset:
 shows "a \<sharp> {||}"
 unfolding fresh_def
 by (simp)
-lemma supp_insert_fset [simp]:
+lemma supp_finsert [simp]:
 fixes x::"'a::fs"
 and   S::"'a fset"
-shows "supp (insert_fset x S) = supp x \<union> supp S"
+shows "supp (finsert x S) = supp x \<union> supp S"
 apply(subst supp_fset[symmetric])
 apply(simp add: supp_of_finite_insert)
 done
-lemma fresh_insert_fset:
+lemma fresh_finsert:
 fixes x::"'a::fs"
 and   S::"'a fset"
-shows "a \<sharp> insert_fset x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+shows "a \<sharp> finsert x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
 unfolding fresh_def
-by (simp)
+by simp
 lemma fset_finite_supp:
 fixes S::"('a::fs) fset"
 shows "finite (supp S)"
 by (induct S) (simp_all add: finite_supp)
 unfolding flip_def
 unfolding atom_eq_iff [symmetric]
 unfolding atom_eqvt [symmetric]
 by simp_all
-text {* the following two lemmas do not hold for at_base,
+text {* the following two lemmas do not hold for @{text at_base},
 only for single sort atoms from at *}
 lemma flip_triple:
 fixes a b c::"'a::at"
 assumes "a \<noteq> b" and "c \<noteq> b"

changeset 3245	017e33849f4d
parent 3244	a44479bde681