1 theory Cas13_vezbe_resenja
   2   imports "HOL-Library.Mapping" "HOL-Library.RBT_Mapping"
   3 
   4 begin
   5 
   6 section‹Računanje vrednosti prefiksno zadatog izraza i generisanje koda za stek
   7 mašinu›
   8 
   9 text‹Na sličan način kao što smo definisali tip binarnog drveta, možemo
  10 definisati tip prefiksnog izraza sa unapred definisanim tipom podataka i
  11 dozvoljenim operacijama.›
  12 
  13 subsection‹Prefiksni izraz nad konstantama›
  14 
  15 text‹\paragraph{Prefiksni izraz:} Prefiksno zadat izraz nad konstantama tipa
  16 @{typ ‹nat›}, sa operacijama sabiranja, oduzimanja i množenja (koje ćemo
  17 označiti ‹PlusI›, ‹MinusI›, ‹PutaI›) se može definisati na sledeći način. ›
  18 
  19 datatype 
  20   Izraz = Const nat | PlusI Izraz Izraz | MinusI Izraz Izraz | PutaI Izraz Izraz
  21 
  22 term PlusI ― ‹operator›
  23 term "PlusI (Const 3) (Const 5)" ― ‹primer prefiksno zadatog izraza›
  24 
  25 text‹Ova definicija veoma podseća na implementaciju koja bi mogla da bude
  26 korišćena u jeziku Haskell tako da ćemo parsiranje ovakvog izraza implementirati
  27 na sličan način kao što bi se parsirao aritmetički izraz u Haskell-u.›
  28 
  29 text‹\paragraph{Vrednost izraza:} Sada lako možemo definisati funkciju koja
  30 računa vrednost ovako zadatog izraza. Vrednost izraza koji se sastoji samo od
  31 konstante je upravo ta konstanta, u suprotnom se vrednost izraza računa prema
  32 operatoru koji ga gradi.
  33 
  34 Napomena: kako radimo sa prirodnim brojevima, vrednost oduzimanja će uvek biti
  35 broj koji je veći ili jednak od 0.›
  36 
  37 primrec vrednost :: "Izraz ⇒ nat" where
  38 "vrednost (Const x) = x" |
  39 "vrednost (PlusI i1 i2) = vrednost i1 + vrednost i2" |
  40 "vrednost (PutaI i1 i2) = vrednost i1 * vrednost i2" |
  41 "vrednost (MinusI i1 i2) = vrednost i1 - vrednost i2"
  42 
  43 value "vrednost (PlusI (Const 3) (Const 5))" ― ‹rezultat je 8, primetimo da moramo koristiti 
  44 zagrade oko ovako zapisanog izraza›
  45 value "vrednost (MinusI (Const 3) (Const 5))" ― ‹rezultat je 0›
  46 
  47 text‹Uz ključnu reč \verb!definition! možemo da uvedemo nekoliko definicija:›
  48 
  49 definition x1 :: "Izraz" where 
  50 "x1 = PlusI (Const 3) (Const 5)"
  51 value "vrednost x1" ― ‹rezultat je 8›
  52 
  53 definition x2 :: "Izraz" where 
  54 "x2 = PutaI (Const 3)(MinusI (Const 5) (Const 2))"
  55 value "vrednost x2" ― ‹rezultat je 9›
  56 
  57 definition x3 :: "Izraz" where 
  58 "x3 = PutaI (PlusI (Const 3) (Const 4)) (MinusI (Const 5)(Const 2))"
  59 value "vrednost x3" ― ‹rezultat je 21›
  60 
  61 text‹Na ovaj način smo prikazali kako možemo direktno da izračunamo vrednost
  62 prefiksno zadatog izraza. Sada ćemo pokazati drugi način za računanje ove
  63 vrednosti. Želimo da izgenerišemo program koji bi izračunavao vrednost ovako
  64 zadatog prefiksnog izraza. Prvi korak je definisanje skupa dozvoljenih
  65 operacija.
  66 
  67 \paragraph{Dozvoljene operacije: } Pored operacija nad prirodnim brojevima
  68 (množenje, sabiranje i oduzimanje), potrebno je i da definišemo operaciju
  69 smeštanja elementa na stek. Kako radimo sa prirodnim brojevima, stek možemo
  70 predstaviti uz pomoć liste prirodnih brojeva. Uvešćemo ga uz pomoć ključne reči
  71 \verb!type_synonym!. Na ovaj način dobijamo samo skraćeni zapis za listu
  72 prirodnih brojeva i povećavamo čitljivost našeg koda. Interno, ovakve skraćenice
  73 se u potpunosti raspisuju.›
  74 
  75 datatype Operacija = OpPuta | OpPlus | OpMinus | OpPush nat
  76 
  77 type_synonym Stek = "nat list"
  78 
  79 text‹\paragraph{Primena operacija:} Sve operacije se izvršavaju nad stekom na
  80 uobičajeni način. Operacija smeštanja elementa na stek u stvari dodaje element
  81 na početak steka (odnosno na početak liste) pa možemo korisiti operaciju
  82 dopisivanja elementa na početak liste ‹(#)›. Ostale operacije se izvršavaju nad
  83 dva elementa koja se nalaze na vrhu steka tako što se skidaju ta dva elementa sa
  84 steka, izvršava se data operacija, i na kraju se rezultat vraća na stek.›
  85 
  86 fun izvrsiOp :: "Operacija ⇒ Stek ⇒ Stek" where
  87 "izvrsiOp (OpPush x) xs = x # xs" |
  88 "izvrsiOp OpPuta (x # y # xs) = (x * y) # xs" |
  89 "izvrsiOp OpPlus (x # y # xs) = (x + y) # xs" |
  90 "izvrsiOp OpMinus (x # y # xs) = (x - y) # xs" 
  91 
  92 text‹\paragraph{Prevođenje izraza i generisanje koda za stek mašinu:} Sada
  93 možemo definisati funkciju koja prevodi dati izraz u listu operacija. Upravo
  94 tako ćemo definisati program - lista operacija nad tipom nat. Ovako dobijena
  95 lista operacija se čita zdesna na levo.
  96 
  97 Prevođenje je manje više trivijalno, konstantni izraz se prevodi u operaciju
  98 dodavanja elementa na stek, dok se izraz koji počinje operatorom prevodi u
  99 operaciju nad stekom (koja odgovara tom konkretnom operatoru) nakon čega
 100 rekurzivno prevodimo njegov prvi pa zatim drugi operand.›
 101 
 102 type_synonym Program = "Operacija list"
 103 
 104 primrec prevedi :: "Izraz ⇒ Program" where 
 105 "prevedi (Const x) = [OpPush x]" |
 106 "prevedi (PlusI i1 i2) = [OpPlus] @ prevedi i1 @ prevedi i2" | 
 107 "prevedi (MinusI i1 i2) = [OpMinus] @ prevedi i1 @ prevedi i2" |
 108 "prevedi (PutaI i1 i2) = [OpPuta] @ prevedi i1 @ prevedi i2"
 109 
 110 term prevedi
 111 
 112 text‹Da bismo izgenerisali kod za stek mašinu za dati izraz (‹x1 = PlusI (Const
 113 3) (Const 5)›), prvo ga prevodimo u listu operacija i dobijamo ‹[OpPlus, OpPush
 114 3, OpPush 5]›. Ovako dobijen program čitamo zdesna na levo, što znači da prvo na
 115 stek stavljamo broj 5, nakon čega stavljamo broj 3 pa tek onda operator
 116 sabiranja.›
 117 
 118 value x1
 119 value "prevedi x1"
 120 
 121 text‹U slučaju malo komplikovanijeg izraza ‹x2›, dobijamo naredni program.
 122 Odnosno, prvo na stek stavljamo broj 2, pa broj 5, pa operaciju oduzimanja;
 123 nakon toga stavljamo broj 3 pa operaciju množenja.›
 124 
 125 value x2 ― ‹PutaI (Const 3) (MinusI (Const 5) (Const 2))›
 126 value "prevedi x2" ― ‹[OpPuta, OpPush 3, OpMinus, OpPush 5, OpPush 2]›
 127 
 128 text‹\paragraph{Izvršavanje programa:} Sada je potrebno definisati rekurzivnu
 129 funkciju koja će izvršiti ovako dobijeni program. Da bi se program izvršio
 130 potrebno je da funkcija zna na kom steku ćemo čuvati podatke (na početku je taj
 131 stek prazan). Povratna vrednost ovakve funkcije će se naći na vrhu rezultujućeg
 132 steka ali to ne možemo tako odmah da zapišemo (zapisaćemo kasnije u okviru
 133 leme), pa kao povratni tip očekujemo isto stek.
 134 
 135 Ako nemamo više operacija i naš program je prazan, vraćamo tekuće stanje steka.
 136 Inače pozivamo funkciju \verb!izvrsiOp! da izvrši operaciju koja se nalazi na
 137 početku našeg programa. Tu operaciju ćemo izvršiti nad stekom koji se dobija
 138 rekurzivnim pozivom nad repom liste (tj. rekurzivnim pozivom nad ostatkom
 139 programa). ›
 140 
 141 primrec izvrsiProgram :: "Program ⇒ Stek ⇒ Stek" where
 142 "izvrsiProgram [] s = s" |
 143 "izvrsiProgram (op # p) s = izvrsiOp op (izvrsiProgram p s)"
 144 
 145 text‹Rezultat ovakve funkcije će biti stek koji će imati samo jedan element, i
 146 taj element će upravo biti jednak vrednosti prefiksno zadatog izraza.›
 147 
 148 value x1 
 149 value "vrednost x1" ― ‹rezultat 8›
 150 value "prevedi x1" ― ‹rezultat [OpPlus, OpPush 3, OpPush 5]›
 151 value "izvrsiProgram (prevedi x1) []" ― ‹rezultat [8]›
 152 
 153 text‹Kako je na početku stek prazan, napravićemo školjku oko ovako definisane
 154 funkcije i nazvaćemo je \verb!racunar!. Sada ćemo dokazati da je ovakva
 155 definicija dobra, odnosno da važi teorema ‹hd_racunar_vrednost: "hd (racunar i)
 156 = vrednost i"›.›
 157 
 158 definition racunar where 
 159 "racunar i = izvrsiProgram (prevedi i) []"
 160 
 161 value "racunar x1" ― ‹rezultat [8]›
 162 
 163 text‹U dokazu leme ‹hd_racunar_vrednost›, nakon raspisivanja ove definicije
 164 dobijamo izraz oblika ‹hd (izvrsiProgram (prevedi i) []) = vrednost i›. Odnosno
 165 imamo poziv funkcije ‹izvrsiProgram› na početku izvršavanja, kada je stek
 166 prazan. Prvo ćemo pokušati sa primenom indukcije (prema definiciji tipa ‹izraz›)
 167 i automatskih alata, i vidimo da se sistem zaustavio kod primene funkcije
 168 ‹izvrsiOp› koja menja stanje steka. Kako je u ovoj lemi početno stanje steka
 169 fiksirano na prazan stek, primećujemo da moramo razmotriti šta se dešava kada
 170 stek nije prazan, odnosno kako neko početno stanje steka utiče na vrednost
 171 izraza koji nam je preostao da izračunamo.
 172 
 173 Pošto je izraz koji pokušavamo da dokažemo ‹hd (izvrsiProgram (prevedi i) []) =
 174 vrednost i› u stvari ekvivalentan izrazu ‹izvrsiProgram (prevedi i) [] =
 175 [vrednost i]›, uopštenjem ovog izraza na proizvoljan stek dobijamo lemu
 176 ‹izvrsiProgram_prevedi:› ‹izvrsiProgram (prevedi i) s = vrednost i # s›.
 177 Odnosno, izvršavanje preostalog dela programa ne utiče na prethodno stanje steka
 178 (odnosno na podatke koji se već nalaze na steku), već se rezultat dopisuje na
 179 početak steka.
 180 
 181 U dokazu ove leme ponovo pokušavamo sa indukcijom i automatskim alatima, ali
 182 opet dolazimo u situaciju da pozivamo funkciju koja treba da menja stanje steka.
 183 Kao što smo ranije videli, ovakva situacija se rešava ključnom rečju
 184 ‹arbitrary›. Sada ponovo pokušavamo sa automatskim dokazivačem i vidimo da je
 185 sistem stao kod izraza oblika ‹(izvrsiProgram (prevedi i1 @ prevedi i2) s› pa
 186 formulišemo još jednu dodatnu lemu ‹izvrsiProgram_append›. Leva strana leme se
 187 formuliše prema stanju u kom je sistem stao, i sami treba da zaključimo kako
 188 izgleda desna strana. Naime pošto smo rekli da se program izvršava tako što se
 189 dobijena lista primenjuje zdesna na levo, očekujemo da ova lema tvrdi da se
 190 program koji se dobija nadovezivanjem dva programa ‹p1› i ‹p2› izvršava tako što
 191 se prvo primeni program ‹p2› (na originalni stek) pa nakon toga program ‹p1› (na
 192 stek dobijen primenom programa ‹p2›). Ova lema se automatski dokazuje uz pomoć
 193 indukcije.
 194 
 195 Nakon dodavanja ovih dveju dodatnih lema i njihovog ubacivanja u simplifikator
 196 (ključnom rečju ‹simp›), originalna lema se dokazuje automatski samo uz pomoć
 197 simplifikatora.›
 198 
 199 ― ‹5.3›
 200 lemma izvrsiProgram_append[simp]: 
 201   shows "izvrsiProgram (p1 @ p2) s = izvrsiProgram p1 (izvrsiProgram p2 s)"
 202   apply (induction p1)
 203    apply auto
 204   done
 205 
 206 ― ‹5.2›
 207 lemma izvrsiProgram_prevedi [simp]: 
 208   "izvrsiProgram (prevedi i) s = vrednost i # s"
 209 ― ‹apply (induction i)›
 210 ― ‹apply auto›
 211   apply (induction i arbitrary: s)
 212      apply auto
 213   done
 214 
 215 ― ‹5.1 krećemo odavde›
 216 theorem hd_racunar_vrednost:
 217   shows "hd (racunar i) = vrednost i"
 218   unfolding racunar_def
 219 ― ‹apply (induction i)›
 220 ― ‹apply auto›
 221   by simp
 222 
 223 
 224 subsection‹Prefiksni izraz sa promenljivima›
 225 
 226 text‹Sada želimo da definišemo prefiksni izraz u kome se mogu javljati i
 227 promenljive. Znači pored konstanti tipa možemo imati i promenjive tipa @{typ
 228 ‹nat›}, ali da bismo naglasili da je to tip koji odgovara promenjivi uvešćemo ga
 229 preko sinonima.
 230 
 231 Napomena: da ne bismo imali konflikt sa prethodnim definicijama koristićemo nova
 232 imena za tipove i operatore.›
 233 
 234 type_synonym var_num = nat
 235 datatype exp = Var var_num | Con int | Add exp exp | Mult exp exp | Minus exp exp
 236 
 237 text‹Sada je potrebno zadati vrednosti promeljivima koje se javljaju u izrazu.
 238 Prvi način je zadavanjem funkcije koja će te promenljive slikati u cele brojeve.
 239 Zbog jednostavnosti, pretpostavimo da se u izrazu javljaju samo naredne
 240 promenljive: x0 = 1; x1 = 2; x2 = 3. Njihove vrednosti ćemo zadati preko naredne
 241 definicije.›
 242 
 243 definition val1 :: "var_num ⇒ int" where
 244   "val1 x = (if x = 0 then 1 else if x = 1 then 2 else 3)"
 245 
 246 text‹Sada ćemo definisati funkciju koja izračunava vrednost ovako zadatog
 247 izraza. U odnosu na inicijalni primer prefiksnog izraza u kome smo imali samo
 248 konstante, ova funkcija mora imati dodatni parametar - funkciju ‹f› koja slika
 249 promenljive u njihove stvarne vrednost.›
 250 
 251 primrec value_exp :: "exp ⇒ (var_num ⇒ int) ⇒ int" where 
 252 "value_exp (Var x) f = f x" |
 253 "value_exp (Con y) f = y" |
 254 "value_exp (Add exp1 exp2) f = (value_exp exp1 f) + (value_exp exp2 f)" |
 255 "value_exp (Mult exp1 exp2) f = (value_exp exp1 f) * (value_exp exp2 f)" |
 256 "value_exp (Minus exp1 exp2) f = (value_exp exp1 f) - (value_exp exp2 f)" 
 257 
 258 text‹Ovako definisana funkcija će se pozivati na naredni način. Koristićemo
 259 funkciju ‹val1› koju smo već definisali.›
 260 
 261 value "value_exp (Add (Con 2) (Var 1)) val1" ― ‹vrednost 4›
 262 definition x4 :: "exp" where "x4 = Add (Con 2) (Var 0)"
 263 value "value_exp x4 val1" ― ‹vrednost 3›
 264 
 265 text‹Naredni korak je definisanje dozvoljenih operacija. Kako sada radimo i sa
 266 promenljivima, biće potrebno dodati posebnu operaciju koja čita vrednost te
 267 promenljive. Stek se definiše na isti način kao ranije, lista (u ovom slučaju)
 268 celih brojeva.›
 269 
 270 datatype Operation = OpAdd | OpMult | OpMin | OpPush int | OpRead var_num 
 271 
 272 type_synonym Stack = "int list"
 273 
 274 text‹I prilikom implementacije funkcije koja izvršava jednu operaciju moramo
 275 imati dodatni argument, funkciju koja slika promenljive u celobrojne vrednosti
 276 (za slučaj kada naiđemo na promenljivu).›
 277 
 278 fun executeOp :: "Operation ⇒ Stack ⇒ (var_num ⇒ int) ⇒ Stack" where
 279 "executeOp OpMult (x # y # xs) f = (x * y) # xs" |
 280 "executeOp OpAdd (x # y # xs) f = (x + y) # xs" |
 281 "executeOp OpMin (x # y # xs) f = (x - y) # xs" |
 282 "executeOp (OpPush x) xs f = (x # xs)" |
 283 "executeOp (OpRead v) xs f = (f v # xs)"
 284 
 285 text‹Program i prevođenje izraza u program se izvršava slično kao ranije.›
 286 
 287 type_synonym Prog = "Operation list"
 288 
 289 primrec translate :: "exp ⇒ Prog" where
 290 "translate (Var x)  = [OpRead x]" |
 291 "translate (Con c) = [OpPush c]" |
 292 "translate (Add e1 e2) = [OpAdd] @ translate e1 @ translate e2" |
 293 "translate (Minus e1 e2) = [OpMin] @ translate e1 @ translate e2" |
 294 "translate (Mult e1 e2) = [OpMult] @ translate e1 @ translate e2" 
 295 
 296 text‹Funkcija koja izvršava program takođe ima kao dodatni argument funkciju
 297 koja slika promenljive u celobrojne vrednosti.›
 298 
 299 primrec executeProg :: "Prog ⇒ Stack ⇒ (var_num ⇒ int) ⇒ Stack" where
 300 "executeProg [] s f = s" |
 301 "executeProg (op # p) s f = executeOp op (executeProg p s f) f"
 302 
 303 text‹Poziv ovako definisanih funkcija:›
 304 
 305 value "x4" ― ‹Add (Con 2) (Var 0)›
 306 value "value_exp x4 val1" ― ‹vrednost 3›
 307 value "translate x4" ― ‹[OpAdd, Operation.OpPush 2, OpRead 0]›
 308 value "executeProg (translate x4) [] val1" ― ‹rezultat [3]›
 309 
 310 text‹Sada ćemo uvesti narednu definiciju i dokazati (na sličan način kao u
 311 prethodnom primeru) da je ta definicija dobro definisana.›
 312 
 313 definition computer where 
 314 "computer i f = executeProg (translate i) [] f"
 315 
 316 lemma executeProg_append[simp]: 
 317   shows "executeProg (p1 @ p2) s f = executeProg p1 (executeProg p2 s f) f"
 318   apply (induction p1)
 319    apply auto
 320 done
 321 
 322 lemma executeProg_translate[simp]: 
 323   shows "executeProg (translate i) s f = (value_exp i f) # s"
 324   apply (induction i arbitrary: s)
 325       apply auto
 326 done
 327 
 328 theorem "hd(computer i f) = value_exp i f"
 329   unfolding computer_def
 330 by simp
 331 
 332 
 333 subsection ‹Interpretator koji izračunava vrednost izraza›
 334 
 335 text‹Prethodno rešenje sa korišćenjem funkcije se može uopštiti. Sada ćemo
 336 prikazati kako možemo vrednosti promenljivih da čuvamo u mapi koja će biti
 337 korišćena da imena promenljivih preslika u njihove stvarne vrednosti.›
 338 
 339 type_synonym var_num' = nat
 340 datatype exp' = Var var_num' | Const int | Add exp' exp' | Mult exp' exp' | Minus exp' exp'
 341 
 342 
 343 ― ‹Čitanje iz memorije ćemo implementirati preko tabele koja će biti
 344 predstavljena uz pomoć mapa. Uključujemo teoriju ‹HOL-Library.Mapping›.
 345 
 346 @{url ‹https://isabelle.in.tum.de/library/HOL/HOL-Library/Mapping.html›}›
 347 
 348 text‹Mapa je predstavljena kao skup uređenih parova, što zapisujemo na sledeći
 349 način:›
 350 
 351 type_synonym Memory = "(nat, int) mapping"
 352 
 353 text‹Za čitanje iz mape koristićemo funkciju ‹lookup_default› koja je
 354 implementirana tako da vraća svoj prvi argument (podrazumevanu, default
 355 vrednost) ako u mapi ne postoji uređeni par koji odgovara vrednosti koja se
 356 traži.›
 357 
 358 definition read_memory where
 359   "read_memory m x = Mapping.lookup_default 0 m x"
 360 
 361 text‹Funkcija koja izračunava vrednost izraza tako što čita vrednosti
 362 promenljivih iz memorije se može implementirati na sledeći način:›
 363 
 364 primrec value_exp_map:: "exp' ⇒ Memory ⇒ int" where
 365 "value_exp_map (Var x) m = read_memory m x" |
 366 "value_exp_map (Const y) m = y" |
 367 "value_exp_map (Add exp1 exp2) m = (value_exp_map exp1 m) + (value_exp_map exp2 m)" |
 368 "value_exp_map (Mult exp1 exp2) m = (value_exp_map exp1 m) * (value_exp_map exp2 m)" |
 369 "value_exp_map (Minus exp1 exp2) m = (value_exp_map exp1 m) - (value_exp_map exp2 m)"
 370 
 371 text‹Za popunjavanje memorije koristimo funkciju 
 372 \verb!bulkload :: "'a list ⇒ (nat, 'a) mapping"! 
 373 koja datu listu preslikava u stanje u memoriji. Ovaj poziv
 374 odgovara vrednostima promenljivih koje smo koristili u prethodnom primeru.›
 375 
 376 definition val_map1 :: "Memory" where
 377   "val_map1 = Mapping.bulkload [1,2,3]"
 378 
 379 text ‹Uključujemo RBT stabla da bi moglo da izvrši računanje, teoriju
 380 ‹RBT_Mapping›. ›
 381 
 382 value "value_exp_map (Mult (Var 2) (Add (Const 2) (Const 5))) val_map1"
 383 
 384 definition x5 :: "exp'" where "x5 = Add (Var 0) (Const 3)"
 385 value "value_exp_map x5 val_map1"
 386 
 387 definition x6 :: "exp'" where "x6 = Mult (Var 0) (Add (Const 2) (Const 5))"
 388 value "value_exp_map x6 val_map1"
 389 
 390 text ‹Uvodimo novu operaciju čitanja iz memorije: ›
 391 
 392 datatype Operation' = OpAdd | OpMult | OpMin | OpPush int | OpRead var_num 
 393 type_synonym Stack' = "int list"
 394 
 395 fun executeOp' :: "Operation' ⇒ Stack' ⇒ Memory ⇒ Stack'" where
 396 "executeOp' OpMult (x # y # xs) m = (x * y) # xs" | 
 397 "executeOp' OpAdd (x # y # xs) m = (x + y) # xs" | 
 398 "executeOp' OpMin (x # y # xs) m = (x - y) # xs" | 
 399 "executeOp' (OpPush x) xs m = (x # xs)" | 
 400 "executeOp' (OpRead x) xs m = ((read_memory m x) # xs)"
 401 
 402 text‹Uvodimo program, prevođenje izraza u program i njegovo izvršavanje:›
 403 
 404 type_synonym Prog' = "Operation' list"
 405 
 406 primrec translate' :: "exp' ⇒ Prog'" where
 407 "translate' (Var x) = [OpRead x]" | 
 408 "translate' (Const x) = [OpPush x]" | 
 409 "translate' (Add i1 i2) = [OpAdd] @ translate' i1 @ translate' i2" | 
 410 "translate' (Minus i1 i2) = [OpMin] @ translate' i1 @ translate' i2" | 
 411 "translate' (Mult i1 i2) = [OpMult] @ translate' i1 @ translate' i2"
 412 
 413 primrec executeProg' :: "Prog' ⇒ Stack' ⇒ Memory ⇒ Stack'" where
 414 "executeProg' [] s m = s" | 
 415 "executeProg' (op # p) s m = executeOp' op (executeProg' p s m) m"
 416 
 417 value "x5"
 418 value "value_exp_map x5 val_map1"
 419 value "translate' x5"
 420 value "executeProg' (translate' x5) [] val_map1"
 421 
 422 text‹Na sličan način kao u prethodna dva primera uvodimo narednu definiciju i
 423 dokazujemo da je dobro definisana:›
 424 
 425 definition computer_map where 
 426 "computer_map i m = executeProg' (translate' i) [] m"
 427 
 428 lemma executeProg'_append[simp]: 
 429   shows "executeProg' (p1 @ p2) s m = executeProg' p1 (executeProg' p2 s m) m"
 430   apply (induction p1)
 431    apply auto
 432 done
 433 
 434 lemma executeProg'_translate[simp]: 
 435   shows "executeProg' (translate' i) s m = (value_exp_map i m) # s"
 436   apply (induction i arbitrary: s)
 437       apply auto
 438 done
 439 
 440 theorem "hd(computer_map i m) = value_exp_map i m"
 441   unfolding computer_map_def
 442 by simp
 443 
 444 end
 445