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
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 ∨
(s,Var y) ∈ mp_mset mp ∧ (t,Var y) ∈ mp_mset mp ∧ Conflict_Var s t x ∧ ¬ inf_sort (snd x)
∧ (improved ⟶ s = Var x ∧ is_Fun t) ⟹
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 pat_fail :: "('f,'v,'s)pat_problem_mset ⇒ bool" where
pat_empty: "pat_fail {#}"
inductive P_step_mset :: "('f,'v,'s)pats_problem_mset ⇒ ('f,'v,'s)pats_problem_mset ⇒ bool"
(infix ‹⇛⇩m› 50)where
P_failure: "pat_fail pp ⟹ add_mset pp P ≠ bottom_mset ⟹ add_mset pp 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_fail_or_trans_or_finite_var_form:
fixes p :: "('f,'v,'s) pat_problem_mset"
assumes "improved ⟹ infinite (UNIV :: 'v set)" and wf: "wf_pat (pat_mset p)"
shows "pat_fail p ∨ (∃ ps. p ⇒⇩m ps) ∨ (improved ∧ finite_var_form_pat C (pat_mset p))"
proof (cases "p = {#}")
case True
with pat_empty show ?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
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 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 "∃ s t x mp'. mp = add_mset (s, Var x) (add_mset (t, Var x) mp') ∧ s ≠ t" unfolding mp mp' by auto
} 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 "∃ 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
show ?thesis
proof (cases improved)
case not_impr: False
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 impr: True
have "(pat_fail p ∨ (∃ps. p ⇒⇩m ps)) ∨ weak_finite_var_form_pat (pat_mset p)"
proof (cases "weak_finite_var_form_pat (pat_mset p)")
case False
from this[unfolded weak_finite_var_form_pat_def] obtain mp
where mp: "mp ∈# p" and nmp: "¬ weak_finite_var_form_match (mp_mset mp)" by auto
from mset_add[OF mp] obtain p' where p': "p = add_mset mp p'" by auto
from rhs_vars[OF mp] have "((∀(t, l)∈#mp. ∃y. l = Var y) ∧ b) = b" for b
by force
note nmp = nmp[unfolded weak_finite_var_form_match_def this]
from this[simplified] obtain f ss y where
s: "(Fun f ss, Var y) ∈# mp" and
violation: "((∀x. (Var x, Var y) ∈# mp ⟶ ¬ inf_sort (snd x)) ∨
(∃t g n. (t, Var y) ∈# mp ∧ root t = Some (g, n) ∧ root t ≠ Some (f, length ss)))"
(is "?A ∨ ?B")
by force
let ?s = "Fun f ss"
let ?n = "length ss"
show ?thesis
proof (cases ?B)
case True
then obtain t g n where t: "(t, Var y) ∈# mp" "root t = Some (g, n)" "root t ≠ Some (f, ?n)"
by auto
from t have st: "(?s, Var y) ≠ (t, Var y)" by (cases t, auto)
define mp' where "mp' = mp - {#(?s, Var y),(t, Var y)#}"
from s t(1) st have "mp = add_mset (?s, Var y) (add_mset (t, Var y) mp')"
unfolding mp'_def
by (metis Multiset.diff_add add_mset_add_single diff_union_swap insert_DiffM)
with no_clash mp have "¬ Conflict_Clash ?s t" by metis
moreover have "Conflict_Clash ?s t"
using t by (cases t, auto simp: conflicts.simps)
ultimately show ?thesis ..
next
case no_clash': False
with violation have finsort: "⋀ x. (Var x, Var y) ∈# mp ⟹ ¬ inf_sort (snd x)" by blast
show ?thesis
proof (cases "∃ x. (Var x, Var y) ∈# mp")
case True
then obtain x where t: "(Var x, Var y) ∈# mp" (is "(?t,_) ∈# _") by auto
from finsort[OF t] have fin: "¬ inf_sort (snd x)" .
from s t fin pat_instantiate[OF _ disjI2, of _ mp p' ?t y ?s x, folded p', OF fresh]
show ?thesis by (auto simp: conflicts.simps)
next
case False
define test_y where "test_y tl = (snd tl = Var y)" for tl :: "('f, nat × 's) term × ('f,'v)term"
define mpy where "mpy = filter_mset test_y mp"
have size: "size mpy ≥ 2"
proof -
from mset_add[OF s] obtain mp' where mp': "mp = add_mset (?s, Var y) mp'" by blast
have "y ∈ ⋃ (vars ` snd ` mp_mset mp')"
using nsvar[rule_format] mp' mp by blast
then obtain t' l' where tl': "(t',l') ∈# mp'" and "y ∈ vars l'" by auto
with rhs_vars[OF mp, of t' l'] mp' have "is_Var l'" by auto
with ‹y ∈ vars l'› have l': "l' = Var y" by auto
hence "(t',Var y) ∈# mp'" using tl' by auto
from mset_add[OF this] obtain mp'' where mp'': "mp' = add_mset (t', Var y) mp''"
by auto
have mpy: "mpy = add_mset (?s, Var y) (add_mset (t', Var y) (filter_mset test_y mp''))"
unfolding mpy_def mp' mp'' by (simp add: test_y_def)
thus ?thesis by simp
qed
define mpny where "mpny = filter_mset (Not o test_y) mp"
have id: "mp = mpy + mpny" by (simp add: mpy_def mpny_def)
{
fix t l
assume "(t, l) ∈# mpny"
hence "l ≠ Var y" "(t,l) ∈# mp" unfolding mpny_def test_y_def o_def by auto
with rhs_vars[OF mp, of t l] have "y ∉ vars l" by (cases l, auto)
} note mpny = this
{
fix t l
assume "(t, l) ∈# mpy"
hence l: "l = Var y" and pair: "(t,Var y) ∈# mp" unfolding mpy_def test_y_def o_def by auto
with False obtain g ts where t: "t = Fun g ts" by (cases t, auto)
from no_clash' pair t have "root t = Some (f,?n)" by auto
with l have "l = Var y ∧ root t = Some (f,?n)" by auto
} note mpy = this
define VV where "VV = ⋃ (vars ` snd ` mp_mset mp)"
have "finite VV" by (auto simp: VV_def)
with assms(1)[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 "lvars_disj_mp ys (mp_mset mp)" "length ys = ?n"
unfolding lvars_disj_mp_def using ys dist unfolding VV_def by auto
from match_decompose'[of mpy y f ?n mpny, folded id, OF mpy mpny this size impr]
obtain mp' where "mp →⇩m mp'" by force
from pat_simp_mp[OF this, of p'] p' show ?thesis by auto
qed
qed
qed auto
thus ?thesis
proof (elim context_disjE)
assume no_step: "¬ (pat_fail p ∨ (∃ps. p ⇒⇩m ps))"
assume "weak_finite_var_form_pat (pat_mset p)"
note wfvf = this[unfolded weak_finite_var_form_pat_def weak_finite_var_form_match_def, rule_format]
note get_var = wfvf[THEN conjunct1, rule_format]
note fun_case = wfvf[THEN conjunct2, rule_format]
define fin where "fin mp = Ball (tvars_match (mp_mset mp)) (λ x. ¬ inf_sort (snd x))" for mp :: "('f,'v,'s) match_problem_mset"
define p_fin where "p_fin = filter_mset fin p"
define p_inf where "p_inf = filter_mset (Not o fin) p"
have p_split: "p = p_inf + p_fin" unfolding p_fin_def p_inf_def by auto
show ?thesis
proof (cases "p_inf = {#}")
case True
have fin: "⋀ mp. mp ∈# p ⟹ fin mp" unfolding p_split True unfolding p_fin_def by auto
have "finite_var_form_pat C (pat_mset p)"
unfolding finite_var_form_pat_def finite_var_form_match_def var_form_match_def
proof (intro ballI conjI subsetI allI impI, clarify)
fix mp l
assume mp: "mp ∈ pat_mset p"
{ fix t assume tl: "(t,l) ∈ mp"
from get_var[OF mp tl] tl obtain y where
ty: "(t, Var y) ∈ mp" and ly: "l = Var y" by (cases l, auto)
have "is_Var t"
proof (cases t)
case (Fun f ts)
with ty have "(Fun f ts, Var y) ∈ mp" by auto
from fun_case[OF _ this] mp obtain x where "(Var x, Var y) ∈ mp" "inf_sort (snd x)" by auto
with fin[unfolded fin_def tvars_match_def] mp tl have False by auto
thus ?thesis by auto
qed auto
with ly show "(t,l) ∈ range (map_prod Var Var)" by auto
} note var_var = this
fix x assume xl: "(Var x, l) ∈ mp"
then have xmp: "x ∈ tvars_match mp" by (force simp: tvars_match_def)
with wf[unfolded wf_pat_def wf_match_def, rule_format, OF mp]
have sxS: "snd x ∈ S" by auto
from mp xmp fin fin_def have "¬inf_sort (snd x)" by auto
with inf_sort[OF sxS]
show fint: "finite_sort C (snd x)" by auto
fix y assume yl: "(Var y, l) ∈ mp"
from yl var_var obtain z where l: "l = Var z" by force
show "snd x = snd y"
proof (cases "x = y")
case False
from mp obtain mp' where mp': "mp' ∈# p" and mp: "mp = mp_mset mp'" by auto
from False xl yl obtain mp''
where "mp' = add_mset (Var x, Var z) (add_mset (Var y, Var z) mp'')"
unfolding l mp by (metis insert_DiffM insert_noteq_member prod.inject term.inject(1))
with no_clash mp' have "¬ Conflict_Clash (Var x) (Var y)"
by (metis conflicts.simps(1))
thus "snd x = snd y" by (simp add: conflicts.simps split: if_splits)
qed auto
qed
with impr show ?thesis by auto
next
case False
have "∀x∈tvars_pat (pat_mset p_fin). ¬ inf_sort (snd x)" unfolding p_fin_def fin_def
by (auto simp: tvars_pat_def)
from pat_inf_var_conflict[OF _ False this, folded p_split] no_step
obtain mp where mp: "mp ∈# p" and inf: "¬ fin mp" and no_confl: "¬ inf_var_conflict (mp_mset mp)"
unfolding p_inf_def using impr by fastforce
from inf[unfolded fin_def tvars_match_def]
obtain t l x where tl: "(t,l) ∈# mp" and x: "x ∈ vars t" and inf: "inf_sort (snd x)" by auto
from get_var[OF _ tl] mp tl obtain y where ty: "(t, Var y) ∈# mp" by auto
have "∃ x. (Var x, Var y) ∈# mp ∧ inf_sort (snd x)"
proof (cases t)
case (Var z)
with ty inf x show ?thesis by (intro exI[of _ z], auto)
next
case (Fun f ts)
from fun_case[OF _ ty[unfolded Fun]] mp show ?thesis by auto
qed
then obtain x where xy: "(Var x, Var y) ∈# mp" and inf: "inf_sort (snd x)" by auto
from mset_add[OF xy] obtain mp' where mp': "mp = add_mset (Var x, Var y) mp'" by auto
from nsvar[simplified, rule_format, OF mp[unfolded mp']] obtain s y' where
sy': "(s,y') ∈# mp'" and y': "y ∈ vars y'" by force
from mset_add[OF sy'] mp' obtain mp'' where
mp'': "mp = add_mset (s,y') (add_mset (Var x, Var y) mp'')"
by auto
from get_var[OF mp_mset_in_pat_mset[OF mp[unfolded mp'']]] y'
have mp'': "mp = add_mset (s, Var y) (add_mset (Var x, Var y) mp'')"
unfolding mp'' by (cases y', auto)
from ndup mp'' mp have sx: "s ≠ Var x" by auto
from no_clash mp'' mp have no_clash: "¬ Conflict_Clash s (Var x)" by metis
from no_confl[unfolded inf_var_conflict_def not_ex, rule_format, of s y "Var x" x] mp'' inf
have "¬ Conflict_Var s (Var x) x" by auto
with sx no_clash have False by (cases s, auto simp: conflicts.simps split: if_splits)
thus ?thesis by auto
qed
qed auto
qed
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
qed
qed
qed
qed
qed
context
assumes non_improved: "¬ improved"
begin
lemma pat_fail_or_trans: "wf_pat (pat_mset p) ⟹ pat_fail p ∨ (∃ ps. p ⇒⇩m ps)"
using pat_fail_or_trans_or_finite_var_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_fail_or_trans
obtain ps where "pat_fail p ∨ p ⇒⇩m ps" by auto
with P_simp_pp[of p ps] NF
have "pat_fail p" unfolding P by auto
from P_failure[OF this, of P', folded P] nNF NF show False by auto
qed
end
context
assumes improved: "improved"
and inf: "infinite (UNIV :: 'v set)"
begin
lemma pat_fail_or_trans_or_fvf:
fixes p :: "('f,'v,'s) pat_problem_mset"
assumes "wf_pat (pat_mset p)"
shows "pat_fail p ∨ (∃ ps. p ⇒⇩m ps) ∨ finite_var_form_pat C (pat_mset p)"
using assms pat_fail_or_trans_or_finite_var_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_var_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_fail_or_trans_or_fvf[OF wfp] nfvf
obtain ps where "pat_fail p ∨ p ⇒⇩m ps" by auto
with P_simp_pp[of p ps] NF
have "pat_fail p" unfolding P by auto
from P_failure[OF this, of P', folded P] NF have "P = {# {#} #}" by auto
with P have "p = {#}" by auto
with nfvf show False unfolding finite_var_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)
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_funs t))"
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 × ('f,'v,'s)pat_problem_mset)set" (‹≺›) where
"(≺) = 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))"
abbreviation gt_rel_pat (infix ‹≻› 50) where
"pp ≻ pp' ≡ (pp',pp) ∈ ≺"
definition rel_pats :: "(('f,'v,'s)pats_problem_mset × ('f,'v,'s)pats_problem_mset)set" (‹≺mul›) where
"≺mul = mult (≺)"
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_pats: "wf ≺mul"
unfolding rel_pats_def
by (intro wf_inv_image wf_mult wf_rel_pat)
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 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_funs t) ≤ sum_list (map num_funs 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_funs t) ≤ sum_list (map num_funs 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_funs t) +
(∑(ti, yi)∈#(∑(t, l)∈#MP. mset (zip (args t) (map ?Var ys))). num_funs ti)
≤ (sum_list (map num_funs TS) + (∑(t, l)∈#MP. num_funs 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_funs ti)
≤ (∑(t, l)∈#MP. num_funs 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'"
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 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
show ?case unfolding p'
by (rule meas_sub_rel_pat, auto)
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 *: "(s, Var y) ∈# mp ∧ (t, Var y) ∈# mp ∧ Conflict_Var s t x ∧ ¬ inf_sort (snd x)
∧ (improved ⟶ s = Var x ∧ is_Fun t)"
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 (intro meas_sub_rel_pat, auto)
next
case *: (pat_inf_var_conflict p)
thus ?case by (intro meas_sub_rel_pat, cases p, auto)
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 P)
from * have "p ≠ {#} ∨ p = {#} ∧ P ≠ {#}" by auto
thus ?case
proof
assume "p ≠ {#}"
then obtain mp p' where p: "p = add_mset mp p'" by (cases p, auto)
have "p ≻ {#}" unfolding p by (intro meas_sub_rel_pat, auto)
thus ?thesis unfolding rel_pats_def using
one_step_implies_mult[of "add_mset p P" "{#{#}#}" _ "{#}"]
by auto
next
assume *: "p = {#} ∧ P ≠ {#}" then obtain p' P' where p: "p = {#}" and P: "P = add_mset p' P'" by (cases P, auto)
show ?thesis unfolding P p unfolding rel_pats_def
by (simp add: subset_implies_mult)
qed
next
case *: (P_simp_pp p ps P)
from rel_pp_step_mset[OF *]
show ?case unfolding rel_pats_def by (metis add_many_mult)
qed
text ‹termination of the multiset based implementation›
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 P_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 "pats_mset P ⇛⇩s pats_mset Q"
using assms
proof (induct)
case *: (P_failure p P)
let ?P = "insert (pat_mset p) (pats_mset P)"
from *(1)
have "?P ⇛⇩s bottom"
proof induct
case pat_empty
show ?case using P_fail by auto
qed
thus ?case by auto
next
case *: (P_simp_pp p ps P)
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]
define P' where "P' = {mp_mset ` set_mset x |. x ∈ set_mset P}"
from *(1)
have "insert (pat_mset p) (pats_mset P) ⇛⇩s pats_mset ps ∪ pats_mset P"
unfolding conv P'_def[symmetric]
proof induction
case (pat_remove_pp p)
show ?case unfolding conv
by (intro P_remove_pp pp_success.intros)
next
case *: (pat_simp_mp mp mp' p)
from P_simp[OF pp_simp_mp[OF mp_step_mset_mp_trans[OF *]]]
show ?case by auto
next
case *: (pat_remove_mp mp p)
from P_simp[OF 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 P_step_set_cong[OF P_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)
from P_simp[OF this]
show ?case by auto
qed
thus ?case unfolding conv .
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) ∈ P_step"
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)
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 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_var_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_var_form_pat C (pat_mset p)" .
qed
end
end