# 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
```