Theory Semantics

header {* \isaheader{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"
   ("(_ \<turnstile> (1⟨_,/_,/_⟩) \<leadsto>/ (1⟨_,/_,/_⟩))" [51,0,0,0,0,0,0] 81)
where

StepLAss:
  "V:=e \<turnstile> ⟨V:=e,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨Skip;;c⇣2,s,l⟩ \<leadsto> ⟨c⇣2,s,#:c⇣1⟩"

| StepSeqWhile:
  "labels (while (b) c') l (Skip;;while (b) c')
  ==> while (b) c' \<turnstile> ⟨Skip;;while (b) c',s,l⟩ \<leadsto> ⟨while (b) c',s,0⟩"

| StepCondTrue:
  "interpret b s = Some true 
     ==> if (b) c⇣1 else c⇣2 \<turnstile> ⟨if (b) c⇣1 else c⇣2,s,0⟩ \<leadsto> ⟨c⇣1,s,1⟩"

| StepCondFalse:
  "interpret b s = Some false 
  ==> if (b) c⇣1 else c⇣2 \<turnstile> ⟨if (b) c⇣1 else c⇣2,s,0⟩ \<leadsto> ⟨c⇣2,s,#:c⇣1 + 1⟩"

| StepWhileTrue:
  "interpret b s = Some true 
     ==> while (b) c \<turnstile> ⟨while (b) c,s,0⟩ \<leadsto> ⟨c;;while (b) c,s,2⟩"

| StepWhileFalse:
  "interpret b s = Some false ==> while (b) c \<turnstile> ⟨while (b) c,s,0⟩ \<leadsto> ⟨Skip,s,1⟩"

| StepRecSeq1:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩
  ==> prog;;c⇣2 \<turnstile> ⟨c;;c⇣2,s,l⟩ \<leadsto> ⟨c';;c⇣2,s',l'⟩"

| StepRecSeq2:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ 
  ==> c⇣1;;prog \<turnstile> ⟨c,s,l + #:c⇣1⟩ \<leadsto> ⟨c',s',l' + #:c⇣1⟩"

| StepRecCond1:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ 
  ==> if (b) prog else c⇣2 \<turnstile> ⟨c,s,l + 1⟩ \<leadsto> ⟨c',s',l' + 1⟩"

| StepRecCond2:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ 
  ==> if (b) c⇣1 else prog \<turnstile> ⟨c,s,l + #:c⇣1 + 1⟩ \<leadsto> ⟨c',s',l' + #:c⇣1 + 1⟩"

| StepRecWhile:
  "cx \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩
  ==> while (b) cx \<turnstile> ⟨c;;while (b) cx,s,l + 2⟩ \<leadsto> ⟨c';;while (b) cx,s',l' + 2⟩"


lemma step_label_less:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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)
  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"
   ("(_ \<turnstile> (1⟨_,/_,/_⟩) \<leadsto>*/ (1⟨_,/_,/_⟩))" [51,0,0,0,0,0,0] 81) where 
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c',s',l'⟩ == 
     (λ(c,s,l) (c',s',l'). prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩)⇧*⇧* (c,s,l) (c',s',l')"


subsection{* Proof of bisimulation of @{term "⟨c,s⟩ -> ⟨c',s'⟩"}\\
  and @{term "prog \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c',s',l'⟩"} to
  @{term "⟨c,s⟩ -> ⟨c',s'⟩"} *}

lemma step_red:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ==> ⟨c,s⟩ -> ⟨c',s'⟩"
by(induct rule:step.induct,rule RedLAss,auto intro:red.intros)



lemma steps_reds:
  "prog \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c'',s'',l''⟩"
    and "⟨c'',s''⟩ ->* ⟨c',s'⟩" by simp_all
  from `prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c',s',l'⟩"} *}

lemma red_step:
  "[|labels prog l c; ⟨c,s⟩ -> ⟨c',s'⟩|]
  ==> ∃l'. prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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 \<turnstile> ⟨V:=e,s,0⟩ \<leadsto> ⟨Skip,s(V:=(interpret e s)),1⟩" by(rule StepLAss)
    have "labels (V:=e) 1 Skip" by(fastforce intro:Labels_LAss)
    with `V:=e \<turnstile> ⟨V:=e,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨c⇣1,s,0⟩ \<leadsto> ⟨c⇣1',s',l'⟩ ∧ labels c⇣1 l' c⇣1'`
    obtain l' where "c⇣1 \<turnstile> ⟨c⇣1,s,0⟩ \<leadsto> ⟨c⇣1',s',l'⟩" and "labels c⇣1 l' c⇣1'" by blast
    from `c⇣1 \<turnstile> ⟨c⇣1,s,0⟩ \<leadsto> ⟨c⇣1',s',l'⟩` have "c⇣1;;c⇣2 \<turnstile> ⟨c⇣1;;c⇣2,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨Skip;;c⇣2,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨if (b) c⇣1 else c⇣2,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨if (b) c⇣1 else c⇣2,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨if (b) c⇣1 else c⇣2,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨if (b) c⇣1 else c⇣2,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨while (b) c,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨while (b) c,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨while (b) c,s,0⟩ \<leadsto> ⟨Skip,s,1⟩"
      by(rule StepWhileFalse)
    have "labels (while (b) c) 1 Skip" by(rule Labels_WhileExit)
    with `while (b) c \<turnstile> ⟨while (b) c,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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 \<turnstile> ⟨Skip;;c⇣2,s,l⟩ \<leadsto> ⟨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
    with `⟨c;;c⇣2,s⟩ -> ⟨c',s'⟩` have "⟨c,s⟩ -> ⟨c'',s'⟩"
      by(auto elim!:red.cases,induct c⇣2,auto)
    from IH[OF this] obtain l' where "c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c'',s',l'⟩"
      and "labels c⇣1 l' c''" by blast
    from `c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c'',s',l'⟩` have "c⇣1;;c⇣2 \<turnstile> ⟨c;;c⇣2,s,l⟩ \<leadsto> ⟨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 \<turnstile> ⟨c;;c⇣2,s,l⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣2 l' c'`
  from IH[OF `⟨c,s⟩ -> ⟨c',s'⟩`] obtain l' where "c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    and "labels c⇣2 l' c'" by blast
  from `c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩` have "c⇣1;; c⇣2 \<turnstile> ⟨c,s,l + #:c⇣1⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣1 l' c'`
  from IH[OF `⟨c,s⟩ -> ⟨c',s'⟩`] obtain l' where "c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    and "labels c⇣1 l' c'" by blast
  from `c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩`
  have "if (b) c⇣1 else c⇣2 \<turnstile> ⟨c,s,l + 1⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣2 l' c'`
  from IH[OF `⟨c,s⟩ -> ⟨c',s'⟩`] obtain l' where "c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    and "labels c⇣2 l' c'" by blast
  from `c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩`
  have "if (b) c⇣1 else c⇣2 \<turnstile> ⟨c,s,l + #:c⇣1 + 1⟩ \<leadsto> ⟨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' \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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' \<turnstile> ⟨Skip;;while (b) c',s,l + 2⟩ \<leadsto> ⟨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' \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c'',s',l'⟩"
      and "labels c' l' c''" by blast
    from `c' \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c'',s',l'⟩` 
    have "while (b) c' \<turnstile> ⟨c;;while (b) c',s,l + 2⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c'',s'',l'⟩ ∧ labels prog l' c''`
  from IH[OF `labels prog l c`] obtain l'' where "prog \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c'',s'',l''⟩"
    and "labels prog l'' c''" by blast
  from `labels prog l'' c''` `⟨c'',s''⟩ -> ⟨c',s'⟩` obtain l'
    where "prog \<turnstile> ⟨c'',s'',l''⟩ \<leadsto> ⟨c',s',l'⟩"
    and "labels prog l' c'" by(auto dest:red_step)
  from `prog \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c'',s'',l''⟩` `prog \<turnstile> ⟨c'',s'',l''⟩ \<leadsto> ⟨c',s',l'⟩`
  have "prog \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto>* ⟨c',s',l'⟩ ∧ labels prog l' c')"
  by(fastforce intro:reds_steps elim:steps_reds)

end