theory Simple_Termination
imports
Well_Quasi_Orders.Kruskal
"HOL-Cardinals.Wellorder_Extension"
"../Orderings/Embedding_Trs"
begin
inductive_set gterms for F
where
Fun [intro]: "(f, n) ∈ F ⟹ length ts = n ⟹ ∀t ∈ set ts. t ∈ gterms F ⟹ Fun f ts ∈ gterms F"
interpretation kruskal_term: kruskal_tree F Fun "the ∘ root" args "gterms F" for F
by standard (auto simp: size_simp1 elim: gterms.cases)
lemma kruskal_emb_imp_embeq:
assumes "kruskal_term.emb F P¯¯⇧=⇧= s t"
shows "(t, s) ∈ embeq F P"
using assms
proof (induct)
case (arg f m ts t s)
then show ?case by (auto dest: embeq_arg embeq_trans)
next
case (list_emb f m g n ss ts)
then have "list_emb (λs t. (t, s) ∈ embeq F P) ss ts" by (auto dest: list_emb_conjunct2)
from list_emb_subseq_right [OF this] obtain us
where sublist: "subseq us ts"
and pairwise: "pairwise (λs t. (t, s) ∈ embeq F P)⇧=⇧= ss us" by blast
then have [simp]: "length us = length ss"
and emb: "(Fun f us, Fun f ss) ∈ embeq F P" by (auto dest: pairwise_embeq pairwise_length)
show ?case using ‹P¯¯⇧=⇧= (f, m) (g, n)›
proof
assume "P¯¯ (f, m) (g, n)"
with embeq_subseq [OF _ _ _ sublist, of P g f F] and list_emb
have "(Fun g ts, Fun f us) ∈ embeq F P" by simp
with emb show ?case by (blast dest: embeq_trans)
next
assume "(f, m) = (g, n)"
then have [simp]: "f = g" "m = n" by auto
have [simp]: "us = ts" using subseq_same_length [OF sublist] by (simp add: list_emb)
show "(Fun g ts, Fun f ss) ∈ embeq F P" using pairwise by (auto dest: pairwise_embeq)
qed
qed
lemma almost_full_on_gterms:
assumes "almost_full_on P¯¯⇧=⇧= F"
shows "almost_full_on (λs t. (t, s) ∈ embeq F P) (gterms F)"
proof -
have *: "almost_full_on (kruskal_term.emb F P¯¯⇧=⇧=) (gterms F)"
using kruskal_term.almost_full_on_trees [OF assms] .
show ?thesis by (intro almost_full_on_mono [OF subset_refl _ *] kruskal_emb_imp_embeq)
qed
definition "rewrite_relation R ⟷
((∀s t C. (s, t) ∈ R ⟶ (C⟨s⟩, C⟨t⟩) ∈ R) ∧
(∀s t σ. (s, t) ∈ R ⟶ (s ⋅ σ, t ⋅ σ) ∈ R))"
definition "rewrite_order R ⟷ rewrite_relation R ∧ irrefl R ∧ trans R"
definition "simplification_order R ⟷ rewrite_order R ∧ (∃Q. wqo_on Q¯¯⇧=⇧= UNIV ∧ emb UNIV Q ⊆ R)"
text ‹Every simplification order is strongly normalizing.›
lemma simplification_order_imp_SN:
fixes R :: "('f, 'v) term rel"
assumes "simplification_order R"
shows "SN R"
proof -
from assms obtain Q
where "rewrite_order R" and "wqo_on Q¯¯⇧=⇧= UNIV" and emb: "emb UNIV Q ⊆ R"
by (auto simp: simplification_order_def)
with almost_full_on_gterms [of Q UNIV]
have af: "almost_full_on (λs t. (t, s) ∈ (emb UNIV Q)⇧=) (gterms UNIV)"
and "trans R"
and "irrefl R"
and "rewrite_relation R"
by (auto simp: wqo_on_imp_almost_full_on rewrite_order_def)
then have subst: "⋀s t σ. (s, t) ∈ R ⟹ (s ⋅ σ, t ⋅ σ) ∈ R" by (auto simp: rewrite_relation_def)
note trans = ‹trans R› [unfolded trans_def, rule_format]
{ fix T :: "nat ⇒ ('f, 'v) term"
assume *: "⋀i. (T i, T (Suc i)) ∈ R"
obtain c where "c ∈ (UNIV :: 'f set)" by auto
def U ≡ "λi. T i ⋅ (λ_. Fun c [] :: ('f, 'v) term)"
have "∀i. U i ∈ gterms UNIV"
proof
fix i
show "U i ∈ gterms UNIV"
unfolding U_def by (induct ("T i")) (auto intro!: gterms.intros)
qed
with af have "good (λs t. (t, s) ∈ (emb UNIV Q)⇧=) U" by (auto simp: almost_full_on_def)
then obtain i j where "i < j"
and "(U j, U i) ∈ (emb UNIV Q)⇧=" by auto
with emb have "(U j, U i) ∈ R⇧=" by blast
moreover have "(U i, U j) ∈ R"
proof -
have "(T i, T j) ∈ R" using * and ‹i < j›
proof (induct j)
case (Suc j)
then show ?case by (cases "i = j") (auto elim: trans)
qed simp
then show "(U i, U j) ∈ R" by (auto simp: U_def subst)
qed
ultimately have "(U i, U i) ∈ R" by (auto dest: trans)
with ‹irrefl R› have False by (auto simp: irrefl_def) }
then show "SN R" by (auto simp: SN_defs)
qed
lemma wfp_on_SN_conv:
"wfp_on P UNIV ⟷ SN {(x, y). P y x}"
unfolding wfp_on_def SN_defs by blast
lemma wfp_on_imp_wf:
assumes "wfp_on P A"
shows "wf {(x, y). x ∈ A ∧ y ∈ A ∧ P x y}"
using wfp_on_imp_inductive_on [OF assms]
unfolding wf_def inductive_on_def
by (simp) (metis)
lemma well_order_extension':
assumes "wfp_on P A"
shows "∃W. (∀x∈A. ∀y∈A. P x y ⟶ W x y) ∧ po_on W A ∧ wfp_on W A ∧ total_on W A"
proof -
let ?R = "{(x, y). x ∈ A ∧ y ∈ A ∧ P x y}"
from wfp_on_imp_wf [OF assms]
have "wf ?R" and "Field ?R ⊆ A" by (auto simp: Field_def)
from well_order_on_extension [OF this] obtain R
where "?R ⊆ R" and "well_order_on A R" by blast
then have wf_R: "wf (R - Id)" and "refl_on A R"
and "antisym R" and "Relation.total_on A R"
and "trans R"
by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def)
note [dest] = ‹antisym R› [unfolded antisym_def, rule_format]
‹trans R› [unfolded trans_def, rule_format]
def W ≡ "λx y. (x, y) ∈ R - Id"
have ext: "∀x ∈ A. ∀y ∈ A. P x y ⟶ W x y"
using ‹?R ⊆ R› using assms [THEN wfp_on_imp_irreflp_on] by (auto simp: W_def irreflp_on_def)
moreover
have "po_on W A"
by (auto simp: po_on_def irreflp_on_def transp_on_def W_def)
moreover
have "wfp_on W A"
by (rule wfp_on_subset [OF subset_UNIV], rule inductive_on_imp_wfp_on, insert wf_R)
(simp only: W_def wfP_def wf_def inductive_on_def ball_UNIV)
moreover
have "total_on W A"
using ‹Relation.total_on A R› by (auto simp: Relation.total_on_def total_on_def W_def)
ultimately
show ?thesis by blast
qed
lemma wqo_on_extension:
assumes "wfp_on P A"
shows "∃W. (∀x∈A. ∀y∈A. P x y ⟶ W x y) ∧ po_on W A ∧ wfp_on W A ∧ almost_full_on W⇧=⇧= A"
using well_order_extension' [OF assms]
and total_on_and_wfp_on_imp_almost_full_on [of _ A] by blast
end