1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Dec 05 04:34:15 2007 +0100
1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Dec 05 14:15:39 2007 +0100
1.3 @@ -12,6 +12,8 @@
1.4 syntax
1.5 "_alpha" :: "type" ("\<alpha>")
1.6 "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
1.7 + "_beta" :: "type" ("\<beta>")
1.8 + "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
1.9
1.10 parse_ast_translation {*
1.11 let
1.12 @@ -20,8 +22,14 @@
1.13 fun alpha_ofsort_ast_tr [ast] =
1.14 Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
1.15 | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
1.16 + fun beta_ast_tr [] = Syntax.Variable "'b"
1.17 + | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
1.18 + fun beta_ofsort_ast_tr [ast] =
1.19 + Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
1.20 + | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
1.21 in [
1.22 - ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr)
1.23 + ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
1.24 + ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
1.25 ] end
1.26 *}
1.27 (*>*)
1.28 @@ -145,38 +153,54 @@
1.29 The concrete type @{text "int"} is made a @{text "semigroup"}
1.30 instance by providing a suitable definition for the class parameter
1.31 @{text "mult"} and a proof for the specification of @{text "assoc"}.
1.32 + This is accomplished by the @{text "\<INSTANTIATION>"} target:
1.33 *}
1.34
1.35 - instance int :: semigroup
1.36 - mult_int_def: "i \<otimes> j \<equiv> i + j"
1.37 - proof
1.38 + instantiation int :: semigroup
1.39 + begin
1.40 +
1.41 + definition
1.42 + mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
1.43 +
1.44 + instance proof
1.45 fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
1.46 then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
1.47 unfolding mult_int_def .
1.48 qed
1.49
1.50 + end
1.51 +
1.52 text {*
1.53 - \noindent From now on, the type-checker will consider @{text "int"}
1.54 - as a @{text "semigroup"} automatically, i.e.\ any general results
1.55 - are immediately available on concrete instances.
1.56 -
1.57 - Note that the first proof step is the @{text default} method,
1.58 - which for instantiation proofs maps to the @{text intro_classes} method.
1.59 - This boils down an instantiation judgement to the relevant primitive
1.60 + \noindent @{text "\<INSTANTIATION>"} allows to define class parameters
1.61 + at a particular instance using common specification tools (here,
1.62 + @{text "\<DEFINITION>"}). The concluding @{text "\<INSTANCE>"}
1.63 + opens a proof that the given parameters actually conform
1.64 + to the class specification. Note that the first proof step
1.65 + is the @{text default} method,
1.66 + which for such instance proofs maps to the @{text intro_classes} method.
1.67 + This boils down an instance judgement to the relevant primitive
1.68 proof goals and should conveniently always be the first method applied
1.69 in an instantiation proof.
1.70
1.71 + From now on, the type-checker will consider @{text "int"}
1.72 + as a @{text "semigroup"} automatically, i.e.\ any general results
1.73 + are immediately available on concrete instances.
1.74 \medskip Another instance of @{text "semigroup"} are the natural numbers:
1.75 *}
1.76
1.77 - instance nat :: semigroup
1.78 - mult_nat_def: "m \<otimes> n \<equiv> m + n"
1.79 - proof
1.80 + instantiation nat :: semigroup
1.81 + begin
1.82 +
1.83 + definition
1.84 + mult_nat_def: "m \<otimes> n = m + (n\<Colon>nat)"
1.85 +
1.86 + instance proof
1.87 fix m n q :: nat
1.88 show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
1.89 unfolding mult_nat_def by simp
1.90 qed
1.91
1.92 + end
1.93
1.94 subsection {* Lifting and parametric types *}
1.95
1.96 @@ -187,14 +211,20 @@
1.97 using our simple algebra:
1.98 *}
1.99
1.100 - instance * :: (semigroup, semigroup) semigroup
1.101 - mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 \<equiv> (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
1.102 - proof
1.103 - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
1.104 + instantiation * :: (semigroup, semigroup) semigroup
1.105 + begin
1.106 +
1.107 + definition
1.108 + mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
1.109 +
1.110 + instance proof
1.111 + fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
1.112 show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
1.113 unfolding mult_prod_def by (simp add: assoc)
1.114 qed
1.115
1.116 + end
1.117 +
1.118 text {*
1.119 \noindent Associativity from product semigroups is
1.120 established using
1.121 @@ -223,33 +253,45 @@
1.122 text {*
1.123 \noindent Again, we prove some instances, by
1.124 providing suitable parameter definitions and proofs for the
1.125 - additional specifications:
1.126 + additional specifications. Obverve that instantiations
1.127 + for types with the same arity may be simultaneous:
1.128 *}
1.129
1.130 - instance nat :: monoidl
1.131 - neutral_nat_def: "\<one> \<equiv> 0"
1.132 - proof
1.133 + instantiation nat and int :: monoidl
1.134 + begin
1.135 +
1.136 + definition
1.137 + neutral_nat_def: "\<one> = (0\<Colon>nat)"
1.138 +
1.139 + definition
1.140 + neutral_int_def: "\<one> = (0\<Colon>int)"
1.141 +
1.142 + instance proof
1.143 fix n :: nat
1.144 show "\<one> \<otimes> n = n"
1.145 unfolding neutral_nat_def mult_nat_def by simp
1.146 - qed
1.147 -
1.148 - instance int :: monoidl
1.149 - neutral_int_def: "\<one> \<equiv> 0"
1.150 - proof
1.151 + next
1.152 fix k :: int
1.153 show "\<one> \<otimes> k = k"
1.154 unfolding neutral_int_def mult_int_def by simp
1.155 qed
1.156
1.157 - instance * :: (monoidl, monoidl) monoidl
1.158 - neutral_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
1.159 - proof
1.160 - fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl"
1.161 + end
1.162 +
1.163 + instantiation * :: (monoidl, monoidl) monoidl
1.164 + begin
1.165 +
1.166 + definition
1.167 + neutral_prod_def: "\<one> = (\<one>, \<one>)"
1.168 +
1.169 + instance proof
1.170 + fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
1.171 show "\<one> \<otimes> p = p"
1.172 unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
1.173 qed
1.174
1.175 + end
1.176 +
1.177 text {*
1.178 \noindent Fully-fledged monoids are modelled by another subclass
1.179 which does not add new parameters but tightens the specification:
1.180 @@ -258,27 +300,32 @@
1.181 class monoid = monoidl +
1.182 assumes neutr: "x \<otimes> \<one> = x"
1.183
1.184 - instance nat :: monoid
1.185 - proof
1.186 + instantiation nat and int :: monoid
1.187 + begin
1.188 +
1.189 + instance proof
1.190 fix n :: nat
1.191 show "n \<otimes> \<one> = n"
1.192 unfolding neutral_nat_def mult_nat_def by simp
1.193 - qed
1.194 -
1.195 - instance int :: monoid
1.196 - proof
1.197 + next
1.198 fix k :: int
1.199 show "k \<otimes> \<one> = k"
1.200 unfolding neutral_int_def mult_int_def by simp
1.201 qed
1.202
1.203 - instance * :: (monoid, monoid) monoid
1.204 - proof
1.205 - fix p :: "'a\<Colon>monoid \<times> 'b\<Colon>monoid"
1.206 + end
1.207 +
1.208 + instantiation * :: (monoid, monoid) monoid
1.209 + begin
1.210 +
1.211 + instance proof
1.212 + fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
1.213 show "p \<otimes> \<one> = p"
1.214 unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
1.215 qed
1.216
1.217 + end
1.218 +
1.219 text {*
1.220 \noindent To finish our small algebra example, we add a @{text "group"} class
1.221 with a corresponding instance:
1.222 @@ -288,15 +335,21 @@
1.223 fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
1.224 assumes invl: "x\<div> \<otimes> x = \<one>"
1.225
1.226 - instance int :: group
1.227 - inverse_int_def: "i\<div> \<equiv> - i"
1.228 - proof
1.229 + instantiation int :: group
1.230 + begin
1.231 +
1.232 + definition
1.233 + inverse_int_def: "i\<div> = - (i\<Colon>int)"
1.234 +
1.235 + instance proof
1.236 fix i :: int
1.237 have "-i + i = 0" by simp
1.238 then show "i\<div> \<otimes> i = \<one>"
1.239 unfolding mult_int_def neutral_int_def inverse_int_def .
1.240 qed
1.241
1.242 + end
1.243 +
1.244 section {* Type classes as locales *}
1.245
1.246 subsection {* A look behind the scene *}
1.247 @@ -335,7 +388,7 @@
1.248 text {* \noindent together with a corresponding interpretation: *}
1.249
1.250 interpretation idem_class:
1.251 - idem ["f \<Colon> ('a\<Colon>idem) \<Rightarrow> \<alpha>"]
1.252 + idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
1.253 by unfold_locales (rule idem)
1.254 (*<*) setup {* Sign.parent_path *} (*>*)
1.255 text {*
1.256 @@ -431,7 +484,7 @@
1.257 *}
1.258
1.259 fun
1.260 - replicate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.261 + replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"
1.262 where
1.263 "replicate 0 _ = []"
1.264 | "replicate (Suc n) xs = xs @ replicate n xs"
1.265 @@ -524,8 +577,9 @@
1.266 text {*
1.267 Turning back to the first motivation for type classes,
1.268 namely overloading, it is obvious that overloading
1.269 - stemming from @{text "\<CLASS>"} and @{text "\<INSTANCE>"}
1.270 - statements naturally maps to Haskell type classes.
1.271 + stemming from @{text "\<CLASS>"} statements and
1.272 + @{text "\<INSTANTIATION>"}
1.273 + targets naturally maps to Haskell type classes.
1.274 The code generator framework \cite{isabelle-codegen}
1.275 takes this into account. Concerning target languages
1.276 lacking type classes (e.g.~SML), type classes
1.277 @@ -533,17 +587,6 @@
1.278 For example, lets go back to the power function:
1.279 *}
1.280
1.281 -(* fun
1.282 - pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
1.283 - "pow_nat 0 x = \<one>"
1.284 - | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
1.285 -
1.286 - definition
1.287 - pow_int :: "int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
1.288 - "pow_int k x = (if k >= 0
1.289 - then pow_nat (nat k) x
1.290 - else (pow_nat (nat (- k)) x)\<div>)"*)
1.291 -
1.292 definition
1.293 example :: int where
1.294 "example = pow_int 10 (-2)"
2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 05 04:34:15 2007 +0100
2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 05 14:15:39 2007 +0100
2.3 @@ -166,15 +166,22 @@
2.4 \begin{isamarkuptext}%
2.5 The concrete type \isa{int} is made a \isa{semigroup}
2.6 instance by providing a suitable definition for the class parameter
2.7 - \isa{mult} and a proof for the specification of \isa{assoc}.%
2.8 + \isa{mult} and a proof for the specification of \isa{assoc}.
2.9 + This is accomplished by the \isa{{\isasymINSTANTIATION}} target:%
2.10 \end{isamarkuptext}%
2.11 \isamarkuptrue%
2.12 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.13 +\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
2.14 +\ \ \ \ \isakeyword{begin}\isanewline
2.15 +\isanewline
2.16 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.17 +\isanewline
2.18 +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.19 +\isanewline
2.20 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.21 -\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
2.22 -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
2.23 %
2.24 \isadelimproof
2.25 -\ \ \ \ %
2.26 +\ %
2.27 \endisadelimproof
2.28 %
2.29 \isatagproof
2.30 @@ -198,27 +205,40 @@
2.31 \isadelimproof
2.32 %
2.33 \endisadelimproof
2.34 +\isanewline
2.35 +\isanewline
2.36 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.37 %
2.38 \begin{isamarkuptext}%
2.39 -\noindent From now on, the type-checker will consider \isa{int}
2.40 - as a \isa{semigroup} automatically, i.e.\ any general results
2.41 - are immediately available on concrete instances.
2.42 -
2.43 - Note that the first proof step is the \isa{default} method,
2.44 - which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.
2.45 - This boils down an instantiation judgement to the relevant primitive
2.46 +\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters
2.47 + at a particular instance using common specification tools (here,
2.48 + \isa{{\isasymDEFINITION}}). The concluding \isa{{\isasymINSTANCE}}
2.49 + opens a proof that the given parameters actually conform
2.50 + to the class specification. Note that the first proof step
2.51 + is the \isa{default} method,
2.52 + which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method.
2.53 + This boils down an instance judgement to the relevant primitive
2.54 proof goals and should conveniently always be the first method applied
2.55 in an instantiation proof.
2.56
2.57 + From now on, the type-checker will consider \isa{int}
2.58 + as a \isa{semigroup} automatically, i.e.\ any general results
2.59 + are immediately available on concrete instances.
2.60 \medskip Another instance of \isa{semigroup} are the natural numbers:%
2.61 \end{isamarkuptext}%
2.62 \isamarkuptrue%
2.63 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.64 +\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
2.65 +\ \ \ \ \isakeyword{begin}\isanewline
2.66 +\isanewline
2.67 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.68 +\isanewline
2.69 +\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.70 +\isanewline
2.71 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.72 -\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
2.73 -\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
2.74 %
2.75 \isadelimproof
2.76 -\ \ \ \ %
2.77 +\ %
2.78 \endisadelimproof
2.79 %
2.80 \isatagproof
2.81 @@ -239,6 +259,9 @@
2.82 \isadelimproof
2.83 %
2.84 \endisadelimproof
2.85 +\isanewline
2.86 +\isanewline
2.87 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.88 %
2.89 \isamarkupsubsection{Lifting and parametric types%
2.90 }
2.91 @@ -251,19 +274,25 @@
2.92 using our simple algebra:%
2.93 \end{isamarkuptext}%
2.94 \isamarkuptrue%
2.95 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.96 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
2.97 +\ \ \ \ \isakeyword{begin}\isanewline
2.98 +\isanewline
2.99 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.100 +\isanewline
2.101 +\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.102 +\isanewline
2.103 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.104 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
2.105 -\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymequiv}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.106 %
2.107 \isadelimproof
2.108 -\ \ \ \ %
2.109 +\ %
2.110 \endisadelimproof
2.111 %
2.112 \isatagproof
2.113 \isacommand{proof}\isamarkupfalse%
2.114 \isanewline
2.115 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
2.116 -\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
2.117 +\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
2.118 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
2.119 \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.120 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
2.121 @@ -277,6 +306,9 @@
2.122 \isadelimproof
2.123 %
2.124 \endisadelimproof
2.125 +\ \ \ \ \ \ \isanewline
2.126 +\isanewline
2.127 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.128 %
2.129 \begin{isamarkuptext}%
2.130 \noindent Associativity from product semigroups is
2.131 @@ -308,15 +340,26 @@
2.132 \begin{isamarkuptext}%
2.133 \noindent Again, we prove some instances, by
2.134 providing suitable parameter definitions and proofs for the
2.135 - additional specifications:%
2.136 + additional specifications. Obverve that instantiations
2.137 + for types with the same arity may be simultaneous:%
2.138 \end{isamarkuptext}%
2.139 \isamarkuptrue%
2.140 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.141 +\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
2.142 +\ \ \ \ \isakeyword{begin}\isanewline
2.143 +\isanewline
2.144 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.145 +\isanewline
2.146 +\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.147 +\isanewline
2.148 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.149 +\isanewline
2.150 +\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.151 +\isanewline
2.152 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.153 -\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
2.154 -\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
2.155 %
2.156 \isadelimproof
2.157 -\ \ \ \ %
2.158 +\ %
2.159 \endisadelimproof
2.160 %
2.161 \isatagproof
2.162 @@ -329,26 +372,7 @@
2.163 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
2.164 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
2.165 \ simp\isanewline
2.166 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
2.167 -%
2.168 -\endisatagproof
2.169 -{\isafoldproof}%
2.170 -%
2.171 -\isadelimproof
2.172 -\isanewline
2.173 -%
2.174 -\endisadelimproof
2.175 -\isanewline
2.176 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
2.177 -\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
2.178 -\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
2.179 -%
2.180 -\isadelimproof
2.181 -\ \ \ \ %
2.182 -\endisadelimproof
2.183 -%
2.184 -\isatagproof
2.185 -\isacommand{proof}\isamarkupfalse%
2.186 +\ \ \ \ \isacommand{next}\isamarkupfalse%
2.187 \isanewline
2.188 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
2.189 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
2.190 @@ -363,23 +387,32 @@
2.191 {\isafoldproof}%
2.192 %
2.193 \isadelimproof
2.194 -\isanewline
2.195 %
2.196 \endisadelimproof
2.197 \isanewline
2.198 +\isanewline
2.199 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.200 +\isanewline
2.201 +\isanewline
2.202 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.203 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
2.204 +\ \ \ \ \isakeyword{begin}\isanewline
2.205 +\isanewline
2.206 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.207 +\isanewline
2.208 +\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.209 +\isanewline
2.210 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.211 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
2.212 -\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.213 %
2.214 \isadelimproof
2.215 -\ \ \ \ %
2.216 +\ %
2.217 \endisadelimproof
2.218 %
2.219 \isatagproof
2.220 \isacommand{proof}\isamarkupfalse%
2.221 \isanewline
2.222 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
2.223 -\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
2.224 +\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
2.225 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
2.226 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
2.227 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
2.228 @@ -393,6 +426,9 @@
2.229 \isadelimproof
2.230 %
2.231 \endisadelimproof
2.232 +\isanewline
2.233 +\isanewline
2.234 +\ \ \ \isacommand{end}\isamarkupfalse%
2.235 %
2.236 \begin{isamarkuptext}%
2.237 \noindent Fully-fledged monoids are modelled by another subclass
2.238 @@ -403,11 +439,14 @@
2.239 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
2.240 \ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
2.241 \isanewline
2.242 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.243 +\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
2.244 +\ \ \ \ \isakeyword{begin}\isanewline
2.245 +\isanewline
2.246 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.247 -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
2.248 %
2.249 \isadelimproof
2.250 -\ \ \ \ %
2.251 +\ %
2.252 \endisadelimproof
2.253 %
2.254 \isatagproof
2.255 @@ -420,25 +459,7 @@
2.256 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
2.257 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
2.258 \ simp\isanewline
2.259 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
2.260 -%
2.261 -\endisatagproof
2.262 -{\isafoldproof}%
2.263 -%
2.264 -\isadelimproof
2.265 -\isanewline
2.266 -%
2.267 -\endisadelimproof
2.268 -\isanewline
2.269 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
2.270 -\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
2.271 -%
2.272 -\isadelimproof
2.273 -\ \ \ \ %
2.274 -\endisadelimproof
2.275 -%
2.276 -\isatagproof
2.277 -\isacommand{proof}\isamarkupfalse%
2.278 +\ \ \ \ \isacommand{next}\isamarkupfalse%
2.279 \isanewline
2.280 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
2.281 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
2.282 @@ -453,22 +474,28 @@
2.283 {\isafoldproof}%
2.284 %
2.285 \isadelimproof
2.286 -\isanewline
2.287 %
2.288 \endisadelimproof
2.289 \isanewline
2.290 +\isanewline
2.291 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.292 +\isanewline
2.293 +\isanewline
2.294 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.295 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
2.296 +\ \ \ \ \isakeyword{begin}\isanewline
2.297 +\isanewline
2.298 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.299 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
2.300 %
2.301 \isadelimproof
2.302 -\ \ \ \ %
2.303 +\ %
2.304 \endisadelimproof
2.305 %
2.306 \isatagproof
2.307 \isacommand{proof}\isamarkupfalse%
2.308 \ \isanewline
2.309 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
2.310 -\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
2.311 +\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
2.312 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
2.313 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
2.314 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
2.315 @@ -482,6 +509,9 @@
2.316 \isadelimproof
2.317 %
2.318 \endisadelimproof
2.319 +\isanewline
2.320 +\isanewline
2.321 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.322 %
2.323 \begin{isamarkuptext}%
2.324 \noindent To finish our small algebra example, we add a \isa{group} class
2.325 @@ -493,12 +523,18 @@
2.326 \ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
2.327 \ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
2.328 \isanewline
2.329 +\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
2.330 +\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
2.331 +\ \ \ \ \isakeyword{begin}\isanewline
2.332 +\isanewline
2.333 +\ \ \ \ \isacommand{definition}\isamarkupfalse%
2.334 +\isanewline
2.335 +\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.336 +\isanewline
2.337 \ \ \ \ \isacommand{instance}\isamarkupfalse%
2.338 -\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
2.339 -\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
2.340 %
2.341 \isadelimproof
2.342 -\ \ \ \ %
2.343 +\ %
2.344 \endisadelimproof
2.345 %
2.346 \isatagproof
2.347 @@ -523,6 +559,9 @@
2.348 \isadelimproof
2.349 %
2.350 \endisadelimproof
2.351 +\isanewline
2.352 +\isanewline
2.353 +\ \ \ \ \isacommand{end}\isamarkupfalse%
2.354 %
2.355 \isamarkupsection{Type classes as locales%
2.356 }
2.357 @@ -584,7 +623,7 @@
2.358 \isamarkuptrue%
2.359 \isacommand{interpretation}\isamarkupfalse%
2.360 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
2.361 -\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
2.362 +\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
2.363 %
2.364 \isadelimproof
2.365 %
2.366 @@ -758,7 +797,7 @@
2.367 \isamarkuptrue%
2.368 \ \ \ \ \isacommand{fun}\isamarkupfalse%
2.369 \isanewline
2.370 -\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
2.371 +\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
2.372 \ \ \ \ \isakeyword{where}\isanewline
2.373 \ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
2.374 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
2.375 @@ -897,8 +936,9 @@
2.376 \begin{isamarkuptext}%
2.377 Turning back to the first motivation for type classes,
2.378 namely overloading, it is obvious that overloading
2.379 - stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
2.380 - statements naturally maps to Haskell type classes.
2.381 + stemming from \isa{{\isasymCLASS}} statements and
2.382 + \isa{{\isasymINSTANTIATION}}
2.383 + targets naturally maps to Haskell type classes.
2.384 The code generator framework \cite{isabelle-codegen}
2.385 takes this into account. Concerning target languages
2.386 lacking type classes (e.g.~SML), type classes
3.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 05 04:34:15 2007 +0100
3.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 05 14:15:39 2007 +0100
3.3 @@ -28,6 +28,7 @@
3.4 \newcommand{\isasymSHOWS}{\cmd{shows}}
3.5 \newcommand{\isasymCLASS}{\cmd{class}}
3.6 \newcommand{\isasymINSTANCE}{\cmd{instance}}
3.7 +\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
3.8 \newcommand{\isasymLEMMA}{\cmd{lemma}}
3.9 \newcommand{\isasymPROOF}{\cmd{proof}}
3.10 \newcommand{\isasymQED}{\cmd{qed}}
4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Dec 05 04:34:15 2007 +0100
4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Dec 05 14:15:39 2007 +0100
4.3 @@ -372,17 +372,24 @@
4.4 | "head (x#xs) = x"
4.5
4.6 text {*
4.7 - We provide some instances for our @{text null}:
4.8 + \noindent We provide some instances for our @{text null}:
4.9 *}
4.10
4.11 -instance option :: (type) null
4.12 - "null \<equiv> None" ..
4.13 +instantiation option and list :: (type) null
4.14 +begin
4.15
4.16 -instance list :: (type) null
4.17 - "null \<equiv> []" ..
4.18 +definition
4.19 + "null = None"
4.20 +
4.21 +definition
4.22 + "null = []"
4.23 +
4.24 +instance ..
4.25 +
4.26 +end
4.27
4.28 text {*
4.29 - Constructing a dummy example:
4.30 + \noindent Constructing a dummy example:
4.31 *}
4.32
4.33 definition
5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Dec 05 04:34:15 2007 +0100
5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Dec 05 14:15:39 2007 +0100
5.3 @@ -464,9 +464,20 @@
5.4 We provide some instances for our \isa{null}:%
5.5 \end{isamarkuptext}%
5.6 \isamarkuptrue%
5.7 +\isacommand{instantiation}\isamarkupfalse%
5.8 +\ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
5.9 +\isakeyword{begin}\isanewline
5.10 +\isanewline
5.11 +\isacommand{definition}\isamarkupfalse%
5.12 +\isanewline
5.13 +\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
5.14 +\isanewline
5.15 +\isacommand{definition}\isamarkupfalse%
5.16 +\isanewline
5.17 +\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
5.18 +\isanewline
5.19 \isacommand{instance}\isamarkupfalse%
5.20 -\ option\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
5.21 -\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ None{\isachardoublequoteclose}%
5.22 +%
5.23 \isadelimproof
5.24 \ %
5.25 \endisadelimproof
5.26 @@ -482,22 +493,7 @@
5.27 \endisadelimproof
5.28 \isanewline
5.29 \isanewline
5.30 -\isacommand{instance}\isamarkupfalse%
5.31 -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
5.32 -\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
5.33 -\isadelimproof
5.34 -\ %
5.35 -\endisadelimproof
5.36 -%
5.37 -\isatagproof
5.38 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
5.39 -%
5.40 -\endisatagproof
5.41 -{\isafoldproof}%
5.42 -%
5.43 -\isadelimproof
5.44 -%
5.45 -\endisadelimproof
5.46 +\isacommand{end}\isamarkupfalse%
5.47 %
5.48 \begin{isamarkuptext}%
5.49 Constructing a dummy example:%
6.1 --- a/doc-src/isar.sty Wed Dec 05 04:34:15 2007 +0100
6.2 +++ b/doc-src/isar.sty Wed Dec 05 14:15:39 2007 +0100
6.3 @@ -78,6 +78,7 @@
6.4 \newcommand{\DEFS}{\isarkeyword{defs}}
6.5 \newcommand{\AXCLASS}{\isarkeyword{axclass}}
6.6 \newcommand{\INSTANCE}{\isarkeyword{instance}}
6.7 +\newcommand{\INSTANTIATION}{\isarkeyword{instantiation}}
6.8 \newcommand{\DECLARE}{\isarkeyword{declare}}
6.9 \newcommand{\LEMMAS}{\isarkeyword{lemmas}}
6.10 \newcommand{\THEOREMS}{\isarkeyword{theorems}}