Theory WEquivalence

section ‹Equivalence›

theory WEquivalence imports Semantics WCFG begin


subsection ‹From @{term "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"} to\\
  @{term "c ⊢ (_ l _) -et→ (_ l' _)"} with @{term transfers} and @{term preds}›

lemma Skip_WCFG_edge_Exit:
  "⟦labels prog l Skip⟧ ⟹ prog ⊢ (_ l _) -⇑id→ (_Exit_)"
proof(induct prog l Skip rule:labels.induct)
  case Labels_Base
  show ?case by(fastforce intro:WCFG_Skip)
next
  case (Labels_LAss V e)
  show ?case by(rule WCFG_LAssSkip)
next
  case (Labels_Seq2 c2 l c1)
  from ‹c2 ⊢ (_ l _) -⇑id→ (_Exit_)›
  have "c1;;c2 ⊢ (_ l _) ⊕ #:c1 -⇑id→ (_Exit_) ⊕ #:c1"
    by(fastforce intro:WCFG_SeqSecond)
  thus ?case by(simp del:id_apply)
next
  case (Labels_CondTrue c1 l b c2)
  from ‹c1 ⊢ (_ l _) -⇑id→ (_Exit_)›
  have "if (b) c1 else c2 ⊢ (_ l _) ⊕ 1 -⇑id→ (_Exit_) ⊕ 1"
    by(fastforce intro:WCFG_CondThen)
  thus ?case by(simp del:id_apply)
next
  case (Labels_CondFalse c2 l b c1)
  from ‹c2 ⊢ (_ l _) -⇑id→ (_Exit_)›
  have "if (b) c1 else c2 ⊢ (_ l _) ⊕ (#:c1 + 1) -⇑id→ (_Exit_) ⊕ (#:c1 + 1)"
    by(fastforce intro:WCFG_CondElse)
  thus ?case by(simp del:id_apply)
next
  case (Labels_WhileExit b c')
  show ?case by(rule WCFG_WhileFalseSkip)
qed


lemma step_WCFG_edge:
  assumes "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
  obtains et where "prog ⊢ (_ l _) -et→ (_ l' _)" and "transfer et s = s'"
  and "pred et s"
proof -
  from ‹prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩›
  have "∃et. prog ⊢ (_ l _) -et→ (_ l' _) ∧ transfer et s = s' ∧ pred et s"
  proof(induct rule:step.induct)
    case (StepLAss V e s)
    have "pred ⇑(λs. s(V:=(interpret e s))) s" by simp
    have "V:=e ⊢ (_0_) -⇑(λs. s(V:=(interpret e s)))→ (_1_)"
      by(rule WCFG_LAss)
    have "transfer ⇑(λs. s(V:=(interpret e s))) s = s(V:=(interpret e s))" by simp
    with ‹pred ⇑(λs. s(V:=(interpret e s))) s›
      ‹V:=e ⊢ (_0_) -⇑(λs. s(V:=(interpret e s)))→ (_1_)› show ?case by blast
  next
    case (StepSeq c1 c2 l s)
    from ‹labels (c1;;c2) l (Skip;;c2)› ‹l < #:c1› have "labels c1 l Skip"
      by(auto elim:labels.cases intro:Labels_Base)
    hence "c1 ⊢ (_ l _) -⇑id→ (_Exit_)" 
      by(fastforce intro:Skip_WCFG_edge_Exit)
    hence "c1;;c2 ⊢ (_ l _) -⇑id→ (_0_) ⊕ #:c1" 
      by(rule WCFG_SeqConnect,simp)
    thus ?case by auto
  next
    case (StepSeqWhile b cx l s)
    from ‹labels (while (b) cx) l (Skip;;while (b) cx)›
    obtain lx where "labels cx lx Skip" 
      and [simp]:"l = lx + 2" by(auto elim:labels.cases)
    hence "cx ⊢ (_ lx _) -⇑id→ (_Exit_)" 
      by(fastforce intro:Skip_WCFG_edge_Exit)
    hence "while (b) cx ⊢ (_ lx _) ⊕ 2 -⇑id→ (_0_)"
      by(fastforce intro:WCFG_WhileBodyExit)
    thus ?case by auto
  next
    case (StepCondTrue b s c1 c2)
    from ‹interpret b s = Some true›
    have "pred (λs. interpret b s = Some true)√ s" by simp
    moreover
    have "if (b) c1 else c2 ⊢ (_0_) -(λs. interpret b s = Some true)√→ (_0_) ⊕ 1"
      by(rule WCFG_CondTrue)
    moreover
    have "transfer (λs. interpret b s = Some true)√ s = s" by simp
    ultimately show ?case by auto
  next
    case (StepCondFalse b s c1 c2)
    from ‹interpret b s = Some false›
    have "pred (λs. interpret b s = Some false)√ s" by simp
    moreover
    have "if (b) c1 else c2 ⊢ (_0_) -(λs. interpret b s = Some false)√→ 
                                   (_0_) ⊕ (#:c1 + 1)"
      by(rule WCFG_CondFalse)
    moreover
    have "transfer (λs. interpret b s = Some false)√ s = s" by simp
    ultimately show ?case by auto
  next
    case (StepWhileTrue b s c)
    from ‹interpret b s = Some true›
    have "pred (λs. interpret b s = Some true)√ s" by simp
    moreover
    have "while (b) c ⊢ (_0_) -(λs. interpret b s = Some true)√→ (_0_) ⊕ 2" 
      by(rule WCFG_WhileTrue)
    moreover
    have "transfer (λs. interpret b s = Some true)√ s = s" by simp
    ultimately show ?case by(auto simp del:add_2_eq_Suc')
  next
    case (StepWhileFalse b s c)
    from ‹interpret b s = Some false›
    have "pred (λs. interpret b s = Some false)√ s" by simp
    moreover
    have "while (b) c ⊢ (_0_) -(λs. interpret b s = Some false)√→ (_1_)"
      by(rule WCFG_WhileFalse)
    moreover
    have "transfer (λs. interpret b s = Some false)√ s = s" by simp
    ultimately show ?case by auto
  next
    case (StepRecSeq1 prog c s l c' s' l' c2)
    from ‹∃et. prog ⊢ (_ l _) -et→ (_ l' _) ∧ transfer et s = s' ∧ pred et s›
    obtain et where "prog ⊢ (_ l _) -et→ (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from ‹prog ⊢ (_ l _) -et→ (_ l' _)› have "prog;;c2 ⊢ (_ l _) -et→ (_ l' _)"
      by(fastforce intro:WCFG_SeqFirst)
    ultimately show ?case by blast
  next
    case (StepRecSeq2 prog c s l c' s' l' c1)
    from ‹∃et. prog ⊢ (_ l _) -et→ (_ l' _) ∧ transfer et s = s' ∧ pred et s›
    obtain et where "prog ⊢ (_ l _) -et→ (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from ‹prog ⊢ (_ l _) -et→ (_ l' _)› 
    have "c1;;prog ⊢ (_ l _) ⊕ #:c1 -et→ (_ l' _) ⊕ #:c1"
      by(fastforce intro:WCFG_SeqSecond)
    ultimately show ?case by simp blast
  next
    case (StepRecCond1 prog c s l c' s' l' b c2)
    from ‹∃et. prog ⊢ (_ l _) -et→ (_ l' _) ∧ transfer et s = s' ∧ pred et s›
    obtain et where "prog ⊢ (_ l _) -et→ (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from ‹prog ⊢ (_ l _) -et→ (_ l' _)› 
    have "if (b) prog else c2 ⊢ (_ l _) ⊕ 1 -et→ (_ l' _) ⊕ 1"
      by(fastforce intro:WCFG_CondThen)
    ultimately show ?case by simp blast
  next
    case (StepRecCond2 prog c s l c' s' l' b c1)
    from ‹∃et. prog ⊢ (_ l _) -et→ (_ l' _) ∧ transfer et s = s' ∧ pred et s›
    obtain et where "prog ⊢ (_ l _) -et→ (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from ‹prog ⊢ (_ l _) -et→ (_ l' _)›
    have "if (b) c1 else prog ⊢ (_ l _) ⊕ (#:c1 + 1) -et→ (_ l' _) ⊕ (#:c1 + 1)"
      by(fastforce intro:WCFG_CondElse)
    ultimately show ?case by simp blast
  next
    case (StepRecWhile cx c s l c' s' l' b)
    from ‹∃et. cx ⊢ (_ l _) -et→ (_ l' _) ∧ transfer et s = s' ∧ pred et s›
    obtain et where "cx ⊢ (_ l _) -et→ (_ l' _)"
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    hence "while (b) cx ⊢ (_ l _) ⊕ 2 -et→ (_ l' _) ⊕ 2"
      by(fastforce intro:WCFG_WhileBody)
    ultimately show ?case by simp blast
  qed
  with that show ?thesis by blast
qed


subsection ‹From @{term "c ⊢ (_ l _) -et→ (_ l' _)"} with @{term transfers} 
  and @{term preds} to\\
  @{term "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"}›

(*<*)declare One_nat_def [simp del] add_2_eq_Suc' [simp del](*>*)

lemma WCFG_edge_Exit_Skip:
  "⟦prog ⊢ n -et→ (_Exit_); n ≠ (_Entry_)⟧
  ⟹ ∃l. n = (_ l _) ∧ labels prog l Skip ∧ et = ⇑id"
proof(induct prog n et "(_Exit_)" rule:WCFG_induct)
  case WCFG_Skip show ?case by(fastforce intro:Labels_Base)
next
  case WCFG_LAssSkip show ?case by(fastforce intro:Labels_LAss)
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = ‹⟦n' = (_Exit_); n ≠ (_Entry_)⟧ 
    ⟹ ∃l. n = (_ l _) ∧ labels c2 l Skip ∧ et = ⇑id›
  from ‹n' ⊕ #:c1 = (_Exit_)› have "n' = (_Exit_)" by(cases n') auto
  from IH[OF this ‹n ≠ (_Entry_)›] obtain l where [simp]:"n = (_ l _)" "et = ⇑id"
    and "labels c2 l Skip" by blast
  hence "labels (c1;;c2) (l + #:c1) Skip" by(fastforce intro:Labels_Seq2)
  thus ?case by(fastforce simp:id_def)
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = ‹⟦n' = (_Exit_); n ≠ (_Entry_)⟧
    ⟹ ∃l. n = (_ l _) ∧ labels c1 l Skip ∧ et = ⇑id›
  from ‹n' ⊕ 1 = (_Exit_)› have "n' = (_Exit_)" by(cases n') auto
  from IH[OF this ‹n ≠ (_Entry_)›] obtain l where [simp]:"n = (_ l _)" "et = ⇑id"
    and "labels c1 l Skip" by blast
  hence "labels (if (b) c1 else c2) (l + 1) Skip"
    by(fastforce intro:Labels_CondTrue)
  thus ?case by(fastforce simp:id_def)
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = ‹⟦n' = (_Exit_); n ≠ (_Entry_)⟧
    ⟹ ∃l. n = (_ l _) ∧ labels c2 l Skip ∧ et = ⇑id›
  from ‹n' ⊕ #:c1 + 1 = (_Exit_)› have "n' = (_Exit_)" by(cases n') auto
  from IH[OF this ‹n ≠ (_Entry_)›] obtain l where [simp]:"n = (_ l _)" "et = ⇑id"
    and label:"labels c2 l Skip" by blast
  hence "labels (if (b) c1 else c2) (l + #:c1 + 1) Skip"
    by(fastforce intro:Labels_CondFalse)
  thus ?case by(fastforce simp:add.assoc id_def)
next
  case WCFG_WhileFalseSkip show ?case by(fastforce intro:Labels_WhileExit)
next
  case (WCFG_WhileBody c' n et n' b) thus ?case by(cases n') auto
qed simp_all


lemma WCFG_edge_step:
  "⟦prog ⊢ (_ l _) -et→ (_ l' _); transfer et s = s'; pred et s⟧
  ⟹ ∃c c'. prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels prog l c ∧ labels prog l' c'"
proof(induct prog "(_ l _)" et "(_ l' _)" arbitrary:l l' rule:WCFG_induct)
  case (WCFG_LAss V e)
  from ‹transfer ⇑λs. s(V:=(interpret e s)) s = s'›
  have [simp]:"s' = s(V:=(interpret e s))" by(simp del:fun_upd_apply)
  have "labels (V:=e) 0 (V:=e)" by(fastforce intro:Labels_Base)
  moreover
  hence "labels (V:=e) 1 Skip" by(fastforce intro:Labels_LAss)
  ultimately show ?case
    apply(rule_tac x="V:=e" in exI)
    apply(rule_tac x="Skip" in exI)
    by(fastforce intro:StepLAss simp del:fun_upd_apply)
next
  case (WCFG_SeqFirst c1 et c2)
  note IH = ‹⟦transfer et s = s'; pred et s⟧
    ⟹ ∃c c'. c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c1 l c ∧ labels c1 l' c'›
  from IH[OF ‹transfer et s = s'› ‹pred et s›]
  obtain c c' where "c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    and "labels c1 l c" 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)
  moreover 
  from ‹labels c1 l c› have "labels (c1;;c2) l (c;;c2)"
    by(fastforce intro:Labels_Seq1)
  moreover 
  from ‹labels c1 l' c'› have "labels (c1;;c2) l' (c';;c2)"
    by(fastforce intro:Labels_Seq1)
  ultimately show ?case by blast
next
  case (WCFG_SeqConnect c1 et c2)
  from ‹c1 ⊢ (_ l _) -et→ (_Exit_)›
  have "labels c1 l Skip" and [simp]:"et = ⇑id"
    by(auto dest:WCFG_edge_Exit_Skip)
  from ‹transfer et s = s'› have [simp]:"s' = s" by simp
  have "labels c2 0 c2" by(fastforce intro:Labels_Base)
  hence "labels (c1;;c2) #:c1 c2" by(fastforce dest:Labels_Seq2)
  moreover
  from ‹labels c1 l Skip› have "labels (c1;;c2) l (Skip;;c2)"
    by(fastforce intro:Labels_Seq1)
  moreover
  from ‹labels c1 l Skip› have "l < #:c1" by(rule label_less_num_inner_nodes)
  ultimately 
  have "c1;;c2 ⊢ ⟨Skip;;c2,s,l⟩ ↝ ⟨c2,s,#:c1⟩" by -(rule StepSeq)
  with ‹labels (c1;;c2) l (Skip;;c2)›
    ‹labels (c1;;c2) #:c1 c2› ‹(_0_) ⊕ #:c1 = (_ l' _)› show ?case by simp blast
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = ‹⋀l l'. ⟦n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s⟧
    ⟹ ∃c c'. c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c2 l c ∧ labels c2 l' c'›
  from ‹n ⊕ #:c1 = (_ l _)› obtain lx where "n = (_ lx _)" 
    and [simp]:"l = lx + #:c1"
    by(cases n) auto
  from ‹n' ⊕ #:c1 = (_ l' _)› obtain lx' where "n' = (_ lx' _)" 
    and [simp]:"l' = lx' + #:c1"
    by(cases n') auto
  from IH[OF ‹n = (_ lx _)› ‹n' = (_ lx' _)› ‹transfer et s = s'› ‹pred et s›]
  obtain c c' where "c2 ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩"
    and "labels c2 lx c" and "labels c2 lx' c'" by blast
  from ‹c2 ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩› have "c1;;c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    by(fastforce intro:StepRecSeq2)
  moreover 
  from ‹labels c2 lx c› have "labels (c1;;c2) l c" by(fastforce intro:Labels_Seq2)
  moreover 
  from ‹labels c2 lx' c'› have "labels (c1;;c2) l' c'" by(fastforce intro:Labels_Seq2)
  ultimately show ?case by blast
next
  case (WCFG_CondTrue b c1 c2)
  from ‹(_0_) ⊕ 1 = (_ l' _)› have [simp]:"l' = 1" by simp
  from ‹transfer (λs. interpret b s = Some true)√ s = s'› have [simp]:"s' = s" by simp
  have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)"
    by(fastforce intro:Labels_Base)
  have "labels c1 0 c1" by(fastforce intro:Labels_Base)
  hence "labels (if (b) c1 else c2) 1 c1" by(fastforce dest:Labels_CondTrue)
  from ‹pred (λs. interpret b s = Some true)√ s›
  have "interpret b s = Some true" by simp
  hence "if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c1,s,1⟩"
    by(rule StepCondTrue)
  with  ‹labels (if (b) c1 else c2) 0 (if (b) c1 else c2)›
    ‹labels (if (b) c1 else c2) 1 c1› show ?case by simp blast
next
  case (WCFG_CondFalse b c1 c2)
  from ‹(_0_) ⊕ #:c1 + 1 = (_ l' _)› have [simp]:"l' = #:c1 + 1" by simp
  from ‹transfer (λs. interpret b s = Some false)√ s = s'› have [simp]:"s' = s"
    by simp
  have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)"
    by(fastforce intro:Labels_Base)
  have "labels c2 0 c2" by(fastforce intro:Labels_Base)
  hence "labels (if (b) c1 else c2) (#:c1 + 1) c2" by(fastforce dest:Labels_CondFalse)
  from ‹pred (λs. interpret b s = Some false)√ s›
  have "interpret b s = Some false" by simp
  hence "if (b) c1 else c2 ⊢ ⟨if (b) c1 else c2,s,0⟩ ↝ ⟨c2,s,#:c1 + 1⟩"
    by(rule StepCondFalse)
  with ‹labels (if (b) c1 else c2) 0 (if (b) c1 else c2)›
    ‹labels (if (b) c1 else c2) (#:c1 + 1) c2› show ?case by simp blast
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = ‹⋀l l'. ⟦n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s⟧
    ⟹ ∃c c'. c1 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c1 l c ∧ labels c1 l' c'›
  from ‹n ⊕ 1 = (_ l _)› obtain lx where "n = (_ lx _)" and [simp]:"l = lx + 1"
    by(cases n) auto
  from ‹n' ⊕ 1 = (_ l' _)› obtain lx' where "n' = (_ lx' _)" and [simp]:"l' = lx' + 1"
    by(cases n') auto
  from IH[OF ‹n = (_ lx _)› ‹n' = (_ lx' _)› ‹transfer et s = s'› ‹pred et s›]
  obtain c c'  where "c1 ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩"
    and "labels c1 lx c" and "labels c1 lx' c'" by blast
  from ‹c1 ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩› have "if (b) c1 else c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    by(fastforce intro:StepRecCond1)
  moreover 
  from ‹labels c1 lx c› have "labels (if (b) c1 else c2) l c"
    by(fastforce intro:Labels_CondTrue)
  moreover 
  from ‹labels c1 lx' c'› have "labels (if (b) c1 else c2) l' c'"
    by(fastforce intro:Labels_CondTrue)
  ultimately show ?case by blast
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = ‹⋀l l'. ⟦n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s⟧
    ⟹ ∃c c'. c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels c2 l c ∧ labels c2 l' c'›
  from ‹n ⊕ #:c1 + 1 = (_ l _)› obtain lx where "n = (_ lx _)" 
    and [simp]:"l = lx + #:c1 + 1"
    by(cases n) auto
  from ‹n' ⊕ #:c1 + 1 = (_ l' _)› obtain lx' where "n' = (_ lx' _)" 
    and [simp]:"l' = lx' + #:c1 + 1"
    by(cases n') auto
  from IH[OF ‹n = (_ lx _)› ‹n' = (_ lx' _)› ‹transfer et s = s'› ‹pred et s›]
  obtain c c' where "c2 ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩"
    and "labels c2 lx c" and "labels c2 lx' c'" by blast
  from ‹c2 ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩› have "if (b) c1 else c2 ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩"
    by(fastforce intro:StepRecCond2)
  moreover 
  from ‹labels c2 lx c› have "labels (if (b) c1 else c2) l c"
    by(fastforce intro:Labels_CondFalse)
  moreover 
  from ‹labels c2 lx' c'› have "labels (if (b) c1 else c2) l' c'"
    by(fastforce intro:Labels_CondFalse)
  ultimately show ?case by blast
next
  case (WCFG_WhileTrue b cx)
  from ‹(_0_) ⊕ 2 = (_ l' _)› have [simp]:"l' = 2" by simp
  from ‹transfer (λs. interpret b s = Some true)√ s = s'› have [simp]:"s' = s" by simp
  have "labels (while (b) cx) 0 (while (b) cx)"
    by(fastforce intro:Labels_Base)
  have "labels cx 0 cx" by(fastforce intro:Labels_Base)
  hence "labels (while (b) cx) 2 (cx;;while (b) cx)"
    by(fastforce dest:Labels_WhileBody)
  from ‹pred (λs. interpret b s = Some true)√ s› have "interpret b s = Some true" by simp
  hence "while (b) cx ⊢ ⟨while (b) cx,s,0⟩ ↝ ⟨cx;;while (b) cx,s,2⟩"
    by(rule StepWhileTrue)
  with ‹labels (while (b) cx) 0 (while (b) cx)›
    ‹labels (while (b) cx) 2 (cx;;while (b) cx)› show ?case by simp blast
next
  case (WCFG_WhileFalse b cx)
  from ‹transfer (λs. interpret b s = Some false)√ s = s'› have [simp]:"s' = s"
    by simp
  have "labels (while (b) cx) 0 (while (b) cx)" by(fastforce intro:Labels_Base)
  have "labels (while (b) cx) 1 Skip" by(fastforce intro:Labels_WhileExit)
  from ‹pred (λs. interpret b s = Some false)√ s› have "interpret b s = Some false"
    by simp
  hence "while (b) cx ⊢ ⟨while (b) cx,s,0⟩ ↝ ⟨Skip,s,1⟩"
    by(rule StepWhileFalse)
  with ‹labels (while (b) cx) 0 (while (b) cx)› ‹labels (while (b) cx) 1 Skip›
  show ?case by simp blast
next
  case (WCFG_WhileBody cx n et n' b)
  note IH = ‹⋀l l'. ⟦n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s⟧
    ⟹ ∃c c'. cx ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩ ∧ labels cx l c ∧ labels cx l' c'›
  from ‹n ⊕ 2 = (_ l _)› obtain lx where "n = (_ lx _)" and [simp]:"l = lx + 2"
    by(cases n) auto
  from ‹n' ⊕ 2 = (_ l' _)› obtain lx' where "n' = (_ lx' _)" 
    and [simp]:"l' = lx' + 2" by(cases n') auto
  from IH[OF ‹n = (_ lx _)› ‹n' = (_ lx' _)› ‹transfer et s = s'› ‹pred et s›]
  obtain c c' where "cx ⊢ ⟨c,s,lx⟩ ↝ ⟨c',s',lx'⟩"
    and "labels cx lx c" and "labels cx lx' c'" by blast
  hence "while (b) cx ⊢ ⟨c;;while (b) cx,s,l⟩ ↝ ⟨c';;while (b) cx,s',l'⟩"
    by(fastforce intro:StepRecWhile)
  moreover 
  from ‹labels cx lx c› have "labels (while (b) cx) l (c;;while (b) cx)"
    by(fastforce intro:Labels_WhileBody)
  moreover 
  from ‹labels cx lx' c'› have "labels (while (b) cx) l' (c';;while (b) cx)"
    by(fastforce intro:Labels_WhileBody)
  ultimately show ?case by blast
next
  case (WCFG_WhileBodyExit cx n et b)
  from ‹n ⊕ 2 = (_ l _)› obtain lx where [simp]:"n = (_ lx _)" and [simp]:"l = lx + 2"
    by(cases n) auto
  from ‹cx ⊢ n -et→ (_Exit_)› have "labels cx lx Skip" and [simp]:"et = ⇑id"
    by(auto dest:WCFG_edge_Exit_Skip)
  from ‹transfer et s = s'› have [simp]:"s' = s" by simp
  from ‹labels cx lx Skip› have "labels (while (b) cx) l (Skip;;while (b) cx)"
    by(fastforce intro:Labels_WhileBody)
  hence "while (b) cx ⊢ ⟨Skip;;while (b) cx,s,l⟩ ↝ ⟨while (b) cx,s,0⟩"
    by(rule StepSeqWhile)
  moreover
  have "labels (while (b) cx) 0 (while (b) cx)"
    by(fastforce intro:Labels_Base)
  ultimately show ?case 
    using ‹labels (while (b) cx) l (Skip;;while (b) cx)› by simp blast
qed


end