Theory Abstract_Substitution.Based_Substitution_Lifting

theory Based_Substitution_Lifting ✐‹contributor ‹Balazs Toth›› 
  imports 
    Based_Substitution
    Substitution_Lifting
begin

section ‹Lifting of based substitutions›

locale based_substitution_lifting =
  substitution_lifting +
  base: base_substitution where subst = base_subst and vars = base_vars +
  sub: based_substitution where subst = sub_subst and vars = sub_vars
begin

sublocale based_substitution where subst = subst and vars = vars
proof unfold_locales
  fix expr ρ

  show "vars (expr ⋅ ρ) = ⋃ (base_vars ` (λx. x ⋅v ρ) ` vars expr)"
    using sub.vars_subst
    unfolding subst_def vars_def
    by simp
qed simp

end

subsection ‹Lifting of properties›

locale variables_in_base_imgu_lifting =
  based_substitution_lifting +
  sub: variables_in_base_imgu where vars = sub_vars and subst = sub_subst
begin

sublocale variables_in_base_imgu where subst = subst and vars = vars
proof unfold_locales
  fix expr μ XX
  assume imgu: "base.is_imgu μ XX" "finite XX" "∀X ∈ XX. finite X"

  show "vars (expr ⋅ μ) ⊆ vars expr ∪ ⋃ (base_vars ` ⋃ XX)"
    using sub.variables_in_base_imgu[OF imgu]
    unfolding vars_def subst_def to_set_map
    by auto
qed

end

end