--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/AExp.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,85 @@
+header "Arithmetic and Boolean Expressions"
+
+theory AExp imports Main begin
+
+subsection "Arithmetic Expressions"
+
+type_synonym name = string
+type_synonym val = int
+type_synonym state = "name \<Rightarrow> val"
+
+datatype aexp = N int | V name | Plus aexp aexp
+
+fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
+"aval (N n) _ = n" |
+"aval (V x) s = s x" |
+"aval (Plus a1 a2) s = aval a1 s + aval a2 s"
+
+
+value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
+
+fun lookup :: "(string * val)list \<Rightarrow> string \<Rightarrow> val" where
+"lookup ((x,i)#xis) y = (if x=y then i else lookup xis y)"
+
+value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])"
+
+value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])"
+
+
+subsection "Optimization"
+
+text{* Evaluate constant subsexpressions: *}
+
+fun asimp_const :: "aexp \<Rightarrow> aexp" where
+"asimp_const (N n) = N n" |
+"asimp_const (V x) = V x" |
+"asimp_const (Plus a1 a2) =
+ (case (asimp_const a1, asimp_const a2) of
+ (N n1, N n2) \<Rightarrow> N(n1+n2) |
+ (a1',a2') \<Rightarrow> Plus a1' a2')"
+
+theorem aval_asimp_const[simp]:
+ "aval (asimp_const a) s = aval a s"
+apply(induct a)
+apply (auto split: aexp.split)
+done
+
+text{* Now we also eliminate all occurrences 0 in additions. The standard
+method: optimized versions of the constructors: *}
+
+fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
+"plus (N i1) (N i2) = N(i1+i2)" |
+"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
+"plus a (N i) = (if i=0 then a else Plus a (N i))" |
+"plus a1 a2 = Plus a1 a2"
+
+text ""
+code_thms plus
+code_thms plus
+
+(* FIXME: dropping subsumed code eqns?? *)
+lemma aval_plus[simp]:
+ "aval (plus a1 a2) s = aval a1 s + aval a2 s"
+apply(induct a1 a2 rule: plus.induct)
+apply simp_all (* just for a change from auto *)
+done
+code_thms plus
+
+fun asimp :: "aexp \<Rightarrow> aexp" where
+"asimp (N n) = N n" |
+"asimp (V x) = V x" |
+"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
+
+text{* Note that in @{const asimp_const} the optimized constructor was
+inlined. Making it a separate function @{const plus} improves modularity of
+the code and the proofs. *}
+
+value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
+
+theorem aval_asimp[simp]:
+ "aval (asimp a) s = aval a s"
+apply(induct a)
+apply simp_all
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/ASM.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,51 @@
+header "Arithmetic Stack Machine and Compilation"
+
+theory ASM imports AExp begin
+
+subsection "Arithmetic Stack Machine"
+
+datatype ainstr = LOADI val | LOAD string | ADD
+
+type_synonym stack = "val list"
+
+abbreviation "hd2 xs == hd(tl xs)"
+abbreviation "tl2 xs == tl(tl xs)"
+
+text{* \noindent Abbreviations are transparent: they are unfolded after
+parsing and folded back again before printing. Internally, they do not
+exist. *}
+
+fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
+"aexec1 (LOADI n) _ stk = n # stk" |
+"aexec1 (LOAD n) s stk = s(n) # stk" |
+"aexec1 ADD _ stk = (hd2 stk + hd stk) # tl2 stk"
+
+fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
+"aexec [] _ stk = stk" |
+"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
+
+value "aexec [LOADI 5, LOAD ''y'', ADD]
+ (lookup[(''x'',42), (''y'',43)]) [50]"
+
+lemma aexec_append[simp]:
+ "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
+apply(induct is1 arbitrary: stk)
+apply (auto)
+done
+
+
+subsection "Compilation"
+
+fun acomp :: "aexp \<Rightarrow> ainstr list" where
+"acomp (N n) = [LOADI n]" |
+"acomp (V x) = [LOAD x]" |
+"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
+
+value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
+
+theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
+apply(induct a arbitrary: stk)
+apply (auto)
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/BExp.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,69 @@
+theory BExp imports AExp begin
+
+subsection "Boolean Expressions"
+
+datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+
+fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
+"bval (B bv) _ = bv" |
+"bval (Not b) s = (\<not> bval b s)" |
+"bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
+"bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
+
+value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
+ (lookup [(''x'',3),(''y'',1)])"
+
+
+subsection "Optimization"
+
+text{* Optimized constructors: *}
+
+fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
+"less (N n1) (N n2) = B(n1 < n2)" |
+"less a1 a2 = Less a1 a2"
+
+lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
+apply(induct a1 a2 rule: less.induct)
+apply simp_all
+done
+
+fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
+"and (B True) b = b" |
+"and b (B True) = b" |
+"and (B False) b = B False" |
+"and b (B False) = B False" |
+"and b1 b2 = And b1 b2"
+
+lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
+apply(induct b1 b2 rule: and.induct)
+apply simp_all
+done
+
+fun not :: "bexp \<Rightarrow> bexp" where
+"not (B True) = B False" |
+"not (B False) = B True" |
+"not b = Not b"
+
+lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
+apply(induct b rule: not.induct)
+apply simp_all
+done
+
+text{* Now the overall optimizer: *}
+
+fun bsimp :: "bexp \<Rightarrow> bexp" where
+"bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
+"bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
+"bsimp (Not b) = not(bsimp b)" |
+"bsimp (B bv) = B bv"
+
+value "bsimp (And (Less (N 0) (N 1)) b)"
+
+value "bsimp (And (Less (N 1) (N 0)) (B True))"
+
+theorem "bval (bsimp b) s = bval b s"
+apply(induct b)
+apply simp_all
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Big_Step.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,243 @@
+(* Author: Gerwin Klein, Tobias Nipkow *)
+
+theory Big_Step imports Com begin
+
+subsection "Big-Step Semantics of Commands"
+
+inductive
+ big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
+where
+Skip: "(SKIP,s) \<Rightarrow> s" |
+Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
+Semi: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+ (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+ (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+ (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+
+WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
+WhileTrue: "\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+ (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
+
+schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
+apply(rule Semi)
+apply(rule Assign)
+apply simp
+apply(rule Assign)
+done
+
+thm ex[simplified]
+
+text{* We want to execute the big-step rules: *}
+
+code_pred big_step .
+
+text{* For inductive definitions we need command
+ \texttt{values} instead of \texttt{value}. *}
+
+values "{t. (SKIP, lookup[]) \<Rightarrow> t}"
+
+text{* We need to translate the result state into a list
+to display it. *}
+
+values "{map t [''x''] |t. (SKIP, lookup [(''x'',42)]) \<Rightarrow> t}"
+
+values "{map t [''x''] |t. (''x'' ::= N 2, lookup [(''x'',42)]) \<Rightarrow> t}"
+
+values "{map t [''x'',''y''] |t.
+ (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
+ lookup [(''x'',0),(''y'',13)]) \<Rightarrow> t}"
+
+
+text{* Proof automation: *}
+
+declare big_step.intros [intro]
+
+text{* The standard induction rule
+@{thm [display] big_step.induct [no_vars]} *}
+
+thm big_step.induct
+
+text{* A customized induction rule for (c,s) pairs: *}
+
+lemmas big_step_induct = big_step.induct[split_format(complete)]
+thm big_step_induct
+text {*
+@{thm [display] big_step_induct [no_vars]}
+*}
+
+
+subsection "Rule inversion"
+
+text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
+That @{prop "s = t"}. This is how we can automatically prove it: *}
+
+inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"
+thm skipE
+
+text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
+blast and friends (but not simp!) to use it automatically; [elim!] means that
+it is applied eagerly.
+
+Similarly for the other commands: *}
+
+inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
+thm AssignE
+inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
+thm SemiE
+inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
+thm IfE
+
+inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
+thm WhileE
+text{* Only [elim]: [elim!] would not terminate. *}
+
+text{* An automatic example: *}
+
+lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
+by blast
+
+text{* Rule inversion by hand via the ``cases'' method: *}
+
+lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
+shows "t = s"
+proof-
+ from assms show ?thesis
+ proof cases --"inverting assms"
+ case IfTrue thm IfTrue
+ thus ?thesis by blast
+ next
+ case IfFalse thus ?thesis by blast
+ qed
+qed
+
+
+subsection "Command Equivalence"
+
+text {*
+ We call two statements @{text c} and @{text c'} equivalent wrt.\ the
+ big-step semantics when \emph{@{text c} started in @{text s} terminates
+ in @{text s'} iff @{text c'} started in the same @{text s} also terminates
+ in the same @{text s'}}. Formally:
+*}
+abbreviation
+ equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
+ "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
+
+text {*
+Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
+
+ As an example, we show that loop unfolding is an equivalence
+ transformation on programs:
+*}
+lemma unfold_while:
+ "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
+proof -
+ -- "to show the equivalence, we look at the derivation tree for"
+ -- "each side and from that construct a derivation tree for the other side"
+ { fix s t assume "(?w, s) \<Rightarrow> t"
+ -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
+ -- "then both statements do nothing:"
+ { assume "\<not>bval b s"
+ hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
+ hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
+ }
+ moreover
+ -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
+ -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
+ { assume "bval b s"
+ with `(?w, s) \<Rightarrow> t` obtain s' where
+ "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
+ -- "now we can build a derivation tree for the @{text IF}"
+ -- "first, the body of the True-branch:"
+ hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
+ -- "then the whole @{text IF}"
+ with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
+ }
+ ultimately
+ -- "both cases together give us what we want:"
+ have "(?iw, s) \<Rightarrow> t" by blast
+ }
+ moreover
+ -- "now the other direction:"
+ { fix s t assume "(?iw, s) \<Rightarrow> t"
+ -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
+ -- "of the @{text IF} is executed, and both statements do nothing:"
+ { assume "\<not>bval b s"
+ hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
+ hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
+ }
+ moreover
+ -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
+ -- {* then this time only the @{text IfTrue} rule can have be used *}
+ { assume "bval b s"
+ with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
+ -- "and for this, only the Semi-rule is applicable:"
+ then obtain s' where
+ "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
+ -- "with this information, we can build a derivation tree for the @{text WHILE}"
+ with `bval b s`
+ have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
+ }
+ ultimately
+ -- "both cases together again give us what we want:"
+ have "(?w, s) \<Rightarrow> t" by blast
+ }
+ ultimately
+ show ?thesis by blast
+qed
+
+text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can
+prove many such facts automatically. *}
+
+lemma
+ "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
+by blast
+
+lemma triv_if:
+ "(IF b THEN c ELSE c) \<sim> c"
+by blast
+
+lemma commute_if:
+ "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)
+ \<sim>
+ (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
+by blast
+
+
+subsection "Execution is deterministic"
+
+text {* This proof is automatic. *}
+theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
+apply (induct arbitrary: u rule: big_step.induct)
+apply blast+
+done
+
+text {*
+ This is the proof as you might present it in a lecture. The remaining
+ cases are simple enough to be proved automatically:
+*}
+theorem
+ "(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t"
+proof (induct arbitrary: t' rule: big_step.induct)
+ -- "the only interesting case, @{text WhileTrue}:"
+ fix b c s s1 t t'
+ -- "The assumptions of the rule:"
+ assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"
+ -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
+ assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"
+ assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"
+ -- "Premise of implication:"
+ assume "(WHILE b DO c,s) \<Rightarrow> t'"
+ with `bval b s` obtain s1' where
+ c: "(c,s) \<Rightarrow> s1'" and
+ w: "(WHILE b DO c,s1') \<Rightarrow> t'"
+ by auto
+ from c IHc have "s1' = s1" by blast
+ with w IHw show "t' = t" by blast
+qed blast+ -- "prove the rest automatically"
+
+
+end
--- a/src/HOL/IMP/Com.thy Wed Jun 01 15:53:47 2011 +0200
+++ b/src/HOL/IMP/Com.thy Wed Jun 01 21:35:34 2011 +0200
@@ -1,33 +1,12 @@
-(* Title: HOL/IMP/Com.thy
- Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
- Author: Gerwin Klein
-*)
-
-header "Syntax of Commands"
-
-theory Com imports Main begin
+header "IMP --- A Simple Imperative Language"
-typedecl loc
- -- "an unspecified (arbitrary) type of locations
- (adresses/names) for variables"
-
-type_synonym val = nat -- "or anything else, @{text nat} used in examples"
-type_synonym state = "loc \<Rightarrow> val"
-type_synonym aexp = "state \<Rightarrow> val"
-type_synonym bexp = "state \<Rightarrow> bool"
- -- "arithmetic and boolean expressions are not modelled explicitly here,"
- -- "they are just functions on states"
+theory Com imports BExp begin
datatype
- com = SKIP
- | Assign loc aexp ("_ :== _ " 60)
- | Semi com com ("_; _" [60, 60] 10)
- | Cond bexp com com ("IF _ THEN _ ELSE _" 60)
- | While bexp com ("WHILE _ DO _" 60)
-
-notation (latex)
- SKIP ("\<SKIP>") and
- Cond ("\<IF> _ \<THEN> _ \<ELSE> _" 60) and
- While ("\<WHILE> _ \<DO> _" 60)
+ com = SKIP
+ | Assign name aexp ("_ ::= _" [1000, 61] 61)
+ | Semi com com ("_;/ _" [60, 61] 60)
+ | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
+ | While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
end
--- a/src/HOL/IMP/Compiler.thy Wed Jun 01 15:53:47 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy Wed Jun 01 21:35:34 2011 +0200
@@ -1,298 +1,237 @@
-(* Title: HOL/IMP/Compiler.thy
- Author: Tobias Nipkow, TUM
- Copyright 1996 TUM
-*)
+(* Author: Tobias Nipkow *)
+
+header "A Compiler for IMP"
-theory Compiler imports Machines begin
+theory Compiler imports Big_Step
+begin
-subsection "The compiler"
+subsection "Instructions and Stack Machine"
-primrec compile :: "com \<Rightarrow> instr list"
-where
- "compile \<SKIP> = []"
-| "compile (x:==a) = [SET x a]"
-| "compile (c1;c2) = compile c1 @ compile c2"
-| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
- [JMPF b (length(compile c1) + 1)] @ compile c1 @
- [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
-| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
- [JMPB (length(compile c)+1)]"
+datatype instr =
+ LOADI int | LOAD string | ADD |
+ STORE string |
+ JMPF nat |
+ JMPB nat |
+ JMPFLESS nat |
+ JMPFGE nat
-subsection "Compiler correctness"
+type_synonym stack = "int list"
+type_synonym config = "nat\<times>state\<times>stack"
+
+abbreviation "hd2 xs == hd(tl xs)"
+abbreviation "tl2 xs == tl(tl xs)"
-theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
- (is "\<And>p q. ?P c s t p q")
-proof -
- from A show "\<And>p q. ?thesis p q"
- proof induct
- case Skip thus ?case by simp
- next
- case Assign thus ?case by force
- next
- case Semi thus ?case by simp (blast intro:rtrancl_trans)
- next
- fix b c0 c1 s0 s1 p q
- assume IH: "\<And>p q. ?P c0 s0 s1 p q"
- assume "b s0"
- thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
- by(simp add: IH[THEN rtrancl_trans])
- next
- case IfFalse thus ?case by(simp)
- next
- case WhileFalse thus ?case by simp
- next
- fix b c and s0::state and s1 s2 p q
- assume b: "b s0" and
- IHc: "\<And>p q. ?P c s0 s1 p q" and
- IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
- show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
- using b IHc[THEN rtrancl_trans] IHw by(simp)
- qed
+inductive exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
+ ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
+ for P :: "instr list"
+where
+"\<lbrakk> i < size P; P!i = LOADI n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
+"\<lbrakk> i < size P; P!i = LOAD x \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
+"\<lbrakk> i < size P; P!i = ADD \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
+"\<lbrakk> i < size P; P!i = STORE n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
+"\<lbrakk> i < size P; P!i = JMPF n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
+"\<lbrakk> i < size P; P!i = JMPB n; n \<le> i+1 \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1-n,s,stk)" |
+"\<lbrakk> i < size P; P!i = JMPFLESS n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
+"\<lbrakk> i < size P; P!i = JMPFGE n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
+
+code_pred exec1 .
+
+declare exec1.intros[intro]
+
+inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
+where
+refl: "P \<turnstile> c \<rightarrow>* c" |
+step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
+
+declare exec.intros[intro]
+
+lemmas exec_induct = exec.induct[split_format(complete)]
+
+code_pred exec .
+
+values
+ "{(i,map t [''x'',''y''],stk) | i t stk.
+ [LOAD ''y'', STORE ''x''] \<turnstile>
+ (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
+
+
+subsection{* Verification infrastructure *}
+
+lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
+apply(induct rule: exec.induct)
+ apply blast
+by (metis exec.step)
+
+lemma exec1_subst: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> c' = c'' \<Longrightarrow> P \<turnstile> c \<rightarrow> c''"
+by auto
+
+lemmas exec1_simps = exec1.intros[THEN exec1_subst]
+
+text{* Below we need to argue about the execution of code that is embedded in
+larger programs. For this purpose we show that execution is preserved by
+appending code to the left or right of a program. *}
+
+lemma exec1_appendR: assumes "P \<turnstile> c \<rightarrow> c'" shows "P@P' \<turnstile> c \<rightarrow> c'"
+proof-
+ from assms show ?thesis
+ by cases (simp_all add: exec1_simps nth_append)
+ -- "All cases proved with the final simp-all"
qed
-text {* The other direction! *}
-
-inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1"
-
-lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
-apply(rule iffI)
- apply(erule rel_pow_E2, simp, fast)
-apply simp
-done
+lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
+apply(induct rule: exec.induct)
+ apply blast
+by (metis exec1_appendR exec.step)
-lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
-by(simp add: rtrancl_is_UN_rel_pow)
-
-definition
- forws :: "instr \<Rightarrow> nat set" where
- "forws instr = (case instr of
- SET x a \<Rightarrow> {0} |
- JMPF b n \<Rightarrow> {0,n} |
- JMPB n \<Rightarrow> {})"
+lemma exec1_appendL:
+assumes "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk')"
+shows "P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
+proof-
+ from assms show ?thesis
+ by cases (simp_all add: exec1_simps)
+qed
-definition
- backws :: "instr \<Rightarrow> nat set" where
- "backws instr = (case instr of
- SET x a \<Rightarrow> {} |
- JMPF b n \<Rightarrow> {} |
- JMPB n \<Rightarrow> {n})"
-
-primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
-where
- "closed m n [] = True"
-| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
- (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
+lemma exec_appendL:
+ "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
+ P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
+apply(induct rule: exec_induct)
+ apply blast
+by (blast intro: exec1_appendL exec.step)
-lemma [simp]:
- "\<And>m n. closed m n (C1@C2) =
- (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
-by(induct C1) (simp, simp add:add_ac)
-
-theorem [simp]: "\<And>m n. closed m n (compile c)"
-by(induct c) (simp_all add:backws_def forws_def)
+text{* Now we specialise the above lemmas to enable automatic proofs of
+@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
+pieces of code that we already know how they execute (by induction), combined
+by @{text "@"} and @{text "#"}. Backward jumps are not supported.
+The details should be skipped on a first reading.
-lemma drop_lem: "n \<le> size(p1@p2)
- \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
- (n \<le> size p1 & p1' = drop n p1)"
-apply(rule iffI)
- defer apply simp
-apply(subgoal_tac "n \<le> size p1")
- apply simp
-apply(rule ccontr)
-apply(drule_tac f = length in arg_cong)
+If the pc points beyond the first instruction or part of the program, drop it: *}
+
+lemma exec_Cons_Suc[intro]:
+ "P \<turnstile> (i,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
+ instr#P \<turnstile> (Suc i,s,stk) \<rightarrow>* (Suc j,t,stk')"
+apply(drule exec_appendL[where P'="[instr]"])
apply simp
done
-lemma reduce_exec1:
- "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
- \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
-by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
-
-
-lemma closed_exec1:
- "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
- \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
- \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
-apply(clarsimp simp add:forws_def backws_def
- split:instr.split_asm split_if_asm)
+lemma exec_appendL_if[intro]:
+ "size P' <= i
+ \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
+ \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
+apply(drule exec_appendL[where P'=P'])
+apply simp
done
-theorem closed_execn_decomp: "\<And>C1 C2 r.
- \<lbrakk> closed 0 0 (rev C1 @ C2);
- \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
- \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
- \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
- n = n1+n2"
-(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
-proof(induct n)
- fix C1 C2 r
- assume "?H C1 C2 r 0"
- thus "?P C1 C2 r 0" by simp
-next
- fix C1 C2 r n
- assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
- assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
- show "?P C1 C2 r (Suc n)"
- proof (cases C2)
- assume "C2 = []" with H show ?thesis by simp
- next
- fix instr tlC2
- assume C2: "C2 = instr # tlC2"
- from H C2 obtain p' q' r'
- where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
- and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
- by(fastsimp simp add:rel_pow_commute)
- from CL closed_exec1[OF _ 1] C2
- obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
- and same: "rev C1' @ C2' = rev C1 @ C2"
- by fastsimp
- have rev_same: "rev C2' @ C1' = rev C2 @ C1"
- proof -
- have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
- also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
- also have "\<dots> = rev C2 @ C1" by simp
- finally show ?thesis .
- qed
- hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
- from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
- \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
- by(simp add:pq' rev_same')
- from IH[OF _ n'] CL
- obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
- "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
- n = n1 + n2"
- by(fastsimp simp add: same rev_same rev_same')
- moreover
- from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
- by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
- ultimately show ?thesis by (fastsimp simp del:relpow.simps)
- qed
-qed
+text{* Split the execution of a compound program up into the excution of its
+parts: *}
-lemma execn_decomp:
-"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
- \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
- \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
- n = n1+n2"
-using closed_execn_decomp[of "[]",simplified] by simp
+lemma exec_append_trans[intro]:
+"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
+ size P \<le> i' \<Longrightarrow>
+ P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
+ j'' = size P + i''
+ \<Longrightarrow>
+ P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
+by(metis exec_trans[OF exec_appendR exec_appendL_if])
-lemma exec_star_decomp:
-"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
- \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
- \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
-by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
+
+declare Let_def[simp] eval_nat_numeral[simp]
-(* Alternative:
-lemma exec_comp_n:
-"\<And>p1 p2 q r t n.
- \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
- \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
- \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
- n = n1+n2"
- (is "\<And>p1 p2 q r t n. ?H c p1 p2 q r t n \<Longrightarrow> ?P c p1 p2 q r t n")
-proof (induct c)
-*)
+subsection "Compilation"
-text{*Warning:
-@{prop"\<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"}
-is not true! *}
+fun acomp :: "aexp \<Rightarrow> instr list" where
+"acomp (N n) = [LOADI n]" |
+"acomp (V x) = [LOAD x]" |
+"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
+
+lemma acomp_correct[intro]:
+ "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
+apply(induct a arbitrary: stk)
+apply(fastsimp)+
+done
-theorem "\<And>s t.
- \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-proof (induct c)
- fix s t
- assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
- thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
-next
- fix s t v f
- assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
- thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
-next
- fix s1 s3 c1 c2
- let ?C1 = "compile c1" let ?C2 = "compile c2"
- assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
- and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
- assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
- then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
- exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
- by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
- from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
- using exec_star_decomp[of _ "[]" "[]"] by fastsimp
- have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
- moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
- ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
+fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> instr list" where
+"bcomp (B bv) c n = (if bv=c then [JMPF n] else [])" |
+"bcomp (Not b) c n = bcomp b (\<not>c) n" |
+"bcomp (And b1 b2) c n =
+ (let cb2 = bcomp b2 c n;
+ m = (if c then size cb2 else size cb2+n);
+ cb1 = bcomp b1 False m
+ in cb1 @ cb2)" |
+"bcomp (Less a1 a2) c n =
+ acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
+
+value
+ "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
+ False 3"
+
+lemma bcomp_correct[intro]:
+ "bcomp b c n \<turnstile>
+ (0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
+proof(induct b arbitrary: c n m)
+ case Not
+ from Not[of "~c"] show ?case by fastsimp
next
- fix s t b c1 c2
- let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
- let ?C1 = "compile c1" let ?C2 = "compile c2"
- assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
- and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
- and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
- show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
- proof cases
- assume b: "b s"
- with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
- by (fastsimp dest:exec_star_decomp
- [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
- hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
- with b show ?thesis ..
- next
- assume b: "\<not> b s"
- with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
- using exec_star_decomp[of _ "[]" "[]"] by simp
- hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
- with b show ?thesis ..
- qed
+ case (And b1 b2)
+ from And(1)[of "False"] And(2)[of "c"] show ?case by fastsimp
+qed fastsimp+
+
+
+fun ccomp :: "com \<Rightarrow> instr list" where
+"ccomp SKIP = []" |
+"ccomp (x ::= a) = acomp a @ [STORE x]" |
+"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
+"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
+ (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
+ in cb @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" |
+"ccomp (WHILE b DO c) =
+ (let cc = ccomp c; cb = bcomp b False (size cc + 1)
+ in cb @ cc @ [JMPB (size cb + size cc + 1)])"
+
+value "ccomp
+ (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
+ ELSE ''v'' ::= V ''u'')"
+
+value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
+
+
+subsection "Preservation of sematics"
+
+lemma ccomp_correct:
+ "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
+proof(induct arbitrary: stk rule: big_step_induct)
+ case (Assign x a s)
+ show ?case by (fastsimp simp:fun_upd_def)
next
- fix b c s t
- let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
- let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
- assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
- and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
- from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
- by(simp add:rtrancl_is_UN_rel_pow) blast
- { fix n have "\<And>s. \<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
- proof (induct n rule: less_induct)
- fix n
- assume IHm: "\<And>m s. \<lbrakk>m < n; \<langle>?W,[],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<rbrakk> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
- fix s
- assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
- show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
- proof cases
- assume b: "b s"
- then obtain m where m: "n = Suc m"
- and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
- using H by fastsimp
- then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
- and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
- and n12: "m = n1+n2"
- using execn_decomp[of _ "[?j2]"]
- by(simp del: execn_simp) fast
- have n2n: "n2 - 1 < n" using m n12 by arith
- note b
- moreover
- { from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
- by (simp add:rtrancl_is_UN_rel_pow) fast
- hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
- }
- moreover
- { have "n2 - 1 < n" using m n12 by arith
- moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
- ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
- }
- ultimately show ?thesis ..
- next
- assume b: "\<not> b s"
- hence "t = s" using H by simp
- with b show ?thesis by simp
- qed
- qed
- }
- with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
-qed
-
-(* TODO: connect with Machine 0 using M_equiv *)
+ case (Semi c1 s1 s2 c2 s3)
+ let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
+ have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
+ using Semi.hyps(2) by (fastsimp)
+ moreover
+ have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
+ using Semi.hyps(4) by (fastsimp)
+ ultimately show ?case by simp (blast intro: exec_trans)
+next
+ case (WhileTrue b s1 c s2 s3)
+ let ?cc = "ccomp c"
+ let ?cb = "bcomp b False (size ?cc + 1)"
+ let ?cw = "ccomp(WHILE b DO c)"
+ have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
+ using WhileTrue(1,3) by fastsimp
+ moreover
+ have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
+ by (fastsimp)
+ moreover
+ have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue(5))
+ ultimately show ?case by(blast intro: exec_trans)
+qed fastsimp+
end
--- a/src/HOL/IMP/ROOT.ML Wed Jun 01 15:53:47 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML Wed Jun 01 21:35:34 2011 +0200
@@ -1,7 +1,23 @@
-(* Title: HOL/IMP/ROOT.ML
- Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
-
-Caveat: HOLCF/IMP depends on HOL/IMP
+use_thys
+["BExp",
+ "ASM",
+ "Small_Step",
+ "Compiler"(*,
+ "Poly_Types",
+ "Sec_Typing",
+ "Sec_TypingT",
+ "Def_Ass_Sound_Big",
+ "Def_Ass_Sound_Small",
+ "Def_Ass2_Sound_Small",
+ "Def_Ass2_Big0",
+ "Live",
+ "Hoare_Examples",
+ "VC",
+ "HoareT",
+ "Procs_Dyn_Vars_Dyn",
+ "Procs_Stat_Vars_Dyn",
+ "Procs_Stat_Vars_Stat",
+ "C_like",
+ "OO"
*)
-
-use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];
+];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Small_Step.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,210 @@
+header "Small-Step Semantics of Commands"
+
+theory Small_Step imports Star Big_Step begin
+
+subsection "The transition relation"
+
+inductive
+ small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
+where
+Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
+
+Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
+Semi2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
+
+IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
+IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
+
+While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+
+
+abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
+where "x \<rightarrow>* y == star small_step x y"
+
+subsection{* Executability *}
+
+code_pred small_step .
+
+values "{(c',map t [''x'',''y'',''z'']) |c' t.
+ (''x'' ::= V ''z''; ''y'' ::= V ''x'',
+ lookup[(''x'',3),(''y'',7),(''z'',5)]) \<rightarrow>* (c',t)}"
+
+
+subsection{* Proof infrastructure *}
+
+subsubsection{* Induction rules *}
+
+text{* The default induction rule @{thm[source] small_step.induct} only works
+for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are
+not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant
+of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
+@{text"\<rightarrow>"} into pairs: *}
+lemmas small_step_induct = small_step.induct[split_format(complete)]
+
+
+subsubsection{* Proof automation *}
+
+declare small_step.intros[simp,intro]
+
+text{* So called transitivity rules. See below. *}
+
+declare step[trans] step1[trans]
+
+lemma step2[trans]:
+ "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''"
+by(metis refl step)
+
+declare star_trans[trans]
+
+text{* Rule inversion: *}
+
+inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
+thm SkipE
+inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
+thm AssignE
+inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
+thm SemiE
+inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
+inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
+
+
+text{* A simple property: *}
+lemma deterministic:
+ "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
+apply(induct arbitrary: cs'' rule: small_step.induct)
+apply blast+
+done
+
+
+subsection "Equivalence with big-step semantics"
+
+lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
+proof(induct rule: star_induct)
+ case refl thus ?case by simp
+next
+ case step
+ thus ?case by (metis Semi2 star.step)
+qed
+
+lemma semi_comp:
+ "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
+ \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
+by(blast intro: star.step star_semi2 star_trans)
+
+text{* The following proof corresponds to one on the board where one would
+show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the
+also/finally proof steps do: they compose chains, implicitly using the rules
+declared with attribute [trans] above. *}
+
+lemma big_to_small:
+ "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
+proof (induct rule: big_step.induct)
+ fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
+next
+ fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
+next
+ fix c1 c2 s1 s2 s3
+ assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
+ thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
+next
+ fix s::state and b c0 c1 t
+ assume "bval b s"
+ hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
+ also assume "(c0,s) \<rightarrow>* (SKIP,t)"
+ finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption"
+next
+ fix s::state and b c0 c1 t
+ assume "\<not>bval b s"
+ hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
+ also assume "(c1,s) \<rightarrow>* (SKIP,t)"
+ finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" .
+next
+ fix b c and s::state
+ assume b: "\<not>bval b s"
+ let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
+ have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
+ also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
+ finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto
+next
+ fix b c s s' t
+ let ?w = "WHILE b DO c"
+ let ?if = "IF b THEN c; ?w ELSE SKIP"
+ assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
+ assume c: "(c,s) \<rightarrow>* (SKIP,s')"
+ assume b: "bval b s"
+ have "(?w,s) \<rightarrow> (?if, s)" by blast
+ also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
+ also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
+ finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
+qed
+
+text{* Each case of the induction can be proved automatically: *}
+lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
+proof (induct rule: big_step.induct)
+ case Skip show ?case by blast
+next
+ case Assign show ?case by blast
+next
+ case Semi thus ?case by (blast intro: semi_comp)
+next
+ case IfTrue thus ?case by (blast intro: step)
+next
+ case IfFalse thus ?case by (blast intro: step)
+next
+ case WhileFalse thus ?case
+ by (metis step step1 small_step.IfFalse small_step.While)
+next
+ case WhileTrue
+ thus ?case
+ by(metis While semi_comp small_step.IfTrue step[of small_step])
+qed
+
+lemma small1_big_continue:
+ "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
+apply (induct arbitrary: t rule: small_step.induct)
+apply auto
+done
+
+lemma small_big_continue:
+ "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
+apply (induct rule: star.induct)
+apply (auto intro: small1_big_continue)
+done
+
+lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
+by (metis small_big_continue Skip)
+
+text {*
+ Finally, the equivalence theorem:
+*}
+theorem big_iff_small:
+ "cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)"
+by(metis big_to_small small_to_big)
+
+
+subsection "Final configurations and infinite reductions"
+
+definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
+
+lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
+apply(simp add: final_def)
+apply(induct c)
+apply blast+
+done
+
+lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
+by (metis SkipE finalD final_def)
+
+text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"}
+terminates: *}
+
+lemma big_iff_small_termination:
+ "(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')"
+by(simp add: big_iff_small final_iff_SKIP)
+
+text{* This is the same as saying that the absence of a big step result is
+equivalent with absence of a terminating small step sequence, i.e.\ with
+nontermination. Since @{text"\<rightarrow>"} is determininistic, there is no difference
+between may and must terminate. *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Star.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,27 @@
+theory Star imports Main
+begin
+
+inductive
+ star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+for r where
+refl: "star r x x" |
+step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+
+lemma star_trans:
+ "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+proof(induct rule: star.induct)
+ case refl thus ?case .
+next
+ case step thus ?case by (metis star.step)
+qed
+
+lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
+
+declare star.refl[simp,intro]
+
+lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
+by(metis refl step)
+
+code_pred star .
+
+end
--- a/src/HOL/IMP/document/root.tex Wed Jun 01 15:53:47 2011 +0200
+++ b/src/HOL/IMP/document/root.tex Wed Jun 01 21:35:34 2011 +0200
@@ -1,13 +1,38 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
-\documentclass[a4wide]{article}
-\usepackage{graphicx,isabelle,isabellesym}
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+ %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+ %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+ %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage[greek,english]{babel}
+ %option greek for \<euro>
+ %option english (default language) for \<guillemotleft>, \<guillemotright>
+
+%\usepackage[latin1]{inputenc}
+ %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
+ %\<threesuperior>, \<threequarters>, \<degree>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+ %for \<Sqinter>
+
+%\usepackage{eufrak}
+ %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+ %for \<cent>, \<currency>
+
+% this should be the last package used
\usepackage{pdfsetup}
+% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
-\renewcommand{\isachardoublequote}{}
+\isabellestyle{it}
-% pretty printing for the Com language
-%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
\newcommand{\isasymSKIP}{\CMD{skip}}
\newcommand{\isasymIF}{\CMD{if}}
@@ -16,37 +41,26 @@
\newcommand{\isasymWHILE}{\CMD{while}}
\newcommand{\isasymDO}{\CMD{do}}
-\addtolength{\hoffset}{-1cm}
-\addtolength{\textwidth}{2cm}
+% for uniform font size
+\renewcommand{\isastyle}{\isastyleminor}
+
\begin{document}
-\title{IMP --- A {\tt WHILE}-language and its Semantics}
-\author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
+\title{Concrete Semantics}
+\author{TN \& GK}
\maketitle
-\parindent 0pt\parskip 0.5ex
+\tableofcontents
+\newpage
-\begin{abstract}\noindent
- The denotational, operational, and axiomatic semantics, a verification
- condition generator, and all the necessary soundness, completeness and
- equivalence proofs. Essentially a formalization of the first 100 pages of
- \cite{Winskel}.
-
- An eminently readable description of this theory is found in \cite{Nipkow}.
- See also HOLCF/IMP for a denotational semantics.
-\end{abstract}
-
-\tableofcontents
-
-\begin{center}
- \includegraphics[scale=0.7]{session_graph}
-\end{center}
-
-\parindent 0pt\parskip 0.5ex
+% generated text of all theories
\input{session}
-\bibliographystyle{plain}
+\nocite{Nipkow}
+
+% optional bibliography
+\bibliographystyle{abbrv}
\bibliography{root}
\end{document}