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