theory GTT_Transitive_Closure_Impl
imports GTT_Transitive_Closure GTT_Compose_Impl GTT_Impl Horn_List
begin
text ‹This is very similar to @{file "GTT_Compose_Impl.thy"}.›
definition Δ_trancl_rules :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) horn set" where
"Δ_trancl_rules A B =
Δ⇩ε_rules A B ∪ {[(p, q), (q, r)] →⇩h (p, r) |p q r. True}"
locale Δ_trancl_horn =
fixes A :: "('q, 'f) ta" and B :: "('q, 'f) ta"
begin
sublocale horn "Δ_trancl_rules A B" .
lemma Δ_trancl_infer0:
"infer0 = horn.infer0 (Δ⇩ε_rules A B)"
by (auto simp: Δ⇩ε_rules_def Δ_trancl_rules_def horn.infer0_def)
lemma Δ_trancl_infer1:
"infer1 pq X = horn.infer1 (Δ⇩ε_rules A B) pq X ∪
{(r, snd pq) |r p'. (r, p') ∈ X ∧ p' = fst pq} ∪
{(fst pq, r) |q' r. (q', r) ∈ (insert pq X) ∧ q' = snd pq}"
unfolding Δ_trancl_rules_def horn_infer1_union Un_assoc
apply (intro arg_cong2[of _ _ _ _ "(∪)"] HOL.refl)
by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+
lemma Δ_trancl_sound:
"Δ_trancl A B = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr x) obtain p q where x: "x = (p, q)" by (cases x)
show ?case using lr unfolding x
proof (induct)
case (Δ_cong f ps p qs q) show ?case
apply (intro infer[of "zip ps qs" "(p, q)"])
subgoal using Δ_cong(1-3) by (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
subgoal using Δ_cong(3,5) by (auto simp: zip_nth_conv)
done
next
case (Δ_eps1 p p' q) then show ?case
by (intro infer[of "[(p, q)]" "(p', q)"]) (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
next
case (Δ_eps2 q q' p) then show ?case
by (intro infer[of "[(p, q)]" "(p, q')"]) (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
next
case (Δ_trans p q r) then show ?case
by (intro infer[of "[(p,q), (q,r)]" "(p, r)"]) (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
qed
next
case (rl x) obtain p q where x: "x = (p, q)" by (cases x)
show ?case using rl unfolding x
proof (induct)
case (infer as a) then show ?case
using Δ_cong[of _ "map fst as" "fst a" A "map snd as" "snd a" B]
Δ_eps1[of _ "fst a" A "snd a" B] Δ_eps2[of _ "snd a" B "fst a" A]
Δ_trans[of "fst a" "snd (hd as)" A B "snd a"] by (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
qed
qed
end
definition Δ_trancl_infer0 where
"Δ_trancl_infer0 A B = Δ⇩ε_infer0_list A B"
definition Δ_trancl_infer1 :: "('q, 'f) ta_list ⇒ ('q, 'f) ta_list ⇒ 'q × 'q ⇒ ('q × 'q) list ⇒ ('q × 'q) list" where
"Δ_trancl_infer1 A B pq bs =
Δ⇩ε_infer1_list A B pq bs @
map (λ(r, p'). (r, snd pq)) (filter (λ(r, p') ⇒ p' = fst pq) bs) @
map (λ(q', r). (fst pq, r)) (filter (λ(q', r) ⇒ q' = snd pq) (pq # bs))"
locale Δ_trancl_list =
fixes A :: "('q, 'f) ta_list" and B :: "('q, 'f) ta_list"
begin
sublocale Δ_trancl_horn "ta_of A" "ta_of B" .
sublocale l: horn_list "Δ_trancl_rules (ta_of A) (ta_of B)" "Δ_trancl_infer0 A B" "Δ_trancl_infer1 A B"
apply (unfold_locales)
unfolding Δ_trancl_rules_def horn_infer0_union horn_infer1_union
Δ_trancl_infer0_def Δ_trancl_infer1_def Δ⇩ε_list.infer set_append
by (auto simp flip: ex_simps(1) simp: horn.infer0_def horn.infer1_def intro!: arg_cong2[of _ _ _ _ "(∪)"])
lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete
end
definition Δ_trancl_impl :: "('q, 'f) ta_list ⇒ ('q, 'f) ta_list ⇒ ('q × 'q) list option" where
"Δ_trancl_impl A B = horn_list_impl.saturate_impl (Δ_trancl_infer0 A B) (Δ_trancl_infer1 A B)"
lemma Δ_trancl_impl_sound:
"Δ_trancl_impl A B = Some xs ⟹ set xs = Δ_trancl (ta_of A) (ta_of B)"
using Δ_trancl_list.saturate_impl_sound unfolding Δ_trancl_impl_def Δ_trancl_horn.Δ_trancl_sound .
lemma Δ_trancl_impl_complete:
fixes A B :: "('q, 'f) ta_list"
shows "Δ_trancl_impl A B ≠ None"
proof -
note * = Δ_trancl_subset_states[of "ta_of A" "ta_of B"]
have "finite (Δ_trancl (ta_of A) (ta_of B))"
by (cases A; cases B; rule finite_subset[OF *])
(auto simp: ta_of_def ta_states_def r_states_def intro!: finite_cartesian_product)
then show ?thesis unfolding Δ_trancl_impl_def
by (intro Δ_trancl_list.saturate_impl_complete) (auto simp: Δ_trancl_horn.Δ_trancl_sound)
qed
definition GTT_trancl_impl :: "('q, 'f) gtt_list ⇒ (_, 'f) gtt_list option" where
"GTT_trancl_impl G = (case (Δ_trancl_impl (snd G) (fst G), Δ_trancl_impl (fst G) (snd G)) of
(Some xs, Some ys) ⇒ Some
(ta_list [] (tal_rules (fst G)) (tal_eps (fst G) @ xs),
ta_list [] (tal_rules (snd G)) (tal_eps (snd G) @ ys))
| _ ⇒ None
)"
lemma GTT_trancl_impl_sound:
"GTT_trancl_impl G = Some H ⟹ gtt_of H = GTT_trancl (gtt_of G)"
by (auto simp: GTT_trancl_def GTT_trancl_impl_def split: option.splits dest!: Δ_trancl_impl_sound
intro!: ta_of_eq_ta_makeI)
lemma GTT_trancl_impl_complete:
"GTT_trancl_impl G ≠ None"
using Δ_trancl_impl_complete[of "snd G" "fst G"] Δ_trancl_impl_complete[of "fst G" "snd G"]
by (auto simp: GTT_trancl_impl_def)
definition Δ⇩_trancl_infer0_rbt where
"Δ⇩_trancl_infer0_rbt A B = Δ⇩ε_infer0_rbt A B"
definition Δ_trancl_infer1_rbt where
"Δ_trancl_infer1_rbt A B pq X = Δ⇩ε_infer1_rbt A B pq X @
map (λ(r, p'). (r, snd pq)) (filter (λ(r, p') ⇒ p' = fst pq) (RBT_Impl.keys X)) @
map (λ(q', r). (fst pq, r)) (filter (λ(q', r) ⇒ q' = snd pq) (pq # (RBT_Impl.keys X)))"
lemma Δ_trancl_infer0_rbt:
assumes A': "(A', A) ∈ dflt_ta_rel"
assumes B': "(B', B) ∈ dflt_ta_rel"
shows "(Δ⇩_trancl_infer0_rbt A' B', horn.infer0 (Δ_trancl_rules A B)) ∈ ⟨Id⟩it_set_rel"
unfolding Δ_trancl_horn.Δ_trancl_infer0 Δ⇩_trancl_infer0_rbt_def
by (rule Δ⇩ε_infer0_rbt[OF assms])
lemma Δ_trancl_infer1_rbt:
assumes A': "(A', A) ∈ dflt_ta_rel"
assumes B': "(B', B) ∈ dflt_ta_rel"
assumes pq': "(pq', pq) ∈ Id"
assumes X': "(X', X) ∈ ⟨Id⟩dflt_rs_rel"
shows "(Δ_trancl_infer1_rbt A' B' pq' X', horn.infer1 (Δ_trancl_rules A B) pq X) ∈ ⟨Id⟩it_set_rel"
unfolding Δ_trancl_infer1_rbt_def Δ_trancl_horn.Δ_trancl_infer1 Un_assoc
using assms(3) assms(4)[THEN keys_it]
apply (intro union_it_set_rel Δ⇩ε_infer1_rbt[OF assms])
by (auto 0 0 simp: it_set_rel_def br_def split: prod.split) force+
schematic_goal Δ_trancl_impl_rbt:
assumes "(A', A) ∈ dflt_ta_rel"
assumes "(B', B) ∈ dflt_ta_rel"
shows "(?f, horn.saturate_impl (Δ_trancl_rules A B)) ∈ ⟨⟨Id⟩dflt_rs_rel⟩nres_rel"
apply (rule horn_linorder.saturate_impl_rbt)
apply (rule Δ_trancl_infer0_rbt[OF assms])
apply (intro fun_relI)
apply (rule Δ_trancl_infer1_rbt[OF assms])
apply assumption+
done
concrete_definition Δ_trancl_rbt uses Δ_trancl_impl_rbt
prepare_code_thms Δ_trancl_rbt_def
schematic_goal GTT_trancl_rbt_aux:
assumes [autoref_rules]: "(G', G) ∈ dflt_gtt_rel"
defines "Δ12 ≡ Δ_trancl (snd G) (fst G)" and "Δ21 ≡ Δ_trancl (fst G) (snd G)"
assumes Δ: "(Δ12', Δ12) ∈ ⟨Id ×⇩r Id⟩dflt_rs_rel" "(Δ21', Δ21) ∈ ⟨Id ×⇩r Id⟩dflt_rs_rel"
notes [autoref_rules] = Δ[THEN keys_list]
shows "(?f, GTT_trancl G) ∈ dflt_gtt_rel"
unfolding GTT_trancl_def Δ12_def[symmetric] Δ21_def[symmetric]
by autoref
concrete_definition GTT_trancl_rbt_aux uses GTT_trancl_rbt_aux
schematic_goal GTT_trancl_rbt:
assumes G: "(G', G) ∈ dflt_gtt_rel"
notes G' = param_prod(4,5)[THEN fun_relD, OF G]
notes * = horn.saturate_impl_sound[unfolded SPEC_eq_is_RETURN, of "Δ_trancl_rules _ _", unfolded Δ_trancl_horn.Δ_trancl_sound[symmetric]]
shows "(?f, RETURN (GTT_trancl G)) ∈ ⟨dflt_gtt_rel⟩nres_rel"
apply (rule HOL.back_subst[of "λx. (x, _) ∈ _"])
apply (rule bind_RETURN[OF conc_trans_additional(1)[OF Δ_trancl_rbt.refine[OF G'(2) G'(1), THEN nres_relD] *, THEN nres_relI]])
apply (rule bind_RETURN[OF conc_trans_additional(1)[OF Δ_trancl_rbt.refine[OF G'(1) G'(2), THEN nres_relD] *, THEN nres_relI]])
apply (rule param_RETURN[THEN fun_relD])
apply (rule GTT_trancl_rbt_aux[OF G, unfolded prod_rel_id_simp]; assumption+)
unfolding nres_of_simps(3)[symmetric] nres_of_bind[symmetric]
by (rule refl)
concrete_definition GTT_trancl_rbt uses GTT_trancl_rbt
export_code GTT_trancl_rbt in Haskell
end