Theory Functional_Substitution_Example
theory Functional_Substitution_Example
imports Functional_Substitution Substitution_First_Order_Term
begin
text ‹A selection of substitution properties for terms.›
locale term_subst_properties =
base_functional_substitution +
finite_variables
global_interpretation term_subst: term_subst_properties where
subst = subst_apply_term and id_subst = Var and comp_subst = subst_compose and
vars = "vars_term :: ('f, 'v) term ⇒ 'v set"
rewrites "⋀t. term_subst.is_ground t ⟷ ground t"
text ‹"rewrites" enables us to use our own equivalent definitions.›
proof unfold_locales
fix t :: "('f, 'v) term" and σ τ :: "('f, 'v) subst"
assume "⋀x. x ∈ vars_term t ⟹ σ x = τ x"
then show "t ⋅ σ = t ⋅ τ"
by(rule term_subst_eq)
next
fix t :: "('f, 'v) term"
show "finite (vars_term t)"
by simp
next
fix t :: "('f, 'v) term" and ρ :: "('f, 'v) subst"
show "vars_term (t ⋅ ρ) = ⋃ (vars_term ` ρ ` vars_term t)"
using vars_term_subst.
next
show "∃t. vars_term t = {}"
by(rule exI[of _ "Fun (SOME f. True) []"]) auto
next
fix x :: 'v
show "vars_term (Var x) = {x}"
by simp
next
fix σ σ' :: "('f, 'v) subst" and x
show "(σ ∘⇩s σ') x = σ x ⋅ σ'"
using subst_compose.
next
fix t :: "('f, 'v) term"
show "is_ground_trm t = ground t"
by (induction t) auto