Theory Substitutions_Lambda_Free
theory Substitutions_Lambda_Free
imports "Lambda_Free_RPOs.Lambda_Free_RPOs" "HOL-Library.LaTeXsugar" "Well_Quasi_Orders.Minimal_Elements"
begin
no_notation (latex)
Cons ("_ ⋅/ _" [66,65] 65)
declare [[syntax_ambiguity_warning = false, names_short = true]]
section ‹Introduction›
text ‹
This theory is based on J. Blanchette's Formalization of Recursive Path Orders
for Lambda-Free Higher-Order Terms \cite{Lambda_Free_RPOs} which defines $\lambda$-free
higher-order terms.
›
subsection ‹Preliminary lemmas›
text‹
The following lemma and definitions would be worth adding in the theory
@{theory Lambda_Free_RPOs.Lambda_Free_Term}.
›
lemma sub_trans: ‹sub x y ⟹ sub y z ⟹ sub x z›
by (induction z arbitrary: x y, blast, elim sub_AppE; simp add: sub_arg sub_fun)
definition subterms :: ‹('s, 'v) tm ⇒ ('s, 'v) tm set› where
‹subterms t ≡ {u. sub u t}›
definition proper_subterms :: ‹('s, 'v) tm ⇒ ('s, 'v) tm set› where
‹proper_subterms t ≡ {u. proper_sub u t}›
text‹
The following lemmas are also helpful in the following and could be easily lifted
higher in the hierarchy of theories.
›
lemmas mult_Suc_left =
mult_Suc_right[unfolded add.commute[of m ‹m*n› for m n]]
lemma inject_nat_in_fset_ninj:
‹finite S ⟹ (range (f::nat⇒_) ⊆ S) ⟹ (∃ x y. x ≠ y ∧ f x = f y)›
apply (induction S rule: finite_induct, fast)
subgoal for x FS
using
finite_insert[of x FS]
infinite_UNIV_char_0 inj_on_finite[of f UNIV ‹{x} ∪ FS›]
unfolding inj_def by blast.
lemma wfPD: ‹wfP P ⟹ wfp_on P A›
by (simp add: wfP_eq_minimal wfp_on_iff_minimal)
lemma set_decr_chain_empty:
fixes u :: ‹nat ⇒ 'a set›
assumes pord: ‹⋀n. u n ≠ ∅ ⟹ u (n+1) ⊂ u n›
and fin: ‹⋀n. finite (u n)›
shows ‹∃ k. u k = ∅›
proof-
have ‹wfp_on (in_rel finite_psubset) (range u)›
using wf_finite_psubset wfPD wf_in_rel
by blast
with fin have wfpon: ‹wfp_on (⊂) (range u)›
unfolding finite_psubset_def in_rel_def wfp_on_def
by (auto iff: image_iff, metis)
then interpret minimal_element ‹(⊂)› ‹range u›
by (unfold_locales; simp add: po_on_def)
show ?thesis
using pord wf
unfolding wfp_on_def[simplified, unfolded Suc_eq_plus1]
using rangeI[of u]
by meson
qed
lemma distinct_in_fset:
‹finite E ⟹ card E = n ⟹ distinct xs ⟹ set xs ⊆ E ⟹ length xs ≤ n›
by (induction n, simp, metis card_mono distinct_card)
section ‹Substitutions›
text ‹
This section embeds substitutions in a proper type, lifting basic operations like
substitution application (i.e. \emph{substitution} as an operation on terms) and
composition.
›
subsection ‹Substitutions for terms›
text ‹
Substitutions in @{theory ‹Lambda_Free_RPOs.Lambda_Free_RPOs›}
\cite{Lambda_Free_RPOs} are not defined as a type, they are implicitly used
as functions from variables to terms.
However, not all functions from variables to terms are substitutions, which
motivates the introduction of a proper type \emph{subst} fitting the
specification of a substitution, namely that only finitely many variables are
not mapped to themselves.
›
abbreviation 𝒱 where ‹𝒱 ≡ Hd ∘ Var›
lemma inj_𝒱: ‹inj 𝒱›
by (intro injI, simp)
lemma fin_var_restr:‹finite (𝒱 ` E) ⟹ finite E›
using inj_𝒱 finite_imageI image_inv_f_f
by metis
definition is_subst :: ‹('v ⇒ ('s, 'v) tm) ⇒ bool› where
‹is_subst σ ≡ finite {t. is_Hd t ∧ is_Var (head t) ∧ subst σ t ≠ t}›
text‹
If type-checking on terms was enforced in @{term is_subst}, the above
definition could be expressed as follows in a more concise way:
@{term ‹is_subst σ ≡ finite {subst σ t ≠ t}›}
Without type-checking, the definition must range over variables and not over
terms since @{term ‹App x x›} is a valid term, even though it does not type check.
If $x\sigma = x$, then $(x(x))\sigma = x(x)$. This inductively allows infinitely many
fixpoints of the substitution @{term σ}.
With type-checking, the second definition would only add finitely many terms,
namely type-correct applied terms of the form @{term ‹(App y x)›} where @{term x}
and @{term y} are substitutable variables.
›
lemma subst_𝒱: ‹is_subst 𝒱›
unfolding is_subst_def
proof -
{
fix t::‹('s, 'v) tm›
assume asm: ‹is_Hd t› ‹is_Var (head t)›
define v where ‹v = var (head t)›
hence t_eq:‹t = Hd (Var v)›
by (simp add: asm(1) asm(2))
hence ‹subst 𝒱 t = t›
by simp
}
thus ‹finite {t. (is_Hd t ∧ is_Var (head t) ∧ subst (Hd ∘ Var) t ≠ t)}›
using not_finite_existsD by blast
qed
typedef ('s, 'v) subst = ‹{σ::('v ⇒ ('s, 'v) tm). is_subst σ}›
using subst_𝒱 by blast
setup_lifting type_definition_subst
lift_definition 𝒱' :: ‹('s, 'v) subst› is ‹𝒱›
using subst_𝒱 by blast
text ‹
Informally, @{term 𝒱} is almost the identity function since it casts variables
to themselves (as terms), but it has the type ‹'v ⇒ ('s, 'v) tm›. @{term 𝒱}
is thus lifted to @{term 𝒱'} that applies on substitutions. The fact that
@{term 𝒱'} leaves ground terms unchanged follows from the definition of @{term subst}
and is obtained by lifting. @{term 𝒱'} \emph{is} the identity substitution.
›
lift_definition
subst_app :: ‹('s, 'v) tm ⇒ ('s, 'v) subst ⇒ ('s, 'v) tm› (‹_⋅_› [56,55] 55) is
‹λ x σ. subst σ x›.
lemma sub_subst': ‹sub x t ⟹ sub (x⋅σ) (t⋅σ)›
by (simp add: subst_app.rep_eq sub_subst)
text ‹
Application for substitutions (i.e.\ \emph{substitution}) is lifted from the
function @{term subst} and denoted as usual in the literature with a post-fix
notation: @{term ‹subst σ x›} is denoted by @{term ‹x⋅σ›}.
›
lemma subst_alt_def:‹finite {t. (𝒱 t)⋅σ ≠ 𝒱 t}›
proof (transfer)
fix σ :: ‹'v ⇒ ('s, 'v) tm›
assume asm: ‹is_subst σ›
have
‹{t. is_Hd t ∧ is_Var (head t) ∧ subst σ t ≠ t} = 𝒱 ` {t. subst σ (𝒱 t) ≠ 𝒱 t}›
apply (standard; clarsimp)
subgoal for x
apply (cases x)
subgoal for hd by (cases hd; simp)
subgoal by simp
done.
then show ‹finite {t. subst σ (𝒱 t) ≠ 𝒱 t}›
using fin_var_restr asm unfolding is_subst_def
by simp
qed
text ‹
The lemma above provides an alternative definition for substitution. Yet, there is
a subtlety since Isabelle does not provide support for dependent types:
one shall understand this lemma as the meta-implication "if
@{term ‹σ::(_,_) subst›} is of type @{term subst} then the aforementioned set is
finite".
A true alternative definition should state an equivalence, however the converse
implication makes no sense in Isabelle.
›
lemma subst_eq_sub:‹sub s t ⟹ t⋅σ = t⋅θ ⟹ s⋅σ = s⋅θ›
by (transfer fixing: s t, induction t arbitrary: s; fastforce)
text ‹
Composition for substitutions is also lifted as follows.
›
lift_definition
rcomp :: ‹('s, 'v) subst ⇒ ('s, 'v) subst ⇒ ('s, 'v) subst›
(infixl ‹∘› 55) is ‹λ σ θ. subst θ ∘ (subst σ ∘ 𝒱)›
proof (transfer)
fix σ::‹'v ⇒ ('s, 'v) tm› and θ::‹'v ⇒ ('s, 'v) tm›
assume asm: ‹is_subst σ› ‹is_subst θ›
define S where ‹S ≡ {t. is_Hd t ∧ is_Var (head t) ∧ subst σ t ≠ t}›
define T where ‹T ≡ {t. is_Hd t ∧ is_Var (head t) ∧ subst θ t ≠ t}›
define TS where ‹TS ≡
{t. is_Hd t ∧ is_Var (head t) ∧ subst (λx. subst θ (subst σ (𝒱 x))) t ≠ t}›
note fin =
asm(1)[unfolded is_subst_def, folded S_def]
asm(2)[unfolded is_subst_def, folded T_def]
have TS_simp:
‹TS = {t. is_Hd t ∧ is_Var (head t) ∧ subst (subst θ ∘ (subst σ ∘ 𝒱)) t ≠ t}›
proof -
have eq:‹(λx. subst θ (subst σ (Hd (Var x)))) = subst θ ∘ (subst σ ∘ 𝒱)›
by (standard, simp)
then show ?thesis
by (simp add: TS_def[simplified eq])
qed
have ‹TS ⊆ S ∪ T›
unfolding S_def T_def TS_def
apply (intro subsetI, simp)
subgoal for t
apply (cases t; simp)
subgoal for x by (cases x; auto)
done
done
from finite_subset[OF this finite_UnI[OF fin], simplified TS_simp]
show ‹is_subst (subst θ ∘ (subst σ ∘ 𝒱))›
unfolding is_subst_def .
qed
lemma rcomp_subst_simp:
‹(x::('s, 'v) tm)⋅(σ ∘ θ) = (x⋅σ)⋅θ›
by (transfer fixing: x, induction x; simp add: hd.case_eq_if)
lift_definition
set_image_subst :: ‹('s, 'v) tm set ⇒ ('s, 'v) subst ⇒ ('s, 'v) tm set›
(infixl ‹⋅› 90) is ‹λ S σ. subst σ ` S› .
lemma set_image_subst_collect:
‹S⋅σ = {x⋅σ | x. x ∈ S}›
by (transfer, blast)
subsection ‹Substitutions as a monoid›
text ‹
First, we state two introduction lemmas for allowing extensional reasoning on
substitutions. The first one is on terms and the second one is for terms that are
variables.
›
lemma subst_ext_tmI:
fixes σ::‹('s, 'v) subst› and θ::‹('s, 'v) subst›
shows ‹∀ (x::('s, 'v) tm). (x⋅σ) = (x⋅θ) ⟹ σ = θ›
proof (transfer, rule ccontr)
fix σ::‹'v ⇒ ('s, 'v) tm› and θ::‹'v ⇒ ('s, 'v) tm›
assume asm:‹is_subst σ› ‹is_subst θ› ‹∀x. subst σ x = subst θ x› ‹σ ≠ θ›
from asm(4) obtain v where v_def:‹σ v ≠ θ v›
by fast
hence ‹subst σ (Hd (Var v)) ≠ subst θ (Hd (Var v))›
by simp
with asm(3) show False
by blast
qed
lemma subst_ext_tmI':
fixes σ::‹('s, 'v) subst› and θ::‹('s, 'v) subst›
shows ‹∀ x. (𝒱 x)⋅σ = (𝒱 x)⋅θ ⟹ σ = θ›
by (transfer, simp, blast)
lemmas subst_extI = subst_ext_tmI subst_ext_tmI'
text ‹
The three following lemmas state that @{term 𝒱'} is the neutral element for composition.
Although uniqueness follows from the definition of a neutral element, the proof
of this claim is given below.
›
lemma 𝒱'_id_tm [simp]:
fixes x::‹(_,_) tm›
shows ‹(x⋅𝒱') = x›
by (transfer fixing: x, induction x; simp add: hd.case_eq_if)
lemma 𝒱'_neutral_rcomp[simp]:
‹σ ∘ 𝒱' = σ›
‹𝒱' ∘ σ = σ›
by (intro subst_ext_tmI allI, simp add: rcomp_subst_simp)+
lemma unique_𝒱':
‹(⋀σ. σ ∘ η = σ) ⟹ η = 𝒱'›
‹(⋀σ. η ∘ σ = σ) ⟹ η = 𝒱'›
proof -
assume ‹σ ∘ η = σ› for σ
from 𝒱'_neutral_rcomp(2)[of η, symmetric, simplified this]
show ‹η = 𝒱'›.
next
assume ‹η ∘ σ = σ› for σ
from 𝒱'_neutral_rcomp(1)[of η, symmetric, simplified this]
show ‹η = 𝒱'›.
qed
lemma 𝒱'_iff:‹σ = 𝒱' ⟷ (∀ x. (𝒱 x)⋅σ = (𝒱 x))›
by (intro iffI; simp add: 𝒱'.rep_eq subst_app.rep_eq subst_ext_tmI')
lemma rcomp_assoc[simp]:
fixes σ::‹('s, 'v) subst›
and θ::‹('s, 'v) subst›
and γ::‹('s, 'v) subst›
shows ‹(σ ∘ θ) ∘ γ = σ ∘ (θ ∘ γ)›
by (intro subst_extI, simp add: rcomp_subst_simp)
text ‹
Knowing that the composition of substitutions @{term ‹(∘) :: (_,_) subst ⇒ _›}
is associative and has a neutral element @{term 𝒱'}, we may embed substitutions
in an algebraic structure with a monoid structure and enjoy Isabelle's lemmas on
monoids.
›
global_interpretation subst_monoid: monoid rcomp 𝒱'
by (unfold_locales; simp)
section ‹Acyclic substitutions›
subsection ‹Definitions and auxiliary lemmas›
text ‹
The iteration on substitutions is defined below and is followed by several
algebraic properties.
In order to show these properties, we give three different definitions for
iterated substitutions. In short, the first one is simply the iteration of
composition using Isabelle's @{term ‹(^^)›} operator. This can be understood as
follows:
\begin{align*}
\sigma^n \triangleq (\underset{n\ \text{times}}{\underbrace{\sigma \circ (\sigma \circ (\dots(\sigma}} \circ \mathcal{V}')\dots))
\end{align*}
Using properties from the monoid structure, this can be written as
\begin{align*}
\sigma^n \triangleq \underset{n\ \text{times}}{\underbrace{\sigma \circ \dots \circ \sigma}}
\end{align*}
The two other definitions are inductively defined using those two schemes:
\begin{align*}
\sigma^{n+1} &= \sigma \circ \sigma^n\\
\sigma^{n+1} &= \sigma^n \circ \sigma
\end{align*}
We prove that these three definitions are equivalent and use them in the proofs
of the properties that follow.
›
definition iter_rcomp :: ‹('s, 'v) subst ⇒ nat ⇒ ('s, 'v) subst›
(‹_⇗_⇖› [200, 0] 1000) where ‹σ⇗n⇖ ≡ ((∘) σ ^^ n) 𝒱'›
lemma iter_rcomp_Suc_right:‹σ⇗Suc n⇖ = σ⇗n⇖ ∘ σ›
unfolding iter_rcomp_def funpow_Suc_right comp_def 𝒱'_neutral_rcomp
by (induction n; simp)
lemma iter_rcomp_Suc_left:‹σ⇗Suc n⇖ = σ ∘ σ⇗n⇖›
unfolding iter_rcomp_def funpow_Suc_right comp_def 𝒱'_neutral_rcomp
by (induction n; simp)
fun iter_rcomp' :: ‹('s, 'v) subst ⇒ nat ⇒ ('s, 'v) subst›
where
‹iter_rcomp' σ 0 = 𝒱'›
| ‹iter_rcomp' σ (Suc n) = σ ∘ (iter_rcomp' σ n)›
lemma iter_rcomp_eq_iter_rcomp':‹σ⇗n⇖ = iter_rcomp' σ n›
by (induction n; simp add: iter_rcomp_def)
fun iter_rcomp'' :: ‹('s, 'v) subst ⇒ nat ⇒ ('s, 'v) subst›
where
‹iter_rcomp'' σ 0 = 𝒱'›
| ‹iter_rcomp'' σ (Suc n) = (iter_rcomp'' σ n) ∘ σ›
lemma iter_rcomp_eq_iter_rcomp'':‹σ⇗n⇖ = iter_rcomp'' σ n›
by (induction n, simp add: iter_rcomp_def, simp add: iter_rcomp_Suc_right)
lemmas iter_rcomp'_eq_iter_rcomp'' =
iter_rcomp_eq_iter_rcomp'[symmetric, simplified iter_rcomp_eq_iter_rcomp'']
text‹
The following lemmas show some algebraic properties on iterations of
substitutions, namely that for any @{term σ}, the function $n~\mapsto~\sigma^n$
i.e.\ @{term ‹iter_rcomp σ›} is a magma homomorphism between $(\mathbb{N}, +)$
and $(subst, \circ)$.
Since @{thm iter_rcomp_def[of σ 0, simplified]}, it is even a (commutative) monoid homomorphism.
›
lemma iter_comp_add_morphism: ‹(σ⇗n⇖) ∘ (σ⇗k⇖) = σ⇗n+k⇖›
unfolding iter_rcomp_eq_iter_rcomp' iter_rcomp'_eq_iter_rcomp''
by(induction k; simp add:
rcomp_assoc[of ‹iter_rcomp'' σ n› ‹iter_rcomp'' σ k› σ for k, symmetric])
lemmas iter_comp_com_add_morphism =
iter_comp_add_morphism[
of σ n k for σ n k,
simplified add.commute,
unfolded iter_comp_add_morphism[of σ k n, symmetric]]
text ‹
There is a similar property with multiplication, stated as follows:
\begin{align*}
\forall \sigma,n,k. (\sigma^n)^k = \sigma^{n\times k}
\end{align*}
This is shown by the following lemma. The next one shows commutativity.
›
lemma iter_comp_mult_morphism: ‹(σ⇗n⇖)⇗k⇖ = σ⇗n*k⇖›
unfolding iter_rcomp_eq_iter_rcomp' iter_rcomp'_eq_iter_rcomp''
by (induction k; simp only:
mult_Suc_left iter_comp_add_morphism[
symmetric,
unfolded iter_rcomp_eq_iter_rcomp' iter_rcomp'_eq_iter_rcomp'']
iter_rcomp''.simps mult_0_right)
lemmas iter_comp_com_mult_morphism =
iter_comp_mult_morphism[
of σ n k for σ k n,
simplified mult.commute,
unfolded iter_comp_mult_morphism[of σ k n, symmetric]]
text‹
Some simplification rules are added to the rules to help automatize subsequent
proofs.
›
lemma iter_rcomp_𝒱'[simp]: ‹𝒱'⇗n⇖ = 𝒱'›
unfolding iter_rcomp_eq_iter_rcomp'
by (induction n; simp)
lemma iter_rcomp_0[simp]: ‹σ⇗0⇖ = 𝒱'›
unfolding iter_rcomp_eq_iter_rcomp' by simp
lemma iter_rcomp_1[simp]: ‹σ⇗Suc 0⇖ = σ›
unfolding iter_rcomp_eq_iter_rcomp' by simp
definition dom :: ‹('s, 'v) subst ⇒ ('s, 'v) tm set› where
‹dom σ ≡ {𝒱 x | x. (𝒱 x)⋅σ ≠ 𝒱 x}›
definition ran :: ‹('s, 'v) subst ⇒ ('s, 'v) tm set› where
‹ran σ ≡ (λx. x⋅σ) ` dom σ›
lemma no_sub_in_dom_subst_eq: ‹(∀ x ∈ dom σ. ¬ sub x t) ⟹ t = t⋅σ›
unfolding dom_def
by (induction t)
((simp add: subst_app.rep_eq split: hd.split, metis sub_refl),
(simp add: subst_app.rep_eq, metis sub_arg sub_fun))
lemma subst_eq_on_domI:
‹(∀x. x ∈ dom σ ∨ x ∈ dom θ ⟶ x⋅σ = x⋅θ) ⟹ σ = θ›
by (intro subst_ext_tmI' allI)
(metis comp_apply no_sub_in_dom_subst_eq sub_HdE)
lemma subst_finite_dom:‹finite (dom σ)›
unfolding dom_def using subst_alt_def[of σ] by simp
lemma 𝒱'_emp_dom: ‹dom 𝒱' = ∅›
unfolding dom_def by simp
lemma var_not_in_dom [simp]: ‹𝒱 x ∉ dom σ ⟹ ((𝒱 x)⋅σ⇗n⇖) = 𝒱 x›
unfolding dom_def
by (induction n; simp add: iter_rcomp_Suc_left rcomp_subst_simp)
lemma ran_alt_def:‹ran σ = {(𝒱 x)⋅σ | x. (𝒱 x)⋅σ ≠ 𝒱 x}›
unfolding ran_def dom_def
by blast
definition is_ground_subst :: ‹('s, 'v) subst ⇒ bool› where
‹is_ground_subst σ ≡ (ground ` ran σ) = {True}›
lemma is_ground_subst_alt_def:
‹is_ground_subst σ ⟷ (ran σ ≠ ∅) ∧ (∀x. (𝒱 x)⋅σ ≠ 𝒱 x ⟶ ground ((𝒱 x)⋅σ))›
unfolding is_ground_subst_def ran_def dom_def
by (standard, auto)
lemma ground_subst_grounds:‹is_ground_subst σ ⟹ x ∈ dom σ ⟹ ground (x⋅σ)›
unfolding dom_def
by (induction x) (auto simp add: is_ground_subst_alt_def)
lemma iter_on_ground:‹ground (x⋅σ) ⟹ n > 0 ⟹ x⋅σ⇗n⇖ = x⋅σ›
using ground_imp_subst_iden
unfolding iter_rcomp_eq_iter_rcomp'
by (induction n, blast)
(simp add: rcomp_subst_simp, simp add: subst_app.rep_eq)
lemma true_subst_nempty_vars:
‹σ ≠ 𝒱 ⟹ {t. is_Hd t ∧ is_Var (head t) ∧ subst σ t ≠ t} ≠ {}›
proof -
assume ‹σ ≠ 𝒱›
then obtain t where ‹σ t ≠ 𝒱 t›
by blast
moreover have ‹is_Hd (𝒱 t)› ‹is_Var (head (𝒱 t))›
by simp+
ultimately show ?thesis
by fastforce
qed
lemma true_subst_nemp_im:‹ran σ = {} ⟹ σ = 𝒱'›
unfolding ran_def dom_def
by (transfer, auto simp add: is_subst_def dest: true_subst_nempty_vars)
lemma ground_subst_imp_no_var_mapped_on_var:
‹is_ground_subst σ ⟹ (∀x y. x ≠ y ⟶ (𝒱 x)⋅σ ≠ (𝒱 y))›
proof -
have ‹¬ (∀ x y. x ≠ y ⟶ (𝒱 x)⋅σ ≠ (𝒱 y)) ⟹ ¬ is_ground_subst σ›
proof -
assume ‹¬ (∀ x y. x ≠ y ⟶ (𝒱 x)⋅σ ≠ (𝒱 y))›
then obtain x y where xy_def:‹x ≠ y› ‹(𝒱 x)⋅σ = (𝒱 y)›
by blast
hence
‹(𝒱 x)⋅σ≠(𝒱 x)›
‹𝒱 x ∈ {x. is_Var (head x) ∧ x ⋅ σ ≠ x}›
‹¬ ground ((𝒱 x)⋅σ)›
by fastforce+
then show ‹¬ is_ground_subst σ›
unfolding is_ground_subst_def ran_def dom_def
by blast
qed
from contrapos_pp[
rotated,
of ‹∀ x y. x ≠ y ⟶ (𝒱 x)⋅σ ≠ (𝒱 y)› ‹is_ground_subst σ›,
OF this]
show ‹is_ground_subst σ ⟹ (∀ x y. x ≠ y ⟶ (𝒱 x)⋅σ ≠ (𝒱 y))›.
qed
lemma ran_𝒱'_empty:‹ran 𝒱' = ∅›
unfolding ran_def dom_def using 𝒱'_iff
by fast
lemma non_ground_𝒱': ‹¬ is_ground_subst 𝒱'›
using is_ground_subst_alt_def ran_𝒱'_empty by blast
subsection ‹Acyclicity›
text ‹
A substitution is said to be \emph{acyclic} if no variable @{term ‹x::(_,_) tm›}
in the domain of @{term σ} occurs as a subterm of @{term ‹(x::(_,_) tm)⋅σ⇗n⇖›}
for any @{term ‹n > 0›}.
›
definition is_acyclic :: ‹('s, 'v) subst ⇒ bool› where
‹is_acyclic σ ≡ (∀ x ∈ dom σ. ∀ n > 0. x ∉ subterms (x⋅σ⇗n⇖))›
lemma is_acyclicE:‹ is_acyclic σ ⟹ x ∈ dom σ ⟹ n > 0 ⟹ x ∉ subterms (x⋅σ⇗n⇖)›
unfolding is_acyclic_def by blast
lemma non_acyclic_𝒱': ‹is_acyclic 𝒱'›
using 𝒱'_emp_dom is_acyclic_def by fast
lemma acyclic_iter_dom_eq:‹is_acyclic σ ⟹ dom σ = dom σ⇗n⇖› if ‹n > 0› for n
using that unfolding dom_def is_acyclic_def subterms_def
by (induction n, fast, simp)
(smt (verit, ccfv_SIG)
Collect_cong
bot_nat_0.not_eq_extremum
𝒱'_id_tm
iter_rcomp_eq_iter_rcomp'
iter_rcomp'.simps
mem_Collect_eq
rcomp_subst_simp
sub_refl
zero_less_Suc)
lemma acyclic_iter: ‹is_acyclic σ ⟹ n > 0 ⟹ is_acyclic σ⇗n⇖›
unfolding is_acyclic_def subterms_def
by (auto simp add: iter_comp_mult_morphism dom_def dest: CollectD,
use var_not_in_dom[unfolded dom_def] in fastforce)
subsection ‹Fixed-point substitution›
text ‹
We define the fixed-point substitution of a substitution @{term σ} as the substitution @{term ‹σ⇗i⇖›} where $\displaystyle{i = \inf \{k \in \mathbb{N} \mid \sigma^k = \sigma^{k+1}\}}$.
›
definition fp_subst :: ‹('s, 'v) subst ⇒ ('s, 'v) subst› (‹_⇧⋆› 1000) where
‹σ⇧⋆ ≡ iter_rcomp σ (LEAST n . σ⇗n⇖ = σ⇗n+1⇖)›
lemma ground_subst_is_fp:‹is_ground_subst σ ⟹ σ⇧⋆ = σ›
proof -
assume asm:‹is_ground_subst σ›
have eq:‹σ⇗1⇖ = σ⇗2⇖›
apply (simp only: one_add_one[symmetric],
simp, intro subst_ext_tmI' allI, simp)
subgoal for x
unfolding iter_rcomp_eq_iter_rcomp'
by (cases ‹𝒱 x ∈ dom σ›,
simp add: rcomp_subst_simp,
metis
ground_subst_grounds[OF asm, THEN ground_imp_subst_iden]
subst_app.rep_eq,
simp add: dom_def rcomp_subst_simp).
note least_le1=Least_le[of ‹λn. σ⇗n⇖ = σ⇗n + 1⇖› 1, unfolded nat_1_add_1, OF this]
have neq:‹σ⇗0⇖ ≠ σ⇗1⇖›
using asm non_ground_𝒱'
unfolding iter_rcomp_eq_iter_rcomp'
by auto
have ‹(LEAST n. σ⇗n⇖ = σ⇗n + 1⇖) ≠ 0›
proof (rule ccontr)
assume ‹¬ (LEAST n. σ⇗n⇖ = σ⇗n + 1⇖) ≠ 0›
hence ‹(LEAST n. σ⇗n⇖ = σ⇗n + 1⇖) = 0› by blast
from
LeastI[of ‹λn. σ⇗n⇖ = σ⇗n + 1⇖› 1, simplified one_add_one, OF eq,
simplified add_0 this]
neq
show False by blast
qed
moreover have ‹(LEAST x. σ⇗x⇖ = σ⇗x + 1⇖) = 0 ∨ (LEAST x. σ⇗x⇖ = σ⇗x + 1⇖) = 1›
using least_le1 by linarith
ultimately have ‹(LEAST n. σ⇗n⇖ = σ⇗n + 1⇖) = 1›
by sat
then show ‹σ⇧⋆ = σ›
unfolding fp_subst_def iter_rcomp_eq_iter_rcomp'
by simp
qed
text ‹
In the following, we prove that fixed-point substitutions are well-defined for
acyclic substitutions. To help visualise how the proofs are carried out, for any
terms @{term x} and @{term y} and any substitution @{term σ}, we denote the fact
that ‹x› is substituted by ‹y› after one application of ‹σ›, i.e.\ that @{term ‹sub y (x⋅σ)›}, by ‹x →⇩σ y›.
\begin{remark}
In fact, automata could be used to model substitutions with variables in the domain as the initial states and variables outside of the domain and constants as final
states. The transitions would be given by the successive substitutions.
Acyclic substitutions would be represented by a DAG.
\end{remark}
›
lemma dom_sub_subst: ‹x ∈ dom σ ⟹ sub x (t⋅σ) ⟹ ∃y ∈ dom σ. sub x (y⋅σ)›
apply (induction t)
subgoal for t0
apply (cases t0)
unfolding dom_def apply fastforce
by (metis (no_types, lifting) hd.set(4) tm.set(3) ground_imp_subst_iden subst_app.rep_eq sub_HdE)
subgoal for t1 t2
by (simp add: dom_def) (metis subst.simps(2) tm.distinct(1) subst_app.rep_eq sub_AppE)
done
lemma dom_sub_subst_contrapos:
‹x ∈ dom σ ⟹ ∀z ∈ dom σ. ¬ sub x (z⋅σ) ⟹ ∀t. ¬ sub x (t⋅σ)›
using dom_sub_subst by blast
lemma dom_sub_subst_iter:
‹x ∈ dom σ ⟹ ∀z ∈ dom σ. ¬ sub x (z⋅σ⇗n⇖) ⟹ ¬ sub x (t⋅σ⇗n⇖)›
by (induction n arbitrary: x σ,
simp, use sub_refl in blast,
smt (verit, ccfv_threshold)
One_nat_def
𝒱'_id_tm
𝒱'_neutral_rcomp(1)
dom_def
dom_sub_subst
iter_comp_add_morphism
iter_rcomp_Suc_right
iter_rcomp_eq_iter_rcomp'
iter_rcomp'.simps(1)
mem_Collect_eq
plus_1_eq_Suc
rcomp_subst_simp
sub_refl
subst_eq_sub)
lemma
assumes ‹x ∈ dom σ› ‹∀y ∈ dom σ. sub y t ⟶ ¬ sub x (y⋅σ)›
shows not_sub_subst_if:‹¬ sub x (t⋅σ)›
using assms
by (induction t)
((smt (verit, ccfv_threshold)
hd.case_eq_if
subst.simps(1)
𝒱'_id_tm
dom_def
𝒱'.rep_eq
subst_app.rep_eq
mem_Collect_eq
sub_HdE
sub_refl),
(smt (verit, ccfv_threshold)
subst.simps(2)
comp_apply
dom_def
subst_app.rep_eq
mem_Collect_eq
sub_Hd_AppE
sub_arg
sub_fun))
lemma dom_sub_subst_iter_Suc:
‹x ∈ dom σ ⟹ sub x (t⋅σ⇗n+1⇖) ⟹
∃y z. y ∈ dom σ ∧ z ∈ dom σ ∧ sub x (z⋅σ) ∧ sub z (y⋅σ⇗n⇖)›
proof (induction n arbitrary: x t)
case 0
then show ?case
unfolding add_0 One_nat_def iter_rcomp_Suc_right rcomp_subst_simp
iter_rcomp_0 𝒱'_neutral_rcomp 𝒱'_id_tm
using dom_sub_subst sub_refl by blast
next
case (Suc n)
then obtain t' where t'_def: ‹sub t' (t⋅σ⇗n+1⇖) › ‹sub x (t'⋅σ)›
by (metis Suc_eq_plus1 iter_rcomp_Suc_right rcomp_subst_simp sub_refl)
have ‹∃w ∈ dom σ. sub w t' ∧ sub x (w⋅σ)›
using not_sub_subst_if Suc.prems(1) t'_def(2) by blast
then obtain w where w_def: ‹w ∈ dom σ› ‹sub w t'› ‹sub x (w⋅σ)›
by blast
then obtain y where ‹y ∈ dom σ› ‹sub w (y⋅σ⇗n+1⇖)›
apply (fold Suc_eq_plus1, unfold iter_rcomp_Suc_right rcomp_subst_simp)
using sub_subst' sub_trans Suc.IH t'_def by meson
with w_def show ?case
by auto
qed
lemma sub_Suc_n_sub_n_sub:
‹(∃ x ∈ dom σ. sub z (x⋅σ⇗n+1⇖)) ⟷
(∃ x y. x ∈ dom σ ∧ y ∈ dom σ ∧ sub z (y⋅σ) ∧ sub y (x⋅σ⇗n⇖))› if ‹z ∈ dom σ›
using that
proof (intro iffI)
show ‹z ∈ dom σ ⟹ ∃x∈dom σ. sub z (x⋅σ⇗n + 1⇖) ⟹
∃x y. x ∈ dom σ ∧ y ∈ dom σ ∧ sub z (y⋅σ) ∧ sub y (x⋅σ⇗n⇖)›
proof-
assume ‹∃x∈dom σ. sub z (x⋅σ⇗n + 1⇖)› ‹z ∈ dom σ›
then obtain x where ‹x∈dom σ› ‹sub z (x⋅σ⇗n+1⇖)›
by blast
then obtain y where ‹y ∈ dom σ› ‹sub z (y⋅σ)› ‹sub y (x⋅σ⇗n⇖)›
by (metis Suc_eq_plus1 ‹z ∈ dom σ› iter_rcomp_Suc_right
not_sub_subst_if rcomp_subst_simp)
then show ‹∃x y. x ∈ dom σ ∧ y ∈ dom σ ∧ sub z (y⋅σ) ∧ sub y (x⋅σ⇗n⇖)›
using ‹x ∈ dom σ› by blast
qed
show ‹z ∈ dom σ ⟹
∃x y. x ∈ dom σ ∧ y ∈ dom σ ∧ sub z (y⋅σ) ∧ sub y (x⋅σ⇗n⇖) ⟹
∃x∈dom σ. sub z (x⋅σ⇗n + 1⇖)›
proof -
assume ‹∃ x y. x ∈ dom σ ∧ y ∈ dom σ ∧ sub z (y⋅σ) ∧ sub y (x⋅σ⇗n⇖)›
then obtain x y where xy_def:
‹x ∈ dom σ› ‹y ∈ dom σ› ‹sub z (y⋅σ)› ‹sub y (x⋅σ⇗n⇖)›
by blast
then have ‹sub (y⋅σ) (x⋅σ⇗n+1⇖)›
unfolding Suc_eq_plus1[symmetric] iter_rcomp_Suc_right rcomp_subst_simp
using sub_subst' by blast
with xy_def(3) have ‹sub z (x⋅σ⇗n+1⇖)›
using sub_trans by blast
with xy_def(1) show ‹∃x∈dom σ. sub z (x⋅σ⇗n + 1⇖)›
by fast
qed
qed
text‹
The following theorem is the main result of this theory and states that for acyclic
substitutions, the fixed-point substitution exists and is well defined. The main
idea of the proof is to define a non-negative quantity and show that successively
applying the substitution makes it decrease.
For any such iteration $n$, we define the set of variables that will be
substituted by the next iteration of the substitution and denote it by $S_n$.
Formally, $S_n$ is defined as follows:
\begin{equation*}
S_n := \{z \in \text{dom}\ \sigma \mid \exists x \in \text{dom}\ \sigma.\ x \rightarrow_{\sigma}^n z\}
\end{equation*}
There is a clear recurrence relation between $S_{n+1}$ and $S_n$, namely that
the variables in $S_{n+1}$ are exactly the variables in $S_n$ that are not sources
in $S_n$, i.e.\ that have a predecessor -- for the subterm relation -- in $S_n$.
This is formalized as follows:
\begin{equation*}
S_{n+1} = S_n - \{z \in S_n \mid \forall x \in S_n.\ x \not\rightarrow_\sigma z \}
\end{equation*}
This implies that the sequence $(S_n)_{n \in \mathbb{N}}$ is strictly monotone
for inclusion.
Since it is bounded and has its values in finite sets, it is convergent and there
is a rank $k$ from which it is constant and equal to the infimum of the range,
the empty set.
›
theorem fp_subst: ‹is_acyclic σ ⟹ ∃n. σ⇗n⇖ = σ⇗n+1⇖›
proof -
assume acyc:‹is_acyclic σ›
define S where ‹S ≡ λ n. ⋃(subterms ` ran σ⇗n⇖) ∩ dom σ›
have S_alt_def: ‹S n = {z ∈ dom σ. ∃x ∈ dom σ. sub z (x⋅σ⇗n⇖)}› if ‹n > 0› for n
unfolding S_def ran_def subterms_def
acyclic_iter_dom_eq[OF that acyc, symmetric]
by blast
have S_σ_unfold:
‹S n ⋅ σ = {x⋅σ | x. x ∈ dom σ ∧ (∃y∈dom σ. sub x (y⋅σ⇗n⇖))}› if ‹n > 0› for n
unfolding set_image_subst_collect[of ‹S n›, unfolded S_def]
S_def subterms_def
unfolding ran_def acyclic_iter_dom_eq[OF that acyc, symmetric]
by blast
have sources_charac:
‹n > 0 ⟹ S (n+1) = S n - {z ∈ S n. ∀x ∈ S n. ¬ sub z (x⋅σ)}› for n
proof (intro subset_antisym subsetI)
fix z assume ‹n > 0›
show ‹z ∈ S (n + 1) ⟹ z ∈ S n - {z ∈ S n. ∀x∈S n. ¬ sub z (x⋅σ)}›
proof-
assume ‹z ∈ S (n + 1)›
then obtain x where x_def: ‹x ∈ dom σ› ‹sub z (x⋅σ⇗n+1⇖)›
unfolding S_alt_def[OF zero_less_Suc[of n, unfolded Suc_eq_plus1]]
by blast
then have ‹z ∈ S n›
unfolding S_def ran_def
acyclic_iter_dom_eq[OF ‹n > 0› acyc, symmetric]
subterms_def
by (simp, metis IntE S_def Suc_eq_plus1 ‹z ∈ S (n + 1)›
dom_sub_subst_iter iter_rcomp_Suc_left rcomp_subst_simp)
moreover have ‹∃x∈S n. sub z (x⋅σ)›
using
S_alt_def[OF ‹n > 0›]
dom_sub_subst_iter_Suc[of z σ]
x_def(2) ‹z ∈ S n›
by fast
ultimately show ‹z ∈ S n - {z ∈ S n. ∀x∈S n. ¬ sub z (x⋅σ)}›
by blast
qed
show ‹z ∈ S n - {z ∈ S n. ∀x∈S n. ¬ sub z (x⋅σ)} ⟹ z ∈ S (n + 1)›
proof-
assume ‹z ∈ S n - {z ∈ S n. ∀x∈S n. ¬ sub z (x⋅σ)}›
hence ‹z ∈ S n› ‹∃y∈S n. sub z (y⋅σ)›
by blast+
then obtain x y w where
‹x ∈ dom σ› ‹sub z (x⋅σ⇗n⇖)›
‹y ∈ dom σ› ‹w ∈ dom σ› ‹sub z (y⋅σ)› ‹sub y (w⋅σ⇗n⇖)›
unfolding S_def subterms_def ran_def
acyclic_iter_dom_eq[OF ‹n > 0› acyc, symmetric]
by blast
show ‹z ∈ S (n+1)›
unfolding S_alt_def[OF zero_less_Suc[of n], unfolded Suc_eq_plus1]
apply (simp, intro conjI, use ‹z ∈ S n›[unfolded S_def] in simp)
using sub_trans[OF ‹sub z (y⋅σ)›
sub_subst'[OF ‹sub y (w⋅σ⇗n⇖)›, of σ]] ‹w ∈ dom σ›
unfolding iter_rcomp_Suc_right rcomp_subst_simp
by (intro bexI[of _ w])
qed
qed
have fin_Sn: ‹finite (S n)› for n
unfolding S_def using subst_finite_dom
by blast
have decr: ‹S n ≠ ∅ ⟹ S (n+1) ⊂ S n› for n
proof
show ‹S n ≠ ∅ ⟹ S (n+1) ⊆ S n›
proof (cases ‹n > 0›)
case True
assume ‹S n ≠ ∅›
show ?thesis
proof (intro subsetI, rule ccontr)
fix x assume ‹x ∈ S(n+1)› ‹x ∉ S n›
from this(1)[
unfolded S_alt_def[OF zero_less_Suc[of n],
unfolded Suc_eq_plus1],
simplified,
unfolded Suc_eq_plus1]
obtain y where ‹x ∈ dom σ› ‹y ∈ dom σ› ‹sub x (y⋅σ⇗n+1⇖)›
by blast
with ‹x ∉ S n›[unfolded S_alt_def[OF True], simplified]
have ‹∀z∈dom σ. ¬ sub x (z⋅σ⇗n⇖)›
by blast
from
dom_sub_subst_iter[OF ‹x ∈ dom σ› this, of ‹y⋅σ›]
show False
using ‹sub x (y⋅σ⇗n+1⇖)›[
folded Suc_eq_plus1,
unfolded iter_rcomp_Suc_left rcomp_subst_simp] ..
qed
next
case False
assume ‹S n ≠ ∅›
moreover have ‹S 0 = ∅›
unfolding S_def iter_rcomp_eq_iter_rcomp'
by (simp add: ran_𝒱'_empty)
ultimately show ?thesis
using False by simp
qed
show ‹S n ≠ ∅ ⟹ S (n+1) ≠ S n›
proof (cases n)
case (Suc m)
hence ‹n > 0› by simp
assume ‹S n ≠ ∅›
have ‹{z ∈ S n. ∀x ∈ S n. ¬ sub z (x⋅σ)} ≠ ∅›
proof (rule ccontr)
assume ‹¬ {z ∈ S n. ∀x∈S n. ¬ sub z (x⋅σ)} ≠ {}›
hence ch: ‹∀x. x ∈ S n ⟶ (∃y ∈ S n. sub x (y⋅σ))›
by simp
define E where ‹E ≡ λx. {y ∈ S n. sub x (y⋅σ)}›
have E_nemp: ‹x ∈ S n ⟹ E x ≠ ∅› for x
unfolding E_def using ch by fast
have ‹x ∈ S n ⟹ x ∉ E x› for x
proof (rule ccontr)
assume a: ‹x ∈ S n› ‹¬ x ∉ E x›
from this(1) have ‹x ∈ dom σ›
unfolding S_def by fast
with conjunct2[OF a(2)[simplified, unfolded E_def, simplified]]
acyc[
unfolded is_acyclic_def subterms_def,
simplified,
rule_format,
OF this zero_less_Suc[of 0],
unfolded iter_rcomp_Suc_right,
simplified]
show False
by satx
qed
with ch ‹S n ≠ ∅› obtain x y where ‹x ∈ S n› ‹y ∈ S n› ‹sub y (x⋅σ)›
by blast
with acyc have ‹y ≠ x›
unfolding S_def is_acyclic_def subterms_def
by (metis IntE One_nat_def 𝒱'_id_tm iter_rcomp_0
iter_rcomp_Suc_left mem_Collect_eq rcomp_subst_simp zero_less_one)
let ?C = ‹card (S n)›
have incl: ‹E v ⊆ S n› for v
unfolding E_def by blast
have ‹k > 0 ⟹
∃ seq. k = length seq ∧
seq!0 ∈ S n ∧
(∀ m < length seq - 1. seq!(m+1) ∈ E (seq!m)) ∧
distinct seq›
for k
proof (induction k rule: nat_induct_non_zero)
case (Suc k)
then obtain seq where seq_def: ‹k = length seq› ‹seq!0 ∈ S n›
‹(∀ m < k-1. seq!(m+1) ∈ E (seq!m))› ‹distinct seq›
by blast
hence ‹l < k ⟹ seq!l ∈ S n› for l
unfolding E_def
by (metis (no_types, lifting) CollectD Suc_eq_plus1
less_Suc_eq less_Suc_eq_0_disj less_diff_conv)
with seq_def obtain v where v_def: ‹v ∈ E (seq!(k-1))›
using E_nemp Suc.hyps
by (metis Suc_eq_plus1 Suc_pred' all_not_in_conv less_add_one)
have seq_sub:
‹i < length seq ⟹ j ≤ i ⟹ sub (seq!j) ((seq!i)⋅σ⇗i-j⇖)› for i j
proof (induction i arbitrary: j)
case (Suc l)
with seq_def have ‹seq!(Suc l) ∈ E (seq!l)›
by simp
hence ‹sub (seq!l) ((seq!(Suc l))⋅σ)›
unfolding E_def by blast
with Suc show ?case
by (smt (verit, ccfv_SIG)
cancel_comm_monoid_add_class.diff_cancel
bot_nat_0.not_eq_extremum
Suc_diff_Suc
Suc_lessD
𝒱'_id_tm
diff_Suc_Suc
diff_diff_cancel
iter_rcomp_0
iter_rcomp_Suc_left
le_Suc_eq
rcomp_subst_simp
sub_refl
sub_subst'
sub_trans
zero_less_diff)
qed (simp add: sub_refl)
define seq' where ‹seq' ≡ seq @ [v]›
hence ‹sub (seq!(k-1)) (v⋅σ)›
using v_def unfolding E_def
by blast
have ‹v ∈ dom σ›
using incl v_def
unfolding E_def S_def
by fast
have ‹v ∉ set seq›
proof
assume ‹v ∈ set seq›
then obtain j where ‹j < k› ‹v = seq!j›
unfolding in_set_conv_nth seq_def(1) by fast
with seq_sub[of ‹k-1› j, folded seq_def(1) this(2)] Suc.hyps
have ‹sub v (seq!(k-1)⋅σ⇗k-1-j⇖)›
by simp
from sub_trans[OF
this
sub_subst'[OF ‹sub (seq!(k-1)) (v⋅σ)›, of ‹σ⇗k-1-j⇖›,
folded rcomp_subst_simp iter_rcomp_Suc_left]]
show False
using acyc ‹v ∈ dom σ›
unfolding is_acyclic_def subterms_def
by blast
qed
show ?case
by (intro exI[of _ seq'] conjI, unfold seq'_def,
simp add: seq_def(1),
simp add:
seq_def(2)
nth_append[
of seq ‹[v]› 0,
folded seq_def(1),
unfolded if_split,
simplified]
Suc.hyps,
intro allI,
metis
butlast_snoc
diff_add_inverse2
length_append_singleton
length_butlast
less_Suc_eq
less_diff_conv
nth_append
nth_append_length
seq_def(1,3)
v_def,
simp add: ‹v ∉ set seq› seq_def(4))
qed (intro exI[of _ ‹[x]›] conjI, (simp add: ‹x ∈ S n›)+)
then obtain seq where seq_def:
‹?C + 1 = length seq› ‹seq!0 ∈ S n› ‹distinct seq›
‹(∀ m < length seq - 1. seq!(m+1) ∈ E (seq!m))›
by auto
have ‹set seq ⊆ S n›
proof
fix x assume ‹x ∈ set seq›
then obtain i where ‹seq!i = x› ‹i < length seq›
by (metis in_set_conv_nth)
then show ‹x ∈ S n›
by (cases i, use seq_def(2) in simp)
(metis seq_def(4) One_nat_def Suc_eq_plus1 in_mono incl less_diff_conv)
qed
from
distinct_in_fset[OF fin_Sn, of n ?C, simplified, OF seq_def(3) this]
seq_def(1)
show False
by simp
qed
thus ?thesis
unfolding sources_charac[OF ‹n > 0›]
by blast
next
case 0 assume ‹S n ≠ ∅›
moreover have ‹S 0 = ∅›
unfolding S_def iter_rcomp_0 ran_𝒱'_empty
by blast
ultimately show ?thesis
using 0 by simp
qed
qed
have subset_dom: ‹n > 0 ⟹ S n ⊆ dom σ› for n
by (induction n) (simp add: S_def)+
have ‹finite (S n)› for n
by (cases n)
(simp add:
S_def subst_finite_dom
subset_dom[THEN finite_subset[OF _ subst_finite_dom[of σ]]])+
moreover have ‹S 0 = ∅›
unfolding S_def iter_rcomp_eq_iter_rcomp'
by (simp add: ran_𝒱'_empty)
ultimately obtain k where ‹k > 0› ‹S k = ∅›
using set_decr_chain_empty[where u=‹λn. S (Suc n)›] decr
by auto
from this(2)[unfolded S_def subterms_def ran_def
acyclic_iter_dom_eq[OF this(1) acyc, symmetric], simplified]
have f: ‹{y. y ∈ dom σ ∧ (∃x∈dom σ. sub y (x⋅σ⇗k⇖))} = ∅›
by blast
then have ‹σ⇗k⇖ = σ⇗k+1⇖›
by (intro subst_eq_on_domI allI impI)
((simp add:
acyclic_iter_dom_eq[OF ‹k > 0› acyc, symmetric]
acyclic_iter_dom_eq[OF zero_less_Suc[of k] acyc, symmetric]),
unfold iter_rcomp_Suc_right rcomp_subst_simp,
simp add: no_sub_in_dom_subst_eq)
then show ?thesis
by (intro exI[of _ k])
qed
lemma fp_subst_comp_stable: ‹is_acyclic σ ⟹ (σ⇧⋆) ∘ (σ⇧⋆) = σ⇧⋆›
proof-
assume ‹is_acyclic σ›
with fp_subst obtain m where m_def: ‹σ⇗m⇖ = σ⇗m+1⇖›
by blast
define n where ‹n ≡ LEAST n. σ⇗n⇖ = σ⇗n+1⇖›
have eq: ‹σ⇧⋆ = σ⇗n⇖›
unfolding fp_subst_def n_def..
from m_def have ‹σ⇗n⇖ = σ⇗n+1⇖›
unfolding n_def
by (intro LeastI[of ‹λn. σ⇗n⇖ = σ⇗n+1⇖› m])
hence ‹σ⇗n⇖ = σ⇗n+k⇖› for k
proof (induction k)
case (Suc k)
show ?case
unfolding add_Suc_right iter_rcomp_Suc_right
Suc.IH[OF Suc.prems, symmetric]
unfolding iter_rcomp_Suc_right[symmetric] Suc_eq_plus1
using Suc.prems.
qed simp
then show ?thesis
unfolding eq iter_comp_com_add_morphism
by (induction n) presburger+
qed
lemma fp_subst_stable_iter: ‹is_acyclic σ ⟹ n > 0 ⟹ (σ⇧⋆)⇗n⇖ = σ⇧⋆›
by (induction n, simp,
unfold iter_rcomp_Suc_right,
use fp_subst_comp_stable in fastforce)
lemma fp_subst_stable_fp: ‹is_acyclic σ ⟹ (σ⇧⋆)⇧⋆ = σ⇧⋆›
proof -
assume ‹is_acyclic σ›
define m where ‹m ≡ LEAST n. (σ⇧⋆)⇗n⇖ = (σ⇧⋆)⇗n+1⇖›
show ?thesis
unfolding fp_subst_def[of ‹σ⇧⋆›, folded m_def]
using fp_subst_stable_iter[OF ‹is_acyclic σ›]
by (metis (mono_tags, lifting) LeastI_ex Suc_eq_plus1 m_def zero_less_Suc)
qed
end