Theory PhiSem_Int_ArbiPrec

theory PhiSem_Int_ArbiPrec
  imports PhiSem_Generic_Boolean PhiSem_Common_Int
  abbrevs "<aint>" = "𝖺𝗂𝗇𝗍"
begin

chapter ‹Integer of Arbitrary Precision›

setup ‹Context.theory_map (Generic_Variable_Access.Process_of_Argument.put
                                          (SOME Generic_Variable_Access.store_value_no_clean))›

section ‹Semantics›

debt_axiomatization 𝖺𝗂𝗇𝗍 :: TY
                and sem_mk_aint   :: ‹int ⇒ VAL›
                and sem_dest_aint :: ‹VAL ⇒ int›
where sem_mk_dest_aint[simp]: ‹sem_dest_aint (sem_mk_aint i) = i›
  and WT_aint[simp]: ‹Well_Type 𝖺𝗂𝗇𝗍 = { sem_mk_aint i |i. True } ›
  and 𝖺𝗂𝗇𝗍_neq_𝗉𝗈𝗂𝗌𝗈𝗇[simp]: ‹𝖺𝗂𝗇𝗍 ≠ 𝗉𝗈𝗂𝗌𝗈𝗇›
  and can_eqcmp_aint[simp]: "Can_EqCompare res (sem_mk_aint i1) (sem_mk_aint i2)"
  and eqcmp_aint[simp]: "EqCompare (sem_mk_aint i1) (sem_mk_aint i2) ⟷ i1 = i2"
  and  zero_aint[simp]: ‹Zero 𝖺𝗂𝗇𝗍   = Some (sem_mk_aint 0)›
  and φSem_aint_to_logic_int[simp]: ‹φSem_int_to_logic_int (sem_mk_aint i) = Some i›
  and φSem_aint_to_logic_nat[simp]: ‹φSem_int_to_logic_nat (sem_mk_aint i) = (if 0 ≤ i then Some (nat i) else None)›

lemma sem_mk_aint_inj[simp]:
  ‹sem_mk_aint i = sem_mk_aint j ≡ i = j›
  by (smt (verit, best) sem_mk_dest_aint)
  

lemma [φreason %logical_spec_of_semantics]:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 0 ≤ n
⟹ get_logical_nat_from_semantic_int (sem_mk_aint n ⦂ Itself) (nat n)›
  unfolding get_logical_nat_from_semantic_int_def Premise_def
  by simp

lemma [φreason %logical_spec_of_semantics]:
  ‹ get_logical_int_from_semantic_int (sem_mk_aint n ⦂ Itself) n›
  unfolding get_logical_int_from_semantic_int_def Premise_def
  by simp

lemma [φreason add]:
  ‹Is_Type_Literal 𝖺𝗂𝗇𝗍›
  unfolding Is_Type_Literal_def ..

lemma has_Zero_𝖺𝗂𝗇𝗍[simp]:
  ‹ has_Zero 𝖺𝗂𝗇𝗍 ›
  unfolding has_Zero_def
  by simp



section ‹φ-Types›

subsection ‹Integer in the normal sense›

φtype_def φAInt :: "(VAL, int) φ" ("ℤ")
  where ‹x ⦂ φAInt ≡ sem_mk_aint x ⦂ Itself›
  deriving Basic
       and Abstract_Domain⇩L
       and Semantic_Zero_Val
       and ‹𝗍𝗒𝗉𝖾𝗈𝖿 ℤ = 𝖺𝗂𝗇𝗍›
       and Functionality
       and Equiv_Class


lemma [φreason 1000]:
    "φEqual ℤ (λx y. True) (=)"
  unfolding φEqual_def by (simp add: eq_nat_nat_iff)

lemma [φreason %logical_spec_of_semantics]:
  ‹get_logical_int_from_semantic_int (n ⦂ ℤ) n›
  unfolding get_logical_int_from_semantic_int_def Ball_def
  by clarsimp

lemma [φreason %logical_spec_of_semantics]:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 0 ≤ n
⟹ get_logical_nat_from_semantic_int (n ⦂ ℤ) (nat n)›
  unfolding get_logical_nat_from_semantic_int_def Ball_def Premise_def
  by clarsimp


subsection ‹Natural Nmber›

declare [[φtrace_reasoning = 0]]

φtype_def φANat ("ℕ")
  where ‹n ⦂ ℕ ≡ of_nat n ⦂ ℤ›
  deriving Basic
       and Abstract_Domain⇩L
       and Semantic_Type
       and Semantic_Zero_Val
       and Inhabited
       and ‹𝗍𝗒𝗉𝖾𝗈𝖿 ℕ = 𝖺𝗂𝗇𝗍›
       and Functionality
       and Equiv_Class


declare [[
    overloaded_operator_in_synthesis ‹Int.int›,
    overloaded_operator_in_synthesis ‹nat›
 ]]


lemma [φreason %ToA_num_conv_cut, φsynthesis %φsynthesis_transformation]:
  " Threshold_Cost 4
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 0 ≤ x
⟹ x ⦂ ℤ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 nat x ⦂ ℕ"
  ❴
    ‹nat x ⦂ MAKE 0 ℕ›
  ❵.

lemma [φreason %ToA_num_conv_cut]:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 0 ≤ x
⟹ x ⦂ ℤ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ ℕ 𝗌𝗎𝖻𝗃 y. y = nat x @tag to ℕ› ❴ ❵.

declare φANat.elim[condition ‹𝗍𝗁𝗋𝖾𝗌𝗁𝗈𝗅𝖽 2›,
                   φreason %ToA_num_conv_cut,
                   φsynthesis %φsynthesis_transformation]

lemma [φreason %ToA_num_conv_cut]:
  " x ⦂ ℕ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ ℤ 𝗌𝗎𝖻𝗃 y. y = Int.int x @tag to ℤ " ❴ ❵.

lemma [φreason 1000]: ‹φEqual ℕ (λ_ _. True) (=)› ❴ to ℤ ❵.

lemma [φreason %logical_spec_of_semantics]:
  ‹get_logical_int_from_semantic_int (n ⦂ ℕ) (of_nat n)›
  unfolding get_logical_int_from_semantic_int_def Ball_def
  by clarsimp

lemma [φreason %logical_spec_of_semantics]:
  ‹get_logical_nat_from_semantic_int (n ⦂ ℕ) n›
  unfolding get_logical_nat_from_semantic_int_def Ball_def
  by clarsimp


section ‹Instructions›

subsection ‹Arithmetic Operations›

(* definition op_const_aint :: "int ⇒ VAL proc"
  where "op_const_aint const = Return (φarg (sem_mk_aint const))" *)

definition op_aadd :: "(VAL × VAL, VAL) proc'"
  where "op_aadd =
      φM_caseV (λvb va.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      Return (φarg (sem_mk_aint (val_a + val_b)))
  )))"

definition op_asub :: "(VAL × VAL, VAL) proc'"
  where "op_asub =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_aint (val_a - val_b)))
  )))"

definition op_aneg :: "(VAL, VAL) proc'"
  where "op_aneg rv =
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint rv (λv.
      Return (φarg (sem_mk_aint (-v))))"

definition op_amul :: "(VAL × VAL, VAL) proc'"
  where "op_amul =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_aint (val_b * val_a)))
  )))"

definition op_adiv :: "(VAL × VAL, VAL) proc'"
  where "op_adiv =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_aint (val_a div val_b)))
  )))"

definition op_amod :: "(VAL × VAL, VAL) proc'"
  where "op_amod =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_aint (val_a mod val_b)))
  )))"

definition op_alshr :: "(VAL × VAL, VAL) proc'"
  where "op_alshr =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_aint (val_a div 2 ^ (Int.nat val_b))))
  )))"

definition op_alshl :: "(VAL × VAL, VAL) proc'"
  where "op_alshl =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_aint (val_a * 2 ^ (Int.nat val_b))))
  )))"

definition op_a_lt :: "(VAL × VAL, VAL) proc'"
  where "op_a_lt =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_bool (val_a < val_b)))
  )))"

definition op_a_le :: "(VAL × VAL, VAL) proc'"
  where "op_a_le =
      φM_caseV (λva vb.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint va (λval_a.
      φM_getV 𝖺𝗂𝗇𝗍 sem_dest_aint vb (λval_b.
      Return (φarg (sem_mk_bool (val_a ≤ val_b)))
  )))"


section ‹Abstraction of Instructions›

subsection ‹Arithmetic Operations›

subsubsection ‹Constant Integer›

lemma op_const_aint_φapp[φreason %φsynthesis_literal_number]:
  ‹ Is_Literal x
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[semantic_literal (sem_mk_aint x)] ℤ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 X @tag synthesis›
  for X :: assn
❴
  semantic_literal ‹sem_mk_aint x ⊨ (x ⦂ ℤ)›
❵ .

lemma op_const_anat_φapp[φreason %φsynthesis_literal_number]:
  ‹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[mode_literal] x' : of_nat x
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ Val (semantic_literal (sem_mk_aint x')) ℕ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 X @tag synthesis›
  for X :: assn
❴
  semantic_literal ‹sem_mk_aint x' ⊨ (x ⦂ ℕ)›
❵ .

lemma [φreason %φsynthesis_parse_number+10
    for ‹Synthesis_Parse (numeral ?n::nat) (?X :: ?'ret ⇒ assn)›
       ‹Synthesis_Parse (1::nat) (?X :: ?'ret ⇒ assn)›
       ‹Synthesis_Parse (0::nat) (?X :: ?'ret ⇒ assn)›
]:
  ‹ Synthesis_Parse (n ⦂ ℕ) X
⟹ Synthesis_Parse n X›
  for X :: ‹'ret ⇒ assn›
  unfolding Synthesis_Parse_def ..

lemma [φreason %φsynthesis_parse_number
    for ‹Synthesis_Parse (numeral ?n::int) (?X :: ?'ret ⇒ assn)›
       ‹Synthesis_Parse (1::int) (?X :: ?'ret ⇒ assn)›
       ‹Synthesis_Parse (0::int) (?X :: ?'ret ⇒ assn)›
]:
  ‹ Synthesis_Parse (n ⦂ ℤ) X
⟹ Synthesis_Parse n X›
  for X :: ‹'ret ⇒ assn›
  unfolding Synthesis_Parse_def ..


(* lemma op_const_size_t:
  ‹𝗉𝗋𝗈𝖼 op_const_size_t n ⦃ Void ⟼ 𝗏𝖺𝗅 n ⦂ Size ⦄›
  unfolding op_const_size_t_def Premise_def
  by (φreason, simp add: φexpns Big_def) *)


(* lemma [φreason 1200
    for ‹𝗉𝗋𝗈𝖼 ?f ⦃ ?X' ⟼ ?X❟ SYNTHESIS 𝗏𝖺𝗅 (numeral ?n) ⦂ Size ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E  @tag synthesis ?G›
       ‹𝗉𝗋𝗈𝖼 ?f ⦃ ?X' ⟼ ?X❟ SYNTHESIS 𝗏𝖺𝗅 0 ⦂ Size ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E  @tag synthesis ?G›
       ‹𝗉𝗋𝗈𝖼 ?f ⦃ ?X' ⟼ ?X❟ SYNTHESIS 𝗏𝖺𝗅 1 ⦂ Size ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E  @tag synthesis ?G›
]:
  ‹𝗉𝗋𝗈𝖼 op_const_size_t n ⦃ R ⟼ R❟ SYNTHESIS 𝗏𝖺𝗅 n ⦂ Size ⦄ @tag synthesis G›
  unfolding Synthesis_def Action_Tag_def
  using op_const_size_t[THEN φframe, simplified] . *)

lemma int_literal_2_literal_int[simp]:
  ‹int (literal x) = literal (int x)›
  unfolding literal_def
  by simp



subsubsection ‹Integer Arithmetic›

paragraph ‹Addition›

lemma op_add_aint_φapp
  [φoverload +,
   φsynthesis for _ (%synthesis_arith)
              and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x + y ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝗈𝖼 op_aadd (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℤ❟ y ⦂ 𝗏𝖺𝗅[vy] ℤ ⟼ 𝗏𝖺𝗅 x + y ⦂ ℤ ⦄ ›
  unfolding op_aadd_def Premise_def
  by (cases vx; cases vy; simp, rule, rule, simp add: Premise_def, rule,
      simp add: Premise_def, rule, simp)

lemma op_add_anat_φapp
  [φoverload +,
   φsynthesis for _ (%synthesis_arith)
              and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x + y ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝗈𝖼 op_aadd (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℕ❟ y ⦂ 𝗏𝖺𝗅[vy] ℕ ⟼ 𝗏𝖺𝗅 x + y ⦂ ℕ ⦄ ›
  ❴ op_add_aint ❵ .


paragraph ‹Subtraction›

lemma op_sub_aint_φapp[φoverload -,
                       φsynthesis for _ (%synthesis_arith)
                                  and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x - y ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝗈𝖼 op_asub (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℤ❟ y ⦂ 𝗏𝖺𝗅[vy] ℤ ⟼ 𝗏𝖺𝗅 x - y ⦂ ℤ ⦄›
  unfolding op_asub_def Premise_def
  by (cases vx; cases vy; simp, rule, rule, simp add: Premise_def,
      rule, simp add: Premise_def, rule, simp)

lemma op_sub_anat_φapp[φoverload -,
                       φsynthesis for _ (%synthesis_arith)
                                  and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x - y ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 y ≤ x
⟹ 𝗉𝗋𝗈𝖼 op_asub (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℕ❟ y ⦂ 𝗏𝖺𝗅[vy] ℕ ⟼ 𝗏𝖺𝗅 x - y ⦂ ℕ ⦄›
  ❴ op_sub_aint ❵ .


paragraph ‹Negation›

lemma op_neg_aint_φapp
  [φoverload ~,
   φsynthesis for _ (%synthesis_arith)
              and ‹x ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. - x ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝗈𝖼 op_aneg rv ⦃ x ⦂ 𝗏𝖺𝗅[rv] ℤ ⟼ 𝗏𝖺𝗅 -x ⦂ ℤ ⦄ ›
  unfolding op_aneg_def Premise_def
  by (cases rv; simp, rule, simp add: Premise_def, rule, simp)


paragraph ‹Times›

lemma op_mul_aint[φoverload *,
                  φsynthesis for _ (%synthesis_arith)
                             and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x * y ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝗈𝖼 op_amul (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℤ❟ y ⦂ 𝗏𝖺𝗅[vy] ℤ ⟼ 𝗏𝖺𝗅 x * y ⦂ ℤ ⦄›
  unfolding op_amul_def
  by (cases vx; cases vy; simp, rule, rule, simp add: Premise_def,
      rule, simp add: Premise_def, rule, simp)

lemma op_mul_anat[φoverload *,
                  φsynthesis for _ (%synthesis_arith)
                             and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x * y ⦂ _› (%synthesis_arith_cut)]:
  ‹ 𝗉𝗋𝗈𝖼 op_amul (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℕ❟ y ⦂ 𝗏𝖺𝗅[vy] ℕ ⟼ 𝗏𝖺𝗅 x * y ⦂ ℕ ⦄›
  ❴ op_mul_aint ❵
      certified by (simp add: nat_mult_distrib) .


paragraph ‹Division›

lemma op_udiv_aint_φapp[φoverload /,
                        φsynthesis for _ (%synthesis_arith)
                                   and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x div y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_adiv (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℤ❟ y ⦂ 𝗏𝖺𝗅[vy] ℤ ⟼ 𝗏𝖺𝗅 x div y ⦂ ℤ ⦄›
  unfolding op_adiv_def
  by (cases vx; cases vy; simp, rule, rule, simp add: Premise_def, rule, simp add: Premise_def,
      rule, simp)

lemma op_udiv_anat_φapp[φoverload /,
                        φsynthesis for _ (%synthesis_arith)
                                   and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x div y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_adiv (φV_pair vx vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℕ❟ y ⦂ 𝗏𝖺𝗅[vy] ℕ ⟼ 𝗏𝖺𝗅 x div y ⦂ ℕ ⦄›
  ❴ op_udiv_aint ❵
      certified by (simp add: div_int_pos_iff nat_div_distrib) .


paragraph ‹Modulo›

lemma op_mod_aint_φapp[φoverload %,
                       φsynthesis for _ (%synthesis_arith)
                                  and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x mod y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_amod (vx❙, vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℤ❟ y ⦂ 𝗏𝖺𝗅[vy] ℤ ⟼ 𝗏𝖺𝗅 x mod y ⦂ ℤ ⦄›
  unfolding op_amod_def
  by (cases vx; cases vy; simp, rule, rule, simp add: Premise_def, rule, simp add: Premise_def,
      rule, simp)

lemma op_mod_anat_φapp[φoverload %,
                       φsynthesis for _ (%synthesis_arith)
                                  and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x mod y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_amod (vx❙, vy) ⦃ x ⦂ 𝗏𝖺𝗅[vx] ℕ❟ y ⦂ 𝗏𝖺𝗅[vy] ℕ ⟼ 𝗏𝖺𝗅 x mod y ⦂ ℕ ⦄›
  ❴ op_mod_aint ❵
      certified by (metis nat_int of_nat_0_le_iff zmod_int) .
    


paragraph ‹Right Shift›

lemma op_lshr_aint_pre_φapp:
  ‹ 𝗉𝗋𝗈𝖼 op_alshr (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℤ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℤ ⟼ 𝗏𝖺𝗅 drop_bit (nat y) x ⦂ ℤ ⦄›
  unfolding op_alshr_def Premise_def
  by (cases raw1; cases raw2; simp; rule, rule, simp, rule, simp, simp,
      rule, simp, insert drop_bit_int_def, presburger)

lemma op_push_bit_right_aint_φapp[φsynthesis for _ (%synthesis_arith)
                                   and ‹x ⦂ 𝗏𝖺𝗅 ℤ ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. drop_bit y x ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_alshr (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℤ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 drop_bit y x ⦂ ℤ ⦄›
  ❴ op_lshr_aint_pre ❵.

lemma op_lshr_aint_φapp[φoverload >>]:
  ‹𝗉𝗋𝗈𝖼 op_alshr (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℤ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 x div 2 ^ y ⦂ ℤ ⦄›
  ❴ op_lshr_aint_pre ❵
      certified using drop_bit_int_def by blast .

lemma op_push_bit_right_anat_φapp[φsynthesis for _ (%synthesis_arith)
                                      and ‹x ⦂ 𝗏𝖺𝗅 ℕ ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λret. drop_bit y x ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_alshr (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℕ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 drop_bit y x ⦂ ℕ ⦄›
  ❴ op_push_bit_right_aint ❵
      certified by (simp add: drop_bit_of_nat)  .

lemma op_lshr_anat_φapp[φoverload >>]:
  ‹𝗉𝗋𝗈𝖼 op_alshr (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℕ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 x div 2 ^ y ⦂ ℕ ⦄›
  ❴ op_lshr_aint ❵
      certified by (metis nat_int of_nat_0_le_iff of_nat_numeral of_nat_power zdiv_int) . 


paragraph ‹Left Shift›

lemma op_lshl_aint_pre_φapp:
  ‹ 𝗉𝗋𝗈𝖼 op_alshl (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℤ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℤ ⟼ 𝗏𝖺𝗅 push_bit (nat y) x ⦂ ℤ ⦄›
  unfolding op_alshl_def Premise_def
  by (cases raw1; cases raw2; simp; rule, rule, simp, rule, simp, rule, simp add: push_bit_int_def)

lemma op_push_bit_left_aint_φapp[φsynthesis for _ (%synthesis_arith)
                                   and ‹x ⦂ 𝗏𝖺𝗅 ℤ ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. push_bit y x ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_alshl (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℤ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 push_bit y x ⦂ ℤ ⦄›
  ❴ op_lshl_aint_pre ❵.

lemma op_lshl_aint_φapp[φoverload <<]:
  ‹𝗉𝗋𝗈𝖼 op_alshl (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℤ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 x * 2 ^ y ⦂ ℤ ⦄›
  ❴ op_lshl_aint_pre ❵ certified by (simp add: push_bit_eq_mult) .

lemma op_push_bit_left_anat_φapp[φsynthesis for _ (%synthesis_arith)
                                   and ‹x ⦂ 𝗏𝖺𝗅 ℕ ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. push_bit y x ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_alshl (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℕ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 push_bit y x ⦂ ℕ ⦄›
  ❴ op_push_bit_left_aint ❵
      certified by (simp add: push_bit_of_nat) .

lemma op_lshl_anat_φapp[φoverload <<]:
  ‹𝗉𝗋𝗈𝖼 op_alshl (raw1❙, raw2) ⦃ x ⦂ 𝗏𝖺𝗅[raw1] ℕ ❟ y ⦂ 𝗏𝖺𝗅[raw2] ℕ ⟼ 𝗏𝖺𝗅 x * 2 ^ y ⦂ ℕ ⦄›
  ❴ op_lshl_aint ❵
      certified by (simp add: nat_mult_distrib) .


paragraph ‹Less Than›

lemma op_lt_aint[φoverload <,
                 φsynthesis for _ (%synthesis_arith)
                            and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x < y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_a_lt (rawx❙, rawy) ⦃ x ⦂ 𝗏𝖺𝗅[rawx] ℤ❟ y ⦂ 𝗏𝖺𝗅[rawy] ℤ ⟼ 𝗏𝖺𝗅 x < y ⦂ 𝔹 ⦄›
  unfolding op_a_lt_def
  by (cases rawx; cases rawy; simp, rule, rule, simp, rule, simp, rule, simp)

lemma op_lt_anat[φoverload <,
                 φsynthesis for _ (%synthesis_arith)
                            and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x < y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_a_lt (rawx❙, rawy) ⦃ x ⦂ 𝗏𝖺𝗅[rawx] ℕ❟ y ⦂ 𝗏𝖺𝗅[rawy] ℕ ⟼ 𝗏𝖺𝗅 x < y ⦂ 𝔹 ⦄›
  ❴ op_lt_aint ❵.

setup ‹Context.theory_map (Generic_Variable_Access.Process_of_Argument.put NONE)›

thm "<_φapp"

proc (nodef) op_gt_aint[φoverload >]:
  input  ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ›
  output ‹𝗏𝖺𝗅 x > y ⦂ 𝔹›
❴
  $y < $x
❵.

proc (nodef) op_gt_anat[φoverload >]:
  input  ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ›
  output ‹𝗏𝖺𝗅 x > y ⦂ 𝔹›
❴
  $y < $x
❵.

setup ‹Context.theory_map (Generic_Variable_Access.Process_of_Argument.put
                                          (SOME Generic_Variable_Access.store_value_no_clean))›

paragraph ‹Less Equal›

lemma op_le_aint_φapp[φoverload ≤,
                      φsynthesis for _ (%synthesis_arith)
                                 and ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ› ⇒ ‹λv. x ≤ y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_a_le (rawx❙, rawy) ⦃ x ⦂ 𝗏𝖺𝗅[rawx] ℤ❟ y ⦂ 𝗏𝖺𝗅[rawy] ℤ ⟼ 𝗏𝖺𝗅 x ≤ y ⦂ 𝔹 ⦄›
  unfolding op_a_le_def
  by (cases rawx; cases rawy; simp, rule, rule, simp add: Premise_def,
      rule, simp add: Premise_def, rule, simp)

lemma op_le_anat_φapp[φoverload ≤,
                      φsynthesis for _ (%synthesis_arith)
                                 and ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ› ⇒ ‹λv. x ≤ y ⦂ _› (%synthesis_arith_cut)]:
  ‹𝗉𝗋𝗈𝖼 op_a_le (rawx❙, rawy) ⦃ x ⦂ 𝗏𝖺𝗅[rawx] ℕ❟ y ⦂ 𝗏𝖺𝗅[rawy] ℕ ⟼ 𝗏𝖺𝗅 x ≤ y ⦂ 𝔹 ⦄›
  ❴ op_le_aint ❵.


setup ‹Context.theory_map (Generic_Variable_Access.Process_of_Argument.put NONE)›


proc (nodef) op_ge_aint[φoverload ≥]:
  input  ‹x ⦂ 𝗏𝖺𝗅 ℤ❟ y ⦂ 𝗏𝖺𝗅 ℤ›
  output ‹𝗏𝖺𝗅 x ≥ y ⦂ 𝔹›
❴
  $y ≤ $x
❵.

proc (nodef) op_ge_anat[φoverload ≥]:
  input  ‹x ⦂ 𝗏𝖺𝗅 ℕ❟ y ⦂ 𝗏𝖺𝗅 ℕ›
  output ‹𝗏𝖺𝗅 x ≥ y ⦂ 𝔹›
❴
  $y ≤ $x
❵.

end