Theory GTT_Impl

theory GTT_Impl
  imports GTT
begin

text ‹Note: should use @{term remdups} or @{term remdups_sort} instead.›

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"


fun list_of_permutation_n where
  "list_of_permutation_n S 0 = [[]]" |
  "list_of_permutation_n S (Suc n) = (let pre = (list_of_permutation_n S n) in
    concat (map (λ x. (map (λ y. x # y) pre)) S))"

lemma list_fun_sym_eq_set_cons_l:
  assumes "x ∈ {gs. length gs = n ∧ (∀ i < n. gs ! i ∈ set L)}"
  shows "x ∈ set (list_of_permutation_n L n)"
  using assms
proof (induct n arbitrary: x)
  case (Suc n)
  then obtain f s where x: "x = f # s" and "f ∈ set L"
    by auto (metis Suc_length_conv nth_Cons_0 zero_less_Suc)
  then have "s ∈ set (list_of_permutation_n L n)" using Suc(1,2) by auto fastforce
  then show ?case using x ‹f ∈ set L› by auto 
qed auto

lemma list_fun_sym_eq_set_cons_r:
  assumes "x ∈ set (list_of_permutation_n L n)"
  shows "x ∈ {gs. length gs = n ∧ (∀ i < n. gs ! i ∈ set L)}"
  using assms by (induct n arbitrary: x) (auto simp add: nth_Cons')

lemma list_fun_sym_eq_set:
  shows "set (list_of_permutation_n L n) = {gs. length gs = n ∧ (∀ i < n. gs ! i ∈ set L)}"
  using list_fun_sym_eq_set_cons_l list_fun_sym_eq_set_cons_r by blast

lemma list_fun_length_n [elim]:
  assumes "x ∈ set (list_of_permutation_n L n)"
  shows "length x = n"
  using assms list_fun_sym_eq_set_cons_r by blast 

end