Theory Pattern_Completeness_List
section ‹A List-Based Implementation to Decide Pattern Completeness›
theory Pattern_Completeness_List
imports
Pattern_Completeness_Multiset
Compute_Nonempty_Infinite_Sorts
"HOL-Library.AList"
begin
subsection ‹Definition of Algorithm›
text ‹We refine the non-deterministic multiset based implementation
to a deterministic one which uses lists as underlying data-structure.
For matching problems we distinguish several different shapes.›
type_synonym ('a,'b)alist = "('a × 'b)list"
type_synonym ('f,'v,'s)match_problem_list = "(('f,nat × 's)term × ('f,'v)term) list"
type_synonym ('f,'v,'s)match_problem_lx = "((nat × 's) × ('f,'v)term) list"
type_synonym ('f,'v,'s)match_problem_rx = "('v,('f,nat × 's)term list) alist × bool"
type_synonym ('f,'v,'s)match_problem_lr = "('f,'v,'s)match_problem_lx × ('f,'v,'s)match_problem_rx"
type_synonym ('f,'v,'s)pat_problem_list = "('f,'v,'s)match_problem_list list"
type_synonym ('f,'v,'s)pat_problem_lr = "('f,'v,'s)match_problem_lr list"
type_synonym ('f,'v,'s)pats_problem_list = "('f,'v,'s)pat_problem_list list"
type_synonym ('f,'v,'s)pat_problem_set_impl = "(('f,nat × 's)term × ('f,'v)term) list list"
abbreviation mp_list :: "('f,'v,'s)match_problem_list ⇒ ('f,'v,'s)match_problem_mset"
where "mp_list ≡ mset"
abbreviation mp_lx :: "('f,'v,'s)match_problem_lx ⇒ ('f,'v,'s)match_problem_list"
where "mp_lx ≡ map (map_prod Var id)"
definition mp_rx :: "('f,'v,'s)match_problem_rx ⇒ ('f,'v,'s)match_problem_mset"
where "mp_rx mp = mset (List.maps (λ (x,ts). map (λ t. (t,Var x)) ts) (fst mp))"
definition mp_rx_list :: "('f,'v,'s)match_problem_rx ⇒ ('f,'v,'s)match_problem_list"
where "mp_rx_list mp = List.maps (λ (x,ts). map (λ t. (t,Var x)) ts) (fst mp)"
definition mp_lr :: "('f,'v,'s)match_problem_lr ⇒ ('f,'v,'s)match_problem_mset"
where "mp_lr pair = (case pair of (lx,rx) ⇒ mp_list (mp_lx lx) + mp_rx rx)"
definition mp_lr_list :: "('f,'v,'s)match_problem_lr ⇒ ('f,'v,'s)match_problem_list"
where "mp_lr_list pair = (case pair of (lx,rx) ⇒ mp_lx lx @ mp_rx_list rx)"
definition pat_lr :: "('f,'v,'s)pat_problem_lr ⇒ ('f,'v,'s)pat_problem_mset"
where "pat_lr ps = mset (map mp_lr ps)"
definition pat_mset_list :: "('f,'v,'s)pat_problem_list ⇒ ('f,'v,'s)pat_problem_mset"
where "pat_mset_list ps = mset (map mp_list ps)"
definition pat_list :: "('f,'v,'s)pat_problem_list ⇒ ('f,'v,'s)pat_problem_set"
where "pat_list ps = set ` set ps"
abbreviation pats_mset_list :: "('f,'v,'s)pats_problem_list ⇒ ('f,'v,'s)pats_problem_mset"
where "pats_mset_list ≡ mset o map pat_mset_list"
definition subst_match_problem_list :: "('f,nat × 's)subst ⇒ ('f,'v,'s)match_problem_list ⇒ ('f,'v,'s)match_problem_list" where
"subst_match_problem_list τ = map (subst_left τ)"
definition subst_pat_problem_list :: "('f,nat × 's)subst ⇒ ('f,'v,'s)pat_problem_list ⇒ ('f,'v,'s)pat_problem_list" where
"subst_pat_problem_list τ = map (subst_match_problem_list τ)"
definition match_var_impl :: "('f,'v,'s)match_problem_lr ⇒ ('f,'v,'s)match_problem_lr" where
"match_var_impl mp = (case mp of (xl,(rx,b)) ⇒
let xs = remdups (List.maps (vars_term_list o snd) xl)
in (xl,(filter (λ (x,ts). tl ts ≠ [] ∨ x ∈ set xs) rx),b))"
definition find_var :: "('f,'v,'s)match_problem_lr list ⇒ _" where "find_var p = (case concat (map (λ (lx,_). lx) p) of
(x,t) # _ ⇒ x
| [] ⇒ let (_,rx,b) = hd (filter (Not o snd o snd) p)
in case hd rx of (x, s # t # _) ⇒ hd (the (conflicts s t)))"
definition empty_lr :: "('f,'v,'s)match_problem_lr ⇒ bool" where
"empty_lr mp = (case mp of (lx,rx,_) ⇒ lx = [] ∧ rx = [])"
context pattern_completeness_context
begin
text ‹insert an element into the part of the mp that stores pairs of form (t,x) for variables x.
Internally this is represented as maps (assoc lists) from x to terms t1,t2,... so that linear terms are easily
identifiable. Duplicates will be removed and clashes will be immediately be detected and result in None.›
definition insert_rx :: "('f,nat × 's)term ⇒ 'v ⇒ ('f,'v,'s)match_problem_rx ⇒ ('f,'v,'s)match_problem_rx option" where
"insert_rx t x rxb = (case rxb of (rx,b) ⇒ (case map_of rx x of
None ⇒ Some (((x,[t]) # rx, b))
| Some ts ⇒ (case those (map (conflicts t) ts)
of None ⇒ None
| Some cs ⇒ if [] ∈ set cs then Some rxb
else Some ((AList.update x (t # ts) rx, b ∨ (∃ y ∈ set (concat cs). inf_sort (snd y))))
)))"
lemma size_zip[termination_simp]: "length ts = length ls ⟹ size_list (λp. size (snd p)) (zip ts ls)
< Suc (size_list size ls)"
by (induct ts ls rule: list_induct2, auto)
text ‹Decomposition applies decomposition, duplicate and clash rule to classify all remaining problems
as being of kind (x,f(l1,..,ln)) or (t,x).›
fun decomp_impl :: "('f,'v,'s)match_problem_list ⇒ ('f,'v,'s)match_problem_lr option" where
"decomp_impl [] = Some ([],([],False))"
| "decomp_impl ((Fun f ts, Fun g ls) # mp) = (if (f,length ts) = (g,length ls) then
decomp_impl (zip ts ls @ mp) else None)"
| "decomp_impl ((Var x, Fun g ls) # mp) = (case decomp_impl mp of Some (lx,rx) ⇒ Some ((x,Fun g ls) # lx,rx)
| None ⇒ None)"
| "decomp_impl ((t, Var y) # mp) = (case decomp_impl mp of Some (lx,rx) ⇒
(case insert_rx t y rx of Some rx' ⇒ Some (lx,rx') | None ⇒ None)
| None ⇒ None)"
definition match_steps_impl :: "('f,'v,'s)match_problem_list ⇒ ('f,'v,'s)match_problem_lr option" where
"match_steps_impl mp = map_option match_var_impl (decomp_impl mp)"
fun pat_inner_impl :: "('f,'v,'s)pat_problem_list ⇒ ('f,'v,'s)pat_problem_lr ⇒ ('f,'v,'s)pat_problem_lr option" where
"pat_inner_impl [] pd = Some pd"
| "pat_inner_impl (mp # p) pd = (case match_steps_impl mp of
None ⇒ pat_inner_impl p pd
| Some mp' ⇒ if empty_lr mp' then None
else pat_inner_impl p (mp' # pd))"
definition pat_impl :: "nat ⇒ ('f,'v,'s)pat_problem_list ⇒ ('f,'v,'s)pat_problem_list list option" where
"pat_impl n p = (case pat_inner_impl p [] of None ⇒ Some []
| Some p' ⇒ (if (∀ mp ∈ set p'. snd (snd mp)) then None
else let p'l = map mp_lr_list p';
x = find_var p'
in
Some (map (λ τ. subst_pat_problem_list τ p'l) (τs_list n x))))"
partial_function (tailrec) pats_impl :: "nat ⇒ ('f,'v,'s)pats_problem_list ⇒ bool" where
"pats_impl n ps = (case ps of [] ⇒ True
| p # ps1 ⇒ (case pat_impl n p of
None ⇒ False
| Some ps2 ⇒ pats_impl (n + m) (ps2 @ ps1)))"
definition pat_complete_impl :: "('f,'v,'s)pats_problem_list ⇒ bool" where
"pat_complete_impl ps = (let
n = Suc (max_list (List.maps (map fst o vars_term_list o fst) (concat (concat ps))))
in pats_impl n ps)"
end
lemmas pat_complete_impl_code =
pattern_completeness_context.pat_complete_impl_def
pattern_completeness_context.pats_impl.simps
pattern_completeness_context.pat_impl_def
pattern_completeness_context.τs_list_def
pattern_completeness_context.insert_rx_def
pattern_completeness_context.decomp_impl.simps
pattern_completeness_context.match_steps_impl_def
pattern_completeness_context.pat_inner_impl.simps
declare pat_complete_impl_code[code]
subsection ‹Partial Correctness of the Implementation›
text ‹We prove that the list-based implementation is
a refinement of the multiset-based one.›
lemma mset_concat_union:
"mset (concat xs) = ∑⇩# (mset (map mset xs))"
by (induct xs, auto simp: union_commute)
lemma in_map_mset[intro]:
"a ∈# A ⟹ f a ∈# image_mset f A"
unfolding in_image_mset by simp
lemma mset_update: "map_of xs x = Some y ⟹
mset (AList.update x z xs) = (mset xs - {# (x,y) #}) + {# (x,z) #}"
by (induction xs, auto)
lemma set_update: "map_of xs x = Some y ⟹ distinct (map fst xs) ⟹
set (AList.update x z xs) = insert (x,z) (set xs - {(x,y)})"
by (induction xs, auto)
context pattern_completeness_context_with_assms
begin
text ‹Various well-formed predicates for intermediate results›
definition wf_ts :: "('f, nat × 's) term list ⇒ bool" where
"wf_ts ts = (ts ≠ [] ∧ distinct ts ∧ (∀ j < length ts. ∀ i < j. conflicts (ts ! i) (ts ! j) ≠ None))"
definition wf_ts2 :: "('f, nat × 's) term list ⇒ bool" where
"wf_ts2 ts = (length ts ≥ 2 ∧ distinct ts ∧ (∀ j < length ts. ∀ i < j. conflicts (ts ! i) (ts ! j) ≠ None))"
definition wf_lx :: "('f,'v,'s)match_problem_lx ⇒ bool" where
"wf_lx lx = (Ball (snd ` set lx) is_Fun)"
definition wf_rx :: "('f,'v,'s)match_problem_rx ⇒ bool" where
"wf_rx rx = (distinct (map fst (fst rx)) ∧ (Ball (snd ` set (fst rx)) wf_ts) ∧ snd rx = inf_var_conflict (set_mset (mp_rx rx)))"
definition wf_rx2 :: "('f,'v,'s)match_problem_rx ⇒ bool" where
"wf_rx2 rx = (distinct (map fst (fst rx)) ∧ (Ball (snd ` set (fst rx)) wf_ts2) ∧ snd rx = inf_var_conflict (set_mset (mp_rx rx)))"
definition wf_lr :: "('f,'v,'s)match_problem_lr ⇒ bool"
where "wf_lr pair = (case pair of (lx,rx) ⇒ wf_lx lx ∧ wf_rx rx)"
definition wf_lr2 :: "('f,'v,'s)match_problem_lr ⇒ bool"
where "wf_lr2 pair = (case pair of (lx,rx) ⇒ wf_lx lx ∧ (if lx = [] then wf_rx2 rx else wf_rx rx))"
definition wf_pat_lr :: "('f,'v,'s)pat_problem_lr ⇒ bool" where
"wf_pat_lr mps = (Ball (set mps) (λ mp. wf_lr2 mp ∧ ¬ empty_lr mp))"
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_mp (mp_mset mp) ⊇ tvars_mp (mp_mset mp')"
using assms by induct (auto simp: tvars_mp_def set_zip)
lemma mp_step_mset_steps_vars: assumes "(→⇩m)⇧*⇧* mp mp'"
shows "tvars_mp (mp_mset mp) ⊇ tvars_mp (mp_mset mp')"
using assms by (induct, insert mp_step_mset_vars, auto)
text ‹Continue with properties of the sub-algorithms›
lemma insert_rx: assumes res: "insert_rx t x rxb = res"
and wf: "wf_rx rxb"
and mp: "mp = (ls,rxb)"
shows "res = Some rx' ⟹ (→⇩m)⇧*⇧* (add_mset (t,Var x) (mp_lr mp + M)) (mp_lr (ls,rx') + M) ∧ wf_rx rx'"
"res = None ⟹ match_fail (add_mset (t,Var x) (mp_lr mp + M))"
proof -
obtain rx b where rxb: "rxb = (rx,b)" by force
note [simp] = List.maps_def
note res = res[unfolded insert_rx_def]
{
assume *: "res = None"
with res rxb obtain ts where look: "map_of rx x = Some ts" by (auto split: option.splits)
with res[unfolded look Let_def rxb split] * obtain t' where t': "t' ∈ set ts" and clash: "Conflict_Clash t t'"
by (auto split: if_splits option.splits)
from map_of_SomeD[OF look] t' have "(t',Var x) ∈# mp_rx rxb"
unfolding mp_rx_def rxb by auto
hence "(t',Var x) ∈# mp_lr mp + M" unfolding mp mp_lr_def by auto
then obtain mp' where mp: "mp_lr mp + M = add_mset (t',Var x) mp'" by (rule mset_add)
show "match_fail (add_mset (t,Var x) (mp_lr mp + M))" unfolding mp
by (rule match_clash'[OF clash])
}
{
assume "res = Some rx'"
note res = res[unfolded this rxb split]
show "mp_step_mset^** (add_mset (t,Var x) (mp_lr mp + M)) (mp_lr (ls,rx') + M) ∧ wf_rx rx'"
proof (cases "map_of rx x")
case look: None
from res[unfolded this]
have rx': "rx' = ((x,[t]) # rx, b)" by auto
have id: "mp_rx rx' = add_mset (t, Var x) (mp_rx rxb)"
using look unfolding mp_rx_def mset_concat_union mset_map rx' o_def rxb
by auto
have [simp]: "(x, t) ∉ set rx" for t using look
using weak_map_of_SomeI by force
have "inf_var_conflict (mp_mset (mp_rx ((x, [t]) # rx, b))) = inf_var_conflict (mp_mset (mp_rx (rx, b)))"
unfolding mp_rx_def fst_conv inf_var_conflict_def
by (intro ex_cong1, auto)
hence wf: "wf_rx rx'" using wf look unfolding wf_rx_def rx' rxb by (auto simp: wf_ts_def)
show ?thesis unfolding mp mp_lr_def split id
using wf unfolding rx' by auto
next
case look: (Some ts)
from map_of_SomeD[OF look] have mem: "(x,ts) ∈ set rx" by auto
note res = res[unfolded look option.simps Let_def]
from res obtain cs where those: "those (map (conflicts t) ts) = Some cs" by (auto split: option.splits)
note res = res[unfolded those option.simps]
from arg_cong[OF those[unfolded those_eq_Some], of set] have confl: "conflicts t ` set ts = Some ` set cs" by auto
show ?thesis
proof (cases "[] ∈ set cs")
case True
with res have rx': "rx' = rxb" by (auto split: if_splits simp: mp rxb those)
from True confl obtain t' where "t' ∈ set ts" and "conflicts t t' = Some []" by force
hence t: "t ∈ set ts" using conflicts(5)[of t t'] by auto
hence "(t, Var x) ∈# mp_rx rxb" unfolding mp_rx_def rxb using mem by auto
hence "(t, Var x) ∈# mp_lr mp + M" unfolding mp mp_lr_def by auto
then obtain sub where id: "mp_lr mp + M = add_mset (t, Var x) sub" by (rule mset_add)
show ?thesis unfolding id rx' mp[symmetric] using match_duplicate[of "(t, Var x)" sub] wf by auto
next
case False
with res have rx': "rx' = (AList.update x (t # ts) rx, b ∨ (∃y∈set (concat cs). inf_sort (snd y)))" by (auto split: if_splits)
from split_list[OF mem] obtain rx1 rx2 where rx: "rx = rx1 @ (x,ts) # rx2" by auto
have id: "mp_rx rx' = add_mset (t, Var x) (mp_rx rxb)"
unfolding rx' mp_rx_def rxb by (simp add: mset_update[OF look] mset_concat_union, auto simp: rx)
from wf[unfolded wf_rx_def] rx rxb have ts: "wf_ts ts" and b: "b = inf_var_conflict (mp_mset (mp_rx rxb))" by auto
from False confl conflicts(5)[of t t] have t: "t ∉ set ts" by force
from confl have "None ∉ set (map (conflicts t) ts)" by auto
with ts t have ts': "wf_ts (t # ts)" unfolding wf_ts_def
apply clarsimp
subgoal for j i by (cases j, force, cases i; force simp: set_conv_nth)
done
have b: "(b ∨ (∃y∈set (concat cs). inf_sort (snd y))) = inf_var_conflict (mp_mset (add_mset (t, Var x) (mp_rx rxb)))" (is "_ = ?ivc")
proof (standard, elim disjE bexE)
show "b ⟹ ?ivc" unfolding b inf_var_conflict_def by force
{
fix y
assume y: "y ∈ set (concat cs)" and inf: "inf_sort (snd y)"
from y confl obtain t' ys where t': "t' ∈ set ts" and c: "conflicts t t' = Some ys" and y: "y ∈ set ys" unfolding set_concat
by (smt (verit, del_insts) UnionE image_iff)
have y: "Conflict_Var t t' y" using c y by auto
from mem t' have "(t',Var x) ∈# mp_rx rxb" unfolding rxb mp_rx_def by auto
thus ?ivc unfolding inf_var_conflict_def using inf y by fastforce
}
assume ?ivc
from this[unfolded inf_var_conflict_def]
obtain s1 s2 x' y
where ic: "(s1, Var x') ∈# add_mset (t, Var x) (mp_rx rxb) ∧ (s2, Var x') ∈# add_mset (t, Var x) (mp_rx rxb) ∧ Conflict_Var s1 s2 y ∧ inf_sort (snd y)"
by blast
show "b ∨ (∃y∈set (concat cs). inf_sort (snd y))"
proof (cases "(s1, Var x') ∈# mp_rx rxb ∧ (s2, Var x') ∈# mp_rx rxb")
case True
with ic have b unfolding b inf_var_conflict_def by blast
thus ?thesis ..
next
case False
with ic have "(s1,Var x') = (t,Var x) ∨ (s2,Var x') = (t,Var x)" by auto
hence "∃ s y. (s, Var x) ∈# add_mset (t, Var x) (mp_rx rxb) ∧ Conflict_Var t s y ∧ inf_sort (snd y)"
proof
assume "(s1, Var x') = (t, Var x)"
thus ?thesis using ic by blast
next
assume *: "(s2, Var x') = (t, Var x)"
with ic have "Conflict_Var s1 t y" by auto
hence "Conflict_Var t s1 y" using conflicts_sym[of s1 t] by (cases "conflicts s1 t"; cases "conflicts t s1", auto)
with ic * show ?thesis by blast
qed
then obtain s y where sx: "(s, Var x) ∈# add_mset (t, Var x) (mp_rx rxb)" and y: "Conflict_Var t s y" and inf: "inf_sort (snd y)"
by blast
from wf have dist: "distinct (map fst rx)" unfolding wf_rx_def rxb by auto
from y have "s ≠ t" by auto
with sx have "(s, Var x) ∈# mp_rx rxb" by auto
hence "s ∈ set ts" unfolding mp_rx_def rxb using mem eq_key_imp_eq_value[OF dist] by auto
with y confl have "y ∈ set (concat cs)" by (cases "conflicts t s"; force)
with inf show ?thesis by auto
qed
qed
have wf: "wf_rx rx'" using wf ts' unfolding wf_rx_def id unfolding rx' rxb snd_conv b by (auto simp: distinct_update set_update[OF look])
show ?thesis using wf id unfolding mp by (auto simp: mp_lr_def)
qed
qed
}
qed
lemma decomp_impl: "decomp_impl mp = res ⟹
(res = Some mp' ⟶ (→⇩m)⇧*⇧* (mp_list mp + M) (mp_lr mp' + M) ∧ wf_lr mp')
∧ (res = None ⟶ (∃ mp'. (→⇩m)⇧*⇧* (mp_list mp + M) mp' ∧ match_fail mp'))"
proof (induct mp arbitrary: res M mp' rule: decomp_impl.induct)
case 1
thus ?case by (auto simp: mp_lr_def mp_rx_def List.maps_def wf_lr_def wf_lx_def wf_rx_def inf_var_conflict_def)
next
case (2 f ts g ls mp res M mp')
have id: "mp_list ((Fun f ts, Fun g ls) # mp) + M = add_mset (Fun f ts, Fun g ls) (mp_list mp + M)"
by auto
show ?case
proof (cases "(f,length ts) = (g,length ls)")
case False
with 2(2-) have res: "res = None" by auto
from match_clash[OF False, of "(mp_list mp + M)", folded id]
show ?thesis unfolding res by blast
next
case True
have id2: "mp_list (zip ts ls @ mp) + M = mp_list mp + M + mp_list (zip ts ls)"
by auto
from True 2(2-) have res: "decomp_impl (zip ts ls @ mp) = res" by auto
note IH = 2(1)[OF True this, of mp' M]
note step = match_decompose[OF True, of "mp_list mp + M", folded id id2]
from IH step show ?thesis by (meson converse_rtranclp_into_rtranclp)
qed
next
case (3 x g ls mp res M mp')
note res = 3(2)[unfolded decomp_impl.simps]
show ?case
proof (cases "decomp_impl mp")
case None
from 3(1)[OF None, of mp' "add_mset (Var x, Fun g ls) M"] None res show ?thesis by auto
next
case (Some mpx)
then obtain lx rx where decomp: "decomp_impl mp = Some (lx,rx)" by (cases mpx, auto)
from res[unfolded decomp option.simps split] have res: "res = Some ( (x, Fun g ls) # lx, rx)" by auto
from 3(1)[OF decomp, of "(lx, rx)" "add_mset (Var x, Fun g ls) M"] res
show ?thesis by (auto simp: mp_lr_def wf_lr_def wf_lx_def)
qed
next
case (4 t y mp res M mp')
note res = 4(2)[unfolded decomp_impl.simps]
show ?case
proof (cases "decomp_impl mp")
case None
from 4(1)[OF None, of mp' "add_mset (t, Var y) M"] None res show ?thesis by auto
next
case (Some mpx)
then obtain lx rx where decomp: "decomp_impl mp = Some (lx,rx)" by (cases mpx, auto)
note res = res[unfolded decomp option.simps split]
from 4(1)[OF decomp, of "( lx, rx)" "add_mset (t, Var y) M"]
have IH: "(→⇩m)⇧*⇧* (mp_list ((t, Var y) # mp) + M) (mp_lr ( lx, rx) + add_mset (t, Var y) M)"
"wf_lr ( lx, rx)" by auto
from IH have wf_rx: "wf_rx rx" unfolding wf_lr_def by auto
show ?thesis
proof (cases "insert_rx t y rx")
case None
with res have res: "res = None" by auto
from insert_rx(2)[OF None wf_rx refl refl, of lx M]
IH res show ?thesis by auto
next
case (Some rx')
with res have res: "res = Some ( lx, rx')" by auto
from insert_rx(1)[OF Some wf_rx refl refl, of lx M]
have wf_rx: "wf_rx rx'"
and steps: "(→⇩m)⇧*⇧* (mp_lr ( lx, rx) + add_mset (t, Var y) M) (mp_lr ( lx, rx') + M)"
by auto
from IH(1) steps
have steps: "(→⇩m)⇧*⇧* (mp_list ((t, Var y) # mp) + M) (mp_lr ( lx, rx') + M)" by auto
from wf_rx IH(2-) have wf: "wf_lr ( lx, rx')"
unfolding wf_lr_def by auto
from res wf steps show ?thesis by auto
qed
qed
qed
lemma match_var_impl: assumes wf: "wf_lr mp"
shows "(→⇩m)⇧*⇧* (mp_lr mp) (mp_lr (match_var_impl mp))"
and "wf_lr2 (match_var_impl mp)"
proof -
note [simp] = List.maps_def
let ?mp' = "match_var_impl mp"
from assms obtain xl rx b where mp3: "mp = (xl,(rx,b))" by (cases mp, auto)
define xs where "xs = remdups (List.maps (vars_term_list o snd) xl)"
have xs: "xl = [] ⟹ xs = []" unfolding xs_def by auto
define f where "f = (λ (x,ts :: ('f, nat × 's)term list). tl ts ≠ [] ∨ x ∈ set xs)"
define mp' where "mp' = mp_rx (filter f rx, b) + mp_list (mp_lx xl)"
define deleted where "deleted = mp_rx (filter (Not o f) rx, b)"
have mp': "mp_lr ?mp' = mp'" "?mp' = (xl, (filter f rx,b))"
unfolding mp3 mp'_def match_var_impl_def split xs_def f_def mp_lr_def by auto
have "mp_rx (rx,b) = mp_rx (filter f rx, b) + mp_rx (filter (Not o f) rx, b)"
unfolding mp_rx_def List.maps_def by (induct rx, auto)
hence mp: "mp_lr mp = deleted + mp'" unfolding mp3 mp_lr_def mp'_def deleted_def by auto
have "inf_var_conflict (mp_mset (mp_rx (filter f rx, b))) = inf_var_conflict (mp_mset (mp_rx (rx, b)))" (is "?ivcf = ?ivc")
proof
show "?ivcf ⟹ ?ivc" unfolding inf_var_conflict_def mp_rx_def fst_conv List.maps_def by force
assume ?ivc
from this[unfolded inf_var_conflict_def]
obtain s t x y where s: "(s, Var x) ∈# mp_rx (rx, b)" and t: "(t, Var x) ∈# mp_rx (rx, b)" and c: "Conflict_Var s t y" and inf: "inf_sort (snd y)"
by blast
from c conflicts(5)[of s t] have st: "s ≠ t" by auto
from s[unfolded mp_rx_def List.maps_def]
obtain ss where xss: "(x,ss) ∈ set rx" and s: "s ∈ set ss" by auto
from t[unfolded mp_rx_def List.maps_def]
obtain ts where xts: "(x,ts) ∈ set rx" and t: "t ∈ set ts" by auto
from wf[unfolded mp3 wf_lr_def wf_rx_def] have "distinct (map fst rx)" by auto
from eq_key_imp_eq_value[OF this xss xts] t have t: "t ∈ set ss" by auto
with s st have "f (x,ss)" unfolding f_def by (cases ss; cases "tl ss"; auto)
hence "(x, ss) ∈ set (filter f rx)" using xss by auto
with s t have "(s, Var x) ∈# mp_rx (filter f rx, b)" "(t, Var x) ∈# mp_rx (filter f rx, b)"
unfolding mp_rx_def List.maps_def by auto
with c inf
show ?ivcf unfolding inf_var_conflict_def by blast
qed
also have "… = b" using wf unfolding mp3 wf_lr_def wf_rx_def by auto
finally have ivcf: "?ivcf = b" .
show "wf_lr2 (match_var_impl mp)"
proof (cases "xl = []")
case False
from ivcf False wf[unfolded mp3] show ?thesis
unfolding mp' wf_lr2_def wf_lr_def split wf_rx_def by (auto simp: distinct_map_filter)
next
case True
with xs have "xs = []" by auto
with True wf[unfolded mp3]
show ?thesis
unfolding wf_lr2_def mp' split wf_rx2_def wf_rx_def ivcf
unfolding mp' wf_lr2_def wf_lr_def split wf_rx_def wf_rx2_def wf_ts_def wf_ts2_def f_def
apply (clarsimp simp: distinct_map_filter)
subgoal for x ts by (cases ts; cases "tl ts"; force)
done
qed
{
fix xt t
assume del: "(t, xt) ∈# deleted"
from this[unfolded deleted_def mp_rx_def, simplified]
obtain x ts where mem: "(x,ts) ∈ set rx" and nf: "¬ f (x, ts)" and t: "t ∈ set ts" and xt: "xt = Var x" by force
note del = del[unfolded xt]
from nf[unfolded f_def split] t have xxs: "x ∉ set xs" and ts: "ts = [t]" by (cases ts; cases "tl ts", auto)+
from split_list[OF mem[unfolded ts]] obtain rx1 rx2 where rx: "rx = rx1 @ (x,[t]) # rx2" by auto
from wf[unfolded wf_lr_def mp3] have wf: "wf_rx (rx,b)" by auto
hence "distinct (map fst rx)" unfolding wf_rx_def by auto
with rx have xrx: "x ∉ fst ` set rx1 ∪ fst ` set rx2" by auto
define mp'' where "mp'' = mp_rx (filter (Not ∘ f) (rx1 @ rx2), b)"
have eq: "deleted = add_mset (t, Var x) mp''"
unfolding deleted_def mp''_def rx mp_rx_def List.maps_def mset_concat_union using nf ts by auto
have "∃ x mp''. xt = Var x ∧ deleted = add_mset (t, Var x) mp'' ∧ x ∉ ⋃ (vars ` snd ` (mp_mset mp'' ∪ mp_mset mp'))"
proof (intro exI conjI, rule xt, rule eq, intro notI)
assume "x ∈ ⋃ (vars ` snd ` (mp_mset mp'' ∪ mp_mset mp'))"
then obtain s t' where st: "(s,t') ∈ mp_mset (mp' + mp'')" and xt: "x ∈ vars t'" by force
from xrx have "(s,t') ∉ mp_mset mp''" using xt unfolding mp''_def mp_rx_def by force
with st have "(s,t') ∈ mp_mset mp'" by auto
with xxs have "(s, t') ∈# mp_rx (filter f rx, b)" using xt unfolding xs_def mp'_def mp_rx_def
by auto
with xt nf show False unfolding mp_rx_def f_def split ts list.sel
by auto (metis Un_iff ‹¬ (tl ts ≠ [] ∨ x ∈ set xs)› fst_conv image_eqI prod.inject rx set_ConsD set_append ts xrx)
qed
} note lin_vars = this
show "(→⇩m)⇧*⇧* (mp_lr mp) (mp_lr (match_var_impl mp))" unfolding mp mp'(1) using lin_vars
proof (induct deleted)
case (add pair deleted)
obtain t xt where pair: "pair = (t,xt)" by force
hence "(t,xt) ∈# add_mset pair deleted" by auto
from add(2)[OF this] pair
obtain x where "add_mset pair deleted + mp' = add_mset (t, Var x) (deleted + mp')"
and x: "x ∉ ⋃ (vars ` snd ` (mp_mset (deleted + mp')))"
and pair: "pair = (t, Var x)"
by auto
from match_match[OF this(2), of t, folded this(1)]
have one: "add_mset pair deleted + mp' →⇩m (deleted + mp')" .
have two: "(→⇩m)⇧*⇧* (deleted + mp') mp'"
proof (rule add(1), goal_cases)
case (1 s yt)
hence "(s,yt) ∈# add_mset pair deleted" by auto
from add(2)[OF this]
obtain y mp'' where yt: "yt = Var y" "add_mset pair deleted = add_mset (s, Var y) mp''"
"y ∉ ⋃ (vars ` snd ` (mp_mset mp'' ∪ mp_mset mp'))"
by auto
from 1[unfolded yt] have "y ∈ ⋃ (vars ` snd ` (mp_mset (deleted + mp')))" by force
with x have "x ≠ y" by auto
with pair yt have "pair ≠ (s,Var y)" by auto
with yt(2) have del: "deleted = add_mset (s, Var y) (mp'' - {#pair#})"
by (meson add_eq_conv_diff)
show ?case
by (intro exI conjI, rule yt, rule del, rule contra_subsetD[OF _ yt(3)])
(intro UN_mono, auto dest: in_diffD)
qed
from one two show ?case by auto
qed auto
qed
lemma match_steps_impl: assumes "match_steps_impl mp = res"
shows "res = Some mp' ⟹ (→⇩m)⇧*⇧* (mp_list mp) (mp_lr mp') ∧ wf_lr2 mp'"
and "res = None ⟹ ∃ mp'. (→⇩m)⇧*⇧* (mp_list mp) mp' ∧ match_fail mp'"
proof (atomize (full), goal_cases)
case 1
obtain res' where decomp: "decomp_impl mp = res'" by auto
note res = assms[unfolded match_steps_impl_def decomp]
note decomp = decomp_impl[OF decomp, of _ "{#}", unfolded empty_neutral]
show ?case
proof (cases res')
case None
with decomp res show ?thesis by auto
next
case (Some mp'')
with decomp[of mp'']
have steps: "(→⇩m)⇧*⇧* (mp_list mp) (mp_lr mp'')" and wf: "wf_lr mp''" by auto
from res[unfolded Some] have res: "res = Some (match_var_impl mp'')" by auto
from match_var_impl[OF wf] steps res show ?thesis by auto
qed
qed
lemma pat_inner_impl: assumes "pat_inner_impl p pd = res"
and "wf_pat_lr pd"
and "tvars_pp (pat_mset (pat_mset_list p + pat_lr pd)) ⊆ V"
shows "res = None ⟹ (add_mset (pat_mset_list p + pat_lr pd) P, P) ∈ ⇛⇧+"
and "res = Some p' ⟹ (add_mset (pat_mset_list p + pat_lr pd) P, add_mset (pat_lr p') P) ∈ ⇛⇧*
∧ wf_pat_lr p' ∧ tvars_pp (pat_mset (pat_lr p')) ⊆ V"
proof (atomize(full), insert assms, induct p arbitrary: pd res p')
case Nil
then show ?case by (auto simp: wf_pat_lr_def pat_mset_list_def pat_lr_def)
next
case (Cons mp p pd res p')
let ?p = "pat_mset_list p + pat_lr pd"
have id: "pat_mset_list (mp # p) + pat_lr pd = add_mset (mp_list mp) ?p" unfolding pat_mset_list_def by auto
show ?case
proof (cases "match_steps_impl mp")
case (Some mp')
from match_steps_impl(1)[OF Some refl]
have steps: "(→⇩m)⇧*⇧* (mp_list mp) (mp_lr mp')" and wf: "wf_lr2 mp'" by auto
have id2: "pat_mset_list p + pat_lr (mp' # pd) = add_mset (mp_lr mp') ?p" unfolding pat_lr_def by auto
from mp_step_mset_steps_vars[OF steps] Cons(4)
have vars: "tvars_pp (pat_mset (pat_mset_list p + pat_lr (mp' # pd))) ⊆ V"
unfolding id2 by (auto simp: tvars_pp_def pat_mset_list_def)
note steps = mp_step_mset_cong[OF steps, of ?p P, folded id]
note res = Cons(2)[unfolded pat_inner_impl.simps Some option.simps]
show ?thesis
proof (cases "empty_lr mp'")
case False
with Cons(3) wf have wf: "wf_pat_lr (mp' # pd)" unfolding wf_pat_lr_def by auto
from res False have "pat_inner_impl p (mp' # pd) = res" by auto
from Cons(1)[OF this wf, of p', OF vars, unfolded id2] steps
show ?thesis by auto
next
case True
with wf have id3: "mp_lr mp' = {#}" unfolding wf_lr2_def empty_lr_def by (cases mp', auto simp: mp_lr_def mp_rx_def List.maps_def)
from True res have res: "res = None" by auto
have "(add_mset (add_mset (mp_lr mp') ?p) P, P) ∈ P_step"
unfolding id3 P_step_def using P_simp_pp[OF pat_remove_pp[of ?p], of P] by auto
with res steps show ?thesis by auto
qed
next
case None
from match_steps_impl(2)[OF None refl] obtain mp' where
"(→⇩m)⇧*⇧* (mp_list mp) mp'" and fail: "match_fail mp'" by auto
note steps = mp_step_mset_cong[OF this(1), of ?p P, folded id]
from P_simp_pp[OF pat_remove_mp[OF fail, of ?p], of P]
have "(add_mset (add_mset mp' ?p) P, add_mset ?p P) ∈ P_step"
unfolding P_step_def by auto
with steps have steps: "(add_mset (pat_mset_list (mp # p) + pat_lr pd) P, add_mset ?p P) ∈ P_step^*" by auto
note res = Cons(2)[unfolded pat_inner_impl.simps None option.simps]
have vars: "tvars_pp (pat_mset (pat_mset_list p + pat_lr pd)) ⊆ V"
using Cons(4) unfolding tvars_pp_def pat_mset_list_def by auto
from Cons(1)[OF res Cons(3), of p', OF vars] steps
show ?thesis by auto
qed
qed
lemma pat_mset_list: "pat_mset (pat_mset_list p) = pat_list p"
unfolding pat_list_def pat_mset_list_def by (auto simp: image_comp)
text ‹Main simulation lemma for a single @{const pat_impl} step.›
lemma pat_impl: assumes "pat_impl n p = res"
and vars: "fst ` tvars_pp (pat_list p) ⊆ {..<n}"
shows "res = None ⟹ ∃ p'. (add_mset (pat_mset_list p) P, add_mset p' P) ∈ ⇛⇧* ∧ pat_fail p'"
and "res = Some ps ⟹ (add_mset (pat_mset_list p) P, mset (map pat_mset_list ps) + P) ∈ ⇛⇧+
∧ fst ` tvars_pp (⋃ (pat_list ` set ps)) ⊆ {..<n+m}"
proof (atomize(full), goal_cases)
case 1
have wf: "wf_pat_lr []" unfolding wf_pat_lr_def by auto
have "fst ` tvars_pp (pat_mset (pat_mset_list p)) ⊆ {..<n}"
using vars unfolding pat_mset_list .
hence vars: "tvars_pp (pat_mset (pat_mset_list p)) ⊆ {..<n} × UNIV" by force
have "pat_mset_list p + pat_lr [] = pat_mset_list p" unfolding pat_lr_def by auto
note pat_inner = pat_inner_impl[OF refl wf, of p, unfolded this, OF vars]
note res = assms(1)[unfolded pat_impl_def]
show ?case
proof (cases "pat_inner_impl p []")
case None
from pat_inner(1)[OF this, of P] res[unfolded None option.simps] vars
show ?thesis by (auto simp: tvars_pp_def)
next
case (Some p')
from pat_inner(2)[OF this, of P]
have steps: "(add_mset (pat_mset_list p) P, add_mset (pat_lr p') P) ∈ ⇛⇧*" and wf: "wf_pat_lr p'"
and varsp': "tvars_pp (pat_mset (pat_lr p')) ⊆ {..<n} × UNIV" by auto
note res = res[unfolded Some option.simps]
show ?thesis
proof (cases "∀mp∈set p'. snd (snd mp)")
case True
with res have res: "res = None" by auto
have "pat_fail (pat_lr p')"
proof (intro pat_failure' ballI)
fix mps
assume "mps ∈ pat_mset (pat_lr p')"
then obtain mp where mem: "mp ∈ set p'" and mps: "mps = mp_mset (mp_lr mp)" by (auto simp: pat_lr_def)
obtain lx rx b where mp: "mp = (lx,rx,b)" by (cases mp, auto)
from mp mem True have b by auto
with wf[unfolded wf_pat_lr_def, rule_format, OF mem, unfolded wf_lr2_def mp split]
have "inf_var_conflict (set_mset (mp_rx (rx,b)))" unfolding wf_rx_def wf_rx2_def by (auto split: if_splits)
thus "inf_var_conflict mps" unfolding mps mp_lr_def mp split
unfolding inf_var_conflict_def by fastforce
qed
with steps res
show ?thesis by auto
next
case False
define p'l where "p'l = map mp_lr_list p'"
define x where "x = find_var p'"
define ps where "ps = map (λτ. subst_pat_problem_list τ p'l) (τs_list n x)"
have id: "pat_lr p' = pat_mset_list p'l" unfolding pat_mset_list_def pat_lr_def p'l_def map_map o_def
by (intro arg_cong[of _ _ mset] map_cong refl, auto simp: mp_lr_def mp_lr_list_def mp_rx_def mp_rx_list_def)
from False have "(∀mp∈set p'. snd (snd mp)) = False" by auto
from res[unfolded this if_False Let_def, folded p'l_def x_def, folded ps_def]
have res: "res = Some ps" by auto
have step: "(add_mset (pat_lr p') P, mset (map pat_mset_list ps) + P) ∈ ⇛"
unfolding P_step_def
proof (standard, unfold split, intro P_simp_pp)
note x = x_def[unfolded find_var_def]
let ?concat = "concat (map (λ (lx,_). lx) p')"
have disj: "tvars_disj_pp {n..<n + m} (pat_mset (pat_lr p'))"
using varsp' unfolding tvars_pp_def tvars_disj_pp_def tvars_mp_def by force
have subst: "map (λτ. subst_pat_problem_mset τ (pat_lr p')) (τs_list n x) = map pat_mset_list ps"
unfolding id
unfolding ps_def subst_pat_problem_list_def subst_pat_problem_mset_def subst_match_problem_mset_def
subst_match_problem_list_def map_map o_def
by (intro list.map_cong0, auto simp: pat_mset_list_def o_def image_mset.compositionality)
show "pat_lr p' ⇒⇩m mset (map pat_mset_list ps)"
proof (cases ?concat)
case (Cons pair list)
with x obtain t where concat: "?concat = (x,t) # list" by (cases pair, auto)
hence "(x,t) ∈ set ?concat" by auto
then obtain mp where "mp ∈ set p'" and "(x,t) ∈ set ((λ (lx,_). lx) mp)" by auto
then obtain lx rx where mem: "(lx,rx) ∈ set p'" and xt: "(x,t) ∈ set lx" by auto
from wf mem have wf: "wf_lx lx" unfolding wf_pat_lr_def wf_lr2_def by auto
with xt have t: "is_Fun t" unfolding wf_lx_def by auto
from mem obtain p'' where pat: "pat_lr p' = add_mset (mp_lr (lx,rx)) p''"
unfolding pat_lr_def by simp (metis in_map_mset mset_add set_mset_mset)
from xt have xt: "(Var x, t) ∈# mp_lr (lx,rx)" unfolding mp_lr_def by force
from pat_instantiate[OF _ disjI1[OF conjI[OF xt t]], of n p'', folded pat, OF disj]
show ?thesis unfolding subst .
next
case Nil
let ?fp = "filter (Not ∘ snd ∘ snd) p'"
from False have "set ?fp ≠ {}" unfolding o_def filter_empty_conv set_empty
by auto
then obtain mp p'' where fp: "?fp = mp # p''" by (cases ?fp) auto
obtain lx rx b where mp: "mp = (lx,rx,b)" by (cases mp) auto
have mpp: "mp ∈ set p'" using arg_cong[OF fp, of set] by auto
from mp mpp Nil have lx: "lx = []" by auto
from fp have "(lx,rx,b) ∈ set ?fp" unfolding mp by auto
hence "¬ b" unfolding o_def by auto
with mp lx have mp: "mp = ([],rx,False)" by auto
from wf mpp have wf: "wf_lr2 mp" and ne: "¬ empty_lr mp" unfolding wf_pat_lr_def by auto
from wf[unfolded wf_lr2_def mp split] mp
have wf: "wf_rx2 (rx, False)" and mp: "mp = ([],rx,False)" by auto
from ne[unfolded empty_lr_def mp split] obtain y ts rx'
where rx: "rx = (y,ts) # rx'" by (cases rx, auto)
from wf[unfolded wf_rx2_def] have ninf: "¬ inf_var_conflict (mp_mset (mp_rx (rx, False)))"
and wf: "wf_ts2 ts" unfolding rx by auto
from wf[unfolded wf_ts2_def] obtain s t ts' where ts: "ts = s # t # ts'" and
diff: "s ≠ t" and conf: "conflicts s t ≠ None"
by (cases ts; cases "tl ts", auto)
from conf obtain xs where conf: "conflicts s t = Some xs" by (cases "conflicts s t", auto)
with conflicts(5)[of s t] diff have "xs ≠ []" by auto
with x[unfolded Nil list.simps fp list.sel mp split Let_def rx ts conf option.sel]
obtain xs' where xs: "xs = x # xs'" by (cases xs) auto
from conf xs have confl: "Conflict_Var s t x" by auto
from ts rx have sty: "(s, Var y) ∈# mp_rx (rx, False)" "(t, Var y) ∈# mp_rx (rx,False)"
by (auto simp: mp_rx_def List.maps_def)
with confl ninf have "¬ inf_sort (snd x)" unfolding inf_var_conflict_def by blast
with sty confl rx have main: "(s, Var y) ∈# mp_lr mp ∧ (t, Var y) ∈# mp_lr mp ∧ Conflict_Var s t x ∧ ¬ inf_sort (snd x)"
unfolding mp by (auto simp: mp_lr_def)
from mpp obtain p'' where pat: "pat_lr p' = add_mset (mp_lr mp) p''"
unfolding pat_lr_def by simp (metis in_map_mset mset_add set_mset_mset)
from pat_instantiate[OF _ disjI2[OF main], of n p'', folded pat, OF disj]
show ?thesis unfolding subst .
qed
qed
have "fst ` tvars_pp (⋃ (pat_list ` set ps)) ⊆ {..<n + m}"
proof
fix yn
assume "yn ∈ fst ` tvars_pp (⋃ (pat_list ` set ps))"
then obtain pi y mp where pi: "pi ∈ set ps" and mp: "mp ∈ set pi" and y: "y ∈ tvars_mp (set mp)" and yn: "yn = fst y"
unfolding tvars_pp_def pat_list_def by force
from pi[unfolded ps_def set_map subst_pat_problem_list_def subst_match_problem_list_def, simplified]
obtain τ where tau: "τ ∈ set (τs_list n x)" and pi: "pi = map (map (subst_left τ)) p'l" by auto
from tau[unfolded τs_list_def]
obtain info where "info ∈ set (Cl (snd x))" and tau: "τ = τc n x info" by auto
from Cl_len[of "snd x"] this(1) have len: "length (snd info) ≤ m" by force
from mp[unfolded pi set_map] obtain mp' where mp': "mp' ∈ set p'l" and mp: "mp = map (subst_left τ) mp'" by auto
from y[unfolded mp tvars_mp_def image_comp o_def set_map]
obtain pair where *: "pair ∈ set mp'" "y ∈ vars (fst (subst_left τ pair))" by auto
obtain s t where pair: "pair = (s,t)" by force
from *[unfolded pair] have st: "(s,t) ∈ set mp'" and y: "y ∈ vars (s ⋅ τ)" unfolding subst_left_def by auto
from y[unfolded vars_term_subst, simplified] obtain z where z: "z ∈ vars s" and y: "y ∈ vars (τ z)" by auto
obtain f ss where info: "info = (f,ss)" by (cases info, auto)
with len have len: "length ss ≤ m" by auto
define ts :: "('f,_)term list" where "ts = map Var (zip [n..<n + length ss] ss)"
from tau[unfolded τc_def info split] have tau: "τ = subst x (Fun f ts)" unfolding ts_def by auto
have "fst ` vars (Fun f ts) ⊆ {..< n + length ss}" unfolding ts_def by (auto simp: set_zip)
also have "… ⊆ {..< n + m}" using len by auto
finally have subst: "fst ` vars (Fun f ts) ⊆ {..< n + m}" by auto
show "yn ∈ {..<n + m}"
proof (cases "z = x")
case True
with y subst tau yn show ?thesis by auto
next
case False
hence "τ z = Var z" unfolding tau by (auto simp: subst_def)
with y have "z = y" by auto
with z have y: "y ∈ vars s" by auto
with st have "y ∈ tvars_mp (set mp')" unfolding tvars_mp_def by force
with mp' have "y ∈ tvars_pp (set ` set p'l)" unfolding tvars_pp_def by auto
also have "… = tvars_pp (pat_mset (pat_mset_list p'l))"
by (rule arg_cong[of _ _ tvars_pp], auto simp: pat_mset_list_def image_comp)
also have "… = tvars_pp (pat_mset (pat_lr p'))" unfolding id[symmetric] by simp
also have "… ⊆ {..<n} × UNIV" using varsp' .
finally show ?thesis using yn by auto
qed
qed
with step steps res show ?thesis by auto
qed
qed
qed
text ‹The simulation property for @{const pats_impl}, proven by induction
on the terminating relation of the multiset-implementation.›
lemma pats_impl_P_step: assumes "Ball (set ps) (λ p. fst ` tvars_pp (pat_list p) ⊆ {..<n})"
shows
"pats_impl n ps ⟹ (pats_mset_list ps, {#}) ∈ ⇛⇧*"
"¬ pats_impl n ps ⟹ (pats_mset_list ps, bottom_mset) ∈ ⇛⇧*"
proof (atomize(full), insert assms, induct ps arbitrary: n rule: SN_induct[OF SN_inv_image[OF SN_imp_SN_trancl[OF SN_P_step]], of pats_mset_list])
case (1 ps n)
show ?case
proof (cases ps)
case Nil
show ?thesis unfolding pats_impl.simps[of n ps] unfolding Nil by auto
next
case (Cons p ps1)
hence id: "pats_mset_list ps = add_mset (pat_mset_list p) (pats_mset_list ps1)" by auto
note res = pats_impl.simps[of n ps, unfolded Cons list.simps, folded Cons]
from 1(2)[rule_format, of p] Cons have "fst ` tvars_pp (pat_list p) ⊆ {..<n}" by auto
note pat_impl = pat_impl[OF refl this]
show ?thesis
proof (cases "pat_impl n p")
case None
with res have res: "pats_impl n ps = False" by auto
from pat_impl(1)[OF None, of "pats_mset_list ps1", folded id]
obtain p' where steps: "(pats_mset_list ps, add_mset p' (pats_mset_list ps1)) ∈ ⇛⇧*" and fail: "pat_fail p'"
by auto
show ?thesis
proof (cases "add_mset p' (pats_mset_list ps1) = bottom_mset")
case True
with res steps show ?thesis by auto
next
case False
from P_failure[OF fail False]
have "(add_mset p' (pats_mset_list ps1), bottom_mset) ∈ ⇛" unfolding P_step_def by auto
with steps res show ?thesis by simp
qed
next
case (Some ps2)
with res have res: "pats_impl n ps = pats_impl (n + m) (ps2 @ ps1)" by auto
from pat_impl(2)[OF Some, of "pats_mset_list ps1", folded id]
have steps: "(pats_mset_list ps, mset (map pat_mset_list (ps2 @ ps1))) ∈ ⇛⇧+"
and vars: "fst ` tvars_pp (⋃ (pat_list ` set ps2)) ⊆ {..<n + m}" by auto
hence rel: "(ps, ps2 @ ps1) ∈ inv_image (P_step⇧+) pats_mset_list" by auto
have vars: "∀p∈set (ps2 @ ps1). fst ` tvars_pp (pat_list p) ⊆ {..<n + m}"
proof
fix p
assume "p ∈ set (ps2 @ ps1)"
hence "p ∈ set ps2 ∨ p ∈ set ps1" by auto
thus "fst ` tvars_pp (pat_list p) ⊆ {..<n + m}"
proof
assume "p ∈ set ps2"
hence "fst ` tvars_pp (pat_list p) ⊆ fst ` tvars_pp (⋃ (pat_list ` set ps2))"
unfolding tvars_pp_def by auto
with vars show ?thesis by auto
next
assume "p ∈ set ps1"
hence "p ∈ set ps" unfolding Cons by auto
from 1(2)[rule_format, OF this] show ?thesis by auto
qed
qed
show ?thesis using 1(1)[OF rel vars] steps unfolding res[symmetric] by auto
qed
qed
qed
text ‹Consequence: partial correctness of the list-based implementation on well-formed inputs›
theorem pats_impl: assumes wf: "∀pp ∈ pat_list ` set P. wf_pat pp"
and n: "∀p∈set P. fst ` tvars_pp (pat_list p) ⊆ {..<n}"
shows "pats_impl n P ⟷ pats_complete (pat_list ` set P)"
proof -
from wf have wf: "wf_pats (pat_list ` set P)" by (auto simp: wf_pats_def)
have id: "pats_mset (pats_mset_list P) = pat_list ` set P" unfolding pat_list_def
by (auto simp: pat_mset_list_def image_comp)
{
assume "pats_impl n P"
from pats_impl_P_step(1)[OF n this]
have "(pats_mset_list P, {#}) ∈ ⇛⇧*" by auto
from P_steps_pcorrect[OF _ this, unfolded id, OF wf]
have "pats_complete (pat_list ` set P)" by auto
}
moreover
{
assume "¬ pats_impl n P"
from pats_impl_P_step(2)[OF n this]
have "(pats_mset_list P, {#{#}#}) ∈ ⇛⇧*" by auto
from P_steps_pcorrect[OF _ this, unfolded id, OF wf]
have "¬ pats_complete (pat_list ` set P)" by auto
}
ultimately show ?thesis by auto
qed
corollary pat_complete_impl:
assumes wf: "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ S"
shows "pat_complete_impl P ⟷ pats_complete (pat_list ` set P)"
proof -
have wf: "Ball (pat_list ` set P) wf_pat"
unfolding pat_list_def wf_pat_def wf_match_def tvars_mp_def using wf[unfolded set_concat image_comp] by force
let ?l = "(List.maps (map fst o vars_term_list o fst) (concat (concat P)))"
define n where "n = Suc (max_list ?l)"
have n: "∀p∈set P. fst ` tvars_pp (pat_list p) ⊆ {..<n}"
proof (intro ballI subsetI)
fix p x
assume "p ∈ set P" and "x ∈ fst ` tvars_pp (pat_list p)"
hence "x ∈ set ?l" unfolding List.maps_def tvars_pp_def tvars_mp_def pat_list_def
by force
from max_list[OF this] have "x < n" unfolding n_def by auto
thus "x ∈ {..<n}" by auto
qed
have "pat_complete_impl P = pats_impl n P"
unfolding pat_complete_impl_def n_def Let_def ..
from pats_impl[OF wf n, folded this]
show ?thesis .
qed
end
subsection ‹Getting the result outside the locale with assumptions›
text ‹We next lift the results for the list-based implementation out of the locale.
Here, we use the existing algorithms to decide non-empty sorts @{const decide_nonempty_sorts}
and to compute the infinite sorts @{const compute_inf_sorts}.›
context pattern_completeness_context
begin
lemma pat_complete_impl_wrapper: assumes C_Cs: "C = map_of Cs"
and dist: "distinct (map fst Cs)"
and inhabited: "decide_nonempty_sorts Sl Cs = None"
and S_Sl: "S = set Sl"
and inf_sort: "inf_sort = (λ s. s ∈ compute_inf_sorts Cs)"
and C: "⋀ f σs σ. ((f,σs),σ) ∈ set Cs ⟹ length σs ≤ m ∧ set (σ # σs) ⊆ S"
and Cl: "⋀ s. Cl s = map fst (filter ((=) s o snd) Cs)"
and P: "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ S"
shows "pat_complete_impl P = pats_complete (pat_list ` set P)"
proof -
from decide_nonempty_sorts(1)[OF dist C_Cs[symmetric] inhabited, folded S_Sl]
have S: "⋀ σ. σ ∈ S ⟹ ∃t. t : σ in 𝒯(C,EMPTY)"
"⋀ σ. σ ∈ S ⟹ ∃t. t : σ in 𝒯(C,EMPTYn)" unfolding EMPTY_def EMPTYn_def by auto
{
fix f ss s
assume "f : ss → s in C"
hence "((f,ss),s) ∈ set Cs" unfolding C_Cs by (auto dest!: hastype_in_ssigD map_of_SomeD)
from C[OF this] have "insert s (set ss) ⊆ S" "length ss ≤ m" by auto
} note Cons = this
{
fix f ss s
assume "(f,ss) ∈ set (Cl s)"
hence "((f,ss),s) ∈ set Cs" unfolding Cl by auto
from C[OF this] have "length ss ≤ m" by auto
}
hence m: "∀a∈length ` snd ` set (Cl s). a ≤ m" for s by auto
have En: "EMPTYn = ∅" unfolding EMPTYn_def by auto
have "∀f ss s s'. f : ss → s in C ⟶ s' ∈ set ss ⟶ (∃t. t : s' in 𝒯(C,EMPTYn))"
proof (intro allI impI)
fix f ss s s'
assume "f : ss → s in C" and "s' ∈ set ss"
hence "s' ∈ S" using Cons(1)[of f ss s] by (auto simp: hastype_in_ssig_def)
from S[OF this] show "∃t. t : s' in 𝒯(C,EMPTYn)" by auto
qed
from compute_inf_sorts[OF En C_Cs this dist] inf_sort
have inf_sort: "inf_sort s = (¬ bdd_above (size ` {t. t : s in 𝒯(C,EMPTYn)}))" for s unfolding inf_sort by auto
have Cl: "set (Cl s) = {(f,ss). f : ss → s in C}" for s
unfolding Cl set_map o_def C_Cs using dist
by (force simp: hastype_in_ssig_def)
interpret pattern_completeness_context_with_assms
apply unfold_locales
subgoal by (rule S(1))
subgoal by (rule Cons)
subgoal by (rule Cons)
subgoal by (rule inf_sort)
subgoal by (rule Cl)
subgoal by (rule m)
done
show ?thesis by (rule pat_complete_impl[OF P])
qed
end
text ‹Next we are also leaving the locale that fixed the common parameters,
and chooses suitable values.›
text ‹extract all sorts from a ssignature (input and target sorts)›
definition sorts_of_ssig_list :: "(('f × 's list) × 's)list ⇒ 's list" where
"sorts_of_ssig_list Cs = remdups (List.maps (λ ((f,ss),s). s # ss) Cs)"
definition decide_pat_complete :: "(('f × 's list) × 's)list ⇒ ('f,'v,'s)pats_problem_list ⇒ bool" where
"decide_pat_complete Cs P = (let Sl = sorts_of_ssig_list Cs;
m = max_list (map (length o snd o fst) Cs);
Cl = (λ s. map fst (filter ((=) s ∘ snd) Cs));
IS = compute_inf_sorts Cs
in pattern_completeness_context.pat_complete_impl m Cl (λ s. s ∈ IS)) P"
abbreviation (input) pat_complete where
"pat_complete ≡ pattern_completeness_context.pat_complete"
abbreviation (input) pats_complete where
"pats_complete ≡ pattern_completeness_context.pats_complete"
text ‹Finally: a pattern completeness decision procedure for arbitrary inputs,
assuming sensible inputs›
theorem decide_pat_complete: assumes C_Cs: "C = map_of Cs"
and dist: "distinct (map fst Cs)"
and non_empty_sorts: "decide_nonempty_sorts (sorts_of_ssig_list Cs) Cs = None"
and S: "S = set (sorts_of_ssig_list Cs)"
and P: "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ S"
shows "decide_pat_complete Cs P = pats_complete S C (pat_list ` set P)"
unfolding decide_pat_complete_def Let_def
proof (rule pattern_completeness_context.pat_complete_impl_wrapper[OF C_Cs dist non_empty_sorts S refl _ refl P])
fix f σs σ
assume mem: "((f, σs), σ) ∈ set Cs"
hence "length σs ∈ set (map (length ∘ snd ∘ fst) Cs)" by force
from max_list[OF this] mem
show "length σs ≤ max_list (map (length ∘ snd ∘ fst) Cs) ∧ set (σ # σs) ⊆ S"
unfolding S sorts_of_ssig_list_def List.maps_def by force
qed
end