--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Nov 02 11:43:02 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Nov 02 13:58:19 2015 +0100
@@ -10,17 +10,16 @@
imports Main
begin
-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>
+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>
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"
@@ -28,16 +27,15 @@
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>
+ 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
@@ -48,16 +46,15 @@
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
@@ -75,8 +72,8 @@
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
@@ -85,9 +82,8 @@
| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
-text \<open>The main result of this development is the correctness theorem
- for @{text compile}. We first establish a lemma about @{text exec}
- 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 =
@@ -127,11 +123,14 @@
qed
-text \<open>\bigskip In the proofs above, the @{text simp} 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.\<close>
+text \<open>
+ \<^bigskip>
+ 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.
+\<close>
lemma exec_append':
"exec (xs @ ys) stack env = exec ys (exec xs stack env) env"