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,