section ‹Persistent decomposition and check functions›
theory LS_Persistence_Impl
imports LS_Persistence
LS_Modularity
QTRS.Position
QTRS.Trs_Impl
"Transitive-Closure.Transitive_Closure_List_Impl"
begin
subsection ‹Misc›
instance prod :: (infinite, type) infinite
by standard (simp add: infinite_UNIV finite_prod)
lemma isOK_try_catch:
"isOK (try a catch b) ⟷ isOK a ∨ (∃e. a = Inl e ∧ isOK (b e))"
by (cases a) (auto)
lemma litsim_empty_empty [simp]:
"R ≐ {} ⟷ R = {}" "{} ≐ R ⟷ R = {}"
by (auto simp: subsumable_trs.litsim_def)
lemma is_Var_permute [simp]: "is_Var (p ∙ t) ⟷ is_Var t"
by (cases t) auto
lemma vars_term_permute [simp]: "vars_term (p ∙ t) = p ∙ vars_term t"
by (induct t) (auto simp: atom_set_pt.insert_eqvt atom_set_pt.inv_mem_simps(1)[symmetric] simp del: atom_set_pt.inv_mem_simps)
lemma wf_trs_permute_imp:
"wf_trs R ⟹ wf_trs (p ∙ R)"
by (auto 0 3 simp: wf_trs_def' trs_pt.permute_set_def rule_pt.permute_prod_eqvt split: prod.splits)
(insert atom_set_pt.inv_mem_simps(1), blast)
lemma wf_trs_permute [simp]:
"wf_trs (p ∙ R) ⟷ wf_trs R"
using wf_trs_permute_imp[of R p] wf_trs_permute_imp[of "p ∙ R" "-p"] by auto
lemma permute_term_by_var_subst [simp]:
"t ⋅ (λx. Var (π ∙ x)) = π ∙ t"
by (induct t) auto
lemma rstep'_permute_sub:
"rstep' (π ∙ R) ⊆ rstep' R"
proof (intro subrelI, unfold rstep'_iff_rstep_r_p_s', elim exE, goal_cases)
case (1 s t l r p σ) then show ?case
using rstep_r_p_s'I[of "-π ∙ (l, r)" R p _ s "(λx. π ∙ Var x) ∘⇩s _" t]
by (auto elim!: rstep_r_p_s'E simp: rule_pt.permute_prod_eqvt) blast
qed
lemma rstep'_permute [simp]:
"rstep' (p ∙ R) = rstep' R"
using rstep'_permute_sub[of p R] rstep'_permute_sub[of "-p" "p ∙ R"] by auto
lemma CR_on_iff_CR:
assumes "wf_trs (ℛ :: ('f, 'v :: infinite) trs)" "funas_trs ℛ ⊆ ℱ"
shows "CR_on (rstep ℛ) { t :: ('f, 'v) term. funas_term t ⊆ ℱ } ⟷ CR (rstep ℛ)"
using assms by (auto simp: CR_on_imp_CR) (auto simp: CR_on_def)
lemma isOK_mapM:
assumes "isOK (mapM f xs)"
shows "(∀x. x ∈ set xs ⟶ isOK (f x)) ∧ run (mapM f xs) = map (λx. run (f x)) xs"
using assms mapM_return[of f xs] by (force simp: isOK_def split: sum.splits)+
lemma rstep'_mono_subsumeseq_trs:
fixes R S :: "('f, 'v :: infinite) trs"
assumes "R ≤⋅ S" shows "rstep' R ⊆ rstep' S"
using assms by (auto simp: subsumeseq_trs_def elim!: rstep'.cases)
(metis rstep'.rstep' rstep'_permute trs_pt.inv_mem_simps(2))
lemma rstep'_eq_litsim_trs:
fixes R S :: "('f, 'v :: infinite) trs"
shows "R ≐ S ⟹ rstep' R = rstep' S"
using rstep'_mono_subsumeseq_trs by (auto simp: subsumable_trs.litsim_def)
lemma wf_trs_mono_subsumeseq_trs:
fixes R S :: "('f, 'v :: infinite) trs"
assumes "R ≤⋅ S" shows "wf_trs S ⟹ wf_trs R"
using assms by (meson subsumeseq_trsE trs_pt.inv_mem_simps(2) wf_trs_def' wf_trs_permute)
lemma wf_trs_lit_sim_trs:
fixes R S :: "('f, 'v :: infinite) trs"
shows "R ≐ S ⟹ wf_trs R ⟷ wf_trs S"
by (auto simp: wf_trs_mono_subsumeseq_trs subsumable_trs.litsim_def)
lemma CR_change_variables:
shows "wf_trs R ⟹ CR (rstep' R :: ('f, 'v :: infinite) trs) ⟹ CR (rstep' R :: ('f, 'w :: infinite) trs)"
proof (standard, goal_cases)
case (1 s t u)
obtain f :: "'w ⇒ 'v" where f: "inj_on f (vars_term s)"
by (metis finite_into_infinite infinite_UNIV finite_vars_term)
let ?g = "inv_into (vars_term s) f"
obtain v where v: "(t ⋅ (Var ∘ f), v) ∈ (rstep' R)⇧*" "(u ⋅ (Var ∘ f), v) ∈ (rstep' R)⇧*"
using CR_onD[OF 1(2) _ rsteps'_stable[OF 1(4)] rsteps'_stable[OF 1(5)], of "Var ∘ f"] by auto
have "vars_term t ⊆ vars_term s" "vars_term u ⊆ vars_term s" using 1(1,4,5) rstep'_sub_vars by metis+
moreover then have "t ⋅ (Var ∘ f) ⋅ (Var ∘ ?g) = t" "u ⋅ (Var ∘ f) ⋅ (Var ∘ ?g) = u"
using f by (auto simp del: subst_subst_compose simp: subst_subst_compose[symmetric]
subst_compose_def term_subst_eq_conv[of _ _ Var, unfolded subst_apply_term_empty])
ultimately show ?case using v by (auto dest!: rsteps'_stable[of _ _ _ "Var ∘ ?g"])
qed
lemma CR_change_variables_iff:
"wf_trs R ⟹ CR (rstep' R :: ('f, 'v :: infinite) trs) ⟷ CR (rstep' R :: ('f, 'w :: infinite) trs)"
by (auto simp: CR_change_variables)
lemma CR_change_variables_iff':
"wf_trs (R :: ('f, 'v :: infinite) trs) ⟹ CR (rstep' R :: ('f, 'w :: infinite) trs) ⟷ CR (rstep R)"
by (simp add: CR_change_variables_iff rstep_eq_rstep')
subsection ‹Executable version of @{const many_sorted_terms.𝒯⇩α}›
fun 𝒯⇩α_code :: "(('f × nat) ⇒ ('t list × 't) option) ⇒ ('v ⇒ 't option) ⇒ 't ⇒ ('f, 'v) term ⇒ bool" where
"𝒯⇩α_code sigF sigV α (Var x) ⟷ sigV x = Some α"
| "𝒯⇩α_code sigF sigV α (Fun f ts) ⟷
case_option False (λ(tys, α'). α = α' ∧ list_all (case_prod (𝒯⇩α_code sigF sigV)) (zip tys ts)) (sigF (f, length ts))"
lemma (in many_sorted_terms) 𝒯⇩α_code:
"𝒯⇩α α t ⟷ 𝒯⇩α_code sigF sigV α t"
proof (induct t arbitrary: α)
case (Fun f ts) then show ?case
using Fun[OF nth_mem] arity by (auto simp: list_all_length split: option.split elim: 𝒯⇩α.cases)
qed (auto elim: 𝒯⇩α.cases)
subsection ‹Make signature from list›
fun mk_sigF :: "('f × ('t list × 't)) list ⇒ ('f × nat) ⇒ ('t list × 't) option" where
"mk_sigF sig (f, a) = map_option snd (find (λ(f', tys, t). f = f' ∧ a = length tys) sig)"
lemma many_sorted_terms_mk_sigF [simp]:
"many_sorted_terms (mk_sigF sig)"
by (unfold_locales) (auto simp: find_Some_iff)
lemma 𝒯⇩α_code:
"𝒯⇩α_code (mk_sigF sig) sigV = many_sorted_terms.𝒯⇩α (mk_sigF sig) sigV"
proof -
interpret many_sorted_terms "mk_sigF sig" sigV by simp
show ?thesis by (force simp: 𝒯⇩α_code)
qed
subsection ‹Executable version of needed_types›
context many_sorted_terms
begin
definition sigF_arcs where
"sigF_arcs = {(α, β) |f n tys α β. sigF (f, n) = Some (tys, α) ∧ β ∈ set tys}"
lemma needed_types_by_sigF_arcs:
"needed_types α β ⟷ (α, β) ∈ sigF_arcs⇧*" (is "?L ⟷ ?R")
proof
assume ?L then show ?R by (induct) (force simp: sigF_arcs_def)+
next
assume ?R then show ?L by (induct) (auto simp: sigF_arcs_def)
qed
end
context
fixes sig :: "('f :: show × 't list × 't :: show) list"
begin
interpretation many_sorted_terms "mk_sigF sig" "Some ∘ snd" by simp
definition sig_is_clean where
"sig_is_clean = distinct (map (λ(f, tys, _). (f, length tys)) sig)"
definition sigF_arcs_code where
"sigF_arcs_code = concat (map (λ(_, tys, ty). map (λty'. (ty, ty')) tys) sig)"
lemma find_distinct:
assumes "distinct (map f xs)"
shows "find (λx. z = f x) xs = Some x ⟷ z = f x ∧ x ∈ set xs"
"find (λx. z = f x) xs = None ⟷ z ∉ f ` set xs"
using assms by (induct xs) auto
lemma sigF_arcs_code:
assumes "sig_is_clean"
shows "set (sigF_arcs_code) = many_sorted_terms.sigF_arcs (mk_sigF sig)"
using find_distinct(1)[OF assms[unfolded sig_is_clean_def]]
by (simp add: sigF_arcs_code_def many_sorted_terms.sigF_arcs_def split_beta split_beta' image_def)
fastforce
definition needed_types_code where
"needed_types_code = memo_list_rtrancl sigF_arcs_code"
lemma needed_types_code:
"sig_is_clean ⟹ set (needed_types_code α) = {β. many_sorted_terms.needed_types (mk_sigF sig) α β}"
by (auto simp: needed_types_code_def memo_list_rtrancl many_sorted_terms.needed_types_by_sigF_arcs sigF_arcs_code)
fun annotate_term where
"annotate_term sigF α (Var x) = return (Var (x, α))"
| "annotate_term sigF α (Fun f ts) = (case sigF (f, length ts) of
None ⇒ error (shows ''persistent decomposition: no signature for symbol '' ∘ shows f)
| Some (tys, ty) ⇒ if α ≠ ty then error (shows ''persistent decomposition: '' ∘ shows f
∘ shows '' has wrong type in '' ∘ shows (Fun f ts))
else do { ts' <- mapM (λ(β, t). annotate_term sigF β t) (zip tys ts); return (Fun f ts') })"
lemma isOK_annotate_term:
"isOK (annotate_term (mk_sigF sig) α t) ⟹ 𝒯⇩α α (run (annotate_term (mk_sigF sig) α t))"
oops
end
lemma isOK_annotate_term:
"isOK (annotate_term (mk_sigF sig) α t) ⟹ many_sorted_terms.𝒯⇩α (mk_sigF sig) (Some ∘ snd) α (run (annotate_term (mk_sigF sig) α t))"
proof (induct t arbitrary: α)
case (Fun f ts)
show ?case using Fun(1)[OF nth_mem] Fun(2)
by (auto simp del: mk_sigF.simps split: prod.splits sum.splits option.splits if_splits dest!: mapM_return
simp: isOK_def zip_nth_conv list_all_length 𝒯⇩α_code[symmetric] many_sorted_terms.arity[OF many_sorted_terms_mk_sigF])
qed (auto simp: 𝒯⇩α_code[symmetric])
context
fixes sig :: "('f :: show × 't list × 't :: show) list"
begin
interpretation many_sorted_terms "mk_sigF sig" "Some ∘ snd" by simp
definition annotate_term' where
"annotate_term' sigF t =
(case root t of None ⇒ error id
| Some fn ⇒ (case sigF fn of None ⇒ error (shows ''persistent decomposition: no signature for symbol '' ∘ shows fn)
| Some (_, α) ⇒ do { t' <- annotate_term sigF α t; return (α, t') }))"
lemma isOK_annotate_term':
"isOK (annotate_term' (mk_sigF sig) t) ⟹ case_prod (many_sorted_terms.𝒯⇩α (mk_sigF sig) (Some ∘ snd)) (run (annotate_term' (mk_sigF sig) t))"
by (auto simp: annotate_term'_def simp del: annotate_term.simps split: option.splits dest: isOK_annotate_term)
">definition
"check_rule sigF rl = do {
let (l, r) = rl;
(α, l') <- annotate_term' sigF l;
r' <- annotate_term sigF α r;
(* check_variants_rule (l, r) (l', r'); (* TODO: message? *) *)
check_variants_rule (map_vars_term (λx. (x, α)) l, map_vars_term (λx. (x, α)) r) (l', r')
<? (shows ''persistent decomposition: inconsistent types of variables in rule ''
∘ shows_rule (l, r));
return (l', r')
}"
lemma isOK_check_rule:
assumes "wf_trs {rl}" "isOK (check_rule (mk_sigF sig) rl)"
defines "res ≡ run (check_rule (mk_sigF sig) rl)"
shows "wf_trs {res} ∧ rstep' {rl} = rstep' {res :: (_, 'v :: {show, infinite} × _) rule} ∧ (∃α. 𝒯⇩α α (fst res) ∧ 𝒯⇩α α (snd res))"
proof (intro conjI, goal_cases)
obtain l r l' r' where [simp]: "rl = (l, r)" "res = (l', r')" by (metis prod.collapse)
obtain α where [simp]:
"projr (annotate_term' (mk_sigF sig) l) = (α, l')"
"projr (annotate_term (mk_sigF sig) α r) = r'"
using assms by (auto simp: check_rule_def del: check_variants_rule) blast
have *: "𝒯⇩α α (fst res)" "𝒯⇩α α (snd res)"
using assms by (auto simp: check_rule_def dest!: isOK_annotate_term' isOK_annotate_term)
obtain p where
**: "(l', r') = p ∙ (map_vars_term (λx. (x, α)) l, map_vars_term (λx. (x, α)) r)"
using assms by (auto simp: check_rule_def) metis
{
case 1
have "wf_trs {(map_vars_term (λx. (x, α)) l, map_vars_term (λx. (x, α)) r)}"
using assms(1) by (auto simp: wf_trs_def term.set_map)
then show ?case using wf_trs_permute[of _ "{_}"]
by (auto simp: ** trs_pt.permute_set_def[unfolded Setcompr_eq_image])
next
case 2
have [simp]: "rstep' {(l, r)} = rstep' {(map_vars_term (λx. (x, α)) l, map_vars_term (λx. (x, α)) r)}"
unfolding map_vars_term_eq
apply (intro equalityI subrelI)
subgoal using rstep'.intros[of "l ⋅ (Var ∘ (λx. (x, α)))" "r ⋅ (Var ∘ (λx. (x, α)))" _ _ "(Var ∘ fst) ∘⇩s _"]
unfolding subst_subst_compose[symmetric] subst_compose_assoc[symmetric] subst_compose_def[of _ "Var ∘ _"]
by (auto elim!: rstep'.cases simp: comp_def)
subgoal by (auto elim!: rstep'.cases simp: subst_subst_compose[symmetric] simp del: subst_subst_compose)
done
show ?case using rstep'_permute[of _ "{_}"]
by (auto simp: ** trs_pt.permute_set_def[unfolded Setcompr_eq_image])
next
case 3 thus ?case using * by auto
}
qed
">definition
"check_persistence1 R Rs = do {
check (sig_is_clean sig) (shows ''persistent decomposition: duplicate function symbol in signature''); (* TODO: message *)
check_wf_trs R;
mapM check_wf_trs Rs;
let sigF = mk_sigF sig;
R' <- mapM (check_rule sigF) R;
Rs' <- mapM (mapM (check_rule sigF)) Rs;
return (R', Rs')
}"
lemma wf_trs_by_singletons:
"wf_trs R ⟷ (∀r ∈ R. wf_trs {r})"
by (auto simp: wf_trs_def)
lemma rstep'_by_singletons:
"rstep' R = ⋃{rstep' {r} |r. r ∈ R}"
by (auto elim!: rstep'.cases)
lemma isOK_check_rules:
fixes R :: "('f :: show, 'v :: {infinite, show}) rule list"
assumes "wf_trs (set R)" "isOK (mapM (check_rule (mk_sigF sig)) R)"
defines "res ≡ run (mapM (check_rule (mk_sigF sig)) R)"
shows "wf_trs (set res)" "rstep' (set R) = rstep' (set res)" "⋀r. r ∈ set res ⟹ ∃α. 𝒯⇩α α (fst r) ∧ 𝒯⇩α α (snd r)"
proof -
note x[simp] = wf_trs_by_singletons[of "set _"] rstep'_by_singletons[of "set _"]
have [simp]: "length res = length R"
using isOK_mapM[OF assms(2)] by (auto simp: res_def)
{ fix i assume *: "i < length R"
then have **: "isOK (check_rule (mk_sigF sig) (R ! i))" "res ! i = run (check_rule (mk_sigF sig) (R ! i))"
by (metis isOK_mapM[OF assms(2)] nth_mem nth_map res_def)+
have "wf_trs {res ! i}" "rstep' {R ! i} = rstep' {res ! i}" "∃α. 𝒯⇩α α (fst (res ! i)) ∧ 𝒯⇩α α (snd (res ! i))"
using assms(1) nth_mem[OF *(1)] isOK_check_rule[OF _ **(1)]
by (auto simp: **(2)[symmetric]) }
note [simp] = this
show "wf_trs (set res)" "⋀r. r ∈ set res ⟹ ∃α. 𝒯⇩α α (fst r) ∧ 𝒯⇩α α (snd r)"
by (auto dest!: in_set_idx)
show "rstep' (set R) = rstep' (set res)" unfolding x Setcompr_eq_image set_map[symmetric]
by (intro arg_cong[of _ _ "λxs. Union (set xs)"]) (auto intro!: nth_equalityI)
qed
lemma isOK_check_persistence1:
fixes R :: "('f :: show, 'v :: {infinite, show}) rule list"
and Rs :: "('f :: show, 'v :: {infinite, show}) rule list list"
assumes "isOK (check_persistence1 R Rs)"
defines "res ≡ run (check_persistence1 R Rs)"
defines "R' ≡ fst res" and "Rs' ≡ snd res"
shows "sig_is_clean sig"
"wf_trs (set R')"
"CR (rstep' (set R) :: ('f, 'w) trs) ⟷ CR (rstep' (set R') :: ('f, 'w) trs)"
"⋀r. r ∈ set R' ⟹ ∃α. 𝒯⇩α α (fst r) ∧ 𝒯⇩α α (snd r)"
"⋀S. S ∈ set Rs' ⟹ wf_trs (set S)"
"(∀S ∈ set Rs. CR (rstep' (set S) :: ('f, 'w) trs)) ⟷ (∀S ∈ set Rs'. CR (rstep' (set S) :: ('f, 'w) trs))"
"⋀S r. S ∈ set Rs' ⟹ r ∈ set S ⟹ ∃α. 𝒯⇩α α (fst r) ∧ 𝒯⇩α α (snd r)"
"length Rs' = length Rs"
proof (goal_cases 0 1 2 3 4 5 6 7)
have *: "sig_is_clean sig" "wf_trs (set R)"
"isOK (mapM (check_rule (mk_sigF sig)) R)"
"R' = run (mapM (check_rule (mk_sigF sig)) R)" and
**: "⋀R. R ∈ set Rs ⟹ wf_trs (set R)"
"⋀R. R ∈ set Rs ⟹ isOK (mapM (check_rule (mk_sigF sig)) R)"
"Rs' = map (λR. run (mapM (check_rule (mk_sigF sig)) R)) Rs"
using assms(1) by (auto simp: check_persistence1_def R'_def Rs'_def res_def dest: isOK_mapM)
(insert isOK_mapM, fastforce)
{ case 0 then show ?case using * by (auto simp: isOK_check_rules)
next case 1 then show ?case using * by (auto simp: isOK_check_rules)
next case 2 then show ?case using * by (auto simp: isOK_check_rules)
next case (3 r) then show ?case using * by (auto simp: isOK_check_rules)
next case (4 S) then show ?case by (auto simp: isOK_check_rules[OF **(1,2)] **(3))
next case 5 then show ?case by (auto simp: isOK_check_rules[OF **(1,2)] **(3))
next case (6 S r) then show ?case by (auto simp: isOK_check_rules[OF **(1,2)] **(3))
next case 7 then show ?case by (auto simp: isOK_check_rules[OF **(1,2)] **(3)) }
qed
lemma interpret_persistent_cr_infinite_vars:
fixes R :: "('f, 'v :: infinite × 't) trs"
assumes "wf_trs R" and "⋀l r. (l, r) ∈ R ⟹ ∃α . 𝒯⇩α α l ∧ 𝒯⇩α α r"
shows "persistent_cr_infinite_vars (mk_sigF sig) (Some ∘ snd) R"
proof (unfold_locales, goal_cases)
case (3 α)
have [simp]: "{v ∈ many_sorted_terms.𝒱 (Some ∘ snd). snd v = α} = UNIV × {α}"
by (auto simp: many_sorted_terms.𝒱_def[OF many_sorted_terms_mk_sigF])
show ?case by (auto simp: infinite_UNIV dest: finite_cartesian_productD1)
qed (auto simp: assms)
">definition
"type_of_rule sigF r = snd (the (sigF (the (root (fst r)))))"
">definition
"R_nα ty R = filter (λr. type_of_rule (mk_sigF sig) r ∈ set (needed_types_code sig ty)) R"
lemma type_of_rule_simp [simp]:
"is_Fun l ⟹ 𝒯⇩α α l ⟹ type_of_rule (mk_sigF sig) (l, r) = α"
by (auto simp: type_of_rule_def elim!: 𝒯⇩α.cases)
lemma R_nα_to_ℛ_nα:
assumes "sig_is_clean sig" "wf_trs (set R)" "⋀l r. (l, r) ∈ set R ⟹ ∃α . 𝒯⇩α α l ∧ 𝒯⇩α α r"
shows "set (R_nα α R) = persistent_cr.ℛ⇩n⇩α (mk_sigF sig) (Some ∘ snd) (set R) α"
using needed_types_code[OF assms(1)] assms(2)
apply (auto simp: R_nα_def wf_trs_def')
by (smt assms(3) case_prodD in_pair_collect_simp type_of_rule_simp)
">definition
"check_persistence_not_cr R S = do {
(R', Ss') <- check_persistence1 R [S];
let sigF = mk_sigF sig;
let types = map (snd ∘ snd) sig;
let needed_types = needed_types_code sig;
existsM (λS. check_litsim_trs S (hd Ss'))
(map (λty. let tys = needed_types ty in filter (λr. type_of_rule sigF r ∈ set tys) R') types)
<? (shows ''persistent decomposition: new system is not induced by any type:'' ∘ shows_nl
∘ shows_trs S)
}"
lemma isOK_check_persistence_not_cr:
fixes R :: "('f, 'v :: {infinite, show}) rule list"
assumes "isOK (check_persistence_not_cr R S)" "CR (rstep' (set R) :: (_, 'w :: infinite) trs)"
shows "CR (rstep' (set S) :: (_, 'w) trs)"
proof -
let ?res1 = "run (check_persistence1 R [S])"
def R' ≡ "fst ?res1" and S' ≡ "hd (snd ?res1)"
have *: "wf_trs (set R')" "⋀l r. (l, r) ∈ (set R') ⟹ ∃α . 𝒯⇩α α l ∧ 𝒯⇩α α r"
and [simp]: "sig_is_clean sig"
"CR (rstep' (set R) :: (_, 'w) trs) ⟷ CR (rstep' (set R') :: (_, 'w) trs)"
using assms(1) isOK_check_persistence1[of R "[S]"] by (auto simp: R'_def check_persistence_not_cr_def)
then interpret persistent_cr_infinite_vars "mk_sigF sig" "Some ∘ snd" "set R'"
by (intro interpret_persistent_cr_infinite_vars)
have [simp]: "CR (rstep' (set S) :: (_, 'w) trs) ⟷ CR (rstep' (set S') :: (_, 'w) trs)"
and **: "wf_trs (set S')" "⋀l r. (l, r) ∈ set S' ⟹ ∃α. 𝒯⇩α α l ∧ 𝒯⇩α α r"
using assms(1) isOK_check_persistence1(5-)[of R "[S]"]
by (cases "snd ?res1", (auto 0 0 simp: S'_def check_persistence_not_cr_def)[2])+
obtain α where "set (R_nα α R') ≐ set S'"
using assms(1) by (auto simp: check_persistence_not_cr_def R_nα_def R'_def S'_def)
note *** = rstep'_eq_litsim_trs[OF subsumable_trs.litsim_sym[OF this]]
wf_trs_lit_sim_trs[OF subsumable_trs.litsim_sym[OF this]]
have "funas_trs (set R') ⊆ ℱ" "funas_trs (set S') ⊆ ℱ"
using * subsetD[OF 𝒯⇩α_𝒯] ** unfolding 𝒯_def by (auto simp: funas_trs_def funas_rule_def) blast+
then show ?thesis
using persistent_decomposition[of UNIV] assms(2) *(1) **(1) R_nα_to_ℛ_nα[OF _ *]
by (auto simp: CR_change_variables_iff' CR_on_iff_CR[symmetric] 𝒯_def)
(auto simp: *** rstep_eq_rstep')
qed
fun maximal_types_loop where
"maximal_types_loop nt [] = []"
| "maximal_types_loop nt (β # tys) =
(let mt = maximal_types_loop nt tys; ntβ = nt β in
if (∃α ∈ set mt. β ∈ set (nt α)) then mt else β # filter (λα. α ∉ set ntβ) mt)"
lemma maximal_types_loop_prop:
assumes "sig_is_clean sig" "β ∈ set tys"
shows "∃α ∈ set (maximal_types_loop (needed_types_code sig) tys). needed_types α β"
using assms(2)
proof (induct tys arbitrary: β)
case (Cons a tys)
show ?case using assms(1) Cons(2-) needed_types_code[of sig]
by (auto dest!: Cons(1) simp: Let_def)
qed auto
">definition
"maximal_types nt = maximal_types_loop nt (map (snd ∘ snd) sig)"
lemma maximal_types_prop:
assumes "wf_trs R" "sig_is_clean sig"
shows "⋃{{(l, r). (l, r) ∈ R ∧ 𝒯⇩α β' l ∧ 𝒯⇩α β' r} |β'. needed_types β β'} = {} ∨
(∃α∈set (maximal_types (needed_types_code sig)). needed_types α β)"
proof -
have *: "needed_types β γ ⟹ (⋀x. x ∈ set sig ⟹ snd (snd x) ≠ β) ⟹ β = γ" for β γ
by (induct rule: needed_types.induct) (auto simp: find_Some_iff split: prod.splits, metis nth_mem prod_cases3)
have **: "is_Fun t ⟹ 𝒯⇩α α t ⟹ ∃x ∈ set sig. snd (snd x) = α" for α t
by (cases t) (auto elim!: 𝒯⇩α.cases simp: find_Some_iff set_conv_nth, metis)
show ?thesis using maximal_types_loop_prop assms
apply (auto simp: maximal_types_def wf_trs_def' Ball_def)
apply (smt * ** comp_apply in_set_idx length_map nth_map nth_mem snd_conv)
done
qed
">definition
"check_persistence_cr R Rs = do {
(R', Rs') <- check_persistence1 R Rs;
let sigF = mk_sigF sig;
let needed_types = needed_types_code sig;
let types = maximal_types needed_types;
check_allm (λty.
let S = filter (λr. type_of_rule sigF r ∈ set (needed_types ty)) R' in
existsM (check_litsim_trs S) ([] # Rs')
<? (shows ''persistent decomposition: missing system induced by sort '' ∘ shows ty ∘ shows '':''
∘ shows_nl ∘ shows_trs (map (λ(l,r). (map_vars_term snd l, map_vars_term snd r)) S))
) types
}"
lemma isOK_check_persistence_cr:
fixes R :: "('f, 'v :: {infinite, show}) rule list"
assumes "isOK (check_persistence_cr R Rs)" "⋀R. R ∈ set Rs ⟹ CR (rstep' (set R) :: (_, 'w :: infinite) trs)"
shows "CR (rstep' (set R) :: (_, 'w) trs)"
proof -
let ?res1 = "run (check_persistence1 R Rs)"
let ?maximal_types = "maximal_types (needed_types_code sig)"
def R' ≡ "fst ?res1" and Rs' ≡ "snd ?res1"
have *: "isOK (local.check_persistence1 R Rs)"
"⋀ty. ty ∈ set ?maximal_types ⟹
let S = filter (λr. type_of_rule (mk_sigF sig) r ∈ set (needed_types_code sig ty)) R' in
S = [] ∨ (∃R ∈ set Rs'. set S ≐ set R)"
using assms(1)
by (auto simp: check_persistence_cr_def R'_def Rs'_def isOK_try_catch check_litsim_trs intro!: filter_False)
have sig: "sig_is_clean sig" and wfx: "wf_trs (set R')" "⋀S. S ∈ set Rs' ⟹ wf_trs (set S)" and
ty: "⋀r. r ∈ set R' ⟹ ∃α. 𝒯⇩α α (fst r) ∧ 𝒯⇩α α (snd r)"
"⋀S r. S ∈ set Rs' ⟹ r ∈ set S ⟹ ∃α. 𝒯⇩α α (fst r) ∧ 𝒯⇩α α (snd r)" and
cr: "CR (rstep' (set R) :: (_, 'w) trs) ⟷ CR (rstep' (set R') :: (_, 'w) trs)"
"(∀S ∈ set Rs. CR (rstep' (set S) :: (_, 'w) trs)) ⟷ (∀S ∈ set Rs'. CR (rstep' (set S) :: (_, 'w) trs))"
using isOK_check_persistence1[OF *(1)] by (auto simp: R'_def Rs'_def)
interpret persistent_cr_infinite_vars "mk_sigF sig" "Some ∘ snd" "set R'"
using wfx(1) ty(1) by (auto intro: interpret_persistent_cr_infinite_vars)
have "⋀S. S ∈ set Rs' ⟹ funas_trs (set S) ⊆ ℱ"
using ty(2) 𝒯⇩α_𝒯 by (auto simp: funas_trs_def funas_rule_def 𝒯_def) blast+
then have **: "⋀R. R ∈ set Rs' ⟹ CR_on (rstep (set R)) 𝒯"
using assms(2) wfx(2) cr(2) by (auto simp: CR_change_variables_iff' 𝒯_def CR_on_iff_CR)
have "CR_on (rstep (set R')) 𝒯"
proof (intro persistent_decomposition[of "set ?maximal_types", THEN iffD2] ballI, goal_cases)
case (1 β) show ?case by (rule maximal_types_prop[OF wfx(1) sig])
next
case (2 α)
have x: "set [r←R' . type_of_rule (mk_sigF sig) r ∈ set (needed_types_code sig α)] = ⋃{ℛ⇩α β |β. needed_types α β}"
using sig ty(1) wfx(1)
apply (auto simp: needed_types_code wf_trs_def' split: prod.splits)
apply (smt type_of_rule_simp in_pair_collect_simp)
done
have [simp]: "rstep' {} = {}" by (auto elim: rstep'.cases)
have [simp]: "R = {} ⟹ CR_on (rstep' R) X" for R X by (auto simp: CR_on_def)
show ?case
using *(2)[OF 2, unfolded x Let_def set_empty2[symmetric]] **
by (auto simp: rstep_eq_rstep' rstep'_eq_litsim_trs)
qed
then show ?thesis using wfx(1) ℛ_sig
by (auto simp: cr(1) CR_change_variables_iff' CR_on_iff_CR 𝒯_def)
qed
end
end