Theory Subsumption
section ‹Subsumption›
text ‹We define the subsumption relation on terms and prove its well-foundedness.›
theory Subsumption
imports
Term
"Abstract-Rewriting.Seq"
"HOL-Library.Adhoc_Overloading"
Fun_More
Seq_More
begin
consts
SUBSUMESEQ :: "'a ⇒ 'a ⇒ bool" (infix "≤⋅" 50)
SUBSUMES :: "'a ⇒ 'a ⇒ bool" (infix "<⋅" 50)
LITSIM :: "'a ⇒ 'a ⇒ bool" (infix "≐" 50)
abbreviation (input) INSTANCEQ (infix "⋅≥" 50)
where
"x ⋅≥ y ≡ y ≤⋅ x"
abbreviation (input) INSTANCE (infix "⋅>" 50)
where
"x ⋅> y ≡ y <⋅ x"
abbreviation INSTANCEEQ_SET ("{⋅≥}")
where
"{⋅≥} ≡ {(x, y). y ≤⋅ x}"
abbreviation INSTANCE_SET ("{⋅>}")
where
"{⋅>} ≡ {(x, y). y <⋅ x}"
abbreviation SUBSUMESEQ_SET ("{≤⋅}")
where
"{≤⋅} ≡ {(x, y). x ≤⋅ y}"
abbreviation SUBSUMES_SET ("{<⋅}")
where
"{<⋅} ≡ {(x, y). x <⋅ y}"
abbreviation LITSIM_SET ("{≐}")
where
"{≐} ≡ {(x, y). x ≐ y}"
locale subsumable =
fixes subsumeseq :: "'a ⇒ 'a ⇒ bool"
assumes refl: "subsumeseq x x"
and trans: "subsumeseq x y ⟹ subsumeseq y z ⟹ subsumeseq x z"
begin
adhoc_overloading
SUBSUMESEQ subsumeseq
definition "subsumes t s ⟷ t ≤⋅ s ∧ ¬ s ≤⋅ t"
definition "litsim s t ⟷ s ≤⋅ t ∧ t ≤⋅ s"
adhoc_overloading
SUBSUMES subsumes and
LITSIM litsim
lemma litsim_refl [simp]:
"s ≐ s"
by (auto simp: litsim_def refl)
lemma litsim_sym:
"s ≐ t ⟹ t ≐ s"
by (auto simp: litsim_def)
lemma litsim_trans:
"s ≐ t ⟹ t ≐ u ⟹ s ≐ u"
by (auto simp: litsim_def dest: trans)
end
sublocale subsumable ⊆ subsumption: preorder "(≤⋅)" "(<⋅)"
by (unfold_locales) (auto simp: subsumes_def refl elim: trans)
inductive subsumeseq_term :: "('a, 'b) term ⇒ ('a, 'b) term ⇒ bool"
where
[intro]: "t = s ⋅ σ ⟹ subsumeseq_term s t"
adhoc_overloading
SUBSUMESEQ subsumeseq_term
lemma subsumeseq_termE [elim]:
assumes "s ≤⋅ t"
obtains σ where "t = s ⋅ σ"
using assms by (cases)
lemma subsumeseq_term_refl:
fixes t :: "('a, 'b) term"
shows "t ≤⋅ t"
by (rule subsumeseq_term.intros [of t t Var]) simp
lemma subsumeseq_term_trans:
fixes s t u :: "('a, 'b) term"
assumes "s ≤⋅ t" and "t ≤⋅ u"
shows "s ≤⋅ u"
proof -
obtain σ τ
where [simp]: "t = s ⋅ σ" "u = t ⋅ τ" using assms by fastforce
show ?thesis
by (rule subsumeseq_term.intros [of _ _ "σ ∘⇩s τ"]) simp
qed