Theory 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 and is_ground = base_is_ground +
  sub: based_substitution where
  subst = sub_subst and vars = sub_vars and is_ground = sub_is_ground
begin

sublocale based_substitution where subst = subst and vars = vars and is_ground = is_ground
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
next
  fix expr γ 
  assume "is_ground (expr ⋅ γ)" 

  then show "∀x∈vars expr. base_is_ground (x ⋅v γ)"
    unfolding is_ground_def vars_def
    using sub.variable_grounding
    by auto
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 and is_ground = sub_is_ground
begin

sublocale variables_in_base_imgu where subst = subst and vars = vars and is_ground = is_ground
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

locale based_subst_update_lifting =
  based_substitution_lifting +
  subst_update_lifting +
  sub: based_subst_update where
  vars = sub_vars and subst = sub_subst and is_ground = sub_is_ground
begin

sublocale based_subst_update where subst = subst and vars = vars and is_ground = is_ground
proof unfold_locales
  fix update expr γ x
  assume "base_is_ground update" "is_ground (expr ⋅ γ)" "x ∈ vars expr"
  
  then show "is_ground (expr ⋅ γ⟦x := update⟧)"
    using sub.ground_subst_update_in_vars
    unfolding is_ground_def subst_def
    by auto
qed

end

end