author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 53015  a1119cf551e8 
child 58620  7435b6a3f72e 
permissions  rwrr 
31678  1 
(*<*)theory Axioms imports Overloading Setup begin(*>*) 
2 

3 
subsection {* Axioms *} 

4 

5 
text {* Attaching axioms to our classes lets us reason on the level of 

6 
classes. The results will be applicable to all types in a class, just 

7 
as in axiomatic mathematics. 

8 

9 
\begin{warn} 

10 
Proofs in this section use structured \emph{Isar} proofs, which are not 

11 
covered in this tutorial; but see \cite{NipkowTYPES02}.% 

12 
\end{warn} *} 

13 

14 
subsubsection {* Semigroups *} 

15 

31682  16 
text{* We specify \emph{semigroups} as subclass of @{class plus}: *} 
31678  17 

18 
class semigroup = plus + 

19 
assumes assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 

20 

21 
text {* \noindent This @{command class} specification requires that 

22 
all instances of @{class semigroup} obey @{fact "assoc:"}~@{prop 

23 
[source] "\<And>x y z \<Colon> 'a\<Colon>semigroup. (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"}. 

10328  24 

31678  25 
We can use this class axiom to derive further abstract theorems 
26 
relative to class @{class semigroup}: *} 

27 

28 
lemma assoc_left: 

29 
fixes x y z :: "'a\<Colon>semigroup" 

30 
shows "x \<oplus> (y \<oplus> z) = (x \<oplus> y) \<oplus> z" 

31 
using assoc by (rule sym) 

32 

33 
text {* \noindent The @{class semigroup} constraint on type @{typ 

34 
"'a"} restricts instantiations of @{typ "'a"} to types of class 

35 
@{class semigroup} and during the proof enables us to use the fact 

36 
@{fact assoc} whose type parameter is itself constrained to class 

31682  37 
@{class semigroup}. The main advantage of classes is that theorems 
38 
can be proved in the abstract and freely reused for each instance. 

31678  39 

40 
On instantiation, we have to give a proof that the given operations 

41 
obey the class axioms: *} 

42 

43 
instantiation nat :: semigroup 

44 
begin 

45 

46 
instance proof 

47 

48 
txt {* \noindent The proof opens with a default proof step, which for 

49 
instance judgements invokes method @{method intro_classes}. *} 

10328  50 

51 

31678  52 
fix m n q :: nat 
53 
show "(m \<oplus> n) \<oplus> q = m \<oplus> (n \<oplus> q)" 

54 
by (induct m) simp_all 

55 
qed 

10328  56 

31678  57 
end 
10328  58 

31678  59 
text {* \noindent Again, the interesting things enter the stage with 
60 
parametric types: *} 

61 

38325  62 
instantiation prod :: (semigroup, semigroup) semigroup 
31678  63 
begin 
10328  64 

31678  65 
instance proof 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset

66 
fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup" 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset

67 
show "p\<^sub>1 \<oplus> p\<^sub>2 \<oplus> p\<^sub>3 = p\<^sub>1 \<oplus> (p\<^sub>2 \<oplus> p\<^sub>3)" 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48985
diff
changeset

68 
by (cases p\<^sub>1, cases p\<^sub>2, cases p\<^sub>3) (simp add: assoc) 
10328  69 

31678  70 
txt {* \noindent Associativity of product semigroups is established 
71 
using the hypothetical associativity @{fact assoc} of the type 

72 
components, which holds due to the @{class semigroup} constraints 

73 
imposed on the type components by the @{command instance} proposition. 

74 
Indeed, this pattern often occurs with parametric types and type 

75 
classes. *} 

10420  76 

31678  77 
qed 
10328  78 

31678  79 
end 
80 

81 
subsubsection {* Monoids *} 

10328  82 

31678  83 
text {* We define a subclass @{text monoidl} (a semigroup with a 
84 
lefthand neutral) by extending @{class semigroup} with one additional 

85 
parameter @{text neutral} together with its property: *} 

10328  86 

31678  87 
class monoidl = semigroup + 
88 
fixes neutral :: "'a" ("\<zero>") 

89 
assumes neutl: "\<zero> \<oplus> x = x" 

10328  90 

31678  91 
text {* \noindent Again, we prove some instances, by providing 
92 
suitable parameter definitions and proofs for the additional 

93 
specifications. *} 

10328  94 

31678  95 
instantiation nat :: monoidl 
96 
begin 

10328  97 

31678  98 
definition 
99 
neutral_nat_def: "\<zero> = (0\<Colon>nat)" 

10328  100 

31678  101 
instance proof 
102 
fix n :: nat 

103 
show "\<zero> \<oplus> n = n" 

104 
unfolding neutral_nat_def by simp 

105 
qed 

10328  106 

31678  107 
end 
10328  108 

31682  109 
text {* \noindent In contrast to the examples above, we here have both 
31678  110 
specification of class operations and a nontrivial instance proof. 
111 

112 
This covers products as well: 

10328  113 
*} 
114 

38325  115 
instantiation prod :: (monoidl, monoidl) monoidl 
31678  116 
begin 
10328  117 

31678  118 
definition 
119 
neutral_prod_def: "\<zero> = (\<zero>, \<zero>)" 

10328  120 

31678  121 
instance proof 
122 
fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl" 

123 
show "\<zero> \<oplus> p = p" 

124 
by (cases p) (simp add: neutral_prod_def neutl) 

125 
qed 

10328  126 

31678  127 
end 
10328  128 

31678  129 
text {* \noindent Fullyfledged monoids are modelled by another 
130 
subclass which does not add new parameters but tightens the 

131 
specification: *} 

10328  132 

31678  133 
class monoid = monoidl + 
134 
assumes neutr: "x \<oplus> \<zero> = x" 

10328  135 

31678  136 
text {* \noindent Corresponding instances for @{typ nat} and products 
137 
are left as an exercise to the reader. *} 

138 

139 
subsubsection {* Groups *} 

10328  140 

31678  141 
text {* \noindent To finish our small algebra example, we add a @{text 
142 
group} class: *} 

10328  143 

31678  144 
class group = monoidl + 
145 
fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80) 

146 
assumes invl: "\<div> x \<oplus> x = \<zero>" 

11196  147 

31678  148 
text {* \noindent We continue with a further example for abstract 
149 
proofs relative to type classes: *} 

11196  150 

31678  151 
lemma left_cancel: 
152 
fixes x y z :: "'a\<Colon>group" 

153 
shows "x \<oplus> y = x \<oplus> z \<longleftrightarrow> y = z" 

154 
proof 

155 
assume "x \<oplus> y = x \<oplus> z" 

156 
then have "\<div> x \<oplus> (x \<oplus> y) = \<div> x \<oplus> (x \<oplus> z)" by simp 

157 
then have "(\<div> x \<oplus> x) \<oplus> y = (\<div> x \<oplus> x) \<oplus> z" by (simp add: assoc) 

158 
then show "y = z" by (simp add: invl neutl) 

159 
next 

160 
assume "y = z" 

161 
then show "x \<oplus> y = x \<oplus> z" by simp 

162 
qed 

10328  163 

31678  164 
text {* \noindent Any @{text "group"} is also a @{text "monoid"}; this 
165 
can be made explicit by claiming an additional subclass relation, 

166 
together with a proof of the logical difference: *} 

10328  167 

31678  168 
instance group \<subseteq> monoid 
169 
proof 

170 
fix x 

171 
from invl have "\<div> x \<oplus> x = \<zero>" . 

172 
then have "\<div> x \<oplus> (x \<oplus> \<zero>) = \<div> x \<oplus> x" 

173 
by (simp add: neutl invl assoc [symmetric]) 

174 
then show "x \<oplus> \<zero> = x" by (simp add: left_cancel) 

175 
qed 

10396  176 

31678  177 
text {* \noindent The proof result is propagated to the type system, 
178 
making @{text group} an instance of @{text monoid} by adding an 

179 
additional edge to the graph of subclass relation; see also 

10396  180 
Figure~\ref{fig:subclass}. 
181 

182 
\begin{figure}[htbp] 

31678  183 
\begin{center} 
184 
\small 

185 
\unitlength 0.6mm 

186 
\begin{picture}(40,60)(0,0) 

187 
\put(20,60){\makebox(0,0){@{text semigroup}}} 

188 
\put(20,40){\makebox(0,0){@{text monoidl}}} 

189 
\put(00,20){\makebox(0,0){@{text monoid}}} 

190 
\put(40,00){\makebox(0,0){@{text group}}} 

191 
\put(20,55){\vector(0,1){10}} 

192 
\put(15,35){\vector(1,1){10}} 

193 
\put(25,35){\vector(1,3){10}} 

194 
\end{picture} 

195 
\hspace{8em} 

196 
\begin{picture}(40,60)(0,0) 

197 
\put(20,60){\makebox(0,0){@{text semigroup}}} 

198 
\put(20,40){\makebox(0,0){@{text monoidl}}} 

199 
\put(00,20){\makebox(0,0){@{text monoid}}} 

200 
\put(40,00){\makebox(0,0){@{text group}}} 

201 
\put(20,55){\vector(0,1){10}} 

202 
\put(15,35){\vector(1,1){10}} 

203 
\put(05,15){\vector(3,1){30}} 

204 
\end{picture} 

205 
\caption{Subclass relationship of monoids and groups: 

206 
before and after establishing the relationship 

207 
@{text "group \<subseteq> monoid"}; transitive edges are left out.} 

208 
\label{fig:subclass} 

209 
\end{center} 

10396  210 
\end{figure} 
211 
*} 

212 

31678  213 
subsubsection {* Inconsistencies *} 
10328  214 

31678  215 
text {* The reader may be wondering what happens if we attach an 
216 
inconsistent set of axioms to a class. So far we have always avoided 

217 
to add new axioms to HOL for fear of inconsistencies and suddenly it 

10328  218 
seems that we are throwing all caution to the wind. So why is there no 
219 
problem? 

220 

31678  221 
The point is that by construction, all type variables in the axioms of 
222 
a \isacommand{class} are automatically constrained with the class 

223 
being defined (as shown for axiom @{thm[source]refl} above). These 

224 
constraints are always carried around and Isabelle takes care that 

225 
they are never lost, unless the type variable is instantiated with a 

226 
type that has been shown to belong to that class. Thus you may be able 

227 
to prove @{prop False} from your axioms, but Isabelle will remind you 

228 
that this theorem has the hidden hypothesis that the class is 

229 
nonempty. 

230 

231 
Even if each individual class is consistent, intersections of 

232 
(unrelated) classes readily become inconsistent in practice. Now we 

233 
know this need not worry us. *} 

234 

235 

236 
subsubsection{* Syntactic Classes and Predefined Overloading *} 

12332  237 

31678  238 
text {* In our algebra example, we have started with a \emph{syntactic 
239 
class} @{class plus} which only specifies operations but no axioms; it 

240 
would have been also possible to start immediately with class @{class 

241 
semigroup}, specifying the @{text "\<oplus>"} operation and associativity at 

242 
the same time. 

10328  243 

31678  244 
Which approach is more appropriate depends. Usually it is more 
245 
convenient to introduce operations and axioms in the same class: then 

246 
the type checker will automatically insert the corresponding class 

247 
constraints whenever the operations occur, reducing the need of manual 

248 
annotations. However, when operations are decorated with popular 

249 
syntax, syntactic classes can be an option to reuse the syntax in 

250 
different contexts; this is indeed the way most overloaded constants 

251 
in HOL are introduced, of which the most important are listed in 

252 
Table~\ref{tab:overloading} in the appendix. Section 

253 
\ref{sec:numericclasses} covers a range of corresponding classes 

254 
\emph{with} axioms. 

10328  255 

31678  256 
Further note that classes may contain axioms but \emph{no} operations. 
257 
An example is class @{class finite} from theory @{theory Finite_Set} 

258 
which specifies a type to be finite: @{lemma [source] "finite (UNIV \<Colon> 'a\<Colon>finite 

259 
set)" by (fact finite_UNIV)}. *} 

260 

10328  261 
(*<*)end(*>*) 