theory Bounded_Increase
imports
Generalized_Usable_Rules
begin
text ‹in this theory, we introduce the induction calculus from
the CADE07 "Bounded Increase" paper, and prove its soundness.
We generalize the result, since we only demand minimality or unique normal forms.›
text ‹free variables of a constraint, as set and as list›
fun vars_cc :: "('f, 'v) cond_constraint ⇒ 'v set" where
"vars_cc (CC_cond ct (s, t)) = vars_term s ∪ vars_term t"
| "vars_cc (CC_rewr s t) = vars_term s ∪ vars_term t"
| "vars_cc (CC_impl cs c) = ⋃(vars_cc ` set cs) ∪ vars_cc c"
| "vars_cc (CC_all x c) = vars_cc c - {x}"
fun vars_cc_list :: "('f, 'v) cond_constraint ⇒ 'v list" where
"vars_cc_list (CC_cond ct (s, t)) = vars_term_list s @ vars_term_list t"
| "vars_cc_list (CC_rewr s t) = vars_term_list s @ vars_term_list t"
| "vars_cc_list (CC_impl c1 c2) = concat (map vars_cc_list c1) @ vars_cc_list c2"
| "vars_cc_list (CC_all x c) = [ y . y <- vars_cc_list c, y ≠ x]"
lemma vars_cc_list [simp]:
"set (vars_cc_list c) = vars_cc c"
by (induct c) auto
text ‹constructor for adding multiple quantors›
fun cc_bound :: "'v list ⇒ ('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint" where
"cc_bound [] c = c"
| "cc_bound (x # xs) c = CC_all x (cc_bound xs c)"
locale fresh =
fixes fresh :: "'v list ⇒ 'v"
begin
text ‹apply a substitution
(where the list besides the substitution contains information on which variables have to be avoided)›
fun cc_subst_apply :: "('f,'v)cond_constraint ⇒ (('f,'v)subst × 'v list) ⇒ ('f,'v)cond_constraint" (infix "⋅⇩cc" 70) where
"CC_cond ct (s,t) ⋅⇩cc (σ,_) = CC_cond ct (s ⋅ σ,t ⋅ σ)"
| "CC_rewr s t ⋅⇩cc (σ,_) = CC_rewr (s ⋅ σ) (t ⋅ σ)"
| "CC_impl c1 c2 ⋅⇩cc σ = CC_impl (map (λ c. c ⋅⇩cc σ) c1) (c2 ⋅⇩cc σ)"
| "CC_all x c ⋅⇩cc (σ,vs) = (let y = fresh (vs @ vars_cc_list (CC_all x c)) in
CC_all y (c ⋅⇩cc (σ(x := Var y), y # vs)))"
text ‹uniquely rename all bound variables by applying empty substitution›
definition normalize_alpha :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint" where
"normalize_alpha c ≡ c ⋅⇩cc (Var,[])"
text ‹construct induction hypothesis for induction rule›
definition cc_ih_prems :: "'f ⇒ ('f,'v)term ⇒ 'v list
⇒ ('f,'v)cond_constraint list ⇒ ('f,'v)cond_constraint ⇒ (('f,'v)term × 'v list) list ⇒ ('f,'v)cond_constraint list" where
"cc_ih_prems f q xs φ ψ rs_ys_list ≡
map (λ (r,ys). let
rs = args r;
μ = mk_subst Var (zip xs rs);
vs' = range_vars_impl (zip xs rs);
mu = λ c. c ⋅⇩cc (μ,vs');
φ' = CC_impl (CC_rewr r (q ⋅ μ) # map mu φ) (mu ψ)
in cc_bound ys φ') rs_ys_list"
text ‹construct constraint for each rule when applying induction rule, the user can choose a list
of subterms (with corresponding free variables) for which IHs should be generated.›
definition cc_rule_constraint :: "'f ⇒ ('f,'v)term list ⇒ ('f,'v)term ⇒ ('f,'v)term ⇒ 'v list
⇒ ('f,'v)cond_constraint list ⇒ ('f,'v)cond_constraint ⇒ (('f,'v)term × 'v list) list ⇒ ('f,'v)cond_constraint" where
"cc_rule_constraint f ls r q xs φ ψ rs_ys_list ≡
let
σ = mk_subst Var (zip xs ls);
vs = range_vars_impl (zip xs ls);
rew = CC_rewr r (q ⋅ σ);
phi_sig = map (λc. c ⋅⇩cc (σ,vs)) φ;
psi_sig = ψ ⋅⇩cc (σ,vs);
ihs = cc_ih_prems f q xs φ ψ rs_ys_list
in CC_impl (rew # phi_sig @ ihs) psi_sig"
end
declare fresh.cc_subst_apply.simps[code]
declare fresh.normalize_alpha_def[code]
declare fresh.cc_rule_constraint_def[code]
declare fresh.cc_ih_prems_def[code]
locale fixed_trs_dep_order_fresh = fixed_trs_dep_order π R Q F S NS nfs m const + fresh fresh
for π :: "('f :: countable) dep"
and R :: "('f,'v :: countable)trs"
and Q :: "('f,'v)terms"
and F :: "'f sig"
and S :: "('f,'v)trs"
and NS :: "('f,'v)trs"
and nfs :: bool
and m :: bool
and fresh :: "'v list ⇒ 'v"
and const :: 'f
+ fixes UR :: "('f,'v)term ⇒ ('f,'v)trs"
assumes fresh: "fresh vs ∉ set vs"
and UR: "⋀ t u σ. σ ` vars_term t ⊆ NF_terms Q ⟹ (t ⋅ σ, u) ∈ (qrstep nfs Q R)^* ⟹ (t ⋅ σ, u) ∈ (qrstep nfs Q (UR t))^*"
and UR_sub: "⋀ t. UR t ⊆ R"
begin
text ‹only the free variables matter, when checking the model condition›
lemma cc_models_vars:
assumes "⋀ x. x ∈ vars_cc c ⟹ σ x = τ x"
shows "σ ⊨ c = τ ⊨ c"
using assms
proof (induct c arbitrary: σ τ)
case (cond ct s t)
have "(Fun f [s,t,Fun const []]) ⋅ σ = (Fun f [s,t,Fun const []] ⋅ τ)"
by (rule term_subst_eq, insert cond, auto)
thus ?case by auto
next
case (rewr s t)
have "(Fun f [s,t]) ⋅ σ = (Fun f [s,t] ⋅ τ)"
by (rule term_subst_eq, insert rewr, auto)
thus ?case by auto
next
case (impl c1 c2 σ τ)
from this(1)[of _ σ τ] this(2)[of σ τ] this(3)
show ?case by auto
next
case (all x c σ τ)
{
fix t
have "σ(x := t) ⊨ c = τ(x := t) ⊨ c"
by (rule all(1), insert all(2), auto)
}
thus ?case by auto
qed
text ‹the substitution lemma for conditional constraints›
lemma cc_models_subst: assumes vs: "range_vars σ1 ⊆ set vs"
shows "(σ2 ⊨ c ⋅⇩cc (σ1,vs)) = (σ1 ∘⇩s σ2 ⊨ c)"
using vs
proof (induct c arbitrary: σ1 σ2 vs)
case (all x c σ1 σ2 vs)
let ?Var = "Var :: 'v ⇒ ('f,'v)term"
obtain y where y: "fresh (vs @ vars_cc_list (CC_all x c)) = y" by auto
with fresh[of "vs @ vars_cc_list (CC_all x c)"] have fresh: "y ∉ set vs ∪ vars_cc (CC_all x c)" by auto
with all(2) have y1: "y ∉ range_vars σ1" by auto
let ?vs = "y # vs"
have "range_vars (σ1(x := ?Var y)) ⊆ set ?vs"
proof
fix z
assume "z ∈ range_vars (σ1(x := ?Var y))"
then obtain u where u: "u ∈ subst_domain (σ1(x := ?Var y))" and z: "z ∈ vars_term ((σ1(x := ?Var y)) u)"
unfolding range_vars_def by auto
show "z ∈ set ?vs"
proof (cases "u = x")
case True
with z show ?thesis by auto
next
case False
with u have "u ∈ subst_domain σ1" unfolding subst_domain_def by auto
with z False have "z ∈ range_vars σ1" unfolding range_vars_def by auto
with all(2) show ?thesis by auto
qed
qed
note IH = all(1)[OF this]
show ?case unfolding cc_subst_apply.simps y Let_def
proof -
show "(σ2 ⊨ CC_all y (c ⋅⇩cc (σ1(x := Var y), ?vs))) =
σ1 ∘⇩s σ2 ⊨ CC_all x c" (is "?l = ?r")
proof -
def P ≡ "λ t. funas_term t ⊆ F ∧ t ∈ NF_trs R"
have l: "?l = (∀ t. P t ⟶ σ2( y := t) ⊨ (c ⋅⇩cc (σ1(x := Var y), ?vs)))" unfolding P_def by auto
have r: "?r = (∀ t. P t ⟶ (σ1 ∘⇩s σ2) (x := t) ⊨ c)" unfolding P_def by auto
{
fix t
assume "P t"
let ?l = "(σ1(x := Var y) ∘⇩s σ2(y := t))"
let ?r = "((σ1 ∘⇩s σ2)(x := t))"
have "((σ2( y := t) ⊨ (c ⋅⇩cc (σ1(x := Var y), ?vs)))
= ((σ1 ∘⇩s σ2) (x := t) ⊨ c)) = (?l ⊨ c = ?r ⊨ c)"
unfolding IH by simp
also have "(?l ⊨ c = ?r ⊨ c) = True"
proof -
{
fix z
assume z: "z ∈ vars_cc c"
have "?l z = ?r z"
proof (cases "z = x")
case True
thus ?thesis by (simp add: subst_compose_def)
next
case False
with z fresh have neq: "y ≠ z" by auto
have "(?l z = ?r z) = (σ1 z ⋅ σ2(y := t) = σ1 z ⋅ σ2)" unfolding subst_compose_def using False by simp
moreover have "..."
proof (cases "z ∈ subst_domain σ1")
case True
hence "vars_term (σ1 z) ⊆ range_vars σ1" unfolding range_vars_def by auto
with y1 have y: "y ∉ vars_term (σ1 z)" by auto
show ?thesis
by (rule term_subst_eq, insert y, auto)
next
case False
hence z1: "σ1 z = Var z" unfolding subst_domain_def by auto
show ?thesis unfolding z1 using neq by simp
qed
ultimately show ?thesis by simp
qed
} note main = this
hence "(?l ⊨ c = ?r ⊨ c)" by (rule cc_models_vars)
thus ?thesis by simp
qed
finally have "(σ2( y := t) ⊨ (c ⋅⇩cc (σ1(x := Var y), ?vs)))
= ((σ1 ∘⇩s σ2) (x := t) ⊨ c)" by simp
} thus ?thesis unfolding l r by auto
qed
qed
qed auto
lemma normalize_alpha: "σ ⊨ normalize_alpha c = σ ⊨ c"
proof -
have id: "σ ⊨ c = Var ∘⇩s σ ⊨ c" by simp
show ?thesis unfolding normalize_alpha_def id
by (rule cc_models_subst, unfold range_vars_def, auto)
qed
lemma alpha_equivalence: assumes eq: "normalize_alpha c = normalize_alpha d"
shows "c =cc d"
proof (rule cc_equivI)
fix σ
have "σ ⊨ c = σ ⊨ normalize_alpha c" unfolding normalize_alpha ..
also have "... = σ ⊨ normalize_alpha d" unfolding eq ..
also have "... = σ ⊨ d" unfolding normalize_alpha ..
finally show "σ ⊨ c = σ ⊨ d" .
qed
lemma cc_models_boundE: assumes ys: "⋀ x. x ∉ set ys ⟹ σ x = δ x"
and models: "σ ⊨ cc_bound ys c"
and F: "normal_F_subst δ"
shows "δ ⊨ c"
using ys models
proof (induct ys arbitrary: σ)
case Nil
thus ?case by simp
next
case (Cons y ys σ)
let ?y = "δ y"
from F[unfolded normal_F_subst_def] have "funas_term ?y ⊆ F" and "?y ∈ NF_trs R" by auto
with Cons(3) have model: "σ(y := ?y) ⊨ cc_bound ys c" by auto
show ?case
by (rule Cons(1)[OF _ model], insert Cons(2), auto)
qed
lemma cc_models_boundI:
assumes ys: "⋀ σ. ⟦⋀x. x ∉ set ys ⟹ σ x = δ x⟧ ⟹ ⟦⋀x. x ∈ set ys ⟹ funas_term (σ x) ⊆ F ∧ σ x ∈ NF_trs R⟧ ⟹ σ ⊨ c"
shows "δ ⊨ cc_bound ys c"
using ys
proof (induct ys arbitrary: δ)
case Nil
thus ?case by simp
next
case (Cons y ys δ)
show ?case unfolding cc_bound.simps cc_models.simps
proof (intro allI impI)
fix t
assume tF: "funas_term t ⊆ F" and t: "t ∈ NF_trs R"
show "δ(y := t) ⊨ cc_bound ys c"
proof (rule Cons(1))
fix σ
assume eq: "⋀x. x ∉ set ys ⟹ σ x = (δ(y := t)) x"
assume fun_NF: "⋀x. x ∈ set ys ⟹ funas_term (σ x) ⊆ F ∧ σ x ∈ NF_trs R"
show "σ ⊨ c"
proof (rule Cons(2))
fix x
assume "x ∉ set (y # ys)" with eq[of x] show "σ x = δ x" by auto
next
fix x
assume "x ∈ set (y # ys)"
thus "funas_term (σ x) ⊆ F ∧ σ x ∈ NF_trs R" using eq[of x] fun_NF[of x] tF t
by (cases "x ∈ set ys", auto)
qed
qed
qed
qed
end
text ‹in the paper, constraints always occur in the form .. ∧ .. ∧ .. ⟶ ..,
therefore we provide means to transform every formula in this form›
fun concl_of :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint" where
"concl_of (CC_impl c1 c2) = c2"
| "concl_of c = c"
fun prems_of :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint list" where
"prems_of (CC_impl c1 c2) = c1"
| "prems_of c = []"
definition normalize_cc :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint" where
"normalize_cc c ≡ CC_impl (prems_of c) (concl_of c)"
lemma vars_cc_normalize[simp]: "vars_cc (normalize_cc c) = vars_cc c"
by (cases c, auto simp: normalize_cc_def)
context fixed_trs_dep_order
begin
lemma normalize_cc: "(σ ⊨ c) = (σ ⊨ normalize_cc c)" unfolding normalize_cc_def
proof (cases c)
case (CC_impl c1 c2)
show "σ ⊨ c = σ ⊨ CC_impl ((prems_of c)) (concl_of c)" unfolding CC_impl by auto
qed auto
lemma normalize_cc_valid: "cc_valid (normalize_cc c) ⟹ cc_valid c"
unfolding cc_valid_def normalize_cc[symmetric] by auto
lemma normalize_cc_equivI: "normalize_cc c = normalize_cc d ⟹ c =cc d"
by (rule cc_equivI, unfold normalize_cc[of _ c] normalize_cc[of _ d], auto)
lemma normalize_validI: "normalize_cc c = CC_impl φ ψ ⟹
⟦⋀ σ. normal_F_subst σ ⟹ ⟦ ⋀ c'. c' ∈ set φ ⟹ σ ⊨ c' ⟧ ⟹ σ ⊨ ψ⟧ ⟹ cc_valid c"
using normalize_cc[of _ c] unfolding cc_valid_def by auto
lemma normalize_validE: "normalize_cc c = CC_impl φ ψ ⟹ cc_valid c ⟹ normal_F_subst σ ⟹
⟦ ⋀ c'. c' ∈ set φ ⟹ σ ⊨ c'⟧ ⟹ σ ⊨ ψ"
using normalize_cc[of _ c] unfolding cc_valid_def by auto
end
context fixed_trs_dep_order_fresh
begin
text ‹Here, all rules of the induction calculus are formulated. We return a list of constraint instead of one
constraint, and therefore do not require the primitives "conjunction" and "TRUE" for conditional constraints.›
inductive cc_simplify :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint list ⇒ bool" (infix "⊢" 51) where
delete_conditions: "normalize_cc c = CC_impl φ ψ ⟹ normalize_cc c' = CC_impl φ' ψ ⟹ set φ' ⊆ set φ ⟹ c ⊢ [c']"
| constructor_different: "normalize_cc c = CC_impl φ ψ ⟹ (f,length ss) ≠ (g,length ts) ⟹ ¬ (defined R (f,length ss))
⟹ CC_rewr (Fun f ss) (Fun g ts) ∈ set φ ⟹ c ⊢ []"
| constructor_same: "normalize_cc c = CC_impl φ ψ
⟹ c' ⟶cc CC_impl (φ @ map (λ (s,t). CC_rewr s t) (zip ss ts)) ψ
⟹ length ss = length ts ⟹ ¬ (defined R (f,length ss))
⟹ CC_rewr (Fun f ss) (Fun f ts) ∈ set φ
⟹ c ⊢ [c']"
| variable_left: "normalize_cc c = CC_impl φ ψ
⟹ c' ⟶cc c ⋅⇩cc τ
⟹ τ = (Var(x := q),vars_term_list q) ⟹ CC_rewr (Var x) q ∈ set φ
⟹ c ⊢ [c']"
| variable_right: "normalize_cc c = CC_impl φ ψ
⟹ c' ⟶cc c ⋅⇩cc τ
⟹ τ = (Var(x := q),vars_term_list q) ⟹ CC_rewr q (Var x) ∈ set φ
⟹ ⟦ ⋀ fn. fn ∈ funas_term q ⟹ ¬ defined R fn⟧
⟹ c ⊢ [c']"
| simplify_condition: "normalize_cc c = CC_impl φ ψ
⟹ cc_bound ys cc ∈ set φ
⟹ normalize_cc cc = CC_impl φ' ψ'
⟹ subst_domain σ ⊆ set ys
⟹ range_vars σ ⊆ set vs
⟹ ⟦⋀ fn. fn ∈ ⋃(funas_term ` subst_range σ) ⟹ fn ∈ F ∧ ¬ (defined R fn)⟧
⟹ ⟦⋀ c. c ∈ set φ' ⟹ ∃ d ∈ set φ. d ⟶cc c ⋅⇩cc (σ,vs)⟧
⟹ c' ⟶cc CC_impl (ψ' ⋅⇩cc (σ,vs) # φ) ψ
⟹ c ⊢ [c']"
| fun_arg_into_var: "normalize_cc c = CC_impl φ ψ
⟹ c' ⟶cc CC_impl (CC_rewr p (Var x) # CC_rewr (Fun f (bef @ Var x # aft)) q # φ) ψ
⟹ x ∉ vars_cc c
⟹ CC_rewr (Fun f (bef @ p # aft)) q ∈ set φ
⟹ funas_term p ⊆ F
⟹ c ⊢ [c']"
| induction: "normalize_cc c = CC_impl φ' ψ
⟹ mgu (Fun f (map Var xs)) q = None
⟹ CC_rewr (Fun f (map Var xs)) q ∈ set φ'
⟹ set φ ⊆ set φ'
⟹ ⟦ ⋀ ls r. length xs = length ls ⟹ (Fun f ls,r) ∈ R ⟹ ∃ d ls' r' r_ys_list.
(Fun f ls,r) =⇩v (Fun f ls',r') ∧ vars_rule (Fun f ls',r') ∩ vars_cc (CC_impl (CC_rewr (Fun f (map Var xs)) q # φ) ψ) = {} ∧ d ∈ set cs ∧ d ⟶cc cc_rule_constraint f ls' r' q xs φ ψ r_ys_list
∧ (∀(r, ys) ∈ set r_ys_list. root r = Some (f,length xs) ∧ r' ⊵ r ∧ vars_term r' ∩ set ys = {} ∧ (∀ fn ∈ funas_args_term r. ¬ defined R fn))⟧
⟹ distinct xs
⟹ m ∨ CR (rstep (UR (Fun f (map Var xs)))) (* we directly require CR instead of UNF, since we only have means to prove the former *)
⟹ c ⊢ cs"
end
text ‹before proving soundness, we need to express the distance to normal form,
which is the induction relation, if minimality is not present›
definition distance :: "'a rel ⇒ 'a set ⇒ 'a ⇒ nat" where
"distance r s a ≡ LEAST n. ∃ b ∈ s. (a,b) ∈ r ^^ n"
lemma distance_path: assumes b: "b ∈ s" and path: "(a,b) ∈ r^*"
shows "∃ b ∈ s. (a,b) ∈ r ^^ distance r s a"
proof -
let ?p = "λ n. ∃ b ∈ s. (a,b) ∈ r ^^ n"
from rtrancl_imp_relpow[OF path] b have "∃ n. ?p n" by blast
from LeastI_ex[of ?p, OF this]
show ?thesis unfolding distance_def .
qed
lemma distance_least: assumes "b ∈ s" and "(a,b) ∈ r^^n"
shows "distance r s a ≤ n"
unfolding distance_def
by (rule Least_le, insert assms, auto)
lemma distance_Suc_relpow: assumes b: "b ∈ s" and path: "(a,b) ∈ r ^^ distance r s a" and a: "a ≠ b"
shows "∃ c. (a,c) ∈ r ∧ (c,b) ∈ r ^^ distance r s c ∧ distance r s a = Suc (distance r s c)"
proof -
from a path obtain n where d: "distance r s a = Suc n" by (cases "distance r s a", auto)
from relpow_Suc_D2[OF path[unfolded d]] obtain c where ac: "(a,c) ∈ r" and cb: "(c,b) ∈ r ^^ n" by auto
from distance_least[OF b cb] have n: "distance r s c ≤ n" .
{
assume n: "distance r s c < n"
from distance_path[OF b relpow_imp_rtrancl[OF cb]] obtain b' where b': "b' ∈ s" and cb': "(c,b') ∈ r ^^ distance r s c" ..
from distance_least[OF b' relpow_Suc_I2[OF ac cb'], unfolded d] n have False by arith
}
with n have n: "n = distance r s c" by arith
show ?thesis
by (intro exI conjI, rule ac, insert cb d n, auto)
qed
lemma distance_Suc_rtrancl: assumes b: "b ∈ s" and path: "(a,b) ∈ r^*" and a: "a ∉ s"
shows "∃ c b. (a,c) ∈ r ∧ (c,b) ∈ r^* ∧ distance r s a = Suc (distance r s c)"
proof -
from distance_path[OF b path] obtain b' where b': "b' ∈ s" "(a,b') ∈ r ^^ distance r s a" by blast
from a b' have "a ≠ b'" by auto
from distance_Suc_relpow[OF b' this] obtain c where ac: "(a, c) ∈ r"
and cb: "(c, b') ∈ r ^^ distance r s c" and d: "distance r s a = Suc (distance r s c)" by blast
from ac relpow_imp_rtrancl[OF cb] d show ?thesis by blast
qed
text ‹the following lemma is essentially proven by using the fact that any normalizing
reduction can be reordered to a reduction, where one first reduces some subterm c to normal form.
Most of the tedious reasoning is hidden in @{thm normalize_subterm_qrsteps_count}.›
lemma distance_subterm: fixes Q R nfs
defines dist: "dist ≡ distance (qrstep nfs Q R) (NF_terms Q)"
assumes b: "b ∈ NF_terms Q" and ab: "(a,b) ∈ (qrstep nfs Q R)^*"
and ac: "a ⊵ c"
shows "dist a ≥ dist c"
proof -
from distance_path[OF b ab] obtain b where
b: "b ∈ NF_terms Q" and ab: "(a, b) ∈ qrstep nfs Q R ^^ dist a" unfolding dist by auto
from supteq_imp_subt_at[OF ac] obtain p where p: "p ∈ poss a" and c: "c = a |_ p" by auto
from normalize_subterm_qrsteps_count[OF p ab b]
obtain n1 n2 u where cu: "(c, u) ∈ qrstep nfs Q R ^^ n1" and u: "u ∈ NF_terms Q" and da: "dist a = n1 + n2"
unfolding c by blast
from distance_least[OF u cu] have "dist c ≤ n1" unfolding dist by auto
also have "… ≤ dist a" unfolding da by simp
finally show ?thesis .
qed
definition UNF_r_q where
"UNF_r_q r q ≡ ∀ a b c. (a,b) ∈ r^* ⟶ (a,c) ∈ r^* ⟶ b ∈ q ⟶ c ∈ q ⟶ b = c"
text ‹confluence is a sufficient condition for unique normal forms. In the following lemma,
usually R' are the usable rules of R.›
lemma CR_imp_UNF_inn: assumes inn: "NF_terms Q ⊆ NF_trs R" and sub: "R' ⊆ R" and cr: "CR (rstep R')"
shows "UNF_r_q (qrstep nfs Q R') (NF_terms Q)"
proof -
let ?QR = "qrstep nfs Q R"
let ?QR' = "qrstep nfs Q R'"
let ?Q = "NF_terms Q"
let ?R' = "rstep R'"
show ?thesis
unfolding UNF_r_q_def
proof (intro allI impI)
fix a b c
assume ab: "(a,b) ∈ ?QR'^*" and ac: "(a,c) ∈ ?QR'^*" and b: "b ∈ ?Q" and c: "c ∈ ?Q"
from inn NF_anti_mono[OF rstep_mono[OF sub]] have inn: "?Q ⊆ NF ?R'" by auto
have sub: "?QR'^* ⊆ ?R'^*" by (rule rtrancl_mono, auto)
from sub ab ac have ab: "(a,b) ∈ ?R'^*" and ac: "(a,c) ∈ ?R'^*" by auto
from inn b c have b: "b ∈ NF ?R'" and c: "c ∈ NF ?R'" by auto
from CR_imp_UNF[OF cr] ab ac b c show "b = c" by auto
qed
qed
text ‹if there unique normal forms, then one can reach any normal form via a path, where the length
of this path is exactly the distance›
lemma distance_NF_UNF: assumes NF: "s ⊆ q" and UNF: "UNF_r_q r q" and b: "b ∈ s" and path: "(a,b) ∈ r^*"
shows "(a,b) ∈ r^^distance r s a"
proof -
from distance_path[OF b path] obtain b' where b': "b' ∈ s" and ab': "(a,b') ∈ r ^^ distance r s a" ..
from b b' NF have "b ∈ q" "b' ∈ q" by auto
with path relpow_imp_rtrancl[OF ab'] UNF[unfolded UNF_r_q_def] have "b' = b" by auto
with ab' show ?thesis by auto
qed
context fixed_trs_dep_order_fresh
begin
text ‹the main soundness lemma for the induction calculus›
lemma cc_simplify: "c ⊢ c' ⟹ Ball (set c') cc_valid ⟹ cc_valid c"
proof -
from wwf_var_cond[OF wwf] have Rfun: "∀(l, r)∈R. is_Fun l" .
note a_ndef = ndef_applicable_rules[of R _ Q]
{
fix δ :: "('f,'v)subst"
fix vs :: "'v list"
fix x :: 'v
fix q :: "('f,'v)term"
fix φ :: "('f,'v)cond_constraint"
assume vs: "vars_term q ⊆ set vs"
assume id: "δ x = q ⋅ δ"
have "(δ ⊨ φ ⋅⇩cc (Var(x := q),vs)) = (Var(x := q) ∘⇩s δ ⊨ φ)"
proof (rule cc_models_subst)
show "range_vars (Var(x := q)) ⊆ set vs" unfolding range_vars_def subst_range.simps subst_domain_def using vs
by auto
qed
also have "(Var(x := q) ∘⇩s δ) = δ"
proof
fix y
show "(Var(x := q) ∘⇩s δ) y = δ y"
by (unfold subst_compose_def, cases "y = x", insert id, auto)
qed
finally have "(δ ⊨ φ ⋅⇩cc (Var(x := q),vs)) = (δ ⊨ φ)" .
} note subst = this
show "c ⊢ c' ⟹ Ball (set c') cc_valid ⟹ cc_valid c"
proof (induct rule: cc_simplify.induct)
case (delete_conditions c φ ψ c' χ)
hence c': "cc_valid c'" by auto
show ?case
by (rule normalize_validI[OF delete_conditions(1)],
insert normalize_validE[OF delete_conditions(2) c'] delete_conditions(3), auto)
next
case (constructor_different c φ ψ f ss g ts)
show ?case
proof (rule normalize_validI[OF constructor_different(1)])
fix σ
assume phi: "⋀ c'. c' ∈ set φ ⟹ σ ⊨ c'"
have "(Fun f ss ⋅ σ, Fun g ts ⋅ σ) ∉ (qrstep nfs Q R)^*"
proof
let ?σ = "map (λ t. t ⋅ σ)"
from constructor_different(3) have ndef: "¬ defined R (the (root (Fun f (?σ ss))))" by simp
assume "(Fun f ss ⋅ σ, Fun g ts ⋅ σ) ∈ (qrstep nfs Q R)^*"
hence "(Fun f (?σ ss), Fun g (?σ ts)) ∈ (qrstep nfs Q R)^*" by simp
from nrqrsteps_preserve_root[OF qrsteps_imp_nrqrsteps[OF Rfun a_ndef[OF ndef] this]]
show False using constructor_different(2) by simp
qed
with phi[OF constructor_different(4)]
show "σ ⊨ ψ" by auto
qed
next
case (constructor_same c φ ψ c' ss ts f)
hence c': "cc_valid c'" by auto
note valid = cc_validE[OF cc_impliesE[OF constructor_same(2) c']]
show ?case
proof (rule normalize_validI[OF constructor_same(1)])
fix σ
assume nfs: "normal_F_subst σ"
note valid = valid[OF nfs]
assume phi: "⋀c'. c' ∈ set φ ⟹ σ ⊨ c'"
from phi[OF constructor_same(5)] have
mrewr: "σ ⊨ CC_rewr (Fun f ss) (Fun f ts)" by auto
from constructor_same have len: "length ss = length ts" by simp
have "Ball (set (map (λ(s, t). CC_rewr s t) (zip ss ts))) (cc_models σ) =
(∀ i. i < length ss ⟶ σ ⊨ CC_rewr (ss ! i) (ts ! i))" using len
by (auto simp: set_zip)
also have "..."
proof (intro allI impI)
fix i
assume i: "i < length ss"
let ?σ = "map (λ t. t ⋅ σ)"
from a_ndef[OF constructor_same(4)] have ndef: "¬ defined (applicable_rules Q R) (the (root (Fun f (?σ ss))))" by simp
from mrewr have steps: "(Fun f (?σ ss), Fun f (?σ ts)) ∈ (qrstep nfs Q R)^*" by simp
from mrewr have nf: "Fun f (?σ ts) ∈ NF_terms Q" by simp
from nrqrsteps_imp_arg_qrsteps[OF qrsteps_imp_nrqrsteps[OF Rfun ndef steps], of i] i len
have steps: "(ss ! i ⋅ σ, ts ! i ⋅ σ) ∈ (qrstep nfs Q R)^*" by auto
have nf: "ts ! i ⋅ σ ∈ NF_terms Q" by (rule NF_subterm[OF nf], insert i len, auto)
{
assume m
with mrewr have SN: "SN_on (qrstep nfs Q R) {Fun f (?σ ss)}" unfolding m_SN_def cc_models.simps by simp
have SN: "SN_on (qrstep nfs Q R) {ss ! i ⋅ σ}"
by (rule SN_imp_SN_arg_gen[OF ctxt_closed_qrstep SN], insert i, auto)
}
hence SN: "m_SN (ss ! i ⋅ σ)" unfolding m_SN_def by simp
show "σ ⊨ CC_rewr (ss ! i) (ts ! i)" using steps nf SN by auto
qed
finally show "σ ⊨ ψ" using valid phi by auto
qed
next
case (variable_left c φ ψ c' τ x q)
hence c': "cc_valid c'" by auto
note valid = cc_validE[OF cc_impliesE[OF variable_left(2) c']]
show ?case
proof (rule normalize_validI[OF variable_left(1)])
fix σ
assume sigma: "normal_F_subst σ"
assume phi: "⋀c'. c' ∈ set φ ⟹ σ ⊨ c'"
from phi[OF variable_left(4)] have
steps: "(σ x, q ⋅ σ) ∈ (qrstep nfs Q R)^*" by auto
from steps rtrancl_mono[OF qrstep_mono[of R R Q "{}" nfs]] have steps: "(σ x, q ⋅ σ) ∈ (rstep R)^*" by auto
from sigma[unfolded normal_F_subst_def] NFQ have sigmax: "σ x ∈ NF_trs R" by force
from steps sigmax have id: "σ x = q ⋅ σ" unfolding NF_def by (induct, auto)
have subset: "vars_term q ⊆ set (vars_term_list q)" by auto
note subst = subst[OF subset id, unfolded variable_left(3)[symmetric]]
from valid[OF sigma, unfolded subst normalize_cc[of _ c] variable_left(1)] phi
show "σ ⊨ ψ" by auto
qed
next
case (variable_right c φ ψ c' τ x q)
hence c': "cc_valid c'" by auto
note valid = cc_validE[OF cc_impliesE[OF variable_right(2) c']]
show ?case
proof (rule normalize_validI[OF variable_right(1)])
fix σ
assume sigma: "normal_F_subst σ"
assume phi: "⋀c'. c' ∈ set φ ⟹ σ ⊨ c'"
from phi[OF variable_right(4)] have
steps: "(q ⋅ σ, σ x) ∈ (qrstep nfs Q R)^*" by auto
have "q ⋅ σ ∈ NF (qrstep nfs Q R)"
proof (rule NF_subst_qrstep[OF a_ndef[OF variable_right(5)] _ Rfun])
fix x
from sigma[unfolded normal_F_subst_def] have NF: "σ x ∈ NF_trs R" by auto
thus "σ x ∈ NF (qrstep nfs Q R)" using NF_anti_mono[OF qrstep_mono[of R R Q "{}" nfs]] by auto
qed
with steps
have id: "σ x = q ⋅ σ" unfolding NF_def by (induct, auto)
have subset: "vars_term q ⊆ set (vars_term_list q)" by auto
note subst = subst[OF subset id, unfolded variable_right(3)[symmetric]]
from valid[OF sigma, unfolded subst normalize_cc[of _ c] variable_right(1)] phi
show "σ ⊨ ψ" by auto
qed
next
case (simplify_condition c φ ψ ys cc φ' ψ' σ vs c')
hence c': "cc_valid c'" by auto
show ?case
proof (rule normalize_validI[OF simplify_condition(1)])
fix δ
assume delta: "normal_F_subst δ"
assume "⋀c'. c' ∈ set φ ⟹ δ ⊨ c'"
with simplify_condition(2)
have delta_bound: "δ ⊨ cc_bound ys cc" and delta_phi: "Ball (set φ) (cc_models δ)" by auto
note delta_nf = delta[unfolded normal_F_subst_def]
let ?δ' = "σ ∘⇩s δ"
{
fix x
assume "x ∉ subst_domain σ"
hence "σ x = Var x" unfolding subst_domain_def by auto
hence "?δ' x = δ x" unfolding subst_compose_def by simp
} note delta_id = this
with simplify_condition(4) have delta_idd: "⋀ x. x ∉ set ys ⟹ δ x = ?δ' x" by force
{
fix t
assume "t ∈ range ?δ'"
then obtain x where x: "?δ' x = t" by auto
have "funas_term t ⊆ F ∧ t ∈ NF_trs R"
proof (cases "x ∈ subst_domain σ")
case False
from x delta_id[OF this] have "t ∈ range δ" by auto
with delta_nf show ?thesis by auto
next
case True
with simplify_condition(4) have x_ys: "x ∈ set ys" by auto
from x have t: "t = σ x ⋅ δ" unfolding subst_compose_def by auto
from True have range: "σ x ∈ subst_range σ" by simp
from range simplify_condition(6) have F: "funas_term (σ x) ⊆ F" by force
from range simplify_condition(6) have ndef: "⋀ fn. fn ∈ funas_term (σ x) ⟹ ¬ defined R fn" by force
show ?thesis unfolding t
proof
show "funas_term (σ x ⋅ δ) ⊆ F" using F delta_nf unfolding funas_term_subst by auto
next
have "σ x ⋅ δ ∈ NF (qrstep nfs {} R)"
proof (rule NF_subst_qrstep[OF _ _ Rfun])
fix fn
assume "fn ∈ funas_term (σ x)"
from ndef[OF this] show "¬ defined (applicable_rules {} R) fn" unfolding applicable_rules_def applicable_rule_def by auto
next
fix y
assume "y ∈ vars_term (σ x)"
show "δ y ∈ NF (qrstep nfs {} R)" using delta_nf by auto
qed
thus "σ x ⋅ δ ∈ NF_trs R" by auto
qed
qed
}
hence nF: "normal_F_subst ?δ'" unfolding normal_F_subst_def by auto
from cc_models_boundE[OF delta_idd delta_bound nF]
have "?δ' ⊨ cc" .
from this[unfolded normalize_cc[of _ cc] simplify_condition(3)]
have "?δ' ⊨ CC_impl φ' ψ'" .
from this[unfolded cc_models_subst[OF simplify_condition(5), symmetric]]
have delta_imp: "δ ⊨ CC_impl φ' ψ' ⋅⇩cc (σ,vs)" .
{
fix c
assume "c ∈ set φ'"
from simplify_condition(7)[OF this] obtain d where d: "d ∈ set φ"
and imp: "d ⟶cc c ⋅⇩cc (σ,vs)" by auto
from d delta_phi have "δ ⊨ d" by auto
from cc_implies_substE[OF imp this]
have "δ ⊨ c ⋅⇩cc (σ,vs)" .
}
with delta_imp have "δ ⊨ ψ' ⋅⇩cc (σ,vs)" by auto
with delta_phi
have "Ball (set (ψ' ⋅⇩cc (σ,vs) # φ)) (cc_models δ)" by auto
with cc_validE[OF cc_impliesE[OF simplify_condition(8) c'] delta]
show "δ ⊨ ψ" by auto
qed
next
case (fun_arg_into_var c φ ψ c' p x f bef aft q)
hence c': "cc_valid c'" by auto
note valid = cc_validE[OF cc_impliesE[OF fun_arg_into_var(2) c']]
note c = fun_arg_into_var(1)
from fun_arg_into_var(1,3) have "x ∉ vars_cc (CC_impl φ ψ)" using vars_cc_normalize[of c] by auto
note x_fresh = this[simplified]
from fun_arg_into_var(4) x_fresh have "x ∉ vars_cc (CC_rewr (Fun f (bef @ p # aft)) q)" by auto
note x_fresh' = this[simplified]
let ?t = "λ x. Fun f (bef @ x # aft)"
show ?case
proof (rule normalize_validI[OF c])
fix σ
assume sigma: "normal_F_subst σ"
assume phi: "⋀c'. c' ∈ set φ ⟹ σ ⊨ c'"
from phi[OF fun_arg_into_var(4)]
have rewr: "σ ⊨ CC_rewr (?t p) q" .
let ?tsig = "λ x. Fun f (map (λ t. t ⋅ σ) bef @ x # map (λ t. t ⋅ σ) aft)"
from rewr have SN: "m_SN (?tsig (p ⋅ σ))" by simp
from rewr have steps: "(?tsig (p ⋅ σ), q ⋅ σ) ∈ (qrstep nfs Q R)^*" by simp
from rewr have NF: "q ⋅ σ ∈ NFQ" by simp
from normalize_subterm_qrsteps[OF _ steps NF, of "<length bef>"]
obtain u where steps1: "(p ⋅ σ, u) ∈ (qrstep nfs Q R)^*" and u: "u ∈ NFQ"
and steps2: "(?tsig u, q ⋅ σ) ∈ (qrstep nfs Q R)^*" by (auto simp: nth_append)
let ?δ = "σ(x := u)"
have p: "p ⋅ ?δ = p ⋅ σ" by (rule term_subst_eq, insert x_fresh', auto)
have q: "q ⋅ ?δ = q ⋅ σ" by (rule term_subst_eq, insert x_fresh', auto)
let ?m = "map (λt. t ⋅ σ)"
let ?mu = "map (λt. t ⋅ σ(x := u))"
have "(?t (Var x) ⋅ σ(x := u) = ?tsig u) = (?mu (bef @ aft) = ?m (bef @ aft))" by simp
moreover have "..."
by (rule map_cong[OF refl term_subst_eq], insert x_fresh', auto)
ultimately have tu: "?t (Var x) ⋅ σ(x := u) = ?tsig u" by simp
{
assume m
with SN[unfolded m_SN_def] have SN: "SN_on (qrstep nfs Q R) {?tsig (p ⋅ σ)}" by blast
from SN_imp_SN_arg_gen[OF ctxt_closed_qrstep SN, of "p ⋅ σ"] have SNp: "SN_on (qrstep nfs Q R) {p ⋅ σ}" by auto
from steps_preserve_SN_on[OF ctxt.closedD[OF ctxt.closed_rtrancl[OF ctxt_closed_qrstep] steps1], of "More f (?m bef) Hole (?m aft)"]
SN have SNu: "SN_on (qrstep nfs Q R) {?tsig u}" by auto
note SNp SNu
}
hence SNp: "m_SN (p ⋅ σ)" and SNu: "m_SN (?tsig u)" unfolding m_SN_def by auto
{
fix c
assume "c ∈ set φ ∪ {ψ}"
with x_fresh have x: "x ∉ vars_cc c" by auto
have "σ ⊨ c = ?δ ⊨ c"
by (rule cc_models_vars, insert x, auto)
} note id = this
have rewr1: "?δ ⊨ CC_rewr p (Var x)" unfolding cc_models.simps p using u SNp steps1 by auto
have rewr2: "?δ ⊨ CC_rewr (?t (Var x)) q" unfolding cc_models.simps tu q using steps2 NF SNu by auto
have phi: "Ball (set φ) (cc_models ?δ)" using phi id by auto
from NFQ u have NF: "u ∈ NF_trs R" by auto
note sigma = sigma[unfolded normal_F_subst_def]
have uF: "funas_term u ⊆ F"
by (rule qrsteps_funas_term[OF wwf RF _ steps1], unfold funas_term_subst, insert sigma fun_arg_into_var(5), auto)
{
fix y
have F: "funas_term (?δ y) ⊆ F" using sigma uF by auto
have NF: "?δ y ∈ NF_trs R" using NF sigma by auto
note F NF
}
hence delta: "normal_F_subst ?δ" unfolding normal_F_subst_def by auto
from id
have "σ ⊨ ψ = ?δ ⊨ ψ" by auto
also have "..." using valid[OF delta] rewr1 rewr2 phi by auto
finally show "σ ⊨ ψ" .
qed
next
case (induction cc φ' ψ f xs q φ cs)
note cc = induction(1)
note φ = induction(4)
note distinct = induction(6)
let ?xs = "map Var xs :: ('f,'v)term list"
let ?φ = "CC_impl (CC_rewr (Fun f ?xs) q # φ) ψ"
let ?P = "λ δ. normal_F_subst δ ⟶ δ ⊨ ?φ"
let ?UR = "UR (Fun f ?xs)"
from qrstep_mono[OF UR_sub subset_refl] have UR_R: "qrstep nfs Q ?UR ⊆ qrstep nfs Q R" .
hence step_UR: "⋀ p. p ∈ qrstep nfs Q ?UR ⟹ p ∈ qrstep nfs Q R" by auto
from rtrancl_mono[OF UR_R] have steps_UR: "⋀ p. p ∈ (qrstep nfs Q ?UR)^* ⟹ p ∈ (qrstep nfs Q R)^*" by auto
{
fix δ
assume delta: "normal_F_subst δ"
def dist ≡ "distance (qrstep nfs Q ?UR) (NF_terms Q)"
def SNrel1 ≡ "inv_image (restrict_SN (qrstep nfs Q R O {⊵}) (qrstep nfs Q R)) (λ δ. (Fun f ?xs) ⋅ δ)"
def SNrel2 ≡ "inv_image {(x,y). x > (y :: nat)} (λ δ. dist (Fun f ?xs ⋅ δ))"
def SNrel ≡ "if m then SNrel1 else SNrel2"
have SN_rel: "SN SNrel"
proof (cases m)
case True
have "SN SNrel1" unfolding SNrel1_def
proof (rule SN_inv_image[OF SN_subset[OF SN_restrict_SN_idemp]])
let ?R = "({⊳} ∪ qrstep nfs Q R)^+"
note d = restrict_SN_def
show "restrict_SN (qrstep nfs Q R O {⊵}) (qrstep nfs Q R) ⊆ restrict_SN ?R ?R" (is "?l ⊆ ?r")
proof
fix s t
assume "(s,t) ∈ ?l"
from this[unfolded d] have step: "(s,t) ∈ qrstep nfs Q R O {⊵}" and SN: "SN_on (qrstep nfs Q R) {s}" by auto
from step have "(s,t) ∈ qrstep nfs Q R ∪ qrstep nfs Q R O {⊳}" by auto
hence step: "(s,t) ∈ ?R" by regexp
with SN_on_trancl[OF SN_on_qrstep_imp_SN_on_supt_union_qrstep[OF SN]] show "(s,t) ∈ ?r" unfolding d by auto
qed
qed
thus ?thesis unfolding SNrel_def using True by simp
next
case False
have id: "{(x, y). y < x} = {(x, y). y > (x :: nat)}^-1" by auto
have "SN SNrel2" unfolding SNrel2_def id
by (rule SN_inv_image, rule wf_imp_SN, insert wf_less, simp)
thus ?thesis unfolding SNrel_def using False by simp
qed
have "δ ⊨ ?φ"
proof (induct δ rule: SN_induct[where P = ?P, rule_format, OF SN_rel])
show "normal_F_subst δ" by fact
next
fix δ
assume delta: "normal_F_subst δ"
assume IH: "⋀ τ. (δ, τ) ∈ SNrel ⟹ normal_F_subst τ ⟹ τ ⊨ ?φ"
show "δ ⊨ ?φ" unfolding cc_models.simps(2)
proof
assume conj: "Ball (set (CC_rewr (Fun f ?xs) q # φ)) (cc_models δ)"
hence rewr: "δ ⊨ CC_rewr (Fun f ?xs) q" and phi: "Ball (set φ) (cc_models δ)" by auto
from rewr have steps: "(Fun f ?xs ⋅ δ, q ⋅ δ) ∈ (qrstep nfs Q R)^*" and nf_q: "q ⋅ δ ∈ NFQ"
and SN: "m_SN (Fun f ?xs ⋅ δ)" by auto
{
fix u R'
assume u: "(Fun f ?xs ⋅ δ, u) ∈ qrstep nfs Q R'" and sub: "R' ⊆ R"
have "(Fun f ?xs ⋅ δ, u) ∉ nrqrstep nfs Q R'"
proof
assume "(Fun f ?xs ⋅ δ, u) ∈ nrqrstep nfs Q R'"
from nrqrstep_imp_arg_qrstep[OF this] obtain i where
"(δ (xs ! i), args u ! i) ∈ qrstep nfs Q R'" by auto
with qrstep_mono[OF sub, of Q "{}" nfs] have "(δ (xs ! i), args u ! i) ∈ rstep R" by auto
moreover from delta[unfolded normal_F_subst_def] have "δ (xs ! i) ∈ NF_trs R" by auto
ultimately show False by auto
qed
with u[unfolded qrstep_iff_rqrstep_or_nrqrstep]
have "(Fun f ?xs ⋅ δ, u) ∈ rqrstep nfs Q R'" by auto
} note rqrstep = this
have neq: "Fun f ?xs ⋅ δ ≠ q ⋅ δ"
proof
assume "Fun f ?xs ⋅ δ = q ⋅ δ"
hence "δ ∈ unifiers {(Fun f ?xs, q)}" unfolding unifiers_def by auto
with mgu_complete[OF induction(2)] show False by auto
qed
{
from rtranclD[OF steps, unfolded trancl_unfold_left] neq
obtain u where step: "(Fun f ?xs ⋅ δ, u) ∈ qrstep nfs Q R" by auto
from rqrstep[OF step subset_refl] have "(Fun f ?xs ⋅ δ, u) ∈ rqrstep nfs Q R" .
from rqrstepE[OF this] have NFQ: "⋀ u. u ⊲ Fun f ?xs ⋅ δ ⟹ u ∈ NFQ" by metis
{
fix x
assume "x ∈ vars_term (Fun f ?xs)"
hence "Var x ⊲ Fun f ?xs" by auto
from NFQ[OF supt_subst[OF this]] have "δ x ∈ NFQ" by auto
}
hence "δ ` vars_term (Fun f ?xs) ⊆ NFQ" by auto
from UR[OF this steps] have "(Fun f ?xs ⋅ δ, q ⋅ δ) ∈ (qrstep nfs Q ?UR)^*" .
} note steps = this
have "∃ u d. (Fun f ?xs ⋅ δ, u) ∈ qrstep nfs Q ?UR ∧ (u,q ⋅ δ) ∈ (qrstep nfs Q ?UR)^^d ∧ (m ∨ dist (Fun f ?xs ⋅ δ) = Suc d)"
proof (cases m)
case True
from rtranclD[OF steps, unfolded trancl_unfold_left] neq
obtain u where step: "(Fun f ?xs ⋅ δ, u) ∈ qrstep nfs Q ?UR" and steps: "(u,q ⋅ δ) ∈ (qrstep nfs Q ?UR)^*" by auto
from step True rtrancl_imp_relpow[OF steps] show ?thesis by auto
next
case False
from False induction(7) have CR: "CR (rstep ?UR)" by auto
from CR_imp_UNF_inn[OF NFQ UR_sub CR] have "UNF_r_q (qrstep nfs Q ?UR) NFQ" .
from distance_NF_UNF[OF subset_refl this nf_q steps]
have "(Fun f ?xs ⋅ δ, q ⋅ δ) ∈ qrstep nfs Q ?UR ^^ distance (qrstep nfs Q ?UR) NFQ (Fun f ?xs ⋅ δ)" .
from distance_Suc_relpow[OF nf_q this neq]
show ?thesis unfolding dist_def by auto
qed
then obtain u d where step: "(Fun f ?xs ⋅ δ, u) ∈ qrstep nfs Q ?UR"
and steps_d: "(u,q ⋅ δ) ∈ (qrstep nfs Q ?UR)^^d" and dist: "m ∨ dist (Fun f ?xs ⋅ δ) = Suc d" by auto
from relpow_imp_rtrancl[OF steps_d] have steps: "(u,q ⋅ δ) ∈ (qrstep nfs Q ?UR)^*" .
from SN step_preserves_SN_on[OF step_UR[OF step]] have SN_u: "m_SN u" unfolding m_SN_def by auto
from rqrstep[OF step UR_sub]
have "(Fun f ?xs ⋅ δ, u) ∈ rqrstep nfs Q ?UR" .
from rqrstepE[OF this] obtain l r σ'' where
nf: "∀u⊲l ⋅ σ''. u ∈ NFQ" and lr_U: "(l, r) ∈ ?UR" and fl: "Fun f ?xs ⋅ δ = l ⋅ σ''" and u: "u = r ⋅ σ''" and nfs: "NF_subst nfs (l, r) σ'' Q" .
from rqrstepI[OF nf _ fl u nfs] have rstep: "(Fun f ?xs ⋅ δ, u) ∈ rqrstep nfs Q {(l,r)}" by auto
from lr_U UR_sub have lr: "(l,r) ∈ R" by auto
from only_applicable_rules[OF nf] lr wwf UR_sub have vars: "vars_term r ⊆ vars_term l" unfolding wwf_qtrs_def by auto
from Rfun lr fl obtain ls where l: "l = Fun f ls" by (cases l, auto)
from fl l have id: "map δ xs = map (λ t. t ⋅ σ'') ls" by (simp add: comp_def)
from arg_cong[OF id, of length] have len: "length ls = length xs" by auto
from induction(5)[OF len[symmetric] lr[unfolded l]] obtain c ls' r' rs_ys_list
where eq: "(Fun f ls, r) =⇩v (Fun f ls', r')" and vars_cc: "vars_rule (Fun f ls', r') ∩ vars_cc ?φ = {}"
and c: "c ⟶cc cc_rule_constraint f ls' r' q xs φ ψ rs_ys_list" and c_cs: "c ∈ set cs"
and pre: "(∀(r, ys)∈set rs_ys_list. root r = Some (f,length xs) ∧ r' ⊵ r ∧ vars_term r' ∩ set ys = {} ∧ (∀fn∈funas_args_term r. ¬ defined R fn))" by auto
from rqrstep_rename_vars[of "{(Fun f ls,r)}" "{(Fun f ls',r')}" nfs Q] rstep[unfolded l] eq
have "(Fun f ?xs ⋅ δ, u) ∈ rqrstep nfs Q {(Fun f ls',r')}" by auto
from rqrstepE[OF this] obtain σ'' where
nf: "∀u⊲Fun f ls' ⋅ σ''. u ∈ NFQ" and fl: "Fun f ?xs ⋅ δ = Fun f ls' ⋅ σ''" and u: "u = r' ⋅ σ''" and nfs: "NF_subst nfs (Fun f ls', r') σ'' Q" by auto
from fl l have id: "map δ xs = map (λ t. t ⋅ σ'') ls'" by (simp add: comp_def)
from arg_cong[OF id, of length] have len: "length ls' = length xs" by auto
from eq_rule_mod_vars_var_cond[OF eq vars[unfolded l]] have vars: "vars_term r' ⊆ vars_term (Fun f ls')" .
def σ ≡ "mk_subst Var (zip xs ls')"
have "ls' = map id ls'" by simp
also have "... = map σ xs"
proof (rule nth_map_conv[OF len], intro allI impI)
fix i
assume i: "i < length ls'"
have "ls' ! i = σ (xs ! i)" unfolding σ_def using mk_subst_distinct[OF distinct len i[unfolded len]]
by simp
thus "id (ls' ! i) = σ (xs ! i)" by simp
qed
finally have ls: "ls' = map σ xs" .
from id[unfolded ls] have "map δ xs = map (λ x. σ x ⋅ σ'') xs" by auto
hence delta_sigma: "⋀ x. x ∈ set xs ⟹ δ x = σ x ⋅ σ''" by auto
def σ' ≡ "λ x. if x ∈ vars_term (Fun f ls') then σ'' x else δ x"
{
fix t :: "('f,'v)term"
assume sub: "vars_term t ⊆ vars_term (Fun f ls')"
have "t ⋅ σ'' = t ⋅ σ'" unfolding σ'_def
by (rule term_subst_eq, insert sub, auto)
} note conv1 = this
have delta_sigma': "⋀ x. x ∉ vars_term (Fun f ls') ⟹ δ x = (σ ∘⇩s σ') x"
proof -
fix x
assume x: "x ∉ vars_term (Fun f ls')"
have "σ x ⋅ σ' = δ x"
proof (cases "x ∈ set xs")
case True
then obtain i where x: "x = xs ! i" and i: "i < length xs" unfolding set_conv_nth by auto
have "σ x = ls' ! i" using arg_cong[OF ls, of "λ xs. xs ! i"] x i by auto
with i len have mem: "σ x ∈ set ls'" by auto
show ?thesis unfolding delta_sigma[OF True]
by (rule conv1[symmetric], insert mem, auto)
next
case False
from mk_subst_not_mem[OF this]
have "σ x = Var x" unfolding σ_def .
hence "σ x ⋅ σ' = σ' x" by simp
also have "... = δ x" unfolding σ'_def using x by simp
finally show ?thesis by simp
qed
thus "δ x = (σ ∘⇩s σ') x" unfolding subst_compose_def by auto
qed
def δ' ≡ "λ x. if x ∈ vars_term (Fun f ls') then (σ ∘⇩s σ') x else δ x"
have delta': "δ' = σ ∘⇩s σ'" unfolding δ'_def using delta_sigma' by auto
{
fix c :: "('f,'v)cond_constraint"
assume "vars_cc c ⊆ vars_cc ?φ"
with vars_cc have disj: "vars_cc c ∩ vars_term (Fun f ls') = {}" unfolding vars_rule_def by auto
have "δ ⊨ c = δ' ⊨ c"
by (rule cc_models_vars, insert disj δ'_def, auto)
} note delta_switch = this
from delta_switch phi have phi: "Ball (set φ) (cc_models δ')" unfolding φ by auto
{
fix x
have "funas_term (σ' x) ⊆ F ∧ σ' x ∈ NF_trs R"
proof (cases "x ∈ vars_term (Fun f ls')")
case True
hence sigma': "σ' x = σ'' x" unfolding σ'_def by simp
from True obtain l where l: "l ∈ set ls'" and x: "x ∈ vars_term l" by auto
from l[unfolded set_conv_nth] obtain i where i: "i < length ls'" and l: "l = ls' ! i" by auto
from arg_cong[OF id, of "λ ls. ls ! i"] i len l have "l ⋅ σ'' = δ (xs ! i)" by auto
with delta[unfolded normal_F_subst_def] have F: "funas_term (l ⋅ σ'') ⊆ F" and NF: "l ⋅ σ'' ∈ NF_trs R" by auto
with l x have F: "funas_term (σ' x) ⊆ F" unfolding sigma' funas_term_subst by auto
from x have "l ⊵ Var x" by auto
hence "l ⋅ σ'' ⊵ Var x ⋅ σ''" by auto
from NF_subterm[OF NF this] F
show ?thesis unfolding sigma' by auto
next
case False
hence "σ' x = δ x" unfolding σ'_def by simp
thus ?thesis using delta unfolding normal_F_subst_def by auto
qed
}
hence sigmaF: "normal_F_subst σ'" unfolding normal_F_subst_def by auto
have q: "q ⋅ δ = q ⋅ δ'"
by (rule term_subst_eq, unfold δ'_def, insert vars_cc, auto simp: vars_rule_def cc φ)
have u: "u = r' ⋅ σ'" unfolding u
proof (rule term_subst_eq)
fix x
assume "x ∈ vars_term r'"
with vars have "x ∈ vars_term (Fun f ls')" by auto
thus "σ'' x = σ' x" unfolding σ'_def by auto
qed
have sigma'_rewr: "σ' ⊨ CC_rewr r' (q ⋅ σ)"
unfolding cc_models.simps using steps_UR[OF steps] nf_q SN_u unfolding q delta' u by auto
from cc_validE[OF _ sigmaF] c_cs induction(8) have sigma'_c: "σ' ⊨ c" by auto
def vs ≡ "range_vars_impl (zip xs ls')"
have "range_vars σ ⊆ set vs" unfolding vs_def σ_def by simp
note cc_sigma = cc_models_subst[OF this]
note c = c[unfolded cc_rule_constraint_def Let_def σ_def[symmetric] vs_def[symmetric]]
have "Ball (set (cc_ih_prems f q xs φ ψ rs_ys_list)) (cc_models σ')" unfolding cc_models.simps
proof
fix c
assume "c ∈ set (cc_ih_prems f q xs φ ψ rs_ys_list)"
note c = this[unfolded cc_ih_prems_def Let_def]
from c obtain rr ys where c: "c = cc_bound ys
(CC_impl (CC_rewr rr (q ⋅ mk_subst Var (zip xs (args rr))) #
map (λc. c ⋅⇩cc (mk_subst Var (zip xs (args rr)), range_vars_impl (zip xs (args rr)))) φ)
(ψ ⋅⇩cc (mk_subst Var (zip xs (args rr)), range_vars_impl (zip xs (args rr)))))" and mem: "(rr,ys) ∈ set rs_ys_list" by force
from mem pre obtain rs where rr: "rr = Fun f rs" "args rr = rs" by (cases rr, auto)
note c = c[unfolded rr]
from mem pre rr have
lenrs: "length rs = length xs" and subt: "r' ⊵ Fun f rs" and rvars: "vars_term r' ∩ set ys = {}"
and ndef: "∀ fn ∈ funas_args_term (Fun f rs). ¬ defined R fn" by auto
from supteq_imp_vars_term_subset[OF subt] rvars have rs_vars: "vars_term (Fun f rs) ∩ set ys = {}" by auto
def vs' ≡ "range_vars_impl (zip xs rs)"
def μ ≡ "mk_subst Var (zip xs rs)"
from c vs'_def μ_def
have c: "c = cc_bound ys (CC_impl (CC_rewr (Fun f rs) (q ⋅ μ) # map (λc. c ⋅⇩cc (μ, vs')) φ) (ψ ⋅⇩cc (μ, vs')))" by simp
have "rs = map id rs" by simp
also have "... = map μ xs"
proof (rule nth_map_conv[OF lenrs], intro allI impI)
fix i
assume i: "i < length rs"
have "rs ! i = μ (xs ! i)" unfolding μ_def using mk_subst_distinct[OF distinct lenrs i[unfolded lenrs]]
by simp
thus "id (rs ! i) = μ (xs ! i)" by simp
qed
finally have "rs = map μ xs" .
hence rsmu: "Fun f rs = Fun f ?xs ⋅ μ" by simp
have rs_mu: "cc_bound ys (CC_impl (CC_rewr (Fun f rs) (q ⋅ μ) # map (λc. c ⋅⇩cc (μ, vs')) φ) (ψ ⋅⇩cc (μ, vs')))
= cc_bound ys ((CC_impl (CC_rewr (Fun f ?xs) q # φ) ψ) ⋅⇩cc (μ,vs'))" unfolding rsmu by simp
have "σ' ⊨ cc_bound ys (CC_impl (CC_rewr (Fun f rs) (q ⋅ μ) # map (λc. c ⋅⇩cc (μ, vs')) φ) (ψ ⋅⇩cc (μ, vs')))" unfolding rs_mu
proof (rule cc_models_boundI)
fix τ
assume tau_sigma: "⋀x. x ∉ set ys ⟹ τ x = σ' x"
and tau: "⋀x. x ∈ set ys ⟹ funas_term (τ x) ⊆ F ∧ τ x ∈ NF_trs R"
{
fix x
have "funas_term (τ x) ⊆ F ∧ τ x ∈ NF_trs R"
using tau_sigma[of x] tau[of x] sigmaF[unfolded normal_F_subst_def]
by (cases "x ∈ set ys", force+)
} note tauF = this
hence tau_F: "normal_F_subst τ" unfolding normal_F_subst_def by auto
have vs': "range_vars μ ⊆ set vs'" unfolding vs'_def μ_def by auto
show "τ ⊨ (CC_impl (CC_rewr (Fun f ?xs) q # φ) ψ) ⋅⇩cc (μ, vs')"
unfolding cc_models_subst[OF vs']
proof (rule IH)
{
fix x
let ?x = "μ x ⋅ τ"
have "funas_term ?x ⊆ F ∧ ?x ∈ NF_trs R"
proof (cases "x ∈ set xs")
case False
from mk_subst_not_mem[OF this]
have "μ x = Var x" unfolding μ_def .
with tauF[of x] show ?thesis by simp
next
case True
then obtain i where i: "i < length xs" and x: "x = xs ! i" unfolding set_conv_nth by auto
from mk_subst_distinct[OF distinct lenrs i[unfolded lenrs]]
have "μ x = rs ! i" unfolding μ_def x .
with i lenrs have mu: "μ x ∈ set rs" by auto
from eq_rule_mod_varsE[OF eq] obtain γ where r: "r = r' ⋅ γ" by auto
have "funas_term (μ x) ⊆ funas_term (Fun f rs)" using mu by auto
also have "… ⊆ funas_term r'" using subt by fastforce
also have "… ⊆ funas_term r" unfolding r funas_term_subst by auto
also have "… ⊆ F"
using lr RF unfolding funas_trs_def funas_rule_def [abs_def] by force
finally have F: "funas_term ?x ⊆ F" using tauF unfolding funas_term_subst by auto
have "(?x ∈ NF_trs R) = (?x ∈ NF (qrstep nfs {} R))" by simp
also have "…"
by (rule NF_subst_qrstep[OF _ _ Rfun], insert tauF ndef mu,
auto simp: applicable_rules_def applicable_rule_def funas_args_term_def)
finally show ?thesis using F by auto
qed
}
thus "normal_F_subst (μ ∘⇩s τ)" unfolding subst_compose_def normal_F_subst_def by auto
have "(Fun f ?xs ⋅ δ, u) ∈ qrstep nfs Q R" using step_UR[OF step] .
also have "u = r' ⋅ σ'" unfolding u ..
finally have step: "(Fun f ?xs ⋅ δ, Fun f rs ⋅ σ') ∈ qrstep nfs Q R O {⊵}" using supteq_subst[OF subt] by auto
have "Fun f rs ⋅ σ' = Fun f rs ⋅ τ"
by (rule term_subst_eq[OF tau_sigma[symmetric]], insert rs_vars, auto)
also have "Fun f rs ⋅ τ = Fun f ?xs ⋅ μ ⋅ τ" unfolding rsmu by simp
finally have id: "Fun f rs ⋅ σ' = Fun f ?xs ⋅ μ ∘⇩s τ" by simp
from step id have stepi: "(Fun f ?xs ⋅ δ, Fun f ?xs ⋅ μ ∘⇩s τ) ∈ qrstep nfs Q R O {⊵}" by simp
show "(δ, μ ∘⇩s τ) ∈ SNrel"
proof (cases m)
case True
with SN have "SN_on (qrstep nfs Q R) {Fun f ?xs ⋅ δ}" unfolding m_SN_def by auto
hence "(δ, μ ∘⇩s τ) ∈ SNrel1" using stepi unfolding SNrel1_def inv_image_def restrict_SN_def by force
thus ?thesis using True unfolding SNrel_def by auto
next
case False
with dist have dist: "dist (Fun f ?xs ⋅ δ) = Suc d" and SNrel: "SNrel = SNrel2" unfolding SNrel_def by auto
from steps_d[unfolded u] have steps_d: "(r' ⋅ σ', q ⋅ δ) ∈ qrstep nfs Q ?UR ^^ d" .
have "dist (Fun f ?xs ⋅ μ ∘⇩s τ) = dist (Fun f rs ⋅ σ')" unfolding id by simp
also have "… ≤ dist (r' ⋅ σ')" unfolding dist_def
by (rule distance_subterm[OF nf_q steps[unfolded u] supteq_subst[OF subt]])
also have "… ≤ d" unfolding dist_def
by (rule distance_least[OF nf_q steps_d])
also have "… < dist (Fun f ?xs ⋅ δ)" unfolding dist by simp
finally have dist: "dist (Fun f ?xs ⋅ μ ∘⇩s τ) < dist (Fun f ?xs ⋅ δ)" .
show ?thesis unfolding SNrel SNrel2_def inv_image_def
by (rule, unfold split, rule, unfold split, rule dist)
qed
qed
qed
thus "σ' ⊨ c" unfolding c .
qed
with sigma'_rewr cc_implies_substE[OF c sigma'_c]
have sigma'_impl: "σ' ⊨ (CC_impl φ ψ) ⋅⇩cc (σ,vs)" by auto
from sigma'_impl[unfolded cc_sigma]
have "δ' ⊨ CC_impl φ ψ" unfolding delta' by auto
with phi have "δ' ⊨ ψ" by auto
with delta_switch[of ψ] show "δ ⊨ ψ" by simp
qed
qed
hence "δ ⊨ CC_impl φ' ψ" using induction(3-4) by auto
}
thus ?case unfolding cc_valid_def normalize_cc[of _ cc] cc by auto
qed
qed
end
end