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