theory TermsAndLiterals imports Main "~~/src/HOL/Library/Countable_Set" begin
section{* Terms and Literals *}
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"
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: "ground⇩l l ⟹ get_atom l ∈ ground_fatoms"
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 {* Convertions terms and Herbrand term *}
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 [simp]: "hterm_of_fterm (fterm_of_hterm t) = t"
by (induction t) (simp add: map_idI)
lemma [simp]: "hterms_of_fterms (fterms_of_hterms ts) = ts"
unfolding hterms_of_fterms_def fterms_of_hterms_def by (simp add: map_idI)
lemma [simp]: "ground⇩t t ⟹ fterm_of_hterm (hterm_of_fterm t) = t"
by (induction t) (auto simp add: map_idI)
lemma [simp]: "ground⇩t⇩s ts ⟹ fterms_of_hterms (hterms_of_fterms ts) = ts"
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 {* Converstions 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]: "ground⇩l l ⟹ flit_of_hlit (hlit_of_flit l) = l" 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 {* Convertions 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]: "ground⇩t⇩s (snd l) ⟹ fatom_of_hatom (hatom_of_fatom l) = l" 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_from_string:: "string ⇒ nat" where
"nat_from_string ≡ (SOME f. bij f)"
definition string_from_nat:: "nat ⇒ string" where
"string_from_nat ≡ inv nat_from_string"
lemma nat_from_string_bij: "bij nat_from_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_from_string_def using someI by metis
qed
lemma string_from_nat_bij: "bij string_from_nat" unfolding string_from_nat_def using nat_from_string_bij bij_betw_inv_into by auto
lemma nat_from_string_string_from_nat[simp]: "nat_from_string (string_from_nat n) = n"
unfolding string_from_nat_def
using nat_from_string_bij f_inv_into_f[of nat_from_string] by simp
lemma string_from_nat_nat_from_string[simp]: "string_from_nat (nat_from_string n) = n"
unfolding string_from_nat_def
using nat_from_string_bij inv_into_f_f[of nat_from_string] by simp
subsubsection {* Enumerating hatoms *}
definition nat_from_hatom:: "hterm atom ⇒ nat" where
"nat_from_hatom ≡ (SOME f. bij f)"
definition hatom_from_nat:: "nat ⇒ hterm atom" where
"hatom_from_nat ≡ inv nat_from_hatom"
instantiation hterm :: countable begin
instance by countable_datatype
end
lemma infinite_hatoms: "infinite (UNIV :: (pred_sym * 't list) set)"
proof -
let ?diago = "λn. (string_from_nat n,[])"
let ?undiago = "λa. nat_from_string (fst a)"
have "∀n. ?undiago (?diago n) = n" using nat_from_string_string_from_nat by auto
moreover
have "∀n. ?diago n ∈ UNIV" by auto
ultimately show "infinite (UNIV :: (pred_sym * 't list) set)" using infinity[of ?undiago ?diago UNIV] by simp
qed
lemma nat_from_hatom_bij: "bij nat_from_hatom"
proof -
let ?S = "UNIV :: (pred_sym * ('t::countable) list) 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_from_hatom" unfolding nat_from_hatom_def using someI by metis
then show "?thesis" unfolding bij_betw_def inj_on_def unfolding nat_from_hatom_def by simp
qed
lemma hatom_from_nat_bij: "bij hatom_from_nat " unfolding hatom_from_nat_def using nat_from_hatom_bij bij_betw_inv_into by auto
lemma nat_from_hatom_hatom_from_nat[simp]: "nat_from_hatom (hatom_from_nat n) = n"
unfolding hatom_from_nat_def
using nat_from_hatom_bij f_inv_into_f[of nat_from_hatom] by simp
lemma hatom_from_nat_nat_from_hatom[simp]: "hatom_from_nat (nat_from_hatom l) = l"
unfolding hatom_from_nat_def
using nat_from_hatom_bij inv_into_f_f[of nat_from_hatom _ UNIV] by simp
subsubsection {* Enumerating ground atoms *}
definition fatom_from_nat :: "nat ⇒ fterm atom" where
"fatom_from_nat = (λn. fatom_of_hatom (hatom_from_nat n))"
definition nat_from_fatom :: "fterm atom ⇒ nat" where
"nat_from_fatom = (λt. nat_from_hatom (hatom_of_fatom t))"
theorem diag_undiag_fatom[simp]: "ground⇩t⇩s ts ⟹ fatom_from_nat (nat_from_fatom (p,ts)) = (p,ts)"
unfolding fatom_from_nat_def nat_from_fatom_def by auto
theorem undiag_diag_fatom[simp]: "nat_from_fatom (fatom_from_nat n) = n" unfolding fatom_from_nat_def nat_from_fatom_def by auto
lemma fatom_from_nat_bij: "bij_betw fatom_from_nat UNIV ground_fatoms"
using hatom_from_nat_bij bij_betw_trans fatom_of_hatom_bij hatom_from_nat_bij unfolding fatom_from_nat_def comp_def by blast
lemma ground_fatom_from_nat: "ground⇩t⇩s (snd (fatom_from_nat x))" unfolding fatom_from_nat_def using ground_fatom_of_hatom by auto
lemma nat_from_fatom_bij: "bij_betw nat_from_fatom ground_fatoms UNIV"
using nat_from_hatom_bij bij_betw_trans hatom_of_fatom_bij hatom_from_nat_bij unfolding nat_from_fatom_def comp_def by blast
end