nominal2: comparison Nominal/Nominal2

equal deleted inserted replaced

-:4af8a92396ce
+:a44479bde681
 "~~/src/HOL/Quotient_Examples/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. *}
 (* types atom_sort = string *)
 "Rep_perm (- p) = inv (Rep_perm p)"
 unfolding uminus_perm_def
 by (simp add: Abs_perm_inverse perm_inv Rep_perm)
 instance
-apply default
+apply standard
 unfolding Rep_perm_inject [symmetric]
 unfolding minus_perm_def
 unfolding Rep_perm_add
 unfolding Rep_perm_uminus
 unfolding Rep_perm_0
 definition
 "p \<bullet> a = (Rep_perm p) a"
 instance
-apply(default)
+apply standard
 apply(simp_all add: permute_atom_def Rep_perm_simps)
 done
 end
 definition
 "p \<bullet> q = p + q - p"
 instance
-apply default
+apply standard
 apply (simp add: permute_perm_def)
 apply (simp add: permute_perm_def algebra_simps)
 done
 end
 definition
 "p \<bullet> f = (\<lambda>x. p \<bullet> (f (- p \<bullet> x)))"
 instance
-apply default
+apply standard
 apply (simp add: permute_fun_def)
 apply (simp add: permute_fun_def minus_add)
 done
 end
 begin
 definition "p \<bullet> (b::bool) = b"
 instance
-apply(default)
+apply standard
 apply(simp_all add: permute_bool_def)
 done
 end
 definition
 "p \<bullet> X = {p \<bullet> x | x. x \<in> X}"
 instance
-apply default
+apply standard
 apply (auto simp: permute_set_def)
 done
 end
 begin
 definition "p \<bullet> (u::unit) = u"
 instance
-by (default) (simp_all add: permute_unit_def)
+by standard (simp_all add: permute_unit_def)
 end
 subsection {* Permutations for products *}
 permute_prod
 where
 Pair_eqvt: "p \<bullet> (x, y) = (p \<bullet> x, p \<bullet> y)"
 instance
-by default auto
+by standard auto
 end
 subsection {* Permutations for sums *}
 where
 Inl_eqvt: "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
 | Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
 instance
-by (default) (case_tac [!] x, simp_all)
+by standard (case_tac [!] x, simp_all)
 end
 subsection {* Permutations for @{typ "'a list"} *}
 where
 Nil_eqvt:  "p \<bullet> [] = []"
 | Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
 instance
-by (default) (induct_tac [!] x, simp_all)
+by standard (induct_tac [!] x, simp_all)
 end
 lemma set_eqvt:
 shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
 where
 None_eqvt: "p \<bullet> None = None"
 | Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
 instance
-by (default) (induct_tac [!] x, simp_all)
+by standard (induct_tac [!] x, simp_all)
 end
 subsection {* Permutations for @{typ "'a multiset"} *}
 apply(assumption)
 apply(simp)
 done
 instance
-apply(default)
+apply standard
 apply(transfer)
 apply(simp)
 apply(transfer)
 apply(simp)
 done
 begin
 definition "p \<bullet> (c::char) = c"
 instance
-by (default) (simp_all add: permute_char_def)
+by standard (simp_all add: permute_char_def)
 end
 instantiation nat :: pt
 begin
 definition "p \<bullet> (n::nat) = n"
 instance
-by (default) (simp_all add: permute_nat_def)
+by standard (simp_all add: permute_nat_def)
 end
 instantiation int :: pt
 begin
 definition "p \<bullet> (i::int) = i"
 instance
-by (default) (simp_all add: permute_int_def)
+by standard (simp_all add: permute_int_def)
 end
 section {* Pure types *}
 text {* Other type constructors preserve purity. *}
 instance "fun" :: (pure, pure) pure
-by default (simp add: permute_fun_def permute_pure)
+by standard (simp add: permute_fun_def permute_pure)
 instance set :: (pure) pure
-by default (simp add: permute_set_def permute_pure)
+by standard (simp add: permute_set_def permute_pure)
 instance prod :: (pure, pure) pure
-by default (induct_tac x, simp add: permute_pure)
+by standard (induct_tac x, simp add: permute_pure)
 instance sum :: (pure, pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+by standard (induct_tac x, simp_all add: permute_pure)
 instance list :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+by standard (induct_tac x, simp_all add: permute_pure)
 instance option :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+by standard (induct_tac x, simp_all add: permute_pure)
 subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *}
 instance char :: pure
 instantiation bool :: le_eqvt
 begin
 instance
-apply(default)
+apply standard
 unfolding le_bool_def
 apply(perm_simp)
 apply(rule refl)
 done
 instantiation "fun" :: (pt, le_eqvt) le_eqvt
 begin
 instance
-apply(default)
+apply standard
 unfolding le_fun_def
 apply(perm_simp)
 apply(rule refl)
 done
 instantiation bool :: inf_eqvt
 begin
 instance
-apply(default)
+apply standard
 unfolding Inf_bool_def
 apply(perm_simp)
 apply(rule refl)
 done
 instantiation "fun" :: (pt, inf_eqvt) inf_eqvt
 begin
 instance
-apply(default)
+apply standard
 unfolding Inf_fun_def INF_def
 apply(perm_simp)
 apply(rule refl)
 done
 lemma snd_eqvt [eqvt]:
 shows "p \<bullet> (snd x) = snd (p \<bullet> x)"
 by (cases x) simp
 lemma split_eqvt [eqvt]:
-shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+shows "p \<bullet> (case_prod P x) = case_prod (p \<bullet> P) (p \<bullet> x)"
 unfolding split_def
 by simp
 subsubsection {* Equivariance for list operations *}
 fixes x::"'a::pure"
 shows "a \<sharp> x"
 unfolding fresh_def by (simp add: pure_supp)
 instance pure < fs
-by default (simp add: pure_supp)
+by standard (simp add: pure_supp)
 subsection  {* Type @{typ atom} is finitely-supported. *}
 lemma supp_atom:
 lemma fresh_atom:
 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> b"
 unfolding fresh_def supp_atom by simp
 instance atom :: fs
-by default (simp add: supp_atom)
+by standard (simp add: supp_atom)
 section {* Type @{typ perm} is finitely-supported. *}
 lemma perm_swap_eq:
 apply(simp add: fresh_def)
 done
 instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
+by standard (simp add: supp_perm finite_perm_lemma)
 section {* Finite Support instances for other types *}
 lemma fresh_Unit:
 shows "a \<sharp> ()"
 by (simp add: fresh_def supp_Unit)
 instance prod :: (fs, fs) fs
-apply default
+apply standard
 apply (case_tac x)
 apply (simp add: supp_Pair finite_supp)
 done
 lemma fresh_Inr:
 shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"
 by (simp add: fresh_def supp_Inr)
 instance sum :: (fs, fs) fs
-apply default
+apply standard
 apply (case_tac x)
 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 done
 lemma fresh_Some:
 shows "a \<sharp> Some x \<longleftrightarrow> a \<sharp> x"
 by (simp add: fresh_def supp_Some)
 instance option :: (fs) fs
-apply default
+apply standard
 apply (induct_tac x)
 apply (simp_all add: supp_None supp_Some finite_supp)
 done
 shows "supp as = set as"
 by (induct as)
 (simp_all add: supp_Nil supp_Cons supp_atom)
 instance list :: (fs) fs
-apply default
+apply standard
 apply (induct_tac x)
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 val argx = Free x
 val absf = absfree x f
 val cty_inst =
 [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
 val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)]
-val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+val thm = Thm.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
 in
 SOME(thm RS @{thm Eq_TrueI})
 end
 | (_, _) => NONE
 end
 by (simp add: supp_set)
 subsection {* Type @{typ "'a multiset"} is finitely supported *}
-lemma set_of_eqvt [eqvt]:
+lemma set_mset_eqvt [eqvt]:
-shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
+shows "p \<bullet> (set_mset M) = set_mset (p \<bullet> M)"
 by (induct M) (simp_all add: insert_eqvt empty_eqvt)
-lemma supp_set_of:
+lemma supp_set_mset:
-shows "supp (set_of M) \<subseteq> supp M"
+shows "supp (set_mset M) \<subseteq> supp M"
 apply (rule supp_fun_app_eqvt)
 unfolding eqvt_def
 apply(perm_simp)
 apply(simp)
 done
 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_of M})" by simp
+have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
-also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
+also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
-also have "... = supp (set_of M)"
+also have "... = supp (set_mset M)"
 by (simp add: supp_of_finite_sets)
-also have " ... \<subseteq> supp M" by (rule supp_set_of)
+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 {#} = {}"
 unfolding supp_def
 by simp
 instance multiset :: (fs) fs
-apply (default)
+by standard (rule multisets_supp_finite)
-apply (rule multisets_supp_finite)
-done
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 lemma supp_fset [simp]:
 shows "supp (fset S) = supp S"
 shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
 unfolding fresh_def
 by (simp add: supp_union_fset)
 instance fset :: (fs) fs
-apply (default)
+by standard (rule fset_finite_supp)
-apply (rule fset_finite_supp)
-done
 subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *}
 lemma fresh_finfun_const:
 shows "supp (finfun_update f x y) \<subseteq> supp(f, x, y)"
 using fresh_finfun_update
 by (auto simp: fresh_def supp_Pair)
 instance finfun :: (fs, fs) fs
-apply(default)
+apply standard
 apply(induct_tac x rule: finfun_weak_induct)
 apply(simp add: supp_finfun_const finite_supp)
 apply(rule finite_subset)
 apply(rule supp_finfun_update)
 apply(simp add: supp_Pair finite_supp)

changeset 3244	a44479bde681
parent 3239	67370521c09c
child 3245	017e33849f4d