Theory Type_Instances_Impl

theory Type_Instances_Impl
  imports Bot_Terms
    TA_Clousure_Const
    Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl
begin


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
begin
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))"
instance
  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)
end

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
qed

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"
instance
  by intro_classes (simp_all add: card_UNIV_cl_states_def finite_UNIV_cl_states_def finite_cl_states)
end

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


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

instantiation cl_states :: cproper_interval
begin

(* 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) ≠ [])))"

instance
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}
  moreover
  {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
qed
end

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

end