header "Small-Step Semantics of Commands" theory Small_Step imports Star Big_Step begin subsection "The transition relation" inductive small_step :: "com * state => com * state => bool" (infix "->" 55) where Assign: "(x ::= a, s) -> (SKIP, s(x := aval a s))" | Seq1: "(SKIP;;c⇩_{2},s) -> (c⇩_{2},s)" | Seq2: "(c⇩_{1},s) -> (c⇩_{1}',s') ==> (c⇩_{1};;c⇩_{2},s) -> (c⇩_{1}';;c⇩_{2},s')" | IfTrue: "bval b s ==> (IF b THEN c⇩_{1}ELSE c⇩_{2},s) -> (c⇩_{1},s)" | IfFalse: "¬bval b s ==> (IF b THEN c⇩_{1}ELSE c⇩_{2},s) -> (c⇩_{2},s)" | While: "(WHILE b DO c,s) -> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" abbreviation small_steps :: "com * state => com * state => bool" (infix "->*" 55) where "x ->* y == star small_step x y" subsection{* Executability *} code_pred small_step . values "{(c',map t [''x'',''y'',''z'']) |c' t. (''x'' ::= V ''z'';; ''y'' ::= V ''x'', <''x'' := 3, ''y'' := 7, ''z'' := 5>) ->* (c',t)}" subsection{* Proof infrastructure *} subsubsection{* Induction rules *} text{* The default induction rule @{thm[source] small_step.induct} only works for lemmas of the form @{text"a -> b ==> …"} where @{text a} and @{text b} are not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments @{text"->"} into pairs: *} lemmas small_step_induct = small_step.induct[split_format(complete)] subsubsection{* Proof automation *} declare small_step.intros[simp,intro] text{* Rule inversion: *} inductive_cases SkipE[elim!]: "(SKIP,s) -> ct" thm SkipE inductive_cases AssignE[elim!]: "(x::=a,s) -> ct" thm AssignE inductive_cases SeqE[elim]: "(c1;;c2,s) -> ct" thm SeqE inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) -> ct" inductive_cases WhileE[elim]: "(WHILE b DO c, s) -> ct" text{* A simple property: *} lemma deterministic: "cs -> cs' ==> cs -> cs'' ==> cs'' = cs'" apply(induction arbitrary: cs'' rule: small_step.induct) apply blast+ done subsection "Equivalence with big-step semantics" lemma star_seq2: "(c1,s) ->* (c1',s') ==> (c1;;c2,s) ->* (c1';;c2,s')" proof(induction rule: star_induct) case refl thus ?case by simp next case step thus ?case by (metis Seq2 star.step) qed lemma seq_comp: "[| (c1,s1) ->* (SKIP,s2); (c2,s2) ->* (SKIP,s3) |] ==> (c1;;c2, s1) ->* (SKIP,s3)" by(blast intro: star.step star_seq2 star_trans) text{* The following proof corresponds to one on the board where one would show chains of @{text "->"} and @{text "->*"} steps. *} lemma big_to_small: "cs => t ==> cs ->* (SKIP,t)" proof (induction rule: big_step.induct) fix s show "(SKIP,s) ->* (SKIP,s)" by simp next fix x a s show "(x ::= a,s) ->* (SKIP, s(x := aval a s))" by auto next fix c1 c2 s1 s2 s3 assume "(c1,s1) ->* (SKIP,s2)" and "(c2,s2) ->* (SKIP,s3)" thus "(c1;;c2, s1) ->* (SKIP,s3)" by (rule seq_comp) next fix s::state and b c0 c1 t assume "bval b s" hence "(IF b THEN c0 ELSE c1,s) -> (c0,s)" by simp moreover assume "(c0,s) ->* (SKIP,t)" ultimately show "(IF b THEN c0 ELSE c1,s) ->* (SKIP,t)" by (metis star.simps) next fix s::state and b c0 c1 t assume "¬bval b s" hence "(IF b THEN c0 ELSE c1,s) -> (c1,s)" by simp moreover assume "(c1,s) ->* (SKIP,t)" ultimately show "(IF b THEN c0 ELSE c1,s) ->* (SKIP,t)" by (metis star.simps) next fix b c and s::state assume b: "¬bval b s" let ?if = "IF b THEN c;; WHILE b DO c ELSE SKIP" have "(WHILE b DO c,s) -> (?if, s)" by blast moreover have "(?if,s) -> (SKIP, s)" by (simp add: b) ultimately show "(WHILE b DO c,s) ->* (SKIP,s)" by(metis star.refl star.step) next fix b c s s' t let ?w = "WHILE b DO c" let ?if = "IF b THEN c;; ?w ELSE SKIP" assume w: "(?w,s') ->* (SKIP,t)" assume c: "(c,s) ->* (SKIP,s')" assume b: "bval b s" have "(?w,s) -> (?if, s)" by blast moreover have "(?if, s) -> (c;; ?w, s)" by (simp add: b) moreover have "(c;; ?w,s) ->* (SKIP,t)" by(rule seq_comp[OF c w]) ultimately show "(WHILE b DO c,s) ->* (SKIP,t)" by (metis star.simps) qed text{* Each case of the induction can be proved automatically: *} lemma "cs => t ==> cs ->* (SKIP,t)" proof (induction rule: big_step.induct) case Skip show ?case by blast next case Assign show ?case by blast next case Seq thus ?case by (blast intro: seq_comp) next case IfTrue thus ?case by (blast intro: star.step) next case IfFalse thus ?case by (blast intro: star.step) next case WhileFalse thus ?case by (metis star.step star_step1 small_step.IfFalse small_step.While) next case WhileTrue thus ?case by(metis While seq_comp small_step.IfTrue star.step[of small_step]) qed lemma small1_big_continue: "cs -> cs' ==> cs' => t ==> cs => t" apply (induction arbitrary: t rule: small_step.induct) apply auto done lemma small_to_big: "cs ->* (SKIP,t) ==> cs => t" apply (induction cs "(SKIP,t)" rule: star.induct) apply (auto intro: small1_big_continue) done text {* Finally, the equivalence theorem: *} theorem big_iff_small: "cs => t = cs ->* (SKIP,t)" by(metis big_to_small small_to_big) subsection "Final configurations and infinite reductions" definition "final cs <-> ¬(EX cs'. cs -> cs')" lemma finalD: "final (c,s) ==> c = SKIP" apply(simp add: final_def) apply(induction c) apply blast+ done lemma final_iff_SKIP: "final (c,s) = (c = SKIP)" by (metis SkipE finalD final_def) text{* Now we can show that @{text"=>"} yields a final state iff @{text"->"} terminates: *} lemma big_iff_small_termination: "(EX t. cs => t) <-> (EX cs'. cs ->* cs' ∧ final cs')" by(simp add: big_iff_small final_iff_SKIP) text{* This is the same as saying that the absence of a big step result is equivalent with absence of a terminating small step sequence, i.e.\ with nontermination. Since @{text"->"} is determininistic, there is no difference between may and must terminate. *} end