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