# HG changeset patch # User haftmann # Date 1469371721 -7200 # Node ID d00db72d86979596e6f4a7ab9fb78a611a731724 # Parent d7c6a3a01b79b637926bdf85e5c749356ff43ee1 more on type class hierarchy diff -r d7c6a3a01b79 -r d00db72d8697 src/Doc/Typeclass_Hierarchy/Setup.thy --- a/src/Doc/Typeclass_Hierarchy/Setup.thy Sun Jul 24 16:48:40 2016 +0200 +++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Sun Jul 24 16:48:41 2016 +0200 @@ -1,5 +1,5 @@ theory Setup -imports Complex_Main "~~/src/HOL/Library/Lattice_Syntax" +imports Complex_Main "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Lattice_Syntax" begin ML_file "../antiquote_setup.ML" @@ -11,6 +11,29 @@ setup \Config.put_global Printer.show_type_emphasis false\ +setup \ +let + fun strip_all t = + if Logic.is_all t + then + case snd (dest_comb t) of Abs (w, T, t') => + strip_all t' |>> cons (w, T) + else ([], t); + fun frugal (w, T as TFree (v, sort)) visited = + if member (op =) visited v + then ((w, dummyT), visited) else ((w, T), v :: visited) + | frugal (w, T) visited = ((w, dummyT), visited); + fun frugal_sorts t = + let + val (vTs, body) = strip_all t + val (vTs', _) = fold_map frugal vTs []; + in Logic.list_all (vTs', map_types (K dummyT) body) end; +in + Term_Style.setup @{binding frugal_sorts} + (Scan.succeed (K frugal_sorts)) +end +\ + declare [[show_sorts]] end diff -r d7c6a3a01b79 -r d00db72d8697 src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy --- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Sun Jul 24 16:48:40 2016 +0200 +++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Sun Jul 24 16:48:41 2016 +0200 @@ -6,7 +6,7 @@ text \ The {Isabelle/HOL} type-class hierarchy entered the stage - in a quite ancient era -- first related \emph{NEWS} entries date + in a quite ancient era -- first related \<^emph>\NEWS\ entries date back to release {Isabelle99-1}. Since then, there have been ongoing modifications and additions, leading to ({Isabelle2016}) more than 180 type-classes. This sheer complexity makes access @@ -79,8 +79,8 @@ types, hence also sharing of notation and names: there is only one plus operation using infix syntax @{text "+"}, only one zero written @{text 0}, and neutrality - (@{thm add_0_left [all, no_vars]} and - @{thm add_0_right [all, no_vars]}) + (@{thm (frugal_sorts) add_0_left [all, no_vars]} and + @{thm (frugal_sorts) add_0_right [all, no_vars]}) is referred to uniformly by names @{fact add_0_left} and @{fact add_0_right}. @@ -128,20 +128,20 @@ section \The hierarchy\ -subsection \Syntactic type classes\ +subsection \Syntactic type classes \label{sec:syntactic-type-class}\ text \ At the top of the hierarchy there are a couple of syntactic type classes, ie. classes with operations but with no axioms, most notably: - \<^item> @{class plus} with @{term [source] "(a::'a::plus) + b"} + \<^item> @{command class} @{class plus} with @{term [source] "(a::'a::plus) + b"} - \<^item> @{class zero} with @{term [source] "0::'a::zero"} + \<^item> @{command class} @{class zero} with @{term [source] "0::'a::zero"} - \<^item> @{class times} with @{term [source] "(a::'a::times) * b"} + \<^item> @{command class} @{class times} with @{term [source] "(a::'a::times) * b"} - \<^item> @{class one} with @{term [source] "1::'a::one"} + \<^item> @{command class} @{class one} with @{term [source] "1::'a::one"} \noindent Before the introduction of the @{command class} statement in Isabelle \cite{Haftmann-Wenzel:2006:classes} it was impossible @@ -173,4 +173,196 @@ not provable without particular type constraints. \ + +subsection \Additive and multiplicative semigroups and monoids\ + +text \ + In common literature, notation for semigroups and monoids + is either multiplicative @{text "(*, 1)"} or additive + @{text "(+, 0)"} with underlying properties isomorphic. + In {Isabelle/HOL}, this is accomplished using the following + abstract setup: + + \<^item> A @{locale semigroup} introduces an abstract binary + associative operation. + + \<^item> A @{locale monoid} is an extension of @{locale semigroup} + with a neutral element. + + \<^item> Both @{locale semigroup} and @{locale monoid} provide + dedicated syntax for their operations @{text "(\<^bold>*, \<^bold>1)"}. + This syntax is not visible on the global theory level + but only for abstract reasoning inside the respective + locale. + + \<^item> Concrete global syntax is added building on existing + syntactic type classes \secref{sec:syntactic-type-class} + using the following classes: + + \<^item> @{command class} @{class semigroup_mult} = @{class times} + + \<^item> @{command class} @{class monoid_mult} = @{class one} + @{class semigroup_mult} + + \<^item> @{command class} @{class semigroup_add} = @{class plus} + + \<^item> @{command class} @{class monoid_add} = @{class zero} + @{class semigroup_add} + + Locales @{locale semigroup} and @{locale monoid} are + interpreted (using @{command sublocale}) into their + corresponding type classes, with prefixes @{text add} + and @{text mult}; hence facts derived in @{locale semigroup} + and @{locale monoid} are propagated simultaneously to + \<^emph>\both\ using a consistent naming policy, ie. + + \<^item> @{fact semigroup.assoc}: @{thm (frugal_sorts) semigroup.assoc [all, no_vars]} + + \<^item> @{fact mult.assoc}: @{thm (frugal_sorts) mult.assoc [all, no_vars]} + + \<^item> @{fact add.assoc}: @{thm (frugal_sorts) add.assoc [all, no_vars]} + + \<^item> @{fact monoid.right_neutral}: @{thm (frugal_sorts) monoid.right_neutral [all, no_vars]} + + \<^item> @{fact mult.right_neutral}: @{thm (frugal_sorts) mult.right_neutral [all, no_vars]} + + \<^item> @{fact add.right_neutral}: @{thm (frugal_sorts) add.right_neutral [all, no_vars]} + + \<^item> Note that the syntax in @{locale semigroup} and @{locale monoid} + is bold; this avoids clashes when writing properties + inside one of these locales in presence of that global + concrete type class syntax. + + \noindent That hierarchy extends in a straightforward manner + to abelian semigroups and commutative monoids\footnote{The + designation \<^emph>\abelian\ is quite standard concerning + (semi)groups, but not for monoids}: + + \<^item> Locales @{locale abel_semigroup} and @{locale comm_monoid} + add commutativity as property. + + \<^item> Concrete syntax emerges through + + \<^item> @{command class} @{class ab_semigroup_add} = @{class semigroup_add} + + \<^item> @{command class} @{class ab_semigroup_mult} = @{class semigroup_mult} + + \<^item> @{command class} @{class comm_monoid_add} = @{class zero} + @{class ab_semigroup_add} + + \<^item> @{command class} @{class comm_monoid_mult} = @{class one} + @{class ab_semigroup_mult} + + and corresponding interpretation of the locales above, yielding + + \<^item> @{fact abel_semigroup.commute}: @{thm (frugal_sorts) abel_semigroup.commute [all, no_vars]} + + \<^item> @{fact mult.commute}: @{thm (frugal_sorts) mult.commute [all, no_vars]} + + \<^item> @{fact add.commute}: @{thm (frugal_sorts) add.commute [all, no_vars]} +\ + +paragraph \Named collection of theorems\ + +text \ + Locale interpretation interacts smoothly with named collections of + theorems as introduced by command @{command named_theorems}. In our + example, rules concerning associativity and commutativity are no + simplification rules by default since they desired orientation may + vary depending on the situation. However, there is a collection + @{fact ac_simps} where facts @{fact abel_semigroup.assoc}, + @{fact abel_semigroup.commute} and @{fact abel_semigroup.left_commute} + are declared as members. Due to interpretation, also + @{fact mult.assoc}, @{fact mult.commute} and @{fact mult.left_commute} + are also members of @{fact ac_simps}, as any corresponding facts + stemming from interpretation of @{locale abel_semigroup}. + Hence adding @{fact ac_simps} to the simplification rules for + a single method call uses all associativity and commutativity + rules known by means of interpretation. +\ + + +subsection \Additive and multiplicative groups\ + +text \ + The hierarchy for inverse group operations takes into account + that there are weaker algebraic structures with only a partially + inverse operation. E. g. the natural numbers have bounded + subtraction @{term "m - (n::nat)"} which is only an inverse + operation if @{term "m \ (n::nat)"}; unary minus @{text "-"} + is pointless on the natural numbers. + + Hence for both additive and multiplicative notation there + are syntactic classes for inverse operations, both unary + and binary: + + \<^item> @{command class} @{class minus} with @{term [source] "(a::'a::minus) - b"} + + \<^item> @{command class} @{class uminus} with @{term [source] "- a::'a::uminus"} + + \<^item> @{command class} @{class divide} with @{term [source] "(a::'a::divide) div b"} + + \<^item> @{command class} @{class inverse} = @{class divide} with @{term [source] "inverse a::'a::inverse"} + \\ and @{term [source] "(a::'a::inverse) / b"} + + \noindent Here @{class inverse} specializes the ``partial'' syntax + @{term [source] "a div b"} to the more specific + @{term [source] "a / b"}. + + Semantic properties are added by + + \<^item> @{command class} @{class cancel_ab_semigroup_add} = @{class ab_semigroup_add} + @{class minus} + + \<^item> @{command class} @{class cancel_comm_monoid_add} = @{class cancel_ab_semigroup_add} + @{class comm_monoid_add} + + \noindent which specify a minimal binary partially inverse operation as + + \<^item> @{fact add_diff_cancel_left'}: @{thm (frugal_sorts) add_diff_cancel_left' [all, no_vars]} + + \<^item> @{fact diff_diff_add}: @{thm (frugal_sorts) diff_diff_add [all, no_vars]} + + \noindent which in turn allow to derive facts like + + \<^item> @{fact add_left_imp_eq}: @{thm (frugal_sorts) add_left_imp_eq [all, no_vars]} + + \noindent The total inverse operation is established as follows: + + \<^item> Locale @{locale group} extends the abstract hierarchy with + the inverse operation. + + \<^item> The concrete additive inverse operation emerges through + + \<^item> @{command class} @{class group_add} = @{class minus} + @{class uminus} + @{class monoid_add} (in @{theory Groups}) \\ + + \<^item> @{command class} @{class ab_group_add} = @{class minus} + @{class uminus} + @{class comm_monoid_add} (in @{theory Groups}) + + and corresponding interpretation of locale @{locale group}, yielding e.g. + + \<^item> @{fact group.left_inverse}: @{thm (frugal_sorts) group.left_inverse [all, no_vars]} + + \<^item> @{fact add.left_inverse}: @{thm (frugal_sorts) add.left_inverse [all, no_vars]} + + \noindent There is no multiplicative counterpart. Why? In rings, + the multiplicative group excludes the zero element, hence + the inverse operation is not total. See further \secref{sec:rings}. +\ + +paragraph \Mitigating against redundancy by default simplification rules\ + +text \ + Inverse operations imposes some redundancy on the type class + hierarchy: in a group with a total inverse operation, the + unary operation is simpler and more primitive than the binary + one; but we cannot eliminate the binary one in favour of + a mere syntactic abbreviation since the binary one is vital + to express a partial inverse operation. + + This is mitigated by providing suitable default simplification + rules: expression involving the unary inverse operation are + simplified to binary inverse operation whenever appropriate. + The rationale is that simplification is a central device in + explorative proving, where proof obligation remaining after certain + default proof steps including simplification are inspected + to get an idea what is missing to finish a proof. When + preferable normal forms are encoded into + default simplification rules, proof obligations after simplification + are normalized and hence more proof-friendly. +\ + end