Theory Event_Data

(*<*)
theory Event_Data
  imports
    "HOL-Library.Char_ord"
begin
(*>*)

section ‹Type of Events›

subsection ‹Code Adaptation for 8-bit strings›

typedef string8 = "UNIV :: char list set" ..

setup_lifting type_definition_string8

lift_definition empty_string :: string8 is "[]" .
lift_definition string8_literal :: "String.literal ⇒ string8" is String.explode .
lift_definition literal_string8:: "string8 ⇒ String.literal" is String.Abs_literal .
declare [[coercion string8_literal]]

instantiation string8 :: "{equal, linorder}"
begin

lift_definition equal_string8 :: "string8 ⇒ string8 ⇒ bool" is HOL.equal .
lift_definition less_eq_string8 :: "string8 ⇒ string8 ⇒ bool" is ord_class.lexordp_eq .
lift_definition less_string8 :: "string8 ⇒ string8 ⇒ bool" is ord_class.lexordp .

instance by intro_classes
    (transfer; auto simp: equal_eq lexordp_conv_lexordp_eq lexordp_eq_linear
      intro: lexordp_eq_refl lexordp_eq_trans lexordp_eq_antisym)+

end

lifting_forget string8.lifting

declare [[code drop: literal_string8 string8_literal "HOL.equal :: string8 ⇒ _"
      "(≤) :: string8 ⇒ _" "(<) :: string8 ⇒ _"
      "Code_Evaluation.term_of :: string8 ⇒ _"]]

code_printing
  type_constructor string8 ⇀ (OCaml) "string"
  | constant "HOL.equal :: string8 ⇒ string8 ⇒ bool" ⇀ (OCaml) "Stdlib.(=)"
  | constant "(≤) :: string8 ⇒ string8 ⇒ bool" ⇀ (OCaml) "Stdlib.(<=)"
  | constant "(<) :: string8 ⇒ string8 ⇒ bool" ⇀ (OCaml) "Stdlib.(<)"
  | constant "empty_string :: string8" ⇀ (OCaml) "\"\""
  | constant "string8_literal :: String.literal ⇒ string8" ⇀ (OCaml) "id"
  | constant "literal_string8 :: string8 ⇒ String.literal" ⇀ (OCaml) "id"

ML ‹structure String8 = struct fun to_term x = @{term Abs_string8} $ HOLogic.mk_string x; end;›

code_printing
  type_constructor string8 ⇀ (Eval) "string"
  | constant "string8_literal :: String.literal ⇒ string8" ⇀ (Eval) "_"
  | constant "HOL.equal :: string8 ⇒ string8 ⇒ bool" ⇀ (Eval) infixl 6 "="
  | constant "(≤) :: string8 ⇒ string8 ⇒ bool" ⇀ (Eval) infixl 6 "<="
  | constant "(<) :: string8 ⇒ string8 ⇒ bool" ⇀ (Eval) infixl 6 "<"
  | constant "empty_string :: string8" ⇀ (Eval) "\"\""
  | constant "Code_Evaluation.term_of :: string8 ⇒ term" ⇀ (Eval) "String8.to'_term"

ML ‹structure String8 =struct fun to_term x = @{term Abs_string8} $ HOLogic.mk_string x; end;›

code_printing
  type_constructor string8 ⇀ (Eval) "string"
  | constant "string8_literal :: String.literal ⇒ string8" ⇀ (Eval) "_"
  | constant "HOL.equal :: string8 ⇒ string8 ⇒ bool" ⇀ (Eval) infixl 6 "="
  | constant "(≤) :: string8 ⇒ string8 ⇒ bool" ⇀ (Eval) infixl 6 "<="
  | constant "(<) :: string8 ⇒ string8 ⇒ bool" ⇀ (Eval) infixl 6 "<"
  | constant "Code_Evaluation.term_of :: string8 ⇒ term" ⇀ (Eval) "String8.to'_term"

subsection ‹Event Parameters›

definition div_to_zero :: "integer ⇒ integer ⇒ integer" where
  "div_to_zero x y = (let z = fst (Code_Numeral.divmod_abs x y) in
    if (x < 0) ≠ (y < 0) then - z else z)"

definition mod_to_zero :: "integer ⇒ integer ⇒ integer" where
  "mod_to_zero x y = (let z = snd (Code_Numeral.divmod_abs x y) in
    if x < 0 then - z else z)"

lemma "b ≠ 0 ⟹ div_to_zero a b * b + mod_to_zero a b = a"
  unfolding div_to_zero_def mod_to_zero_def Let_def
  by (auto simp: minus_mod_eq_mult_div[symmetric] div_minus_right mod_minus_right ac_simps)

datatype event_data = EInt integer | EString string8

instantiation event_data :: "{ord, plus, minus, uminus, times, divide, modulo}"
begin

fun less_eq_event_data where
  "EInt x ≤ EInt y ⟷ x ≤ y"
| "EString x ≤ EString y ⟷ x ≤ y"
| "EInt _ ≤ EString _ ⟷ True"
| "(_ :: event_data) ≤ _ ⟷ False"

definition less_event_data :: "event_data ⇒ event_data ⇒ bool" where
  "less_event_data x y ⟷ x ≤ y ∧ ¬ y ≤ x"

fun plus_event_data where
  "EInt x + EInt y = EInt (x + y)"
| "(_::event_data) + _ = undefined"

fun minus_event_data where
  "EInt x - EInt y = EInt (x - y)"
| "(_::event_data) - _ = undefined"

fun uminus_event_data where
  "- EInt x = EInt (- x)"
| "- (_::event_data) = undefined"

fun times_event_data where
  "EInt x * EInt y = EInt (x * y)"
| "(_::event_data) * _ = undefined"

fun divide_event_data where
  "EInt x div EInt y = EInt (div_to_zero x y)"
| "(_::event_data) div _ = undefined"

fun modulo_event_data where
  "EInt x mod EInt y = EInt (mod_to_zero x y)"
| "(_::event_data) mod _ = undefined"

instance ..

end

lemma infinite_UNIV_event_data:
  "¬finite (UNIV :: event_data set)"
proof -
  define f where "f = (λk. EInt k)"
  have inj: "inj_on f (UNIV :: integer set)"
    unfolding f_def by (meson event_data.inject(1) injI)
  show ?thesis using finite_imageD[OF _ inj]
    by (meson infinite_UNIV_char_0 infinite_iff_countable_subset top_greatest)
qed

primrec integer_of_event_data :: "event_data ⇒ integer" where
  "integer_of_event_data (EInt _) = undefined"
| "integer_of_event_data (EString _) = undefined"

instantiation event_data :: default begin

definition default_event_data :: event_data where "default = EInt 0"

instance proof qed

end

instantiation event_data :: linorder begin
instance
proof (standard, unfold less_event_data_def, goal_cases less refl trans antisym total)
  case (refl x)
  then show ?case
    by (cases x) auto
next
  case (trans x y z)
  then show ?case
    by (cases x; cases y; cases z) auto
next
  case (antisym x y)
  then show ?case
    by (cases x; cases y) auto
next
  case (total x y)
  then show ?case
    by (cases x; cases y) auto
qed simp

end


(*<*)
end
(*>*)