Theory Timed_Automata.Approx_Beta

theory Approx_Beta
  imports DBM_Zone_Semantics Regions_Beta Closure
begin

no_notation infinity ()

chapter ‹Correctness of β›-approximation from α›-regions›

text ‹Merging the locales for the two types of regions›

locale Regions_defs =
  Alpha_defs X for X :: "'c set"+
  fixes v :: "'c  nat" and n :: nat
begin

abbreviation vabstr :: "('c, t) zone  _  _" where
  "vabstr S M  S = [M]⇘v,n ( in.  jn. M i j    get_const (M i j)  )"

definition "V'  {Z. Z  V  ( M. vabstr Z M)}"

end

locale Regions_global =
  Regions_defs X v n for X :: "'c set" and v n +
  fixes k :: "'c  nat" and not_in_X
  assumes finite: "finite X"
  assumes clock_numbering: "clock_numbering' v n" "kn. k > 0  (c  X. v c = k)"
                           " c  X. v c  n"
  assumes not_in_X: "not_in_X  X"
  assumes non_empty: "X  {}"
begin

definition ℛ_def:  "  {Regions.region X I r | I r. Regions.valid_region X k I r}"

sublocale alpha_interp:
  AlphaClosure_global X k  by (unfold_locales) (auto simp: finite ℛ_def V_def)

sublocale beta_interp: Beta_Regions' X k v n not_in_X
  rewrites "beta_interp.V = V"
  using finite non_empty clock_numbering not_in_X unfolding V_def
  by - ((subst Beta_Regions.V_def)?, unfold_locales; (assumption | rule HOL.refl))+

abbreviation β where "β  beta_interp.ℛ"

lemmas β_def = beta_interp.ℛ_def

abbreviation "Approxβ  beta_interp.Approxβ"

section ‹Preparing Bouyer's Theorem›

lemma region_dbm:
  assumes "R  "
  defines "v'  λ i. THE c. c  X  v c = i"
  obtains M
  where"[M]⇘v,n= R"
  and " i  n.  j  n. M i 0 =   j > 0  i  j M i j =   M j i = "
  and " i  n. M i i = Le 0"
  and " i  n.  j  n. i > 0  j > 0  M i 0    M j 0    ( d :: int.
        (- k (v' j)  d  d  k (v' i)  M i j = Le d  M j i = Le (-d))
       (- k (v' j)  d - 1  d  k (v' i)  M i j = Lt d  M j i = Lt (-d + 1)))"
  and " i  n. i > 0  M i 0   
        ( d :: int. d  k (v' i)  d  0
           (M i 0 = Le d  M 0 i = Le (-d)  M i 0 = Lt d  M 0 i = Lt (-d + 1)))"
  and " i  n. i > 0  ( d :: int. - k (v' i)  d  d  0  (M 0 i = Le d  M 0 i = Lt d))"
  and " i.  j. M i j    get_const (M i j)  "
  and " i  n.  j  n. M i j    i > 0  j > 0 
      ( d:: int. (M i j = Le d  M i j = Lt d)  (- k (v' j))  d  d  k (v' i))"
proof -
  from assms obtain I r where R: "R = region X I r" "valid_region X k I r" unfolding ℛ_def by blast
  let ?X0 = "{x  X. d. I x = Regions.intv.Intv d}"
  define f where "f 
  λ x. if isIntv (I x) then Lt (real (intv_const (I x) + 1))
       else if isConst (I x) then Le (real (intv_const (I x)))
       else "
  define g where "g 
  λ x. if isIntv (I x) then Lt (- real (intv_const (I x)))
       else if isConst (I x) then Le (- real (intv_const (I x)))
       else Lt (- real (k x))"
  define h where "h 
  λ x y. if isIntv (I x)  isIntv (I y) then
      if (y, x)  r  (x, y)  r then Lt (real_of_int (int (intv_const (I x)) - intv_const (I y) + 1))
      else if (x, y)  r  (y, x)  r then Lt (int (intv_const (I x)) - intv_const (I y))
      else Le (int (intv_const (I x)) - intv_const (I y))
   else if isConst (I x)  isConst (I y) then Le (int (intv_const (I x)) - intv_const (I y))
   else if isIntv (I x)  isConst (I y) then Lt (int (intv_const (I x)) + 1 - intv_const (I y))
   else if isConst (I x)  isIntv (I y) then Lt (int (intv_const (I x)) - intv_const (I y))
   else "
  let ?M = "λ i j. if i = 0 then if j = 0 then Le 0 else g (v' j)
                   else if j = 0 then f (v' i) else if i = j then Le 0 else h (v' i) (v' j)"
  have "[?M]⇘v,n R"
  proof
    fix u assume u: "u  [?M]⇘v,n⇙"
    show "u  R" unfolding R
    proof (standard, goal_cases)
      case 1
      show ?case
      proof
        fix c assume c: "c  X"
        with clock_numbering have c2: "v c  n" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
        with u have "dbm_entry_val u None (Some c) (g c)"
        unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
        then show "0  u c" by (cases "isIntv (I c)"; cases "isConst (I c)") (auto simp: g_def)
      qed
    next
      case 2
      show ?case
      proof
        fix c assume c: "c  X"
        with clock_numbering have c2: "v c  n" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
        with u have *: "dbm_entry_val u None (Some c) (g c)" "dbm_entry_val u (Some c) None (f c)"
        unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
        show "intv_elem c u (I c)"
        proof (cases "I c")
          case (Const d)
          then have "¬ isIntv (I c)" "isConst (I c)" by auto
          with * Const show ?thesis unfolding g_def f_def using Const by auto
        next
          case (Intv d)
          then have "isIntv (I c)" "¬ isConst (I c)" by auto
          with * Intv show ?thesis unfolding g_def f_def by auto
        next
          case (Greater d)
          then have "¬ isIntv (I c)" "¬ isConst (I c)" by auto
          with * Greater R(2) c show ?thesis unfolding g_def f_def by fastforce
        qed
      qed
    next
      show "?X0 = ?X0" ..
      show "x  ?X0.  y  ?X0. (x, y)  r  frac (u x)  frac (u y)"
      proof (standard, standard)
        fix x y assume A: "x  ?X0" "y  ?X0"
        show "(x, y)  r  frac (u x)  frac (u y)"
        proof (cases "x = y")
          case True
          have "refl_on ?X0 r" using R(2) by auto
          with A True show ?thesis unfolding refl_on_def by auto
        next
          case False
          from A obtain d d' where AA:
            "I x = Intv d" "I y = Intv d'" "isIntv (I x)" "isIntv (I y)" "¬ isConst (I x)" "¬ isConst (I y)"
          by auto
          from A False clock_numbering have B:
            "v x  n" "v x > 0" "v' (v x) = x" "v y  n" "v y > 0" "v' (v y) = y" "v x  v y"
          unfolding v'_def by auto
          with u have *:
            "dbm_entry_val u (Some x) (Some y) (h x y)" "dbm_entry_val u (Some y) (Some x) (h y x)"
            "dbm_entry_val u None (Some x) (g x)" "dbm_entry_val u (Some x) None (f x)"
            "dbm_entry_val u None (Some y) (g y)" "dbm_entry_val u (Some y) None (f y)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by force+
          show "(x, y)  r  frac (u x)  frac (u y)"
          proof
            assume C: "(x, y)  r"
            show "frac (u x)  frac (u y)"
            proof (cases "(y, x)  r")
              case False
              with * AA C have **:
                "u x - u y < int d - d'"
                "d < u x" "u x < d + 1" "d' < u y" "u y < d' + 1"
              unfolding f_def g_def h_def by auto
              from nat_intv_frac_decomp[OF **(2,3)] nat_intv_frac_decomp[OF **(4,5)] **(1) show
                "frac (u x)  frac (u y)"
              by simp
            next
              case True
              with * AA C have **:
                "u x - u y  int d - d'"
                "d < u x" "u x < d + 1" "d' < u y" "u y < d' + 1"
              unfolding f_def g_def h_def by auto
              from nat_intv_frac_decomp[OF **(2,3)] nat_intv_frac_decomp[OF **(4,5)] **(1) show
                "frac (u x)  frac (u y)"
              by simp
            qed
          next
            assume "frac (u x)  frac (u y)"
            show "(x, y)  r"
            proof (rule ccontr)
              assume C: "(x,y)  r"
              moreover from R(2) have "total_on ?X0 r" by auto
              ultimately have "(y, x)  r" using False A unfolding total_on_def by auto
              with *(2-) AA C have **:
                "u y - u x < int d' - d"
                "d < u x" "u x < d + 1" "d' < u y" "u y < d' + 1"
              unfolding f_def g_def h_def by auto
              from nat_intv_frac_decomp[OF **(2,3)] nat_intv_frac_decomp[OF **(4,5)] **(1) have
                "frac (u y) < frac (u x)"
              by simp
              with frac _  _ show False by auto
            qed
          qed
        qed
      qed
    qed
  qed
  moreover have "R  [?M]⇘v,n⇙"
  proof
    fix u assume u: "u  R"
    show "u  [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
    proof (safe, goal_cases)
      case 1 then show ?case by auto
    next
      case (2 c)
      with clock_numbering have "c  X" by metis
      with clock_numbering have *: "c  X" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
      with R u have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
      then have "dbm_entry_val u None (Some c) (g c)" unfolding g_def by (cases "I c") auto
      with * show ?case by auto
    next
      case (3 c)
      with clock_numbering have "c  X" by metis
      with clock_numbering have *: "c  X" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
      with R u have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
      then have "dbm_entry_val u (Some c) None (f c)" unfolding f_def by (cases "I c") auto
      with * show ?case by auto
    next
      case (4 c1 c2)
      with clock_numbering have "c1  X" "c2  X" by metis+
      with clock_numbering have *:
        "c1  X" "v c1 > 0" "v' (v c1) = c1" "c2  X" "v c2 > 0" "v' (v c2) = c2"
      unfolding v'_def by auto
      with R u have
        "intv_elem c1 u (I c1)" "valid_intv (k c1) (I c1)"
        "intv_elem c2 u (I c2)" "valid_intv (k c2) (I c2)"
      by auto
      then have "dbm_entry_val u (Some c1) (Some c2) (h c1 c2)" unfolding h_def
      proof(cases "I c1", cases "I c2", fastforce+, cases "I c2", fastforce, goal_cases)
      case (1 d d')
        then show ?case
        proof (cases "(c2, c1)  r", goal_cases)
          case 1
          show ?case
          proof (cases "(c1, c2)  r")
            case True
            with 1 *(1,4) R(1) u have "frac (u c1) = frac (u c2)" by auto
            with 1 have "u c1 - u c2 = real d - d'" by (fastforce dest: nat_intv_frac_decomp)
            with 1 show ?thesis by auto
          next
            case False with 1 show ?thesis by auto
          qed
        next
          case 2
          show ?case
          proof (cases "c1 = c2")
            case True then show ?thesis by auto
          next
            case False
            with 2 R(2) *(1,4) have "(c1, c2)  r" by (fastforce simp: total_on_def)
            with 2 *(1,4) R(1) u have "frac (u c1) < frac (u c2)" by auto
            with 2 have "u c1 - u c2 < real d - d'" by (fastforce dest: nat_intv_frac_decomp)
            with 2 show ?thesis by auto
          qed
        qed
      qed fastforce+
      then show ?case
      proof (cases "v c1 = v c2", goal_cases)
        case True with * clock_numbering have "c1 = c2" by auto
        then show ?thesis by auto
      next
        case 2 with * show ?case by auto
      qed
    qed
  qed
  ultimately have "[?M]⇘v,n= R" by blast
  moreover have " i  n.  j  n. ?M i 0 =   j > 0  i  j  ?M i j =   ?M j i = "
  unfolding f_def h_def by auto
  moreover have " i  n. ?M i i = Le 0" by auto
  moreover
  { fix i j assume A: "i  n" "j  n" "i > 0" "j > 0" "?M i 0  " "?M j 0  "
    with clock_numbering(2) obtain c1 c2 where B: "v c1 = i" "v c2 = j" "c1  X" "c2  X" by meson
    with clock_numbering(1) A have C: "v' i = c1" "v' j = c2" unfolding v'_def by force+
    from R(2) B have valid: "valid_intv (k c1) (I c1)" "valid_intv (k c2) (I c2)" by auto
    have " d :: int. (- k (v' j)  d  d  k (v' i)  ?M i j = Le d  ?M j i = Le (-d)
       (- k (v' j)  d - 1  d  k (v' i)  ?M i j = Lt d  ?M j i = Lt (-d + 1)))"
    proof (cases "i = j")
      case True
      then show ?thesis by auto
    next
      case False
      then show ?thesis
      proof (cases "I c1", goal_cases)
        case 1
        then show ?case
        proof (cases "I c2")
          case Const
          let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
          from Const 1 have "isConst (I c1)" "isConst (I c2)" by auto
          with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
        next
          case Intv
          let ?d = "int(intv_const (I c1)) - int (intv_const (I c2))"
          from Intv 1 have "isConst (I c1)" "isIntv (I c2)" by auto
          with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
        next
          case Greater
          then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
          with A 1(1) C have False unfolding f_def by simp
          then show ?thesis by fast
        qed
      next
        case 2
        then show ?case
        proof (cases "I c2")
          case Const
          let ?d = "int (intv_const (I c1)) + 1 - int (intv_const (I c2))"
          from Const 2 have "isIntv (I c1)" "isConst (I c2)" by auto
          with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
        next
          case Intv
          with 2 have *: "isIntv (I c1)" "isIntv (I c2)" by auto
          from Intv A(1-4) C show ?thesis apply simp
          proof (standard, goal_cases)
            case 1
            show ?case
            proof (cases "(c2, c1)  r")
              case True
              note T = this
              show ?thesis
              proof (cases "(c1, c2)  r")
                case True
                let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
                from True T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
              next
                case False
                let ?d = "int (intv_const (I c1)) - int (intv_const (I c2)) + 1"
                from False T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
              qed
            next
              case False
              let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
              from False * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
            qed
          qed
        next
          case Greater
          then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
          with A 2(1) C have False unfolding f_def by simp
          then show ?thesis by fast
        qed
      next
        case 3
        then have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
        with A 3(1) C have False unfolding f_def by simp
        then show ?thesis by fast
      qed
    qed
  }
  moreover
  { fix i assume A: "i  n" "i > 0" "?M i 0  "
    with clock_numbering(2) obtain c1 where B: "v c1 = i" "c1  X" by meson
    with clock_numbering(1) A have C: "v' i = c1" unfolding v'_def by force+
    from R(2) B have valid: "valid_intv (k c1) (I c1)" by auto
    have " d :: int. d  k (v' i)  d  0
       (?M i 0 = Le d  ?M 0 i = Le (-d)  ?M i 0 = Lt d  ?M 0 i = Lt (-d + 1))"
    proof (cases "i = 0")
      case True
      then show ?thesis by auto
    next
      case False
      then show ?thesis
      proof (cases "I c1", goal_cases)
        case 1
        let ?d = "int (intv_const (I c1))"
        from 1 have "isConst (I c1)" "¬ isIntv (I c1)" by auto
        with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
      next
        case 2
        let ?d = "int (intv_const (I c1)) + 1"
        from 2 have "isIntv(I c1)" "¬ isConst (I c1)" by auto
        with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
      next
        case 3
        then have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
        with A 3(1) C have False unfolding f_def by simp
        then show ?thesis by fast
      qed
    qed
  }
  moreover
  { fix i assume A: "i  n" "i > 0"
    with clock_numbering(2) obtain c1 where B: "v c1 = i" "c1  X" by meson
    with clock_numbering(1) A have C: "v' i = c1" unfolding v'_def by force+
    from R(2) B have valid: "valid_intv (k c1) (I c1)" by auto
    have " d :: int. - k (v' i)  d  d  0  (?M 0 i = Le d  ?M 0 i = Lt d)"
    proof (cases "i = 0")
      case True
      then show ?thesis by auto
    next
      case False
      then show ?thesis
      proof (cases "I c1", goal_cases)
        case 1
        let ?d = "- int (intv_const (I c1))"
        from 1 have "isConst (I c1)" "¬ isIntv (I c1)" by auto
        with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
      next
        case 2
        let ?d = "- int (intv_const (I c1))"
        from 2 have "isIntv(I c1)" "¬ isConst (I c1)" by auto
        with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
      next
        case 3
        let ?d = "- (k c1)"
        from 3 have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
        with A C show ?thesis unfolding g_def by (intro exI[where x = ?d]) auto
      qed
    qed
  }
  moreover have " i.  j. ?M i j    get_const (?M i j)  " unfolding f_def g_def h_def by auto
  moreover have " i  n.  j  n. i > 0  j > 0  ?M i j  
     ( d:: int. (?M i j = Le d  ?M i j = Lt d)  (- k (v' j))  d  d  k (v' i))"
  proof (auto, goal_cases)
    case A: (1 i j)
    with clock_numbering(2) obtain c1 c2 where B: "v c1 = i" "c1  X" "v c2 = j" "c2  X" by meson
    with clock_numbering(1) A have C: "v' i = c1" "v' j = c2" unfolding v'_def by force+
    from R(2) B have valid: "valid_intv (k c1) (I c1)" "valid_intv (k c2) (I c2)" by auto
    with A B C show ?case
    proof (simp, goal_cases)
      case 1
      show ?case
      proof (cases "I c1", goal_cases)
        case 1
        then show ?case
        proof (cases "I c2")
          case Const
          let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
          from Const 1 have "isConst (I c1)" "isConst (I c2)" by auto
          with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
        next
          case Intv
          let ?d = "int(intv_const (I c1)) - int (intv_const (I c2))"
          from Intv 1 have "isConst (I c1)" "isIntv (I c2)" by auto
          with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
        next
          case Greater
          then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
          with A 1(1) C show ?thesis unfolding h_def by simp
        qed
      next
        case 2
        then show ?case
        proof (cases "I c2")
          case Const
          let ?d = "int (intv_const (I c1)) + 1 - int (intv_const (I c2))"
          from Const 2 have "isIntv (I c1)" "isConst (I c2)" by auto
          with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
        next
          case Intv
          with 2 have *: "isIntv (I c1)" "isIntv (I c2)" by auto
          from Intv A(1-4) C show ?thesis
          proof goal_cases
            case 1
            show ?case
            proof (cases "(c2, c1)  r")
              case True
              note T = this
              show ?thesis
              proof (cases "(c1, c2)  r")
                case True
                let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
                from True T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
              next
                case False
                let ?d = "int (intv_const (I c1)) - int (intv_const (I c2)) + 1"
                from False T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
              qed
            next
              case False
              let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
              from False * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
            qed
          qed
        next
          case Greater
          then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
          with A 2(1) C show ?thesis unfolding h_def by simp
        qed
      next
        case 3
        then have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
        with A 3(1) C show ?thesis unfolding h_def by simp
      qed
    qed
  qed
  moreover show ?thesis
    apply (rule that)
           apply (rule calculation(1))
          apply (rule calculation(2))
         apply (rule calculation(3))
        apply (blast intro: calculation)+
     apply (rule calculation(7))
    using calculation(8) apply blast
  done
qed

lemma len_inf_elem:
  "(a, b)  set (arcs i j xs)  M a b =   len M i j xs = "
apply (induction rule: arcs.induct)
  apply (auto simp: add)
  apply (rename_tac a' b' x xs)
  apply (case_tac "M a' x")
by auto

lemma zone_diag_lt:
  assumes "a  n" "b  n" and C: "v c1 = a" "v c2 = b" and not0: "a > 0" "b > 0"
  shows "[(λ i j. if i = a  j = b then Lt d else )]⇘v,n= {u. u c1 - u c2 < d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (standard, goal_cases)
  case 1
  then show ?case using a  n b  n C by fastforce
next
  case 2
  then show ?case
  proof (safe, goal_cases)
    case 1 from not0 show ?case unfolding dbm_le_def by auto
  next
    case 2 with not0 show ?case by auto
  next
    case 3 with not0 show ?case by auto
  next
    case (4 u' y z)
    show ?case
    proof (cases "v y = a  v z = b")
      case True
      with 4 clock_numbering C a  n b  n have "u' y - u' z < d" by metis
      with True show ?thesis by auto
    next
      case False then show ?thesis by auto
    qed
  qed
qed

lemma zone_diag_le:
  assumes "a  n" "b  n" and C: "v c1 = a" "v c2 = b" and not0: "a > 0" "b > 0"
  shows "[(λ i j. if i = a  j = b then Le d else )]⇘v,n= {u. u c1 - u c2  d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
  case 1
  then show ?case using a  n b  n C by fastforce
next
  case 2
  then show ?case
  proof (safe, goal_cases)
    case 1 from not0 show ?case unfolding dbm_le_def by auto
  next
    case 2 with not0 show ?case by auto
  next
    case 3 with not0 show ?case by auto
  next
    case (4 u' y z)
    show ?case
    proof (cases "v y = a  v z = b")
      case True
      with 4 clock_numbering C a  n b  n have "u' y - u' z  d" by metis
      with True show ?thesis by auto
    next
      case False then show ?thesis by auto
    qed
  qed
qed

lemma zone_diag_lt_2:
  assumes "a  n" and C: "v c = a" and not0: "a > 0"
  shows "[(λ i j. if i = a  j = 0 then Lt d else )]⇘v,n= {u. u c < d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
  case 1
  then show ?case using a  n C by fastforce
next
  case 2
  then show ?case
  proof (safe, goal_cases)
    case 1 from not0 show ?case unfolding dbm_le_def by auto
  next
    case 2 with not0 show ?case by auto
  next
    case (3 u c)
    show ?case
    proof (cases "v c = a")
      case False then show ?thesis by auto
    next
      case True
      with 3 clock_numbering C a  n have "u c < d" by metis
      with C show ?thesis by auto
    qed
  next
    case (4 u' y z)
    from clock_numbering(1) have "0 < v z" by auto
    then show ?case by auto
  qed
qed

lemma zone_diag_le_2:
  assumes "a  n" and C: "v c = a" and not0: "a > 0"
  shows "[(λ i j. if i = a  j = 0 then Le d else )]⇘v,n= {u. u c  d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
  case 1
  then show ?case using a  n C by fastforce
next
  case 2
  then show ?case
  proof (safe, goal_cases)
    case 1 from not0 show ?case unfolding dbm_le_def by auto
  next
    case 2 with not0 show ?case by auto
  next
    case (3 u c)
    show ?case
    proof (cases "v c = a")
      case False then show ?thesis by auto
    next
      case True
      with 3 clock_numbering C a  n have "u c  d" by metis
      with C show ?thesis by auto
    qed
  next
    case (4 u' y z)
    from clock_numbering(1) have "0 < v z" by auto
    then show ?case by auto
  qed
qed

lemma zone_diag_lt_3:
  assumes "a  n" and C: "v c = a" and not0: "a > 0"
  shows "[(λ i j. if i = 0  j = a then Lt d else )]⇘v,n= {u. - u c < d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
  case 1
  then show ?case using a  n C by fastforce
next
  case 2
  then show ?case
  proof (safe, goal_cases)
    case 1 from not0 show ?case unfolding dbm_le_def by auto
  next
    case (2 u c)
    show ?case
    proof (cases "v c = a", goal_cases)
      case False then show ?thesis by auto
    next
      case True
      with 2 clock_numbering C a  n have "- u c < d" by metis
      with C show ?thesis by auto
    qed
  next
    case (3 u) with not0 show ?case by auto
  next
    case (4 u' y z)
    from clock_numbering(1) have "0 < v y" by auto
    then show ?case by auto
  qed
qed

lemma len_int_closed:
  " i j. (M i j :: real)    len M i j xs  "
by (induction xs arbitrary: i) auto

lemma get_const_distr:
  "a    b    get_const (a + b) = get_const a + get_const b"
by (cases a) (cases b, auto simp: add)+

lemma len_int_dbm_closed:
  " (i, j)  set (arcs i j xs). (get_const (M i j) :: real)    M i j  
   get_const (len M i j xs)    len M i j xs  "
by (induction xs arbitrary: i) (auto simp: get_const_distr, simp add: dbm_add_not_inf add)

lemma zone_diag_le_3:
  assumes "a  n" and C: "v c = a" and not0: "a > 0"
  shows "[(λ i j. if i = 0  j = a then Le d else )]⇘v,n= {u. - u c  d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
  case 1
  then show ?case using a  n C by fastforce
next
  case 2
  then show ?case
  proof (safe, goal_cases)
    case 1 from not0 show ?case unfolding dbm_le_def by auto
  next
    case (2 u c)
    show ?case
    proof (cases "v c = a")
      case False then show ?thesis by auto
    next
      case True
      with 2 clock_numbering C a  n have "- u c  d" by metis
      with C show ?thesis by auto
    qed
  next
    case (3 u) with not0 show ?case by auto
  next
    case (4 u' y z)
    from clock_numbering(1) have "0 < v y" by auto
    then show ?case by auto
  qed
qed

lemma dbm_lt':
  assumes "[M]⇘v,n V" "M a b  Lt d" "a  n" "b  n" "v c1 = a" "v c2 = b" "a > 0" "b > 0"
  shows "[M]⇘v,n {u  V. u c1 - u c2 < d}"
proof -
  from assms have "[M]⇘v,n [(λ i j. if i = a  j = b then Lt d else )]⇘v,n⇙"
    apply safe
    apply (rule DBM_le_subset)
  unfolding less_eq dbm_le_def by auto
  moreover from zone_diag_lt[OF a  n b  n assms(5-)]
  have "[(λ i j. if i = a  j = b then Lt d else )]⇘v,n= {u. u c1 - u c2 < d}" by blast
  moreover from assms have "[M]⇘v,n V" by auto
  ultimately show ?thesis by auto
qed

lemma dbm_lt'2:
  assumes "[M]⇘v,n V" "M a 0  Lt d" "a  n" "v c1 = a" "a > 0"
  shows "[M]⇘v,n {u  V. u c1 < d}"
proof -
  from assms(2) have "[M]⇘v,n [(λ i j. if i = a  j = 0 then Lt d else )]⇘v,n⇙"
    apply safe
    apply (rule DBM_le_subset)
  unfolding less_eq dbm_le_def by auto
  moreover from zone_diag_lt_2[OF a  n assms(4,5)]
  have "[(λ i j. if i = a  j = 0 then Lt d else )]⇘v,n= {u. u c1 < d}" by blast
  ultimately show ?thesis using assms(1) by auto
qed

lemma dbm_lt'3:
  assumes "[M]⇘v,n V" "M 0 a  Lt d" "a  n" "v c1 = a" "a > 0"
  shows "[M]⇘v,n {u  V. - u c1 < d}"
proof -
  from assms(2) have "[M]⇘v,n [(λ i j. if i = 0  j = a then Lt d else )]⇘v,n⇙"
    apply safe
    apply (rule DBM_le_subset)
  unfolding less_eq dbm_le_def by auto
  moreover from zone_diag_lt_3[OF a  n assms(4,5)]
  have "[(λ i j. if i = 0  j = a then Lt d else )]⇘v,n= {u. - u c1 < d}" by blast
  ultimately show ?thesis using assms(1) by auto
qed

lemma dbm_le':
  assumes "[M]⇘v,n V" "M a b  Le d" "a  n" "b  n" "v c1 = a" "v c2 = b" "a > 0" "b > 0"
  shows "[M]⇘v,n {u  V. u c1 - u c2  d}"
proof -
  from assms have "[M]⇘v,n [(λ i j. if i = a  j = b then Le d else )]⇘v,n⇙"
    apply safe
    apply (rule DBM_le_subset)
  unfolding less_eq dbm_le_def by auto
  moreover from zone_diag_le[OF a  n b  n assms(5-)]
  have "[(λ i j. if i = a  j = b then Le d else )]⇘v,n= {u. u c1 - u c2  d}" by blast
  moreover from assms have "[M]⇘v,n V" by auto
  ultimately show ?thesis by auto
qed

lemma dbm_le'2:
  assumes "[M]⇘v,n V" "M a 0  Le d" "a  n" "v c1 = a" "a > 0"
  shows "[M]⇘v,n {u  V. u c1  d}"
proof -
  from assms(2) have "[M]⇘v,n [(λ i j. if i = a  j = 0 then Le d else )]⇘v,n⇙"
    apply safe
    apply (rule DBM_le_subset)
  unfolding less_eq dbm_le_def by auto
  moreover from zone_diag_le_2[OF a  n assms(4,5)]
  have "[(λ i j. if i = a  j = 0 then Le d else )]⇘v,n= {u. u c1  d}" by blast
  ultimately show ?thesis using assms(1) by auto
qed

lemma dbm_le'3:
  assumes "[M]⇘v,n V" "M 0 a  Le d" "a  n" "v c1 = a" "a > 0"
  shows "[M]⇘v,n {u  V. - u c1  d}"
proof -
  from assms(2) have "[M]⇘v,n [(λ i j. if i = 0  j = a then Le d else )]⇘v,n⇙"
    apply safe
    apply (rule DBM_le_subset)
  unfolding less_eq dbm_le_def by auto
  moreover from zone_diag_le_3[OF a  n assms(4,5)]
  have "[(λ i j. if i = 0  j = a then Le d else )]⇘v,n= {u. - u c1  d}" by blast
  ultimately show ?thesis using assms(1) by auto
qed

lemma int_zone_dbm:
  assumes " (_,d)  collect_clock_pairs cc. d  " " c  collect_clks cc. v c  n"
  obtains M where "{u. u  cc} = [M]⇘v,n⇙" and "dbm_int M n"
using int_zone_dbm[OF _ assms] clock_numbering(1) by auto

lemma non_empty_dbm_diag_set':
  assumes "clock_numbering' v n" "in. jn. M i j    get_const (M i j)  "
          "[M]⇘v,n {}"
  obtains M' where "[M]⇘v,n= [M']⇘v,n (in. jn. M' i j    get_const (M' i j)  )
     ( i  n. M' i i = 0)"
proof -
  let ?M = "λi j. if i = j then 0 else M i j"
  from non_empty_dbm_diag_set[OF assms(1,3)] have "[M]⇘v,n= [?M]⇘v,n⇙" by auto
  moreover from assms(2) have "in. jn. ?M i j    get_const (?M i j)  "
  unfolding neutral by auto
  moreover have " i  n. ?M i i = 0" by auto
  ultimately show ?thesis by (auto intro: that)
qed

lemma dbm_entry_int:
  "(x :: t DBMEntry)    get_const x     d :: int. x = Le d  x = Lt d"
apply (cases x) using Ints_cases by auto


section ‹Bouyer's Main Theorem›

theorem region_zone_intersect_empty_approx_correct:
  assumes "R  " "Z  V" "R  Z = {}" "vabstr Z M"
  shows "R  Approxβ Z = {}"
proof -
  define v' where "v'  λ i. THE c. c  X  v c = i"
  from region_dbm[OF assms(1)] obtain MR where MR:
    "[MR]⇘v,n= R" "in. jn. MR i 0 =   0 < j  i  j  MR i j =   MR j i = "
    "in. MR i i = Le 0"
    "in. jn. 0 < i  0 < j  MR i 0    MR j 0   
     (d. - int (k (THE c. c  X  v c = j))  d  d  int (k (THE c. c  X  v c = i))
           MR i j = Le d  MR j i = Le (real_of_int (- d))
         - int (k (THE c. c  X  v c = j))  d - 1  d  int (k (THE c. c  X  v c = i))
           MR i j = Lt d  MR j i = Lt (real_of_int (- d + 1)))"
    "in. 0 < i  MR i 0    (dint (k (THE c. c  X  v c = i)). d  0 
      (MR i 0 = Le d  MR 0 i = Le (real_of_int (- d))  MR i 0 = Lt d  MR 0 i = Lt (real_of_int (- d + 1))))"
    "in. 0 < i  (d- int (k (THE c. c  X  v c = i)). d  0  (MR 0 i = Le d  MR 0 i = Lt d))"
    "i j. MR i j    get_const (MR i j)  "
    "in. jn. MR i j    0 < i  0 < j  (d. (MR i j = Le d  MR i j = Lt d)
         - int (k (THE c. c  X  v c = j))  d  d  int (k (THE c. c  X  v c = i)))"
  .
  show ?thesis
  proof (cases "R = {}")
    case True then show ?thesis by auto
  next
    case False
    from clock_numbering(2) have cn_weak: "kn. 0 < k  ( c. v c = k)" by auto

    show ?thesis
    proof (cases "Z = {}")
      case True
      then show ?thesis using beta_interp.apx_empty by blast
    next
      case False
      from assms(4) have
        "Z = [M]⇘v,n⇙" " in.  jn. M i j    get_const (M i j)  "
      by auto
      from this(1) non_empty_dbm_diag_set'[OF clock_numbering(1) this(2)] Z  {} obtain M where M:
        "Z = [M]⇘v,n (in. jn. M i j    get_const (M i j)  )  (in. M i i = 0)"
      by auto
      with not_empty_cyc_free[OF cn_weak] False have "cyc_free M n" by auto
      then have "cycle_free M n" using cycle_free_diag_equiv by auto
      from M have "Z = [FW M n]⇘v,n⇙" unfolding neutral by (auto intro!: FW_zone_equiv[OF cn_weak])
      moreover from fw_canonical[OF cyc_free M _] M have "canonical (FW M n) n"
        unfolding neutral by auto
      moreover from FW_int_preservation M have
        "in. jn. FW M n i j    get_const (FW M n i j)  "
      by auto
      ultimately obtain M where M:
        "[M]⇘v,n= Z" "canonical M n" "in. jn. M i j    get_const (M i j)  "
      by blast
      let ?M = "λ i j. min (M i j) (MR i j)"
      from M(1) MR(1) assms have "[M]⇘v,n [MR]⇘v,n= {}" by auto
      moreover from DBM_le_subset[folded less_eq, of n ?M M] have "[?M]⇘v,n [M]⇘v,n⇙" by auto
      moreover from DBM_le_subset[folded less_eq, of n ?M MR] have "[?M]⇘v,n [MR]⇘v,n⇙" by auto
      ultimately have "[?M]⇘v,n= {}" by blast
      then have "¬ cyc_free ?M n" using cyc_free_not_empty[of n ?M v] clock_numbering(1) by auto
      then obtain i xs where xs: "i  n" "set xs  {0..n}" "len ?M i i xs < 0" by auto
      from this(1,2) canonical_shorten_rotate_neg_cycle[OF M(2) this(2,1,3)] obtain i ys where ys:
        "len ?M i i ys < 0"
        "set ys  {0..n}" "successive (λ(a, b). ?M a b = M a b) (arcs i i ys)" "i  n"
        and distinct: "distinct ys" "i  set ys"
        and cycle_closes: "ys  []  ?M i (hd ys)  M i (hd ys)  ?M (last ys) i  M (last ys) i"
      by fastforce

      have one_M_aux:
        "len ?M i j ys = len MR i j ys" if " (a,b)  set (arcs i j ys). M a b  MR a b" for j
      using that by (induction ys arbitrary: i) (auto simp: min_def)
      have one_M: " (a,b)  set (arcs i i ys). M a b < MR a b"
      proof (rule ccontr, goal_cases)
        case 1
        then have "(a, b)set (arcs i i ys). MR a b  M a b" by auto
        from one_M_aux[OF this] have "len ?M i i ys = len MR i i ys" .
        with Nil ys(1) xs(3) have "len MR i i ys < 0" by simp
        from DBM_val_bounded_neg_cycle[OF _ i  n set ys  _ this cn_weak]
        have "[MR]⇘v,n= {}" unfolding DBM_zone_repr_def by auto
        with R  {} MR(1) show False by auto
      qed
      have one_M_R_aux:
        "len ?M i j ys = len M i j ys" if " (a,b)  set (arcs i j ys). M a b  MR a b" for j
      using that by (induction ys arbitrary: i) (auto simp: min_def)
      have one_M_R: " (a,b)  set (arcs i i ys). M a b > MR a b"
      proof (rule ccontr, goal_cases)
        case 1
        then have "(a, b)set (arcs i i ys). MR a b  M a b" by auto
        from one_M_R_aux[OF this] have "len ?M i i ys = len M i i ys" .
        with Nil ys(1) xs(3) have "len M i i ys < 0" by simp
        from DBM_val_bounded_neg_cycle[OF _ i  n set ys  _ this cn_weak]
        have "[M]⇘v,n= {}" unfolding DBM_zone_repr_def by auto
        with Z  {} M(1) show False by auto
      qed

      have 0: "(0,0)  set (arcs i i ys)"
      proof (cases "ys = []")
        case False with distinct show ?thesis using arcs_distinct1 by blast
      next
        case True with ys(1) have "?M i i < 0" by auto
        then have "M i i < 0  MR i i < 0" by (simp add: min_less_iff_disj)
        from one_M one_M_R True show ?thesis by auto
      qed

      { fix a b assume A: "(a,b)  set (arcs i i ys)"
        assume not0: "a > 0"
        from aux1[OF ys(4,4,2) A] have C2: "a  n" by auto
        then obtain c1 where C: "v c1 = a" "c1  X"
        using clock_numbering(2) not0 unfolding v'_def by meson
        then have "v' a = c1" using clock_numbering C2 not0 unfolding v'_def by fastforce
        with C C2 have " c  X. v c = a  v' a = c" "a  n" by auto
      } note clock_dest_1 = this
      { fix a b assume A: "(a,b)  set (arcs i i ys)"
        assume not0: "b > 0"
        from aux1[OF ys(4,4,2) A] have C2: "b  n" by auto
        then obtain c2 where C: "v c2 = b" "c2  X"
        using clock_numbering(2) not0 unfolding v'_def by meson
        then have "v' b = c2" using clock_numbering C2 not0 unfolding v'_def by fastforce
        with C C2 have " c  X. v c = b  v' b = c" "b  n" by auto
      } note clock_dest_2 = this
      have clock_dest:
        " a b. (a,b)  set (arcs i i ys)  a > 0  b > 0 
           c1  X.  c2  X. v c1 = a  v c2 = b  v' a = c1  v' b = c2 &&& a  n &&& b  n"
      using clock_dest_1 clock_dest_2 by (auto) presburger

      { fix a assume A: "(a,0)  set (arcs i i ys)"
        assume not0: "a > 0"
        assume bounded: "MR a 0  "
        assume lt: "M a 0 < MR a 0"
        from clock_dest_1[OF A not0] obtain c1 where C:
          "v c1 = a" "c1  X" "v' a = c1" and C2: "a  n"
        by blast
        from C2 not0 bounded MR(5) obtain d :: int where *:
          "d  int (k (v' a))"
          "MR a 0 = Le d  MR 0 a = Le (- d)  MR a 0 = Lt d  MR 0 a = Lt (- d + 1)"
        unfolding v'_def by auto
        with C have **: "d  int (k c1)" by auto
        from *(2) have ?thesis
        proof (standard, goal_cases)
          case 1
          with lt have "M a 0 < Le d" by auto
          then have "M a 0  Lt d" unfolding less less_eq dbm_le_def by (fastforce elim!: dbm_lt.cases)
          from dbm_lt'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. u c1 < d}"
          by auto
          from beta_interp.β_boundedness_lt'[OF ** C(2) this, unfolded β_def] have
            "Approxβ ([M]⇘v,n)  {u  V. u c1 < d}"
          .
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c1) None (MR a 0)" "dbm_entry_val u None (Some c1) (MR 0 a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            then have "u c1 = d" using 1 by auto
            then have "u  {u  V. u c1 < d}" by auto
          }
          ultimately show ?thesis using MR(1) M(1) by auto
        next
          case 2
          from 2 lt have "M a 0  " by auto
          with dbm_entry_int[OF this] M(3) a  n
          obtain d' :: int where d': "M a 0 = Le d'  M a 0 = Lt d'" by auto
          then have "M a 0  Le (d - 1)" using lt 2
          apply (auto simp: less_eq dbm_le_def less)
           apply (cases rule: dbm_lt.cases)
                 apply auto
          apply rule
          apply (cases rule: dbm_lt.cases)
          by auto
          with lt have "M a 0  Le (d - 1)" by auto
          from dbm_le'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. u c1  d - 1}"
          by auto
          from beta_interp.β_boundedness_le'[OF _ C(2) this] ** have
            "Approxβ ([M]⇘v,n)  {u  V. u c1  d - 1}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u None (Some c1) (MR 0 a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            then have "u c1 > d - 1" using 2 by auto
            then have "u  {u  V. u c1  d - 1}" by auto
          }
          ultimately show ?thesis using MR(1) M(1) by auto
        qed
      } note bounded_zero_1 = this

      { fix a assume A: "(0,a)  set (arcs i i ys)"
        assume not0: "a > 0"
        assume bounded: "MR a 0  "
        assume lt: "M 0 a < MR 0 a"
        from clock_dest_2[OF A not0] obtain c1 where C:
          "v c1 = a" "c1  X" "v' a = c1" and C2: "a  n"
        by blast
        from C2 not0 bounded MR(5) obtain d :: int where *:
          "d  int (k (v' a))"
          "MR a 0 = Le d  MR 0 a = Le (- d)  MR a 0 = Lt d  MR 0 a = Lt (- d + 1)"
        unfolding v'_def by auto
        with C have **: "- int (k c1)  - d" by auto
        from *(2) have ?thesis
        proof (standard, goal_cases)
          case 1
          with lt have "M 0 a < Le (-d)" by auto
          then have "M 0 a  Lt (-d)" unfolding less less_eq dbm_le_def by (fastforce elim!: dbm_lt.cases)
          from dbm_lt'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. d < u c1}"
          by auto
          from beta_interp.β_boundedness_gt'[OF _ C(2) this] ** have
            "Approxβ ([M]⇘v,n)  {u  V. - u c1 < -d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c1) None (MR a 0)" "dbm_entry_val u None (Some c1) (MR 0 a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with 1 have "u  {u  V. - u c1 < -d}" by auto
          }
          ultimately show ?thesis using MR(1) M(1) by auto
        next
          case 2
          from 2 lt have "M 0 a  " by auto
          with dbm_entry_int[OF this] M(3) a  n
          obtain d' :: int where d': "M 0 a = Le d'  M 0 a = Lt d'" by auto
          then have "M 0 a  Le (-d)" using lt 2
            apply (auto simp: less_eq dbm_le_def less)
             apply (cases rule: dbm_lt.cases)
                    apply auto
             apply rule
             apply (metis get_const.simps(2) 2 of_int_less_iff of_int_minus zless_add1_eq)
            apply (cases rule: dbm_lt.cases)
            apply auto
            apply (rule dbm_lt.intros(5))
          by (simp add: int_lt_Suc_le)
          from dbm_le'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. d  u c1}"
          by auto
          from beta_interp.β_boundedness_ge'[OF _ C(2) this] ** have
            "Approxβ ([M]⇘v,n)  {u  V. - u c1  -d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c1) None (MR a 0)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with 2 have "u  {u  V. - u c1  -d}" by auto
          }
          ultimately show ?thesis using MR(1) M(1) by auto
        qed
      } note bounded_zero_2 = this

      { fix a b c c1 c2 assume A: "(a,b)  set (arcs i i ys)"
        assume not0: "a > 0" "b > 0"
        assume lt: "M a b = Lt c"
        assume neg: "M a b + MR b a < 0"
        assume C: "v c1 = a" "v c2 = b" "c1  X" "c2  X" and C2: "a  n" "b  n"
        assume valid: "-k c2  -get_const (MR b a)" "-get_const (MR b a)  k c1"
        from neg have "MR b a  " by auto
        then obtain d where *: "MR b a = Le d  MR b a = Lt d" by (cases "MR b a", auto)+
        with MR(7) _ _ _   have "d  " by fastforce
        with * obtain d :: int where *: "MR b a = Le d  MR b a = Lt d" using Ints_cases by auto
        with valid have valid: "- k c2  -d" "-d  k c1" by auto
        from * neg lt have "M a b  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
        by (auto elim!: dbm_lt.cases)
        from dbm_lt'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
          "[M]⇘v,n {u  V. u c1 - u c2 < - d}"
        .
        from beta_interp.β_boundedness_diag_lt'[OF valid C(3,4) this] have
          "Approxβ ([M]⇘v,n)  {u  V. u c1 - u c2 < -d}"
        .
        moreover
        { fix u assume u: "u  [MR]⇘v,n⇙"
          with C C2 have
            "dbm_entry_val u (Some c2) (Some c1) (MR b a)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
          with * have "u  {u  V. u c1 - u c2 < -d}" by auto
        }
        ultimately have ?thesis using MR(1) M(1) by auto
      } note neg_sum_lt = this

      { fix a b assume A: "(a,b)  set (arcs i i ys)"
        assume not0: "a > 0" "b > 0"
        assume neg: "M a b + MR b a < 0"
        from clock_dest[OF A not0] obtain c1 c2 where
          C: "v c1 = a" "v c2 = b" "c1  X" "c2  X" and C2: "a  n" "b  n"
        by blast
        then have C3: "v' a = c1" "v' b = c2" unfolding v'_def using clock_numbering(1) by auto
        from neg have inf: "M a b  " "MR b a  " by auto
        from MR(8) inf not0 C(3,4) C2 C3 obtain d :: int where d:
          "MR b a = Le d  MR b a = Lt d" "- int (k c1)  d" "d  int (k c2)"
        unfolding v'_def by auto
        from inf obtain c where c: "M a b = Le c  M a b = Lt c" by (cases "M a b") auto
        { assume **: "M a b  Lt (-d)"
          from dbm_lt'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
            "[M]⇘v,n {u  V. u c1 - u c2 < (- d)}"
          .
          from beta_interp.β_boundedness_diag_lt'[OF _ _ C(3,4) this] d have
            "Approxβ ([M]⇘v,n)  {u  V. u c1 - u c2 < -d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c2) (Some c1) (MR b a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with d have "u  {u  V. u c1 - u c2 < -d}" by auto
          }
          ultimately have ?thesis using MR(1) M(1) by auto
        } note aux = this
        from c have ?thesis
        proof (standard, goal_cases)
          case 2
          with neg d have "M a b  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
          by (auto elim!: dbm_lt.cases)
          with aux show ?thesis .
        next
          case 1
          note A = this
          from d(1) show ?thesis
          proof (standard, goal_cases)
            case 1
            with A neg d have "M a b  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            with aux show ?thesis .
          next
            case 2
            with A neg d have "M a b  Le (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            from dbm_le'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
              "[M]⇘v,n {u  V. u c1 - u c2  - d}"
            .
            from beta_interp.β_boundedness_diag_le'[OF _ _ C(3,4) this] d have
              "Approxβ ([M]⇘v,n)  {u  V. u c1 - u c2  -d}"
            by auto
            moreover
            { fix u assume u: "u  [MR]⇘v,n⇙"
              with C C2 have
                "dbm_entry_val u (Some c2) (Some c1) (MR b a)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with A 2 have "u  {u  V. u c1 - u c2  -d}" by auto
            }
            ultimately show ?thesis using MR(1) M(1) by auto
          qed
        qed
      } note neg_sum_1 = this

      { fix a b assume A: "(a,0)  set (arcs i i ys)"
        assume not0: "a > 0"
        assume neg: "M a 0 + MR 0 a < 0"
        from clock_dest_1[OF A not0] obtain c1 where C: "v c1 = a" "c1  X" and C2: "a  n" by blast
        with clock_numbering(1) have C3: "v' a = c1" unfolding v'_def by auto
        from neg have inf: "M a 0  " "MR 0 a  " by auto
        from MR(6) not0 C2 C3 obtain d :: int where d:
          "MR 0 a = Le d  MR 0 a = Lt d" "- int (k c1)  d" "d  0"
        unfolding v'_def by auto
        from inf obtain c where c: "M a 0 = Le c  M a 0 = Lt c" by (cases "M a 0") auto
        { assume "M a 0  Lt (-d)"
          from dbm_lt'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. u c1 < - d}"
          .
          from beta_interp.β_boundedness_lt'[OF _ C(2) this] d have
            "Approxβ ([M]⇘v,n)  {u  V. u c1 < -d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u None (Some c1) (MR 0 a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with d have "u  {u  V. u c1 < -d}" by auto
          }
          ultimately have ?thesis using MR(1) M(1) by auto
        } note aux = this
        from c have ?thesis
        proof (standard, goal_cases)
          case 2
          with neg d have "M a 0  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
          by (auto elim!: dbm_lt.cases)
          with aux show ?thesis .
        next
          case 1
          note A = this
          from d(1) show ?thesis
          proof (standard, goal_cases)
            case 1
            with A neg d have "M a 0  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            with aux show ?thesis .
          next
            case 2
            with A neg d have "M a 0  Le (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            from dbm_le'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
              "[M]⇘v,n {u  V. u c1  - d}"
            .
            from beta_interp.β_boundedness_le'[OF _ C(2) this] d have
              "Approxβ ([M]⇘v,n)  {u  V. u c1  -d}"
            by auto
            moreover
            { fix u assume u: "u  [MR]⇘v,n⇙"
              with C C2 have
                "dbm_entry_val u None (Some c1) (MR 0 a)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with A 2 have "u  {u  V. u c1  -d}" by auto
            }
            ultimately show ?thesis using MR(1) M(1) by auto
          qed
        qed
      } note neg_sum_1' = this

      { fix a b assume A: "(0,b)  set (arcs i i ys)"
        assume not0: "b > 0"
        assume neg: "M 0 b + MR b 0 < 0"
        from clock_dest_2[OF A not0] obtain c2 where
          C:  "v c2 = b" "c2  X" and C2: "b  n"
        by blast
        with clock_numbering(1) have C3: "v' b = c2" unfolding v'_def by auto
        from neg have "M 0 b  " "MR b 0  " by auto
        with MR(5) not0 C2 C3 obtain d :: int where d:
          "MR b 0 = Le d  MR b 0 = Lt d" "d  k c2"
        unfolding v'_def by fastforce
        from M 0 b   obtain c where c: "M 0 b = Le c  M 0 b = Lt c" by (cases "M 0 b") auto
        { assume "M 0 b  Lt (-d)"
          from dbm_lt'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. u c2 > d}"
          by simp
          from beta_interp.β_boundedness_gt'[OF _ C(2) this] d have
            "Approxβ ([M]⇘v,n)  {u  V. - u c2 < -d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c2) None (MR b 0)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with d have "u  {u  V. - u c2 < -d}" by auto
          }
          ultimately have ?thesis using MR(1) M(1) by auto
        } note aux = this
        from c have ?thesis
        proof (standard, goal_cases)
          case 2
          with neg d have "M 0 b  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
          by (auto elim!: dbm_lt.cases)
          with aux show ?thesis .
        next
          case A: 1
          from d(1) show ?thesis
          proof (standard, goal_cases)
            case 1
            with A neg have "M 0 b  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            with aux show ?thesis .
          next
            case 2
            with A neg c have "M 0 b  Le (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            from dbm_le'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
              "[M]⇘v,n {u  V. u c2  d}"
            by simp
            from beta_interp.β_boundedness_ge'[OF _ C(2) this] d(2) have
              "Approxβ ([M]⇘v,n)  {u  V. - u c2  -d}"
            by auto
            moreover
            { fix u assume u: "u  [MR]⇘v,n⇙"
              with C C2 have
                "dbm_entry_val u (Some c2) None (MR b 0)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with A 2 have "u  {u  V. - u c2  -d}" by auto
            }
            ultimately show ?thesis using MR(1) M(1) by auto
          qed
        qed
      } note neg_sum_1'' = this

      { fix a b assume A: "(a,b)  set (arcs i i ys)"
        assume not0: "b > 0" "a > 0"
        assume neg: "MR a b + M b a < 0"
        from clock_dest[OF A not0(2,1)] obtain c1 c2 where
          C: "v c1 = a" "v c2 = b" "c1  X" "c2  X" and C2: "a  n" "b  n"
        by blast
        then have C3: "v' a = c1" "v' b = c2" unfolding v'_def using clock_numbering(1) by auto
        from neg have inf: "M b a  " "MR a b  " by auto
        with MR(8) not0 C(3,4) C2 C3 obtain d :: int where d:
          "MR a b = Le d  MR a b = Lt d" "d  -int (k c2)" "d  int (k c1)"
        unfolding v'_def by blast
        from inf obtain c where c: "M b a = Le c  M b a = Lt c" by (cases "M b a") auto
        { assume "M b a  Lt (-d)"
          from dbm_lt'[OF assms(2)[folded M(1)] this C2(2,1) C(2,1) not0] have
            "[M]⇘v,n {u  V. u c2 - u c1 < - d}"
          .
          from beta_interp.β_boundedness_diag_lt'[OF _ _ C(4,3) this] d
          have "Approxβ ([M]⇘v,n)  {u  V. u c2 - u c1 < -d}" by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c1) (Some c2) (MR a b)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with d have "u  {u  V. u c2 - u c1 < -d}" by auto
          }
          ultimately have ?thesis using MR(1) M(1) by auto
        } note aux = this
        from c have ?thesis
        proof (standard, goal_cases)
          case 2
          with neg d have "M b a  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
          by (auto elim!: dbm_lt.cases)
          with aux show ?thesis .
        next
          case A: 1
          from d(1) show ?thesis
          proof (standard, goal_cases)
            case 1
            with A neg d have "M b a  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            with aux show ?thesis .
          next
            case 2
            with A neg d have "M b a  Le (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            from dbm_le'[OF assms(2)[folded M(1)] this C2(2,1) C(2,1) not0] have
              "[M]⇘v,n {u  V. u c2 - u c1  - d}"
            .
            from beta_interp.β_boundedness_diag_le'[OF _ _ C(4,3) this] d
            have "Approxβ ([M]⇘v,n)  {u  V. u c2 - u c1  -d}" by auto
            moreover
            { fix u assume u: "u  [MR]⇘v,n⇙"
              with C C2 have
                "dbm_entry_val u (Some c1) (Some c2) (MR a b)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with A 2 have "u  {u  V. u c2 - u c1  -d}" by auto
            }
            ultimately show ?thesis using MR(1) M(1) by auto
          qed
        qed
      } note neg_sum_2 = this

      { fix a b assume A: "(a,0)  set (arcs i i ys)"
        assume not0: "a > 0"
        assume neg: "MR a 0 + M 0 a < 0"
        from clock_dest_1[OF A not0] obtain c1 where C: "v c1 = a" "c1  X" and C2: "a  n" by blast
        with clock_numbering(1) have C3: "v' a = c1" unfolding v'_def by auto
        from neg have inf: "M 0 a  " "MR a 0  " by auto
        with MR(5) not0 C2 C3 obtain d :: int where d:
          "MR a 0 = Le d  MR a 0 = Lt d" "d  int (k c1)" "d  0"
        unfolding v'_def by auto
        from inf obtain c where c: "M 0 a = Le c  M 0 a = Lt c" by (cases "M 0 a") auto
        { assume "M 0 a  Lt (-d)"
          from dbm_lt'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. u c1 > d}"
          by simp
          from beta_interp.β_boundedness_gt'[OF _ C(2) this] d have
            "Approxβ ([M]⇘v,n)  {u  V. u c1 > d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c1) None (MR a 0)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with d have "u  {u  V. u c1 > d}" by auto
          }
          ultimately have ?thesis using MR(1) M(1) by auto
        } note aux = this
        from c have ?thesis
        proof (standard, goal_cases)
          case 2
          with neg d have "M 0 a  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
          by (auto elim!: dbm_lt.cases)
          with aux show ?thesis .
        next
          case A: 1
          from d(1) show ?thesis
          proof (standard, goal_cases)
            case 1
            with A neg d have "M 0 a  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            with aux show ?thesis .
          next
            case 2
            with A neg d have "M 0 a  Le (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            from dbm_le'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
              "[M]⇘v,n {u  V. u c1  d}"
            by simp
            from beta_interp.β_boundedness_ge'[OF _ C(2) this] d have
              "Approxβ ([M]⇘v,n)  {u  V. u c1  d}"
            by auto
            moreover
            { fix u assume u: "u  [MR]⇘v,n⇙"
              with C C2 have
                "dbm_entry_val u (Some c1) None (MR a 0)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with A 2 have "u  {u  V. u c1  d}" by auto
            }
            ultimately show ?thesis using MR(1) M(1) by auto
          qed
        qed
      } note neg_sum_2' = this

      { fix a b assume A: "(0,b)  set (arcs i i ys)"
        assume not0: "b > 0"
        assume neg: "MR 0 b + M b 0 < 0"
        from clock_dest_2[OF A not0] obtain c2 where
          C:  "v c2 = b" "c2  X" and C2: "b  n"
        by blast
        with clock_numbering(1) have C3: "v' b = c2" unfolding v'_def by auto
        from neg have "M b 0  " "MR 0 b  " by auto
        with MR(6) not0 C2 C3 obtain d :: int where d:
          "MR 0 b = Le d  MR 0 b = Lt d" "-d  k c2"
        unfolding v'_def by fastforce
        from M b 0   obtain c where c: "M b 0 = Le c  M b 0 = Lt c" by (cases "M b 0") auto
        { assume "M b 0  Lt (-d)"
          from dbm_lt'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
            "[M]⇘v,n {u  V. u c2 < - d}"
          by simp
          from beta_interp.β_boundedness_lt'[OF _ C(2) this] d have
            "Approxβ ([M]⇘v,n)  {u  V. u c2 < -d}"
          by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u None (Some c2) (MR 0 b)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with d have "u  {u  V. u c2 < -d}" by auto
          }
          ultimately have ?thesis using MR(1) M(1) by auto
        } note aux = this
        from c have ?thesis
        proof (standard, goal_cases)
          case 2
          with neg d have "M b 0  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
          by (auto elim!: dbm_lt.cases)
          with aux show ?thesis .
        next
          case 1
          note A = this
          from d(1) show ?thesis
          proof (standard, goal_cases)
            case 1
            with A neg have "M b 0  Lt (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            with aux show ?thesis .
          next
            case 2
            with A neg c have "M b 0  Le (-d)" unfolding less_eq dbm_le_def add neutral less
            by (auto elim!: dbm_lt.cases)
            from dbm_le'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
              "[M]⇘v,n {u  V. u c2  - d}"
            by simp
            from beta_interp.β_boundedness_le'[OF _ C(2) this] d(2) have
              "Approxβ ([M]⇘v,n)  {u  V. u c2  -d}"
            by auto
            moreover
            { fix u assume u: "u  [MR]⇘v,n⇙"
              with C C2 have
                "dbm_entry_val u None (Some c2) (MR 0 b)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with A 2 have "u  {u  V. u c2  -d}" by auto
            }
            ultimately show ?thesis using MR(1) M(1) by auto
          qed
        qed
      } note neg_sum_2'' = this

      { fix a b assume A: "(a,b)  set (arcs i i ys)"
        assume not0: "a > 0" "b > 0"
        assume bounded: "MR a 0  " "MR b 0  "
        assume lt: "M a b < MR a b"
        from clock_dest[OF A not0] obtain c1 c2 where
          C: "v c1 = a" "v c2 = b" "c1  X" "c2  X" and C2: "a  n" "b  n"
        by blast
        from C C2 clock_numbering(1,3) have C3: "v' b = c2" "v' a = c1" unfolding v'_def by blast+
        with C C2 not0 bounded MR(4) obtain d :: int where *:
          "- int (k c2)  d  d  int (k c1)  MR a b = Le d  MR b a = Le (- d)
          - int (k c2)  d - 1  d  int (k c1)  MR a b = Lt d  MR b a = Lt (- d + 1)"
        unfolding v'_def by force
        from * have ?thesis
        proof (standard, goal_cases)
          case 1
          with lt have "M a b < Le d" by auto
          then have "M a b  Lt d" unfolding less less_eq dbm_le_def by (fastforce elim!: dbm_lt.cases)
          from dbm_lt'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
            "[M]⇘v,n {u  V. u c1 - u c2 < d}"
          .
          from beta_interp.β_boundedness_diag_lt'[OF _ _ C(3,4) this] 1
          have "Approxβ ([M]⇘v,n)  {u  V. u c1 - u c2 < d}" by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c1) (Some c2) (MR a b)" "dbm_entry_val u (Some c2) (Some c1) (MR b a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with 1 have "u  {u  V. u c1 - u c2 < d}" by auto
          }
          ultimately show ?thesis using MR(1) M(1) by auto
        next
          case 2
          with lt have "M a b  " by auto
          with dbm_entry_int[OF this] M(3) a  n b  n
          obtain d' :: int where d': "M a b = Le d'  M a b = Lt d'" by auto
          then have "M a b  Le (d - 1)" using lt 2
           apply (auto simp: less_eq dbm_le_def less)
            apply (cases rule: dbm_lt.cases)
                 apply auto
           apply (rule dbm_lt.intros)
           apply (cases rule: dbm_lt.cases)
          by auto
          with lt have "M a b  Le (d - 1)" by auto
          from dbm_le'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
            "[M]⇘v,n {u  V. u c1 - u c2  d - 1}"
          .
          from beta_interp.β_boundedness_diag_le'[OF _ _ C(3,4) this] 2
          have "Approxβ ([M]⇘v,n)  {u  V. u c1 - u c2  d - 1}" by auto
          moreover
          { fix u assume u: "u  [MR]⇘v,n⇙"
            with C C2 have
              "dbm_entry_val u (Some c2) (Some c1) (MR b a)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with 2 have "u  {u  V. u c1 - u c2  d - 1}" by auto
          }
          ultimately show ?thesis using MR(1) M(1) by auto
        qed
      } note bounded = this

      { assume not_bounded: " (a,b)  set (arcs i i ys). M a b < MR a b  MR a 0 =   MR b 0 = "
        have " y z zs. set zs  {0, y, z} = set (i # ys)  len ?M 0 0 (y # z # zs) < Le 0 
                    ( (a,b)  set (arcs 0 0 (y # z # zs)). M a b < MR a b  a = y  b = z)
                     M y z < MR y z  distinct (0 # y # z # zs)  ?thesis"
        proof (cases ys)
          case Nil
          show ?thesis
          proof (cases "M i i < MR i i")
            case True
            then have "?M i i = M i i" by simp
            with Nil ys(1) xs(3) have *: "M i i < 0" by simp
            with neg_cycle_empty[OF cn_weak _ i  n, of "[]" M] have "[M]⇘v,n= {}" by auto
            with Z  {} M(1) show ?thesis by auto
          next
            case False
            then have "?M i i = MR i i" by (simp add: min_absorb2)
            with Nil ys(1) xs(3) have "MR i i < 0" by simp
            with neg_cycle_empty[OF cn_weak _ i  n, of "[]" MR] have "[MR]⇘v,n= {}" by auto
            with R  {} MR(1) show ?thesis by auto
          qed
        next
          case (Cons w ws)
          note ws = this
          show ?thesis
          proof (cases ws)
            case Nil
            with ws ys xs(3) have *:
              "?M i w + ?M w i < 0" "?M w i = M w i  ?M i w  M i w" "(i, w)  set (arcs i i ys)"
            by auto
            have "R  Approxβ Z = {}"
            proof (cases "?M w i = M w i")
              case True
              with *(2) have "?M i w = MR i w" unfolding min_def by auto
              with *(1) True have neg: "MR i w + M w i < 0" by auto
              show ?thesis
              proof (cases "i = 0")
                case True
                show ?thesis
                proof (cases "w = 0")
                  case True with 0 i = 0 *(3) show ?thesis by auto
                next
                  case False with i = 0 neg_sum_2'' *(3) neg show ?thesis by blast
                qed
              next
                case False
                show ?thesis
                proof (cases "w = 0")
                  case True with i  0 neg_sum_2' *(3) neg show ?thesis by blast
                next
                  case False with i  0 neg_sum_2 *(3) neg show ?thesis by blast
                qed
              qed
            next
              case False
              have "MR w i < M w i"
              proof (rule ccontr, goal_cases)
                case 1
                then have "MR w i  M w i" by auto
                with False show False unfolding min_def by auto
              qed
              with one_M ws Nil have "M i w < MR i w" by auto
              then have "?M i w = M i w" unfolding min_def by auto
              moreover from False *(2) have "?M w i = MR w i" unfolding min_def by auto
              ultimately have neg: "M i w + MR w i < 0" using *(1) by auto
              show ?thesis
              proof (cases "i = 0")
                case True
                show ?thesis
                proof (cases "w = 0")
                  case True with 0 i = 0 *(3) show ?thesis by auto
                next
                  case False with i = 0 neg_sum_1'' *(3) neg show ?thesis by blast
                qed
              next
                case False
                show ?thesis
                proof (cases "w = 0")
                  case True with i  0 neg_sum_1' *(3) neg show ?thesis by blast
                next
                  case False with i  0 neg_sum_1 *(3) neg show ?thesis by blast
                qed
              qed
            qed
            then show ?thesis by simp
          next
            case zs: (Cons z zs)
            from one_M obtain a b where *:
              "(a,b)  set (arcs i i ys)" "M a b < MR a b"
            by fastforce
            from cycle_rotate_3'[OF _ *(1) ys(3)] ws cycle_closes obtain ws' where ws':
              "len ?M i i ys = len ?M a a (b # ws')" "set (a # b # ws') = set (i # ys)"
              "1 + length ws' = length ys" "set (arcs i i ys) = set (arcs a a (b # ws'))"
              and successive: "successive (λ(a, b). ?M a b = M a b) (arcs a a (b # ws') @ [(a, b)])"
            by blast
            from successive have successive_arcs:
              "successive (λ(a, b). ?M a b = M a b) (arcs a b (b # ws' @ [a]))"
            using arcs_decomp_tail by auto
            from ws'(4) one_M_R *(2) obtain c d where **:
              "(c,d)  set (arcs a a (b # ws'))" "M c d > MR c d" "(a,b)  (c,d)"
            by fastforce
            from card_distinct[of "a # b # ws'"] distinct_card[of "i # ys"] ws'(2,3) distinct
            have distinct: "distinct (a # b # ws')" by simp
            from ws zs ws'(3) have "ws'  []" by auto
            then obtain z zs where z: "ws' = zs @ [z]" by (metis append_butlast_last_id)
            then have "b # ws' = (b # zs) @ [z]" by simp
            with len_decomp[OF this, of ?M a a] arcs_decomp_tail have rotated:
              "len ?M a a (b # ws') = len ?M z z (a # b # zs)"
              "set (arcs a a (b # ws')) = set (arcs z z (a # b # zs))"
            by (auto simp add: comm)
            from ys(1) xs(3) ws'(1) have "len ?M a a (b # ws') < 0" by auto
            from ws'(2) ys(2) i  n z have n_bounds: "a  n" "b  n" "set ws'  {0..n}" "z  n" by auto
            from * have a_b: "?M a b = M a b" by simp
            from successive successive_split[of _ "arcs a z (b # zs)" "[(z,a), (a,b)]"]
            have first: "successive (λ(a, b). ?M a b = M a b) (arcs a z (b # zs))" and
                 last_two: "successive (λ(a, b). ?M a b = M a b) [(z, a), (a, b)]"
            using arcs_decomp_tail z by auto
            from * not_bounded have not_bounded': "MR a 0 =   MR b 0 = " by auto
            from this(1) have "z = 0"
            proof
              assume inf: "MR b 0 = "
              from a_b successive obtain z where z: "(b,z)  set (arcs b a ws')" "?M b z  M b z"
              by (cases ws') auto
              then have "?M b z = MR b z" by (meson min_def)
              from arcs_distinct2[OF _ _ _ _ z(1)] distinct have "b  z" by auto
              from z n_bounds have "z  n"
                apply (induction ws' arbitrary: b)
                 apply auto[]
                 apply (rename_tac ws' b)
                apply (case_tac ws')
                 apply auto
              done
              have "MR b z = "
              proof (cases "z = 0")
                case True
                with inf show ?thesis by auto
              next
                case False
                with inf MR(2) b  z z  n b  n show ?thesis by blast
              qed
              with ?M b z = MR b z have "len ?M b a ws' = " by (auto intro: len_inf_elem[OF z(1)])
              then have " = len ?M a a (b # ws')" by simp
              with len ?M a a _ < 0 show ?thesis by auto
            next
              assume inf: "MR a 0 = "
              show "z = 0"
              proof (rule ccontr)
                assume "z  0"
                with last_two a_b have "?M z a = MR z a" by (auto simp: min_def)
                from distinct z have "a  z" by auto
                with z  0 a  n z  n MR(2) inf have "MR z a = " by blast
                with ?M z a = MR z a have "len ?M z z (a # b # zs) = " by (auto intro: len_inf_elem)
                with len ?M a a _ < 0 rotated show False by auto
              qed
            qed
            { fix c d assume A: "(c, d)  set (arcs 0 0 (a # b # zs))" "M c d < MR c d"
              then have *: "?M c d = M c d" by simp
              from rotated(2) A z = 0 not_bounded ws'(4) have **: "MR c 0 =   MR d 0 = " by auto
              { assume inf: "MR c 0 = "
                fix x assume x: "(x, c)  set (arcs a 0 (b # zs))" "?M x c  M x c"
                from x(2) have "?M x c = MR x c" unfolding min_def by auto
                from arcs_elem[OF x(1)] z z = 0 have
                  "x  set (a # b # ws')" "c  set (a # b # ws')"
                by auto
                with n_bounds have "x  n" "c  n" by auto
                have "x = 0"
                proof (rule ccontr)
                  assume "x  0"
                  from distinct z arcs_distinct1[OF _ _ _ _ x(1)] z = 0have "x  c" by auto
                  with x  0 c  n x  n MR(2) inf have "MR x c = " by blast
                  with ?M x c = MR x c have
                    "len ?M a 0 (b # zs) = "
                  by (fastforce intro: len_inf_elem[OF x(1)])
                  with z = 0 have "len ?M z z (a # b # zs) = " by auto
                  with len ?M a a _ < 0 rotated show False by auto
                qed
                with arcs_distinct_dest1[OF _ x(1), of z] z distinct x z = 0 have False by auto
              } note c_0_inf = this
              have "a = c  b = d"
              proof (cases "(c, d) = (0, a)")
                case True
                with last_two z = 0 * a_b have False by auto
                then show ?thesis by simp
              next
                case False
                show ?thesis
                proof (rule ccontr, goal_cases)
                  case 1
                  with False A(1) have ***: "(c, d)  set (arcs b 0 zs)" by auto
                  from successive z z = 0 have
                    "successive (λ(a, b). ?M a b = M a b) ([(a, b)] @ arcs b 0 zs @ [(0, a), (a, b)])"
                  by (simp add: arcs_decomp)
                  then have ****: "successive (λ(a, b). ?M a b = M a b) (arcs b 0 zs)"
                  using successive_split[of _ "[(a, b)]" "arcs b 0 zs @ [(0, a), (a, b)]"]
                        successive_split[of _ "arcs b 0 zs" "[(0, a), (a, b)]"]
                  by auto
                  from successive_predecessor[OF *** _ this] successive z
                  obtain x where x: "(x, c)  set (arcs a 0 (b # zs))" "?M x c  M x c"
                  proof (cases "c = b")
                    case False
                    then have "zs  []" using *** by auto
                    from successive_predecessor[OF *** False **** _ this] * obtain x where x:
                      "(zs = [c]  x = b  (ys. zs = c # d # ys  x = b)
                         (ys. zs = ys @ [x, c]  d = 0)  (ys ws. zs = ys @ x # c # d # ws))"
                      "?M x c  M x c"
                    by blast+
                    from this(1) have "(x, c)  set (arcs a 0 (b # zs))" using arcs_decomp by auto
                    with x(2) show ?thesis by (auto intro: that)
                  next
                    case True
                    have ****: "successive (λ(a, b). ?M a b = M a b) (arcs a 0 (b # zs))"
                    using first z = 0 arcs_decomp successive_arcs z by auto
                    show ?thesis
                    proof (cases zs)
                      case Nil
                      with **** True *** * show ?thesis by (auto intro: that)
                    next
                      case (Cons u us)
                      with *** True distinct z z = 0 have "distinct (b # u # us @ [0])" by auto
                      from arcs_distinct_fix[OF this] *** True Cons have "d = u" by auto
                      with **** * Cons True show ?thesis by (auto intro: that)
                    qed
                  qed
                  show False
                  proof (cases "d = 0")
                    case True
                    from ** show False
                    proof
                      assume "MR c 0 = " from c_0_inf[OF this x] show False .
                    next
                      assume "MR d 0 = " with d = 0 MR(3) show False by auto
                    qed
                  next
                    case False with *** have "zs  []" by auto
                    from successive_successor[OF (c,d)  set (arcs b 0 zs) False **** _ this] *
                    obtain e where
                      "(zs = [d]  e = 0  (ys. zs = d # e # ys)  (ys. zs = ys @ [c, d]  e = 0)
                         (ys ws. zs = ys @ c # d # e # ws))" "?M d e  M d e"
                    by blast
                    then have e: "(d, e)  set (arcs b 0 zs)" "?M d e  M d e" using arcs_decomp by auto
                    from ** show False
                    proof
                      assume inf: "MR d 0 = "
                      from e have "?M d e = MR d e" by (meson min_def)
                      from arcs_distinct2[OF _ _ _ _ e(1)] z z = 0 distinct have "d  e" by auto
                      from z n_bounds have "set zs  {0..n}" by auto
                      with e have "e  n"
                        apply (induction zs arbitrary: d)
                         apply auto
                        apply (case_tac zs)
                         apply auto
                      done
                      from n_bounds z arcs_elem(2)[OF A(1)] have "d  n" by auto
                      have "MR d e = "
                      proof (cases "e = 0")
                        case True
                        with inf show ?thesis by auto
                      next
                        case False
                        with inf MR(2) d  e e  n d  n show ?thesis by blast
                      qed
                      with ?M d e = MR d e have "len ?M b 0 zs = " by (auto intro: len_inf_elem[OF e(1)])
                      with z = 0 rotated have " = len ?M a a (b # ws')" by simp
                      with len ?M a a _ < 0 show ?thesis by auto
                    next
                      assume "MR c 0 = " from c_0_inf[OF this x] show False .
                    qed
                  qed
                qed
              qed
            }
            then have "(c, d)set (arcs 0 0 (a # b # zs)). M c d < MR c d  c = a  d = b"
            by blast
            moreover from ys(1) xs(3) have "len ?M i i ys < Le 0" unfolding neutral by auto
            moreover with rotated ws'(1) have "len ?M z z (a # b # zs) < Le 0" by auto
            moreover from z = 0 z ws'(2) have "set zs  {0, a, b} = set (i # ys)" by auto
            moreover from z = 0 distinct z have "distinct (0 # a # b # zs)" by auto
            ultimately show ?thesis using z = 0 M a b < MR a b by blast
          qed
        qed note * = this
        { assume "¬ ?thesis"
          with * obtain y z zs where *:
            "set zs  {0, y, z} = set (i # ys)" "len ?M 0 0 (y # z # zs) < Le 0"
            "(a, b)set (arcs 0 0 (y # z # zs)). M a b < MR a b  a = y  b = z" "M y z < MR y z"
            and distinct': "distinct (0 # y # z # zs)"
          by blast
          then have "y  0" "z  0" by auto
          let ?r = "len MR z 0 zs"
          have "(a, b)set (arcs z 0 zs). ?M a b = MR a b"
          proof (safe, goal_cases)
            case A: (1 a b)
            have "MR a b  M a b"
            proof (rule ccontr, goal_cases)
              case 1
              with *(3) A have "a = y" "b = z" by auto
              with A distinct' arcs_distinct3[OF _ A, of y] show False by auto
            qed
            then show ?case by (simp add: min_def)
          qed
          then have r: "len ?M z 0 zs = ?r" by (induction zs arbitrary: z) auto
          with *(2) have **: "?M 0 y + (?M y z + ?r) < Le 0" by simp
          from MR(1) R  {} obtain u where u: "DBM_val_bounded v u MR n"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
          from *(1) i  n set ys  _ have "y  n" "z  n" by fastforce+
          from *(1) ys(2,4) have "set zs  {0 ..n}" by auto
          from y  n z  n clock_numbering(2) y  0 z  0 obtain c1 c2 where C:
            "c1  X" "c2  X" "v c1 = y" "v c2 = z"
          by blast+
          with clock_numbering(1,3) have C2: "v' y = c1" "v' z = c2" unfolding v'_def by auto
          with C have "v (v' z) = z" by auto
          with DBM_val_bounded_len'1[OF u, of zs "v' z"] have "dbm_entry_val u (Some (v' z)) None ?r"
          using z  n clock_numbering(2) set zs  _ distinct' by force
          from len_inf_elem ** have tl_not_inf: "(a, b)set (arcs z 0 zs). MR a b  " by fastforce
          with MR(7) len_int_dbm_closed have "get_const ?r    ?r  " by blast
          then obtain r :: int where r': "?r = Le r  ?r = Lt r" using Ints_cases by (cases ?r) auto
          from r' dbm_entry_val _ _ _ _ C C2 have le: "u (v' z)  r" by fastforce
          from arcs_ex_head obtain z' where "(z, z')  set (arcs z 0 zs)" by blast
          then have z':
            "(z, z')  set (arcs 0 0 (y # z # zs))" "(z, z')  set (arcs z 0 zs)"
          by auto
          have "MR z 0  "
          proof (rule ccontr, goal_cases)
            case 1
            then have inf: "MR z 0 = " by auto
            have "MR z z' = "
            proof (cases "z' = 0")
              case True
              with 1 show ?thesis by auto
            next
              case False
              from arcs_elem[OF z'(1)] *(1) i  n set ys  _ have "z'  n" by fastforce
              moreover from distinct' *(1) arcs_distinct1[OF _ _ _ _ z'(1)] have "z  z'" by auto
              ultimately show ?thesis using MR(2) z  n False inf by blast
            qed
            with tl_not_inf z'(2) show False by auto
          qed
          with MR(5) z  0 z  n obtain d :: int where d:
            "MR z 0 = Le d  MR 0 z = Le (-d)  MR z 0 = Lt d  MR 0 z = Lt (-d + 1)"
            "d  k (v' z)" "0  d"
          unfolding v'_def by auto
          text ‹Needs property that len of integral dbm entries is integral and definition of M_R›
          from this (1) have rr: "?r  MR z 0"
          proof (standard, goal_cases)
            case A: 1
            with u z  n C C2 have *: "- u (v' z)  -d" unfolding DBM_val_bounded_def by fastforce
            from r' show ?case
            proof (standard, goal_cases)
              case 1
              with le * A show ?case unfolding less_eq dbm_le_def by fastforce
            next
              case 2
              with dbm_entry_val _ _ _ _ C C2 have "u (v' z) < r" by fastforce
              with * have "r > d" by auto
              with A 2 show ?case unfolding less_eq dbm_le_def by fastforce
            qed
          next
            case A: 2
            with u z  n C C2 have *: "- u (v' z) < -d + 1" unfolding DBM_val_bounded_def by fastforce
            from r' show ?case
            proof (standard, goal_cases)
              case 1
              with le * A show ?case unfolding less_eq dbm_le_def by fastforce
            next
              case 2
              with dbm_entry_val _ _ _ _ C C2 have "u (v' z)  r" by fastforce
              with * have "r  d" by auto
              with A 2 show ?case unfolding less_eq dbm_le_def by fastforce
            qed
          qed
          with *(3) y  0 have "M 0 y  MR 0 y" by fastforce
          then have "?M 0 y = MR 0 y" by (simp add: min.absorb2)
          moreover from *(4) have "?M y z = M y z" unfolding min_def by auto
          ultimately have **: "MR 0 y + (M y z + MR z 0) < Le 0"
          using ** add_mono_right[OF add_mono_right[OF rr], of "MR 0 y" "M y z"] by simp
          from ** have not_inf: "MR 0 y  " "M y z  " "MR z 0  " by auto
          from MR(6) y  0 y  n obtain c :: int where c:
            "MR 0 y = Le c  MR 0 y = Lt c" "- k (v' y)  c" "c  0"
          unfolding v'_def by auto
          have ?thesis
          proof (cases "MR 0 y + MR z 0 = Lt (c + d)")
            case True
            from ** have "(MR 0 y + MR z 0) + M y z < Le 0" using comm add.assoc by metis
            with True have **: "Lt (c + d) + M y z < Le 0" by simp
            then have "M y z  Le (- (c + d))" unfolding less less_eq dbm_le_def add
            by (cases "M y z") (fastforce elim!: dbm_lt.cases)+
            from dbm_le'[OF assms(2)[folded M(1)] this y  n z  n C(3,4)] y  0 z  0 M
            have subs: "Z  {u  V. u c1 - u c2  - (c + d)}" by blast
            with c d have "- k (v' z)  - (c + d)" "- (c + d)  k (v' y)" by auto
            with beta_interp.β_boundedness_diag_le'[OF _ _ C(1,2) subs] C2 have
              "Approxβ Z  {u  V. u c1 - u c2  - (c + d)}"
            by auto
            moreover
            { fix u assume u: "u  R"
              with C y  n z  n MR(1) have
                "dbm_entry_val u (Some c2) None (MR z 0)" "dbm_entry_val u None (Some c1) (MR 0 y)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with True c d(1) have "u  {u  V. u c1 - u c2  - (c + d)}" unfolding add by auto
            }
            ultimately show ?thesis by blast
          next
            case False
            with c d have "MR 0 y + MR z 0 = Le (c + d)" unfolding add by fastforce
            moreover from ** have "(MR 0 y + MR z 0) + M y z < Le 0" using comm add.assoc by metis
            ultimately have **: "Le (c + d) + M y z < Le 0" by simp
            then have "M y z  Lt (- (c + d))" unfolding less less_eq dbm_le_def add
            by (cases "M y z") (fastforce elim!: dbm_lt.cases)+
            from dbm_lt'[OF assms(2)[folded M(1)] this y  n z  n C(3,4)] y  0 z  0 M
            have subs: "Z  {u  V. u c1 - u c2 < - (c + d)}" by auto
            from c d(2-) C2 have "- k c2  - (c + d)" "- (c + d)  k c1" by auto
            from beta_interp.β_boundedness_diag_lt'[OF this C(1,2) subs] have
              "Approxβ Z  {u  V. u c1 - u c2 < - (c + d)}"
            .
            moreover
            { fix u assume u: "u  R"
              with C y  n z  n MR(1) have
                "dbm_entry_val u (Some c2) None (MR z 0)" "dbm_entry_val u None (Some c1) (MR 0 y)"
              unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
              with c d(1) have "u  {u  V. u c1 - u c2 < - (c + d)}" by auto
            }
            ultimately show ?thesis by auto
          qed
        } then have ?thesis by auto
      }
      with bounded 0 bounded_zero_1 bounded_zero_2 show ?thesis by blast
    qed
  qed
qed


section ‹Nice Corollaries of Bouyer's Theorem›

lemma ℛ_V: "  = V" unfolding V_def ℛ_def using region_cover[of X _ k] by auto

lemma regions_beta_V: "R  β  R  V" unfolding V_def β_def by auto

lemma apx_V: "Z  V  Approxβ Z  V"
proof (goal_cases)
  case 1
  from beta_interp.apx_in[OF 1] obtain U where "Approxβ Z = U" "U  β" by auto
  with regions_beta_V show ?thesis by auto
qed

corollary approx_β_closure_α:
  assumes "Z  V" "vabstr Z M"
  shows "Approxβ Z  Closureα Z"
proof -
  note T = region_zone_intersect_empty_approx_correct[OF _ assms(1) _ assms(2-)]
  have "- {R  . R  Z  {}} = {R  . R  Z = {}}  - V"
  proof (safe, goal_cases)
    case 1 with ℛ_V show False by fast
  next
    case 2 then show ?case using alpha_interp.valid_regions_distinct_spec by fastforce
  next
    case 3 then show ?case using ℛ_V unfolding V_def by blast
  qed
  with T apx_V[OF assms(1)] have "Approxβ Z  - {R  . R  Z  {}} = {}" by auto
  then show ?thesis unfolding alpha_interp.cla_def by blast
qed

corollary approx_β_closure_α': "Z  V'  Approxβ Z  Closureα Z"
using approx_β_closure_α unfolding V'_def by auto

text ‹We could prove this more directly too (without using Closureα Z›), obviously›
lemma apx_empty_iff:
  assumes "Z  V" "vabstr Z M"
  shows "Z = {}  Approxβ Z = {}"
using alpha_interp.cla_empty_iff[OF assms(1)] approx_β_closure_α[OF assms] beta_interp.apx_subset
by auto

lemma apx_empty_iff':
  assumes "Z  V'" shows "Z = {}  Approxβ Z = {}"
using apx_empty_iff assms unfolding V'_def by force

lemma apx_V':
  assumes "Z  V" shows "Approxβ Z  V'"
proof (cases "Z = {}")
  case True
  with beta_interp.apx_empty beta_interp.empty_zone_dbm show ?thesis unfolding V'_def neutral by auto
next
  case False
  then have non_empty: "Approxβ Z  {}" using beta_interp.apx_subset by blast
  from beta_interp.apx_in[OF assms] obtain U M where *:
    "Approxβ Z = U" "U  β" "Z  Approxβ Z" "vabstr (Approxβ Z) M"
  by blast
  moreover from * beta_interp.ℛ_union have " U  V" by blast
  ultimately show ?thesis using *(1,4) unfolding V'_def by auto
qed

end (* End of context for global regions *)

lemma valid_abstraction_pairsD:
  "(x, m)Timed_Automata.clkp_set A. x  X  m  " if "valid_abstraction A X k"
  using that
  apply cases
  unfolding clkp_set_def Timed_Automata.clkp_set_def
  unfolding collect_clki_def Timed_Automata.collect_clki_def
  unfolding collect_clkt_def Timed_Automata.collect_clkt_def
  by blast

section ‹A New Zone Semantics Abstracting with Approxβ

locale Regions =
  Regions_defs X v n for X and v :: "'c  nat" and n :: nat +
  fixes k :: "'s  'c  nat" and not_in_X
  assumes finite: "finite X"
  assumes clock_numbering:
    "clock_numbering' v n" "kn. k > 0  (c  X. v c = k)" " c  X. v c  n"
  assumes not_in_X: "not_in_X  X"
  assumes non_empty: "X  {}"
begin

definition ℛ_def: " l  {Regions.region X I r | I r. Regions.valid_region X (k l) I r}"

definition β_def:
  "β l  {Regions_Beta.region X I J r | I J r. Regions_Beta.valid_region X (k l) I J r}"

sublocale
  AlphaClosure X k  by (unfold_locales) (auto simp: finite ℛ_def V_def)

abbreviation "Approxβ l Z  Beta_Regions'.Approxβ X (k l) v n not_in_X Z"


subsection ‹Single Step›

inductive step_z_beta ::
  "('a, 'c, t, 's) ta  's  ('c, t) zone  'a action  's  ('c, t) zone  bool"
(‹_  _, _ ↝⇘β(_) _, _ [61,61,61,61] 61)
where
  step_beta: "A  l, Z ↝⇘al', Z'  A  l, Z ↝⇘β(a)l', Approxβ l' Z'"

inductive_cases[elim!]: "A  l, u ↝⇘β(a)l',u'"

declare step_z_beta.intros[intro]


(* XXX All of these should be considered for moving into the locales for global sets of regions *)
context
  fixes l' :: 's
begin

interpretation regions: Regions_global _ _ _ "k l'"
  by standard (rule finite clock_numbering not_in_X non_empty)+

lemma step_z_V':
  assumes "A  l,Z ↝⇘al',Z'" "valid_abstraction A X k" "cclk_set A. v c  n" "Z  V'"
  shows "Z'  V'"
proof -
  from assms(3) clock_numbering have numbering: "global_clock_numbering A v n" by metis
  from assms(4) obtain M where M:
    "Z  V" "Z = [M]⇘v,n⇙" "dbm_int M n"
    unfolding V'_def by auto
  from valid_abstraction_pairsD[OF assms(2)] have "(x, m)Timed_Automata.clkp_set A. m  "
    by blast
  from step_z_V[OF assms(1) M(1)] M(2) assms(1) step_z_dbm_DBM[OF _ numbering]
       step_z_dbm_preserves_int[OF _ numbering this M(3)]
  obtain M' where M': "Z'  V" "Z' = [M']⇘v,n⇙" "dbm_int M' n" by metis
  then show ?thesis unfolding V'_def by blast
qed

lemma step_z_alpha_sound:
  "A  l, Z ↝⇘β(a)l',Z'  valid_abstraction A X k  cclk_set A. v c  n  Z  V'
   Z'  {}   Z''. A  l, Z ↝⇘al',Z''  Z''  {}"
 apply (induction l'  l' Z' rule: step_z_beta.induct)
 apply (frule step_z_V')
    apply assumption+
  apply (rotate_tac 5)
 apply (drule regions.apx_empty_iff')
by blast

lemma step_z_alpha_complete:
  "A  l, Z ↝⇘al',Z'  valid_abstraction A X k  cclk_set A. v c  n  Z  V'
   Z'  {}   Z''. A  l, Z ↝⇘β(a)l', Z''  Z''  {}"
 apply (frule step_z_V')
    apply assumption+
 apply (rotate_tac 4)
 apply (drule regions.apx_empty_iff')
 by blast

lemma alpha_beta_step:
  "A  l, Z ↝⇘β(a)l', Z'  valid_abstraction A X k  cclk_set A. v c  n  Z  V'
    Z''. A  l, Z ↝⇘α(a)l', Z''  Z'  Z''"
  apply (induction l'  l' Z' rule: step_z_beta.induct)
  apply (frule step_z_V')
    apply assumption+
  apply (rotate_tac 4)
  apply (drule regions.approx_β_closure_α')
  apply auto
done

lemma alpha_beta_step':
  "A  l, Z ↝⇘β(a)l', Z'  valid_abstraction A X k  cclk_set A. v c  n  Z  V'  W  V
   Z  W   W'. A  l, W ↝⇘α(a)l', W'  Z'  W'"
proof (induction l'  l' Z' rule: step_z_beta.induct)
  case (step_beta A l Z a Z')
  from step_z_mono[OF step_beta(1,6)] obtain W' where W':
    "A  l, W ↝⇘al',W'" "Z'  W'"
  by blast
  from regions.approx_β_closure_α'[OF step_z_V'[OF step_beta(1-4)]]
       regions.alpha_interp.cla_mono[OF this(2)] this(1)
  show ?case by auto
qed

lemma apx_mono:
  "Z'  V  Z  Z'  Approxβ l' Z  Approxβ l' Z'"
proof (goal_cases)
  case 1
  with regions.beta_interp.apx_in have
    "regions.Approxβ Z'  {S. U M. S = U  U  regions.ℛβ  Z'  S  regions.beta_interp.vabstr S M
                       regions.beta_interp.normalized M}"
  by auto
  with 1 obtain U M where
    "regions.Approxβ Z' = U" "U  regions.ℛβ" "Z  regions.Approxβ Z'"
    "regions.beta_interp.vabstr (regions.Approxβ Z') M"
    "regions.beta_interp.normalized M"
  by auto
  with regions.beta_interp.apx_min show ?thesis by auto
qed

end (* End of context for global regions *)

lemma step_z'_V':
  assumes "A  l,Z  l',Z'" "valid_abstraction A X k" "cclk_set A. v c  n" "Z  V'"
  shows "Z'  V'"
  using assms unfolding step_z'_def by (auto elim: step_z_V')

lemma steps_z_V':
  "A  l,Z ↝* l',Z'  valid_abstraction A X k  cclk_set A. v c  n  Z  V'  Z'  V'"
  by (induction rule: rtranclp_induct2; blast intro: step_z'_V')

subsection ‹Multi step›

definition
  step_z_beta' :: "('a, 'c, t, 's) ta  's  ('c, t) zone  's  ('c, t) zone  bool"
(‹_  _, _ β _, _ [61,61,61] 61)
where
  "A  l, Z β l', Z'' = ( Z' a. A  l, Z ↝⇘τl, Z'  A  l, Z' ↝⇘β(a)l', Z'')"

abbreviation
  steps_z_beta :: "('a, 'c, t, 's) ta  's  ('c, t) zone  's  ('c, t) zone  bool"
(‹_  _, _ β* _, _ [61,61,61] 61)
where
  "A  l, Z β* l', Z''  (λ (l, Z) (l', Z''). A  l, Z β l', Z'')** (l, Z) (l', Z'')"

lemma V'_V: "Z  V'  Z  V" unfolding V'_def by auto

context
  fixes A :: "('a, 'c, t, 's) ta"
  assumes valid_ta: "valid_abstraction A X k" "cclk_set A. v c  n"
begin

interpretation alpha: AlphaClosure_global _ "k l'" " l'" by standard (rule finite)
lemma [simp]: "alpha.cla l' = cla l'" unfolding alpha.cla_def cla_def ..

lemma step_z_alpha'_V:
  "Z'  V" if "Z  V" "A  l, Z α l', Z'"
  using that alpha.closure_V[simplified] unfolding step_z_alpha'_def by blast

lemma step_z_beta'_V':
  "Z'  V'" if "A  l,Z β l',Z'" "Z  V'"
proof -
  interpret regions: Regions_global _ _ _ "k l'"
    by standard (rule finite clock_numbering not_in_X non_empty)+
  from that valid_ta show ?thesis
    unfolding step_z_beta'_def by (blast intro: step_z_V' regions.apx_V'[OF V'_V])
qed

lemma steps_z_beta_V':
  "A  l,Z β* l',Z'  Z  V'  Z'  V'"
  by (induction rule: rtranclp_induct2; blast intro: step_z_beta'_V')

subsubsection ‹Soundness›

lemma alpha'_beta'_step:
  "A  l, Z β l', Z'  Z  V'  W  V  Z  W   W'. A  l, W α l', W'  Z'  W'"
  unfolding step_z_beta'_def step_z_alpha'_def
  apply (elim exE conjE)
  apply (frule step_z_mono, assumption)
  apply (elim exE conjE)
  apply (frule alpha_beta_step'[OF _ valid_ta])
     prefer 3
  using valid_ta by (blast intro: step_z_V' dest: step_z_V)+

lemma alpha_beta_sim:
  "Simulation_Invariant 
    (λ(l, Z) (l', Z''). A  l, Z β l', Z'')
    (λ(l, Z) (l', Z''). A  l, Z α l', Z'')
    (λ(l, Z) (l', Z'). l = l'  Z  Z') (λ(_, Z). Z  V') (λ(_, Z). Z  V)"
  by standard (auto elim: alpha'_beta'_step step_z_beta'_V' dest: step_z_alpha'_V)

interpretation
  Simulation_Invariant
  "λ (l, Z) (l', Z''). A  l, Z β l', Z''"
  "λ (l, Z) (l', Z''). A  l, Z α l', Z''"
  "λ (l, Z) (l', Z'). l = l'  Z  Z'"
  "λ (_, Z). Z  V'" "λ (_, Z). Z  V"
  by (fact alpha_beta_sim)

lemma alpha_beta_steps:
  "A  l, Z β* l', Z'  Z  V'   Z''. A  l, Z α* l', Z''  Z'  Z''"
  using simulation_reaches[of "(l, Z)" "(l', Z')" "(l, Z)"] by (auto dest: V'_V)

(*
corollary steps_z_beta_sound:
  "A ⊢ ⟨l, Z⟩ ↝β* ⟨l', Z'⟩ ⟹ ∀c∈clk_set A. v c ≤ n ⟹ valid_abstraction A X k ⟹ Z ∈ V' ⟹ Z' ≠ {}
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z''⟩ ∧ Z'' ≠ {}"
proof (goal_cases)
  case 1
  interpret regions: Regions_global _ _ _ "k l'"
    by standard (rule finite clock_numbering not_in_X non_empty)+
  from 1 have "Z ⊆ V" unfolding V'_def by auto
  from alpha_beta_steps[OF 1(1,3,2,4)] obtain Z''' where *:
    "A ⊢ ⟨l, Z⟩ ↝α* ⟨l',Z'''⟩" "Z' ⊆ Z'''"
  by blast
  from steps_z_alpha_closure_involutive[OF *(1) 1(3) ‹Z ⊆ V›] obtain Z'' where
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩" "Closureα,l' Z''' ⊆ Closureα,l' Z''" "Z'' ⊆ Z'''"
  by blast
  moreover with
    regions.alpha_interp.closure_subs[OF steps_z_alpha_V[OF *(1) ‹Z ⊆ V›]] 1(5)
    regions.alpha_interp.cla_empty_iff[OF steps_z_V, OF this(1) ‹Z ⊆ V›] *(2)
  have "Z'' ≠ {}" by auto
  ultimately show ?thesis by auto
qed
*)

end (* Valid TA *)

subsubsection ‹Completeness›

lemma step_z_beta_mono:
  "A  l, Z ↝⇘β(a)l', Z'  Z  W  W  V   W'. A  l, W ↝⇘β(a)l', W'  Z'  W'"
proof (goal_cases)
  case 1
  then obtain Z'' where *: "A  l, Z ↝⇘al',Z''" "Z' = Approxβ l' Z''" by auto
  from step_z_mono[OF this(1) 1(2)] obtain W' where
    "A  l, W ↝⇘al',W'" "Z''  W'"
  by auto
  moreover with *(2) apx_mono[OF step_z_V] W  V have
    "Z'  Approxβ l' W'"
  by metis
  ultimately show ?case by blast
qed

lemma step_z_beta'_V:
  "Z'  V" if "A  l, Z β l', Z'" "Z  V"
proof -
  interpret regions: Regions_global _ _ _ "k l'"
    by standard (rule finite clock_numbering not_in_X non_empty)+
  from that show ?thesis unfolding step_z_beta'_def
    by (auto intro: regions.apx_V dest: step_z_V del: subsetI)
qed

lemma steps_z_beta_V:
  "Z'  V" if "A  l, Z β* l', Z'" "Z  V"
  using that by (induction rule: rtranclp_induct2; blast intro: step_z_beta'_V del: subsetI)

lemma step_z_beta'_mono:
  " W'. A  l, W β l', W'  Z'  W'" if "A  l, Z β l', Z'" "Z  W" "W  V"
  using that unfolding step_z_beta'_def
  apply (elim exE conjE)
  apply (frule step_z_mono, assumption)
  apply (elim exE conjE)
  apply (drule step_z_beta_mono, assumption)
   apply (auto dest: step_z_V)
  done
(*
lemma steps_z_beta_V: "A ⊢ ⟨l, Z⟩ ↝β* ⟨l', Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
proof (induction rule: steps_z_beta.induct)
  case refl then show ?case by blast
next
  case (step A l Z l' Z' Z'' a l'' Z''')
  interpret regions: Regions_global _ _ _ "k l''"
    by standard (rule finite clock_numbering not_in_X non_empty)+
  from step have "Z'' ⊆ V" by (metis step_z_V)
  from step obtain W''' where "A ⊢ ⟨l', Z''⟩ ↝↿a ⟨l'', W'''⟩" "Z''' = Approxβ l'' W'''" by auto
  with ‹Z'' ⊆ V› show ?case by (metis regions.apx_V step_z_V)
qed
*)



lemma steps_z_beta_mono:
  "A  l, Z β* l', Z'  Z  W  W  V   W'. A  l, W β* l', W'  Z'  W'"
  apply (induction rule: rtranclp_induct2)
   apply blast
  apply (clarsimp; drule step_z_beta'_mono;
      blast intro: rtranclp.intros(2) steps_z_beta_V del: subsetI)
  done

(*
lemma steps_z_beta_complete:
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝β* ⟨l',Z''⟩ ∧ Z' ⊆ Z''"
proof (induction rule: steps_z.induct)
  case refl show ?case by blas
next
  case (step A l Z l' Z' a l'' Z'' l''' Z''')
  interpret regions: Regions_global _ _ _ "k l''"
    by standard (rule finite clock_numbering not_in_X non_empty)+
  from step_z_V[OF step(2) step_z_V[OF step(1,6)]] have "Z'' ⊆ V" .
  with step obtain W''' where W'':
    "A ⊢ ⟨l'', Z''⟩ ↝β* ⟨l''', W'''⟩" "Z''' ⊆ W'''"
    by blast
  with steps_z_beta_mono[OF W''(1) regions.beta_interp.apx_subset regions.apx_V[OF ‹Z'' ⊆ V›]]
  obtain W4 where
    "A ⊢ ⟨l'', Approxβ l'' Z''⟩ ↝β* ⟨l''', W4⟩" "W''' ⊆ W4"
    by auto
  with step(1,2) have "A ⊢ ⟨l, Z⟩ ↝β* ⟨l''', W4⟩"
    by (blast intro: steps_z_beta_alt elim!: step_z.cases)
  with ‹Z''' ⊆ W'''› ‹W''' ⊆ W4› show ?case by auto
qed

lemma steps_z_beta_complete':
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝β* ⟨l',Z''⟩ ∧ Z'' ≠ {}"
using steps_z_beta_complete by blast
*)

end (* End of locale for local regions *)

end (* End of Theory *)