Theory Variable_Substitution

theory Variable_Substitution
  imports
    Abstract_Substitution.Substitution
    "HOL-Library.FSet"
    "HOL-Library.Multiset"
begin

locale finite_set =
  fixes set :: "'b ⇒ 'a set"
  assumes finite_set [simp]: "⋀b. finite (set b)"
begin

abbreviation finite_set :: "'b ⇒ 'a fset" where 
  "finite_set b ≡ Abs_fset (set b)"

lemma finite_set': "set b ∈ {A. finite A}"
  by simp

lemma fset_finite_set [simp]: "fset (finite_set b) = set b"
  using Abs_fset_inverse[OF finite_set'].

end

locale variable_substitution = substitution _ _ subst "λa. vars a = {}" 
for
  subst :: "'expression ⇒ ('variable ⇒ 'base_expression) ⇒ 'expression" (infixl "⋅" 70) and
  vars :: "'expression ⇒ 'variable set" +
assumes 
  subst_eq: "⋀a σ τ. (⋀x. x ∈ (vars a) ⟹ σ x = τ x) ⟹ a ⋅ σ = a ⋅ τ"
begin

abbreviation is_ground where "is_ground a ≡ vars a = {}"

definition vars_set :: "'expression set ⇒ 'variable set" where
  "vars_set expressions ≡ ⋃expression ∈ expressions. vars expression"

lemma subst_reduntant_upd [simp]:
  assumes "var ∉ vars a"
  shows "a ⋅ σ(var := update) = a ⋅ σ"
  using assms subst_eq
  by fastforce

lemma subst_reduntant_if [simp]: 
  assumes "vars a ⊆ vars'"
  shows "a ⋅ (λvar. if var ∈ vars' then σ var else σ' var) = a ⋅ σ"
  using assms 
  by (smt (verit, best) subset_eq subst_eq)

lemma subst_reduntant_if' [simp]: 
  assumes "vars a ∩ vars' = {}"  
  shows "a ⋅ (λvar. if var ∈ vars' then σ' var else σ var) = a ⋅ σ"
  using assms subst_eq 
  unfolding disjoint_iff
  by presburger

lemma subst_cannot_unground:
  assumes "¬is_ground (a ⋅ σ)"  
  shows "¬is_ground a" 
  using assms by force

end

locale finite_variables = finite_set vars for vars :: "'expression ⇒ 'variable set"
begin

lemmas finite_vars = finite_set finite_set'
lemmas fset_finite_vars = fset_finite_set

abbreviation "finite_vars ≡ finite_set"

end

locale all_subst_ident_iff_ground =
  fixes is_ground :: "'expression ⇒ bool" and subst 
  assumes
    all_subst_ident_iff_ground: "⋀a. is_ground a ⟷ (∀σ. subst a σ = a)" and
    exists_non_ident_subst: 
      "⋀a s. finite s ⟹ ¬is_ground a ⟹ ∃σ. subst a σ ≠ a ∧ subst a σ ∉ s"

locale grounding = variable_substitution 
  where vars = vars for vars :: "'a ⇒ 'var set" +
  fixes to_ground :: "'a ⇒ 'g" and from_ground :: "'g ⇒ 'a"
  assumes 
    range_from_ground_iff_is_ground: "{f. is_ground f} = range from_ground" and
    from_ground_inverse [simp]: "⋀g. to_ground (from_ground g) = g"
begin

definition groundings ::"'a ⇒ 'g set" where
  "groundings a = { to_ground (a ⋅ γ) | γ. is_ground (a ⋅ γ) }"

lemma to_ground_from_ground_id: "to_ground ∘ from_ground = id"
  using from_ground_inverse
  by auto

lemma surj_to_ground: "surj to_ground"
  using from_ground_inverse
  by (metis surj_def)

lemma inj_from_ground: "inj_on from_ground domain⇩G"
  by (metis from_ground_inverse inj_on_inverseI)
 
lemma inj_on_to_ground: "inj_on to_ground (from_ground ` domain⇩G)"
  unfolding inj_on_def
  by simp

lemma bij_betw_to_ground: "bij_betw to_ground (from_ground ` domain⇩G) domain⇩G"
  by (smt (verit, best) bij_betwI' from_ground_inverse image_iff)

lemma bij_betw_from_ground: "bij_betw from_ground domain⇩G (from_ground ` domain⇩G)"
  by (simp add: bij_betw_def inj_from_ground)

lemma ground_is_ground [simp, intro]: "is_ground (from_ground g)"
  using range_from_ground_iff_is_ground
  by blast

lemma is_ground_iff_range_from_ground: "is_ground f ⟷ f ∈ range from_ground"
  using range_from_ground_iff_is_ground
  by auto

lemma to_ground_inverse [simp]: 
  assumes "is_ground f"
  shows "from_ground (to_ground f) = f"
  using inj_on_to_ground from_ground_inverse is_ground_iff_range_from_ground assms
  unfolding inj_on_def
  by blast

corollary obtain_grounding: 
  assumes "is_ground f"
  obtains g where "from_ground g = f"
  using to_ground_inverse assms by blast

end

locale base_variable_substitution = variable_substitution 
  where subst = subst
  for subst :: "'expression ⇒ ('variable ⇒ 'expression) ⇒ 'expression"  (infixl "⋅" 70) +
  assumes
    is_grounding_iff_vars_grounded: 
      "⋀exp. is_ground (exp ⋅ γ) ⟷ (∀x ∈ vars exp. is_ground (γ x))" and
    ground_exists: "∃exp. is_ground exp"
begin 

lemma obtain_ground_subst:
  obtains γ 
  where "is_ground_subst γ"
proof-
  obtain g where "is_ground g"
    using ground_exists by blast

  then have "is_ground_subst  (λ_. g)"
    by (simp add: is_grounding_iff_vars_grounded is_ground_subst_def)

  then show ?thesis
    using that
    by simp
qed

lemma ground_subst_extension:
  assumes "is_ground (exp ⋅ γ)"
  obtains γ'
  where "exp ⋅ γ = exp ⋅ γ'" and "is_ground_subst γ'"
proof-
  obtain γ'' where 
    γ'': "is_ground_subst γ''"
    using obtain_ground_subst
    by blast
                    
  define γ' where 
    γ':  "γ' = (λvar. if var ∈ vars exp then γ var else γ'' var)"

  have "is_ground_subst γ'"
    using assms γ'' is_grounding_iff_vars_grounded
    unfolding γ' is_ground_subst_def
    by simp

  moreover have "exp ⋅ γ = exp ⋅ γ'"
    unfolding γ'
    using subst_eq by presburger

  ultimately show ?thesis
    using that
    by blast
qed

lemma ground_subst_upd [simp]:
  assumes "is_ground update" "is_ground (exp ⋅ γ)" 
  shows "is_ground (exp ⋅ γ(var := update))"
  using assms is_grounding_iff_vars_grounded by auto

lemma variable_grounding:
  assumes "is_ground (t ⋅ γ)" "x ∈ vars t" 
  shows "is_ground (γ x)"
  using assms is_grounding_iff_vars_grounded 
  by blast

end

locale based_variable_substitution = 
  base: base_variable_substitution where subst = base_subst and vars = base_vars + 
  variable_substitution
for base_subst base_vars +
assumes
  ground_subst_iff_base_ground_subst [simp]: "is_ground_subst γ ⟷ base.is_ground_subst γ" and
  is_grounding_iff_vars_grounded: 
    "⋀exp. is_ground (exp ⋅ γ) ⟷ (∀x ∈ vars exp. base.is_ground (γ x))"
begin

lemma obtain_ground_subst:
  obtains γ 
  where "is_ground_subst γ"
  using base.obtain_ground_subst by auto

lemma ground_subst_extension:
  assumes "is_ground (exp ⋅ γ)"
  obtains γ'
  where "exp ⋅ γ = exp ⋅ γ'" and "is_ground_subst γ'"
  using obtain_ground_subst assms
  by (metis all_subst_ident_if_ground is_ground_subst_comp_right subst_comp_subst)

lemma ground_subst_extension':
  assumes "is_ground (exp ⋅ γ)"
  obtains γ'
  where "exp ⋅ γ = exp ⋅ γ'" and "base.is_ground_subst γ'"
  using ground_subst_extension assms
  by auto

lemma ground_subst_upd [simp]:
  assumes "base.is_ground update" "is_ground (exp ⋅ γ)" 
  shows "is_ground (exp ⋅ γ(var := update))"
  using base.ground_subst_upd assms is_grounding_iff_vars_grounded by simp  

lemma ground_exists: "∃exp. is_ground exp"
  using base.ground_exists
  by (meson is_grounding_iff_vars_grounded)

lemma variable_grounding:
  assumes "is_ground (t ⋅ γ)" "x ∈ vars t" 
  shows "base.is_ground (γ x)"
  using assms is_grounding_iff_vars_grounded 
  by blast

end
                                             
section ‹Liftings›

locale variable_substitution_lifting = 
  sub: variable_substitution
  where subst = sub_subst and vars = sub_vars
  for
    sub_vars :: "'sub_expression ⇒ 'variable set" and
    sub_subst :: "'sub_expression ⇒ ('variable ⇒ 'base_expression) ⇒ 'sub_expression" +
  fixes
    map :: "('sub_expression ⇒ 'sub_expression) ⇒ 'expression ⇒ 'expression" and
    to_set :: "'expression ⇒ 'sub_expression set"
  assumes
    map_comp: "⋀d f g. map f (map g d) = map (f ∘ g) d" and
    map_id: "map id d = d" and
    map_cong: "⋀d f g. (⋀c. c ∈ to_set d ⟹ f c = g c) ⟹ map f d = map g d" and
    to_set_map: "⋀d f. to_set (map f d) = f ` to_set d" and
    exists_expression: "⋀c. ∃d. c ∈ to_set d" 
begin

definition vars :: "'expression ⇒ 'variable set" where
  "vars d ≡ ⋃ (sub_vars ` to_set d)"

definition subst :: "'expression ⇒ ('variable ⇒ 'base_expression) ⇒ 'expression" where
  "subst d σ ≡ map (λc. sub_subst c σ) d"

lemma map_id_cong: 
  assumes "⋀c. c ∈ to_set d ⟹ f c = c"  
  shows "map f d = d"
  using map_cong map_id assms
  unfolding id_def
  by metis

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

lemma subst_in_to_set_subst:
  assumes "c ∈ to_set d" 
  shows "sub_subst c σ ∈ to_set (subst d σ)"
  unfolding subst_def
  using assms to_set_map by auto

sublocale variable_substitution where subst = subst and vars = vars
proof unfold_locales
  show "⋀x a b. subst x (comp_subst a b) = subst (subst x a) b"
    using sub.subst_comp_subst
    unfolding subst_def map_comp comp_apply
    by presburger
next
  show "⋀x. subst x id_subst = x"
    using map_id
    unfolding subst_def sub.subst_id_subst id_def.
next
   show "⋀x. vars x = {} ⟹ ∀σ. subst x σ = x"
     unfolding vars_def subst_def    
     using map_id_cong 
     by simp
next
  show "⋀a σ τ. (⋀x. x ∈ vars a ⟹ σ x = τ x) ⟹ subst a σ = subst a τ "
    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 c 
  assume all_d_ground: "∀d. is_ground (subst d γ)"
  show "sub.is_ground (sub_subst c γ)"
  proof(rule ccontr)
    assume c_not_ground: "¬sub.is_ground (sub_subst c γ)"

    then obtain d where "c ∈ to_set d"
      using exists_expression by auto

    then have "¬is_ground (subst d γ)"
      using c_not_ground to_set_map 
      unfolding subst_def vars_def
      by auto

    then show False
      using all_d_ground
      by blast
  qed
next
  fix d
  assume all_c_ground: "∀c. sub.is_ground (sub_subst c γ)"

  then show "is_ground (subst d γ)"
    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 (subst expr γ)"  
  shows "sub.is_ground (sub_subst sub γ)"
  using assms
  by (meson subst_in_to_set_subst to_set_is_ground)

lemma subst_empty:
  assumes "to_set expr' = {}"
  shows "subst expr σ = expr' ⟷ expr = expr'"
  using assms map_id_cong subst_def to_set_map 
  by fastforce

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

end

locale based_variable_substitution_lifting = 
  variable_substitution_lifting +
  base: base_variable_substitution where subst = base_subst and vars = base_vars
for base_subst base_vars +
assumes 
  sub_is_grounding_iff_vars_grounded: 
    "⋀exp γ. sub.is_ground (sub_subst exp γ) ⟷ (∀x ∈ sub_vars exp. base.is_ground (γ x))" and
  sub_ground_subst_iff_base_ground_subst: "⋀γ. sub.is_ground_subst γ ⟷ base.is_ground_subst γ"
begin

lemma is_grounding_iff_vars_grounded: 
  "is_ground (subst exp γ) ⟷ (∀x ∈ vars exp. base.is_ground (γ x))"
  using sub_is_grounding_iff_vars_grounded subst_def to_set_map vars_def
  by auto

lemma ground_subst_iff_base_ground_subst [simp]: 
  "⋀γ. is_ground_subst γ ⟷ base.is_ground_subst γ"
  using sub_ground_subst_iff_base_ground_subst ground_subst_iff_sub_ground_subst by blast

lemma obtain_ground_subst:
  obtains γ 
  where "is_ground_subst γ"
  using base.obtain_ground_subst
  by (meson base.ground_exists is_grounding_iff_vars_grounded is_ground_subst_def that)

lemma ground_subst_extension:
  assumes "is_ground (subst exp γ)"
  obtains γ'
  where "subst exp γ = subst exp γ'" and "is_ground_subst γ'"
  by (metis all_subst_ident_if_ground assms comp_subst.left.monoid_action_compatibility 
        is_ground_subst_comp_right obtain_ground_subst)

lemma ground_subst_extension':
  assumes "is_ground (subst exp γ)"
  obtains γ'
  where "subst exp γ = subst exp γ'" and "base.is_ground_subst γ'"
  by (metis all_subst_ident_if_ground assms base.is_ground_subst_comp_right 
        base.obtain_ground_subst subst_comp_subst)
 
lemma ground_subst_upd [simp]:
  assumes "base.is_ground update" "is_ground (subst exp γ)" 
  shows "is_ground (subst exp  (γ(var := update)))"
  using assms(1) assms(2) is_grounding_iff_vars_grounded by auto

lemma ground_exists: "∃exp. is_ground exp"
  using base.ground_exists
  by (meson is_grounding_iff_vars_grounded)

lemma variable_grounding:
  assumes "is_ground (subst t γ)" "x ∈ vars t" 
  shows "base.is_ground (γ x)"
  using assms is_grounding_iff_vars_grounded 
  by blast

end

locale finite_variables_lifting = 
  variable_substitution_lifting + 
  sub: finite_variables where vars = sub_vars +
  to_set: finite_set where set = to_set
begin

abbreviation to_fset :: "'d ⇒ 'c fset" where 
  "to_fset ≡ to_set.finite_set"

lemmas finite_to_set = to_set.finite_set to_set.finite_set'
lemmas fset_to_fset = to_set.fset_finite_set

sublocale finite_variables where vars = vars
  by unfold_locales (simp add: vars_def)

end

locale grounding_lifting = 
  variable_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 
for
  sub_to_ground :: "'sub ⇒ 'ground_sub" and 
  sub_from_ground :: "'ground_sub ⇒ 'sub" and
  sub_vars :: "'sub ⇒ 'variable set" and 
  sub_subst :: "'sub ⇒ ('variable ⇒ 'base) ⇒ 'sub" and
  map :: "('sub ⇒ 'sub) ⇒ 'expr ⇒ 'expr" +
fixes
  to_ground_map :: "('sub ⇒ 'ground_sub) ⇒ 'expr ⇒ 'ground_expr" and
  from_ground_map :: "('ground_sub ⇒ 'sub) ⇒ 'ground_expr ⇒ 'expr" and
  ground_map :: "('ground_sub ⇒ 'ground_sub) ⇒ 'ground_expr ⇒ 'ground_expr" and
  to_set_ground :: "'ground_expr ⇒ 'ground_sub set"
assumes
  to_set_from_ground_map: "⋀d f. to_set (from_ground_map f d) = f ` to_set_ground d" and
  map_comp': "⋀d f g. from_ground_map f (to_ground_map g d) = map (f ∘ g) d" and
  ground_map_comp: "⋀d f g. to_ground_map f (from_ground_map g d) = ground_map (f ∘ g) d" and
  ground_map_id: "ground_map id g = g"
begin

definition to_ground where "to_ground expr ≡ to_ground_map sub_to_ground expr"

definition from_ground where "from_ground expr ≡ from_ground_map sub_from_ground expr"

sublocale grounding where 
  vars = vars and subst = subst and to_ground = to_ground and from_ground = from_ground
proof unfold_locales
  have "⋀expr. vars expr = {} ⟹ expr ∈ range from_ground"
  proof-
    fix expr
    assume "vars 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_ground. sub_from_ground sub_ground = sub"
      by fast

    then have "∃ground_expr. from_ground ground_expr = expr"
      using map_comp'[symmetric] map_id_cong
      unfolding from_ground_def comp_def
      by metis

    then show "expr ∈ range from_ground"
      unfolding from_ground_def
      by blast
  qed

  moreover have "⋀expr x. x ∈ vars (from_ground expr) ⟹ False"
  proof-
    fix expr x
    assume "x ∈ vars (from_ground expr)"
    then show False
      unfolding vars_def from_ground_def
      using sub.ground_is_ground to_set_from_ground_map by auto
  qed

  ultimately show "{f. vars f = {}} = range from_ground"
    by blast   
next
  show "⋀g. to_ground (from_ground g) = g"
    using ground_map_id
    unfolding to_ground_def from_ground_def ground_map_comp sub.to_ground_from_ground_id.
qed

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

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 +  
  sub: all_subst_ident_iff_ground where subst = sub_subst and is_ground = sub.is_ground
begin

sublocale all_subst_ident_iff_ground 
  where subst = subst and is_ground = is_ground
proof unfold_locales
  show "⋀x. is_ground x = (∀σ. subst x σ = x)"
  proof(rule iffI allI)
    show "⋀x. is_ground x ⟹ ∀σ. subst x σ = x"
      by simp
  next
    fix d x
    assume all_subst_ident: "∀σ. subst d σ = d"
    
    show "is_ground d"
    proof(rule ccontr)
      assume "¬is_ground d"

      then obtain c where c_in_d: "c ∈ to_set d" and c_not_ground: "¬sub.is_ground c"
        unfolding vars_def
        by blast

      then obtain σ where "sub_subst c σ ≠ c" and "sub_subst c σ ∉ to_set d"
        using sub.exists_non_ident_subst finite_to_set
        by blast
        
      then show False
        using all_subst_ident c_in_d to_set_map
        unfolding subst_def 
        by (metis image_eqI)
    qed
  qed
next
  fix d :: 'd and ds :: "'d set"
  assume finite_ds: "finite ds" and d_not_ground: "¬is_ground d"

  then have finite_cs: "finite (⋃(to_set ` insert d ds))"
    using finite_to_set by blast

  obtain c where c_in_d: "c ∈ to_set d" and c_not_ground: "¬sub.is_ground c"
    using d_not_ground
    unfolding vars_def
    by blast

  obtain σ where σ_not_ident: "sub_subst c σ ≠ c" "sub_subst c σ ∉ ⋃ (to_set ` insert d ds)"
    using sub.exists_non_ident_subst[OF finite_cs c_not_ground]
    by blast

  then have "subst d σ ≠ d"
    using c_in_d
    unfolding subst_def
    by (simp add: to_set_map_not_ident)

  moreover have "subst d σ ∉ ds"
    using σ_not_ident(2) c_in_d to_set_map
    unfolding subst_def
    by auto

  ultimately show "∃σ. subst d σ ≠ d ∧ subst d σ ∉ ds"
    by blast
qed

end

end