Theory Abstract_Substitution.Functional_Substitution_Lifting

theory Functional_Substitution_Lifting ✐‹contributor ‹Balazs Toth››
  imports Functional_Substitution Natural_Magma_Functor
begin

locale functional_substitution_lifting =
  sub: functional_substitution where subst = sub_subst and vars = sub_vars +
  natural_functor where map = map and to_set = to_set
  for
    sub_vars :: "'sub ⇒ 'var set" and
    sub_subst :: "'sub ⇒ ('var ⇒ 'base) ⇒ 'sub" and
    map :: "('sub ⇒ 'sub) ⇒ 'expr ⇒ 'expr" and
    to_set :: "'expr ⇒ 'sub set"
begin

definition vars :: "'expr ⇒ 'var set" where
  "vars expr ≡ ⋃ (sub_vars ` to_set expr)"

notation sub_subst (infixl "⋅⇩s" 70)

definition subst :: "'expr ⇒ ('var ⇒ 'base) ⇒ 'expr" (infixl "⋅" 70) where
  "expr ⋅ σ ≡ map (λsub. sub ⋅⇩s σ) expr"

lemma map_id_cong [simp]:
  assumes "⋀sub. sub ∈ to_set expr ⟹ f sub = sub"
  shows "map f expr = expr"
  using assms
  by simp

lemma to_set_map_not_ident:
  assumes "sub ∈ to_set expr" "f sub ∉ to_set expr"
  shows "map f expr ≠ expr"
  using assms
  by (metis rev_image_eqI to_set_map)

lemma subst_in_to_set_subst [intro]:
  assumes "sub ∈ to_set expr"
  shows "sub ⋅⇩s σ ∈ to_set (expr ⋅ σ)"
  unfolding subst_def to_set_map
  using assms
  by simp

sublocale functional_substitution where subst = "(⋅)" and vars = vars
proof unfold_locales
  fix expr σ⇩1 σ⇩2

  show "expr ⋅ (σ⇩1 ⊙ σ⇩2) = expr ⋅ σ⇩1 ⋅ σ⇩2"
    unfolding subst_def map_comp comp_apply sub.subst_comp_subst
    ..
next
  fix expr
  show "expr ⋅ id_subst = expr"
    using map_ident
    unfolding subst_def sub.subst_id_subst.
next
  fix expr
  assume "vars expr = {}"
  then show "∀σ. expr ⋅ σ = expr"
    unfolding vars_def subst_def
    by simp
next
  fix expr and σ⇩1 σ⇩2 :: "'var ⇒ 'base"
  assume "⋀var. var ∈ vars expr ⟹ σ⇩1 var = σ⇩2 var"

  then show "expr ⋅ σ⇩1 = expr ⋅ σ⇩2"
    unfolding vars_def subst_def
    using map_cong sub.subst_eq
    by (meson UN_I)
qed

lemma ground_subst_iff_sub_ground_subst [simp]: "is_ground_subst γ ⟷ sub.is_ground_subst γ"
proof(unfold is_ground_subst_def sub.is_ground_subst_def, intro iffI allI)
  fix sub
  assume all_ground: "∀expr. is_ground (expr ⋅ γ)"
  show "sub.is_ground (sub ⋅⇩s γ)"
  proof(rule ccontr)
    assume sub_not_ground: "¬sub.is_ground (sub ⋅⇩s γ)"

    then obtain expr where "sub ∈ to_set expr"
      using exists_functor by blast

    then have "¬is_ground (expr ⋅ γ)"
      using sub_not_ground to_set_map
      unfolding subst_def vars_def
      by auto

    then show False
      using all_ground
      by blast
  qed
next
  fix expr
  assume "∀sub. sub.is_ground (sub ⋅⇩s γ)"

  then show "is_ground (expr ⋅ γ)"
    unfolding vars_def subst_def
    using to_set_map
    by simp
qed

lemma to_set_is_ground [intro]:
  assumes "sub ∈ to_set expr" "is_ground expr"
  shows "sub.is_ground sub"
  using assms
  by (simp add: vars_def)

lemma to_set_is_ground_subst:
  assumes "sub ∈ to_set expr" "is_ground (expr ⋅ γ)"
  shows "sub.is_ground (sub ⋅⇩s γ)"
  using assms
  by (meson subst_in_to_set_subst to_set_is_ground)

lemma subst_empty:
  assumes "to_set expr' = {}"
  shows "expr ⋅ σ = expr' ⟷ expr = expr'"
  using assms map_id_cong to_set_map
  unfolding subst_def
  by (metis empty_iff image_is_empty)

lemma empty_is_ground:
  assumes "to_set expr = {}"
  shows "is_ground expr"
  using assms
  by (simp add: vars_def)

lemma to_set_image: "to_set (expr ⋅ σ) = (λa. a ⋅⇩s σ) ` to_set expr"
  unfolding subst_def to_set_map..

lemma to_set_subset_vars_subset:
  assumes "to_set expr ⊆ to_set expr'"
  shows "vars expr ⊆ vars expr'"
  using assms
  unfolding vars_def
  by blast

lemma to_set_subset_is_ground:
  assumes "to_set expr' ⊆ to_set expr" "is_ground expr"
  shows "is_ground expr'"
  using assms to_set_subset_vars_subset by blast

end

locale based_functional_substitution_lifting =
  functional_substitution_lifting +
  base: base_functional_substitution where subst = base_subst and vars = base_vars +
  sub: based_functional_substitution where subst = sub_subst and vars = sub_vars
begin

sublocale based_functional_substitution where subst = subst and vars = vars
proof unfold_locales
  fix γ

  show "is_ground_subst γ = base.is_ground_subst γ"
    using ground_subst_iff_sub_ground_subst sub.ground_subst_iff_base_ground_subst
    by blast
next
  fix expr ρ

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

end

locale finite_variables_lifting =
  sub: finite_variables where vars = "sub_vars :: 'sub ⇒ 'var set" and subst = sub_subst +
  finite_natural_functor where to_set = "to_set :: 'expr ⇒ 'sub set" +
  functional_substitution_lifting
begin

abbreviation to_fset :: "'expr ⇒ 'sub fset" where
  "to_fset expr ≡ Abs_fset (to_set expr)"

sublocale finite_variables where vars = vars and subst = subst
  by unfold_locales (auto simp: vars_def finite_to_set)

lemma fset_to_fset [simp]: "fset (to_fset expr) = to_set expr"
  using Abs_fset_inverse finite_to_set
  by blast

lemma to_fset_map: "to_fset (map f expr) = f |`| to_fset expr"
  using to_set_map
  by (metis fset.set_map fset_inverse fset_to_fset)

lemma to_fset_is_ground_subst:
  assumes "sub |∈| to_fset expr" "is_ground (subst expr γ)"
  shows "sub.is_ground (sub ⋅⇩s γ)"
  using assms
  by (simp add: to_set_is_ground_subst)

end

locale renaming_variables_lifting =
  functional_substitution_lifting +
  sub: renaming_variables where vars = sub_vars and subst = sub_subst
begin

sublocale renaming_variables where subst = subst and vars = vars
proof unfold_locales
  fix expr ρ
  assume "sub.is_renaming ρ"

  then show "vars (expr ⋅ ρ) = rename ρ ` vars expr"
    using sub.rename_variables
    unfolding vars_def subst_def to_set_map
    by fastforce
qed (rule sub.is_renaming_iff)

end

locale based_renaming_variables_lifting = 
  renaming_variables_lifting +
  based_functional_substitution_lifting +
  base: renaming_variables where vars = base_vars and subst = base_subst

locale variables_in_base_imgu_lifting =
  based_functional_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 μ unifications
  assume imgu:
    "base.is_imgu μ unifications"
    "finite unifications"
    "∀unification ∈ unifications. finite unification"

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

end

locale grounding_lifting =
  functional_substitution_lifting where sub_vars = sub_vars and sub_subst = sub_subst and
  map = map +
  sub: grounding where vars = sub_vars and subst = sub_subst and to_ground = sub_to_ground and
  from_ground = sub_from_ground +
  natural_functor_conversion where map = map and map_to = to_ground_map and
  map_from = from_ground_map and map' = ground_map and to_set' = to_set_ground
  for
    sub_to_ground :: "'sub ⇒ 'sub⇩G" and
    sub_from_ground :: "'sub⇩G ⇒ 'sub" and
    sub_vars :: "'sub ⇒ 'var set" and
    sub_subst :: "'sub ⇒ ('var ⇒ 'base) ⇒ 'sub" and
    map :: "('sub ⇒ 'sub) ⇒ 'expr ⇒ 'expr" and
    to_ground_map :: "('sub ⇒ 'sub⇩G) ⇒ 'expr ⇒ 'expr⇩G" and
    from_ground_map :: "('sub⇩G ⇒ 'sub) ⇒ 'expr⇩G ⇒ 'expr" and
    ground_map :: "('sub⇩G ⇒ 'sub⇩G) ⇒ 'expr⇩G ⇒ 'expr⇩G" and
    to_set_ground :: "'expr⇩G ⇒ 'sub⇩G set"
begin

definition to_ground :: "'expr ⇒ 'expr⇩G" where
  "to_ground expr ≡ to_ground_map sub_to_ground expr"

definition from_ground :: "'expr⇩G ⇒ 'expr" where
  "from_ground expr⇩G ≡ from_ground_map sub_from_ground expr⇩G"

sublocale grounding
  where vars = vars and subst = subst and to_ground = to_ground and from_ground = from_ground
proof unfold_locales

  {
    fix expr

    assume "is_ground expr"

    then have "∀sub∈to_set expr. sub ∈ range sub_from_ground"
      by (simp add: sub.is_ground_iff_range_from_ground vars_def)

    then have "∀sub∈to_set expr. ∃sub⇩G. sub_from_ground sub⇩G = sub"
      by fast

    then have "∃expr⇩G. from_ground expr⇩G = expr"
      unfolding from_ground_def
      by (metis conversion_map_comp map_id_cong)

    then have "expr ∈ range from_ground"
      unfolding from_ground_def
      by blast
  }

  moreover {
    fix expr var

    assume "var ∈ vars (from_ground expr)"

    then have False
      unfolding vars_def from_ground_def
      using sub.ground_is_ground to_set_map_from by auto
  }

  ultimately show "{expr. is_ground expr} = range from_ground"
    by blast
next
  fix expr⇩G
  show "to_ground (from_ground expr⇩G) = expr⇩G"
    unfolding from_ground_def to_ground_def
    by simp
qed

lemma to_set_from_ground: "to_set (from_ground expr) = sub_from_ground ` (to_set_ground expr)"
  unfolding from_ground_def
  by simp

lemma sub_in_ground_is_ground:
  assumes "sub ∈ to_set (from_ground expr)"
  shows "sub.is_ground sub"
  using assms
  by (simp add: to_set_is_ground)

lemma ground_sub_in_ground:
  "sub ∈ to_set_ground expr ⟷ sub_from_ground sub ∈ to_set (from_ground expr)"
  by (simp add: inj_image_mem_iff sub.inj_from_ground to_set_from_ground)

lemma ground_sub:
  "(∀sub ∈ to_set (from_ground expr⇩G). P sub) ⟷
   (∀sub⇩G ∈ to_set_ground expr⇩G. P (sub_from_ground sub⇩G))"
  by (simp add: to_set_from_ground)

end

locale all_subst_ident_iff_ground_lifting =
  finite_variables_lifting where map = map +
  sub: all_subst_ident_iff_ground where subst = sub_subst and vars = sub_vars
for map :: "('sub ⇒ 'sub) ⇒ 'expr ⇒ 'expr"
begin

sublocale all_subst_ident_iff_ground where subst = subst and vars = vars
proof unfold_locales
  fix expr

  show "is_ground expr ⟷ (∀σ. expr ⋅ σ = expr)"
  proof(rule iffI allI)
    assume "is_ground expr"
    then show "∀σ. expr ⋅ σ = expr"
      by simp
  next
    assume all_subst_ident: "∀σ. expr ⋅ σ = expr"

    show "is_ground expr"
    proof(rule ccontr)
      assume "¬is_ground expr"

      then obtain sub where sub: "sub ∈ to_set expr" "¬sub.is_ground sub"
        unfolding vars_def
        by blast

      then obtain σ where "sub ⋅⇩s σ ≠ sub" and "sub ⋅⇩s σ ∉ to_set expr"
        using sub.exists_non_ident_subst finite_to_set
        by blast

      then show False
        using sub subst_in_to_set_subst all_subst_ident
        by metis
    qed
  qed
next
  fix expr :: 'expr and S :: "'expr set"

  assume finite: "finite S" and not_ground: "¬is_ground expr"

  then have finite_subs: "finite (⋃(to_set ` insert expr S))"
    using finite_to_set by blast

  obtain sub where sub: "sub ∈ to_set expr" and sub_not_ground: "¬sub.is_ground sub"
    using not_ground
    unfolding vars_def
    by blast

  obtain σ where σ_not_ident: "sub ⋅⇩s σ ≠ sub" "sub ⋅⇩s σ ∉ ⋃ (to_set ` insert expr S)"
    using sub.exists_non_ident_subst[OF finite_subs sub_not_ground]
    by blast

  then have "expr ⋅ σ ≠ expr"
    using sub
    unfolding subst_def
    by (simp add: to_set_map_not_ident)

  moreover have "expr ⋅ σ ∉ S"
    using σ_not_ident(2) sub to_set_map
    unfolding subst_def
    by auto

  ultimately show "∃σ. expr ⋅ σ ≠ expr ∧ expr ⋅ σ ∉ S"
    by blast
qed

end

locale natural_magma_functional_substitution_lifting =
  functional_substitution_lifting + natural_magma
begin

lemma vars_add [simp]:
  "vars (add sub expr) = sub_vars sub ∪ vars expr"
  unfolding vars_def
  using to_set_add by auto

lemma vars_plus [simp]:
  "vars (plus expr expr') = vars expr ∪ vars expr'"
  unfolding vars_def
  by simp

lemma is_ground_add [simp]:
  "is_ground (add sub expr) ⟷ sub.is_ground sub ∧ is_ground expr"
  by simp

end

locale natural_magma_functor_functional_substitution_lifting =
  natural_magma_functional_substitution_lifting + natural_magma_functor
begin

lemma add_subst [simp]:
  "(add sub expr) ⋅ σ = add (sub ⋅⇩s σ) (expr ⋅ σ)"
  unfolding subst_def
  using map_add
  by simp

lemma plus_subst [simp]: "(plus expr expr') ⋅ σ = plus (expr ⋅ σ) (expr' ⋅ σ)"
  unfolding subst_def
  using map_plus
  by simp

end

locale natural_magma_grounding_lifting =
  grounding_lifting +
  natural_magma_functional_substitution_lifting +
  ground: natural_magma where
  to_set = to_set_ground and plus = plus_ground and wrap = wrap_ground and add = add_ground
for plus_ground wrap_ground add_ground +
assumes
  to_ground_plus [simp]:
   "⋀expr expr'. to_ground (plus expr expr') = plus_ground (to_ground expr) (to_ground expr')" and
  wrap_from_ground: "⋀sub. from_ground (wrap_ground sub) = wrap (sub_from_ground sub)" and
  wrap_to_ground: "⋀sub. to_ground (wrap sub) = wrap_ground (sub_to_ground sub)"
begin

lemma from_ground_plus [simp]:
  "from_ground (plus_ground expr expr') = plus (from_ground expr) (from_ground expr')"
  using to_ground_plus
  by (metis Un_empty_left from_ground_inverse ground_is_ground to_ground_inverse vars_plus)

lemma from_ground_add [simp]:
  "from_ground (add_ground sub expr) = add (sub_from_ground sub) (from_ground expr)"
  unfolding ground.add_def add_def
  using from_ground_plus
  by (simp add: wrap_from_ground)

lemma to_ground_add [simp]:
  "to_ground (add sub expr) = add_ground (sub_to_ground sub) (to_ground expr)"
  unfolding ground.add_def add_def
  using from_ground_add wrap_to_ground
  by simp

lemma ground_add:
  assumes "from_ground expr = add sub expr'"
  shows "expr = add_ground (sub_to_ground sub) (to_ground expr')"
  using assms
  by (metis from_ground_inverse to_ground_add)

end

locale natural_magma_with_empty_grounding_lifting =
  natural_magma_grounding_lifting +
  natural_magma_with_empty +
  ground: natural_magma_with_empty where 
  to_set = to_set_ground and plus = plus_ground and wrap = wrap_ground and add = add_ground and 
  empty = empty_ground
for empty_ground +
assumes to_ground_empty [simp]: "to_ground empty = empty_ground"
begin

lemmas empty_magma_is_ground [simp] = empty_is_ground[OF to_set_empty]

lemmas magma_subst_empty [simp] =
  subst_ident_if_ground[OF empty_magma_is_ground]
  subst_empty[OF to_set_empty]

lemma from_ground_empty [simp]: "from_ground empty_ground = empty"
  using to_ground_inverse[OF empty_magma_is_ground]
  by simp

lemma to_ground_empty' [simp]: "to_ground expr = empty_ground ⟷ expr = empty"
  using from_ground_empty to_ground_empty ground.to_set_empty to_ground_inverse
  unfolding to_ground_def vars_def
  by fastforce

lemma from_ground_empty' [simp]: "from_ground expr = empty ⟷ expr = empty_ground"
  using from_ground_empty from_ground_eq
  unfolding from_ground_def  
  by auto

end

end