# HG changeset patch # User wenzelm # Date 1737976417 -3600 # Node ID 96afb07075323ffd398d76da74f4c799760b0fc6 # Parent 846293abd12d6223ecbb0e535b62b043640a9068 move theory "HOL-Library.Adhoc_Overloading" to Pure; diff -r 846293abd12d -r 96afb0707532 NEWS --- 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 *** diff -r 846293abd12d -r 96afb0707532 src/Doc/Isar_Ref/HOL_Specific.thy --- 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 @@ \ -section \Adhoc overloading of constants\ - -text \ - \begin{tabular}{rcll} - @{command_def "adhoc_overloading"} & : & \local_theory \ local_theory\ \\ - @{command_def "no_adhoc_overloading"} & : & \local_theory \ local_theory\ \\ - @{attribute_def "show_variants"} & : & \attribute\ & default \false\ \\ - \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>\~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy\ and - \<^file>\~~/src/HOL/Library/Monad_Syntax.thy\. - - \<^rail>\ - (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) - (@{syntax name} (@{syntax term} + ) + @'and') - \ - - \<^descr> @{command "adhoc_overloading"}~\c v\<^sub>1 ... v\<^sub>n\ 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. -\ - - section \Definition by specification \label{sec:hol-specification}\ text \ diff -r 846293abd12d -r 96afb0707532 src/Doc/Isar_Ref/Spec.thy --- 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 \Overloaded constant abbreviations: adhoc overloading\ + +text \ + \begin{tabular}{rcll} + @{command_def "adhoc_overloading"} & : & \local_theory \ local_theory\ \\ + @{command_def "no_adhoc_overloading"} & : & \local_theory \ local_theory\ \\ + @{attribute_def "show_variants"} & : & \attribute\ & default \false\ \\ + \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>\~~/src/HOL/Examples/Adhoc_Overloading.thy\ and + \<^file>\~~/src/HOL/Library/Monad_Syntax.thy\. + + \<^rail>\ + (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) + (@{syntax name} (@{syntax term} + ) + @'and') + \ + + \<^descr> @{command "adhoc_overloading"}~\c v\<^sub>1 ... v\<^sub>n\ 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. +\ + + section \Incorporating ML code \label{sec:ML}\ text \ diff -r 846293abd12d -r 96afb0707532 src/HOL/Examples/Adhoc_Overloading.thy --- /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 \Ad Hoc Overloading\ + +theory Adhoc_Overloading +imports + Main + "HOL-Library.Infinite_Set" +begin + +text \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).\ + +subsection \Plain Ad Hoc Overloading\ + +text \Consider the type of first-order terms.\ +datatype ('a, 'b) "term" = + Var 'b | + Fun 'a "('a, 'b) term list" + +text \The set of variables of a term might be computed as follows.\ +fun term_vars :: "('a, 'b) term \ 'b set" where + "term_vars (Var x) = {x}" | + "term_vars (Fun f ts) = \(set (map term_vars ts))" + +text \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 \vars\.\ + +consts vars :: "'a \ 'b set" + +text \Which is then overloaded with variants for terms, rules, and TRSs.\ +adhoc_overloading + vars term_vars + +value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" + +fun rule_vars :: "('a, 'b) term \ ('a, 'b) term \ 'b set" where + "rule_vars (l, r) = vars l \ vars r" + +adhoc_overloading + vars rule_vars + +value [nbe] "vars (Var 1, Var 0)" + +definition trs_vars :: "(('a, 'b) term \ ('a, 'b) term) set \ 'b set" where + "trs_vars R = \(rule_vars ` R)" + +adhoc_overloading + vars trs_vars + +value [nbe] "vars {(Var 1, Var 0)}" + +text \Sometimes it is necessary to add explicit type constraints +before a variant can be determined.\ +(*value "vars R" (*has multiple instances*)*) +value "vars (R :: (('a, 'b) term \ ('a, 'b) term) set)" + +text \It is also possible to remove variants.\ +no_adhoc_overloading + vars term_vars rule_vars + +(*value "vars (Var 1)" (*does not have an instance*)*) + +text \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 \show_variants\.\ + +adhoc_overloading + vars term_vars + +declare [[show_variants]] + +term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*) + + +subsection \Adhoc Overloading inside Locales\ + +text \As example we use permutations that are parametrized over an +atom type \<^typ>\'a\.\ + +definition perms :: "('a \ 'a) set" where + "perms = {f. bij f \ finite {x. f x \ x}}" + +typedef 'a perm = "perms :: ('a \ 'a) set" + by standard (auto simp: perms_def) + +text \First we need some auxiliary lemmas.\ +lemma permsI [Pure.intro]: + assumes "bij f" and "MOST x. f x = x" + shows "f \ perms" + using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg) + +lemma perms_imp_bij: + "f \ perms \ bij f" + by (simp add: perms_def) + +lemma perms_imp_MOST_eq: + "f \ perms \ MOST x. f x = x" + by (simp add: perms_def) (metis MOST_iff_finiteNeg) + +lemma id_perms [simp]: + "id \ perms" + "(\x. x) \ perms" + by (auto simp: perms_def bij_def) + +lemma perms_comp [simp]: + assumes f: "f \ perms" and g: "g \ perms" + shows "(f \ g) \ 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 \ perms" + shows "inv f \ 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 \ 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 \ 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 \Permutation Types\ + +text \We want to be able to apply permutations to arbitrary types. To +this end we introduce a constant \PERMUTE\ together with +convenient infix syntax.\ + +consts PERMUTE :: "'a perm \ 'b \ 'b" (infixr \\\ 75) + +text \Then we add a locale for types \<^typ>\'b\ that support +appliciation of permutations.\ +locale permute = + fixes permute :: "'a perm \ 'b \ '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 \Permuting atoms.\ +definition permute_atom :: "'a perm \ 'a \ '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 \Permuting permutations.\ +definition permute_perm :: "'a perm \ 'a perm \ '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 \Permuting functions.\ +locale fun_permute = + dom: permute perm1 + ran: permute perm2 + for perm1 :: "'a perm \ 'b \ 'b" + and perm2 :: "'a perm \ 'c \ 'c" +begin + +adhoc_overloading + PERMUTE perm1 perm2 + +definition permute_fun :: "'a perm \ ('b \ 'c) \ ('b \ 'c)" where + "permute_fun p f = (\x. p \ (f (-p \ x)))" + +adhoc_overloading + PERMUTE permute_fun + +end + +sublocale fun_permute \ permute permute_fun + by (unfold_locales, auto simp: permute_fun_def) + (metis dom.permute_plus minus_add) + +lemma "(Abs_perm id :: nat perm) \ 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) \ 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 diff -r 846293abd12d -r 96afb0707532 src/HOL/Examples/Adhoc_Overloading_Examples.thy --- 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 \Ad Hoc Overloading\ - -theory Adhoc_Overloading_Examples -imports - Main - "HOL-Library.Infinite_Set" - "HOL-Library.Adhoc_Overloading" -begin - -text \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).\ - -subsection \Plain Ad Hoc Overloading\ - -text \Consider the type of first-order terms.\ -datatype ('a, 'b) "term" = - Var 'b | - Fun 'a "('a, 'b) term list" - -text \The set of variables of a term might be computed as follows.\ -fun term_vars :: "('a, 'b) term \ 'b set" where - "term_vars (Var x) = {x}" | - "term_vars (Fun f ts) = \(set (map term_vars ts))" - -text \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 \vars\.\ - -consts vars :: "'a \ 'b set" - -text \Which is then overloaded with variants for terms, rules, and TRSs.\ -adhoc_overloading - vars term_vars - -value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" - -fun rule_vars :: "('a, 'b) term \ ('a, 'b) term \ 'b set" where - "rule_vars (l, r) = vars l \ vars r" - -adhoc_overloading - vars rule_vars - -value [nbe] "vars (Var 1, Var 0)" - -definition trs_vars :: "(('a, 'b) term \ ('a, 'b) term) set \ 'b set" where - "trs_vars R = \(rule_vars ` R)" - -adhoc_overloading - vars trs_vars - -value [nbe] "vars {(Var 1, Var 0)}" - -text \Sometimes it is necessary to add explicit type constraints -before a variant can be determined.\ -(*value "vars R" (*has multiple instances*)*) -value "vars (R :: (('a, 'b) term \ ('a, 'b) term) set)" - -text \It is also possible to remove variants.\ -no_adhoc_overloading - vars term_vars rule_vars - -(*value "vars (Var 1)" (*does not have an instance*)*) - -text \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 \show_variants\.\ - -adhoc_overloading - vars term_vars - -declare [[show_variants]] - -term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*) - - -subsection \Adhoc Overloading inside Locales\ - -text \As example we use permutations that are parametrized over an -atom type \<^typ>\'a\.\ - -definition perms :: "('a \ 'a) set" where - "perms = {f. bij f \ finite {x. f x \ x}}" - -typedef 'a perm = "perms :: ('a \ 'a) set" - by standard (auto simp: perms_def) - -text \First we need some auxiliary lemmas.\ -lemma permsI [Pure.intro]: - assumes "bij f" and "MOST x. f x = x" - shows "f \ perms" - using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg) - -lemma perms_imp_bij: - "f \ perms \ bij f" - by (simp add: perms_def) - -lemma perms_imp_MOST_eq: - "f \ perms \ MOST x. f x = x" - by (simp add: perms_def) (metis MOST_iff_finiteNeg) - -lemma id_perms [simp]: - "id \ perms" - "(\x. x) \ perms" - by (auto simp: perms_def bij_def) - -lemma perms_comp [simp]: - assumes f: "f \ perms" and g: "g \ perms" - shows "(f \ g) \ 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 \ perms" - shows "inv f \ 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 \ 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 \ 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 \Permutation Types\ - -text \We want to be able to apply permutations to arbitrary types. To -this end we introduce a constant \PERMUTE\ together with -convenient infix syntax.\ - -consts PERMUTE :: "'a perm \ 'b \ 'b" (infixr \\\ 75) - -text \Then we add a locale for types \<^typ>\'b\ that support -appliciation of permutations.\ -locale permute = - fixes permute :: "'a perm \ 'b \ '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 \Permuting atoms.\ -definition permute_atom :: "'a perm \ 'a \ '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 \Permuting permutations.\ -definition permute_perm :: "'a perm \ 'a perm \ '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 \Permuting functions.\ -locale fun_permute = - dom: permute perm1 + ran: permute perm2 - for perm1 :: "'a perm \ 'b \ 'b" - and perm2 :: "'a perm \ 'c \ 'c" -begin - -adhoc_overloading - PERMUTE perm1 perm2 - -definition permute_fun :: "'a perm \ ('b \ 'c) \ ('b \ 'c)" where - "permute_fun p f = (\x. p \ (f (-p \ x)))" - -adhoc_overloading - PERMUTE permute_fun - -end - -sublocale fun_permute \ permute permute_fun - by (unfold_locales, auto simp: permute_fun_def) - (metis dom.permute_plus minus_add) - -lemma "(Abs_perm id :: nat perm) \ 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) \ 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 - diff -r 846293abd12d -r 96afb0707532 src/HOL/Library/Adhoc_Overloading.thy --- 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 \Adhoc overloading of constants based on their types\ - -theory Adhoc_Overloading - imports Main - keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl -begin - -ML_file \adhoc_overloading.ML\ - -end diff -r 846293abd12d -r 96afb0707532 src/HOL/Library/Library.thy --- 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 diff -r 846293abd12d -r 96afb0707532 src/HOL/Library/Monad_Syntax.thy --- 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 \Monad notation for arbitrary types\ theory Monad_Syntax - imports Adhoc_Overloading + imports Main begin text \ diff -r 846293abd12d -r 96afb0707532 src/HOL/Library/adhoc_overloading.ML --- 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>\show_variants\ (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>\adhoc_overloading\ - "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>\no_adhoc_overloading\ - "delete adhoc overloading for constants / fixed variables" - (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false); - -end; - diff -r 846293abd12d -r 96afb0707532 src/HOL/ROOT --- 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 diff -r 846293abd12d -r 96afb0707532 src/Pure/Pure.thy --- 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>\tag \" @@ -1416,6 +1417,27 @@ in end\ +subsubsection \Adhoc overloading\ + +ML \ +local + +val _ = + Outer_Syntax.local_theory \<^command_keyword>\adhoc_overloading\ + "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>\no_adhoc_overloading\ + "delete adhoc overloading for constants / fixed variables" + (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) + >> Adhoc_Overloading.adhoc_overloading_cmd false); + +in end +\ + + subsubsection \Find consts and theorems\ ML \ diff -r 846293abd12d -r 96afb0707532 src/Pure/ROOT.ML --- 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"; diff -r 846293abd12d -r 96afb0707532 src/Pure/Tools/adhoc_overloading.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>\show_variants\ (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; +