Theory GTT_TRS_Impl

theory GTT_TRS_Impl
  imports GTT_TRS GTT_Impl
begin

definition TRS_terms_impl :: "('f, 'v) rule list ⇒ ('f, 'v) term list" where
  "TRS_terms_impl R = concat (map (λ(l, r) ⇒ [l, r]) R)"

lemma TRS_terms_impl_sound:
  "set (TRS_terms_impl R) = TRS_terms (set R)"
  by (auto simp: TRS_fst_def TRS_snd_def TRS_terms_impl_def TRS_terms_def)

fun cmn_ta_rules1_impl :: "('f, 'v) term ⇒ (('f, 'v) term option, 'f) ta_rule list" where
  "cmn_ta_rules1_impl (Fun f ts) = (f (map Some ts) → Some (Fun f ts)) # concat (map cmn_ta_rules1_impl ts)"
| "cmn_ta_rules1_impl (Var x) = []"

lemma cmn_ta_rules1_impl_sound:
  "set (cmn_ta_rules1_impl t) = cmn_ta_rules {t}"
proof (induct t)
  have *: "s ⊳ t ⟷ (∃f ss s'. s = Fun f ss ∧ s' ∈ set ss ∧ s' ⊵ t)" for f ss t s
    by (metis supt_Fun_imp_arg_supteq set_supteq_into_supt Var_supt term.exhaust)
  case (Fun f ts)
  have *: "cmn_ta_rules {Fun f ts} = {f (map Some ts) → Some (Fun f ts)} ∪ ⋃((λt. cmn_ta_rules {t}) ` set ts)"
    unfolding cmn_ta_rules_def
    apply (subst subterm.order.order_iff_strict)
    apply (simp only: * singleton_iff term.simps conj_assoc ex_simps simp_thms cong: rev_conj_cong)
    by auto
  show ?case by (simp add: * Fun)
qed (auto 0 1 simp: cmn_ta_rules_def dest: supteq_Var_id)


definition cmn_ta_rules_impl :: "('f, 'v) term list ⇒ (('f, 'v) term option, 'f) ta_rule list" where
  "cmn_ta_rules_impl ts = concat (map cmn_ta_rules1_impl ts)"

lemma cmn_ta_rules_impl_sound:
  "set (cmn_ta_rules_impl ts) = cmn_ta_rules (set ts)"
  apply (simp add: cmn_ta_rules_impl_def cmn_ta_rules1_impl_sound)
  unfolding cmn_ta_rules_def by blast

definition trs_to_ta_A_impl :: "(('f, 'v) term × ('f, 'v) term) list ⇒ (('f, 'v) term option, 'f) ta_list" where
  "trs_to_ta_A_impl R = ta_list [] (cmn_ta_rules_impl (TRS_terms_impl R))
    (map (map_prod Some Some) R)"

lemma trs_to_ta_A_impl_sound:
  "ta_of (trs_to_ta_A_impl R) = trs_to_ta_A (set R)"
  by (auto simp: trs_to_ta_A_impl_def trs_to_ta_A_def cmn_ta_rules_impl_sound ta_of_def TRS_terms_impl_sound)

definition trs_to_ta_B_impl :: "(('f, 'v) term × ('f, 'v) term) list ⇒ (('f, 'v) term option, 'f) ta_list" where
  "trs_to_ta_B_impl R = ta_list [] (cmn_ta_rules_impl (TRS_terms_impl R))
    (map (map_prod Some Some ∘ prod.swap) R)"

lemma trs_to_ta_B_impl_sound:
  "ta_of (trs_to_ta_B_impl R) = trs_to_ta_B (set R)"
  by (force simp: trs_to_ta_B_impl_def trs_to_ta_B_def cmn_ta_rules_impl_sound ta_of_def TRS_terms_impl_sound)

definition trs_to_gtt_impl where
  "trs_to_gtt_impl R = (trs_to_ta_A_impl R, trs_to_ta_B_impl R)"

end