Theory CR.Okui_Criterion_Impl
text ‹In this theory, the executable function ‹sim_cp_impl› is defined.
It is proven that it computes exactly the set of simultaneous critical pairs.›
theory Okui_Criterion_Impl
imports
Okui_subsumes_DC
First_Order_Rewriting.Trs_Impl
begin
lemma map2_to_map: "map2 (λ x y. f x y) xs [0..<length xs] = map (λ i. f (xs ! i) i) [0..<length xs]"
by (intro nth_equalityI, auto)
lemma map2_to_map': "map2 (λ x y. f x y) [0..<length xs] xs = map (λ i. f i (xs ! i)) [0..<length xs]"
by (intro nth_equalityI, auto)
lemma distinct_filter_map: assumes dist: "distinct xs"
and inj: "inj_on f (set xs - {x. ¬ g (f x)})"
shows "distinct (filter g (map f xs))"
proof (intro distinct_filter2 allI impI conjI; unfold length_map, goal_cases)
case (1 i j)
hence diff: "xs ! i ≠ xs ! j" using dist unfolding distinct_conv_nth by auto
from 1 have "xs ! i ∈ set xs - {x. ¬ g (f x)}" "xs ! j ∈ set xs - {x. ¬ g (f x)}" by auto
from inj_onD[OF inj _ this] 1 diff
show ?case by auto
qed
lemma distinct_concat_lists: assumes "⋀ xs. xs ∈ set xss ⟹ distinct xs"
shows "distinct (concat_lists xss)"
using assms
proof (induct xss)
case (Cons xs xss)
have IH: "distinct (concat_lists xss)"
by (rule Cons(1)[OF Cons(2)], auto)
from Cons(2)[of xs] have xs: "distinct xs" by auto
show ?case unfolding concat_lists.simps
unfolding distinct_concat_iff set_map removeAll_filter_not_eq
proof (intro conjI allI impI, goal_cases)
case 1
show ?case
by (rule distinct_filter_map[OF IH inj_onI], auto)
next
case (2 yss)
then obtain zs where zs: "zs ∈ set (concat_lists xss)" and yss: "yss = map (λa. a # zs) xs" by auto
show ?case unfolding yss distinct_map
by (intro conjI[OF xs inj_onI], auto)
next
case (3 yss zss)
from 3 obtain ys where ys: "ys ∈ set (concat_lists xss)" and yss: "yss = map (λa. a # ys) xs" by auto
from 3 obtain zs where zs: "zs ∈ set (concat_lists xss)" and zss: "zss = map (λa. a # zs) xs" by auto
from 3 have diff: "yss ≠ zss" by auto
from diff[unfolded yss zss] have diff: "ys ≠ zs" by auto
show ?case
proof (rule ccontr)
assume "¬ ?thesis"
from this[unfolded yss zss, simplified]
obtain x1 x2 where "x1 # ys = x2 # zs" by auto
with diff show False by auto
qed
qed
qed (simp add: concat_lists.simps)
lemma distinct_maps: assumes xs: "distinct xs"
and disj: "⋀ x y. x ∈ set xs ⟹ y ∈ set xs ⟹ x ≠ y ⟹ set (f x) ∩ set (f y) = {}"
and dist: "⋀ x. x ∈ set xs ⟹ distinct (f x)"
shows "distinct (List.maps f xs)"
unfolding List.maps_eq distinct_concat_iff removeAll_filter_not_eq
proof (intro conjI allI impI, goal_cases)
case 2
thus ?case using dist by auto
next
case 3
thus ?case using disj by auto
next
case 1
have inj: "inj_on f (set xs - {x. set (f x) = {}})"
proof (intro inj_onI, goal_cases)
case (1 x y)
with disj[of x y] show ?case by auto
qed
show ?case
by (rule distinct_filter_map[OF xs], insert inj, auto simp: inj_on_def)
qed
lemma distinct_fun_poss_list: "distinct (fun_poss_list t)"
proof (induct t)
case (Fun f ts)
have id: "map2 (λi. map ((#) i)) [0..<length ts] (map fun_poss_list ts)
= map (λ i. map ((#) i) (fun_poss_list (ts ! i))) [ 0..< length ts]"
by (intro nth_equalityI, auto)
have id2: "set [0..<length ts] = {..<length ts}" by auto
show ?case unfolding fun_poss_list.simps distinct.simps distinct_concat_iff id
unfolding set_map id2 removeAll_filter_not_eq
proof (intro conjI allI impI distinct_filter_map inj_onI, goal_cases)
case (3 i j)
thus ?case by (cases "fun_poss_list (ts ! i)"; cases "fun_poss_list (ts ! j)"; auto)
next
case (4 ps)
then obtain i where i: "i < length ts" and ps: "ps = map ((#) i) (fun_poss_list (ts ! i))"
by auto
from Fun[of "ts ! i"] i ps
show ?case by (auto simp: distinct_map)
qed auto
qed auto
lemma those_map_Some[simp]: "those (map Some xs) = Some xs" by (induct xs, auto)
lemma poss_to_pterm[simp]: "poss (to_pterm t) = poss t"
by (induct t, auto)
lemma linear_term_to_pterm[simp]: "linear_term (to_pterm t) = linear_term t"
by (simp add: distinct_vars_eq_linear vars_to_pterm)
lemma to_pterm_subt_at[simp]: "p ∈ poss t ⟹ (to_pterm t) |_p = to_pterm (t |_ p)"
by (induct t arbitrary: p, auto)
lemma vars_term_to_pterm[simp]: "vars_term (to_pterm t) = vars_term t"
by (induct t, auto)
lemma ctxt_of_pos_term_subt_at: "p ∈ poss t ⟹ ctxt_of_pos_term (p @ q) t |_c p = ctxt_of_pos_term q (t |_ p)"
proof (induct p arbitrary: t)
case (Cons i p t)
then obtain f ts where "t = Fun f ts" "i < length ts" "p ∈ poss (ts ! i)" by (cases t, auto)
with Cons(1)[OF this(3)]
show ?case by auto
qed auto
context single_redex
begin
interpretation join_op: op_proof_term "R" "join"
using op_proof_term.intro[OF left_lin_no_var_lhs_axioms] op_proof_term_axioms.intro[of R join] join_with_source by force
lemma difference_join_A: assumes C_def: "C = (ctxt_of_pos_term q A)⟨to_pterm (lhs α) ⋅ ⟨As⟩⇩α⟩"
and ap: "(α, p) ∈ set (redex_patterns A)"
and q: "q ∈ poss A"
and "left_lin_wf_trs R"
shows "Δ ⊔ C = Some A"
proof -
interpret left_lin_wf_trs R by fact
from a_well have A: "A ∈ wf_pterm R" .
define B where "B = Δ"
have Aq: "A |_ q = Prule α (map (λi. A |_ (q @ [i])) [0..<length (var_rule α)])" by (rule aq)
define As' where "As' = As"
define Left where "Left = Prule α (map (to_pterm ∘ source) As')"
define Right where "Right = to_pterm (lhs α) ⋅ ⟨As'⟩⇩α"
have "to_rule α ∈ R" using A by (metis rule_in_TRS)
hence "is_Fun (lhs α)"
by (metis is_Fun_Fun_conv wf_trs_alt wf_trs_imp_lhs_Fun)
then obtain f ls where lhs: "lhs α = Fun f ls" by auto
define list where "list = map2 (⊔) (map (to_pterm ∘ source) As) (map ⟨As⟩⇩α (var_rule α))"
have lenl: "length list = length As" unfolding list_def by simp
have "Left ⊔ Right = Left ⊔ (to_pterm (lhs α) ⋅ ⟨As⟩⇩α)"
unfolding Right_def Left_def As'_def by auto
also have id: "to_pterm (lhs α) ⋅ ⟨As⟩⇩α = Pfun f (map (λ l. to_pterm l ⋅ ⟨As⟩⇩α) ls)"
unfolding lhs to_pterm.simps unfolding lhs[symmetric] by simp
also have "Left ⊔ … = (
case those list of None ⇒ None
| Some xs ⇒ Some (Prule α xs))" unfolding Left_def As'_def join.simps list_def unfolding id[symmetric]
unfolding lhs_subst_trivial by simp
also have "list = map Some As"
proof (intro nth_equalityI; unfold lenl)
fix i
assume i: "i < length As"
hence "list ! i = to_pterm (source (As ! i)) ⊔ ⟨As⟩⇩α (var_rule α ! i)" unfolding list_def
by auto
also have "… = Some (As ! i)" using i
by (metis Residual_Join_Deletion.join_sym as_well join_with_source length_as lhs_subst_var_i)
finally show "list ! i = map Some As ! i" using i by simp
qed simp
also have "those … = Some As" by (rule those_map_Some)
finally have RL: "Right ⊔ Left = Some (Prule α As')"
by (simp add: As'_def Residual_Join_Deletion.join_sym)
have wf_ctxt:"ctxt_of_pos_term q A ∈ wf_pterm_ctxt R"
by (simp add: a_well ctxt_of_pos_term_well q)
have ctxt_alt:"(ctxt_of_pos_term p (to_pterm (source A)))⟨Left⟩ = (to_pterm_ctxt (source_ctxt (ctxt_of_pos_term q A)))⟨Left⟩"
by (simp add: p pq to_pterm_ctxt_at_pos)
have "(ctxt_of_pos_term q A)⟨Right⟩ ⊔ (ctxt_of_pos_term p (to_pterm (source A)))⟨Left⟩ = Some A"
using join_op.apply_f_ctxt[OF wf_ctxt RL] unfolding ctxt_alt using a As'_def by argo
then have main: "(ctxt_of_pos_term p (to_pterm (source A)))⟨Left⟩ ⊔ (ctxt_of_pos_term q A)⟨Right⟩ = Some A"
by (simp add: Residual_Join_Deletion.join_sym)
hence "B ⊔ C = Some A"
unfolding single_redex_pterm C_def B_def Left_def Right_def As'_def .
thus ?thesis unfolding B_def .
qed
end
lemma get_overlapping_part_alt:
"get_overlapping_part A B = (let As = filter (λ A'. possL A' ∩ possL B ≠ {}) (single_steps A) in ⨆ As)"
unfolding get_overlapping_part_def
apply (intro arg_cong[of _ _ "λ x. Let x _"])
apply (intro arg_cong[of _ _ "λ x. filter x _"])
by (simp add: finite_labelposs)
context left_lin_wf_trs
begin
sublocale left_lin_no_var_lhs ..
lemma single_steps_split: assumes A: "A ∈ wf_pterm R" and ne: "¬ is_empty_step A"
shows "∃ A' B. single_steps A = B # single_steps A' ∧ A' ∈ wf_pterm R ∧ B ∈ wf_pterm R ∧ B ⊔ A' = Some A"
proof -
from ne have "single_steps A ≠ []"
using redex_poss_empty_imp_empty_step by fastforce
then obtain α p rps where rpA: "redex_patterns A = (α, p) # rps" by (cases "single_steps A", auto)
define B where "B = ll_single_redex (source A) p α"
define Bs where "Bs = map (λ (α, p). ll_single_redex (source A) p α) rps"
have sA: "single_steps A = B # Bs" unfolding rpA B_def Bs_def by auto
from sA have BA: "B ∈ set (single_steps A)" by auto
with A have B: "B ∈ wf_pterm R"
by (metis A single_step_wf)
have ap: "(α, p) ∈ set (redex_patterns A)" using rpA by auto
from A ap have p: "p ∈ poss (source A)"
using redex_patterns_label by blast
from A ap obtain q where qq: "q ∈ poss A" "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term q A)"
and Aq: "A |_ q = Prule α (map (λi. A |_ (q @ [i])) [0..<length (var_rule α)])"
by (metis labeled_source_to_term poss_labeled_source poss_term_lab_to_term redex_patterns_label)
interpret single_redex R A B p q α
by (unfold_locales; intro A p qq B_def Aq)
from BA A have srcB: "source B = source A"
by (metis source_delta)
have sort: "sorted_wrt (ord.lexordp (<)) (map snd (redex_patterns A))"
by (rule redex_patterns_sorted[OF A])
define C where "C = (ctxt_of_pos_term q A)⟨to_pterm (lhs α) ⋅ ⟨As⟩⇩α⟩"
from deletion have ABC: "A -⇩p B = Some C" unfolding C_def by auto
have srcC: "source C = source A" using ABC A B
by (metis a_well ABC deletion_source)
from ABC have C: "C ∈ wf_pterm R"
using deletion_well by force
show ?thesis
proof (rule exI[of _ C], rule exI[of _ B], intro conjI B C)
from difference_join_A[OF C_def ap qq(1)]
show join: "B ⊔ C = Some A"
using left_lin_wf_trs_axioms by metis
from redex_patterns_join[OF B C join]
have "set (redex_patterns A) = set (redex_patterns B) ∪ set (redex_patterns C)" by auto
also have "set (redex_patterns A) = insert (α,p) (set rps)" unfolding rpA by auto
also have "set (redex_patterns B) = {(α,p)}" unfolding B_def using A
using p redex_patterns_single rule_in_TRS by auto
finally have "set rps - {(α,p)} = set (redex_patterns C) - {(α,p)}" by blast
also have "set rps - {(α,p)} = set rps"
using distinct_snd_rdp[OF A] rpA unfolding distinct_map by auto
also have "set (redex_patterns C) - {(α,p)} = set (redex_patterns C)"
proof (rule ccontr)
assume "¬ ?thesis"
hence mem: "(α,p) ∈ set (redex_patterns C)" by auto
have "is_Fun (lhs α)"
by (metis is_Fun_Fun_conv rule_in_TRS wf_trs_alt wf_trs_imp_lhs_Fun)
then obtain f ls where lhs: "lhs α = Fun f ls" by auto
from mem[unfolded redex_patterns_label[OF C]]
have "get_label (labeled_source C |_ p) = Some (α, 0)" by auto
also have "labeled_source C |_ p = labeled_source (to_pterm (lhs α) ⋅ ⟨As⟩⇩α)"
unfolding C_def
by (metis (no_types, lifting) a_well label_source_ctxt labeled_source_to_term p poss_term_lab_to_term pq q replace_at_subt_at)
also have "get_label … = None" unfolding lhs by auto
finally show False by auto
qed
finally have "set rps = set (redex_patterns C)" by auto
from redex_patterns_equal[OF C _ this] sort[unfolded rpA]
have rps: "rps = redex_patterns C" by auto
show "single_steps A = B # single_steps C" unfolding B_def rpA
unfolding srcC rps by auto
qed
qed
lemma join_single_steps: assumes "A ∈ wf_pterm R" "¬ is_empty_step A"
shows "⨆ (single_steps A) = Some A"
proof -
define xs where "xs = single_steps A"
from assms have "xs ≠ []" unfolding xs_def
using redex_poss_empty_imp_empty_step by fastforce
with xs_def assms(1)
show ?thesis
proof (induct xs arbitrary: A)
case (Cons B xs A)
have A: "A ∈ wf_pterm R" by fact
from Cons(2-) have "¬ is_empty_step A"
by (metis list.discI map_is_Nil_conv redex_patterns_to_pterm source_empty_step)
from single_steps_split[OF A this] Cons(2) obtain A' where
xs: "xs = single_steps A'" and A': "A' ∈ wf_pterm R"
and BA': "B ⊔ A' = Some A" by auto
note IH = Cons(1)[OF this(1-2)]
show ?case
proof (cases "xs = []")
case True
with Cons have "single_steps A = [B]" by auto
with single_steps_singleton[OF A this]
have "single_steps A = [A]" by auto
with A show ?thesis by auto
next
case False
from IH[OF this]
have IH: "⨆ (single_steps A') = Some A'" by auto
show ?thesis unfolding Cons(2)[symmetric] xs using IH BA'
by (metis False join_list.simps(3) join_opt.simps(1) neq_Nil_conv xs)
qed
qed simp
qed
lemma redex_patt_possL: "A ∈ wf_pterm R ⟹ (α,p) ∈ set (redex_patterns A) ⟹ p ∈ possL A"
by (simp add: get_label_imp_labelposs redex_patterns_label)
lemma get_overlap_cond_alt: assumes "A ∈ wf_pterm R" "¬ is_empty_step A"
shows "get_overlapping_part A B = Some A ⟷ (∀ A' ∈ set (single_steps A). possL A' ∩ possL B ≠ {})"
proof -
from assms(1) have ss_wf: "set (single_steps A) ⊆ wf_pterm R"
using single_step_wf by auto
define filt where "filt = filter (λA'. possL A' ∩ possL B ≠ {}) (single_steps A)"
define all where "all = (single_steps A)"
from ss_wf have filt_wf: "set filt ⊆ wf_pterm R" by (auto simp: filt_def)
have id: "⨆ (single_steps A) = Some A" using join_single_steps[OF assms] .
show ?thesis
proof
assume "∀A'∈set (single_steps A). possL A' ∩ possL B ≠ {}"
hence filt: "filt = single_steps A" by (auto simp: filt_def)
thus "get_overlapping_part A B = Some A" unfolding get_overlapping_part_alt filt_def using id by auto
next
assume "get_overlapping_part A B = Some A"
from this[unfolded get_overlapping_part_alt Let_def]
have "⨆ filt = Some A" by (auto simp: filt_def)
from redex_patterns_join_list[OF this]
have "⋃ (set (map (set ∘ redex_patterns) filt)) = set (redex_patterns A)" using filt_wf by auto
also have "… = ⋃ (set (map (set ∘ redex_patterns) all))"
using redex_patterns_join_list[OF id] ss_wf unfolding all_def
by blast
finally have eq: "(⋃x∈set filt. set (redex_patterns x)) = (⋃x∈set all. set (redex_patterns x))" by simp
show "∀A'∈set (single_steps A). possL A' ∩ possL B ≠ {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A' where A': "A' ∈ set (single_steps A)" "A' ∈ set all" "A' ∉ set filt"
unfolding all_def filt_def by auto
from single_step_redex_patterns[OF assms(1) A'(1)] obtain p α where
"A' = ll_single_redex (source A) p α" and "(α, p) ∈ set (redex_patterns A)" and αpA: "redex_patterns A' = [(α, p)]"
by auto
hence "(α,p) ∈ (⋃x∈set all. set (redex_patterns x))" using A' by fastforce
from this[folded eq] obtain B' where B': "B' ∈ set filt" and αpB: "(α,p) ∈ set (redex_patterns B')" by fastforce
from B' A' have AB: "A' ≠ B'" and BA: "B' ∈ set (single_steps A)" unfolding filt_def by auto
from single_steps_measure[OF A'(1) BA assms(1) AB] have "measure_ov A' B' = 0" by auto
hence "possL A' ∩ possL B' = {}" by (simp add: finite_labelposs)
moreover have "p ∈ possL A'" using A'(1) αpA ss_wf by (intro redex_patt_possL, auto)
moreover have "p ∈ possL B'" using αpB BA ss_wf by (intro redex_patt_possL, auto)
ultimately show False by blast
qed
qed
qed
end
lemma wf_pterm_ctxt_apply: "(C⟨t⟩ ∈ wf_pterm R) = (C ∈ wf_pterm_ctxt R ∧ t ∈ wf_pterm R)"
proof (induct C)
case Hole
then show ?case by simp
next
case (Cfun f ss1 C ss2)
then show ?case by (auto simp add: wf_pterm.simps[of "Pfun _ _"] wf_pterm_ctxt.simps[of "Cfun _ _ _ _"])
next
case (Crule α ss1 C ss2)
then show ?case by (auto simp add: wf_pterm.simps[of "Prule _ _"] wf_pterm_ctxt.simps[of "Crule _ _ _ _"])
qed
context left_lin_no_var_lhs
begin
lemma vars_rule_vars_lhs: assumes "to_rule α ∈ R"
shows "var_rule α = vars_term_list (lhs α)"
proof -
from assms left_lin
have "linear_term (lhs α)" unfolding left_linear_trs_def by blast
thus ?thesis by (metis linear_term_var_vars_term_list)
qed
end
context left_lin_wf_trs
begin
lemma possL_root_step: assumes A: "A ∈ wf_pterm R"
and rp_root: "redex_patterns A = [(α, [])]"
shows "possL A = fun_poss (lhs α)"
proof -
have rule: "to_rule α ∈ R"
using A rp_root redex_pattern_rule_symbol by simp
from A rp_root have "possL A = possL (ll_single_redex (source A) [] α)"
using single_steps_singleton by fastforce
also have "… = fun_poss (lhs α)" using A rp_root
by (subst single_redex_possL[OF rule], auto)
finally show ?thesis .
qed
end
context ren_wf_trs
begin
sublocale R:left_lin_no_var_lhs R ..
sublocale S:left_lin_no_var_lhs S ..
definition alt_cond where "alt_cond τ rdp_A l β q A B As renamed_lhs_αs =
(A ∈ wf_pterm R ∧ B ∈ wf_pterm S ∧
redex_patterns A = rdp_A ∧ redex_patterns B = [(β, q)] ∧
renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A) ∧
(q = [] ∨ snd (hd rdp_A) = []) ∧
l = replace_at (hd renamed_lhs_αs) q (map_vars_term (ren_l ren) (lhs β)) ∧
mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) = Some τ ∧
join_list As = Some A
∧ As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]
∧ B = replace_at (to_pterm (l ⋅ τ)) q (Prule β (map (to_pterm ∘ τ ∘ ren_l ren) (vars_term_list (lhs β))))
∧ (∀ (α,p) ∈ set rdp_A. (@) p ` fun_poss (lhs α) ∩ (@) q ` fun_poss (lhs β) ≠ {})
∧ (∀ (α,p) ∈ set rdp_A. to_rule α ∈ R)
∧ to_rule β ∈ S
∧ rdp_A ≠ [])"
lemma sim_cp_alt_def:
"sim_cp = { (A, B) | τ rdp_A l β q A B As renamed_lhs_αs.
alt_cond τ rdp_A l β q A B As renamed_lhs_αs}" (is "_ = ?RHS")
proof -
have "sim_cp = { (A, B) | τ rdp_A l β q A B As renamed_lhs_αs.
A ∈ wf_pterm R ∧ B ∈ wf_pterm S ∧
redex_patterns A = rdp_A ∧ redex_patterns B = [(β, q)] ∧
renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A) ∧
(q = [] ∨ snd (hd rdp_A) = []) ∧
l = replace_at (hd renamed_lhs_αs) q (map_vars_term (ren_l ren) (lhs β)) ∧
mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) = Some τ ∧
join_list As = Some A ∧
As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (var_rule αi))⟩)
rdp_A [0..<length rdp_A] ∧
B = replace_at (to_pterm (l ⋅ τ)) q (Prule β (map (to_pterm ∘ τ ∘ ren_l ren) (var_rule β))) ∧
get_overlapping_part A B = Some A ∧ True}"
unfolding sim_cp_def map_map by blast
also have "… = ?RHS" unfolding alt_cond_def
proof (intro Collect_cong ex_cong1 conj_cong refl)
fix τ rdp_A l β q A B As renamed_lhs_αs
assume A: "A ∈ wf_pterm R" and B: "B ∈ wf_pterm S" and rdp_A: "redex_patterns A = rdp_A"
and rdp_B: "redex_patterns B = [(β, q)]"
and join: "join_list As = Some A"
have β: "to_rule β ∈ S" using B rdp_B S.redex_pattern_rule_symbol by simp
from join have Asne: "As ≠ []" by auto
show "(As =
map2
(λx. case x of
(αi, pi) ⇒
λi. (ctxt_of_pos_term pi
(to_pterm
(l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (var_rule αi))⟩)
rdp_A [0..<length rdp_A]) =
(As =
map2
(λx. case x of
(αi, pi) ⇒
λi. (ctxt_of_pos_term pi
(to_pterm
(l ⋅ τ)))⟨Prule αi
(map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A])"
(is "_ = ?Aseq")
apply (intro arg_cong[of _ _ "(=) _"])
apply (intro map_cong refl prod.case_cong)
subgoal for pair x y
apply (rule fun_cong[of _ _ y], intro prod.case_cong ext refl)
subgoal for α p
apply (subst R.vars_rule_vars_lhs)
subgoal using rdp_A A
by (meson in_set_zipE R.redex_pattern_rule_symbol)
subgoal by auto
done
done
done
show "(B =
(ctxt_of_pos_term q
(to_pterm (l ⋅ τ)))⟨Prule β (map (to_pterm ∘ τ ∘ rename_single ren) (var_rule β))⟩) =
(B =
(ctxt_of_pos_term q
(to_pterm (l ⋅ τ)))⟨Prule β (map (to_pterm ∘ τ ∘ rename_single ren) (vars_term_list (lhs β)))⟩)"
by (subst S.vars_rule_vars_lhs[OF β]) simp
from rdp_B B have q: "q ∈ poss (source B)"
using S.redex_patterns_label by fastforce
from R.redex_patterns_label[OF A]
have p: "(α,p) ∈ set (redex_patterns A) ⟹ p ∈ poss (source A)" for α p
by auto
assume ?Aseq
with Asne have rdp_ne: "rdp_A ≠ []" by auto
with rdp_A A have "¬ is_empty_step A"
by (metis redex_patterns_to_pterm source_empty_step)
from R.get_overlap_cond_alt[OF A this]
have "get_overlapping_part A B = Some A ⟷ (∀A'∈set (single_steps A). possL A' ∩ possL B ≠ {})" .
also have "… = (∀ (α,p) ∈ set rdp_A. (@) p ` fun_poss (lhs α) ∩ possL B ≠ {})"
using R.single_redex_possL[OF R.redex_pattern_rule_symbol[OF A] p]
unfolding rdp_A by fastforce
also have "possL B = possL (ll_single_redex (source B) q β)"
using B rdp_B S.single_steps_singleton by fastforce
also have "… = (@) q ` fun_poss (lhs β)"
by (subst S.single_redex_possL[OF β q], auto)
finally show "(get_overlapping_part A B = Some A) =
(∀ (α,p) ∈ set rdp_A. (@) p ` fun_poss (lhs α) ∩ (@) q ` fun_poss (lhs β) ≠ {})"
by auto
show "True = ((∀(α, p)∈set rdp_A. to_rule α ∈ R) ∧ to_rule β ∈ S ∧ rdp_A ≠ [])"
using β rdp_ne A rdp_A R.redex_pattern_rule_symbol[OF A] by auto
qed
finally show ?thesis .
qed
definition sim_cp_root where "sim_cp_root = { (A, B) | τ rdp_A l β A B As renamed_lhs_αs.
alt_cond τ rdp_A l β [] A B As renamed_lhs_αs}"
definition sim_cp_non_root where "sim_cp_non_root = { (A, B) | τ rdp_A l β q A B As renamed_lhs_αs.
alt_cond τ rdp_A l β q A B As renamed_lhs_αs ∧ q ≠ []}"
lemma sim_cp_split: "sim_cp = sim_cp_root ∪ sim_cp_non_root"
unfolding sim_cp_alt_def sim_cp_root_def sim_cp_non_root_def by blast
lemma sim_cp_root_many_conds: "sim_cp_root = { (A, B) | τ rdp_A l β A B As renamed_lhs_αs.
alt_cond τ rdp_A l β [] A B As renamed_lhs_αs ∧
(∀ (α,p) ∈ set rdp_A. to_rule α ∈ R ∧ p ∈ fun_poss (lhs β)
∧ mgu_vd_list ren [(lhs β|_p, lhs α)] ≠ None)}" (is "_ = ?Many")
proof
show "?Many ⊆ sim_cp_root" unfolding sim_cp_root_def by blast
show "sim_cp_root ⊆ ?Many" unfolding sim_cp_root_def
proof (intro Collect_mono ex_mono, intro impI, elim conjE, goal_cases)
case (1 pair τ rdp_A l β A B As renamed_lhs_αs)
from ‹alt_cond τ rdp_A l β [] A B As renamed_lhs_αs›[unfolded alt_cond_def]
have A: "A ∈ wf_pterm R" and B: "B ∈ wf_pterm S"
and rdp_A: "redex_patterns A = rdp_A"
and rdp_B: "redex_patterns B = [(β, [])]"
and l_def: "l = map_vars_term (rename_single ren) (lhs β)"
and unif: "mgu_list (map2 (λx y. (x, l |_ y)) (rename_list (map (λ(α, p). lhs α) rdp_A)) (map snd rdp_A)) = Some τ"
and rdp_cond: "(∀(α, p)∈set rdp_A. to_rule α ∈ R ∧ (@) p ` fun_poss (lhs α) ∩ fun_poss (lhs β) ≠ {})"
and β: "to_rule β ∈ S"
by auto
show ?case
proof (intro conjI; (fact)?)
{
fix α p
assume mem: "(α,p) ∈ set rdp_A"
with rdp_cond have rule: "to_rule α ∈ R" and p: "(@) p ` fun_poss (lhs α) ∩ fun_poss (lhs β) ≠ {}"
by auto
from p have p: "p ∈ fun_poss (lhs β)"
using fun_poss_append_poss' by fastforce
hence p': "p ∈ poss (lhs β)" using fun_poss_imp_poss by blast
from mem obtain i where i: "i < length rdp_A" and rdp_A: "rdp_A ! i = (α,p)" unfolding set_conv_nth by auto
define list where "list = map2 (λx y. (x, l |_ y)) (rename_list (map (λ(α, p). lhs α) rdp_A)) (map snd rdp_A)"
have len: "length list = length rdp_A" unfolding list_def by (auto simp: rename_list_def)
from mgu_list_Some[OF unif(1), folded list_def, unfolded is_imgu_def unifiers_def]
have unif: "⋀ pair. pair ∈ set list ⟹ fst pair ⋅ τ = snd pair ⋅ τ" by auto
have "(map_vars_term (rename_many' ren i) (lhs α), l |_ p) = list ! i"
unfolding list_def rename_list_def using i rdp_A by auto
also have "… ∈ set list" using i len by auto
finally have "map_vars_term (rename_many' ren i) (lhs α) ⋅ τ = l |_ p ⋅ τ"
using unif by auto
also have "l |_ p = map_vars_term (rename_single ren) (lhs β) |_ p"
unfolding l_def by simp
also have "… = map_vars_term (rename_single ren) (lhs β |_ p)" using p' by simp
finally obtain σ δ :: "('b,'a)subst" where "lhs β |_ p ⋅ δ = lhs α ⋅ σ"
unfolding map_vars_term_eq subst_subst by metis
hence mgu: "mgu_vd_list ren [(lhs β|_p, lhs α)] ≠ None"
using mgu_vd_list_complete[of "[(lhs β|_p, lhs α)]" "λ _. δ" σ ren] by auto
note p mgu rule
}
thus "∀(α, p)∈set rdp_A. to_rule α ∈ R ∧ p ∈ fun_poss (lhs β) ∧ mgu_vd_list ren [(lhs β |_ p, lhs α)] ≠ None"
by auto
qed
qed
qed
lemma sim_cp_non_root_many_conds: "sim_cp_non_root = { (A, B) | τ rdp_A l β q A B As renamed_lhs_αs.
alt_cond τ rdp_A l β q A B As renamed_lhs_αs ∧ q ≠ [] ∧
(∃ α rdpA Bs. A = Prule α Bs ∧ rdp_A = (α,[]) # rdpA ∧ to_rule α ∈ R ∧ q ∈ fun_poss (lhs α) ∧ mgu_vd_list ren [(lhs β, lhs α |_q)] ≠ None
∧ (∀ (α',p) ∈ set rdpA. to_rule α' ∈ R ∧ p ∈ (@) q ` fun_poss (lhs β) ∧ mgu_vd_list ren [(lhs β |_ (p -⇩p q), lhs α')] ≠ None))}" (is "_ = ?Many")
proof
show "?Many ⊆ sim_cp_non_root" unfolding sim_cp_non_root_def by blast
show "sim_cp_non_root ⊆ ?Many" unfolding sim_cp_non_root_def
proof (intro Collect_mono ex_mono, intro impI, elim conjE, goal_cases)
case (1 pair τ rdp_A l β q A B As renamed_lhs_αs)
from ‹alt_cond τ rdp_A l β q A B As renamed_lhs_αs›[unfolded alt_cond_def] ‹q ≠ []›
have A: "A ∈ wf_pterm R" and B: "B ∈ wf_pterm S"
and rdp_A: "redex_patterns A = rdp_A"
and rdp_B: "redex_patterns B = [(β, q)]"
and renl: "renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A)"
and l_def: "l = (ctxt_of_pos_term q (hd renamed_lhs_αs))⟨map_vars_term (rename_single ren) (lhs β)⟩"
and unif: "mgu_list (map2 (λx y. (x, l |_ y)) (rename_list (map (λ(α, p). lhs α) rdp_A)) (map snd rdp_A)) = Some τ"
and rdp_cond: "⋀ α p. (α, p)∈set rdp_A ⟹ to_rule α ∈ R ∧ (@) p ` fun_poss (lhs α) ∩ (@) q ` fun_poss (lhs β) ≠ {}"
and β: "to_rule β ∈ S"
and ne: "rdp_A ≠ []"
and root: "snd (hd rdp_A) = []"
by auto
from ne root obtain α rdpA where split: "rdp_A = (α,[]) # rdpA" by (cases rdp_A, auto)
from split have αmem: "(α,[]) ∈ set rdp_A" by auto
from rdp_cond[OF this]
have α: "to_rule α ∈ R" and q: "q ∈ fun_poss (lhs α)" by (auto simp: fun_poss_append_poss')
define list where "list = map2 (λx y. (x, l |_ y)) (rename_list (map (λ(α, p). lhs α) rdp_A)) (map snd rdp_A)"
have len: "length list = length rdp_A" unfolding list_def by (auto simp: rename_list_def)
obtain other where [simp]: "[0..<length rdpA] @ [length rdpA] = 0 # other"
by (metis gr0_conv_Suc less_eq_nat.simps(1) upt_Suc_append upt_conv_Cons)
note q' = fun_poss_imp_poss[OF q]
from mgu_list_Some[OF unif(1), folded list_def, unfolded is_imgu_def unifiers_def]
have unif: "⋀ pair. pair ∈ set list ⟹ fst pair ⋅ τ = snd pair ⋅ τ" by auto
define σ :: "('b,'a)subst" where "σ = Var o rename_many' ren 0"
define δ :: "('b,'a)subst" where "δ = Var o rename_single ren"
have "(lhs α ⋅ σ, l) ∈ set list"
unfolding list_def split by (simp add: rename_list_def map_vars_term_eq σ_def)
from unif[OF this]
have "lhs α ⋅ (σ ∘⇩s τ) |_q = (l ⋅ τ) |_q"
by simp
also have "l ⋅ τ = (ctxt_of_pos_term q (lhs α ⋅ σ))⟨lhs β ⋅ δ⟩ ⋅ τ"
unfolding l_def renl split rename_list_def σ_def map_vars_term_eq δ_def
by simp
also have "… |_q = lhs β ⋅ δ ⋅ τ"
using q' by (metis hole_pos_ctxt_of_pos_term hole_pos_poss poss_imp_subst_poss replace_at_subt_at subt_at_subst)
also have "… = lhs β ⋅ (δ ∘⇩s τ)" by simp
also have "lhs α ⋅ (σ ∘⇩s τ) |_q = lhs α |_q ⋅ (σ ∘⇩s τ)" using q' by simp
finally obtain σ δ :: "('b,'a)subst" where "lhs β ⋅ δ = lhs α |_q ⋅ σ" by metis
hence mgu_α: "mgu_vd_list ren [(lhs β, lhs α |_q)] ≠ None"
using mgu_vd_list_complete[of "[(lhs β, lhs α |_q)]" "λ _. δ" σ ren] by auto
from split[folded rdp_A] have redA_eq: "redex_patterns A = (α, []) # rdpA" by auto
have "∃ As. A = Prule α As"
proof (cases A)
case (Pfun f As)
with redA_eq have "(α,[]) ∈ set (concat (map2 (λi. map (λ(α, p). (α, i # p))) [0..<length As] (map redex_patterns As)))" by simp
hence False unfolding set_concat set_zip by force
thus ?thesis ..
qed (insert redA_eq, auto)
then obtain As where rule: "A = Prule α As" by auto
{
fix α' p
assume memA: "(α',p) ∈ set rdpA"
hence mem: "(α',p) ∈ set rdp_A" unfolding split by auto
from rdp_cond[OF this]
have α': "to_rule α' ∈ R" and over: "(@) p ` fun_poss (lhs α') ∩ (@) q ` fun_poss (lhs β) ≠ {}" by auto
then obtain p' q' where p': "p' ∈ fun_poss (lhs α')" and q'': "q' ∈ fun_poss (lhs β)" and eq: "p @ p' = q @ q'" by auto
from eq have disj: "p ≤⇩p q ∨ q ≤⇩p p"
by (metis prefix_append prefix_order.dual_order.eq_iff)
{
assume "p ≤⇩p q"
with q have p: "p ∈ fun_poss (lhs α)"
by (metis fun_poss_append_poss' prefix_def)
from A[unfolded rule]
have lenv: "length (var_poss_list (lhs α)) = length As"
by (metis Inl_inject term.simps(4) length_var_poss_list R.vars_rule_vars_lhs sum.simps(4) term.inject(2)
wf_pterm.cases)
from redA_eq[unfolded rule]
have eq': "rdpA = concat (map2 (λp1. map (λ(α, p2). (α, p1 @ p2))) (var_poss_list (lhs α)) (map redex_patterns As))" by auto
have "snd ` set rdpA ⊆ {(var_poss_list (lhs α) ! i) @ p2 |i p2. i < length As}"
unfolding eq' by (force simp: set_zip)
with memA obtain p2 i where i: "i < length As" and pp2: "p = var_poss_list (lhs α) ! i @ p2" by auto
let ?p1 = "var_poss_list (lhs α) ! i"
from i lenv have "?p1 ∈ var_poss (lhs α)"
by (metis nth_mem var_poss_list_sound)
hence "?p1 ∉ fun_poss (lhs α)"
by (metis DiffE poss_simps(3))
hence "?p1 @ p2 ∉ fun_poss (lhs α)"
using fun_poss_append_poss' by blast
from this[folded pp2] p have False ..
} note impossible = this
have pq: "p ∈ (@) q ` fun_poss (lhs β)"
by (smt (verit, best) eq fun_poss_append_poss' image_iff impossible pos_append_cases prefix_append prefix_order.order_refl q'')
then obtain p1 where "p1 ∈ fun_poss (lhs β)" and peq: "p = q @ p1" by auto
from this have p1: "p1 ∈ poss (lhs β)"
using fun_poss_imp_poss by blast
from mem obtain i where i: "i < length rdp_A" and rdpi: "rdp_A ! i = (α',p)" unfolding set_conv_nth by auto
define σ :: "('b,'a)subst" where "σ = Var o rename_many' ren i"
define δ :: "('b,'a)subst" where "δ = Var o rename_single ren"
from i len have "list ! i ∈ set list" by auto
also have "list ! i = (lhs α' ⋅ σ, l |_ p)" using i unfolding list_def rename_list_def
by (simp add: rdpi σ_def map_vars_term_as_subst o_def)
finally have "(lhs α' ⋅ σ, l |_ p) ∈ set list" by auto
from unif[OF this] have "lhs α' ⋅ σ ⋅ τ = l |_ p ⋅ τ" by auto
also have "l |_ p = lhs β ⋅ δ |_ p1" using q' unfolding l_def peq renl split rename_list_def δ_def o_def
by (simp add: map_vars_term_as_subst replace_at_below_poss replace_at_subt_at)
also have "… = lhs β |_ p1 ⋅ δ" using p1 by simp
finally have "lhs β |_ p1 ⋅ (δ ∘⇩s τ) = lhs α' ⋅ (σ ∘⇩s τ)"
by simp
then obtain σ δ :: "('b,'a)subst" where "lhs β |_ p1 ⋅ δ = lhs α' ⋅ σ" by metis
hence "mgu_vd_list ren [(lhs β |_ p1, lhs α')] ≠ None"
using mgu_vd_list_complete[of "[(lhs β |_ p1, lhs α')]" "λ _. δ" σ ren] by auto
also have "p1 = p -⇩p q" using peq
by (metis disj impossible prefix_pos_diff same_append_eq)
finally have mgu_α': "mgu_vd_list ren [(lhs β |_ (p -⇩p q), lhs α')] ≠ None" by auto
note α' pq mgu_α'
} note rdpA = this
show ?case
by (intro conjI exI; (fact)?) (insert rdpA, auto)
qed
qed
end
context
fixes ren :: "'v :: infinite renamingN"
and R :: "('f,'v)rules"
and S :: "('f,'v)rules"
begin
abbreviation unify_vd where "unify_vd pairs ≡ mgu_vd_list ren pairs ≠ None"
function compute_rp :: "('f,'v)term ⇒ (('f, 'v) prule × pos) list list" where
"compute_rp (Var x) = [[]]"
| "compute_rp (Fun f ts) =
(map concat o concat_lists) (map2 (λ i ti. map (map (map_prod id ((#) i))) (compute_rp ti)) [0..<length ts] ts)
@ List.maps (λ rule. let ps = filter ((≠) []) (var_poss_list (fst rule));
rec = map (λ p. if p ∈ fun_poss (Fun f ts) then map (map (map_prod id ((@) p))) (compute_rp (Fun f ts |_ p)) else [[]]) ps in
map ((#) (Rule (fst rule) (snd rule), [])) ((map concat o concat_lists) rec))
(filter (λ rule. unify_vd [ (Fun f ts, fst rule)]) R)"
by pat_completeness auto
termination
proof (standard, rule wf_measure[of size], goal_cases)
case (2 f ts rule filt p)
hence "p ≠ []" and "p ∈ poss (Fun f ts)" by (auto simp: fun_poss_imp_poss)
then show ?case
by simp (metis nth_mem size_simp1 size_simp5 subt_at.simps(1,2) subt_at_subterm supt_size)
qed (auto simp: termination_simp)
definition "rp_sub t p = (if p ∈ fun_poss t then map (map (map_prod id ((@) p))) (compute_rp (t |_ p)) else [[]])"
definition "rp_root t alpha l = (let
ps = filter ((≠) []) (var_poss_list l);
rec = map (λ p. rp_sub t p) ps
in map ((#) (alpha, [])) ((map concat o concat_lists) rec))"
lemma compute_rp_alt_def: "compute_rp (Fun f ts) =
(map concat o concat_lists) (map2 (λ i ti. map (map (map_prod id ((#) i))) (compute_rp ti)) [0..<length ts] ts)
@ List.maps (λ rule. let alpha = Rule (fst rule) (snd rule) in rp_root (Fun f ts) alpha (fst rule))
(filter (λ rule. unify_vd [ (Fun f ts, fst rule)]) R)"
unfolding compute_rp.simps(2) unfolding rp_root_def rp_sub_def Let_def by auto
lemma empty_compute_rp: "[] ∈ set (compute_rp t)"
proof (induct t rule: compute_rp.induct)
case (2 f ts)
define e :: "(('f, 'v) prule × nat list) list" where "e = []"
have IH: "i < length ts ⟹ e ∈ set (compute_rp (ts ! i))" for i
using 2(1)[of "(i, ts ! i)", OF _ refl] by (force simp: set_zip e_def)
let ?list = "map (λ i. map (map (map_prod id ((#) i))) (compute_rp (ts ! i))) [0..<length ts]"
have "concat (replicate (length ts) e) ∈ set (compute_rp (Fun f ts))"
unfolding compute_rp.simps set_append
apply (intro UnI1)
apply (unfold o_def)
apply simp
apply (intro imageI)
using IH by (auto simp: e_def)
also have "concat (replicate (length ts) e) = []" unfolding e_def by auto
finally show ?case .
qed auto
lemma positions_compute_rp: "snd ` (⋃ (set ` set (compute_rp t))) ⊆ poss t"
proof (induct t rule: compute_rp.induct)
case (2 f ts)
have len: "length [0..<length ts] = length ts" by simp
define S1 where "S1 = set (map concat
(concat_lists
(map (λi. map (map (map_prod id ((#) i))) (compute_rp (ts ! i)))
[0..<length ts])))"
define RR where "RR = (filter (λrule. unify_vd [(Fun f ts, fst rule)]) R)"
define ff where "ff = (λp. if p ∈ fun_poss (Fun f ts)
then map (map (map_prod id ((@) p)))
(compute_rp (Fun f ts |_ p))
else [[]])"
define gen where "gen = (λ rule. let ps = filter ((≠) []) (var_poss_list (fst rule));
rec = map ff ps
in map ((#) (fst rule → snd rule, [])) (map concat (concat_lists rec)))"
define S2 where "S2 = set (List.maps gen RR)"
show ?case unfolding compute_rp.simps o_def map2_to_map' len image_comp image_Union set_append
unfolding S1_def[symmetric] ff_def[symmetric] gen_def[symmetric] RR_def[symmetric] S2_def[symmetric]
proof (intro Union_least)
fix P
assume "P ∈ (λx. snd ` set x) ` (S1 ∪ S2)"
then obtain rdp where rdp: "rdp ∈ S1 ∪ S2" and P: "P = snd ` set rdp" by auto
show "P ⊆ poss (Fun f ts)"
proof
fix p
assume "p ∈ P"
with P rdp obtain rp where "rp ∈ S1 ∪ S2" and p: "p ∈ snd ` set rp" by auto
from this(1) show "p ∈ poss (Fun f ts)"
proof
assume "rp ∈ S1"
from this[unfolded S1_def, simplified]
obtain as where len: "length as = length ts"
and as: "⋀ i. i < length ts ⟹ as ! i ∈ map (map_prod id ((#) i)) ` set (compute_rp (ts ! i))"
and rp: "rp = concat as" by auto
from p[unfolded rp] obtain i where i: "i < length ts" and p: "p ∈ snd ` set (as ! i)"
using len set_conv_nth[of as] by auto
from as[OF i] obtain rpi where rpi: "rpi ∈ set (compute_rp (ts ! i))" and asi: "as ! i = map (map_prod id ((#) i)) rpi"
by auto
from i have "(i, ts ! i) ∈ set (zip [0..<length ts] ts)" unfolding set_conv_nth by force
from 2(1)[OF this refl] have IH: "snd ` ⋃ (set ` set (compute_rp (ts ! i))) ⊆ poss (ts ! i)" .
from p[unfolded asi] rpi obtain q where q: "q ∈ snd ` ⋃ (set ` set (compute_rp (ts ! i)))"
and p: "p = i # q" by force
from p q IH i show "p ∈ poss (Fun f ts)" by auto
next
assume "rp ∈ S2"
from this[unfolded S2_def List.maps_eq]
obtain rule where "rule ∈ set RR" and rp: "rp ∈ set (gen rule)" by auto
define ps where "ps = filter ((≠) []) (var_poss_list (fst rule))"
from rp[unfolded gen_def, folded ps_def, unfolded Let_def] p
have "p = [] ∨ (p ≠ [] ∧ (∃ rp. p ∈ snd ` set rp ∧ rp ∈ set (map concat (concat_lists (map ff ps)))))" (is "_ ∨ ?Ex")
by (smt (verit) imageE image_eqI in_set_idx length_map list.inject list.set_cases nth_map
nth_mem snd_conv)
thus "p ∈ poss (Fun f ts)"
proof
assume ?Ex
then obtain rp where p: "p ∈ snd ` set rp" and rp: "rp ∈ set (map concat (concat_lists (map ff ps)))"
and pne: "p ≠ []" by blast
note IH = 2(2)[OF ps_def]
from rp obtain as where rp: "rp = concat as"
and len: "length as = length ps"
and as: "⋀ i. i < length ps ⟹ as ! i ∈ set (ff (ps ! i))" by auto
from p[unfolded rp, simplified] obtain i where i: "i < length ps" and p: "p ∈ snd ` set (as ! i)"
using len set_conv_nth[of as] by auto
from i have pi: "ps ! i ∈ set ps" by auto
note IH = IH[OF this]
from as[OF i, unfolded ff_def] p pne
have mem: "ps ! i ∈ fun_poss (Fun f ts)"
and asi: "as ! i ∈ set (map (map (map_prod id ((@) (ps ! i)))) (compute_rp (Fun f ts |_ ps ! i)))"
by (auto split: if_splits)
from p asi[simplified] obtain q where q: "q ∈ snd ` ⋃ (set ` set (compute_rp (Fun f ts |_ ps ! i)))"
and p: "p = ps ! i @ q" by fastforce
from IH[OF mem] q have q: "q ∈ poss (Fun f ts |_ ps ! i)" by auto
show ?thesis using q pi unfolding p
using fun_poss_poss mem pos_append_poss by blast
qed auto
qed
qed
qed
qed auto
definition sim_cp_root_of where
"sim_cp_root_of rule rdp_A = (let l = map_vars_term (ren_l ren) (fst rule);
renamed_lhs_αs = ren.rename_list ren (map (λ(α, p). lhs α) rdp_A) in
case mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) of
None ⇒ []
| Some τ ⇒ (let As = map2 (λ prod i. case prod of (αi, pi) ⇒ (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]
in (case join_list As of None ⇒ []
| Some A ⇒ (let B = Prule (Rule (fst rule) (snd rule)) (map (to_pterm ∘ τ ∘ ren_l ren) (vars_term_list (fst rule)))
in [(A,B)]))))"
definition sim_cp_root_impl where "sim_cp_root_impl =
List.maps (λ rule. List.maps (λ rdp_A. sim_cp_root_of rule rdp_A) (filter ((≠) []) (compute_rp (fst rule)))) S"
definition non_root_rdps where "non_root_rdps α q ll =
(map concat (concat_lists (map (λ q⇩i. if q ≤⇩p q⇩i ∧ q⇩i -⇩p q ∈ fun_poss ll
then map (map (map_prod id ((@) q⇩i))) (compute_rp (ll |_ (q⇩i -⇩p q))) else [[]]) (var_poss_list (lhs α)))))"
definition sim_cp_non_root_of where
"sim_cp_non_root_of α q β rdpA = (let rdp_A = (α, []) # rdpA;
renamed_lhs_αs = ren.rename_list ren (map (λ(α, p). lhs α) rdp_A);
l = replace_at (hd renamed_lhs_αs) q (map_vars_term (ren_l ren) (lhs β))
in (case mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) of
None ⇒ []
| Some τ ⇒ (let As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]
in (case join_list As of None ⇒ []
| Some A ⇒ (let B = replace_at (to_pterm (l ⋅ τ)) q (Prule β (map (to_pterm ∘ τ ∘ ren_l ren) (vars_term_list (lhs β))))
in [(A,B)])))))"
definition non_root_sim_cps where "non_root_sim_cps α q β = (List.maps (sim_cp_non_root_of α q β)
(non_root_rdps α q (lhs β)))"
definition sim_cp_non_root_impl where "sim_cp_non_root_impl =
List.maps (λ (lf,rf). let α = Rule lf rf in List.maps (λ q. List.maps ( λ (ll,rr). non_root_sim_cps α q (Rule ll rr))
(filter (λ (ll,rr). unify_vd [(ll, lf |_q)]) S)) (filter ((≠) []) (fun_poss_list (lhs α)))) R"
definition sim_cp_impl where "sim_cp_impl = sim_cp_root_impl @ sim_cp_non_root_impl"
definition sim_cps_impl where "sim_cps_impl = map (map_prod target target) sim_cp_impl"
end
lemma no_pair_iff_empty[simp]: "(∀a b. (a, b) ∉ set xs) ⟷ xs = []"
by (metis in_set_simps(3) length_greater_0_conv nth_mem old.prod.exhaust)
lemma split_upt: "i < length xs ⟹ [0..< length xs] = [0..< i] @ i # [Suc i ..< length xs]"
by (metis le_Suc_ex less_Suc_eq_le less_imp_le_nat upt_add_eq_append upt_rec zero_less_Suc)
lemma list_app_eqI: "xs = [] ⟹ ys = us ⟹ zs = [] ⟹ xs @ ys @ zs = us" by auto
definition "below_var_poss p t = (∃ q ∈ var_poss t. q ≤⇩p p)"
lemma below_var_poss_simps[simp]: "below_var_poss p (Var x)"
"¬ below_var_poss [] (Fun f ts)"
"below_var_poss (i # p) (Fun f ts) = (i < length ts ∧ below_var_poss p (ts ! i))"
unfolding below_var_poss_def by force+
context ren_wf_trs
begin
context
fixes RR :: "('b,'a)rules"
and SS :: "('b,'a)rules"
assumes RR: "set RR = R" and SS: "set SS = S"
begin
lemma compute_rp: "set (compute_rp ren RR t) =
{ rp | rp A. A ∈ wf_pterm R ∧ rp = redex_patterns A ∧
(∀ (α,q) ∈ set rp. q ∈ fun_poss t ∧ unify_vd ren [(t|_q, lhs α)])}"
(is "?Left t = ?Right t")
proof -
have empty: "[] ∈ ?Right t" for t
by (auto intro!: exI[of _ "Var undefined"])
hence [simp]: "∃A. A ∈ wf_pterm R ∧ [] = redex_patterns A" by auto
show ?thesis
proof (induct t rule: compute_rp.induct)
case (2 f ts)
let ?t = "Fun f ts"
define addi :: "nat ⇒ (('b, 'a) prule × nat list) list ⇒ (('b, 'a) prule × nat list) list"
where "addi = (λ i. map (map_prod id ((#) i)))"
have addi: "addi i = map (λ(α, p). (α, i # p))" for i unfolding addi_def by (intro ext, force)
define addp :: "pos ⇒ (('b, 'a) prule × nat list) list ⇒ (('b, 'a) prule × nat list) list"
where "addp = (λ p. map (map_prod id ((@) p)))"
have addi: "addi i = map (λ(α, p). (α, i # p))" for i unfolding addi_def by (intro ext, force)
have addp: "addp p = map (λ(α, q). (α, p @ q))" for p unfolding addp_def by (intro ext, force)
define set1 where "set1 = concat ` set (concat_lists (map2 (λx y. map (addi x) (compute_rp ren RR y)) [0..<length ts] ts))"
let ?addp = "λ p. map (map (map_prod id ((@) p)))"
define set2 where "set2 = ⋃ (set `
(λ rule.
let ps = filter ((≠) []) (var_poss_list (fst rule));
rec = map (λp. if p ∈ fun_poss ?t then map (addp p) (compute_rp ren RR (?t |_ p)) else [[]]) ps
in map ((#) (fst rule → snd rule, [])) (map concat (concat_lists rec))) `
set (filter (λrule. unify_vd ren [(?t, fst rule)]) RR))"
have left: "?Left ?t = set1 ∪ set2"
unfolding compute_rp.simps set_append o_def set_map List.maps_eq set_concat addi_def addp_def set1_def set2_def by auto
show ?case unfolding left
proof
show "set1 ∪ set2 ⊆ ?Right ?t"
proof
fix rp
assume "rp ∈ set1 ∪ set2"
thus "rp ∈ ?Right ?t"
proof
assume "rp ∈ set1"
from this[unfolded set1_def, simplified]
obtain rps where len: "length rps = length ts" and rps: "⋀ i. i<length ts ⟹ rps ! i ∈ addi i ` ?Left (ts ! i)"
and rp: "rp = concat rps" by blast
let ?cond = "λ i rpi Ai. rps ! i = addi i rpi ∧ Ai ∈ wf_pterm R ∧
rpi = redex_patterns Ai ∧ (∀(α, q)∈set rpi. q ∈ fun_poss (ts ! i) ∧ unify_vd ren [(ts ! i |_ q, lhs α)])"
{
fix i
assume i: "i < length ts"
hence "(i, ts ! i) ∈ set (zip [0..<length ts] ts)" by (force simp: set_zip)
from 2(1)[OF this refl]
have "?Left (ts ! i) = ?Right (ts ! i)" .
from rps[OF i, unfolded this] have "∃ rpi Ai. ?cond i rpi Ai"
by auto
}
hence "∀ i. ∃ rpi Ai. i < length ts ⟶ ?cond i rpi Ai" by blast
from choice[OF this] obtain rpi where "∀ i. ∃ Ai. i < length ts ⟶ ?cond i (rpi i) Ai" by blast
from choice[OF this] obtain Ai where cond: "⋀ i. i < length ts ⟹ ?cond i (rpi i) (Ai i)" by blast
let ?A = "Pfun f (map Ai [0..<length ts])"
have A: "?A ∈ wf_pterm R" using cond by (auto intro!: wf_pterm.intros)
have rpA: "redex_patterns ?A = rp" unfolding rp redex_patterns.simps length_map length_upt
apply (intro arg_cong[of _ _ concat], rule sym, rule nth_equalityI; unfold len)
apply force
subgoal for i using cond[of i] by (auto simp: addi)
done
{
fix α q
assume "(α,q) ∈ set rp"
from this[unfolded rp] obtain i where i: "i < length ts" and mem: "(α,q) ∈ set (rps ! i)"
by (metis in_set_conv_nth nth_concat_split len)
note mem
also have "rps ! i = addi i (rpi i)" using cond[OF i] by auto
finally obtain r where mem: "(α,r) ∈ set (rpi i)" and q: "q = i # r"
unfolding addi_def by auto
from cond[OF i] mem have "r ∈ fun_poss (ts ! i) ∧ unify_vd ren [(ts ! i |_ r, lhs α)]" by auto
hence "q ∈ fun_poss (Fun f ts) ∧ unify_vd ren [(Fun f ts |_ q, lhs α)]" unfolding q using i by auto
}
thus ?thesis
by (intro CollectI exI[of _ rp] exI[of _ ?A] conjI A refl rpA[symmetric], auto)
next
assume "rp ∈ set2"
from this[unfolded set2_def set_filter RR] obtain l r ps rec where
lr: "(l,r) ∈ R"
and mgu: "unify_vd ren [(?t, l)]"
and ps: "ps = filter ((≠) []) (var_poss_list (fst (l,r)))"
and rec: "rec = map (λp. if p ∈ fun_poss ?t then map (addp p) (compute_rp ren RR (?t |_ p)) else [[]]) ps"
and rp: "rp ∈ set (map ((#) (l → r, [])) (map concat (concat_lists rec)))"
by force
from rec have len_rec: "length rec = length ps" by auto
note IH = 2(2)[OF ps]
from lr have "is_Fun l" using R.no_var_lhs by fastforce
hence "[] ∉ set (var_poss_list l)" by (cases l, auto)
hence ps: "ps = var_poss_list l" unfolding ps fst_conv
using filter_id_conv by blast
from rp len_rec obtain rps where
rp: "rp = (l → r, []) # concat rps"
and len_rps: "length rps = length ps"
and as_mem: "⋀ i. i < length ps ⟹ rps ! i ∈ set (rec ! i)"
by auto
let ?cond = "λ i rpi A. (A ∈ wf_pterm R ∧ rps ! i = addp (ps ! i) rpi ∧ rpi = redex_patterns A ∧
(∀ α q. (α,q) ∈set rpi ⟶
q ∈ fun_poss (?t |_ ps ! i) ∧
unify_vd ren [(?t |_ ps ! i |_ q, lhs α)]))"
{
fix i
assume i: "i < length ps"
hence mem: "ps ! i ∈ set ps" by auto
{
assume fp: "ps ! i ∈ fun_poss ?t"
have "set (rec ! i) = addp (ps ! i) ` ?Left (?t |_ ps ! i)" unfolding rec
using i fp by auto
also have "… = addp (ps ! i) ` ?Right (?t |_ ps ! i)" unfolding IH[OF mem fp] ..
finally have "set (rec ! i) = addp (ps ! i) ` ?Right (?t |_ ps ! i)" .
from as_mem[OF i, unfolded this]
have "∃A rpi. ?cond i rpi A" by fast
}
moreover
{
assume "ps ! i ∉ fun_poss ?t"
hence "rec ! i = [[]]" unfolding rec using i by auto
from as_mem[OF i, unfolded this] have "rps ! i = []" by auto
hence "∃ A rpi. ?cond i rpi A"
by (intro exI[of _ "Var undefined"], auto simp: addp)
}
ultimately have "∃ A rpi. ?cond i rpi A" by blast
}
hence "∀ i. ∃ A rpi. i < length ps ⟶ ?cond i rpi A" by blast
from choice[OF this] obtain As where "∀ i. ∃ rpi. i < length ps ⟶ ?cond i rpi (As i)" by blast
from choice[OF this] obtain rpi where cond: "⋀ i. i < length ps ⟹ ?cond i (rpi i) (As i)" by blast
let ?A = "Prule (Rule l r) (map As [0..<length ps])"
let ?addi = "λ i. map (λ(α, p2). (α, ps ! i @ p2))"
from lr have len_ps: "length ps = length (var_rule (l → r))"
unfolding ps by (metis length_var_poss_list R.length_var_rule prule.sel(1,2))
have vpl: "var_poss_list (lhs (l → r)) = ps" unfolding ps by simp
let ?rp = "(l → r, []) # concat (map (λ i. rps ! i) [0..<length ps])"
have rpA: "redex_patterns ?A = ?rp"
unfolding rp redex_patterns.simps vpl
by (intro arg_cong[of _ _ "λ x. _ # concat x"], rule nth_equalityI; insert cond, auto simp: addp)
have A: "?A ∈ wf_pterm R" using lr len_ps cond by (intro wf_pterm.intros, auto)
have rp_id: "rp = ?rp" unfolding rp
by (intro arg_cong[of _ _ "λ x. _ # concat x"], rule nth_equalityI; insert len_rps cond, auto)
{
fix α q
assume mem: "(α,q) ∈ set ((l → r, []) # concat (map ((!) rps) [0..<length ps]))"
have "q ∈ fun_poss (Fun f ts) ∧ unify_vd ren [(Fun f ts |_ q, lhs α)]"
proof (cases "(α,q) = (l → r, [])")
case True
with mgu show ?thesis by auto
next
case False
with mem obtain i where i: "i < length ps" and aq: "(α,q) ∈ set (rps ! i)" by auto
with cond[OF i] have "(α,q) ∈ set (addp (ps ! i) (rpi i))" by auto
then obtain p where mem: "(α,p) ∈ set (rpi i)" and q: "q = ps ! i @ p"
by (force simp: addp)
from cond[OF i] mem
have cond: "p ∈ fun_poss (?t |_ ps ! i)" "unify_vd ren [(?t |_ ps ! i |_ p, lhs α)]"
by auto
show ?thesis
proof (cases "ps ! i ∈ fun_poss ?t")
case True
hence "ps ! i ∈ poss ?t" by (rule fun_poss_imp_poss)
hence id: "?t |_ ps ! i |_ p = ?t |_ q" unfolding q by auto
with cond have mgu: "unify_vd ren [(?t |_ q, lhs α)]" by auto
from cond(1-2) True have "q ∈ fun_poss ?t" unfolding q
by (metis Term.term.simps(4) fun_poss_fun_conv fun_poss_imp_poss id is_VarE poss_append_poss
poss_is_Fun_fun_poss q)
thus ?thesis
by (intro conjI mgu)
next
case False
from False i have "set (rec ! i) = {[]}" unfolding rec by (force simp: addp_def)
with as_mem[OF i] have "rps ! i = []" by auto
with aq show ?thesis by auto
qed
qed
}
thus ?thesis
by (intro CollectI exI[of _ ?A] exI[of _ ?rp] conjI refl rpA[symmetric] A rp_id, blast)
qed
qed
show "?Right ?t ⊆ set1 ∪ set2"
proof
fix rp
assume "rp ∈ ?Right ?t"
then obtain A where A: "A ∈ wf_pterm R"
and rp: "rp = redex_patterns A"
and cond: "⋀ α q. (α,q) ∈ set rp ⟹ q ∈ fun_poss ?t ∧ unify_vd ren [(?t |_ q, lhs α)]" by blast
from A show "rp ∈ set1 ∪ set2"
proof cases
case Var: (1 x)
with rp have "rp = []" by simp
thus ?thesis unfolding left[symmetric] by (metis empty_compute_rp)
next
case Pfun: (2 As f)
hence Asi: "⋀ i. i < length As ⟹ As ! i ∈ wf_pterm R" by auto
define m where "m = min (length As) (length ts)"
define Bs where "Bs i = (if i < m then As ! i else Var undefined)" for i
have Bsi: "⋀ i. Bs i ∈ wf_pterm R" unfolding Bs_def m_def using Asi by auto
have "rp = concat (map2 addi [0..<length As] (map redex_patterns As))"
using rp Pfun by (simp add: addi)
also have "map2 addi [0..<length As] (map redex_patterns As) = map (λ i. addi i (redex_patterns (As ! i))) [0..<length As]"
by (intro nth_equalityI, auto)
finally have rp: "rp = concat (map (λ i. addi i (redex_patterns (As ! i))) [0..<length As])" .
{
fix i
assume i: "i < length As" "¬ i < length ts"
have "redex_patterns (As ! i) = []"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain p α Bs where "redex_patterns (As ! i) = (α,p) # Bs" (is "?e = _") by (cases ?e, auto)
with i have "(α,i # p) ∈ set rp" unfolding rp addi by force
from cond[OF this] i show False by auto
qed
} note large_i = this
note rp
also have "[0..<length As] = [0..<m] @ [m ..< length As]" unfolding m_def
by (metis (no_types, lifting) append_Nil2 min.absorb1 min.absorb3 min.left_idem split_upt upt_eq_Nil_conv upt_rec)
also have "map (λ i. addi i (redex_patterns (As ! i))) … =
map (λ i. addi i (redex_patterns (As ! i))) [0..<m] @
map (λ i. addi i (redex_patterns (As ! i))) [m ..< length As]"
by simp
also have "map (λ i. addi i (redex_patterns (As ! i))) [m ..< length As] = map (λ _. []) [m ..< length As]"
proof (intro map_cong[OF refl])
fix i
assume "i ∈ set [m ..< length As]"
hence "i < length As" "¬ i < length ts" unfolding m_def by force+
from large_i[OF this]
show "addi i (redex_patterns (As ! i)) = []" unfolding addi by simp
qed
also have "map (λ i. addi i (redex_patterns (As ! i))) [0..<m] = map (λ i. addi i (redex_patterns (Bs i))) [0..<m]"
unfolding Bs_def by auto
finally have "rp = concat (map (λi. addi i (redex_patterns (Bs i))) [0..<m])" by simp
also have "… = … @ concat (map (λi. addi i (redex_patterns (Bs i))) [m..<length ts])"
unfolding Bs_def by (auto simp: addi)
also have "… = concat (map (λi. addi i (redex_patterns (Bs i))) ([0..<m] @ [m ..<length ts]))" by simp
also have "[0..<m] @ [m ..<length ts] = [0..<length ts]" unfolding m_def
by (metis append_Nil2 le_neq_implies_less min.cobounded2 split_upt upt_rec)
finally have rp_ts: "rp = concat (map (λi. addi i (redex_patterns (Bs i))) [0..<length ts])" by auto
have len_id: "length (zip [0..<length ts] ts) = length ts" by auto
{
fix i
assume i: "i < length ts"
have "addi i (redex_patterns (Bs i)) ∈ addi i ` set (compute_rp ren RR (ts ! i))"
proof (intro imageI, cases "i < length As")
case False
hence id: "redex_patterns (Bs i) = []" unfolding Bs_def m_def by auto
show "redex_patterns (Bs i) ∈ set (compute_rp ren RR (ts ! i))"
unfolding id by (rule empty_compute_rp)
next
case True
from i have "(i, ts ! i) ∈ set (zip [0..<length ts] ts)" by (force simp: set_zip)
note IH = 2(1)[OF this refl]
{
fix α q
assume "(α, q)∈set (redex_patterns (As ! i))"
hence "(α, i # q) ∈ set rp" using True unfolding rp by (auto simp: addi)
from cond[OF this]
have "q ∈ fun_poss (ts ! i) ∧ unify_vd ren [(ts ! i |_ q, lhs α)]"
by auto
} note cond = this
have "redex_patterns (Bs i) = redex_patterns (As ! i)" unfolding Bs_def using True i m_def by auto
also have "… ∈ set (compute_rp ren RR (ts ! i))" unfolding IH
by (intro CollectI exI[of _ "redex_patterns (As ! i)"] exI[of _ "As ! i"] conjI refl Asi[OF True])
(insert cond, auto)
finally show "redex_patterns (Bs i) ∈ set (compute_rp ren RR (ts ! i))" .
qed
} note IH = this
have "rp ∈ set1" unfolding set1_def rp_ts set_concat_lists length_map len_id
by (intro imageI CollectI conjI, insert IH, auto)
thus ?thesis ..
next
case Prule: (3 α As)
then obtain l r where α: "α = Rule l r" by (cases α, auto)
with Prule have lr: "(l,r) ∈ R" and lhs[simp]: "lhs α = l" by auto
define fR where "fR = set (filter (λrule. unify_vd ren [(Fun f ts, fst rule)]) RR)"
note rp_id = rp[unfolded Prule]
hence rp: "rp = (α, []) # concat (map2 addp (var_poss_list l) (map redex_patterns As))"
by (auto simp: addp)
hence "(α, []) ∈ set rp" by auto
from cond[OF this] have "unify_vd ren [(Fun f ts |_ [], l)]" by auto
hence lr_fR: "(l,r) ∈ fR" unfolding fR_def using lr RR by auto
define ps where "ps = filter ((≠) []) (var_poss_list (fst (l,r)))"
from lr have "is_Fun l"
using A Prule(1) lhs R.lhs_is_Fun by blast
hence "[] ∉ set (var_poss_list l)" by (cases l, auto)
hence ps: "ps = var_poss_list l" unfolding ps_def fst_conv
using filter_id_conv by blast
from Prule(3) have len: "length As = length ps" unfolding ps using lr
by (metis α left_lin.length_var_rule R.left_lin_axioms length_var_poss_list lhs prule.sel(2))
let ?f = "(λp. if p ∈ fun_poss ?t
then map (addp p) (compute_rp ren RR (?t |_ p)) else [[]])"
define rec where "rec = map ?f ps"
have "concat (map2 addp ps (map redex_patterns As)) ∈ concat ` set (concat_lists rec)"
proof (intro imageI, unfold set_concat_lists, intro CollectI conjI allI impI, force simp: len rec_def)
fix i
assume "i < length rec"
hence i: "i < length ps" "i < length As"
unfolding rec_def using len by auto
have id1: "map2 addp ps (map redex_patterns As) ! i = addp (ps ! i) (redex_patterns (As ! i))"
using i by auto
have id2: "set (rec ! i) = set (?f (ps ! i))" unfolding rec_def using i by auto
from i have psi: "ps ! i ∈ set ps" by auto
from Prule i have Asi: "As ! i ∈ wf_pterm R" by auto
have "addp (ps ! i) (redex_patterns (As ! i)) ∈ set (?f (ps ! i))"
proof (cases "ps ! i ∈ fun_poss ?t")
case False
hence "redex_patterns (As ! i) = []"
by (metis
‹⋀thesis. (⋀A. A ∈ wf_pterm R ⟹ rp = redex_patterns A ⟹
(⋀α q. (α, q) ∈ set rp ⟹ q ∈ fun_poss ?t ∧ unify_vd ren [(?t |_ q, lhs α)]) ⟹ thesis) ⟹ thesis›
rp_id fun_poss_append_poss' i(2) len lhs no_pair_iff_empty ps
redex_patterns_elem_rule')
with False show ?thesis by (auto simp: addp)
next
case True
hence id: "(ps ! i ∈ fun_poss (Fun f ts)) = True" by auto
show ?thesis unfolding id if_True set_map
proof (intro imageI)
note IH = 2(2)[OF ps_def psi True]
{
fix α q
assume "(α, q) ∈ set (redex_patterns (As ! i))"
hence "(α, ps ! i @ q) ∈ set rp" unfolding rp[folded ps] addp using i
by (metis lhs ps redex_patterns.simps(3) redex_patterns_elem_rule')
note cond = cond[OF this]
from True have psi': "ps ! i ∈ poss ?t" by (rule fun_poss_imp_poss)
from psi' have "?t |_ ps ! i |_ q = ?t |_ (ps ! i @ q)" by simp
with cond have unif: "unify_vd ren [(?t |_ ps ! i |_ q, lhs α)]" by auto
from cond have "ps ! i @ q ∈ fun_poss ?t" by auto
hence q_fp: "q ∈ fun_poss (?t |_ ps ! i)"
by (metis fun_poss_poss subterm_poss_conv)
note q_fp unif
}
thus "redex_patterns (As ! i) ∈ ?Left (Fun f ts |_ ps ! i)"
unfolding IH
by (intro CollectI exI[of _ "redex_patterns (As ! i)"] exI[of _ "As ! i"] conjI refl Asi, auto)
qed
qed
thus "map2 addp ps (map redex_patterns As) ! i ∈ set (rec ! i) " unfolding id1 id2 .
qed
hence rp: "rp ∈ set (map ((#) (α, [])) (map concat (concat_lists rec)))"
unfolding rp ps by auto
have "rp ∈ set2" unfolding set2_def fR_def[symmetric]
apply (intro UnionI)
apply (rule imageI, rule imageI)
apply (rule lr_fR)
using rp by (auto simp: rec_def ps_def Let_def α)
thus ?thesis ..
qed
qed
qed
qed auto
qed
lemma sim_cp_root_impl_complete: "sim_cp_root ⊆ set (sim_cp_root_impl ren RR SS)"
proof
fix A B
assume "(A,B) ∈ sim_cp_root"
from this[unfolded sim_cp_root_many_conds]
obtain τ rdp_A l β As renamed_lhs_αs where
alt: "alt_cond τ rdp_A l β [] A B As renamed_lhs_αs"
and cond: "∀(α, p)∈set rdp_A. p ∈ fun_poss (lhs β) ∧ unify_vd ren [(lhs β |_ p, lhs α)]"
by blast
obtain ll rr where β: "β = Rule ll rr" by (cases β, auto)
note alt = alt[unfolded alt_cond_def β]
from alt have l: "l = map_vars_term (rename_single ren) ll" by (simp add: β)
from alt have ren_as: "renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A)" by (simp add: β)
from alt SS have llrr: "(ll,rr) ∈ set SS" by auto
from alt have mgu: "mgu_list (map2 (λx y. (x, l |_ y)) renamed_lhs_αs (map snd rdp_A)) = Some τ" by auto
from alt have As: "As = map2
(λ prod i. case prod of (αi, pi) ⇒
(ctxt_of_pos_term pi
(to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]" by auto
from alt have join: "⨆ As = Some A" by auto
have rdp_A: "rdp_A ∈ set (filter ((≠) []) (compute_rp ren RR ll))"
unfolding set_filter
apply (intro CollectI conjI)
apply (unfold compute_rp, intro CollectI exI[of _ A] exI[of _ rdp_A])
using alt cond by (auto simp add: β)
have AB: "(A, B) ∈ set (sim_cp_root_of ren (ll,rr) rdp_A)"
unfolding sim_cp_root_of_def fst_conv snd_conv
apply (unfold l[symmetric])
apply (unfold ren_as[symmetric])
apply (unfold Let_def[of l])
apply (unfold Let_def[of renamed_lhs_αs])
apply (unfold mgu option.simps)
apply (unfold As[symmetric] Let_def)
apply (unfold join option.simps)
using alt cond by auto
show "(A,B) ∈ set (sim_cp_root_impl ren RR SS)" unfolding sim_cp_root_impl_def List.maps_eq set_concat set_map image_cong
apply (intro UnionI, rule imageI, rule imageI[OF llrr])
apply (unfold set_concat, intro UnionI, rule imageI)
apply (unfold set_map fst_conv, rule imageI[OF rdp_A])
by (rule AB)
qed
lemma sim_cp_non_root_impl_complete: "sim_cp_non_root ⊆ set (sim_cp_non_root_impl ren RR SS)"
proof
fix A B
assume "(A,B) ∈ sim_cp_non_root"
from this[unfolded sim_cp_non_root_many_conds]
obtain τ rdp_A l β q As renamed_lhs_αs α rdpA Bs where
alt: "alt_cond τ rdp_A l β q A B As renamed_lhs_αs"
and q_ne: "q ≠ []"
and rdpA: "rdp_A = (α, []) # rdpA"
and ruleA: "to_rule α ∈ R"
and q: "q ∈ fun_poss (lhs α)"
and mgu_root: "unify_vd ren [(lhs β, lhs α |_ q)]"
and cond: "∀(α', p)∈set rdpA. to_rule α' ∈ R ∧ p ∈ (@) q ` fun_poss (lhs β) ∧ unify_vd ren [(lhs β |_ (p -⇩p q), lhs α')]"
and ABs: "A = Prule α Bs"
by blast
define addp :: "pos ⇒ (('b, 'a) prule × nat list) ⇒ (('b, 'a) prule × nat list)"
where "addp p = (map_prod id ((@) p))" for p
have addp: "addp p = (λ(α, q). (α, p @ q))" for p unfolding addp_def by (intro ext, force)
let ?addp = "λ p. map (addp p)"
obtain ll rr where β: "β = Rule ll rr" by (cases β, auto)
hence lhsb: "lhs β = ll" by simp
note cond = cond[unfolded this]
obtain lf rf where α: "α = Rule lf rf" by (cases α, auto)
hence lhsa: "lhs α = lf" by simp
from q_ne q have qmem: "q ∈ set (filter ((≠) []) (fun_poss_list (lhs (Rule lf rf))))" by (auto simp: α)
note alt = alt[unfolded alt_cond_def β α]
from alt have l: "l = (ctxt_of_pos_term q (hd renamed_lhs_αs))⟨map_vars_term (rename_single ren) ll⟩" by (simp add: β)
from alt have ren_as: "renamed_lhs_αs = rename_list (map (λ(α, p). lhs α) rdp_A)" by (simp add: β)
from alt SS have llrr: "(ll,rr) ∈ set SS" by auto
from alt have mgu: "mgu_list (map2 (λx y. (x, l |_ y)) renamed_lhs_αs (map snd rdp_A)) = Some τ" by auto
from alt have As: "As = map2
(λ(αi, pi) i.
(ctxt_of_pos_term pi
(to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]" by auto
from alt have join: "⨆ As = Some A" by auto
from alt have A: "A ∈ wf_pterm R" by auto
from ruleA have lfrf: "(lf,rf) ∈ R" unfolding α by auto
define ps where "ps = var_poss_list (lhs α)"
from A[unfolded ABs] have "length Bs = length (var_rule α)" using wf_pterm.cases by force
also have "… = length (var_poss_list (lhs α))" using ruleA
by (metis length_var_poss_list R.vars_rule_vars_lhs)
finally have len_ps: "length ps = length Bs" by (simp add: ps_def)
from alt rdpA have "(α, []) # rdpA = redex_patterns A" by simp
also have "… = (α, []) # concat (map2 ?addp ps (map redex_patterns Bs))"
unfolding ABs redex_patterns.simps addp ps_def by simp
also have "map2 ?addp ps (map redex_patterns Bs) = map (λ i. ?addp (ps ! i) (redex_patterns (Bs ! i))) [0..<length Bs]"
using len_ps by (intro nth_equalityI, auto)
finally have rdpABs: "rdpA = concat (map (λi. ?addp (ps ! i) (redex_patterns (Bs ! i))) [0..<length Bs])" by auto
from llrr have mgu_mem: "(ll,rr) ∈ set (filter (λ(ll, rr). unify_vd ren [(ll, lf |_ q)]) SS)"
using mgu_root unfolding α β by auto
have vp_lf: "var_poss_list lf = ps" unfolding ps_def α by simp
{
fix i
assume i: "i < length ps"
let ?p = "ps ! i"
have "?addp ?p (redex_patterns (Bs ! i))
∈ set (if q ≤⇩p ?p ∧ ?p -⇩p q ∈ fun_poss ll then map (?addp ?p) (compute_rp ren RR (ll |_ (?p -⇩p q))) else [[]])" (is "?prp ∈ ?Set")
proof (cases "q ≤⇩p ?p ∧ ?p -⇩p q ∈ fun_poss ll")
case False
have "redex_patterns (Bs ! i) = []"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain γ r where mem: "(γ,r) ∈ set (redex_patterns (Bs ! i))" (is "_ ∈ set ?e") by (cases ?e, auto)
with i len_ps have "addp ?p (γ,r) ∈ set rdpA" unfolding rdpABs by auto
from cond[rule_format, OF this]
have "?p @ r ∈ (@) q ` fun_poss ll" by (auto simp: addp)
then obtain u where u: "u ∈ fun_poss ll" and id: "?p @ r = q @ u" by auto
from q have q: "q ∈ fun_poss lf" unfolding lhsa .
from i have "?p ∈ set ps" by auto
also have "set ps = var_poss lf" unfolding vp_lf[symmetric] by simp
finally have "?p ∈ var_poss lf" by auto
with q have not: "¬ ?p ≤⇩p q"
by (metis Term.term.simps(4) fun_poss_append_poss' fun_poss_fun_conv prefix_def var_poss_iff)
with id have qp: "q ≤⇩p ?p"
by (metis prefixI prefix_append)
with False have "¬ ?p -⇩p q ∈ fun_poss ll" by auto
with id u qp show False
by (metis fun_poss_append_poss' less_eq_pos_simps(2) prefixI prefix_pos_diff)
qed
with False show ?thesis by auto
next
case True
hence qp: "q ≤⇩p ?p" and pq: "?p -⇩p q ∈ fun_poss ll" by auto
hence id: "?Set = ?addp ?p ` set (compute_rp ren RR (ll |_ (?p -⇩p q)))" by auto
from A ABs i len_ps have Bsi: "Bs ! i ∈ wf_pterm R" by auto
{
fix γ r
assume "(γ, r)∈set (redex_patterns (Bs ! i))"
hence "addp ?p (γ, r) ∈ set rdpA" unfolding rdpABs using i len_ps by auto
from cond[rule_format, OF this, unfolded split addp]
have cond: "?p @ r ∈ (@) q ` fun_poss ll" "unify_vd ren [(ll |_ ((?p @ r) -⇩p q), lhs γ)]"
by auto
from qp fun_poss_imp_poss[OF pq] have "ll |_ ((?p @ r) -⇩p q) = ll |_ (?p -⇩p q) |_ r"
by (metis append.assoc less_eq_pos_simps(1) prefix_pos_diff same_append_eq subt_at_append)
moreover from cond qp pq have "r ∈ fun_poss (ll |_ (?p -⇩p q))"
by (smt (verit, ccfv_threshold) append.assoc fun_poss_poss imageE prefix_pos_diff same_append_eq subterm_poss_conv)
ultimately have "r ∈ fun_poss (ll |_ (?p -⇩p q)) ∧ unify_vd ren [(ll |_ (?p -⇩p q) |_ r, lhs γ)]"
using cond by auto
} note mgu = this
show ?thesis unfolding id
proof (rule imageI)
show "redex_patterns (Bs ! i) ∈ set (compute_rp ren RR (ll |_ (?p -⇩p q)))"
unfolding compute_rp
apply (intro CollectI exI conjI)
apply (rule refl)
apply (rule Bsi)
using mgu by auto
qed
qed
} note member = this
have rdpA': "(lf → rf, []) # rdpA = rdp_A" unfolding rdpA α by simp
show "(A,B) ∈ set (sim_cp_non_root_impl ren RR SS)" unfolding sim_cp_non_root_impl_def List.maps_eq set_concat set_map image_cong RR
apply (intro UnionI, rule imageI, rule imageI[OF lfrf])
apply (unfold split Let_def)
apply (unfold set_concat, intro UnionI, rule imageI)
apply (unfold set_map, rule imageI[OF qmem])
apply (unfold set_concat, intro UnionI, rule imageI)
apply (unfold set_map, rule imageI, rule mgu_mem)
apply (unfold non_root_sim_cps_def List.maps_eq)
apply (unfold split set_concat, intro UnionI, rule imageI)
apply (unfold set_map, rule imageI)
apply (rule eq_mem_trans[OF rdpABs])
apply (unfold non_root_rdps_def set_concat set_map prule.sel)
apply (rule imageI)
apply (unfold vp_lf addp_def[symmetric])
apply (unfold set_concat_lists length_map)
apply (rule CollectI, rule conjI, force simp: len_ps)
apply (intro allI impI)
subgoal for i using member[of i] by (simp add: len_ps)
apply (unfold sim_cp_non_root_of_def)
apply (unfold rdpA' Let_def[of rdp_A])
apply (unfold ren_as[symmetric] Let_def[of renamed_lhs_αs] prule.sel)
apply (unfold l[symmetric] Let_def[of l])
apply (unfold mgu option.simps)
apply (unfold As[symmetric] Let_def)
apply (unfold join option.simps)
using alt cond by auto
qed
lemma sim_cp_root_of_alt_cond: assumes AB: "(A,B) ∈ set (sim_cp_root_of ren (ll,rr) rdp_A)"
and llrr: "(ll,rr) ∈ S"
and ne: "rdp_A ≠ []"
and rdpA: "rdp_A ∈ set (compute_rp ren RR ll)"
shows "∃ τ l As ren_as. alt_cond τ rdp_A l (Rule ll rr) [] A B As ren_as"
proof -
from AB obtain l ren_as τ As where
l: "l = map_vars_term (rename_single ren) ll"
and ren_as: "ren_as = rename_list (map (λ(α, p). lhs α) rdp_A)"
and mgu: "mgu_list (map2 (λx y. (x, l |_ y)) ren_as (map snd rdp_A)) = Some τ"
and As: "As = map2 (λ prod i. case prod of (αi, pi) ⇒ (ctxt_of_pos_term pi
(to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]"
and join: "⨆ As = Some A"
and B: "B = Prule (ll → rr) (map (to_pterm ∘ τ ∘ rename_single ren) (vars_term_list ll))"
unfolding sim_cp_root_of_def
by (force simp: Let_def o_def)
have As': "As = map2 (λ (αi, pi) i. (ctxt_of_pos_term pi
(to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]" unfolding As by auto
from rdpA[unfolded compute_rp]
obtain A' where A': "A' ∈ wf_pterm R" "rdp_A = redex_patterns A'"
and rdp_cond: "⋀ α q. (α,q) ∈ set rdp_A ⟹ q ∈ fun_poss ll ∧ unify_vd ren [(ll |_ q, lhs α)]"
by force
show ?thesis
proof (intro exI conjI)
show "alt_cond τ rdp_A l (Rule ll rr) [] A B As ren_as" unfolding alt_cond_def prule.sel ctxt_of_pos_term.simps intp_actxt.simps
proof (intro conjI; (fact)?)
{
fix α p
assume mem: "(α,p) ∈ set rdp_A"
with A' have rule: "to_rule α ∈ R"
using R.redex_pattern_rule_symbol by blast
from rule have len: "length (vars_term_list (lhs α)) = length (var_rule α)"
by (metis R.length_var_rule)
from rule have fn: "is_Fun (lhs α)"
using R.no_var_lhs by fastforce
from rdp_cond[OF mem]
have p: "p ∈ fun_poss ll" by auto
hence inter: "p ∈ (@) p ` fun_poss (lhs α) ∩ (@) [] ` fun_poss ll" using fn by (cases "lhs α", auto)
from fun_poss_imp_poss[OF p] have "p ∈ poss (l ⋅ τ)" unfolding l by auto
note rule len inter this
} note rdp_A_conds = this
thus "∀(α, p)∈set rdp_A. (@) p ` fun_poss (lhs α) ∩ (@) [] ` fun_poss ll ≠ {}" "∀(α, p)∈set rdp_A. to_rule α ∈ R" by fast+
show "redex_patterns B = [(ll → rr, [])]" unfolding B by (auto simp: set_zip redex_patterns_to_pterm)
from llrr have "length (vars_term_list ll) = length (var_rule (Rule ll rr))"
by (metis S.length_var_rule prule.sel(1,2))
thus "B ∈ wf_pterm S" unfolding B by (auto intro!: wf_pterm.intros llrr)
{
fix i α p
assume "i < length rdp_A" "(α, p) = rdp_A ! i"
hence "(α,p) ∈ set rdp_A" by auto
note rdp_A_conds = rdp_A_conds[OF this]
} note rdp_A_conds_ith = this
have wf_As: "set As ⊆ wf_pterm R" unfolding As using rdp_A_conds_ith
by (auto simp: wf_pterm_ctxt_apply set_zip intro!: ctxt_of_pos_term_well wf_pterm.intros)
thus wf_A: "A ∈ wf_pterm R" using R.join_list_wf_pterm[OF _ join] by auto
from R.redex_patterns_join_list[OF join] wf_As
have "set (redex_patterns A) = ⋃ (set (map (set ∘ redex_patterns) As))" by auto
also have "… = ⋃ { set (redex_patterns ((ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (λx. to_pterm (τ (rename_many' ren i x))) (vars_term_list (lhs αi)))⟩))
| i αi pi. i < length rdp_A ∧ rdp_A ! i = (αi,pi)}" unfolding set_map o_def As set_zip by force
also have "… = ⋃ { {(αi, pi)} | i αi pi. i < length rdp_A ∧ rdp_A ! i = (αi,pi)}"
proof (intro arg_cong[of _ _ "(⋃)"] Collect_cong ex_cong1 rev_conj_cong refl arg_cong[of _ _ "(=) _"])
fix αi pi i
assume "i < length rdp_A ∧ rdp_A ! i = (αi, pi)"
hence "(αi, pi) ∈ set rdp_A" by (force simp: set_conv_nth)
from rdp_A_conds[OF this]
have "to_rule αi ∈ R" and pi: "pi ∈ poss (l ⋅ τ)" by auto
have "set (redex_patterns
(ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (λx. to_pterm (τ (rename_many' ren i x))) (vars_term_list (lhs αi)))⟩)
= (λ(α, q). (α, pi @ q)) ` set (redex_patterns (Prule αi (map (λx. to_pterm (τ (rename_many' ren i x))) (vars_term_list (lhs αi)))))" (is "?lhs = _")
by (subst R.redex_patterns_context[OF pi], simp)
also have "set (redex_patterns (Prule αi (map (λx. to_pterm (τ (rename_many' ren i x))) (vars_term_list (lhs αi))))) = {(αi, [])}"
by (auto simp: o_def redex_patterns_to_pterm set_zip)
also have "(λ(α, q). (α, pi @ q)) ` … = {(αi, pi)}" by auto
finally show "?lhs = {(αi, pi)} " .
qed
also have "… = ⋃ {u. ∃i. u = {rdp_A ! i} ∧ i < length rdp_A}"
by (intro arg_cong[of _ _ "(⋃)"] Collect_cong ex_cong1, force)
also have "… = set rdp_A" unfolding set_conv_nth by blast
finally have "set rdp_A = set (redex_patterns A)" by auto
from R.redex_patterns_equal[OF wf_A _ this] A'
show "redex_patterns A = rdp_A" using R.redex_patterns_sorted by auto
qed auto
qed
qed
lemma sim_cp_root_impl_sound: "set (sim_cp_root_impl ren RR SS) ⊆ sim_cp_root"
proof
fix A B
assume "(A, B) ∈ set (sim_cp_root_impl ren RR SS)"
from this[unfolded sim_cp_root_impl_def List.maps_eq, simplified] SS obtain rule rdp_A
where llrr: "rule ∈ S"
and rdpA: "rdp_A ∈ set (compute_rp ren RR (fst rule))"
and ne: "rdp_A ≠ []"
and AB: "(A, B) ∈ set (sim_cp_root_of ren rule rdp_A)" by auto
obtain ll rr where rule: "rule = (ll,rr)" by force
from sim_cp_root_of_alt_cond[OF AB[unfolded rule] llrr[unfolded rule]] ne rdpA[unfolded rule fst_conv]
show "(A,B) ∈ sim_cp_root" unfolding sim_cp_root_def by blast
qed
lemma sim_cp_non_root_of_alt_cond:
assumes lfrf: "(lf,rf) ∈ R"
and llrr: "(ll,rr) ∈ S"
and q_ne: "q ≠ []"
and q: "q ∈ fun_poss lf"
and rdpA: "rdpA ∈ set (non_root_rdps ren RR (Rule lf rf) q ll)"
and AB: "(A,B) ∈ set (sim_cp_non_root_of ren (Rule lf rf) q (Rule ll rr) rdpA)"
shows "∃ l As τ ren_as Bs. alt_cond τ ((Rule lf rf, []) # rdpA) l (Rule ll rr) q A B As ren_as ∧ q ≠ [] ∧ A = Prule (Rule lf rf) Bs"
proof -
define rdp_A where rdp_A_eq: "rdp_A = (Rule lf rf, []) # rdpA"
define ren_as where ren_as: "ren_as = rename_list (map (λ(α, p). lhs α) rdp_A)"
define l where l: "l = (ctxt_of_pos_term q (hd ren_as))⟨map_vars_term (rename_single ren) ll⟩"
from AB[unfolded sim_cp_non_root_of_def List.maps_eq Let_def prule.sel, folded rdp_A_eq, folded ren_as, folded l]
obtain As τ
where mgu: "mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) ren_as (map snd rdp_A)) = Some τ"
and As: "As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i)
(vars_term_list (lhs αi)))⟩) rdp_A [0..<length rdp_A]"
and join: "⨆ As = Some A"
and B: "B = replace_at (to_pterm (l ⋅ τ)) q (Prule (Rule ll rr) (map (to_pterm ∘ τ ∘ ren_l ren) (vars_term_list ll)))"
by (force simp: Let_def o_def)
show ?thesis unfolding rdp_A_eq[symmetric]
unfolding alt_cond_def
proof (intro exI conjI)
show "mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) ren_as (map snd rdp_A)) = Some τ" by fact
show "ren_as = rename_list (map (λ(α, p). lhs α) rdp_A)" by fact
show "l = (ctxt_of_pos_term q (hd ren_as))⟨map_vars_term (rename_single ren) (lhs (Rule ll rr))⟩"
unfolding l by simp
show "q = [] ∨ snd (hd rdp_A) = []" unfolding rdp_A_eq by auto
show "⨆ As = Some A" by fact
show "B = (ctxt_of_pos_term q (to_pterm (l ⋅ τ)))⟨Prule (ll → rr) (map (to_pterm ∘ τ ∘ rename_single ren) (vars_term_list (lhs (ll → rr))))⟩"
unfolding B by simp
show "rdp_A ≠ []" unfolding rdp_A_eq by simp
show "to_rule (ll → rr) ∈ S" using llrr by auto
show "q ≠ []" by fact
show "As =
map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs αi)))⟩)
rdp_A [0..<length rdp_A]"
by fact
have idx: "[0..<length (x # rdpA)] = 0 # map Suc [0..<length rdpA]" for x unfolding rdp_A_eq
using map_Suc_upt upt_rec by fastforce
from fun_poss_imp_poss[OF q] have ql: "q ∈ poss l" unfolding l ren_as rename_list_def rdp_A_eq length_map idx
by simp (metis hole_pos_ctxt_of_pos_term hole_pos_poss poss_map_vars_term)
show "redex_patterns B = [(ll → rr, q)]" unfolding B o_def
by (subst S.redex_patterns_context, insert ql, auto dest!: set_zip_rightD simp: redex_patterns_to_pterm)
from llrr have len_llrr: "length (var_rule (Rule ll rr)) = length (vars_term_list ll)"
by (metis prule.sel(1,2) S.vars_rule_vars_lhs)
show "B ∈ wf_pterm S" unfolding B using len_llrr ql
by (auto simp: wf_pterm_ctxt_apply to_pterm_trs_ctxt intro!: wf_pterm.intros llrr)
have len_As: "length As = length rdp_A" unfolding As by auto
define ps where "ps = var_poss_list lf"
define addp :: "pos ⇒ (('b, 'a) prule × nat list) ⇒ (('b, 'a) prule × nat list)"
where "addp p = (map_prod id ((@) p))" for p
have addp: "addp p = (λ(α, q). (α, p @ q))" for p unfolding addp_def by (intro ext, force)
from rdpA[unfolded non_root_rdps_def set_map set_concat_lists prule.sel, folded ps_def, simplified]
obtain rdps where rdpA_conv: "rdpA = concat rdps"
and len_rdps: "length rdps = length ps"
and rdps_cond: "⋀ i. i < length ps ⟹ rdps ! i
∈ set (if q ≤⇩p ps ! i ∧ ps ! i -⇩p q ∈ fun_poss ll
then map (map (addp (ps ! i))) (compute_rp ren RR (ll |_ (ps ! i -⇩p q))) else [[]])"
unfolding addp_def by auto
from llrr have funl: "is_Fun ll"
using S.no_var_lhs by auto
hence qll: "q ∈ (@) q ` fun_poss (lhs (ll → rr))" by (cases ll, auto)
{
fix αi p
assume "(αi,p) ∈ set rdpA"
from this[unfolded rdpA_conv set_concat set_conv_nth[of rdps] len_rdps]
obtain i where i: "i < length ps" and mem: "(αi,p) ∈ set (rdps ! i)" by auto
from rdps_cond[OF i] mem
have pos: "q ≤⇩p ps ! i" "ps ! i -⇩p q ∈ fun_poss ll"
and rdpsi: "rdps ! i ∈ map (addp (ps ! i)) ` set (compute_rp ren RR (ll |_ (ps ! i -⇩p q)))"
by (auto split: if_splits)
then obtain rdpi where rdpi: "rdpi ∈ set (compute_rp ren RR (ll |_ (ps ! i -⇩p q)))"
and rdpsi: "rdps ! i = map (addp (ps ! i)) rdpi" by auto
from mem[unfolded rdpsi] obtain u where mem: "(αi,u) ∈ set rdpi"
and p: "p = ps ! i @ u" unfolding addp_def by auto
from rdpi[unfolded compute_rp] mem obtain C where C: "(αi,u) ∈ set (redex_patterns C)" "C ∈ wf_pterm R"
and u: "u ∈ fun_poss (ll |_ (ps ! i -⇩p q))" by auto
from C have αi: "to_rule αi ∈ R" using R.redex_pattern_rule_symbol by blast
hence "is_Fun (lhs αi)"
using R.no_var_lhs by fastforce
hence "p ∈ (@) p ` fun_poss (lhs αi)" by (cases "lhs αi", auto)
moreover have p: "p ∈ (@) q ` fun_poss (lhs (ll → rr))" using u p pos
by simp (smt (verit, best) append.assoc fun_poss_poss image_eqI poss_append_poss prefix_pos_diff subt_at_append)
ultimately have over: "(@) p ` fun_poss (lhs αi) ∩ (@) q ` fun_poss (lhs (ll → rr)) ≠ {}" by auto
from p have "p ∈ (@) q ` fun_poss ll" by auto
note αi over this
} note rdpA_cond = this
thus "∀(α, p)∈set rdp_A. (@) p ` fun_poss (lhs α) ∩ (@) q ` fun_poss (lhs (ll → rr)) ≠ {}"
"∀(α, p)∈set rdp_A. to_rule α ∈ R"
unfolding rdp_A_eq using lfrf qll q
by auto
{
fix i
assume i: "i < length ps"
have "∃ C. C ∈ wf_pterm R ∧ rdps ! i = map (addp (ps ! i)) (redex_patterns C)"
proof (cases "q ≤⇩p ps ! i ∧ ps ! i -⇩p q ∈ fun_poss ll")
case True
with rdps_cond[OF i] compute_rp[of "ll |_ (ps ! i -⇩p q)"]
show ?thesis by auto
next
case False
with rdps_cond[OF i]
show ?thesis by (intro exI[of _ "Var undefined"], auto)
qed
}
hence "∀ i. ∃ C. i < length ps ⟶ C ∈ wf_pterm R ∧ rdps ! i = map (addp (ps ! i)) (redex_patterns C)" by auto
from choice[OF this] obtain C where C: "⋀ i. i < length ps ⟹ C i ∈ wf_pterm R"
and rdpsi: "⋀i. i < length ps ⟹ rdps ! i = map (addp (ps ! i)) (redex_patterns (C i))" by auto
have rdpsC: "rdpA = concat (map (λ i. map (addp (ps ! i)) (redex_patterns (C i))) [0..<length ps])"
unfolding rdpA_conv
by (rule arg_cong[of _ _ concat], rule nth_equalityI, insert rdpsi, auto simp: len_rdps)
hence rdp_AC: "rdp_A = (lf → rf, []) # concat (map (λ i. map (addp (ps ! i)) (redex_patterns (C i))) [0..<length ps])"
unfolding rdp_A_eq by auto
let ?D = "Prule (lf → rf) (map C [0..<length ps])"
from lfrf have len_lf: "length (var_rule (lf → rf)) = length ps"
by (metis length_var_poss_list R.length_var_rule prule.sel(1,2) ps_def)
have D: "?D ∈ wf_pterm R" using lfrf len_lf C by (auto intro!: wf_pterm.intros)
have rp_D: "redex_patterns ?D = rdp_A" unfolding rdp_AC using len_lf
by (auto simp: addp o_def ps_def[symmetric] intro!: arg_cong[of _ _ concat] nth_equalityI)
have As: "As = Prule (lf → rf) (map (to_pterm ∘ τ ∘ rename_many' ren 0) (vars_term_list lf)) #
map (λ i. case rdpA ! i of (αi,pi) ⇒
(ctxt_of_pos_term pi (to_pterm (l ⋅ τ)))⟨Prule αi (map (to_pterm ∘ τ ∘ rename_many' ren (Suc i)) (vars_term_list (lhs αi)))⟩)
[0..<length rdpA]"
unfolding As rdp_A_eq idx
apply simp
apply (intro nth_equalityI)
apply force
subgoal for i by (cases "rdpA ! i", auto)
done
have len_lf': "length (var_rule (Rule lf rf)) = length (vars_term_list lf)"
unfolding len_lf ps_def using length_var_poss_list by blast
have "hd ren_as = map_vars_term (rename_many' ren 0) lf"
unfolding ren_as rdp_A_eq rename_list_def length_map
by (simp add: upt_conv_Cons del: upt_Suc)
note l = l[unfolded this]
{
fix i α p
assume "i < length rdpA" "rdpA ! i = (α, p)"
hence "(α,p) ∈ set rdpA" by (force simp: set_conv_nth)
from rdpA_cond[OF this] have rule: "to_rule α ∈ R"
and "p ∈ (@) q ` fun_poss ll" by auto
then obtain r where p: "p = q @ r" "r ∈ fun_poss ll" by auto
from rule have len: "length (vars_term_list (lhs α)) = length (var_rule α)"
using R.length_var_rule by auto
have p: "p ∈ poss (l ⋅ τ)" unfolding l using fun_poss_imp_poss[OF q] fun_poss_imp_poss[OF p(2)] p(1)
by (auto simp add: poss_ctxt_apply map_vars_term_as_subst)
note p rule len
} note rdpA_conds = this
hence wf_As: "∀a∈set As. a ∈ wf_pterm R" unfolding As using len_lf'
by (auto split: prod.splits simp: wf_pterm_ctxt_apply intro!: ctxt_of_pos_term_well wf_pterm.intros lfrf)
from R.join_list_wf_pterm[OF wf_As join]
show A: "A ∈ wf_pterm R" by auto
show "redex_patterns A = rdp_A"
proof (rule R.redex_patterns_equal[OF A R.redex_patterns_sorted, symmetric, unfolded R.redex_patterns_join_list[OF join wf_As],
OF D, unfolded rp_D])
have "⋃ (set (map (set ∘ redex_patterns) As)) =
insert (lf → rf, [])
(⋃x∈{0..<length rdpA}. case rdpA ! x of
(αi, pi) ⇒
set (redex_patterns (
(ctxt_of_pos_term pi
(to_pterm (l ⋅ τ)))⟨Prule αi (map (λxa. to_pterm (τ (rename_many' ren (Suc x) xa))) (vars_term_list (lhs αi)))⟩)))" (is "_ = insert ?rp ?rest")
unfolding As o_def set_map
by (auto simp add: set_zip o_def redex_patterns_to_pterm)
also have "?rest = (⋃x∈{0..<length rdpA}. {rdpA ! x})"
proof (rule arg_cong[of _ _ Union], intro image_cong refl, goal_cases)
case (1 i)
hence i: "i < length rdpA" by auto
obtain αi pi where eq: "rdpA ! i = (αi,pi)" by force
from rdpA_conds[OF i eq] have pi: "pi ∈ poss (l ⋅ τ)" by auto
have "set (redex_patterns
(ctxt_of_pos_term pi
(to_pterm (l ⋅ τ)))⟨Prule αi (map (λxa. to_pterm (τ (rename_many' ren (Suc i) xa))) (vars_term_list (lhs αi)))⟩)
= {(αi,pi)}"
unfolding R.redex_patterns_context[OF pi]
by (auto simp add: o_def redex_patterns_to_pterm set_zip)
with eq show ?case by simp
qed
also have "… = set rdpA" unfolding set_conv_nth by auto
also have "insert ?rp … = set rdp_A" unfolding rdp_A_eq by simp
finally show "set rdp_A = ⋃ (set (map (set ∘ redex_patterns) As))" ..
qed
note rdp = this[unfolded rdp_A_eq]
have "∃ As. A = Prule (Rule lf rf) As"
proof (cases A)
case (Pfun f As)
have "[] ∉ snd ` set (redex_patterns A)" unfolding Pfun by force
from this[unfolded rdp] have False by force
thus ?thesis by auto
qed (insert rdp, auto)
thus "A = Prule (Rule lf rf) (args A)" by (cases A, auto)
qed
qed
lemma non_root_sim_cps_alt_cond:
assumes lfrf: "(lf,rf) ∈ R"
and llrr: "(ll,rr) ∈ S"
and q_ne: "q ≠ []"
and q: "q ∈ fun_poss lf"
and AB: "(A,B) ∈ set (non_root_sim_cps ren RR (Rule lf rf) q (Rule ll rr))"
shows "∃ rdp_A l As τ ren_as Bs. alt_cond τ rdp_A l (Rule ll rr) q A B As ren_as ∧ q ≠ [] ∧ A = Prule (Rule lf rf) Bs"
proof -
from AB[unfolded non_root_sim_cps_def List.maps_eq, simplified]
obtain rdpA where "rdpA ∈ set (non_root_rdps ren RR (Rule lf rf) q ll)"
and "(A, B) ∈ set (sim_cp_non_root_of ren (Rule lf rf) q (Rule ll rr) rdpA)" by auto
from sim_cp_non_root_of_alt_cond[OF lfrf llrr q_ne q this]
show ?thesis by blast
qed
lemma sim_cp_non_root_impl_sound: "set (sim_cp_non_root_impl ren RR SS) ⊆ sim_cp_non_root"
proof
fix A B
assume "(A, B) ∈ set (sim_cp_non_root_impl ren RR SS)"
from this[unfolded sim_cp_non_root_impl_def List.maps_eq Let_def o_def, simplified] RR SS obtain lf rf q ll rr
where lfrf: "(lf,rf) ∈ R"
and llrr: "(ll,rr) ∈ S"
and q_ne: "q ≠ []"
and q: "q ∈ fun_poss lf"
and AB: "(A,B) ∈ set (non_root_sim_cps ren RR (Rule lf rf) q (Rule ll rr))"
by metis
from non_root_sim_cps_alt_cond[OF this]
show "(A,B) ∈ sim_cp_non_root" unfolding sim_cp_non_root_def using q_ne by blast
qed
lemma sim_cp_root_impl: "set (sim_cp_root_impl ren RR SS) = sim_cp_root"
using sim_cp_root_impl_sound sim_cp_root_impl_complete by blast
lemma sim_cp_non_root_impl: "set (sim_cp_non_root_impl ren RR SS) = sim_cp_non_root"
using sim_cp_non_root_impl_sound sim_cp_non_root_impl_complete by blast
theorem sim_cp_impl: "set (sim_cp_impl ren RR SS) = sim_cp"
unfolding sim_cp_impl_def set_append sim_cp_root_impl sim_cp_non_root_impl
by (metis sim_cp_split)
lemma sim_cp_root_non_root_disj: "sim_cp_root ∩ sim_cp_non_root = {}"
unfolding sim_cp_root_def sim_cp_non_root_def
by (auto simp: alt_cond_def)
context
assumes distRR: "distinct RR" and distSS: "distinct SS"
begin
lemma distinct_compute_rp: "distinct (compute_rp ren RR t)"
proof (induct t rule: compute_rp.induct)
case Fun: (2 f ts)
show ?case unfolding compute_rp.simps distinct_append
proof (intro conjI, goal_cases)
case 3
show ?case (is "?A ∩ ?B = {}")
proof (rule ccontr)
assume "?A ∩ ?B ≠ {}"
then obtain rdp where A: "rdp ∈ ?A" and B: "rdp ∈ ?B" by blast
from B[unfolded Let_def o_def List.maps_eq set_concat set_map set_filter map_map]
obtain l r xs where "rdp = (l → r, []) # xs" by force
hence "(l → r, []) ∈ set rdp" by auto
with A have "(l → r, []) ∈ ⋃ (set ` ?A)" by auto
thus False
apply clarsimp
subgoal for xs xsi unfolding set_conv_nth[of xs] by auto
done
qed
next
case 2
show ?case
proof (intro distinct_maps, goal_cases)
case 1
show ?case by (rule distinct_filter, rule distRR)
next
case (2 ruleA ruleB)
from ‹ruleA ≠ ruleB› obtain llA rrA llB rrB where
rule: "ruleA = (llA,rrA)" "ruleB = (llB,rrB)" and diff: "Rule llA rrA ≠ Rule llB rrB"
by (cases ruleA; cases ruleB; auto)
define list where "list ll rr = (let ps = filter ((≠) []) (var_poss_list ll);
rec =
map (λp. if p ∈ fun_poss (Fun f ts) then map (map (map_prod id ((@) p))) (compute_rp ren RR (Fun f ts |_ p))
else [[]])
ps
in map ((#) (ll → rr, [])) ((map concat ∘ concat_lists) rec))" for ll rr
{
fix ll rr
have one: "[(ll → rr,[])] ∈ set (list ll rr)"
proof -
define ps where "ps = filter ((≠) []) (var_poss_list ll)"
define seti where "seti i = set (map (λp. if p ∈ fun_poss (Fun f ts)
then map (map (map_prod id ((@) p))) (compute_rp ren RR (Fun f ts |_ p)) else [[]])
ps !
i)" for i
have "replicate (length ps) [] ∈ {as. length as = length ps ∧ (∀i<length ps. as ! i ∈ seti i)}"
apply (intro CollectI conjI allI impI)
subgoal by simp
subgoal for i unfolding seti_def using empty_compute_rp[of ren RR "Fun f ts |_ p" for p]
by auto
done
thus ?thesis unfolding list_def Let_def set_map o_def set_concat_lists length_map ps_def[symmetric] seti_def[symmetric]
by (intro imageI) (metis (no_types, lifting) concat_replicate_trivial image_iff)
qed
moreover have "hd ` set (list ll rr) ⊆ {(Rule ll rr, [])}"
unfolding list_def Let_def set_map image_comp o_def list.sel by blast
ultimately have "hd ` set (list ll rr) = {(Rule ll rr, [])}" by force
} note hd_list = this
show ?case (is "?A ∩ ?B = {}")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain rdp where A: "rdp ∈ ?A" and B: "rdp ∈ ?B" by blast
from A[unfolded rule split fst_conv snd_conv, folded list_def] have "rdp ∈ set (list llA rrA)" .
with hd_list[of llA rrA] have "hd rdp = (Rule llA rrA, [])" by auto
moreover
from B[unfolded rule split fst_conv snd_conv, folded list_def] have "rdp ∈ set (list llB rrB)" .
with hd_list[of llB rrB] have "hd rdp = (Rule llB rrB, [])" by auto
ultimately show False using diff by auto
qed
next
case (3 rule)
obtain ll rr where rule: "rule = (ll,rr)" by force
with 3 RR have "(ll,rr) ∈ R" by auto
define ps where "ps = filter ((≠) []) (var_poss_list (fst (ll,rr)))"
define addp :: "pos ⇒ (('b, 'a) prule × nat list) ⇒ (('b, 'a) prule × nat list)"
where "addp = (λ p. (map_prod id ((@) p)))"
define list where "list p = (if p ∈ fun_poss (Fun f ts) then map (map (addp p)) (compute_rp ren RR (Fun f ts |_ p))
else [[]])" for p
have "?case = distinct (map (λx. (ll → rr, []) # concat x) (concat_lists (map list ps)))"
unfolding rule split ps_def Let_def o_def list_def addp_def
by (simp add: o_def)
also have "…" unfolding distinct_map set_concat_lists length_map
proof (intro conjI inj_onI, goal_cases)
case (2 rdpsA rdpsB)
from 2(1) have lenA: "length rdpsA = length ps"
and memA: "⋀ i. i<length ps ⟹ rdpsA ! i ∈ set (list (ps ! i))" by auto
from 2(2) have lenB: "length rdpsB = length ps"
and memB: "⋀ i. i<length ps ⟹ rdpsB ! i ∈ set (list (ps ! i))" by auto
from 2(3) have conc: "concat rdpsA = concat rdpsB" by auto
show "rdpsA = rdpsB"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain i where i: "i < length ps" and diff: "rdpsA ! i ≠ rdpsB ! i" using lenA lenB
by (metis nth_equalityI)
define filt :: "(('b, 'a) prule × nat list) list ⇒ (('b, 'a) prule × nat list) list"
where "filt = filter (λ pair. pair ∈ range (addp (ps ! i)))"
{
fix as :: "(('b, 'a) prule × nat list) list list"
assume len: "length as = length ps" and mem: "⋀ i. i < length ps ⟹ as ! i ∈ set (list (ps ! i))"
{
fix nums
assume nums: "set nums ⊆ {..<length ps} - {i}"
have "filt (concat (map (λ j. as ! j) nums)) = []"
proof (rule ccontr)
assume "¬ ?thesis"
hence "set (filt (concat (map (λ j. as ! j) nums))) ≠ {}" by auto
from this[unfolded filt_def, simplified]
obtain j a where "j ∈ set nums"
and a: "a ∈ set (as ! j)" and ai: "a ∈ range (addp (ps ! i))" by auto
with nums have ji: "j ≠ i" and j: "j < length ps" by auto
from mem[OF j, unfolded list_def] a
have "as ! j ∈ set (map (map (addp (ps ! j))) (compute_rp ren RR (Fun f ts |_ ps ! j)))"
by (simp split: if_splits)
from this a have aj: "a ∈ range (addp (ps ! j))" by auto
from aj ai obtain pi pj where eq: "ps ! i @ pi = ps ! j @ pj" unfolding addp_def
by (metis (no_types, lifting) prod.inject prod_fun_imageE)
have dist: "distinct ps" unfolding ps_def fst_conv using distinct_var_poss_list[of ll] by (rule distinct_filter)
with i j ji have diff: "ps ! i ≠ ps ! j"
using distinct_conv_nth by blast
{
fix k
assume "k < length ps"
hence "ps ! k ∈ set ps" by auto
hence "ps ! k ∈ var_poss ll" unfolding ps_def by auto
}
with i j have mem: "ps ! i ∈ var_poss ll" "ps ! j ∈ var_poss ll" by auto
with diff have "ps ! i ⊥ ps ! j"
using var_poss_parallel by blast
with eq show False
by (metis less_eq_pos_simps(1) pos_less_eq_append_not_parallel)
qed
} note filt = this
have "filt (concat as) = filt (concat (map ((!) as) [0..<length ps]))"
unfolding len[symmetric] by (simp add: map_nth)
also have "[0..<length ps] = [0..<i] @ i # [Suc i ..< length ps]"
by (metis i split_upt)
also have "filt (concat (map ((!) as) …)) =
filt (concat (map ((!) as) [0..<i])) @ filt (as ! i) @ filt (concat (map ((!) as) [Suc i ..< length ps]))"
by (simp add: filt_def)
also have "filt (as ! i) = as ! i" using mem[OF i] unfolding filt_def list_def addp_def
by (simp split: if_splits, force)
also have "filt (concat (map (λ i. as ! i) [0..<i])) = []"
by (rule filt, insert i, auto)
also have "filt (concat (map (λ i. as ! i) [Suc i..<length ps])) = []"
by (rule filt, insert i, auto)
finally have "filt (concat as) = as ! i" by auto
} note filt_concat = this
from conc have "filt (concat rdpsA) = filt (concat rdpsB)" by simp
also have "filt (concat rdpsA) = rdpsA ! i"
by (rule filt_concat, insert lenA memA, auto)
also have "filt (concat rdpsB) = rdpsB ! i"
by (rule filt_concat, insert lenB memB, auto)
finally have "rdpsA ! i = rdpsB ! i" .
with ‹rdpsA ! i ≠ rdpsB ! i› show False ..
qed
next
show "distinct (concat_lists (map list ps))"
proof (rule distinct_concat_lists, unfold length_map set_map, goal_cases)
case (1 xs)
from this[unfolded list_def] obtain t p where
"xs = map (map (addp p)) (compute_rp ren RR t) ∧ p ∈ fun_poss (Fun f ts) ∧ p ∈ set ps ∧ t = Fun f ts |_ p ∨ xs = [[]]"
(is "?Eq ∧ ?p ∧ ?ps ∧ ?t ∨ _") by auto
thus "distinct xs"
proof
assume "?Eq ∧ ?p ∧ ?ps ∧ ?t"
hence ?Eq ?p ?t ?ps by auto
have inj: "inj_on (map (addp p)) (set (compute_rp ren RR t))" unfolding addp_def
by (intro inj_on_mapI inj_onI, auto)
show ?thesis unfolding ‹?Eq› distinct_map
proof (intro conjI inj)
show "distinct (compute_rp ren RR t)" unfolding ‹?t›
by (rule Fun(2)[OF ps_def ‹?ps› ‹?p›])
qed
qed simp
qed
qed
finally show ?case .
qed
next
case 1
define addi :: "nat ⇒ (('b, 'a) prule × nat list) ⇒ (('b, 'a) prule × nat list)"
where "addi i = map_prod id ((#) i)" for i
have len: "length (zip [0..<length ts] ts) = length ts" by auto
have map2: "map2 (λx y. map (map (map_prod id ((#) x))) (compute_rp ren RR y)) [0..<length ts] ts
= map (λ i. map (map (addi i)) (compute_rp ren RR (ts ! i))) [0..<length ts]"
by (intro nth_equalityI, auto simp: addi_def)
show ?case unfolding o_def distinct_map set_concat_lists length_map len map2
unfolding set_map
proof (intro conjI inj_onI, goal_cases)
case (2 as bs)
from 2(1) have lenA: "length as = length ts"
and memA: "⋀ i. i < length ts ⟹ as ! i ∈ map (addi i) ` set (compute_rp ren RR (ts ! i))" by auto
from 2(2) have lenB: "length bs = length ts"
and memB: "⋀ i. i < length ts ⟹ bs ! i ∈ map (addi i) ` set (compute_rp ren RR (ts ! i))" by auto
from 2(3) have conc: "concat as = concat bs" .
show "as = bs"
proof (rule ccontr)
assume "as ≠ bs"
with lenA lenB obtain i where i: "i < length ts" and diff: "as ! i ≠ bs ! i"
by (metis nth_equalityI)
define filt where "filt = filter (λ pair. pair ∈ range (addi i))"
{
fix as :: "(('b, 'a) prule × nat list) list list"
assume len: "length as = length ts" and mem: "⋀ i. i < length ts ⟹ as ! i ∈ map (addi i) ` set (compute_rp ren RR (ts ! i))"
{
fix nums
assume nums: "set nums ⊆ {..<length ts} - {i}"
have "filt (concat (map (λ j. as ! j) nums)) = []"
proof (rule ccontr)
assume "¬ ?thesis"
hence "set (filt (concat (map (λ j. as ! j) nums))) ≠ {}" by auto
from this[unfolded filt_def, simplified]
obtain j a where "j ∈ set nums"
and a: "a ∈ set (as ! j)" "a ∈ range (addi i)" by auto
with nums have ji: "j ≠ i" and j: "j < length ts" by auto
from mem[OF j] a ji show False unfolding addi_def by auto
qed
} note filt = this
have "filt (concat as) = filt (concat (map (λ i. as ! i) [0..<length ts]))"
unfolding len[symmetric] by (simp add: map_nth)
also have "[0..<length ts] = [0..<i] @ i # [Suc i ..< length ts]"
by (metis i split_upt)
also have "filt (concat (map (λ i. as ! i) …)) =
filt (concat (map (λ i. as ! i) [0..<i])) @ filt (as ! i) @ filt (concat (map (λ i. as ! i) [Suc i..<length ts]))"
by (simp add: filt_def)
also have "filt (as ! i) = as ! i" using mem[OF i] unfolding filt_def by auto
also have "filt (concat (map (λ i. as ! i) [0..<i])) = []"
by (rule filt, insert i, auto)
also have "filt (concat (map (λ i. as ! i) [Suc i..<length ts])) = []"
by (rule filt, insert i, auto)
finally have "filt (concat as) = as ! i" by auto
} note filt_concat = this
from conc have "filt (concat as) = filt (concat bs)" by simp
also have "filt (concat as) = as ! i"
by (rule filt_concat, insert lenA memA, auto)
also have "filt (concat bs) = bs ! i"
by (rule filt_concat, insert lenB memB, auto)
finally have "as ! i = bs ! i" .
with ‹as ! i ≠ bs ! i› show False ..
qed
next
case 1
show "distinct (concat_lists (map (λi. map (map (addi i)) (compute_rp ren RR (ts ! i))) [0..<length ts]))"
proof (rule distinct_concat_lists, unfold set_map, goal_cases)
case (1 rdp)
then obtain i where i: "i < length ts"
and rdp: "rdp = map (map (addi i)) (compute_rp ren RR (ts ! i))" by auto
have inj: "inj_on (map (addi i)) (set (compute_rp ren RR (ts ! i)))"
by (intro inj_on_mapI inj_onI, auto simp: addi_def)
show "distinct rdp" unfolding rdp distinct_map
proof (intro conjI inj)
show "distinct (compute_rp ren RR (ts ! i))"
by (rule Fun(1)[OF _ refl, of i], insert i, force simp: set_zip)
qed
qed
qed
qed
qed simp
lemma distinct_sim_cp_root_impl: "distinct (sim_cp_root_impl ren RR SS)"
unfolding sim_cp_root_impl_def
proof (rule distinct_maps[OF distSS], goal_cases)
case *: (2 rule)
obtain ll rr where rule: "rule = (ll,rr)" by force
with * have llrr: "(ll,rr) ∈ S" using SS by auto
show ?case unfolding rule split fst_conv
proof (rule distinct_maps, goal_cases)
case (3 rdp_A)
show ?case unfolding sim_cp_root_of_def Let_def
by (auto split: option.splits)
next
case (2 rdp_A rdp_B)
from 2 have rdpA: "rdp_A ≠ []" "rdp_A ∈ set (compute_rp ren RR ll)" by auto
from 2 have rdpB: "rdp_B ≠ []" "rdp_B ∈ set (compute_rp ren RR ll)" by auto
show ?case
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A B where AB_A: "(A,B) ∈ set (sim_cp_root_of ren (ll,rr) rdp_A)"
and AB_B: "(A,B) ∈ set (sim_cp_root_of ren (ll, rr) rdp_B)"
by auto
from sim_cp_root_of_alt_cond[OF AB_A llrr rdpA, unfolded alt_cond_def]
have "rdp_A = redex_patterns A" by auto
moreover from sim_cp_root_of_alt_cond[OF AB_B llrr rdpB, unfolded alt_cond_def]
have "rdp_B = redex_patterns A" by auto
ultimately show False using ‹rdp_A ≠ rdp_B› by auto
qed
next
case 1
show ?case
by (rule distinct_filter[OF distinct_compute_rp])
qed
next
case (1 ruleA ruleB)
from 1(3) obtain llA rrA llB rrB where rule: "ruleA = (llA,rrA)" "ruleB = (llB,rrB)"
and diff: "(llA,rrA) ≠ (llB,rrB)" by (cases ruleA; cases ruleB; auto)
from 1(1-2) rule have mem: "(llA,rrA) ∈ S" "(llB,rrB) ∈ S" using SS by auto
show ?case (is "?L ∩ ?R = {}")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A B where L: "(A,B) ∈ ?L" and R: "(A,B) ∈ ?R" by fastforce
from L[unfolded rule split List.maps_eq, simplified] obtain rdpL where
rdpL: "rdpL ∈ set (compute_rp ren RR llA)" "rdpL ≠ []"
and ABL: "(A,B) ∈ set (sim_cp_root_of ren (llA,rrA) rdpL)" by force
from sim_cp_root_of_alt_cond[OF ABL mem(1) rdpL(2,1), unfolded alt_cond_def]
have "redex_patterns B = [(llA → rrA, [])]" by auto
moreover
from R[unfolded rule split List.maps_eq, simplified] obtain rdpR where
rdpR: "rdpR ∈ set (compute_rp ren RR llB)" "rdpR ≠ []"
and ABR: "(A,B) ∈ set (sim_cp_root_of ren (llB,rrB) rdpR)" by force
from sim_cp_root_of_alt_cond[OF ABR mem(2) rdpR(2,1), unfolded alt_cond_def]
have "redex_patterns B = [(llB → rrB, [])]" by auto
ultimately
have "(llA,rrA) = (llB,rrB)" by auto
with diff show False by auto
qed
qed
lemma distinct_non_root_rdps: "distinct (non_root_rdps ren RR (Rule ll rf) q lf)"
proof -
define cond where "cond p = (q ≤⇩p p ∧ p -⇩p q ∈ fun_poss lf)" for p
define addp :: "pos ⇒ (('b, 'a) prule × nat list) ⇒ (('b, 'a) prule × nat list)"
where "addp p = (map_prod id ((@) p))" for p
define list where "list = (λp. if cond p then map (map (addp p)) (compute_rp ren RR (lf |_ (p -⇩p q)))
else [[]])"
define ps where "ps = var_poss_list ll"
show ?thesis
unfolding non_root_rdps_def cond_def[symmetric] addp_def[symmetric] list_def[symmetric]
unfolding distinct_map prule.sel ps_def[symmetric]
proof (intro conjI inj_onI distinct_concat_lists, goal_cases)
case (1 qs)
then obtain p where p: "p ∈ set ps" and qs: "qs = list p" by auto
show "distinct qs"
proof (cases "cond p")
case True
hence qs: "qs = map (map (addp p)) (compute_rp ren RR (lf |_ (p -⇩p q)))"
unfolding qs list_def by auto
show ?thesis unfolding qs distinct_map
by (intro conjI distinct_compute_rp inj_on_mapI inj_onI, auto simp: addp_def)
qed (auto simp: qs list_def)
next
case (2 rdp1 rdp2)
from 2(1)[unfolded set_concat_lists]
have len1: "length rdp1 = length ps"
and mem1: "⋀ i. i < length ps ⟹ rdp1 ! i ∈ set (list (ps ! i))" by auto
from 2(2)[unfolded set_concat_lists]
have len2: "length rdp2 = length ps"
and mem2: "⋀ i. i < length ps ⟹ rdp2 ! i ∈ set (list (ps ! i))" by auto
have conc: "concat rdp1 = concat rdp2" by fact
show "rdp1 = rdp2"
proof (rule ccontr)
assume "rdp1 ≠ rdp2"
with len1 len2 obtain i where i: "i < length ps" and diff: "rdp1 ! i ≠ rdp2 ! i"
by (metis nth_equalityI)
from mem1[OF i] mem2[OF i] diff have "cond (ps ! i)" unfolding list_def
by (auto split: if_splits)
define filt where "filt = filter (λ x. x ∈ range (addp (ps ! i)))"
{
fix as :: "(('b, 'a) prule × nat list) list list"
assume len: "length as = length ps" and mem: "⋀ i. i < length ps ⟹ as ! i ∈ set (list (ps ! i))"
{
fix nums
assume nums: "set nums ⊆ {..<length ps} - {i}"
have "filt (concat (map (λ j. as ! j) nums)) = []"
proof (rule ccontr)
assume "¬ ?thesis"
hence "set (filt (concat (map (λ j. as ! j) nums))) ≠ {}" by auto
from this[unfolded filt_def, simplified]
obtain j a where "j ∈ set nums"
and a: "a ∈ set (as ! j)" and ai: "a ∈ range (addp (ps ! i))" by auto
with nums have ji: "j ≠ i" and j: "j < length ps" by auto
from mem[OF j, unfolded list_def] a
have "as ! j ∈ set (map (map (addp (ps ! j))) (compute_rp ren RR (lf |_ (ps ! j -⇩p q))))"
by (simp split: if_splits)
from this a have aj: "a ∈ range (addp (ps ! j))" by auto
from aj ai obtain pi pj where eq: "ps ! i @ pi = ps ! j @ pj" unfolding addp_def
by (metis (no_types, lifting) prod.inject prod_fun_imageE)
have dist: "distinct ps" unfolding ps_def using distinct_var_poss_list[of ll] .
with i j ji have diff: "ps ! i ≠ ps ! j"
using distinct_conv_nth by blast
{
fix k
assume "k < length ps"
hence "ps ! k ∈ set ps" by auto
hence "ps ! k ∈ var_poss ll" unfolding ps_def by auto
}
with i j have mem: "ps ! i ∈ var_poss ll" "ps ! j ∈ var_poss ll" by auto
with diff have "ps ! i ⊥ ps ! j"
using var_poss_parallel by blast
with eq show False
by (metis less_eq_pos_simps(1) pos_less_eq_append_not_parallel)
qed
} note filt = this
have "filt (concat as) = filt (concat (map ((!) as) [0..<length ps]))"
unfolding len[symmetric] by (simp add: map_nth)
also have "[0..<length ps] = [0..<i] @ i # [Suc i ..< length ps]"
by (metis i split_upt)
also have "filt (concat (map ((!) as) …)) =
filt (concat (map ((!) as) [0..<i])) @ filt (as ! i) @ filt (concat (map ((!) as) [Suc i ..< length ps]))"
by (simp add: filt_def)
also have "filt (as ! i) = as ! i" using mem[OF i] unfolding filt_def list_def addp_def
by (simp split: if_splits, force)
also have "filt (concat (map (λ i. as ! i) [0..<i])) = []"
by (rule filt, insert i, auto)
also have "filt (concat (map (λ i. as ! i) [Suc i..<length ps])) = []"
by (rule filt, insert i, auto)
finally have "filt (concat as) = as ! i" by auto
} note filt_concat = this
from conc have "filt (concat rdp1) = filt (concat rdp2)" by simp
also have "filt (concat rdp1) = rdp1 ! i"
by (rule filt_concat, insert len1 mem1, auto)
also have "filt (concat rdp2) = rdp2 ! i"
by (rule filt_concat, insert len2 mem2, auto)
finally have "rdp1 ! i = rdp2 ! i" .
with ‹rdp1 ! i ≠ rdp2 ! i› show False ..
qed
qed
qed
lemma distinct_sim_cp_non_root_impl: "distinct (sim_cp_non_root_impl ren RR SS)"
unfolding sim_cp_non_root_impl_def
proof (rule distinct_maps[OF distRR], goal_cases)
case (1 rule1 rule2)
obtain ll1 rr1 ll2 rr2 where rule: "rule1 = (ll1,rr1)" "rule2 = (ll2,rr2)" by force
from 1[unfolded rule] have rule1: "(ll1,rr1) ∈ R" and rule2: "(ll2,rr2) ∈ R"
and diff: "(ll1,rr1) ≠ (ll2,rr2)" unfolding RR by auto
show ?case (is "?S1 ∩ ?S2 = {}")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A B where mem1: "(A,B) ∈ ?S1" and mem2: "(A,B) ∈ ?S2" by fast
from mem1[unfolded rule split List.maps_eq set_concat set_map RR image_comp o_def Let_def prule.sel]
obtain q1 l1 r1
where cond1: "q1 ∈ set (filter ((≠) []) (fun_poss_list ll1))" "(l1,r1) ∈ S"
and AB1: "(A, B) ∈ set (non_root_sim_cps ren RR (Rule ll1 rr1) q1 (Rule l1 r1))"
by (force simp: RR SS)
from mem2[unfolded rule split List.maps_eq set_concat set_map RR image_comp o_def] obtain q2 l2 r2
where cond2: "q2 ∈ set (filter ((≠) []) (fun_poss_list ll2))" "(l2,r2) ∈ S"
and AB2: "(A, B) ∈ set (non_root_sim_cps ren RR (Rule ll2 rr2) q2 (Rule l2 r2))"
by (force simp: RR SS)
from cond1 have q1: "q1 ≠ []" "q1 ∈ fun_poss ll1" by auto
from non_root_sim_cps_alt_cond[OF rule1 cond1(2) q1 AB1] obtain Bs1
where AB1: "A = Prule (ll1 → rr1) Bs1" "redex_patterns B = [(Rule l1 r1, q1)]"
by (auto simp: alt_cond_def)
from cond2 have q2: "q2 ≠ []" "q2 ∈ fun_poss ll2" by auto
from non_root_sim_cps_alt_cond[OF rule2 cond2(2) q2 AB2] obtain Bs2
where AB2: "A = Prule (ll2 → rr2) Bs2" "redex_patterns B = [(Rule l2 r2, q2)]"
by (auto simp: alt_cond_def)
from AB1 AB2
have "(ll1,rr1) = (ll2,rr2)" by auto
with diff show False by auto
qed
next
case (2 rule)
obtain ll rr where rule: "rule = (ll,rr)" by force
from 2[unfolded rule] have llrr: "(ll,rr) ∈ R" unfolding RR by auto
let ?ps = "(filter ((≠) []) (fun_poss_list ll))"
show ?case unfolding rule split Let_def prule.sel
proof (rule distinct_maps, goal_cases)
case 1
show "distinct ?ps"
by (rule distinct_filter[OF distinct_fun_poss_list])
next
case (2 q1 q2)
show ?case (is "?M1 ∩ ?M2 = {}")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A B where AB1: "(A,B) ∈ ?M1" and AB2: "(A,B) ∈ ?M2" by force
from 2 have q1: "q1 ≠ []" "q1 ∈ fun_poss ll" by auto
from 2 have q2: "q2 ≠ []" "q2 ∈ fun_poss ll" by auto
from AB1[unfolded List.maps_eq] obtain l1 r1 where
cond1: "(l1,r1) ∈ S"
and AB1: "(A, B) ∈ set (non_root_sim_cps ren RR (Rule ll rr) q1 (Rule l1 r1))"
by (auto simp: SS)
from AB2[unfolded List.maps_eq] obtain l2 r2 where
cond2: "(l2,r2) ∈ S"
and AB2: "(A, B) ∈ set (non_root_sim_cps ren RR (Rule ll rr) q2 (Rule l2 r2))"
by (auto simp: SS)
from non_root_sim_cps_alt_cond[OF llrr cond1 q1 AB1, unfolded alt_cond_def]
have "redex_patterns B = [(l1 → r1, q1)]" by auto
moreover
from non_root_sim_cps_alt_cond[OF llrr cond2 q2 AB2, unfolded alt_cond_def]
have "redex_patterns B = [(l2 → r2, q2)]" by auto
ultimately have "q1 = q2" by auto
with ‹q1 ≠ q2› show False by auto
qed
next
case q: (3 q)
hence q: "q ≠ []" "q ∈ fun_poss ll" by auto
show ?case
proof (rule distinct_maps, goal_cases)
case 1
show ?case by (rule distinct_filter, rule distSS)
next
case (2 rule1 rule2)
obtain lf1 rf1 where rule1: "rule1 = (lf1,rf1)" by force
obtain lf2 rf2 where rule2: "rule2 = (lf2,rf2)" by force
from 2 rule1 rule2
have lf1: "(lf1,rf1) ∈ S"
and lf2: "(lf2,rf2) ∈ S"
and diff: "(lf1,rf1) ≠ (lf2,rf2)" by (auto simp: SS)
show ?case (is "?M1 ∩ ?M2 = {}")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A B where AB1: "(A,B) ∈ ?M1" and AB2: "(A,B) ∈ ?M2" by force
from AB1[unfolded rule1] have AB1: "(A,B) ∈ set (non_root_sim_cps ren RR (Rule ll rr) q (Rule lf1 rf1))" by auto
from AB2[unfolded rule2] have AB2: "(A,B) ∈ set (non_root_sim_cps ren RR (Rule ll rr) q (Rule lf2 rf2))" by auto
from non_root_sim_cps_alt_cond[OF llrr lf1 q AB1, unfolded alt_cond_def]
have "redex_patterns B = [(lf1 → rf1, q)]" by auto
moreover
from non_root_sim_cps_alt_cond[OF llrr lf2 q AB2, unfolded alt_cond_def]
have "redex_patterns B = [(lf2 → rf2, q)]" by auto
ultimately have "(lf1,rf1) = (lf2,rf2)" by auto
with diff show False by auto
qed
next
case Rule: (3 Rul)
obtain lf rf where id: "Rul = (lf,rf)" by force
from Rule[unfolded id] have lfrf: "(lf, rf) ∈ S" using SS by auto
show ?case unfolding id split non_root_sim_cps_def
proof (rule distinct_maps[OF distinct_non_root_rdps], goal_cases)
case (1 rdp1 rdp2)
show ?case (is "?M1 ∩ ?M2 = {}")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A B where AB1: "(A,B) ∈ ?M1" and AB2: "(A,B) ∈ ?M2" by fast
from sim_cp_non_root_of_alt_cond[OF llrr lfrf q 1(1)[unfolded prule.sel] AB1, unfolded alt_cond_def]
have "redex_patterns A = (ll → rr, []) # rdp1" by auto
moreover
from sim_cp_non_root_of_alt_cond[OF llrr lfrf q 1(2)[unfolded prule.sel] AB2, unfolded alt_cond_def]
have "redex_patterns A = (ll → rr, []) # rdp2" by auto
ultimately have "rdp1 = rdp2" by auto
with ‹rdp1 ≠ rdp2› show False by auto
qed
next
case (2 rdp)
show "distinct (sim_cp_non_root_of ren (Rule ll rr) q (Rule lf rf) rdp)"
unfolding sim_cp_non_root_of_def Let_def
by (auto split: option.splits)
qed
qed
qed
qed
lemma sim_cp_impl_dist: "distinct (sim_cp_impl ren RR SS)"
unfolding sim_cp_impl_def distinct_append sim_cp_root_impl sim_cp_non_root_impl
by (intro conjI sim_cp_root_non_root_disj distinct_sim_cp_root_impl distinct_sim_cp_non_root_impl)
end
end
lemma finite_sim_cp: assumes "finite R" "finite S"
shows "finite sim_cp"
proof -
from assms obtain RR SS where "set RR = R" "set SS = S"
using finite_list[of R] finite_list[of S] by auto
from sim_cp_impl[OF this] show ?thesis using finite_set[of "sim_cp_impl ren RR SS"] by auto
qed
end
lemma mstep_subst: assumes "(s,t) ∈ mstep R"
shows "(s ⋅ σ, t ⋅ σ) ∈ mstep R"
using assms
proof (induct s t)
next
case (rule l r σ' τ)
then show ?case
by (simp add: eval_subst mstep.rule subst_compose_def)
qed (auto intro: mstep.intros)
lemma sim_cps_impl: "sim_cp_closed ren (set R) = (left_lin_wf_trs (set R)
∧ (∀ cp ∈ set (sim_cps_impl ren R R). fst cp = snd cp ∨
(∃ l r v. instance_rule cp (l,r) ∧ (l, v) ∈ (rstep (set R))⇧* ∧ (r, v) ∈ mstep (set R))))"
unfolding sim_cp_closed_def
proof (intro conj_cong refl)
assume ll: "left_lin_wf_trs (set R)"
interpret left_lin_wf_trs "set R" by fact
interpret ren_wf_trs ren "set R" "set R" by intro_locales
have set: "set (sim_cps_impl ren R R) = map_prod target target ` sim_cp"
unfolding sim_cps_impl_def set_map sim_cp_impl[OF refl refl] ..
show "(∀A B. (A, B) ∈ sim_cp ⟶
(∃v. (target A, v) ∈ (rstep (set R))⇧* ∧
(target B, v) ∈ mstep (set R))) ⟷
(∀cp∈set (sim_cps_impl ren R R).
fst cp = snd cp ∨
(∃ l r v.
instance_rule cp (l, r) ∧
(l, v) ∈ (rstep (set R))⇧* ∧ (r, v) ∈ mstep (set R)))"
(is "(∀ A B. ?cond A B) ⟷ (∀ cp ∈ _. ?condR cp)")
proof (intro iffI allI impI ballI disjI2)
fix cp
assume cond: "∀ A B. ?cond A B"
assume cp: "cp ∈ set (sim_cps_impl ren R R)"
from this[unfolded set] obtain A B where AB: "(A,B) ∈ sim_cp"
and cp: "cp = (target A, target B)" by auto
from cond[rule_format, OF AB] obtain v where
join: "(target A, v) ∈ (rstep (set R))⇧*" "(target B, v) ∈ mstep (set R)" by auto
have inst: "instance_rule cp (target A, target B)" unfolding cp by auto
show "∃l r v.
instance_rule cp (l, r) ∧
(l, v) ∈ (rstep (set R))⇧* ∧ (r, v) ∈ mstep (set R)"
using inst join by auto
next
fix A B
assume cond: "∀cp∈set (sim_cps_impl ren R R). ?condR cp"
assume AB: "(A, B) ∈ sim_cp"
from AB have "(target A, target B) ∈ set (sim_cps_impl ren R R)"
unfolding set by auto
from cond[rule_format, OF this] obtain v l r
where "target A = target B ∨
instance_rule (target A, target B) (l, r) ∧ (l, v) ∈ (rstep (set R))⇧* ∧ (r, v) ∈ mstep (set R)"
(is "?eq ∨ ?inst ∧ ?join")
by auto
thus "∃v. (target A, v) ∈ (rstep (set R))⇧* ∧ (target B, v) ∈ mstep (set R)"
proof
assume ?eq
thus ?thesis by (intro exI[of _ "target B"], auto)
next
assume "?inst ∧ ?join"
hence ?inst and ?join by auto
from ‹?inst› obtain σ where target: "target A = l ⋅ σ" "target B = r ⋅ σ"
unfolding instance_rule_def by auto
from ‹?join› have "(l ⋅ σ, v ⋅ σ) ∈ (rstep (set R))⇧*"
using rsteps_closed_subst by blast
moreover from ‹?join› have "(r ⋅ σ, v ⋅ σ) ∈ mstep (set R)"
by (intro mstep_subst, auto)
ultimately show ?thesis unfolding target by auto
qed
qed
qed
context
begin
private fun in_funposs :: "pos ⇒ ('f, 'v) term ⇒ bool"
where
"in_funposs (Cons i p) (Fun f ts) ⟷ i < length ts ∧ in_funposs p (ts ! i)" |
"in_funposs [] (Fun _ _) ⟷ True" |
"in_funposs p (Var _) ⟷ False"
lemma funposs_code[code_unfold]:
"p ∈ fun_poss t = in_funposs p t" by (induct rule: in_funposs.induct) auto
end
typedef ('f,'v)ll_rule = "{(l :: ('f,'v)term ,r :: ('f,'v)term ,p ,xs) |
l r p xs. is_Fun l ∧ vars_term r ⊆ vars_term l ∧ p = var_poss_list l ∧ linear_term l ∧ xs = vars_term_list l}"
morphisms ll_rule_tuple LL_Rule
by (intro exI[of _ "(Fun undefined [], Fun undefined [], [], [])"])
(auto simp: is_partition_def vars_term_list.simps)
setup_lifting type_definition_ll_rule
instantiation ll_rule :: (type,type)equal
begin
lift_definition equal_ll_rule :: "('a,'b)ll_rule ⇒ ('a,'b)ll_rule ⇒ bool" is "λ (l,r,_) (l',r',_). l = l' ∧ r = r'" .
instance
proof
fix x y :: "('a,'b)ll_rule"
show "equal_class.equal x y = (x = y)"
by (transfer, auto)
qed
end
lift_definition Lhs :: "('f,'v)ll_rule ⇒ ('f,'v)term" is fst .
lift_definition Rhs :: "('f,'v)ll_rule ⇒ ('f,'v)term" is "fst o snd" .
lift_definition Var_rule_list :: "('f,'v)ll_rule ⇒ 'v list" is "snd o snd o snd" .
lift_definition Var_poss_list :: "('f,'v)ll_rule ⇒ pos list" is "fst o snd o snd" .
lift_definition To_rule :: "('f,'v)ll_rule ⇒ ('f,'v)rule" is "λ (l,r,_). (l,r)" .
lift_definition To_prule :: "('f,'v)ll_rule ⇒ ('f,'v)prule" is "λ (l,r,_). Rule l r" .
lift_definition rel_ll_rule :: "('f,'v)ll_rule ⇒ ('f,'v)prule ⇒ bool" is "λ (l,r,_) rule. Rule l r = rule" .
lift_definition rel_ll_rule' :: "('f,'v)ll_rule ⇒ ('f,'v)rule ⇒ bool" is "λ (l,r,_) rule. (l,r) = rule" .
context includes lifting_syntax
begin
lemma zip_option_non_rec: "zip_option xs ys = (if length xs = length ys then Some (zip xs ys) else None)"
by auto
lemma zip_option_transfer[transfer_rule]: "(list_all2 R ===> list_all2 S ===> rel_option (list_all2 (rel_prod R S))) zip_option zip_option"
unfolding zip_option_non_rec by transfer_prover
lemma decompose_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique RF"
shows "(rel_term RF RX ===> rel_term RF RY ===>
rel_option (list_all2 (rel_prod (rel_term RF RX) (rel_term RF RY)))) decompose decompose"
proof (intro rel_funI, goal_cases)
case (1 T t S s)
note [transfer_rule] = 1
have id: "(is_Var T ∨ is_Var S) = (is_Var t ∨ is_Var s)"
by transfer_prover
show ?case
proof (cases "is_Var t ∨ is_Var s")
case True
hence dec: "decompose t s = None" by (cases t; cases s; auto simp: decompose_def)
from True id have "is_Var T ∨ is_Var S" by auto
hence Dec: "decompose T S = None" by (cases T; cases S; auto simp: decompose_def)
show ?thesis unfolding dec Dec by transfer_prover
next
case False
then obtain f ss g ts where id2: "s = Fun f ss" "t = Fun g ts" by (cases s; cases t, auto)
hence dec: "decompose t s = (if g = f then zip_option ts ss else None)" by (simp add: decompose_def)
from False id have "¬ (is_Var T ∨ is_Var S)" by auto
then obtain F Ss G Ts where id3: "S = Fun F Ss" "T = Fun G Ts" by (cases S; cases T, auto)
hence Dec: "decompose T S = (if G = F then zip_option Ts Ss else None)" by (simp add: decompose_def)
from 1[unfolded id2 id3] have [transfer_rule]: "RF F f" "RF G g"
"list_all2 (rel_term RF RX) Ts ts" "list_all2 (rel_term RF RY) Ss ss"
by auto
show ?thesis unfolding dec Dec by transfer_prover
qed
qed
lemma concat_lists_transfer[transfer_rule]: "(list_all2 (list_all2 A) ===> list_all2 (list_all2 A)) concat_lists concat_lists"
unfolding rel_fun_def
proof (intro allI impI, goal_cases)
case (1 xss yss)
thus ?case
proof (induct xss yss)
case Nil
show ?case by (simp add: concat_lists.simps)
next
case (Cons x xs y ys)
note [transfer_rule] = Cons
show ?case unfolding concat_lists.simps
by transfer_prover
qed
qed
lemma match_term_list_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique RF" "bi_unique RX"
shows "(list_all2 (rel_prod (rel_term RF RX) (rel_term RF RX))
===> (RX ===> rel_option (rel_term RF RX))
===> rel_option (RX ===> rel_option (rel_term RF RX))) match_term_list match_term_list"
(is "(?LRel ===> ?SRel ===> ?ORel) _ _")
proof -
let ?RT = "rel_term RF RX"
let ?TRel = "list_all2 ?RT"
show ?thesis
proof (intro rel_funI, goal_cases)
case (1 Xs xs Sig sig)
thus ?case
proof (induct xs sig arbitrary: Xs Sig rule: match_term_list.induct)
case (2 x t ps sig Qs Sig)
have [transfer_rule]: "?SRel Sig sig" by fact
from 2(2) obtain S T Ps where Qs: "Qs = (S, T) # Ps" and
Ps: "?LRel Ps ps" and
"?RT S (Var x)" and T[transfer_rule]: "?RT T t"
by (cases Qs, auto)
from this(3) obtain X where S: "S = Var X" and [transfer_rule]: "RX X x" by cases auto
have id: "(Sig X = None ∨ Sig X = Some T) = (sig x = None ∨ sig x = Some t)"
by transfer_prover
have Sig: "?SRel (Sig(X ↦ T)) (sig(x ↦ t))" by transfer_prover
show ?case
proof (cases "sig x = None ∨ sig x = Some t")
case True
have [transfer_rule]: "?ORel (match_term_list Ps (Sig(X ↦ T))) (match_term_list ps (sig(x ↦ t)))"
by (rule 2(1)[OF True Ps Sig])
show ?thesis unfolding Qs S match_term_list.simps id by transfer_prover
next
case False
hence id2: "(sig x = None ∨ sig x = Some t) = False" by simp
show ?thesis unfolding Qs S match_term_list.simps id id2 if_False by transfer_prover
qed
next
case (3 f ss g ts ps sig Qs Sig)
from 3(2) obtain S T Ps where Qs: "Qs = (S,T) # Ps"
and [transfer_rule]: "?LRel Ps ps" and S: "?RT S (Fun f ss)" and T: "?RT T (Fun g ts)"
by (cases Qs, auto)
from S obtain F Ss where S: "S = Fun F Ss" and [transfer_rule]: "?TRel Ss ss" "RF F f"
by (cases S, auto)
from T obtain G Ts where T: "T = Fun G Ts" and [transfer_rule]: "?TRel Ts ts" "RF G g"
by (cases T, auto)
have id [transfer_rule]: "rel_option (list_all2 (rel_prod ?RT ?RT))
(decompose (Fun F Ss) (Fun G Ts)) (decompose (Fun f ss) (Fun g ts))" (is "rel_option ?Rel ?D ?d")
by transfer_prover
show ?case
proof (cases ?d)
case d: None
with id have D: "?D = None" by auto
show ?thesis unfolding Qs S T match_term_list.simps D d option.simps by simp
next
case d: (Some xs)
with id obtain Xs where D: "?D = Some Xs" and [transfer_rule]: "?Rel Xs xs" by (cases ?D, auto)
have "?Rel (Xs @ Ps) (xs @ ps)" by transfer_prover
from 3(1)[OF d this 3(3)]
show ?thesis unfolding Qs S T match_term_list.simps d D option.simps .
qed
next
case (4 f ss x ps sig Qs Sig)
from 4(1) obtain S T Ps where Qs: "Qs = (S,T) # Ps"
and [transfer_rule]: "?LRel Ps ps" and S: "?RT S (Fun f ss)" and T: "?RT T (Var x)"
by (cases Qs, auto)
from S obtain F Ss where S: "S = Fun F Ss"
by (cases S, auto)
from T obtain X where T: "T = Var X" by (cases T, auto)
show ?case unfolding T S Qs unfolding match_term_list.simps by transfer_prover
qed auto
qed
qed
lemma subst_of_map_transfer[transfer_rule]:
"((RA ===> RB) ===> (RA ===> rel_option RB) ===> (RA ===> RB)) subst_of_map subst_of_map"
proof (intro rel_funI, goal_cases)
case (1 D d S s X x)
note [transfer_rule] = 1
have sx: "rel_option RB (S X) (s x)" by transfer_prover
show ?case
proof (cases "S X")
case None
with sx have sx: "s x = None" by (cases "s x", auto)
show ?thesis unfolding subst_of_map_def sx None option.simps by transfer_prover
next
case (Some B)
with sx obtain b where sx: "s x = Some b" and [transfer_rule]: "RB B b" by (cases "s x", auto)
show ?thesis unfolding subst_of_map_def sx Some option.simps by transfer_prover
qed
qed
lemma match_list_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique RF" "bi_unique RX"
shows "((RX ===> rel_term RF RX)
===> list_all2 (rel_prod (rel_term RF RX) (rel_term RF RX))
===> rel_option (RX ===> rel_term RF RX)) match_list match_list"
unfolding match_list_def by transfer_prover
lemma match_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique RF" "bi_unique RX"
shows "(rel_term RF RX ===> rel_term RF RX
===> rel_option (RX ===> rel_term RF RX)) match match"
unfolding match_def by transfer_prover
lemma To_rule[transfer_rule]: "(rel_ll_rule ===> (=)) To_rule to_rule"
unfolding rel_fun_def
by (transfer, auto)
lemma Var_rule_list_term_list[transfer_rule]: "(rel_ll_rule ===> (=)) Var_rule_list (λ r. vars_term_list (lhs r))"
unfolding rel_fun_def
by transfer auto
lemma Var_rule_list[transfer_rule]: "(rel_ll_rule ===> (=)) Var_rule_list var_rule"
unfolding rel_fun_def
proof (transfer, clarsimp, goal_cases)
case (1 l r)
hence "distinct (vars_term_list l)"
using linear_term_distinct_vars by blast
thus "vars_term_list l = rev (remdups (rev (vars_term_list l)))"
by (simp add: distinct_remdups_id)
qed
lemma Var_rule_list'[transfer_rule]: "(rel_ll_rule' ===> (=)) Var_rule_list (λ rule. vars_term_list (fst rule))"
unfolding rel_fun_def
by (transfer, auto)
lemma Var_poss_list[transfer_rule]: "(rel_ll_rule ===> (=)) Var_poss_list (λ rule. var_poss_list (lhs rule)) "
unfolding rel_fun_def
by (transfer, simp)
lemma To_prule[transfer_rule]: "(rel_ll_rule' ===> (=)) To_prule (λ r. Rule (fst r) (snd r))"
unfolding rel_fun_def
by (transfer, auto)
lemma rel_ll_rule'_to_rel_ll_rule[transfer_rule]: "(rel_ll_rule' ===> rel_ll_rule) (λ Ru. Ru) (λ r. Rule (fst r) (snd r))"
unfolding rel_fun_def
by (transfer, auto)
lemma Rhs[transfer_rule]: "(rel_ll_rule ===> (=)) Rhs rhs"
unfolding rel_fun_def
by (transfer, auto)
lemma Lhs[transfer_rule]: "(rel_ll_rule ===> (=)) Lhs lhs"
unfolding rel_fun_def
by (transfer, auto)
lemma Lhs'[transfer_rule]: "(rel_ll_rule' ===> (=)) Lhs fst"
unfolding rel_fun_def
by (transfer, auto)
lemma Rhs'[transfer_rule]: "(rel_ll_rule' ===> (=)) Rhs snd"
unfolding rel_fun_def
by (transfer, auto)
lemma To_rule'[transfer_rule]: "(rel_ll_rule' ===> (=)) To_rule (λ x. x)"
unfolding rel_fun_def
by (transfer, auto)
lemma Domainp_rel_ll_rule [transfer_domain_rule]:
"Domainp (rel_ll_rule) = (λ i. True)"
by (intro ext, unfold Domainp_iff, transfer, auto)
lemma bi_unique_rel_ll_rule [transfer_rule]: "bi_unique rel_ll_rule" "left_unique rel_ll_rule" "right_unique rel_ll_rule"
unfolding bi_unique_def left_unique_def right_unique_def
by (transfer, auto)+
type_synonym
('f, 'v) Pterm = "(('f, 'v) ll_rule + 'f, 'v) term"
abbreviation rel_Pterm :: "('f,'v)Pterm ⇒ ('f,'v)pterm ⇒ bool" where
"rel_Pterm ≡ rel_term (rel_sum rel_ll_rule (=)) (=)"
lemma To_prule_transfer: "rel_ll_rule r (To_prule r)"
by (transfer, auto)
lemma rel_Pterm_map: "rel_Pterm t (map_term (map_sum To_prule id) id t)"
proof (induct t)
case (Fun f ts)
then show ?case
by (smt (verit) To_prule_transfer id_apply sum.rel_map(2) sum.rel_refl term.rel_map(2)
term.rel_refl)
qed simp
fun Target :: "('f,'v)Pterm ⇒ ('f,'v)term" where
"Target (Var x) = (Var x)"
| "Target (Fun (Inr f) As) = Fun f (map Target As)"
| "Target (Fun (Inl Alpha) As) = Rhs Alpha ⋅ mk_subst Var (zip (Var_rule_list Alpha) (map Target As))"
lemma Target[transfer_rule]: "(rel_Pterm ===> (=)) Target target"
unfolding rel_fun_def
proof (intro allI impI, goal_cases)
case (1 Pt pt)
from ‹rel_Pterm Pt pt›
show "Target Pt = target pt"
proof (induct)
case (Fun Fs fs Ts ts)
have IH: "list_all2 (λa b. Target a = target b) fs ts" by fact
hence map: "map Target fs = map target ts"
by (simp add: list_all2_conv_all_nth map_eq_conv')
from ‹rel_sum rel_ll_rule (=) Fs Ts›
show ?case
proof induct
case (2 F f)
thus ?case using map by simp
next
case (1 Rule rule)
with rel_funD[OF To_rule this] rel_funD[OF Rhs this] rel_funD[OF Var_rule_list this] map
show ?case by simp
qed
qed simp
qed
fun to_Pterm :: "('f, 'v) term ⇒ ('f, 'v) Pterm" where
"to_Pterm (Var x) = Var x"
| "to_Pterm (Fun f ts) = Fun (Inr f) (map to_Pterm ts)"
lemma to_Pterm[transfer_rule]: "((=) ===> rel_Pterm) to_Pterm to_pterm"
proof (intro rel_funI, clarify)
fix t :: "('a,'b)term"
show "rel_Pterm (to_Pterm t) (to_pterm t)"
proof (induct t)
case (Var x)
then show ?case by auto
next
case (Fun f ts)
show ?case unfolding to_Pterm.simps to_pterm.simps term.simps
apply (intro conjI list_all2_map_map)
subgoal by transfer_prover
subgoal using Fun by auto
done
qed
qed
lemma match_Var_to_Pterm_termination[termination_simp]:
assumes "match (Var x) (to_Pterm l) = Some σ"
and "(a, b) ∈ set (zip (map σ (vars_term_list l)) ts)"
shows "size a = 1"
proof-
from assms(1) have *:"(to_Pterm l) ⋅ σ = Var x" by (simp add: match_matches)
then obtain y where y:"l = Var y" by (metis subst_apply_eq_Var term.distinct(1) to_Pterm.elims)
with * have **:"σ y = Var x" by simp
from y have "vars_term_list l = [y]" by (simp add: vars_term_list.simps(1))
with assms(2) y have "a = Var x" by (simp add: "**" in_set_zip)
then show ?thesis by simp
qed
lemma match_Fun_to_Pterm_termination[termination_simp]:
assumes "match (Fun f ss) (to_Pterm l) = Some σ"
and *: "(s, t) ∈ set (zip (map σ (vars_term_list l)) ts)"
shows "size s ≤ Suc (size_list size ss)"
proof -
from * have "s ∈ set (map σ (vars_term_list l))" by (blast elim: in_set_zipE)
then obtain x where [simp]: "s = σ x"
and x: "x ∈ vars_term (to_Pterm l)" by (induct l) auto
from match_vars_term_size [OF assms(1) x]
show ?thesis by simp
qed
lemma Var_rule_list_vars_term[termination_simp]: "Var_rule_list α = vars_term_list (Lhs α)"
by transfer auto
fun Join :: "('f, 'v) Pterm ⇒ ('f,'v) Pterm ⇒ ('f,'v) Pterm option"
where
"Join (Var x) (Var y) =
(if x = y then Some (Var x) else None)"
| "Join (Fun (Inr f) As) (Fun (Inr g) Bs) =
(if (f = g ∧ length As = length Bs) then
(case those (map2 Join As Bs) of
Some xs ⇒ Some (Fun (Inr f) xs)
| None ⇒ None)
else None)"
| "Join (Fun (Inl α) As) (Fun (Inl β) Bs) =
(if α = β then
(case those (map2 Join As Bs) of
Some xs ⇒ Some (Fun (Inl α) xs)
| None ⇒ None)
else None)"
| "Join (Fun (Inl α) As) B =
(case match B (to_Pterm (Lhs α)) of
None ⇒ None
| Some σ ⇒
(case those (map2 Join As (map σ (Var_rule_list α))) of
Some xs ⇒ Some (Fun (Inl α) xs)
| None ⇒ None))"
| "Join A (Fun (Inl α) Bs) =
(case match A (to_Pterm (Lhs α)) of
None ⇒ None
| Some σ ⇒
(case those (map2 Join (map σ (Var_rule_list α)) Bs) of
Some xs ⇒ Some (Fun (Inl α) xs)
| None ⇒ None))"
| "Join A B = None"
lemma Join[transfer_rule]: "(rel_Pterm ===> rel_Pterm ===> rel_option rel_Pterm) Join join"
proof (intro rel_funI, goal_cases)
case (1 A a B b)
let ?L = "rel_ll_rule"
let ?P = "rel_Pterm"
let ?PS = "list_all2 ?P"
let ?POS = "list_all2 (rel_option ?P)"
let ?S = "rel_option ((=) ===> ?P)"
note j_def = join.simps Join.simps
from 1 show ?case
proof (induct a b arbitrary: A B rule: join.induct)
case *: (1 x y A B)
from *(1) have A: "A = Var x" by (cases A, auto)
from *(2) have B: "B = Var y" by (cases B, auto)
show ?case unfolding j_def A B by auto
next
case *: (2 f as g bs A B)
from *(2) obtain As where A: "A = Fun (Inr f) As" and As[transfer_rule]: "?PS As as"
by (cases, auto, auto simp: rel_sum.simps)
from *(3) obtain Bs where B: "B = Fun (Inr g) Bs" and Bs[transfer_rule]: "?PS Bs bs"
by (cases, auto, auto simp: rel_sum.simps)
have id: "(f = g ∧ length As = length Bs) = (f = g ∧ length as = length bs)" (is "_ = ?cond")
by transfer_prover
show ?case
proof (cases ?cond)
case False
hence cond: "?cond = False" by auto
show ?thesis unfolding j_def A B cond id if_False by transfer_prover
next
case True
hence cond: "?cond = True" by auto
have IH[transfer_rule]: "?POS (map2 Join As Bs) (map2 join as bs)"
using *(1)[OF True _ refl, of "as ! i" "bs ! i" "As ! i" "Bs ! i" for i] As Bs True
unfolding set_zip list_all2_conv_all_nth
by auto blast
show ?thesis unfolding j_def A B cond id if_True by transfer_prover
qed
next
case *: (3 α as β bs A B)
from *(2) obtain Al As where A: "A = Fun (Inl Al) As" and As[transfer_rule]: "?PS As as" "?L Al α"
by (cases A, auto, auto simp: rel_sum.simps)
from *(3) obtain Be Bs where B: "B = Fun (Inl Be) Bs" and Bs[transfer_rule]: "?PS Bs bs" "?L Be β"
by (cases B, auto, auto simp: rel_sum.simps)
have id: "(Al = Be) = (α = β)" (is "_ = ?cond") by transfer_prover
show ?case
proof (cases ?cond)
case True
hence cond: "?cond = True" by auto
have IH[transfer_rule]: "?POS (map2 Join As Bs) (map2 join as bs)"
using *(1)[OF True _ refl, of "as ! i" "bs ! i" "As ! i" "Bs ! i" for i] As Bs True
unfolding set_zip list_all2_conv_all_nth
by fastforce
show ?thesis unfolding j_def A B cond id if_True by transfer_prover
next
case False
hence cond: "?cond = False" by auto
show ?thesis unfolding j_def A B cond id if_False by transfer_prover
qed
next
case *: ("4_1" α as x A B)
from *(2) obtain Al As where A: "A = Fun (Inl Al) As" and As[transfer_rule]: "?PS As as" "?L Al α"
by (cases A, auto, auto simp: rel_sum.simps)
from *(3) have B: "B = Var x" by (cases, auto)
have "?S (match (Var x) (to_Pterm (Lhs Al))) (match (Var x) (to_pterm (lhs α)))"
by transfer_prover
thus ?case
proof cases
case None
show ?thesis unfolding j_def A B None option.simps by transfer_prover
next
case (Some Tau tau)
note [transfer_rule] = Some(3)
from rel_funD[OF Var_rule_list As(2)]
have vars: "var_rule α = Var_rule_list Al" (is "_ = ?xs") ..
have taus: "?PS (map Tau ?xs) (map tau ?xs)" unfolding vars
by transfer_prover
have [transfer_rule]: "?POS (map2 Join As (map Tau ?xs)) (map2 join as (map tau ?xs))"
using *(1)[OF Some(2) _ refl, of "as ! i" for i] As taus
unfolding set_zip list_all2_conv_all_nth vars length_map
by fastforce
show ?thesis unfolding j_def A B Some option.simps vars by transfer_prover
qed
next
case *: ("4_2" α as f bs A B)
from *(2) obtain Al As where A: "A = Fun (Inl Al) As" and As[transfer_rule]: "?PS As as" "?L Al α"
by (cases A, auto, auto simp: rel_sum.simps)
from *(3) obtain Bs where B: "B = Fun (Inr f) Bs" and Bs[transfer_rule]: "?PS Bs bs"
by (cases, auto, auto simp: rel_sum.simps)
have "?S (match (Fun (Inr f) Bs) (to_Pterm (Lhs Al))) (match (Pfun f bs) (to_pterm (lhs α)))"
by transfer_prover
thus ?case
proof cases
case None
show ?thesis unfolding j_def A B None option.simps by transfer_prover
next
case (Some Tau tau)
note [transfer_rule] = Some(3)
from rel_funD[OF Var_rule_list As(2)]
have vars: "var_rule α = Var_rule_list Al" (is "_ = ?xs") ..
have taus: "?PS (map Tau ?xs) (map tau ?xs)" unfolding vars
by transfer_prover
have [transfer_rule]: "?POS (map2 Join As (map Tau ?xs)) (map2 join as (map tau ?xs))"
using *(1)[OF Some(2) _ refl, of "as ! i" for i] As taus
unfolding set_zip list_all2_conv_all_nth vars length_map
by fastforce
show ?thesis unfolding j_def A B Some option.simps vars by transfer_prover
qed
next
case *: ("5_1" x α as B A)
from *(3) obtain Al As where A: "A = Fun (Inl Al) As" and As[transfer_rule]: "?PS As as" "?L Al α"
by (cases A, auto, auto simp: rel_sum.simps)
from *(2) have B: "B = Var x" by (cases, auto)
have "?S (match (Var x) (to_Pterm (Lhs Al))) (match (Var x) (to_pterm (lhs α)))"
by transfer_prover
thus ?case
proof cases
case None
show ?thesis unfolding j_def A B None option.simps by transfer_prover
next
case (Some Tau tau)
note [transfer_rule] = Some(3)
from rel_funD[OF Var_rule_list As(2)]
have vars: "var_rule α = Var_rule_list Al" (is "_ = ?xs") ..
have taus: "?PS (map Tau ?xs) (map tau ?xs)" unfolding vars
by transfer_prover
have [transfer_rule]: "?POS (map2 Join (map Tau ?xs) As) (map2 join (map tau ?xs) as)"
using *(1)[OF Some(2) _ refl, of _ "as ! i" for i] As taus
unfolding set_zip list_all2_conv_all_nth vars length_map
by fastforce
show ?thesis unfolding j_def A B Some option.simps vars by transfer_prover
qed
next
case *: ("5_2" f bs α as B A)
from *(3) obtain Al As where A: "A = Fun (Inl Al) As" and As[transfer_rule]: "?PS As as" "?L Al α"
by (cases A, auto, auto simp: rel_sum.simps)
from *(2) obtain Bs where B: "B = Fun (Inr f) Bs" and Bs[transfer_rule]: "?PS Bs bs"
by (cases, auto, auto simp: rel_sum.simps)
have "?S (match (Fun (Inr f) Bs) (to_Pterm (Lhs Al))) (match (Pfun f bs) (to_pterm (lhs α)))"
by transfer_prover
thus ?case
proof cases
case None
show ?thesis unfolding j_def A B None option.simps by transfer_prover
next
case (Some Tau tau)
note [transfer_rule] = Some(3)
from rel_funD[OF Var_rule_list As(2)]
have vars: "var_rule α = Var_rule_list Al" (is "_ = ?xs") ..
have taus: "?PS (map Tau ?xs) (map tau ?xs)" unfolding vars
by transfer_prover
have [transfer_rule]: "?POS (map2 Join (map Tau ?xs) As) (map2 join (map tau ?xs) as)"
using *(1)[OF Some(2) _ refl, of _ "as ! i" for i] As taus
unfolding set_zip list_all2_conv_all_nth vars length_map
by fastforce
show ?thesis unfolding j_def A B Some option.simps vars by transfer_prover
qed
next
case *: ("6_1" f as x A B)
from *(1) obtain As where A: "A = Fun (Inr f) As" and As[transfer_rule]: "?PS As as"
by (cases, auto, auto simp: rel_sum.simps)
from *(2) have B: "B = Var x" by (cases, auto)
show ?case unfolding A B j_def by transfer_prover
next
case *: ("6_2" x f as B A)
from *(2) obtain As where A: "A = Fun (Inr f) As" and As[transfer_rule]: "?PS As as"
by (cases, auto, auto simp: rel_sum.simps)
from *(1) have B: "B = Var x" by (cases, auto)
show ?case unfolding A B j_def by transfer_prover
qed
qed
fun Join_opt :: "('f, 'v) Pterm ⇒ ('f, 'v) Pterm option ⇒ ('f, 'v) Pterm option"
where
"Join_opt A (Some B) = Join A B"
| "Join_opt _ _ = None"
lemma Join_opt[transfer_rule]: "(rel_Pterm ===> rel_option rel_Pterm ===> rel_option rel_Pterm) Join_opt join_opt"
proof (intro rel_funI, goal_cases)
case (1 A Bo A' Bo')
from 1(2) rel_funD[OF rel_funD[OF Join 1(1)]]
show ?case
by (cases, auto)
qed
fun Join_list :: "('f, 'v) Pterm list ⇒ ('f,'v) Pterm option"
where
"Join_list [] = None"
| "Join_list (A # []) = Some A"
| "Join_list (A # As) = Join_opt A (Join_list As)"
lemma Join_list[transfer_rule]: "(list_all2 rel_Pterm ===> rel_option rel_Pterm) Join_list join_list"
proof (intro rel_funI, goal_cases)
case (1 As as)
thus ?case
proof induct
case C: (Cons A As a as)
from C(2) show ?case
proof cases
case Nil
then show ?thesis using C(1) by auto
next
case (Cons B Bs b bs)
note [transfer_rule] = C(1,3)
show ?thesis unfolding Cons Join_list.simps join_list.simps
unfolding Cons(1-2)[symmetric] by transfer_prover
qed
qed auto
qed
context
fixes ren :: "'v :: infinite renamingN"
and R :: "('f,'v)ll_rule list"
and S :: "('f,'v)ll_rule list"
begin
function Compute_rp :: "('f,'v)term ⇒ (('f, 'v) ll_rule × pos) list list" where
"Compute_rp (Var x) = [[]]"
| "Compute_rp (Fun f ts) =
(map concat o concat_lists) (map2 (λ i ti. map (map (map_prod id ((#) i))) (Compute_rp ti)) [0..<length ts] ts)
@ List.maps (λ rule. let ps = filter ((≠) []) (Var_poss_list rule);
rec = map (λ p. if p ∈ fun_poss (Fun f ts) then map (map (map_prod id ((@) p))) (Compute_rp (Fun f ts |_ p)) else [[]]) ps in
map ((#) (rule, [])) ((map concat o concat_lists) rec))
(filter (λ rule. unify_vd ren [ (Fun f ts, Lhs rule)]) R)"
by pat_completeness auto
termination
proof (standard, rule wf_measure[of size], goal_cases)
case (2 f ts rule filt p)
hence "p ≠ []" and "p ∈ poss (Fun f ts)" by (auto simp: fun_poss_imp_poss)
then show ?case
by simp (metis nth_mem size_simp1 size_simp5 subt_at.simps(1,2) subt_at_subterm supt_size)
qed (auto simp: termination_simp)
definition Sim_cp_root_of where
"Sim_cp_root_of rule rdp_A = (let l = map_vars_term (ren_l ren) (Lhs rule);
renamed_lhs_αs = ren.rename_list ren (map (λ(α, p). Lhs α) rdp_A) in
case mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) of
None ⇒ []
| Some τ ⇒ (let As = map2 (λ prod i. case prod of (αi, pi) ⇒ (ctxt_of_pos_term pi (to_Pterm (l ⋅ τ)))⟨
Fun (Inl αi) (map (to_Pterm ∘ τ ∘ rename_many' ren i) (Var_rule_list αi))⟩)
rdp_A [0..<length rdp_A]
in (case Join_list As of None ⇒ []
| Some A ⇒ (let B = Fun (Inl rule) (map (to_Pterm ∘ τ ∘ ren_l ren)
(Var_rule_list rule))
in [(A,B)]))))"
definition "Sim_cp_root_impl =
List.maps (λ rule. List.maps (λ rdp_A. Sim_cp_root_of rule rdp_A) (filter ((≠) []) (Compute_rp (Lhs rule)))) S"
definition Non_root_rdps where "Non_root_rdps α q ll =
(map concat (concat_lists (map (λ p. if q ≤⇩p p ∧ p -⇩p q ∈ fun_poss ll
then map (map (map_prod id ((@) p))) (Compute_rp (ll |_ (p -⇩p q))) else [[]]) (Var_poss_list α))))"
definition Sim_cp_non_root_of where
"Sim_cp_non_root_of α q β rdpA = (let rdp_A = (α, []) # rdpA;
renamed_lhs_αs = ren.rename_list ren (map (λ(α, p). Lhs α) rdp_A);
l = replace_at (hd renamed_lhs_αs) q (map_vars_term (ren_l ren) (Lhs β))
in (case mgu_list (map2 (λ lhs_α p. (lhs_α, l|_p)) renamed_lhs_αs (map snd rdp_A)) of
None ⇒ []
| Some τ ⇒ (let As = map2 (λ(αi, pi) i. (ctxt_of_pos_term pi (to_Pterm (l ⋅ τ)))⟨Fun (Inl αi) (map (to_Pterm ∘ τ ∘ rename_many' ren i) (Var_rule_list αi))⟩)
rdp_A [0..<length rdp_A]
in (case Join_list As of None ⇒ []
| Some A ⇒ (let B = replace_at (to_Pterm (l ⋅ τ)) q (Fun (Inl β) (map (to_Pterm ∘ τ ∘ ren_l ren) (Var_rule_list β)))
in [(A,B)])))))"
definition Non_root_sim_cps where "Non_root_sim_cps α q β = (List.maps (Sim_cp_non_root_of α q β)
(Non_root_rdps α q (Lhs β)))"
definition Sim_cp_non_root_impl where
"Sim_cp_non_root_impl = List.maps (λ α. List.maps (λ q. List.maps ( λ β. Non_root_sim_cps α q β)
(filter (λ β. unify_vd ren [(Lhs β, Lhs α |_q)]) S)) (filter ((≠) []) (fun_poss_list (Lhs α)))) R"
definition Sim_cp_impl where "Sim_cp_impl = Sim_cp_root_impl @ Sim_cp_non_root_impl"
definition Sim_cps_impl where "Sim_cps_impl = map (map_prod Target Target) Sim_cp_impl"
end
lemma Compute_rp[transfer_rule]: "((=) ===> (list_all2 rel_ll_rule') ===> (=) ===>
list_all2 (list_all2 (rel_prod rel_ll_rule (=)))) Compute_rp compute_rp"
unfolding rel_fun_def
proof (intro allI impI, clarify, goal_cases)
case (1 _ ren R r _ t)
have R[transfer_rule]: ‹list_all2 rel_ll_rule' R r› by fact
show "list_all2 (list_all2 (rel_prod rel_ll_rule (=))) (Compute_rp ren R t)
(compute_rp ren r t)"
proof (induct t rule: compute_rp.induct)
case Var: (1 x)
then show ?case by auto
next
case Fun: (2 f ts)
have len: "length (zip [0..<length ts] ts) = length ts" by simp
{
fix n
assume "n < length ts"
hence "(n,ts ! n) ∈ set (zip [0..<length ts] ts)" by (force simp: set_zip)
from Fun(1)[OF this refl]
have IH[transfer_rule]: "list_all2 (list_all2 (rel_prod rel_ll_rule (=))) (local.Compute_rp ren R (ts ! n))
(compute_rp ren r (ts ! n))" .
have "list_all2 (list_all2 (rel_prod rel_ll_rule (list_all2 (=))))
(map (map (map_prod id ((#) n))) (local.Compute_rp ren R (ts ! n)))
(map (map (map_prod id ((#) n))) (compute_rp ren r (ts ! n)))"
by transfer_prover
} note IH1 = this
show ?case unfolding Compute_rp.simps compute_rp.simps o_def
proof (intro list_all2_appendI, goal_cases)
case 1
show ?case
apply (rule rel_funD[OF rel_funD[OF list.map_transfer]])
apply transfer_prover
apply (rule rel_funD[OF concat_lists_transfer])
apply (rule list_all2_all_nthI, force)
using IH1 by simp
next
case 2
show ?case unfolding List.maps_eq
apply (rule rel_funD[OF concat_transfer])
apply (rule rel_funD[OF rel_funD[OF list.map_transfer]])
defer
apply transfer_prover
apply (rule rel_funI)
apply (unfold Let_def)
apply (rule rel_funD[OF rel_funD[OF list.map_transfer, of "list_all2 (rel_prod rel_ll_rule (=))"]])
subgoal for Rule rule
proof (goal_cases)
case 1
from rel_funD[OF rel_ll_rule'_to_rel_ll_rule 1]
have [transfer_rule]: "rel_ll_rule Rule (fst rule → snd rule)" .
show ?case by transfer_prover
qed
apply (rule rel_funD[OF rel_funD[OF list.map_transfer]])
apply (rule concat_transfer)
apply (rule rel_funD[OF concat_lists_transfer])
proof (goal_cases)
case (1 Rule rule)
from rel_funD[OF rel_ll_rule'_to_rel_ll_rule 1]
have "rel_ll_rule Rule (fst rule → snd rule)" by auto
from rel_funD[OF Var_poss_list this]
have Vp: "Var_poss_list Rule = var_poss_list (fst rule)" by simp
show ?case unfolding Vp
proof (rule list_all2_map_map, goal_cases)
case (1 p)
show ?case
proof (cases "p ∈ fun_poss (Fun f ts)")
case True
hence id: "(p ∈ fun_poss (Fun f ts)) = True" by simp
note IH[transfer_rule] = Fun(2)[OF refl 1 True]
show ?thesis unfolding id if_True
by transfer_prover
qed auto
qed
qed
qed
qed
qed
lemma rel_Pterm_replace_at_to_pterm: assumes "rel_Pterm T t"
shows "p ∈ poss u ⟹
rel_Pterm (ctxt_of_pos_term p (to_Pterm u))⟨T⟩ (ctxt_of_pos_term p (to_pterm u))⟨t⟩"
proof (induct p arbitrary: u)
case Nil
thus ?case using assms by auto
next
case (Cons i p)
then obtain f us where u: "u = Fun f us" and i: "i < length us" and p: "p ∈ poss (us ! i)" by (cases u, auto)
note [transfer_rule] = Cons(1)[OF p]
show ?case unfolding u
by (simp add: i) transfer_prover
qed
lemma Sim_cp_root_of: fixes Rule :: "('a,'b :: infinite) ll_rule"
assumes rule [transfer_rule]: "rel_ll_rule' Rule rule"
and Rdp[transfer_rule]: "list_all2 (rel_prod rel_ll_rule (=)) Rdp rdp"
and pos: "snd ` set rdp ⊆ poss (fst rule)"
shows "list_all2 (rel_prod rel_Pterm rel_Pterm) (Sim_cp_root_of ren Rule Rdp)
(sim_cp_root_of ren rule rdp)"
proof -
define l where l: "l = map_vars_term (rename_single ren) (fst rule)"
define ren_as where ren_as: "ren_as = ren.rename_list ren (map (λ(α, p). lhs α) rdp)"
define mgu where mgu: "mgu = mgu_list (map2 (λx y. (x, l |_ y)) ren_as (map snd rdp))"
define xs where xs: "xs = vars_term_list (fst rule)"
have id1: "Lhs Rule = fst rule" by transfer_prover
have id2: "map (λ(α, p). Lhs α) Rdp = map (λ(α, p). lhs α) rdp" by transfer_prover
have id3: "map snd Rdp = map snd rdp" by transfer_prover
have id4: "Var_rule_list Rule = vars_term_list (fst rule)"
using rel_funD[OF Var_rule_list' rule] .
have len: "length Rdp = length rdp" by transfer_prover
show ?thesis
unfolding sim_cp_root_of_def Sim_cp_root_of_def id1 id2
unfolding l[symmetric] ren_as[symmetric]
unfolding Let_def[of l] Let_def[of ren_as]
unfolding id3 id4 len
unfolding mgu[symmetric] xs[symmetric]
apply (rule rel_funD[OF rel_funD[OF rel_funD[OF option.case_transfer]], of _ _ _ "(=)"])
subgoal by transfer_prover
defer
subgoal by transfer_prover
apply (intro rel_funI)
apply (elim subst)
apply (unfold map2_to_map)
apply (unfold len[symmetric], unfold map2_to_map, unfold len)
proof goal_cases
case (1 τ)
define As1 where "As1 = map (λi. case Rdp ! i of
(αi, pi) ⇒
(ctxt_of_pos_term pi
(to_Pterm
(l ⋅ τ)))⟨Fun (Inl αi)
(map (to_Pterm ∘ τ ∘ rename_many' ren i)
(Var_rule_list αi))⟩)
[0..<length rdp]" (is "_ = map ?F _")
define As2 where "As2 = map (λi. case rdp ! i of
(αi, pi) ⇒
(ctxt_of_pos_term pi
(to_pterm
(l ⋅ τ)))⟨Prule αi
(map (to_pterm ∘ τ ∘ rename_many' ren i)
(vars_term_list (lhs αi)))⟩)
[0..<length rdp]" (is "_ = map ?f _")
have As12[transfer_rule]: "list_all2 rel_Pterm As1 As2"
unfolding As1_def As2_def
proof (rule list_all2_map_map)
fix i
assume "i ∈ set [0..<length rdp]"
hence i: "i < length rdp" by auto
with Rdp have rel_prod: "rel_prod rel_ll_rule (=) (Rdp ! i) (rdp ! i)" unfolding list_all2_conv_all_nth by auto
then obtain Rp rp p where Rp[transfer_rule]: "rel_ll_rule Rp rp" and rdpi: "Rdp ! i = (Rp,p)" "rdp ! i = (rp,p)"
by (metis (full_types) prod.collapse rel_prod_inject)
from i have "snd (rdp ! i) ∈ snd ` set rdp" by auto
with assms have "snd (rdp ! i) ∈ poss (fst rule)" by auto
with rdpi have "p ∈ poss (fst rule)" by auto
hence p: "p ∈ poss l" unfolding l by auto
have vars: "Var_rule_list Rp = vars_term_list (lhs rp)"
using rel_funD[OF Var_rule_list_term_list Rp] .
define T where "T = Fun (Inl Rp)
(map (to_Pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs rp)))"
define t where "t = Prule rp (map (to_pterm ∘ τ ∘ rename_many' ren i) (vars_term_list (lhs rp)))"
have T: "rel_Pterm T t" unfolding T_def t_def by transfer_prover
show "rel_Pterm (?F i) (?f i)" unfolding rdpi split vars unfolding T_def[symmetric] t_def[symmetric]
by (rule rel_Pterm_replace_at_to_pterm[OF T], insert p, auto)
qed
define B1 where "B1 = Fun (Inl Rule) (map (to_Pterm ∘ τ ∘ rename_single ren) xs)"
define B2 where "B2 = Prule (fst rule → snd rule) (map (to_pterm ∘ τ ∘ rename_single ren) xs)"
have [transfer_rule]: "rel_ll_rule Rule (fst rule → snd rule)" using rel_funD[OF rel_ll_rule'_to_rel_ll_rule rule] .
have Bb[transfer_rule]: "rel_Pterm B1 B2" unfolding B1_def B2_def o_def
by transfer_prover
show ?case unfolding As1_def[symmetric] As2_def[symmetric] B1_def[symmetric] B2_def[symmetric] Let_def
by transfer_prover
qed
qed
lemma Sim_cp_root_impl[transfer_rule]: "((=) ===> list_all2 rel_ll_rule' ===> list_all2 rel_ll_rule' ===> list_all2 (rel_prod rel_Pterm rel_Pterm))
Sim_cp_root_impl sim_cp_root_impl"
proof (intro rel_funI, clarify, goal_cases)
case (1 ren' ren Rules rules Srules srules)
have Rules[transfer_rule]: "list_all2 rel_ll_rule' Rules rules" by fact
have Rules[transfer_rule]: "list_all2 rel_ll_rule' Srules srules" by fact
have len: "length Rules = length rules" "length Srules = length srules" by transfer_prover+
show ?case unfolding Sim_cp_root_impl_def sim_cp_root_impl_def List.maps_eq
apply (rule rel_funD[OF concat_transfer])
apply (unfold list_all2_conv_all_nth[of _ "map _ Srules"] length_map len)
apply (intro conjI refl allI impI)
proof goal_cases
case (1 i)
hence i: "i < length Srules" using len by auto
from Rules i have rulei [transfer_rule]: "rel_ll_rule' (Srules ! i) (srules ! i)" unfolding list_all2_conv_all_nth by auto
define t where "t = fst (srules ! i)"
have id: "Lhs (Srules ! i) = t" unfolding t_def by transfer_prover
have id2: "fst (srules ! i) = t" unfolding t_def by simp
define Rdp where "Rdp = filter ((≠) []) (Compute_rp ren Rules t)"
define rdp where "rdp = filter ((≠) []) (compute_rp ren rules t)"
have Rdp[transfer_rule]: "list_all2 (list_all2 (rel_prod rel_ll_rule (=))) Rdp rdp"
unfolding Rdp_def rdp_def
apply (rule rel_funD[OF rel_funD[OF filter_transfer]])
subgoal unfolding rel_fun_def by auto
by transfer_prover
have id3: "map (Sim_cp_root_of ren (Srules ! i)) Rdp =
map (λ j. Sim_cp_root_of ren (Srules ! i) (Rdp ! j)) [0..<length Rdp]"
by (intro nth_equalityI, auto)
have id4: "map (sim_cp_root_of ren (srules ! i)) rdp =
map (λ j. sim_cp_root_of ren (srules ! i) (rdp ! j)) [0..<length rdp]"
by (intro nth_equalityI, auto)
have len2: "length Rdp = length rdp" by transfer_prover
show ?case unfolding nth_map[OF i] nth_map[OF 1] id id2
unfolding Rdp_def[symmetric] rdp_def[symmetric]
apply (rule rel_funD[OF concat_transfer])
apply (unfold id3 id4 len2)
apply (rule list_all2_map_map)
apply (rule Sim_cp_root_of[OF rulei]; (unfold t_def[symmetric])?)
proof -
fix j
assume "j ∈ set [0 ..< length rdp]"
hence j: "j < length rdp" by simp
with Rdp show "list_all2 (rel_prod rel_ll_rule (=)) (Rdp ! j) (rdp ! j)"
unfolding list_all2_conv_all_nth by auto
from j have "rdp ! j ∈ set rdp" by auto
also have "set rdp ⊆ set (compute_rp ren rules t)" unfolding rdp_def by auto
finally have "rdp ! j ∈ set (compute_rp ren rules t)" .
thus "snd ` set (rdp ! j) ⊆ poss t" using positions_compute_rp[of ren rules t] by auto
qed
qed
qed
lemma Non_root_rdps[transfer_rule]: "((=) ===> list_all2 rel_ll_rule' ===> rel_ll_rule ===> (=) ===> (=) ===>
list_all2 (list_all2 (rel_prod rel_ll_rule (=))))
Non_root_rdps non_root_rdps"
proof (intro rel_funI, clarify, goal_cases)
case (1 ren' ren Rules rules R r Q q LL ll)
have [transfer_rule]: "list_all2 rel_ll_rule' Rules rules" by fact
have "rel_ll_rule R r" by fact
from rel_funD[OF Var_poss_list this]
have vp: "Var_poss_list R = var_poss_list (lhs r)" by simp
show "list_all2 (list_all2 (rel_prod rel_ll_rule (=))) (Non_root_rdps ren Rules R q ll)
(non_root_rdps ren rules r q ll)"
unfolding Non_root_rdps_def non_root_rdps_def vp by transfer_prover
qed
lemma Sim_cp_non_root_of: fixes Rule :: "('a,'b :: infinite) ll_rule"
assumes rule [transfer_rule]: "rel_ll_rule Rule rule"
and rule' [transfer_rule]: "rel_ll_rule Rule' rule'"
and Rdp[transfer_rule]: "list_all2 (rel_prod rel_ll_rule (=)) Rdp rdp"
and q: "q ∈ poss (lhs rule)"
and pos: "snd ` set rdp ⊆ (@) q ` poss (lhs rule')"
shows "list_all2 (rel_prod rel_Pterm rel_Pterm) (Sim_cp_non_root_of ren Rule q Rule' Rdp)
(sim_cp_non_root_of ren rule q rule' rdp)"
proof -
define rdp_A where "rdp_A = (rule, []) # rdp"
define Rdp_A where "Rdp_A = (Rule, []) # Rdp"
have Rdp_A[transfer_rule]: "list_all2 (rel_prod rel_ll_rule (=)) Rdp_A rdp_A" unfolding rdp_A_def Rdp_A_def by transfer_prover
define Ren_as where "Ren_as = ren.rename_list ren (map (λ(α, p). Lhs α) Rdp_A)"
define ren_as where "ren_as = ren.rename_list ren (map (λ(α, p). lhs α) rdp_A)"
define l where "l = (ctxt_of_pos_term q (hd ren_as))⟨map_vars_term (rename_single ren) (lhs rule')⟩"
have Ren_as: "Ren_as = ren_as" unfolding Ren_as_def ren_as_def by transfer_prover
have Lhs_rule': "Lhs Rule' = lhs rule'" by transfer_prover
have snd: "map snd Rdp_A = map snd rdp_A" by transfer_prover
have len: "length Rdp_A = length rdp_A" by transfer_prover
let ?mgu = "mgu_list (map2 (λx y. (x, l |_ y)) ren_as (map snd rdp_A))"
show ?thesis
unfolding sim_cp_non_root_of_def Sim_cp_non_root_of_def
unfolding rdp_A_def[symmetric] Rdp_A_def[symmetric] Let_def[of rdp_A] Let_def[of Rdp_A]
unfolding ren_as_def[symmetric] Ren_as_def[symmetric] Let_def[of Ren_as] Let_def[of ren_as] Ren_as
unfolding Lhs_rule' l_def[symmetric] Let_def[of l]
unfolding snd len
proof (goal_cases)
case 1
show ?case
proof (cases ?mgu)
case None
show ?thesis unfolding None option.simps by transfer_prover
next
case mgu: (Some τ)
obtain xs where xs: "[0..<length ((rule, []) # rdp)] = 0 # xs"
using upt_conv_Cons by fastforce
have hd_ren: "hd ren_as = map_vars_term (rename_many' ren 0) (lhs rule)"
unfolding ren_as_def rdp_A_def ren.rename_list_def length_map xs by simp
from q have hole_q: "hole_pos (ctxt_of_pos_term q (hd ren_as)) = q"
unfolding hd_ren by auto
from q have q: "q ∈ poss l" unfolding l_def hd_ren
by (simp add: replace_at_below_poss)
define Asi where "Asi i αi pi = (ctxt_of_pos_term pi
(to_Pterm
(l ⋅ τ)))⟨Fun (Inl αi)
(map (to_Pterm ∘ τ ∘ rename_many' ren i)
(Var_rule_list αi))⟩" for i αi pi
define As where "As = map (λi. (case Rdp_A ! i of (αi, pi) ⇒ λi. Asi i αi pi) i) [0..<length rdp_A]"
define asi where "asi i αi pi = (ctxt_of_pos_term pi
(to_pterm
(l ⋅ τ)))⟨Prule αi
(map (to_pterm ∘ τ ∘ rename_many' ren i)
(vars_term_list (lhs αi)))⟩" for i αi pi
define as where "as = map (λi. (case rdp_A ! i of (αi, pi) ⇒ λi. asi i αi pi) i) [0..<length rdp_A]"
have [transfer_rule]: "list_all2 rel_Pterm As as"
unfolding As_def as_def
proof (rule list_all2_map_map)
fix i
assume "i ∈ set [0..<length rdp_A]"
hence i: "i < length rdp_A" by auto
with Rdp_A have rel_prod: "rel_prod rel_ll_rule (=) (Rdp_A ! i) (rdp_A ! i)" unfolding list_all2_conv_all_nth by auto
then obtain Rp rp p where Rp[transfer_rule]: "rel_ll_rule Rp rp" and rdpi: "Rdp_A ! i = (Rp,p)" "rdp_A ! i = (rp,p)"
by (metis (full_types) prod.collapse rel_prod_inject)
show "rel_Pterm ((case Rdp_A ! i of (αi, pi) ⇒ λi. Asi i αi pi) i) ((case rdp_A ! i of (αi, pi) ⇒ λ i. asi i αi pi) i)"
unfolding rdpi split
proof -
have vars: "Var_rule_list Rp = vars_term_list (lhs rp)"
using rel_funD[OF Var_rule_list_term_list Rp] .
from i have "snd (rdp_A ! i) ∈ snd ` set rdp_A" by auto
with rdpi have p: "p ∈ snd ` set rdp_A" by auto
have p: "p ∈ poss l"
proof (cases "p = []")
case False
with p have "p ∈ snd ` set rdp" unfolding rdp_A_def by auto
with assms obtain q' where p: "p = q @ q'" and q': "q' ∈ poss (lhs rule')"
by auto
show ?thesis unfolding l_def p
unfolding hole_pos_poss_conv[where C = "ctxt_of_pos_term q (hd ren_as)", unfolded hole_q]
using q' by auto
qed auto
show "rel_Pterm (Asi i Rp p) (asi i rp p)" unfolding asi_def Asi_def vars
by (rule rel_Pterm_replace_at_to_pterm, transfer_prover, insert p, auto)
qed
qed
show ?thesis unfolding mgu option.simps map2_to_map
unfolding len[symmetric] map2_to_map
unfolding len
unfolding Asi_def[symmetric] asi_def[symmetric]
unfolding As_def[symmetric] as_def[symmetric] Let_def[of As] Let_def[of as]
proof goal_cases
case 1
have "rel_option rel_Pterm (Join_list As) (join_list as)" by transfer_prover
thus ?case
proof cases
case None
show ?thesis unfolding None option.simps by transfer_prover
next
case (Some A a)
note [transfer_rule] = Some(3)
have vars': "Var_rule_list Rule' = vars_term_list (lhs rule')"
using rel_funD[OF Var_rule_list_term_list rule'] .
define B where "B = (ctxt_of_pos_term q
(to_Pterm
(l ⋅ τ)))⟨Fun (Inl Rule')
(map (to_Pterm ∘ τ ∘ rename_single ren) (vars_term_list (lhs rule')))⟩"
define b where "b = (ctxt_of_pos_term q
(to_pterm
(l ⋅ τ)))⟨Prule rule'
(map (to_pterm ∘ τ ∘ rename_single ren) (vars_term_list (lhs rule')))⟩"
have [transfer_rule]: "rel_Pterm B b"
unfolding B_def b_def
by (rule rel_Pterm_replace_at_to_pterm, transfer_prover, insert q, auto)
show ?thesis unfolding Some option.simps vars' B_def[symmetric] b_def[symmetric] by transfer_prover
qed
qed
qed
qed
qed
lemma Non_root_sim_cps: fixes Rule :: "('a,'b :: infinite) ll_rule"
assumes rules[transfer_rule]: "list_all2 rel_ll_rule' Rules rules"
and rule [transfer_rule]: "rel_ll_rule Rule rule"
and rule' [transfer_rule]: "rel_ll_rule Rule' rule'"
and q: "q ∈ poss (lhs rule)"
shows "list_all2 (rel_prod rel_Pterm rel_Pterm) (Non_root_sim_cps ren Rules Rule q Rule')
(non_root_sim_cps ren rules rule q rule')"
proof -
define Rdps where "Rdps = Non_root_rdps ren Rules Rule q (Lhs Rule')"
define rdps where "rdps = non_root_rdps ren rules rule q (lhs rule')"
have rdps[transfer_rule]: "list_all2 (list_all2 (rel_prod rel_ll_rule (=))) Rdps rdps"
unfolding Rdps_def rdps_def by transfer_prover
have len: "length Rdps = length rdps" by transfer_prover
show ?thesis
unfolding non_root_sim_cps_def Non_root_sim_cps_def List.maps_eq Rdps_def[symmetric] rdps_def[symmetric]
proof (rule rel_funD[OF concat_transfer], rule list_all2_all_nthI, unfold length_map len, force, simp add: len)
fix i
assume i: "i < length rdps"
with rdps have rdpsi: "list_all2 (rel_prod rel_ll_rule (=)) (Rdps ! i) (rdps ! i)"
unfolding list_all2_conv_all_nth by auto
from i have mem: "rdps ! i ∈ set (non_root_rdps ren rules rule q (lhs rule'))"
unfolding rdps_def by auto
show "list_all2 (rel_prod rel_Pterm rel_Pterm) (Sim_cp_non_root_of ren Rule q Rule' (Rdps ! i))
(sim_cp_non_root_of ren rule q rule' (rdps ! i))"
proof (rule Sim_cp_non_root_of[OF rule rule' rdpsi q], rule ccontr)
assume "¬ (snd ` set (rdps ! i) ⊆ (@) q ` poss (lhs rule'))"
then obtain r p where rp: "(r,p) ∈ set (rdps ! i)" and p: "p ∉ (@) q ` poss (lhs rule')"
by force
define ps where "ps = var_poss_list (lhs rule)"
from mem[unfolded non_root_rdps_def, simplified, folded ps_def] rp obtain as
where lenas: "length as = length ps"
and asj: "⋀ j. j < length ps ⟹ as ! j
∈ set (if q ≤⇩p ps ! j ∧ ps ! j -⇩p q ∈ fun_poss (lhs rule')
then map (map (map_prod id ((@) (ps ! j))))
(compute_rp ren rules (lhs rule' |_ (ps ! j -⇩p q)))
else [[]])"
and rdpsi: "rdps ! i = concat as" by auto
from rp[unfolded rdpsi] obtain j where j: "j < length ps" and rp: "(r,p) ∈ set (as ! j)"
using lenas by (auto simp: set_conv_nth[of as])
let ?map = "map (map_prod id ((@) (ps ! j)))"
define crdp where "crdp = compute_rp ren rules (lhs rule' |_ (ps ! j -⇩p q))"
from asj[OF j] rp have cond: "q ≤⇩p ps ! j" "ps ! j -⇩p q ∈ fun_poss (lhs rule')"
and asj_mem: "as ! j ∈ set (map ?map crdp)"
by (auto split: if_splits simp: crdp_def)
from asj_mem obtain rdp where rdp: "rdp ∈ set crdp"
and asj: "as ! j = ?map rdp" by auto
from positions_compute_rp[of ren rules "(lhs rule' |_ (ps ! j -⇩p q))", folded crdp_def]
have pos_crdp: "snd ` ⋃ (set ` set crdp) ⊆ poss (lhs rule' |_ (ps ! j -⇩p q))" by auto
from rp[unfolded asj] obtain p' where rp': "(r,p') ∈ set rdp" and pp': "p = ps ! j @ p'" by force
from rp' rdp pos_crdp have p': "p' ∈ poss (lhs rule' |_ (ps ! j -⇩p q))" by fastforce
from p p' cond q show False unfolding pp'
by (metis append.assoc fun_poss_imp_poss image_eqI pos_append_poss prefix_pos_diff)
qed
qed
qed
lemma Sim_cp_non_root_impl[transfer_rule]: "((=) ===> list_all2 rel_ll_rule' ===> list_all2 rel_ll_rule' ===> list_all2 (rel_prod rel_Pterm rel_Pterm))
Sim_cp_non_root_impl sim_cp_non_root_impl"
proof (intro rel_funI, clarify, goal_cases)
case (1 ren' ren Rules rules Srules srules)
have rules[transfer_rule]: "list_all2 rel_ll_rule' Rules rules" by fact
have srules[transfer_rule]: "list_all2 rel_ll_rule' Srules srules" by fact
show ?case unfolding Sim_cp_non_root_impl_def sim_cp_non_root_impl_def Let_def
List.maps_eq[of _ Rules] List.maps_eq[of _ rules]
apply (rule rel_funD[OF concat_transfer])
apply (rule rel_funD[OF rel_funD[OF list.map_transfer] rules])
apply (rule rel_funI)
proof goal_cases
case (1 R1 r1)
obtain lf rf where r1: "r1 = (lf,rf)" by force
with 1 have "rel_ll_rule' R1 (lf,rf)" by auto
hence R1[transfer_rule]: "rel_ll_rule R1 (Rule lf rf)" by transfer auto
have LR1: "Lhs R1 = lhs (Rule lf rf)" by transfer_prover
define qs where "qs = (filter ((≠) []) (fun_poss_list lf))"
show ?case unfolding r1 split prule.sel LR1
unfolding qs_def[symmetric]
unfolding List.maps_eq[of _ qs]
apply (rule rel_funD[OF concat_transfer])
apply (rule list_all2_all_nthI, force, unfold length_map)
proof goal_cases
case (1 i)
have i: "i < length qs" by fact
hence "qs ! i ∈ set qs" by auto
hence qsi: "qs ! i ∈ poss (lhs (lf → rf))" unfolding arg_cong[OF qs_def, of set]
by (auto intro: fun_poss_imp_poss)
define Fs where "Fs = (filter (λβ. unify_vd ren [(Lhs β, lf |_ qs ! i)]) Srules)"
define fs where "fs = filter (λ(ll, rr). unify_vd ren [(ll, lf |_ qs ! i)]) srules"
have fs': "fs = filter (λ rl. unify_vd ren [(fst rl, lf |_ qs ! i)]) srules"
unfolding fs_def by (induct srules, auto)
have Fs[transfer_rule]: "list_all2 rel_ll_rule' Fs fs"
unfolding fs' Fs_def
by transfer_prover
have len: "length Fs = length fs" by transfer_prover
have "list_all2 (list_all2 (rel_prod rel_Pterm rel_Pterm))
(map (Non_root_sim_cps ren Rules R1 (qs ! i)) Fs)
(map (λ(ll, rr). non_root_sim_cps ren rules (lf → rf) (qs ! i) (ll → rr)) fs)"
proof (rule list_all2_all_nthI, unfold length_map, rule len, goal_cases)
case (1 j)
hence j: "j < length fs" using len by auto
obtain ll rr where fsj: "fs ! j = (ll,rr)" by force
from Fs j have "rel_ll_rule' (Fs ! j) (fs ! j)" unfolding list_all2_conv_all_nth by auto
from rel_funD[OF rel_ll_rule'_to_rel_ll_rule this[unfolded fsj]]
have Fsj: "rel_ll_rule (Fs ! j) (Rule ll rr)" by simp
have "list_all2 (rel_prod rel_Pterm rel_Pterm) (Non_root_sim_cps ren Rules R1 (qs ! i) (Fs ! j))
(non_root_sim_cps ren rules (Rule lf rf) (qs ! i) (Rule ll rr))"
by (rule Non_root_sim_cps[OF rules R1 Fsj qsi])
thus ?case using j 1 fsj by simp
qed
thus ?case using i
apply simp
apply (rule rel_funD[OF concat_transfer])
by (auto simp: Fs_def fs_def)
qed
qed
qed
lemma Sim_cp_impl[transfer_rule]: "((=) ===> list_all2 rel_ll_rule' ===> list_all2 rel_ll_rule' ===> list_all2 (rel_prod rel_Pterm rel_Pterm))
Sim_cp_impl sim_cp_impl"
unfolding Sim_cp_impl_def sim_cp_impl_def by transfer_prover
lemma Sim_cps_impl[transfer_rule]: "((=) ===> list_all2 rel_ll_rule' ===> list_all2 rel_ll_rule' ===> (=))
Sim_cps_impl sim_cps_impl"
unfolding Sim_cps_impl_def sim_cps_impl_def by transfer_prover
end
definition to_ll_rule_intern where
"to_ll_rule_intern rule = (let xs = vars_term_list (fst rule) in
do
{check (is_Fun (fst rule))
(STR ''variable left-hand side in rule'');
check (linear_term (fst rule))
(STR ''left-hand side is not linear '');
check_subseteq (vars_term_impl (snd rule)) xs
<+? (λ _. (STR ''free variable in right-hand side''));
return (fst rule, snd rule, var_poss_list (fst rule), xs)})"
lemma isOK_to_ll_rule_intern: "isOK (to_ll_rule_intern rule) =
(is_Fun (fst rule) ∧ linear_term (fst rule) ∧ vars_term (snd rule) ⊆ vars_term (fst rule))"
unfolding to_ll_rule_intern_def Let_def
by auto
lemma to_ll_rule_intern: assumes "to_ll_rule_intern rule = return (l,r,ps,xs)"
shows "is_Fun (fst rule) ∧ linear_term (fst rule) ∧ vars_term (snd rule) ⊆ vars_term (fst rule) ∧
(l,r) = rule ∧ ps = var_poss_list l ∧ xs = vars_term_list l"
using assms unfolding to_ll_rule_intern_def Let_def
by (cases rule, auto)
lift_definition (code_dt) to_ll_rule_lift :: "('f :: showl,'v :: showl)rule ⇒ String.literal + ('f,'v)ll_rule"
is to_ll_rule_intern
proof goal_cases
case (1 rule)
show ?case
proof (cases "to_ll_rule_intern rule")
case (Inl err)
show ?thesis unfolding Inl by auto
next
case (Inr tuple)
obtain l r ps xs where tuple: "tuple = (l,r,ps,xs)" by (cases tuple, auto)
from to_ll_rule_intern[OF Inr[unfolded tuple]]
show ?thesis unfolding Inr tuple by auto
qed
qed
lemma to_ll_rule_lift_return: assumes "to_ll_rule_lift lr = return Lr"
shows "rel_ll_rule' Lr lr"
using assms
proof (transfer, goal_cases)
case (1 lr Lr)
obtain l r ps xs where Lr: "Lr = (l,r,ps,xs)" by (cases Lr, auto)
from to_ll_rule_intern[OF 1(2)[unfolded Lr]] 1(1) show ?case
unfolding Lr
by (cases lr, auto)
qed
lemma isOK_to_ll_rule_lift: "isOK(to_ll_rule_lift rule) =
(is_Fun (fst rule) ∧ linear_term (fst rule) ∧ vars_term (snd rule) ⊆ vars_term (fst rule))"
unfolding isOK_to_ll_rule_intern[of rule, symmetric]
by (metis isOK_iff map_sum.simps(2) to_ll_rule_lift.abs_eq
to_ll_rule_lift.rep_eq)
definition "to_ll_rule rule = (to_ll_rule_lift rule
<+? (λ e. showsl_lit (STR ''rule '') o showsl_rule rule o
showsl_lit (STR '' is not a well-formed left-linear rule⏎'') o showsl_lit e))"
lemma to_ll_rule: assumes "to_ll_rule lr = return Lr"
shows "rel_ll_rule' Lr lr"
using assms to_ll_rule_lift_return[of lr Lr] unfolding to_ll_rule_def
by auto
lemma isOK_to_ll_rule[simp]: "isOK(to_ll_rule rule) =
(is_Fun (fst rule) ∧ linear_term (fst rule) ∧ vars_term (snd rule) ⊆ vars_term (fst rule))"
unfolding to_ll_rule_def
by (auto simp: isOK_to_ll_rule_lift)
definition "to_ll_rules = mapM to_ll_rule"
lemma isOK_mapM_simp[simp]: "isOK(mapM f xs) = (∀ x ∈ set xs. isOK (f x))"
by (induct xs, auto)
lemma is_OK_to_ll_rules[simp]: "isOK(to_ll_rules rules) = (left_lin_wf_trs (set rules))"
unfolding to_ll_rules_def
by (force simp: left_lin_wf_trs_def left_lin_def
left_linear_trs_def wf_trs_def no_var_lhs_def var_rhs_subset_lhs_def)
lemma to_ll_rules_return: assumes "to_ll_rules rules = return Rules"
shows "list_all2 rel_ll_rule' Rules rules"
proof -
from assms have "isOK (to_ll_rules rules)" by auto
from isOK_mapM[OF this[unfolded to_ll_rules_def], folded to_ll_rules_def, unfolded assms]
have "⋀ x. x ∈ set rules ⟹ isOK (to_ll_rule x)"
and "Rules = map (λx. projr (to_ll_rule x)) rules" by auto
thus ?thesis using to_ll_rule
by (metis (mono_tags, lifting) isOK_iff list.rel_map(1) list_all2_same
sum.sel(2))
qed
lemma sim_cp_closed_via_Sim_cps_impl: "sim_cp_closed ren (set rules) = (∃ Rules.
to_ll_rules rules = return Rules ∧ (∀ cp ∈ set (Sim_cps_impl ren Rules Rules).
fst cp = snd cp ∨
(∃ l r v. instance_rule cp (l,r) ∧ (l, v) ∈ (rstep (set rules))⇧* ∧ (r, v) ∈ mstep (set rules))))"
proof (cases "left_lin_wf_trs (set rules)")
case False
thus ?thesis using is_OK_to_ll_rules[of rules]
by (cases "to_ll_rules rules", auto simp: sim_cp_closed_def)
next
case True
then obtain Rules where ret: "to_ll_rules rules = return Rules"
using is_OK_to_ll_rules[of rules]
by (cases "to_ll_rules rules", auto)
from to_ll_rules_return[OF this] have [transfer_rule]: "list_all2 rel_ll_rule' Rules rules" by auto
have Sim: "Sim_cps_impl ren Rules Rules = sim_cps_impl ren rules rules" by transfer_prover
show ?thesis unfolding ret unfolding sim_cps_impl Sim[symmetric] using True
by auto
qed
definition "check_sim_cps_equiv = False"
fun check_sim_cps_closed_joins where
"check_sim_cps_closed_joins R S scps (CP_Auto n) = do {
check_allm (λ (s, t). do {
check (is_mstep_join R S (if n = 0 then None else Some n) t s)
(showsl_lit (STR ''the simultaneous critical pair '') ∘ showsl s ∘ showsl_lit (STR '' <-o- . -> '') ∘ showsl t ∘
showsl_lit (STR '' is not almost closed within '') ∘ (if n = 0 then showsl_lit (STR '' one multistep'') else showsl n ∘ showsl_lit (STR '' steps.'')))
}) scps
} <+? (λs. s ∘ showsl_lit (STR ''⏎hence the it could not shown that the sim.-crit pairs are closed⏎''))"
| "check_sim_cps_closed_joins R S scps (CP_Sequences cps) = do {
check_allm (λ scp. check (fst scp = snd scp ∨ (∃ cp ∈ set cps. instance_rule scp (cp_left cp, cp_right cp)))
(showsl_lit (STR ''could not find critical pair '') o showsl scp))
scps;
check_allm (λ scp. check (check_sim_cps_equiv ⟶ fst scp ≠ snd scp ⟶ (∃ cp ∈ set scps. instance_rule scp cp))
(showsl_lit (STR ''pair '') o showsl scp o showsl_lit (STR '' is not a simultaneous critical pair'')))
(map (λ cp. (cp_left cp, cp_right cp)) cps);
check_allm (λ cp. check_single_rsteps_join_sequence_gen (λ s t. (s,t) ∈ mstep (set R)) (STR '''') S (STR '''') (cp_right cp) (cp_left cp) (rev (cp_join cp))
<+? (λ s. showsl_lit (STR ''problem with sim. crit pair '') o showsl (cp_left cp) o
showsl_lit (STR '' <-o- . -> '') o showsl (cp_right cp) o showsl_nl o s)) cps
}"
lemma check_sim_cps_closed_joins: assumes ok: "isOK(check_sim_cps_closed_joins R S scps hints)"
and st: "(s,t) ∈ set scps"
shows "∃ l r v. instance_rule (s,t) (l,r) ∧ (l,v) ∈ (rstep (set S))^* ∧ (r,v) ∈ mstep (set R)"
proof (cases hints)
case (CP_Auto n)
from ok[unfolded CP_Auto] st obtain c where
"is_mstep_join R S c t s" by auto
from is_mstep_join[OF this] show ?thesis using instance_rule_refl[of "(s,t)"] by blast
next
case (CP_Sequences c)
show ?thesis
proof (cases "s = t")
case False
from ok[unfolded CP_Sequences, simplified] st False
obtain cp d R' S' where inst: "instance_rule (s,t) (cp_left cp, cp_right cp)"
and ok: "isOK
(check_single_rsteps_join_sequence_gen (λs t. (s, t) ∈ mstep (set R)) R' S S'
(cp_right cp) (cp_left cp) d)" by fastforce
from check_single_rsteps_join_sequence_gen[OF _ ok] obtain v
where "(cp_right cp, v) ∈ mstep (set R)" "(cp_left cp, v) ∈ (rstep (set S))⇧*" by auto
thus ?thesis using inst by blast
next
case True
show ?thesis unfolding True by (intro exI[of _ t], auto)
qed
qed
definition "check_sim_cps_closed ren R infos = do {
rules <- to_ll_rules R;
check_sim_cps_closed_joins R R (Sim_cps_impl ren rules rules) infos
} <+? (λ s. showsl_lit (STR ''problem checking Okui's simultenous critical pair condition⏎'') o s)"
lemma check_sim_cps_closed:
assumes "isOK(check_sim_cps_closed ren R info)"
shows "CR (rstep (set R))"
proof -
from assms obtain Rules where ret: "to_ll_rules R = return Rules"
unfolding check_sim_cps_closed_def by (cases "to_ll_rules R", auto)
let ?SCP = "Sim_cps_impl ren Rules Rules"
from assms[unfolded check_sim_cps_closed_def ret]
have "isOK (check_sim_cps_closed_joins R R ?SCP info)"
by simp
note check = check_sim_cps_closed_joins[OF this]
show ?thesis
proof (intro sim_cp_closed[of ren], unfold sim_cp_closed_via_Sim_cps_impl,
intro exI conjI ballI, rule ret)
fix cp
assume mem: "cp ∈ set ?SCP"
obtain s t where cp: "cp = (s,t)" by force
show "fst cp = snd cp ∨ (∃l r v. instance_rule cp (l, r) ∧ (l, v) ∈ (rstep (set R))⇧* ∧ (r, v) ∈ mstep (set R))"
using check[of s t] unfolding cp[symmetric] using mem by blast
qed
qed
definition "check_sim_cps_closed_comm ren R S infos = do {
rules <- to_ll_rules R;
srules <- to_ll_rules S;
check_sim_cps_closed_joins R S (Sim_cps_impl ren rules srules) infos
} <+? (λ s. showsl_lit (STR ''problem checking Okui's simultenous critical pair condition⏎'') o s)"
lemma check_sim_cps_closed_comm:
assumes "isOK(check_sim_cps_closed_comm ren R S info)"
shows "commute (rstep (set R)) (rstep (set S))"
proof -
from assms obtain Rules Srules where ret: "to_ll_rules R = return Rules" "to_ll_rules S = return Srules"
unfolding check_sim_cps_closed_comm_def by (cases "to_ll_rules R"; cases "to_ll_rules S"; auto)
let ?SCP = "Sim_cps_impl ren Rules Srules"
from assms[unfolded check_sim_cps_closed_comm_def ret]
have "isOK (check_sim_cps_closed_joins R S ?SCP info)"
by simp
note check = check_sim_cps_closed_joins[OF this]
from is_OK_to_ll_rules[of R] ret have R: "left_lin_wf_trs (set R)" by auto
from is_OK_to_ll_rules[of S] ret have S: "left_lin_wf_trs (set S)" by auto
show ?thesis
proof (intro okui_imp_commute[OF R S, of ren])
fix A B
assume "(A,B) ∈ ren.sim_cp ren (set R) (set S)"
hence "(A,B) ∈ set (sim_cp_impl ren R S)"
by (metis R S ren_wf_trs.intro ren_wf_trs.sim_cp_impl)
hence "(target A, target B) ∈ set (sim_cps_impl ren R S)"
unfolding sim_cps_impl_def by auto
also have "sim_cps_impl ren R S = ?SCP"
using to_ll_rules_return[OF ret(1)] to_ll_rules_return[OF ret(2)] Sim_cps_impl
unfolding rel_fun_def by metis
finally have "(target A, target B) ∈ set ?SCP" by auto
from check[OF this] obtain l r v where
inst: "instance_rule (target A, target B) (l, r)" and
lv: "(l, v) ∈ (rstep (set S))⇧*" and rv: "(r, v) ∈ mstep (set R)"
by auto
from inst[unfolded instance_rule_def] obtain σ where
tgt: "target A = l ⋅ σ" "target B = r ⋅ σ" by auto
from lv have lvs: "(l ⋅ σ, v ⋅ σ) ∈ (rstep (set S))⇧*"
by (metis rsteps_closed_subst)
from rv have rvs: "(r ⋅ σ, v ⋅ σ) ∈ mstep (set R)" by (rule mstep_subst)
show "∃v. (target A, v) ∈ (rstep (set S))⇧* ∧ (target B, v) ∈ mstep (set R)"
unfolding tgt using lvs rvs by blast
qed
qed
end