Theory Def_Init_Small

(* Author: Tobias Nipkow *)

theory Def_Init_Small
imports Star Def_Init_Exp Def_Init
begin

subsection "Initialization-Sensitive Small Step Semantics"

inductive
  small_step :: "(com × state) ⇒ (com × state) ⇒ bool" (infix "→" 55)
where
Assign:  "aval a s = Some i ⟹ (x ::= a, s) → (SKIP, s(x := Some i))" |

Seq1:   "(SKIP;;c,s) → (c,s)" |
Seq2:   "(c⇩1,s) → (c⇩1',s') ⟹ (c⇩1;;c⇩2,s) → (c⇩1';;c⇩2,s')" |

IfTrue:  "bval b s = Some True ⟹ (IF b THEN c⇩1 ELSE c⇩2,s) → (c⇩1,s)" |
IfFalse: "bval b s = Some False ⟹ (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)"

lemmas small_step_induct = small_step.induct[split_format(complete)]

abbreviation small_steps :: "com * state ⇒ com * state ⇒ bool" (infix "→*" 55)
where "x →* y == star small_step x y"


subsection "Soundness wrt Small Steps"

theorem progress:
  "D (dom s) c A' ⟹ c ≠ SKIP ⟹ ∃cs'. (c,s) → cs'"
proof (induction c arbitrary: s A')
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
next
  case (If b c1 c2)
  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
  then show ?case
    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
qed (fastforce intro: small_step.intros)+

lemma D_mono:  "D A c M ⟹ A ⊆ A' ⟹ ∃M'. D A' c M' & M <= M'"
proof (induction c arbitrary: A A' M)
  case Seq thus ?case by auto (metis D.intros(3))
next
  case (If b c1 c2)
  then obtain M1 M2 where "vars b ⊆ A" "D A c1 M1" "D A c2 M2" "M = M1 ∩ M2"
    by auto
  with If.IH ‹A ⊆ A'› obtain M1' M2'
    where "D A' c1 M1'" "D A' c2 M2'" and "M1 ⊆ M1'" "M2 ⊆ M2'" by metis
  hence "D A' (IF b THEN c1 ELSE c2) (M1' ∩ M2')" and "M ⊆ M1' ∩ M2'"
    using ‹vars b ⊆ A› ‹A ⊆ A'› ‹M = M1 ∩ M2› by(fastforce intro: D.intros)+
  thus ?case by metis
next
  case While thus ?case by auto (metis D.intros(5) subset_trans)
qed (auto intro: D.intros)

theorem D_preservation:
  "(c,s) → (c',s') ⟹ D (dom s) c A ⟹ ∃A'. D (dom s') c' A' & A <= A'"
proof (induction arbitrary: A rule: small_step_induct)
  case (While b c s)
  then obtain A' where A': "vars b ⊆ dom s" "A = dom s" "D (dom s) c A'" by blast
  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
  with A' have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
    by (metis D.If[OF ‹vars b ⊆ dom s› D.Seq[OF ‹D (dom s) c A'› D.While[OF _ ‹D A' c A''›]] D.Skip] D_incr Int_absorb1 subset_trans)
  thus ?case by (metis D_incr ‹A = dom s›)
next
  case Seq2 thus ?case by auto (metis D_mono D.intros(3))
qed (auto intro: D.intros)

theorem D_sound:
  "(c,s) →* (c',s') ⟹ D (dom s) c A'
   ⟹ (∃cs''. (c',s') → cs'') ∨ c' = SKIP"
apply(induction arbitrary: A' rule:star_induct)
apply (metis progress)
by (metis D_preservation)

end