# HG changeset patch # User wenzelm # Date 943446974 -3600 # Node ID 826c6222cca2fa475b9df4728ba7795ab9860947 # Parent af8db187296040b56b21abd37b95289057ac1a13 renamed comp to compile (avoids clash with Relation.comp); diff -r af8db1872960 -r 826c6222cca2 src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Wed Nov 24 13:35:31 1999 +0100 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Nov 24 13:36:14 1999 +0100 @@ -97,17 +97,17 @@ *}; consts - comp :: "('adr, 'val) expr => (('adr, 'val) instr) list"; + compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"; primrec - "comp (Variable x) = [Load x]" - "comp (Constant c) = [Const c]" - "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]"; + "compile (Variable x) = [Load x]" + "compile (Constant c) = [Const c]" + "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"; text {* The main result of this development is the correctness theorem for - $\idt{comp}$. We first establish some lemmas about $\idt{exec}$. + $\idt{compile}$. We first establish some lemmas about $\idt{exec}$. *}; lemma exec_append: @@ -128,8 +128,8 @@ qed; qed; -lemma exec_comp: - "ALL stack. exec (comp e) stack env = +lemma exec_compile: + "ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e"); proof (induct ?P e type: expr); fix adr; show "?P (Variable adr)"; by (simp!); @@ -143,7 +143,7 @@ text {* Main theorem ahead. *}; -theorem correctness: "execute (comp e) env = eval e env"; - by (simp add: execute_def exec_comp); +theorem correctness: "execute (compile e) env = eval e env"; + by (simp add: execute_def exec_compile); end;