# Theory Natural

Up to index of Isabelle/HOLCF/IMP

theory Natural
imports Com
begin

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

    header "Natural Semantics of Commands"

    theory Natural imports Com begin

    subsection "Execution of commands"

    consts  evalc   :: "(com × state × state) set"
    syntax "_evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,60] 60)

    syntax (xsymbols)
      "_evalc" :: "[com,state,state] => bool" ("⟨_,_⟩/ -->c _" [0,0,60] 60)

    syntax (HTML output)
      "_evalc" :: "[com,state,state] => bool" ("⟨_,_⟩/ -->c _" [0,0,60] 60)

    text {*
      We write @{text "⟨c,s⟩ -->c s'"} for \emph{Statement @{text c}, started
      in state @{text s}, terminates in state @{text s'}}. Formally,
      @{text "⟨c,s⟩ -->c s'"} is just another form of saying \emph{the tuple
      @{text "(c,s,s')"} is part of the relation @{text evalc}}:
    *}
    translations  "⟨c,s⟩ -->c s'" == "(c,s,s') ∈ evalc"

    constdefs
      update :: "('a => 'b) => 'a => 'b => ('a => 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
      "update == fun_upd"

    syntax (xsymbols)
      update :: "('a => 'b) => 'a => 'b => ('a => 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)

    text {*
      The big-step execution relation @{text evalc} is defined inductively:
    *}
    inductive evalc
      intros
      Skip:    "⟨\<SKIP>,s⟩ -->c s"
      Assign:  "⟨x :== a,s⟩ -->c s[x\<mapsto>a s]"

      Semi:    "⟨c0,s⟩ -->c s'' ==> ⟨c1,s''⟩ -->c s' ==> ⟨c0; c1, s⟩ -->c s'"

      IfTrue:  "b s ==> ⟨c0,s⟩ -->c s' ==> ⟨\<IF> b \<THEN> c0 \<ELSE> c1, s⟩ -->c s'"
      IfFalse: "¬b s ==> ⟨c1,s⟩ -->c s' ==> ⟨\<IF> b \<THEN> c0 \<ELSE> c1, s⟩ -->c s'"

      WhileFalse: "¬b s ==> ⟨\<WHILE> b \<DO> c,s⟩ -->c s"
      WhileTrue:  "b s ==> ⟨c,s⟩ -->c s'' ==> ⟨\<WHILE> b \<DO> c, s''⟩ -->c s'
                   ==> ⟨\<WHILE> b \<DO> c, s⟩ -->c s'"

    lemmas evalc.intros [intro] -- "use those rules in automatic proofs"

    text {*
    The induction principle induced by this definition looks like this:

    @{thm [display] evalc.induct [no_vars]}

    (@{text "!!"} and @{text "==>"} are Isabelle's
      meta symbols for @{text "∀"} and @{text "-->"})
    *}

    text {*
      The rules of @{text evalc} are syntax directed, i.e.~for each
      syntactic category there is always only one rule applicable. That
      means we can use the rules in both directions. The proofs for this
      are all the same: one direction is trivial, the other one is shown
      by using the @{text evalc} rules backwards:
    *}
    lemma skip:
      "⟨\<SKIP>,s⟩ -->c s' = (s' = s)"
      by (rule, erule evalc.elims) auto

    lemma assign:
      "⟨x :== a,s⟩ -->c s' = (s' = s[x\<mapsto>a s])"
      by (rule, erule evalc.elims) auto

    lemma semi:
      "⟨c0; c1, s⟩ -->c s' = (∃s''. ⟨c0,s⟩ -->c s'' ∧ ⟨c1,s''⟩ -->c s')"
      by (rule, erule evalc.elims) auto

    lemma ifTrue:
      "b s ==> ⟨\<IF> b \<THEN> c0 \<ELSE> c1, s⟩ -->c s' = ⟨c0,s⟩ -->c s'"
      by (rule, erule evalc.elims) auto

    lemma ifFalse:
      "¬b s ==> ⟨\<IF> b \<THEN> c0 \<ELSE> c1, s⟩ -->c s' = ⟨c1,s⟩ -->c s'"
      by (rule, erule evalc.elims) auto

    lemma whileFalse:
      "¬ b s ==> ⟨\<WHILE> b \<DO> c,s⟩ -->c s' = (s' = s)"
      by (rule, erule evalc.elims) auto

    lemma whileTrue:
      "b s ==>
      ⟨\<WHILE> b \<DO> c, s⟩ -->c s' =
      (∃s''. ⟨c,s⟩ -->c s'' ∧ ⟨\<WHILE> b \<DO> c, s''⟩ -->c s')"
      by (rule, erule evalc.elims) auto

    text "Again, Isabelle may use these rules in automatic proofs:"
    lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue

    subsection "Equivalence of statements"

    text {*
      We call two statements @{text c} and @{text c'} equivalent wrt.~the
      big-step semantics when \emph{@{text c} started in @{text s} terminates
      in @{text s'} iff @{text c'} started in the same @{text s} also terminates
      in the same @{text s'}}. Formally:
    *}
    constdefs
      equiv_c :: "com => com => bool" ("_ ∼ _")
      "c ∼ c' ≡ ∀s s'. ⟨c, s⟩ -->c s' = ⟨c', s⟩ -->c s'"

    text {*
      Proof rules telling Isabelle to unfold the definition
      if there is something to be proved about equivalent
      statements: *}
    lemma equivI [intro!]:
      "(!!s s'. ⟨c, s⟩ -->c s' = ⟨c', s⟩ -->c s') ==> c ∼ c'"
      by (unfold equiv_c_def) blast

    lemma equivD1:
      "c ∼ c' ==> ⟨c, s⟩ -->c s' ==> ⟨c', s⟩ -->c s'"
      by (unfold equiv_c_def) blast

    lemma equivD2:
      "c ∼ c' ==> ⟨c', s⟩ -->c s' ==> ⟨c, s⟩ -->c s'"
      by (unfold equiv_c_def) blast

    text {*
      As an example, we show that loop unfolding is an equivalence
      transformation on programs:
    *}
    lemma unfold_while:
      "(\<WHILE> b \<DO> c) ∼ (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w ∼ ?if")
    proof -
      -- "to show the equivalence, we look at the derivation tree for"
      -- "each side and from that construct a derivation tree for the other side"
      { fix s s' assume w: "⟨?w, s⟩ -->c s'"
        -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
        -- "then both statements do nothing:"
        hence "¬b s ==> s = s'" by simp
        hence "¬b s ==> ⟨?if, s⟩ -->c s'" by simp
        moreover
        -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
        -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "⟨?w, s⟩ -->c s'"} *}
        { assume b: "b s"
          with w obtain s'' where
            "⟨c, s⟩ -->c s''" and "⟨?w, s''⟩ -->c s'" by (cases set: evalc) auto
          -- "now we can build a derivation tree for the @{text \<IF>}"
          -- "first, the body of the True-branch:"
          hence "⟨c; ?w, s⟩ -->c s'" by (rule Semi)
          -- "then the whole @{text \<IF>}"
          with b have "⟨?if, s⟩ -->c s'" by (rule IfTrue)
        }
        ultimately
        -- "both cases together give us what we want:"
        have "⟨?if, s⟩ -->c s'" by blast
      }
      moreover
      -- "now the other direction:"
      { fix s s' assume if: "⟨?if, s⟩ -->c s'"
        -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
        -- "of the @{text \<IF>} is executed, and both statements do nothing:"
        hence "¬b s ==> s = s'" by simp
        hence "¬b s ==> ⟨?w, s⟩ -->c s'" by simp
        moreover
        -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
        -- {* then this time only the @{text IfTrue} rule can have be used *}
        { assume b: "b s"
          with if have "⟨c; ?w, s⟩ -->c s'" by (cases set: evalc) auto
          -- "and for this, only the Semi-rule is applicable:"
          then obtain s'' where
            "⟨c, s⟩ -->c s''" and "⟨?w, s''⟩ -->c s'" by (cases set: evalc) auto
          -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
          with b
          have "⟨?w, s⟩ -->c s'" by (rule WhileTrue)
        }
        ultimately
        -- "both cases together again give us what we want:"
        have "⟨?w, s⟩ -->c s'" by blast
      }
      ultimately
      show ?thesis by blast
    qed

    subsection "Execution is deterministic"

    text {*
    The following proof presents all the details:
    *}
    theorem com_det: "⟨c,s⟩ -->c t ∧ ⟨c,s⟩ -->c u --> u=t"
    proof clarify -- "transform the goal into canonical form"
      assume "⟨c,s⟩ -->c t"
      thus "!!u. ⟨c,s⟩ -->c u ==> u=t"
      proof (induct set: evalc)
        fix s u assume "⟨\<SKIP>,s⟩ -->c u"
        thus "u = s" by simp
      next
        fix a s x u assume "⟨x :== a,s⟩ -->c u"
        thus "u = s[x \<mapsto> a s]" by simp
      next
        fix c0 c1 s s1 s2 u
        assume IH0: "!!u. ⟨c0,s⟩ -->c u ==> u = s2"
        assume IH1: "!!u. ⟨c1,s2⟩ -->c u ==> u = s1"

        assume "⟨c0;c1, s⟩ -->c u"
        then obtain s' where
          c0: "⟨c0,s⟩ -->c s'" and
          c1: "⟨c1,s'⟩ -->c u"
          by auto

        from c0 IH0 have "s'=s2" by blast
        with c1 IH1 show "u=s1" by blast
      next
        fix b c0 c1 s s1 u
        assume IH: "!!u. ⟨c0,s⟩ -->c u ==> u = s1"

        assume "b s" and "⟨\<IF> b \<THEN> c0 \<ELSE> c1,s⟩ -->c u"
        hence "⟨c0, s⟩ -->c u" by simp
        with IH show "u = s1" by blast
      next
        fix b c0 c1 s s1 u
        assume IH: "!!u. ⟨c1,s⟩ -->c u ==> u = s1"

        assume "¬b s" and "⟨\<IF> b \<THEN> c0 \<ELSE> c1,s⟩ -->c u"
        hence "⟨c1, s⟩ -->c u" by simp
        with IH show "u = s1" by blast
      next
        fix b c s u
        assume "¬b s" and "⟨\<WHILE> b \<DO> c,s⟩ -->c u"
        thus "u = s" by simp
      next
        fix b c s s1 s2 u
        assume "IHc": "!!u. ⟨c,s⟩ -->c u ==> u = s2"
        assume "IHw": "!!u. ⟨\<WHILE> b \<DO> c,s2⟩ -->c u ==> u = s1"

        assume "b s" and "⟨\<WHILE> b \<DO> c,s⟩ -->c u"
        then obtain s' where
          c: "⟨c,s⟩ -->c s'" and
          w: "⟨\<WHILE> b \<DO> c,s'⟩ -->c u"
          by auto

        from c "IHc" have "s' = s2" by blast
        with w "IHw" show "u = s1" by blast
      qed
    qed

    text {*
      This is the proof as you might present it in a lecture. The remaining
      cases are simple enough to be proved automatically:
    *}
    theorem "⟨c,s⟩ -->c t ∧ ⟨c,s⟩ -->c u --> u=t"
    proof clarify
      assume "⟨c,s⟩ -->c t"
      thus "!!u. ⟨c,s⟩ -->c u ==> u=t"
      proof (induct set: evalc)
        -- "the simple @{text \<SKIP>} case for demonstration:"
        fix s u assume "⟨\<SKIP>,s⟩ -->c u"
        thus "u = s" by simp
      next
        -- "and the only really interesting case, @{text \<WHILE>}:"
        fix b c s s1 s2 u
        assume "IHc": "!!u. ⟨c,s⟩ -->c u ==> u = s2"
        assume "IHw": "!!u. ⟨\<WHILE> b \<DO> c,s2⟩ -->c u ==> u = s1"

        assume "b s" and "⟨\<WHILE> b \<DO> c,s⟩ -->c u"
        then obtain s' where
          c: "⟨c,s⟩ -->c s'" and
          w: "⟨\<WHILE> b \<DO> c,s'⟩ -->c u"
          by auto

        from c "IHc" have "s' = s2" by blast
        with w "IHw" show "u = s1" by blast
      qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
    qed

    end

### Execution of commands

lemmas

      ⟨SKIP,s⟩ -->c s

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

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

      [| b s; ⟨c0.0,s⟩ -->c s' |] ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s'

      [| ¬ b s; ⟨c1.0,s⟩ -->c s' |] ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s'

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

      [| b s; ⟨c,s⟩ -->c s''; ⟨WHILE b DO c,s''⟩ -->c s' |]
      ==> ⟨WHILE b DO c,s⟩ -->c s'

lemmas

      ⟨SKIP,s⟩ -->c s

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

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

      [| b s; ⟨c0.0,s⟩ -->c s' |] ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s'

      [| ¬ b s; ⟨c1.0,s⟩ -->c s' |] ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s'

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

      [| b s; ⟨c,s⟩ -->c s''; ⟨WHILE b DO c,s''⟩ -->c s' |]
      ==> ⟨WHILE b DO c,s⟩ -->c s'

lemma skip:

      ⟨SKIP,s⟩ -->c s' = (s' = s)

lemma assign:

      ⟨x :== a ,s⟩ -->c s' = (s' = s[x ::= a s])

lemma semi:

      ⟨c0.0; c1.0,s⟩ -->c s' = (∃s''. ⟨c0.0,s⟩ -->c s'' ∧ ⟨c1.0,s''⟩ -->c s')

lemma ifTrue:

      b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c0.0,s⟩ -->c s'

lemma ifFalse:

      ¬ b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c1.0,s⟩ -->c s'

lemma whileFalse:

      ¬ b s ==> ⟨WHILE b DO c,s⟩ -->c s' = (s' = s)

lemma whileTrue:

      b s ==> ⟨WHILE b DO c,s⟩ -->c s' =
              (∃s''. ⟨c,s⟩ -->c s'' ∧ ⟨WHILE b DO c,s''⟩ -->c s')

lemmas evalc_cases:

      ⟨SKIP,s⟩ -->c s' = (s' = s)

      ⟨x :== a ,s⟩ -->c s' = (s' = s[x ::= a s])

      b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c0.0,s⟩ -->c s'

      ¬ b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c1.0,s⟩ -->c s'

      ¬ b s ==> ⟨WHILE b DO c,s⟩ -->c s' = (s' = s)

      ⟨c0.0; c1.0,s⟩ -->c s' = (∃s''. ⟨c0.0,s⟩ -->c s'' ∧ ⟨c1.0,s''⟩ -->c s')

      b s ==> ⟨WHILE b DO c,s⟩ -->c s' =
              (∃s''. ⟨c,s⟩ -->c s'' ∧ ⟨WHILE b DO c,s''⟩ -->c s')

lemmas evalc_cases:

      ⟨SKIP,s⟩ -->c s' = (s' = s)

      ⟨x :== a ,s⟩ -->c s' = (s' = s[x ::= a s])

      b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c0.0,s⟩ -->c s'

      ¬ b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c1.0,s⟩ -->c s'

      ¬ b s ==> ⟨WHILE b DO c,s⟩ -->c s' = (s' = s)

      ⟨c0.0; c1.0,s⟩ -->c s' = (∃s''. ⟨c0.0,s⟩ -->c s'' ∧ ⟨c1.0,s''⟩ -->c s')

      b s ==> ⟨WHILE b DO c,s⟩ -->c s' =
              (∃s''. ⟨c,s⟩ -->c s'' ∧ ⟨WHILE b DO c,s''⟩ -->c s')

### Equivalence of statements

lemma equivI:

      (!!s s'. ⟨c,s⟩ -->c s' = ⟨c',s⟩ -->c s') ==> c ∼ c'

lemma equivD1:

      [| c ∼ c'; ⟨c,s⟩ -->c s' |] ==> ⟨c',s⟩ -->c s'

lemma equivD2:

      [| c ∼ c'; ⟨c',s⟩ -->c s' |] ==> ⟨c,s⟩ -->c s'

lemma unfold_while:

      WHILE b DO c ∼ IF b THEN c; WHILE b DO c ELSE SKIP

### Execution is deterministic

theorem com_det:

      ⟨c,s⟩ -->c t ∧ ⟨c,s⟩ -->c u --> u = t

theorem

      ⟨c,s⟩ -->c t ∧ ⟨c,s⟩ -->c u --> u = t