Theory Semantics

section ‹Semantics›

theory Semantics imports Labels Com begin

subsection ‹Small Step Semantics›


inductive red :: "cmd * state ⇒ cmd * state ⇒ bool"
and red' :: "cmd ⇒ state ⇒ cmd ⇒ state ⇒ bool"
  (‹((1⟨_,/_⟩) →/ (1⟨_,/_⟩))› [0,0,0,0] 81)
where
   "⟨c,s⟩ → ⟨c',s'⟩ == red (c,s) (c',s')"
  | RedLAss:
   "⟨V:=e,s⟩ → ⟨Skip,s(V:=(interpret e s))⟩"

  | SeqRed:
  "⟨c1,s⟩ → ⟨c1',s'⟩ ⟹ ⟨c1;;c2,s⟩ → ⟨c1';;c2,s'⟩"

  | RedSeq:
  "⟨Skip;;c2,s⟩ → ⟨c2,s⟩"

  | RedCondTrue:
  "interpret b s = Some true ⟹ ⟨if (b) c1 else c2,s⟩ → ⟨c1,s⟩"

  | RedCondFalse:
  "interpret b s = Some false ⟹ ⟨if (b) c1 else c2,s⟩ → ⟨c2,s⟩"

  | RedWhileTrue:
  "interpret b s = Some true ⟹ ⟨while (b) c,s⟩ → ⟨c;;while (b) c,s⟩"

  | RedWhileFalse:
  "interpret b s = Some false ⟹ ⟨while (b) c,s⟩ → ⟨Skip,s⟩"

lemmas red_induct = red.induct[split_format (complete)]

abbreviation reds ::"cmd ⇒ state ⇒ cmd ⇒ state ⇒ bool" 
   (‹((1⟨_,/_⟩) →*/ (1⟨_,/_⟩))› [0,0,0,0] 81) where
  "⟨c,s⟩ →* ⟨c',s'⟩ == red** (c,s) (c',s')"


subsection‹Label Semantics›

inductive step :: "cmd ⇒ cmd ⇒ state ⇒ nat ⇒ cmd ⇒ state ⇒ nat ⇒ bool"
   (‹(_ ⊢ (1⟨_,/_,/_⟩) ↝/ (1⟨_,/_,/_⟩))› [51,0,0,0,0,0,0] 81)
where

StepLAss:
  "V:=e ⊢ ⟨V:=e,s,0⟩ ↝ ⟨Skip,s(V:=(interpret e s)),1⟩"

| StepSeq:
  "⟦labels (c1;;c2) l (Skip;;c2); labels (c1;;c2) #:c1 c2; l < #:c1⟧ 
  ⟹ c1;;c2 ⊢ ⟨Skip;;c2,s,l⟩ ↝ ⟨c2,s,#:c1⟩"

| StepSeqWhile:
  "labels (while (b) c') l (Skip;;while (b) c')
  ⟹ while (b) c' ⊢ ⟨Skip;;while (b) c',s,l⟩ ↝ ⟨while (b) c',s,0⟩"

| StepCondTrue:
  "interpret b s = Some true 
     ⟹ if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c1,s,1⟩"

| StepCondFalse:
  "interpret b s = Some false 
  ⟹ if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c2,s,#:c1 + 1⟩"

| StepWhileTrue:
  "interpret b s = Some true 
     ⟹ while (b) c ⊢ ⟨while (b) c,s,0⟩ ↝ ⟨c;;while (b) c,s,2⟩"

| StepWhileFalse:
  "interpret b s = Some false ⟹ while (b) c ⊢ ⟨while (b) c,s,0⟩ ↝ ⟨Skip,s,1⟩"

| StepRecSeq1:
  "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩
  ⟹ prog;;c2 ⊢ ⟨c;;c2,s,l⟩ ↝ ⟨c';;c2,s',l'⟩"

| StepRecSeq2:
  "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ 
  ⟹ c1;;prog ⊢ ⟨c,s,l + #:c1⟩ ↝ ⟨c',s',l' + #:c1⟩"

| StepRecCond1:
  "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ 
  ⟹ if (b) prog else c2 ⊢ ⟨c,s,l + 1⟩ ↝ ⟨c',s',l' + 1⟩"

| StepRecCond2:
  "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ 
  ⟹ if (b) c1 else prog ⊢ ⟨c,s,l + #:c1 + 1⟩ ↝ ⟨c',s',l' + #:c1 + 1⟩"

| StepRecWhile:
  "cx ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩
  ⟹ while (b) cx ⊢ ⟨c;;while (b) cx,s,l + 2⟩ ↝ ⟨c';;while (b) cx,s',l' + 2⟩"


lemma step_label_less:
  "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ⟹ l < #:prog ∧ l' < #:prog"
proof(induct rule:step.induct)
  case (StepSeq c1 c2 l s)
  from ‹labels (c1;;c2) l (Skip;;c2)›
  have "l < #:(c1;; c2)" by(rule label_less_num_inner_nodes)
  thus ?case by(simp add:num_inner_nodes_gr_0)
next
  case (StepSeqWhile b cx l s)
  from ‹labels (while (b) cx) l (Skip;;while (b) cx)›
  have "l < #:(while (b) cx)" by(rule label_less_num_inner_nodes)
  thus ?case by simp
qed (auto intro:num_inner_nodes_gr_0)



abbreviation steps :: "cmd ⇒ cmd ⇒ state ⇒ nat ⇒ cmd ⇒ state ⇒ nat ⇒ bool"
   (‹(_ ⊢ (1⟨_,/_,/_⟩) ↝*/ (1⟨_,/_,/_⟩))› [51,0,0,0,0,0,0] 81) where 
  "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩ == 
     (λ(c,s,l) (c',s',l'). prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩)** (c,s,l) (c',s',l')"


subsection‹Proof of bisimulation of @{term "⟨c,s⟩ → ⟨c',s'⟩"}\\
  and @{term "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩"} via @{term "labels"}›

(*<*)
lemmas converse_rtranclp_induct3 =
  converse_rtranclp_induct[of _ "(ax,ay,az)" "(bx,by,bz)", split_rule,
                 consumes 1, case_names refl step]
(*>*)


subsubsection ‹From @{term "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩"} to
  @{term "⟨c,s⟩ → ⟨c',s'⟩"}›

lemma step_red:
  "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ⟹ ⟨c,s⟩ → ⟨c',s'⟩"
by(induct rule:step.induct,rule RedLAss,auto intro:red.intros)



lemma steps_reds:
  "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩ ⟹ ⟨c,s⟩ →* ⟨c',s'⟩"
proof(induct rule:converse_rtranclp_induct3)
  case refl thus ?case by simp
next
  case (step c s l c'' s'' l'')
  then have "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s'',l''⟩"
    and "⟨c'',s''⟩ →* ⟨c',s'⟩" by simp_all
  from ‹prog ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s'',l''⟩› have "⟨c,s⟩ → ⟨c'',s''⟩"
    by(fastforce intro:step_red)
  with ‹⟨c'',s''⟩ →* ⟨c',s'⟩› show ?case
    by(fastforce intro:converse_rtranclp_into_rtranclp)
qed


(*<*)declare fun_upd_apply [simp del] One_nat_def [simp del](*>*)

subsubsection ‹From @{term "⟨c,s⟩ → ⟨c',s'⟩"} and @{term labels} to
  @{term "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩"}›

lemma red_step:
  "⟦labels prog l c; ⟨c,s⟩ → ⟨c',s'⟩⟧
  ⟹ ∃l'. prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels prog l' c'"
proof(induct arbitrary:c' rule:labels.induct)
  case (Labels_Base c)
  from ‹⟨c,s⟩ → ⟨c',s'⟩› show ?case
  proof(induct rule:red_induct)
    case (RedLAss V e s)
    have "V:=e ⊢ ⟨V:=e,s,0⟩ ↝ ⟨Skip,s(V:=(interpret e s)),1⟩" by(rule StepLAss)
    have "labels (V:=e) 1 Skip" by(fastforce intro:Labels_LAss)
    with ‹V:=e ⊢ ⟨V:=e,s,0⟩ ↝ ⟨Skip,s(V:=(interpret e s)),1⟩› show ?case by blast
  next
    case (SeqRed c1 s c1' s' c2)
    from ‹∃l'. c1 ⊢ ⟨c1,s,0⟩ ↝ ⟨c1',s',l'⟩ ∧ labels c1 l' c1'›
    obtain l' where "c1 ⊢ ⟨c1,s,0⟩ ↝ ⟨c1',s',l'⟩" and "labels c1 l' c1'" by blast
    from ‹c1 ⊢ ⟨c1,s,0⟩ ↝ ⟨c1',s',l'⟩› have "c1;;c2 ⊢ ⟨c1;;c2,s,0⟩ ↝ ⟨c1';;c2,s',l'⟩"
      by(rule StepRecSeq1)
    moreover
    from ‹labels c1 l' c1'› have "labels (c1;;c2) l' (c1';;c2)" by(rule Labels_Seq1)
    ultimately show ?case by blast
  next
    case (RedSeq c2 s)
    have "labels c2 0 c2" by(rule Labels.Labels_Base)
    hence "labels (Skip;;c2) (0 + #:Skip) c2" by(rule Labels_Seq2)
    have "labels (Skip;;c2) 0 (Skip;;c2)" by(rule Labels.Labels_Base)
    with ‹labels (Skip;;c2) (0 + #:Skip) c2›
    have "Skip;;c2 ⊢ ⟨Skip;;c2,s,0⟩ ↝ ⟨c2,s,#:Skip⟩"
      by(fastforce intro:StepSeq)
    with ‹labels (Skip;;c2) (0 + #:Skip) c2› show ?case by auto
  next
    case (RedCondTrue b s c1 c2)
    from ‹interpret b s = Some true›
    have "if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c1,s,1⟩"
      by(rule StepCondTrue)
    have "labels (if (b) c1 else c2) (0 + 1) c1"
      by(rule Labels_CondTrue,rule Labels.Labels_Base)
    with ‹if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c1,s,1⟩› show ?case by auto
  next
    case (RedCondFalse b s c1 c2)
    from ‹interpret b s = Some false› 
    have "if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c2,s,#:c1 + 1⟩"
      by(rule StepCondFalse)
    have "labels (if (b) c1 else c2) (0 + #:c1 + 1) c2"
      by(rule Labels_CondFalse,rule Labels.Labels_Base)
    with ‹if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c2,s,#:c1 + 1⟩›
    show ?case by auto
  next
    case (RedWhileTrue b s c)
    from ‹interpret b s = Some true›
    have "while (b) c ⊢ ⟨while (b) c,s,0⟩ ↝ ⟨c;; while (b) c,s,2⟩"
      by(rule StepWhileTrue)
    have "labels (while (b) c) (0 + 2) (c;; while (b) c)"
      by(rule Labels_WhileBody,rule Labels.Labels_Base)
    with ‹while (b) c ⊢ ⟨while (b) c,s,0⟩ ↝ ⟨c;; while (b) c,s,2⟩›
    show ?case by(auto simp del:add_2_eq_Suc')
  next
    case (RedWhileFalse b s c)
    from ‹interpret b s = Some false›
    have "while (b) c ⊢ ⟨while (b) c,s,0⟩ ↝ ⟨Skip,s,1⟩"
      by(rule StepWhileFalse)
    have "labels (while (b) c) 1 Skip" by(rule Labels_WhileExit)
    with ‹while (b) c ⊢ ⟨while (b) c,s,0⟩ ↝ ⟨Skip,s,1⟩› show ?case by auto
  qed
next
  case (Labels_LAss V e)
  from ‹⟨Skip,s⟩ → ⟨c',s'⟩› have False by(auto elim:red.cases)
  thus ?case by simp
next
  case (Labels_Seq1 c1 l c c2)
  note IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
        ∃l'. c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c1 l' c'›
  from ‹⟨c;;c2,s⟩ → ⟨c',s'⟩› 
  have "(c = Skip ∧ c' = c2 ∧ s = s') ∨ (∃c''. c' = c'';;c2)"
    by -(erule red.cases,auto)
  thus ?case
  proof
    assume [simp]:"c = Skip ∧ c' = c2 ∧ s = s'"
    from ‹labels c1 l c› have "l < #:c1"
      by(rule label_less_num_inner_nodes[simplified])
    have "labels (c1;;c2) (0 + #:c1) c2"
      by(rule Labels_Seq2,rule Labels_Base)
    from ‹labels c1 l c› have "labels (c1;; c2) l (Skip;;c2)"
      by(fastforce intro:Labels.Labels_Seq1)
    with ‹labels (c1;;c2) (0 + #:c1) c2› ‹l < #:c1› 
    have "c1;; c2 ⊢ ⟨Skip;;c2,s,l⟩ ↝ ⟨c2,s,#:c1⟩"
      by(fastforce intro:StepSeq)
    with ‹labels (c1;;c2) (0 + #:c1) c2› show ?case by auto
  next
    assume "∃c''. c' = c'';;c2"
    then obtain c'' where [simp]:"c' = c'';;c2" by blast
    have "c2 ≠ c'';; c2"
      by (induction c2) auto
    with ‹⟨c;;c2,s⟩ → ⟨c',s'⟩› have "⟨c,s⟩ → ⟨c'',s'⟩"
      by (auto elim!:red.cases)
    from IH[OF this] obtain l' where "c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩"
      and "labels c1 l' c''" by blast
    from ‹c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩› have "c1;;c2 ⊢ ⟨c;;c2,s,l⟩ ↝ ⟨c'';;c2,s',l'⟩"
      by(rule StepRecSeq1)
    from ‹labels c1 l' c''› have "labels (c1;;c2) l' (c'';;c2)"
      by(rule Labels.Labels_Seq1)
    with ‹c1;;c2 ⊢ ⟨c;;c2,s,l⟩ ↝ ⟨c'';;c2,s',l'⟩› show ?case by auto
  qed
next
  case (Labels_Seq2 c2 l c c1 c')
  note IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
            ∃l'. c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c2 l' c'›
  from IH[OF ‹⟨c,s⟩ → ⟨c',s'⟩›] obtain l' where "c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    and "labels c2 l' c'" by blast
  from ‹c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩› have "c1;; c2 ⊢ ⟨c,s,l + #:c1⟩ ↝ ⟨c',s',l' + #:c1⟩"
    by(rule StepRecSeq2)
  moreover
  from ‹labels c2 l' c'› have "labels (c1;;c2) (l' + #:c1) c'"
    by(rule Labels.Labels_Seq2)
  ultimately show ?case by blast
next
  case (Labels_CondTrue c1 l c b c2 c')
  note label = ‹labels c1 l c› and red = ‹⟨c,s⟩ → ⟨c',s'⟩›
    and IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
                   ∃l'. c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c1 l' c'›
  from IH[OF ‹⟨c,s⟩ → ⟨c',s'⟩›] obtain l' where "c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    and "labels c1 l' c'" by blast
  from ‹c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩›
  have "if (b) c1 else c2 ⊢ ⟨c,s,l + 1⟩ ↝ ⟨c',s',l' + 1⟩"
    by(rule StepRecCond1)
  moreover
  from ‹labels c1 l' c'› have "labels (if (b) c1 else c2) (l' + 1) c'"
    by(rule Labels.Labels_CondTrue)
  ultimately show ?case by blast
next
  case (Labels_CondFalse c2 l c b c1 c')
  note IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
            ∃l'. c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c2 l' c'›
  from IH[OF ‹⟨c,s⟩ → ⟨c',s'⟩›] obtain l' where "c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    and "labels c2 l' c'" by blast
  from ‹c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩›
  have "if (b) c1 else c2 ⊢ ⟨c,s,l + #:c1 + 1⟩ ↝ ⟨c',s',l' + #:c1 + 1⟩"
    by(rule StepRecCond2)
  moreover
  from ‹labels c2 l' c'› have "labels (if (b) c1 else c2) (l' + #:c1 + 1) c'"
    by(rule Labels.Labels_CondFalse)
  ultimately show ?case by blast
next
  case (Labels_WhileBody c' l c b cx)
  note IH = ‹⋀c''. ⟨c,s⟩ → ⟨c'',s'⟩ ⟹
            ∃l'. c' ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩ ∧ labels c' l' c''›
  from ‹⟨c;;while (b) c',s⟩ → ⟨cx,s'⟩›
  have "(c = Skip ∧ cx = while (b) c' ∧ s = s') ∨ (∃c''. cx = c'';;while (b) c')"
    by -(erule red.cases,auto)
  thus ?case
  proof
    assume [simp]:"c = Skip ∧ cx = while (b) c' ∧ s = s'"
    have "labels (while (b) c') 0 (while (b) c')"
      by(fastforce intro:Labels_Base)
    from ‹labels c' l c› have "labels (while (b) c') (l + 2) (Skip;;while (b) c')"
      by(fastforce intro:Labels.Labels_WhileBody simp del:add_2_eq_Suc')
    hence "while (b) c' ⊢ ⟨Skip;;while (b) c',s,l + 2⟩ ↝ ⟨while (b) c',s,0⟩"
      by(rule StepSeqWhile)
    with ‹labels (while (b) c') 0 (while (b) c')› show ?case by simp blast
  next
    assume "∃c''. cx = c'';;while (b) c'"
    then obtain c'' where [simp]:"cx = c'';;while (b) c'" by blast
    with ‹⟨c;;while (b) c',s⟩ → ⟨cx,s'⟩› have "⟨c,s⟩ → ⟨c'',s'⟩"
      by(auto elim:red.cases)
    from IH[OF this] obtain l' where "c' ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩"
      and "labels c' l' c''" by blast
    from ‹c' ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩› 
    have "while (b) c' ⊢ ⟨c;;while (b) c',s,l + 2⟩ ↝ ⟨c'';;while (b) c',s',l' + 2⟩"
      by(rule StepRecWhile)
    moreover
    from ‹labels c' l' c''› have "labels (while (b) c') (l' + 2) (c'';;while (b) c')"
      by(rule Labels.Labels_WhileBody)
    ultimately show ?case by simp blast
  qed
next
  case (Labels_WhileExit b c' c'')
  from ‹⟨Skip,s⟩ → ⟨c'',s'⟩› have False by(auto elim:red.cases)
  thus ?case by simp
qed


lemma reds_steps:
  "⟦⟨c,s⟩ →* ⟨c',s'⟩; labels prog l c⟧
  ⟹ ∃l'. prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩ ∧ labels prog l' c'"
proof(induct rule:rtranclp_induct2)
  case refl
  from ‹labels prog l c› show ?case by blast
next
  case (step c'' s'' c' s')
  note IH = ‹labels prog l c ⟹    
    ∃l'. prog ⊢ ⟨c,s,l⟩ ↝* ⟨c'',s'',l'⟩ ∧ labels prog l' c''›
  from IH[OF ‹labels prog l c›] obtain l'' where "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c'',s'',l''⟩"
    and "labels prog l'' c''" by blast
  from ‹labels prog l'' c''› ‹⟨c'',s''⟩ → ⟨c',s'⟩› obtain l'
    where "prog ⊢ ⟨c'',s'',l''⟩ ↝ ⟨c',s',l'⟩"
    and "labels prog l' c'" by(auto dest:red_step)
  from ‹prog ⊢ ⟨c,s,l⟩ ↝* ⟨c'',s'',l''⟩› ‹prog ⊢ ⟨c'',s'',l''⟩ ↝ ⟨c',s',l'⟩›
  have "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩"
    by(fastforce elim:rtranclp_trans)
  with ‹labels prog l' c'› show ?case by blast
qed

subsubsection ‹The bisimulation theorem›

theorem reds_steps_bisimulation:
  "labels prog l c ⟹ (⟨c,s⟩ →* ⟨c',s'⟩) = 
     (∃l'. prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩ ∧ labels prog l' c')"
  by(fastforce intro:reds_steps elim:steps_reds)

end