Theory TermsAndLiterals

section ‹Terms and Literals›

theory TermsAndLiterals imports Main "HOL-Library.Countable_Set" begin

type_synonym var_sym  = string
type_synonym fun_sym  = string
type_synonym pred_sym = string

datatype fterm = 
  Fun fun_sym (get_sub_terms: "fterm list")
| Var var_sym

datatype hterm = HFun fun_sym "hterm list" ― ‹Herbrand terms defined as in Berghofer's FOL-Fitting›


type_synonym 't atom = "pred_sym * 't list"

datatype 't literal = 
  sign: Pos (get_pred: pred_sym) (get_terms: "'t list")
| Neg (get_pred: pred_sym) (get_terms: "'t list")

fun get_atom :: "'t literal ⇒ 't atom" where
  "get_atom (Pos p ts) = (p, ts)"
| "get_atom (Neg p ts) = (p, ts)"


subsection ‹Ground›

fun ground⇩t :: "fterm ⇒ bool" where
  "ground⇩t (Var x) ⟷ False"
| "ground⇩t (Fun f ts) ⟷ (∀t ∈ set ts. ground⇩t t)"

abbreviation ground⇩t⇩s :: "fterm list ⇒ bool" where
  "ground⇩t⇩s ts ≡ (∀t ∈ set ts. ground⇩t t)"

abbreviation ground⇩l :: "fterm literal ⇒ bool" where
  "ground⇩l l ≡ ground⇩t⇩s (get_terms l)"

abbreviation ground⇩l⇩s :: "fterm literal set ⇒ bool" where
  "ground⇩l⇩s C ≡ (∀l ∈ C. ground⇩l l)"
  
definition ground_fatoms :: "fterm atom set" where
  "ground_fatoms ≡ {a. ground⇩t⇩s (snd a)}"

lemma ground⇩l_ground_fatom: 
  assumes "ground⇩l l"
  shows "get_atom l ∈ ground_fatoms"
  using assms unfolding ground_fatoms_def by (induction l) auto


subsection ‹Auxiliary›

lemma infinity:
  assumes inj: "∀n :: nat. undiago (diago n) = n" 
  assumes all_tree: "∀n :: nat. (diago n) ∈ S"
  shows "¬finite S"
proof -
  from inj all_tree have "∀n. n = undiago (diago n) ∧ (diago n) ∈ S" by auto
  then have "∀n. ∃ds. n = undiago ds ∧ ds ∈ S" by auto
  then have "undiago ` S = (UNIV :: nat set)" by auto
  then show "¬finite S" by (metis finite_imageI infinite_UNIV_nat) 
qed

lemma inv_into_f_f:
  assumes "bij_betw f A B"
  assumes "a∈A"
  shows "(inv_into A f) (f a) = a"
using assms bij_betw_inv_into_left by metis

lemma f_inv_into_f:
  assumes "bij_betw f A B"
  assumes "b∈B"
  shows "f ((inv_into A f) b) = b"
using assms bij_betw_inv_into_right by metis


subsection ‹Conversions›


subsubsection ‹Conversions - Terms and Herbrand Terms›

fun fterm_of_hterm :: "hterm ⇒ fterm" where
  "fterm_of_hterm (HFun p ts) = Fun p (map fterm_of_hterm ts)"

definition fterms_of_hterms :: "hterm list ⇒ fterm list" where
  "fterms_of_hterms ts ≡ map fterm_of_hterm ts"

fun hterm_of_fterm :: "fterm ⇒ hterm" where
  "hterm_of_fterm (Fun p ts) = HFun p (map hterm_of_fterm ts)"

definition hterms_of_fterms :: "fterm list ⇒ hterm list" where
"hterms_of_fterms ts ≡ map hterm_of_fterm ts"

lemma hterm_of_fterm_fterm_of_hterm[simp]: "hterm_of_fterm (fterm_of_hterm t) = t" 
  by (induction t) (simp add: map_idI)

lemma hterms_of_fterms_fterms_of_hterms[simp]: "hterms_of_fterms (fterms_of_hterms ts) = ts" 
  unfolding hterms_of_fterms_def fterms_of_hterms_def by (simp add: map_idI)

lemma fterm_of_hterm_hterm_of_fterm[simp]:
  assumes "ground⇩t t"
  shows "fterm_of_hterm (hterm_of_fterm t) = t" 
  using assms by (induction t) (auto simp add: map_idI)

lemma fterms_of_hterms_hterms_of_fterms[simp]: 
  assumes "ground⇩t⇩s ts"
  shows "fterms_of_hterms (hterms_of_fterms ts) = ts" 
  using assms unfolding fterms_of_hterms_def hterms_of_fterms_def by (simp add: map_idI)

lemma ground_fterm_of_hterm:  "ground⇩t (fterm_of_hterm t)"
  by (induction t) (auto simp add: map_idI)

lemma ground_fterms_of_hterms: "ground⇩t⇩s (fterms_of_hterms ts)"
  unfolding fterms_of_hterms_def using ground_fterm_of_hterm by auto


subsubsection ‹Conversions -  Literals and Herbrand Literals›

fun flit_of_hlit :: "hterm literal ⇒ fterm literal" where
  "flit_of_hlit (Pos p ts) = Pos p (fterms_of_hterms ts)"
| "flit_of_hlit (Neg p ts) = Neg p (fterms_of_hterms ts)"

fun hlit_of_flit :: "fterm literal ⇒ hterm literal" where
  "hlit_of_flit (Pos p ts) = Pos p (hterms_of_fterms ts)"
| "hlit_of_flit (Neg p ts) = Neg p (hterms_of_fterms ts)"

lemma ground_flit_of_hlit: "ground⇩l (flit_of_hlit l)" 
  by  (induction l)  (simp add: ground_fterms_of_hterms)+

theorem hlit_of_flit_flit_of_hlit [simp]: "hlit_of_flit (flit_of_hlit l) =  l" by (cases l) auto

theorem flit_of_hlit_hlit_of_flit [simp]:
  assumes "ground⇩l l"
  shows "flit_of_hlit (hlit_of_flit l) = l"
  using assms by (cases l) auto

lemma sign_flit_of_hlit: "sign (flit_of_hlit l) = sign l" by (cases l) auto

lemma hlit_of_flit_bij: "bij_betw hlit_of_flit {l. ground⇩l l} UNIV" 
 unfolding bij_betw_def
proof
  show "inj_on hlit_of_flit {l. ground⇩l l}" using inj_on_inverseI flit_of_hlit_hlit_of_flit 
    by (metis (mono_tags, lifting) mem_Collect_eq) 
next 
  have "∀l. ∃l'. ground⇩l l' ∧ l = hlit_of_flit l'" 
    using ground_flit_of_hlit hlit_of_flit_flit_of_hlit by metis
  then show "hlit_of_flit ` {l. ground⇩l l} = UNIV" by auto
qed

lemma flit_of_hlit_bij: "bij_betw flit_of_hlit UNIV {l. ground⇩l l}" 
 unfolding bij_betw_def inj_on_def
proof
  show "∀x∈UNIV. ∀y∈UNIV. flit_of_hlit x = flit_of_hlit y ⟶ x = y" 
    using ground_flit_of_hlit hlit_of_flit_flit_of_hlit by metis
next
  have "∀l. ground⇩l l ⟶ (l = flit_of_hlit (hlit_of_flit l))" using hlit_of_flit_flit_of_hlit by auto
  then have "{l. ground⇩l l}  ⊆ flit_of_hlit ` UNIV " by blast
  moreover
  have "∀l. ground⇩l (flit_of_hlit l)" using ground_flit_of_hlit by auto
  ultimately show "flit_of_hlit ` UNIV = {l. ground⇩l l}" using hlit_of_flit_flit_of_hlit ground_flit_of_hlit by auto
qed


subsubsection ‹Conversions - Atoms and Herbrand Atoms›

fun fatom_of_hatom :: "hterm atom ⇒ fterm atom" where
  "fatom_of_hatom (p, ts) = (p, fterms_of_hterms ts)"

fun hatom_of_fatom :: "fterm atom ⇒ hterm atom" where
  "hatom_of_fatom (p, ts) = (p, hterms_of_fterms ts)"

lemma ground_fatom_of_hatom: "ground⇩t⇩s (snd (fatom_of_hatom a))" 
  by  (induction a) (simp add: ground_fterms_of_hterms)+

theorem hatom_of_fatom_fatom_of_hatom [simp]: "hatom_of_fatom (fatom_of_hatom l) = l" 
  by (cases l) auto

theorem fatom_of_hatom_hatom_of_fatom [simp]: 
  assumes "ground⇩t⇩s (snd l)"
  shows "fatom_of_hatom (hatom_of_fatom l) = l"
  using assms by (cases l) auto

lemma hatom_of_fatom_bij: "bij_betw hatom_of_fatom ground_fatoms UNIV" 
 unfolding bij_betw_def
proof
  show "inj_on hatom_of_fatom ground_fatoms" using inj_on_inverseI fatom_of_hatom_hatom_of_fatom unfolding ground_fatoms_def 
    by (metis (mono_tags, lifting) mem_Collect_eq) 
next 
  have "∀a. ∃a'. ground⇩t⇩s (snd a') ∧ a = hatom_of_fatom a'" 
    using ground_fatom_of_hatom hatom_of_fatom_fatom_of_hatom by metis
  then show "hatom_of_fatom ` ground_fatoms = UNIV" unfolding ground_fatoms_def by blast
qed

lemma fatom_of_hatom_bij: "bij_betw fatom_of_hatom UNIV ground_fatoms" 
 unfolding bij_betw_def inj_on_def
proof
  show "∀x∈UNIV. ∀y∈UNIV. fatom_of_hatom x = fatom_of_hatom y ⟶ x = y" 
    using ground_fatom_of_hatom hatom_of_fatom_fatom_of_hatom by metis
next
  have "∀a. ground⇩t⇩s (snd a) ⟶ (a = fatom_of_hatom (hatom_of_fatom a))" using hatom_of_fatom_fatom_of_hatom by auto
  then have "ground_fatoms  ⊆ fatom_of_hatom ` UNIV " unfolding ground_fatoms_def by blast
  moreover
  have "∀l. ground⇩t⇩s (snd (fatom_of_hatom l))" using ground_fatom_of_hatom by auto
  ultimately show "fatom_of_hatom ` UNIV = ground_fatoms" 
    using hatom_of_fatom_fatom_of_hatom ground_fatom_of_hatom unfolding ground_fatoms_def by auto
qed


subsection ‹Enumerations›


subsubsection ‹Enumerating Strings›

definition nat_of_string:: "string ⇒ nat" where
  "nat_of_string ≡ (SOME f. bij f)"

definition string_of_nat:: "nat ⇒ string" where
  "string_of_nat ≡ inv nat_of_string"

lemma nat_of_string_bij: "bij nat_of_string"
  proof -
  have "countable (UNIV::string set)" by auto
  moreover
  have "infinite (UNIV::string set)" using infinite_UNIV_listI by auto
  ultimately
  obtain x where "bij (x:: string ⇒ nat)" using countableE_infinite[of UNIV] by blast
  then show "?thesis" unfolding nat_of_string_def using someI by metis
qed

lemma string_of_nat_bij: "bij string_of_nat" unfolding string_of_nat_def using nat_of_string_bij bij_betw_inv_into by auto

lemma nat_of_string_string_of_nat[simp]: "nat_of_string (string_of_nat n) = n" 
  unfolding string_of_nat_def 
  using nat_of_string_bij f_inv_into_f[of nat_of_string] by simp

lemma string_of_nat_nat_of_string[simp]: "string_of_nat (nat_of_string n) = n" 
  unfolding string_of_nat_def 
  using nat_of_string_bij inv_into_f_f[of nat_of_string] by simp


subsubsection ‹Enumerating Herbrand Atoms›

definition nat_of_hatom:: "hterm atom ⇒ nat" where
  "nat_of_hatom ≡ (SOME f. bij f)"

definition hatom_of_nat:: "nat ⇒ hterm atom" where
  "hatom_of_nat ≡ inv nat_of_hatom"

instantiation hterm :: countable begin
instance by countable_datatype
end

lemma infinite_hatoms: "infinite (UNIV :: ('t atom) set)"
proof -
  let ?diago = "λn. (string_of_nat n,[])"
  let ?undiago = "λa. nat_of_string (fst a)"
  have "∀n. ?undiago (?diago n) = n" using nat_of_string_string_of_nat by auto
  moreover
  have "∀n. ?diago n ∈ UNIV" by auto
  ultimately show "infinite (UNIV :: ('t atom) set)" using infinity[of ?undiago ?diago UNIV] by simp
qed

lemma nat_of_hatom_bij: "bij nat_of_hatom"
proof -
  let ?S = "UNIV :: (('t::countable) atom) set"
  have "countable ?S" by auto
  moreover
  have "infinite ?S" using infinite_hatoms by auto
  ultimately
  obtain x where "bij (x :: hterm atom ⇒ nat)" using countableE_infinite[of ?S] by blast
  then have "bij nat_of_hatom" unfolding nat_of_hatom_def using someI by metis
  then show "?thesis" unfolding bij_betw_def inj_on_def unfolding nat_of_hatom_def by simp
qed

lemma hatom_of_nat_bij: "bij hatom_of_nat" unfolding hatom_of_nat_def using nat_of_hatom_bij bij_betw_inv_into by auto

lemma nat_of_hatom_hatom_of_nat[simp]: "nat_of_hatom (hatom_of_nat n) = n" 
  unfolding hatom_of_nat_def 
  using nat_of_hatom_bij f_inv_into_f[of nat_of_hatom] by simp

lemma hatom_of_nat_nat_of_hatom[simp]: "hatom_of_nat (nat_of_hatom l) = l" 
  unfolding hatom_of_nat_def 
  using nat_of_hatom_bij inv_into_f_f[of nat_of_hatom _ UNIV] by simp


subsubsection ‹Enumerating Ground Atoms›

definition fatom_of_nat :: "nat ⇒ fterm atom" where
  "fatom_of_nat = (λn. fatom_of_hatom (hatom_of_nat n))"

definition nat_of_fatom :: "fterm atom ⇒ nat" where
  "nat_of_fatom = (λt. nat_of_hatom (hatom_of_fatom t))"

theorem diag_undiag_fatom[simp]: 
  assumes "ground⇩t⇩s ts"
  shows "fatom_of_nat (nat_of_fatom (p,ts)) = (p,ts)"
using assms unfolding fatom_of_nat_def nat_of_fatom_def by auto

theorem undiag_diag_fatom[simp]: "nat_of_fatom (fatom_of_nat n) = n" unfolding fatom_of_nat_def nat_of_fatom_def by auto

lemma fatom_of_nat_bij: "bij_betw fatom_of_nat UNIV ground_fatoms" 
  using hatom_of_nat_bij bij_betw_trans fatom_of_hatom_bij hatom_of_nat_bij unfolding fatom_of_nat_def comp_def by blast

lemma ground_fatom_of_nat: "ground⇩t⇩s (snd (fatom_of_nat x))" unfolding fatom_of_nat_def using ground_fatom_of_hatom by auto

lemma nat_of_fatom_bij: "bij_betw nat_of_fatom ground_fatoms UNIV"
   using nat_of_hatom_bij bij_betw_trans hatom_of_fatom_bij hatom_of_nat_bij unfolding nat_of_fatom_def comp_def by blast

end