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