Theory Constant_Folding

section‹Constant Folding›
theory Constant_Folding
imports
  Solidity_Main 
begin

text‹
  The following function optimizes expressions w.r.t. gas consumption.
›
primrec eupdate :: "E ⇒ E"
and lupdate :: "L ⇒ L"
where
  "lupdate (Id i) = Id i"
| "lupdate (Ref i exp) = Ref i (map eupdate exp)"
| "eupdate (E.INT b v) =
    (if (b∈vbits)
      then if v ≥ 0
        then E.INT b (-(2^(b-1)) + (v+2^(b-1)) mod (2^b))
        else E.INT b (2^(b-1) - (-v+2^(b-1)-1) mod (2^b) - 1)
      else E.INT b v)"
| "eupdate (UINT b v) = (if (b∈vbits) then UINT b (v mod (2^b)) else UINT b v)"
| "eupdate (ADDRESS a) = ADDRESS a"
| "eupdate (BALANCE a) = BALANCE a"
| "eupdate THIS = THIS"
| "eupdate SENDER = SENDER"
| "eupdate VALUE = VALUE"
| "eupdate TRUE = TRUE"
| "eupdate FALSE = FALSE"
| "eupdate (LVAL l) = LVAL (lupdate l)"
| "eupdate (PLUS ex1 ex2) =
    (case (eupdate ex1) of
      E.INT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            E.INT b2 v2 ⇒
              if b2∈vbits
                then let v=v1+v2 in
                  if v ≥ 0
                    then E.INT (max b1 b2) (-(2^((max b1 b2)-1)) + (v+2^((max b1 b2)-1)) mod (2^(max b1 b2)))
                    else E.INT (max b1 b2) (2^((max b1 b2)-1) - (-v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1)
                else (PLUS (E.INT b1 v1) (E.INT b2 v2))
          | UINT b2 v2 ⇒
              if b2∈vbits ∧ b2 < b1
                then let v=v1+v2 in
                  if v ≥ 0
                    then E.INT b1 (-(2^(b1-1)) + (v+2^(b1-1)) mod (2^b1))
                    else E.INT b1 (2^(b1-1) - (-v+2^(b1-1)-1) mod (2^b1) - 1)
                else PLUS (E.INT b1 v1) (UINT b2 v2)
          | _ ⇒ PLUS (E.INT b1 v1) (eupdate ex2))
        else PLUS (E.INT b1 v1) (eupdate ex2)
    | UINT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            UINT b2 v2 ⇒
              if b2 ∈ vbits
                then UINT (max b1 b2) ((v1 + v2) mod (2^(max b1 b2)))
                else (PLUS (UINT b1 v1) (UINT b2 v2))
          | E.INT b2 v2 ⇒
              if b2∈vbits ∧ b1 < b2
                then let v=v1+v2 in
                  if v ≥ 0
                    then E.INT b2 (-(2^(b2-1)) + (v+2^(b2-1)) mod (2^b2))
                    else E.INT b2 (2^(b2-1) - (-v+2^(b2-1)-1) mod (2^b2) - 1)
                else PLUS (UINT b1 v1) (E.INT b2 v2)
          | _ ⇒ PLUS (UINT b1 v1) (eupdate ex2))
        else PLUS (UINT b1 v1) (eupdate ex2)
    | _ ⇒ PLUS (eupdate ex1) (eupdate ex2))"
| "eupdate (MINUS ex1 ex2) =
    (case (eupdate ex1) of
      E.INT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            E.INT b2 v2 ⇒
              if b2∈vbits
                then let v=v1-v2 in
                  if v ≥ 0
                    then E.INT (max b1 b2) (-(2^((max b1 b2)-1)) + (v+2^((max b1 b2)-1)) mod (2^(max b1 b2)))
                    else E.INT (max b1 b2) (2^((max b1 b2)-1) - (-v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1)
                else (MINUS (E.INT b1 v1) (E.INT b2 v2))
          | UINT b2 v2 ⇒
              if b2∈vbits ∧ b2 < b1
                then let v=v1-v2 in
                  if v ≥ 0
                    then E.INT b1 (-(2^(b1-1)) + (v+2^(b1-1)) mod (2^b1))
                    else E.INT b1 (2^(b1-1) - (-v+2^(b1-1)-1) mod (2^b1) - 1)
                else MINUS (E.INT b1 v1) (UINT b2 v2)
          | _ ⇒ MINUS (E.INT b1 v1) (eupdate ex2))
        else MINUS (E.INT b1 v1) (eupdate ex2)
    | UINT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            UINT b2 v2 ⇒
              if b2 ∈ vbits
                then UINT (max b1 b2) ((v1 - v2) mod (2^(max b1 b2)))
                else (MINUS (UINT b1 v1) (UINT b2 v2))
          | E.INT b2 v2 ⇒
              if b2∈vbits ∧ b1 < b2
                then let v=v1-v2 in
                  if v ≥ 0
                    then E.INT b2 (-(2^(b2-1)) + (v+2^(b2-1)) mod (2^b2))
                    else E.INT b2 (2^(b2-1) - (-v+2^(b2-1)-1) mod (2^b2) - 1)
                else MINUS (UINT b1 v1) (E.INT b2 v2)
          | _ ⇒ MINUS (UINT b1 v1) (eupdate ex2))
        else MINUS (UINT b1 v1) (eupdate ex2)
    | _ ⇒ MINUS (eupdate ex1) (eupdate ex2))"
| "eupdate (EQUAL ex1 ex2) =
    (case (eupdate ex1) of
      E.INT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            E.INT b2 v2 ⇒
              if b2∈vbits
                then if v1 = v2
                  then TRUE
                  else FALSE
                else EQUAL (E.INT b1 v1) (E.INT b2 v2)
          | UINT b2 v2 ⇒
              if b2∈vbits ∧ b2 < b1
                then if v1 = v2
                  then TRUE
                  else FALSE
                else EQUAL (E.INT b1 v1) (UINT b2 v2)
          | _ ⇒ EQUAL (E.INT b1 v1) (eupdate ex2))
        else EQUAL (E.INT b1 v1) (eupdate ex2)
    | UINT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            UINT b2 v2 ⇒
              if b2 ∈ vbits
                then if v1 = v2
                  then TRUE
                  else FALSE
                else EQUAL (E.INT b1 v1) (UINT b2 v2)
          | E.INT b2 v2 ⇒
              if b2∈vbits ∧ b1 < b2
                then if v1 = v2
                    then TRUE
                    else FALSE
                else EQUAL (UINT b1 v1) (E.INT b2 v2)
          | _ ⇒ EQUAL (UINT b1 v1) (eupdate ex2))
        else EQUAL (UINT b1 v1) (eupdate ex2)
    | _ ⇒ EQUAL (eupdate ex1) (eupdate ex2))"
| "eupdate (LESS ex1 ex2) =
    (case (eupdate ex1) of
      E.INT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            E.INT b2 v2 ⇒
              if b2∈vbits
                then if v1 < v2
                  then TRUE
                  else FALSE
                else LESS (E.INT b1 v1) (E.INT b2 v2)
          | UINT b2 v2 ⇒
              if b2∈vbits ∧ b2 < b1
                then if v1 < v2
                  then TRUE
                  else FALSE
                else LESS (E.INT b1 v1) (UINT b2 v2)
          | _ ⇒ LESS (E.INT b1 v1) (eupdate ex2))
        else LESS (E.INT b1 v1) (eupdate ex2)
    | UINT b1 v1 ⇒
        if b1 ∈ vbits
          then (case (eupdate ex2) of
            UINT b2 v2 ⇒
              if b2 ∈ vbits
                then if v1 < v2
                  then TRUE
                  else FALSE
                else LESS (E.INT b1 v1) (UINT b2 v2)
          | E.INT b2 v2 ⇒
              if b2∈vbits ∧ b1 < b2
                then if v1 < v2
                    then TRUE
                    else FALSE
                else LESS (UINT b1 v1) (E.INT b2 v2)
          | _ ⇒ LESS (UINT b1 v1) (eupdate ex2))
        else LESS (UINT b1 v1) (eupdate ex2)
    | _ ⇒ LESS (eupdate ex1) (eupdate ex2))"
| "eupdate (AND ex1 ex2) =
    (case (eupdate ex1) of
      TRUE ⇒ (case (eupdate ex2) of
                TRUE ⇒ TRUE
              | FALSE ⇒ FALSE
              | _ ⇒ AND TRUE (eupdate ex2))
    | FALSE ⇒ (case (eupdate ex2) of
                TRUE ⇒ FALSE
              | FALSE ⇒ FALSE
              | _ ⇒ AND FALSE (eupdate ex2))
    | _ ⇒ AND (eupdate ex1) (eupdate ex2))"
| "eupdate (OR ex1 ex2) =
    (case (eupdate ex1) of
      TRUE ⇒ (case (eupdate ex2) of
                TRUE ⇒ TRUE
              | FALSE ⇒ TRUE
              | _ ⇒ OR TRUE (eupdate ex2))
    | FALSE ⇒ (case (eupdate ex2) of
                TRUE ⇒ TRUE
              | FALSE ⇒ FALSE
              | _ ⇒ OR FALSE (eupdate ex2))
    | _ ⇒ OR (eupdate ex1) (eupdate ex2))"
| "eupdate (NOT ex1) =
    (case (eupdate ex1) of
      TRUE ⇒ FALSE
    | FALSE ⇒ TRUE
    | _ ⇒ NOT (eupdate ex1))"
| "eupdate (CALL i xs) = CALL i xs"
| "eupdate (ECALL e i xs r) = ECALL e i xs r"

value "eupdate (UINT 8 250)"
lemma "eupdate (UINT 8 250)
      =UINT 8 250"
  by(simp)
lemma "eupdate (UINT 8 500)
      = UINT 8 244"
  by(simp)
lemma "eupdate (E.INT 8 (-100))
      = E.INT 8 (- 100)"
  by(simp)
lemma "eupdate (E.INT 8 (-150))
      = E.INT 8 106"
  by(simp)
lemma "eupdate (PLUS (UINT 8 100) (UINT 8 100))
      = UINT 8 200"
  by(simp)
lemma "eupdate (PLUS (UINT 8 257) (UINT 16 100))
      = UINT 16 101"
  by(simp)
lemma "eupdate (PLUS (E.INT 8 100) (UINT 8 250)) 
      = PLUS (E.INT 8 100) (UINT 8 250)"
  by(simp)
lemma  "eupdate (PLUS (E.INT 8 250) (UINT 8 500)) 
      = PLUS (E.INT 8 (- 6)) (UINT 8 244)"
  by(simp)
lemma "eupdate (PLUS (E.INT 16 250) (UINT 8 500)) 
      = E.INT 16 494"
  by(simp)
lemma "eupdate (EQUAL (UINT 16 250) (UINT 8 250))
      = TRUE"
  by(simp)
lemma  "eupdate (EQUAL (E.INT 16 100) (UINT 8 100))
      = TRUE"
  by(simp)
lemma "eupdate (EQUAL (E.INT 8 100) (UINT 8 100)) 
      = EQUAL (E.INT 8 100) (UINT 8 100)"
  by(simp)

lemma update_bounds_int:
  assumes "eupdate ex = (E.INT b v)" and "b∈vbits"
  shows "(v < 2^(b-1)) ∧ v ≥ -(2^(b-1))"
proof (cases ex)
  case (INT b' v')
  then show ?thesis
  proof cases
    assume "b'∈vbits"
    show ?thesis
    proof cases
      let ?x="-(2^(b'-1)) + (v'+2^(b'-1)) mod 2^b'"
      assume "v'≥0"
      with `b'∈vbits` have "eupdate (E.INT b' v') = E.INT b' ?x" by simp
      with assms have "b=b'" and "v=?x" using INT by (simp,simp)
      moreover from `b'∈vbits` have "b'>0" by auto
      hence "?x < 2 ^(b'-1)" using upper_bound2[of b' "(v' + 2 ^ (b' - 1)) mod 2^b'"] by simp
      moreover have "?x ≥ -(2^(b'-1))" by simp
      ultimately show ?thesis by simp
    next
      let ?x="2^(b'-1) - (-v'+2^(b'-1)-1) mod (2^b') - 1"
      assume "¬v'≥0"
      with `b'∈vbits` have "eupdate (E.INT b' v') = E.INT b' ?x" by simp
      with assms have "b=b'" and "v=?x" using INT by (simp,simp)
      moreover have "(-v'+2^(b'-1)-1) mod (2^b')≥0" by simp
      hence "?x < 2 ^(b'-1)" by arith
      moreover from `b'∈vbits` have "b'>0" by auto
      hence "?x ≥ -(2^(b'-1))" using lower_bound2[of b' v'] by simp
      ultimately show ?thesis by simp
    qed
  next
    assume "¬ b'∈vbits"
    with assms show ?thesis using INT by simp
  qed
next
  case (UINT b' v')
  with assms show ?thesis
  proof cases
    assume "b'∈vbits"
    with assms show ?thesis using UINT by simp
  next
    assume "¬ b'∈vbits"
    with assms show ?thesis using UINT by simp
  qed
next
  case (ADDRESS x3)
  with assms show ?thesis by simp
next
  case (BALANCE x4)
  with assms show ?thesis by simp
next
  case THIS
  with assms show ?thesis by simp
next
  case SENDER
  with assms show ?thesis by simp
next
  case VALUE
  with assms show ?thesis by simp
next
  case TRUE
  with assms show ?thesis by simp
next
  case FALSE
  with assms show ?thesis by simp
next
  case (LVAL x7)
  with assms show ?thesis by simp
next
  case p: (PLUS e1 e2)
  show ?thesis
  proof (cases "eupdate e1")
    case i: (INT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i2: (INT b2 v2)
        then show ?thesis
        proof cases
          let ?v="v1+v2"
          assume "b2∈vbits"
          show ?thesis
          proof cases
            let ?x="-(2^((max b1 b2)-1)) + (?v+2^((max b1 b2)-1)) mod 2^(max b1 b2)"
            assume "?v≥0"
            with `b1∈vbits` `b2∈vbits` i i2 have "eupdate (PLUS e1 e2) = E.INT (max b1 b2) ?x" by simp
            with assms have "b=max b1 b2" and "v=?x" using p by (simp,simp)
            moreover from `b1∈vbits` have "max b1 b2>0" by auto
            hence "?x < 2 ^(max b1 b2 - 1)"
              using upper_bound2[of "max b1 b2" "(?v + 2 ^ (max b1 b2 - 1)) mod 2^max b1 b2"] by simp
            moreover have "?x ≥ -(2^(max b1 b2-1))" by simp
            ultimately show ?thesis by simp
          next
            let ?x="2^((max b1 b2)-1) - (-?v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1"
            assume "¬?v≥0"
            with `b1∈vbits` `b2∈vbits` i i2 have "eupdate (PLUS e1 e2) = E.INT (max b1 b2) ?x" by simp
            with assms have "b=max b1 b2" and "v=?x" using p by (simp,simp)
            moreover have "(-?v+2^(max b1 b2-1)-1) mod (2^max b1 b2)≥0" by simp
            hence "?x < 2 ^(max b1 b2-1)" by arith
            moreover from `b1∈vbits` have "max b1 b2>0" by auto
            hence "?x ≥ -(2^(max b1 b2-1))" using lower_bound2[of "max b1 b2" ?v] by simp
            ultimately show ?thesis by simp
          qed
        next
          assume "b2∉vbits"
          with p i i2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u: (UINT b2 v2)
        then show ?thesis
        proof cases
          let ?v="v1+v2"
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b2<b1"
            then show ?thesis
            proof cases
              let ?x="(-(2^(b1-1)) + (?v+2^(b1-1)) mod (2^b1))"
              assume "?v≥0"
              with `b1∈vbits` `b2∈vbits` `b2<b1` i u have "eupdate (PLUS e1 e2) = E.INT b1 ?x" by simp
              with assms have "b=b1" and "v=?x" using p by (simp,simp)
              moreover from `b1∈vbits` have "b1>0" by auto
              hence "?x < 2 ^(b1 - 1)" using upper_bound2[of b1] by simp
              moreover have "?x ≥ -(2^(b1-1))" by simp
              ultimately show ?thesis by simp
            next
              let ?x="2^(b1-1) - (-?v+2^(b1-1)-1) mod (2^b1) - 1"
              assume "¬?v≥0"
              with `b1∈vbits` `b2∈vbits` `b2<b1` i u have "eupdate (PLUS e1 e2) = E.INT b1 ?x" by simp
              with assms have "b=b1" and "v=?x" using p i u by (simp,simp)
              moreover have "(-?v+2^(b1-1)-1) mod 2^b1≥0" by simp
              hence "?x < 2 ^(b1-1)" by arith
              moreover from `b1∈vbits` have "b1>0" by auto
              hence "?x ≥ -(2^(b1-1))" using lower_bound2[of b1 ?v] by simp
              ultimately show ?thesis by simp
            qed
          next
            assume "¬ b2<b1"
            with p i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with p i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with p i `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with p i `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with p i show ?thesis using assms by simp
    qed
  next
    case u: (UINT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i: (INT b2 v2)
        then show ?thesis
        proof cases
          let ?v="v1+v2"
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b1<b2"
            then show ?thesis
            proof cases
              let ?x="(-(2^(b2-1)) + (?v+2^(b2-1)) mod (2^b2))"
              assume "?v≥0"
              with `b1∈vbits` `b2∈vbits` `b1<b2` i u have "eupdate (PLUS e1 e2) = E.INT b2 ?x" by simp
              with assms have "b=b2" and "v=?x" using p by (simp,simp)
              moreover from `b2∈vbits` have "b2>0" by auto
              hence "?x < 2 ^(b2 - 1)" using upper_bound2[of b2] by simp
              moreover have "?x ≥ -(2^(b2-1))" by simp
              ultimately show ?thesis by simp
            next
              let ?x="2^(b2-1) - (-?v+2^(b2-1)-1) mod (2^b2) - 1"
              assume "¬?v≥0"
              with `b1∈vbits` `b2∈vbits` `b1<b2` i u have "eupdate (PLUS e1 e2) = E.INT b2 ?x" by simp
              with assms have "b=b2" and "v=?x" using p i u by (simp,simp)
              moreover have "(-?v+2^(b2-1)-1) mod 2^b2≥0" by simp
              hence "?x < 2 ^(b2-1)" by arith
              moreover from `b2∈vbits` have "b2>0" by auto
              hence "?x ≥ -(2^(b2-1))" using lower_bound2[of b2 ?v] by simp
              ultimately show ?thesis by simp
            qed
          next
            assume "¬ b1<b2"
            with p i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with p i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u2: (UINT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          with `b1∈vbits` u u2 p show ?thesis using assms by simp
        next
          assume "¬b2∈vbits"
          with p u u2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with p u `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with p u `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with p u show ?thesis using assms by simp
    qed
  next
    case (ADDRESS x3)
    with p show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with p show ?thesis using assms by simp
  next
    case THIS
    with p show ?thesis using assms by simp
  next
    case SENDER
    with p show ?thesis using assms by simp
  next
    case VALUE
    with p show ?thesis using assms by simp
  next
    case TRUE
    with p show ?thesis using assms by simp
  next
    case FALSE
    with p show ?thesis using assms by simp
  next
    case (LVAL x7)
    with p show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with p show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with p show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with p show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with p show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with p show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with p show ?thesis using assms by simp
  next
    case (NOT x131)
    with p show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with p show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with p show ?thesis using assms by simp
  qed
next
  case m: (MINUS e1 e2)
  show ?thesis
  proof (cases "eupdate e1")
    case i: (INT b1 v1)
    with m show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i2: (INT b2 v2)
        then show ?thesis
        proof cases
          let ?v="v1-v2"
          assume "b2∈vbits"
          with `b1 ∈ vbits` have
            u_def: "eupdate (MINUS e1 e2) =
            (let v = v1 - v2
              in if 0 ≤ v
                then E.INT (max b1 b2)
                  (- (2 ^ (max b1 b2 - 1)) + (v + 2 ^ (max b1 b2 - 1)) mod 2 ^ max b1 b2)
                else E.INT (max b1 b2)
                  (2 ^ (max b1 b2 - 1) - (- v + 2 ^ (max b1 b2 - 1) - 1) mod 2 ^ max b1 b2 - 1))"
            using i i2 eupdate.simps(11)[of e1 e2] by simp
          show ?thesis
          proof cases
            let ?x="-(2^((max b1 b2)-1)) + (?v+2^((max b1 b2)-1)) mod 2^(max b1 b2)"
            assume "?v≥0"
            with u_def have "eupdate (MINUS e1 e2) = E.INT (max b1 b2) ?x" by simp
            with assms have "b=max b1 b2" and "v=?x" using m by (simp,simp)
            moreover from `b1∈vbits` have "max b1 b2>0" by auto
            hence "?x < 2 ^(max b1 b2 - 1)"
              using upper_bound2[of "max b1 b2" "(?v + 2 ^ (max b1 b2 - 1)) mod 2^max b1 b2"] by simp
            moreover have "?x ≥ -(2^(max b1 b2-1))" by simp
            ultimately show ?thesis by simp
          next
            let ?x="2^((max b1 b2)-1) - (-?v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1"
            assume "¬?v≥0"
            with u_def have "eupdate (MINUS e1 e2) = E.INT (max b1 b2) ?x" using u_def by simp
            with assms have "b=max b1 b2" and "v=?x" using m by (simp,simp)
            moreover have "(-?v+2^(max b1 b2-1)-1) mod (2^max b1 b2)≥0" by simp
            hence "?x < 2 ^(max b1 b2-1)" by arith
            moreover from `b1∈vbits` have "max b1 b2>0" by auto
            hence "?x ≥ -(2^(max b1 b2-1))" using lower_bound2[of "max b1 b2" ?v] by simp
            ultimately show ?thesis by simp
          qed
        next
          assume "b2∉vbits"
          with m i i2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u: (UINT b2 v2)
        then show ?thesis
        proof cases
          let ?v="v1-v2"
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b2<b1"
            with `b1 ∈ vbits` `b2 ∈ vbits` have
              u_def: "eupdate (MINUS e1 e2) =
              (let v = v1 - v2
                in if 0 ≤ v
                  then E.INT b1 (- (2 ^ (b1 - 1)) + (v + 2 ^ (b1 - 1)) mod 2 ^ b1)
                  else E.INT b1 (2 ^ (b1 - 1) - (- v + 2 ^ (b1 - 1) - 1) mod 2 ^ b1 - 1))"
              using i u eupdate.simps(11)[of e1 e2] by simp
            then show ?thesis
            proof cases
              let ?x="(-(2^(b1-1)) + (?v+2^(b1-1)) mod (2^b1))"
              assume "?v≥0"
              with u_def have "eupdate (MINUS e1 e2) = E.INT b1 ?x" by simp
              with assms have "b=b1" and "v=?x" using m by (simp,simp)
              moreover from `b1∈vbits` have "b1>0" by auto
              hence "?x < 2 ^(b1 - 1)" using upper_bound2[of b1] by simp
              moreover have "?x ≥ -(2^(b1-1))" by simp
              ultimately show ?thesis by simp
            next
              let ?x="2^(b1-1) - (-?v+2^(b1-1)-1) mod (2^b1) - 1"
              assume "¬?v≥0"
              with u_def have "eupdate (MINUS e1 e2) = E.INT b1 ?x" by simp
              with assms have "b=b1" and "v=?x" using m i u by (simp,simp)
              moreover have "(-?v+2^(b1-1)-1) mod 2^b1≥0" by simp
              hence "?x < 2 ^(b1-1)" by arith
              moreover from `b1∈vbits` have "b1>0" by auto
              hence "?x ≥ -(2^(b1-1))" using lower_bound2[of b1 ?v] by simp
              ultimately show ?thesis by simp
            qed
          next
            assume "¬ b2<b1"
            with m i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with m i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with m i `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with m i `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with m i show ?thesis using assms by simp
    qed
  next
    case u: (UINT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i: (INT b2 v2)
        then show ?thesis
        proof cases
          let ?v="v1-v2"
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b1<b2"
            with `b1 ∈ vbits` `b2 ∈ vbits` have
              u_def: "eupdate (MINUS e1 e2) =
              (let v = v1 - v2
                in if 0 ≤ v
                  then E.INT b2 (- (2 ^ (b2 - 1)) + (v + 2 ^ (b2 - 1)) mod 2 ^ b2)
                  else E.INT b2 (2 ^ (b2 - 1) - (- v + 2 ^ (b2 - 1) - 1) mod 2 ^ b2 - 1))"
              using i u eupdate.simps(11)[of e1 e2] by simp
            then show ?thesis
            proof cases
              let ?x="(-(2^(b2-1)) + (?v+2^(b2-1)) mod (2^b2))"
              assume "?v≥0"
              with u_def have "eupdate (MINUS e1 e2) = E.INT b2 ?x" by simp
              with assms have "b=b2" and "v=?x" using m by (simp,simp)
              moreover from `b2∈vbits` have "b2>0" by auto
              hence "?x < 2 ^(b2 - 1)" using upper_bound2[of b2] by simp
              moreover have "?x ≥ -(2^(b2-1))" by simp
              ultimately show ?thesis by simp
            next
              let ?x="2^(b2-1) - (-?v+2^(b2-1)-1) mod (2^b2) - 1"
              assume "¬?v≥0"
              with u_def have "eupdate (MINUS e1 e2) = E.INT b2 ?x" by simp
              with assms have "b=b2" and "v=?x" using m i u by (simp,simp)
              moreover have "(-?v+2^(b2-1)-1) mod 2^b2≥0" by simp
              hence "?x < 2 ^(b2-1)" by arith
              moreover from `b2∈vbits` have "b2>0" by auto
              hence "?x ≥ -(2^(b2-1))" using lower_bound2[of b2 ?v] by simp
              ultimately show ?thesis by simp
            qed
          next
            assume "¬ b1<b2"
            with m i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with m i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u2: (UINT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          with `b1∈vbits` u u2 m show ?thesis using assms by simp
        next
          assume "¬b2∈vbits"
          with m u u2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with m u `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with m u `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with m u show ?thesis using assms by simp
    qed
  next
    case (ADDRESS x3)
    with m show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with m show ?thesis using assms by simp
  next
    case THIS
    with m show ?thesis using assms by simp
  next
    case SENDER
    with m show ?thesis using assms by simp
  next
    case VALUE
    with m show ?thesis using assms by simp
  next
    case TRUE
    with m show ?thesis using assms by simp
  next
    case FALSE
    with m show ?thesis using assms by simp
  next
    case (LVAL x7)
    with m show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with m show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with m show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with m show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with m show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with m show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with m show ?thesis using assms by simp
  next
    case (NOT x131)
    with m show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with m show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with m show ?thesis using assms by simp
  qed
next
  case e: (EQUAL e1 e2)
  show ?thesis
  proof (cases "eupdate e1")
    case i: (INT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i2: (INT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "v1=v2"
            with assms show ?thesis using e i i2 `b1∈vbits` `b2∈vbits` by simp
          next
            assume "¬ v1=v2"
            with assms show ?thesis using e i i2 `b1∈vbits` `b2∈vbits` by simp
          qed
        next
          assume "b2∉vbits"
          with e i i2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u: (UINT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b2<b1"
            then show ?thesis
            proof cases
              assume "v1=v2"
              with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp
            next
              assume "¬ v1=v2"
              with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp
            qed
          next
            assume "¬ b2<b1"
            with e i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with e i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with e i `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with e i `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with e i show ?thesis using assms by simp
    qed
  next
    case u: (UINT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i: (INT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b1<b2"
            then show ?thesis
            proof cases
              assume "v1=v2"
              with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp
            next
              assume "¬ v1=v2"
              with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp
            qed
          next
            assume "¬ b1<b2"
            with e i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with e i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u2: (UINT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "v1=v2"
            with assms show ?thesis using e u u2 `b1∈vbits` `b2∈vbits` by simp
          next
            assume "¬ v1=v2"
            with assms show ?thesis using e u u2 `b1∈vbits` `b2∈vbits` by simp
          qed
        next
          assume "¬b2∈vbits"
          with e u u2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with e u `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with e u `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with e u show ?thesis using assms by simp
    qed
  next
    case (ADDRESS x3)
    with e show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with e show ?thesis using assms by simp
  next
    case THIS
    with e show ?thesis using assms by simp
  next
    case SENDER
    with e show ?thesis using assms by simp
  next
    case VALUE
    with e show ?thesis using assms by simp
  next
    case TRUE
    with e show ?thesis using assms by simp
  next
    case FALSE
    with e show ?thesis using assms by simp
  next
    case (LVAL x7)
    with e show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with e show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with e show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with e show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with e show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with e show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with e show ?thesis using assms by simp
  next
    case (NOT x131)
    with e show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with e show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with e show ?thesis using assms by simp
  qed
next
  case l: (LESS e1 e2)
  show ?thesis
  proof (cases "eupdate e1")
    case i: (INT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i2: (INT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "v1<v2"
            with assms show ?thesis using l i i2 `b1∈vbits` `b2∈vbits` by simp
          next
            assume "¬ v1<v2"
            with assms show ?thesis using l i i2 `b1∈vbits` `b2∈vbits` by simp
          qed
        next
          assume "b2∉vbits"
          with l i i2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u: (UINT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b2<b1"
            then show ?thesis
            proof cases
              assume "v1<v2"
              with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp
            next
              assume "¬ v1<v2"
              with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp
            qed
          next
            assume "¬ b2<b1"
            with l i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with l i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with l i `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with l i `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with l i show ?thesis using assms by simp
    qed
  next
    case u: (UINT b1 v1)
    show ?thesis
    proof cases
      assume "b1∈vbits"
      show ?thesis
      proof (cases "eupdate e2")
        case i: (INT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "b1<b2"
            then show ?thesis
            proof cases
              assume "v1<v2"
              with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp
            next
              assume "¬ v1<v2"
              with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp
            qed
          next
            assume "¬ b1<b2"
            with l i u `b1∈vbits` show ?thesis using assms by simp
          qed
        next
          assume "b2∉vbits"
          with l i u `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case u2: (UINT b2 v2)
        then show ?thesis
        proof cases
          assume "b2∈vbits"
          show ?thesis
          proof cases
            assume "v1<v2"
            with assms show ?thesis using l u u2 `b1∈vbits` `b2∈vbits` by simp
          next
            assume "¬ v1<v2"
            with assms show ?thesis using l u u2 `b1∈vbits` `b2∈vbits` by simp
          qed
        next
          assume "¬b2∈vbits"
          with l u u2 `b1∈vbits` show ?thesis using assms by simp
        qed
      next
        case (ADDRESS x3)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (BALANCE x4)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case THIS
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case SENDER
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case VALUE
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case TRUE
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case FALSE
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LVAL x7)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (PLUS x81 x82)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (MINUS x91 x92)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (EQUAL x101 x102)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (LESS x111 x112)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (AND x121 x122)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (OR x131 x132)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (NOT x131)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (CALL x181 x182)
        with l u `b1∈vbits` show ?thesis using assms by simp
      next
        case (ECALL x191 x192 x193 x194)
        with l u `b1∈vbits` show ?thesis using assms by simp
      qed
    next
      assume "¬ b1∈vbits"
      with l u show ?thesis using assms by simp
    qed
  next
    case (ADDRESS x3)
    with l show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with l show ?thesis using assms by simp
  next
    case THIS
    with l show ?thesis using assms by simp
  next
    case SENDER
    with l show ?thesis using assms by simp
  next
    case VALUE
    with l show ?thesis using assms by simp
  next
    case TRUE
    with l show ?thesis using assms by simp
  next
    case FALSE
    with l show ?thesis using assms by simp
  next
    case (LVAL x7)
    with l show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with l show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with l show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with l show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with l show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with l show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with l show ?thesis using assms by simp
  next
    case (NOT x131)
    with l show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with l show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with l show ?thesis using assms by simp
  qed
next
  case a: (AND e1 e2)
  show ?thesis
  proof (cases "eupdate e1")
    case (INT x11 x12)
    with a show ?thesis using assms by simp
  next
    case (UINT x21 x22)
    with a show ?thesis using assms by simp
  next
    case (ADDRESS x3)
    with a show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with a show ?thesis using assms by simp
  next
    case THIS
    with a show ?thesis using assms by simp
  next
    case SENDER
    with a show ?thesis using assms by simp
  next
    case VALUE
    with a show ?thesis using assms by simp
  next
    case t: TRUE
    show ?thesis
    proof (cases "eupdate e2")
      case (INT x11 x12)
      with a t show ?thesis using assms by simp
    next
      case (UINT x21 x22)
      with a t show ?thesis using assms by simp
    next
      case (ADDRESS x3)
      with a t show ?thesis using assms by simp
    next
      case (BALANCE x4)
      with a t show ?thesis using assms by simp
    next
      case THIS
      with a t show ?thesis using assms by simp
    next
      case SENDER
      with a t show ?thesis using assms by simp
    next
      case VALUE
      with a t show ?thesis using assms by simp
    next
      case TRUE
      with a t show ?thesis using assms by simp
    next
      case FALSE
      with a t show ?thesis using assms by simp
    next
      case (LVAL x7)
      with a t show ?thesis using assms by simp
    next
      case (PLUS x81 x82)
      with a t show ?thesis using assms by simp
    next
      case (MINUS x91 x92)
      with a t show ?thesis using assms by simp
    next
      case (EQUAL x101 x102)
      with a t show ?thesis using assms by simp
    next
      case (LESS x111 x112)
      with a t show ?thesis using assms by simp
    next
      case (AND x121 x122)
      with a t show ?thesis using assms by simp
    next
      case (OR x131 x132)
      with a t show ?thesis using assms by simp
    next
      case (NOT x131)
      with a t show ?thesis using assms by simp
    next
      case (CALL x181 x182)
      with a t show ?thesis using assms by simp
    next
      case (ECALL x191 x192 x193 x194)
      with a t show ?thesis using assms by simp
    qed
  next
    case f: FALSE
    show ?thesis
    proof (cases "eupdate e2")
      case (INT x11 x12)
      with a f show ?thesis using assms by simp
    next
      case (UINT x21 x22)
      with a f show ?thesis using assms by simp
    next
      case (ADDRESS x3)
      with a f show ?thesis using assms by simp
    next
      case (BALANCE x4)
      with a f show ?thesis using assms by simp
    next
      case THIS
      with a f show ?thesis using assms by simp
    next
      case SENDER
      with a f show ?thesis using assms by simp
    next
      case VALUE
      with a f show ?thesis using assms by simp
    next
      case TRUE
      with a f show ?thesis using assms by simp
    next
      case FALSE
      with a f show ?thesis using assms by simp
    next
      case (LVAL x7)
      with a f show ?thesis using assms by simp
    next
      case (PLUS x81 x82)
      with a f show ?thesis using assms by simp
    next
      case (MINUS x91 x92)
      with a f show ?thesis using assms by simp
    next
      case (EQUAL x101 x102)
      with a f show ?thesis using assms by simp
    next
      case (LESS x111 x112)
      with a f show ?thesis using assms by simp
    next
      case (AND x121 x122)
      with a f show ?thesis using assms by simp
    next
      case (OR x131 x132)
      with a f show ?thesis using assms by simp
    next
      case (NOT x131)
      with a f show ?thesis using assms by simp
    next
      case (CALL x181 x182)
      with a f show ?thesis using assms by simp
    next
      case (ECALL x191 x192 x193 x194)
      with a f show ?thesis using assms by simp
    qed
  next
    case (LVAL x7)
    with a show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with a show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with a show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with a show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with a show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with a show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with a show ?thesis using assms by simp
  next
    case (NOT x131)
    with a show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with a show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with a show ?thesis using assms by simp
  qed
next
  case o: (OR e1 e2)
  show ?thesis
  proof (cases "eupdate e1")
    case (INT x11 x12)
    with o show ?thesis using assms by simp
  next
    case (UINT x21 x22)
    with o show ?thesis using assms by simp
  next
    case (ADDRESS x3)
    with o show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with o show ?thesis using assms by simp
  next
    case THIS
    with o show ?thesis using assms by simp
  next
    case SENDER
    with o show ?thesis using assms by simp
  next
    case VALUE
    with o show ?thesis using assms by simp
  next
    case t: TRUE
    show ?thesis
    proof (cases "eupdate e2")
      case (INT x11 x12)
      with o t show ?thesis using assms by simp
    next
      case (UINT x21 x22)
      with o t show ?thesis using assms by simp
    next
      case (ADDRESS x3)
      with o t show ?thesis using assms by simp
    next
      case (BALANCE x4)
      with o t show ?thesis using assms by simp
    next
      case THIS
      with o t show ?thesis using assms by simp
    next
      case SENDER
      with o t show ?thesis using assms by simp
    next
      case VALUE
      with o t show ?thesis using assms by simp
    next
      case TRUE
      with o t show ?thesis using assms by simp
    next
      case FALSE
      with o t show ?thesis using assms by simp
    next
      case (LVAL x7)
      with o t show ?thesis using assms by simp
    next
      case (PLUS x81 x82)
      with o t show ?thesis using assms by simp
    next
      case (MINUS x91 x92)
      with o t show ?thesis using assms by simp
    next
      case (EQUAL x101 x102)
      with o t show ?thesis using assms by simp
    next
      case (LESS x111 x112)
      with o t show ?thesis using assms by simp
    next
      case (AND x121 x122)
      with o t show ?thesis using assms by simp
    next
      case (OR x131 x132)
      with o t show ?thesis using assms by simp
    next
      case (NOT x131)
      with o t show ?thesis using assms by simp
    next
      case (CALL x181 x182)
      with o t show ?thesis using assms by simp
    next
      case (ECALL x191 x192 x193 x194)
      with o t show ?thesis using assms by simp
    qed
  next
    case f: FALSE
    show ?thesis
    proof (cases "eupdate e2")
      case (INT x11 x12)
      with o f show ?thesis using assms by simp
    next
      case (UINT x21 x22)
      with o f show ?thesis using assms by simp
    next
      case (ADDRESS x3)
      with o f show ?thesis using assms by simp
    next
      case (BALANCE x4)
      with o f show ?thesis using assms by simp
    next
      case THIS
      with o f show ?thesis using assms by simp
    next
      case SENDER
      with o f show ?thesis using assms by simp
    next
      case VALUE
      with o f show ?thesis using assms by simp
    next
      case TRUE
      with o f show ?thesis using assms by simp
    next
      case FALSE
      with o f show ?thesis using assms by simp
    next
      case (LVAL x7)
      with o f show ?thesis using assms by simp
    next
      case (PLUS x81 x82)
      with o f show ?thesis using assms by simp
    next
      case (MINUS x91 x92)
      with o f show ?thesis using assms by simp
    next
      case (EQUAL x101 x102)
      with o f show ?thesis using assms by simp
    next
      case (LESS x111 x112)
      with o f show ?thesis using assms by simp
    next
      case (AND x121 x122)
      with o f show ?thesis using assms by simp
    next
      case (OR x131 x132)
      with o f show ?thesis using assms by simp
    next
      case (NOT x131)
      with o f show ?thesis using assms by simp
    next
      case (CALL x181 x182)
      with o f show ?thesis using assms by simp
    next
      case (ECALL x191 x192 x193 x194)
      with o f show ?thesis using assms by simp
    qed
  next
    case (LVAL x7)
    with o show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with o show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with o show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with o show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with o show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with o show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with o show ?thesis using assms by simp
  next
    case (NOT x131)
    with o show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with o show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with o show ?thesis using assms by simp
  qed
next
  case o: (NOT e1)
  show ?thesis
  proof (cases "eupdate e1")
    case (INT x11 x12)
    with o show ?thesis using assms by simp
  next
    case (UINT x21 x22)
    with o show ?thesis using assms by simp
  next
    case (ADDRESS x3)
    with o show ?thesis using assms by simp
  next
    case (BALANCE x4)
    with o show ?thesis using assms by simp
  next
    case THIS
    with o show ?thesis using assms by simp
  next
    case SENDER
    with o show ?thesis using assms by simp
  next
    case VALUE
    with o show ?thesis using assms by simp
  next
    case t: TRUE
    with o show ?thesis using assms by simp
  next
    case f: FALSE
    with o show ?thesis using assms by simp
  next
    case (LVAL x7)
    with o show ?thesis using assms by simp
  next
    case (PLUS x81 x82)
    with o show ?thesis using assms by simp
  next
    case (MINUS x91 x92)
    with o show ?thesis using assms by simp
  next
    case (EQUAL x101 x102)
    with o show ?thesis using assms by simp
  next
    case (LESS x111 x112)
    with o show ?thesis using assms by simp
  next
    case (AND x121 x122)
    with o show ?thesis using assms by simp
  next
    case (OR x131 x132)
    with o show ?thesis using assms by simp
  next
    case (NOT x131)
    with o show ?thesis using assms by simp
  next
    case (CALL x181 x182)
    with o show ?thesis using assms by simp
  next
    case (ECALL x191 x192 x193 x194)
    with o show ?thesis using assms by simp
  qed
next
  case (CALL x181 x182)
  with assms show ?thesis by simp
next
  case (ECALL x191 x192 x193 x194)
  with assms show ?thesis by simp
qed

lemma update_bounds_uint:
  assumes "eupdate ex = UINT b v" and "b∈vbits"
  shows "v < 2^b ∧ v ≥ 0"
proof (cases ex)
  case (INT b' v')
  with assms show ?thesis
  proof cases
    assume "b'∈vbits"
    show ?thesis
    proof cases
      assume "v'≥0"
      with INT show ?thesis using assms `b'∈vbits` by simp
    next
      assume "¬ v'≥0"
      with INT show ?thesis using assms `b'∈vbits` by simp
    qed
  next
    assume "¬ b'∈vbits"
    with INT show ?thesis using assms by simp
  qed
next
  case (UINT b' v')
  then show ?thesis
  proof cases
    assume "b'∈vbits"
    with UINT show ?thesis using assms by auto
  next
    assume "¬ b'∈vbits"
    with UINT show ?thesis using assms by auto
  qed
next
  case (ADDRESS x3)
  with assms show ?thesis by simp
next
  case (BALANCE x4)
  with assms show ?thesis by simp
next
  case THIS
  with assms show ?thesis by simp
next
  case SENDER
  with assms show ?thesis by simp
next
  case VALUE
  with assms show ?thesis by simp
next
  case TRUE
  with assms show ?thesis by simp
next
  case FALSE
  with assms show ?thesis by simp
next
  case (LVAL x7)
  with assms show ?thesis by