Theory GTT_Transitive_Closure_Impl

theory GTT_Transitive_Closure_Impl
  imports GTT_Compose_Impl GTT_Transitive_Closure
begin

(* Future plan: compute the new epsilon transitions in a single inference pass *)

inductive_set Δ_trancl' :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for A B where
  Δ_cong: "f ps → p ∈ ta_rules A ⟹ f qs → q ∈ ta_rules B ⟹ length ps = length qs ⟹
   (⋀i. i < length qs ⟹ (ps ! i, qs ! i) ∈ Δ_trancl' A B) ⟹ (p, q) ∈ Δ_trancl' A B"
| Δ_eps1: "(p, p') ∈ ta_eps A ⟹ (p, q) ∈ Δ_trancl' A B ⟹ (p', q) ∈ Δ_trancl' A B"
| Δ_eps2: "(q, q') ∈ ta_eps B ⟹ (p, q) ∈ Δ_trancl' A B ⟹ (p, q') ∈ Δ_trancl' A B"
| Δ_trans: "(p, q) ∈ Δ_trancl A B ⟹ (q, r) ∈ Δ_trancl' A B ⟹ (p, r) ∈ Δ_trancl' A B"

"GTT_rtrancl' G ≡">definition "GTT_rtrancl' G ≡
  (ta.make {} (ta_rules (fst G)) (ta_eps (fst G) ∪ Δ_trancl' (snd G) (fst G)),
   ta.make {} (ta_rules (snd G)) (ta_eps (snd G) ∪ Δ_trancl' (fst G) (snd G)))"

lemma [code_unfold]:
  "GTT_rtrancl G = GTT_rtrancl' G"
  oops

(* But for now let's implement 𝒢⇩N as simply as possible *)

partial_function (tailrec) GTT_rtrancl_impl :: "('q, 'f) gtt_list ⇒ ('q, 'f) gtt_list option" where
  [code]: "GTT_rtrancl_impl G = (case GTT_comp_impl G G of
       Some G' ⇒ (let G'' = map_prod uniq_ta uniq_ta G' in
       (if gtt_of G = gtt_of G'' then Some G else GTT_rtrancl_impl G''))
     | None ⇒ None)"

lemma step_Δ⇩ε_to_GTT_comp:
  "step_Δ⇩ε A B = GTT_comp (A, B) (A, B)"
  by (auto simp: GTT_comp_def)

lemma make_Δ⇩ε_GTT_comp_commute:
  "GTT_comp (make_Δ⇩ε A B n) (make_Δ⇩ε A B n) =
   make_Δ⇩ε (fst (GTT_comp (A, B) (A, B))) (snd (GTT_comp (A, B) (A, B))) n"
  by (induct n) (simp_all add: step_Δ⇩ε_to_GTT_comp)

lemma step_Δ⇩ε_decrease:
  assumes "finite (ta_states A)" "finite (ta_states B)"
  shows "least_fp_N A B = 0 ∧ step_Δ⇩ε A B = (A, B) ∨ least_fp_N A B = Suc (case_prod least_fp_N (step_Δ⇩ε A B))"
proof -
  have *: "(∀x ≥ Suc m. P x) ⟷ (∀x ≥ m. P (Suc x))" for m P
    using Suc_le_D by blast
  show ?thesis
  apply (cases "least_fp_N A B")
  subgoal using spec[OF LeastI_ex[OF trans_closure_fixpoint[OF assms], folded least_fp_N_def], of 1]
    by simp
  subgoal for n
    using Least_Suc[of "λn. ∀m ≥ n. make_Δ⇩ε A B m = make_Δ⇩ε A B n", OF LeastI_ex[OF trans_closure_fixpoint[OF assms]]]
      not_less_Least[of 0 "λn. ∀m ≥ n. make_Δ⇩ε A B m = make_Δ⇩ε A B n"]
    unfolding least_fp_N_def * make_Δ⇩ε.simps Let_def step_Δ⇩ε_to_GTT_comp
    by (auto simp: case_prod_beta make_Δ⇩ε_GTT_comp_commute least_fp_N_def[symmetric])
  done
qed

lemma finite_ta_states_ta_of:
  "finite (ta_states (ta_of A))"
  by (cases A) (auto simp: ta_of_def ta_states_def r_states_def)

lemma GTT_rtrancl_impl_sound:
  "GTT_rtrancl_impl G = Some G' ⟹ gtt_of G' = GTT_rtrancl (gtt_of G)"
  unfolding 𝒢⇩N_def fst_map_prod snd_map_prod
proof (induct "least_fp_N (ta_of (fst G)) (ta_of (snd G))" arbitrary: G rule: less_induct)
  case less show ?case
  proof (cases "GTT_comp_impl G G")
    case None then show ?thesis using less(2) by (subst (asm) GTT_rtrancl_impl.simps) auto
  next
    case (Some G'')
    show ?thesis
      using less(1)[unfolded map_prod_def[abs_def] case_prod_beta, of "map_prod uniq_ta uniq_ta G''"] less(2)
        arg_cong[OF GTT_comp_impl_sound[OF Some], of fst, symmetric]
        arg_cong[OF GTT_comp_impl_sound[OF Some], of snd, symmetric]
      apply (subst (asm) GTT_rtrancl_impl.simps)
      apply (cases rule: disjE[OF
       step_Δ⇩ε_decrease[OF finite_ta_states_ta_of finite_ta_states_ta_of, unfolded step_Δ⇩ε_to_GTT_comp,
       of "fst G" "snd G", unfolded case_prod_beta]])
       apply (auto simp: Some map_prod_def case_prod_beta)[1]
      apply (simp only: make_Δ⇩ε.simps step_Δ⇩ε_to_GTT_comp)
      apply (auto simp: make_Δ⇩ε_GTT_comp_commute Some Let_def map_prod_def case_prod_beta
        dest: GTT_comp_impl_sound split: if_splits)
      done
  qed
qed

(* export_code GTT_rtrancl_impl in Haskell *)

end