Theory Pattern_Completeness
section ‹Pattern-Completeness and Related Properties›
text ‹We use the core decision procedure for pattern completeness
and connect it to other properties like pattern completeness of programs (where the lhss are given),
or (strong) quasi-reducibility.›
theory Pattern_Completeness
imports
Pattern_Completeness_List
Show.Shows_Literal
Certification_Monads.Check_Monad
begin
text ‹A pattern completeness decision procedure for a set of lhss›
definition basic_terms :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('v ⇀ 's) ⇒ ('f,'v)term set" (‹ℬ'(_,_,_')›) where
"ℬ(C,D,V) = { Fun f ts | f ss s ts . f : ss → s in D ∧ ts :⇩l ss in 𝒯(C,V)}"
abbreviation basic_ground_terms :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,unit)term set" (‹ℬ'(_,_')›) where
"ℬ(C,D) ≡ ℬ(C,D,λx. None)"
definition matches :: "('f,'v)term ⇒ ('f,'w)term ⇒ bool" (infix ‹matches› 50) where
"l matches t = (∃ σ. t = l ⋅ σ)"
lemma matches_subst: "l matches t ⟹ l matches t⋅σ"
by (auto simp: matches_def simp flip: subst_subst_compose)
definition pat_complete_lhss :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,'v)term set ⇒ bool" where
"pat_complete_lhss C D L = (∀ t ∈ ℬ(C,D). ∃l ∈ L. l matches t)"
lemma pat_complete_lhssD:
assumes comp: "pat_complete_lhss C D L" and t: "t ∈ ℬ(C,D,∅)"
shows "∃l ∈ L. l matches t"
proof -
note * = map_subst_hastype[OF sorted_map_empty, of C _ _ "∅::unit⇀_" undefined]
from t have "t⋅undefined ∈ ℬ(C,D)" (is "?t ∈ _")
by (force simp: basic_terms_def * cong: ex_cong)
from comp[unfolded pat_complete_lhss_def, rule_format, OF this]
obtain l where l: "l ∈ L" "l matches ?t" by auto
from t
have t2: "?t ⋅ undefined = t"
by (auto simp: basic_terms_def o_def
simp: hastype_in_Term_empty_imp_map_subst_subst hastype_in_Term_empty_imp_map_subst_id)
from l show "∃l ∈ L. l matches t"
apply (subst t2[symmetric])
by (force simp: matches_subst)
qed
definition pats_of_lhss :: "(('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ ('f,'v,'s)pat_problem_list list" where
"pats_of_lhss D lhss = (let pats = [Fun f (map Var (zip [0..<length ss] ss)). ((f,ss),s) ← D]
in [[[(pat,lhs)]. lhs ← lhss]. pat ← pats])"
definition check_signatures :: "(('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ showsl check" where
"check_signatures C D = do {
check (distinct (map fst C)) (showsl_lit (STR ''constructor information contains duplicate''));
check (distinct (map fst D)) (showsl_lit (STR ''defined symbol information contains duplicate''));
let S = sorts_of_ssig_list C;
check_allm (λ ((f,ss),_). check_allm (λ s. check (s ∈ set S)
(showsl_lit (STR ''a defined symbol has argument sort that is not known in constructors''))) ss) D;
(case (decide_nonempty_sorts S C) of None ⇒ return () | Some s ⇒ error (showsl_lit (STR ''some sort is empty'')))
}"
definition decide_pat_complete_linear_lhss ::
"(('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ showsl + bool" where
"decide_pat_complete_linear_lhss C D lhss = do {
check_signatures C D;
return (decide_pat_complete_lin C (pats_of_lhss D lhss))
}"
definition decide_pat_complete_lhss ::
"(('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ showsl + bool" where
"decide_pat_complete_lhss C D lhss = do {
check_signatures C D;
return (decide_pat_complete C (pats_of_lhss D lhss))
}"
definition decide_pat_complete_lhss_fidl ::
"_ ⇒ _ ⇒ _ ⇒ (('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ showsl + bool" where
"decide_pat_complete_lhss_fidl rn rv fidl_solver C D lhss = do {
check_signatures C D;
return (decide_pat_complete_fidl rn rv fidl_solver C (pats_of_lhss D lhss))
}"
lemma pats_of_lhss_vars: assumes condD: "∀x∈set D. ∀a b. (∀x2. x ≠ ((a, b), x2)) ∨ (∀x∈set b. x ∈ S)"
shows "snd ` ⋃ (vars ` fst ` set (concat (concat (pats_of_lhss D lhss)))) ⊆ S"
proof -
{
fix i si f ss s
assume mem: "((f, ss), s) ∈ set D" and isi: "(i, si) ∈ set (zip [0..<length ss] ss)"
from isi have si: "si ∈ set ss" by (metis in_set_zipE)
from mem si condD
have "si ∈ S" by auto
}
thus ?thesis unfolding pats_of_lhss_def by force
qed
lemma check_signatures: assumes "isOK(check_signatures C D)"
shows "distinct (map fst C)" (is ?G1)
and "distinct (map fst D)" (is ?G2)
and "∀x∈set D. ∀a b. (∀x2. x ≠ ((a, b), x2)) ∨ (∀x∈set b. x ∈ set (sorts_of_ssig_list C))" (is ?G3)
and "decide_nonempty_sorts (sorts_of_ssig_list C) C = None" (is ?G4)
proof -
let ?C = "map_of C"
let ?D = "map_of D"
define S where "S = sorts_of_ssig_list C"
have dist: "distinct (map fst C)" and distD: "distinct (map fst D)"
and dec: "decide_nonempty_sorts S C = None"
and condD: "∀x∈set D. ∀a b. (∀x2. x ≠ ((a, b), x2)) ∨ (∀x∈set b. x ∈ set S)"
using assms
apply (unfold check_signatures_def)
apply (unfold Let_def S_def[symmetric])
apply (auto split: prod.splits option.splits)
done
show ?G1 ?G2 ?G3 ?G4 unfolding S_def[symmetric] by fact+
qed
lemma pats_of_lhss:
assumes "isOK(check_signatures C D)"
shows "pats_complete (map_of C) (pat_list ` set (pats_of_lhss D lhss)) =
(∀t∈ℬ(map_of C,map_of D). ∃l∈set lhss. l matches t)"
proof -
define S where "S = sorts_of_ssig_list C"
note * = check_signatures[OF assms, folded S_def]
note distC = *(1) note distD = *(2) note condD = *(3) note dec = *(4)
define pats where "pats = map (λ ((f,ss),s). Fun f (map Var (zip [0..<length ss] ss))) D"
define P where "P = map (λ pat. map (λ lhs. [(pat,lhs)]) lhss) pats"
note condD = condD[folded S_def]
note dec = dec[folded S_def]
let ?C = "map_of C"
let ?D = "map_of D"
let ?L = "{ pat ⋅ σ | pat σ. pat ∈ set pats ∧ σ :⇩s {x : ι in 𝒱. ι ∈ set S} → 𝒯(?C)}"
interpret pattern_completeness_list C
rewrites "sorts_of_ssig_list C = S"
apply unfold_locales
using distC dec by (auto simp: S_def)
from condD
have wf: "wf_pats (pat_list ` set P)"
by (force simp: P_def pats_def wf_pats_def wf_pat_def pat_list_def wf_match_def tvars_match_def
elim!: in_set_zipE)
let ?match_lhs = "λt. ∃l ∈ set lhss. l matches t"
have "pats_complete ?C (pat_list ` set (pats_of_lhss D lhss))
= pats_complete ?C (pat_list ` set P)" unfolding P_def pats_of_lhss_def pats_def by auto
also note wf_pats_complete_iff[OF wf]
also have "pat_list ` set P = { { {(pat,lhs)} | lhs. lhs ∈ set lhss} | pat. pat ∈ set pats}"
unfolding pat_list_def P_def by (auto simp: image_comp)
also have "(∀f :⇩s {x : ι in 𝒱. ι ∈ set S} → 𝒯(map_of C).
∀pp∈{{{(pat, lhs)} |lhs. lhs ∈ set lhss} |pat. pat ∈ set pats}.
∃mp∈pp. match_complete_wrt f mp) = Ball { pat ⋅ σ | pat σ. pat ∈ set pats ∧ σ :⇩s {x : ι in 𝒱. ι ∈ set S} → 𝒯(?C)} ?match_lhs" (is "_ = Ball ?L _")
apply (simp add: imp_ex match_complete_wrt_def matches_def Bex_def conj_commute
imp_conjL flip:ex_simps(1) all_simps(6) split: prod.splits
cong: all_cong1 ex_cong1 conj_cong imp_cong)
apply (subst all_comm)
by (simp add: ac_simps verit_bool_simplify(4) o_def)
also have "?L = ℬ(?C,?D,∅)" (is "_ = ?R")
proof
{
fix pat and σ
assume pat: "pat ∈ set pats" and subst: "σ :⇩s {x : ι in 𝒱. ι ∈ set S} → 𝒯(?C)"
from pat[unfolded pats_def] obtain f ss s where pat: "pat = Fun f (map Var (zip [0..<length ss] ss))"
and inDs: "((f,ss),s) ∈ set D" by auto
from distD inDs have f: "f : ss → s in ?D" unfolding fun_hastype_def by simp
{
fix i
assume i: "i < length ss"
hence "ss ! i ∈ set ss" by auto
with inDs condD have "ss ! i ∈ set S" by (auto simp: S_def)
then
have "σ (i, ss ! i) : ss ! i in 𝒯(?C)"
by (auto intro!: sorted_mapD[OF subst] simp: hastype_restrict)
} note ssigma = this
define ts where "ts = (map (λ i. σ (i, ss ! i)) [0..<length ss])"
have ts: "ts :⇩l ss in 𝒯(?C)" unfolding list_all2_conv_all_nth ts_def using ssigma by auto
have pat: "pat ⋅ σ = Fun f ts"
unfolding pat ts_def by (auto intro: nth_equalityI)
from pat f ts have "pat ⋅ σ ∈ ?R" unfolding basic_terms_def by auto
}
thus "?L ⊆ ?R" by auto
{
fix f ss s and ts
assume f: "f : ss → s in ?D" and ts: "ts :⇩l ss in 𝒯(?C)"
from ts have len: "length ts = length ss" by (metis list_all2_lengthD)
define pat where "pat = Fun f (map Var (zip [0..<length ss] ss))"
from f have "((f,ss),s) ∈ set D" unfolding fun_hastype_def by (metis map_of_SomeD)
hence pat: "pat ∈ set pats" unfolding pat_def pats_def by force
define σ where "σ x = (case x of (i,s) ⇒ if i < length ss ∧ s = ss ! i then ts ! i else
(SOME t. t : s in 𝒯(?C)))" for x
have id: "Fun f ts = pat ⋅ σ" unfolding pat_def using len
by (auto intro!: nth_equalityI simp: σ_def)
have ssigma: "σ :⇩s {x : ι in 𝒱. ι ∈ set S} → 𝒯(?C)"
proof (intro sorted_mapI)
fix x ι
assume "x : ι in {x : ι in 𝒱. ι ∈ set S}"
then have "ι = snd x" and s: "ι ∈ set S" by auto
then obtain i where x: "x = (i,ι)" by (cases x, auto)
show "σ x : ι in 𝒯(?C)"
proof (cases "i < length ss ∧ ι = ss ! i")
case True
hence id: "σ x = ts ! i" unfolding x σ_def by auto
from ts True show ?thesis unfolding id unfolding x snd_conv
by (auto simp add: list_all2_conv_all_nth)
next
case False
hence id: "σ x = (SOME t. t : ι in 𝒯(?C))" unfolding x σ_def by auto
from decide_nonempty_sorts(1)[OF distC dec] s
have "∃ t. t : ι in 𝒯(?C)" by (auto elim!: not_empty_sortE simp: S_def)
from someI_ex[OF this] have "σ x : ι in 𝒯(?C)" unfolding id .
thus ?thesis unfolding x by auto
qed
qed
from pat id ssigma
have "Fun f ts ∈ ?L" by auto
}
thus "?R ⊆ ?L" unfolding basic_terms_def by auto
qed
finally show ?thesis .
qed
theorem decide_pat_complete_lhss:
fixes C D :: "(('f × 's list) × 's) list" and lhss :: "('f,'v)term list"
assumes "decide_pat_complete_lhss C D lhss = return b"
shows "b = pat_complete_lhss (map_of C) (map_of D) (set lhss)"
proof -
let ?C = "map_of C"
let ?D = "map_of D"
define S where "S = sorts_of_ssig_list C"
define P where "P = pats_of_lhss D lhss"
have sig: "isOK(check_signatures C D)"
and b: "b = decide_pat_complete C P"
using assms
apply (unfold decide_pat_complete_lhss_def)
apply (unfold Let_def P_def[symmetric] S_def[symmetric])
by auto
note * = check_signatures[OF sig]
note distC = *(1) note distD = *(2) note condD = *(3) note dec = *(4)
interpret pattern_completeness_list C
rewrites "sorts_of_ssig_list C = S"
apply unfold_locales
using * by (auto simp: S_def)
have "b = pats_complete ?C (pat_list ` set P)"
apply (unfold b)
apply (rule decide_pat_complete[OF distC dec[unfolded S_def]])
apply (unfold P_def)
apply (rule pats_of_lhss_vars[OF condD[unfolded P_def S_def]])
done
also have "… = (∀t∈ℬ(?C,?D). ∃l∈set lhss. l matches t)" unfolding P_def
by (rule pats_of_lhss[OF sig])
finally show ?thesis unfolding pat_complete_lhss_def .
qed
theorem decide_pat_complete_linear_lhss:
fixes C D :: "(('f × 's list) × 's) list" and lhss :: "('f,'v)term list"
assumes "decide_pat_complete_linear_lhss C D lhss = return b"
and linear: "Ball (set lhss) linear_term"
shows "b = pat_complete_lhss (map_of C) (map_of D) (set lhss)"
proof -
let ?C = "map_of C"
let ?D = "map_of D"
define S where "S = sorts_of_ssig_list C"
define P where "P = pats_of_lhss D lhss"
have sig: "isOK(check_signatures C D)"
and b: "b = decide_pat_complete_lin C P"
using assms
apply (unfold decide_pat_complete_linear_lhss_def)
apply (unfold Let_def P_def[symmetric] S_def[symmetric])
by auto
note * = check_signatures[OF sig]
note distC = *(1) note distD = *(2) note condD = *(3) note dec = *(4)
interpret pattern_completeness_list C
rewrites "sorts_of_ssig_list C = S"
apply unfold_locales
using * by (auto simp: S_def)
have "b = pats_complete ?C (pat_list ` set P)"
apply (unfold b)
apply (rule decide_pat_complete_lin[OF distC dec[unfolded S_def]])
apply (unfold P_def)
apply (rule pats_of_lhss_vars[OF condD[unfolded P_def S_def]])
apply (fold P_def)
proof -
show "Ball (set P) ll_pp" unfolding ll_pp_def
proof (intro ballI)
fix p mp
assume "p ∈ set P" and mp: "mp ∈ set p"
from this[unfolded P_def pats_of_lhss_def, simplified]
obtain pat where p: "p = map (λlhs. [(pat, lhs)]) lhss" by auto
from mp[unfolded p, simplified] obtain l where mp: "mp = [(pat, l)]"
and l: "l ∈ set lhss" by auto
have vars: "vars_mp_mset (mp_list mp) = vars_term_ms l"
unfolding mp vars_mp_mset_def by auto
from l linear have l: "linear_term l" by auto
hence dist: "distinct (vars_term_list l)" by (rule linear_term_distinct_vars)
have id: "vars_term_ms l = mset (vars_term_list l)"
proof (induct l)
case (Fun f ts)
thus ?case by (simp add: vars_term_list.simps, induct ts, auto)
qed (auto simp: vars_term_list.simps)
show "ll_mp (mp_list mp)" unfolding ll_mp_def vars id using dist
by (simp add: distinct_count_atmost_1)
qed
qed
also have "… = (∀t∈ℬ(?C,?D). ∃l∈set lhss. l matches t)" unfolding P_def
by (rule pats_of_lhss[OF sig])
finally show ?thesis unfolding pat_complete_lhss_def .
qed
theorem decide_pat_complete_lhss_fidl:
fixes C D :: "(('f × 's list) × 's) list" and lhss :: "('f,'v)term list"
assumes "decide_pat_complete_lhss_fidl rn rv fidl_solver C D lhss = return b"
and ren: "renaming_funs rn rv"
and idl: "finite_idl_solver fidl_solver"
shows "b = pat_complete_lhss (map_of C) (map_of D) (set lhss)"
proof -
let ?C = "map_of C"
let ?D = "map_of D"
define S where "S = sorts_of_ssig_list C"
define P where "P = pats_of_lhss D lhss"
have sig: "isOK(check_signatures C D)"
and b: "b = decide_pat_complete_fidl rn rv fidl_solver C P"
using assms
apply (unfold decide_pat_complete_lhss_fidl_def)
apply (unfold Let_def P_def[symmetric] S_def[symmetric])
by auto
note * = check_signatures[OF sig]
note distC = *(1) note distD = *(2) note condD = *(3) note dec = *(4)
interpret pattern_completeness_list C
rewrites "sorts_of_ssig_list C = S"
apply unfold_locales
using * by (auto simp: S_def)
have "b = pats_complete ?C (pat_list ` set P)"
apply (unfold b)
apply (rule decide_pat_complete_fidl[OF distC dec[unfolded S_def] _ ren idl])
apply (unfold P_def)
apply (rule pats_of_lhss_vars[OF condD[unfolded P_def S_def]])
done
also have "… = (∀t∈ℬ(?C,?D). ∃l∈set lhss. l matches t)" unfolding P_def
by (rule pats_of_lhss[OF sig])
finally show ?thesis unfolding pat_complete_lhss_def .
qed
text ‹Definition of strong quasi-reducibility and a corresponding decision procedure›
definition strong_quasi_reducible :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,'v)term set ⇒ bool" where
"strong_quasi_reducible C D L =
(∀ t ∈ ℬ(C,D,∅::unit⇀'s). ∃ ti ∈ set (t # args t). ∃l ∈ L. l matches ti)"
definition term_and_args :: "'f ⇒ ('f,'v)term list ⇒ ('f,'v)term list" where
"term_and_args f ts = Fun f ts # ts"
definition decide_strong_quasi_reducible ::
"(('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ showsl + bool" where
"decide_strong_quasi_reducible C D lhss = do {
check_signatures C D;
let pats = map (λ ((f,ss),s). term_and_args f (map Var (zip [0..<length ss] ss))) D;
let P = map (List.maps (λ pat. map (λ lhs. [(pat,lhs)]) lhss)) pats;
return (decide_pat_complete C P)
}"
lemma decide_strong_quasi_reducible:
fixes C D :: "(('f × 's list) × 's) list" and lhss :: "('f,'v)term list"
assumes "decide_strong_quasi_reducible C D lhss = return b"
shows "b = strong_quasi_reducible (map_of C) (map_of D) (set lhss)"
proof -
let ?C = "map_of C"
let ?D = "map_of D"
let ?S = "sorts_of_ssig_list C"
define pats where "pats = map (λ ((f,ss),s). term_and_args f (map Var (zip [0..<length ss] ss))) D"
have pats: "patL ∈ set pats ⟷ (∃((f,ss),s) ∈ set D. patL = term_and_args f (map Var (zip [0..<length ss] ss)))"
for patL
by (force simp: pats_def split: prod.splits)
define P where "P = map (List.maps (λ pat. map (λ lhs. [(pat,lhs)]) lhss)) pats"
define V where "V = {x : ι in 𝒱. ι ∈ set (sorts_of_ssig_list C)}"
let ?match_lhs = "λt. ∃l ∈ set lhss. l matches t"
from assms(1)
have b: "b = decide_pat_complete C P"
and sig: "isOK (check_signatures C D)"
by (auto simp: decide_strong_quasi_reducible_def pats_def[symmetric] Let_def P_def[symmetric]
split: prod.splits option.splits)
note * = check_signatures[OF sig]
note distC = *(1) note distD = *(2) note condD = *(3) note dec = *(4)
interpret pattern_completeness_list C
apply unfold_locales using distC dec.
have wf: "wf_pats (pat_list ` set P)" using condD
by (force simp: P_def pats_def wf_pats_def wf_pat_def pat_list_def wf_match_def tvars_match_def
term_and_args_def List.maps_def
elim!: in_set_zipE split: prod.splits)
have *: "pat_list ` set P = { { {(pat,lhs)} | lhs pat. pat ∈ set patL ∧ lhs ∈ set lhss} | patL. patL ∈ set pats}"
unfolding pat_list_def P_def List.maps_def by (auto simp: image_comp) force+
have "b = pats_complete ?C (pat_list ` set P)"
apply (unfold b)
proof (rule decide_pat_complete[OF dist(1) dec])
{
fix f ss s i si
assume mem: "((f, ss), s) ∈ set D" and isi: "(i, si) ∈ set (zip [0..<length ss] ss)"
from isi have si: "si ∈ set ss" by (metis in_set_zipE)
from mem si condD
have "si ∈ set ?S" by auto
}
thus "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ set ?S" unfolding P_def pats_def term_and_args_def List.maps_def
by fastforce
qed
also have "… ⟷
(∀ σ :⇩s V → 𝒯(?C). ∀patL ∈ set pats. (∃ pat ∈ set patL. ?match_lhs (pat ⋅ σ)))" (is "_ ⟷ ?L")
apply (unfold wf_pats_complete_iff[OF wf])
apply (fold V_def)
apply (unfold *)
apply (simp add: imp_ex match_complete_wrt_def matches_def flip: Ball_def)
apply (rule all_cong)
apply (rule ball_cong)
apply simp
apply (auto simp: pats)
by blast
also have "… ⟷
(∀ f ss s ts. f : ss → s in ?D ⟶ ts :⇩l ss in 𝒯(?C) ⟶
(∃ ti ∈ set (term_and_args f ts). ?match_lhs ti))" (is "_ = ?R")
proof (intro iffI allI ballI impI)
fix patL and σ
assume patL: "patL ∈ set pats" and subst: "σ :⇩s V → 𝒯(?C)" and R: ?R
from patL[unfolded pats_def] obtain f ss s where patL: "patL = term_and_args f (map Var (zip [0..<length ss] ss))"
and inDs: "((f,ss),s) ∈ set D" by auto
from distD inDs have f: "f : ss → s in ?D" unfolding fun_hastype_def by simp
{
fix i
assume i: "i < length ss"
hence "ss ! i ∈ set ss" by auto
with inDs condD have "ss ! i ∈ set ?S" by auto
then have "σ (i, ss ! i) : ss ! i in 𝒯(?C)"
by (auto intro!: sorted_mapD[OF subst] simp: V_def)
} note ssigma = this
define ts where "ts = (map (λ i. σ (i, ss ! i)) [0..<length ss])"
have ts: "ts :⇩l ss in 𝒯(?C)" unfolding list_all2_conv_all_nth ts_def using ssigma by auto
from R[rule_format, OF f ts] obtain ti where ti: "ti ∈ set (term_and_args f ts)" and match: "?match_lhs ti" by auto
have "map (λ pat. pat ⋅ σ) patL = term_and_args f ts" unfolding patL term_and_args_def ts_def
by (auto intro: nth_equalityI)
from ti[folded this] match
show "∃pat∈set patL. ?match_lhs (pat ⋅ σ)" by auto
next
fix f ss s ts
assume f: "f : ss → s in ?D" and ts: "ts :⇩l ss in 𝒯(?C)" and L: ?L
from ts have len: "length ts = length ss" by (metis list_all2_lengthD)
define patL where "patL = term_and_args f (map Var (zip [0..<length ss] ss))"
from f have "((f,ss),s) ∈ set D" unfolding fun_hastype_def by (metis map_of_SomeD)
hence patL: "patL ∈ set pats" unfolding patL_def pats_def by force
define σ where "σ x = (case x of (i,s) ⇒ if i < length ss ∧ s = ss ! i then ts ! i else
(SOME t. t : s in 𝒯(?C)))" for x
have ssigma: "σ :⇩s V → 𝒯(?C)"
proof (intro sorted_mapI)
fix x s
assume "x : s in V"
then obtain i where x: "x = (i,s)" and s: "s ∈ set ?S" by (cases x, auto simp: V_def)
show "σ x : s in 𝒯(?C)"
proof (cases "i < length ss ∧ s = ss ! i")
case True
hence id: "σ x = ts ! i" unfolding x σ_def by auto
from ts True show ?thesis unfolding id unfolding x snd_conv
by (simp add: list_all2_conv_all_nth)
next
case False
hence id: "σ x = (SOME t. t : s in 𝒯(?C))" unfolding x σ_def by auto
from decide_nonempty_sorts(1)[OF dist dec, rule_format, OF s]
have "∃ t. t : s in 𝒯(?C)" by (auto elim!: not_empty_sortE)
from someI_ex[OF this] have "σ x : s in 𝒯(?C,∅)" unfolding id .
thus ?thesis unfolding x by auto
qed
qed
from L[rule_format, OF ssigma patL]
obtain pat where pat: "pat ∈ set patL" and match: "?match_lhs (pat ⋅ σ)" by auto
have id: "map (λ pat. pat ⋅ σ) patL = term_and_args f ts" unfolding patL_def term_and_args_def using len
by (auto intro!: nth_equalityI simp: σ_def)
show "∃ti ∈ set (term_and_args f ts). ?match_lhs ti" unfolding id[symmetric] using pat match by auto
qed
also have "… = (∀t. t ∈ ℬ(?C,?D,∅::unit⇀_) ⟶ (∃ ti ∈ set (t # args t). ?match_lhs ti))"
unfolding basic_terms_def term_and_args_def by fastforce
finally show ?thesis unfolding strong_quasi_reducible_def by blast
qed
subsection ‹Connecting Pattern-Completeness, Strong Quasi-Reducibility and Quasi-Reducibility›
definition quasi_reducible :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,'v)term set ⇒ bool" where
"quasi_reducible C D L = (∀ t ∈ ℬ(C,D,∅::unit⇀'s). ∃ tp ⊴ t. ∃l ∈ L. l matches tp)"
lemma pat_complete_imp_strong_quasi_reducible:
"pat_complete_lhss C D L ⟹ strong_quasi_reducible C D L"
unfolding pat_complete_lhss_def strong_quasi_reducible_def by force
lemma arg_imp_subt: "s ∈ set (args t) ⟹ t ⊵ s"
by (cases t, auto)
lemma strong_quasi_reducible_imp_quasi_reducible:
"strong_quasi_reducible C D L ⟹ quasi_reducible C D L"
unfolding strong_quasi_reducible_def quasi_reducible_def
by (force dest: arg_imp_subt)
text ‹If no root symbol of a left-hand sides is a constructor, then pattern completeness and
quasi-reducibility coincide.›
lemma quasi_reducible_iff_pat_complete: fixes L :: "('f,'v)term set"
assumes "⋀ l f ls τs τ. l ∈ L ⟹ l = Fun f ls ⟹ ¬ f : τs → τ in C"
shows "pat_complete_lhss C D L ⟷ quasi_reducible C D L"
proof (standard, rule strong_quasi_reducible_imp_quasi_reducible[OF pat_complete_imp_strong_quasi_reducible])
assume q: "quasi_reducible C D L"
show "pat_complete_lhss C D L"
unfolding pat_complete_lhss_def
proof
fix t :: "('f,unit)term"
assume t: "t ∈ ℬ(C,D,∅)"
from q[unfolded quasi_reducible_def, rule_format, OF this]
obtain tp where tp: "t ⊵ tp" and match: "∃l ∈ L. l matches tp" by auto
show "∃l ∈ L. l matches t"
proof (cases "t = tp")
case True
thus ?thesis using match by auto
next
case False
from t[unfolded basic_terms_def] obtain f ts ss where t: "t = Fun f ts" and ts: "ts :⇩l ss in 𝒯(C,∅)" by auto
from t False tp obtain ti where ti: "ti ∈ set ts" and subt: "ti ⊵ tp"
by (meson Fun_supteq)
from subt obtain CC where ctxt: "ti = CC ⟨ tp ⟩" by auto
from ti ts obtain s where "ti : s in 𝒯(C)" unfolding list_all2_conv_all_nth set_conv_nth by auto
from hastype_context_decompose[OF this[unfolded ctxt]] obtain s where tp: "tp : s in 𝒯(C,∅)" by blast
from match[unfolded matches_def] obtain l σ where l: "l ∈ L" and match: "tp = l ⋅ σ" by auto
show ?thesis
proof (cases l)
case (Var x)
with l show ?thesis unfolding matches_def by (auto intro!: bexI[of _ l])
next
case (Fun f ls)
from tp[unfolded match this, simplified] obtain ss where "f : ss → s in C"
by (meson Fun_hastype hastype_def fun_hastype_def)
with assms[OF l Fun, of ss s] show ?thesis by auto
qed
qed
qed
qed
end