Theory Pattern_Completeness_Set
section ‹Pattern Completeness›
text ‹Pattern-completeness is the question whether in a given program all terms
of the form f(c1,..,cn) are matched by some lhs of the program,
where here each ci is a constructor ground term and f is a defined symbol.
This will be represented as a pattern problem of the shape
(f(x1,...xn), {lhs1, ..., lhsn}) where the xi will represent arbitrary constructor terms.›
section ‹A Set-Based Inference System to Decide Pattern Completeness›
text ‹This theory contains an algorithm to decide whether pattern problems are complete.
It represents the inference rules of the paper on the set-based level.
On this level we prove partial correctness and preservation of well-formed inputs,
but not termination.›
theory Pattern_Completeness_Set
imports
First_Order_Terms.Term_More
Sorted_Terms.Sorted_Contexts
begin
subsection ‹Definition of Algorithm -- Inference Rules›
text ‹We first consider matching problems which are sets of term pairs.
Note that in the term pairs the type of variables differ:
Each left term has natural numbers (with sorts) as variables,
so that it is easy to generate new variables,
whereas each right term has arbitrary variables of type ‹'v› without any further information.
Then pattern problems are sets of matching problems, and we also have sets of pattern problems.
The suffix ‹_set› is used to indicate that here these problems are modeled via sets.›
type_synonym ('f,'v,'s)match_problem_set = "(('f,nat × 's)term × ('f,'v)term) set"
type_synonym ('f,'v,'s)pat_problem_set = "('f,'v,'s)match_problem_set set"
type_synonym ('f,'v,'s)pats_problem_set = "('f,'v,'s)pat_problem_set set"
abbreviation (input) bottom :: "('f,'v,'s)pats_problem_set" where "bottom ≡ {{}}"
definition subst_left :: "('f,nat × 's)subst ⇒ (('f,nat × 's)term × ('f,'v)term) ⇒ (('f,nat × 's)term × ('f,'v)term)" where
"subst_left τ = (λ(t,r). (t ⋅ τ, r))"
text ‹A function to compute for a variable $x$ all substitution that instantiate
$x$ by $c(x_n, ..., x_{n+a})$ where $c$ is an constructor of arity $a$ and $n$ is a parameter that
determines from where to start the numbering of variables.›
definition τc :: "nat ⇒ nat × 's ⇒ 'f × 's list ⇒ ('f,nat × 's)subst" where
"τc n x = (λ(f,ss). subst x (Fun f (map Var (zip [n ..< n + length ss] ss))))"
text ‹Compute the list of conflicting variables (Some list), or detect a clash (None)›
fun conflicts :: "('f,'v)term ⇒ ('f,'v)term ⇒ 'v list option" where
"conflicts (Var x) (Var y) = (if x = y then Some [] else Some [x,y])"
| "conflicts (Var x) (Fun _ _) = (Some [x])"
| "conflicts (Fun _ _) (Var x) = (Some [x])"
| "conflicts (Fun f ss) (Fun g ts) = (if (f,length ss) = (g,length ts)
then map_option concat (those (map2 conflicts ss ts))
else None)"
abbreviation "Conflict_Var s t x ≡ conflicts s t ≠ None ∧ x ∈ set (the (conflicts s t))"
abbreviation "Conflict_Clash s t ≡ conflicts s t = None"
locale pattern_completeness_context =
fixes S :: "'s set"
and C :: "('f,'s)ssig"
and m :: nat
and Cl :: "'s ⇒ ('f × 's list)list"
and inf_sort :: "'s ⇒ bool"
and ty :: "'v itself"
begin
definition tvars_disj_pp :: "nat set ⇒ ('f,'v,'s)pat_problem_set ⇒ bool" where
"tvars_disj_pp V p = (∀ mp ∈ p. ∀ (ti,pi) ∈ mp. fst ` vars ti ∩ V = {})"
definition inf_var_conflict :: "('f,'v,'s)match_problem_set ⇒ bool" where
"inf_var_conflict mp = (∃ s t x y.
(s,Var x) ∈ mp ∧ (t,Var x) ∈ mp ∧ Conflict_Var s t y ∧ inf_sort (snd y))"
definition tvars_mp :: "('f,'v,'s)match_problem_set ⇒ (nat × 's) set" where
"tvars_mp mp = (⋃(t,l) ∈ mp. vars t)"
definition tvars_pp :: "('f,'v,'s)pat_problem_set ⇒ (nat × 's) set" where
"tvars_pp pp = (⋃mp ∈ pp. tvars_mp mp)"
definition subst_match_problem_set :: "('f,nat × 's)subst ⇒ ('f,'v,'s)match_problem_set ⇒ ('f,'v,'s)match_problem_set" where
"subst_match_problem_set τ pp = subst_left τ ` pp"
definition subst_pat_problem_set :: "('f,nat × 's)subst ⇒ ('f,'v,'s)pat_problem_set ⇒ ('f,'v,'s)pat_problem_set" where
"subst_pat_problem_set τ P = subst_match_problem_set τ ` P"
definition τs :: "nat ⇒ nat × 's ⇒ ('f,nat × 's)subst set" where
"τs n x = {τc n x (f,ss) | f ss. f : ss → snd x in C}"
text ‹The transformation rules of the paper.
The formal definition contains two deviations from the rules in the paper: first, the instantiate-rule
can always be applied; and second there is an identity rule, which will simplify later refinement
proofs. Both of the deviations cause non-termination.
The formal inference rules further separate those rules that deliver a bottom- or top-element from
the ones that deliver a transformed problem.›
inductive mp_step :: "('f,'v,'s)match_problem_set ⇒ ('f,'v,'s)match_problem_set ⇒ bool"
(infix "→⇩s" 50) where
mp_decompose: "length ts = length ls ⟹ insert (Fun f ts, Fun f ls) mp →⇩s set (zip ts ls) ∪ mp"
| mp_match: "x ∉ ⋃ (vars ` snd ` mp) ⟹ insert (t, Var x) mp →⇩s mp"
| mp_identity: "mp →⇩s mp"
inductive mp_fail :: "('f,'v,'s)match_problem_set ⇒ bool" where
mp_clash: "(f,length ts) ≠ (g,length ls) ⟹ mp_fail (insert (Fun f ts, Fun g ls) mp)"
| mp_clash': "Conflict_Clash s t ⟹ mp_fail ({(s,Var x),(t, Var x)} ∪ mp)"
inductive pp_step :: "('f,'v,'s)pat_problem_set ⇒ ('f,'v,'s)pat_problem_set ⇒ bool"
(infix "⇒⇩s" 50) where
pp_simp_mp: "mp →⇩s mp' ⟹ insert mp pp ⇒⇩s insert mp' pp"
| pp_remove_mp: "mp_fail mp ⟹ insert mp pp ⇒⇩s pp"
inductive pp_success :: "('f,'v,'s)pat_problem_set ⇒ bool" where
"pp_success (insert {} pp)"
inductive P_step_set :: "('f,'v,'s)pats_problem_set ⇒ ('f,'v,'s)pats_problem_set ⇒ bool"
(infix "⇛⇩s" 50) where
P_fail: "insert {} P ⇛⇩s bottom"
| P_simp: "pp ⇒⇩s pp' ⟹ insert pp P ⇛⇩s insert pp' P"
| P_remove_pp: "pp_success pp ⟹ insert pp P ⇛⇩s P"
| P_instantiate: "tvars_disj_pp {n ..< n+m} pp ⟹ x ∈ tvars_pp pp ⟹
insert pp P ⇛⇩s {subst_pat_problem_set τ pp |. τ ∈ τs n x} ∪ P"
| P_failure': "∀mp ∈ pp. inf_var_conflict mp ⟹ finite pp ⟹ insert pp P ⇛⇩s {{}}"
text ‹Note that in @{thm[source] P_failure'} the conflicts have to be simultaneously occurring.
If just some matching problem has such a conflict, then this cannot be deleted immediately!
Example-program: f(x,x) = ..., f(s(x),y) = ..., f(x,s(y)) = ... cover all cases of natural numbers,
i.e., f(x1,x2), but if one would immediately delete the matching problem of the first lhs
because of the resulting @{const inf_var_conflict} in {(x1,x),(x2,x)} then it is no longer complete.›
subsection ‹Soundness of the inference rules›
text ‹The empty set of variables›
definition EMPTY :: "'v ⇒ 's option" where "EMPTY x = None"
definition EMPTYn :: "nat × 's ⇒ 's option" where "EMPTYn x = None"
text ‹A constructor-ground substitution for the fixed set of constructors and set of sorts.
Note that variables to instantiate are represented as pairs of (number, sort).›
definition cg_subst :: "('f,nat × 's,'v)gsubst ⇒ bool" where
"cg_subst σ = (∀ x. snd x ∈ S ⟶ (σ x : snd x in 𝒯(C,EMPTY)))"
text ‹A definition of pattern completeness for pattern problems.›
definition match_complete_wrt :: "('f,nat × 's,'v)gsubst ⇒ ('f,'v,'s)match_problem_set ⇒ bool" where
"match_complete_wrt σ mp = (∃ μ. ∀ (t,l) ∈ mp. t ⋅ σ = l ⋅ μ)"
definition pat_complete :: "('f,'v,'s)pat_problem_set ⇒ bool" where
"pat_complete pp = (∀σ. cg_subst σ ⟶ (∃ mp ∈ pp. match_complete_wrt σ mp))"
abbreviation "pats_complete P ≡ ∀pp ∈ P. pat_complete pp"
text ‹Well-formed matching and pattern problems: all occurring variables
(in left-hand sides of matching problems) have a known sort.›
definition wf_match :: "('f,'v,'s)match_problem_set ⇒ bool" where
"wf_match mp = (snd ` tvars_mp mp ⊆ S)"
definition wf_pat :: "('f,'v,'s)pat_problem_set ⇒ bool" where
"wf_pat pp = (∀mp ∈ pp. wf_match mp)"
definition wf_pats :: "('f,'v,'s)pats_problem_set ⇒ bool" where
"wf_pats P = (∀pp ∈ P. wf_pat pp)"
end
lemma type_conversion: "t : s in 𝒯(C,∅) ⟹ t ⋅ σ : s in 𝒯(C,∅)"
proof (induct t s rule: hastype_in_Term_induct)
case (Fun f ss σs τ)
then show ?case unfolding eval_term.simps
by (smt (verit, best) Fun_hastype list_all2_map1 list_all2_mono)
qed auto
lemma ball_insert_un_cong: "f y = Ball zs f ⟹ Ball (insert y A) f = Ball (zs ∪ A) f"
by auto
lemma bex_insert_cong: "f y = f z ⟹ Bex (insert y A) f = Bex (insert z A) f"
by auto
lemma not_bdd_above_natD:
assumes "¬ bdd_above (A :: nat set)"
shows "∃ x ∈ A. x > n"
using assms by (meson bdd_above.unfold linorder_le_cases order.strict_iff)
lemma list_eq_nth_eq: "xs = ys ⟷ length xs = length ys ∧ (∀ i < length ys. xs ! i = ys ! i)"
using nth_equalityI by metis
lemma subt_size: "p ∈ poss t ⟹ size (t |_ p) ≤ size t"
proof (induct p arbitrary: t)
case (Cons i p t)
thus ?case
proof (cases t)
case (Fun f ss)
from Cons Fun have i: "i < length ss" and sub: "t |_ (i # p) = (ss ! i) |_ p"
and "p ∈ poss (ss ! i)" by auto
with Cons(1)[OF this(3)]
have "size (t |_ (i # p)) ≤ size (ss ! i)" by auto
also have "… ≤ size t" using i unfolding Fun by (simp add: termination_simp)
finally show ?thesis .
qed auto
qed auto
lemma conflicts_sym: "rel_option (λ xs ys. set xs = set ys) (conflicts s t) (conflicts t s)" (is "rel_option _ (?c s t) _")
proof (induct s t rule: conflicts.induct)
case (4 f ss g ts)
define c where "c = ?c"
show ?case
proof (cases "(f,length ss) = (g,length ts)")
case True
hence len: "length ss = length ts"
"((f, length ss) = (g, length ts)) = True"
"((g, length ts) = (f, length ss)) = True" by auto
show ?thesis using len(1) 4[OF True _ refl]
unfolding conflicts.simps len(2,3) if_True
unfolding option.rel_map c_def[symmetric] set_concat
proof (induct ss ts rule: list_induct2, goal_cases)
case (2 s ss t ts)
hence IH: "rel_option (λx y. ⋃ (set ` set x) = ⋃ (set ` set y)) (those (map2 c ss ts)) (those (map2 c ts ss))" by auto
from 2 have st: "rel_option (λxs ys. set xs = set ys) (c s t) (c t s)" by auto
from IH st show ?case by (cases "c s t"; cases "c t s"; auto simp: option.rel_map)
(simp add: option.rel_sel)
qed simp
qed auto
qed auto
lemma conflicts: fixes x :: 'v
shows "Conflict_Clash s t ⟹ ∃ p. p ∈ poss s ∧ p ∈ poss t ∧ is_Fun (s |_p) ∧ is_Fun (t |_p) ∧ root (s |_p) ≠ root (t |_ p)" (is "?B1 ⟹ ?B2")
and "Conflict_Var s t x ⟹
∃ p . p ∈ poss s ∧ p ∈ poss t ∧ s |_p ≠ t |_p ∧ (s |_p = Var x ∨ t |_p = Var x)" (is "?C1 x ⟹ ?C2 x")
and "s ≠ t ⟹ ∃ x. Conflict_Clash s t ∨ Conflict_Var s t x"
and "Conflict_Var s t x ⟹ x ∈ vars s ∪ vars t"
and "conflicts s t = Some [] ⟷ s = t" (is ?A)
proof -
let ?B = "?B1 ⟶ ?B2"
let ?C = "λ x. ?C1 x ⟶ ?C2 x"
{
fix x :: 'v
have "(conflicts s t = Some [] ⟶ s = t) ∧ ?B ∧ ?C x"
proof (induction s arbitrary: t)
case (Var y t)
thus ?case by (cases t, auto)
next
case (Fun f ss t)
show ?case
proof (cases t)
case t: (Fun g ts)
show ?thesis
proof (cases "(f,length ss) = (g,length ts)")
case False
hence res: "conflicts (Fun f ss) t = None" unfolding t by auto
show ?thesis unfolding res unfolding t using False
by (auto intro!: exI[of _ Nil])
next
case f: True
let ?s = "Fun f ss"
show ?thesis
proof (cases "those (map2 conflicts ss ts)")
case None
hence res: "conflicts ?s t = None" unfolding t by auto
from None[unfolded those_eq_None] obtain i where i: "i < length ss" "i < length ts" and
confl: "conflicts (ss ! i) (ts ! i) = None"
using f unfolding set_conv_nth set_zip by auto
from i have "ss ! i ∈ set ss" by auto
from Fun.IH[OF this, of "ts ! i"] confl obtain p
where p: "p ∈ poss (ss ! i) ∧ p ∈ poss (ts ! i) ∧ is_Fun (ss ! i |_ p) ∧ is_Fun (ts ! i |_ p) ∧ root (ss ! i |_ p) ≠ root (ts ! i |_ p)"
by auto
from p have p: "∃ p. p ∈ poss ?s ∧ p ∈ poss t ∧ is_Fun (?s |_ p) ∧ is_Fun (t |_ p) ∧ root (?s |_ p) ≠ root (t |_ p)"
by (intro exI[of _ "i # p"], unfold t, insert i f, auto)
from p res show ?thesis by auto
next
case (Some xss)
hence res: "conflicts ?s t = Some (concat xss)" unfolding t using f by auto
from Some have map2: "map2 conflicts ss ts = map Some xss" by auto
from arg_cong[OF this, of length] have len: "length xss = length ss" using f by auto
have rec: "i < length ss ⟹ conflicts (ss ! i) (ts ! i) = Some (xss ! i)" for i
using arg_cong[OF map2, of "λ xs. xs ! i"] len f by auto
{
assume "x ∈ set (the (conflicts ?s t))"
hence "x ∈ set (concat xss)" unfolding res by auto
then obtain xs where xs: "xs ∈ set xss" and x: "x ∈ set xs" by auto
from xs len obtain i where i: "i < length ss" and xs: "xs = xss ! i" by (auto simp: set_conv_nth)
from i have "ss ! i ∈ set ss" by auto
from Fun.IH[OF this, of "ts ! i", unfolded rec[OF i, folded xs]] x
obtain p where "p ∈ poss (ss ! i) ∧ p ∈ poss (ts ! i) ∧ ss ! i |_ p ≠ ts ! i |_ p ∧ (ss ! i |_ p = Var x ∨ ts ! i |_ p = Var x)"
by auto
hence "∃ p. p ∈ poss ?s ∧ p ∈ poss t ∧ ?s |_ p ≠ t |_ p ∧ (?s |_ p = Var x ∨ t |_ p = Var x)"
by (intro exI[of _ "i # p"], insert i f, auto simp: t)
}
moreover
{
assume "conflicts ?s t = Some []"
with res have empty: "concat xss = []" by auto
{
fix i
assume i: "i < length ss"
from rec[OF i] have "conflicts (ss ! i) (ts ! i) = Some (xss ! i)" .
moreover from empty i len have "xss ! i = []" by auto
ultimately have res: "conflicts (ss ! i) (ts ! i) = Some []" by simp
from i have "ss ! i ∈ set ss" by auto
from Fun.IH[OF this, of "ts ! i", unfolded res] have "ss ! i = ts ! i" by auto
}
with f have "?s = t" unfolding t by (auto intro: nth_equalityI)
}
ultimately show ?thesis unfolding res by auto
qed
qed
qed auto
qed
} note main = this
from main show B: "?B1 ⟹ ?B2" and C: "?C1 x ⟹ ?C2 x" by blast+
show ?A
proof
assume "s = t"
with B have "conflicts s t ≠ None" by blast
then obtain xs where res: "conflicts s t = Some xs" by auto
show "conflicts s t = Some []"
proof (cases xs)
case Nil
thus ?thesis using res by auto
next
case (Cons x xs)
with main[of x] res ‹s = t› show ?thesis by auto
qed
qed (insert main, blast)
{
assume diff: "s ≠ t"
show "∃ x. Conflict_Clash s t ∨ Conflict_Var s t x"
proof (cases "conflicts s t")
case (Some xs)
with ‹?A› diff obtain x where "x ∈ set xs" by (cases xs, auto)
thus ?thesis unfolding Some by auto
qed auto
}
assume "Conflict_Var s t x"
with C obtain p where "p ∈ poss s" "p ∈ poss t" "(s |_ p = Var x ∨ t |_ p = Var x)"
by blast
thus "x ∈ vars s ∪ vars t"
by (metis UnCI subt_at_imp_supteq' subteq_Var_imp_in_vars_term)
qed
declare conflicts.simps[simp del]
lemma conflicts_refl[simp]: "conflicts t t = Some []"
using conflicts(5)[of t t] by auto
text ‹For proving partial correctness we need further properties of the fixed parameters:
We assume that ‹m› is sufficiently large and that there exists some constructor ground terms.
Moreover ‹inf_sort› really computes whether a sort has terms of arbitrary size.
Further all symbols in ‹C› must have sorts of ‹S›.
Finally, ‹Cl› should precisely compute the constructors of a sort.›
locale pattern_completeness_context_with_assms = pattern_completeness_context S C m Cl inf_sort ty
for S and C :: "('f,'s)ssig"
and m Cl inf_sort
and ty :: "'v itself" +
assumes sorts_non_empty: "⋀ s. s ∈ S ⟹ ∃ t. t : s in 𝒯(C, EMPTY)"
and C_sub_S: "⋀ f ss s. f : ss → s in C ⟹ insert s (set ss) ⊆ S"
and m: "⋀ f ss s. f : ss → s in C ⟹ length ss ≤ m"
and inf_sort_def: "s ∈ S ⟹ inf_sort s = (¬ bdd_above (size ` {t . t : s in 𝒯(C,EMPTYn)}))"
and Cl: "⋀ s. set (Cl s) = {(f,ss). f : ss → s in C}"
and Cl_len: "⋀ σ. Ball (length ` snd ` set (Cl σ)) (λ a. a ≤ m)"
begin
lemmas subst_defs_set =
subst_pat_problem_set_def
subst_match_problem_set_def
text ‹Preservation of well-formedness›
lemma mp_step_wf: "mp →⇩s mp' ⟹ wf_match mp ⟹ wf_match mp'"
unfolding wf_match_def tvars_mp_def
proof (induct mp mp' rule: mp_step.induct)
case (mp_decompose f ts ls mp)
then show ?case by (auto dest!: set_zip_leftD)
qed auto
lemma pp_step_wf: "pp ⇒⇩s pp' ⟹ wf_pat pp ⟹ wf_pat pp'"
unfolding wf_pat_def
proof (induct pp pp' rule: pp_step.induct)
case (pp_simp_mp mp mp' pp)
then show ?case using mp_step_wf[of mp mp'] by auto
qed auto
theorem P_step_set_wf: "P ⇛⇩s P' ⟹ wf_pats P ⟹ wf_pats P'"
unfolding wf_pats_def
proof (induct P P' rule: P_step_set.induct)
case (P_simp pp pp' P)
then show ?case using pp_step_wf[of pp pp'] by auto
next
case *: (P_instantiate n p x P)
let ?s = "snd x"
from * have sS: "?s ∈ S" and p: "wf_pat p" unfolding wf_pat_def wf_match_def tvars_pp_def by auto
{
fix τ
assume tau: "τ ∈ τs n x"
from tau[unfolded τs_def τc_def, simplified]
obtain f sorts where f: "f : sorts → snd x in C" and τ: "τ = subst x (Fun f (map Var (zip [n..<n + length sorts] sorts)))" by auto
let ?i = "length sorts"
let ?xs = "zip [n..<n + length sorts] sorts"
from C_sub_S[OF f] have sS: "?s ∈ S" and xs: "snd ` set ?xs ⊆ S"
unfolding set_conv_nth set_zip by auto
{
fix mp y
assume mp: "mp ∈ p" and "y ∈ tvars_mp (subst_left τ ` mp)"
then obtain s t where y: "y ∈ vars (s ⋅ τ)" and st: "(s,t) ∈ mp"
unfolding tvars_mp_def subst_left_def by auto
from y have "y ∈ vars s ∪ set ?xs" unfolding vars_term_subst τ
by (auto simp: subst_def split: if_splits)
hence "snd y ∈ snd ` vars s ∪ snd ` set ?xs" by auto
also have "… ⊆ snd ` vars s ∪ S" using xs by auto
also have "… ⊆ S" using p mp st
unfolding wf_pat_def wf_match_def tvars_mp_def by force
finally have "snd y ∈ S" .
}
hence "wf_pat (subst_pat_problem_set τ p)"
unfolding wf_pat_def wf_match_def subst_defs_set by auto
}
with * show ?case by auto
qed (auto simp: wf_pat_def)
text ‹Soundness requires some preparations›
lemma cg_exists: "∃ σg. cg_subst σg"
proof
show "cg_subst (λ x. SOME t. t : snd x in 𝒯(C, EMPTY))"
unfolding cg_subst_def
proof (intro allI impI, goal_cases)
case (1 x)
from someI_ex[OF sorts_non_empty[OF 1]] show ?case by simp
qed
qed
definition σg :: "('f,nat × 's,'v)gsubst" where "σg = (SOME σ. cg_subst σ)"
lemma σg: "cg_subst σg" unfolding σg_def using cg_exists by (metis someI_ex)
lemma pat_complete_empty[simp]: "pat_complete {} = False"
unfolding pat_complete_def using σg by auto
lemma inf_var_conflictD: assumes "inf_var_conflict mp"
shows "∃ p s t x y.
(s,Var x) ∈ mp ∧ (t,Var x) ∈ mp ∧ s |_p = Var y ∧ s |_ p ≠ t |_p ∧ p ∈ poss s ∧ p ∈ poss t ∧ inf_sort (snd y)"
proof -
from assms[unfolded inf_var_conflict_def]
obtain s t x y where "(s, Var x) ∈ mp ∧ (t, Var x) ∈ mp" and conf: "Conflict_Var s t y" and y: "inf_sort (snd y)" by blast
with conflicts(2)[OF conf] show ?thesis by metis
qed
lemma cg_term_vars: "t : s in 𝒯(C,EMPTYn) ⟹ vars t = {}"
proof (induct t s rule: hastype_in_Term_induct)
case (Var v σ)
then show ?case by (auto simp: EMPTYn_def)
next
case (Fun f ss σs τ)
then show ?case unfolding term.simps unfolding set_conv_nth list_all2_conv_all_nth by auto
qed
lemma type_conversion1: "t : s in 𝒯(C,EMPTYn) ⟹ t ⋅ σ' : s in 𝒯(C,EMPTY)"
unfolding EMPTYn_def EMPTY_def by (rule type_conversion)
lemma type_conversion2: "t : s in 𝒯(C,EMPTY) ⟹ t ⋅ σ' : s in 𝒯(C,EMPTYn)"
unfolding EMPTYn_def EMPTY_def by (rule type_conversion)
lemma term_of_sort: assumes "s ∈ S"
shows "∃ t. t : s in 𝒯(C,EMPTYn)"
proof -
from σg[unfolded cg_subst_def] assms
have "∃ t. t : s in 𝒯(C,EMPTY)" by force
with type_conversion2[of _ s]
show ?thesis by auto
qed
text ‹Main partial correctness theorems on well-formed problems: the transformation rules do
not change the semantics of a problem›
lemma mp_step_pcorrect: "mp →⇩s mp' ⟹ match_complete_wrt σ mp = match_complete_wrt σ mp'"
proof (induct mp mp' rule: mp_step.induct)
case *: (mp_decompose f ts ls mp)
show ?case unfolding match_complete_wrt_def
apply (rule ex_cong1)
apply (rule ball_insert_un_cong)
apply (unfold split) using * by (auto simp add: set_zip list_eq_nth_eq)
next
case *: (mp_match x mp t)
show ?case unfolding match_complete_wrt_def
proof
assume "∃μ. ∀(ti, li)∈mp. ti ⋅ σ = li ⋅ μ"
then obtain μ where eq: "⋀ ti li. (ti, li)∈mp ⟹ ti ⋅ σ = li ⋅ μ" by auto
let ?μ = "μ(x := t ⋅ σ)"
have "(ti, li) ∈ mp ⟹ ti ⋅ σ = li ⋅ ?μ" for ti li using * eq[of ti li]
by (auto intro!: term_subst_eq)
thus "∃μ. ∀(ti, li)∈insert (t, Var x) mp. ti ⋅ σ = li ⋅ μ" by (intro exI[of _ ?μ], auto)
qed auto
qed auto
lemma mp_fail_pcorrect: "mp_fail mp ⟹ ¬ match_complete_wrt σ mp"
proof (induct mp rule: mp_fail.induct)
case *: (mp_clash f ts g ls mp)
{
assume "length ts ≠ length ls"
hence "(map (λt. t ⋅ μ) ls = map (λt. t ⋅ σ) ts) = False" for σ :: "('f,nat × 's,'a)gsubst" and μ
by (metis length_map)
} note len = this
from * show ?case unfolding match_complete_wrt_def
by (auto simp: len)
next
case *: (mp_clash' s t x mp)
from conflicts(1)[OF *(1)]
obtain po where *: "po ∈ poss s" "po ∈ poss t" "is_Fun (s |_ po)" "is_Fun (t |_ po)" "root (s |_ po) ≠ root (t |_ po)"
by auto
show ?case
proof
assume "match_complete_wrt σ ({(s, Var x), (t, Var x)} ∪ mp)"
from this[unfolded match_complete_wrt_def]
have "s ⋅ σ = t ⋅ σ" by auto
hence "root (s ⋅ σ |_po) = root (t ⋅ σ |_po)" by auto
also have "root (s ⋅ σ |_po) = root (s |_po ⋅ σ)" using * by auto
also have "… = root (s |_po)" using * by (cases "s |_ po", auto)
also have "root (t ⋅ σ |_po) = root (t |_po ⋅ σ)" using * by (cases "t |_ po", auto)
also have "… = root (t |_po)" using * by (cases "t |_ po", auto)
finally show False using * by auto
qed
qed
lemma pp_step_pcorrect: "pp ⇒⇩s pp' ⟹ pat_complete pp = pat_complete pp'"
proof (induct pp pp' rule: pp_step.induct)
case (pp_simp_mp mp mp' pp)
then show ?case using mp_step_pcorrect[of mp mp'] unfolding pat_complete_def by auto
next
case (pp_remove_mp mp pp)
then show ?case using mp_fail_pcorrect[of mp] unfolding pat_complete_def by auto
qed
lemma pp_success_pcorrect: "pp_success pp ⟹ pat_complete pp"
by (induct pp rule: pp_success.induct, auto simp: pat_complete_def match_complete_wrt_def)
theorem P_step_set_pcorrect: "P ⇛⇩s P' ⟹ wf_pats P ⟹
pats_complete P ⟷ pats_complete P'"
proof (induct P P' rule: P_step_set.induct)
case (P_fail P)
then show ?case by (auto simp: pat_complete_def)
next
case (P_simp pp pp' P)
then show ?case using pp_step_pcorrect[of pp pp'] by auto
next
case (P_remove_pp pp P)
then show ?case using pp_success_pcorrect[of pp] by auto
next
case *: (P_instantiate n pp x P)
note def = pat_complete_def[unfolded match_complete_wrt_def]
show ?case
proof (rule ball_insert_un_cong, standard)
assume complete: "pats_complete {subst_pat_problem_set τ pp |. τ ∈ τs n x}"
show "pat_complete pp" unfolding def
proof (intro allI impI)
fix σ :: "('f,nat × 's,'v)gsubst"
from * have "wf_pat pp" unfolding wf_pats_def by auto
with *(2) have x: "snd x ∈ S" unfolding tvars_pp_def tvars_mp_def wf_pat_def wf_match_def by force
assume cg: "cg_subst σ"
from this[unfolded cg_subst_def] x
have "σ x : snd x in 𝒯(C,EMPTY)" by blast
then obtain f ts σs where f: "f : σs → snd x in C"
and args: "ts :⇩l σs in 𝒯(C,EMPTY)"
and σx: "σ x = Fun f ts"
by (induct, auto simp: EMPTY_def)
from f have f: "f : σs → snd x in C"
by (meson hastype_in_ssig_def)
let ?l = "length ts"
from args have len: "length σs = ?l"
by (simp add: list_all2_lengthD)
have l: "?l ≤ m" using m[OF f] len by auto
define σ' where "σ' = (λ ys. let y = fst ys in if n ≤ y ∧ y < n + ?l ∧ σs ! (y - n) = snd ys then ts ! (y - n) else σ ys)"
have cg: "cg_subst σ'" unfolding cg_subst_def
proof (intro allI impI)
fix ys :: "nat × 's"
assume ysS: "snd ys ∈ S"
show "σ' ys : snd ys in 𝒯(C,EMPTY)"
proof (cases "σ' ys = σ ys")
case True
thus ?thesis using cg ysS unfolding cg_subst_def by metis
next
case False
obtain y s where ys: "ys = (y,s)" by force
with False have y: "y - n < ?l" "n ≤ y" "y < n + ?l" and arg: "σs ! (y - n) = s" and σ': "σ' ys = ts ! (y - n)"
unfolding σ'_def Let_def by (auto split: if_splits)
show ?thesis unfolding σ' unfolding ys snd_conv arg[symmetric] using y(1) len args
by (metis list_all2_nthD)
qed
qed
define τ where "τ = subst x (Fun f (map Var (zip [n..<n + ?l] σs)))"
from f have "τ ∈ τs n x" unfolding τs_def τ_def τc_def using len[symmetric] by auto
hence "pat_complete (subst_pat_problem_set τ pp)" using complete by auto
from this[unfolded def, rule_format, OF cg]
obtain tl μ where tl: "tl ∈ subst_pat_problem_set τ pp"
and match: "⋀ ti li. (ti, li) ∈ tl ⟹ ti ⋅ σ' = li ⋅ μ" by force
from tl[unfolded subst_defs_set subst_left_def set_map]
obtain tl' where tl': "tl' ∈ pp" and tl: "tl = {(t' ⋅ τ, l) |. (t',l) ∈ tl'}" by auto
show "∃tl∈ pp. ∃μ. ∀(ti, li)∈ tl. ti ⋅ σ = li ⋅ μ"
proof (intro bexI[OF _ tl'] exI[of _ μ], clarify)
fix ti li
assume tli: "(ti, li) ∈ tl'"
hence tlit: "(ti ⋅ τ, li) ∈ tl" unfolding tl by force
from match[OF this] have match: "ti ⋅ τ ⋅ σ' = li ⋅ μ" by auto
from *(1)[unfolded tvars_disj_pp_def, rule_format, OF tl' tli]
have vti: "fst ` vars_term ti ∩ {n..<n + m} = {}" by auto
have "ti ⋅ σ = ti ⋅ (τ ∘⇩s σ')"
proof (rule term_subst_eq, unfold subst_compose_def)
fix y
assume "y ∈ vars_term ti"
with vti have y: "fst y ∉ {n..<n + m}" by auto
show "σ y = τ y ⋅ σ'"
proof (cases "y = x")
case False
hence "τ y ⋅ σ' = σ' y" unfolding τ_def subst_def by auto
also have "… = σ y"
unfolding σ'_def using y l by auto
finally show ?thesis by simp
next
case True
show ?thesis unfolding True τ_def subst_simps σx eval_term.simps map_map o_def term.simps
by (intro conjI refl nth_equalityI, auto simp: len σ'_def)
qed
qed
also have "… = li ⋅ μ" using match by simp
finally show "ti ⋅ σ = li ⋅ μ" by blast
qed
qed
next
assume complete: "pat_complete pp"
{
fix τ
assume "τ ∈ τs n x"
from this[unfolded τs_def τc_def, simplified]
obtain f sorts where f: "f : sorts → snd x in C" and τ: "τ = subst x (Fun f (map Var (zip [n..<n + length sorts] sorts)))" by auto
let ?i = "length sorts"
let ?xs = "zip [n..<n + length sorts] sorts"
have i: "?i ≤ m" by (rule m[OF f])
have "pat_complete (subst_pat_problem_set τ pp)" unfolding def
proof (intro allI impI)
fix σ :: "('f,nat × 's,'v)gsubst"
assume cg: "cg_subst σ"
define σ' where "σ' = σ(x := Fun f (map σ ?xs))"
from C_sub_S[OF f] have sortsS: "set sorts ⊆ S" by auto
from f have f: "f : sorts → snd x in C" by (simp add: hastype_in_ssig_def)
hence "Fun f (map σ ?xs) : snd x in 𝒯(C,EMPTY)"
proof (rule Fun_hastypeI)
show "map σ ?xs :⇩l sorts in 𝒯(C,EMPTY)"
using cg[unfolded cg_subst_def, rule_format, OF set_mp[OF sortsS]]
by (smt (verit) add_diff_cancel_left' length_map length_upt length_zip list_all2_conv_all_nth min.idem nth_map nth_mem nth_zip prod.sel(2))
qed
hence cg: "cg_subst σ'" using cg f unfolding cg_subst_def σ'_def by auto
from complete[unfolded def, rule_format, OF this]
obtain tl μ where tl: "tl ∈ pp" and tli: "⋀ ti li. (ti, li)∈ tl ⟹ ti ⋅ σ' = li ⋅ μ" by force
from tl have tlm: "{(t ⋅ τ, l) |. (t,l) ∈ tl} ∈ subst_pat_problem_set τ pp"
unfolding subst_defs_set subst_left_def by auto
{
fix ti li
assume mem: "(ti, li) ∈ tl"
from *[unfolded tvars_disj_pp_def] tl mem have vti: "fst ` vars_term ti ∩ {n..<n + m} = {}" by force
from tli[OF mem] have "li ⋅ μ = ti ⋅ σ'" by auto
also have "… = ti ⋅ (τ ∘⇩s σ)"
proof (intro term_subst_eq, unfold subst_compose_def)
fix y
assume "y ∈ vars_term ti"
with vti have y: "fst y ∉ {n..<n + m}" by auto
show "σ' y = τ y ⋅ σ"
proof (cases "y = x")
case False
hence "τ y ⋅ σ = σ y" unfolding τ subst_def by auto
also have "… = σ' y"
unfolding σ'_def using False by auto
finally show ?thesis by simp
next
case True
show ?thesis unfolding True τ
by (simp add: o_def σ'_def)
qed
qed
finally have "ti ⋅ τ ⋅ σ = li ⋅ μ" by auto
}
thus "∃tl ∈ subst_pat_problem_set τ pp. ∃μ. ∀(ti, li)∈tl. ti ⋅ σ = li ⋅ μ"
by (intro bexI[OF _ tlm], auto)
qed
}
thus "pats_complete {subst_pat_problem_set τ pp |. τ ∈ τs n x}" by auto
qed
next
case *: (P_failure' pp P)
{
assume pp: "pat_complete pp"
with *(3) have wf: "wf_pat pp" by (auto simp: wf_pats_def)
define confl' :: "('f, nat × 's) term ⇒ ('f, nat × 's)term ⇒ nat × 's ⇒ bool" where "confl' = (λ sp tp y.
sp = Var y ∧ inf_sort (snd y) ∧ sp ≠ tp)"
define P1 where "P1 = (λ mp s t x y p. mp ∈ pp ⟶ (s, Var x) ∈ mp ∧ (t, Var x) ∈ mp ∧ p ∈ poss s ∧ p ∈ poss t ∧ confl' (s |_ p) (t |_ p) y)"
{
fix mp
assume "mp ∈ pp"
hence "inf_var_conflict mp" using * by auto
from inf_var_conflictD[OF this]
have "∃ s t x y p. P1 mp s t x y p" unfolding P1_def confl'_def by force
}
hence "∀ mp. ∃ s t x y p. P1 mp s t x y p" unfolding P1_def by blast
from choice[OF this] obtain s where "∀ mp. ∃ t x y p. P1 mp (s mp) t x y p" by blast
from choice[OF this] obtain t where "∀ mp. ∃ x y p. P1 mp (s mp) (t mp) x y p" by blast
from choice[OF this] obtain x where "∀ mp. ∃ y p. P1 mp (s mp) (t mp) (x mp) y p" by blast
from choice[OF this] obtain y where "∀ mp. ∃ p. P1 mp (s mp) (t mp) (x mp) (y mp) p" by blast
from choice[OF this] obtain p where "∀ mp. P1 mp (s mp) (t mp) (x mp) (y mp) (p mp)" by blast
note P1 = this[unfolded P1_def, rule_format]
from *(2) have "finite (y ` pp)" by blast
from ex_bij_betw_finite_nat[OF this] obtain index and n :: nat where
bij: "bij_betw index (y ` pp) {..<n}"
by (auto simp add: atLeast0LessThan)
define var_ind :: "nat ⇒ nat × 's ⇒ bool" where
"var_ind i x = (x ∈ y ` pp ∧ index x ∈ {..<n} - {..<i})" for i x
have [simp]: "var_ind n x = False" for x
unfolding var_ind_def by auto
define cg_subst_ind :: "nat ⇒ ('f,nat × 's)subst ⇒ bool" where
"cg_subst_ind i σ = (∀ x. (var_ind i x ⟶ σ x = Var x)
∧ (¬ var_ind i x ⟶ (vars_term (σ x) = {} ∧ (snd x ∈ S ⟶ σ x : snd x in 𝒯(C,EMPTYn)))))" for i σ
define confl :: "nat ⇒ ('f, nat × 's) term ⇒ ('f, nat × 's)term ⇒ bool" where "confl = (λ i sp tp.
(case (sp,tp) of (Var x, Var y) ⇒ x ≠ y ∧ var_ind i x ∧ var_ind i y
| (Var x, Fun _ _) ⇒ var_ind i x
| (Fun _ _, Var x) ⇒ var_ind i x
| (Fun f ss, Fun g ts) ⇒ (f,length ss) ≠ (g,length ts)))"
have confl_n: "confl n s t ⟹ ∃ f g ss ts. s = Fun f ss ∧ t = Fun g ts ∧ (f,length ss) ≠ (g,length ts)" for s t
by (cases s; cases t; auto simp: confl_def)
{
fix i
assume "i ≤ n"
hence "∃ σ. cg_subst_ind i σ ∧ (∀ mp ∈ pp. ∃ p. p ∈ poss (s mp ⋅ σ) ∧ p ∈ poss (t mp ⋅ σ) ∧ confl i (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p))"
proof (induction i)
case 0
define σ where "σ x = (if var_ind 0 x then Var x else if snd x ∈ S then map_vars undefined (σg x) else Fun undefined [])" for x
{
fix x :: "nat × 's"
define t where "t = σg x"
define s where "s = snd x"
assume "snd x ∈ S"
hence "σg x : snd x in 𝒯(C,EMPTY)" using σg unfolding cg_subst_def by blast
hence "map_vars undefined (σg x) : snd x in 𝒯(C,EMPTYn)" (is "?m : _ in _")
unfolding t_def[symmetric] s_def[symmetric]
proof (induct t s rule: hastype_in_Term_induct)
case (Var v σ)
then show ?case by (auto simp: EMPTY_def)
next
case (Fun f ss σs τ)
then show ?case unfolding term.simps
by (smt (verit, best) Fun_hastype list_all2_map1 list_all2_mono)
qed
}
from this cg_term_vars[OF this] have σ: "cg_subst_ind 0 σ" unfolding cg_subst_ind_def σ_def by auto
show ?case
proof (rule exI, rule conjI[OF σ], intro ballI exI conjI)
fix mp
assume mp: "mp ∈ pp"
note P1 = P1[OF this]
from mp have mem: "y mp ∈ y ` pp" by auto
with bij have y: "index (y mp) ∈ {..<n}" by (metis bij_betw_apply)
hence y0: "var_ind 0 (y mp)" using mem unfolding var_ind_def by auto
show "p mp ∈ poss (s mp ⋅ σ)" using P1 by auto
show "p mp ∈ poss (t mp ⋅ σ)" using P1 by auto
let ?t = "t mp |_ p mp"
define c where "c = confl 0 (s mp ⋅ σ |_ p mp) (t mp ⋅ σ |_ p mp)"
have "c = confl 0 (s mp |_ p mp ⋅ σ) (?t ⋅ σ)"
using P1 unfolding c_def by auto
also have s: "s mp |_ p mp = Var (y mp)" using P1 unfolding confl'_def by auto
also have "… ⋅ σ = Var (y mp)" using y0 unfolding σ_def by auto
also have "confl 0 (Var (y mp)) (?t ⋅ σ)"
proof (cases "?t ⋅ σ")
case Fun
thus ?thesis using y0 unfolding confl_def by auto
next
case (Var z)
then obtain u where t: "?t = Var u" and ssig: "σ u = Var z"
by (cases ?t, auto)
from P1[unfolded s] have "confl' (Var (y mp)) ?t (y mp)" by auto
from this[unfolded confl'_def t] have uy: "y mp ≠ u" by auto
show ?thesis
proof (cases "var_ind 0 u")
case True
with y0 uy show ?thesis unfolding t σ_def confl_def by auto
next
case False
with ssig[unfolded σ_def] have uS: "snd u ∈ S" and contra: "map_vars undefined (σg u) = Var z"
by (auto split: if_splits)
from σg[unfolded cg_subst_def, rule_format, OF uS] contra
have False by (cases "σg u", auto simp: EMPTY_def)
thus ?thesis ..
qed
qed
finally show "confl 0 (s mp ⋅ σ |_ p mp) (t mp ⋅ σ |_ p mp)" unfolding c_def .
qed
next
case (Suc i)
then obtain σ where σ: "cg_subst_ind i σ" and confl: "(∀mp∈pp. ∃p. p ∈ poss (s mp ⋅ σ) ∧ p ∈ poss (t mp ⋅ σ) ∧ confl i (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p))"
by auto
from Suc have "i ∈ {..< n}" and i: "i < n" by auto
with bij obtain z where z: "z ∈ y ` pp" "index z = i" unfolding bij_betw_def by (metis imageE)
{
from z obtain mp where "mp ∈ pp" and "index (y mp) = i" and "z = y mp" by auto
with P1[OF this(1), unfolded confl'_def] have inf: "inf_sort (snd z)"
and *: "p mp ∈ poss (s mp)" "s mp |_ p mp = Var z" "(s mp, Var (x mp)) ∈ mp"
by auto
from *(1,2) have "z ∈ vars (s mp)" using vars_term_subt_at by fastforce
with *(3) have "z ∈ tvars_mp mp" unfolding tvars_mp_def by force
with ‹mp ∈ pp› wf have "snd z ∈ S" unfolding wf_pat_def wf_match_def by auto
from not_bdd_above_natD[OF inf[unfolded inf_sort_def[OF this]]] term_of_sort[OF this]
have "⋀ n. ∃ t. t : snd z in 𝒯(C,EMPTYn) ∧ n < size t" by auto
} note z_inf = this
define all_st where "all_st = (λ mp. s mp ⋅ σ) ` pp ∪ (λ mp. t mp ⋅ σ) ` pp"
have fin_all_st: "finite all_st" unfolding all_st_def using *(2) by simp
define d :: nat where "d = Suc (Max (size ` all_st))"
from z_inf[of d]
obtain u where u: "u : snd z in 𝒯(C,EMPTYn)" and du: "d ≤ size u" by auto
have vars_u: "vars u = {}" by (rule cg_term_vars[OF u])
define σ' where "σ' x = (if x = z then u else σ x)" for x
have σ'_def': "σ' x = (if x ∈ y ` pp ∧ index x = i then u else σ x)" for x
unfolding σ'_def by (rule if_cong, insert bij z, auto simp: bij_betw_def inj_on_def)
have var_ind_conv: "var_ind i x = (x = z ∨ var_ind (Suc i) x)" for x
proof
assume "x = z ∨ var_ind (Suc i) x"
thus "var_ind i x" using z i unfolding var_ind_def by auto
next
assume "var_ind i x"
hence x: "x ∈ y ` pp" "index x ∈ {..<n} - {..<i}" unfolding var_ind_def by auto
with i have "index x = i ∨ index x ∈ {..<n} - {..<Suc i}" by auto
thus "x = z ∨ var_ind (Suc i) x"
proof
assume "index x = i"
with x(1) z bij have "x = z" by (auto simp: bij_betw_def inj_on_def)
thus ?thesis by auto
qed (insert x, auto simp: var_ind_def)
qed
have [simp]: "var_ind i z" unfolding var_ind_conv by auto
have [simp]: "var_ind (Suc i) z = False" unfolding var_ind_def using z by auto
have σz[simp]: "σ z = Var z" using σ[unfolded cg_subst_ind_def, rule_format, of z] by auto
have σ'_upd: "σ' = σ(z := u)" unfolding σ'_def by (intro ext, auto)
have σ'_comp: "σ' = σ ∘⇩s Var(z := u)" unfolding subst_compose_def σ'_upd
proof (intro ext)
fix x
show "(σ(z := u)) x = σ x ⋅ Var(z := u)"
proof (cases "x = z")
case False
hence "σ x ⋅ (Var(z := u)) = σ x ⋅ Var"
proof (intro term_subst_eq)
fix y
assume y: "y ∈ vars (σ x)"
show "(Var(z := u)) y = Var y"
proof (cases "var_ind i x")
case True
with σ[unfolded cg_subst_ind_def, rule_format, of x]
have "σ x = Var x" by auto
with False y show ?thesis by auto
next
case False
with σ[unfolded cg_subst_ind_def, rule_format, of x]
have "vars (σ x) = {}" by auto
with y show ?thesis by auto
qed
qed
thus ?thesis by auto
qed simp
qed
have σ': "cg_subst_ind (Suc i) σ'" unfolding cg_subst_ind_def
proof (intro allI conjI impI)
fix x
assume "var_ind (Suc i) x"
hence "var_ind i x" and diff: "index x ≠ i" unfolding var_ind_def by auto
hence "σ x = Var x" using σ[unfolded cg_subst_ind_def] by blast
thus "σ' x = Var x" unfolding σ'_def' using diff by auto
next
fix x
assume "¬ var_ind (Suc i) x" and "snd x ∈ S"
thus "σ' x : snd x in 𝒯(C,EMPTYn)"
using σ[unfolded cg_subst_ind_def, rule_format, of x] u
unfolding σ'_def var_ind_conv by auto
next
fix x
assume "¬ var_ind (Suc i) x"
hence "x = z ∨ ¬ var_ind i x" unfolding var_ind_conv by auto
thus "vars (σ' x) = {}" unfolding σ'_upd using σ[unfolded cg_subst_ind_def, rule_format, of x] vars_u by auto
qed
show ?case
proof (intro exI[of _ σ'] conjI σ' ballI)
fix mp
assume mp: "mp ∈ pp"
define s' where "s' = s mp ⋅ σ"
define t' where "t' = t mp ⋅ σ"
from confl[rule_format, OF mp]
obtain p where p: "p ∈ poss s'" "p ∈ poss t'" and confl: "confl i (s' |_ p) (t' |_ p)" by (auto simp: s'_def t'_def)
{
fix s' t' :: "('f, nat × 's) term" and p f ss x
assume *: "(s' |_ p, t' |_p) = (Fun f ss, Var x)" "var_ind i x" and p: "p ∈ poss s'" "p ∈ poss t'"
and range_all_st: "s' ∈ all_st"
hence s': "s' ⋅ Var(z := u) |_ p = Fun f ss ⋅ Var(z := u)" (is "_ = ?s")
and t': "t' ⋅ Var(z := u) |_ p = (if x = z then u else Var x)" using p by auto
from range_all_st[unfolded all_st_def]
have rangeσ: "∃ S. s' = S ⋅ σ" by auto
define s where "s = ?s"
have "∃p. p ∈ poss (s' ⋅ Var(z := u)) ∧ p ∈ poss (t' ⋅ Var(z := u)) ∧ confl (Suc i) (s' ⋅ Var(z := u) |_ p) (t' ⋅ Var(z := u) |_ p)"
proof (cases "x = z")
case False
thus ?thesis using * p unfolding s' t' by (intro exI[of _ p], auto simp: confl_def var_ind_conv)
next
case True
hence t': "t' ⋅ Var(z := u) |_ p = u" unfolding t' by auto
have "∃ p'. p' ∈ poss u ∧ p' ∈ poss s ∧ confl (Suc i) (s |_ p') (u |_ p')"
proof (cases "∃ x. x ∈ vars s ∧ var_ind (Suc i) x")
case True
then obtain x where xs: "x ∈ vars s" and x: "var_ind (Suc i) x" by auto
from xs obtain p' where p': "p' ∈ poss s" and sp: "s |_ p' = Var x" by (metis vars_term_poss_subt_at)
from p' sp vars_u show ?thesis
proof (induct u arbitrary: p' s)
case (Fun f us p' s)
show ?case
proof (cases s)
case (Var y)
with Fun have s: "s = Var x" by auto
with x show ?thesis by (intro exI[of _ Nil], auto simp: confl_def)
next
case s: (Fun g ss)
with Fun obtain j p where p: "p' = j # p" "j < length ss" "p ∈ poss (ss ! j)" "(ss ! j) |_ p = Var x" by auto
show ?thesis
proof (cases "(f,length us) = (g,length ss)")
case False
thus ?thesis by (intro exI[of _ Nil], auto simp: s confl_def)
next
case True
with p have j: "j < length us" by auto
hence usj: "us ! j ∈ set us" by auto
with Fun have "vars (us ! j) = {}" by auto
from Fun(1)[OF usj p(3,4) this] obtain p' where
"p' ∈ poss (us ! j) ∧ p' ∈ poss (ss ! j) ∧ confl (Suc i) (ss ! j |_ p') (us ! j |_ p')" by auto
thus ?thesis using j p by (intro exI[of _ "j # p'"], auto simp: s)
qed
qed
qed auto
next
case False
from * have fss: "Fun f ss = s' |_ p" by auto
from rangeσ obtain S where sS: "s' = S ⋅ σ" by auto
from p have "vars (s' |_ p) ⊆ vars s'" by (metis vars_term_subt_at)
also have "… = (⋃y∈vars S. vars (σ y))" unfolding sS by (simp add: vars_term_subst)
also have "… ⊆ (⋃y∈vars S. Collect (var_ind i))"
proof -
{
fix x y
assume "x ∈ vars (σ y)"
hence "var_ind i x"
using σ[unfolded cg_subst_ind_def, rule_format, of y] by auto
}
thus ?thesis by auto
qed
finally have sub: "vars (s' |_ p) ⊆ Collect (var_ind i)" by blast
have "vars s = vars (s' |_ p ⋅ Var(z := u))" unfolding s_def s' fss by auto
also have "… = ⋃ (vars ` Var(z := u) ` vars (s' |_ p))" by (simp add: vars_term_subst)
also have "… ⊆ ⋃ (vars ` Var(z := u) ` Collect (var_ind i))" using sub by auto
also have "… ⊆ Collect (var_ind (Suc i))"
by (auto simp: vars_u var_ind_conv)
finally have vars_s: "vars s = {}" using False by auto
{
assume "s = u"
from this[unfolded s_def fss]
have eq: "s' |_ p ⋅ Var(z := u) = u" by auto
have False
proof (cases "z ∈ vars (s' |_ p)")
case True
have diff: "s' |_ p ≠ Var z" using * by auto
from True obtain C where id: "s' |_ p = C ⟨ Var z ⟩"
by (metis ctxt_supt_id vars_term_poss_subt_at)
with diff have diff: "C ≠ Hole" by (cases C, auto)
from eq[unfolded id, simplified] diff
obtain C where "C⟨u⟩ = u" and "C ≠ Hole" by (cases C; force)
from arg_cong[OF this(1), of size] this(2) show False
by (simp add: less_not_refl2 size_ne_ctxt)
next
case False
have size: "size s' ∈ size ` all_st" using range_all_st by auto
from False have "s' |_ p ⋅ Var(z := u) = s' |_ p ⋅ Var"
by (intro term_subst_eq, auto)
with eq have eq: "s' |_ p = u" by auto
hence "size u = size (s' |_ p)" by auto
also have "… ≤ size s'" using p(1)
by (rule subt_size)
also have "… ≤ Max (size ` all_st)"
using size fin_all_st by simp
also have "… < d" unfolding d_def by simp
also have "… ≤ size u" using du .
finally show False by simp
qed
}
hence "s ≠ u" by auto
with vars_s vars_u
show ?thesis
proof (induct s arbitrary: u)
case s: (Fun f ss u)
then obtain g us where u: "u = Fun g us" by (cases u, auto)
show ?case
proof (cases "(f,length ss) = (g,length us)")
case False
thus ?thesis unfolding u by (intro exI[of _ Nil], auto simp: confl_def)
next
case True
with s(4)[unfolded u] have "∃ j < length us. ss ! j ≠ us ! j"
by (auto simp: list_eq_nth_eq)
then obtain j where j: "j < length us" and diff: "ss ! j ≠ us ! j" by auto
from j True have mem: "ss ! j ∈ set ss" "us ! j ∈ set us" by auto
with s(2-) u have "vars (ss ! j) = {}" "vars (us ! j) = {}" by auto
from s(1)[OF mem(1) this diff] obtain p' where
"p' ∈ poss (us ! j) ∧ p' ∈ poss (ss ! j) ∧ confl (Suc i) (ss ! j |_ p') (us ! j |_ p')"
by blast
thus ?thesis unfolding u using True j by (intro exI[of _ "j # p'"], auto)
qed
qed auto
qed
then obtain p' where p': "p' ∈ poss u" "p' ∈ poss s" and confl: "confl (Suc i) (s |_ p') (u |_ p')" by auto
have s'': "s' ⋅ Var(z := u) |_ (p @ p') = s |_ p'" unfolding s_def s'[symmetric] using p p' by auto
have t'': "t' ⋅ Var(z := u) |_ (p @ p') = u |_ p'" using t' p p' by auto
show ?thesis
proof (intro exI[of _ "p @ p'"], unfold s'' t'', intro conjI confl)
have "p ∈ poss (s' ⋅ Var(z := u))" using p by auto
moreover have "p' ∈ poss ((s' ⋅ Var(z := u)) |_ p)" using s' p' p unfolding s_def by auto
ultimately show "p @ p' ∈ poss (s' ⋅ Var(z := u))" by simp
have "p ∈ poss (t' ⋅ Var(z := u))" using p by auto
moreover have "p' ∈ poss ((t' ⋅ Var(z := u)) |_ p)" using t' p' p by auto
ultimately show "p @ p' ∈ poss (t' ⋅ Var(z := u))" by simp
qed
qed
} note main = this
consider (FF) f g ss ts where "(s' |_ p, t' |_ p) = (Fun f ss, Fun g ts)" "(f,length ss) ≠ (g,length ts)"
| (FV) f ss x where "(s' |_ p, t' |_ p) = (Fun f ss, Var x)" "var_ind i x"
| (VF) f ss x where "(s' |_ p, t' |_ p) = (Var x, Fun f ss)" "var_ind i x"
| (VV) x x' where "(s' |_ p, t' |_ p) = (Var x, Var x')" "x ≠ x'" "var_ind i x" "var_ind i x'"
using confl by (auto simp: confl_def split: term.splits)
hence "∃p. p ∈ poss (s' ⋅ Var(z := u)) ∧ p ∈ poss (t' ⋅ Var(z := u)) ∧ confl (Suc i) (s' ⋅ Var(z := u) |_ p) (t' ⋅ Var(z := u) |_ p)"
proof cases
case (FF f g ss ts)
thus ?thesis using p by (intro exI[of _ p], auto simp: confl_def)
next
case (FV f ss x)
have "s' ∈ all_st" unfolding s'_def using mp all_st_def by auto
from main[OF FV p this] show ?thesis by auto
next
case (VF f ss x)
have t': "t' ∈ all_st" unfolding t'_def using mp all_st_def by auto
from VF have "(t' |_ p, s' |_ p) = (Fun f ss, Var x)" "var_ind i x" by auto
from main[OF this p(2,1) t']
obtain p where "p ∈ poss (t' ⋅ Var(z := u))" "p ∈ poss (s' ⋅ Var(z := u))" "confl (Suc i) (t' ⋅ Var(z := u) |_ p) (s' ⋅ Var(z := u) |_ p)"
by auto
thus ?thesis by (intro exI[of _ p], auto simp: confl_def split: term.splits)
next
case (VV x x')
thus ?thesis using p vars_u by (intro exI[of _ p], cases u, auto simp: confl_def var_ind_conv)
qed
thus "∃p. p ∈ poss (s mp ⋅ σ') ∧ p ∈ poss (t mp ⋅ σ') ∧ confl (Suc i) (s mp ⋅ σ' |_ p) (t mp ⋅ σ' |_ p)"
unfolding σ'_comp subst_subst_compose s'_def t'_def by auto
qed
qed
}
from this[of n]
obtain σ where σ: "cg_subst_ind n σ" and confl: "⋀ mp. mp ∈ pp ⟹ ∃p. p ∈ poss (s mp ⋅ σ) ∧ p ∈ poss (t mp ⋅ σ) ∧ confl n (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p)"
by blast
define σ' :: "('f,nat × 's,'v)gsubst" where "σ' x = Var undefined" for x
let ?σ = "σ ∘⇩s σ'"
have "cg_subst ?σ" unfolding cg_subst_def subst_compose_def
proof (intro allI impI)
fix x :: "nat × 's"
assume "snd x ∈ S"
with σ[unfolded cg_subst_ind_def, rule_format, of x]
have "σ x : snd x in 𝒯(C,EMPTYn)" by auto
thus "σ x ⋅ σ' : snd x in 𝒯(C,EMPTY)" by (rule type_conversion1)
qed
from pp[unfolded pat_complete_def match_complete_wrt_def, rule_format, OF this]
obtain mp μ where mp: "mp ∈ pp" and match: "⋀ ti li. (ti, li)∈ mp ⟹ ti ⋅ ?σ = li ⋅ μ" by force
from P1[OF this(1)]
have "(s mp, Var (x mp)) ∈ mp" "(t mp, Var (x mp)) ∈ mp" by auto
from match[OF this(1)] match[OF this(2)] have ident: "s mp ⋅ ?σ = t mp ⋅ ?σ" by auto
from confl[OF mp] obtain p
where p: "p ∈ poss (s mp ⋅ σ)" "p ∈ poss (t mp ⋅ σ)" and confl: "confl n (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p)"
by auto
let ?s = "s mp ⋅ σ" let ?t = "t mp ⋅ σ"
from confl_n[OF confl] obtain f g ss ts where
confl: "?s |_p = Fun f ss" "?t |_p = Fun g ts" and diff: "(f,length ss) ≠ (g,length ts)" by auto
define s' where "s' = s mp ⋅ σ"
define t' where "t' = t mp ⋅ σ"
from confl p ident
have False
unfolding subst_subst_compose s'_def[symmetric] t'_def[symmetric]
proof (induction p arbitrary: s' t')
case Nil
then show ?case using diff by (auto simp: list_eq_nth_eq)
next
case (Cons i p s t)
from Cons obtain h1 us1 where s: "s = Fun h1 us1" by (cases s, auto)
from Cons obtain h2 us2 where t: "t = Fun h2 us2" by (cases t, auto)
from Cons(2,4)[unfolded s] have si: "(us1 ! i) |_ p = Fun f ss" "p ∈ poss (us1 ! i)" and i1: "i < length us1" by auto
from Cons(3,5)[unfolded t] have ti: "(us2 ! i) |_ p = Fun g ts" "p ∈ poss (us2 ! i)" and i2: "i < length us2" by auto
from Cons(6)[unfolded s t] i1 i2 have " us1 ! i ⋅ σ' = us2 ! i ⋅ σ'" by (auto simp: list_eq_nth_eq)
from Cons.IH[OF si(1) ti(1) si(2) ti(2) this]
show False .
qed
}
thus ?case by auto
qed
end
end