Theory BinOp

(*  Title:      JinjaThreads/Common/BinOp.thy
    Author:     Andreas Lochbihler
*)

section ‹Binary Operators›

theory BinOp
imports
  WellForm "Word_Lib.Bit_Shifts_Infix_Syntax"
begin

datatype bop =  ― ‹names of binary operations›
    Eq
  | NotEq
  | LessThan
  | LessOrEqual
  | GreaterThan
  | GreaterOrEqual
  | Add    
  | Subtract
  | Mult
  | Div
  | Mod
  | BinAnd
  | BinOr
  | BinXor
  | ShiftLeft
  | ShiftRightZeros
  | ShiftRightSigned

subsection‹The semantics of binary operators›

context
  includes bit_operations_syntax
begin

type_synonym 'addr binop_ret = "'addr val + 'addr" ― ‹a value or the address of an exception›

fun binop_LessThan :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_LessThan (Intg i1) (Intg i2) = Some (Inl (Bool (i1 <s i2)))"
| "binop_LessThan v1 v2 = None"

fun binop_LessOrEqual :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_LessOrEqual (Intg i1) (Intg i2) = Some (Inl (Bool (i1 <=s i2)))"
| "binop_LessOrEqual v1 v2 = None"

fun binop_GreaterThan :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_GreaterThan (Intg i1) (Intg i2) = Some (Inl (Bool (i2 <s i1)))"
| "binop_GreaterThan v1 v2 = None"

fun binop_GreaterOrEqual :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_GreaterOrEqual (Intg i1) (Intg i2) = Some (Inl (Bool (i2 <=s i1)))"
| "binop_GreaterOrEqual v1 v2 = None"

fun binop_Add :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_Add (Intg i1) (Intg i2) = Some (Inl (Intg (i1 + i2)))"
| "binop_Add v1 v2 = None"

fun binop_Subtract :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_Subtract (Intg i1) (Intg i2) = Some (Inl (Intg (i1 - i2)))"
| "binop_Subtract v1 v2 = None"

fun binop_Mult :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_Mult (Intg i1) (Intg i2) = Some (Inl (Intg (i1 * i2)))"
| "binop_Mult v1 v2 = None"

fun binop_BinAnd :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_BinAnd (Intg i1) (Intg i2) = Some (Inl (Intg (i1 AND i2)))"
| "binop_BinAnd (Bool b1) (Bool b2) = Some (Inl (Bool (b1 ∧ b2)))"
| "binop_BinAnd v1 v2 = None"

fun binop_BinOr :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_BinOr (Intg i1) (Intg i2) = Some (Inl (Intg (i1 OR i2)))"
| "binop_BinOr (Bool b1) (Bool b2) = Some (Inl (Bool (b1 ∨ b2)))"
| "binop_BinOr v1 v2 = None"

fun binop_BinXor :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_BinXor (Intg i1) (Intg i2) = Some (Inl (Intg (i1 XOR i2)))"
| "binop_BinXor (Bool b1) (Bool b2) = Some (Inl (Bool (b1 ≠ b2)))"
| "binop_BinXor v1 v2 = None"

fun binop_ShiftLeft :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_ShiftLeft (Intg i1) (Intg i2) = Some (Inl (Intg (i1 << unat (i2 AND 0x1f))))"
| "binop_ShiftLeft v1 v2 = None"

fun binop_ShiftRightZeros :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_ShiftRightZeros (Intg i1) (Intg i2) = Some (Inl (Intg (i1 >> unat (i2 AND 0x1f))))"
| "binop_ShiftRightZeros v1 v2 = None"

fun binop_ShiftRightSigned :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_ShiftRightSigned (Intg i1) (Intg i2) = Some (Inl (Intg (i1 >>> unat (i2 AND 0x1f))))"
| "binop_ShiftRightSigned v1 v2 = None"

text ‹
  Division on @{typ "'a word"} is unsigned, but JLS specifies signed division.
›
definition word_sdiv :: "'a :: len word ⇒ 'a word ⇒ 'a word" (infixl ‹sdiv› 70)
where [code]:
  "x sdiv y =
   (let x' = sint x; y' = sint y;
        negative = (x' < 0) ≠ (y' < 0);
        result = abs x' div abs y'
    in word_of_int (if negative then -result else result))"

definition word_smod :: "'a :: len word ⇒ 'a word ⇒ 'a word" (infixl ‹smod› 70)
where [code]:
  "x smod y =
   (let x' = sint x; y' = sint y;
        negative = (x' < 0);
        result = abs x' mod abs y'
    in word_of_int (if negative then -result else result))"

declare word_sdiv_def [simp] word_smod_def [simp]

lemma sdiv_smod_id: "(a sdiv b) * b + (a smod b) = a"
proof -
  have F5: "∀u::'a word. - (- u) = u"
    by simp
  have F7: "∀v u::'a word. u + v = v + u"
    by (simp add: ac_simps)
  have F8: "∀(w::'a word) (v::int) u::int. word_of_int u + word_of_int v * w = word_of_int (u + v * sint w)"
    by simp
  have "∃u. u = - sint b ∧ word_of_int (sint a mod u + - (- u * (sint a div u))) = a"
    using F5 by simp
  hence "word_of_int (sint a mod - sint b + - (sint b * (sint a div - sint b))) = a"
    by (metis equation_minus_iff)
  hence "word_of_int (sint a mod - sint b) + word_of_int (- (sint a div - sint b)) * b = a"
    using F8 by (simp add: ac_simps)
  hence eq: "word_of_int (- (sint a div - sint b)) * b + word_of_int (sint a mod - sint b) = a"
    using F7 by simp

  show ?thesis
  proof(cases "sint a < 0")
    case True note a = this
    show ?thesis
    proof(cases "sint b < 0")
      case True
      with a show ?thesis
        by simp (metis F7 F8 eq minus_equation_iff minus_mult_minus mod_div_mult_eq)
    next
      case False
      from eq have "word_of_int (- (- sint a div sint b)) * b + word_of_int (- (- sint a mod sint b)) = a"
        by (metis div_minus_right mod_minus_right)
      with a False show ?thesis by simp
    qed
  next
    case False note a = this
    show ?thesis
    proof(cases "sint b < 0")
      case True
      with a eq show ?thesis by simp
    next
      case False with a show ?thesis
        by (simp add: F7 F8)
    qed
  qed
qed

end

notepad begin
have  "  5  sdiv ( 3 :: word32) =  1"
  and "  5  smod ( 3 :: word32) =  2"
  and "  5  sdiv (-3 :: word32) = -1"
  and "  5  smod (-3 :: word32) =  2"
  and "(-5) sdiv ( 3 :: word32) = -1"
  and "(-5) smod ( 3 :: word32) = -2"
  and "(-5) sdiv (-3 :: word32) =  1"
  and "(-5) smod (-3 :: word32) = -2"
  and "-2147483648 sdiv 1 = (-2147483648 :: word32)"
  by eval+
end

context heap_base
begin

fun binop_Mod :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_Mod (Intg i1) (Intg i2) = 
   Some (if i2 = 0 then Inr (addr_of_sys_xcpt ArithmeticException) else Inl (Intg (i1 smod i2)))"
| "binop_Mod v1 v2 = None"

fun binop_Div :: "'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop_Div (Intg i1) (Intg i2) = 
   Some (if i2 = 0 then Inr (addr_of_sys_xcpt ArithmeticException) else Inl (Intg (i1 sdiv i2)))"
| "binop_Div v1 v2 = None"

primrec binop :: "bop ⇒ 'addr val ⇒ 'addr val ⇒ 'addr binop_ret option"
where
  "binop Eq v1 v2 =  Some (Inl (Bool (v1 = v2)))"
| "binop NotEq v1 v2 = Some (Inl (Bool (v1 ≠ v2)))"
| "binop LessThan = binop_LessThan"
| "binop LessOrEqual = binop_LessOrEqual"
| "binop GreaterThan = binop_GreaterThan"
| "binop GreaterOrEqual = binop_GreaterOrEqual"
| "binop Add = binop_Add"
| "binop Subtract = binop_Subtract"
| "binop Mult = binop_Mult"
| "binop Mod = binop_Mod"
| "binop Div = binop_Div"
| "binop BinAnd = binop_BinAnd"
| "binop BinOr = binop_BinOr"
| "binop BinXor = binop_BinXor"
| "binop ShiftLeft = binop_ShiftLeft"
| "binop ShiftRightZeros = binop_ShiftRightZeros"
| "binop ShiftRightSigned = binop_ShiftRightSigned"

end

context
  includes bit_operations_syntax
begin

lemma [simp]:
  "(binop_LessThan v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Bool (i1 <s i2)))"
by(cases "(v1, v2)" rule: binop_LessThan.cases) auto

lemma [simp]:
  "(binop_LessOrEqual v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Bool (i1 <=s i2)))"
by(cases "(v1, v2)" rule: binop_LessOrEqual.cases) auto

lemma [simp]:
  "(binop_GreaterThan v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Bool (i2 <s i1)))"
by(cases "(v1, v2)" rule: binop_GreaterThan.cases) auto

lemma [simp]:
  "(binop_GreaterOrEqual v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Bool (i2 <=s i1)))"
by(cases "(v1, v2)" rule: binop_GreaterOrEqual.cases) auto

lemma [simp]:
  "(binop_Add v1 v2  = Some va) ⟷
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1+i2)))"
by(cases "(v1, v2)" rule: binop_Add.cases) auto

lemma [simp]:
  "(binop_Subtract v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 - i2)))"
by(cases "(v1, v2)" rule: binop_Subtract.cases) auto

lemma [simp]: 
  "(binop_Mult v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 * i2)))"
by(cases "(v1, v2)" rule: binop_Mult.cases) auto

lemma [simp]:
  "(binop_BinAnd v1 v2 = Some va) ⟷ 
   (∃b1 b2. v1 = Bool b1 ∧ v2 = Bool b2 ∧ va = Inl (Bool (b1 ∧ b2))) ∨ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 AND i2)))"
by(cases "(v1, v2)" rule: binop_BinAnd.cases) auto

lemma [simp]:
  "(binop_BinOr v1 v2 = Some va) ⟷ 
   (∃b1 b2. v1 = Bool b1 ∧ v2 = Bool b2 ∧ va = Inl (Bool (b1 ∨ b2))) ∨
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 OR i2)))"
by(cases "(v1, v2)" rule: binop_BinOr.cases) auto

lemma [simp]:
  "(binop_BinXor v1 v2 = Some va) ⟷
   (∃b1 b2. v1 = Bool b1 ∧ v2 = Bool b2 ∧ va = Inl (Bool (b1 ≠ b2))) ∨
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 XOR i2)))"
by(cases "(v1, v2)" rule: binop_BinXor.cases) auto

lemma [simp]:
  "(binop_ShiftLeft v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 << unat (i2 AND 0x1f))))"
by(cases "(v1, v2)" rule: binop_ShiftLeft.cases) auto

lemma [simp]:
  "(binop_ShiftRightZeros v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 >> unat (i2 AND 0x1f))))"
by(cases "(v1, v2)" rule: binop_ShiftRightZeros.cases) auto

lemma [simp]:
  "(binop_ShiftRightSigned v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ va = Inl (Intg (i1 >>> unat (i2 AND 0x1f))))"
by(cases "(v1, v2)" rule: binop_ShiftRightSigned.cases) auto

end

context heap_base
begin

lemma [simp]:
  "(binop_Mod v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ 
      va = (if i2 = 0 then Inr (addr_of_sys_xcpt ArithmeticException) else Inl (Intg(i1 smod i2))))"
by(cases "(v1, v2)" rule: binop_Mod.cases) auto

lemma [simp]:
  "(binop_Div v1 v2 = Some va) ⟷ 
   (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ 
      va = (if i2 = 0 then Inr (addr_of_sys_xcpt ArithmeticException) else Inl (Intg(i1 sdiv i2))))"
by(cases "(v1, v2)" rule: binop_Div.cases) auto

end

subsection ‹Typing for binary operators›

inductive WT_binop :: "'m prog ⇒ ty ⇒ bop ⇒ ty ⇒ ty ⇒ bool" (‹_ ⊢ _«_»_ :: _› [51,0,0,0,51] 50)
where
  WT_binop_Eq:
  "P ⊢ T1 ≤ T2 ∨ P ⊢ T2 ≤ T1 ⟹ P ⊢ T1«Eq»T2 :: Boolean"

| WT_binop_NotEq:
  "P ⊢ T1 ≤ T2 ∨ P ⊢ T2 ≤ T1 ⟹ P ⊢ T1«NotEq»T2 :: Boolean"

| WT_binop_LessThan:
  "P ⊢ Integer«LessThan»Integer :: Boolean"

| WT_binop_LessOrEqual:
  "P ⊢ Integer«LessOrEqual»Integer :: Boolean"

| WT_binop_GreaterThan:
  "P ⊢ Integer«GreaterThan»Integer :: Boolean"

| WT_binop_GreaterOrEqual:
  "P ⊢ Integer«GreaterOrEqual»Integer :: Boolean"

| WT_binop_Add:
  "P ⊢ Integer«Add»Integer :: Integer"

| WT_binop_Subtract:
  "P ⊢ Integer«Subtract»Integer :: Integer"

| WT_binop_Mult:
  "P ⊢ Integer«Mult»Integer :: Integer"

| WT_binop_Div:
  "P ⊢ Integer«Div»Integer :: Integer"

| WT_binop_Mod:
  "P ⊢ Integer«Mod»Integer :: Integer"

| WT_binop_BinAnd_Bool:
  "P ⊢ Boolean«BinAnd»Boolean :: Boolean"

| WT_binop_BinAnd_Int:
  "P ⊢ Integer«BinAnd»Integer :: Integer"

| WT_binop_BinOr_Bool:
  "P ⊢ Boolean«BinOr»Boolean :: Boolean"

| WT_binop_BinOr_Int:
  "P ⊢ Integer«BinOr»Integer :: Integer"

| WT_binop_BinXor_Bool:
  "P ⊢ Boolean«BinXor»Boolean :: Boolean"

| WT_binop_BinXor_Int:
  "P ⊢ Integer«BinXor»Integer :: Integer"

| WT_binop_ShiftLeft:
  "P ⊢ Integer«ShiftLeft»Integer :: Integer"

| WT_binop_ShiftRightZeros:
  "P ⊢ Integer«ShiftRightZeros»Integer :: Integer"

| WT_binop_ShiftRightSigned:
  "P ⊢ Integer«ShiftRightSigned»Integer :: Integer"

lemma WT_binopI [intro]:
  "P ⊢ T1 ≤ T2 ∨ P ⊢ T2 ≤ T1 ⟹ P ⊢ T1«Eq»T2 :: Boolean"
  "P ⊢ T1 ≤ T2 ∨ P ⊢ T2 ≤ T1 ⟹ P ⊢ T1«NotEq»T2 :: Boolean"
  "bop = Add ∨ bop = Subtract ∨ bop = Mult ∨ bop = Mod ∨ bop = Div ∨ bop = BinAnd ∨ bop = BinOr ∨ bop = BinXor ∨ 
   bop = ShiftLeft ∨ bop = ShiftRightZeros ∨ bop = ShiftRightSigned
   ⟹ P ⊢ Integer«bop»Integer :: Integer"
  "bop = LessThan ∨ bop = LessOrEqual ∨ bop = GreaterThan ∨ bop = GreaterOrEqual ⟹ P ⊢ Integer«bop»Integer :: Boolean"
  "bop = BinAnd ∨ bop = BinOr ∨ bop = BinXor ⟹ P ⊢ Boolean«bop»Boolean :: Boolean"
by(auto intro: WT_binop.intros)

inductive_cases [elim]:
  "P ⊢ T1«Eq»T2 :: T"
  "P ⊢ T1«NotEq»T2 :: T"
  "P ⊢ T1«LessThan»T2 :: T"
  "P ⊢ T1«LessOrEqual»T2 :: T"
  "P ⊢ T1«GreaterThan»T2 :: T"
  "P ⊢ T1«GreaterOrEqual»T2 :: T"
  "P ⊢ T1«Add»T2 :: T"
  "P ⊢ T1«Subtract»T2 :: T"
  "P ⊢ T1«Mult»T2 :: T"
  "P ⊢ T1«Div»T2 :: T"
  "P ⊢ T1«Mod»T2 :: T"
  "P ⊢ T1«BinAnd»T2 :: T"
  "P ⊢ T1«BinOr»T2 :: T"
  "P ⊢ T1«BinXor»T2 :: T"
  "P ⊢ T1«ShiftLeft»T2 :: T"
  "P ⊢ T1«ShiftRightZeros»T2 :: T"
  "P ⊢ T1«ShiftRightSigned»T2 :: T"

lemma WT_binop_fun: "⟦ P ⊢ T1«bop»T2 :: T; P ⊢ T1«bop»T2 :: T' ⟧ ⟹ T = T'"
by(cases bop)(auto)

lemma WT_binop_is_type:
  "⟦ P ⊢ T1«bop»T2 :: T; is_type P T1; is_type P T2 ⟧ ⟹ is_type P T"
by(cases bop) auto

inductive WTrt_binop :: "'m prog ⇒ ty ⇒ bop ⇒ ty ⇒ ty ⇒ bool" (‹_ ⊢ _«_»_ : _› [51,0,0,0,51] 50)
where
  WTrt_binop_Eq:
  "P ⊢ T1«Eq»T2 : Boolean"

| WTrt_binop_NotEq:
  "P ⊢ T1«NotEq»T2 : Boolean"

| WTrt_binop_LessThan:
  "P ⊢ Integer«LessThan»Integer : Boolean"

| WTrt_binop_LessOrEqual:
  "P ⊢ Integer«LessOrEqual»Integer : Boolean"

| WTrt_binop_GreaterThan:
  "P ⊢ Integer«GreaterThan»Integer : Boolean"

| WTrt_binop_GreaterOrEqual:
  "P ⊢ Integer«GreaterOrEqual»Integer : Boolean"

| WTrt_binop_Add:
  "P ⊢ Integer«Add»Integer : Integer"

| WTrt_binop_Subtract:
  "P ⊢ Integer«Subtract»Integer : Integer"

| WTrt_binop_Mult:
  "P ⊢ Integer«Mult»Integer : Integer"

| WTrt_binop_Div:
  "P ⊢ Integer«Div»Integer : Integer"

| WTrt_binop_Mod:
  "P ⊢ Integer«Mod»Integer : Integer"

| WTrt_binop_BinAnd_Bool:
  "P ⊢ Boolean«BinAnd»Boolean : Boolean"

| WTrt_binop_BinAnd_Int:
  "P ⊢ Integer«BinAnd»Integer : Integer"

| WTrt_binop_BinOr_Bool:
  "P ⊢ Boolean«BinOr»Boolean : Boolean"

| WTrt_binop_BinOr_Int:
  "P ⊢ Integer«BinOr»Integer : Integer"

| WTrt_binop_BinXor_Bool:
  "P ⊢ Boolean«BinXor»Boolean : Boolean"

| WTrt_binop_BinXor_Int:
  "P ⊢ Integer«BinXor»Integer : Integer"

| WTrt_binop_ShiftLeft:
  "P ⊢ Integer«ShiftLeft»Integer : Integer"

| WTrt_binop_ShiftRightZeros:
  "P ⊢ Integer«ShiftRightZeros»Integer : Integer"

| WTrt_binop_ShiftRightSigned:
  "P ⊢ Integer«ShiftRightSigned»Integer : Integer"

lemma WTrt_binopI [intro]:
  "P ⊢ T1«Eq»T2 : Boolean"
  "P ⊢ T1«NotEq»T2 : Boolean"
  "bop = Add ∨ bop = Subtract ∨ bop = Mult ∨ bop = Div ∨ bop = Mod ∨ bop = BinAnd ∨ bop = BinOr ∨ bop = BinXor ∨
   bop = ShiftLeft ∨ bop = ShiftRightZeros ∨ bop = ShiftRightSigned
   ⟹ P ⊢ Integer«bop»Integer : Integer"
  "bop = LessThan ∨ bop = LessOrEqual ∨ bop = GreaterThan ∨ bop = GreaterOrEqual ⟹ P ⊢ Integer«bop»Integer : Boolean"
  "bop = BinAnd ∨ bop = BinOr ∨ bop = BinXor ⟹ P ⊢ Boolean«bop»Boolean : Boolean"
by(auto intro: WTrt_binop.intros)

inductive_cases WTrt_binop_cases [elim]:
  "P ⊢ T1«Eq»T2 : T"
  "P ⊢ T1«NotEq»T2 : T"
  "P ⊢ T1«LessThan»T2 : T"
  "P ⊢ T1«LessOrEqual»T2 : T"
  "P ⊢ T1«GreaterThan»T2 : T"
  "P ⊢ T1«GreaterOrEqual»T2 : T"
  "P ⊢ T1«Add»T2 : T"
  "P ⊢ T1«Subtract»T2 : T"
  "P ⊢ T1«Mult»T2 : T"
  "P ⊢ T1«Div»T2 : T"
  "P ⊢ T1«Mod»T2 : T"
  "P ⊢ T1«BinAnd»T2 : T"
  "P ⊢ T1«BinOr»T2 : T"
  "P ⊢ T1«BinXor»T2 : T"
  "P ⊢ T1«ShiftLeft»T2 : T"
  "P ⊢ T1«ShiftRightZeros»T2 : T"
  "P ⊢ T1«ShiftRightSigned»T2 : T"

inductive_simps WTrt_binop_simps [simp]:
  "P ⊢ T1«Eq»T2 : T"
  "P ⊢ T1«NotEq»T2 : T"
  "P ⊢ T1«LessThan»T2 : T"
  "P ⊢ T1«LessOrEqual»T2 : T"
  "P ⊢ T1«GreaterThan»T2 : T"
  "P ⊢ T1«GreaterOrEqual»T2 : T"
  "P ⊢ T1«Add»T2 : T"
  "P ⊢ T1«Subtract»T2 : T"
  "P ⊢ T1«Mult»T2 : T"
  "P ⊢ T1«Div»T2 : T"
  "P ⊢ T1«Mod»T2 : T"
  "P ⊢ T1«BinAnd»T2 : T"
  "P ⊢ T1«BinOr»T2 : T"
  "P ⊢ T1«BinXor»T2 : T"
  "P ⊢ T1«ShiftLeft»T2 : T"
  "P ⊢ T1«ShiftRightZeros»T2 : T"
  "P ⊢ T1«ShiftRightSigned»T2 : T"

fun binop_relevant_class :: "bop ⇒ 'm prog ⇒ cname ⇒ bool"
where
  "binop_relevant_class Div = (λP C. P ⊢ ArithmeticException ≼* C )"
| "binop_relevant_class Mod = (λP C. P ⊢ ArithmeticException ≼* C )"
| "binop_relevant_class _ = (λP C. False)"

lemma WT_binop_WTrt_binop:
  "P ⊢ T1«bop»T2 :: T ⟹ P ⊢ T1«bop»T2 : T"
by(auto elim: WT_binop.cases)

context heap begin

lemma binop_progress:
  "⟦ typeof⇘h⇙ v1 = ⌊T1⌋; typeof⇘h⇙ v2 = ⌊T2⌋; P ⊢ T1«bop»T2 : T ⟧
  ⟹ ∃va. binop bop v1 v2 = ⌊va⌋"
by(cases bop)(auto del: disjCI split del: if_split)

lemma binop_type:
  assumes wf: "wf_prog wf_md P"
  and pre: "preallocated h"
  and type: "typeof⇘h⇙ v1 = ⌊T1⌋" "typeof⇘h⇙ v2 = ⌊T2⌋" "P ⊢ T1«bop»T2 : T"
  shows "binop bop v1 v2 = ⌊Inl v⌋ ⟹ P,h ⊢ v :≤ T"
  and "binop bop v1 v2 = ⌊Inr a⌋ ⟹ P,h ⊢ Addr a :≤ Class Throwable"
using type
apply(case_tac [!] bop)
apply(auto split: if_split_asm simp add: conf_def wf_preallocatedD[OF wf pre])
done

lemma binop_relevant_class:
  assumes wf: "wf_prog wf_md P"
  and pre: "preallocated h"
  and bop: "binop bop v1 v2 = ⌊Inr a⌋"
  and sup: "P ⊢ cname_of h a ≼* C"
  shows "binop_relevant_class bop P C"
using assms
by(cases bop)(auto split: if_split_asm)

end

lemma WTrt_binop_fun: "⟦ P ⊢ T1«bop»T2 : T; P ⊢ T1«bop»T2 : T' ⟧ ⟹ T = T'"
by(cases bop)(auto)

lemma WTrt_binop_THE [simp]: "P ⊢ T1«bop»T2 : T ⟹ The (WTrt_binop P T1 bop T2) = T"
by(auto dest: WTrt_binop_fun)

lemma WTrt_binop_widen_mono:
  "⟦ P ⊢ T1«bop»T2 : T; P ⊢ T1' ≤ T1; P ⊢ T2' ≤ T2 ⟧ ⟹ ∃T'. P ⊢ T1'«bop»T2' : T' ∧ P ⊢ T' ≤ T"
by(cases bop)(auto elim!: WTrt_binop_cases)

lemma WTrt_binop_is_type:
  "⟦ P ⊢ T1«bop»T2 : T; is_type P T1; is_type P T2 ⟧ ⟹ is_type P T"
by(cases bop) auto

subsection ‹Code generator setup›

lemmas [code] =
  heap_base.binop_Div.simps
  heap_base.binop_Mod.simps
  heap_base.binop.simps

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  WT_binop
.

code_pred
  (modes: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  WTrt_binop
.

lemma eval_WTrt_binop_i_i_i_i_o:
  "Predicate.eval (WTrt_binop_i_i_i_i_o P T1 bop T2) T ⟷ P ⊢ T1«bop»T2 : T"
by(auto elim: WTrt_binop_i_i_i_i_oE intro: WTrt_binop_i_i_i_i_oI)

lemma the_WTrt_binop_code:
  "(THE T. P ⊢ T1«bop»T2 : T) = Predicate.the (WTrt_binop_i_i_i_i_o P T1 bop T2)"
by(simp add: Predicate.the_def eval_WTrt_binop_i_i_i_i_o)

end