# 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 (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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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 ```