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  %