Theory terms
theory terms
imports "HOL-ex.Unification"
begin
section ‹Terms›
subsection ‹Basic Syntax›
text ‹We use the same term representation as in the Unification theory provided in Isabelle.
Terms are represented by binary trees built on variables and constant symbols.›
fun is_a_variable
where
"(is_a_variable (Var x)) = True" |
"(is_a_variable (Const x)) = False" |
"(is_a_variable (Comb x y)) = False"
fun is_a_constant
where
"(is_a_constant (Var x)) = False" |
"(is_a_constant (Const x)) = True" |
"(is_a_constant (Comb x y)) = False"
fun is_compound
where
"(is_compound (Var x)) = False" |
"(is_compound (Const x)) = False" |
"(is_compound (Comb x y)) = True"
definition ground_term :: "'a trm ⇒ bool"
where
"(ground_term t) = (vars_of t = {})"
lemma constants_are_not_variables :
assumes "is_a_constant x"
shows "¬ (is_a_variable x)"
by (metis assms is_a_constant.elims(2) is_a_variable.elims(2) trm.distinct(2))
lemma constants_are_ground :
assumes "is_a_constant x"
shows "ground_term x"
proof -
from assms obtain y where "x = (Const y)" using is_a_constant.elims(2) by auto
then show ?thesis by (simp add: ground_term_def)
qed
subsection ‹Positions›
text ‹We define the notion of a position together with functions to access to subterms and
replace them. We establish some basic properties of these functions.›
text ‹Since terms are binary trees, positions are sequences of binary digits.›
datatype indices = Left | Right
type_synonym position = "indices list"
fun left_app
where "left_app x = Left # x"
fun right_app
where "right_app x = Right # x"
definition strict_prefix
where
"strict_prefix p q = (∃r. (r ≠ []) ∧ (q = (append p r)))"
fun subterm :: "'a trm ⇒ position ⇒ 'a trm ⇒ bool"
where
"(subterm T [] S) = (T = S)" |
"(subterm (Var v) (first # next) S) = False" |
"(subterm (Const c) (first # next) S) = False" |
"(subterm (Comb x y) (Left # next) S) = (subterm x next S)" |
"(subterm (Comb x y) (Right # next) S) = (subterm y next S)"
definition occurs_in :: "'a trm ⇒ 'a trm ⇒ bool"
where
"occurs_in t s = (∃p. subterm s p t)"
definition position_in :: "position ⇒ 'a trm ⇒ bool"
where
"position_in p s = (∃t. subterm s p t)"
fun subterms_of
where
"subterms_of t = { s. (occurs_in s t) }"
fun proper_subterms_of
where
"proper_subterms_of t = { s. ∃p. (p ≠ Nil ∧ (subterm t p s)) }"
fun pos_of
where
"pos_of t = { p. (position_in p t) }"
fun replace_subterm ::
"'a trm ⇒ position ⇒ 'a trm ⇒ 'a trm ⇒ bool"
where
"(replace_subterm T [] u S) = (S = u) " |
"(replace_subterm (Var x) (first # next) u S) = False" |
"(replace_subterm (Const c) (first # next) u S) = False" |
"(replace_subterm (Comb x y) (Left # next) u S) =
(∃S1. (replace_subterm x next u S1) ∧ (S = Comb S1 y))" |
"(replace_subterm (Comb x y) (Right # next) u S) =
(∃S2. (replace_subterm y next u S2) ∧ (S = Comb x S2))"
lemma replace_subterm_is_a_function:
shows "⋀t u v. subterm t p u ⟹ ∃s. replace_subterm t p v s"
proof (induction p,auto)
next case (Cons i q)
from ‹subterm t (Cons i q) u› obtain t1 t2 where "t = (Comb t1 t2)"
using subterm.elims(2) by blast
have "i = Right ∨ i = Left" using indices.exhaust by auto
then show ?case
proof
assume "i = Right"
from this and ‹t = (Comb t1 t2)› and ‹subterm t (Cons i q) u› have "subterm t2 q u" by auto
from this obtain s where "replace_subterm t2 q v s" using Cons.IH [of t2 u] by auto
from this and ‹t = (Comb t1 t2)› and ‹i = Right› have "replace_subterm t (Cons i q) v (Comb t1 s)"
by auto
from this show ?case by auto
next assume "i = Left"
from this and ‹t = (Comb t1 t2)› and ‹subterm t (Cons i q) u› have "subterm t1 q u" by auto
from this obtain s where "replace_subterm t1 q v s" using Cons.IH [of t1 u] by auto
from this and ‹t = (Comb t1 t2)› and ‹i = Left› have "replace_subterm t (Cons i q) v (Comb s t2)"
by auto
from this show ?case by auto
qed
qed
text ‹We prove some useful lemmata concerning the set of variables or subterms occurring in a
term.›
lemma root_subterm:
shows "t ∈ (subterms_of t)"
by (metis mem_Collect_eq occurs_in_def subterm.simps(1) subterms_of.simps)
lemma root_position:
shows "Nil ∈ (pos_of t)"
by (metis mem_Collect_eq subterm.simps(1) position_in_def pos_of.simps)
lemma subterms_of_an_atomic_term:
assumes "is_a_variable t ∨ is_a_constant t"
shows "subterms_of t = { t }"
proof
show "subterms_of t ⊆ { t }"
proof
fix x assume "x ∈ subterms_of t"
then have "occurs_in x t" by auto
then have "∃p. (subterm t p x)" unfolding occurs_in_def by auto
from this and assms have "x = t"
by (metis is_a_constant.simps(3) is_a_variable.simps(3) subterm.elims(2))
thus "x ∈ { t }" by auto
qed
next
show "{ t } ⊆ subterms_of t"
proof
fix x assume "x ∈ { t }"
then show "x ∈ subterms_of t" using root_subterm by auto
qed
qed
lemma positions_of_an_atomic_term:
assumes "is_a_variable t ∨ is_a_constant t"
shows "pos_of t = { Nil }"
proof
show "pos_of t ⊆ { Nil }"
proof
fix x assume "x ∈ pos_of t"
then have "position_in x t" by auto
then have "∃s. (subterm t x s)" unfolding position_in_def by auto
from this and assms have "x = Nil"
by (metis is_a_constant.simps(3) is_a_variable.simps(3) subterm.elims(2))
thus "x ∈ { Nil }" by auto
qed
next
show "{ Nil } ⊆ pos_of t"
proof
fix x :: "indices list" assume "x ∈ { Nil }"
then show "x ∈ pos_of t" using root_position by auto
qed
qed
lemma subterm_of_a_subterm_is_a_subterm :
assumes "subterm u q v"
shows "⋀ t. subterm t p u ⟹ subterm t (append p q) v"
proof (induction p)
case Nil
show "?case" using Nil.prems assms by auto
next case (Cons i p')
from ‹subterm t (Cons i p') u› obtain t1 t2 where "t = (Comb t1 t2)"
using subterm.elims(2) by blast
have "i = Right ∨ i = Left" using indices.exhaust by auto
then show ?case
proof
assume "i = Right"
from this and ‹subterm t (Cons i p') u› and ‹t = (Comb t1 t2)›
have "subterm t2 p' u" by auto
from this have "subterm t2 (append p' q) v" by (simp add: Cons.IH)
from this and ‹t = (Comb t1 t2)› and ‹i = Right› show "subterm t (append (Cons i p') q) v"
by simp
next assume "i = Left"
from this and ‹subterm t (Cons i p') u› and ‹t = (Comb t1 t2)›
have "subterm t1 p' u" by auto
from this have "subterm t1 (append p' q) v" by (simp add: Cons.IH)
from this and ‹t = (Comb t1 t2)› and ‹i = Left› show "subterm t (append (Cons i p') q) v"
by simp
qed
qed
lemma occur_in_subterm:
assumes "occurs_in u t"
assumes "occurs_in t s"
shows "occurs_in u s"
by (meson assms(1) assms(2) occurs_in_def subterm_of_a_subterm_is_a_subterm)
lemma vars_of_subterm :
assumes "x ∈ vars_of s"
shows "⋀ t. subterm t p s ⟹ x ∈ vars_of t"
proof (induction p)
case Nil
show "?case" using Nil.prems assms by auto
next case (Cons i p')
from ‹subterm t (Cons i p') s› obtain t1 t2 where "t = (Comb t1 t2)"
using subterm.elims(2) by blast
have "i = Right ∨ i = Left" using indices.exhaust by auto
then show ?case
proof
assume "i = Right"
from this and ‹subterm t (Cons i p') s› and ‹t = (Comb t1 t2)›
have "subterm t2 p' s" by auto
from this have "x ∈ vars_of t2" by (simp add: Cons.IH)
from this and ‹t = (Comb t1 t2)› and ‹i = Right› show ?case
by simp
next assume "i = Left"
from this and ‹subterm t (Cons i p') s› and ‹t = (Comb t1 t2)›
have "subterm t1 p' s" by auto
from this have "x ∈ vars_of t1" by (simp add: Cons.IH)
from this and ‹t = (Comb t1 t2)› and ‹i = Left› show ?case
by simp
qed
qed
lemma vars_subterm :
assumes "subterm t p s"
shows "vars_of s ⊆ vars_of t"
by (meson assms subsetI vars_of_subterm)
lemma vars_subterms_of :
assumes "s ∈ subterms_of t"
shows "vars_of s ⊆ vars_of t"
using assms occurs_in_def vars_subterm by fastforce
lemma subterms_of_a_non_atomic_term:
shows "subterms_of (Comb t1 t2) = (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
proof
show "subterms_of (Comb t1 t2) ⊆ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
proof
fix x assume "x ∈ (subterms_of (Comb t1 t2))"
then have "occurs_in x (Comb t1 t2)" by auto
then obtain p where "subterm (Comb t1 t2) p x" unfolding occurs_in_def by auto
have "p = [] ∨ (∃i q. p = i #q)" using neq_Nil_conv by blast
then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
proof
assume "p = []"
from this and ‹subterm (Comb t1 t2) p x› show ?thesis by auto
next
assume "∃i q. p = i #q"
then obtain i q where "p = i # q" by auto
have "i = Left ∨ i = Right" using indices.exhaust by blast
then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
proof
assume "i = Left"
from this and ‹p = i # q› and ‹subterm (Comb t1 t2) p x›
have "subterm t1 q x" by auto
then have "occurs_in x t1" unfolding occurs_in_def by auto
then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }" by auto
next
assume "i = Right"
from this and ‹p = i # q› and ‹subterm (Comb t1 t2) p x›
have "subterm t2 q x" by auto
then have "occurs_in x t2" unfolding occurs_in_def by auto
then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }" by auto
qed
qed
qed
next
show "(subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) } ⊆ subterms_of (Comb t1 t2)"
proof
fix x assume "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
then have "x ∈ (subterms_of t1) ∨ (x ∈ (subterms_of t2) ∨ x = (Comb t1 t2))" by auto
thus "x ∈ subterms_of (Comb t1 t2)"
proof
assume "x ∈ (subterms_of t1)"
then have "occurs_in x t1" by auto
then obtain p where "subterm t1 p x" unfolding occurs_in_def by auto
then have "subterm (Comb t1 t2) (Left # p) x" by auto
then have "occurs_in x (Comb t1 t2)" using occurs_in_def by blast
then show "x ∈ subterms_of (Comb t1 t2)" by auto
next
assume "(x ∈ (subterms_of t2) ∨ x = (Comb t1 t2))"
then show "x ∈ subterms_of (Comb t1 t2)"
proof
assume "x ∈ (subterms_of t2)"
then have "occurs_in x t2" by auto
then obtain p where "subterm t2 p x" unfolding occurs_in_def by auto
then have "subterm (Comb t1 t2) (Right # p) x" by auto
then have "occurs_in x (Comb t1 t2)" using occurs_in_def by blast
then show "x ∈ subterms_of (Comb t1 t2)" by auto
next
assume "x = (Comb t1 t2)"
show "x ∈ subterms_of (Comb t1 t2)" using ‹x = t1 ⋅ t2› root_subterm by blast
qed
qed
qed
qed
lemma positions_of_a_non_atomic_term:
shows "pos_of (Comb t1 t2) = (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
proof
show "pos_of (Comb t1 t2) ⊆ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
proof
fix x assume "x ∈ pos_of (Comb t1 t2)"
then have "position_in x (Comb t1 t2)" by auto
then obtain s where "subterm (Comb t1 t2) x s" unfolding position_in_def by auto
have "x = [] ∨ (∃i q. x = i #q)" using neq_Nil_conv by blast
then show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
proof
assume "x = []"
from this and ‹subterm (Comb t1 t2) x s› show ?thesis by auto
next
assume "∃i q. x = i #q"
then obtain i q where "x = i # q" by auto
have "i = Left ∨ i = Right" using indices.exhaust by blast
then show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
proof
assume "i = Left"
from this and ‹x = i # q› and ‹subterm (Comb t1 t2) x s›
have "subterm t1 q s" by auto
then have "position_in q t1" unfolding position_in_def by auto
from this and ‹x = i # q› ‹i = Left›
show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }" by auto
next
assume "i = Right"
from this and ‹x = i # q› and ‹subterm (Comb t1 t2) x s›
have "subterm t2 q s" by auto
then have "position_in q t2" unfolding position_in_def by auto
from this and ‹x = i # q› ‹i = Right›
show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }" by auto
qed
qed
qed
next
show "(left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil } ⊆ pos_of (Comb t1 t2)"
proof
fix x assume "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
then have "(x ∈ left_app ` (pos_of t1)) ∨ ((x ∈ (right_app ` (pos_of t2))) ∨ (x = Nil))" by auto
thus "x ∈ pos_of (Comb t1 t2)"
proof
assume "x ∈ left_app ` (pos_of t1)"
then obtain q where "x = Left # q" and "position_in q t1" by auto
then obtain s where "subterm t1 q s" unfolding position_in_def by auto
then have "subterm (Comb t1 t2) (Left # q) s" by auto
from this and ‹x = Left # q› have "position_in x (Comb t1 t2)" using position_in_def by blast
then show "x ∈ pos_of (Comb t1 t2)" by auto
next
assume "(x ∈ (right_app ` (pos_of t2))) ∨ (x = Nil)"
then show "x ∈ pos_of (Comb t1 t2)"
proof
assume "x ∈ right_app ` (pos_of t2)"
then obtain q where "x = Right # q" and "position_in q t2" by auto
then obtain s where "subterm t2 q s" unfolding position_in_def by auto
then have "subterm (Comb t1 t2) (Right # q) s" by auto
from this and ‹x = Right # q› have "position_in x (Comb t1 t2)" using position_in_def by blast
then show "x ∈ pos_of (Comb t1 t2)" by auto
next
assume "x = Nil"
show "x ∈ pos_of (Comb t1 t2)" using ‹x = Nil› root_position by blast
qed
qed
qed
qed
lemma set_of_subterms_is_finite :
shows "(finite (subterms_of (t :: 'a trm)))"
proof (induction t)
case (Var x)
then show ?case using subterms_of_an_atomic_term [of "Var x"] by simp
next
case (Const x)
then show ?case using subterms_of_an_atomic_term [of "Const x"] by simp
next
case (Comb t1 t2) assume "finite (subterms_of t1)" and "finite (subterms_of t2)"
have "subterms_of (Comb t1 t2) = subterms_of t1 ∪ subterms_of t2 ∪ { Comb t1 t2 }"
using subterms_of_a_non_atomic_term by auto
from this and ‹finite (subterms_of t1)› and ‹finite (subterms_of t2)›
show "finite (subterms_of (Comb t1 t2))" by simp
qed
lemma set_of_positions_is_finite :
shows "(finite (pos_of (t :: 'a trm)))"
proof (induction t)
case (Var x)
then show ?case using positions_of_an_atomic_term [of "Var x"] by simp
next
case (Const x)
then show ?case using positions_of_an_atomic_term [of "Const x"] by simp
next
case (Comb t1 t2) assume "finite (pos_of t1)" and "finite (pos_of t2)"
from ‹finite (pos_of t1)› have i: "finite (left_app ` (pos_of t1))" by auto
from ‹finite (pos_of t2)› have ii: "finite (right_app ` (pos_of t2))" by auto
have "pos_of (Comb t1 t2) = (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
using positions_of_a_non_atomic_term by metis
from this and i ii show "finite (pos_of (Comb t1 t2))" by simp
qed
lemma vars_of_instances:
shows "vars_of (subst t σ)
= ⋃ { V. ∃x. (x ∈ (vars_of t)) ∧ (V = vars_of (subst (Var x) σ)) }"
proof (induction t)
case (Const a)
have "vars_of (Const a) = {}" by auto
then have rhs_empty: "⋃ { V. ∃x. (x ∈ (vars_of (Const a))) ∧ (V = vars_of (subst (Var x) σ)) } = {}" by auto
have lhs_empty: "(subst (Const a) σ) = (Const a)" by auto
from rhs_empty and lhs_empty show ?case by auto
next
case (Var a)
have "vars_of (Var a) = { a }" by auto
then have rhs: "⋃ { V. ∃x. (x ∈ (vars_of (Var a))) ∧ (V = vars_of (subst (Var x) σ)) } =
vars_of (subst (Var a) σ)" by auto
have lhs: "(subst (Var a) σ) = (subst (Var a) σ)" by auto
from rhs and lhs show ?case by auto
next
case (Comb t1 t2)
have "vars_of (Comb t1 t2) = (vars_of t1) ∪ (vars_of t2)" by auto
then have "⋃ { V. ∃x. (x ∈ (vars_of (Comb t1 t2))) ∧ (V = vars_of (subst (Var x) σ)) }
= ⋃ { V. ∃x. (x ∈ (vars_of t1)) ∧ (V = vars_of (subst(Var x) σ)) }
∪ ⋃ { V. ∃x. (x ∈ (vars_of t2)) ∧ (V = vars_of (subst (Var x) σ)) }"
by auto
then have rhs: "⋃ { V. ∃x. (x ∈ (vars_of (Comb t1 t2))) ∧ (V = vars_of (subst (Var x) σ)) }
= (vars_of (subst t1 σ)) ∪ (vars_of (subst t2 σ))"
using ‹vars_of (subst t1 σ)
= ⋃ { V. ∃x. (x ∈ (vars_of t1)) ∧ (V = vars_of (subst (Var x) σ)) }›
and
‹vars_of (subst t2 σ)
= ⋃ { V. ∃x. (x ∈ (vars_of t2)) ∧ (V = vars_of (subst (Var x) σ)) }›
by auto
have "(subst (Comb t1 t2) σ) = (Comb (subst t1 σ) (subst t2 σ))"
by auto
then have lhs: "(vars_of (subst (Comb t1 t2) σ)) =
(vars_of (subst t1 σ)) ∪ (vars_of (subst t2 σ))" by auto
from lhs and rhs show ?case by auto
qed
lemma subterms_of_instances :
"∀u v u' s. (u = (subst v s) ⟶ (subterm u p u')
⟶ (∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
(subterm v q2 x) ∧ (p = (append q2 q1))) ∨
((∃ v'. ((¬ is_a_variable v') ∧ (subterm v p v') ∧ (u' = (subst v' s))))))" (is "?prop p")
proof (induction p)
case Nil
show "?case"
proof ((rule allI)+,(rule impI)+)
fix u ::"'a trm" fix v u' s assume "u = (subst v s)" and "subterm u [] u'"
then have "u = u'" by auto
show "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
(subterm v q2 x) ∧ ([] = (append q2 q1))) ∨
((∃ v'. ((¬ is_a_variable v') ∧ (subterm v [] v') ∧ (u' = (subst v' s)))))"
proof (cases)
assume "is_a_variable v"
from ‹u = u'›and ‹u = (subst v s)›
have "(subterm (subst v s) [] u')" by auto
have "subterm v [] v" by auto
from this and ‹(subterm (subst v s) [] u')› and ‹is_a_variable v›
show ?thesis by auto
next assume "¬ is_a_variable v"
from ‹u = u'› and ‹u = (subst v s)›
have "((subterm v [] v) ∧ (u' = (subst v s)))" by auto
then show ?thesis by auto
qed
qed
next
case (Cons i q)
show ?case
proof ((rule allI)+,(rule impI)+)
fix u ::"'a trm" fix v u' s assume "u = (subst v s)"
and "subterm u (Cons i q) u'"
show "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
(subterm v q2 x) ∧ ((Cons i q) = (append q2 q1))) ∨
((∃ v'. ((¬ is_a_variable v') ∧ (subterm v (Cons i q) v') ∧ (u' = (subst v' s)))))"
proof (cases v)
fix x assume "v = (Var x)"
then have "subterm v [] v" by auto
from ‹v = (Var x)› have "is_a_variable v" by auto
have "Cons i q = (append [] (Cons i q))" by auto
from ‹subterm u (Cons i q) u'› and ‹u = (subst v s)›
and ‹v = (Var x)› have "subterm (subst v s) (Cons i q) u'" by auto
from ‹is_a_variable v› and ‹subterm v [] v› and ‹Cons i q = (append [] (Cons i q))› and this
show ?thesis by blast
next
fix x assume "v = (Const x)"
from this and ‹u = (subst v s)› have "u = v" by auto
from this and ‹v = (Const x)› and ‹subterm u (Cons i q) u'› show ?thesis by auto
next
fix t1 t2 assume "v = (Comb t1 t2)"
from this and ‹u = (subst v s)›
have "u = (Comb (subst t1 s) (subst t2 s))" by auto
have "i = Left ∨ i = Right" using indices.exhaust by auto
from ‹i = Left ∨ i = Right› and ‹u = (Comb (subst t1 s) (subst t2 s))›
and ‹subterm u (Cons i q) u'› obtain ti where
"subterm (subst ti s) q u'" and "ti = t1 ∨ ti = t2" and "subterm v [i] ti"
using ‹v = t1 ⋅ t2› by auto
from ‹?prop q› and ‹subterm (subst ti s) q u'› have
"(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
(subterm ti q2 x) ∧ (q = (append q2 q1))) ∨
((∃ v'. ((¬ is_a_variable v') ∧ (subterm ti q v') ∧ (u' = (subst v' s)))))"
by auto
then show ?thesis
proof
assume "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
(subterm ti q2 x) ∧ (q = (append q2 q1)))"
then obtain x q1 q2 where "is_a_variable x" and "subterm (subst x s) q1 u'"
and "subterm ti q2 x" and "q = (append q2 q1)"
by auto
from ‹subterm ti q2 x› and ‹subterm v [i] ti› have "subterm v (i # q2) x"
using ‹i = indices.Left ∨ i = indices.Right› ‹v = t1 ⋅ t2› by auto
from ‹q = append q2 q1› have "i # q = (append (i # q2) q1)" by auto
from ‹i # q = (append (i # q2) q1)› and ‹is_a_variable x›
and ‹subterm (subst x s) q1 u'› and ‹subterm v (i # q2) x›
show ?thesis by blast
next
assume "((∃ v'. ((¬ is_a_variable v') ∧ (subterm ti q v') ∧ (u' = (subst v' s)))))"
then obtain v' where "(¬ is_a_variable v')" "(subterm ti q v')" and "u' = (subst v' s)" by auto
from ‹subterm ti q v'› and ‹subterm v [i] ti› have "subterm v (i # q) v'"
using ‹i = indices.Left ∨ i = indices.Right› ‹v = t1 ⋅ t2› by auto
from this and ‹(¬ is_a_variable v')› ‹subterm ti q v'› and ‹u' = (subst v' s)›
show ?thesis by auto
qed
qed
qed
qed
lemma vars_of_replacement:
shows "⋀ t s. x ∈ vars_of s ⟹ replace_subterm t p v s ⟹ x ∈ (vars_of t) ∪ (vars_of v)"
proof (induction p)
case Nil
from ‹replace_subterm t Nil v s› have "s = v" by auto
from this and ‹x ∈ vars_of s› show ?case by auto
next case (Cons i q)
from ‹replace_subterm t (Cons i q) v s› obtain t1 t2 where
"t = (Comb t1 t2)"
by (metis is_a_variable.cases replace_subterm.simps(2) replace_subterm.simps(3))
have "i = Left ∨ i = Right" using indices.exhaust by blast
then show ?case
proof
assume "i = Left"
from this and ‹t = Comb t1 t2› and ‹replace_subterm t (Cons i q) v s›
obtain s1 where "s = Comb s1 t2" and "replace_subterm t1 q v s1"
using replace_subterm.simps(4) by auto
from ‹s = Comb s1 t2› and ‹x ∈ vars_of s› have "x ∈ vars_of s1 ∨ x ∈ vars_of t2"
by simp
then show ?case
proof
assume "x ∈ vars_of s1"
from this and Cons.IH [of s1 t1] and ‹replace_subterm t1 q v s1› have "x ∈ (vars_of t1) ∪ (vars_of v)"
by auto
from this and ‹t = (Comb t1 t2)› show ?case by auto
next
assume "x ∈ vars_of t2"
from this and ‹t = (Comb t1 t2)› show ?case by auto
qed
next
assume "i = Right"
from this and ‹t = Comb t1 t2› and ‹replace_subterm t (Cons i q) v s›
obtain s2 where "s = Comb t1 s2" and "replace_subterm t2 q v s2"
using replace_subterm.simps by auto
from ‹s = Comb t1 s2› and ‹x ∈ vars_of s› have "x ∈ vars_of t1 ∨ x ∈ vars_of s2"
by simp
then show ?case
proof
assume "x ∈ vars_of s2"
from this and Cons.IH [of s2 t2] and ‹replace_subterm t2 q v s2› have "x ∈ (vars_of t2) ∪ (vars_of v)"
by auto
from this and ‹t = (Comb t1 t2)› show ?case by auto
next
assume "x ∈ vars_of t1"
from this and ‹t = (Comb t1 t2)› show ?case by auto
qed
qed
qed
lemma vars_of_replacement_set:
assumes "replace_subterm t p v s"
shows "vars_of s ⊆ (vars_of t) ∪ (vars_of v)"
by (meson assms subsetI vars_of_replacement)
subsection ‹Substitutions and Most General Unifiers›
text ‹Substitutions are defined in the Unification theory. We provide some
additional definitions and lemmata.›
fun subst_set :: "'a trm set => 'a subst => 'a trm set"
where
"(subst_set S σ) = { u. ∃t. u = (subst t σ) ∧ t ∈ S }"
definition subst_codomain
where
"subst_codomain σ V = { x. ∃y. (subst (Var y) σ) = (Var x) ∧ (y ∈ V) }"
lemma subst_codomain_is_finite:
assumes "finite A"
shows "finite (subst_codomain η A)"
proof -
have i: "((λx. (Var x)) ` (subst_codomain η A)) ⊆ ((λx. (subst (Var x) η)) ` A)"
proof
fix x assume "x ∈ ((λx. (Var x)) ` (subst_codomain η A))"
from this obtain y where "y ∈ (subst_codomain η A)" and "x = (Var y)" by auto
from ‹y ∈ (subst_codomain η A)› obtain z where "(subst (Var z) η) = (Var y)" "(z ∈ A)"
unfolding subst_codomain_def by auto
from ‹(z ∈ A)› ‹x = (Var y)› ‹(subst (Var z) η) = (Var y)› this show
"x ∈ ((λx. (subst (Var x) η)) ` A)"using image_iff by fastforce
qed
have "inj_on (λx. (Var x)) (subst_codomain η A)" by (meson inj_onI trm.inject(1))
from assms(1) have "finite ((λx. (subst (Var x) η)) ` A)" by auto
from this and i have "finite ((λx. (Var x)) ` (subst_codomain η A))"
using rev_finite_subset by auto
from this and ‹inj_on (λx. (Var x)) (subst_codomain η A)› show ?thesis using finite_imageD [of "(λx. (Var x))" "subst_codomain η A"]
by auto
qed
text ‹The notions of unifiers, most general unifiers, the unification algorithm and a
proof of correctness are provided in the Unification theory. Below, we prove that the algorithm
is complete.›
lemma subt_decompose:
shows "∀t1 t2. Comb t1 t2 ≺ s ⟶ (t1 ≺ s ∧ t2≺ s) "
proof ((induction s),(simp),(simp))
case (Comb s1 s2)
show ?case
proof ((rule allI)+,(rule impI))
fix t1 t2 assume "Comb t1 t2 ≺ Comb s1 s2"
show "t1 ≺ (Comb s1 s2) ∧ t2 ≺ (Comb s1 s2)"
proof (rule ccontr)
assume neg: "¬(t1 ≺ (Comb s1 s2) ∧ t2 ≺ (Comb s1 s2))"
from ‹Comb t1 t2 ≺ Comb s1 s2› have
d: "Comb t1 t2 = s1 ∨ Comb t1 t2 = s2 ∨ Comb t1 t2 ≺ s1 ∨ Comb t1 t2 ≺ s2"
by auto
have i: "¬ (Comb t1 t2 = s1)"
proof
assume "(Comb t1 t2 = s1)"
then have "t1 ≺ s1" and "t2 ≺ s1" by auto
from this and neg show False by auto
qed
have ii: "¬ (Comb t1 t2 = s2)"
proof
assume "(Comb t1 t2 = s2)"
then have "t1 ≺ s2" and "t2 ≺ s2" by auto
from this and neg show False by auto
qed
have iii: "¬ (Comb t1 t2 ≺ s1)"
proof
assume "(Comb t1 t2 ≺ s1)"
then have "t1 ≺ s1 ∧ t2 ≺ s1" using Comb.IH by metis
from this and neg show False by auto
qed
have iv: "¬ (Comb t1 t2 ≺ s2)"
proof
assume "(Comb t1 t2 ≺ s2)"
then have "t1 ≺ s2 ∧ t2 ≺ s2" using Comb.IH by metis
from this and neg show False by auto
qed
from d and i ii iii iv show False by auto
qed
qed
qed
lemma subt_irrefl:
shows "¬ (s ≺ s)"
proof ((induction s),(simp),(simp))
case (Comb t1 t2)
show ?case
proof
assume "Comb t1 t2 ≺ Comb t1 t2"
then have i: "Comb t1 t2 ≠ t1" using Comb.IH(1) by fastforce
from ‹Comb t1 t2 ≺ Comb t1 t2› have ii: "Comb t1 t2 ≠ t2" using Comb.IH(2) by fastforce
from i ii and ‹Comb t1 t2 ≺ Comb t1 t2› have "Comb t1 t2 ≺ t1 ∨ Comb t1 t2 ≺ t2" by auto
then show False
proof
assume "Comb t1 t2 ≺ t1"
then have "t1 ≺ t1" using subt_decompose [of t1] by metis
from this show False using Comb.IH by auto
next
assume "Comb t1 t2 ≺ t2"
then have "t2 ≺ t2" using subt_decompose [of t2] by metis
from this show False using Comb.IH by auto
qed
qed
qed
lemma MGU_exists:
shows "∀σ. ((subst t σ) = (subst s σ) ⟶ unify t s ≠ None)"
proof (rule unify.induct)
fix x s1 s2 show "∀σ :: 'a subst .((subst (Const x) σ) = (subst (Comb s1 s2) σ)
⟶ unify (Const x) (Comb s1 s2) ≠ None)" by simp
next
fix t1 t2 y show "∀σ :: 'a subst.(subst (Comb t1 t2) σ) = (subst (Const y) σ)
⟶ unify (Comb t1 t2) (Const y) ≠ None" by simp
next
fix x y show "∀σ :: 'a subst.(subst (Const x) σ) = (subst (Var y) σ)
⟶ unify (Const x) (Var y) ≠ None" using unify.simps(3) by fastforce
next
fix t1 t2 y show "∀σ :: 'a subst.(subst (Comb t1 t2) σ) = (subst (Var y) σ)
⟶ unify (Comb t1 t2) (Var y) ≠ None"
by (metis option.distinct(1) subst_mono subt_irrefl unify.simps(4))
next
fix x s show "∀σ :: 'a subst.(subst (Var x) σ) = (subst s σ)
⟶ unify (Var x) s ≠ None"
by (metis option.distinct(1) subst_mono subt_irrefl unify.simps(5))
next
fix x y show "∀σ :: 'a subst.(subst (Const x) σ) = (subst (Const y) σ)
⟶ unify (Const x) (Const y) ≠ None" by simp
next
fix t1 t2 s1 s2
show "∀σ :: 'a subst. (subst t1 σ = subst s1 σ ⟶ unify t1 s1 ≠ None) ⟹
(⋀x2. unify t1 s1 = Some x2 ⟹
∀σ. subst (t2 ⊲ x2) σ = subst (s2 ⊲ x2) σ ⟶
unify (t2 ⊲ x2) (s2 ⊲ x2) ≠ None) ⟹
∀σ. (subst (t1 ⋅ t2) σ = subst (s1 ⋅ s2) σ ⟶
unify (t1 ⋅ t2) (s1 ⋅ s2) ≠ None)"
proof -
assume h1: "∀σ. (subst t1 σ = subst s1 σ ⟶ unify t1 s1 ≠ None)"
assume h2: "(⋀x2. unify t1 s1 = Some x2 ⟹
∀σ. subst (t2 ⊲ x2) σ = subst (s2 ⊲ x2) σ ⟶
unify (t2 ⊲ x2) (s2 ⊲ x2) ≠ None)"
show "∀σ. (subst (t1 ⋅ t2) σ = subst (s1 ⋅ s2) σ ⟶
unify (t1 ⋅ t2) (s1 ⋅ s2) ≠ None)"
proof ((rule allI),(rule impI))
fix σ assume h3: "subst (t1 ⋅ t2) σ = subst (s1 ⋅ s2) σ"
from h3 have "subst t1 σ = subst s1 σ" by auto
from this and h1 have "unify t1 s1 ≠ None" by auto
from this obtain θ where "unify t1 s1 = Some θ" and "MGU θ t1 s1"
by (meson option.exhaust unify_computes_MGU)
from ‹subst t1 σ = subst s1 σ› have "Unifier σ t1 s1"
unfolding Unifier_def by auto
from this and ‹MGU θ t1 s1› obtain η where "σ ≐ θ ◊ η" using MGU_def by metis
from h3 have "subst t2 σ = subst s2 σ" by auto
from this and ‹σ ≐ θ ◊ η›
have "subst (subst t2 θ) η
= subst (subst s2 θ) η"
by (simp add: subst_eq_def)
from this and ‹unify t1 s1 = Some θ› and h2 [of θ] have "unify (t2 ⊲ θ) (s2 ⊲ θ) ≠ None"
by auto
from this show "unify (t1 ⋅ t2) (s1 ⋅ s2) ≠ None"
by (simp add: ‹unify t1 s1 = Some θ› option.case_eq_if)
qed
qed
qed
text ‹We establish some useful properties of substitutions and instances.›
definition ground_on :: "'a set ⇒ 'a subst ⇒ bool"
where "ground_on V σ = (∀x ∈ V. (ground_term (subst (Var x) σ)))"
lemma comp_subst_terms:
assumes "σ ≐ θ ◊ η"
shows "(subst t σ) = (subst (subst t θ) η)"
proof -
from ‹σ ≐ θ ◊ η› have "((subst t σ) = (subst t (θ ◊ η)))" by auto
have "(subst t (θ ◊ η) = (subst (subst t θ) η))" by auto
from this and ‹((subst t σ) = (subst t (θ ◊ η)))› show ?thesis by auto
qed
lemma ground_instance:
assumes "ground_on (vars_of t) σ"
shows "ground_term (subst t σ)"
proof (rule ccontr)
assume "¬ ground_term (subst t σ)"
then have "vars_of (subst t σ) ≠ {}" unfolding ground_term_def by auto
then obtain x where "x ∈ vars_of (subst t σ)" by auto
then have "x ∈ ⋃ { V. ∃x. (x ∈ (vars_of t)) ∧ (V = vars_of (subst (Var x) σ)) }"
using vars_of_instances by force
then obtain y where "x ∈ (vars_of (subst (Var y) σ))" and "y ∈ (vars_of t)" by blast
from assms(1) and ‹y ∈ (vars_of t)› have "ground_term (subst (Var y) σ)" unfolding ground_on_def
by auto
from this and ‹x ∈ (vars_of (subst (Var y) σ))› show False unfolding ground_term_def by auto
qed
lemma substs_preserve_groundness:
assumes "ground_term t"
shows "ground_term (subst t σ)"
by (metis assms equals0D ground_instance ground_on_def ground_term_def)
lemma ground_subst_exists :
"finite V ⟹ ∃σ. (ground_on V σ)"
proof (induction rule: finite.induct)
case emptyI
show ?case unfolding ground_on_def by simp
next
fix A :: "'a set" and a::'a
assume "finite A"
assume hyp_ind: "∃σ. ground_on A σ"
then obtain σ where "ground_on A σ" by auto
then show "∃σ. ground_on (insert a A) σ"
proof cases
assume "a ∈ A"
from this and hyp_ind show "∃σ. ground_on (insert a A) σ"
unfolding ground_on_def by auto
next
assume "a ∉ A"
obtain c where "c = (Const a)" and "is_a_constant c" by auto
obtain θ where "θ = (a,c) # σ" by auto
have "∀x. (x ∈ insert a A ⟶ (ground_term (subst (Var x) θ)))"
proof ((rule allI)+,(rule impI)+)
fix x assume "x ∈ insert a A"
show "ground_term (subst (Var x) θ)"
proof cases
assume "x = a"
from this and ‹θ = (a,c) # σ› have "(subst (Var x) θ) = c" by auto
from ‹is_a_constant c› have "ground_term c" using constants_are_ground by auto
from this and ‹(subst (Var x) θ) = c› show "ground_term (subst (Var x) θ)" by auto
next
assume "x ≠ a"
from ‹x ≠ a› and ‹x ∈ insert a A› have "x ∈ A" by auto
from ‹x ≠ a› and ‹θ = (a,c) # σ› have "(subst (Var x) θ) = (subst (Var x) σ)" by auto
from this and ‹x ∈ A› and ‹ground_on A σ›
show "ground_term (subst (Var x) θ)" unfolding ground_on_def by auto
qed
qed
from this show ?thesis unfolding ground_on_def by auto
qed
qed
lemma substs_preserve_ground_terms :
assumes "ground_term t"
shows "subst t σ = t"
by (metis agreement assms equals0D ground_term_def subst_Nil)
lemma substs_preserve_subterms :
shows "⋀ t s. subterm t p s ⟹ subterm (subst t σ) p (subst s σ)"
proof (induction p)
case Nil
then have "t = s" using subterm.elims(2) by auto
from ‹t = s› have "(subst t σ) = (subst s σ)" by auto
from this show ?case using Nil.prems by auto
next case (Cons i q)
from ‹subterm t (i # q) s› obtain t1 t2 where
"t = (Comb t1 t2)" using subterm.elims(2) by blast
have "i = Left ∨ i = Right" using indices.exhaust by blast
then show "subterm (subst t σ) (i # q) (subst s σ)"
proof
assume "i = Left"
from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) s›
have "subterm t1 q s" by auto
from this have "subterm (subst t1 σ) q (subst s σ)" using Cons.IH by auto
from this and ‹t = Comb t1 t2›
show "subterm (subst t σ) (i # q) (subst s σ)"
by (simp add: ‹i = indices.Left›)
next assume "i = Right"
from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) s›
have "subterm t2 q s" by auto
from this have "subterm (subst t2 σ) q (subst s σ)" using Cons.IH by auto
from this and ‹t = Comb t1 t2›
show "subterm (subst t σ) (i # q) (subst s σ)"
by (simp add: ‹i = indices.Right›)
qed
qed
lemma substs_preserve_occurs_in:
assumes "occurs_in s t"
shows "occurs_in (subst s σ) (subst t σ)"
using substs_preserve_subterms
using assms occurs_in_def by blast
definition coincide_on
where "coincide_on σ η V = (∀x ∈ V. (subst (Var x) σ) = ( (subst (Var x) η)))"
lemma coincide_sym:
assumes "coincide_on σ η V"
shows "coincide_on η σ V"
by (metis assms coincide_on_def)
lemma coincide_on_term:
shows "⋀ σ η. coincide_on σ η (vars_of t) ⟹ subst t σ = subst t η"
proof (induction t)
case (Var x)
from this show "subst (Var x) σ = subst (Var x) η"
unfolding coincide_on_def by auto
next case (Const x)
show "subst (Const x) σ = subst (Const x) η" by auto
next case (Comb t1 t2)
from this show ?case unfolding coincide_on_def by auto
qed
lemma ground_replacement:
assumes "replace_subterm t p v s"
assumes "ground_term (subst t σ)"
assumes "ground_term (subst v σ)"
shows "ground_term (subst s σ)"
proof -
from assms(1) have "vars_of s ⊆ (vars_of t) ∪ (vars_of v)" using vars_of_replacement_set [of t p v s]
by auto
from assms(2) have "ground_on (vars_of t) σ" unfolding ground_on_def
by (metis contra_subsetD ex_in_conv ground_term_def
occs_vars_subset subst_mono vars_iff_occseq)
from assms(3) have "ground_on (vars_of v) σ" unfolding ground_on_def
by (metis contra_subsetD ex_in_conv ground_term_def
occs_vars_subset subst_mono vars_iff_occseq)
from ‹vars_of s ⊆ (vars_of t) ∪ (vars_of v)› ‹ground_on (vars_of t) σ›
and ‹ground_on (vars_of v) σ› have "ground_on (vars_of s) σ"
by (meson UnE ground_on_def rev_subsetD)
from this show ?thesis using ground_instance by blast
qed
text ‹We now show that two disjoint substitutions can always be fused.›
lemma combine_substs:
assumes "finite V1"
assumes "V1 ∩ V2 = {}"
assumes "ground_on V1 η1"
shows "∃σ. (coincide_on σ η1 V1) ∧ (coincide_on σ η2 V2)"
proof -
have "finite V1 ⟹ ground_on V1 η1 ⟹ V1 ∩ V2 = {} ⟹ ∃σ. (coincide_on σ η1 V1) ∧ (coincide_on σ η2 V2)"
proof (induction rule: finite.induct)
case emptyI
show ?case unfolding coincide_on_def by auto
next fix V1 :: "'a set" and a::'a
assume "finite V1"
assume hyp_ind: "ground_on V1 η1 ⟹ V1 ∩ V2 = {}
⟹ ∃σ. (coincide_on σ η1 V1) ∧ (coincide_on σ η2 V2)"
assume "ground_on (insert a V1) η1"
assume "(insert a V1) ∩ V2 = {}"
from this have "V1 ∩ V2 = {}" by auto
from ‹ground_on (insert a V1) η1› have "ground_on V1 η1"
unfolding ground_on_def by auto
from this and hyp_ind and ‹V1 ∩ V2 = {}› obtain σ'
where c:"(coincide_on σ' η1 V1) ∧ (coincide_on σ' η2 V2)" by auto
let ?t = "subst (Var a) η1"
from assms(2) have "ground_term ?t"
by (meson ‹ground_on (insert a V1) η1› ground_on_def insertI1)
let ?σ = "comp [(a,?t)] σ'"
have "coincide_on ?σ η1 (insert a V1)"
proof (rule ccontr)
assume "¬coincide_on ?σ η1 (insert a V1)"
then obtain x where "x ∈ (insert a V1)" and
"(subst (Var x) ?σ) ≠ ( (subst (Var x) η1))"
unfolding coincide_on_def by blast
have "subst (Var a) ?σ = subst ?t σ'" by simp
from ‹ground_term ?t› have "subst (Var a) ?σ = ?t"
using substs_preserve_ground_terms by auto
from this and ‹(subst (Var x) ?σ) ≠ ( (subst (Var x) η1))›
have "x ≠ a" by blast
from this and ‹x ∈ (insert a V1)› have "x ∈ V1" by auto
from ‹x ≠ a› have "(subst (Var x) ?σ) = (subst (Var x) σ')" by auto
from c and ‹x ∈ V1› have "(subst (Var x) σ') = (subst (Var x) η1)"
unfolding coincide_on_def by blast
from this and ‹(subst (Var x) ?σ) = (subst (Var x) σ')›
and ‹(subst (Var x) ?σ) ≠ ( (subst (Var x) η1))› show False by auto
qed
have "coincide_on ?σ η2 V2"
proof (rule ccontr)
assume "¬coincide_on ?σ η2 V2"
then obtain x where "x ∈ V2" and
"(subst (Var x) ?σ) ≠ ( (subst (Var x) η2))"
unfolding coincide_on_def by blast
from ‹(insert a V1) ∩ V2 = {}› and ‹x ∈ V2› have "x ≠ a" by auto
from this have "(subst (Var x) ?σ) = (subst (Var x) σ')" by auto
from c and ‹x ∈ V2› have "(subst (Var x) σ') = (subst (Var x) η2)"
unfolding coincide_on_def by blast
from this and ‹(subst (Var x) ?σ) = (subst (Var x) σ')›
and ‹(subst (Var x) ?σ) ≠ ( (subst (Var x) η2))› show False by auto
qed
from ‹coincide_on ?σ η1 (insert a V1)› ‹coincide_on ?σ η2 V2›
show "∃σ. (coincide_on σ η1 (insert a V1)) ∧ (coincide_on σ η2 V2)" by auto
qed
from this and assms show ?thesis by auto
qed
text ‹We define a map function for substitutions and prove its correctness.›
fun map_subst
where "map_subst f Nil = Nil"
| "map_subst f ((x,y) # l) = (x,(f y)) # (map_subst f l)"
lemma map_subst_lemma:
shows "((subst (Var x) σ) ≠ (Var x) ∨ (subst (Var x) σ) ≠ (subst (Var x) (map_subst f σ)))
⟶ ((subst (Var x) (map_subst f σ)) = (f (subst (Var x) σ)))"
proof (induction σ,simp)
next case (Cons p σ)
let ?u = "(fst p)"
let ?v = "(snd p)"
show ?case
proof
assume "((subst (Var x) (Cons p σ)) ≠ (Var x)
∨ (subst (Var x) (Cons p σ))
≠ (subst (Var x) (map_subst f (Cons p σ))))"
have "map_subst f (Cons p σ) = ( (?u, (f ?v)) # (map_subst f σ))"
by (metis map_subst.simps(2) prod.collapse)
show "(subst (Var x) (map_subst f (Cons p σ))) = (f (subst (Var x) (Cons p σ)))"
proof cases
assume "x = ?u"
from this have "subst (Var x) (Cons p σ) = ?v"
by (metis assoc.simps(2) prod.collapse subst.simps(1))
from ‹map_subst f (Cons p σ) = ( (?u, (f ?v)) # (map_subst f σ))›
and ‹x = ?u›
have "subst (Var x) (map_subst f (Cons p σ)) = (f ?v)" by simp
from ‹subst (Var x) (Cons p σ) = ?v› ‹subst (Var x) (map_subst f (Cons p σ)) = (f ?v)› show ?thesis by auto
next
assume "x ≠ ?u"
from this have "subst (Var x) (Cons p σ) = (subst (Var x) σ)"
by (metis assoc.simps(2) prod.collapse subst.simps(1))
from ‹map_subst f (Cons p σ) = ( (?u, (f ?v)) # (map_subst f σ))›
and ‹x ≠ ?u›
have "subst (Var x) (map_subst f (Cons p σ)) =
subst (Var x) (map_subst f σ)" by simp
from this and "Cons.IH" have
"subst (Var x) (map_subst f (Cons p σ)) = (f (subst (Var x) σ))"
using ‹subst (Var x) (p # σ) = subst (Var x) σ› ‹subst (Var x) (p # σ) ≠ Var x ∨ subst (Var x) (p # σ) ≠ subst (Var x) (map_subst f (p # σ))› by auto
from this and ‹subst (Var x) (Cons p σ) = (subst (Var x) σ)› show ?thesis by auto
qed
qed
qed
subsubsection ‹Minimum Idempotent Most General Unifier›
definition min_IMGU :: "'a subst ⇒ 'a trm ⇒ 'a trm ⇒ bool" where
"min_IMGU μ t u ⟷
IMGU μ t u ∧ fst ` set μ ⊆ vars_of t ∪ vars_of u ∧ range_vars μ ⊆ vars_of t ∪ vars_of u"
lemma unify_computes_min_IMGU:
"unify M N = Some σ ⟹ min_IMGU σ M N"
by (simp add: min_IMGU_def IMGU_iff_Idem_and_MGU unify_computes_MGU unify_gives_Idem
unify_gives_minimal_domain unify_gives_minimal_range)
subsection ‹Congruences›
text ‹We now define the notion of a congruence on ground terms, i.e., an equivalence relation
that is closed under contextual embedding.›
type_synonym 'a binary_relation_on_trms = "'a trm ⇒ 'a trm ⇒ bool"
definition reflexive :: "'a binary_relation_on_trms ⇒ bool"
where
"(reflexive x) = (∀y. (x y y))"
definition symmetric :: "'a binary_relation_on_trms ⇒ bool"
where
"(symmetric x) = (∀y. ∀z. ((x y z) = (x z y)))"
definition transitive :: "'a binary_relation_on_trms ⇒ bool"
where
"(transitive x) = (∀y. ∀z. ∀u. (x y z) ⟶ (x z u) ⟶ (x y u))"
definition equivalence_relation :: "'a binary_relation_on_trms ⇒ bool"
where
"(equivalence_relation x) = ((reflexive x) ∧ (symmetric x) ∧ (transitive x))"
definition compatible_with_structure :: "('a binary_relation_on_trms) ⇒ bool"
where
"(compatible_with_structure x) = (∀t1 t2 s1 s2.
(x t1 s1) ⟶ (x t2 s2) ⟶ (x (Comb t1 t2) (Comb s1 s2)))"
definition congruence :: "'a binary_relation_on_trms ⇒ bool"
where
"(congruence x) = ((equivalence_relation x) ∧ (compatible_with_structure x))"
lemma replacement_preserves_congruences :
shows "⋀ t s. (congruence I) ⟹ (I (subst u σ) (subst v σ))
⟹ subterm t p u ⟹ replace_subterm t p v s
⟹ (I (subst t σ) (subst s σ))"
proof (induction p)
case Nil
from ‹subterm t Nil u› have "t = u" by auto
from ‹replace_subterm t Nil v s› have "s = v" by auto
from ‹t = u› and ‹s = v› and ‹(I (subst u σ) (subst v σ))›
show ?case by auto
next case (Cons i q)
from ‹subterm t (i # q) u› obtain t1 t2 where
"t = (Comb t1 t2)" using subterm.elims(2) by blast
have "i = Left ∨ i = Right" using indices.exhaust by blast
then show "I (subst t σ) (subst s σ)"
proof
assume "i = Left"
from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) u›
have "subterm t1 q u" by auto
from ‹i = Left› and ‹t = Comb t1 t2› and ‹replace_subterm t (i # q) v s›
obtain t1' where "replace_subterm t1 q v t1'" and "s = Comb t1' t2" by auto
from ‹congruence I› and ‹(I (subst u σ) (subst v σ))›
and ‹subterm t1 q u› and ‹replace_subterm t1 q v t1'› have
"I (subst t1 σ) (subst t1' σ)" using Cons.IH Cons.prems(1) by blast
from ‹congruence I› have "I (subst t2 σ) (subst t2 σ)"
unfolding congruence_def equivalence_relation_def reflexive_def by auto
from ‹I (subst t1 σ) (subst t1' σ)›
and ‹I (subst t2 σ) (subst t2 σ)›
and ‹congruence I› and ‹t = (Comb t1 t2)› and ‹s = (Comb t1' t2)›
show "I (subst t σ) (subst s σ)"
unfolding congruence_def compatible_with_structure_def by auto
next
assume "i = Right"
from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) u›
have "subterm t2 q u" by auto
from ‹i = Right› and ‹t = Comb t1 t2› and ‹replace_subterm t (i # q) v s›
obtain t2' where "replace_subterm t2 q v t2'" and "s = Comb t1 t2'" by auto
from ‹congruence I› and ‹(I (subst u σ) (subst v σ))›
and ‹subterm t2 q u› and ‹replace_subterm t2 q v t2'› have
"I (subst t2 σ) (subst t2' σ)" using Cons.IH Cons.prems(1) by blast
from ‹congruence I› have "I (subst t1 σ) (subst t1 σ)"
unfolding congruence_def equivalence_relation_def reflexive_def by auto
from ‹I (subst t2 σ) (subst t2' σ)›
and ‹I (subst t1 σ) (subst t1 σ)›
and ‹congruence I› and ‹t = (Comb t1 t2)› and ‹s = (Comb t1 t2')›
show "I (subst t σ) (subst s σ)"
unfolding congruence_def compatible_with_structure_def by auto
qed
qed
definition equivalent_on
where "equivalent_on σ η V I = (∀x ∈ V.
(I (subst (Var x) σ) ( (subst (Var x) η))))"
lemma equivalent_on_term:
assumes "congruence I"
shows "⋀ σ η. equivalent_on σ η (vars_of t) I ⟹ (I (subst t σ) (subst t η))"
proof (induction t)
case (Var x)
from this show "(I (subst (Var x) σ) (subst (Var x) η))"
unfolding equivalent_on_def by auto
next case (Const x)
from assms(1) show "(I (subst (Const x) σ) (subst (Const x) η))"
unfolding congruence_def equivalence_relation_def reflexive_def by auto
next case (Comb t1 t2)
from this assms(1) show ?case unfolding equivalent_on_def
unfolding congruence_def compatible_with_structure_def by auto
qed
subsection ‹Renamings›
text ‹We define the usual notion of a renaming. We show that fresh renamings always exist
(provided the set of variables is infinite) and that renamings admit inverses.›
definition renaming
where
"renaming σ V = (∀x ∈ V. (is_a_variable (subst (Var x) σ))
∧ (∀ x y. ((x ∈ V) ⟶ (y ∈ V) ⟶ x ≠ y ⟶ (subst (Var x) σ) ≠ (subst (Var y) σ))))"
lemma renamings_admit_inverse:
shows "finite V ⟹ renaming σ V ⟹ ∃ θ. (∀ x ∈ V. (subst (subst (Var x) σ ) θ) = (Var x))
∧ (∀ x. (x ∉ (subst_codomain σ V) ⟶ (subst (Var x) θ) = (Var x)))
∧ (∀x. is_a_variable (subst (Var x) θ))"
proof (induction rule: finite.induct)
case emptyI
let ?θ = "[]"
have i: "(∀ x ∈ {}. (subst (subst (Var x) σ ) ?θ) = (Var x))" by auto
have ii: "(∀ x. (x ∉ (subst_codomain σ {}) ⟶ (subst (Var x) ?θ) = (Var x)))" by auto
have iii: "∀x. is_a_variable (subst (Var x) ?θ)" by simp
from i ii iii show ?case by metis
next
fix A :: "'a set" and a::'a
assume "finite A"
assume hyp_ind: "renaming σ A ⟹ ∃ θ. (∀ x ∈ A. (subst (subst (Var x) σ ) θ) = (Var x))
∧ (∀ x. (x ∉ (subst_codomain σ A) ⟶ (subst (Var x) θ) = (Var x)))
∧ (∀x. is_a_variable (subst (Var x) θ))"
show "renaming σ (insert a A) ⟹ ∃ θ. (∀ x ∈ (insert a A). (subst (subst (Var x) σ ) θ) = (Var x))
∧ (∀ x. (x ∉ (subst_codomain σ (insert a A)) ⟶ (subst (Var x) θ) = (Var x)))
∧ (∀x. is_a_variable (subst (Var x) θ))"
proof -
assume "renaming σ (insert a A)"
show "∃ θ. (∀ x ∈ (insert a A). (subst (subst (Var x) σ ) θ) = (Var x))
∧ (∀ x. (x ∉ (subst_codomain σ (insert a A)) ⟶ (subst (Var x) θ) = (Var x)))
∧ (∀x. is_a_variable (subst (Var x) θ))"
proof (cases)
assume "a ∈ A"
from this have "insert a A = A" by auto
from this and ‹renaming σ (insert a A)› hyp_ind show ?thesis by metis
next assume "a ∉ A"
from ‹renaming σ (insert a A)› have "renaming σ A" unfolding renaming_def by blast
from this and hyp_ind obtain θ where i: "(∀ x ∈ A. (subst (subst (Var x) σ ) θ) = (Var x))" and
ii: "(∀ x. (x ∉ (subst_codomain σ A) ⟶ (subst (Var x) θ) = (Var x)))" and
iii: "∀x. is_a_variable (Var x ⊲ θ)" by metis
from ‹renaming σ (insert a A)› have "is_a_variable (subst (Var a) σ)" unfolding renaming_def by blast
from this obtain b where "(subst (Var a) σ) = (Var b)" using is_a_variable.elims(2) by auto
let ?η = "(b,(Var a)) # θ"
have i': "(∀ x ∈ (insert a A). (subst (subst (Var x) σ ) ?η) = (Var x))"
proof
fix x assume "x ∈ (insert a A)"
show "(subst (subst (Var x) σ ) ?η) = (Var x)"
proof (cases)
assume "x = a"
from this
have "(subst (Var b) ( (b,(Var a)) # Nil)) = (Var a)"
by simp
have "b ∉ (subst_codomain σ A)"
proof
assume "b ∈ (subst_codomain σ A)"
from this have "∃y. (subst (Var y) σ) = (Var b) ∧ (y ∈ A)" unfolding subst_codomain_def
by force
then obtain a' where "a' ∈ A" and "subst (Var a') σ = (Var b)"
by metis
from ‹a' ∈ A› and ‹a ∉ A› have "a ≠ a'" by auto
have "a ∈ (insert a A)" by auto
from ‹a ≠ a'› and ‹a' ∈ A› and ‹a ∈ (insert a A)› and ‹renaming σ (insert a A)›
have "(subst (Var a) σ ≠ (subst (Var a') σ))"
unfolding renaming_def by blast
from this and ‹subst (Var a') σ = (Var b)› ‹(subst (Var a) σ) = (Var b)›
show False by auto
qed
from this and ii have "(subst (Var b) θ) = (Var b)" by auto
from this and ‹x = a› ‹(subst (Var a) σ) = (Var b)›
‹(subst (Var b) ( (b,(Var a)) # Nil)) = (Var a)›
show "(subst (subst (Var x) σ ) ?η) = (Var x)"
by simp
next assume "x ≠ a"
from this and ‹x ∈ insert a A› obtain "x ∈ A" by auto
from this i have "(subst (subst (Var x) σ ) θ) = (Var x)"
by auto
then show "(subst (subst (Var x) σ ) ?η) = (Var x)"
by (metis ‹subst (Var a) σ = Var b› ‹renaming σ (insert a A)›
‹x ∈ insert a A› ‹x ≠ a› insertI1 is_a_variable.elims(2)
occs.simps(1) renaming_def repl_invariance vars_iff_occseq)
qed
qed
have ii': "(∀ x. (x ∉ (subst_codomain σ (insert a A)) ⟶ (subst (Var x) ?η) = (Var x)))"
proof ((rule allI),(rule impI))
fix x assume "x ∉ subst_codomain σ (insert a A)"
from this ‹(subst (Var a) σ) = (Var b)› have "x≠ b" unfolding subst_codomain_def
by auto
from this have "(subst (Var x) ?η) = (subst (Var x) θ)" by auto
from ‹x ∉ subst_codomain σ (insert a A)› have "x ∉ (subst_codomain σ A)" unfolding subst_codomain_def
by auto
from this and ii have "(subst (Var x) θ) = (Var x)" by auto
from ‹(subst (Var x) ?η) = (subst (Var x) θ)›
and ‹(subst (Var x) θ) = (Var x)› show "(subst (Var x) ?η) = (Var x)"
by auto
qed
have iii': "∀x. is_a_variable (subst (Var x) ?η)"
using iii by auto
from i' ii' iii' show ?thesis by auto
qed
qed
qed
lemma renaming_exists:
assumes "¬ finite (Vars :: ('a set))"
shows "finite V ⟹ (∀V'::'a set. finite V' ⟶ (∃η. ((renaming η V) ∧ ((subst_codomain η V) ∩ V') = {})))"
proof (induction rule: finite.induct)
case emptyI
let ?η = "[]"
show ?case unfolding renaming_def subst_codomain_def by auto
next
fix A :: "'a set" and a::'a
assume "finite A"
assume hyp_ind: "∀V' :: 'a set. finite V' ⟶ (∃η. renaming η A ∧ subst_codomain η A ∩ V' = {})"
show "∀V':: 'a set. finite V' ⟶ (∃η. renaming η (insert a A) ∧ subst_codomain η (insert a A) ∩ V' = {})"
proof ((rule allI),(rule impI))
fix V':: "'a set" assume "finite V'"
from this have "finite (insert a V')" by auto
from this and hyp_ind obtain η where "renaming η A" and "(subst_codomain η A) ∩ (insert a V') = {}" by metis
from ‹finite A› have "finite (subst_codomain η A)"
using subst_codomain_is_finite by auto
from this ‹finite V'› have "finite (V' ∪ (subst_codomain η A))" by auto
from this have "finite ((insert a V') ∪ (subst_codomain η A))" by auto
from this ‹¬ finite Vars› have "¬ (Vars ⊆ ((insert a V') ∪ (subst_codomain η A)))" using rev_finite_subset
by metis
from this obtain nv where "nv ∈ Vars" and "nv ∉ (insert a V')" and "nv ∉ (subst_codomain η A)" by auto
let ?η = "(a,(Var nv)) # η"
have i: "(∀x ∈ (insert a A). (is_a_variable (subst (Var x) ?η)))"
proof (rule ccontr)
assume "¬ (∀x ∈ (insert a A). (is_a_variable (subst (Var x) ?η)))"
then obtain x where "x ∈ (insert a A)" and "¬is_a_variable (subst (Var x) ?η)"
by auto
from ‹¬is_a_variable (subst (Var x) ?η)› have "x ≠ a" by auto
from this and ‹x ∈ (insert a A)› have "x ∈ A" by auto
from ‹x ≠ a› have "(subst (Var x) ?η) = (subst (Var x) η)" by auto
from ‹renaming η A› and ‹x ∈ A› have "is_a_variable (subst (Var x) η)"
unfolding renaming_def by metis
from this and ‹¬is_a_variable (subst (Var x) ?η)›
‹(subst (Var x) ?η) = (subst (Var x) η)› show False by auto
qed
have ii: "(∀ x y. ((x ∈ (insert a A)) ⟶ (y ∈ (insert a A)) ⟶ x ≠ y
⟶ (subst (Var x) ?η) ≠ (subst (Var y) ?η)))"
proof (rule ccontr)
assume "¬(∀ x y. ((x ∈ (insert a A)) ⟶ (y ∈ (insert a A)) ⟶ x ≠ y
⟶ (subst (Var x) ?η) ≠ (subst (Var y) ?η)))"
from this obtain x y where "x ∈ insert a A" "y ∈ insert a A" "x ≠ y"
"(subst (Var x) ?η) = (subst (Var y) ?η)" by blast
from i obtain y' where "(subst (Var y) ?η) = (Var y')"
using is_a_variable.simps using ‹y ∈ insert a A› is_a_variable.elims(2) by auto
from i obtain x' where "(subst (Var x) ?η) = (Var x')"
using is_a_variable.simps using ‹x ∈ insert a A› is_a_variable.elims(2) by auto
from ‹(subst (Var x) ?η) = (Var x')› ‹(subst (Var y) ?η) = (Var y')›
‹(subst (Var x) ?η) = (subst (Var y) ?η)› have "x' = y'" by auto
have "x ≠ a"
proof
assume "x = a"
from this and ‹x ≠ y› and ‹y ∈ insert a A› have "y ∈ A" by auto
from this and ‹x ≠ y› and ‹x = a› and ‹(subst (Var y) ?η) = (Var y')›
have "y' ∈ (subst_codomain η A)" unfolding subst_codomain_def by auto
from ‹x = a› and ‹(subst (Var x) ?η) = (Var x')› have "x' = nv" by auto
from this and ‹y' ∈ (subst_codomain η A)› and ‹x' = y'› and ‹nv ∉ (subst_codomain η A)›
show False by auto
qed
from this and ‹x ∈ insert a A› have "x ∈ A" and
"(subst (Var x) ?η) = (subst (Var x) η)" by auto
have "y ≠ a"
proof
assume "y = a"
from this and ‹x ≠ y› and ‹x ∈ insert a A› have "x ∈ A" by auto
from this and ‹x ≠ y› and ‹y = a› and ‹(subst (Var x) ?η) = (Var x')›
have "x' ∈ (subst_codomain η A)" unfolding subst_codomain_def by auto
from ‹y = a› and ‹(subst (Var y) ?η) = (Var y')› have "y' = nv" by auto
from this and ‹x' ∈ (subst_codomain η A)› and ‹x' = y'› and ‹nv ∉ (subst_codomain η A)›
show False by auto
qed
from this and ‹y ∈ insert a A› have "y ∈ A" and
"(subst (Var y) ?η) = (subst (Var y) η)" by auto
from ‹(subst (Var x) ?η) = (subst (Var x) η)›
‹(subst (Var y) ?η) = (subst (Var y) η)›
‹(subst (Var x) ?η) = (subst (Var y) ?η)›
have "(subst (Var x) η) = (subst (Var y) η)" by auto
from this and ‹x ∈ A› and ‹y ∈ A›and ‹renaming η A› and ‹x ≠ y› show False
unfolding renaming_def by metis
qed
from i ii have "renaming ?η (insert a A)" unfolding renaming_def by auto
have "((subst_codomain ?η (insert a A)) ∩ V') = {}"
proof (rule ccontr)
assume "(subst_codomain ?η (insert a A)) ∩ V' ≠ {}"
then obtain x where "x ∈ (subst_codomain ?η (insert a A))" and "x ∈ V'" by auto
from ‹x ∈ (subst_codomain ?η (insert a A))› obtain x' where "x' ∈ (insert a A)"
and "subst (Var x') ?η = (Var x)" unfolding subst_codomain_def by blast
have "x' ≠ a"
proof
assume "x' = a"
from this and ‹subst (Var x') ?η = (Var x)› have "x = nv" by auto
from this and ‹x ∈ V'› and ‹nv ∉ (insert a V')› show False by auto
qed
from this and ‹x' ∈ (insert a A)› have "x' ∈ A" by auto
from ‹x' ≠ a› and ‹subst (Var x') ?η = (Var x)› have
"(Var x) = (subst (Var x') η)" by auto
from this and ‹x' ∈ A› have "x ∈ subst_codomain η A" unfolding subst_codomain_def by auto
from ‹x ∈ subst_codomain η A› and ‹(subst_codomain η A) ∩ (insert a V') = {}› and ‹x ∈ V'›
show False by auto
qed
from this and ‹renaming ?η (insert a A)›
show "∃η. renaming η (insert a A) ∧ subst_codomain η (insert a A) ∩ V' = {}" by auto
qed
qed
end