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