src/HOL/Isar_Examples/Expr_Compiler.thy
changeset 46582 dcc312f22ee8
parent 41818 6d4c3ee8219d
child 55640 abc140f21caa
     1.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 21 21:15:57 2012 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 21 22:50:28 2012 +0100
     1.3 @@ -59,9 +59,7 @@
     1.4  text {* Execution of a list of stack machine instructions is easily
     1.5    defined as follows. *}
     1.6  
     1.7 -primrec
     1.8 -  exec :: "(('adr, 'val) instr) list
     1.9 -    => 'val list => ('adr => 'val) => 'val list"
    1.10 +primrec exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"
    1.11  where
    1.12    "exec [] stack env = stack"
    1.13  | "exec (instr # instrs) stack env =
    1.14 @@ -71,8 +69,7 @@
    1.15      | Apply f => exec instrs (f (hd stack) (hd (tl stack))
    1.16                     # (tl (tl stack))) env)"
    1.17  
    1.18 -definition
    1.19 -  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
    1.20 +definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
    1.21    where "execute instrs env = hd (exec instrs [] env)"
    1.22  
    1.23  
    1.24 @@ -81,8 +78,7 @@
    1.25  text {* We are ready to define the compilation function of expressions
    1.26    to lists of stack machine instructions. *}
    1.27  
    1.28 -primrec
    1.29 -  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
    1.30 +primrec compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
    1.31  where
    1.32    "compile (Variable x) = [Load x]"
    1.33  | "compile (Constant c) = [Const c]"