1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/IMP/AExp.thy Wed Jun 01 21:35:34 2011 +0200
1.3 @@ -0,0 +1,85 @@
1.4 +header "Arithmetic and Boolean Expressions"
1.5 +
1.6 +theory AExp imports Main begin
1.7 +
1.8 +subsection "Arithmetic Expressions"
1.9 +
1.10 +type_synonym name = string
1.11 +type_synonym val = int
1.12 +type_synonym state = "name \<Rightarrow> val"
1.13 +
1.14 +datatype aexp = N int | V name | Plus aexp aexp
1.15 +
1.16 +fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
1.17 +"aval (N n) _ = n" |
1.18 +"aval (V x) s = s x" |
1.19 +"aval (Plus a1 a2) s = aval a1 s + aval a2 s"
1.20 +
1.21 +
1.22 +value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
1.23 +
1.24 +fun lookup :: "(string * val)list \<Rightarrow> string \<Rightarrow> val" where
1.25 +"lookup ((x,i)#xis) y = (if x=y then i else lookup xis y)"
1.26 +
1.27 +value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])"
1.28 +
1.29 +value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])"
1.30 +
1.31 +
1.32 +subsection "Optimization"
1.33 +
1.34 +text{* Evaluate constant subsexpressions: *}
1.35 +
1.36 +fun asimp_const :: "aexp \<Rightarrow> aexp" where
1.37 +"asimp_const (N n) = N n" |
1.38 +"asimp_const (V x) = V x" |
1.39 +"asimp_const (Plus a1 a2) =
1.40 + (case (asimp_const a1, asimp_const a2) of
1.41 + (N n1, N n2) \<Rightarrow> N(n1+n2) |
1.42 + (a1',a2') \<Rightarrow> Plus a1' a2')"
1.43 +
1.44 +theorem aval_asimp_const[simp]:
1.45 + "aval (asimp_const a) s = aval a s"
1.46 +apply(induct a)
1.47 +apply (auto split: aexp.split)
1.48 +done
1.49 +
1.50 +text{* Now we also eliminate all occurrences 0 in additions. The standard
1.51 +method: optimized versions of the constructors: *}
1.52 +
1.53 +fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
1.54 +"plus (N i1) (N i2) = N(i1+i2)" |
1.55 +"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
1.56 +"plus a (N i) = (if i=0 then a else Plus a (N i))" |
1.57 +"plus a1 a2 = Plus a1 a2"
1.58 +
1.59 +text ""
1.60 +code_thms plus
1.61 +code_thms plus
1.62 +
1.63 +(* FIXME: dropping subsumed code eqns?? *)
1.64 +lemma aval_plus[simp]:
1.65 + "aval (plus a1 a2) s = aval a1 s + aval a2 s"
1.66 +apply(induct a1 a2 rule: plus.induct)
1.67 +apply simp_all (* just for a change from auto *)
1.68 +done
1.69 +code_thms plus
1.70 +
1.71 +fun asimp :: "aexp \<Rightarrow> aexp" where
1.72 +"asimp (N n) = N n" |
1.73 +"asimp (V x) = V x" |
1.74 +"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
1.75 +
1.76 +text{* Note that in @{const asimp_const} the optimized constructor was
1.77 +inlined. Making it a separate function @{const plus} improves modularity of
1.78 +the code and the proofs. *}
1.79 +
1.80 +value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
1.81 +
1.82 +theorem aval_asimp[simp]:
1.83 + "aval (asimp a) s = aval a s"
1.84 +apply(induct a)
1.85 +apply simp_all
1.86 +done
1.87 +
1.88 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/IMP/ASM.thy Wed Jun 01 21:35:34 2011 +0200
2.3 @@ -0,0 +1,51 @@
2.4 +header "Arithmetic Stack Machine and Compilation"
2.5 +
2.6 +theory ASM imports AExp begin
2.7 +
2.8 +subsection "Arithmetic Stack Machine"
2.9 +
2.10 +datatype ainstr = LOADI val | LOAD string | ADD
2.11 +
2.12 +type_synonym stack = "val list"
2.13 +
2.14 +abbreviation "hd2 xs == hd(tl xs)"
2.15 +abbreviation "tl2 xs == tl(tl xs)"
2.16 +
2.17 +text{* \noindent Abbreviations are transparent: they are unfolded after
2.18 +parsing and folded back again before printing. Internally, they do not
2.19 +exist. *}
2.20 +
2.21 +fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
2.22 +"aexec1 (LOADI n) _ stk = n # stk" |
2.23 +"aexec1 (LOAD n) s stk = s(n) # stk" |
2.24 +"aexec1 ADD _ stk = (hd2 stk + hd stk) # tl2 stk"
2.25 +
2.26 +fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
2.27 +"aexec [] _ stk = stk" |
2.28 +"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
2.29 +
2.30 +value "aexec [LOADI 5, LOAD ''y'', ADD]
2.31 + (lookup[(''x'',42), (''y'',43)]) [50]"
2.32 +
2.33 +lemma aexec_append[simp]:
2.34 + "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
2.35 +apply(induct is1 arbitrary: stk)
2.36 +apply (auto)
2.37 +done
2.38 +
2.39 +
2.40 +subsection "Compilation"
2.41 +
2.42 +fun acomp :: "aexp \<Rightarrow> ainstr list" where
2.43 +"acomp (N n) = [LOADI n]" |
2.44 +"acomp (V x) = [LOAD x]" |
2.45 +"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
2.46 +
2.47 +value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
2.48 +
2.49 +theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
2.50 +apply(induct a arbitrary: stk)
2.51 +apply (auto)
2.52 +done
2.53 +
2.54 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/IMP/BExp.thy Wed Jun 01 21:35:34 2011 +0200
3.3 @@ -0,0 +1,69 @@
3.4 +theory BExp imports AExp begin
3.5 +
3.6 +subsection "Boolean Expressions"
3.7 +
3.8 +datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
3.9 +
3.10 +fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
3.11 +"bval (B bv) _ = bv" |
3.12 +"bval (Not b) s = (\<not> bval b s)" |
3.13 +"bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
3.14 +"bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
3.15 +
3.16 +value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
3.17 + (lookup [(''x'',3),(''y'',1)])"
3.18 +
3.19 +
3.20 +subsection "Optimization"
3.21 +
3.22 +text{* Optimized constructors: *}
3.23 +
3.24 +fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
3.25 +"less (N n1) (N n2) = B(n1 < n2)" |
3.26 +"less a1 a2 = Less a1 a2"
3.27 +
3.28 +lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
3.29 +apply(induct a1 a2 rule: less.induct)
3.30 +apply simp_all
3.31 +done
3.32 +
3.33 +fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
3.34 +"and (B True) b = b" |
3.35 +"and b (B True) = b" |
3.36 +"and (B False) b = B False" |
3.37 +"and b (B False) = B False" |
3.38 +"and b1 b2 = And b1 b2"
3.39 +
3.40 +lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
3.41 +apply(induct b1 b2 rule: and.induct)
3.42 +apply simp_all
3.43 +done
3.44 +
3.45 +fun not :: "bexp \<Rightarrow> bexp" where
3.46 +"not (B True) = B False" |
3.47 +"not (B False) = B True" |
3.48 +"not b = Not b"
3.49 +
3.50 +lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
3.51 +apply(induct b rule: not.induct)
3.52 +apply simp_all
3.53 +done
3.54 +
3.55 +text{* Now the overall optimizer: *}
3.56 +
3.57 +fun bsimp :: "bexp \<Rightarrow> bexp" where
3.58 +"bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
3.59 +"bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
3.60 +"bsimp (Not b) = not(bsimp b)" |
3.61 +"bsimp (B bv) = B bv"
3.62 +
3.63 +value "bsimp (And (Less (N 0) (N 1)) b)"
3.64 +
3.65 +value "bsimp (And (Less (N 1) (N 0)) (B True))"
3.66 +
3.67 +theorem "bval (bsimp b) s = bval b s"
3.68 +apply(induct b)
3.69 +apply simp_all
3.70 +done
3.71 +
3.72 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/IMP/Big_Step.thy Wed Jun 01 21:35:34 2011 +0200
4.3 @@ -0,0 +1,243 @@
4.4 +(* Author: Gerwin Klein, Tobias Nipkow *)
4.5 +
4.6 +theory Big_Step imports Com begin
4.7 +
4.8 +subsection "Big-Step Semantics of Commands"
4.9 +
4.10 +inductive
4.11 + big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
4.12 +where
4.13 +Skip: "(SKIP,s) \<Rightarrow> s" |
4.14 +Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
4.15 +Semi: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
4.16 + (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
4.17 +
4.18 +IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
4.19 + (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
4.20 +IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
4.21 + (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
4.22 +
4.23 +WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
4.24 +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>
4.25 + (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
4.26 +
4.27 +schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
4.28 +apply(rule Semi)
4.29 +apply(rule Assign)
4.30 +apply simp
4.31 +apply(rule Assign)
4.32 +done
4.33 +
4.34 +thm ex[simplified]
4.35 +
4.36 +text{* We want to execute the big-step rules: *}
4.37 +
4.38 +code_pred big_step .
4.39 +
4.40 +text{* For inductive definitions we need command
4.41 + \texttt{values} instead of \texttt{value}. *}
4.42 +
4.43 +values "{t. (SKIP, lookup[]) \<Rightarrow> t}"
4.44 +
4.45 +text{* We need to translate the result state into a list
4.46 +to display it. *}
4.47 +
4.48 +values "{map t [''x''] |t. (SKIP, lookup [(''x'',42)]) \<Rightarrow> t}"
4.49 +
4.50 +values "{map t [''x''] |t. (''x'' ::= N 2, lookup [(''x'',42)]) \<Rightarrow> t}"
4.51 +
4.52 +values "{map t [''x'',''y''] |t.
4.53 + (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
4.54 + lookup [(''x'',0),(''y'',13)]) \<Rightarrow> t}"
4.55 +
4.56 +
4.57 +text{* Proof automation: *}
4.58 +
4.59 +declare big_step.intros [intro]
4.60 +
4.61 +text{* The standard induction rule
4.62 +@{thm [display] big_step.induct [no_vars]} *}
4.63 +
4.64 +thm big_step.induct
4.65 +
4.66 +text{* A customized induction rule for (c,s) pairs: *}
4.67 +
4.68 +lemmas big_step_induct = big_step.induct[split_format(complete)]
4.69 +thm big_step_induct
4.70 +text {*
4.71 +@{thm [display] big_step_induct [no_vars]}
4.72 +*}
4.73 +
4.74 +
4.75 +subsection "Rule inversion"
4.76 +
4.77 +text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
4.78 +That @{prop "s = t"}. This is how we can automatically prove it: *}
4.79 +
4.80 +inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"
4.81 +thm skipE
4.82 +
4.83 +text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
4.84 +blast and friends (but not simp!) to use it automatically; [elim!] means that
4.85 +it is applied eagerly.
4.86 +
4.87 +Similarly for the other commands: *}
4.88 +
4.89 +inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
4.90 +thm AssignE
4.91 +inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
4.92 +thm SemiE
4.93 +inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
4.94 +thm IfE
4.95 +
4.96 +inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
4.97 +thm WhileE
4.98 +text{* Only [elim]: [elim!] would not terminate. *}
4.99 +
4.100 +text{* An automatic example: *}
4.101 +
4.102 +lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
4.103 +by blast
4.104 +
4.105 +text{* Rule inversion by hand via the ``cases'' method: *}
4.106 +
4.107 +lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
4.108 +shows "t = s"
4.109 +proof-
4.110 + from assms show ?thesis
4.111 + proof cases --"inverting assms"
4.112 + case IfTrue thm IfTrue
4.113 + thus ?thesis by blast
4.114 + next
4.115 + case IfFalse thus ?thesis by blast
4.116 + qed
4.117 +qed
4.118 +
4.119 +
4.120 +subsection "Command Equivalence"
4.121 +
4.122 +text {*
4.123 + We call two statements @{text c} and @{text c'} equivalent wrt.\ the
4.124 + big-step semantics when \emph{@{text c} started in @{text s} terminates
4.125 + in @{text s'} iff @{text c'} started in the same @{text s} also terminates
4.126 + in the same @{text s'}}. Formally:
4.127 +*}
4.128 +abbreviation
4.129 + equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
4.130 + "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
4.131 +
4.132 +text {*
4.133 +Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
4.134 +
4.135 + As an example, we show that loop unfolding is an equivalence
4.136 + transformation on programs:
4.137 +*}
4.138 +lemma unfold_while:
4.139 + "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
4.140 +proof -
4.141 + -- "to show the equivalence, we look at the derivation tree for"
4.142 + -- "each side and from that construct a derivation tree for the other side"
4.143 + { fix s t assume "(?w, s) \<Rightarrow> t"
4.144 + -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
4.145 + -- "then both statements do nothing:"
4.146 + { assume "\<not>bval b s"
4.147 + hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
4.148 + hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
4.149 + }
4.150 + moreover
4.151 + -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
4.152 + -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
4.153 + { assume "bval b s"
4.154 + with `(?w, s) \<Rightarrow> t` obtain s' where
4.155 + "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
4.156 + -- "now we can build a derivation tree for the @{text IF}"
4.157 + -- "first, the body of the True-branch:"
4.158 + hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
4.159 + -- "then the whole @{text IF}"
4.160 + with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
4.161 + }
4.162 + ultimately
4.163 + -- "both cases together give us what we want:"
4.164 + have "(?iw, s) \<Rightarrow> t" by blast
4.165 + }
4.166 + moreover
4.167 + -- "now the other direction:"
4.168 + { fix s t assume "(?iw, s) \<Rightarrow> t"
4.169 + -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
4.170 + -- "of the @{text IF} is executed, and both statements do nothing:"
4.171 + { assume "\<not>bval b s"
4.172 + hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
4.173 + hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
4.174 + }
4.175 + moreover
4.176 + -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
4.177 + -- {* then this time only the @{text IfTrue} rule can have be used *}
4.178 + { assume "bval b s"
4.179 + with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
4.180 + -- "and for this, only the Semi-rule is applicable:"
4.181 + then obtain s' where
4.182 + "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
4.183 + -- "with this information, we can build a derivation tree for the @{text WHILE}"
4.184 + with `bval b s`
4.185 + have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
4.186 + }
4.187 + ultimately
4.188 + -- "both cases together again give us what we want:"
4.189 + have "(?w, s) \<Rightarrow> t" by blast
4.190 + }
4.191 + ultimately
4.192 + show ?thesis by blast
4.193 +qed
4.194 +
4.195 +text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can
4.196 +prove many such facts automatically. *}
4.197 +
4.198 +lemma
4.199 + "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
4.200 +by blast
4.201 +
4.202 +lemma triv_if:
4.203 + "(IF b THEN c ELSE c) \<sim> c"
4.204 +by blast
4.205 +
4.206 +lemma commute_if:
4.207 + "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)
4.208 + \<sim>
4.209 + (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
4.210 +by blast
4.211 +
4.212 +
4.213 +subsection "Execution is deterministic"
4.214 +
4.215 +text {* This proof is automatic. *}
4.216 +theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
4.217 +apply (induct arbitrary: u rule: big_step.induct)
4.218 +apply blast+
4.219 +done
4.220 +
4.221 +text {*
4.222 + This is the proof as you might present it in a lecture. The remaining
4.223 + cases are simple enough to be proved automatically:
4.224 +*}
4.225 +theorem
4.226 + "(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t"
4.227 +proof (induct arbitrary: t' rule: big_step.induct)
4.228 + -- "the only interesting case, @{text WhileTrue}:"
4.229 + fix b c s s1 t t'
4.230 + -- "The assumptions of the rule:"
4.231 + assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"
4.232 + -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
4.233 + assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"
4.234 + assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"
4.235 + -- "Premise of implication:"
4.236 + assume "(WHILE b DO c,s) \<Rightarrow> t'"
4.237 + with `bval b s` obtain s1' where
4.238 + c: "(c,s) \<Rightarrow> s1'" and
4.239 + w: "(WHILE b DO c,s1') \<Rightarrow> t'"
4.240 + by auto
4.241 + from c IHc have "s1' = s1" by blast
4.242 + with w IHw show "t' = t" by blast
4.243 +qed blast+ -- "prove the rest automatically"
4.244 +
4.245 +
4.246 +end
5.1 --- a/src/HOL/IMP/Com.thy Wed Jun 01 15:53:47 2011 +0200
5.2 +++ b/src/HOL/IMP/Com.thy Wed Jun 01 21:35:34 2011 +0200
5.3 @@ -1,33 +1,12 @@
5.4 -(* Title: HOL/IMP/Com.thy
5.5 - Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
5.6 - Author: Gerwin Klein
5.7 -*)
5.8 +header "IMP --- A Simple Imperative Language"
5.9
5.10 -header "Syntax of Commands"
5.11 -
5.12 -theory Com imports Main begin
5.13 -
5.14 -typedecl loc
5.15 - -- "an unspecified (arbitrary) type of locations
5.16 - (adresses/names) for variables"
5.17 -
5.18 -type_synonym val = nat -- "or anything else, @{text nat} used in examples"
5.19 -type_synonym state = "loc \<Rightarrow> val"
5.20 -type_synonym aexp = "state \<Rightarrow> val"
5.21 -type_synonym bexp = "state \<Rightarrow> bool"
5.22 - -- "arithmetic and boolean expressions are not modelled explicitly here,"
5.23 - -- "they are just functions on states"
5.24 +theory Com imports BExp begin
5.25
5.26 datatype
5.27 - com = SKIP
5.28 - | Assign loc aexp ("_ :== _ " 60)
5.29 - | Semi com com ("_; _" [60, 60] 10)
5.30 - | Cond bexp com com ("IF _ THEN _ ELSE _" 60)
5.31 - | While bexp com ("WHILE _ DO _" 60)
5.32 -
5.33 -notation (latex)
5.34 - SKIP ("\<SKIP>") and
5.35 - Cond ("\<IF> _ \<THEN> _ \<ELSE> _" 60) and
5.36 - While ("\<WHILE> _ \<DO> _" 60)
5.37 + com = SKIP
5.38 + | Assign name aexp ("_ ::= _" [1000, 61] 61)
5.39 + | Semi com com ("_;/ _" [60, 61] 60)
5.40 + | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
5.41 + | While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
5.42
5.43 end
6.1 --- a/src/HOL/IMP/Compiler.thy Wed Jun 01 15:53:47 2011 +0200
6.2 +++ b/src/HOL/IMP/Compiler.thy Wed Jun 01 21:35:34 2011 +0200
6.3 @@ -1,298 +1,237 @@
6.4 -(* Title: HOL/IMP/Compiler.thy
6.5 - Author: Tobias Nipkow, TUM
6.6 - Copyright 1996 TUM
6.7 -*)
6.8 +(* Author: Tobias Nipkow *)
6.9
6.10 -theory Compiler imports Machines begin
6.11 +header "A Compiler for IMP"
6.12
6.13 -subsection "The compiler"
6.14 +theory Compiler imports Big_Step
6.15 +begin
6.16
6.17 -primrec compile :: "com \<Rightarrow> instr list"
6.18 +subsection "Instructions and Stack Machine"
6.19 +
6.20 +datatype instr =
6.21 + LOADI int | LOAD string | ADD |
6.22 + STORE string |
6.23 + JMPF nat |
6.24 + JMPB nat |
6.25 + JMPFLESS nat |
6.26 + JMPFGE nat
6.27 +
6.28 +type_synonym stack = "int list"
6.29 +type_synonym config = "nat\<times>state\<times>stack"
6.30 +
6.31 +abbreviation "hd2 xs == hd(tl xs)"
6.32 +abbreviation "tl2 xs == tl(tl xs)"
6.33 +
6.34 +inductive exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
6.35 + ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
6.36 + for P :: "instr list"
6.37 where
6.38 - "compile \<SKIP> = []"
6.39 -| "compile (x:==a) = [SET x a]"
6.40 -| "compile (c1;c2) = compile c1 @ compile c2"
6.41 -| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
6.42 - [JMPF b (length(compile c1) + 1)] @ compile c1 @
6.43 - [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
6.44 -| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
6.45 - [JMPB (length(compile c)+1)]"
6.46 +"\<lbrakk> i < size P; P!i = LOADI n \<rbrakk> \<Longrightarrow>
6.47 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
6.48 +"\<lbrakk> i < size P; P!i = LOAD x \<rbrakk> \<Longrightarrow>
6.49 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
6.50 +"\<lbrakk> i < size P; P!i = ADD \<rbrakk> \<Longrightarrow>
6.51 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
6.52 +"\<lbrakk> i < size P; P!i = STORE n \<rbrakk> \<Longrightarrow>
6.53 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
6.54 +"\<lbrakk> i < size P; P!i = JMPF n \<rbrakk> \<Longrightarrow>
6.55 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
6.56 +"\<lbrakk> i < size P; P!i = JMPB n; n \<le> i+1 \<rbrakk> \<Longrightarrow>
6.57 + P \<turnstile> (i,s,stk) \<rightarrow> (i+1-n,s,stk)" |
6.58 +"\<lbrakk> i < size P; P!i = JMPFLESS n \<rbrakk> \<Longrightarrow>
6.59 + P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
6.60 +"\<lbrakk> i < size P; P!i = JMPFGE n \<rbrakk> \<Longrightarrow>
6.61 + P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
6.62
6.63 -subsection "Compiler correctness"
6.64 +code_pred exec1 .
6.65
6.66 -theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
6.67 -shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
6.68 - (is "\<And>p q. ?P c s t p q")
6.69 -proof -
6.70 - from A show "\<And>p q. ?thesis p q"
6.71 - proof induct
6.72 - case Skip thus ?case by simp
6.73 - next
6.74 - case Assign thus ?case by force
6.75 - next
6.76 - case Semi thus ?case by simp (blast intro:rtrancl_trans)
6.77 - next
6.78 - fix b c0 c1 s0 s1 p q
6.79 - assume IH: "\<And>p q. ?P c0 s0 s1 p q"
6.80 - assume "b s0"
6.81 - thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
6.82 - by(simp add: IH[THEN rtrancl_trans])
6.83 - next
6.84 - case IfFalse thus ?case by(simp)
6.85 - next
6.86 - case WhileFalse thus ?case by simp
6.87 - next
6.88 - fix b c and s0::state and s1 s2 p q
6.89 - assume b: "b s0" and
6.90 - IHc: "\<And>p q. ?P c s0 s1 p q" and
6.91 - IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
6.92 - show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
6.93 - using b IHc[THEN rtrancl_trans] IHw by(simp)
6.94 - qed
6.95 +declare exec1.intros[intro]
6.96 +
6.97 +inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
6.98 +where
6.99 +refl: "P \<turnstile> c \<rightarrow>* c" |
6.100 +step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
6.101 +
6.102 +declare exec.intros[intro]
6.103 +
6.104 +lemmas exec_induct = exec.induct[split_format(complete)]
6.105 +
6.106 +code_pred exec .
6.107 +
6.108 +values
6.109 + "{(i,map t [''x'',''y''],stk) | i t stk.
6.110 + [LOAD ''y'', STORE ''x''] \<turnstile>
6.111 + (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
6.112 +
6.113 +
6.114 +subsection{* Verification infrastructure *}
6.115 +
6.116 +lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
6.117 +apply(induct rule: exec.induct)
6.118 + apply blast
6.119 +by (metis exec.step)
6.120 +
6.121 +lemma exec1_subst: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> c' = c'' \<Longrightarrow> P \<turnstile> c \<rightarrow> c''"
6.122 +by auto
6.123 +
6.124 +lemmas exec1_simps = exec1.intros[THEN exec1_subst]
6.125 +
6.126 +text{* Below we need to argue about the execution of code that is embedded in
6.127 +larger programs. For this purpose we show that execution is preserved by
6.128 +appending code to the left or right of a program. *}
6.129 +
6.130 +lemma exec1_appendR: assumes "P \<turnstile> c \<rightarrow> c'" shows "P@P' \<turnstile> c \<rightarrow> c'"
6.131 +proof-
6.132 + from assms show ?thesis
6.133 + by cases (simp_all add: exec1_simps nth_append)
6.134 + -- "All cases proved with the final simp-all"
6.135 qed
6.136
6.137 -text {* The other direction! *}
6.138 +lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
6.139 +apply(induct rule: exec.induct)
6.140 + apply blast
6.141 +by (metis exec1_appendR exec.step)
6.142
6.143 -inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1"
6.144 +lemma exec1_appendL:
6.145 +assumes "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk')"
6.146 +shows "P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
6.147 +proof-
6.148 + from assms show ?thesis
6.149 + by cases (simp_all add: exec1_simps)
6.150 +qed
6.151
6.152 -lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
6.153 -apply(rule iffI)
6.154 - apply(erule rel_pow_E2, simp, fast)
6.155 +lemma exec_appendL:
6.156 + "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
6.157 + P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
6.158 +apply(induct rule: exec_induct)
6.159 + apply blast
6.160 +by (blast intro: exec1_appendL exec.step)
6.161 +
6.162 +text{* Now we specialise the above lemmas to enable automatic proofs of
6.163 +@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
6.164 +pieces of code that we already know how they execute (by induction), combined
6.165 +by @{text "@"} and @{text "#"}. Backward jumps are not supported.
6.166 +The details should be skipped on a first reading.
6.167 +
6.168 +If the pc points beyond the first instruction or part of the program, drop it: *}
6.169 +
6.170 +lemma exec_Cons_Suc[intro]:
6.171 + "P \<turnstile> (i,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
6.172 + instr#P \<turnstile> (Suc i,s,stk) \<rightarrow>* (Suc j,t,stk')"
6.173 +apply(drule exec_appendL[where P'="[instr]"])
6.174 apply simp
6.175 done
6.176
6.177 -lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
6.178 -by(simp add: rtrancl_is_UN_rel_pow)
6.179 -
6.180 -definition
6.181 - forws :: "instr \<Rightarrow> nat set" where
6.182 - "forws instr = (case instr of
6.183 - SET x a \<Rightarrow> {0} |
6.184 - JMPF b n \<Rightarrow> {0,n} |
6.185 - JMPB n \<Rightarrow> {})"
6.186 -
6.187 -definition
6.188 - backws :: "instr \<Rightarrow> nat set" where
6.189 - "backws instr = (case instr of
6.190 - SET x a \<Rightarrow> {} |
6.191 - JMPF b n \<Rightarrow> {} |
6.192 - JMPB n \<Rightarrow> {n})"
6.193 -
6.194 -primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
6.195 -where
6.196 - "closed m n [] = True"
6.197 -| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
6.198 - (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
6.199 -
6.200 -lemma [simp]:
6.201 - "\<And>m n. closed m n (C1@C2) =
6.202 - (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
6.203 -by(induct C1) (simp, simp add:add_ac)
6.204 -
6.205 -theorem [simp]: "\<And>m n. closed m n (compile c)"
6.206 -by(induct c) (simp_all add:backws_def forws_def)
6.207 -
6.208 -lemma drop_lem: "n \<le> size(p1@p2)
6.209 - \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
6.210 - (n \<le> size p1 & p1' = drop n p1)"
6.211 -apply(rule iffI)
6.212 - defer apply simp
6.213 -apply(subgoal_tac "n \<le> size p1")
6.214 - apply simp
6.215 -apply(rule ccontr)
6.216 -apply(drule_tac f = length in arg_cong)
6.217 +lemma exec_appendL_if[intro]:
6.218 + "size P' <= i
6.219 + \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
6.220 + \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
6.221 +apply(drule exec_appendL[where P'=P'])
6.222 apply simp
6.223 done
6.224
6.225 -lemma reduce_exec1:
6.226 - "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
6.227 - \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
6.228 -by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
6.229 +text{* Split the execution of a compound program up into the excution of its
6.230 +parts: *}
6.231
6.232 +lemma exec_append_trans[intro]:
6.233 +"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
6.234 + size P \<le> i' \<Longrightarrow>
6.235 + P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
6.236 + j'' = size P + i''
6.237 + \<Longrightarrow>
6.238 + P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
6.239 +by(metis exec_trans[OF exec_appendR exec_appendL_if])
6.240
6.241 -lemma closed_exec1:
6.242 - "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
6.243 - \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
6.244 - \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
6.245 -apply(clarsimp simp add:forws_def backws_def
6.246 - split:instr.split_asm split_if_asm)
6.247 +
6.248 +declare Let_def[simp] eval_nat_numeral[simp]
6.249 +
6.250 +
6.251 +subsection "Compilation"
6.252 +
6.253 +fun acomp :: "aexp \<Rightarrow> instr list" where
6.254 +"acomp (N n) = [LOADI n]" |
6.255 +"acomp (V x) = [LOAD x]" |
6.256 +"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
6.257 +
6.258 +lemma acomp_correct[intro]:
6.259 + "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
6.260 +apply(induct a arbitrary: stk)
6.261 +apply(fastsimp)+
6.262 done
6.263
6.264 -theorem closed_execn_decomp: "\<And>C1 C2 r.
6.265 - \<lbrakk> closed 0 0 (rev C1 @ C2);
6.266 - \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
6.267 - \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
6.268 - \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
6.269 - n = n1+n2"
6.270 -(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
6.271 -proof(induct n)
6.272 - fix C1 C2 r
6.273 - assume "?H C1 C2 r 0"
6.274 - thus "?P C1 C2 r 0" by simp
6.275 +fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> instr list" where
6.276 +"bcomp (B bv) c n = (if bv=c then [JMPF n] else [])" |
6.277 +"bcomp (Not b) c n = bcomp b (\<not>c) n" |
6.278 +"bcomp (And b1 b2) c n =
6.279 + (let cb2 = bcomp b2 c n;
6.280 + m = (if c then size cb2 else size cb2+n);
6.281 + cb1 = bcomp b1 False m
6.282 + in cb1 @ cb2)" |
6.283 +"bcomp (Less a1 a2) c n =
6.284 + acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
6.285 +
6.286 +value
6.287 + "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
6.288 + False 3"
6.289 +
6.290 +lemma bcomp_correct[intro]:
6.291 + "bcomp b c n \<turnstile>
6.292 + (0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
6.293 +proof(induct b arbitrary: c n m)
6.294 + case Not
6.295 + from Not[of "~c"] show ?case by fastsimp
6.296 next
6.297 - fix C1 C2 r n
6.298 - assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
6.299 - assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
6.300 - show "?P C1 C2 r (Suc n)"
6.301 - proof (cases C2)
6.302 - assume "C2 = []" with H show ?thesis by simp
6.303 - next
6.304 - fix instr tlC2
6.305 - assume C2: "C2 = instr # tlC2"
6.306 - from H C2 obtain p' q' r'
6.307 - where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
6.308 - and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
6.309 - by(fastsimp simp add:rel_pow_commute)
6.310 - from CL closed_exec1[OF _ 1] C2
6.311 - obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
6.312 - and same: "rev C1' @ C2' = rev C1 @ C2"
6.313 - by fastsimp
6.314 - have rev_same: "rev C2' @ C1' = rev C2 @ C1"
6.315 - proof -
6.316 - have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
6.317 - also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
6.318 - also have "\<dots> = rev C2 @ C1" by simp
6.319 - finally show ?thesis .
6.320 - qed
6.321 - hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
6.322 - from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
6.323 - \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
6.324 - by(simp add:pq' rev_same')
6.325 - from IH[OF _ n'] CL
6.326 - obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
6.327 - "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
6.328 - n = n1 + n2"
6.329 - by(fastsimp simp add: same rev_same rev_same')
6.330 - moreover
6.331 - from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
6.332 - by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
6.333 - ultimately show ?thesis by (fastsimp simp del:relpow.simps)
6.334 - qed
6.335 -qed
6.336 + case (And b1 b2)
6.337 + from And(1)[of "False"] And(2)[of "c"] show ?case by fastsimp
6.338 +qed fastsimp+
6.339
6.340 -lemma execn_decomp:
6.341 -"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
6.342 - \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
6.343 - \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
6.344 - n = n1+n2"
6.345 -using closed_execn_decomp[of "[]",simplified] by simp
6.346
6.347 -lemma exec_star_decomp:
6.348 -"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
6.349 - \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
6.350 - \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
6.351 -by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
6.352 +fun ccomp :: "com \<Rightarrow> instr list" where
6.353 +"ccomp SKIP = []" |
6.354 +"ccomp (x ::= a) = acomp a @ [STORE x]" |
6.355 +"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
6.356 +"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
6.357 + (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
6.358 + in cb @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" |
6.359 +"ccomp (WHILE b DO c) =
6.360 + (let cc = ccomp c; cb = bcomp b False (size cc + 1)
6.361 + in cb @ cc @ [JMPB (size cb + size cc + 1)])"
6.362
6.363 +value "ccomp
6.364 + (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
6.365 + ELSE ''v'' ::= V ''u'')"
6.366
6.367 -(* Alternative:
6.368 -lemma exec_comp_n:
6.369 -"\<And>p1 p2 q r t n.
6.370 - \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
6.371 - \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
6.372 - \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
6.373 - n = n1+n2"
6.374 - (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")
6.375 -proof (induct c)
6.376 -*)
6.377 +value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
6.378
6.379 -text{*Warning:
6.380 -@{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"}
6.381 -is not true! *}
6.382
6.383 -theorem "\<And>s t.
6.384 - \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
6.385 -proof (induct c)
6.386 - fix s t
6.387 - assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
6.388 - thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
6.389 +subsection "Preservation of sematics"
6.390 +
6.391 +lemma ccomp_correct:
6.392 + "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
6.393 +proof(induct arbitrary: stk rule: big_step_induct)
6.394 + case (Assign x a s)
6.395 + show ?case by (fastsimp simp:fun_upd_def)
6.396 next
6.397 - fix s t v f
6.398 - assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
6.399 - thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
6.400 + case (Semi c1 s1 s2 c2 s3)
6.401 + let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
6.402 + have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
6.403 + using Semi.hyps(2) by (fastsimp)
6.404 + moreover
6.405 + have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
6.406 + using Semi.hyps(4) by (fastsimp)
6.407 + ultimately show ?case by simp (blast intro: exec_trans)
6.408 next
6.409 - fix s1 s3 c1 c2
6.410 - let ?C1 = "compile c1" let ?C2 = "compile c2"
6.411 - assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
6.412 - and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
6.413 - assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
6.414 - then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
6.415 - exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
6.416 - by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
6.417 - from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
6.418 - using exec_star_decomp[of _ "[]" "[]"] by fastsimp
6.419 - have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
6.420 - moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
6.421 - ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
6.422 -next
6.423 - fix s t b c1 c2
6.424 - let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
6.425 - let ?C1 = "compile c1" let ?C2 = "compile c2"
6.426 - assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
6.427 - and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
6.428 - and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
6.429 - show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
6.430 - proof cases
6.431 - assume b: "b s"
6.432 - with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
6.433 - by (fastsimp dest:exec_star_decomp
6.434 - [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
6.435 - hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
6.436 - with b show ?thesis ..
6.437 - next
6.438 - assume b: "\<not> b s"
6.439 - with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
6.440 - using exec_star_decomp[of _ "[]" "[]"] by simp
6.441 - hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
6.442 - with b show ?thesis ..
6.443 - qed
6.444 -next
6.445 - fix b c s t
6.446 - let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
6.447 - let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
6.448 - assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
6.449 - and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
6.450 - from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
6.451 - by(simp add:rtrancl_is_UN_rel_pow) blast
6.452 - { 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"
6.453 - proof (induct n rule: less_induct)
6.454 - fix n
6.455 - 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"
6.456 - fix s
6.457 - assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
6.458 - show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
6.459 - proof cases
6.460 - assume b: "b s"
6.461 - then obtain m where m: "n = Suc m"
6.462 - and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
6.463 - using H by fastsimp
6.464 - then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
6.465 - and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
6.466 - and n12: "m = n1+n2"
6.467 - using execn_decomp[of _ "[?j2]"]
6.468 - by(simp del: execn_simp) fast
6.469 - have n2n: "n2 - 1 < n" using m n12 by arith
6.470 - note b
6.471 - moreover
6.472 - { from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
6.473 - by (simp add:rtrancl_is_UN_rel_pow) fast
6.474 - hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
6.475 - }
6.476 - moreover
6.477 - { have "n2 - 1 < n" using m n12 by arith
6.478 - moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
6.479 - ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
6.480 - }
6.481 - ultimately show ?thesis ..
6.482 - next
6.483 - assume b: "\<not> b s"
6.484 - hence "t = s" using H by simp
6.485 - with b show ?thesis by simp
6.486 - qed
6.487 - qed
6.488 - }
6.489 - with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
6.490 -qed
6.491 -
6.492 -(* TODO: connect with Machine 0 using M_equiv *)
6.493 + case (WhileTrue b s1 c s2 s3)
6.494 + let ?cc = "ccomp c"
6.495 + let ?cb = "bcomp b False (size ?cc + 1)"
6.496 + let ?cw = "ccomp(WHILE b DO c)"
6.497 + have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
6.498 + using WhileTrue(1,3) by fastsimp
6.499 + moreover
6.500 + have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
6.501 + by (fastsimp)
6.502 + moreover
6.503 + have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue(5))
6.504 + ultimately show ?case by(blast intro: exec_trans)
6.505 +qed fastsimp+
6.506
6.507 end
7.1 --- a/src/HOL/IMP/ROOT.ML Wed Jun 01 15:53:47 2011 +0200
7.2 +++ b/src/HOL/IMP/ROOT.ML Wed Jun 01 21:35:34 2011 +0200
7.3 @@ -1,7 +1,23 @@
7.4 -(* Title: HOL/IMP/ROOT.ML
7.5 - Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
7.6 -
7.7 -Caveat: HOLCF/IMP depends on HOL/IMP
7.8 +use_thys
7.9 +["BExp",
7.10 + "ASM",
7.11 + "Small_Step",
7.12 + "Compiler"(*,
7.13 + "Poly_Types",
7.14 + "Sec_Typing",
7.15 + "Sec_TypingT",
7.16 + "Def_Ass_Sound_Big",
7.17 + "Def_Ass_Sound_Small",
7.18 + "Def_Ass2_Sound_Small",
7.19 + "Def_Ass2_Big0",
7.20 + "Live",
7.21 + "Hoare_Examples",
7.22 + "VC",
7.23 + "HoareT",
7.24 + "Procs_Dyn_Vars_Dyn",
7.25 + "Procs_Stat_Vars_Dyn",
7.26 + "Procs_Stat_Vars_Stat",
7.27 + "C_like",
7.28 + "OO"
7.29 *)
7.30 -
7.31 -use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];
7.32 +];
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/IMP/Small_Step.thy Wed Jun 01 21:35:34 2011 +0200
8.3 @@ -0,0 +1,210 @@
8.4 +header "Small-Step Semantics of Commands"
8.5 +
8.6 +theory Small_Step imports Star Big_Step begin
8.7 +
8.8 +subsection "The transition relation"
8.9 +
8.10 +inductive
8.11 + small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
8.12 +where
8.13 +Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
8.14 +
8.15 +Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
8.16 +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')" |
8.17 +
8.18 +IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
8.19 +IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
8.20 +
8.21 +While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
8.22 +
8.23 +
8.24 +abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
8.25 +where "x \<rightarrow>* y == star small_step x y"
8.26 +
8.27 +subsection{* Executability *}
8.28 +
8.29 +code_pred small_step .
8.30 +
8.31 +values "{(c',map t [''x'',''y'',''z'']) |c' t.
8.32 + (''x'' ::= V ''z''; ''y'' ::= V ''x'',
8.33 + lookup[(''x'',3),(''y'',7),(''z'',5)]) \<rightarrow>* (c',t)}"
8.34 +
8.35 +
8.36 +subsection{* Proof infrastructure *}
8.37 +
8.38 +subsubsection{* Induction rules *}
8.39 +
8.40 +text{* The default induction rule @{thm[source] small_step.induct} only works
8.41 +for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are
8.42 +not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant
8.43 +of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
8.44 +@{text"\<rightarrow>"} into pairs: *}
8.45 +lemmas small_step_induct = small_step.induct[split_format(complete)]
8.46 +
8.47 +
8.48 +subsubsection{* Proof automation *}
8.49 +
8.50 +declare small_step.intros[simp,intro]
8.51 +
8.52 +text{* So called transitivity rules. See below. *}
8.53 +
8.54 +declare step[trans] step1[trans]
8.55 +
8.56 +lemma step2[trans]:
8.57 + "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''"
8.58 +by(metis refl step)
8.59 +
8.60 +declare star_trans[trans]
8.61 +
8.62 +text{* Rule inversion: *}
8.63 +
8.64 +inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
8.65 +thm SkipE
8.66 +inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
8.67 +thm AssignE
8.68 +inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
8.69 +thm SemiE
8.70 +inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
8.71 +inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
8.72 +
8.73 +
8.74 +text{* A simple property: *}
8.75 +lemma deterministic:
8.76 + "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
8.77 +apply(induct arbitrary: cs'' rule: small_step.induct)
8.78 +apply blast+
8.79 +done
8.80 +
8.81 +
8.82 +subsection "Equivalence with big-step semantics"
8.83 +
8.84 +lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
8.85 +proof(induct rule: star_induct)
8.86 + case refl thus ?case by simp
8.87 +next
8.88 + case step
8.89 + thus ?case by (metis Semi2 star.step)
8.90 +qed
8.91 +
8.92 +lemma semi_comp:
8.93 + "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
8.94 + \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
8.95 +by(blast intro: star.step star_semi2 star_trans)
8.96 +
8.97 +text{* The following proof corresponds to one on the board where one would
8.98 +show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the
8.99 +also/finally proof steps do: they compose chains, implicitly using the rules
8.100 +declared with attribute [trans] above. *}
8.101 +
8.102 +lemma big_to_small:
8.103 + "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
8.104 +proof (induct rule: big_step.induct)
8.105 + fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
8.106 +next
8.107 + fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
8.108 +next
8.109 + fix c1 c2 s1 s2 s3
8.110 + assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
8.111 + thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
8.112 +next
8.113 + fix s::state and b c0 c1 t
8.114 + assume "bval b s"
8.115 + hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
8.116 + also assume "(c0,s) \<rightarrow>* (SKIP,t)"
8.117 + finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption"
8.118 +next
8.119 + fix s::state and b c0 c1 t
8.120 + assume "\<not>bval b s"
8.121 + hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
8.122 + also assume "(c1,s) \<rightarrow>* (SKIP,t)"
8.123 + finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" .
8.124 +next
8.125 + fix b c and s::state
8.126 + assume b: "\<not>bval b s"
8.127 + let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
8.128 + have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
8.129 + also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
8.130 + finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto
8.131 +next
8.132 + fix b c s s' t
8.133 + let ?w = "WHILE b DO c"
8.134 + let ?if = "IF b THEN c; ?w ELSE SKIP"
8.135 + assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
8.136 + assume c: "(c,s) \<rightarrow>* (SKIP,s')"
8.137 + assume b: "bval b s"
8.138 + have "(?w,s) \<rightarrow> (?if, s)" by blast
8.139 + also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
8.140 + also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
8.141 + finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
8.142 +qed
8.143 +
8.144 +text{* Each case of the induction can be proved automatically: *}
8.145 +lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
8.146 +proof (induct rule: big_step.induct)
8.147 + case Skip show ?case by blast
8.148 +next
8.149 + case Assign show ?case by blast
8.150 +next
8.151 + case Semi thus ?case by (blast intro: semi_comp)
8.152 +next
8.153 + case IfTrue thus ?case by (blast intro: step)
8.154 +next
8.155 + case IfFalse thus ?case by (blast intro: step)
8.156 +next
8.157 + case WhileFalse thus ?case
8.158 + by (metis step step1 small_step.IfFalse small_step.While)
8.159 +next
8.160 + case WhileTrue
8.161 + thus ?case
8.162 + by(metis While semi_comp small_step.IfTrue step[of small_step])
8.163 +qed
8.164 +
8.165 +lemma small1_big_continue:
8.166 + "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
8.167 +apply (induct arbitrary: t rule: small_step.induct)
8.168 +apply auto
8.169 +done
8.170 +
8.171 +lemma small_big_continue:
8.172 + "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
8.173 +apply (induct rule: star.induct)
8.174 +apply (auto intro: small1_big_continue)
8.175 +done
8.176 +
8.177 +lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
8.178 +by (metis small_big_continue Skip)
8.179 +
8.180 +text {*
8.181 + Finally, the equivalence theorem:
8.182 +*}
8.183 +theorem big_iff_small:
8.184 + "cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)"
8.185 +by(metis big_to_small small_to_big)
8.186 +
8.187 +
8.188 +subsection "Final configurations and infinite reductions"
8.189 +
8.190 +definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
8.191 +
8.192 +lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
8.193 +apply(simp add: final_def)
8.194 +apply(induct c)
8.195 +apply blast+
8.196 +done
8.197 +
8.198 +lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
8.199 +by (metis SkipE finalD final_def)
8.200 +
8.201 +text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"}
8.202 +terminates: *}
8.203 +
8.204 +lemma big_iff_small_termination:
8.205 + "(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')"
8.206 +by(simp add: big_iff_small final_iff_SKIP)
8.207 +
8.208 +text{* This is the same as saying that the absence of a big step result is
8.209 +equivalent with absence of a terminating small step sequence, i.e.\ with
8.210 +nontermination. Since @{text"\<rightarrow>"} is determininistic, there is no difference
8.211 +between may and must terminate. *}
8.212 +
8.213 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/IMP/Star.thy Wed Jun 01 21:35:34 2011 +0200
9.3 @@ -0,0 +1,27 @@
9.4 +theory Star imports Main
9.5 +begin
9.6 +
9.7 +inductive
9.8 + star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
9.9 +for r where
9.10 +refl: "star r x x" |
9.11 +step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
9.12 +
9.13 +lemma star_trans:
9.14 + "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
9.15 +proof(induct rule: star.induct)
9.16 + case refl thus ?case .
9.17 +next
9.18 + case step thus ?case by (metis star.step)
9.19 +qed
9.20 +
9.21 +lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
9.22 +
9.23 +declare star.refl[simp,intro]
9.24 +
9.25 +lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
9.26 +by(metis refl step)
9.27 +
9.28 +code_pred star .
9.29 +
9.30 +end
10.1 --- a/src/HOL/IMP/document/root.tex Wed Jun 01 15:53:47 2011 +0200
10.2 +++ b/src/HOL/IMP/document/root.tex Wed Jun 01 21:35:34 2011 +0200
10.3 @@ -1,13 +1,38 @@
10.4 +\documentclass[11pt,a4paper]{article}
10.5 +\usepackage{isabelle,isabellesym}
10.6
10.7 -\documentclass[a4wide]{article}
10.8 -\usepackage{graphicx,isabelle,isabellesym}
10.9 +% further packages required for unusual symbols (see also
10.10 +% isabellesym.sty), use only when needed
10.11 +
10.12 +%\usepackage{amssymb}
10.13 + %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
10.14 + %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
10.15 + %\<triangleq>, \<yen>, \<lozenge>
10.16 +
10.17 +%\usepackage[greek,english]{babel}
10.18 + %option greek for \<euro>
10.19 + %option english (default language) for \<guillemotleft>, \<guillemotright>
10.20 +
10.21 +%\usepackage[latin1]{inputenc}
10.22 + %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
10.23 + %\<threesuperior>, \<threequarters>, \<degree>
10.24 +
10.25 +%\usepackage[only,bigsqcap]{stmaryrd}
10.26 + %for \<Sqinter>
10.27 +
10.28 +%\usepackage{eufrak}
10.29 + %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
10.30 +
10.31 +%\usepackage{textcomp}
10.32 + %for \<cent>, \<currency>
10.33 +
10.34 +% this should be the last package used
10.35 \usepackage{pdfsetup}
10.36
10.37 +% urls in roman style, theory text in math-similar italics
10.38 \urlstyle{rm}
10.39 -\renewcommand{\isachardoublequote}{}
10.40 +\isabellestyle{it}
10.41
10.42 -% pretty printing for the Com language
10.43 -%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
10.44 \newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
10.45 \newcommand{\isasymSKIP}{\CMD{skip}}
10.46 \newcommand{\isasymIF}{\CMD{if}}
10.47 @@ -16,37 +41,26 @@
10.48 \newcommand{\isasymWHILE}{\CMD{while}}
10.49 \newcommand{\isasymDO}{\CMD{do}}
10.50
10.51 -\addtolength{\hoffset}{-1cm}
10.52 -\addtolength{\textwidth}{2cm}
10.53 +% for uniform font size
10.54 +\renewcommand{\isastyle}{\isastyleminor}
10.55 +
10.56
10.57 \begin{document}
10.58
10.59 -\title{IMP --- A {\tt WHILE}-language and its Semantics}
10.60 -\author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
10.61 +\title{Concrete Semantics}
10.62 +\author{TN \& GK}
10.63 \maketitle
10.64
10.65 -\parindent 0pt\parskip 0.5ex
10.66 +\tableofcontents
10.67 +\newpage
10.68
10.69 -\begin{abstract}\noindent
10.70 - The denotational, operational, and axiomatic semantics, a verification
10.71 - condition generator, and all the necessary soundness, completeness and
10.72 - equivalence proofs. Essentially a formalization of the first 100 pages of
10.73 - \cite{Winskel}.
10.74 -
10.75 - An eminently readable description of this theory is found in \cite{Nipkow}.
10.76 - See also HOLCF/IMP for a denotational semantics.
10.77 -\end{abstract}
10.78 -
10.79 -\tableofcontents
10.80 -
10.81 -\begin{center}
10.82 - \includegraphics[scale=0.7]{session_graph}
10.83 -\end{center}
10.84 -
10.85 -\parindent 0pt\parskip 0.5ex
10.86 +% generated text of all theories
10.87 \input{session}
10.88
10.89 -\bibliographystyle{plain}
10.90 +\nocite{Nipkow}
10.91 +
10.92 +% optional bibliography
10.93 +\bibliographystyle{abbrv}
10.94 \bibliography{root}
10.95
10.96 \end{document}