Dear Makarius,
actually even more is missing, since I was not able to properly use "hg
export" (I am used to "hg bundle" which "exports" *all* changesets that
are only local, whereas for "hg export" I have to give all revisions
that should be exported explicitly). Sorry for that. Please find
attached a file containing all my changes.
cheers
chris
On 08/06/2013 03:34 AM, Makarius wrote:
On Fri, 2 Aug 2013, Christian Sternagel wrote:
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
isar-ref manual? E.g. somewhere here
http://isabelle.in.tum.de/repos/isabelle/annotate/122416054a9c/src/Doc/IsarRef/HOL_Specific.thy
I gave both a try. Please find the resulting changesets (via "hg
export") attached (I also squeezed in some unrelated changes:
spell-checking, tuning of error messages. I hope that is okay).
The tuning etc. is fine (it looks like done with care).
What is missing in the commit is your new file
src/HOL/ex/Adhoc_Overloading_Examples.thy
Makarius
# HG changeset patch
# User Christian Sternagel
# Date 1375413062 -32400
# Fri Aug 02 12:11:02 2013 +0900
# Node ID 8173d8eb92c59711abede67ca2c035ed3e02beb6
# Parent cc425a7dc9adbcc95b7c6ed124466384e087275e
tuned formatting of error message
diff --git a/src/Tools/adhoc_overloading.ML b/src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML
+++ b/src/Tools/adhoc_overloading.ML
@@ -41,7 +41,7 @@
"in term " ::
quote (Syntax.string_of_term ctxt' t) ::
(if null instances then "no instances" else "multiple instances:") ::
- map (Syntax.string_of_term ctxt') instances)
+ map (Markup.markup Markup.item o Syntax.string_of_term ctxt') instances)
|> error
end;
# HG changeset patch
# User Christian Sternagel
# Date 1375425679 -32400
# Fri Aug 02 15:41:19 2013 +0900
# Node ID f3ab98f28d70c18a919b23fbd6a5daffba212251
# Parent 8173d8eb92c59711abede67ca2c035ed3e02beb6
use uniform spelling of "adhoc"
diff --git a/src/Tools/Adhoc_Overloading.thy b/src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy
+++ b/src/Tools/Adhoc_Overloading.thy
@@ -2,7 +2,7 @@
Author: Christian Sternagel, University of Innsbruck
*)
-header {* Ad-hoc overloading of constants based on their types *}
+header {* Adhoc overloading of constants based on their types *}
theory Adhoc_Overloading
imports Pure
diff --git a/src/Tools/adhoc_overloading.ML b/src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML
+++ b/src/Tools/adhoc_overloading.ML
@@ -1,7 +1,7 @@
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
-Ad-hoc overloading of constants based on their types.
+Adhoc overloading of constants based on their types.
*)
signature ADHOC_OVERLOADING =
@@ -227,12 +227,12 @@
val _ =
Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
- "add ad-hoc overloading for constants / fixed variables"
+ "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_spec "no_adhoc_overloading"}
- "add ad-hoc overloading for constants / fixed variables"
+ "add adhoc overloading for constants / fixed variables"
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
end;
# HG changeset patch
# User Christian Sternagel
# Date 1375425721 -32400
# Fri Aug 02 15:42:01 2013 +0900
# Node ID 5e53d4373e38de46b1f0358aeca06ecd8fbb4bdb
# Parent f3ab98f28d70c18a919b23fbd6a5daffba212251
added examples of adhoc overloading
diff --git a/src/HOL/ex/Adhoc_Overloading_Examples.thy b/src/HOL/ex/Adhoc_Overloading_Examples.thy
new file mode 100644
--- /dev/null
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy
@@ -0,0 +1,250 @@
+(* Title: HOL/ex/Adhoc_Overloading_Examples.thy
+ Author: Christian Sternagel
+*)
+
+header {* Ad Hoc Overloading *}
+
+theory Adhoc_Overloading_Examples
+imports
+ Main
+ "~~/src/Tools/Adhoc_Overloading"
+ "~~/src/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 \<Rightarrow> 'b set" where
+ "term_vars (Var x) = {x}" |
+ "term_vars (Fun f ts) = \<Union>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 @{text vars}.*}
+
+consts vars :: "'a \<Rightarrow> 'b set"
+
+text {*Which is then overloaded with variants for terms, rules, and TRSs.*}
+adhoc_overloading
+ vars term_vars
+
+value "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 "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 "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 \<times> ('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 @{text 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 \<Rightarrow> 'a) set" where
+ "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
+
+typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
+ by (default) (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 \<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)
+ by (rule bij_is_inj [OF perms_imp_bij [OF f]])
+
+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 default
+ unfolding Rep_perm_inject [symmetric]
+ unfolding minus_perm_def
+ unfolding Rep_perm_add
+ unfolding Rep_perm_uminus
+ unfolding Rep_perm_0
+ by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+
+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 @{text PERMUTE} together with
+convenient infix syntax.*}
+
+consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
+
+text {*Then we add a locale for types @{typ 'b} that support
+appliciation of permutations.*}
+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 {*Permuting atoms.*}
+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 (default) (simp add: permute_atom_def Rep_perm_simps)+
+
+text {*Permuting permutations.*}
+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
+ by (default) (simp add: diff_minus minus_add add_assoc permute_perm_def)+
+
+text {*Permuting functions.*}
+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
+
# HG changeset patch
# User Christian Sternagel
# Date 1375425767 -32400
# Fri Aug 02 15:42:47 2013 +0900
# Node ID a854ff7d191ae0735664632516e3274a1e7bd2f7
# Parent 5e53d4373e38de46b1f0358aeca06ecd8fbb4bdb
some documentation for adhoc overloading;
spell-checked;
diff --git a/src/Doc/IsarRef/HOL_Specific.thy b/src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy
+++ b/src/Doc/IsarRef/HOL_Specific.thy
@@ -1,5 +1,5 @@
theory HOL_Specific
-imports Base Main "~~/src/HOL/Library/Old_Recdef"
+imports Base Main "~~/src/HOL/Library/Old_Recdef" "~~/src/Tools/Adhoc_Overloading"
begin
chapter {* Higher-Order Logic *}
@@ -588,7 +588,7 @@
There are no fixed syntactic restrictions on the body of the
function, but the induced functional must be provably monotonic
- wrt.\ the underlying order. The monotonicitity proof is performed
+ wrt.\ the underlying order. The monotonicity proof is performed
internally, and the definition is rejected when it fails. The proof
can be influenced by declaring hints using the
@{attribute (HOL) partial_function_mono} attribute.
@@ -622,7 +622,7 @@
@{const "partial_function_definitions"} appropriately.
\item @{attribute (HOL) partial_function_mono} declares rules for
- use in the internal monononicity proofs of partial function
+ use in the internal monotonicity proofs of partial function
definitions.
\end{description}
@@ -1288,7 +1288,7 @@
"morphisms"} specification provides alternative names. @{command
(HOL) "quotient_type"} requires the user to prove that the relation
is an equivalence relation (predicate @{text equivp}), unless the
- user specifies explicitely @{text partial} in which case the
+ user specifies explicitly @{text partial} in which case the
obligation is @{text part_equivp}. A quotient defined with @{text
partial} is weaker in the sense that less things can be proved
automatically.
@@ -1318,7 +1318,7 @@
and @{method (HOL) "descending"} continues in the same way as
@{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries
to solve the arising regularization, injection and cleaning
- subgoals with the analoguous method @{method (HOL)
+ subgoals with the analogous method @{method (HOL)
"descending_setup"} which leaves the four unsolved subgoals.
\item @{method (HOL) "partiality_descending"} finds the regularized
@@ -1416,6 +1416,46 @@
problem, one should use @{command (HOL) "ax_specification"}.
*}
+section {* Adhoc overloading of constants *}
+
+text {*
+ \begin{tabular}{rcll}
+ @{command_def "adhoc_overloading"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "no_adhoc_overloading"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{attribute_def "show_variants"} & : & @{text "attribute"} & default @{text 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/ex/Adhoc_Overloading_Examples.thy"} and
+ @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
+
+ @{rail "
+ (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
+ (@{syntax nameref} (@{syntax term} + ) + @'and')
+ "}
+
+ \begin{description}
+
+ \item @{command "adhoc_overloading"}~@{text "c v\<^isub>1 ... v\<^isub>n"}
+ associates variants with an existing constant.
+
+ \item @{command "no_adhoc_overloading"} is similar to
+ @{command "adhoc_overloading"}, but removes the specified variants
+ from the present context.
+
+ \item @{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.
+
+ \end{description}
+*}
chapter {* Proof tools *}
@@ -1553,7 +1593,7 @@
equations in the code generator. The option @{text "no_code"}
of the command @{command (HOL) "setup_lifting"} can turn off that
behavior and causes that code certificate theorems generated by
- @{command (HOL) "lift_definition"} are not registred as abstract
+ @{command (HOL) "lift_definition"} are not registered as abstract
code equations.
\item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}
@@ -1607,7 +1647,7 @@
files.
\item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects reflexivity and left-totality. For exampless
+ that a relator respects reflexivity and left-totality. For examples
see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
The property is used in generation of abstraction function equations.
@@ -2009,7 +2049,7 @@
counterexamples using a series of assignments for its free
variables; by default the first subgoal is tested, an other can be
selected explicitly using an optional goal index. Assignments can
- be chosen exhausting the search space upto a given size, or using a
+ be chosen exhausting the search space up to a given size, or using a
fixed number of random assignments in the search space, or exploring
the search space symbolically using narrowing. By default,
quickcheck uses exhaustive testing. A number of configuration
@@ -2373,12 +2413,12 @@
internally.
Constants may be specified by giving them literally, referring to
- all executable contants within a certain theory by giving @{text
+ all executable constants within a certain theory by giving @{text
"name.*"}, or referring to \emph{all} executable constants currently
available by giving @{text "*"}.
By default, for each involved theory one corresponding name space
- module is generated. Alternativly, a module name may be specified
+ module is generated. Alternatively, a module name may be specified
after the @{keyword "module_name"} keyword; then \emph{all} code is
placed in this module.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
