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)[1]
  apply (subst subst1.simps, auto split: option.splits)[1]
  apply (subst subst1.simps, auto split: option.splits)[1]
  apply (subst subst1.simps, auto split: option.splits)[1]
  apply (subst subst1.simps, auto split: option.splits, simp only: Let_def map_lc.simps)[1]
  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 
by (auto simp add: map_of_map_apsnd)

lemma map_apsnd_zip[simp]: "map (apsnd f) (zip a b) = zip a (map f b)"
  by (simp add: apsnd_def' zip_map2)

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)[1]›)
       apply (solves ‹(subst subst'.simps, auto split: option.splits cong: map_cong)[1]›)
      apply (solves ‹(subst subst'.simps, auto split: option.splits)[1]›)
     apply (solves ‹(subst subst'.simps, auto split: option.splits)[1]›)
    apply (solves ‹(subst subst'.simps, auto split: option.splits)[1]›)
   apply (solves ‹(subst subst'.simps, auto split: option.splits, simp only: Let_def map_lc.simps)[1]›)
  apply (solves ‹(subst subst'.simps, auto split: option.splits)[1]›)
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