Theory FinRep

header {* Finite representable types *}

theory FinRep
imports Main
begin

text {*
  A type is finitely representable if we can define
  a list containing all of its elements.
*}

consts
  LIST :: "'a list"

axclass finrep ⊆ type
  set_LIST [simp]: "set LIST = UNIV"

instance finrep ⊆ finite
apply (intro_classes)
apply (subst set_LIST [symmetric])
apply (rule finite_set)
done

defs (overloaded)
  LIST_unit_def: "LIST ≡ [()]"
  LIST_bool_def: "LIST ≡ [True, False]"
  LIST_sum_def:  "LIST ≡ map Inl LIST @ map Inr LIST"
  LIST_opt_def:  "LIST ≡ None # map Some LIST"
  LIST_prod_def: "LIST ≡ concat (map (λa. map (Pair a) LIST) LIST)"
  LIST_set_def:  "LIST ≡ foldr (λx As. map (insert x) As @ As) LIST [{}]"
  LIST_fun_def:
  "LIST ≡ foldr (λx fs. concat (map (λy. map (λf. f(x:=y)) fs) LIST))
                    LIST [arbitrary]"

instance unit :: finrep
by (intro_classes, unfold LIST_unit_def, auto)

instance bool :: finrep
by (intro_classes, unfold LIST_bool_def, auto)

instance "+" :: (finrep, finrep) finrep
apply (intro_classes, unfold LIST_sum_def)
apply (auto, case_tac x, simp_all)
done

instance option :: (finrep) finrep
apply (intro_classes, unfold LIST_opt_def)
apply (auto, case_tac x, simp_all)
done

instance "*" :: (finrep, finrep) finrep
by (intro_classes, unfold LIST_prod_def, auto)

instance set :: (finrep) finrep
apply (intro_classes, auto, rename_tac A)
apply (subgoal_tac "A ∩ set LIST ∈ set LIST", simp)
apply (unfold LIST_set_def)
apply (rule_tac x="LIST::'a list" in spec, clarify, rename_tac xs)
apply (induct_tac xs)
apply simp
apply (simp add: Int_insert_right)
done

instance fun :: (finrep, finrep) finrep
apply (intro_classes, auto, rename_tac f)
apply (subgoal_tac "∃g∈set LIST. ∀x∈set LIST. f x = g x")
apply (simp add: expand_fun_eq [symmetric])
apply (unfold LIST_fun_def)
apply (rule_tac x="LIST::'a list" in spec, clarify, rename_tac xs)
apply (induct_tac xs)
apply simp
apply clarify
apply (rule_tac x="g(a:=f a)" in bexI)
apply simp
apply (simp del: fun_upd_apply)
apply (rule_tac x="f a" in exI)
apply simp
done

end