doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
changeset 28714 1992553cccfe
parent 28566 be2a72b421ae
child 28727 185110a4b97a
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 31 10:39:04 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 03 14:15:25 2008 +0100
     1.3 @@ -1116,69 +1116,69 @@
     1.4  \begin{isamarkuptext}%
     1.5  \isaverbatim%
     1.6  \noindent%
     1.7 -\verb|module Example where {|\newline%
     1.8 -\newline%
     1.9 -\newline%
    1.10 -\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
    1.11 -\newline%
    1.12 -\verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
    1.13 -\verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
    1.14 -\newline%
    1.15 -\verb|nat :: Integer -> Nat;|\newline%
    1.16 -\verb|nat i = nat_aux i Zero_nat;|\newline%
    1.17 -\newline%
    1.18 -\verb|class Semigroup a where {|\newline%
    1.19 -\verb|  mult :: a -> a -> a;|\newline%
    1.20 -\verb|};|\newline%
    1.21 -\newline%
    1.22 -\verb|class (Semigroup a) => Monoidl a where {|\newline%
    1.23 -\verb|  neutral :: a;|\newline%
    1.24 -\verb|};|\newline%
    1.25 -\newline%
    1.26 -\verb|class (Monoidl a) => Monoid a where {|\newline%
    1.27 -\verb|};|\newline%
    1.28 -\newline%
    1.29 -\verb|class (Monoid a) => Group a where {|\newline%
    1.30 -\verb|  inverse :: a -> a;|\newline%
    1.31 -\verb|};|\newline%
    1.32 -\newline%
    1.33 -\verb|inverse_int :: Integer -> Integer;|\newline%
    1.34 -\verb|inverse_int i = negate i;|\newline%
    1.35 -\newline%
    1.36 -\verb|neutral_int :: Integer;|\newline%
    1.37 -\verb|neutral_int = 0;|\newline%
    1.38 -\newline%
    1.39 -\verb|mult_int :: Integer -> Integer -> Integer;|\newline%
    1.40 -\verb|mult_int i j = i + j;|\newline%
    1.41 -\newline%
    1.42 -\verb|instance Semigroup Integer where {|\newline%
    1.43 -\verb|  mult = mult_int;|\newline%
    1.44 -\verb|};|\newline%
    1.45 -\newline%
    1.46 -\verb|instance Monoidl Integer where {|\newline%
    1.47 -\verb|  neutral = neutral_int;|\newline%
    1.48 -\verb|};|\newline%
    1.49 -\newline%
    1.50 -\verb|instance Monoid Integer where {|\newline%
    1.51 -\verb|};|\newline%
    1.52 -\newline%
    1.53 -\verb|instance Group Integer where {|\newline%
    1.54 -\verb|  inverse = inverse_int;|\newline%
    1.55 -\verb|};|\newline%
    1.56 -\newline%
    1.57 -\verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
    1.58 -\verb|pow_nat Zero_nat x = neutral;|\newline%
    1.59 -\verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
    1.60 -\newline%
    1.61 -\verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
    1.62 -\verb|pow_int k x =|\newline%
    1.63 -\verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
    1.64 -\verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
    1.65 -\newline%
    1.66 -\verb|example :: Integer;|\newline%
    1.67 -\verb|example = pow_int 10 (-2);|\newline%
    1.68 -\newline%
    1.69 -\verb|}|%
    1.70 +\hspace*{0pt}module Example where {\char123}\\
    1.71 +\hspace*{0pt}\\
    1.72 +\hspace*{0pt}\\
    1.73 +\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
    1.74 +\hspace*{0pt}\\
    1.75 +\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
    1.76 +\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
    1.77 +\hspace*{0pt}\\
    1.78 +\hspace*{0pt}nat ::~Integer -> Nat;\\
    1.79 +\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
    1.80 +\hspace*{0pt}\\
    1.81 +\hspace*{0pt}class Semigroup a where {\char123}\\
    1.82 +\hspace*{0pt} ~mult ::~a -> a -> a;\\
    1.83 +\hspace*{0pt}{\char125};\\
    1.84 +\hspace*{0pt}\\
    1.85 +\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
    1.86 +\hspace*{0pt} ~neutral ::~a;\\
    1.87 +\hspace*{0pt}{\char125};\\
    1.88 +\hspace*{0pt}\\
    1.89 +\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
    1.90 +\hspace*{0pt}{\char125};\\
    1.91 +\hspace*{0pt}\\
    1.92 +\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
    1.93 +\hspace*{0pt} ~inverse ::~a -> a;\\
    1.94 +\hspace*{0pt}{\char125};\\
    1.95 +\hspace*{0pt}\\
    1.96 +\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
    1.97 +\hspace*{0pt}inverse{\char95}int i = negate i;\\
    1.98 +\hspace*{0pt}\\
    1.99 +\hspace*{0pt}neutral{\char95}int ::~Integer;\\
   1.100 +\hspace*{0pt}neutral{\char95}int = 0;\\
   1.101 +\hspace*{0pt}\\
   1.102 +\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
   1.103 +\hspace*{0pt}mult{\char95}int i j = i + j;\\
   1.104 +\hspace*{0pt}\\
   1.105 +\hspace*{0pt}instance Semigroup Integer where {\char123}\\
   1.106 +\hspace*{0pt} ~mult = mult{\char95}int;\\
   1.107 +\hspace*{0pt}{\char125};\\
   1.108 +\hspace*{0pt}\\
   1.109 +\hspace*{0pt}instance Monoidl Integer where {\char123}\\
   1.110 +\hspace*{0pt} ~neutral = neutral{\char95}int;\\
   1.111 +\hspace*{0pt}{\char125};\\
   1.112 +\hspace*{0pt}\\
   1.113 +\hspace*{0pt}instance Monoid Integer where {\char123}\\
   1.114 +\hspace*{0pt}{\char125};\\
   1.115 +\hspace*{0pt}\\
   1.116 +\hspace*{0pt}instance Group Integer where {\char123}\\
   1.117 +\hspace*{0pt} ~inverse = inverse{\char95}int;\\
   1.118 +\hspace*{0pt}{\char125};\\
   1.119 +\hspace*{0pt}\\
   1.120 +\hspace*{0pt}pow{\char95}nat ::~forall a. (Monoid a) => Nat -> a -> a;\\
   1.121 +\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
   1.122 +\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
   1.123 +\hspace*{0pt}\\
   1.124 +\hspace*{0pt}pow{\char95}int ::~forall a. (Group a) => Integer -> a -> a;\\
   1.125 +\hspace*{0pt}pow{\char95}int k x =\\
   1.126 +\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
   1.127 +\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
   1.128 +\hspace*{0pt}\\
   1.129 +\hspace*{0pt}example ::~Integer;\\
   1.130 +\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
   1.131 +\hspace*{0pt}\\
   1.132 +\hspace*{0pt}{\char125}%
   1.133  \end{isamarkuptext}%
   1.134  \isamarkuptrue%
   1.135  %
   1.136 @@ -1203,64 +1203,64 @@
   1.137  \begin{isamarkuptext}%
   1.138  \isaverbatim%
   1.139  \noindent%
   1.140 -\verb|structure Example = |\newline%
   1.141 -\verb|struct|\newline%
   1.142 -\newline%
   1.143 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   1.144 -\newline%
   1.145 -\verb|fun nat_aux i n =|\newline%
   1.146 -\verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
   1.147 -\verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
   1.148 -\newline%
   1.149 -\verb|fun nat i = nat_aux i Zero_nat;|\newline%
   1.150 -\newline%
   1.151 -\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
   1.152 -\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
   1.153 -\newline%
   1.154 -\verb|type 'a monoidl =|\newline%
   1.155 -\verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
   1.156 -\verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
   1.157 -\verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
   1.158 -\newline%
   1.159 -\verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
   1.160 -\verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
   1.161 -\newline%
   1.162 -\verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
   1.163 -\verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
   1.164 -\verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
   1.165 -\newline%
   1.166 -\verb|fun inverse_int i = IntInf.~ i;|\newline%
   1.167 -\newline%
   1.168 -\verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
   1.169 -\newline%
   1.170 -\verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
   1.171 -\newline%
   1.172 -\verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
   1.173 -\newline%
   1.174 -\verb|val monoidl_int =|\newline%
   1.175 -\verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
   1.176 -\verb|  IntInf.int monoidl;|\newline%
   1.177 -\newline%
   1.178 -\verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
   1.179 -\verb|  IntInf.int monoid;|\newline%
   1.180 -\newline%
   1.181 -\verb|val group_int =|\newline%
   1.182 -\verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
   1.183 -\verb|  IntInf.int group;|\newline%
   1.184 -\newline%
   1.185 -\verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
   1.186 -\verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
   1.187 -\verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
   1.188 -\newline%
   1.189 -\verb|fun pow_int A_ k x =|\newline%
   1.190 -\verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
   1.191 -\verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
   1.192 -\verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
   1.193 -\newline%
   1.194 -\verb|val example : IntInf.int =|\newline%
   1.195 -\verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline%
   1.196 -\newline%
   1.197 -\verb|end; (*struct Example*)|%
   1.198 +\hspace*{0pt}structure Example = \\
   1.199 +\hspace*{0pt}struct\\
   1.200 +\hspace*{0pt}\\
   1.201 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   1.202 +\hspace*{0pt}\\
   1.203 +\hspace*{0pt}fun nat{\char95}aux i n =\\
   1.204 +\hspace*{0pt} ~(if IntInf.<= (i, (0 :~IntInf.int)) then n\\
   1.205 +\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i, (1 :~IntInf.int))) (Suc n));\\
   1.206 +\hspace*{0pt}\\
   1.207 +\hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
   1.208 +\hspace*{0pt}\\
   1.209 +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
   1.210 +\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
   1.211 +\hspace*{0pt}\\
   1.212 +\hspace*{0pt}type 'a monoidl =\\
   1.213 +\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup, neutral :~'a{\char125};\\
   1.214 +\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
   1.215 +\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
   1.216 +\hspace*{0pt}\\
   1.217 +\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
   1.218 +\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
   1.219 +\hspace*{0pt}\\
   1.220 +\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid, inverse :~'a -> 'a{\char125};\\
   1.221 +\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
   1.222 +\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
   1.223 +\hspace*{0pt}\\
   1.224 +\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
   1.225 +\hspace*{0pt}\\
   1.226 +\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
   1.227 +\hspace*{0pt}\\
   1.228 +\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i, j);\\
   1.229 +\hspace*{0pt}\\
   1.230 +\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
   1.231 +\hspace*{0pt}\\
   1.232 +\hspace*{0pt}val monoidl{\char95}int =\\
   1.233 +\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int, neutral = neutral{\char95}int{\char125}~:\\
   1.234 +\hspace*{0pt} ~IntInf.int monoidl;\\
   1.235 +\hspace*{0pt}\\
   1.236 +\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
   1.237 +\hspace*{0pt} ~IntInf.int monoid;\\
   1.238 +\hspace*{0pt}\\
   1.239 +\hspace*{0pt}val group{\char95}int =\\
   1.240 +\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int, inverse = inverse{\char95}int{\char125}~:\\
   1.241 +\hspace*{0pt} ~IntInf.int group;\\
   1.242 +\hspace*{0pt}\\
   1.243 +\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
   1.244 +\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
   1.245 +\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
   1.246 +\hspace*{0pt}\\
   1.247 +\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
   1.248 +\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int), k)\\
   1.249 +\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
   1.250 +\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
   1.251 +\hspace*{0pt}\\
   1.252 +\hspace*{0pt}val example :~IntInf.int =\\
   1.253 +\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
   1.254 +\hspace*{0pt}\\
   1.255 +\hspace*{0pt}end; (*struct Example*)%
   1.256  \end{isamarkuptext}%
   1.257  \isamarkuptrue%
   1.258  %