--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/Isar_Examples/Expr_Compiler.thy
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
Correctness of a simple expression/stack-machine compiler.
*)
@@ -10,32 +10,40 @@
imports Main
begin
-text \<open>This is a (rather trivial) example of program verification. We model a
+text \<open>
+ This is a (rather trivial) example of program verification. We model a
compiler for translating expressions to stack machine instructions, and
- prove its correctness wrt.\ some evaluation semantics.\<close>
+ prove its correctness wrt.\ some evaluation semantics.
+\<close>
subsection \<open>Binary operations\<close>
-text \<open>Binary operations are just functions over some type of values. This is
- both for abstract syntax and semantics, i.e.\ we use a ``shallow
- embedding'' here.\<close>
+text \<open>
+ Binary operations are just functions over some type of values. This is both
+ for abstract syntax and semantics, i.e.\ we use a ``shallow embedding''
+ here.
+\<close>
type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
subsection \<open>Expressions\<close>
-text \<open>The language of expressions is defined as an inductive type,
- consisting of variables, constants, and binary operations on expressions.\<close>
+text \<open>
+ The language of expressions is defined as an inductive type, consisting of
+ variables, constants, and binary operations on expressions.
+\<close>
datatype (dead 'adr, dead 'val) expr =
Variable 'adr
| Constant 'val
| Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
-text \<open>Evaluation (wrt.\ some environment of variable assignments) is defined
- by primitive recursion over the structure of expressions.\<close>
+text \<open>
+ Evaluation (wrt.\ some environment of variable assignments) is defined by
+ primitive recursion over the structure of expressions.
+\<close>
primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where
@@ -46,15 +54,19 @@
subsection \<open>Machine\<close>
-text \<open>Next we model a simple stack machine, with three instructions.\<close>
+text \<open>
+ Next we model a simple stack machine, with three instructions.
+\<close>
datatype (dead 'adr, dead 'val) instr =
Const 'val
| Load 'adr
| Apply "'val binop"
-text \<open>Execution of a list of stack machine instructions is easily defined as
- follows.\<close>
+text \<open>
+ Execution of a list of stack machine instructions is easily defined as
+ follows.
+\<close>
primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
where
@@ -72,8 +84,10 @@
subsection \<open>Compiler\<close>
-text \<open>We are ready to define the compilation function of expressions to
- lists of stack machine instructions.\<close>
+text \<open>
+ We are ready to define the compilation function of expressions to lists of
+ stack machine instructions.
+\<close>
primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
where
@@ -82,8 +96,10 @@
| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
-text \<open>The main result of this development is the correctness theorem for
- \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.\<close>
+text \<open>
+ The main result of this development is the correctness theorem for
+ \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.
+\<close>
lemma exec_append:
"exec (xs @ ys) stack env =
@@ -128,8 +144,8 @@
In the proofs above, the \<open>simp\<close> method does quite a lot of work behind the
scenes (mostly ``functional program execution''). Subsequently, the same
reasoning is elaborated in detail --- at most one recursive function
- definition is used at a time. Thus we get a better idea of what is
- actually going on.
+ definition is used at a time. Thus we get a better idea of what is actually
+ going on.
\<close>
lemma exec_append':