Theory Ground_Confluence_Impl

theory Ground_Confluence_Impl
  imports GTT_RRn GTT_Transitive_Closure_Impl GTT_TRS_Impl
    (* TA.Tree_Automata_Wit_Impl "$ISAFOR/Tree_Automata/Tree_Automata_Containment" *)
begin

lemma ta_rule_to_triple [code_unfold]:
  "(λ(g, x, y). g x → y) -` X = case_ta_rule (λg x y. (g, x, y)) ` X"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) then show ?case by (cases x) (auto simp: image_def split: ta_rule.splits)
next
  case (rl x) then show ?case by (cases x) (auto split: ta_rule.splits)
qed

lemma triple_to_triple [code_unfold]:
  "(λ(a, b, y). ((a, b), y)) -` X = (λ((a, b), y). (a, b, y)) ` X"
  by (auto 0 3 simp: image_def split: prod.splits)

definition rtrancl_gtt where
  "rtrancl_gtt R = GTT_rtrancl_impl (trs_to_gtt_impl R)"

definition left_gtt where
  "left_gtt R = rtrancl_gtt R ⤜ (λ(A, B) ⇒ GTT_comp_impl (B, A) (A, B))"

definition right_gtt where
  "right_gtt R = rtrancl_gtt R ⤜ (λ(A, B) ⇒ GTT_comp_impl (A, B) (B, A))"

export_code left_gtt right_gtt in Haskell

export_code GTT_to_RR2 in Haskell

end