Theory Type_Instances_Impl

theory Type_Instances_Impl
  imports Bot_Terms

section ‹Type class instantiations for the implementation›

derive linorder sum
derive linorder bot_term
derive linorder cl_states

derive compare bot_term
derive compare cl_states

derive (eq) ceq bot_term mctxt cl_states

derive (compare) ccompare bot_term cl_states

derive (rbt) set_impl bot_term cl_states

derive (no) cenum bot_term

instantiation cl_states :: cenum
abbreviation "cl_all_list  [cl_state, tr_state, fin_state, fin_clstate]"
definition cEnum_cl_states :: "(cl_states list × ((cl_states  bool)  bool) × ((cl_states  bool)  bool)) option"
  where "cEnum_cl_states = Some (cl_all_list, (λ P. list_all P cl_all_list),  (λ P. list_ex P cl_all_list))"
  apply intro_classes apply (auto simp: cEnum_cl_states_def elim!: cl_states.induct)
  using cl_states.exhaust apply blast
  by (metis cl_states.exhaust)

lemma infinite_bot_term_UNIV[simp, intro]: "infinite (UNIV :: 'f bot_term set)"
proof -
  fix f :: 'f
  let ?inj = "λn. BFun f (replicate n Bot)"
  have "inj ?inj" unfolding inj_on_def by auto
  from infinite_super[OF _ range_inj_infinite[OF this]]
  show ?thesis by blast

lemma finite_cl_states: "(UNIV :: cl_states set) = {cl_state, tr_state, fin_state, fin_clstate}"
  using cl_states.exhaust
  by auto

instantiation cl_states :: card_UNIV begin
definition "finite_UNIV = Phantom(cl_states) True"
definition "card_UNIV = Phantom(cl_states) 4"
  by intro_classes (simp_all add: card_UNIV_cl_states_def finite_UNIV_cl_states_def finite_cl_states)

instantiation bot_term :: (type) finite_UNIV
definition "finite_UNIV = Phantom('a bot_term) False"
  by (intro_classes, unfold finite_UNIV_bot_term_def, simp)

instantiation bot_term :: (compare) cproper_interval
definition "cproper_interval = (λ ( _ :: 'a bot_term option) _ . False)"
instance by (intro_classes, auto)

instantiation cl_states :: cproper_interval

(* cl_all_list *)
definition cproper_interval_cl_states :: "cl_states option  cl_states option  bool"
  where "cproper_interval_cl_states x y =
   (case ID CCOMPARE(cl_states) of Some f 
   (case x of None 
     (case y of None  True | Some c  list_ex (λ x. (lt_of_comp f) x c) cl_all_list)
   | Some c 
     (case y of None  list_ex (λ x. (lt_of_comp f) c x) cl_all_list
      | Some d  (filter (λ x. (lt_of_comp f) x d  (lt_of_comp f) c x) cl_all_list)  [])))"

proof (intro_classes)
  assume ass: "(ID ccompare :: (cl_states  cl_states  order) option)  None"
  from ass obtain f where comp: "(ID ccompare :: (cl_states  cl_states  order) option) = Some f" by auto
  let ?g = "cproper_interval :: cl_states option  cl_states option  bool"
  have [simp]: "x < y  lt_of_comp f x y" for x y
    by (metis ID_Some ccompare_cl_states_def comp compare_cl_states_def less_cl_states_def option.sel)
  {fix c d x assume "lt_of_comp f x d" "lt_of_comp f c x"
    then have "c < x" "x < d" by simp_all}
  {fix c d assume " z. (c ::cl_states) < z  z < d"
    then obtain z where w: "c < z  z < d" by blast
    then have "z  set cl_all_list" by (cases z) auto
    moreover have "lt_of_comp f z d  lt_of_comp f c z" using w comp
      by auto
    ultimately have "filter (λx. lt_of_comp f x d  lt_of_comp f c x) cl_all_list  []" using w
      by auto}
  ultimately have "filter (λx. lt_of_comp f x d  lt_of_comp f c x) cl_all_list  []  ( z. c < z  z < d)" for d c using comp
    unfolding filter_empty_conv by simp blast
  then have "?g (Some x) (Some y) = ( z. x < z  z < y)" for x y
    by (simp add: comp cproper_interval_cl_states_def)
  moreover have "?g None None = True" by (simp add: comp cproper_interval_cl_states_def)
  moreover have "?g None (Some y) = (z. z < y)" for y using comp
    by (auto simp add: cproper_interval_cl_states_def ccompare_cl_states_def) (metis cl_states.exhaust)+
  moreover have "?g (Some y) None = (z. y < z)" for y using comp
    by (auto simp add: cproper_interval_cl_states_def) (metis cl_states.exhaust)+
  ultimately show "class.proper_interval cless ?g"
    unfolding class.proper_interval_def comp
    by simp

derive (rbt) mapping_impl cl_states
derive (rbt) mapping_impl bot_term