Theory Op_example

theory Op_example
  imports OpUbx Global Unboxed_lemmas
begin


section ‹Dynamic values›

datatype dynamic = DNil | DBool bool | DNum int

definition is_true where
  "is_true d ≡ (d = DBool True)"

definition is_false where
  "is_false d ≡ (d = DBool False)"

interpretation dynval_dynamic: dynval DNil is_true is_false
proof unfold_locales
  fix d
  show "¬ (is_true d ∧ is_false d)"
    by (cases d) (simp_all add: is_true_def is_false_def)
qed

fun unbox_num :: "dynamic ⇒ int option" where
   "unbox_num (DNum n) = Some n" |
   "unbox_num _ = None"

fun unbox_bool :: "dynamic ⇒ bool option" where
   "unbox_bool (DBool b) = Some b" |
   "unbox_bool _ = None"

interpretation unboxed_dynamic:
  unboxedval DNil is_true is_false DNum unbox_num DBool unbox_bool
proof (unfold_locales)
  fix d n
  show "unbox_num d = Some n ⟹ DNum n = d"
    by (cases d; simp add: )
next
  fix d b
  show "unbox_bool d = Some b ⟹ DBool b = d"
    by (cases d; simp add:)
qed


section ‹Normal operations›

datatype op =
  OpNeg |
  OpAdd |
  OpMul

fun ar :: "op ⇒ nat" where
  "ar OpNeg = 1" |
  "ar OpAdd = 2" |
  "ar OpMul = 2"

fun eval_Neg :: "dynamic list ⇒ dynamic" where
  "eval_Neg [DBool b] = DBool (¬b)" |
  "eval_Neg [_] = DNil"

fun eval_Add :: "dynamic list ⇒ dynamic" where
  "eval_Add [DBool x, DBool y] = DBool (x ∨ y)" |
  "eval_Add [DNum x, DNum y] = DNum (x + y)" |
  "eval_Add [_, _] = DNil"

fun eval_Mul :: "dynamic list ⇒ dynamic" where
  "eval_Mul [DBool x, DBool y] = DBool (x ∧ y)" |
  "eval_Mul [DNum x, DNum y] = DNum (x * y)" |
  "eval_Mul [_, _] = DNil"

fun eval :: "op ⇒ dynamic list ⇒ dynamic" where
  "eval OpNeg = eval_Neg" |
  "eval OpAdd = eval_Add" |
  "eval OpMul = eval_Mul"

lemma eval_arith_domain: "length xs = ar op ⟹ ∃y. eval op xs = y"
  by simp

interpretation op_Op: nary_operations eval ar
  using eval_arith_domain
  by (unfold_locales; simp)


section ‹Inlined operations›

datatype opinl =
  OpAddNum |
  OpMulNum

fun inl :: "op ⇒ dynamic list ⇒ opinl option" where
  "inl OpAdd [DNum _, DNum _] = Some OpAddNum" |
  "inl OpMul [DNum _, DNum _] = Some OpMulNum" |
  "inl _ _ = None"

inductive isinl :: "opinl ⇒ dynamic list ⇒ bool" where
  "isinl OpAddNum [DNum _, DNum _]" |
  "isinl OpMulNum [DNum _, DNum _]"

fun deinl :: "opinl ⇒ op" where
  "deinl OpAddNum = OpAdd" |
  "deinl OpMulNum = OpMul"

lemma inl_inj: "inj inl"
  unfolding inj_def
proof (intro allI impI)
  fix x y
  assume "inl x = inl y"
  thus "x = y"
    unfolding fun_eq_iff
    by (cases x; cases y; auto elim: inl.elims simp: HOL.eq_commute[of None])
qed

lemma inl_invertible: "inl op xs = Some opinl ⟹ deinl opinl = op"
  by (induction op xs rule: inl.induct; simp)

fun eval_AddNum :: "dynamic list ⇒ dynamic" where
  "eval_AddNum [DNum x, DNum y] = DNum (x + y)" |
  "eval_AddNum [DBool x, DBool y] = DBool (x ∨ y)" |
  "eval_AddNum [_, _] = DNil"

fun eval_MulNum :: "dynamic list ⇒ dynamic" where
  "eval_MulNum [DNum x, DNum y] = DNum (x * y)" |
  "eval_MulNum [DBool x, DBool y] = DBool (x ∧ y)" |
  "eval_MulNum [_, _] = DNil"

fun eval_inl :: "opinl ⇒ dynamic list ⇒ dynamic" where
  "eval_inl OpAddNum = eval_AddNum" |
  "eval_inl OpMulNum = eval_MulNum"

lemma eval_AddNum_correct:
  "length xs = 2 ⟹ eval_AddNum xs = eval_Add xs"
  by (induction xs rule: eval_AddNum.induct; simp)

lemma eval_MulNum_correct:
  "length xs = 2 ⟹ eval_MulNum xs = eval_Mul xs"
  by (induction xs rule: eval_MulNum.induct; simp)

lemma eval_inl_correct:
  "length xs = ar (deinl opinl) ⟹ eval_inl opinl xs = eval (deinl opinl) xs"
  using eval_AddNum_correct eval_MulNum_correct
  by (cases opinl; simp)

lemma inl_isinl:
  "inl op xs = Some opinl ⟹ isinl opinl xs"
  by (induction op xs rule: inl.induct; auto intro: isinl.intros)

interpretation op_OpInl: nary_operations_inl eval ar eval_inl inl isinl deinl
  using inl_invertible
  using eval_inl_correct
  using inl_isinl
  by (unfold_locales; simp)


section ‹Unboxed operations›

datatype opubx =
  OpAddNumUbx

fun ubx :: "opinl ⇒ type option list ⇒ opubx option" where
  "ubx OpAddNum [Some Ubx1, Some Ubx1] = Some OpAddNumUbx" |
  "ubx _ _ = None"

fun deubx :: "opubx ⇒ opinl" where
  "deubx OpAddNumUbx = OpAddNum"

lemma ubx_invertible: "ubx opinl xs = Some opubx ⟹ deubx opubx = opinl"
  by (induction opinl xs rule: ubx.induct; simp)

fun eval_AddNumUbx where
  "eval_AddNumUbx [OpUbx1 x, OpUbx1 y] = Some (OpUbx1 (x + y))" |
  "eval_AddNumUbx _ = None"

fun eval_ubx where
  "eval_ubx OpAddNumUbx = eval_AddNumUbx"

lemma eval_ubx_correct:
  "eval_ubx opubx xs = Some z ⟹
    eval_inl (deubx opubx) (map unboxed_dynamic.norm_unboxed xs) = unboxed_dynamic.norm_unboxed z"
  apply (cases opubx; simp)
  by (induction xs rule: eval_AddNumUbx.induct) auto

lemma eval_ubx_to_inl:
  assumes "eval_ubx opubx Σ = Some z"
  shows "inl (deinl (deubx opubx)) (map unboxed_dynamic.norm_unboxed Σ) = Some (deubx opubx)"
proof (cases opubx)
  case OpAddNumUbx
  then have "eval_AddNumUbx Σ = Some z"
    using assms by simp
  then show ?thesis
    using OpAddNumUbx
    by (induction Σ rule: eval_AddNumUbx.induct) simp_all
qed


subsection ‹Typing›

fun typeof_opubx :: "opubx ⇒ type option list × type option" where
  "typeof_opubx OpAddNumUbx = ([Some Ubx1, Some Ubx1], Some Ubx1)"

lemma ubx_imp_typeof_opubx:
  "ubx opinl ts = Some opubx ⟹ fst (typeof_opubx opubx) = ts"
  by (induction opinl ts rule: ubx.induct; simp)

lemma typeof_opubx_correct:
  "typeof_opubx opubx = (map typeof xs, codomain) ⟹
    ∃y. eval_ubx opubx xs = Some y ∧ typeof y = codomain"
proof (induction opubx)
  case OpAddNumUbx
  obtain n1 n2 where xs_def: "xs = [OpUbx1 n1, OpUbx1 n2]" and "codomain = Some Ubx1"
    using OpAddNumUbx[symmetric]
    by (auto dest!: typeof_unboxed_inversion)
  then show ?case by simp
qed

lemma typeof_opubx_complete:
  "eval_ubx opubx xs = Some y ⟹
    typeof_opubx opubx = (map typeof xs, typeof y)"
proof (induction opubx)
  case OpAddNumUbx
  then show ?case
    by (auto elim: eval_AddNumUbx.elims)
qed

lemma typeof_opubx_ar: "length (fst (typeof_opubx opubx)) = ar (deinl (deubx opubx))"
  by (induction opubx; simp)

interpretation op_OpUbx:
  nary_operations_ubx
    eval ar eval_inl inl isinl deinl
    DNil is_true is_false DNum unbox_num DBool unbox_bool
    eval_ubx ubx deubx typeof_opubx
  using ubx_invertible
  using eval_ubx_correct
  using eval_ubx_to_inl
  using ubx_imp_typeof_opubx
  using typeof_opubx_correct
  using typeof_opubx_complete
  using typeof_opubx_ar
  by (unfold_locales; (simp; fail)?)

end