Theory Unboxed_lemmas

theory Unboxed_lemmas
  imports Unboxed
begin

lemma cast_Dyn_eq_Some_imp_typeof: "cast_Dyn u = Some d ⟹ typeof u = None"
  by (auto elim: cast_Dyn.elims)

lemma typeof_bind_OpDyn[simp]: "typeof ∘ OpDyn = (λ_. None)"
  by auto

lemma is_dyn_operand_eq_typeof: "is_dyn_operand = (λx. typeof x = None)"
proof (intro ext)
  fix x
  show "is_dyn_operand x = (typeof x = None)"
    by (cases x; simp)
qed

lemma is_dyn_operand_eq_typeof_Dyn[simp]: "is_dyn_operand x ⟷ typeof x = None"
  by (cases x; simp)

lemma typeof_unboxed_eq_const:
  fixes x
  shows
    "typeof x = None ⟷ (∃d. x = OpDyn d)"
    "typeof x = Some Ubx1 ⟷ (∃n. x = OpUbx1 n)"
    "typeof x = Some Ubx2 ⟷ (∃b. x = OpUbx2 b)"
  by (cases x; simp)+

lemmas typeof_unboxed_inversion = typeof_unboxed_eq_const[THEN iffD1]

lemma cast_inversions:
  "cast_Dyn x = Some d ⟹ x = OpDyn d"
  "cast_Ubx1 x = Some n ⟹ x = OpUbx1 n"
  "cast_Ubx2 x = Some b ⟹ x = OpUbx2 b"
  by (cases x; simp)+

lemma ap_map_list_cast_Dyn_replicate:
  assumes "ap_map_list cast_Dyn xs = Some ys"
  shows "map typeof xs = replicate (length xs) None"
  using assms
proof (induction xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  from Cons.prems show ?case
    by (auto intro: Cons.IH dest: cast_inversions(1) simp: ap_option_eq_Some_conv)
qed

context unboxedval begin

lemma unbox_typeof[simp]: "unbox τ d = Some blob ⟹ typeof blob = Some τ"
  by (cases τ; auto)

lemma cast_and_box_imp_typeof[simp]: "cast_and_box τ blob = Some d ⟹ typeof blob = Some τ"
  using cast_inversions[of blob]
  by (induction τ; auto dest: cast_inversions[of blob])

lemma norm_unbox_inverse[simp]: "unbox τ d = Some blob ⟹ norm_unboxed blob = d"
  using box_unbox_inverse
  by (cases τ; auto)

lemma norm_cast_and_box_inverse[simp]:
  "cast_and_box τ blob = Some d ⟹ norm_unboxed blob = d"
  by (induction τ; auto elim: cast_Dyn.elims cast_Ubx1.elims cast_Ubx2.elims)

lemma typeof_and_norm_unboxed_imp_cast_Dyn:
  assumes "typeof x' = None" "norm_unboxed x' = x"
  shows "cast_Dyn x' = Some x"
  using assms
  unfolding typeof_unboxed_eq_const
  by auto

lemma typeof_and_norm_unboxed_imp_cast_and_box:
  assumes "typeof x' = Some τ" "norm_unboxed x' = x"
  shows "cast_and_box τ x' = Some x"
  using assms
  by (induction τ; induction x'; simp)

lemma norm_unboxed_bind_OpDyn[simp]: "norm_unboxed ∘ OpDyn = id"
  by auto

lemmas box_stack_Nil[simp] = list.map(1)[of "box_frame f" for f, folded box_stack_def]
lemmas box_stack_Cons[simp] = list.map(2)[of "box_frame f" for f, folded box_stack_def]

lemma typeof_box_operand[simp]: "typeof (box_operand u) = None"
  by (cases u) simp_all

lemma typeof_box_operand_comp[simp]:  "typeof ∘ box_operand = (λ_. None)"
  by auto

lemma is_dyn_box_operand: "is_dyn_operand (box_operand x)"
  by (cases x) simp_all

lemma is_dyn_operand_comp_box_operand[simp]: "is_dyn_operand ∘ box_operand = (λ_. True)"
  using is_dyn_box_operand by auto

lemma norm_box_operand[simp]: "norm_unboxed (box_operand x) = norm_unboxed x"
  by (cases x) simp_all

end

end