Theory WEquivalence

header {* \isaheader{Equivalence} *}

theory WEquivalence imports Semantics WCFG begin


subsection {* From @{term "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"} to\\
  @{term "c \<turnstile> (_ l _) -et-> (_ l' _)"} with @{term transfers} and @{term preds} *}

lemma Skip_WCFG_edge_Exit:
  "[|labels prog l Skip|] ==> prog \<turnstile> (_ l _) -\<Up>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 c⇣2 l c⇣1)
  from `c⇣2 \<turnstile> (_ l _) -\<Up>id-> (_Exit_)`
  have "c⇣1;;c⇣2 \<turnstile> (_ l _) ⊕ #:c⇣1 -\<Up>id-> (_Exit_) ⊕ #:c⇣1"
    by(fastforce intro:WCFG_SeqSecond)
  thus ?case by(simp del:id_apply)
next
  case (Labels_CondTrue c⇣1 l b c⇣2)
  from `c⇣1 \<turnstile> (_ l _) -\<Up>id-> (_Exit_)`
  have "if (b) c⇣1 else c⇣2 \<turnstile> (_ l _) ⊕ 1 -\<Up>id-> (_Exit_) ⊕ 1"
    by(fastforce intro:WCFG_CondThen)
  thus ?case by(simp del:id_apply)
next
  case (Labels_CondFalse c⇣2 l b c⇣1)
  from `c⇣2 \<turnstile> (_ l _) -\<Up>id-> (_Exit_)`
  have "if (b) c⇣1 else c⇣2 \<turnstile> (_ l _) ⊕ (#:c⇣1 + 1) -\<Up>id-> (_Exit_) ⊕ (#:c⇣1 + 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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
  obtains et where "prog \<turnstile> (_ l _) -et-> (_ l' _)" and "transfer et s = s'"
  and "pred et s"
proof -
  from `prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩`
  have "∃et. prog \<turnstile> (_ l _) -et-> (_ l' _) ∧ transfer et s = s' ∧ pred et s"
  proof(induct rule:step.induct)
    case (StepLAss V e s)
    have "pred \<Up>(λs. s(V:=(interpret e s))) s" by simp
    have "V:=e \<turnstile> (_0_) -\<Up>(λs. s(V:=(interpret e s)))-> (_1_)"
      by(rule WCFG_LAss)
    have "transfer \<Up>(λs. s(V:=(interpret e s))) s = s(V:=(interpret e s))" by simp
    with `pred \<Up>(λs. s(V:=(interpret e s))) s`
      `V:=e \<turnstile> (_0_) -\<Up>(λs. s(V:=(interpret e s)))-> (_1_)` show ?case by blast
  next
    case (StepSeq c⇣1 c⇣2 l s)
    from `labels (c⇣1;;c⇣2) l (Skip;;c⇣2)` `l < #:c⇣1` have "labels c⇣1 l Skip"
      by(auto elim:labels.cases intro:Labels_Base)
    hence "c⇣1 \<turnstile> (_ l _) -\<Up>id-> (_Exit_)" 
      by(fastforce intro:Skip_WCFG_edge_Exit)
    hence "c⇣1;;c⇣2 \<turnstile> (_ l _) -\<Up>id-> (_0_) ⊕ #:c⇣1" 
      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 \<turnstile> (_ lx _) -\<Up>id-> (_Exit_)" 
      by(fastforce intro:Skip_WCFG_edge_Exit)
    hence "while (b) cx \<turnstile> (_ lx _) ⊕ 2 -\<Up>id-> (_0_)"
      by(fastforce intro:WCFG_WhileBodyExit)
    thus ?case by auto
  next
    case (StepCondTrue b s c⇣1 c⇣2)
    from `interpret b s = Some true`
    have "pred (λs. interpret b s = Some true)⇣\<surd> s" by simp
    moreover
    have "if (b) c⇣1 else c⇣2 \<turnstile> (_0_) -(λs. interpret b s = Some true)⇣\<surd>-> (_0_) ⊕ 1"
      by(rule WCFG_CondTrue)
    moreover
    have "transfer (λs. interpret b s = Some true)⇣\<surd> s = s" by simp
    ultimately show ?case by auto
  next
    case (StepCondFalse b s c⇣1 c⇣2)
    from `interpret b s = Some false`
    have "pred (λs. interpret b s = Some false)⇣\<surd> s" by simp
    moreover
    have "if (b) c⇣1 else c⇣2 \<turnstile> (_0_) -(λs. interpret b s = Some false)⇣\<surd>-> 
                                   (_0_) ⊕ (#:c⇣1 + 1)"
      by(rule WCFG_CondFalse)
    moreover
    have "transfer (λs. interpret b s = Some false)⇣\<surd> 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)⇣\<surd> s" by simp
    moreover
    have "while (b) c \<turnstile> (_0_) -(λs. interpret b s = Some true)⇣\<surd>-> (_0_) ⊕ 2" 
      by(rule WCFG_WhileTrue)
    moreover
    have "transfer (λs. interpret b s = Some true)⇣\<surd> 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)⇣\<surd> s" by simp
    moreover
    have "while (b) c \<turnstile> (_0_) -(λs. interpret b s = Some false)⇣\<surd>-> (_1_)"
      by(rule WCFG_WhileFalse)
    moreover
    have "transfer (λs. interpret b s = Some false)⇣\<surd> s = s" by simp
    ultimately show ?case by auto
  next
    case (StepRecSeq1 prog c s l c' s' l' c⇣2)
    from `∃et. prog \<turnstile> (_ l _) -et-> (_ l' _) ∧ transfer et s = s' ∧ pred et s`
    obtain et where "prog \<turnstile> (_ l _) -et-> (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from `prog \<turnstile> (_ l _) -et-> (_ l' _)` have "prog;;c⇣2 \<turnstile> (_ l _) -et-> (_ l' _)"
      by(fastforce intro:WCFG_SeqFirst)
    ultimately show ?case by blast
  next
    case (StepRecSeq2 prog c s l c' s' l' c⇣1)
    from `∃et. prog \<turnstile> (_ l _) -et-> (_ l' _) ∧ transfer et s = s' ∧ pred et s`
    obtain et where "prog \<turnstile> (_ l _) -et-> (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from `prog \<turnstile> (_ l _) -et-> (_ l' _)` 
    have "c⇣1;;prog \<turnstile> (_ l _) ⊕ #:c⇣1 -et-> (_ l' _) ⊕ #:c⇣1"
      by(fastforce intro:WCFG_SeqSecond)
    ultimately show ?case by simp blast
  next
    case (StepRecCond1 prog c s l c' s' l' b c⇣2)
    from `∃et. prog \<turnstile> (_ l _) -et-> (_ l' _) ∧ transfer et s = s' ∧ pred et s`
    obtain et where "prog \<turnstile> (_ l _) -et-> (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from `prog \<turnstile> (_ l _) -et-> (_ l' _)` 
    have "if (b) prog else c⇣2 \<turnstile> (_ 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 c⇣1)
    from `∃et. prog \<turnstile> (_ l _) -et-> (_ l' _) ∧ transfer et s = s' ∧ pred et s`
    obtain et where "prog \<turnstile> (_ l _) -et-> (_ l' _)" 
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    from `prog \<turnstile> (_ l _) -et-> (_ l' _)`
    have "if (b) c⇣1 else prog \<turnstile> (_ l _) ⊕ (#:c⇣1 + 1) -et-> (_ l' _) ⊕ (#:c⇣1 + 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 \<turnstile> (_ l _) -et-> (_ l' _) ∧ transfer et s = s' ∧ pred et s`
    obtain et where "cx \<turnstile> (_ l _) -et-> (_ l' _)"
      and "transfer et s = s'" and "pred et s" by blast
    moreover
    hence "while (b) cx \<turnstile> (_ 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 \<turnstile> (_ l _) -et-> (_ l' _)"} with @{term transfers} 
  and @{term preds} to\\
  @{term "prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"} *}

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

lemma WCFG_edge_Exit_Skip:
  "[|prog \<turnstile> n -et-> (_Exit_); n ≠ (_Entry_)|]
  ==> ∃l. n = (_ l _) ∧ labels prog l Skip ∧ et = \<Up>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 c⇣2 n et n' c⇣1)
  note IH = `[|n' = (_Exit_); n ≠ (_Entry_)|] 
    ==> ∃l. n = (_ l _) ∧ labels c⇣2 l Skip ∧ et = \<Up>id`
  from `n' ⊕ #:c⇣1 = (_Exit_)` have "n' = (_Exit_)" by(cases n') auto
  from IH[OF this `n ≠ (_Entry_)`] obtain l where [simp]:"n = (_ l _)" "et = \<Up>id"
    and "labels c⇣2 l Skip" by blast
  hence "labels (c⇣1;;c⇣2) (l + #:c⇣1) Skip" by(fastforce intro:Labels_Seq2)
  thus ?case by(fastforce simp:id_def)
next
  case (WCFG_CondThen c⇣1 n et n' b c⇣2)
  note IH = `[|n' = (_Exit_); n ≠ (_Entry_)|]
    ==> ∃l. n = (_ l _) ∧ labels c⇣1 l Skip ∧ et = \<Up>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 = \<Up>id"
    and "labels c⇣1 l Skip" by blast
  hence "labels (if (b) c⇣1 else c⇣2) (l + 1) Skip"
    by(fastforce intro:Labels_CondTrue)
  thus ?case by(fastforce simp:id_def)
next
  case (WCFG_CondElse c⇣2 n et n' b c⇣1)
  note IH = `[|n' = (_Exit_); n ≠ (_Entry_)|]
    ==> ∃l. n = (_ l _) ∧ labels c⇣2 l Skip ∧ et = \<Up>id`
  from `n' ⊕ #:c⇣1 + 1 = (_Exit_)` have "n' = (_Exit_)" by(cases n') auto
  from IH[OF this `n ≠ (_Entry_)`] obtain l where [simp]:"n = (_ l _)" "et = \<Up>id"
    and label:"labels c⇣2 l Skip" by blast
  hence "labels (if (b) c⇣1 else c⇣2) (l + #:c⇣1 + 1) Skip"
    by(fastforce intro:Labels_CondFalse)
  thus ?case by(fastforce simp:nat_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 \<turnstile> (_ l _) -et-> (_ l' _); transfer et s = s'; pred et s|]
  ==> ∃c c'. prog \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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 \<Up>λ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 c⇣1 et c⇣2)
  note IH = `[|transfer et s = s'; pred et s|]
    ==> ∃c c'. c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣1 l c ∧ labels c⇣1 l' c'`
  from IH[OF `transfer et s = s'` `pred et s`]
  obtain c c' where "c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    and "labels c⇣1 l c" 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)
  moreover 
  from `labels c⇣1 l c` have "labels (c⇣1;;c⇣2) l (c;;c⇣2)"
    by(fastforce intro:Labels_Seq1)
  moreover 
  from `labels c⇣1 l' c'` have "labels (c⇣1;;c⇣2) l' (c';;c⇣2)"
    by(fastforce intro:Labels_Seq1)
  ultimately show ?case by blast
next
  case (WCFG_SeqConnect c⇣1 et c⇣2)
  from `c⇣1 \<turnstile> (_ l _) -et-> (_Exit_)`
  have "labels c⇣1 l Skip" and [simp]:"et = \<Up>id"
    by(auto dest:WCFG_edge_Exit_Skip)
  from `transfer et s = s'` have [simp]:"s' = s" by simp
  have "labels c⇣2 0 c⇣2" by(fastforce intro:Labels_Base)
  hence "labels (c⇣1;;c⇣2) #:c⇣1 c⇣2" by(fastforce dest:Labels_Seq2)
  moreover
  from `labels c⇣1 l Skip` have "labels (c⇣1;;c⇣2) l (Skip;;c⇣2)"
    by(fastforce intro:Labels_Seq1)
  moreover
  from `labels c⇣1 l Skip` have "l < #:c⇣1" by(rule label_less_num_inner_nodes)
  ultimately 
  have "c⇣1;;c⇣2 \<turnstile> ⟨Skip;;c⇣2,s,l⟩ \<leadsto> ⟨c⇣2,s,#:c⇣1⟩" by -(rule StepSeq)
  with `labels (c⇣1;;c⇣2) l (Skip;;c⇣2)`
    `labels (c⇣1;;c⇣2) #:c⇣1 c⇣2` `(_0_) ⊕ #:c⇣1 = (_ l' _)` show ?case by simp blast
next
  case (WCFG_SeqSecond c⇣2 n et n' c⇣1)
  note IH = `!!l l'. [|n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s|]
    ==> ∃c c'. c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣2 l c ∧ labels c⇣2 l' c'`
  from `n ⊕ #:c⇣1 = (_ l _)` obtain lx where "n = (_ lx _)" 
    and [simp]:"l = lx + #:c⇣1"
    by(cases n) auto
  from `n' ⊕ #:c⇣1 = (_ l' _)` obtain lx' where "n' = (_ lx' _)" 
    and [simp]:"l' = lx' + #:c⇣1"
    by(cases n') auto
  from IH[OF `n = (_ lx _)` `n' = (_ lx' _)` `transfer et s = s'` `pred et s`]
  obtain c c' where "c⇣2 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩"
    and "labels c⇣2 lx c" and "labels c⇣2 lx' c'" by blast
  from `c⇣2 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩` have "c⇣1;;c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    by(fastforce intro:StepRecSeq2)
  moreover 
  from `labels c⇣2 lx c` have "labels (c⇣1;;c⇣2) l c" by(fastforce intro:Labels_Seq2)
  moreover 
  from `labels c⇣2 lx' c'` have "labels (c⇣1;;c⇣2) l' c'" by(fastforce intro:Labels_Seq2)
  ultimately show ?case by blast
next
  case (WCFG_CondTrue b c⇣1 c⇣2)
  from `(_0_) ⊕ 1 = (_ l' _)` have [simp]:"l' = 1" by simp
  from `transfer (λs. interpret b s = Some true)⇣\<surd> s = s'` have [simp]:"s' = s" by simp
  have "labels (if (b) c⇣1 else c⇣2) 0 (if (b) c⇣1 else c⇣2)"
    by(fastforce intro:Labels_Base)
  have "labels c⇣1 0 c⇣1" by(fastforce intro:Labels_Base)
  hence "labels (if (b) c⇣1 else c⇣2) 1 c⇣1" by(fastforce dest:Labels_CondTrue)
  from `pred (λs. interpret b s = Some true)⇣\<surd> s`
  have "interpret b s = Some true" by simp
  hence "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)
  with  `labels (if (b) c⇣1 else c⇣2) 0 (if (b) c⇣1 else c⇣2)`
    `labels (if (b) c⇣1 else c⇣2) 1 c⇣1` show ?case by simp blast
next
  case (WCFG_CondFalse b c⇣1 c⇣2)
  from `(_0_) ⊕ #:c⇣1 + 1 = (_ l' _)` have [simp]:"l' = #:c⇣1 + 1" by simp
  from `transfer (λs. interpret b s = Some false)⇣\<surd> s = s'` have [simp]:"s' = s"
    by simp
  have "labels (if (b) c⇣1 else c⇣2) 0 (if (b) c⇣1 else c⇣2)"
    by(fastforce intro:Labels_Base)
  have "labels c⇣2 0 c⇣2" by(fastforce intro:Labels_Base)
  hence "labels (if (b) c⇣1 else c⇣2) (#:c⇣1 + 1) c⇣2" by(fastforce dest:Labels_CondFalse)
  from `pred (λs. interpret b s = Some false)⇣\<surd> s`
  have "interpret b s = Some false" by simp
  hence "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)
  with `labels (if (b) c⇣1 else c⇣2) 0 (if (b) c⇣1 else c⇣2)`
    `labels (if (b) c⇣1 else c⇣2) (#:c⇣1 + 1) c⇣2` show ?case by simp blast
next
  case (WCFG_CondThen c⇣1 n et n' b c⇣2)
  note IH = `!!l l'. [|n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s|]
    ==> ∃c c'. c⇣1 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣1 l c ∧ labels c⇣1 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 "c⇣1 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩"
    and "labels c⇣1 lx c" and "labels c⇣1 lx' c'" by blast
  from `c⇣1 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩` have "if (b) c⇣1 else c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    by(fastforce intro:StepRecCond1)
  moreover 
  from `labels c⇣1 lx c` have "labels (if (b) c⇣1 else c⇣2) l c"
    by(fastforce intro:Labels_CondTrue)
  moreover 
  from `labels c⇣1 lx' c'` have "labels (if (b) c⇣1 else c⇣2) l' c'"
    by(fastforce intro:Labels_CondTrue)
  ultimately show ?case by blast
next
  case (WCFG_CondElse c⇣2 n et n' b c⇣1)
  note IH = `!!l l'. [|n = (_ l _); n' = (_ l' _); transfer et s = s'; pred et s|]
    ==> ∃c c'. c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩ ∧ labels c⇣2 l c ∧ labels c⇣2 l' c'`
  from `n ⊕ #:c⇣1 + 1 = (_ l _)` obtain lx where "n = (_ lx _)" 
    and [simp]:"l = lx + #:c⇣1 + 1"
    by(cases n) auto
  from `n' ⊕ #:c⇣1 + 1 = (_ l' _)` obtain lx' where "n' = (_ lx' _)" 
    and [simp]:"l' = lx' + #:c⇣1 + 1"
    by(cases n') auto
  from IH[OF `n = (_ lx _)` `n' = (_ lx' _)` `transfer et s = s'` `pred et s`]
  obtain c c' where "c⇣2 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩"
    and "labels c⇣2 lx c" and "labels c⇣2 lx' c'" by blast
  from `c⇣2 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩` have "if (b) c⇣1 else c⇣2 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨c',s',l'⟩"
    by(fastforce intro:StepRecCond2)
  moreover 
  from `labels c⇣2 lx c` have "labels (if (b) c⇣1 else c⇣2) l c"
    by(fastforce intro:Labels_CondFalse)
  moreover 
  from `labels c⇣2 lx' c'` have "labels (if (b) c⇣1 else c⇣2) 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)⇣\<surd> 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)⇣\<surd> s` have "interpret b s = Some true" by simp
  hence "while (b) cx \<turnstile> ⟨while (b) cx,s,0⟩ \<leadsto> ⟨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)⇣\<surd> 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)⇣\<surd> s` have "interpret b s = Some false"
    by simp
  hence "while (b) cx \<turnstile> ⟨while (b) cx,s,0⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,l⟩ \<leadsto> ⟨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 \<turnstile> ⟨c,s,lx⟩ \<leadsto> ⟨c',s',lx'⟩"
    and "labels cx lx c" and "labels cx lx' c'" by blast
  hence "while (b) cx \<turnstile> ⟨c;;while (b) cx,s,l⟩ \<leadsto> ⟨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 \<turnstile> n -et-> (_Exit_)` have "labels cx lx Skip" and [simp]:"et = \<Up>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 \<turnstile> ⟨Skip;;while (b) cx,s,l⟩ \<leadsto> ⟨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