Determinism of Evaluation

Deterministic.thy

lemma ceval_deterministic_lemma: "c %: st ⇓ st' ⟹ (⋀u. c %: st ⇓ u ⟹ st' = u)"
using ceval.induct [of c st st' "λc0 st0 st'0. ((c0 %: st0 ⇓ st'0) ⟶ (∀u. (c0 %: st0 ⇓ u) ⟶ (st'0 = u)))"]
apply rule
apply simp
proof-
  fix u sta
  assume "c %: st ⇓ st'" "c %: st ⇓ u"
  show "(SKIP %: sta ⇓ sta) ⟶ (∀u. (SKIP %: sta ⇓ u) ⟶ sta = u)"
    by (auto, erule ceval.cases, auto, erule ceval.cases, auto)
next
  fix u sta a1 n x
  assume a: "c %: st ⇓ st'" "c %: st ⇓ u" "aeval3 sta a1 = n"
  show "(x ::= a1 %: sta ⇓ update sta x n) ⟶ (∀u. (x ::= a1 %: sta ⇓ u) ⟶ update sta x n = u)"
    apply (auto, erule ceval.cases, auto)
    apply (erule ceval.cases, auto simp add: a)
    done
next
  fix u c1 sta st'a c2 st''
  assume a1: "c %: st ⇓ st'" "c %: st ⇓ u"
  and a2: "c1 %: sta ⇓ st'a" "(c1 %: sta ⇓ st'a) ⟶ (∀u. (c1 %: sta ⇓ u) ⟶ st'a = u)"
  and a3: "c2 %: st'a ⇓ st''" "(c2 %: st'a ⇓ st'') ⟶ (∀u. (c2 %: st'a ⇓ u) ⟶ st'' = u)"
  show "((c1 ;; c2) %: sta ⇓ st'') ⟶ (∀u. ((c1 ;; c2) %: sta ⇓ u) ⟶ st'' = u)"
    proof auto
      fix u
      assume "(c1 ;; c2) %: sta ⇓ st''" "(c1 ;; c2) %: sta ⇓ u"
      from this(2) obtain u0 where
        u0: "c1 %: sta ⇓ u0" "c2 %: u0 ⇓ u" by (rule, auto)
      have 1: "st'a = u0" using u0(1) a2 by simp
      show "st'' = u" using a3(2) u0(2) by (simp add: a3(1), simp add: 1)
    qed
next
  fix u sta b c1 st'a c2
  assume a: "c %: st ⇓ st'" "c %: st ⇓ u" "beval3 sta b = True" "c1 %: sta ⇓ st'a" "(c1 %: sta ⇓ st'a) ⟶ (∀u. (c1 %: sta ⇓ u) ⟶ st'a = u)"
  show "(IF b THEN c1 ELSE c2 FI %: sta ⇓ st'a) ⟶ (∀u. (IF b THEN c1 ELSE c2 FI %: sta ⇓ u) ⟶ st'a = u)"
    proof auto
      fix u
      assume "IF b THEN c1 ELSE c2 FI %: sta ⇓ st'a" "IF b THEN c1 ELSE c2 FI %: sta ⇓ u"
      from this(2) have "c1 %: sta ⇓ u" by (rule, auto, auto simp add: a(3))
      thus "st'a = u" using a(5) a(4) by simp
    qed
next
  fix u sta b c2 st'a c1
  assume a: "c %: st ⇓ st'" "c %: st ⇓ u" "beval3 sta b = False" "c2 %: sta ⇓ st'a" "(c2 %: sta ⇓ st'a) ⟶ (∀u. (c2 %: sta ⇓ u) ⟶ st'a = u)"
  show "(IF b THEN c1 ELSE c2 FI %: sta ⇓ st'a) ⟶ (∀u. (IF b THEN c1 ELSE c2 FI %: sta ⇓ u) ⟶ st'a = u)"
    proof auto
      fix u
      assume "IF b THEN c1 ELSE c2 FI %: sta ⇓ st'a" "IF b THEN c1 ELSE c2 FI %: sta ⇓ u"
      from this(2) have "c2 %: sta ⇓ u" by (rule, auto, auto simp add: a(3))
      thus "st'a = u" using a(5) a(4) by simp
    qed
next
  fix u sta b ca
  assume a: "c %: st ⇓ st'" "c %: st ⇓ u" "beval3 sta b = False"
  show "(WHILE b DO ca END %: sta ⇓ sta) ⟶ (∀u. (WHILE b DO ca END %: sta ⇓ u) ⟶ sta = u)"
    proof auto
      fix u
      assume "WHILE b DO ca END %: sta ⇓ sta" "WHILE b DO ca END %: sta ⇓ u"
      from this(2) show "sta = u"
        by (rule, auto, auto simp add: a(3))
    qed
next
  fix u sta b ca st'a st''
  assume "c %: st ⇓ st'" "c %: st ⇓ u"
  and a: "beval3 sta b = True" "ca %: sta ⇓ st'a" "ca %: sta ⇓ st'a ⟶ (∀u. ca %: sta ⇓ u ⟶ st'a = u)"
  and a2: "WHILE b DO ca END %: st'a ⇓ st''" "(WHILE b DO ca END %: st'a ⇓ st'') ⟶ (∀u. (WHILE b DO ca END %: st'a ⇓ u) ⟶ st'' = u)"

  have b1: "⋀u. ca %: sta ⇓ u ⟹ st'a = u" using a by simp
  have b2: "⋀u. (WHILE b DO ca END) %: st'a ⇓ u ⟹ st'' = u" using a2 by simp
  show "(WHILE b DO ca END %: sta ⇓ st'') ⟶ (∀u. (WHILE b DO ca END %: sta ⇓ u) ⟶ st'' = u)"
    proof auto
      fix u
      assume a4: "WHILE b DO ca END %: sta ⇓ st''" "WHILE b DO ca END %: sta ⇓ u"
      from this(2) obtain u' where
        u': "ca %: sta ⇓ u'" "(WHILE b DO ca END) %: u' ⇓ u" by (rule, auto, auto simp add: a(1))
      have "st'a = u'" using b1 [OF u'(1)] by simp
      thus "st'' = u" using b2 u'(2) by auto
    qed
qed (auto)

theorem ceval_deterministic: "⟦ c %: st ⇓ st1; c %: st ⇓ st2 ⟧ ⟹ st1 = st2"
by (auto simp add: ceval_deterministic_lemma)


(* ---------------------------- *)

lemma while_induction:
  assumes red: "(WHILE b DO c END) %: st ⇓ st'"
  and base: "⋀t t'. ⟦ beval3 t b = False; t' = t ⟧ ⟹ P t t'"
  and step: "⋀t t' t''. ⟦ beval3 t b = True; c %: t ⇓ t'; (WHILE b DO c END) %: t' ⇓ t''; P t' t'' ⟧ ⟹ P t t''"
  shows "P st st'"
proof-
  have "(WHILE b DO c END) %: st ⇓ st' ⟹ P st st'"
    using ceval.induct [of _ _ _ "λc0 t t'. WHILE b DO c END = c0 ⟶ P t t'"] apply rule
    apply (simp, auto, simp add: base)
    apply (fastforce simp add: step)
    apply (fastforce simp add: step)
    done
  thus ?thesis by (simp add: red)
qed

theorem loop_never_stops: "¬ (loop %: st ⇓ st')"
proof (unfold loop_def, auto)
  assume p: "WHILE BTrue DO SKIP END %: st ⇓ st'"
  show "False"
    using while_induction [of BTrue SKIP st st' "λ_. λ_. False"]
    by (rule, simp add: p, auto)
qed