43141

1 
(* Author: Gerwin Klein, Tobias Nipkow *)


2 


3 
theory Big_Step imports Com begin


4 


5 
subsection "BigStep Semantics of Commands"


6 

45321

7 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepdef}{% *}

43141

8 
inductive


9 
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)


10 
where


11 
Skip: "(SKIP,s) \<Rightarrow> s" 


12 
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" 


13 
Semi: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>


14 
(c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" 


15 


16 
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>


17 
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" 


18 
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>


19 
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" 


20 


21 
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" 


22 
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>


23 
(WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"

45321

24 
text_raw{*}\end{isaverbatimwrite}*}

43141

25 

45324

26 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}

43141

27 
schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"


28 
apply(rule Semi)


29 
apply(rule Assign)


30 
apply simp


31 
apply(rule Assign)


32 
done

45324

33 
text_raw{*}\end{isaverbatimwrite}*}

43141

34 


35 
thm ex[simplified]


36 


37 
text{* We want to execute the bigstep rules: *}


38 


39 
code_pred big_step .


40 


41 
text{* For inductive definitions we need command


42 
\texttt{values} instead of \texttt{value}. *}


43 

44923

44 
values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"

43141

45 


46 
text{* We need to translate the result state into a list


47 
to display it. *}


48 

44036

49 
values "{map t [''x''] t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"

43141

50 

44036

51 
values "{map t [''x''] t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}"

43141

52 


53 
values "{map t [''x'',''y''] t.


54 
(WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),

44036

55 
<''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"

43141

56 


57 


58 
text{* Proof automation: *}


59 


60 
declare big_step.intros [intro]


61 


62 
text{* The standard induction rule


63 
@{thm [display] big_step.induct [no_vars]} *}


64 


65 
thm big_step.induct


66 


67 
text{* A customized induction rule for (c,s) pairs: *}


68 


69 
lemmas big_step_induct = big_step.induct[split_format(complete)]


70 
thm big_step_induct


71 
text {*


72 
@{thm [display] big_step_induct [no_vars]}


73 
*}


74 


75 


76 
subsection "Rule inversion"


77 


78 
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?


79 
That @{prop "s = t"}. This is how we can automatically prove it: *}


80 


81 
inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"


82 
thm skipE


83 


84 
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,


85 
blast and friends (but not simp!) to use it automatically; [elim!] means that


86 
it is applied eagerly.


87 


88 
Similarly for the other commands: *}


89 


90 
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"


91 
thm AssignE


92 
inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"


93 
thm SemiE


94 
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"


95 
thm IfE


96 


97 
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"


98 
thm WhileE


99 
text{* Only [elim]: [elim!] would not terminate. *}


100 


101 
text{* An automatic example: *}


102 


103 
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"


104 
by blast


105 


106 
text{* Rule inversion by hand via the ``cases'' method: *}


107 


108 
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"


109 
shows "t = s"


110 
proof


111 
from assms show ?thesis


112 
proof cases "inverting assms"


113 
case IfTrue thm IfTrue


114 
thus ?thesis by blast


115 
next


116 
case IfFalse thus ?thesis by blast


117 
qed


118 
qed


119 

44070

120 
(* Using rule inversion to prove simplification rules: *)


121 
lemma assign_simp:


122 
"(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"


123 
by auto

43141

124 


125 
subsection "Command Equivalence"


126 


127 
text {*


128 
We call two statements @{text c} and @{text c'} equivalent wrt.\ the


129 
bigstep semantics when \emph{@{text c} started in @{text s} terminates


130 
in @{text s'} iff @{text c'} started in the same @{text s} also terminates


131 
in the same @{text s'}}. Formally:


132 
*}

45321

133 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEquiv}{% *}

43141

134 
abbreviation


135 
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where


136 
"c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"

45321

137 
text_raw{*}\end{isaverbatimwrite}*}

43141

138 


139 
text {*


140 
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).


141 


142 
As an example, we show that loop unfolding is an equivalence


143 
transformation on programs:


144 
*}


145 
lemma unfold_while:


146 
"(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")


147 
proof 


148 
 "to show the equivalence, we look at the derivation tree for"


149 
 "each side and from that construct a derivation tree for the other side"


150 
{ fix s t assume "(?w, s) \<Rightarrow> t"


151 
 "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"


152 
 "then both statements do nothing:"


153 
{ assume "\<not>bval b s"


154 
hence "t = s" using `(?w,s) \<Rightarrow> t` by blast


155 
hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast


156 
}


157 
moreover


158 
 "on the other hand, if @{text b} is @{text True} in state @{text s},"


159 
 {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}


160 
{ assume "bval b s"


161 
with `(?w, s) \<Rightarrow> t` obtain s' where


162 
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto


163 
 "now we can build a derivation tree for the @{text IF}"


164 
 "first, the body of the Truebranch:"


165 
hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)


166 
 "then the whole @{text IF}"


167 
with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)


168 
}


169 
ultimately


170 
 "both cases together give us what we want:"


171 
have "(?iw, s) \<Rightarrow> t" by blast


172 
}


173 
moreover


174 
 "now the other direction:"


175 
{ fix s t assume "(?iw, s) \<Rightarrow> t"


176 
 "again, if @{text b} is @{text False} in state @{text s}, then the Falsebranch"


177 
 "of the @{text IF} is executed, and both statements do nothing:"


178 
{ assume "\<not>bval b s"


179 
hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast


180 
hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast


181 
}


182 
moreover


183 
 "on the other hand, if @{text b} is @{text True} in state @{text s},"


184 
 {* then this time only the @{text IfTrue} rule can have be used *}


185 
{ assume "bval b s"


186 
with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto


187 
 "and for this, only the Semirule is applicable:"


188 
then obtain s' where


189 
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto


190 
 "with this information, we can build a derivation tree for the @{text WHILE}"


191 
with `bval b s`


192 
have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)


193 
}


194 
ultimately


195 
 "both cases together again give us what we want:"


196 
have "(?w, s) \<Rightarrow> t" by blast


197 
}


198 
ultimately


199 
show ?thesis by blast


200 
qed


201 


202 
text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can


203 
prove many such facts automatically. *}


204 

45321

205 
lemma while_unfold:

43141

206 
"(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"


207 
by blast


208 


209 
lemma triv_if:


210 
"(IF b THEN c ELSE c) \<sim> c"


211 
by blast


212 


213 
lemma commute_if:


214 
"(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)


215 
\<sim>


216 
(IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"


217 
by blast


218 


219 


220 
subsection "Execution is deterministic"


221 


222 
text {* This proof is automatic. *}

45321

223 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDeterministic}{% *}

43141

224 
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"

45321

225 
by (induction arbitrary: u rule: big_step.induct) blast+


226 
text_raw{*}\end{isaverbatimwrite}*}


227 

43141

228 


229 
text {*


230 
This is the proof as you might present it in a lecture. The remaining


231 
cases are simple enough to be proved automatically:


232 
*}

45324

233 
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDetLong}{% *}

43141

234 
theorem


235 
"(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t"

45015

236 
proof (induction arbitrary: t' rule: big_step.induct)

43141

237 
 "the only interesting case, @{text WhileTrue}:"


238 
fix b c s s1 t t'


239 
 "The assumptions of the rule:"


240 
assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"


241 
 {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}


242 
assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"


243 
assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"


244 
 "Premise of implication:"


245 
assume "(WHILE b DO c,s) \<Rightarrow> t'"


246 
with `bval b s` obtain s1' where


247 
c: "(c,s) \<Rightarrow> s1'" and


248 
w: "(WHILE b DO c,s1') \<Rightarrow> t'"


249 
by auto


250 
from c IHc have "s1' = s1" by blast


251 
with w IHw show "t' = t" by blast


252 
qed blast+  "prove the rest automatically"

45321

253 
text_raw{*}\end{isaverbatimwrite}*}

43141

254 


255 
end
