# Theory Transition

Up to index of Isabelle/HOL/IMP

theory Transition
imports Natural
begin

    (*  Title:        HOL/IMP/Transition.thy
        ID:           $Id: Transition.thy,v 1.17 2005/06/17 14:13:07 haftmann Exp $
        Author:       Tobias Nipkow & Robert Sandner, TUM
        Isar Version: Gerwin Klein, 2001
        Copyright     1996 TUM
    *)

    header "Transition Semantics of Commands"

    theory Transition imports Natural begin

    subsection "The transition relation"

    text {*
      We formalize the transition semantics as in \cite{Nielson}. This
      makes some of the rules a bit more intuitive, but also requires
      some more (internal) formal overhead.

      Since configurations that have terminated are written without
      a statement, the transition relation is not
      @{typ "((com × state) × (com × state)) set"}
      but instead:
    *}
    consts evalc1 :: "((com option × state) × (com option × state)) set"

    text {*
      Some syntactic sugar that we will use to hide the
      @{text option} part in configurations:
    *}
    syntax
      "_angle" :: "[com, state] => com option × state" ("<_,_>")
      "_angle2" :: "state => com option × state" ("<_>")

    syntax (xsymbols)
      "_angle" :: "[com, state] => com option × state" ("⟨_,_⟩")
      "_angle2" :: "state => com option × state" ("⟨_⟩")

    syntax (HTML output)
      "_angle" :: "[com, state] => com option × state" ("⟨_,_⟩")
      "_angle2" :: "state => com option × state" ("⟨_⟩")

    translations
      "⟨c,s⟩" == "(Some c, s)"
      "⟨s⟩" == "(None, s)"

    text {*
      More syntactic sugar for the transition relation, and its
      iteration.
    *}
    syntax
      "_evalc1" :: "[(com option×state),(com option×state)] => bool"
        ("_ -1-> _" [60,60] 60)
      "_evalcn" :: "[(com option×state),nat,(com option×state)] => bool"
        ("_ -_-> _" [60,60,60] 60)
      "_evalc*" :: "[(com option×state),(com option×state)] => bool"
        ("_ -*-> _" [60,60] 60)

    syntax (xsymbols)
      "_evalc1" :: "[(com option×state),(com option×state)] => bool"
        ("_ -->1 _" [60,60] 61)
      "_evalcn" :: "[(com option×state),nat,(com option×state)] => bool"
        ("_ -_->1 _" [60,60,60] 60)
      "_evalc*" :: "[(com option×state),(com option×state)] => bool"
        ("_ -->1* _" [60,60] 60)

    translations
      "cs -->1 cs'" == "(cs,cs') ∈ evalc1"
      "cs -n->1 cs'" == "(cs,cs') ∈ evalc1^n"
      "cs -->1* cs'" == "(cs,cs') ∈ evalc1^*"

      -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"},
            so we also include: *}
      "cs0 -->1 (c1,s1)" == "(cs0,c1,s1) ∈ evalc1"
      "cs0 -n->1 (c1,s1)" == "(cs0,c1,s1) ∈ evalc1^n"
      "cs0 -->1* (c1,s1)" == "(cs0,c1,s1) ∈ evalc1^*"

    text {*
      Now, finally, we are set to write down the rules for our small step semantics:
    *}
    inductive evalc1
      intros
      Skip:    "⟨\<SKIP>, s⟩ -->1 ⟨s⟩"
      Assign:  "⟨x :== a, s⟩ -->1 ⟨s[x \<mapsto> a s]⟩"

      Semi1:   "⟨c0,s⟩ -->1 ⟨s'⟩ ==> ⟨c0;c1,s⟩ -->1 ⟨c1,s'⟩"
      Semi2:   "⟨c0,s⟩ -->1 ⟨c0',s'⟩ ==> ⟨c0;c1,s⟩ -->1 ⟨c0';c1,s'⟩"

      IfTrue:  "b s ==> ⟨\<IF> b \<THEN> c1 \<ELSE> c2,s⟩ -->1 ⟨c1,s⟩"
      IfFalse: "¬b s ==> ⟨\<IF> b \<THEN> c1 \<ELSE> c2,s⟩ -->1 ⟨c2,s⟩"

      While:   "⟨\<WHILE> b \<DO> c,s⟩ -->1 ⟨\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s⟩"

    lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"

    (*<*)
    (* fixme: move to Relation_Power.thy *)
    lemma rel_pow_Suc_E2 [elim!]:
      "[| (x, z) ∈ R ^ Suc n; !!y. [| (x, y) ∈ R; (y, z) ∈ R ^ n |] ==> P |] ==> P"
      by (drule rel_pow_Suc_D2) blast

    lemma rtrancl_imp_rel_pow: "p ∈ R^* ==> ∃n. p ∈ R^n"
    proof -
      assume "p ∈ R*"
      moreover obtain x y where p: "p = (x,y)" by (cases p)
      ultimately have "(x,y) ∈ R*" by hypsubst
      hence "∃n. (x,y) ∈ R^n"
      proof induct
        fix a have "(a,a) ∈ R^0" by simp
        thus "∃n. (a,a) ∈ R ^ n" ..
      next
        fix a b c assume "∃n. (a,b) ∈ R ^ n"
        then obtain n where "(a,b) ∈ R^n" ..
        moreover assume "(b,c) ∈ R"
        ultimately have "(a,c) ∈ R^(Suc n)" by auto
        thus "∃n. (a,c) ∈ R^n" ..
      qed
      with p show ?thesis by hypsubst
    qed
    (*>*)
    text {*
      As for the big step semantics you can read these rules in a
      syntax directed way:
    *}
    lemma SKIP_1: "⟨\<SKIP>, s⟩ -->1 y = (y = ⟨s⟩)"
      by (rule, cases set: evalc1, auto)

    lemma Assign_1: "⟨x :== a, s⟩ -->1 y = (y = ⟨s[x \<mapsto> a s]⟩)"
      by (rule, cases set: evalc1, auto)

    lemma Cond_1:
      "⟨\<IF> b \<THEN> c1 \<ELSE> c2, s⟩ -->1 y = ((b s --> y = ⟨c1, s⟩) ∧ (¬b s --> y = ⟨c2, s⟩))"
      by (rule, cases set: evalc1, auto)

    lemma While_1:
      "⟨\<WHILE> b \<DO> c, s⟩ -->1 y = (y = ⟨\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s⟩)"
      by (rule, cases set: evalc1, auto)

    lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1

    subsection "Examples"

    lemma
      "s x = 0 ==> ⟨\<WHILE> λs. s x ≠ 1 \<DO> (x:== λs. s x+1), s⟩ -->1* ⟨s[x \<mapsto> 1]⟩"
      (is "_ ==> ⟨?w, _⟩ -->1* _")
    proof -
      let ?c  = "x:== λs. s x+1"
      let ?if = "\<IF> λs. s x ≠ 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
      assume [simp]: "s x = 0"
      have "⟨?w, s⟩ -->1  ⟨?if, s⟩" ..
      also have "⟨?if, s⟩ -->1 ⟨?c; ?w, s⟩" by simp
      also have "⟨?c; ?w, s⟩ -->1 ⟨?w, s[x \<mapsto> 1]⟩" by (rule Semi1, simp)
      also have "⟨?w, s[x \<mapsto> 1]⟩ -->1 ⟨?if, s[x \<mapsto> 1]⟩" ..
      also have "⟨?if, s[x \<mapsto> 1]⟩ -->1 ⟨\<SKIP>, s[x \<mapsto> 1]⟩" by (simp add: update_def)
      also have "⟨\<SKIP>, s[x \<mapsto> 1]⟩ -->1 ⟨s[x \<mapsto> 1]⟩" ..
      finally show ?thesis ..
    qed

    lemma
      "s x = 2 ==> ⟨\<WHILE> λs. s x ≠ 1 \<DO> (x:== λs. s x+1), s⟩ -->1* s'"
      (is "_ ==> ⟨?w, _⟩ -->1* s'")
    proof -
      let ?c = "x:== λs. s x+1"
      let ?if = "\<IF> λs. s x ≠ 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
      assume [simp]: "s x = 2"
      note update_def [simp]
      have "⟨?w, s⟩ -->1  ⟨?if, s⟩" ..
      also have "⟨?if, s⟩ -->1 ⟨?c; ?w, s⟩" by simp
      also have "⟨?c; ?w, s⟩ -->1 ⟨?w, s[x \<mapsto> 3]⟩" by (rule Semi1, simp)
      also have "⟨?w, s[x \<mapsto> 3]⟩ -->1 ⟨?if, s[x \<mapsto> 3]⟩" ..
      also have "⟨?if, s[x \<mapsto> 3]⟩ -->1  ⟨?c; ?w, s[x \<mapsto> 3]⟩" by simp
      also have "⟨?c; ?w, s[x \<mapsto> 3]⟩ -->1 ⟨?w, s[x \<mapsto> 4]⟩" by (rule Semi1, simp)
      also have "⟨?w, s[x \<mapsto> 4]⟩ -->1 ⟨?if, s[x \<mapsto> 4]⟩" ..
      also have "⟨?if, s[x \<mapsto> 4]⟩ -->1  ⟨?c; ?w, s[x \<mapsto> 4]⟩" by simp
      also have "⟨?c; ?w, s[x \<mapsto> 4]⟩ -->1 ⟨?w, s[x \<mapsto> 5]⟩" by (rule Semi1, simp)
      oops

    subsection "Basic properties"

    text {*
      There are no \emph{stuck} programs:
    *}
    lemma no_stuck: "∃y. ⟨c,s⟩ -->1 y"
    proof (induct c)
      -- "case Semi:"
      fix c1 c2 assume "∃y. ⟨c1,s⟩ -->1 y"
      then obtain y where "⟨c1,s⟩ -->1 y" ..
      then obtain c1' s' where "⟨c1,s⟩ -->1 ⟨s'⟩ ∨ ⟨c1,s⟩ -->1 ⟨c1',s'⟩"
        by (cases y, cases "fst y", auto)
      thus "∃s'. ⟨c1;c2,s⟩ -->1 s'" by auto
    next
      -- "case If:"
      fix b c1 c2 assume "∃y. ⟨c1,s⟩ -->1 y" and "∃y. ⟨c2,s⟩ -->1 y"
      thus "∃y. ⟨\<IF> b \<THEN> c1 \<ELSE> c2, s⟩ -->1 y" by (cases "b s") auto
    qed auto -- "the rest is trivial"

    text {*
      If a configuration does not contain a statement, the program
      has terminated and there is no next configuration:
    *}
    lemma stuck [elim!]: "⟨s⟩ -->1 y ==> P"
      by (auto elim: evalc1.elims)

    lemma evalc_None_retrancl [simp, dest!]: "⟨s⟩ -->1* s' ==> s' = ⟨s⟩"
      by (erule rtrancl_induct) auto

    (*<*)
    (* fixme: relpow.simps don't work *)
    lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
    lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
    lemmas [simp del] = relpow.simps
    (*>*)
    lemma evalc1_None_0 [simp, dest!]: "⟨s⟩ -n->1 y = (n = 0 ∧ y = ⟨s⟩)"
      by (cases n) auto

    lemma SKIP_n: "⟨\<SKIP>, s⟩ -n->1 ⟨s'⟩ ==> s' = s ∧ n=1"
      by (cases n) auto

    subsection "Equivalence to natural semantics (after Nielson and Nielson)"

    text {*
      We first need two lemmas about semicolon statements:
      decomposition and composition.
    *}
    lemma semiD:
      "!!c1 c2 s s''. ⟨c1; c2, s⟩ -n->1 ⟨s''⟩ ==>
      ∃i j s'. ⟨c1, s⟩ -i->1 ⟨s'⟩ ∧ ⟨c2, s'⟩ -j->1 ⟨s''⟩ ∧ n = i+j"
      (is "PROP ?P n")
    proof (induct n)
      show "PROP ?P 0" by simp
    next
      fix n assume IH: "PROP ?P n"
      show "PROP ?P (Suc n)"
      proof -
        fix c1 c2 s s''
        assume "⟨c1; c2, s⟩ -Suc n->1 ⟨s''⟩"
        then obtain y where
          1: "⟨c1; c2, s⟩ -->1 y" and
          n: "y -n->1 ⟨s''⟩"
          by blast

        from 1
        show "∃i j s'. ⟨c1, s⟩ -i->1 ⟨s'⟩ ∧ ⟨c2, s'⟩ -j->1 ⟨s''⟩ ∧ Suc n = i+j"
          (is "∃i j s'. ?Q i j s'")
        proof (cases set: evalc1)
          case Semi1
          then obtain s' where
            "y = ⟨c2, s'⟩" and "⟨c1, s⟩ -->1 ⟨s'⟩"
            by auto
          with 1 n have "?Q 1 n s'" by simp
          thus ?thesis by blast
        next
          case Semi2
          then obtain c1' s' where
            y:  "y = ⟨c1'; c2, s'⟩" and
            c1: "⟨c1, s⟩ -->1 ⟨c1', s'⟩"
            by auto
          with n have "⟨c1'; c2, s'⟩ -n->1 ⟨s''⟩" by simp
          with IH obtain i j s0 where
            c1': "⟨c1',s'⟩ -i->1 ⟨s0⟩" and
            c2:  "⟨c2,s0⟩ -j->1 ⟨s''⟩" and
            i:   "n = i+j"
            by fast

          from c1 c1'
          have "⟨c1,s⟩ -(i+1)->1 ⟨s0⟩" by (auto intro: rel_pow_Suc_I2)
          with c2 i
          have "?Q (i+1) j s0" by simp
          thus ?thesis by blast
        qed auto -- "the remaining cases cannot occur"
      qed
    qed

    lemma semiI:
      "!!c0 s s''. ⟨c0,s⟩ -n->1 ⟨s''⟩ ==> ⟨c1,s''⟩ -->1* ⟨s'⟩ ==> ⟨c0; c1, s⟩ -->1* ⟨s'⟩"
    proof (induct n)
      fix c0 s s'' assume "⟨c0,s⟩ -(0::nat)->1 ⟨s''⟩"
      hence False by simp
      thus "?thesis c0 s s''" ..
    next
      fix c0 s s'' n
      assume c0: "⟨c0,s⟩ -Suc n->1 ⟨s''⟩"
      assume c1: "⟨c1,s''⟩ -->1* ⟨s'⟩"
      assume IH: "!!c0 s s''.
        ⟨c0,s⟩ -n->1 ⟨s''⟩ ==> ⟨c1,s''⟩ -->1* ⟨s'⟩ ==> ⟨c0; c1,s⟩ -->1* ⟨s'⟩"
      from c0 obtain y where
        1: "⟨c0,s⟩ -->1 y" and n: "y -n->1 ⟨s''⟩" by blast
      from 1 obtain c0' s0' where
        "y = ⟨s0'⟩ ∨ y = ⟨c0', s0'⟩"
        by (cases y, cases "fst y", auto)
      moreover
      { assume y: "y = ⟨s0'⟩"
        with n have "s'' = s0'" by simp
        with y 1 have "⟨c0; c1,s⟩ -->1 ⟨c1, s''⟩" by blast
        with c1 have "⟨c0; c1,s⟩ -->1* ⟨s'⟩" by (blast intro: rtrancl_trans)
      }
      moreover
      { assume y: "y = ⟨c0', s0'⟩"
        with n have "⟨c0', s0'⟩ -n->1 ⟨s''⟩" by blast
        with IH c1 have "⟨c0'; c1,s0'⟩ -->1* ⟨s'⟩" by blast
        moreover
        from y 1 have "⟨c0; c1,s⟩ -->1 ⟨c0'; c1,s0'⟩" by blast
        hence "⟨c0; c1,s⟩ -->1* ⟨c0'; c1,s0'⟩" by blast
        ultimately
        have "⟨c0; c1,s⟩ -->1* ⟨s'⟩" by (blast intro: rtrancl_trans)
      }
      ultimately
      show "⟨c0; c1,s⟩ -->1* ⟨s'⟩" by blast
    qed

    text {*
      The easy direction of the equivalence proof:
    *}
    lemma evalc_imp_evalc1:
      "⟨c,s⟩ -->c s' ==> ⟨c, s⟩ -->1* ⟨s'⟩"
    proof -
      assume "⟨c,s⟩ -->c s'"
      thus "⟨c, s⟩ -->1* ⟨s'⟩"
      proof induct
        fix s show "⟨\<SKIP>,s⟩ -->1* ⟨s⟩" by auto
      next
        fix x a s show "⟨x :== a ,s⟩ -->1* ⟨s[x\<mapsto>a s]⟩" by auto
      next
        fix c0 c1 s s'' s'
        assume "⟨c0,s⟩ -->1* ⟨s''⟩"
        then obtain n where "⟨c0,s⟩ -n->1 ⟨s''⟩" by (blast dest: rtrancl_imp_rel_pow)
        moreover
        assume "⟨c1,s''⟩ -->1* ⟨s'⟩"
        ultimately
        show "⟨c0; c1,s⟩ -->1* ⟨s'⟩" by (rule semiI)
      next
        fix s::state and b c0 c1 s'
        assume "b s"
        hence "⟨\<IF> b \<THEN> c0 \<ELSE> c1,s⟩ -->1 ⟨c0,s⟩" by simp
        also assume "⟨c0,s⟩ -->1* ⟨s'⟩"
        finally show "⟨\<IF> b \<THEN> c0 \<ELSE> c1,s⟩ -->1* ⟨s'⟩" .
      next
        fix s::state and b c0 c1 s'
        assume "¬b s"
        hence "⟨\<IF> b \<THEN> c0 \<ELSE> c1,s⟩ -->1 ⟨c1,s⟩" by simp
        also assume "⟨c1,s⟩ -->1* ⟨s'⟩"
        finally show "⟨\<IF> b \<THEN> c0 \<ELSE> c1,s⟩ -->1* ⟨s'⟩" .
      next
        fix b c and s::state
        assume b: "¬b s"
        let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
        have "⟨\<WHILE> b \<DO> c,s⟩ -->1 ⟨?if, s⟩" by blast
        also have "⟨?if,s⟩ -->1 ⟨\<SKIP>, s⟩" by (simp add: b)
        also have "⟨\<SKIP>, s⟩ -->1 ⟨s⟩" by blast
        finally show "⟨\<WHILE> b \<DO> c,s⟩ -->1* ⟨s⟩" ..
      next
        fix b c s s'' s'
        let ?w  = "\<WHILE> b \<DO> c"
        let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
        assume w: "⟨?w,s''⟩ -->1* ⟨s'⟩"
        assume c: "⟨c,s⟩ -->1* ⟨s''⟩"
        assume b: "b s"
        have "⟨?w,s⟩ -->1 ⟨?if, s⟩" by blast
        also have "⟨?if, s⟩ -->1 ⟨c; ?w, s⟩" by (simp add: b)
        also
        from c obtain n where "⟨c,s⟩ -n->1 ⟨s''⟩" by (blast dest: rtrancl_imp_rel_pow)
        with w have "⟨c; ?w,s⟩ -->1* ⟨s'⟩" by - (rule semiI)
        finally show "⟨\<WHILE> b \<DO> c,s⟩ -->1* ⟨s'⟩" ..
      qed
    qed

    text {*
      Finally, the equivalence theorem:
    *}
    theorem evalc_equiv_evalc1:
      "⟨c, s⟩ -->c s' = ⟨c,s⟩ -->1* ⟨s'⟩"
    proof
      assume "⟨c,s⟩ -->c s'"
      show "⟨c, s⟩ -->1* ⟨s'⟩" by (rule evalc_imp_evalc1)
    next
      assume "⟨c, s⟩ -->1* ⟨s'⟩"
      then obtain n where "⟨c, s⟩ -n->1 ⟨s'⟩" by (blast dest: rtrancl_imp_rel_pow)
      moreover
      have "!!c s s'. ⟨c, s⟩ -n->1 ⟨s'⟩ ==> ⟨c,s⟩ -->c s'"
      proof (induct rule: nat_less_induct)
        fix n
        assume IH: "∀m. m < n --> (∀c s s'. ⟨c, s⟩ -m->1 ⟨s'⟩ --> ⟨c,s⟩ -->c s')"
        fix c s s'
        assume c:  "⟨c, s⟩ -n->1 ⟨s'⟩"
        then obtain m where n: "n = Suc m" by (cases n) auto
        with c obtain y where
          c': "⟨c, s⟩ -->1 y" and m: "y -m->1 ⟨s'⟩" by blast
        show "⟨c,s⟩ -->c s'"
        proof (cases c)
          case SKIP
          with c n show ?thesis by auto
        next
          case Assign
          with c n show ?thesis by auto
        next
          fix c1 c2 assume semi: "c = (c1; c2)"
          with c obtain i j s'' where
            c1: "⟨c1, s⟩ -i->1 ⟨s''⟩" and
            c2: "⟨c2, s''⟩ -j->1 ⟨s'⟩" and
            ij: "n = i+j"
            by (blast dest: semiD)
          from c1 c2 obtain
            "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
          with ij obtain
            i: "i < n" and j: "j < n" by simp
          from c1 i IH
          have "⟨c1,s⟩ -->c s''" by blast
          moreover
          from c2 j IH
          have "⟨c2,s''⟩ -->c s'" by blast
          moreover
          note semi
          ultimately
          show "⟨c,s⟩ -->c s'" by blast
        next
          fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
          { assume True: "b s = True"
            with If c n
            have "⟨c1,s⟩ -m->1 ⟨s'⟩" by auto
            with n IH
            have "⟨c1,s⟩ -->c s'" by blast
            with If True
            have "⟨c,s⟩ -->c s'" by simp
          }
          moreover
          { assume False: "b s = False"
            with If c n
            have "⟨c2,s⟩ -m->1 ⟨s'⟩" by auto
            with n IH
            have "⟨c2,s⟩ -->c s'" by blast
            with If False
            have "⟨c,s⟩ -->c s'" by simp
          }
          ultimately
          show "⟨c,s⟩ -->c s'" by (cases "b s") auto
        next
          fix b c' assume w: "c = \<WHILE> b \<DO> c'"
          with c n
          have "⟨\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s⟩ -m->1 ⟨s'⟩"
            (is "⟨?if,_⟩ -m->1 _") by auto
          with n IH
          have "⟨\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s⟩ -->c s'" by blast
          moreover note unfold_while [of b c']
          -- {* @{thm unfold_while [of b c']} *}
          ultimately
          have "⟨\<WHILE> b \<DO> c',s⟩ -->c s'" by (blast dest: equivD2)
          with w show "⟨c,s⟩ -->c s'" by simp
        qed
      qed
      ultimately
      show "⟨c,s⟩ -->c s'" by blast
    qed

    subsection "Winskel's Proof"

    declare rel_pow_0_E [elim!]

    text {*
      Winskel's small step rules are a bit different \cite{Winskel};
      we introduce their equivalents as derived rules:
    *}
    lemma whileFalse1 [intro]:
      "¬ b s ==> ⟨\<WHILE> b \<DO> c,s⟩ -->1* ⟨s⟩" (is "_ ==> ⟨?w, s⟩ -->1* ⟨s⟩")
    proof -
      assume "¬b s"
      have "⟨?w, s⟩ -->1 ⟨\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s⟩" ..
      also have "⟨\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s⟩ -->1 ⟨\<SKIP>, s⟩" ..
      also have "⟨\<SKIP>, s⟩ -->1 ⟨s⟩" ..
      finally show "⟨?w, s⟩ -->1* ⟨s⟩" ..
    qed

    lemma whileTrue1 [intro]:
      "b s ==> ⟨\<WHILE> b \<DO> c,s⟩ -->1* ⟨c;\<WHILE> b \<DO> c, s⟩"
      (is "_ ==> ⟨?w, s⟩ -->1* ⟨c;?w,s⟩")
    proof -
      assume "b s"
      have "⟨?w, s⟩ -->1 ⟨\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s⟩" ..
      also have "⟨\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s⟩ -->1 ⟨c;?w, s⟩" ..
      finally show "⟨?w, s⟩ -->1* ⟨c;?w,s⟩" ..
    qed

    inductive_cases evalc1_SEs:
      "⟨\<SKIP>,s⟩ -->1 t"
      "⟨x:==a,s⟩ -->1 t"
      "⟨c1;c2, s⟩ -->1 t"
      "⟨\<IF> b \<THEN> c1 \<ELSE> c2, s⟩ -->1 t"
      "⟨\<WHILE> b \<DO> c, s⟩ -->1 t"

    inductive_cases evalc1_E: "⟨\<WHILE> b \<DO> c, s⟩ -->1 t"

    declare evalc1_SEs [elim!]

    lemma evalc_impl_evalc1: "⟨c,s⟩ -->c s1 ==> ⟨c,s⟩ -->1* ⟨s1⟩"
    apply (erule evalc.induct)

    -- SKIP
    apply blast

    -- ASSIGN
    apply fast

    -- SEMI
    apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)

    -- IF
    apply (fast intro: converse_rtrancl_into_rtrancl)
    apply (fast intro: converse_rtrancl_into_rtrancl)

    -- WHILE
    apply fast
    apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)

    done

    lemma lemma2 [rule_format (no_asm)]:
      "∀c d s u. ⟨c;d,s⟩ -n->1 ⟨u⟩ --> (∃t m. ⟨c,s⟩ -->1* ⟨t⟩ ∧ ⟨d,t⟩ -m->1 ⟨u⟩ ∧ m ≤ n)"
    apply (induct_tac "n")
     -- "case n = 0"
     apply fastsimp
    -- "induction step"
    apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
                elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
    done

    lemma evalc1_impl_evalc [rule_format (no_asm)]:
      "∀s t. ⟨c,s⟩ -->1* ⟨t⟩ --> ⟨c,s⟩ -->c t"
    apply (induct_tac "c")
    apply (safe dest!: rtrancl_imp_UN_rel_pow)

    -- SKIP
    apply (simp add: SKIP_n)

    -- ASSIGN
    apply (fastsimp elim: rel_pow_E2)

    -- SEMI
    apply (fast dest!: rel_pow_imp_rtrancl lemma2)

    -- IF
    apply (erule rel_pow_E2)
    apply simp
    apply (fast dest!: rel_pow_imp_rtrancl)

    -- "WHILE, induction on the length of the computation"
    apply (rename_tac b c s t n)
    apply (erule_tac P = "?X -n->1 ?Y" in rev_mp)
    apply (rule_tac x = "s" in spec)
    apply (induct_tac "n" rule: nat_less_induct)
    apply (intro strip)
    apply (erule rel_pow_E2)
     apply simp
    apply (erule evalc1_E)

    apply simp
    apply (case_tac "b x")
     -- WhileTrue
     apply (erule rel_pow_E2)
      apply simp
     apply (clarify dest!: lemma2)
     apply (erule allE, erule allE, erule impE, assumption)
     apply (erule_tac x=mb in allE, erule impE, fastsimp)
     apply blast
    -- WhileFalse
    apply (erule rel_pow_E2)
     apply simp
    apply (simp add: SKIP_n)
    done

    text {* proof of the equivalence of evalc and evalc1 *}
    lemma evalc1_eq_evalc: "(⟨c, s⟩ -->1* ⟨t⟩) = (⟨c,s⟩ -->c t)"
    apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
    done

    subsection "A proof without n"

    text {*
      The inductions are a bit awkward to write in this section,
      because @{text None} as result statement in the small step
      semantics doesn't have a direct counterpart in the big step
      semantics.

      Winskel's small step rule set (using the @{text "\<SKIP>"} statement
      to indicate termination) is better suited for this proof.
    *}

    lemma my_lemma1 [rule_format (no_asm)]:
      "⟨c1,s1⟩ -->1* ⟨s2⟩ ==> ⟨c2,s2⟩ -->1* cs3 ==> ⟨c1;c2,s1⟩ -->1* cs3"
    proof -
      -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
      have "⟨c1,s1⟩ -->1* ⟨s2⟩ ==> ⟨c2,s2⟩ -->1* cs3 -->
           ⟨(λc. if c = None then c2 else the c; c2) (Some c1),s1⟩ -->1* cs3"
        apply (erule converse_rtrancl_induct2)
         apply simp
        apply (rename_tac c s')
        apply simp
        apply (rule conjI)
         apply fast
        apply clarify
        apply (case_tac c)
        apply (auto intro: converse_rtrancl_into_rtrancl)
        done
      moreover assume "⟨c1,s1⟩ -->1* ⟨s2⟩" "⟨c2,s2⟩ -->1* cs3"
      ultimately show "⟨c1;c2,s1⟩ -->1* cs3" by simp
    qed

    lemma evalc_impl_evalc1': "⟨c,s⟩ -->c s1 ==> ⟨c,s⟩ -->1* ⟨s1⟩"
    apply (erule evalc.induct)

    -- SKIP
    apply fast

    -- ASSIGN
    apply fast

    -- SEMI
    apply (fast intro: my_lemma1)

    -- IF
    apply (fast intro: converse_rtrancl_into_rtrancl)
    apply (fast intro: converse_rtrancl_into_rtrancl)

    -- WHILE
    apply fast
    apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)

    done

    text {*
      The opposite direction is based on a Coq proof done by Ranan Fraer and
      Yves Bertot. The following sketch is from an email by Ranan Fraer.

    \begin{verbatim}
    First we've broke it into 2 lemmas:

    Lemma 1
    ((c,s) --> (SKIP,t)) => (<c,s> -c-> t)

    This is a quick one, dealing with the cases skip, assignment
    and while_false.

    Lemma 2
    ((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
      =>
    <c,s> -c-> t

    This is proved by rule induction on the  -*-> relation
    and the induction step makes use of a third lemma:

    Lemma 3
    ((c,s) --> (c',s')) /\ <c',s'> -c'-> t
      =>
    <c,s> -c-> t

    This captures the essence of the proof, as it shows that <c',s'>
    behaves as the continuation of <c,s> with respect to the natural
    semantics.
    The proof of Lemma 3 goes by rule induction on the --> relation,
    dealing with the cases sequence1, sequence2, if_true, if_false and
    while_true. In particular in the case (sequence1) we make use again
    of Lemma 1.
    \end{verbatim}
    *}

    inductive_cases evalc1_term_cases: "⟨c,s⟩ -->1 ⟨s'⟩"

    lemma FB_lemma3 [rule_format]:
      "(c,s) -->1 (c',s') ==> c ≠ None -->
      (∀t. ⟨if c'=None then \<SKIP> else the c',s'⟩ -->c t --> ⟨the c,s⟩ -->c t)"
      apply (erule evalc1.induct)
      apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
      done

    lemma FB_lemma2 [rule_format]:
      "(c,s) -->1* (c',s') ==> c ≠ None -->
       ⟨if c' = None then \<SKIP> else the c',s'⟩ -->c t --> ⟨the c,s⟩ -->c t"
      apply (erule converse_rtrancl_induct2)
       apply simp
      apply clarsimp
      apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
      done

    lemma evalc1_impl_evalc': "⟨c,s⟩ -->1* ⟨t⟩ ==> ⟨c,s⟩ -->c t"
      apply (fastsimp dest: FB_lemma2)
      done

    end

### The transition relation

lemmas

      ⟨SKIP,s⟩ -1-> ⟨s⟩

      ⟨x :== a ,s⟩ -1-> ⟨s[x ::= a s]⟩

      ⟨c0.0,s⟩ -1-> ⟨s'⟩ ==> ⟨c0.0; c1.0,s⟩ -1-> ⟨c1.0,s'⟩

      ⟨c0.0,s⟩ -1-> ⟨c0',s'⟩ ==> ⟨c0.0; c1.0,s⟩ -1-> ⟨c0'; c1.0,s'⟩

      b s ==> ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> ⟨c1.0,s⟩

      ¬ b s ==> ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> ⟨c2.0,s⟩

      ⟨WHILE b DO c,s⟩ -1-> ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩

lemmas

      ⟨SKIP,s⟩ -1-> ⟨s⟩

      ⟨x :== a ,s⟩ -1-> ⟨s[x ::= a s]⟩

      ⟨c0.0,s⟩ -1-> ⟨s'⟩ ==> ⟨c0.0; c1.0,s⟩ -1-> ⟨c1.0,s'⟩

      ⟨c0.0,s⟩ -1-> ⟨c0',s'⟩ ==> ⟨c0.0; c1.0,s⟩ -1-> ⟨c0'; c1.0,s'⟩

      b s ==> ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> ⟨c1.0,s⟩

      ¬ b s ==> ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> ⟨c2.0,s⟩

      ⟨WHILE b DO c,s⟩ -1-> ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩

lemma rel_pow_Suc_E2:

      [| (x, z) ∈ R ^ Suc n; !!y. [| (x, y) ∈ R; (y, z) ∈ R ^ n |] ==> P |] ==> P

lemma rtrancl_imp_rel_pow:

      p ∈ R* ==> ∃n. p ∈ R ^ n

lemma SKIP_1:

      ⟨SKIP,s⟩ -1-> y = (y = ⟨s⟩)

lemma Assign_1:

      ⟨x :== a ,s⟩ -1-> y = (y = ⟨s[x ::= a s]⟩)

lemma Cond_1:

      ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> y =
      ((b s --> y = ⟨c1.0,s⟩) ∧ (¬ b s --> y = ⟨c2.0,s⟩))

lemma While_1:

      ⟨WHILE b DO c,s⟩ -1-> y = (y = ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩)

lemmas

      ⟨SKIP,s⟩ -1-> y = (y = ⟨s⟩)

      ⟨x :== a ,s⟩ -1-> y = (y = ⟨s[x ::= a s]⟩)

      ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> y =
      ((b s --> y = ⟨c1.0,s⟩) ∧ (¬ b s --> y = ⟨c2.0,s⟩))

      ⟨WHILE b DO c,s⟩ -1-> y = (y = ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩)

lemmas

      ⟨SKIP,s⟩ -1-> y = (y = ⟨s⟩)

      ⟨x :== a ,s⟩ -1-> y = (y = ⟨s[x ::= a s]⟩)

      ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> y =
      ((b s --> y = ⟨c1.0,s⟩) ∧ (¬ b s --> y = ⟨c2.0,s⟩))

      ⟨WHILE b DO c,s⟩ -1-> y = (y = ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩)

### Examples

lemma

      s x = 0 ==> ⟨WHILE %s. s x ≠ 1 DO x :== %s. s x + 1 ,s⟩ -*-> ⟨s[x ::= 1]⟩

### Basic properties

lemma no_stuck:

      ∃y. ⟨c,s⟩ -1-> y

lemma stuck:

      ⟨s⟩ -1-> y ==> P

lemma evalc_None_retrancl:

      ⟨s⟩ -*-> s' ==> s' = ⟨s⟩

lemma rel_pow_0:

      R ^ 0 = Id

lemma rel_pow_Suc_0:

      R ^ Suc 0 = R

lemmas

      R ^ 0 = Id

      R ^ Suc n = R O R ^ n

lemmas

      R ^ 0 = Id

      R ^ Suc n = R O R ^ n

lemma evalc1_None_0:

      ⟨s⟩ -n-> y = (n = 0 ∧ y = ⟨s⟩)

lemma SKIP_n:

      ⟨SKIP,s⟩ -n-> ⟨s'⟩ ==> s' = s ∧ n = 1

### Equivalence to natural semantics (after Nielson and Nielson)

lemma semiD:

      ⟨c1.0; c2.0,s⟩ -n-> ⟨s''⟩
      ==> ∃i j s'. ⟨c1.0,s⟩ -i-> ⟨s'⟩ ∧ ⟨c2.0,s'⟩ -j-> ⟨s''⟩ ∧ n = i + j

lemma semiI:

      [| ⟨c0.0,s⟩ -n-> ⟨s''⟩; ⟨c1.0,s''⟩ -*-> ⟨s'⟩ |] ==> ⟨c0.0; c1.0,s⟩ -*-> ⟨s'⟩

lemma evalc_imp_evalc1:

      ⟨c,s⟩ -->c s' ==> ⟨c,s⟩ -*-> ⟨s'⟩

theorem evalc_equiv_evalc1:

      ⟨c,s⟩ -->c s' = ⟨c,s⟩ -*-> ⟨s'⟩

### Winskel's Proof

lemma whileFalse1:

      ¬ b s ==> ⟨WHILE b DO c,s⟩ -*-> ⟨s⟩

lemma whileTrue1:

      b s ==> ⟨WHILE b DO c,s⟩ -*-> ⟨c; WHILE b DO c,s⟩

lemmas evalc1_SEs:

      [| ⟨SKIP,s⟩ -1-> t; t = ⟨s⟩ ==> P |] ==> P

      [| ⟨x :== a ,s⟩ -1-> t; t = ⟨s[x ::= a s]⟩ ==> P |] ==> P

      [| ⟨c1.0; c2.0,s⟩ -1-> t; !!s'. [| ⟨c1.0,s⟩ -1-> ⟨s'⟩; t = ⟨c2.0,s'⟩ |] ==> P;
         !!c0' s'. [| ⟨c1.0,s⟩ -1-> ⟨c0',s'⟩; t = ⟨c0'; c2.0,s'⟩ |] ==> P |]
      ==> P

      [| ⟨IF b THEN c1.0 ELSE c2.0,s⟩ -1-> t; [| b s; t = ⟨c1.0,s⟩ |] ==> P;
         [| ¬ b s; t = ⟨c2.0,s⟩ |] ==> P |]
      ==> P

      [| ⟨WHILE b DO c,s⟩ -1-> t; t = ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩ ==> P |]
      ==> P

lemmas evalc1_E:

      [| ⟨WHILE b DO c,s⟩ -1-> t; t = ⟨IF b THEN c; WHILE b DO c ELSE SKIP,s⟩ ==> P |]
      ==> P

lemma evalc_impl_evalc1:

      ⟨c,s⟩ -->c s1.0 ==> ⟨c,s⟩ -*-> ⟨s1.0⟩

lemma lemma2:

      ⟨c; d,s⟩ -n-> ⟨u⟩ ==> ∃t m. ⟨c,s⟩ -*-> ⟨t⟩ ∧ ⟨d,t⟩ -m-> ⟨u⟩ ∧ m ≤ n

lemma evalc1_impl_evalc:

      ⟨c,s⟩ -*-> ⟨t⟩ ==> ⟨c,s⟩ -->c t

lemma evalc1_eq_evalc:

      ⟨c,s⟩ -*-> ⟨t⟩ = ⟨c,s⟩ -->c t

### A proof without n

lemma my_lemma1:

      [| ⟨c1.0,s1.0⟩ -*-> ⟨s2.0⟩; ⟨c2.0,s2.0⟩ -*-> cs3.0 |]
      ==> ⟨c1.0; c2.0,s1.0⟩ -*-> cs3.0

lemma evalc_impl_evalc1':

      ⟨c,s⟩ -->c s1.0 ==> ⟨c,s⟩ -*-> ⟨s1.0⟩

lemmas evalc1_term_cases:

      [| ⟨c,s⟩ -1-> ⟨s'⟩; [| c = SKIP; s' = s |] ==> P;
         !!a x. [| c = x :== a ; s' = s[x ::= a s] |] ==> P |]
      ==> P

lemma FB_lemma3:

      [| (c, s) -1-> (c', s'); c ≠ None;
         ⟨if c' = None then SKIP else the c',s'⟩ -->c t |]
      ==> ⟨the c,s⟩ -->c t

lemma FB_lemma2:

      [| (c, s) -*-> (c', s'); c ≠ None;
         ⟨if c' = None then SKIP else the c',s'⟩ -->c t |]
      ==> ⟨the c,s⟩ -->c t

lemma evalc1_impl_evalc':

      ⟨c,s⟩ -*-> ⟨t⟩ ==> ⟨c,s⟩ -->c t