# Theory Predicate_Formulas

```theory Predicate_Formulas
imports
"HOL-Library.Countable"
"HOL-Library.Infinite_Set"
"HOL-Eisbach.Eisbach"
Abstract_Formula
begin

text ‹This theory contains an example instantiation of @{term Abstract_Formulas} with an
formula type with local constants. It is a rather ad-hoc type that may not be very useful to
work with, though.›

type_synonym var = nat
type_synonym lconst = nat

text ‹
We support higher order variables, in order to express ‹∀x.?P x›. But we stay first order,
i.e. the parameters of such a variables will only be instantiated with ground terms.
›

datatype form =
Var (var:var) (params: "form list")
| LC (var:lconst)
| Op (name:string) (params: "form list")
| Quant (name:string) (var:nat) (body: form)

type_synonym schema = "var list × form"

type_synonym subst = "(nat × schema) list"

fun fv :: "form ⇒ var set" where
"fv (Var v xs) = insert v (Union (fv ` set xs))"
| "fv (LC v) = {}"
| "fv (Op n xs) = Union (fv ` set xs)"
| "fv (Quant n v f) = fv f - {v}"

definition fresh_for :: "var set ⇒ var" where
"fresh_for V = (SOME n. n ∉ V)"

lemma fresh_for_fresh: "finite V ⟹ fresh_for V ∉ V"
unfolding fresh_for_def
apply (rule someI2_ex)
using infinite_nat_iff_unbounded_le
apply auto
done

text ‹Free variables›

fun fv_schema :: "schema ⇒ var set" where
"fv_schema (ps,f) = fv f - set ps"

definition fv_subst :: "subst ⇒ var set" where
"fv_subst s = ⋃(fv_schema ` ran (map_of s))"

definition fv_subst1 where
"fv_subst1 s = ⋃(fv ` snd ` set s)"

lemma fv_subst_Nil[simp]: "fv_subst1 [] = {}"
unfolding fv_subst1_def by auto

text ‹Local constants, separate from free variables.›

fun lc :: "form ⇒ lconst set" where
"lc (Var v xs) = Union (lc ` set xs)"
| "lc (LC c) = {c}"
| "lc (Op n xs) = Union (lc ` set xs)"
| "lc (Quant n v f) = lc f"

fun lc_schema :: "schema ⇒ lconst set" where
"lc_schema (ps,f) = lc f"

definition lc_subst1 where
"lc_subst1 s = ⋃(lc ` snd ` set s)"

fun lc_subst :: "subst ⇒ lconst set" where
"lc_subst s = ⋃(lc_schema ` snd ` set s)"

fun map_lc :: "(lconst ⇒ lconst) ⇒ form ⇒ form" where
"map_lc f (Var v xs) = Var v (map (map_lc f) xs)"
| "map_lc f (LC n) = LC (f n)"
| "map_lc f (Op n xs) = Op n (map (map_lc f) xs)"
| "map_lc f (Quant n v f') = Quant n v (map_lc f f')"

lemma fv_map_lc[simp]: "fv (map_lc p f) = fv f"
by (induction f) auto

lemma lc_map_lc[simp]: "lc (map_lc p f) = p ` lc f"
by (induction f) auto

lemma map_lc_map_lc[simp]: "map_lc p1 (map_lc p2 f) = map_lc (p1 ∘ p2) f"
by (induction f) auto

fun map_lc_subst1 :: "(lconst ⇒ lconst) ⇒ (var × form) list ⇒ (var × form) list" where
"map_lc_subst1 f s = map (apsnd (map_lc f)) s"

fun map_lc_subst :: "(lconst ⇒ lconst) ⇒ subst ⇒ subst" where
"map_lc_subst f s = map (apsnd (apsnd (map_lc f))) s"

lemma map_lc_noop[simp]: "lc f = {} ⟹ map_lc p f = f"
by (induction f) (auto simp add: map_idI)

lemma map_lc_cong[cong]: "(⋀x. x ∈ lc f ⟹ f1 x = f2 x) ⟹ map_lc f1 f = map_lc f2 f"
by (induction f) auto

lemma [simp]: "fv_subst1 (map (apsnd (map_lc p)) s) = fv_subst1 s"
unfolding fv_subst1_def
by auto

lemma map_lc_subst_cong[cong]:
assumes "(⋀x. x ∈ lc_subst s ⟹ f1 x = f2 x)"
shows "map_lc_subst f1 s = map_lc_subst f2 s"
by (force intro!: map_lc_cong assms)

text ‹In order to make the termination checker happy, we define substitution in two stages: One
that substitutes only ground terms for variables, and the real one that can substitute schematic
terms (or lambda expression, if you want).›

fun subst1 :: "(var × form) list ⇒ form ⇒ form" where
"subst1 s (Var v []) = (case map_of s v of Some f ⇒ f | None ⇒ Var v [])"
| "subst1 s (Var v xs) = Var v xs"
| "subst1 s (LC n) = LC n"
| "subst1 s (Op n xs) = Op n (map (subst1 s) xs)"
| "subst1 s (Quant n v f) =
(if v ∈ fv_subst1 s then
(let v' = fresh_for (fv_subst1 s)
in Quant n v' (subst1 ((v, Var v' [])#s) f))
else Quant n v (subst1 s f))"

lemma subst1_Nil[simp]: "subst1 [] f = f"
by (induction "[]::(var × form) list" f  rule:subst1.induct)
(auto simp add: map_idI split: option.splits)

lemma lc_subst1: "lc (subst1 s f) ⊆ lc f ∪ ⋃(lc ` snd ` set s)"
by (induction s f rule: subst1.induct)
(auto split: option.split dest: map_of_SomeD simp add: Let_def)

lemma apsnd_def': "apsnd f = (λ(k, v). (k, f v))"
by auto

lemma map_of_map_apsnd:
"map_of (map (apsnd f) xs) = map_option f ∘ map_of xs"
unfolding apsnd_def' by (rule map_of_map)

lemma map_lc_subst1[simp]: "map_lc p (subst1 s f) = subst1 (map_lc_subst1 p s) (map_lc p f)"
apply (induction s f rule: subst1.induct)
apply (auto split: option.splits simp add: map_of_map_apsnd Let_def)
apply (subst subst1.simps, auto split: option.splits)
apply (subst subst1.simps, auto split: option.splits)
apply (subst subst1.simps, auto split: option.splits)
apply (subst subst1.simps, auto split: option.splits)
apply (subst subst1.simps, auto split: option.splits, simp only: Let_def map_lc.simps)
apply (subst subst1.simps, auto split: option.splits)
done

fun subst' :: "subst ⇒ form ⇒ form" where
"subst' s (Var v xs) =
(case map_of s v of None ⇒ (Var v (map (subst' s) xs))
| Some (ps,rhs) ⇒
if length ps = length xs
then subst1 (zip ps (map (subst' s) xs)) rhs
else (Var v (map (subst' s) xs)))"
| "subst' s (LC n) = LC n"
| "subst' s (Op n xs) = Op n (map (subst' s) xs)"
| "subst' s (Quant n v f) =
(if v ∈ fv_subst s then
(let v' = fresh_for (fv_subst s)
in Quant n v' (subst' ((v,([], Var v' []))#s) f))
else Quant n v (subst' s f))"

lemma subst'_Nil[simp]: "subst' [] f = f"
by (induction f) (auto simp add: map_idI fv_subst_def)

lemma lc_subst': "lc (subst' s f) ⊆ lc f ∪ lc_subst s"
apply (induction s f rule: subst'.induct)
apply (auto split: option.splits dest: map_of_SomeD  dest!: subsetD[OF lc_subst1] simp add: fv_subst_def)
apply (fastforce dest!: set_zip_rightD)+
done

lemma ran_map_option_comp[simp]:
"ran (map_option f ∘ m) = f ` ran m"
unfolding comp_def by (rule ran_map_option)

lemma fv_schema_apsnd_map_lc[simp]:
"fv_schema (apsnd (map_lc p) a) = fv_schema a"
by (cases a) auto

lemma fv_subst_map_apsnd_map_lc[simp]:
"fv_subst (map (apsnd (apsnd (map_lc p))) s) = fv_subst s"
unfolding fv_subst_def

lemma map_apsnd_zip[simp]: "map (apsnd f) (zip a b) = zip a (map f b)"

lemma map_lc_subst'[simp]: "map_lc p (subst' s f) = subst' (map_lc_subst p s) (map_lc p f)"
apply (induction s f rule: subst'.induct)
apply (auto split: option.splits dest: map_of_SomeD simp add: map_of_map_apsnd Let_def)
apply (solves ‹(subst subst'.simps, auto split: option.splits)›)
apply (solves ‹(subst subst'.simps, auto split: option.splits cong: map_cong)›)
apply (solves ‹(subst subst'.simps, auto split: option.splits)›)
apply (solves ‹(subst subst'.simps, auto split: option.splits)›)
apply (solves ‹(subst subst'.simps, auto split: option.splits)›)
apply (solves ‹(subst subst'.simps, auto split: option.splits, simp only: Let_def map_lc.simps)›)
apply (solves ‹(subst subst'.simps, auto split: option.splits)›)
done

text ‹Since subst' happily renames quantified variables, we have a simple wrapper that
ensures that the substitution is minimal, and is empty if ‹f› is closed. This is
a hack to support lemma  ‹subst_noop›. ›

fun subst :: "subst ⇒ form ⇒ form" where
"subst s f = subst' (filter (λ (v,s). v ∈ fv f) s) f"

lemma subst_Nil[simp]: "subst [] f = f"
by auto

lemma subst_noop[simp]: "fv f = {} ⟹ subst s f = f"
by simp

lemma lc_subst: "lc (subst s f) ⊆ lc f ∪ lc_subst s"
by (auto dest: subsetD[OF lc_subst'])

lemma lc_subst_map_lc_subst[simp]: "lc_subst (map_lc_subst p s) = p ` lc_subst s"
by force

lemma map_lc_subst[simp]: "map_lc p (subst s f) = subst (map_lc_subst p s) (map_lc p f)"
unfolding subst.simps
by (auto simp add: filter_map intro!: arg_cong[OF filter_cong] )

fun closed :: "form ⇒ bool" where
"closed f ⟷ fv f = {} ∧ lc f = {}"

interpretation predicate: Abstract_Formulas
"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
apply unfold_locales
apply (solves fastforce)
apply (solves fastforce)
apply (solves fastforce)
apply (solves fastforce)
apply (solves fastforce)
apply (solves ‹rule lc_subst›)
apply (solves fastforce)
apply (solves fastforce)
apply (solves fastforce)
apply (solves ‹metis map_lc_subst_cong›)
apply (solves ‹rule lc_subst_map_lc_subst›)
apply (solves simp)
apply (solves ‹rule exI[where x = "[]"], simp›)
apply (solves ‹rename_tac f, rule_tac x = "[(0, ([],f))]" in exI, simp›)
done

declare predicate.subst_lconsts_empty_subst [simp del]

end
```