1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Jul 24 15:20:53 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Jul 24 15:21:54 2007 +0200
1.3 @@ -3,7 +3,7 @@
1.4
1.5 (*<*)
1.6 theory Classes
1.7 -imports Main
1.8 +imports Main Pretty_Int
1.9 begin
1.10
1.11 ML {*
1.12 @@ -106,7 +106,7 @@
1.13
1.14 Indeed, type classes not only allow for simple overloading
1.15 but form a generic calculus, an instance of order-sorted
1.16 - algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
1.17 + algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
1.18
1.19 From a software enigineering point of view, type classes
1.20 correspond to interfaces in object-oriented languages like Java;
1.21 @@ -136,7 +136,8 @@
1.22 \item instantating those abstract operations by a particular
1.23 type
1.24 \item in connection with a ``less ad-hoc'' approach to overloading,
1.25 - \item with a direct link to the Isabelle module system (aka locales).
1.26 + \item with a direct link to the Isabelle module system
1.27 + (aka locales \cite{kammueller-locales}).
1.28 \end{enumerate}
1.29
1.30 \noindent Isar type classes also directly support code generation
1.31 @@ -145,12 +146,12 @@
1.32 This tutorial demonstrates common elements of structured specifications
1.33 and abstract reasoning with type classes by the algebraic hierarchy of
1.34 semigroups, monoids and groups. Our background theory is that of
1.35 - Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
1.36 + Isabelle/HOL \cite{isa-tutorial}, for which some
1.37 familiarity is assumed.
1.38
1.39 Here we merely present the look-and-feel for end users.
1.40 Internally, those are mapped to more primitive Isabelle concepts.
1.41 - See \cite{haftmann_wenzel2006classes} for more detail.
1.42 + See \cite{Haftmann-Wenzel:2006:classes} for more detail.
1.43 *}
1.44
1.45 section {* A simple algebra example \label{sec:example} *}
1.46 @@ -403,12 +404,33 @@
1.47 *}
1.48
1.49
1.50 -(*subsection {* Derived definitions *}
1.51 +subsection {* Derived definitions *}
1.52
1.53 text {*
1.54 -*}*)
1.55 + Isabelle locales support a concept of local definitions
1.56 + in locales:
1.57 +*}
1.58
1.59 -(* subsection {* Additional subclass relations *}
1.60 + fun (in monoid)
1.61 + pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.62 + "pow_nat 0 x = \<^loc>\<one>"
1.63 + | "pow_nat (Suc n) x = x \<^loc>\<otimes> pow_nat n x"
1.64 +
1.65 +text {*
1.66 + \noindent If the locale @{text group} is also a class, this local
1.67 + definition is propagated onto a global definition of
1.68 + @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
1.69 + with corresponding theorems
1.70 +
1.71 + @{thm pow_nat.simps [no_vars]}.
1.72 +
1.73 + \noindent As you can see from this example, for local
1.74 + definitions you may use any specification tool
1.75 + which works together with locales (e.g. \cite{krauss2006}).
1.76 +*}
1.77 +
1.78 +
1.79 +(*subsection {* Additional subclass relations *}
1.80
1.81 text {*
1.82 Any @{text "group"} is also a @{text "monoid"}; this
1.83 @@ -416,13 +438,36 @@
1.84 together with a proof of the logical difference:
1.85 *}
1.86
1.87 - instance group < monoid
1.88 - proof -
1.89 + instance advanced group < monoid
1.90 + proof unfold_locales
1.91 fix x
1.92 from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
1.93 with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
1.94 with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
1.95 - qed *)
1.96 + qed
1.97 +
1.98 +text {*
1.99 + The logical proof is carried out on the locale level
1.100 + and thus conveniently is opened using the @{text unfold_locales}
1.101 + method which only leaves the logical differences still
1.102 + open to proof to the user. After the proof it is propagated
1.103 + to the type system, making @{text group} an instance of
1.104 + @{text monoid}. For illustration, a derived definition
1.105 + in @{text group} which uses @{text of_nat}:
1.106 +*}
1.107 +
1.108 + definition (in group)
1.109 + pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
1.110 + "pow_int k x = (if k >= 0
1.111 + then pow_nat (nat k) x
1.112 + else (pow_nat (nat (- k)) x)\<^loc>\<div>)"
1.113 +
1.114 +text {*
1.115 + yields the global definition of
1.116 + @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
1.117 + with the corresponding theorem @{thm pow_int_def [no_vars]}.
1.118 +*} *)
1.119 +
1.120
1.121 section {* Further issues *}
1.122
1.123 @@ -437,11 +482,11 @@
1.124 takes this into account. Concerning target languages
1.125 lacking type classes (e.g.~SML), type classes
1.126 are implemented by explicit dictionary construction.
1.127 - As example, the natural power function on groups:
1.128 + For example, lets go back to the power function:
1.129 *}
1.130
1.131 fun
1.132 - pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>monoidl \<Rightarrow> \<alpha>\<Colon>monoidl" where
1.133 + pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
1.134 "pow_nat 0 x = \<one>"
1.135 | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
1.136
1.137 @@ -459,19 +504,17 @@
1.138 \noindent This maps to Haskell as:
1.139 *}
1.140
1.141 -code_gen example in Haskell file "code_examples/"
1.142 +code_gen example in Haskell to Classes file "code_examples/"
1.143 (* NOTE: you may use Haskell only once in this document, otherwise
1.144 you have to work in distinct subdirectories *)
1.145
1.146 text {*
1.147 \lsthaskell{Thy/code_examples/Classes.hs}
1.148
1.149 - \noindent (we have left out all other modules).
1.150 -
1.151 \noindent The whole code in SML with explicit dictionary passing:
1.152 *}
1.153
1.154 -code_gen example (*<*)in SML(*>*)in SML file "code_examples/classes.ML"
1.155 +code_gen example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
1.156
1.157 text {*
1.158 \lstsml{Thy/code_examples/classes.ML}
2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Tue Jul 24 15:20:53 2007 +0200
2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Tue Jul 24 15:21:54 2007 +0200
2.3 @@ -1,61 +1,59 @@
2.4 module Classes where {
2.5
2.6 -import qualified Integer;
2.7 -import qualified Nat;
2.8 +
2.9 +data Nat = Zero_nat | Suc Nat;
2.10 +
2.11 +data Bit = B0 | B1;
2.12 +
2.13 +nat_aux :: Integer -> Nat -> Nat;
2.14 +nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
2.15 +
2.16 +nat :: Integer -> Nat;
2.17 +nat i = nat_aux i Zero_nat;
2.18
2.19 class Semigroup a where {
2.20 mult :: a -> a -> a;
2.21 };
2.22
2.23 -class (Classes.Semigroup a) => Monoidl a where {
2.24 +class (Semigroup a) => Monoidl a where {
2.25 neutral :: a;
2.26 };
2.27
2.28 -class (Classes.Monoidl a) => Group a where {
2.29 +class (Monoidl a) => Group a where {
2.30 inverse :: a -> a;
2.31 };
2.32
2.33 -inverse_int :: Integer.Inta -> Integer.Inta;
2.34 -inverse_int i = Integer.uminus_int i;
2.35 +inverse_int :: Integer -> Integer;
2.36 +inverse_int i = negate i;
2.37
2.38 -neutral_int :: Integer.Inta;
2.39 -neutral_int = Integer.Number_of_int Integer.Pls;
2.40 +neutral_int :: Integer;
2.41 +neutral_int = 0;
2.42
2.43 -mult_int :: Integer.Inta -> Integer.Inta -> Integer.Inta;
2.44 -mult_int i j = Integer.plus_int i j;
2.45 +mult_int :: Integer -> Integer -> Integer;
2.46 +mult_int i j = i + j;
2.47
2.48 -instance Classes.Semigroup Integer.Inta where {
2.49 - mult = Classes.mult_int;
2.50 +instance Semigroup Integer where {
2.51 + mult = mult_int;
2.52 };
2.53
2.54 -instance Classes.Monoidl Integer.Inta where {
2.55 - neutral = Classes.neutral_int;
2.56 +instance Monoidl Integer where {
2.57 + neutral = neutral_int;
2.58 };
2.59
2.60 -instance Classes.Group Integer.Inta where {
2.61 - inverse = Classes.inverse_int;
2.62 +instance Group Integer where {
2.63 + inverse = inverse_int;
2.64 };
2.65
2.66 -pow_nat :: (Classes.Monoidl b) => Nat.Nat -> b -> b;
2.67 -pow_nat (Nat.Suc n) x = Classes.mult x (Classes.pow_nat n x);
2.68 -pow_nat Nat.Zero_nat x = Classes.neutral;
2.69 +pow_nat :: (Group b) => Nat -> b -> b;
2.70 +pow_nat (Suc n) x = mult x (pow_nat n x);
2.71 +pow_nat Zero_nat x = neutral;
2.72
2.73 -pow_int :: (Classes.Group a) => Integer.Inta -> a -> a;
2.74 +pow_int :: (Group a) => Integer -> a -> a;
2.75 pow_int k x =
2.76 - (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k
2.77 - then Classes.pow_nat (Integer.nat k) x
2.78 - else Classes.inverse
2.79 - (Classes.pow_nat (Integer.nat (Integer.uminus_int k)) x));
2.80 + (if 0 <= k then pow_nat (nat k) x
2.81 + else inverse (pow_nat (nat (negate k)) x));
2.82
2.83 -example :: Integer.Inta;
2.84 -example =
2.85 - Classes.pow_int
2.86 - (Integer.Number_of_int
2.87 - (Integer.Bit
2.88 - (Integer.Bit
2.89 - (Integer.Bit (Integer.Bit Integer.Pls Integer.B1) Integer.B0)
2.90 - Integer.B1)
2.91 - Integer.B0))
2.92 - (Integer.Number_of_int (Integer.Bit Integer.Min Integer.B0));
2.93 +example :: Integer;
2.94 +example = pow_int 10 (-2);
2.95
2.96 }
3.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Jul 24 15:20:53 2007 +0200
3.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Jul 24 15:21:54 2007 +0200
3.3 @@ -1,141 +1,53 @@
3.4 -structure ROOT =
3.5 -struct
3.6 -
3.7 -structure Nat =
3.8 +structure Classes =
3.9 struct
3.10
3.11 datatype nat = Zero_nat | Suc of nat;
3.12
3.13 -end; (*struct Nat*)
3.14 -
3.15 -structure Integer =
3.16 -struct
3.17 -
3.18 datatype bit = B0 | B1;
3.19
3.20 -datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
3.21 +fun nat_aux i n =
3.22 + (if IntInf.<= (i, (0 : IntInf.int)) then n
3.23 + else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));
3.24
3.25 -fun pred (Bit (k, B0)) = Bit (pred k, B1)
3.26 - | pred (Bit (k, B1)) = Bit (k, B0)
3.27 - | pred Min = Bit (Min, B0)
3.28 - | pred Pls = Min;
3.29 -
3.30 -fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
3.31 - | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
3.32 - | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
3.33 - | uminus_int Min = Bit (Pls, B1)
3.34 - | uminus_int Pls = Pls;
3.35 -
3.36 -fun succ (Bit (k, B0)) = Bit (k, B1)
3.37 - | succ (Bit (k, B1)) = Bit (succ k, B0)
3.38 - | succ Min = Pls
3.39 - | succ Pls = Bit (Pls, B1);
3.40 -
3.41 -fun plus_int (Number_of_int v) (Number_of_int w) =
3.42 - Number_of_int (plus_int v w)
3.43 - | plus_int k Min = pred k
3.44 - | plus_int k Pls = k
3.45 - | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
3.46 - | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
3.47 - | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
3.48 - | plus_int Min k = pred k
3.49 - | plus_int Pls k = k;
3.50 -
3.51 -fun minus_int (Number_of_int v) (Number_of_int w) =
3.52 - Number_of_int (plus_int v (uminus_int w))
3.53 - | minus_int z w = plus_int z (uminus_int w);
3.54 -
3.55 -fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l
3.56 - | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2
3.57 - | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2
3.58 - | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2
3.59 - | less_eq_int (Bit (k, v)) Min = less_eq_int k Min
3.60 - | less_eq_int (Bit (k, B1)) Pls = less_int k Pls
3.61 - | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls
3.62 - | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k
3.63 - | less_eq_int Min (Bit (k, B0)) = less_int Min k
3.64 - | less_eq_int Min Min = true
3.65 - | less_eq_int Min Pls = true
3.66 - | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k
3.67 - | less_eq_int Pls Min = false
3.68 - | less_eq_int Pls Pls = true
3.69 -and less_int (Number_of_int k) (Number_of_int l) = less_int k l
3.70 - | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2
3.71 - | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2
3.72 - | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2
3.73 - | less_int (Bit (k, B1)) Min = less_int k Min
3.74 - | less_int (Bit (k, B0)) Min = less_eq_int k Min
3.75 - | less_int (Bit (k, v)) Pls = less_int k Pls
3.76 - | less_int Min (Bit (k, v)) = less_int Min k
3.77 - | less_int Min Min = false
3.78 - | less_int Min Pls = true
3.79 - | less_int Pls (Bit (k, B1)) = less_eq_int Pls k
3.80 - | less_int Pls (Bit (k, B0)) = less_int Pls k
3.81 - | less_int Pls Min = false
3.82 - | less_int Pls Pls = false;
3.83 -
3.84 -fun nat_aux n i =
3.85 - (if less_eq_int i (Number_of_int Pls) then n
3.86 - else nat_aux (Nat.Suc n)
3.87 - (minus_int i (Number_of_int (Bit (Pls, B1)))));
3.88 -
3.89 -fun nat i = nat_aux Nat.Zero_nat i;
3.90 -
3.91 -end; (*struct Integer*)
3.92 -
3.93 -structure Classes =
3.94 -struct
3.95 +fun nat i = nat_aux i Zero_nat;
3.96
3.97 type 'a semigroup = {mult : 'a -> 'a -> 'a};
3.98 fun mult (A_:'a semigroup) = #mult A_;
3.99
3.100 type 'a monoidl =
3.101 - {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a};
3.102 -fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_;
3.103 + {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};
3.104 +fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;
3.105 fun neutral (A_:'a monoidl) = #neutral A_;
3.106
3.107 -type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a};
3.108 -fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_;
3.109 +type 'a group = {Classes__monoidl_group : 'a monoidl, inverse : 'a -> 'a};
3.110 +fun monoidl_group (A_:'a group) = #Classes__monoidl_group A_;
3.111 fun inverse (A_:'a group) = #inverse A_;
3.112
3.113 -fun inverse_int i = Integer.uminus_int i;
3.114 +fun inverse_int i = IntInf.~ i;
3.115
3.116 -val neutral_int : Integer.int = Integer.Number_of_int Integer.Pls;
3.117 +val neutral_int : IntInf.int = (0 : IntInf.int);
3.118
3.119 -fun mult_int i j = Integer.plus_int i j;
3.120 +fun mult_int i j = IntInf.+ (i, j);
3.121
3.122 -val semigroup_int = {mult = mult_int} : Integer.int semigroup;
3.123 +val semigroup_int = {mult = mult_int} : IntInf.int semigroup;
3.124
3.125 val monoidl_int =
3.126 - {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} :
3.127 - Integer.int monoidl;
3.128 + {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :
3.129 + IntInf.int monoidl;
3.130
3.131 val group_int =
3.132 - {Classes__group_monoidl = monoidl_int, inverse = inverse_int} :
3.133 - Integer.int group;
3.134 + {Classes__monoidl_group = monoidl_int, inverse = inverse_int} :
3.135 + IntInf.int group;
3.136
3.137 -fun pow_nat B_ (Nat.Suc n) x =
3.138 - mult (monoidl_semigroup B_) x (pow_nat B_ n x)
3.139 - | pow_nat B_ Nat.Zero_nat x = neutral B_;
3.140 +fun pow_nat B_ (Suc n) x =
3.141 + mult ((semigroup_monoidl o monoidl_group) B_) x (pow_nat B_ n x)
3.142 + | pow_nat B_ Zero_nat x = neutral (monoidl_group B_);
3.143
3.144 fun pow_int A_ k x =
3.145 - (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k
3.146 - then pow_nat (group_monoidl A_) (Integer.nat k) x
3.147 - else inverse A_
3.148 - (pow_nat (group_monoidl A_)
3.149 - (Integer.nat (Integer.uminus_int k)) x));
3.150 + (if IntInf.<= ((0 : IntInf.int), k) then pow_nat A_ (nat k) x
3.151 + else inverse A_ (pow_nat A_ (nat (IntInf.~ k)) x));
3.152
3.153 -val example : Integer.int =
3.154 - pow_int group_int
3.155 - (Integer.Number_of_int
3.156 - (Integer.Bit
3.157 - (Integer.Bit
3.158 - (Integer.Bit
3.159 - (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0),
3.160 - Integer.B1),
3.161 - Integer.B0)))
3.162 - (Integer.Number_of_int (Integer.Bit (Integer.Min, Integer.B0)));
3.163 +val example : IntInf.int =
3.164 + pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);
3.165
3.166 end; (*struct Classes*)
3.167 -
3.168 -end; (*struct ROOT*)
4.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Jul 24 15:20:53 2007 +0200
4.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Jul 24 15:21:54 2007 +0200
4.3 @@ -85,7 +85,7 @@
4.4
4.5 Indeed, type classes not only allow for simple overloading
4.6 but form a generic calculus, an instance of order-sorted
4.7 - algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
4.8 + algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
4.9
4.10 From a software enigineering point of view, type classes
4.11 correspond to interfaces in object-oriented languages like Java;
4.12 @@ -115,7 +115,8 @@
4.13 \item instantating those abstract operations by a particular
4.14 type
4.15 \item in connection with a ``less ad-hoc'' approach to overloading,
4.16 - \item with a direct link to the Isabelle module system (aka locales).
4.17 + \item with a direct link to the Isabelle module system
4.18 + (aka locales \cite{kammueller-locales}).
4.19 \end{enumerate}
4.20
4.21 \noindent Isar type classes also directly support code generation
4.22 @@ -124,12 +125,12 @@
4.23 This tutorial demonstrates common elements of structured specifications
4.24 and abstract reasoning with type classes by the algebraic hierarchy of
4.25 semigroups, monoids and groups. Our background theory is that of
4.26 - Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
4.27 + Isabelle/HOL \cite{isa-tutorial}, for which some
4.28 familiarity is assumed.
4.29
4.30 Here we merely present the look-and-feel for end users.
4.31 Internally, those are mapped to more primitive Isabelle concepts.
4.32 - See \cite{haftmann_wenzel2006classes} for more detail.%
4.33 + See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
4.34 \end{isamarkuptext}%
4.35 \isamarkuptrue%
4.36 %
4.37 @@ -662,6 +663,35 @@
4.38 \end{isamarkuptext}%
4.39 \isamarkuptrue%
4.40 %
4.41 +\isamarkupsubsection{Derived definitions%
4.42 +}
4.43 +\isamarkuptrue%
4.44 +%
4.45 +\begin{isamarkuptext}%
4.46 +Isabelle locales support a concept of local definitions
4.47 + in locales:%
4.48 +\end{isamarkuptext}%
4.49 +\isamarkuptrue%
4.50 +\ \ \ \ \isacommand{fun}\isamarkupfalse%
4.51 +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
4.52 +\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
4.53 +\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
4.54 +\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
4.55 +\begin{isamarkuptext}%
4.56 +\noindent If the locale \isa{group} is also a class, this local
4.57 + definition is propagated onto a global definition of
4.58 + \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
4.59 + with corresponding theorems
4.60 +
4.61 + \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
4.62 +pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
4.63 +
4.64 + \noindent As you can see from this example, for local
4.65 + definitions you may use any specification tool
4.66 + which works together with locales (e.g. \cite{krauss2006}).%
4.67 +\end{isamarkuptext}%
4.68 +\isamarkuptrue%
4.69 +%
4.70 \isamarkupsection{Further issues%
4.71 }
4.72 \isamarkuptrue%
4.73 @@ -679,12 +709,12 @@
4.74 takes this into account. Concerning target languages
4.75 lacking type classes (e.g.~SML), type classes
4.76 are implemented by explicit dictionary construction.
4.77 - As example, the natural power function on groups:%
4.78 + For example, lets go back to the power function:%
4.79 \end{isamarkuptext}%
4.80 \isamarkuptrue%
4.81 \ \ \ \ \isacommand{fun}\isamarkupfalse%
4.82 \isanewline
4.83 -\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
4.84 +\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
4.85 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
4.86 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
4.87 \isanewline
4.88 @@ -704,17 +734,15 @@
4.89 \end{isamarkuptext}%
4.90 \isamarkuptrue%
4.91 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.92 -\ example\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
4.93 +\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
4.94 \begin{isamarkuptext}%
4.95 \lsthaskell{Thy/code_examples/Classes.hs}
4.96
4.97 - \noindent (we have left out all other modules).
4.98 -
4.99 \noindent The whole code in SML with explicit dictionary passing:%
4.100 \end{isamarkuptext}%
4.101 \isamarkuptrue%
4.102 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.103 -\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
4.104 +\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
4.105 \begin{isamarkuptext}%
4.106 \lstsml{Thy/code_examples/classes.ML}%
4.107 \end{isamarkuptext}%
5.1 --- a/doc-src/IsarAdvanced/Classes/classes.bib Tue Jul 24 15:20:53 2007 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,211 +0,0 @@
5.4 -
5.5 -@InProceedings{Ballarin:2004,
5.6 - author = {Clemens Ballarin},
5.7 - title = {Locales and Locale Expressions in {Isabelle/Isar}},
5.8 - booktitle = {Types for Proofs and Programs (TYPES 2003)},
5.9 - year = 2004,
5.10 - editor = {Stefano Berardi and others},
5.11 - series = {LNCS 3085}
5.12 -}
5.13 -
5.14 -@InProceedings{Ballarin:2006,
5.15 - author = {Clemens Ballarin},
5.16 - title = {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts},
5.17 - booktitle = {Mathematical Knowledge Management (MKM 2006)},
5.18 - year = 2006,
5.19 - editor = {J.M. Borwein and W.M. Farmer},
5.20 - series = {LNAI 4108}
5.21 -}
5.22 -
5.23 -@InProceedings{Berghofer-Nipkow:2000,
5.24 - author = {Stefan Berghofer and Tobias Nipkow},
5.25 - title = {Proof terms for simply typed higher order logic},
5.26 - booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} 2000)},
5.27 - editor = {J. Harrison and M. Aagaard},
5.28 - series = {LNCS 1869},
5.29 - year = 2000
5.30 -}
5.31 -
5.32 -@Manual{Coq-Manual:2006,
5.33 - title = {The {Coq} Proof Assistant Reference Manual, version 8},
5.34 - author = {B. Barras and others},
5.35 - organization = {INRIA},
5.36 - year = 2006
5.37 -}
5.38 -
5.39 -@Article{Courant:2006,
5.40 - author = {Judica{\"e}l Courant},
5.41 - title = {{$\mathcal{MC}_2$: A Module Calculus for Pure Type Systems}},
5.42 - journal = {The Journal of Functional Programming},
5.43 - year = 2006,
5.44 - note = {To appear},
5.45 - abstract = {Several proof-assistants rely on the very formal basis
5.46 - of Pure Type Systems (PTS) as their foundations. We are concerned
5.47 - with the issues involved in the development of large proofs in
5.48 - these provers such as namespace management, development of
5.49 - reusable proof libraries and separate verification. Although
5.50 - implementations offer many features to address them, few
5.51 - theoretical foundations have been laid for them up to now. This is
5.52 - a problem as features dealing with modularity may have harmful,
5.53 - unsuspected effects on the reliability or usability of an
5.54 - implementation.
5.55 -
5.56 - In this paper, we propose an extension of Pure Type Systems with a
5.57 - module system, MC2, adapted from SML-like module systems for
5.58 - programming languages. This system gives a theoretical framework
5.59 - addressing the issues mentioned above in a quite uniform way. It
5.60 - is intended to be a theoretical foundation for the module systems
5.61 - of proof-assistants such as Coq or Agda. We show how reliability
5.62 - and usability can be formalized as metatheoretical properties and
5.63 - prove they hold for MC2.}
5.64 -}
5.65 -
5.66 -@PhdThesis{Jacek:2004,
5.67 - author = {Jacek Chrz\c{a}szcz},
5.68 - title = {Modules in type theory with generative definitions},
5.69 - school = {Universit{\'e} Paris-Sud},
5.70 - year = {2004},
5.71 -}
5.72 -
5.73 -@InProceedings{Kamm-et-al:1999,
5.74 - author = {Florian Kamm{\"u}ller and Markus Wenzel and
5.75 - Lawrence C. Paulson},
5.76 - title = {Locales: A Sectioning Concept for {Isabelle}},
5.77 - booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '99)},
5.78 - editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
5.79 - Paulin, C. and Thery, L.},
5.80 - series = {LNCS 1690},
5.81 - year = 1999
5.82 -}
5.83 -
5.84 -@InProceedings{Nipkow-Prehofer:1993,
5.85 - author = {T. Nipkow and C. Prehofer},
5.86 - title = {Type checking type classes},
5.87 - booktitle = {ACM Symp.\ Principles of Programming Languages},
5.88 - year = 1993
5.89 -}
5.90 -
5.91 -@Book{Nipkow-et-al:2002:tutorial,
5.92 - author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
5.93 - title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
5.94 - series = {LNCS 2283},
5.95 - year = 2002
5.96 -}
5.97 -
5.98 -@InCollection{Nipkow:1993,
5.99 - author = {T. Nipkow},
5.100 - title = {Order-Sorted Polymorphism in {Isabelle}},
5.101 - booktitle = {Logical Environments},
5.102 - publisher = {Cambridge University Press},
5.103 - year = 1993,
5.104 - editor = {G. Huet and G. Plotkin}
5.105 -}
5.106 -
5.107 -@InProceedings{Nipkow:2002,
5.108 - author = {Tobias Nipkow},
5.109 - title = {Structured Proofs in {Isar/HOL}},
5.110 - booktitle = {Types for Proofs and Programs (TYPES 2002)},
5.111 - year = 2003,
5.112 - editor = {H. Geuvers and F. Wiedijk},
5.113 - series = {LNCS 2646}
5.114 -}
5.115 -
5.116 -@InCollection{Paulson:1990,
5.117 - author = {L. C. Paulson},
5.118 - title = {Isabelle: the next 700 theorem provers},
5.119 - booktitle = {Logic and Computer Science},
5.120 - publisher = {Academic Press},
5.121 - year = 1990,
5.122 - editor = {P. Odifreddi}
5.123 -}
5.124 -
5.125 -@BOOK{Pierce:TypeSystems,
5.126 - AUTHOR = {B.C. Pierce},
5.127 - TITLE = {Types and Programming Languages},
5.128 - PUBLISHER = {MIT Press},
5.129 - YEAR = 2002,
5.130 - PLCLUB = {Yes},
5.131 - BCP = {Yes},
5.132 - KEYS = {books},
5.133 - HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl},
5.134 - ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
5.135 -}
5.136 -
5.137 -@Book{Schmidt-Schauss:1989,
5.138 - author = {Manfred Schmidt-Schau{\ss}},
5.139 - title = {Computational Aspects of an Order-Sorted Logic with Term Declarations},
5.140 - series = {LNAI 395},
5.141 - year = 1989
5.142 -}
5.143 -
5.144 -@InProceedings{Wenzel:1997,
5.145 - author = {M. Wenzel},
5.146 - title = {Type Classes and Overloading in Higher-Order Logic},
5.147 - booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '97)},
5.148 - editor = {Elsa L. Gunter and Amy Felty},
5.149 - series = {LNCS 1275},
5.150 - year = 1997}
5.151 -
5.152 -@article{hall96type,
5.153 - author = "Cordelia Hall and Kevin Hammond and Peyton Jones, S. and Philip Wadler",
5.154 - title = "Type Classes in {Haskell}",
5.155 - journal = "ACM Transactions on Programming Languages and Systems",
5.156 - volume = "18",
5.157 - number = "2",
5.158 - publisher = "ACM Press",
5.159 - year = "1996"
5.160 -}
5.161 -
5.162 -@inproceedings{hindleymilner,
5.163 - author = {L. Damas and H. Milner},
5.164 - title = {Principal type schemes for functional programs},
5.165 - booktitle = {ACM Symp. Principles of Programming Languages},
5.166 - year = 1982
5.167 -}
5.168 -
5.169 -@manual{isabelle-axclass,
5.170 - author = {Markus Wenzel},
5.171 - title = {Using Axiomatic Type Classes in {I}sabelle},
5.172 - institution = {TU Munich},
5.173 - year = 2005,
5.174 - note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
5.175 -
5.176 -@InProceedings{krauss:2006:functions,
5.177 - author = {A. Krauss},
5.178 - title = {Partial Recursive Functions in Higher-Order Logic},
5.179 - booktitle = {Int. Joint Conference on Automated Reasoning (IJCAR 2006)},
5.180 - year = 2006,
5.181 - editor = {Ulrich Furbach and Natarajan Shankar},
5.182 - series = {LNCS}
5.183 -}
5.184 -
5.185 -@inproceedings{peterson93implementing,
5.186 - author = "J. Peterson and Peyton Jones, S.",
5.187 - title = "Implementing Type Classes",
5.188 - booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
5.189 - year = 1993
5.190 -}
5.191 -
5.192 -@inproceedings{wadler89how,
5.193 - author = {P. Wadler and S. Blott},
5.194 - title = {How to make ad-hoc polymorphism less ad-hoc},
5.195 - booktitle = {ACM Symp.\ Principles of Programming Languages},
5.196 - year = 1989
5.197 -}
5.198 -
5.199 -@misc{jones97type,
5.200 - author = "S. Jones and M. Jones and E. Meijer",
5.201 - title = "Type classes: an exploration of the design space",
5.202 - text = "Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration
5.203 - of the design space. In Haskell Workshop, June 1997.",
5.204 - year = "1997",
5.205 - url = "citeseer.ist.psu.edu/peytonjones97type.html"
5.206 -}
5.207 -
5.208 -@article{haftmann_wenzel2006classes,
5.209 - author = "Florian Haftmann and Makarius Wenzel",
5.210 - title = "Constructive Type Classes in Isabelle",
5.211 - year = 2006,
5.212 - note = {To appear}
5.213 -}
5.214 -
6.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex Tue Jul 24 15:20:53 2007 +0200
6.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Tue Jul 24 15:21:54 2007 +0200
6.3 @@ -79,7 +79,7 @@
6.4 \begingroup
6.5 %\tocentry{\bibname}
6.6 \bibliographystyle{plain} \small\raggedright\frenchspacing
6.7 -\bibliography{../../manual,classes}
6.8 +\bibliography{../../manual}
6.9 \endgroup
6.10
6.11 \end{document}
7.1 --- a/doc-src/manual.bib Tue Jul 24 15:20:53 2007 +0200
7.2 +++ b/doc-src/manual.bib Tue Jul 24 15:21:54 2007 +0200
7.3 @@ -441,6 +441,13 @@
7.4
7.5 %H
7.6
7.7 +@InProceedings{Haftmann-Wenzel:2006:classes,
7.8 + author = {Florian Haftmann and Makarius Wenzel},
7.9 + title = {Constructive Type Classes in {Isabelle}},
7.10 + year = 2006,
7.11 + note = {To appear}
7.12 +}
7.13 +
7.14 @manual{isabelle-classes,
7.15 author = {Florian Haftmann},
7.16 title = {Haskell-style type classes with {Isabelle}/{Isar}},
7.17 @@ -803,6 +810,13 @@
7.18 year = 1995,
7.19 pages = {201-224}}
7.20
7.21 +@InProceedings{Nipkow-Prehofer:1993,
7.22 + author = {T. Nipkow and C. Prehofer},
7.23 + title = {Type checking type classes},
7.24 + booktitle = {ACM Symp.\ Principles of Programming Languages},
7.25 + year = 1993
7.26 +}
7.27 +
7.28 @Book{isa-tutorial,
7.29 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
7.30 title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
7.31 @@ -1231,6 +1245,13 @@
7.32
7.33 %W
7.34
7.35 +@inproceedings{wadler89how,
7.36 + author = {P. Wadler and S. Blott},
7.37 + title = {How to make ad-hoc polymorphism less ad-hoc},
7.38 + booktitle = {ACM Symp.\ Principles of Programming Languages},
7.39 + year = 1989
7.40 +}
7.41 +
7.42 @Misc{x-symbol,
7.43 author = {Christoph Wedler},
7.44 title = {Emacs package ``{X-Symbol}''},
7.45 @@ -1531,6 +1552,6 @@
7.46 year = 2006}
7.47
7.48 @unpublished{classes_modules,
7.49 - title = {ML Modules and Haskell Type Classes: A Constructive Comparison},
7.50 + title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
7.51 author = {Stefan Wehr et. al.}
7.52 }