src/HOL/IMP/Small_Step.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45218 f115540543d8
child 45265 521508e85c0d
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@43141
     1
header "Small-Step Semantics of Commands"
nipkow@43141
     2
nipkow@43141
     3
theory Small_Step imports Star Big_Step begin
nipkow@43141
     4
nipkow@43141
     5
subsection "The transition relation"
nipkow@43141
     6
nipkow@43141
     7
inductive
nipkow@43141
     8
  small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
nipkow@43141
     9
where
nipkow@43141
    10
Assign:  "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
nipkow@43141
    11
nipkow@43141
    12
Semi1:   "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
nipkow@43141
    13
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')" |
nipkow@43141
    14
nipkow@43141
    15
IfTrue:  "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
nipkow@43141
    16
IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
nipkow@43141
    17
nipkow@43141
    18
While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
nipkow@43141
    19
nipkow@43141
    20
nipkow@43141
    21
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
nipkow@43141
    22
where "x \<rightarrow>* y == star small_step x y"
nipkow@43141
    23
nipkow@43141
    24
subsection{* Executability *}
nipkow@43141
    25
nipkow@43141
    26
code_pred small_step .
nipkow@43141
    27
nipkow@43141
    28
values "{(c',map t [''x'',''y'',''z'']) |c' t.
nipkow@43141
    29
   (''x'' ::= V ''z''; ''y'' ::= V ''x'',
kleing@44036
    30
    <''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
nipkow@43141
    31
nipkow@43141
    32
nipkow@43141
    33
subsection{* Proof infrastructure *}
nipkow@43141
    34
nipkow@43141
    35
subsubsection{* Induction rules *}
nipkow@43141
    36
nipkow@43141
    37
text{* The default induction rule @{thm[source] small_step.induct} only works
nipkow@43141
    38
for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are
nipkow@43141
    39
not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant
nipkow@43141
    40
of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
nipkow@43141
    41
@{text"\<rightarrow>"} into pairs: *}
nipkow@43141
    42
lemmas small_step_induct = small_step.induct[split_format(complete)]
nipkow@43141
    43
nipkow@43141
    44
nipkow@43141
    45
subsubsection{* Proof automation *}
nipkow@43141
    46
nipkow@43141
    47
declare small_step.intros[simp,intro]
nipkow@43141
    48
nipkow@43141
    49
text{* Rule inversion: *}
nipkow@43141
    50
nipkow@43141
    51
inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
nipkow@43141
    52
thm SkipE
nipkow@43141
    53
inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
nipkow@43141
    54
thm AssignE
nipkow@43141
    55
inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
nipkow@43141
    56
thm SemiE
nipkow@43141
    57
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
nipkow@43141
    58
inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
nipkow@43141
    59
nipkow@43141
    60
nipkow@43141
    61
text{* A simple property: *}
nipkow@43141
    62
lemma deterministic:
nipkow@43141
    63
  "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
nipkow@45015
    64
apply(induction arbitrary: cs'' rule: small_step.induct)
nipkow@43141
    65
apply blast+
nipkow@43141
    66
done
nipkow@43141
    67
nipkow@43141
    68
nipkow@43141
    69
subsection "Equivalence with big-step semantics"
nipkow@43141
    70
nipkow@43141
    71
lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
nipkow@45015
    72
proof(induction rule: star_induct)
nipkow@43141
    73
  case refl thus ?case by simp
nipkow@43141
    74
next
nipkow@43141
    75
  case step
nipkow@43141
    76
  thus ?case by (metis Semi2 star.step)
nipkow@43141
    77
qed
nipkow@43141
    78
nipkow@43141
    79
lemma semi_comp:
nipkow@43141
    80
  "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
nipkow@43141
    81
   \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
nipkow@43141
    82
by(blast intro: star.step star_semi2 star_trans)
nipkow@43141
    83
nipkow@43141
    84
text{* The following proof corresponds to one on the board where one would
kleing@45218
    85
show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *}
nipkow@43141
    86
nipkow@43141
    87
lemma big_to_small:
nipkow@43141
    88
  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
nipkow@45015
    89
proof (induction rule: big_step.induct)
nipkow@43141
    90
  fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
nipkow@43141
    91
next
nipkow@43141
    92
  fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
nipkow@43141
    93
next
nipkow@43141
    94
  fix c1 c2 s1 s2 s3
nipkow@43141
    95
  assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
nipkow@43141
    96
  thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
nipkow@43141
    97
next
nipkow@43141
    98
  fix s::state and b c0 c1 t
nipkow@43141
    99
  assume "bval b s"
nipkow@43141
   100
  hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
kleing@45218
   101
  moreover assume "(c0,s) \<rightarrow>* (SKIP,t)"
kleing@45218
   102
  ultimately 
kleing@45218
   103
  show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
nipkow@43141
   104
next
nipkow@43141
   105
  fix s::state and b c0 c1 t
nipkow@43141
   106
  assume "\<not>bval b s"
nipkow@43141
   107
  hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
kleing@45218
   108
  moreover assume "(c1,s) \<rightarrow>* (SKIP,t)"
kleing@45218
   109
  ultimately 
kleing@45218
   110
  show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
nipkow@43141
   111
next
nipkow@43141
   112
  fix b c and s::state
nipkow@43141
   113
  assume b: "\<not>bval b s"
nipkow@43141
   114
  let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
nipkow@43141
   115
  have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
kleing@45218
   116
  moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
kleing@45218
   117
  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by (metis refl step)
nipkow@43141
   118
next
nipkow@43141
   119
  fix b c s s' t
nipkow@43141
   120
  let ?w  = "WHILE b DO c"
nipkow@43141
   121
  let ?if = "IF b THEN c; ?w ELSE SKIP"
nipkow@43141
   122
  assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
nipkow@43141
   123
  assume c: "(c,s) \<rightarrow>* (SKIP,s')"
nipkow@43141
   124
  assume b: "bval b s"
nipkow@43141
   125
  have "(?w,s) \<rightarrow> (?if, s)" by blast
kleing@45218
   126
  moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
kleing@45218
   127
  moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
kleing@45218
   128
  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
nipkow@43141
   129
qed
nipkow@43141
   130
nipkow@43141
   131
text{* Each case of the induction can be proved automatically: *}
nipkow@43141
   132
lemma  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
nipkow@45015
   133
proof (induction rule: big_step.induct)
nipkow@43141
   134
  case Skip show ?case by blast
nipkow@43141
   135
next
nipkow@43141
   136
  case Assign show ?case by blast
nipkow@43141
   137
next
nipkow@43141
   138
  case Semi thus ?case by (blast intro: semi_comp)
nipkow@43141
   139
next
nipkow@43141
   140
  case IfTrue thus ?case by (blast intro: step)
nipkow@43141
   141
next
nipkow@43141
   142
  case IfFalse thus ?case by (blast intro: step)
nipkow@43141
   143
next
nipkow@43141
   144
  case WhileFalse thus ?case
nipkow@43141
   145
    by (metis step step1 small_step.IfFalse small_step.While)
nipkow@43141
   146
next
nipkow@43141
   147
  case WhileTrue
nipkow@43141
   148
  thus ?case
nipkow@43141
   149
    by(metis While semi_comp small_step.IfTrue step[of small_step])
nipkow@43141
   150
qed
nipkow@43141
   151
nipkow@43141
   152
lemma small1_big_continue:
nipkow@43141
   153
  "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
nipkow@45015
   154
apply (induction arbitrary: t rule: small_step.induct)
nipkow@43141
   155
apply auto
nipkow@43141
   156
done
nipkow@43141
   157
nipkow@43141
   158
lemma small_big_continue:
nipkow@43141
   159
  "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
nipkow@45015
   160
apply (induction rule: star.induct)
nipkow@43141
   161
apply (auto intro: small1_big_continue)
nipkow@43141
   162
done
nipkow@43141
   163
nipkow@43141
   164
lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
nipkow@43141
   165
by (metis small_big_continue Skip)
nipkow@43141
   166
nipkow@43141
   167
text {*
nipkow@43141
   168
  Finally, the equivalence theorem:
nipkow@43141
   169
*}
nipkow@43141
   170
theorem big_iff_small:
nipkow@43141
   171
  "cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)"
nipkow@43141
   172
by(metis big_to_small small_to_big)
nipkow@43141
   173
nipkow@43141
   174
nipkow@43141
   175
subsection "Final configurations and infinite reductions"
nipkow@43141
   176
nipkow@43141
   177
definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
nipkow@43141
   178
nipkow@43141
   179
lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
nipkow@43141
   180
apply(simp add: final_def)
nipkow@45015
   181
apply(induction c)
nipkow@43141
   182
apply blast+
nipkow@43141
   183
done
nipkow@43141
   184
nipkow@43141
   185
lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
nipkow@43141
   186
by (metis SkipE finalD final_def)
nipkow@43141
   187
nipkow@43141
   188
text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"}
nipkow@43141
   189
terminates: *}
nipkow@43141
   190
nipkow@43141
   191
lemma big_iff_small_termination:
nipkow@43141
   192
  "(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')"
nipkow@43141
   193
by(simp add: big_iff_small final_iff_SKIP)
nipkow@43141
   194
nipkow@43141
   195
text{* This is the same as saying that the absence of a big step result is
nipkow@43141
   196
equivalent with absence of a terminating small step sequence, i.e.\ with
nipkow@43141
   197
nontermination.  Since @{text"\<rightarrow>"} is determininistic, there is no difference
nipkow@43141
   198
between may and must terminate. *}
nipkow@43141
   199
nipkow@43141
   200
end