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