Theory Expressions

Up to index of Isabelle/HOL/IsarTut

theory Expressions = Main:
theory Expressions = Main:

text {* Beginning section 3.3 *}

types 'v binop = "'v => 'v => 'v"

datatype ('a,'v)expr = Cex 'v
                     | Vex 'a
                     | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"

consts value:: "('a,'v)expr => ('a => 'v) => 'v"
"value (Cex v) env = v"
"value (Vex a) env = env a"
"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"

datatype ('a,'v)instr = Const 'v
                      | Load 'a
                      | Apply "'v binop"

consts exec:: "('a,'v)instr list => ('a => 'v) => 'v list => 'v list"

text {* In other words, currying exec with a program (list of
instructions) and an environment gives you a stack transformation
function.  I've taken the liberty of renaming some of the
variables in the definition.  *}

"exec [] env stk = stk"
"exec (i#is) env stk = (case i of
    Const v => exec is env (v#stk)
  | Load a  => exec is env ((env a)#stk)
  | Apply f => exec is env ( (f (hd stk) (hd(tl stk))) # (tl(tl stk)) ))"

consts comp:: "('a,'v)expr => ('a,'v)instr list"
"comp (Cex v) = [Const v]"
"comp (Vex a) = [Load a]"
"comp (Bex f e1 e2) = (comp e2)@(comp e1)@[Apply f]"

lemma sequence[simp]: "!ys stk. exec (xs@ys) env stk =
                        exec ys env (exec xs env stk)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
  fix x xs assume "?P xs" from prems show "?P (x#xs)"
        by (simp split: instr.split)

theorem "exec (comp e) env [] = [value e env]"
proof -
  have "!stk. exec (comp e) env stk = (value e env)#stk" (is "?P e")
  proof (induct e)
    fix v show "?P (Cex v)" by simp
    fix a show "?P (Vex a)" by simp
    fix f e1 e2 assume "?P e1" "?P e2"
    from prems show "?P (Bex f e1 e2)" by simp
  thus ?thesis ..

text {* Trying to write the simplification lemma inline
reveals a real limitation to that approach.  It lets you
express and prove the lemma, name it, and use it.  But
it does not universalize the free variable the way
a top-level lemma declaration does, so you can only
use it once!  If you try to universally quantify xs
in the lemma statement you can't prove it.  Interesting. *}


lemma sequence:

  ALL ys stk. exec (xs @ ys) env stk = exec ys env (exec xs env stk)


  exec (Expressions.comp e) env [] = [value e env]