Theory GTT_Impl

theory GTT_Impl
  imports GTT
begin

fun uniq_list where
  "uniq_list [] = []"
| "uniq_list (x # xs) = list_union [x] (uniq_list xs)"

lemma set_uniq_list [simp]:
  "set (uniq_list xs) = set xs"
  by (induct xs) auto

declare uniq_list.simps [simp del]

datatype ('q,'f) ta_list = ta_list (tal_final: "'q list") (tal_rules: "('q, 'f) ta_rule list") (tal_eps: "('q × 'q) list")

definition ta_of :: "('q, 'f) ta_list ⇒ ('q, 'f) ta" where
  "ta_of A = case_ta_list (λf r e. ta.make (set f) (set r) (set e)) A"

lemma ta_of_simps [simp]:
  "ta_final (ta_of A) = set (tal_final A)"
  "ta_rules (ta_of A) = set (tal_rules A)"
  "ta_eps (ta_of A) = set (tal_eps A)"
  by (auto simp: ta_of_def split: ta_list.splits)

lemma ta_of_eq_ta_makeI:
   "set xs = X ⟹ set ys = Y ⟹ set zs = Z ⟹ ta_of (ta_list xs ys zs) = ta.make X Y Z"
   by auto

definition uniq_ta where
  "uniq_ta A = ta_list (uniq_list (tal_final A)) (uniq_list (tal_rules A)) (uniq_list (tal_eps A))"

lemma ta_of_uniq_ta [simp]:
  "ta_of (uniq_ta A) = ta_of A"
  by (auto simp: uniq_ta_def ta_of_def split: ta_list.splits)

type_synonym ('q, 'f) gtt_list = "('q, 'f) ta_list × ('q, 'f) ta_list"

abbreviation gtt_of :: "('q, 'f) gtt_list ⇒ ('q, 'f) gtt" where
  "gtt_of ≡ map_prod ta_of ta_of"

end