Theory FCF_Multiset
theory FCF_Multiset
imports
FCF_Set
Pattern_Completeness_Multiset
begin
fun depth_gterm :: "('f,'v)term ⇒ nat" where
"depth_gterm (Fun f ts) = Suc (max_list (map depth_gterm ts))"
| "depth_gterm _ = Suc 0"
lemma depth_gterm_arg: "t ∈ set ts ⟹ depth_gterm t < depth_gterm (Fun f ts)"
unfolding less_eq_Suc_le by (auto intro: max_list)
lemma Max_le_MaxI: assumes "finite A" "A ≠ {}" "finite B"
"⋀ a. a ∈ A ⟹ ∃ b ∈ B. a ≤ b"
shows "Max A ≤ Max B"
using assms by (metis Max_ge_iff Max_in empty_iff)
type_synonym('f,'s)simple_match_problem_ms = "('f,nat × 's)term multiset multiset"
type_synonym('f,'s)simple_pat_problem_ms = "('f,'s)simple_match_problem_ms multiset"
abbreviation mset2 :: "('f,'s)simple_match_problem_ms ⇒ ('f,'s)simple_match_problem" where
"mset2 ≡ image set_mset o set_mset"
abbreviation mset3 :: "('f,'s)simple_pat_problem_ms ⇒ ('f,'s)simple_pat_problem" where
"mset3 ≡ image mset2 o set_mset"
lemma mset2_simps:
"mset2 (add_mset eq mp) = insert (set_mset eq) (mset2 mp)"
"set_mset (add_mset t eq) = insert t (set_mset eq)"
"set_mset {#} = {}"
"mset2 (mp1 + mp2) = mset2 mp1 ∪ mset2 mp2"
"mset3 (add_mset mp p) = insert (mset2 mp) (mset3 p)"
by auto
context pattern_completeness_context
begin
inductive smp_step_ms :: "('f,'s)simple_match_problem_ms ⇒ ('f,'s)simple_match_problem_ms ⇒ bool"
(infix ‹→⇩s⇩s› 50) where
smp_dup: "add_mset (add_mset t (add_mset t eqc)) mp →⇩s⇩s add_mset (add_mset t eqc) mp"
| smp_singleton: "add_mset {# t #} mp →⇩s⇩s mp"
| smp_triv_sort: "t : ι in 𝒯(C,𝒱) ⟹ cd_sort ι = 1 ⟹ add_mset (add_mset t eq) mp →⇩s⇩s mp"
| smp_decomp: "(⋀ t. t ∈ set_mset eqc ⟹ root t = Some (f,n))
⟹ eqcn = {#{#args t ! i. t ∈# eqc#}. i ∈# mset [0..<n]#}
⟹ (⋀ eq. eq ∈ set_mset eqcn ⟹ UNIQ (𝒯(C,𝒱) ` set_mset eq))
⟹ add_mset eqc mp →⇩s⇩s eqcn + mp"
inductive smp_fail_ms :: "('f,'s)simple_match_problem_ms ⇒ bool" where
smp_clash: "Conflict_Clash s t ⟹
s ∈ eqc ⟹ t ∈ eqc ⟹ eqc ∈ mset2 mp ⟹ smp_fail_ms mp"
| smp_decomp_fail: "(⋀ t. t ∈ set_mset eqc ⟹ root t = Some (f,n))
⟹ i < n
⟹ ¬ UNIQ (𝒯(C,𝒱) ` (λ t. args t ! i) ` set_mset eqc)
⟹ smp_fail_ms (add_mset eqc mp)"
inductive spp_step_ms :: "('f,'s)simple_pat_problem_ms ⇒ ('f,'s)simple_pat_problem_ms multiset ⇒ bool"
(infix ‹⇒⇩s⇩s› 50) where
spp_solved: "add_mset {#} p ⇒⇩s⇩s {#}"
| spp_simp: "mp →⇩s⇩s mp' ⟹ add_mset mp p ⇒⇩s⇩s {#add_mset mp' p#}"
| spp_delete: "smp_fail_ms mp ⟹ add_mset mp p ⇒⇩s⇩s {#p#}"
| spp_delete_large_sort: "
(⋀ i. i ≤ (n :: nat) ⟹ snd (x i) = ι ∧ eq i ∈# mp i ∧ Var (x i) ≠ t i ∧ {Var (x i), t i} ⊆ set_mset (eq i)) ⟹
(t ` {0..n} ∪ (Var o x) ` {0..n}) ∩ Var ` tvars_spat (mset3 p) = {} ⟹
(card (t ` {0..n}) < cd_sort ι) ⟹
p + mset (map mp [0..< Suc n]) ⇒⇩s⇩s {# p #}"
| spp_inst: "{#{#Var x, t#}#} ∈# p
⟹ is_Fun t
⟹ fst ` tvars_spat (mset3 p) ∩ {n..<n + m} = {}
⟹ p ⇒⇩s⇩s mset (map (λ τ. image_mset (image_mset (image_mset (λt. t ⋅ τ))) p) (τs_list n x))"
| spp_split: "mp = add_mset (add_mset s (add_mset t eqc)) mp'
⟹ is_Var s ≠ is_Var t ⟹ eqc ≠ {#} ∨ mp' ≠ {#}
⟹ add_mset mp p ⇒⇩s⇩s {#add_mset {# {# s, t #} #} p, add_mset (add_mset (add_mset s eqc) mp') p#}"
end
context pattern_completeness_context_with_assms
begin
lemma smp_fail_ms: assumes "smp_fail_ms mp"
and "finite_constructor_form_pat (insert (mset2 mp) p)"
shows "finite_constructor_form_pat p"
"simple_pat_complete C SS (insert (mset2 mp) p) ⟷ simple_pat_complete C SS p"
proof -
show "finite_constructor_form_pat p" using assms(2) unfolding finite_constructor_form_pat_def by auto
show "simple_pat_complete C SS (insert (mset2 mp) p) ⟷ simple_pat_complete C SS p"
using assms
proof (induct mp rule: smp_fail_ms.induct)
case *: (smp_clash s t eqc mp)
from *(4) obtain eq mp' where mp: "mp = add_mset eq mp'" and eqc: "eqc = set_mset eq"
by (metis comp_apply image_iff mset_add)
from eqc *(2-3) have "set_mset eq = {s,t} ∪ eqc" by auto
from eliminate_clash_spp(1)[OF *(5)[unfolded mset2_simps mp] refl refl this *(1)]
show ?case unfolding mp mset2_simps .
next
case *: (smp_decomp_fail eqc f n i mp)
from *(2-3) have "(∀eq∈{{args t ! i |. t ∈ set_mset eqc} |. i ∈ {0..<n}}. UNIQ (𝒯(C,𝒱) ` eq)) = False"
by auto
from decompose_spp(1)[OF *(4)[unfolded mset2_simps] refl refl *(1) refl refl, unfolded this if_False]
show ?case unfolding mset2_simps by auto
qed
qed
lemma smp_step_ms: assumes "mp →⇩s⇩s mp'"
and "finite_constructor_form_pat (insert (mset2 mp) p)"
shows "finite_constructor_form_pat (insert (mset2 mp') p)"
"simple_pat_complete C SS (insert (mset2 mp) p) ⟷ simple_pat_complete C SS (insert (mset2 mp') p)"
proof (atomize(full), insert assms, induct mp mp' rule: smp_step_ms.induct)
case (smp_singleton t mp)
from eliminate_uniq_spp[OF this[unfolded mset2_simps] refl refl refl]
show ?case by (auto simp: Uniq_def)
next
case *: (smp_triv_sort t ι eq mp)
show ?case
proof (intro conjI)
show "finite_constructor_form_pat (insert (mset2 mp) p)"
using * unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def by auto
show "simple_pat_complete C SS (insert (mset2 (add_mset (add_mset t eq) mp)) p) =
simple_pat_complete C SS (insert (mset2 mp) p)"
unfolding simple_pat_complete_def bex_simps
proof (rule all_cong, intro disj_cong refl)
fix σ
assume sig: "σ :⇩s 𝒱 |` SS → 𝒯(C)"
from * obtain τ where typed: "u ∈ insert t (set_mset eq) ⟹ u : τ in 𝒯(C,𝒱 |` SS)" for u
unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def by auto
from typed_S_eq[OF this *(1)] have tau: "τ = ι" by auto
from typed_imp_S[OF typed, of t] tau have "ι ∈ S" by auto
from cd[OF this] * minBnd1
have card: "card_of_sort C ι = 1" by auto
have "UNIQ_subst σ (insert t (set_mset eq))" unfolding UNIQ_subst_alt_def
proof (intro allI impI, goal_cases)
case (1 u v)
{
fix w
assume "w ∈ {u,v}"
with 1 typed tau have "w : ι in 𝒯(C,𝒱 |` SS)" by auto
with sig have "w ⋅ σ : ι in 𝒯(C)" by (rule subst_hastype)
}
hence "u ⋅ σ : ι in 𝒯(C)" "v ⋅ σ : ι in 𝒯(C)" by auto
with card
show "u ⋅ σ = v ⋅ σ" unfolding card_of_sort_def card_eq_1_iff by auto
qed
thus "simple_match_complete_wrt σ (mset2 (add_mset (add_mset t eq) mp)) =
simple_match_complete_wrt σ (mset2 mp)"
unfolding simple_match_complete_wrt_def by simp
qed
qed
next
case *: (smp_decomp eqc f n eqcn mp)
have eq: "(∀eq∈mset2 eqcn. UNIQ (𝒯(C,𝒱) ` eq)) = True"
using *(2-3) by auto
define N where "N = {0..<n}"
have fin: "finite N" unfolding N_def by auto
have "mset2 eqcn = {{args t ! i |. t ∈ set_mset eqc} |. i ∈ {0..<n}}"
unfolding *(2) mset_upt N_def[symmetric]
apply (subst (2) finite_set_mset_mset_set[OF fin, symmetric])
by (metis (no_types, lifting) comp_apply image_cong image_image multiset.set_map)
from decompose_spp[OF *(4)[unfolded mset2_simps] refl refl *(1) this, unfolded eq if_True, OF _ refl]
show ?case unfolding mset2_simps by auto
qed auto
lemma spp_step_ms: assumes "p ⇒⇩s⇩s Pn"
and "finite_constructor_form_pat (mset3 p)"
shows "Ball (set_mset Pn) (λ p'. finite_constructor_form_pat (mset3 p'))"
"simple_pat_complete C SS (mset3 p) ⟷ Ball (set_mset Pn) (λ p'. simple_pat_complete C SS (mset3 p'))"
proof (atomize(full), insert assms, induct p Pn rule: spp_step_ms.induct)
case (spp_solved p)
show ?case unfolding mset2_simps using detect_sat_spp by auto
next
case *: (spp_simp mp mp' p)
from smp_step_ms[OF *(1) *(2)[unfolded mset2_simps]]
show ?case unfolding mset2_simps by auto
next
case *: (spp_delete mp p)
from smp_fail_ms[OF *(1) *(2)[unfolded mset2_simps]]
show ?case unfolding mset2_simps by auto
next
case *: (spp_inst x t p n)
from mset_add[OF *(1)] have mem: "{{Var x,t}} ∈ mset3 p" by fastforce
define p' where "p' = mset3 p"
have id: "{(`) ((`) (λt. t ⋅ τ)) ` mset3 p |. τ ∈ τs n x} = mset3 ` {image_mset (image_mset (image_mset (λt. t ⋅ τ))) p |. τ ∈ τs n x}"
unfolding image_comp o_def image_mset.comp set_image_mset by auto
from mem have "x ∈ tvars_spat (mset3 p)" unfolding p'_def[symmetric]
by (auto intro!: bexI[of _ "{{Var x, t}}"])
from instantiate_spp[OF *(4,3) this refl]
show ?case unfolding id using τs_list by auto
next
case *: (spp_split mp s t eqc mp' p)
have "insert s (insert t (set_mset eqc)) = {s, t} ∪ set_mset eqc" by auto
from separate_var_fun_spp_single[OF *(4)[unfolded mset2_simps *(1)] refl refl this refl]
show ?case unfolding mset2_simps *(1) by auto
next
case *: (spp_delete_large_sort n x ι eq mp t p)
have "mset3 (p + mset (map mp [0..<Suc n])) = mset3 p ∪ (mset2 o mp) ` set [0..< Suc n]"
by auto
also have "set [0..< Suc n] = {0..n}" by auto
finally have id: "mset3 (p + mset (map mp [0..<Suc n])) = mset3 p ∪ (mset2 ∘ mp) ` {0..n} " by auto
have main: "simple_pat_complete C SS (mset3 (p + mset (map mp [0..<Suc n]))) =
simple_pat_complete C SS (mset3 p)" unfolding id
apply (rule eliminate_large_sort[OF _ *(2,3), of "set_mset o eq"])
subgoal for i using *(1)[of i] by auto
subgoal using *(4) unfolding id by (auto simp: finite_constructor_form_pat_def)
done
show ?case unfolding main using *(4) by (auto simp: finite_constructor_form_pat_def)
qed
lemma finite_tvars_spat_mset3: "finite (tvars_spat (mset3 p))"
by (intro finite_Union; fastforce)
lemma finite_tvars_smp_mset2: "finite (tvars_smp (mset2 mp))"
by (intro finite_Union; fastforce)
lemma normal_form_spp_step_fvf: assumes "finite_constructor_form_pat (mset3 p)"
and "∄ P. p ⇒⇩s⇩s P"
and mp: "mp ∈ mset3 p"
and eqc: "eqc ∈ mp"
and t: "t ∈ eqc"
shows "is_Var t"
proof (rule ccontr)
assume f: "is_Fun t"
from mp obtain mp' where mp': "mp' ∈ set_mset p" and mp: "mp = mset2 mp'" by auto
from eqc[unfolded mp] obtain eqc' where eqc': "eqc' ∈ set_mset mp'" and eqc: "eqc = set_mset eqc'" by auto
from t[unfolded eqc] obtain eqc2 where id1: "eqc' = add_mset t eqc2" by (rule mset_add)
from eqc' obtain mp2 where id2: "mp' = add_mset eqc' mp2" by (rule mset_add)
from mp' obtain p2 where id3: "p = add_mset mp' p2" by (rule mset_add)
have p: "p = add_mset (add_mset (add_mset t eqc2) mp2) p2" unfolding id1 id2 id3 ..
with assms have contra: "add_mset (add_mset (add_mset t eqc2) mp2) p2 ⇒⇩s⇩s P ⟹ False" for P by auto
show False
proof (cases "eqc2 = {#}")
case True
show False
apply (rule contra)
apply (unfold True)
by (rule spp_simp, rule smp_singleton)
next
case ne: False
show False
proof (cases "∃ s ∈ set_mset eqc2. is_Var s")
case True
then obtain s eqc3 where "eqc2 = add_mset s eqc3" and "is_Var s" by (metis mset_add)
then obtain x where eqc: "add_mset t eqc2 = add_mset (Var x) (add_mset t eqc3)" by (cases s, auto)
show False
proof (cases "eqc3 = {#} ∧ mp2 = {#}")
case True
hence True: "eqc3 = {#}" "mp2 = {#}" by auto
define names where "names = fst ` ⋃ (⋃ (⋃ ((`) ((`) vars) ` insert (insert {Var x, t} (mset2 {#})) (mset3 p2))))"
define n where "n = Max names"
have id: "mset3 (add_mset {#{#Var x, t#}#} p2) =
insert (insert {Var x, t} (mset2 {#})) (mset3 p2)" by auto
have "names = fst ` tvars_spat (mset3 p)" unfolding p eqc True names_def by simp
also have "finite …" using finite_tvars_spat_mset3[of p] by blast
finally have names: "⋀ k. k ∈ names ⟹ k ≤ n" unfolding n_def by auto
show False
apply (rule contra)
apply (unfold eqc, unfold True)
apply (rule spp_inst[OF _ f, of x _ "Suc n"])
apply force
apply (unfold id)
apply (unfold names_def[symmetric])
using names by fastforce
next
case False
hence diff: "eqc3 ≠ {#} ∨ mp2 ≠ {#}" by auto
from contra[OF spp_split[OF _ _ diff], unfolded eqc True, OF refl] f
show ?thesis by auto
qed
next
case False
hence funs: "⋀ s. s ∈# eqc2 ⟹ is_Fun s" by auto
show False
proof (cases "∃ s ∈# eqc2. root s ≠ root t")
case True
then obtain s eqc3 where eqc2: "eqc2 = add_mset s eqc3" and diff: "root s ≠ root t"
by (meson mset_add)
from funs[of s] eqc2 diff f obtain f g where rt: "root t = Some f" "root s = Some g" and diff: "f ≠ g"
by (cases s; cases t; auto)
hence conf: "Conflict_Clash s t" by (cases s; cases t; auto simp: conflicts.simps)
show False
apply (rule contra)
apply (unfold eqc2)
apply (rule spp_delete)
apply (rule smp_clash[OF conf, of "insert t (insert s (set_mset eqc3))"])
by auto
next
case False
from f obtain f n where "root t = Some (f,n)" by (cases t, auto)
with False have rt: "⋀ s. s ∈# add_mset t eqc2 ⟹ root s = Some (f,n)" by auto
let ?cond = "∀ eq ∈# {#{#args t ! i. t ∈# add_mset t eqc2#}. i ∈# mset [0..<n]#}. UNIQ (𝒯(C,𝒱) ` set_mset eq)"
show False
proof (cases ?cond)
case True
show False
apply (rule contra)
apply (rule spp_simp)
apply (rule smp_decomp[OF rt refl])
using True by auto
next
case False
define eqc3 where "eqc3 = add_mset t eqc2"
from False obtain i where i: "i < n" and nuniq: "¬ UNIQ (𝒯(C,𝒱) ` set_mset {#args t ! i. t ∈# add_mset t eqc2 #})"
unfolding mset2_simps by auto
show False
apply (rule contra)
apply (rule spp_delete)
apply (rule smp_decomp_fail[OF rt i])
using nuniq by auto
qed
qed
qed
qed
qed
definition max_depth_sort :: "'s ⇒ nat" where
"max_depth_sort s = Maximum (depth_gterm ` {t. t : s in 𝒯(C)})"
lemma max_depth_sort_wit: assumes "finite_sort C s"
and "s ∈ S"
shows "∃ t. t : s in 𝒯(C) ∧
depth_gterm t = max_depth_sort s ∧
(∀ t'. t' : s in 𝒯(C) ⟶ depth_gterm t' ≤ depth_gterm t)"
proof -
let ?T = "{t. t : s in 𝒯(C)}"
from sorts_non_empty[OF assms(2)] have "depth_gterm ` ?T ≠ {}" by auto
moreover from assms(1)[unfolded finite_sort_def] have fin: "finite (depth_gterm ` ?T)" by auto
ultimately obtain d where "d ∈ depth_gterm ` ?T" and d: "d = Maximum (depth_gterm ` ?T)"
by (metis has_MaximumD(1) has_Maximum_nat_iff_finite)
from this obtain t where t: "t ∈ ?T"
and depth: "depth_gterm t = Maximum (depth_gterm ` ?T)" "d = depth_gterm t" by auto
have "t' ∈ ?T ⟹ depth_gterm t' ≤ depth_gterm t" for t'
unfolding depth(2)[symmetric] unfolding d using fin
by (meson bdd_above_Maximum_nat bdd_above_nat image_iff)
thus ?thesis unfolding max_depth_sort_def depth(1)[symmetric] using t
by (intro exI[of _ t], auto)
qed
lemma max_depth_sort_Fun: assumes f: "f : σs → s in C"
and si: "si ∈ set σs"
and fins: "finite_sort C s"
shows "max_depth_sort si < max_depth_sort s"
proof -
from C_sub_S[OF f] si have s: "s ∈ S" and siS: "si ∈ S" by auto
from finite_arg_sort[OF fins f si]
have "finite_sort C si" .
from max_depth_sort_wit[OF this siS] obtain ti where
ti: "ti : si in 𝒯(C)" and depi: "depth_gterm ti = max_depth_sort si" by auto
define t where "t s = (SOME t. t : s in 𝒯(C))" for s
have t: "s ∈ set σs ⟹ t s : s in 𝒯(C)" for s
using someI_ex[OF sorts_non_empty[of s]] C_sub_S[OF f]
unfolding t_def by auto
from si obtain i where si: "si = σs ! i" and i: "i < length σs" by (auto simp: set_conv_nth)
define trm where "trm = Fun f (map (λ j. if j = i then ti else t (σs ! j)) [0..<length σs])"
have trm: "trm : s in 𝒯(C)"
unfolding trm_def
apply (intro Fun_hastypeI[OF f] list_all2_all_nthI)
apply force
subgoal for j using t si ti by (auto simp: set_conv_nth)
done
have "max_depth_sort si = depth_gterm ti" using depi by auto
also have "… < depth_gterm trm" unfolding trm_def
by (rule depth_gterm_arg, insert i, auto)
also have "… ≤ max_depth_sort s"
using max_depth_sort_wit[OF fins s] trm by auto
finally show ?thesis .
qed
lemma max_depth_sort_var: assumes "t : s in 𝒯(C, 𝒱 |` SS)"
and "x ∈ vars t"
and "finite_sort C s"
shows "max_depth_sort (snd x) ≤ max_depth_sort s"
using assms
proof (induct)
case (Var y s)
thus ?case by (auto simp: hastype_def restrict_map_def split: if_splits)
next
case (Fun f ts σs τ)
from Fun(4) obtain i where i: "i < length ts" and x: "x ∈ vars (ts ! i)"
by (auto simp: set_conv_nth)
from i Fun(2) have mem: "σs ! i ∈ set σs" by (auto simp: set_conv_nth list_all2_conv_all_nth)
from finite_arg_sort[OF Fun(5,1) mem]
have "finite_sort C (σs ! i)" .
with Fun(3) i x have "max_depth_sort (snd x) ≤ max_depth_sort (σs ! i)"
by (auto simp: list_all2_conv_all_nth)
with max_depth_sort_Fun[OF Fun(1) mem Fun(5)]
show ?case by simp
qed
definition max_depth_sort_mp :: "('f,'s) simple_match_problem_ms ⇒ nat" where
"max_depth_sort_mp mp = Max (insert 0 (max_depth_sort ` snd ` tvars_smp (mset2 mp)))"
definition max_depth_sort_p :: "('f,'s) simple_pat_problem_ms ⇒ nat" where
"max_depth_sort_p p = sum_mset (image_mset max_depth_sort_mp p)"
lemma max_depth_sort_p_add[simp]: "max_depth_sort_p (add_mset mp p) =
max_depth_sort_mp mp + max_depth_sort_p p"
unfolding max_depth_sort_p_def by simp
lemma finite_constructor_form_pat_add: "finite_constructor_form_pat (mset3 (add_mset mp p))
= (finite_constructor_form_mp (mset2 mp) ∧ finite_constructor_form_pat (mset3 p))"
unfolding finite_constructor_form_pat_def by auto
lemma mds_decrease_inst: assumes ft: "is_Fun t"
and tau: "τ ∈ τs n x"
and mp: "mp = {#{#Var x, t#}#}"
and fin: "finite_constructor_form_mp (mset2 mp)"
shows "max_depth_sort_mp mp > max_depth_sort_mp (image_mset (image_mset (λt. t ⋅ τ)) mp)"
proof -
from fin[unfolded finite_constructor_form_mp_def mp] obtain ι
where fin: "finite_sort C ι" and x: "Var x : ι in 𝒯(C,𝒱 |` SS)" and t: "t : ι in 𝒯(C,𝒱 |` SS)"
by auto
from x have iota: "ι = snd x" and xS: "snd x ∈ S" by (auto simp: hastype_def restrict_map_def split: if_splits)
from ft obtain f ts where ft: "t = Fun f ts" by (cases t, auto)
from t[unfolded ft Fun_hastype] obtain σs where f: "f : σs → ι in C"
and ts: "ts :⇩l σs in 𝒯(C,𝒱 |` SS)"
by auto
{
fix y
assume "y ∈ vars t"
from this[unfolded ft] obtain ti where y: "y ∈ vars ti" and ti: "ti ∈ set ts" by auto
from ti ts obtain σi where σi: "σi ∈ set σs" and ti: "ti : σi in 𝒯(C,𝒱 |` SS)"
unfolding list_all2_conv_all_nth set_conv_nth by force
from max_depth_sort_var[OF ti y finite_arg_sort[OF fin f σi]]
have "max_depth_sort (snd y) ≤ max_depth_sort σi" .
also have "… < max_depth_sort (snd x)"
using max_depth_sort_Fun[OF f σi fin] iota by auto
finally have "max_depth_sort (snd y) < max_depth_sort (snd x)" by auto
} note max_x = this
from max_depth_sort_wit[OF fin, unfolded iota, OF xS] obtain wx
where wx: "wx : snd x in 𝒯(C)" and to_wx: "max_depth_sort (snd x) = depth_gterm wx"
and wx_max: "⋀ t'. t' : snd x in 𝒯(C) ⟹ depth_gterm t' ≤ depth_gterm wx" by auto
have "max_depth_sort_mp mp = Max (max_depth_sort ` snd ` insert x (vars t))" unfolding mp
max_depth_sort_mp_def by auto
also have "… = max_depth_sort (snd x)"
by (rule Max_eqI, insert max_x, force+)
finally have max_mp: "max_depth_sort_mp mp = max_depth_sort (snd x)" .
from tau[unfolded τs_def] obtain f σs where f: "f : σs → snd x in C"
and tau: "τ = τc n x (f,σs)" by auto
have "max_depth_sort_mp (image_mset (image_mset (λt. t ⋅ τ)) mp) =
Max (insert 0 (max_depth_sort ` snd ` (vars (τ x) ∪ vars (t ⋅ τ))))"
unfolding max_depth_sort_mp_def mp by simp
also have "… ≤ Max (insert 0 (max_depth_sort ` (snd ` vars (τ x) ∪ snd ` vars t)))"
by (rule Max_mono, auto simp: vars_term_subst tau τc_def subst_def)
also have "snd ` vars (τ x) = set σs" unfolding tau τc_def subst_def
by (force simp: set_zip set_conv_nth[of σs])
also have "Max (insert 0 (max_depth_sort ` (set σs ∪ snd ` vars t))) < max_depth_sort (snd x)"
proof (subst Max_less_iff, force, force, intro ballI)
fix d
assume d: "d ∈ insert 0 (max_depth_sort ` (set σs ∪ snd ` vars t))"
show "d < max_depth_sort (snd x)"
proof (cases "d ∈ max_depth_sort ` snd ` vars t")
case True
with max_x show ?thesis by auto
next
case False
hence "d = 0 ∨ d ∈ max_depth_sort ` set σs" using d by auto
thus ?thesis
proof
assume "d = 0"
thus ?thesis unfolding to_wx by (cases wx, auto)
next
assume "d ∈ max_depth_sort ` set σs"
then obtain σ where mem: "σ ∈ set σs" and d: "d = max_depth_sort σ" by auto
from max_depth_sort_Fun[OF f mem] d fin iota show ?thesis by auto
qed
qed
qed
finally show ?thesis unfolding max_mp .
qed
lemma mds_weak_decrease_inst: assumes tau: "τ ∈ τs n x"
and fin: "finite_sort C (snd x)"
shows "max_depth_sort_mp mp ≥ max_depth_sort_mp (image_mset (image_mset (λt. t ⋅ τ)) mp)"
proof -
from tau[unfolded τs_def] obtain f σs where f: "f : σs → snd x in C"
and tau: "τ = τc n x (f,σs)" by auto
note tau = tau[unfolded τc_def split]
show ?thesis
proof (cases "x ∈ tvars_smp (mset2 mp)")
case False
have "image_mset (image_mset (λt. t ⋅ τ)) mp = image_mset (image_mset (λ t. t ⋅ Var)) mp"
proof (intro image_mset_cong refl term_subst_eq, goal_cases)
case (1 eqc t y)
with False have "x ≠ y" by auto
thus ?case unfolding tau by (auto simp: subst_def)
qed
also have "… = mp" by simp
finally show ?thesis by simp
next
case True
define tv where "tv = tvars_smp (mset2 mp)"
let ?mp = "image_mset (image_mset (λt. t ⋅ τ)) mp"
from True have x: "x ∈ tv" unfolding tv_def .
have fin: "finite tv" unfolding tv_def by auto
have "max_depth_sort_mp mp = Max (insert 0 (max_depth_sort ` snd ` (insert x tv)))"
unfolding max_depth_sort_mp_def tv_def using True by auto
also have "… = Max (max_depth_sort ` snd ` (insert x tv))" using fin by simp
finally have max_mp: "max_depth_sort_mp mp = Max (max_depth_sort ` snd ` insert x tv)" .
have "tvars_smp (mset2 ?mp) = ⋃ (vars ` τ ` tv)"
by (fastforce simp add: tv_def vars_term_subst)
also have "… = vars (τ x) ∪ ⋃ (vars ` τ ` tv)" using x by auto
also have "… = vars (τ x) ∪ (tv - {x})" unfolding tau subst_def by auto
finally have tvars: "tvars_smp (mset2 ?mp) = vars (τ x) ∪ (tv - {x})" .
have "max_depth_sort_mp ?mp = Max (insert 0 (max_depth_sort ` (snd ` vars (τ x) ∪ snd ` (tv - {x}))))"
unfolding max_depth_sort_mp_def tvars by (metis image_Un)
also have "snd ` vars (τ x) = set σs" unfolding tau subst_def
by (force simp: set_zip set_conv_nth[of σs])
also have "Max (insert 0 (max_depth_sort ` (set σs ∪ snd ` (tv - {x}))))
≤ max_depth_sort_mp mp" unfolding max_mp
proof (intro Max_le_MaxI)
fix d
assume d: "d ∈ insert 0 (max_depth_sort ` (set σs ∪ snd ` (tv - {x})))"
show "∃d'∈max_depth_sort ` snd ` insert x tv. d ≤ d'"
proof (cases "d ∈ max_depth_sort ` set σs")
case True
then obtain σ where mem: "σ ∈ set σs" and d: "d = max_depth_sort σ" by auto
from max_depth_sort_Fun[OF f mem assms(2)]
show ?thesis unfolding d by auto
qed (insert d, auto)
qed (insert fin, auto)
finally show ?thesis .
qed
qed
lemma max_depth_sort_le: assumes "tvars_smp (mset2 mp) ⊆ tvars_smp (mset2 mp')"
shows "max_depth_sort_mp mp ≤ max_depth_sort_mp mp'"
unfolding max_depth_sort_mp_def
apply (rule Max_le_MaxI)
apply force
apply force
apply force
using assms by auto
lemma mp_step_tvars: "mp →⇩s⇩s mp' ⟹ tvars_smp (mset2 mp') ⊆ tvars_smp (mset2 mp)"
proof (induct rule: smp_step_ms.induct)
case *: (smp_decomp eqc f n eqcn mp)
from *(2) show ?case
proof (clarsimp, goal_cases)
case (1 x s i ti)
from *(1)[OF 1(4)] 1(2,3)
show ?case by (intro bexI[OF _ 1(4)], cases ti, auto)
qed
qed auto
lemma max_depth_sort_p_inst: assumes mem: "{#{#Var x, t#}#} ∈# p"
and t: "is_Fun t"
and tau: "τ ∈ τs n x"
and fin: "finite_constructor_form_pat (mset3 p)"
shows "max_depth_sort_p p > max_depth_sort_p (image_mset (image_mset (image_mset (λt. t ⋅ τ))) p)"
proof -
obtain mp p' where p: "p = add_mset mp p'" and mp: "mp = {#{#Var x, t#}#}"
using mset_add[OF mem, of thesis] by simp
from fin[unfolded finite_constructor_form_pat_def p]
have fin: "finite_constructor_form_mp (mset2 mp)" by auto
show ?thesis unfolding p
proof (simp add: max_depth_sort_p_def image_mset.compositionality o_def)
show "max_depth_sort_mp (image_mset (image_mset (λt. t ⋅ τ)) mp) +
(∑x∈#p'. max_depth_sort_mp (image_mset (image_mset (λt. t ⋅ τ)) x))
< max_depth_sort_mp mp + ∑⇩# (image_mset max_depth_sort_mp p')" (is "?a1 + ?b1 < ?a2 + ?b2")
proof (rule add_less_le_mono)
show "?a1 < ?a2"
by (rule mds_decrease_inst[OF t tau mp fin])
show "?b1 ≤ ?b2"
proof (rule sum_mset_mono, rule mds_weak_decrease_inst[OF tau])
from fin[unfolded finite_constructor_form_mp_def mp] obtain ι
where fin: "finite_sort C ι" and x: "Var x : ι in 𝒯(C,𝒱 |` SS)"
by auto
from x fin show "finite_sort C (snd x)"
by (auto simp: hastype_def restrict_map_def split: if_splits)
qed
qed
qed
qed
lemma num_syms_τc: "num_syms (t ⋅ τc n x (f,σs)) = num_syms t + count (syms_term t) (Inl x) * length σs"
unfolding num_syms_subst τc_def split
by (simp add: num_syms_def image_mset.compositionality o_def)
lemma num_syms_τs: assumes "τ ∈ τs n x"
shows "num_syms (t ⋅ τ) ≤ num_syms t + count (syms_term t) (Inl x) * m"
proof -
from assms[unfolded τs_def]
obtain f ss where τ: "τ = τc n x (f, ss)" and "f : ss → snd x in C" by auto
from m[OF this(2)] have len: "length ss ≤ m" .
hence "count (syms_term t) (Inl x) * length ss ≤ count (syms_term t) (Inl x) * m" by auto
thus ?thesis unfolding τ num_syms_τc by auto
qed
definition num_syms_mp :: "('f,'s)simple_match_problem_ms ⇒ nat" where
"num_syms_mp mp = sum_mset (image_mset num_syms (sum_mset mp))"
lemma num_syms_lt: assumes "sum_mset mp ⊂# sum_mset mp'"
shows "num_syms_mp mp < num_syms_mp mp'"
proof -
from assms obtain ts where "sum_mset mp' = ts + sum_mset mp" and "ts ≠ {#}"
by (metis add.commute subset_mset.lessE)
thus ?thesis unfolding num_syms_mp_def
by (cases ts, auto)
qed
definition max_dupl_mp where
"max_dupl_mp mp = Max (insert 0 ((λ x. (∑ t∈# sum_mset mp. count (syms_term t) (Inl x))) ` tvars_smp (mset2 mp)))"
definition max_dupl_p :: "('f,'s)simple_pat_problem_ms ⇒ nat" where
"max_dupl_p p = sum_mset (image_mset max_dupl_mp p)"
lemma max_dupl_mp: "(∑ t∈# sum_mset mp. count (syms_term t) (Inl x)) ≤ max_dupl_mp mp"
proof (cases "x ∈ tvars_smp (mset2 mp)")
case True
thus ?thesis unfolding max_dupl_mp_def
by (intro Max_ge[OF finite.insertI[OF finite_imageI]], auto)
next
case False
have "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) = 0"
proof (clarsimp)
fix eq t
assume "eq ∈# mp" "t ∈# eq"
with False have "x ∉ vars t" by auto
thus "count (syms_term t) (Inl x) = 0"
proof (induct t)
case (Fun f ts)
hence "t ∈ set ts ⟹ count (syms_term t) (Inl x) = 0" for t by auto
thus ?case
by (simp, induct ts, auto)
qed auto
qed
thus ?thesis by linarith
qed
lemma num_syms_mp_τs: assumes τ: "τ ∈ τs n x"
shows "num_syms_mp (image_mset (image_mset (λt. t ⋅ τ)) mp) ≤ num_syms_mp mp + max_dupl_mp mp * m"
proof -
have "num_syms_mp (image_mset (image_mset (λt. t ⋅ τ)) mp) =
(∑ eq∈#mp. (∑ t∈#eq. num_syms (t ⋅ τ)))"
unfolding num_syms_mp_def image_mset.compositionality o_def
by (induct mp, auto simp: image_mset.compositionality o_def)
also have "… ≤ (∑ eq∈#mp. (∑ t∈#eq. num_syms t + count (syms_term t) (Inl x) * m))"
using num_syms_τs[OF τ]
by (intro sum_mset_mono, auto)
also have "… = (∑ eq∈#mp. (∑ t∈#eq. num_syms t)) + (∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x) * m))"
unfolding sum_mset.distrib by simp
also have "(∑ eq∈#mp. (∑ t∈#eq. num_syms t)) = num_syms_mp mp"
unfolding num_syms_mp_def by (induct mp, auto)
also have "(∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x) * m))
= (∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x))) * m"
unfolding sum_mset_distrib_right by simp
also have "(∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x)))
= (∑ t∈# sum_mset mp. count (syms_term t) (Inl x))"
by (induct mp, auto)
also have "… * m ≤ max_dupl_mp mp * m"
using max_dupl_mp[of x mp] by simp
finally show ?thesis by simp
qed
lemma max_dupl_mp_τs: assumes τ: "τ ∈ τs n x"
and disj: "fst ` tvars_smp (mset2 mp) ∩ {n..<n + m} = {}"
shows "max_dupl_mp (image_mset (image_mset (λt. t ⋅ τ)) mp) ≤ max_dupl_mp mp"
proof -
from τ[unfolded τs_def] obtain f ss
where f: "f : ss → snd x in C" and τ: "τ = τc n x (f,ss)" by auto
define vs where "vs = (zip [n..<n + length ss] ss)"
define s where "s = (Fun f (map Var vs))"
have tau: "τ = subst x s" unfolding τ τc_def s_def vs_def by auto
show ?thesis
proof (cases "x ∈ tvars_smp (mset2 mp)")
case False
have "image_mset (image_mset (λt. t ⋅ τ)) mp = image_mset (image_mset (λt. t ⋅ Var)) mp"
proof (intro image_mset_cong term_subst_eq, goal_cases)
case (1 eq t y)
with False show ?case by (auto simp: tau subst_def)
qed
thus ?thesis by simp
next
case x: True
show ?thesis unfolding max_dupl_mp_def
proof ((intro Max_le_MaxI; (intro finite.insertI, force)?), force, goal_cases)
case (1 d)
show ?case
proof (cases "d = 0")
case False
with 1 obtain y where
d: "d = (∑t∈#∑⇩# (image_mset (image_mset (λt. t ⋅ τ)) mp). count (syms_term t) (Inl y))"
and y: "y ∈ tvars_smp (mset2 (image_mset (image_mset (λt. t ⋅ τ)) mp))" by auto
have syms_s: "syms_term s = add_mset (Inr f) (mset (map Inl vs))" unfolding s_def
by (simp, induct vs, auto)
define repl :: "('f, nat × 's) Term.term ⇒ (nat × 's + 'f) multiset"
where "repl t = replicate_mset (count (syms_term t) (Inl x)) (Inl x)" for t
let ?add = "(∑t∈#∑⇩# mp. count (repl t) (Inl y))"
let ?symsy = "(∑t∈#∑⇩# mp. count (syms_term t) (Inl y))"
let ?symsxy = "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x) * count (syms_term s) (Inl y))"
let ?symsx = "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x))"
have "d = (∑t∈#∑⇩# mp. count (syms_term (t ⋅ τ)) (Inl y))"
unfolding d
proof (induct mp, auto, goal_cases)
case (1 eq mp)
show ?case by (induct eq, auto)
qed
also have "… ≤ … + ?add" by simp
also have "… =
(∑t∈#∑⇩# mp. count (syms_term (t ⋅ τ) + repl t) (Inl y))"
unfolding sum_mset.distrib[symmetric]
by (rule arg_cong[of _ _ sum_mset], rule image_mset_cong, simp)
also have "… = ?symsy + ?symsxy"
unfolding repl_def tau syms_term_subst sum_mset.distrib[symmetric] by simp
finally have d: "d ≤ ?symsy + ?symsxy" .
show ?thesis
proof (cases "y ∈ set vs")
case False
hence "?symsxy = 0" unfolding syms_s by auto
with d have d: "d ≤ ?symsy" by auto
from y[simplified] obtain eq t
where eq: "eq ∈# mp" and t: "t ∈# eq" and y: "y ∈ vars (t ⋅ τ)"
by auto
from False this[unfolded vars_term_subst tau subst_def s_def]
have "y ∈ vars t" by (auto split: if_splits)
hence "y ∈ tvars_smp (mset2 mp)" using eq t by auto
with d show ?thesis by auto
next
case True
have dist: "distinct vs" unfolding vs_def
by (metis distinct_enumerate enumerate_eq_zip)
from split_list[OF True] obtain vs1 vs2 where vs: "vs = vs1 @ y # vs2" by auto
with dist have nmem: "y ∉ set vs1" "y ∉ set vs2" by auto
have "count (syms_term s) (Inl y) = 1" unfolding syms_s vs using nmem
by (auto simp: count_eq_zero_iff)
with d have d: "d ≤ ?symsy + ?symsx" by auto
from True have "fst y ∈ {n..<n + m}" unfolding vs_def using m[OF f]
by (auto simp: set_zip)
with disj have "y ∉ tvars_smp (mset2 mp)" by blast
hence "?symsy = 0"
proof (clarsimp simp add: count_eq_zero_iff, goal_cases)
case (1 eq t)
from 1 have "Inl y ∈# syms_term t" "y ∉ vars t" by auto
thus False
by (induct t, auto)
qed
with d have "d ≤ ?symsx" by auto
with x show ?thesis by auto
qed
qed auto
qed
qed
qed
definition num_syms_p :: "('f,'s)simple_pat_problem_ms ⇒ nat" where
"num_syms_p p = sum_mset (image_mset num_syms_mp p)"
lemma num_syms_p_add[simp]: "num_syms_p (add_mset mp p) = num_syms_mp mp + num_syms_p p"
unfolding num_syms_p_def by simp
lemma max_dupl_p_add[simp]: "max_dupl_p (add_mset mp p) = max_dupl_mp mp + max_dupl_p p"
unfolding max_dupl_p_def by simp
lemma max_dupl_mono_main: assumes "⋀ x. (∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) ≤ (∑t∈#∑⇩# mp'. count (syms_term t) (Inl x))"
and "tvars_smp (mset2 mp) ⊆ tvars_smp (mset2 mp')"
shows "max_dupl_mp mp ≤ max_dupl_mp mp'"
unfolding max_dupl_mp_def
proof ((intro Max_le_MaxI; (intro finite.insertI, force)?), force, goal_cases)
case (1 d)
show ?case
proof (cases "d = 0")
case False
with 1 obtain x where d: "d = (∑t∈#∑⇩# mp. count (syms_term t) (Inl x))"
and x: "x ∈ tvars_smp (mset2 mp)" by auto
with x assms(2) have x: "x ∈ tvars_smp (mset2 mp')" by blast
define d' where "d' = (∑t∈#∑⇩# mp'. count (syms_term t) (Inl x))"
have "d ≤ d'" unfolding d d'_def by fact
with x show ?thesis unfolding d'_def by blast
qed auto
qed
lemma max_dupl_mono: assumes "sum_mset mp ⊆# sum_mset mp'"
shows "max_dupl_mp mp ≤ max_dupl_mp mp'"
proof (rule max_dupl_mono_main)
from set_mp[OF set_mset_mono[OF assms]]
show "tvars_smp (mset2 mp) ⊆ tvars_smp (mset2 mp')" by force
from assms obtain mp2 where eq: "sum_mset mp' = sum_mset mp + mp2" by (rule subset_mset.less_eqE)
fix x
show "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) ≤ (∑t∈#∑⇩# mp'. count (syms_term t) (Inl x))"
unfolding eq image_mset_union by auto
qed
definition syms_mp :: "('f,'s)simple_match_problem_ms ⇒ (nat × 's + 'f) multiset" where
"syms_mp mp = sum_mset (image_mset syms_term (sum_mset mp))"
definition syms_eqc :: "('f,nat × 's)term multiset ⇒ (nat × 's + 'f) multiset" where
"syms_eqc eqc = sum_mset (image_mset syms_term eqc)"
lemma syms_mp_to_eqc: "syms_mp mp = sum_mset (image_mset syms_eqc mp)"
unfolding syms_mp_def syms_eqc_def
by (induct mp, auto)
lemma nums_eq_size_syms_mp: "num_syms_mp mp = size (syms_mp mp)"
unfolding num_syms_mp_def syms_mp_def num_syms_def
proof (induct mp)
case (add eq mp)
show ?case
apply (simp add: add)
apply (induct eq, auto)
done
qed auto
lemma num_syms_sym_subset: assumes "syms_mp mp ⊂# syms_mp mp'"
shows "num_syms_mp mp < num_syms_mp mp'"
proof -
from assms obtain d where mp': "syms_mp mp' = d + syms_mp mp" and d: "d ≠ {#}"
by (metis add.commute subset_mset.lessE)
thus ?thesis unfolding nums_eq_size_syms_mp by (cases d, auto)
qed
lemma num_syms_subset: assumes "sum_mset mp ⊂# sum_mset mp'"
shows "num_syms_mp mp < num_syms_mp mp'"
proof -
from assms obtain d where mp': "sum_mset mp' = d + sum_mset mp" and d: "d ≠ {#}"
by (metis add.commute subset_mset.lessE)
have "∑⇩# (image_mset num_syms d) > 0" using d num_syms_pos
by (cases d, auto)
hence "num_syms_mp mp < num_syms_mp mp + ∑⇩# (image_mset num_syms d)" by auto
also have "… = num_syms_mp mp'" unfolding num_syms_mp_def mp' by simp
finally show ?thesis .
qed
lemma num_syms_smp_step: "mp →⇩s⇩s mp' ⟹ finite_constructor_form_mp (mset2 mp)
⟹ num_syms_mp mp' < num_syms_mp mp"
proof (induct rule: smp_step_ms.induct)
case (smp_dup t eqc mp)
show ?case by (rule num_syms_subset, auto)
next
case (smp_singleton t mp)
show ?case by (rule num_syms_subset, auto)
next
case (smp_triv_sort t ι eq mp)
show ?case by (rule num_syms_subset, auto)
next
case *: (smp_decomp eqc f n eqcn mp)
define nums where "nums = mset_set {0..<n}"
from *(4) have eqc: "eqc ≠ {#}" unfolding finite_constructor_form_mp_def by auto
define arg where "arg t = (∑i∈#nums. syms_term (args t ! i))" for t :: "('f, nat × 's) term"
{
fix t
assume "t ∈# eqc"
from *(1)[OF this] obtain ts where t: "t = Fun f ts" and len: "n = length ts" by (cases t, auto)
have id: "mset ts = image_mset ((!) ts) (mset [0..<length ts])"
by (metis map_nth' mset_map)
have "syms_term t = add_mset (Inr f) (arg t)" unfolding t arg_def nums_def len
by (auto simp: id image_mset.compositionality o_def)
} note step = this
have "?case ⟷ num_syms_mp eqcn < num_syms_mp {#eqc#}" using * unfolding num_syms_mp_def by auto
also have …
proof (rule num_syms_sym_subset)
from eqc obtain t eqc' where eqc: "eqc = add_mset t eqc'" by (cases eqc, auto)
have "syms_mp eqcn = (∑i∈#nums. syms_eqc {#args t ! i. t ∈# eqc#})"
unfolding image_mset.compositionality o_def nums_def syms_mp_to_eqc *(2)
by simp
also have "… = (∑t∈#eqc. arg t)" unfolding arg_def
unfolding syms_eqc_def image_mset.compositionality o_def
by (rule sum_mset.swap)
also have "… = arg t + (∑t∈#eqc'. arg t)" unfolding eqc by auto
also have "… ⊂# syms_term t + (∑t∈#eqc'. syms_term t)"
proof (rule subset_mset.add_less_le_mono)
from step[of t] eqc
show "arg t ⊂# syms_term t" by auto
from step have step: "t ∈# eqc' ⟹ syms_term t = add_mset (Inr f) (arg t)" for t unfolding eqc by auto
have "∑⇩# (image_mset syms_term eqc') = ∑⇩# (image_mset (λ t. add_mset (Inr f) (arg t)) eqc')"
by (subst image_mset_cong[OF step], auto)
also have "… = ∑⇩# (image_mset (λ t. arg t) eqc') + image_mset (λ t. Inr f) eqc'"
by (induct eqc', auto)
finally
show "∑⇩# (image_mset arg eqc') ⊆# ∑⇩# (image_mset syms_term eqc')" by simp
qed
also have "syms_term t + (∑t∈#eqc'. syms_term t) = (∑t∈#eqc. syms_term t)" unfolding eqc by simp
also have "… = syms_mp {#eqc#}" unfolding syms_mp_to_eqc syms_eqc_def by simp
finally show "syms_mp eqcn ⊂# syms_mp {#eqc#}" .
qed
finally show ?case .
qed
lemma num_syms_mp_pos[simp]: assumes "finite_constructor_form_mp (mset2 mp)"
and "mp ≠ {#}"
shows "num_syms_mp mp > 0"
proof -
from assms obtain eqc mp' where mp: "mp = add_mset eqc mp'" by (cases mp, auto)
with assms have "eqc ≠ {#}" unfolding finite_constructor_form_mp_def by auto
thus ?thesis unfolding mp num_syms_mp_def by (cases eqc, auto)
qed
lemma count_syms_mp: "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) = (count (syms_mp mp) (Inl x))"
unfolding syms_mp_def
proof (induct mp, auto simp: image_mset.compositionality o_def, goal_cases)
case (1 eq mp)
show ?case by (induct eq, auto)
qed
lemma max_dupl_smp_step: "mp →⇩s⇩s mp' ⟹ max_dupl_mp mp' ≤ max_dupl_mp mp"
proof (induct rule: smp_step_ms.induct)
case (smp_dup t eqc mp)
show ?case by (rule max_dupl_mono, auto)
next
case (smp_singleton t mp)
show ?case by (rule max_dupl_mono, auto)
next
case (smp_triv_sort t ι eq mp)
show ?case by (rule max_dupl_mono, auto)
next
case *: (smp_decomp eqc f n eqcn mp)
show ?case
proof (rule max_dupl_mono_main, unfold count_syms_mp, rule mset_subset_eq_count)
have "syms_mp eqcn ⊆# syms_mp {#eqc#}"
proof -
define nums where "nums = mset_set {0..<n}"
define arg where "arg t = (∑i∈#nums. syms_term (args t ! i))" for t :: "('f, nat × 's) term"
have "syms_mp eqcn = (∑i∈#nums. syms_eqc {#args t ! i. t ∈# eqc#})"
unfolding image_mset.compositionality o_def nums_def syms_mp_to_eqc *(2)
by simp
also have "… = (∑t∈#eqc. arg t)" unfolding arg_def
unfolding syms_eqc_def image_mset.compositionality o_def
by (rule sum_mset.swap)
finally have transform: "syms_mp eqcn = ∑⇩# (image_mset arg eqc)" .
have "?thesis ⟷ ∑⇩# (image_mset arg eqc) ⊆# ∑⇩# (image_mset syms_term eqc)"
unfolding transform unfolding syms_mp_def by simp
also have "…"
proof -
{
fix t
assume "t ∈# eqc"
from *(1)[OF this] obtain ts where t: "t = Fun f ts" and len: "length ts = n" by (cases t, auto)
have id: "mset ts = mset (map (λ i. ts ! i) [0..< length ts])"
by (intro arg_cong[of _ _ mset], rule nth_equalityI, auto)
have "arg t = (∑i∈#mset_set {0..<length ts}. syms_term (ts ! i))"
unfolding arg_def t nums_def len by simp
also have "… = (∑⇩# (image_mset syms_term (mset ts)))"
unfolding id
by (auto simp: image_mset.compositionality o_def)
finally have "arg t ⊆# syms_term t" unfolding t by simp
}
thus ?thesis
by (induct eqc, auto intro: subset_mset.add_mono)
qed
finally show ?thesis .
qed
thus "syms_mp (eqcn + mp) ⊆# syms_mp (add_mset eqc mp)"
unfolding syms_mp_def by auto
have "⋃ (⋃x∈set_mset eqcn. vars ` set_mset x) ⊆ ⋃ (vars ` set_mset eqc)" unfolding *(2)
proof (clarsimp, goal_cases)
case (1 x s i t)
from *(1) 1 have "root t = Some (f,n)" by auto
with 1 have "(x,s) ∈ vars t" by (cases t, auto)
with 1 show ?case by auto
qed
thus "tvars_smp (mset2 (eqcn + mp)) ⊆ tvars_smp (mset2 (add_mset eqc mp))"
by force
qed
qed
definition measure_p :: "('f,'s) simple_pat_problem_ms ⇒ nat" where
"measure_p p = max_depth_sort_p p * (max_dupl_p p * m + 1) + num_syms_p p"
lemma measure_p_num_syms: assumes "max_depth_sort_p p ≤ max_depth_sort_p p'"
and "max_dupl_p p ≤ max_dupl_p p'"
and "num_syms_p p < num_syms_p p'"
shows "measure_p p < measure_p p'"
unfolding measure_p_def
by (intro add_le_less_mono mult_mono, insert assms, auto)
lemma spp_step_complexity_and_termination:
assumes "p ⇒⇩s⇩s Pn"
and "finite_constructor_form_pat (mset3 p)"
and "pn ∈# Pn"
shows "measure_p pn < measure_p p"
using assms
proof (induct)
case *: (spp_simp mp mp' p)
hence pn: "pn = add_mset mp' p" by simp
let ?p = "add_mset mp p"
from * have fin: "finite_constructor_form_mp (mset2 mp)"
unfolding finite_constructor_form_pat_def by auto
from num_syms_smp_step[OF *(1) fin]
have n: "num_syms_p pn < num_syms_p ?p" unfolding pn by simp
have d: "max_depth_sort_p pn ≤ max_depth_sort_p ?p"
unfolding pn
apply simp
apply (rule max_depth_sort_le)
apply (rule mp_step_tvars)
by fact
from max_dupl_smp_step[OF *(1)] *
have m: "max_dupl_p pn ≤ max_dupl_p ?p" by simp
from d n m show ?case by (intro measure_p_num_syms, auto)
next
case *: (spp_delete mp p)
hence pn: "pn = p"
and fin: "finite_constructor_form_mp (mset2 mp)"
unfolding finite_constructor_form_pat_def by auto
let ?p = "add_mset mp p"
have d: "max_depth_sort_p pn ≤ max_depth_sort_p ?p" unfolding pn max_depth_sort_p_def by auto
from *(1) have "mp ≠ {#}" by (cases, auto)
from num_syms_mp_pos[OF fin this]
have n: "num_syms_p pn < num_syms_p ?p" unfolding pn by simp
have m: "max_dupl_p pn ≤ max_dupl_p ?p" unfolding pn by simp
from d n m show ?case by (intro measure_p_num_syms, auto)
next
case *: (spp_delete_large_sort n x ι eq mp t p)
define pd where "pd = mset (map mp [0..<Suc n])"
from *(5) have pn: "pn = p" by auto
let ?p = "p + pd"
have m: "max_dupl_p p ≤ max_dupl_p ?p" unfolding max_dupl_p_def by auto
have d: "max_depth_sort_p p ≤ max_depth_sort_p ?p" unfolding max_depth_sort_p_def by auto
have "num_syms_p p < num_syms_p p + 1" by auto
also have "… ≤ num_syms_p p + num_syms_p pd"
proof (rule add_left_mono)
have mem: "mp n ∈# pd" unfolding pd_def by auto
from *(4) have "finite_constructor_form_mp (mset2 (mp n))"
by (auto simp: finite_constructor_form_pat_def)
from *(1)[OF le_refl] num_syms_mp_pos[OF this]
have "1 ≤ num_syms_mp (mp n)" by (cases "mp n", auto)
thus "1 ≤ num_syms_p pd" using mem unfolding num_syms_p_def
by (metis One_nat_def add_eq_0_iff_both_eq_0 less_Suc0 linorder_not_less multi_member_split sum_mset.insert)
qed
finally have n: "num_syms_p p < num_syms_p ?p" unfolding num_syms_p_def by auto
from n m d have "measure_p p < measure_p (p + pd)" by (metis measure_p_num_syms)
thus ?case unfolding pn pd_def by auto
next
case *: (spp_inst x t p n)
then obtain τ where pn: "pn = image_mset (image_mset (image_mset (λt. t ⋅ τ))) p"
and τ: "τ ∈ τs n x" using τs_list by auto
from max_depth_sort_p_inst[OF *(1-2) τ *(4)] *(5)
have d: "max_depth_sort_p pn < max_depth_sort_p p" unfolding pn by auto
have "num_syms_p pn = (∑mp∈#p. num_syms_mp (image_mset (image_mset (λt. t ⋅ τ)) mp))"
unfolding num_syms_p_def pn image_mset.compositionality o_def by simp
also have "… ≤ (∑mp∈#p. num_syms_mp mp + max_dupl_mp mp * m)"
by (rule sum_mset_mono, rule num_syms_mp_τs[OF τ])
also have "… = num_syms_p p + max_dupl_p p * m"
unfolding sum_mset.distrib num_syms_p_def max_dupl_p_def sum_mset_distrib_right by auto
finally have n: "num_syms_p pn ≤ num_syms_p p + max_dupl_p p * m" .
have m: "max_dupl_p pn ≤ max_dupl_p p"
unfolding max_dupl_p_def pn image_mset.compositionality o_def
proof (rule sum_mset_mono, rule max_dupl_mp_τs[OF τ], goal_cases)
case (1 mp)
thus ?case using *(3) by fastforce
qed
from d have d: "1 + max_depth_sort_p pn ≤ max_depth_sort_p p" by auto
have "1 + measure_p pn ≤ 1 + (max_depth_sort_p pn * (max_dupl_p p * m + 1) + (num_syms_p p + max_dupl_p p * m))"
unfolding measure_p_def using n m
by (intro add_mono mult_mono, auto)
also have "… = (1 + max_depth_sort_p pn) * (max_dupl_p p * m + 1) + num_syms_p p"
by (simp add: algebra_simps)
also have "… ≤ measure_p p" unfolding measure_p_def
by (intro add_mono mult_mono d, auto)
finally show ?case by simp
next
case *: (spp_split mp x t eqc mp' p)
let ?p = "add_mset mp p"
from *(1,5) have d: "max_depth_sort_p pn ≤ max_depth_sort_p ?p"
by (auto, auto intro!: max_depth_sort_le)
from *(1,5) have m: "max_dupl_p pn ≤ max_dupl_p ?p"
by (auto, auto intro!: max_dupl_mono)
have n: "num_syms_p pn < num_syms_p ?p"
proof (cases eqc)
case add
from *(1,5) add
show ?thesis by auto (auto intro!: num_syms_lt)
next
case empty
with *(3) obtain eq2 mp2 where mp': "mp' = add_mset eq2 mp2" by (cases mp', auto)
from *(1,4) mp' have eq2: "eq2 ≠ {#}"
unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def by auto
from *(1,5) mp' eq2
show ?thesis by auto (cases eq2, auto intro!: num_syms_lt)
qed
from d n m show ?case by (intro measure_p_num_syms, auto)
qed auto
inductive_set spp_det_step_ms :: "('f,'s)simple_pat_problem_ms multiset rel" (‹⇛⇩s⇩s›)
where spp_non_det_step: "p ⇒⇩s⇩s P' ⟹ finite_constructor_form_pat (mset3 p) ⟹ (add_mset p P, P' + P) ∈ ⇛⇩s⇩s"
| spp_non_det_fail: "P ≠ {#} ⟹ (add_mset {#} P, {#{#}#}) ∈ ⇛⇩s⇩s"
| spp_fvf_succ: "(⋀ t. t ∈# ∑⇩# (image_mset ∑⇩# p) ⟹ is_Var t) ⟹ simple_pat_complete C SS (mset3 p)
⟹ (add_mset p P, P) ∈ ⇛⇩s⇩s"
| spp_fvf_fail: "(⋀ t. t ∈# ∑⇩# (image_mset ∑⇩# p) ⟹ is_Var t) ⟹ ¬ simple_pat_complete C SS (mset3 p)
⟹ finite_constructor_form_pat (mset3 p) ⟹ p ≠ {#} ⟹ (add_mset p P, {#{#}#}) ∈ ⇛⇩s⇩s"
definition spp_det_prob :: "('f,'s)simple_pat_problem_ms multiset ⇒ bool" where
"spp_det_prob P = (∀ p ∈# P. finite_constructor_form_pat (mset3 p))"
definition spp_pat_complete :: "('f,'s)simple_pat_problem_ms multiset ⇒ bool" where
"spp_pat_complete P = (∀ p ∈# P. simple_pat_complete C SS (mset3 p))"
lemma spp_det_prob_add[simp]: "spp_det_prob (add_mset p P) =
(finite_constructor_form_pat (mset3 p) ∧ spp_det_prob P)"
unfolding spp_det_prob_def by simp
lemma spp_det_prob_plus[simp]: "spp_det_prob (P + P') =
(spp_det_prob P ∧ spp_det_prob P')"
unfolding spp_det_prob_def by auto
lemma spp_det_prob_empty[simp]: "spp_det_prob {#}"
by (simp add: spp_det_prob_def)
lemma spp_det_step_ms: "(P,P') ∈ ⇛⇩s⇩s ⟹
spp_pat_complete P = spp_pat_complete P' ∧ (spp_det_prob P ⟶ spp_det_prob P')"
proof (induct rule: spp_det_step_ms.induct)
case *: (spp_non_det_step p P' P)
from spp_step_ms[OF *(1), folded spp_det_prob_def] *(2)
show ?case by (auto simp: spp_pat_complete_def)
next
case *: (spp_non_det_fail P)
show ?case using detect_unsat_spp by (simp add: finite_constructor_form_pat_def spp_pat_complete_def)
next
case (spp_fvf_succ p P)
thus ?case by (auto simp: spp_pat_complete_def)
next
case (spp_fvf_fail p P)
thus ?case using detect_unsat_spp by (simp add: finite_constructor_form_pat_def spp_pat_complete_def)
qed
lemma spp_det_steps_ms: "(P,P') ∈ ⇛⇩s⇩s⇧* ⟹
spp_pat_complete P = spp_pat_complete P' ∧ (spp_det_prob P ⟶ spp_det_prob P')"
by (induct rule: rtrancl_induct, insert spp_det_step_ms, auto)
lemma SN_spp_det_step: "SN ⇛⇩s⇩s"
proof (rule SN_subset)
show "⇛⇩s⇩s ⊆ (mult (measure measure_p))^-1"
proof (standard, simp, goal_cases)
case (1 P P')
thus ?case
proof (induct rule: spp_det_step_ms.induct)
case *: (spp_non_det_step p P' P)
from spp_step_complexity_and_termination[OF *(1-2)] show ?case
by (simp add: add_many_mult)
next
case *: (spp_non_det_fail P)
then obtain p P' where P: "P = add_mset p P'" by (cases P, auto)
show ?case unfolding P by (simp add: subset_implies_mult)
next
case (spp_fvf_succ p P)
show ?case by (simp add: subset_implies_mult)
next
case *: (spp_fvf_fail p P)
then obtain mp p' where p: "p = add_mset mp p'" by (cases p, auto)
with *(2) have "mp ≠ {#}" unfolding simple_pat_complete_def simple_match_complete_wrt_def by auto
then obtain eq mp' where mp: "mp = add_mset eq mp'" by (cases mp, auto)
with *(3,4) have eq: "eq ≠ {#}"
unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def mp p
by auto
have p: "measure_p p > 0" unfolding measure_p_def p num_syms_p_def num_syms_mp_def mp
using eq by (cases eq, auto)
have e: "measure_p {#} = 0" unfolding measure_p_def p num_syms_p_def max_depth_sort_p_def
max_dupl_p_def by auto
from p e have "({#}, p) ∈ measure measure_p" by auto
thus ?case
by (metis add_cancel_left_left add_mset_eq_single empty_not_add_mset multi_member_split
one_step_implies_mult union_single_eq_member)
qed
qed
show "SN ((mult (measure measure_p))¯)"
by (rule wf_imp_SN, simp add: wf_mult[OF wf_measure])
qed
lemma NF_spp_det_step: assumes "spp_det_prob P"
and "P ∈ NF ⇛⇩s⇩s"
shows "P = {#} ∨ P = {#{#}#}"
proof (rule ccontr)
assume contr: "¬ ?thesis"
from assms(2) have NF: "(P,P') ∈ ⇛⇩s⇩s ⟹ False" for P' by auto
from contr obtain p P2 where P: "P = add_mset p P2" and disj: "p ≠ {#} ∨ P2 ≠ {#}" by (cases P, auto)
from assms[unfolded P] have fin: "finite_constructor_form_pat (mset3 p)" by auto
show False
proof (cases "p = {#}")
case True
with disj have P2: "P2 ≠ {#}" by auto
show False
apply (rule NF)
apply (unfold P True)
by (rule spp_non_det_fail[OF P2])
next
case False
have "∄P. p ⇒⇩s⇩s P" using NF[unfolded P, OF spp_non_det_step[OF _ fin]] by auto
note fvf = normal_form_spp_step_fvf[OF fin this]
show ?thesis
proof (cases "simple_pat_complete C SS (mset3 p)")
case True
show False
by (rule NF, unfold P, rule spp_fvf_succ[OF _ True], insert fvf, auto)
next
case unsat: False
show False
by (rule NF, unfold P, rule spp_fvf_fail[OF _ unsat fin False], insert fvf, auto)
qed
qed
qed
lemma decision_procedure_spp_det:
assumes valid_input: "spp_det_prob P" and NF: "(P,Q) ∈ ⇛⇩s⇩s⇧!"
shows "Q = {#} ∧ spp_pat_complete P
∨ Q = {#{#}#} ∧ ¬ spp_pat_complete P "
proof -
from NF have steps: "(P,Q) ∈ ⇛⇩s⇩s⇧*" and Q: "Q ∈ NF ⇛⇩s⇩s" by auto
from spp_det_steps_ms[OF steps] valid_input
have equiv: "spp_pat_complete P = spp_pat_complete Q" and valid_out: "spp_det_prob Q" by auto
from NF_spp_det_step[OF valid_out Q]
show ?thesis
proof
assume "Q = {#}"
thus ?thesis unfolding equiv by (simp add: spp_pat_complete_def)
next
assume "Q = {#{#}#}"
thus ?thesis unfolding equiv using detect_unsat_spp by (simp add: spp_pat_complete_def)
qed
qed
end
end