Up to index of Isabelle/HOL/IsarTut

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" primrec "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. *} primrec "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" primrec "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 next fix x xs assume "?P xs" from prems show "?P (x#xs)" by (simp split: instr.split) qed 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 next fix a show "?P (Vex a)" by simp next fix f e1 e2 assume "?P e1" "?P e2" from prems show "?P (Bex f e1 e2)" by simp qed thus ?thesis .. qed 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. *} end

**lemma** *sequence:*

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

**theorem**

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