# 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:
"⟨c⇩1,s⟩ → ⟨c⇩1',s'⟩ ⟹ ⟨c⇩1;;c⇩2,s⟩ → ⟨c⇩1';;c⇩2,s'⟩"

| RedSeq:
"⟨Skip;;c⇩2,s⟩ → ⟨c⇩2,s⟩"

| RedCondTrue:
"interpret b s = Some true ⟹ ⟨if (b) c⇩1 else c⇩2,s⟩ → ⟨c⇩1,s⟩"

| RedCondFalse:
"interpret b s = Some false ⟹ ⟨if (b) c⇩1 else c⇩2,s⟩ → ⟨c⇩2,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 (c⇩1;;c⇩2) l (Skip;;c⇩2); labels (c⇩1;;c⇩2) #:c⇩1 c⇩2; l < #:c⇩1⟧
⟹ c⇩1;;c⇩2 ⊢ ⟨Skip;;c⇩2,s,l⟩ ↝ ⟨c⇩2,s,#:c⇩1⟩"

| 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) c⇩1 else c⇩2 ⊢ ⟨if (b) c⇩1 else c⇩2,s,0⟩ ↝ ⟨c⇩1,s,1⟩"

| StepCondFalse:
"interpret b s = Some false
⟹ if (b) c⇩1 else c⇩2 ⊢ ⟨if (b) c⇩1 else c⇩2,s,0⟩ ↝ ⟨c⇩2,s,#:c⇩1 + 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;;c⇩2 ⊢ ⟨c;;c⇩2,s,l⟩ ↝ ⟨c';;c⇩2,s',l'⟩"

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

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

| StepRecCond2:
"prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩
⟹ if (b) c⇩1 else prog ⊢ ⟨c,s,l + #:c⇩1 + 1⟩ ↝ ⟨c',s',l' + #:c⇩1 + 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 c⇩1 c⇩2 l s)
from ‹labels (c⇩1;;c⇩2) l (Skip;;c⇩2)›
have "l < #:(c⇩1;; c⇩2)" by(rule label_less_num_inner_nodes)
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 c⇩1 s c⇩1' s' c⇩2)
from ‹∃l'. c⇩1 ⊢ ⟨c⇩1,s,0⟩ ↝ ⟨c⇩1',s',l'⟩ ∧ labels c⇩1 l' c⇩1'›
obtain l' where "c⇩1 ⊢ ⟨c⇩1,s,0⟩ ↝ ⟨c⇩1',s',l'⟩" and "labels c⇩1 l' c⇩1'" by blast
from ‹c⇩1 ⊢ ⟨c⇩1,s,0⟩ ↝ ⟨c⇩1',s',l'⟩› have "c⇩1;;c⇩2 ⊢ ⟨c⇩1;;c⇩2,s,0⟩ ↝ ⟨c⇩1';;c⇩2,s',l'⟩"
by(rule StepRecSeq1)
moreover
from ‹labels c⇩1 l' c⇩1'› have "labels (c⇩1;;c⇩2) l' (c⇩1';;c⇩2)" by(rule Labels_Seq1)
ultimately show ?case by blast
next
case (RedSeq c⇩2 s)
have "labels c⇩2 0 c⇩2" by(rule Labels.Labels_Base)
hence "labels (Skip;;c⇩2) (0 + #:Skip) c⇩2" by(rule Labels_Seq2)
have "labels (Skip;;c⇩2) 0 (Skip;;c⇩2)" by(rule Labels.Labels_Base)
with ‹labels (Skip;;c⇩2) (0 + #:Skip) c⇩2›
have "Skip;;c⇩2 ⊢ ⟨Skip;;c⇩2,s,0⟩ ↝ ⟨c⇩2,s,#:Skip⟩"
by(fastforce intro:StepSeq)
with ‹labels (Skip;;c⇩2) (0 + #:Skip) c⇩2› show ?case by auto
next
case (RedCondTrue b s c⇩1 c⇩2)
from ‹interpret b s = Some true›
have "if (b) c⇩1 else c⇩2 ⊢ ⟨if (b) c⇩1 else c⇩2,s,0⟩ ↝ ⟨c⇩1,s,1⟩"
by(rule StepCondTrue)
have "labels (if (b) c⇩1 else c⇩2) (0 + 1) c⇩1"
by(rule Labels_CondTrue,rule Labels.Labels_Base)
with ‹if (b) c⇩1 else c⇩2 ⊢ ⟨if (b) c⇩1 else c⇩2,s,0⟩ ↝ ⟨c⇩1,s,1⟩› show ?case by auto
next
case (RedCondFalse b s c⇩1 c⇩2)
from ‹interpret b s = Some false›
have "if (b) c⇩1 else c⇩2 ⊢ ⟨if (b) c⇩1 else c⇩2,s,0⟩ ↝ ⟨c⇩2,s,#:c⇩1 + 1⟩"
by(rule StepCondFalse)
have "labels (if (b) c⇩1 else c⇩2) (0 + #:c⇩1 + 1) c⇩2"
by(rule Labels_CondFalse,rule Labels.Labels_Base)
with ‹if (b) c⇩1 else c⇩2 ⊢ ⟨if (b) c⇩1 else c⇩2,s,0⟩ ↝ ⟨c⇩2,s,#:c⇩1 + 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⟩›
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 c⇩1 l c c⇩2)
note IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
∃l'. c⇩1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c⇩1 l' c'›
from ‹⟨c;;c⇩2,s⟩ → ⟨c',s'⟩›
have "(c = Skip ∧ c' = c⇩2 ∧ s = s') ∨ (∃c''. c' = c'';;c⇩2)"
by -(erule red.cases,auto)
thus ?case
proof
assume [simp]:"c = Skip ∧ c' = c⇩2 ∧ s = s'"
from ‹labels c⇩1 l c› have "l < #:c⇩1"
by(rule label_less_num_inner_nodes[simplified])
have "labels (c⇩1;;c⇩2) (0 + #:c⇩1) c⇩2"
by(rule Labels_Seq2,rule Labels_Base)
from ‹labels c⇩1 l c› have "labels (c⇩1;; c⇩2) l (Skip;;c⇩2)"
by(fastforce intro:Labels.Labels_Seq1)
with ‹labels (c⇩1;;c⇩2) (0 + #:c⇩1) c⇩2› ‹l < #:c⇩1›
have "c⇩1;; c⇩2 ⊢ ⟨Skip;;c⇩2,s,l⟩ ↝ ⟨c⇩2,s,#:c⇩1⟩"
by(fastforce intro:StepSeq)
with ‹labels (c⇩1;;c⇩2) (0 + #:c⇩1) c⇩2› show ?case by auto
next
assume "∃c''. c' = c'';;c⇩2"
then obtain c'' where [simp]:"c' = c'';;c⇩2" by blast
have "c⇩2 ≠ c'';; c⇩2"
by (induction c⇩2) auto
with ‹⟨c;;c⇩2,s⟩ → ⟨c',s'⟩› have "⟨c,s⟩ → ⟨c'',s'⟩"
by (auto elim!:red.cases)
from IH[OF this] obtain l' where "c⇩1 ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩"
and "labels c⇩1 l' c''" by blast
from ‹c⇩1 ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s',l'⟩› have "c⇩1;;c⇩2 ⊢ ⟨c;;c⇩2,s,l⟩ ↝ ⟨c'';;c⇩2,s',l'⟩"
by(rule StepRecSeq1)
from ‹labels c⇩1 l' c''› have "labels (c⇩1;;c⇩2) l' (c'';;c⇩2)"
by(rule Labels.Labels_Seq1)
with ‹c⇩1;;c⇩2 ⊢ ⟨c;;c⇩2,s,l⟩ ↝ ⟨c'';;c⇩2,s',l'⟩› show ?case by auto
qed
next
case (Labels_Seq2 c⇩2 l c c⇩1 c')
note IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
∃l'. c⇩2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c⇩2 l' c'›
from IH[OF ‹⟨c,s⟩ → ⟨c',s'⟩›] obtain l' where "c⇩2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
and "labels c⇩2 l' c'" by blast
from ‹c⇩2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩› have "c⇩1;; c⇩2 ⊢ ⟨c,s,l + #:c⇩1⟩ ↝ ⟨c',s',l' + #:c⇩1⟩"
by(rule StepRecSeq2)
moreover
from ‹labels c⇩2 l' c'› have "labels (c⇩1;;c⇩2) (l' + #:c⇩1) c'"
by(rule Labels.Labels_Seq2)
ultimately show ?case by blast
next
case (Labels_CondTrue c⇩1 l c b c⇩2 c')
note label = ‹labels c⇩1 l c› and red = ‹⟨c,s⟩ → ⟨c',s'⟩›
and IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
∃l'. c⇩1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c⇩1 l' c'›
from IH[OF ‹⟨c,s⟩ → ⟨c',s'⟩›] obtain l' where "c⇩1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
and "labels c⇩1 l' c'" by blast
from ‹c⇩1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩›
have "if (b) c⇩1 else c⇩2 ⊢ ⟨c,s,l + 1⟩ ↝ ⟨c',s',l' + 1⟩"
by(rule StepRecCond1)
moreover
from ‹labels c⇩1 l' c'› have "labels (if (b) c⇩1 else c⇩2) (l' + 1) c'"
by(rule Labels.Labels_CondTrue)
ultimately show ?case by blast
next
case (Labels_CondFalse c⇩2 l c b c⇩1 c')
note IH = ‹⋀c'. ⟨c,s⟩ → ⟨c',s'⟩ ⟹
∃l'. c⇩2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c⇩2 l' c'›
from IH[OF ‹⟨c,s⟩ → ⟨c',s'⟩›] obtain l' where "c⇩2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
and "labels c⇩2 l' c'" by blast
from ‹c⇩2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩›
have "if (b) c⇩1 else c⇩2 ⊢ ⟨c,s,l + #:c⇩1 + 1⟩ ↝ ⟨c',s',l' + #:c⇩1 + 1⟩"
by(rule StepRecCond2)
moreover
from ‹labels c⇩2 l' c'› have "labels (if (b) c⇩1 else c⇩2) (l' + #:c⇩1 + 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')"
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
```