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"
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))"
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) ⟹
add_mset mp pp ⇒⇩m mset (map (λ τ. subst_pat_problem_mset τ (add_mset mp pp)) (τs_list n x))"
inductive pat_fail :: "('f,'v,'s)pat_problem_mset ⇒ bool" where
pat_failure': "Ball (pat_mset pp) inf_var_conflict ⟹ pat_fail pp"
| 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 pat_fail_or_trans:
"pat_fail p ∨ (∃ ps. p ⇒⇩m ps)"
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 y. add_mset (s, Var x) (add_mset (t, Var x) mp) ∈# p ∧ Conflict_Var s t y ∧ ¬ inf_sort (snd y)")
case True
then 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 conflicts(4)[OF conf] have "y ∈ vars s ∪ vars t" by auto
with mp have "y ∈ tvars_mp (mp_mset ?mp)" unfolding tvars_mp_def by auto
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 by auto
next
case no_non_inf: False
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 (intro disjI1 pat_failure' 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
qed
qed
qed
qed
qed
qed
text ‹Pattern problems just have two normal forms:
empty set (solvable) or bottom (not solvable)›
theorem P_step_NF:
assumes 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
from 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
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,EMPTYn)}) else 0)"
definition meas_finvars :: "('f,'v,'s)pat_problem_mset ⇒ nat" where
"meas_finvars = sum_ms (λ mp. sum (max_size o snd) (tvars_mp (mp_mset mp)))"
definition meas_symbols :: "('f,'v,'s)pat_problem_mset ⇒ nat" where
"meas_symbols = sum_ms size_mset"
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_mp_fin:
"finite (tvars_mp (mp_mset mp))"
unfolding tvars_mp_def by auto
lemmas meas_def = meas_finvars_def meas_diff_def meas_symbols_def meas_setsize_def
lemma tvars_mp_mono: "mp ⊆# mp' ⟹ tvars_mp (mp_mset mp) ⊆ tvars_mp (mp_mset mp')"
unfolding tvars_mp_def
by (intro image_mono subset_refl set_mset_mono UN_mono)
lemma meas_finvars_mono: assumes "tvars_mp (mp_mset mp) ⊆ tvars_mp (mp_mset mp')"
shows "meas_finvars {#mp#} ≤ meas_finvars {#mp'#}"
using tvars_mp_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_mp_mono[OF this]]
show ?thesis unfolding meas_def rel_pat_def by auto
qed
lemma rel_mp_mp_step_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_mp (mp_mset mp') ⊆ tvars_mp (mp_mset mp)"
unfolding tvars_mp_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 "meas_symbols {#mp'#} < meas_symbols {#mp#}"
unfolding meas_def * using *(3) size_mset_Fun_less[of ts ls g g]
by (auto simp: sum_mset_sum_list)
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,EMPTYn) ∧ max_size s = size t ∧ (∀ t'. t' : s in 𝒯(C,EMPTYn) ⟶ size t' ≤ size t)"
proof -
let ?set = "λ s. size ` {t. t : s in 𝒯(C,EMPTYn)}"
have m: "max_size s = Maximum (?set s)" unfolding o_def max_size_def using inf sS by auto
from inf[unfolded inf_sort_def[OF sS]] have "bdd_above (?set s)" by auto
moreover from sorts_non_empty[OF sS] type_conversion2 have "?set s ≠ {}" by auto
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,EMPTYn)"
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 term_of_sort[OF this]
}
hence "∀ v. ∃ t. v ∈ set vs ⟶ t : snd v in 𝒯(C,EMPTYn)" by auto
from choice[OF this] obtain t where
t: "⋀ v. v ∈ set vs ⟹ t v : snd v in 𝒯(C,EMPTYn)" 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
from not_bdd_above_natD[OF inf_vl[unfolded inf_sort_def[OF vlS]], of ?m] t[OF vl]
obtain tl where
tl: "tl : snd vl in 𝒯(C,EMPTYn)" 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,EMPTYn)"
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,EMPTYn) ∧ size t = max_size (snd v)" by auto
}
hence "∀ v. ∃ t. v ∈ set vs ⟶ t : snd v in 𝒯(C,EMPTYn) ∧ 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,EMPTYn) ∧ size (t v) = max_size (snd v)" for v by blast
let ?t = "Fun c (map t vs)"
have "?t : s in 𝒯(C,EMPTYn)"
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:
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)"
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 τ"
let ?tau = "subst_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_mp_subst: "tvars_mp (mp_mset (?tau mp)) =
tvars_mp (mp_mset mp) - {x} ∪ (if x ∈ tvars_mp (mp_mset mp) then set vs else {})" for mp
unfolding subst_defs subst_left_def tvars_mp_def
by (auto simp:vars_τ split: if_splits prod.split)
have id1: "meas_finvars (?tau_mset {#mp#}) = (∑x∈ tvars_mp (mp_mset (?tau mp)). max_size (snd x))" for mp
unfolding meas_def subst_defs by auto
have id2: "meas_finvars {#mp#} = (∑x∈tvars_mp (mp_mset mp). max_size (snd x))" for mp
unfolding meas_def subst_defs by simp
have eq: "x ∉ tvars_mp (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_mp_subst)
{
fix mp
assume xmp: "x ∈ tvars_mp (mp_mset mp)"
let ?mp = "(mp_mset mp)"
have fin: "finite (tvars_mp ?mp)" by (rule tvars_mp_fin)
define Mp where "Mp = tvars_mp ?mp - {x}"
from xmp have 1: "tvars_mp (mp_mset (?tau mp)) = set vs ∪ Mp"
unfolding tvars_mp_subst Mp_def by auto
from xmp have 2: "tvars_mp ?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_mp_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)
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])
using wf_rel_pats by (simp add: wf_imp_SN)
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)
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)
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_failure' p)
from P_failure'[OF this]
show ?case by auto
next
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_mp (mp_mset mp)"
using conflicts(4)[of s t x] unfolding tvars_mp_def
by (auto intro!:term.set_intros(3))
hence x: "x ∈ tvars_pp (pat_mset (add_mset mp p))" unfolding tvars_pp_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)
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 (pats_mset P) = pats_complete (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 (pats_mset P) ⟷ pats_complete (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 wf: "wf_pats (pats_mset P)" and NF: "(P,Q) ∈ ⇛⇧!"
shows "Q = {#} ∧ pats_complete (pats_mset P)
∨ Q = bottom_mset ∧ ¬ pats_complete (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 (pats_mset P) = pats_complete (pats_mset Q)"
by blast+
from P_step_NF[OF NF] have "Q ∈ {{#},bottom_mset}" .
thus ?thesis unfolding sound by auto
qed
end
end