theory GTT_Compose_Impl
imports GTT_Compose GTT_Impl Horn_List
begin
inductive_set Δ⇩ε' :: "('p, 'f) ta ⇒ ('q, 'f) ta ⇒ ('p × '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) ∈ Δ⇩ε' A B) ⟹ (p, q) ∈ Δ⇩ε' A B"
| Δ⇩ε'_eps1: "(p, p') ∈ ta_eps A ⟹ (p, q) ∈ Δ⇩ε' A B ⟹ (p', q) ∈ Δ⇩ε' A B"
| Δ⇩ε'_eps2: "(q, q') ∈ ta_eps B ⟹ (p, q) ∈ Δ⇩ε' A B ⟹ (p, q') ∈ Δ⇩ε' A B"
lemma Δ⇩ε_eq_Δ⇩ε' [code_unfold]:
"Δ⇩ε A B = Δ⇩ε' A B"
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr x) obtain p q where x [simp]: "x = (p, q)" by (cases x)
obtain t where "ground t" "p ∈ ta_res A t" "q ∈ ta_res B t" using lr by (auto simp: Δ⇩ε_def)
then show ?case unfolding x
proof (induct t arbitrary: p q)
case (Fun f ts)
obtain p' ps where p': "f ps → p' ∈ ta_rules A" "(p', p) ∈ (ta_eps A)⇧*" "length ps = length ts"
"⋀i. i < length ts ⟹ ps ! i ∈ ta_res A (ts ! i)" using Fun(3) by auto
obtain q' qs where q': "f qs → q' ∈ ta_rules B" "(q', q) ∈ (ta_eps B)⇧*" "length qs = length ts"
"⋀i. i < length ts ⟹ qs ! i ∈ ta_res B (ts ! i)" using Fun(4) by auto
have "(p', q') ∈ Δ⇩ε' A B"
using Fun(1)[OF nth_mem _ p'(4) q'(4)] Fun(2) Δ⇩ε'_cong[OF p'(1) q'(1)] p'(3) q'(3) by auto
with p'(2) have "(p, q') ∈ Δ⇩ε' A B" by (induct) (auto intro: Δ⇩ε'_eps1)
with q'(2) show "(p, q) ∈ Δ⇩ε' A B" by (induct) (auto intro: Δ⇩ε'_eps2)
qed auto
next
case (rl x) obtain p q where x [simp]: "x = (p, q)" by (cases x)
have "∃t. ground t ∧ p ∈ ta_res A t ∧ q ∈ ta_res B t" using rl unfolding x
proof (induct)
case (Δ⇩ε'_cong f ps p qs q)
obtain ts where ts: "ground (ts i) ∧ ps ! i ∈ ta_res A (ts i) ∧ qs ! i ∈ ta_res B (ts i)"
if "i < length qs" for i using Δ⇩ε'_cong(5) by metis
then show ?case using Δ⇩ε'_cong(1-3)
by (auto intro!: exI[of _ "Fun f (map ts [0..<length qs])"]) blast+
qed (auto intro: ta_res_eps)
then show ?case by (auto simp: Δ⇩ε_def)
qed
definition Δ⇩ε'_rules :: "('p, 'f) ta ⇒ ('q, 'f) ta ⇒ ('p × 'q) horn set" where
"Δ⇩ε'_rules A B =
{zip ps qs →⇩h (p, q) |f ps p qs q. f ps → p ∈ ta_rules A ∧ f qs → q ∈ ta_rules B ∧ length ps = length qs} ∪
{[(p, q)] →⇩h (p', q) |p p' q. (p, p') ∈ ta_eps A} ∪
{[(p, q)] →⇩h (p, q') |p q q'. (q, q') ∈ ta_eps B}"
locale Δ⇩ε'_horn =
fixes A :: "('p, 'f) ta" and B :: "('q, 'f) ta"
begin
sublocale horn "Δ⇩ε'_rules A B" .
lemma Δ⇩ε'_sound:
"Δ⇩ε' 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: Δ⇩ε'_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: Δ⇩ε'_rules_def)
next
case (Δ⇩ε'_eps2 q q' p) then show ?case
by (intro infer[of "[(p, q)]" "(p, q')"]) (auto simp: Δ⇩ε'_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]
by (auto simp: Δ⇩ε'_rules_def)
qed
qed
end
definition Δ⇩ε'_infer0 where
"Δ⇩ε'_infer0 A B = map (map_prod r_rhs r_rhs) (
filter (λ(ra, rb). case (ra, rb) of (f ps → p, g qs → q) ⇒ f = g ∧ ps = [] ∧ qs = []) (List.product (tal_rules A) (tal_rules B)))"
definition Δ⇩ε'_infer1 :: "('p, 'f) ta_list ⇒ ('q, 'f) ta_list ⇒ 'p × 'q ⇒ ('p × 'q) list ⇒ ('p × 'q) list" where
"Δ⇩ε'_infer1 A B pq bs =
map (map_prod r_rhs r_rhs) (filter (λ(ra, rb). case (ra, rb) of (f ps → p, g qs → q) ⇒ f = g ∧ length ps = length qs ∧ (fst pq, snd pq) ∈ set (zip ps qs) ∧ set (zip ps qs) ⊆ set ((fst pq, snd pq) # bs)) (List.product (tal_rules A) (tal_rules B))) @
map (λ(p, p'). (p', snd pq)) (filter (λ(p, p') ⇒ p = fst pq) (tal_eps A)) @
map (λ(q, q'). (fst pq, q')) (filter (λ(q, q') ⇒ q = snd pq) (tal_eps B))"
locale Δ⇩ε'_list =
fixes A :: "('p, 'f) ta_list" and B :: "('q, 'f) ta_list"
begin
sublocale Δ⇩ε'_horn "ta_of A" "ta_of B" .
sublocale horn_list "Δ⇩ε'_rules (ta_of A) (ta_of B)" "Δ⇩ε'_infer0 A B" "Δ⇩ε'_infer1 A B"
apply (unfold_locales)
unfolding Δ⇩ε'_rules_def horn_infer0_union horn_infer1_union
unfolding horn.infer0_def horn.infer1_def Δ⇩ε'_infer0_def Δ⇩ε'_infer1_def set_append Un_assoc[symmetric]
subgoal
apply (subst HOL.trans[OF Un_empty_right Un_empty_right, symmetric, of "set _"])
apply (intro arg_cong2[of _ _ _ _ "op ∪"])
subgoal
apply (auto cong: conj_cong simp del: ex_simps(1) simp: ex_simps(1)[symmetric] simp: r_rhs_def split: ta_rule.splits)
subgoal for f ps p qs q by (rule image_eqI[where x = "(f ps → p, f qs → q)"]) (cases ps; cases qs, auto)+
subgoal for f p q by (auto intro!: exI[of _ f] exI[of _ "[]"])
done
subgoal by auto
subgoal by auto
done
subgoal for x bs
apply (cases x)
apply (intro arg_cong2[of _ _ _ _ "op ∪"])
subgoal for p' q'
apply (auto cong: conj_cong simp del: ex_simps(1) simp: ex_simps(1)[symmetric] simp: r_rhs_def[abs_def])
subgoal for f ps p qs q by (rule image_eqI[where x = "(f ps → p, f qs → q)"]) auto
subgoal by (auto split: ta_rule.splits)
done
subgoal by (auto cong: conj_cong simp del: ex_simps(1) simp: ex_simps(1)[symmetric])
subgoal by (auto cong: conj_cong simp del: ex_simps(1) simp: ex_simps(1)[symmetric])
done
done
lemmas saturate_impl_sound = saturate_impl_sound
lemmas saturate_impl_complete = saturate_impl_complete
end
definition Δ⇩ε'_impl :: "('p, 'f) ta_list ⇒ ('q, 'f) ta_list ⇒ ('p × 'q) list option" where
"Δ⇩ε'_impl A B = horn_list_impl.saturate_impl (Δ⇩ε'_infer0 A B) (Δ⇩ε'_infer1 A B)"
lemma Δ⇩ε'_impl_sound:
"Δ⇩ε'_impl A B = Some xs ⟹ set xs = Δ⇩ε' (ta_of A) (ta_of B)"
using Δ⇩ε'_list.saturate_impl_sound unfolding Δ⇩ε'_impl_def Δ⇩ε'_horn.Δ⇩ε'_sound .
lemma Δ⇩ε'_impl_complete:
fixes A B :: "('q, 'f) ta_list"
shows "Δ⇩ε'_impl A B ≠ None"
proof -
have *: "Δ⇩ε (ta_of A) (ta_of B) ⊆ ta_states (ta_of A) × ta_states (ta_of B)"
by (auto simp: Δ⇩ε_def ta_of_def subsetD[OF ta_res_states])
have "finite (Δ⇩ε (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 Δ⇩ε'_impl_def
by (intro Δ⇩ε'_list.saturate_impl_complete) (auto simp: Δ⇩ε'_horn.Δ⇩ε'_sound Δ⇩ε_eq_Δ⇩ε')
qed
definition GTT_comp_impl :: "('p, 'f) gtt_list ⇒ ('p, 'f) gtt_list ⇒ (_, 'f) gtt_list option" where
"GTT_comp_impl G1 G2 = (case (Δ⇩ε'_impl (snd G1) (fst G2), Δ⇩ε'_impl (fst G2) (snd G1)) of
(Some xs, Some ys) ⇒ Some
(ta_list [] (tal_rules (fst G1) @ tal_rules (fst G2)) (tal_eps (fst G1) @ tal_eps (fst G2) @ xs),
ta_list [] (tal_rules (snd G1) @ tal_rules (snd G2)) (tal_eps (snd G1) @ tal_eps (snd G2) @ ys))
| _ ⇒ None
)"
lemma GTT_comp_impl_sound:
"GTT_comp_impl G1 G2 = Some G ⟹ gtt_of G = GTT_comp (gtt_of G1) (gtt_of G2)"
by (auto simp: GTT_comp_def GTT_comp_impl_def Δ⇩ε_eq_Δ⇩ε' split: option.splits dest!: Δ⇩ε'_impl_sound
intro!: ta_of_eq_ta_makeI)
lemma GTT_comp_impl_complete:
"GTT_comp_impl G1 G2 ≠ None"
using Δ⇩ε'_impl_complete[of "snd G1" "fst G2"] Δ⇩ε'_impl_complete[of "fst G2" "snd G1"]
by (auto simp: GTT_comp_impl_def)
end