Theory Pattern_Completeness_Multiset
section ‹A Multiset-Based Inference System to Decide Pattern Completeness›
theory Pattern_Completeness_Multiset
imports
Pattern_Completeness_Set
LP_Duality.Minimum_Maximum
Polynomial_Factorization.Missing_List
First_Order_Terms.Term_Pair_Multiset
FCF_Problem
begin
subsection ‹Definition of the Inference Rules›
text ‹We next switch to a multiset based implementation of the inference rules.
At this level, termination is proven and further, that the evaluation cannot get stuck.
The inference rules closely mimic the ones in the paper, though there is one additional
inference rule for getting rid of duplicates (which are automatically removed when working
on sets).›
type_synonym ('f,'v,'s)match_problem_mset = "(('f,nat × 's)term × ('f,'v)term) multiset"
type_synonym ('f,'v,'s)pat_problem_mset = "('f,'v,'s)match_problem_mset multiset"
type_synonym ('f,'v,'s)pats_problem_mset = "('f,'v,'s)pat_problem_mset multiset"
abbreviation mp_mset :: "('f,'v,'s)match_problem_mset ⇒ ('f,'v,'s)match_problem_set"
where "mp_mset ≡ set_mset"
abbreviation pat_mset :: "('f,'v,'s)pat_problem_mset ⇒ ('f,'v,'s)pat_problem_set"
where "pat_mset ≡ image mp_mset o set_mset"
abbreviation pats_mset :: "('f,'v,'s)pats_problem_mset ⇒ ('f,'v,'s)pats_problem_set"
where "pats_mset ≡ image pat_mset o set_mset"
abbreviation (input) bottom_mset :: "('f,'v,'s)pats_problem_mset" where "bottom_mset ≡ {# {#} #}"
context pattern_completeness_context
begin
text ‹A terminating version of @{const P_step_set} working on multisets
that also treats the transformation on a more modular basis.›
definition subst_match_problem_mset :: "('f,nat × 's)subst ⇒ ('f,'v,'s)match_problem_mset ⇒ ('f,'v,'s)match_problem_mset" where
"subst_match_problem_mset τ = image_mset (subst_left τ)"
definition subst_pat_problem_mset :: "('f,nat × 's)subst ⇒ ('f,'v,'s)pat_problem_mset ⇒ ('f,'v,'s)pat_problem_mset" where
"subst_pat_problem_mset τ = image_mset (subst_match_problem_mset τ)"
definition τs_list :: "nat ⇒ nat × 's ⇒ ('f,nat × 's)subst list" where
"τs_list n x = map (τc n x) (Cl (snd x))"
inductive mp_step_mset :: "('f,'v,'s)match_problem_mset ⇒ ('f,'v,'s)match_problem_mset ⇒ bool" (infix ‹→⇩m› 50)where
match_decompose: "(f,length ts) = (g,length ls)
⟹ add_mset (Fun f ts, Fun g ls) mp →⇩m mp + mset (zip ts ls)"
| match_match: "x ∉ ⋃ (vars ` snd ` set_mset mp)
⟹ add_mset (t, Var x) mp →⇩m mp"
| match_duplicate: "add_mset pair (add_mset pair mp) →⇩m add_mset pair mp"
| match_decompose': "mp + mp' →⇩m (∑(t, l) ∈# mp. mset (zip (args t) (map Var ys))) + mp'"
if "⋀ t l. (t,l) ∈# mp ⟹ l = Var y ∧ root t = Some (f,n)"
"⋀ t l. (t,l) ∈# mp' ⟹ y ∉ vars l"
"lvars_disj_mp ys (mp_mset (mp + mp'))" "length ys = n"
"size mp ≥ 2"
improved
inductive match_fail :: "('f,'v,'s)match_problem_mset ⇒ bool" where
match_clash: "(f,length ts) ≠ (g,length ls)
⟹ match_fail (add_mset (Fun f ts, Fun g ls) mp)"
| match_clash': "Conflict_Clash s t ⟹ match_fail (add_mset (s, Var x) (add_mset (t, Var x) mp))"
| match_clash_sort: "𝒯(C,𝒱) s ≠ 𝒯(C,𝒱) t ⟹ match_fail (add_mset (s, Var x) (add_mset (t, Var x) mp))"
inductive pp_step_mset :: "('f,'v,'s)pat_problem_mset ⇒ ('f,'v,'s)pats_problem_mset ⇒ bool"
(infix ‹⇒⇩m› 50) where
pat_remove_pp: "add_mset {#} pp ⇒⇩m {#}"
| pat_simp_mp: "mp_step_mset mp mp' ⟹ add_mset mp pp ⇒⇩m {# (add_mset mp' pp) #}"
| pat_remove_mp: "match_fail mp ⟹ add_mset mp pp ⇒⇩m {# pp #}"
| pat_instantiate: "tvars_disj_pp {n ..< n+m} (pat_mset (add_mset mp pp)) ⟹
(Var x, l) ∈ mp_mset mp ∧ is_Fun l ∨
¬ improved ∧ (s,Var y) ∈ mp_mset mp ∧ (t,Var y) ∈ mp_mset mp ∧ Conflict_Var s t x ∧ ¬ inf_sort (snd x)
⟹
add_mset mp pp ⇒⇩m mset (map (λ τ. subst_pat_problem_mset τ (add_mset mp pp)) (τs_list n x))"
| pat_inf_var_conflict: "Ball (pat_mset pp) inf_var_conflict ⟹ pp ≠ {#}
⟹ Ball (tvars_pat (pat_mset pp')) (λ x. ¬ inf_sort (snd x)) ⟹
(¬ improved ⟹ pp' = {#})
⟹ pp + pp' ⇒⇩m {# pp' #}"
inductive pp_nd_step_mset :: "('f,'v,'s)pat_problem_mset ⇒ ('f,'v,'s)pat_problem_mset ⇒ bool"
(infix ‹⇒⇩n⇩d› 50) where
"pp ⇒⇩m P ⟹ p' ∈# P ⟹ pp ⇒⇩n⇩d p'"
inductive P_step_mset :: "('f,'v,'s)pats_problem_mset ⇒ ('f,'v,'s)pats_problem_mset ⇒ bool"
(infix ‹⇛⇩m› 50)where
P_failure: "add_mset {#} P ≠ bottom_mset ⟹ add_mset {#} P ⇛⇩m bottom_mset"
| P_simp_pp: "pp ⇒⇩m pp' ⟹ add_mset pp P ⇛⇩m pp' + P"
text ‹The relation (encoded as predicate) is finally wrapped in a set›
definition P_step :: "(('f,'v,'s)pats_problem_mset × ('f,'v,'s)pats_problem_mset)set" (‹⇛›) where
"⇛ = {(P,P'). P ⇛⇩m P'}"
subsection ‹The evaluation cannot get stuck›
lemmas subst_defs =
subst_pat_problem_mset_def
subst_pat_problem_set_def
subst_match_problem_mset_def
subst_match_problem_set_def
lemma pat_mset_fresh_vars:
"∃ n. tvars_disj_pp {n..<n + m} (pat_mset p)"
proof -
define p' where "p' = pat_mset p"
define V where "V = fst ` ⋃ (vars ` (fst ` ⋃ p'))"
have "finite V" unfolding V_def p'_def by auto
define n where "n = Suc (Max V)"
{
fix mp t l
assume "mp ∈ p'" "(t,l) ∈ mp"
hence sub: "fst ` vars t ⊆ V" unfolding V_def by force
{
fix x
assume "x ∈ fst ` vars t"
with sub have "x ∈ V" by auto
with ‹finite V› have "x ≤ Max V" by simp
also have "… < n" unfolding n_def by simp
finally have "x < n" .
}
hence "fst ` vars t ∩ {n..<n + m} = {}" by force
}
thus ?thesis unfolding tvars_disj_pp_def p'_def[symmetric]
by (intro exI[of _ n] ballI, force)
qed
lemma mp_mset_in_pat_mset: "mp ∈# pp ⟹ mp_mset mp ∈ pat_mset pp"
by auto
lemma mp_step_mset_cong:
assumes "(→⇩m)⇧*⇧* mp mp'"
shows "(add_mset (add_mset mp p) P, add_mset (add_mset mp' p) P) ∈ ⇛⇧*"
using assms
proof induct
case (step mp' mp'')
from P_simp_pp[OF pat_simp_mp[OF step(2), of p], of P]
have "(add_mset (add_mset mp' p) P, add_mset (add_mset mp'' p) P) ∈ P_step"
unfolding P_step_def by auto
with step(3)
show ?case by simp
qed auto
lemma mp_step_mset_vars: assumes "mp →⇩m mp'"
shows "tvars_match (mp_mset mp) ⊇ tvars_match (mp_mset mp')"
using assms
proof induct
case *: (match_decompose' mp y f n mp' ys)
{
let ?mset = "mset :: _ ⇒ ('f,'v,'s)match_problem_mset"
fix x
assume "x ∈ tvars_match (mp_mset ((∑(t, l)∈#mp. ?mset (zip (args t) (map Var ys)))))"
from this[unfolded tvars_match_def, simplified]
obtain t l ti yi where tl: "(t,l) ∈# mp" and tiyi: "(ti,yi) ∈# ?mset (zip (args t) (map Var ys))"
and x: "x ∈ vars ti"
by auto
from *(1)[OF tl] obtain ts where l: "l = Var y" and t: "t = Fun f ts" and lts: "length ts = n"
by (cases t, auto)
from tiyi[unfolded t] have "ti ∈ set ts"
using set_zip_leftD by fastforce
with x t have "x ∈ vars t" by auto
hence "x ∈ tvars_match (mp_mset mp)" using tl unfolding tvars_match_def by auto
}
thus ?case unfolding tvars_match_def by force
qed (auto simp: tvars_match_def set_zip)
lemma mp_step_mset_steps_vars: assumes "(→⇩m)⇧*⇧* mp mp'"
shows "tvars_match (mp_mset mp) ⊇ tvars_match (mp_mset mp')"
using assms by (induct, insert mp_step_mset_vars, auto)
end
context pattern_completeness_context_with_assms begin
lemma pat_empty_or_trans_or_finite_constr_form:
fixes p :: "('f,'v,'s) pat_problem_mset"
assumes inf: "improved ⟹ infinite (UNIV :: 'v set)" and wf: "wf_pat (pat_mset p)"
shows "p = {#} ∨ (∃ ps. p ⇒⇩m ps) ∨ (improved ∧ finite_constr_form_pat C (pat_mset p))"
proof (cases "p = {#}")
case True
thus ?thesis by auto
next
case pne: False
from pat_mset_fresh_vars obtain n where fresh: "tvars_disj_pp {n..<n + m} (pat_mset p)" by blast
show ?thesis
proof (cases "{#} ∈# p")
case True
then obtain p' where "p = add_mset {#} p'" by (rule mset_add)
with pat_remove_pp show ?thesis by auto
next
case empty_p: False
show ?thesis
proof (cases "∃ mp s t. mp ∈# p ∧ (s,t) ∈# mp ∧ is_Fun t")
case True
then obtain mp s t where mp: "mp ∈# p" and "(s,t) ∈# mp" and "is_Fun t" by auto
then obtain g ts where mem: "(s,Fun g ts) ∈# mp" by (cases t, auto)
from mp obtain p' where p: "p = add_mset mp p'" by (rule mset_add)
from mem obtain mp' where mp: "mp = add_mset (s, Fun g ts) mp'" by (rule mset_add)
show ?thesis
proof (cases s)
case s: (Fun f ss)
from pat_simp_mp[OF match_decompose, of f ss] pat_remove_mp[OF match_clash, of f ss]
show ?thesis unfolding p mp s by blast
next
case (Var x)
from Var mem obtain l where "(Var x, l) ∈# mp ∧ is_Fun l" by auto
from pat_instantiate[OF fresh[unfolded p] disjI1[OF this]]
show ?thesis unfolding p by auto
qed
next
case False
hence rhs_vars: "⋀ mp s l. mp ∈# p ⟹ (s,l) ∈# mp ⟹ is_Var l" by auto
let ?single_var = "(∃ mp t x. add_mset (t,Var x) mp ∈# p ∧ x ∉ ⋃ (vars ` snd ` set_mset mp))"
let ?duplicate = "(∃ mp pair. add_mset pair (add_mset pair mp) ∈# p)"
show ?thesis
proof (cases "?single_var ∨ ?duplicate")
case True
thus ?thesis
proof
assume ?single_var
then obtain mp t x where mp: "add_mset (t,Var x) mp ∈# p" and x: "x ∉ ⋃ (vars ` snd ` set_mset mp)"
by auto
from mp obtain p' where "p = add_mset (add_mset (t,Var x) mp) p'" by (rule mset_add)
with pat_simp_mp[OF match_match[OF x]] show ?thesis by auto
next
assume ?duplicate
then obtain mp pair where "add_mset pair (add_mset pair mp) ∈# p" (is "?dup ∈# p") by auto
from mset_add[OF this] obtain p' where
p: "p = add_mset ?dup p'" .
from pat_simp_mp[OF match_duplicate[of pair]] show ?thesis unfolding p by auto
qed
next
case False
hence ndup: "¬ ?duplicate" and nsvar: "¬ ?single_var" by auto
{
fix mp s x
assume mpp: "mp ∈# p" and sx: "(s, Var x) ∈# mp"
from mpp obtain p' where p: "p = add_mset mp p'" by (rule mset_add)
from sx obtain mp' where mp: "mp = add_mset (s, Var x) mp'" by (rule mset_add)
from nsvar[simplified, rule_format, OF mpp[unfolded mp]]
obtain t l where "(t,l) ∈# mp'" and "x ∈ vars (snd (t,l))" by force
with rhs_vars[OF mpp, of t l] have tx: "(t,Var x) ∈# mp'" unfolding mp by auto
then obtain mp'' where mp': "mp' = add_mset (t, Var x) mp''" by (rule mset_add)
from ndup[simplified, rule_format] mpp have "s ≠ t" unfolding mp mp' by auto
hence "∃ t mp'. mp = add_mset (s, Var x) (add_mset (t, Var x) mp') ∧ s ≠ t" unfolding mp mp' by auto
} note twoX = this
{
fix mp
assume mpp: "mp ∈# p"
with empty_p have mp_e: "mp ≠ {#}" by auto
obtain s l where sl: "(s,l) ∈# mp" using mp_e by auto
from rhs_vars[OF mpp sl] sl obtain x where sx: "(s, Var x) ∈# mp" by (cases l, auto)
from twoX[OF mpp sx]
have "∃ s t x mp'. mp = add_mset (s, Var x) (add_mset (t, Var x) mp') ∧ s ≠ t" by blast
} note two = this
show ?thesis
proof (cases "∃ mp s t x. add_mset (s, Var x) (add_mset (t, Var x) mp) ∈# p ∧ Conflict_Clash s t")
case True
then obtain mp s t x where
mp: "add_mset (s, Var x) (add_mset (t, Var x) mp) ∈# p" (is "?mp ∈# _") and conf: "Conflict_Clash s t"
by blast
from pat_remove_mp[OF match_clash'[OF conf, of x mp]]
show ?thesis using mset_add[OF mp] by metis
next
case no_clash: False
show ?thesis
proof (cases improved)
case not_impr: False
show ?thesis
proof (cases "∃ mp s t x y. add_mset (s, Var x) (add_mset (t, Var x) mp) ∈# p ∧ Conflict_Var s t y ∧ ¬ inf_sort (snd y)")
case True
from True obtain mp s t x y where
mp: "add_mset (s, Var x) (add_mset (t, Var x) mp) ∈# p" (is "?mp ∈# _") and conf: "Conflict_Var s t y" and y: "¬ inf_sort (snd y)"
by blast
from mp obtain p' where p: "p = add_mset ?mp p'" by (rule mset_add)
let ?mp = "add_mset (s, Var x) (add_mset (t, Var x) mp)"
from pat_instantiate[OF _ disjI2, of n ?mp p' s x t y, folded p, OF fresh]
show ?thesis using y conf not_impr by auto
next
case no_non_inf: False
have "∃ ps. p + {#} ⇒⇩m ps"
proof (intro exI, rule pat_inf_var_conflict[OF _ pne], intro ballI)
fix mp
assume mp: "mp ∈ pat_mset p"
then obtain mp' where mp': "mp' ∈# p" and mp: "mp = mp_mset mp'" by auto
from two[OF mp']
obtain s t x mp''
where mp'': "mp' = add_mset (s, Var x) (add_mset (t, Var x) mp'')" and diff: "s ≠ t" by auto
from conflicts(3)[OF diff] obtain y where "Conflict_Clash s t ∨ Conflict_Var s t y" by auto
with no_clash mp'' mp' have conf: "Conflict_Var s t y" by force
with no_non_inf mp'[unfolded mp''] have inf: "inf_sort (snd y)" by blast
show "inf_var_conflict mp" unfolding inf_var_conflict_def mp mp''
apply (rule exI[of _ s], rule exI[of _ t])
apply (intro exI[of _ x] exI[of _ y])
using insert inf conf by auto
qed (auto simp: tvars_pat_def)
thus ?thesis by auto
qed
next
case impr: True
define exVar where "exVar mp = (∀ x t. (t, Var x) ∈# mp ⟶ (∃ y. (Var y, Var x) ∈# mp))"
for mp :: "('f,'v,'s)match_problem_mset"
show ?thesis
proof (cases "∀ mp ∈# p. exVar mp")
case False
then obtain mp where mpp: "mp ∈# p" and "¬ exVar mp" by auto
from this[unfolded exVar_def] obtain s x where sx: "(s, Var x) ∈# mp" and
no_var: "⋀ y. (Var y, Var x) ∉# mp"
by auto
from no_var have allFun: "(t, Var x) ∈# mp ⟹ is_Fun t" for t by (cases t, auto)
from sx no_var obtain f ss where s: "s = Fun f ss" by (cases s, auto)
from twoX[OF mpp sx] obtain t mp' where stx: "mp = add_mset (s, Var x) (add_mset (t, Var x) mp')"
and st: "s ≠ t" by auto
let ?Var = "Var :: 'v ⇒ ('f, 'v)term"
let ?f = "λ tl. snd tl = ?Var x"
define mp1 where "mp1 = filter_mset ?f mp"
have size: "size mp1 ≥ 2" unfolding mp1_def stx by auto
define mp2 where "mp2 = filter_mset (Not o ?f) mp"
{
fix t l
assume "(t,l) ∈# mp2"
hence "(t,l) ∈# mp" and "l ≠ Var x" unfolding mp2_def by auto
from rhs_vars[OF mpp this(1)] this(2) have "x ∉ vars l" by (cases l, auto)
} note mp2 = this
define n where "n = length ss"
with s have rtS: "root s = Some (f,n)" unfolding n_def by auto
from stx have smp: "(s, Var x) ∈# mp" by auto
{
fix t l
assume "(t,l) ∈# mp1"
from this[unfolded mp1_def]
have l: "l = Var x" and tmp: "(t,Var x) ∈# mp" by auto
from allFun tmp obtain g ts where t: "t = Fun g ts" by (cases t, auto)
{
assume rtT: "root t ≠ Some (f,n)"
hence st: "s ≠ t" using rtS by auto
from rtS rtT have clash: "Conflict_Clash s t" unfolding s t
by (auto simp: conflicts.simps)
from smp tmp st have "∃ mp'. mp = add_mset (s, Var x) (add_mset (t, Var x) mp')"
by (metis insert_noteq_member multi_member_split prod.inject)
with clash no_clash mpp have False by blast
}
hence "l = Var x ∧ root t = Some (f,n)" using l by auto
} note mp1 = this
define VV where "VV = ⋃ (vars ` snd ` mp_mset mp)"
have "finite VV" by (auto simp: VV_def)
with inf[OF impr] have "infinite (UNIV - VV)" by auto
then obtain Ys where Ys: "Ys ⊆ UNIV - VV" "card Ys = n" "finite Ys"
by (meson infinite_arbitrarily_large)
from Ys(2-3) obtain ys where ys: "distinct ys" "length ys = n" "set ys = Ys"
by (metis distinct_card finite_distinct_list)
with Ys have dist: "VV ∩ set ys = {}" by auto
have disj: "lvars_disj_mp ys (mp_mset mp)" "length ys = n"
unfolding lvars_disj_mp_def using ys dist unfolding VV_def by auto
have "mp = mp1 + mp2" unfolding mp1_def mp2_def by simp
from match_decompose'[of mp1 x _ _ mp2, folded this, OF mp1 mp2 disj size impr]
obtain mp' where "mp →⇩m mp'" by fast
from pat_simp_mp[OF this] mpp
show ?thesis by (metis mset_add)
next
case exVar: True
show ?thesis
proof (cases "∀ mp ∈# p. (∀ t l. (t,l) ∈# mp ⟶ is_Var l ∧ 𝒯(C,𝒱) t ≠ None)")
case False
then obtain mp s l where mpp: "mp ∈# p" and sl: "(s,l) ∈# mp" and
ch: "¬ is_Var l ∨ 𝒯(C,𝒱) s = None"
by auto
from rhs_vars[OF mpp sl] obtain x where l: "l = Var x" by auto
with ch have None: "𝒯(C,𝒱) s = None" by auto
from None obtain f ss where s: "s = Fun f ss" by (cases s, auto)
from sl l have sx: "(s, Var x) ∈# mp" by auto
from exVar[unfolded exVar_def, rule_format, OF mpp sx] obtain y
where "(Var y, Var x) ∈# mp" by auto
with sx obtain mp' where "mp = add_mset (Var y, Var x) (add_mset (s, Var x) mp')"
unfolding s by (metis insert_noteq_member is_FunI is_VarI mset_add prod.inject)
from match_clash_sort[of "Var y" s x mp', unfolded None, folded this]
have "match_fail mp" by auto
from pat_remove_mp[OF this] mpp
show ?thesis by (metis mset_add)
next
case constr_form: True
define finmp where "finmp mp = (∀ t l. (t, l) ∈# mp ⟶ (∃ ι. finite_sort C ι ∧ t : ι in 𝒯(C,𝒱)))"
for mp :: "('f,'v,'s)match_problem_mset"
show ?thesis
proof (cases "∀ mp ∈# p. finmp mp")
case True
{
fix mp
assume mp: "mp ∈# p"
hence "finmp mp" using True by auto
with constr_form mp have "finite_constr_form_mp C (mp_mset mp)"
unfolding finmp_def by (simp add: finite_constr_form_mp_def)
}
thus ?thesis using impr unfolding finite_constr_form_pat_def by auto
next
case someInf: False
show ?thesis
proof (cases "∃ s t x mp. mp ∈# p ∧ (s, Var x) ∈# mp ∧ (t, Var x) ∈# mp ∧ 𝒯(C,𝒱) s ≠ 𝒯(C,𝒱) t")
case True
then obtain s t x mp where mp: "mp ∈# p" and s: "(s, Var x) ∈# mp" and t: "(t, Var x) ∈# mp"
and sort_clash: "𝒯(C,𝒱) s ≠ 𝒯(C,𝒱) t"
by auto
from sort_clash have st: "s ≠ t" by auto
with s t obtain mp' where "mp = add_mset (s, Var x) (add_mset (t, Var x) mp')"
by (metis insert_noteq_member mset_add prod.inject)
from match_clash_sort[of s t x mp', folded this] sort_clash
have "match_fail mp" by auto
from pat_remove_mp[OF this] show ?thesis using mp
by (metis mset_add)
next
case False
hence noSortClash: "⋀ s t x mp. mp ∈# p ⟹ (s, Var x) ∈# mp ⟹ (t, Var x) ∈# mp ⟹ 𝒯(C,𝒱) s = 𝒯(C,𝒱) t"
by blast
define p1 where "p1 = filter_mset (Not o finmp) p"
define p2 where "p2 = filter_mset finmp p"
have p: "p = p1 + p2" unfolding p1_def p2_def by simp
have "p ⇒⇩m {#p2#}" unfolding p
proof (rule pat_inf_var_conflict[of p1 p2]; (intro ballI, clarsimp)?)
{
from someInf obtain mp where "mp ∈# p" and "¬ finmp mp" by auto
hence "mp ∈# p1" unfolding p1_def by auto
thus "p1 ≠ {#}" by auto
}
{
fix mp
assume "mp ∈# p1"
from this[unfolded p1_def] have nfin: "¬ finmp mp" and mp: "mp ∈# p" by auto
from nfin[unfolded finmp_def, simplified]
obtain t l where tl: "(t, l) ∈# mp" and inf: "⋀ ι. finite_sort C ι ⟹ ¬ t : ι in 𝒯(C,𝒱)"
by auto
from constr_form[rule_format, OF mp tl] have l: "is_Var l" and sorted: "𝒯(C,𝒱) t ≠ None"
by auto
from l obtain x where l: "l = Var x" by auto
from sorted obtain ι where sorted: "t : ι in 𝒯(C,𝒱)" by (cases "𝒯(C,𝒱) t", auto simp: hastype_def)
from inf sorted have inf: "¬ finite_sort C ι" by auto
from tl l have tx: "(t, Var x) ∈# mp" by auto
from exVar[unfolded exVar_def, rule_format, OF mp tx] obtain y
where yx: "(Var y, Var x) ∈# mp" by auto
have y: "Var y : snd y in 𝒯(C,𝒱)" by simp
from noSortClash[OF mp yx tx] sorted y inf
have inf: "¬ finite_sort C (snd y)" by (auto simp: hastype_def)
from wf[unfolded wf_pat_def wf_match_def tvars_match_def, simplified, rule_format, OF mp]
yx
have "snd y ∈ S" by force
with inf have inf: "inf_sort (snd y)" using inf_sort by auto
from twoX[OF mp yx]
obtain t mp' where mp': "mp = add_mset (Var y, Var x) (add_mset (t, Var x) mp')"
and yt: "Var y ≠ t" by auto
from mp' have tx: "(t, Var x) ∈# mp" by auto
from noSortClash[OF mp yx tx] y
have t: "t : snd y in 𝒯(C,𝒱)" by (auto simp: hastype_def)
obtain cs where conf: "conflicts (Var y) t = Some cs" "y ∈ set cs"
using t yt by (cases t, auto simp: conflicts.simps)
show "inf_var_conflict (mp_mset mp)"
unfolding inf_var_conflict_def
by (intro exI conjI, rule yx, rule tx, insert inf conf, auto)
}
{
fix x
assume x: "x ∈ tvars_pat (mp_mset ` set_mset p2)" and inf: "inf_sort (snd x)"
from x[unfolded tvars_pat_def tvars_match_def]
obtain mp t l where mp: "mp ∈# p2" and tl: "(t,l) ∈# mp" and x: "x ∈ vars t" by auto
from mp[unfolded p2_def] have fin: "finmp mp" and mp: "mp ∈# p" by auto
from wf[unfolded wf_pat_def wf_match_def, simplified, rule_format, OF mp] x tl
have xS: "snd x ∈ S" unfolding tvars_match_def by auto
from inf_sort[OF this] inf have inf: "¬ finite_sort C (snd x)" by auto
from constr_form[rule_format, OF mp tl] obtain y where l: "l = Var y"
and sorted: "𝒯(C,𝒱) t ≠ None" by auto
note ty = tl[unfolded l]
from fin[unfolded finmp_def, rule_format, OF tl] obtain ι where
fin: "finite_sort C ι" and sorted: "t : ι in 𝒯(C,𝒱)" by auto
from sorted x fin have "finite_sort C (snd x)"
proof (induct)
case (Fun f ss σs τ)
then obtain s where s: "s ∈ set ss" and x: "x ∈ vars s" by auto
from s obtain i where i: "i < length ss" and si: "s = ss ! i" by (auto simp: set_conv_nth)
from Fun(2) si i have "s : σs ! i in 𝒯(C,𝒱)"
and "i < length σs" unfolding list_all2_conv_all_nth by auto
hence "σs ! i ∈ set σs" by auto
from finite_arg_sort[OF Fun(5,1) this] have "finite_sort C (σs ! i)" by auto
with Fun(3) x show "finite_sort C (snd x)" unfolding si using i
unfolding list_all2_conv_all_nth by auto
qed auto
with inf have False by simp
}
thus "⋀ x ι. (x, ι) ∈ tvars_pat (mp_mset ` set_mset p2) ⟹ inf_sort ι ⟹ False"
by auto
qed (insert impr, auto)
thus ?thesis by auto
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed
context
assumes non_improved: "¬ improved"
begin
lemma pat_empty_or_trans: "wf_pat (pat_mset p) ⟹ p = {#} ∨ (∃ ps. p ⇒⇩m ps)"
using pat_empty_or_trans_or_finite_constr_form[of p] non_improved by auto
text ‹Pattern problems just have two normal forms:
empty set (solvable) or bottom (not solvable)›
theorem P_step_NF:
assumes wf: "wf_pats (pats_mset P)" and NF: "P ∈ NF ⇛"
shows "P ∈ {{#}, bottom_mset}"
proof (rule ccontr)
assume nNF: "P ∉ {{#}, bottom_mset}"
from NF have NF: "¬ (∃ Q. P ⇛⇩m Q)" unfolding P_step_def by blast
from nNF obtain p P' where P: "P = add_mset p P'"
using multiset_cases by auto
with wf have "wf_pat (pat_mset p)" by (auto simp: wf_pats_def)
with pat_empty_or_trans
obtain ps where "p = {#} ∨ p ⇒⇩m ps" by auto
with P_simp_pp[of p ps] NF
have "p = {#}" unfolding P by auto
from P_failure[of P'] P this nNF NF show False by blast
qed
end
context
assumes improved: "improved"
and inf: "infinite (UNIV :: 'v set)"
begin
lemma pat_empty_or_trans_or_fvf:
fixes p :: "('f,'v,'s) pat_problem_mset"
assumes "wf_pat (pat_mset p)"
shows "p = {#} ∨ (∃ ps. p ⇒⇩m ps) ∨ finite_constr_form_pat C (pat_mset p)"
using assms pat_empty_or_trans_or_finite_constr_form[of p, OF inf] by auto
text ‹Normal forms only consist of finite-var-form pattern problems›
theorem P_step_NF_fvf:
assumes wf: "wf_pats (pats_mset P)"
and NF: "(P::('f,'v,'s) pats_problem_mset) ∈ NF ⇛"
and p: "p ∈# P"
shows "finite_constr_form_pat C (pat_mset p)"
proof (rule ccontr)
assume nfvf: "¬ ?thesis"
from wf p have wfp: "wf_pat (pat_mset p)" by (auto simp: wf_pats_def)
from mset_add[OF p] obtain P' where P: "P = add_mset p P'" by auto
from NF have NF: "¬ (∃ Q. P ⇛⇩m Q)" unfolding P_step_def by blast
from pat_empty_or_trans_or_fvf[OF wfp] nfvf
obtain ps where "p = {#} ∨ p ⇒⇩m ps" by auto
with P_simp_pp[of p ps] NF
have "p = {#}" unfolding P by auto
with nfvf show False unfolding finite_constr_form_pat_def by auto
qed
end
end
subsection ‹Termination›
text ‹A measure to count the number of function symbols of the first argument that don't
occur in the second argument›
fun fun_diff :: "('f,'v)term ⇒ ('f,'w)term ⇒ nat" where
"fun_diff l (Var x) = num_funs l"
| "fun_diff (Fun g ls) (Fun f ts) = (if f = g ∧ length ts = length ls then
sum_list (map2 fun_diff ls ts) else 0)"
| "fun_diff l t = 0"
lemma fun_diff_Var[simp]: "fun_diff (Var x) t = 0"
by (cases t, auto)
lemma add_many_mult: "(⋀ y. y ∈# N ⟹ (y,x) ∈ R) ⟹ (N + M, add_mset x M) ∈ mult R"
by (metis add.commute add_mset_add_single multi_member_last multi_self_add_other_not_self one_step_implies_mult)
lemma fun_diff_num_funs: "fun_diff l t ≤ num_funs l"
proof (induct l t rule: fun_diff.induct)
case (2 f ls g ts)
show ?case
proof (cases "f = g ∧ length ts = length ls")
case True
have "sum_list (map2 fun_diff ls ts) ≤ sum_list (map num_funs ls)"
by (intro sum_list_mono2, insert True 2, (force simp: set_zip)+)
with 2 show ?thesis by auto
qed auto
qed auto
lemma fun_diff_subst: "fun_diff l (t ⋅ σ) ≤ fun_diff l t"
proof (induct l arbitrary: t)
case l: (Fun f ls)
show ?case
proof (cases t)
case t: (Fun g ts)
show ?thesis unfolding t using l by (auto intro: sum_list_mono2)
next
case t: (Var x)
show ?thesis unfolding t using fun_diff_num_funs[of "Fun f ls"] by auto
qed
qed auto
lemma fun_diff_num_funs_lt: assumes t': "t' = Fun c cs"
and "is_Fun l"
shows "fun_diff l t' < num_funs l"
proof -
from assms obtain g ls where l: "l = Fun g ls" by (cases l, auto)
show ?thesis
proof (cases "c = g ∧ length cs = length ls")
case False
thus ?thesis unfolding t' l by auto
next
case True
have "sum_list (map2 fun_diff ls cs) ≤ sum_list (map num_funs ls)"
apply (rule sum_list_mono2; (intro impI)?)
subgoal using True by auto
subgoal for i using True by (auto intro: fun_diff_num_funs)
done
thus ?thesis unfolding t' l using True by auto
qed
qed
lemma sum_union_le_nat: "sum (f :: 'a ⇒ nat) (A ∪ B) ≤ sum f A + sum f B"
by (metis finite_Un le_iff_add sum.infinite sum.union_inter zero_le)
lemma sum_le_sum_list_nat: "sum f (set xs) ≤ (sum_list (map f xs) :: nat)"
proof (induct xs)
case (Cons x xs)
thus ?case
by (cases "x ∈ set xs", auto simp: insert_absorb)
qed auto
lemma bdd_above_has_Maximum_nat: "bdd_above (A :: nat set) ⟹ A ≠ {} ⟹ has_Maximum A"
unfolding has_Maximum_def
by (meson Max_ge Max_in bdd_above_nat)
fun syms_term :: "('f,'v)term ⇒ ('v + 'f)multiset" where
"syms_term (Var x) = {# Inl x #}"
| "syms_term (Fun f ts) = add_mset (Inr f) (sum_mset (image_mset syms_term (mset ts)))"
lemma replicate_mset_add: "replicate_mset (n + m) a = replicate_mset n a + replicate_mset m a"
by (metis repeat_mset_distrib repeat_mset_replicate_mset)
lemma syms_term_subst: "syms_term (t ⋅ subst x s) + replicate_mset (count (syms_term t) (Inl x)) (Inl x)
= syms_term t + repeat_mset (count (syms_term t) (Inl x)) (syms_term s)" (is "?l t = ?r t")
proof (induct t)
case (Var y)
show ?case unfolding subst_def by auto
next
case (Fun f ts)
have "?case ⟷
(∑⇩# (image_mset syms_term {#sa ⋅ subst x s. sa ∈# mset ts#}) +
replicate_mset (count (∑⇩# (image_mset syms_term (mset ts))) (Inl x)) (Inl x) =
∑⇩# (image_mset syms_term (mset ts)) +
repeat_mset (count (∑⇩# (image_mset syms_term (mset ts))) (Inl x)) (syms_term s))"
(is "_ ⟷ ?ls ts = ?rs ts") by simp
also have "…" using Fun
proof (induct ts)
case (Cons t ts)
have "?rs (t # ts) = ?r t + ?rs ts" by auto
also have "… = ?l t + ?ls ts" using Cons by auto
also have "… = ?ls (t # ts)" by (simp add: replicate_mset_add)
finally show ?case ..
qed auto
finally show ?case by simp
qed
definition num_syms :: "('f,'v)term ⇒ nat" where
"num_syms t = size (syms_term t)"
lemma num_syms_pos[simp]: "num_syms t > 0"
unfolding num_syms_def by (cases t, auto)
lemma num_syms_0[simp]: "num_syms t ≠ 0"
unfolding num_syms_def by (cases t, auto)
lemma num_syms_subst: "num_syms (t ⋅ subst x s) = num_syms t + count (syms_term t) (Inl x) * (num_syms s - 1)"
proof -
let ?cx = "count (syms_term t) (Inl x)"
from arg_cong[OF syms_term_subst[of t x s], of size]
have "num_syms (t ⋅ subst x s) + ?cx = num_syms t + ?cx * num_syms s"
unfolding size_union num_syms_def by simp
from arg_cong[OF this, of "λ n . n - ?cx"]
have "num_syms (t ⋅ subst x s) = num_syms t + ?cx * num_syms s - ?cx" by auto
also have "… = num_syms t + ?cx * (num_syms s - 1)"
using num_syms_pos[of s] by (cases "num_syms s", auto)
finally show ?thesis .
qed
lemma num_syms_Fun[simp]: "num_syms (Fun f ts) = Suc (sum_list (map num_syms ts))"
unfolding num_syms_def
by (simp, induct ts, auto)
context pattern_completeness_context_with_assms
begin
lemma τs_list: "set (τs_list n x) = τs n x"
unfolding τs_list_def τs_def using Cl by auto
abbreviation (input) sum_ms :: "('a ⇒ nat) ⇒ 'a multiset ⇒ nat" where
"sum_ms f ms ≡ sum_mset (image_mset f ms)"
definition meas_diff :: "('f,'v,'s)pat_problem_mset ⇒ nat" where
"meas_diff = sum_ms (sum_ms (λ (t,l). fun_diff l t))"
definition max_size :: "'s ⇒ nat" where
"max_size s = (if s ∈ S ∧ ¬ inf_sort s then Maximum (size ` {t. t : s in 𝒯(C)}) else 0)"
definition meas_finvars :: "('f,'v,'s)pat_problem_mset ⇒ nat" where
"meas_finvars = sum_ms (λ mp. sum (max_size o snd) (tvars_match (mp_mset mp)))"
definition meas_symbols :: "('f,'v,'s)pat_problem_mset ⇒ nat" where
"meas_symbols = sum_ms (sum_ms (λ (t,l). num_syms t))"
definition rel_pat :: "('f,'v,'s)pat_problem_mset rel" (‹≺›) where
"(≺) = inv_image ({(x, y). x < y} <*lex*> {(x, y). x < y} <*lex*> {(x, y). x < y})
(λ mp. (meas_diff mp, meas_finvars mp, meas_symbols mp))"
abbreviation gt_rel_pat (infix ‹≻› 50) where
"pp ≻ pp' ≡ (pp',pp) ∈ ≺"
definition meas_setsize :: "('f,'v,'s)pat_problem_mset ⇒ nat" where
"meas_setsize p = sum_ms (sum_ms (λ _. 1)) p + size p"
definition rel_pat' :: "('f,'v,'s)pat_problem_mset rel" where
"rel_pat' = inv_image ({(x, y). x < y} <*lex*> {(x, y). x < y} <*lex*> {(x, y). x < y} <*lex*> {(x, y). x < y})
(λ mp. (meas_diff mp, meas_finvars mp, meas_symbols mp, meas_setsize mp))"
definition rel_pats :: "(('f,'v,'s)pats_problem_mset × ('f,'v,'s)pats_problem_mset)set" (‹≺mul›) where
"≺mul = mult rel_pat'"
abbreviation gt_rel_pats (infix ‹≻mul› 50) where
"P ≻mul P' ≡ (P',P) ∈ ≺mul"
lemma wf_rel_pat: "wf ≺"
unfolding rel_pat_def
by (intro wf_inv_image wf_lex_prod wf_less)
lemma wf_rel_pat': "wf rel_pat'"
unfolding rel_pat'_def
by (intro wf_inv_image wf_lex_prod wf_less)
lemma wf_rel_pats: "wf ≺mul"
unfolding rel_pats_def
by (intro wf_inv_image wf_mult wf_rel_pat')
lemma rel_pat_sub_rel_pat': "rel_pat ⊆ rel_pat'"
unfolding rel_pat_def rel_pat'_def by auto
lemma tvars_match_fin:
"finite (tvars_match (mp_mset mp))"
unfolding tvars_match_def by auto
lemmas meas_def = meas_finvars_def meas_diff_def meas_symbols_def meas_setsize_def
lemma tvars_match_mono: "mp ⊆# mp' ⟹ tvars_match (mp_mset mp) ⊆ tvars_match (mp_mset mp')"
unfolding tvars_match_def
by (intro image_mono subset_refl set_mset_mono UN_mono)
lemma meas_finvars_mono: assumes "tvars_match (mp_mset mp) ⊆ tvars_match (mp_mset mp')"
shows "meas_finvars {#mp#} ≤ meas_finvars {#mp'#}"
using tvars_match_fin[of mp'] assms
unfolding meas_def by (auto intro: sum_mono2)
lemma rel_mp_sub: "{# add_mset p mp#} ≻ {# mp #}"
proof -
let ?mp' = "add_mset p mp"
have "mp ⊆# ?mp'" by auto
from meas_finvars_mono[OF tvars_match_mono[OF this]]
show ?thesis unfolding meas_def rel_pat_def by (cases p, auto)
qed
lemma rel_mp_mp_step_mset:
fixes mp :: "('f,'v,'s) match_problem_mset"
assumes "mp →⇩m mp'"
shows "{#mp#} ≻ {#mp'#}"
using assms
proof cases
case *: (match_decompose f ts g ls mp'')
have "meas_finvars {#mp'#} ≤ meas_finvars {#mp#}"
proof (rule meas_finvars_mono)
show "tvars_match (mp_mset mp') ⊆ tvars_match (mp_mset mp)"
unfolding tvars_match_def * using *(3) by (auto simp: set_zip set_conv_nth)
qed
moreover
have id: "(case case x of (x, y) ⇒ (y, x) of (t, l) ⇒ f t l) = (case x of (a,b) ⇒ f b a)" for
x :: "('f, 'v) Term.term × ('f, nat × 's) Term.term" and f :: "_ ⇒ _ ⇒ nat"
by (cases x, auto)
have "meas_diff {#mp'#} ≤ meas_diff {#mp#}"
unfolding meas_def * using *(3)
by (auto simp: sum_mset_sum_list[symmetric] zip_commute[of ts ls] image_mset.compositionality o_def id)
moreover have "length ts = length ls ⟹ (∑(t, l)∈#mset (zip ts ls). num_syms t) ≤ sum_list (map num_syms ts)"
by (induct ts ls rule: list_induct2, auto)
hence "meas_symbols {#mp'#} < meas_symbols {#mp#}"
unfolding meas_def * using *(3)
by (auto simp: sum_mset_sum_list)
ultimately show ?thesis unfolding rel_pat_def by auto
next
case *: (match_decompose' mp1 y f n mp2 ys)
let ?Var = "Var :: 'v ⇒ ('f, 'v) term"
have "meas_diff {#mp'#} ≤ meas_diff {#mp#}
⟷ (∑(ti, yi)∈#(∑(t, l)∈#mp1. mset (zip (args t) (map ?Var ys))). fun_diff yi ti)
≤ (∑(t, l)∈#mp1. fun_diff l t)" (is "_ ⟷ ?sum ≤ _")
unfolding * meas_diff_def by simp
also have "?sum = 0"
by (intro sum_mset.neutral ballI, auto simp: set_zip)
finally have "meas_diff {#mp'#} ≤ meas_diff {#mp#}" by simp
moreover
have "meas_finvars {#mp'#} ≤ meas_finvars {#mp#}"
proof (rule meas_finvars_mono)
show "tvars_match (mp_mset mp') ⊆ tvars_match (mp_mset mp)"
unfolding tvars_match_def * using *(3,6)
by (auto simp: set_zip set_conv_nth)
(metis case_prod_conv nth_mem option.simps(3) root.elims term.sel(4) term.set_intros(4))
qed
moreover
have "meas_symbols {#mp'#} < meas_symbols {#mp#}"
proof -
from ‹2 ≤ size mp1› obtain T L MP where mp1: "mp1 = add_mset (T,L) MP"
by (cases mp1; force)
from *(3)[of T L] mp1 obtain TS where id: "T = Fun f TS" "L = Var y" and lTS: "length TS = n"
by (cases T, auto)
have aux: "length ts = length ls ⟹
(∑(t, l)∈#mset (zip ts ls). num_syms t) ≤ sum_list (map num_syms ts)"
for ts :: "('f, nat × 's)term list" and ls :: "('f,'v)term list"
by (induct ts ls rule: list_induct2, auto)
have "meas_symbols {#mp'#} < meas_symbols {#mp#} ⟷
((∑(t, l)∈#mset (zip TS (map ?Var ys)). num_syms t) +
(∑(ti, yi)∈#(∑(t, l)∈#MP. mset (zip (args t) (map ?Var ys))). num_syms ti)
≤ (sum_list (map num_syms TS) + (∑(t, l)∈#MP. num_syms t)))"
(is "_ ⟷ (?a + ?b ≤ ?c + ?d)")
unfolding meas_symbols_def * mp1 id by (simp add: sum_mset_sum_list less_Suc_eq_le)
also have …
proof (rule add_le_mono)
show "?a ≤ ?c" using aux lTS ‹length ys = n› by auto
from *(3) mp1 have "(t, l) ∈# MP ⟹ l = Var y ∧ root t = Some (f, n)" for l t by auto
thus "?b ≤ ?d"
proof (induct MP)
case (add pair MP)
obtain t l where pair: "pair = (t,l)" by force
from add(2)[of t l] obtain ts where id: "l = Var y" "t = Fun f ts" and lts: "length ts = n"
by (cases t, auto simp: pair)
from add(1)[OF add(2)]
have IH: "(∑(ti, yi)∈#(∑(t, l)∈#MP. mset (zip (args t) (map ?Var ys))). num_syms ti)
≤ (∑(t, l)∈#MP. num_syms t)" by auto
from IH aux[of ts, unfolded lts, of "map ?Var ys"] ‹length ys = n›
show ?case unfolding pair id by auto
qed auto
qed
finally show "meas_symbols {#mp'#} < meas_symbols {#mp#}" .
qed
ultimately show ?thesis unfolding rel_pat_def by auto
next
case *: (match_match x t)
show ?thesis unfolding *
by (rule rel_mp_sub)
next
case *: (match_duplicate pair mp)
show ?thesis unfolding *
by (rule rel_mp_sub)
qed
lemma sum_ms_image: "sum_ms f (image_mset g ms) = sum_ms (f o g) ms"
by (simp add: multiset.map_comp)
lemma meas_diff_subst_le: "meas_diff (subst_pat_problem_mset τ p) ≤ meas_diff p"
unfolding meas_def subst_match_problem_set_def subst_defs subst_left_def
unfolding sum_ms_image o_def
apply (rule sum_mset_mono, rule sum_mset_mono)
apply clarify
unfolding map_prod_def split id_apply
by (rule fun_diff_subst)
lemma meas_sub: assumes sub: "p' ⊆# p"
shows "meas_diff p' ≤ meas_diff p"
"meas_finvars p' ≤ meas_finvars p"
"meas_symbols p' ≤ meas_symbols p"
proof -
from sub obtain p'' where p: "p = p' + p''" by (metis subset_mset.less_eqE)
show "meas_diff p' ≤ meas_diff p" "meas_finvars p' ≤ meas_finvars p" "meas_symbols p' ≤ meas_symbols p"
unfolding meas_def p by auto
qed
lemma meas_sub_rel_pat: assumes sub: "p' ⊂# p"
shows "(p', p) ∈ rel_pat'"
proof -
from sub obtain x p'' where p: "p = add_mset x p' + p''"
by (metis multi_nonempty_split subset_mset.lessE union_mset_add_mset_left union_mset_add_mset_right)
hence lt: "meas_setsize p' < meas_setsize p" unfolding meas_def by auto
from sub have "p' ⊆# p" by auto
from lt meas_sub[OF this]
show ?thesis unfolding rel_pat'_def by auto
qed
lemma max_size_term_of_sort: assumes sS: "s ∈ S" and inf: "¬ inf_sort s"
shows "∃ t. t : s in 𝒯(C) ∧ max_size s = size t ∧ (∀ t'. t' : s in 𝒯(C) ⟶ size t' ≤ size t)"
proof -
let ?set = "λ s. size ` {t. t : s in 𝒯(C)}"
have m: "max_size s = Maximum (?set s)" unfolding o_def max_size_def using inf sS by auto
from inf inf_sort_not_bdd[OF sS] have "bdd_above (?set s)" by auto
moreover have "?set s ≠ {}" by (auto intro!: sorts_non_empty sS)
ultimately have "has_Maximum (?set s)" by (rule bdd_above_has_Maximum_nat)
from has_MaximumD[OF this, folded m] show ?thesis by auto
qed
lemma max_size_max: assumes sS: "s ∈ S"
and inf: "¬ inf_sort s"
and sort: "t : s in 𝒯(C)"
shows "size t ≤ max_size s"
using max_size_term_of_sort[OF sS inf] sort by auto
lemma finite_sort_size: assumes c: "c : map snd vs → s in C"
and inf: "¬ inf_sort s"
shows "sum (max_size o snd) (set vs) < max_size s"
proof -
from c have vsS: "insert s (set (map snd vs)) ⊆ S" using C_sub_S
by (metis (mono_tags))
hence sS: "s ∈ S" by auto
let ?m = "max_size s"
show ?thesis
proof (cases "∃ v ∈ set vs. inf_sort (snd v)")
case True
{
fix v
assume "v ∈ set vs"
with vsS have v: "snd v ∈ S" by auto
note sorts_non_empty[OF this]
}
hence "∀ v. ∃ t. v ∈ set vs ⟶ t : snd v in 𝒯(C)" by auto
from choice[OF this] obtain t where
t: "⋀ v. v ∈ set vs ⟹ t v : snd v in 𝒯(C)" by blast
from True vsS obtain vl where vl: "vl ∈ set vs" and vlS: "snd vl ∈ S" and inf_vl: "inf_sort (snd vl)" by auto
note nbdd = inf_sort_not_bdd[OF vlS, THEN iffD2, OF inf_vl]
from not_bdd_above_natD[OF nbdd, of ?m] t[OF vl]
obtain tl where
tl: "tl : snd vl in 𝒯(C)" and large: "?m ≤ size tl" by fastforce
let ?t = "Fun c (map (λ v. if v = vl then tl else t v) vs)"
have "?t : s in 𝒯(C)"
by (intro Fun_hastypeI[OF c] list_all2_map_map, insert tl t, auto)
from max_size_max[OF sS inf this]
have False using large split_list[OF vl] by auto
thus ?thesis ..
next
case False
{
fix v
assume v: "v ∈ set vs"
with False have inf: "¬ inf_sort (snd v)" by auto
from vsS v have "snd v ∈ S" by auto
from max_size_term_of_sort[OF this inf]
have "∃ t. t : snd v in 𝒯(C) ∧ size t = max_size (snd v)" by auto
}
hence "∀ v. ∃ t. v ∈ set vs ⟶ t : snd v in 𝒯(C) ∧ size t = max_size (snd v)" by auto
from choice[OF this] obtain t where
t: "v ∈ set vs ⟹ t v : snd v in 𝒯(C) ∧ size (t v) = max_size (snd v)" for v by blast
let ?t = "Fun c (map t vs)"
have "?t : s in 𝒯(C)"
by (intro Fun_hastypeI[OF c] list_all2_map_map, insert t, auto)
from max_size_max[OF sS inf this]
have "size ?t ≤ max_size s" .
have "sum (max_size ∘ snd) (set vs) = sum (size o t) (set vs)"
by (rule sum.cong[OF refl], unfold o_def, insert t, auto)
also have "… ≤ sum_list (map (size o t) vs)"
by (rule sum_le_sum_list_nat)
also have "… ≤ size_list (size o t) vs" by (induct vs, auto)
also have "… < size ?t" by simp
also have "… ≤ max_size s" by fact
finally show ?thesis .
qed
qed
lemma add_mset_rel_pat: assumes sub: "mp ≠ {#}"
shows "add_mset mp p ≻ p"
proof -
from sub obtain t l mp' where mp: "mp = add_mset (t,l) mp'" by (cases mp, auto)
hence lt: "meas_symbols p < meas_symbols (add_mset mp p)" unfolding meas_def by auto
from lt meas_sub[of p "add_mset mp p"]
show ?thesis unfolding rel_pat_def by auto
qed
lemma rel_pp_step_mset:
fixes p :: "('f,'v,'s) pat_problem_mset"
assumes "p ⇒⇩m ps"
and "p' ∈# ps"
shows "p ≻ p'"
using assms
proof induct
case *: (pat_simp_mp mp mp' p)
hence p': "p' = add_mset mp' p" by auto
from rel_mp_mp_step_mset[OF *(1)]
show ?case unfolding p' rel_pat_def meas_def by auto
next
case *: (pat_remove_mp mp p)
hence p': "p' = p" by auto
from *(1) have "mp ≠ {#}" by (cases, auto)
show ?case unfolding p' by (rule add_mset_rel_pat, fact)
next
case *: (pat_instantiate n mp p x l s y t)
from *(2) have "∃ s t. (s,t) ∈# mp ∧ (s = Var x ∧ is_Fun t
∨ (x ∈ vars s ∧ ¬ inf_sort (snd x)))"
proof
assume *: "¬ improved ∧ (s, Var y) ∈# mp ∧ (t, Var y) ∈# mp ∧ Conflict_Var s t x ∧ ¬ inf_sort (snd x)"
hence "Conflict_Var s t x" and "¬ inf_sort (snd x)" by auto
from conflicts(4)[OF this(1)] this(2) *
show ?thesis by auto
qed auto
then obtain s t where st: "(s,t) ∈# mp" and choice: "s = Var x ∧ is_Fun t ∨ x ∈ vars s ∧ ¬ inf_sort (snd x)"
by auto
let ?p = "add_mset mp p"
let ?s = "snd x"
from *(3) τs_list
obtain τ where τ: "τ ∈ τs n x" and p': "p' = subst_pat_problem_mset τ ?p" by auto
let ?tau_mset = "subst_pat_problem_mset τ :: ('f,'v,'s) pat_problem_mset ⇒ _"
let ?tau = "subst_match_problem_mset τ :: ('f,'v,'s) match_problem_mset ⇒ _"
from τ[unfolded τs_def τc_def List.maps_def]
obtain c sorts where c: "c : sorts → ?s in C" and tau: "τ = subst x (Fun c (map Var (zip [n..<n + length sorts] sorts)))"
by auto
with C_sub_S have sS: "?s ∈ S" and sorts: "set sorts ⊆ S" by auto
define vs where "vs = zip [n..<n + length sorts] sorts"
have τ: "τ = subst x (Fun c (map Var vs))" unfolding tau vs_def by auto
have "snd ` vars (τ y) ⊆ insert (snd y) S" for y
using sorts unfolding tau by (auto simp: subst_def set_zip set_conv_nth)
hence vars_sort: "(a,b) ∈ vars (τ y) ⟹ b ∈ insert (snd y) S" for a b y by fastforce
from st obtain mp' where mp: "mp = add_mset (s,t) mp'" by (rule mset_add)
from choice have "?p ≻ ?tau_mset ?p"
proof
assume "s = Var x ∧ is_Fun t"
then obtain f ts where s: "s = Var x" and t: "t = Fun f ts" by (cases t, auto)
have "meas_diff (?tau_mset ?p) =
meas_diff (?tau_mset (add_mset mp' p)) + fun_diff t (s ⋅ τ)"
unfolding meas_def subst_defs subst_left_def mp by simp
also have "… ≤ meas_diff (add_mset mp' p) + fun_diff t (τ x)" using meas_diff_subst_le[of τ] s by auto
also have "… < meas_diff (add_mset mp' p) + fun_diff t s"
proof (rule add_strict_left_mono)
have "fun_diff t (τ x) < num_funs t"
unfolding tau subst_simps fun_diff.simps
by (rule fun_diff_num_funs_lt[OF refl], auto simp: t)
thus "fun_diff t (τ x) < fun_diff t s" by (auto simp: s t)
qed
also have "… = meas_diff ?p" unfolding mp meas_def by auto
finally show ?thesis unfolding rel_pat_def by auto
next
assume "x ∈ vars s ∧ ¬ inf_sort (snd x)"
hence x: "x ∈ vars s" and inf: "¬ inf_sort (snd x)" by auto
from meas_diff_subst_le[of τ]
have fd: "meas_diff p' ≤ meas_diff ?p" unfolding p' .
have "meas_finvars (?tau_mset ?p) = meas_finvars (?tau_mset {#mp#}) + meas_finvars (?tau_mset p)"
unfolding subst_defs meas_def by auto
also have "… < meas_finvars {#mp#} + meas_finvars p"
proof (rule add_less_le_mono)
have vars_τ_var: "vars (τ y) = (if x = y then set vs else {y})" for y unfolding τ subst_def by auto
have vars_τ: "vars (t ⋅ τ) = vars t - {x} ∪ (if x ∈ vars t then set vs else {})" for t
unfolding vars_term_subst image_comp o_def vars_τ_var by auto
have tvars_match_subst: "tvars_match (mp_mset (?tau mp)) =
tvars_match (mp_mset mp) - {x} ∪ (if x ∈ tvars_match (mp_mset mp) then set vs else {})" for mp
unfolding subst_defs subst_left_def tvars_match_def
by (auto simp:vars_τ split: if_splits prod.split)
have id1: "meas_finvars (?tau_mset {#mp#}) = (∑x∈ tvars_match (mp_mset (?tau mp)). max_size (snd x))" for mp
unfolding meas_def subst_defs by auto
have id2: "meas_finvars {#mp#} = (∑x∈tvars_match (mp_mset mp). max_size (snd x))"
for mp :: "('f,'v,'s) match_problem_mset"
unfolding meas_def subst_defs by simp
have eq: "x ∉ tvars_match (mp_mset mp) ⟹ meas_finvars (?tau_mset {# mp #}) = meas_finvars {#mp#}" for mp
unfolding id1 id2 by (rule sum.cong[OF _ refl], auto simp: tvars_match_subst)
{
fix mp :: "('f,'v,'s) match_problem_mset"
assume xmp: "x ∈ tvars_match (mp_mset mp)"
let ?mp = "(mp_mset mp)"
have fin: "finite (tvars_match ?mp)" by (rule tvars_match_fin)
define Mp where "Mp = tvars_match ?mp - {x}"
from xmp have 1: "tvars_match (mp_mset (?tau mp)) = set vs ∪ Mp"
unfolding tvars_match_subst Mp_def by auto
from xmp have 2: "tvars_match ?mp = insert x Mp" and xMp: "x ∉ Mp" unfolding Mp_def by auto
from fin have fin: "finite Mp" unfolding Mp_def by auto
have "meas_finvars (?tau_mset {# mp #}) = sum (max_size ∘ snd) (set vs ∪ Mp)" (is "_ = sum ?size _")
unfolding id1 id2 using 1 by auto
also have "… ≤ sum ?size (set vs) + sum ?size Mp" by (rule sum_union_le_nat)
also have "… < ?size x + sum ?size Mp"
proof -
have sS: "?s ∈ S" by fact
have sorts: "sorts = map snd vs" unfolding vs_def by (intro nth_equalityI, auto)
have "sum ?size (set vs) < ?size x"
using finite_sort_size[OF c[unfolded sorts] inf] by auto
thus ?thesis by auto
qed
also have "… = meas_finvars {#mp#}" unfolding id2 2 using fin xMp by auto
finally have "meas_finvars (?tau_mset {# mp #}) < meas_finvars {#mp#}" .
} note less = this
have le: "meas_finvars (?tau_mset {# mp #}) ≤ meas_finvars {#mp#}" for mp
using eq[of mp] less[of mp] by linarith
show "meas_finvars (?tau_mset {#mp#}) < meas_finvars {#mp#}" using x
by (intro less, unfold mp, force simp: tvars_match_def)
show "meas_finvars (?tau_mset p) ≤ meas_finvars p"
unfolding subst_pat_problem_mset_def meas_finvars_def sum_ms_image o_def
apply (rule sum_mset_mono)
subgoal for mp using le[of mp] unfolding meas_finvars_def o_def subst_defs by auto
done
qed
also have "… = meas_finvars ?p" unfolding p' meas_def by simp
finally show ?thesis using fd unfolding rel_pat_def p' by auto
qed
thus ?case unfolding p' .
next
case *: (pat_remove_pp p)
thus ?case by auto
next
case *: (pat_inf_var_conflict pp pp')
hence p': "p' = pp'" by auto
have "p' ⊆# pp + pp'" unfolding p' by auto
note mono = meas_sub[OF this]
from *(2) obtain mp pp2 where pp: "pp = add_mset mp pp2" by (cases pp, auto)
with *(1) have "inf_var_conflict (mp_mset mp)" by auto
hence "mp ≠ {#}" unfolding inf_var_conflict_def by auto
hence "meas_symbols p' < meas_symbols (pp + pp')" unfolding p' pp using num_syms_pos
by (cases mp, auto simp: meas_symbols_def)
thus ?case using mono by (auto simp: rel_pat_def)
qed
text ‹finally: the transformation is terminating w.r.t. @{term "(≻mul)"}›
lemma rel_P_trans:
assumes "P ⇛⇩m P'"
shows "P ≻mul P'"
using assms
proof induct
case *: (P_failure P)
from * have "P ≠ {#}" by auto
then obtain p' P' where P: "P = add_mset p' P'" by (cases P, auto)
show ?case unfolding P unfolding rel_pats_def
by (simp add: subset_implies_mult)
next
case *: (P_simp_pp p ps P)
from set_mp[OF rel_pat_sub_rel_pat'] rel_pp_step_mset[OF *]
show ?case unfolding rel_pats_def by (metis add_many_mult)
qed
text ‹termination of the multiset based implementation›
lemma nd_step_decrease: assumes "p ⇒⇩n⇩d q"
shows "p ≻ q"
proof -
from assms
obtain P where "p ⇒⇩m P" and "q ∈# P"
by cases auto
from rel_pp_step_mset[OF this]
show "p ≻ q" .
qed
theorem SN_nd_pstep: "SN {(p,q). p ⇒⇩n⇩d q}"
proof (rule SN_subset[of "{(p,q). p ≻ q}"], rule wf_imp_SN)
show "wf ({(p, q). p ≻ q}¯)" using wf_rel_pat
by (simp add: converse_unfold)
qed (insert nd_step_decrease, auto)
theorem SN_P_step: "SN ⇛"
proof -
have sub: "⇛ ⊆ ≺mul^-1"
using rel_P_trans unfolding P_step_def by auto
show ?thesis
apply (rule SN_subset[OF _ sub])
apply (rule wf_imp_SN)
using wf_rel_pats by simp
qed
subsection ‹Partial Correctness via Refinement›
text ‹Obtain partial correctness via a simulation property, that the multiset-based
implementation is a refinement of the set-based implementation.›
lemma mp_step_cong: "mp1 →⇩s mp2 ⟹ mp1 = mp1' ⟹ mp2 = mp2' ⟹ mp1' →⇩s mp2'" by auto
lemma mp_step_mset_mp_trans: "mp →⇩m mp' ⟹ mp_mset mp →⇩s mp_mset mp'"
proof (induct mp mp' rule: mp_step_mset.induct)
case *: (match_decompose f ts g ls mp)
show ?case by (rule mp_step_cong[OF mp_decompose], insert *, auto)
next
case *: (match_match x mp t)
show ?case by (rule mp_step_cong[OF mp_match], insert *, auto)
next
case (match_duplicate pair mp)
show ?case by (rule mp_step_cong[OF mp_identity], auto)
next
case *: (match_decompose' mp y f n mp' ys)
show ?case by (rule mp_step_cong[OF mp_decompose'[OF *(1,2) *(3)[unfolded set_mset_union] *(4,6)]], auto)
qed
lemma mp_fail_cong: "mp_fail mp ⟹ mp = mp' ⟹ mp_fail mp'" by auto
lemma match_fail_mp_fail: "match_fail mp ⟹ mp_fail (mp_mset mp)"
proof (induct mp rule: match_fail.induct)
case *: (match_clash f ts g ls mp)
show ?case by (rule mp_fail_cong[OF mp_clash], insert *, auto)
next
case *: (match_clash' s t x mp)
show ?case by (rule mp_fail_cong[OF mp_clash'], insert *, auto)
next
case *: (match_clash_sort s t x mp)
show ?case by (rule mp_fail_cong[OF mp_clash_sort], insert *, auto)
qed
lemma pp_step_set_cong: "P ⇒⇩s Q ⟹ P = P' ⟹ Q = Q' ⟹ P' ⇒⇩s Q'" by auto
lemma p_step_mset_imp_set: assumes "p ⇒⇩m Q"
shows "pat_mset p ⇒⇩s pats_mset Q"
using assms
proof -
note conv = o_def image_mset_union image_empty image_mset_add_mset Un_empty_left
set_mset_add_mset_insert set_mset_union image_Un image_insert set_mset_empty
set_mset_mset set_image_mset
set_map image_comp insert_is_Un[symmetric]
show ?thesis using assms(1) unfolding conv
proof induction
case (pat_remove_pp p)
show ?case unfolding conv using pp_success by auto
next
case *: (pat_simp_mp mp mp' p)
from pp_simp_mp[OF mp_step_mset_mp_trans[OF *]]
show ?case by auto
next
case *: (pat_remove_mp mp p)
from pp_remove_mp[OF match_fail_mp_fail[OF *]]
show ?case by simp
next
case *: (pat_instantiate n mp p x l s y t)
from *(2) have "x ∈ tvars_match (mp_mset mp)"
using conflicts(4)[of s t x] unfolding tvars_match_def
by (auto intro!:term.set_intros(3))
hence x: "x ∈ tvars_pat (pat_mset (add_mset mp p))" unfolding tvars_pat_def
using *(2) by auto
show ?case unfolding conv τs_list
apply (rule pp_step_set_cong[OF pp_instantiate[OF *(1) x]])
by (unfold conv subst_defs set_map image_comp, auto)
next
case *: (pat_inf_var_conflict pp pp')
from pp_inf_var_conflict[OF *(1), of "pat_mset pp'"]
have "pat_mset (pp + pp') ⇒⇩s {pat_mset pp'}"
using * by (auto simp: tvars_pat_def image_Un)
thus ?case by auto
qed
qed
lemma pp_step_mset_pcorrect: "p ⇒⇩m P' ⟹ wf_pat (pat_mset p) ⟹
pat_complete C (pat_mset p) = pats_complete C (pats_mset P')"
by (rule pp_step_pcorrect[OF p_step_mset_imp_set])
lemma P_step_mset_imp_set: assumes "P ⇛⇩m Q"
shows "pats_mset P ⇛⇩s pats_mset Q"
using assms
proof (induction)
case *: (P_failure P)
from *(1) show ?case
by (induct, auto intro: P_fail)
next
case (P_simp_pp pp pp' P)
from P_simp[OF p_step_mset_imp_set[OF this]]
show ?case by (simp add: image_Un)
qed
lemma P_step_pp_trans: assumes "(P,Q) ∈ ⇛"
shows "pats_mset P ⇛⇩s pats_mset Q"
by (rule P_step_mset_imp_set, insert assms, unfold P_step_def, auto)
theorem P_step_pcorrect: assumes wf: "wf_pats (pats_mset P)" and step: "(P,Q) ∈ ⇛"
shows "wf_pats (pats_mset Q) ∧ (pats_complete C (pats_mset P) = pats_complete C (pats_mset Q))"
proof -
note step = P_step_pp_trans[OF step]
from P_step_set_pcorrect[OF step] P_step_set_wf[OF step] wf
show ?thesis by auto
qed
corollary P_steps_pcorrect: assumes wf: "wf_pats (pats_mset P)"
and step: "(P,Q) ∈ ⇛⇧*"
shows "wf_pats (pats_mset Q) ∧ (pats_complete C (pats_mset P) ⟷ pats_complete C (pats_mset Q))"
using step by induct (insert wf P_step_pcorrect, auto)
lemma nd_step_to_P_step: assumes "p ⇒⇩n⇩d q"
shows "∃ Q. add_mset p P ⇛⇩m add_mset q Q"
using assms
proof cases
case (1 Q)
then show ?thesis using P_simp_pp[of p Q P]
by (metis mset_add union_iff)
qed
lemma nd_steps_to_P_steps: assumes "(⇒⇩n⇩d)⇧*⇧* p q"
shows "∃ Q. (⇛⇩m)⇧*⇧* (add_mset p P) (add_mset q Q)"
using assms
proof (induct arbitrary: P)
case *: (step y z)
from nd_step_to_P_step[OF *(2)] *(3) show ?case
by (meson r_into_rtranclp rtranclp_trans)
qed auto
lemma P_step_to_nd_step: assumes "P ⇛⇩m Q"
and "q ∈# Q" shows "∃ p ∈# P. (⇒⇩n⇩d)⇧=⇧= p q"
using assms(1)
proof cases
case *: (P_simp_pp pp P' P)
with assms have "q ∈# P' ∨ q ∈# P" by auto
thus ?thesis
proof
assume "q ∈# P"
thus ?thesis using * by auto
next
assume "q ∈# P'"
with * have "pp ⇒⇩n⇩d q" by (intro pp_nd_step_mset.intros)
with * show ?thesis by auto
qed
qed (insert assms, auto)
lemma P_steps_to_nd_steps: assumes "(⇛⇩m)⇧*⇧* P Q"
and "q ∈# Q" shows "∃ p ∈# P. (⇒⇩n⇩d)⇧*⇧* p q"
using assms
proof (induct arbitrary: q)
case *: (step Q R r)
from P_step_to_nd_step[OF *(2,4)]
obtain q where "q ∈# Q" and "(⇒⇩n⇩d)⇧=⇧= q r" by auto
from *(3)[OF this(1)] this(2) show ?case
by (metis r_into_rtranclp rtranclp_reflclp rtranclp_trans)
qed auto
lemma nd_steps_fail_iff_Psteps_fail: "(⇒⇩n⇩d)⇧*⇧* p {#} ⟷ (⇛⇩m)⇧*⇧* {#p#} bottom_mset"
proof
assume "(⇒⇩n⇩d)⇧*⇧* p {#}"
from nd_steps_to_P_steps[OF this] obtain P
where steps: "(⇛⇩m)⇧*⇧* {#p#} (add_mset {#} P)" by auto
from P_failure[of P] have "(⇛⇩m)⇧*⇧* (add_mset {#} P) bottom_mset"
by (cases "add_mset {#} P = bottom_mset", auto)
with steps show "(⇛⇩m)⇧*⇧* {#p#} bottom_mset" by simp
next
assume "(⇛⇩m)⇧*⇧* {#p#} bottom_mset"
from P_steps_to_nd_steps[OF this, of "{#}"]
show "(⇒⇩n⇩d)⇧*⇧* p {#}" by auto
qed
text ‹Gather all results for the multiset-based implementation:
decision procedure on well-formed inputs (termination was proven before)›
theorem P_step:
assumes non_improved: "¬ improved"
and wf: "wf_pats (pats_mset P)" and NF: "(P,Q) ∈ ⇛⇧!"
shows "Q = {#} ∧ pats_complete C (pats_mset P)
∨ Q = bottom_mset ∧ ¬ pats_complete C (pats_mset P) "
proof -
from NF have steps: "(P,Q) ∈ ⇛^*" and NF: "Q ∈ NF P_step" by auto
from P_steps_pcorrect[OF wf steps]
have wf: "wf_pats (pats_mset Q)" and
sound: "pats_complete C (pats_mset P) = pats_complete C (pats_mset Q)"
by blast+
from P_step_NF[OF non_improved wf NF] have "Q ∈ {{#},bottom_mset}" .
thus ?thesis unfolding sound by auto
qed
theorem nd_pstep:
assumes non_improved: "¬ improved"
and wf: "wf_pat (pat_mset p)"
shows "¬ pat_complete C (pat_mset p) ⟷ (⇒⇩n⇩d)⇧*⇧* p {#}"
proof -
from wf have wf: "wf_pats (pats_mset {#p#})" by (auto simp: wf_pats_def)
have "¬ pat_complete C (pat_mset p) ⟷ ({#p#}, bottom_mset) ∈ ⇛⇧*"
proof -
{
assume "({#p#}, {#{#}#}) ∈ ⇛⇧*"
from P_steps_pcorrect[OF wf this]
have "¬ pat_complete C (pat_mset p)"
by auto
} note bot = this
from SN_P_step obtain Q where NF: "({#p#}, Q) ∈ ⇛⇧!"
by (metis SN_def SN_on_imp_normalizability)
from P_step[OF non_improved wf NF]
have res: "Q = {#} ∧ pat_complete C (pat_mset p) ∨ Q = {#{#}#} ∧ ¬ pat_complete C (pat_mset p)" by auto
hence pcQ: "pat_complete C (pat_mset p) = (Q = {#})" by auto
from NF have "({#p#},Q) ∈ ⇛⇧*" by auto
thus ?thesis unfolding pcQ using res bot by auto
qed
also have "… ⟷ (⇛⇩m)⇧*⇧* ({#p#}) bottom_mset"
unfolding P_step_def by (meson Enum.rtranclp_rtrancl_eq)
also have "… ⟷ (⇒⇩n⇩d)⇧*⇧* p {#}"
unfolding nd_steps_fail_iff_Psteps_fail ..
finally show ?thesis by auto
qed
theorem P_step_improved:
fixes P :: "('f,'v,'s) pats_problem_mset"
assumes improved
and inf: "infinite (UNIV :: 'v set)"
and wf: "wf_pats (pats_mset P)" and NF: "(P,Q) ∈ ⇛⇧!"
shows "pats_complete C (pats_mset P) ⟷ pats_complete C (pats_mset Q)"
"p ∈# Q ⟹ finite_constr_form_pat C (pat_mset p)"
proof -
from NF have steps: "(P,Q) ∈ ⇛^*" and NF: "Q ∈ NF P_step" by auto
note * = P_steps_pcorrect[OF wf steps]
from *
show "pats_complete C (pats_mset P) = pats_complete C (pats_mset Q)" ..
from * have wfQ: "wf_pats (pats_mset Q)" by auto
from P_step_NF_fvf[OF ‹improved› inf this NF]
show "p ∈# Q ⟹ finite_constr_form_pat C (pat_mset p)" .
qed
end
end