Theory Abstract_Formula

theory Abstract_Formula
imports
  Main
  "HOL-Library.FSet"
  "HOL-Library.Stream"
  Indexed_FSet
begin

text ‹
The following locale describes an abstract interface for a set of formulas, without fixing the
concret shape, or set of variables.

The variables mentioned in this locale are only the @{emph ‹locally fixed constants›} occurring in
formulas, e.g.\@ in the introduction rule for the universal quantifier. Normal variables are not
something we care about at this point; they are handled completely abstractly by the abstract notion
of a substitution.
›

locale Abstract_Formulas =
  ― ‹Variables can be renamed injectively›
  fixes freshenLC :: "nat ⇒ 'var ⇒ 'var"
  ― ‹A variable-changing function can be mapped over a formula›
  fixes renameLCs :: "('var ⇒ 'var) ⇒ ('form ⇒ 'form)"
  ― ‹The set of variables occurring in a formula›
  fixes lconsts :: "'form ⇒ 'var set"
  ― ‹A closed formula has no variables, and substitions do not affect it.›
  fixes closed :: "'form ⇒ bool"
  ― ‹A substitution can be applied to a formula.›
  fixes subst :: "'subst ⇒ 'form ⇒ 'form"
  ― ‹The set of variables occurring (in the image) of a substitution.›
  fixes subst_lconsts :: "'subst ⇒ 'var set"
  ― ‹A variable-changing function can be mapped over a substitution›
  fixes subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
  ― ‹A most generic formula, can be substitutied to anything.›
  fixes anyP :: "'form"

  assumes freshenLC_eq_iff[simp]: "freshenLC a v = freshenLC a' v' ⟷ a = a' ∧ v = v'"
  assumes lconsts_renameLCs: "lconsts (renameLCs p f) = p ` lconsts f"
  assumes rename_closed: "lconsts f = {} ⟹ renameLCs p f = f"
  assumes subst_closed: "closed f ⟹ subst s f = f"
  assumes closed_no_lconsts: "closed f ⟹ lconsts f = {}"
  assumes fv_subst: "lconsts (subst s f) ⊆ lconsts f ∪ subst_lconsts s"
  assumes rename_rename: "renameLCs p1 (renameLCs p2 f) = renameLCs (p1 ∘ p2) f"
  assumes rename_subst: "renameLCs p (subst s f) = subst (subst_renameLCs p s) (renameLCs p f)"
  assumes renameLCs_cong: "(⋀ x. x ∈ lconsts f ⟹ f1 x = f2 x) ⟹ renameLCs f1 f = renameLCs f2 f"
  assumes subst_renameLCs_cong: "(⋀ x. x ∈ subst_lconsts s ⟹ f1 x = f2 x) ⟹ subst_renameLCs f1 s = subst_renameLCs f2 s"
  assumes subst_lconsts_subst_renameLCs: "subst_lconsts (subst_renameLCs p s) = p ` subst_lconsts s"
  assumes lconsts_anyP: "lconsts anyP = {}"
  assumes empty_subst: "∃ s. (∀ f. subst s f = f) ∧ subst_lconsts s = {}"
  assumes anyP_is_any: "∃ s. subst s anyP = f"
begin
  definition freshen :: "nat ⇒ 'form ⇒ 'form" where
    "freshen n = renameLCs (freshenLC n)"

  definition empty_subst :: "'subst" where
    "empty_subst = (SOME s. (∀ f. subst s f = f) ∧ subst_lconsts s = {})"

  lemma empty_subst_spec:
    "(∀ f. subst empty_subst f = f) ∧ subst_lconsts empty_subst = {}"
    unfolding empty_subst_def using empty_subst by (rule someI_ex)
  lemma subst_empty_subst[simp]: "subst empty_subst f = f"
    by (metis empty_subst_spec)
  lemma subst_lconsts_empty_subst[simp]: "subst_lconsts empty_subst = {}"
    by (metis empty_subst_spec)

  lemma lconsts_freshen: "lconsts (freshen a f) = freshenLC a ` lconsts f"
    unfolding freshen_def by (rule lconsts_renameLCs)

  lemma freshen_closed: "lconsts f = {} ⟹ freshen a f = f"
    unfolding freshen_def by (rule rename_closed)
    
  lemma closed_eq:
    assumes "closed f1"
    assumes "closed f2"
    shows "subst s1 (freshen a1 f1) = subst s2 (freshen a2 f2) ⟷ f1 = f2"
  using assms
    by (auto simp add: closed_no_lconsts freshen_def lconsts_freshen subst_closed rename_closed)

  lemma freshenLC_range_eq_iff[simp]: "freshenLC a v ∈ range (freshenLC a') ⟷ a = a'"
    by auto

  definition rerename :: "'var set ⇒ nat ⇒ nat ⇒ ('var ⇒ 'var) ⇒ ('var ⇒ 'var)" where
    "rerename V from to f x = (if x ∈ freshenLC from ` V then freshenLC to (inv (freshenLC from) x) else f x)"
  
  lemma inj_freshenLC[simp]: "inj (freshenLC i)"
    by (rule injI) simp
  
  lemma rerename_freshen[simp]: "x ∈ V ⟹ rerename  V i (isidx is) f (freshenLC i x) = freshenLC (isidx is) x"
    unfolding rerename_def by simp

  lemma range_rerename: "range (rerename V  from to f) ⊆ freshenLC to ` V ∪ range f"
    by (auto simp add: rerename_def split: if_splits)

  lemma rerename_noop:
      "x ∉ freshenLC from ` V  ⟹ rerename V from to f x = f x"
    by (auto simp add: rerename_def split: if_splits)

  lemma rerename_rename_noop:
      "freshenLC from ` V ∩ lconsts form  = {}  ⟹ renameLCs (rerename V from to f) form = renameLCs f form"
      by (intro renameLCs_cong rerename_noop) auto

  lemma rerename_subst_noop:
      "freshenLC from ` V ∩ subst_lconsts s  = {}  ⟹ subst_renameLCs (rerename V from to f) s = subst_renameLCs f s"
      by (intro subst_renameLCs_cong rerename_noop) auto
end
end