--- a/NEWS Sun Jan 26 22:45:57 2025 +0100
+++ b/NEWS Mon Jan 27 12:13:37 2025 +0100
@@ -313,6 +313,9 @@
* Theory "HOL-Library.Suc_Notation" provides compact notation for
iterated Suc terms.
+* Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor
+INCOMPATIBILITY: need to adjust theory imports.
+
*** ML ***
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jan 27 12:13:37 2025 +0100
@@ -5,7 +5,6 @@
Main
"HOL-Library.Old_Datatype"
"HOL-Library.Old_Recdef"
- "HOL-Library.Adhoc_Overloading"
"HOL-Library.Dlist"
"HOL-Library.FSet"
Base
@@ -648,41 +647,6 @@
\<close>
-section \<open>Adhoc overloading of constants\<close>
-
-text \<open>
- \begin{tabular}{rcll}
- @{command_def "adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
- @{command_def "no_adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
- @{attribute_def "show_variants"} & : & \<open>attribute\<close> & default \<open>false\<close> \\
- \end{tabular}
-
- \<^medskip>
- Adhoc overloading allows to overload a constant depending on its type.
- Typically this involves the introduction of an uninterpreted constant (used
- for input and output) and the addition of some variants (used internally).
- For examples see \<^file>\<open>~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy\<close> and
- \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
-
- \<^rail>\<open>
- (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
- (@{syntax name} (@{syntax term} + ) + @'and')
- \<close>
-
- \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
- existing constant.
-
- \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
- "adhoc_overloading"}, but removes the specified variants from the present
- context.
-
- \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded
- constants. If enabled, the internally used variants are printed instead of
- their respective overloaded constants. This is occasionally useful to check
- whether the system agrees with a user's expectations about derived variants.
-\<close>
-
-
section \<open>Definition by specification \label{sec:hol-specification}\<close>
text \<open>
--- a/src/Doc/Isar_Ref/Spec.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 12:13:37 2025 +0100
@@ -1093,6 +1093,41 @@
lemma "Length ((a, b, c, d, e), ()) = 1" by simp
+section \<open>Overloaded constant abbreviations: adhoc overloading\<close>
+
+text \<open>
+ \begin{tabular}{rcll}
+ @{command_def "adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "no_adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{attribute_def "show_variants"} & : & \<open>attribute\<close> & default \<open>false\<close> \\
+ \end{tabular}
+
+ \<^medskip>
+ Adhoc overloading allows to overload a constant depending on its type.
+ Typically this involves the introduction of an uninterpreted constant (used
+ for input and output) and the addition of some variants (used internally).
+ For examples see \<^file>\<open>~~/src/HOL/Examples/Adhoc_Overloading.thy\<close> and
+ \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
+
+ \<^rail>\<open>
+ (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
+ (@{syntax name} (@{syntax term} + ) + @'and')
+ \<close>
+
+ \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
+ existing constant.
+
+ \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
+ "adhoc_overloading"}, but removes the specified variants from the present
+ context.
+
+ \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded
+ constants. If enabled, the internally used variants are printed instead of
+ their respective overloaded constants. This is occasionally useful to check
+ whether the system agrees with a user's expectations about derived variants.
+\<close>
+
+
section \<open>Incorporating ML code \label{sec:ML}\<close>
text \<open>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Adhoc_Overloading.thy Mon Jan 27 12:13:37 2025 +0100
@@ -0,0 +1,254 @@
+(* Title: HOL/Examples/Adhoc_Overloading.thy
+ Author: Christian Sternagel
+*)
+
+section \<open>Ad Hoc Overloading\<close>
+
+theory Adhoc_Overloading
+imports
+ Main
+ "HOL-Library.Infinite_Set"
+begin
+
+text \<open>Adhoc overloading allows to overload a constant depending on
+its type. Typically this involves to introduce an uninterpreted
+constant (used for input and output) and then add some variants (used
+internally).\<close>
+
+subsection \<open>Plain Ad Hoc Overloading\<close>
+
+text \<open>Consider the type of first-order terms.\<close>
+datatype ('a, 'b) "term" =
+ Var 'b |
+ Fun 'a "('a, 'b) term list"
+
+text \<open>The set of variables of a term might be computed as follows.\<close>
+fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
+ "term_vars (Var x) = {x}" |
+ "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
+
+text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
+rewrite systems (i.e., sets of rules), the set of variables makes
+sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
+
+consts vars :: "'a \<Rightarrow> 'b set"
+
+text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
+adhoc_overloading
+ vars term_vars
+
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
+
+fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
+ "rule_vars (l, r) = vars l \<union> vars r"
+
+adhoc_overloading
+ vars rule_vars
+
+value [nbe] "vars (Var 1, Var 0)"
+
+definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
+ "trs_vars R = \<Union>(rule_vars ` R)"
+
+adhoc_overloading
+ vars trs_vars
+
+value [nbe] "vars {(Var 1, Var 0)}"
+
+text \<open>Sometimes it is necessary to add explicit type constraints
+before a variant can be determined.\<close>
+(*value "vars R" (*has multiple instances*)*)
+value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
+
+text \<open>It is also possible to remove variants.\<close>
+no_adhoc_overloading
+ vars term_vars rule_vars
+
+(*value "vars (Var 1)" (*does not have an instance*)*)
+
+text \<open>As stated earlier, the overloaded constant is only used for
+input and output. Internally, always a variant is used, as can be
+observed by the configuration option \<open>show_variants\<close>.\<close>
+
+adhoc_overloading
+ vars term_vars
+
+declare [[show_variants]]
+
+term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
+
+
+subsection \<open>Adhoc Overloading inside Locales\<close>
+
+text \<open>As example we use permutations that are parametrized over an
+atom type \<^typ>\<open>'a\<close>.\<close>
+
+definition perms :: "('a \<Rightarrow> 'a) set" where
+ "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
+
+typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
+ by standard (auto simp: perms_def)
+
+text \<open>First we need some auxiliary lemmas.\<close>
+lemma permsI [Pure.intro]:
+ assumes "bij f" and "MOST x. f x = x"
+ shows "f \<in> perms"
+ using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
+
+lemma perms_imp_bij:
+ "f \<in> perms \<Longrightarrow> bij f"
+ by (simp add: perms_def)
+
+lemma perms_imp_MOST_eq:
+ "f \<in> perms \<Longrightarrow> MOST x. f x = x"
+ by (simp add: perms_def) (metis MOST_iff_finiteNeg)
+
+lemma id_perms [simp]:
+ "id \<in> perms"
+ "(\<lambda>x. x) \<in> perms"
+ by (auto simp: perms_def bij_def)
+
+lemma perms_comp [simp]:
+ assumes f: "f \<in> perms" and g: "g \<in> perms"
+ shows "(f \<circ> g) \<in> perms"
+ apply (intro permsI bij_comp)
+ apply (rule perms_imp_bij [OF g])
+ apply (rule perms_imp_bij [OF f])
+ apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
+ apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
+ by simp
+
+lemma perms_inv:
+ assumes f: "f \<in> perms"
+ shows "inv f \<in> perms"
+ apply (rule permsI)
+ apply (rule bij_imp_bij_inv)
+ apply (rule perms_imp_bij [OF f])
+ apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
+ apply (erule subst, rule inv_f_f)
+ apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
+ done
+
+lemma bij_Rep_perm: "bij (Rep_perm p)"
+ using Rep_perm [of p] unfolding perms_def by simp
+
+instantiation perm :: (type) group_add
+begin
+
+definition "0 = Abs_perm id"
+definition "- p = Abs_perm (inv (Rep_perm p))"
+definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
+definition "(p1::'a perm) - p2 = p1 + - p2"
+
+lemma Rep_perm_0: "Rep_perm 0 = id"
+ unfolding zero_perm_def by (simp add: Abs_perm_inverse)
+
+lemma Rep_perm_add:
+ "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"
+ unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
+
+lemma Rep_perm_uminus:
+ "Rep_perm (- p) = inv (Rep_perm p)"
+ unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
+
+instance
+ apply standard
+ unfolding Rep_perm_inject [symmetric]
+ unfolding minus_perm_def
+ unfolding Rep_perm_add
+ unfolding Rep_perm_uminus
+ unfolding Rep_perm_0
+ apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+ done
+
+end
+
+lemmas Rep_perm_simps =
+ Rep_perm_0
+ Rep_perm_add
+ Rep_perm_uminus
+
+
+section \<open>Permutation Types\<close>
+
+text \<open>We want to be able to apply permutations to arbitrary types. To
+this end we introduce a constant \<open>PERMUTE\<close> together with
+convenient infix syntax.\<close>
+
+consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr \<open>\<bullet>\<close> 75)
+
+text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
+appliciation of permutations.\<close>
+locale permute =
+ fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
+ assumes permute_zero [simp]: "permute 0 x = x"
+ and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
+begin
+
+adhoc_overloading
+ PERMUTE permute
+
+end
+
+text \<open>Permuting atoms.\<close>
+definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "permute_atom p a = (Rep_perm p) a"
+
+adhoc_overloading
+ PERMUTE permute_atom
+
+interpretation atom_permute: permute permute_atom
+ by standard (simp_all add: permute_atom_def Rep_perm_simps)
+
+text \<open>Permuting permutations.\<close>
+definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
+ "permute_perm p q = p + q - p"
+
+adhoc_overloading
+ PERMUTE permute_perm
+
+interpretation perm_permute: permute permute_perm
+ apply standard
+ unfolding permute_perm_def
+ apply simp
+ apply (simp only: diff_conv_add_uminus minus_add add.assoc)
+ done
+
+text \<open>Permuting functions.\<close>
+locale fun_permute =
+ dom: permute perm1 + ran: permute perm2
+ for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
+ and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
+begin
+
+adhoc_overloading
+ PERMUTE perm1 perm2
+
+definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
+ "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
+
+adhoc_overloading
+ PERMUTE permute_fun
+
+end
+
+sublocale fun_permute \<subseteq> permute permute_fun
+ by (unfold_locales, auto simp: permute_fun_def)
+ (metis dom.permute_plus minus_add)
+
+lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0"
+ unfolding permute_atom_def
+ by (metis Rep_perm_0 id_apply zero_perm_def)
+
+interpretation atom_fun_permute: fun_permute permute_atom permute_atom
+ by (unfold_locales)
+
+adhoc_overloading
+ PERMUTE atom_fun_permute.permute_fun
+
+lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
+ unfolding atom_fun_permute.permute_fun_def
+ unfolding permute_atom_def
+ by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)
+
+end
--- a/src/HOL/Examples/Adhoc_Overloading_Examples.thy Sun Jan 26 22:45:57 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(* Title: HOL/Examples/Adhoc_Overloading_Examples.thy
- Author: Christian Sternagel
-*)
-
-section \<open>Ad Hoc Overloading\<close>
-
-theory Adhoc_Overloading_Examples
-imports
- Main
- "HOL-Library.Infinite_Set"
- "HOL-Library.Adhoc_Overloading"
-begin
-
-text \<open>Adhoc overloading allows to overload a constant depending on
-its type. Typically this involves to introduce an uninterpreted
-constant (used for input and output) and then add some variants (used
-internally).\<close>
-
-subsection \<open>Plain Ad Hoc Overloading\<close>
-
-text \<open>Consider the type of first-order terms.\<close>
-datatype ('a, 'b) "term" =
- Var 'b |
- Fun 'a "('a, 'b) term list"
-
-text \<open>The set of variables of a term might be computed as follows.\<close>
-fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
- "term_vars (Var x) = {x}" |
- "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
-
-text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
-rewrite systems (i.e., sets of rules), the set of variables makes
-sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
-
-consts vars :: "'a \<Rightarrow> 'b set"
-
-text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
-adhoc_overloading
- vars term_vars
-
-value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
-
-fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
- "rule_vars (l, r) = vars l \<union> vars r"
-
-adhoc_overloading
- vars rule_vars
-
-value [nbe] "vars (Var 1, Var 0)"
-
-definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
- "trs_vars R = \<Union>(rule_vars ` R)"
-
-adhoc_overloading
- vars trs_vars
-
-value [nbe] "vars {(Var 1, Var 0)}"
-
-text \<open>Sometimes it is necessary to add explicit type constraints
-before a variant can be determined.\<close>
-(*value "vars R" (*has multiple instances*)*)
-value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
-
-text \<open>It is also possible to remove variants.\<close>
-no_adhoc_overloading
- vars term_vars rule_vars
-
-(*value "vars (Var 1)" (*does not have an instance*)*)
-
-text \<open>As stated earlier, the overloaded constant is only used for
-input and output. Internally, always a variant is used, as can be
-observed by the configuration option \<open>show_variants\<close>.\<close>
-
-adhoc_overloading
- vars term_vars
-
-declare [[show_variants]]
-
-term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
-
-
-subsection \<open>Adhoc Overloading inside Locales\<close>
-
-text \<open>As example we use permutations that are parametrized over an
-atom type \<^typ>\<open>'a\<close>.\<close>
-
-definition perms :: "('a \<Rightarrow> 'a) set" where
- "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
-
-typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
- by standard (auto simp: perms_def)
-
-text \<open>First we need some auxiliary lemmas.\<close>
-lemma permsI [Pure.intro]:
- assumes "bij f" and "MOST x. f x = x"
- shows "f \<in> perms"
- using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
-
-lemma perms_imp_bij:
- "f \<in> perms \<Longrightarrow> bij f"
- by (simp add: perms_def)
-
-lemma perms_imp_MOST_eq:
- "f \<in> perms \<Longrightarrow> MOST x. f x = x"
- by (simp add: perms_def) (metis MOST_iff_finiteNeg)
-
-lemma id_perms [simp]:
- "id \<in> perms"
- "(\<lambda>x. x) \<in> perms"
- by (auto simp: perms_def bij_def)
-
-lemma perms_comp [simp]:
- assumes f: "f \<in> perms" and g: "g \<in> perms"
- shows "(f \<circ> g) \<in> perms"
- apply (intro permsI bij_comp)
- apply (rule perms_imp_bij [OF g])
- apply (rule perms_imp_bij [OF f])
- apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
- apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
- by simp
-
-lemma perms_inv:
- assumes f: "f \<in> perms"
- shows "inv f \<in> perms"
- apply (rule permsI)
- apply (rule bij_imp_bij_inv)
- apply (rule perms_imp_bij [OF f])
- apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
- apply (erule subst, rule inv_f_f)
- apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
- done
-
-lemma bij_Rep_perm: "bij (Rep_perm p)"
- using Rep_perm [of p] unfolding perms_def by simp
-
-instantiation perm :: (type) group_add
-begin
-
-definition "0 = Abs_perm id"
-definition "- p = Abs_perm (inv (Rep_perm p))"
-definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
-definition "(p1::'a perm) - p2 = p1 + - p2"
-
-lemma Rep_perm_0: "Rep_perm 0 = id"
- unfolding zero_perm_def by (simp add: Abs_perm_inverse)
-
-lemma Rep_perm_add:
- "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"
- unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
-
-lemma Rep_perm_uminus:
- "Rep_perm (- p) = inv (Rep_perm p)"
- unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
-
-instance
- apply standard
- unfolding Rep_perm_inject [symmetric]
- unfolding minus_perm_def
- unfolding Rep_perm_add
- unfolding Rep_perm_uminus
- unfolding Rep_perm_0
- apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
- done
-
-end
-
-lemmas Rep_perm_simps =
- Rep_perm_0
- Rep_perm_add
- Rep_perm_uminus
-
-
-section \<open>Permutation Types\<close>
-
-text \<open>We want to be able to apply permutations to arbitrary types. To
-this end we introduce a constant \<open>PERMUTE\<close> together with
-convenient infix syntax.\<close>
-
-consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr \<open>\<bullet>\<close> 75)
-
-text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
-appliciation of permutations.\<close>
-locale permute =
- fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes permute_zero [simp]: "permute 0 x = x"
- and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
-begin
-
-adhoc_overloading
- PERMUTE permute
-
-end
-
-text \<open>Permuting atoms.\<close>
-definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
- "permute_atom p a = (Rep_perm p) a"
-
-adhoc_overloading
- PERMUTE permute_atom
-
-interpretation atom_permute: permute permute_atom
- by standard (simp_all add: permute_atom_def Rep_perm_simps)
-
-text \<open>Permuting permutations.\<close>
-definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
- "permute_perm p q = p + q - p"
-
-adhoc_overloading
- PERMUTE permute_perm
-
-interpretation perm_permute: permute permute_perm
- apply standard
- unfolding permute_perm_def
- apply simp
- apply (simp only: diff_conv_add_uminus minus_add add.assoc)
- done
-
-text \<open>Permuting functions.\<close>
-locale fun_permute =
- dom: permute perm1 + ran: permute perm2
- for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
- and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
-begin
-
-adhoc_overloading
- PERMUTE perm1 perm2
-
-definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
- "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
-
-adhoc_overloading
- PERMUTE permute_fun
-
-end
-
-sublocale fun_permute \<subseteq> permute permute_fun
- by (unfold_locales, auto simp: permute_fun_def)
- (metis dom.permute_plus minus_add)
-
-lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0"
- unfolding permute_atom_def
- by (metis Rep_perm_0 id_apply zero_perm_def)
-
-interpretation atom_fun_permute: fun_permute permute_atom permute_atom
- by (unfold_locales)
-
-adhoc_overloading
- PERMUTE atom_fun_permute.permute_fun
-
-lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
- unfolding atom_fun_permute.permute_fun_def
- unfolding permute_atom_def
- by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)
-
-end
-
--- a/src/HOL/Library/Adhoc_Overloading.thy Sun Jan 26 22:45:57 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: HOL/Library/Adhoc_Overloading.thy
- Author: Alexander Krauss, TU Muenchen
- Author: Christian Sternagel, University of Innsbruck
-*)
-
-section \<open>Adhoc overloading of constants based on their types\<close>
-
-theory Adhoc_Overloading
- imports Main
- keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
-begin
-
-ML_file \<open>adhoc_overloading.ML\<close>
-
-end
--- a/src/HOL/Library/Library.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/HOL/Library/Library.thy Mon Jan 27 12:13:37 2025 +0100
@@ -2,7 +2,6 @@
theory Library
imports
AList
- Adhoc_Overloading
BNF_Axiomatization
BNF_Corec
Bourbaki_Witt_Fixpoint
--- a/src/HOL/Library/Monad_Syntax.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Mon Jan 27 12:13:37 2025 +0100
@@ -6,7 +6,7 @@
section \<open>Monad notation for arbitrary types\<close>
theory Monad_Syntax
- imports Adhoc_Overloading
+ imports Main
begin
text \<open>
--- a/src/HOL/Library/adhoc_overloading.ML Sun Jan 26 22:45:57 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,247 +0,0 @@
-(* Author: Alexander Krauss, TU Muenchen
- Author: Christian Sternagel, University of Innsbruck
-
-Adhoc overloading of constants based on their types.
-*)
-
-signature ADHOC_OVERLOADING =
-sig
- val is_overloaded: Proof.context -> string -> bool
- val generic_add_overloaded: string -> Context.generic -> Context.generic
- val generic_remove_overloaded: string -> Context.generic -> Context.generic
- val generic_add_variant: string -> term -> Context.generic -> Context.generic
- (*If the list of variants is empty at the end of "generic_remove_variant", then
- "generic_remove_overloaded" is called implicitly.*)
- val generic_remove_variant: string -> term -> Context.generic -> Context.generic
- val show_variants: bool Config.T
-end
-
-structure Adhoc_Overloading: ADHOC_OVERLOADING =
-struct
-
-val show_variants = Attrib.setup_config_bool \<^binding>\<open>show_variants\<close> (K false);
-
-
-(* errors *)
-
-fun err_duplicate_variant oconst =
- error ("Duplicate variant of " ^ quote oconst);
-
-fun err_not_a_variant oconst =
- error ("Not a variant of " ^ quote oconst);
-
-fun err_not_overloaded oconst =
- error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
-
-fun err_unresolved_overloading ctxt0 (c, T) t instances =
- let
- val ctxt = Config.put show_variants true ctxt0
- val const_space = Proof_Context.const_space ctxt
- val prt_const =
- Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1,
- Pretty.quote (Syntax.pretty_typ ctxt T)]
- in
- error (Pretty.string_of (Pretty.chunks [
- Pretty.block [
- Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1,
- prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1,
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]],
- Pretty.block (
- (if null instances then [Pretty.str "no instances"]
- else Pretty.fbreaks (
- Pretty.str "multiple instances:" ::
- map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))]))
- end;
-
-
-(* generic data *)
-
-fun variants_eq ((v1, T1), (v2, T2)) =
- Term.aconv_untyped (v1, v2) andalso T1 = T2;
-
-structure Overload_Data = Generic_Data
-(
- type T =
- {variants : (term * typ) list Symtab.table,
- oconsts : string Termtab.table};
- val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
-
- fun merge
- ({variants = vtab1, oconsts = otab1},
- {variants = vtab2, oconsts = otab2}) : T =
- let
- fun merge_oconsts _ (oconst1, oconst2) =
- if oconst1 = oconst2 then oconst1
- else err_duplicate_variant oconst1;
- in
- {variants = Symtab.merge_list variants_eq (vtab1, vtab2),
- oconsts = Termtab.join merge_oconsts (otab1, otab2)}
- end;
-);
-
-fun map_tables f g =
- Overload_Data.map (fn {variants = vtab, oconsts = otab} =>
- {variants = f vtab, oconsts = g otab});
-
-val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof;
-val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof;
-val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof;
-
-fun generic_add_overloaded oconst context =
- if is_overloaded (Context.proof_of context) oconst then context
- else map_tables (Symtab.update (oconst, [])) I context;
-
-fun generic_remove_overloaded oconst context =
- let
- fun remove_oconst_and_variants context oconst =
- let
- val remove_variants =
- (case get_variants (Context.proof_of context) oconst of
- NONE => I
- | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs);
- in map_tables (Symtab.delete_safe oconst) remove_variants context end;
- in
- if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst
- else err_not_overloaded oconst
- end;
-
-local
- fun generic_variant add oconst t context =
- let
- val ctxt = Context.proof_of context;
- val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst;
- val T = t |> fastype_of;
- val t' = Term.map_types (K dummyT) t;
- in
- if add then
- let
- val _ =
- (case get_overloaded ctxt t' of
- NONE => ()
- | SOME oconst' => err_duplicate_variant oconst');
- in
- map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context
- end
- else
- let
- val _ =
- if member variants_eq (the (get_variants ctxt oconst)) (t', T) then ()
- else err_not_a_variant oconst;
- in
- map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
- (Termtab.delete_safe t') context
- |> (fn context =>
- (case get_variants (Context.proof_of context) oconst of
- SOME [] => generic_remove_overloaded oconst context
- | _ => context))
- end
- end;
-in
- val generic_add_variant = generic_variant true;
- val generic_remove_variant = generic_variant false;
-end;
-
-
-(* check / uncheck *)
-
-fun unifiable_with thy T1 T2 =
- let
- val maxidx1 = Term.maxidx_of_typ T1;
- val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
- val maxidx2 = Term.maxidx_typ T2' maxidx1;
- in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
-
-fun get_candidates ctxt (c, T) =
- get_variants ctxt c
- |> Option.map (map_filter (fn (t, T') =>
- if unifiable_with (Proof_Context.theory_of ctxt) T T'
- (*keep the type constraint for the type-inference check phase*)
- then SOME (Type.constraint T t)
- else NONE));
-
-fun insert_variants ctxt t (oconst as Const (c, T)) =
- (case get_candidates ctxt (c, T) of
- SOME [] => err_unresolved_overloading ctxt (c, T) t []
- | SOME [variant] => variant
- | _ => oconst)
- | insert_variants _ _ oconst = oconst;
-
-fun insert_overloaded ctxt =
- let
- fun proc t =
- Term.map_types (K dummyT) t
- |> get_overloaded ctxt
- |> Option.map (Const o rpair (Term.type_of t));
- in
- Pattern.rewrite_term_yoyo (Proof_Context.theory_of ctxt) [] [proc]
- end;
-
-fun check ctxt =
- map (fn t => Term.map_aterms (insert_variants ctxt t) t);
-
-fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts
- else map (insert_overloaded ctxt) ts;
-
-fun reject_unresolved ctxt =
- let
- val the_candidates = the o get_candidates ctxt;
- fun check_unresolved t =
- (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
- [] => t
- | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
- in map check_unresolved end;
-
-
-(* setup *)
-
-val _ = Context.>>
- (Syntax_Phases.term_check 0 "adhoc_overloading" check
- #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
- #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck);
-
-
-(* commands *)
-
-fun generic_adhoc_overloading_cmd add =
- if add then
- fold (fn (oconst, ts) =>
- generic_add_overloaded oconst
- #> fold (generic_add_variant oconst) ts)
- else
- fold (fn (oconst, ts) =>
- fold (generic_remove_variant oconst) ts);
-
-fun adhoc_overloading_cmd' add args phi =
- let val args' = args
- |> map (apsnd (map_filter (fn t =>
- let val t' = Morphism.term phi t;
- in if Term.aconv_untyped (t, t') then SOME t' else NONE end)));
- in generic_adhoc_overloading_cmd add args' end;
-
-fun adhoc_overloading_cmd add raw_args lthy =
- let
- fun const_name ctxt =
- dest_Const_name o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *)
- fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
- val args =
- raw_args
- |> map (apfst (const_name lthy))
- |> map (apsnd (map (read_term lthy)));
- in
- Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
- (adhoc_overloading_cmd' add args) lthy
- end;
-
-val _ =
- Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close>
- "add adhoc overloading for constants / fixed variables"
- (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
-
-val _ =
- Outer_Syntax.local_theory \<^command_keyword>\<open>no_adhoc_overloading\<close>
- "delete adhoc overloading for constants / fixed variables"
- (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
-
-end;
-
--- a/src/HOL/ROOT Sun Jan 26 22:45:57 2025 +0100
+++ b/src/HOL/ROOT Mon Jan 27 12:13:37 2025 +0100
@@ -22,7 +22,7 @@
sessions
"HOL-Computational_Algebra"
theories
- Adhoc_Overloading_Examples
+ Adhoc_Overloading
Ackermann
Cantor
Coherent
--- a/src/Pure/Pure.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Pure/Pure.thy Mon Jan 27 12:13:37 2025 +0100
@@ -96,6 +96,7 @@
and "realizers" :: thy_decl
and "realizability" :: thy_decl
and "extract_type" "extract" :: thy_decl
+ and "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
abbrevs "\\tag" = "\<^marker>\<open>tag \<close>"
@@ -1416,6 +1417,27 @@
in end\<close>
+subsubsection \<open>Adhoc overloading\<close>
+
+ML \<open>
+local
+
+val _ =
+ Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close>
+ "add adhoc overloading for constants / fixed variables"
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+ >> Adhoc_Overloading.adhoc_overloading_cmd true);
+
+val _ =
+ Outer_Syntax.local_theory \<^command_keyword>\<open>no_adhoc_overloading\<close>
+ "delete adhoc overloading for constants / fixed variables"
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+ >> Adhoc_Overloading.adhoc_overloading_cmd false);
+
+in end
+\<close>
+
+
subsubsection \<open>Find consts and theorems\<close>
ML \<open>
--- a/src/Pure/ROOT.ML Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Pure/ROOT.ML Mon Jan 27 12:13:37 2025 +0100
@@ -365,6 +365,7 @@
ML_file "Tools/rule_insts.ML";
ML_file "Tools/thy_deps.ML";
ML_file "Tools/class_deps.ML";
+ML_file "Tools/adhoc_overloading.ML";
ML_file "Tools/find_theorems.ML";
ML_file "Tools/find_consts.ML";
ML_file "Tools/simplifier_trace.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/adhoc_overloading.ML Mon Jan 27 12:13:37 2025 +0100
@@ -0,0 +1,239 @@
+(* Title: Pure/Tools/adhoc_overloading.ML
+ Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
+
+Adhoc overloading of constants based on their types.
+*)
+
+signature ADHOC_OVERLOADING =
+sig
+ val show_variants: bool Config.T
+ val is_overloaded: Proof.context -> string -> bool
+ val generic_add_overloaded: string -> Context.generic -> Context.generic
+ val generic_remove_overloaded: string -> Context.generic -> Context.generic
+ val generic_add_variant: string -> term -> Context.generic -> Context.generic
+ (*If the list of variants is empty at the end of "generic_remove_variant", then
+ "generic_remove_overloaded" is called implicitly.*)
+ val generic_remove_variant: string -> term -> Context.generic -> Context.generic
+ val adhoc_overloading_cmd: bool -> (string * string list) list -> local_theory -> local_theory
+end
+
+structure Adhoc_Overloading: ADHOC_OVERLOADING =
+struct
+
+val show_variants = Attrib.setup_config_bool \<^binding>\<open>show_variants\<close> (K false);
+
+
+(* errors *)
+
+fun err_duplicate_variant oconst =
+ error ("Duplicate variant of " ^ quote oconst);
+
+fun err_not_a_variant oconst =
+ error ("Not a variant of " ^ quote oconst);
+
+fun err_not_overloaded oconst =
+ error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
+
+fun err_unresolved_overloading ctxt0 (c, T) t instances =
+ let
+ val ctxt = Config.put show_variants true ctxt0
+ val const_space = Proof_Context.const_space ctxt
+ val prt_const =
+ Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ ctxt T)]
+ in
+ error (Pretty.string_of (Pretty.chunks [
+ Pretty.block [
+ Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1,
+ prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1,
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]],
+ Pretty.block (
+ (if null instances then [Pretty.str "no instances"]
+ else Pretty.fbreaks (
+ Pretty.str "multiple instances:" ::
+ map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))]))
+ end;
+
+
+(* generic data *)
+
+fun variants_eq ((v1, T1), (v2, T2)) =
+ Term.aconv_untyped (v1, v2) andalso T1 = T2;
+
+structure Overload_Data = Generic_Data
+(
+ type T =
+ {variants : (term * typ) list Symtab.table,
+ oconsts : string Termtab.table};
+ val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
+
+ fun merge
+ ({variants = vtab1, oconsts = otab1},
+ {variants = vtab2, oconsts = otab2}) : T =
+ let
+ fun merge_oconsts _ (oconst1, oconst2) =
+ if oconst1 = oconst2 then oconst1
+ else err_duplicate_variant oconst1;
+ in
+ {variants = Symtab.merge_list variants_eq (vtab1, vtab2),
+ oconsts = Termtab.join merge_oconsts (otab1, otab2)}
+ end;
+);
+
+fun map_tables f g =
+ Overload_Data.map (fn {variants = vtab, oconsts = otab} =>
+ {variants = f vtab, oconsts = g otab});
+
+val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof;
+val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof;
+val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof;
+
+fun generic_add_overloaded oconst context =
+ if is_overloaded (Context.proof_of context) oconst then context
+ else map_tables (Symtab.update (oconst, [])) I context;
+
+fun generic_remove_overloaded oconst context =
+ let
+ fun remove_oconst_and_variants context oconst =
+ let
+ val remove_variants =
+ (case get_variants (Context.proof_of context) oconst of
+ NONE => I
+ | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs);
+ in map_tables (Symtab.delete_safe oconst) remove_variants context end;
+ in
+ if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst
+ else err_not_overloaded oconst
+ end;
+
+local
+ fun generic_variant add oconst t context =
+ let
+ val ctxt = Context.proof_of context;
+ val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst;
+ val T = t |> fastype_of;
+ val t' = Term.map_types (K dummyT) t;
+ in
+ if add then
+ let
+ val _ =
+ (case get_overloaded ctxt t' of
+ NONE => ()
+ | SOME oconst' => err_duplicate_variant oconst');
+ in
+ map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context
+ end
+ else
+ let
+ val _ =
+ if member variants_eq (the (get_variants ctxt oconst)) (t', T) then ()
+ else err_not_a_variant oconst;
+ in
+ map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
+ (Termtab.delete_safe t') context
+ |> (fn context =>
+ (case get_variants (Context.proof_of context) oconst of
+ SOME [] => generic_remove_overloaded oconst context
+ | _ => context))
+ end
+ end;
+in
+ val generic_add_variant = generic_variant true;
+ val generic_remove_variant = generic_variant false;
+end;
+
+
+(* check / uncheck *)
+
+fun unifiable_with thy T1 T2 =
+ let
+ val maxidx1 = Term.maxidx_of_typ T1;
+ val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
+ val maxidx2 = Term.maxidx_typ T2' maxidx1;
+ in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
+
+fun get_candidates ctxt (c, T) =
+ get_variants ctxt c
+ |> Option.map (map_filter (fn (t, T') =>
+ if unifiable_with (Proof_Context.theory_of ctxt) T T'
+ (*keep the type constraint for the type-inference check phase*)
+ then SOME (Type.constraint T t)
+ else NONE));
+
+fun insert_variants ctxt t (oconst as Const (c, T)) =
+ (case get_candidates ctxt (c, T) of
+ SOME [] => err_unresolved_overloading ctxt (c, T) t []
+ | SOME [variant] => variant
+ | _ => oconst)
+ | insert_variants _ _ oconst = oconst;
+
+fun insert_overloaded ctxt =
+ let
+ fun proc t =
+ Term.map_types (K dummyT) t
+ |> get_overloaded ctxt
+ |> Option.map (Const o rpair (Term.type_of t));
+ in
+ Pattern.rewrite_term_yoyo (Proof_Context.theory_of ctxt) [] [proc]
+ end;
+
+fun check ctxt =
+ map (fn t => Term.map_aterms (insert_variants ctxt t) t);
+
+fun uncheck ctxt ts =
+ if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts
+ else map (insert_overloaded ctxt) ts;
+
+fun reject_unresolved ctxt =
+ let
+ val the_candidates = the o get_candidates ctxt;
+ fun check_unresolved t =
+ (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
+ [] => t
+ | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
+ in map check_unresolved end;
+
+
+(* setup *)
+
+val _ = Context.>>
+ (Syntax_Phases.term_check 0 "adhoc_overloading" check
+ #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
+ #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck);
+
+
+(* commands *)
+
+fun generic_adhoc_overloading_cmd add =
+ if add then
+ fold (fn (oconst, ts) =>
+ generic_add_overloaded oconst
+ #> fold (generic_add_variant oconst) ts)
+ else
+ fold (fn (oconst, ts) =>
+ fold (generic_remove_variant oconst) ts);
+
+fun adhoc_overloading_cmd' add args phi =
+ let val args' = args
+ |> map (apsnd (map_filter (fn t =>
+ let val t' = Morphism.term phi t;
+ in if Term.aconv_untyped (t, t') then SOME t' else NONE end)));
+ in generic_adhoc_overloading_cmd add args' end;
+
+fun adhoc_overloading_cmd add raw_args lthy =
+ let
+ fun const_name ctxt =
+ dest_Const_name o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *)
+ fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
+ val args =
+ raw_args
+ |> map (apfst (const_name lthy))
+ |> map (apsnd (map (read_term lthy)));
+ in
+ Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
+ (adhoc_overloading_cmd' add args) lthy
+ end;
+
+end;
+