Theory LV_to_GTT_Impl

theory LV_to_GTT_Impl
  imports LV_to_GTT GTT_TRS_Impl TRS.Term_Impl TA.Tree_Automata_Autoref_Setup Refine_Iterator
begin

(* TODO: move; a variation of this is reproved in GTT_RRn_Impl *)
lemma map_of_keys:
  "map_of (map (λx. (x, ())) xs) x = (if x ∈ set xs then Some () else None)"
  by (induct xs) auto

lemma trs_to_ta_extra_simps:
  "⋀f g P. f ` {g x |x. P x} = {f (g x) |x. P x}"
  "⋀f g P. f ` {g x y |x y. P x y} = {f (g x y) |x y. P x y}"
  "⋀ f X. {f x y |x y. (x, y) ∈ X} = case_prod f ` X"
  "⋀ f X. {f x |x. x ∈ X} = f ` X"
  (* "⋀f y g. f (let x = y in g x) = (let x = y in f (g x))" *)
  by auto

definition (in fixed_signature) term_TA' ::
  "(('f,'v) term ⇒ 'b) ⇒ ('f,'v) term ⇒ ('b, 'f) ta_rule set" where
  "term_TA' h t = ({(f (map h ts) → h (Fun f ts))|f ts. Fun f ts ⊴ t})"

fun term_TA'_list :: "(('f,'v) term ⇒ 'b) ⇒ ('f, 'v) term ⇒ ('b, 'f) ta_rule list" where
  "term_TA'_list h (Fun f ts) = (TA_rule f (map h ts) (h (Fun f ts))) # concat (map (term_TA'_list h) ts)"
| "term_TA'_list h (Var x) = []"

lemma term_TA'_list:
  shows "fixed_signature.term_TA' h t = set (term_TA'_list h 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 *: "fixed_signature.term_TA' h (Fun f ts) = {f (map h ts) → h (Fun f ts)} ∪ ⋃((λt. fixed_signature.term_TA' h t) ` set ts)"
    unfolding fixed_signature.term_TA'_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: fixed_signature.term_TA'_def dest: supteq_Var_id)

definition term_TA'_impl ::
  "(('f, 'v) term ⇒ 'b :: compare_order) ⇒ ('f :: compare_order,'v) term ⇒ (('b, 'f) ta_rule, unit) RBT_Impl.rbt" where
  "term_TA'_impl h t = rbt_bulkload (map (λk. (k, ())) (term_TA'_list h t))"

lemma term_TA'_impl:
  assumes "FORCE_id R" "FORCE_id Q"
  shows "(term_TA'_impl, fixed_signature.term_TA') ∈
   (⟨Id :: _ :: compare_order rel,Id :: _ :: compare_order rel⟩term_rel → R) → ⟨Id,Id⟩term_rel → ⟨⟨Q,Id⟩ta_rule_rel⟩comp_rs_rel"
  using assms
  apply (refine_vcg)
  subgoal for h' h t' t
    by (auto intro!: relcompI[of _ "λx. if x ∈ set (term_TA'_list h t) then Some () else None"]
      simp: map_of_keys compare_order_class.ord_defs autoref_post_simps rbt_lookup_rbt_bulkload
      term_TA'_impl_def term_TA'_list map2set_rel_def rbt_map_rel_def rbt_map_rel'_def
      split: if_splits intro!: brI)
  done

lemma ta_make_autoref':
  "FORCE_id R ⟹
   (ta_make_code, ta.make)
    ∈ ⟨Id⟩comp_rs_rel → ⟨⟨Id, Id⟩ta_rule_rel⟩comp_rs_rel → ⟨R ×⇩r R⟩list_set_rel → dflt_ta_rel"
  using ta_make_autoref by simp

definition Inl_rule where
  "Inl_rule ≡ λ(f :: 'f) n. f (replicate n (Inl (Var ()))) → Inl (Var ())"

schematic_goal trs_to_ta_L_impl:
  notes [autoref_rules] = term_TA'_impl FORCE_id[of _ fixed_signature.embed_term] FORCE_id[of _ replicate]
    FORCE_id[of _ Inl_rule] ta_make_autoref'
  shows "(?f, fixed_signature.trs_to_ta_L) ∈ ⟨Id ×⇩r Id⟩comp_rs_rel → ⟨⟨Id :: 'f :: compare_order rel,Id :: 'q :: compare_order rel⟩term_rel ×⇩r ⟨Id,Id⟩term_rel⟩comp_rs_rel → dflt_ta_rel"
  unfolding fixed_signature.trs_to_ta_L_def fixed_signature.L_trs_ta_set_def
  unfolding trs_to_ta_extra_simps(1,2) fixed_signature.ta_rules_Inl_eq
  unfolding
    fixed_signature.term_to_ta_L_def fixed_signature.term_to_ta_def fmap_states_ta_def
  unfolding trs_to_ta_extra_simps ta.simps ta.make_def
  unfolding ta.make_def[symmetric] fixed_signature.term_TA'_def[of Inl, symmetric] Inl_rule_def[symmetric]
  by (autoref)

concrete_definition trs_to_ta_L_impl uses trs_to_ta_L_impl

definition Inr_rule where
  "Inr_rule ≡ λ(f :: 'f) n. f (replicate n (Inr (Var ()))) → Inr (Var ())"

schematic_goal trs_to_ta_R_impl:
  notes [autoref_rules] = term_TA'_impl FORCE_id[of _ fixed_signature.embed_term] FORCE_id[of _ replicate]
    FORCE_id[of _ Inr_rule] ta_make_autoref'
  shows "(?f, fixed_signature.trs_to_ta_R) ∈ ⟨Id ×⇩r Id⟩comp_rs_rel → ⟨⟨Id :: 'f :: compare_order rel,Id :: 'q :: compare_order rel⟩term_rel ×⇩r ⟨Id,Id⟩term_rel⟩comp_rs_rel → dflt_ta_rel"
  unfolding fixed_signature.trs_to_ta_R_def fixed_signature.R_trs_ta_set_def
  unfolding trs_to_ta_extra_simps(1,2) fixed_signature.ta_rules_Inr_eq
  unfolding
    fixed_signature.term_to_ta_L_def fixed_signature.term_to_ta_def fmap_states_ta_def
  unfolding trs_to_ta_extra_simps ta.simps ta.make_def
  unfolding ta.make_def[symmetric] fixed_signature.term_TA'_def[of Inr, symmetric] Inr_rule_def[symmetric]
  by (autoref)

concrete_definition trs_to_ta_R_impl uses trs_to_ta_R_impl

declare fixed_signature.embed_term_def [code]

definition lv_trs_to_gtt_impl :: "_ ⇒ (('f :: compare_order, 'v :: compare_order) term × _, unit) RBT_Impl.rbt ⇒ _" where
  "lv_trs_to_gtt_impl F R = (trs_to_ta_L_impl F R, trs_to_ta_R_impl F R)"

lemma prod_binary_function:
  assumes "(f', f) ∈ P → Q → Rf"
  assumes "(g', g) ∈ P → Q → Rg"
  shows "(λx y. (f' x y, g' x y), λx y. (f x y, g x y)) ∈ P → Q → Rf ×⇩r Rg"
  using assms by (auto intro!: fun_relI prod_relI dest: fun_relD)

lemmas trs_to_gtt_autoref [autoref_rules] =
  prod_binary_function[OF trs_to_ta_L_impl.refine trs_to_ta_R_impl.refine, folded fixed_signature.trs_to_gtt_def lv_trs_to_gtt_impl_def]

(* export_code lv_trs_to_gtt_impl in Haskell *)

end