Session Resolution_FOL

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 groundt :: "fterm  bool" where
  "groundt (Var x)  False"
| "groundt (Fun f ts)  (t  set ts. groundt t)"

abbreviation groundts :: "fterm list  bool" where
  "groundts ts  (t  set ts. groundt t)"

abbreviation groundl :: "fterm literal  bool" where
  "groundl l  groundts (get_terms l)"

abbreviation groundls :: "fterm literal set  bool" where
  "groundls C  (l  C. groundl l)"
  
definition ground_fatoms :: "fterm atom set" where
  "ground_fatoms  {a. groundts (snd a)}"

lemma groundl_ground_fatom: 
  assumes "groundl 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 "aA"
  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 "bB"
  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 "groundt 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 "groundts 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:  "groundt (fterm_of_hterm t)"
  by (induction t) (auto simp add: map_idI)

lemma ground_fterms_of_hterms: "groundts (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: "groundl (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 "groundl 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. groundl l} UNIV" 
 unfolding bij_betw_def
proof
  show "inj_on hlit_of_flit {l. groundl l}" using inj_on_inverseI flit_of_hlit_hlit_of_flit 
    by (metis (mono_tags, lifting) mem_Collect_eq) 
next 
  have "l. l'. groundl 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. groundl l} = UNIV" by auto
qed

lemma flit_of_hlit_bij: "bij_betw flit_of_hlit UNIV {l. groundl l}" 
 unfolding bij_betw_def inj_on_def
proof
  show "xUNIV. yUNIV. 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. groundl l  (l = flit_of_hlit (hlit_of_flit l))" using hlit_of_flit_flit_of_hlit by auto
  then have "{l. groundl l}   flit_of_hlit ` UNIV " by blast
  moreover
  have "l. groundl (flit_of_hlit l)" using ground_flit_of_hlit by auto
  ultimately show "flit_of_hlit ` UNIV = {l. groundl 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: "groundts (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 "groundts (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'. groundts (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 "xUNIV. yUNIV. 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. groundts (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. groundts (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 "groundts 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: "groundts (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

Theory Tree

section ‹Trees›

theory Tree imports Main begin

text ‹Sometimes it is nice to think of @{typ bool}s as directions in a binary tree›
hide_const (open) Left Right
type_synonym dir = bool
definition Left :: bool where "Left = True"
definition Right :: bool where "Right = False"
declare Left_def [simp]
declare Right_def [simp]

datatype tree =
  Leaf
| Branching (ltree: tree) (rtree: tree) 


subsection ‹Sizes›

fun treesize :: "tree  nat" where
  "treesize Leaf = 0"
| "treesize (Branching l r) = 1 + treesize l + treesize r"

lemma treesize_Leaf:
  assumes "treesize T = 0"
  shows "T = Leaf"
  using assms by (cases T) auto

lemma treesize_Branching:
  assumes "treesize T = Suc n"
  shows "l r. T = Branching l r" 
  using assms by (cases T) auto


subsection ‹Paths›

fun path :: "dir list  tree  bool" where
  "path [] T  True"
| "path (d#ds) (Branching T1 T2)  (if d then path ds T1 else path ds T2)"
| "path _ _  False"

lemma path_inv_Leaf: "path p Leaf  p = []"
  by (induction p)  auto

lemma path_inv_Cons: "path (a#ds) T  (l r. T=Branching l r)"
  by  (cases T) (auto simp add: path_inv_Leaf)


lemma path_inv_Branching_Left: "path (Left#p) (Branching l r)  path p l"
  using Left_def Right_def path.cases by (induction p) auto

lemma path_inv_Branching_Right: "path (Right#p) (Branching l r)  path p r"
using Left_def Right_def path.cases by (induction p)  auto


lemma path_inv_Branching: 
  "path p (Branching l r)  (p=[]  (a p'. p=a#p' (a  path p' l)  (¬a  path p' r)))" (is "?L  ?R")
proof
  assume ?L then show ?R by (induction p) auto
next
  assume r: ?R
  then show ?L
    proof
      assume "p = []" then show ?L by auto
    next
      assume "a p'. p=a#p' (a  path p' l)  (¬a  path p' r)"
      then obtain a p' where "p=a#p' (a  path p' l)  (¬a  path p' r)" by auto
      then show ?L by (cases a) auto
    qed
qed

lemma path_prefix: 
  assumes "path (ds1@ds2) T"
  shows "path ds1 T"
using assms proof (induction ds1 arbitrary: T)
  case (Cons a ds1)
  then have "l r. T = Branching l r" using path_inv_Leaf by (cases T) auto
  then obtain l r where p_lr: "T = Branching l r" by auto
  show ?case
    proof (cases a)
      assume atrue: "a"
      then have "path ((ds1) @ ds2) l" using p_lr Cons(2) path_inv_Branching by auto
      then have "path ds1 l" using Cons(1) by auto
      then show "path (a # ds1) T" using p_lr atrue by auto
    next
      assume afalse: "¬a"
      then have "path ((ds1) @ ds2) r" using p_lr Cons(2) path_inv_Branching by auto
      then have "path ds1 r" using Cons(1) by auto
      then show "path (a # ds1) T" using p_lr afalse by auto
    qed
next
  case (Nil) then show ?case  by auto
qed


subsection ‹Branches›

fun branch :: "dir list  tree  bool" where
  "branch [] Leaf  True"    
| "branch (d # ds) (Branching l r)  (if d then branch ds l else branch ds r)"
| "branch _ _  False"

lemma has_branch: "b. branch b T"
proof (induction T)
  case (Leaf) 
  have "branch [] Leaf" by auto
  then show ?case by blast
next
  case (Branching T1 T2)
  then obtain b where "branch b T1" by auto
  then have "branch (Left#b) (Branching T1 T2)"  by auto
  then show ?case by blast
qed

lemma branch_inv_Leaf: "branch b Leaf  b = []"
by (cases b) auto

lemma branch_inv_Branching_Left:  
  "branch (Left#b) (Branching l r)  branch b l"
by auto

lemma branch_inv_Branching_Right: 
  "branch (Right#b) (Branching l r)  branch b r"
by auto

lemma branch_inv_Branching: 
  "branch b (Branching l r)  
     (a b'. b=a#b' (a  branch b' l)  (¬a   branch b' r))"
by (induction b) auto

lemma branch_inv_Leaf2:
  "T = Leaf  (b. branch b T  b = [])"
proof -
  {
    assume "T=Leaf"
    then have "b. branch b T  b = []" using branch_inv_Leaf by auto
  }
  moreover 
  {
    assume "b. branch b T  b = []"
    then have "b. branch b T  ¬(a b'. b = a # b')" by auto
    then have "b. branch b T  ¬(l r. branch b (Branching l r))" 
      using branch_inv_Branching by auto
    then have "T=Leaf" using has_branch[of T] by (metis branch.elims(2))
  }
  ultimately show "T = Leaf  (b. branch b T  b = [])" by auto
qed

lemma branch_is_path: 
  assumes"branch ds T"
  shows "path ds T"
using assms proof (induction T arbitrary: ds)
  case Leaf
  then have "ds = []" using branch_inv_Leaf by auto
  then show ?case  by auto
next
  case (Branching T1 T2) 
  then obtain a b where ds_p: "ds = a # b  (a  branch b T1)  (¬ a  branch b T2)" using branch_inv_Branching[of ds] by blast
  then have "(a  path b T1)  (¬a  path b T2)" using Branching by auto
  then show "?case" using ds_p by (cases a) auto
qed

lemma Branching_Leaf_Leaf_Tree:
  assumes "T = Branching T1 T2"
  shows "(B. branch (B@[True]) T  branch (B@[False]) T)"
using assms proof (induction T arbitrary: T1 T2)
  case Leaf then show ?case by auto
next
  case (Branching T1' T2')
  {
    assume "T1'=Leaf  T2'=Leaf"
    then have "branch ([] @ [True]) (Branching T1' T2')  branch ([] @ [False]) (Branching T1' T2')" by auto
    then have ?case by metis
  }
  moreover
  {
    fix T11 T12
    assume "T1' = Branching T11 T12"
    then obtain B where "branch (B @ [True]) T1' 
                        branch (B @ [False]) T1'" using Branching by blast
    then have "branch (([True] @ B) @ [True]) (Branching T1' T2') 
              branch (([True] @ B) @ [False]) (Branching T1' T2')" by auto
    then have ?case by blast
  }
  moreover
  {
    fix T11 T12
    assume "T2' = Branching T11 T12"
    then obtain B where "branch (B @ [True]) T2' 
                        branch (B @ [False]) T2'" using Branching by blast
    then have "branch (([False] @ B) @ [True]) (Branching T1' T2') 
              branch (([False] @ B) @ [False]) (Branching T1' T2')" by auto
    then have ?case by blast
  }
  ultimately show ?case using tree.exhaust by blast
qed


subsection ‹Internal Paths›

fun internal :: "dir list  tree  bool" where
  "internal [] (Branching l r)  True"
| "internal (d#ds) (Branching l r)  (if d then internal ds l else internal ds r)"
| "internal _ _  False"

lemma internal_inv_Leaf: "¬internal b Leaf" using internal.simps by blast

lemma internal_inv_Branching_Left:  
  "internal (Left#b) (Branching l r)  internal b l" by auto

lemma internal_inv_Branching_Right: 
  "internal (Right#b) (Branching l r)  internal b r"
by auto

lemma internal_inv_Branching: 
  "internal p (Branching l r)  (p=[]  (a p'. p=a#p' (a  internal p' l)  (¬a  internal p' r)))" (is "?L  ?R")
proof
  assume ?L then show ?R by (metis internal.simps(2) neq_Nil_conv) 
next
  assume r: ?R
  then show ?L
    proof
      assume "p = []" then show ?L by auto
    next
      assume "a p'. p=a#p' (a  internal p' l)  (¬a  internal p' r)"
      then obtain a p' where "p=a#p' (a  internal p' l)  (¬a  internal p' r)" by auto
      then show ?L by (cases a) auto
    qed
qed

lemma internal_is_path: 
  assumes "internal ds T"
  shows "path ds T"
using assms proof (induction T arbitrary: ds)
  case Leaf
  then have "False" using internal_inv_Leaf by auto
  then show ?case by auto
next
  case (Branching T1 T2) 
  then obtain a b where ds_p: "ds=[]  ds = a # b  (a  internal b T1)  (¬ a  internal b T2)" using internal_inv_Branching by blast
  then have "ds = []  (a  path b T1)  (¬a  path b T2)" using Branching by auto
  then show "?case" using ds_p by (cases a) auto
qed

lemma internal_prefix:
  assumes "internal (ds1@ds2@[d]) T"
  shows "internal ds1 T" (* more or less copy paste of path_prefix *)
using assms proof (induction ds1 arbitrary: T)
  case (Cons a ds1)
  then have "l r. T = Branching l r" using internal_inv_Leaf by (cases T) auto
  then obtain l r where p_lr: "T = Branching l r" by auto
  show ?case
    proof (cases a)
      assume atrue: "a"
      then have "internal ((ds1) @ ds2 @[d]) l" using p_lr Cons(2) internal_inv_Branching by auto
      then have "internal ds1 l" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr atrue by auto
    next
      assume afalse: "~a"
      then have "internal ((ds1) @ ds2 @[d]) r" using p_lr Cons(2) internal_inv_Branching by auto
      then have "internal ds1 r" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr afalse by auto
    qed
next
  case (Nil)
  then have "l r. T = Branching l r" using internal_inv_Leaf by (cases T) auto 
  then show ?case by auto
qed


lemma internal_branch:
  assumes "branch (ds1@ds2@[d]) T"
  shows "internal ds1 T" (* more or less copy paste of path_prefix *)
using assms proof (induction ds1 arbitrary: T)
  case (Cons a ds1)
  then have "l r. T = Branching l r" using branch_inv_Leaf by (cases T) auto
  then obtain l r where p_lr: "T = Branching l r" by auto
  show ?case
    proof (cases a)
      assume atrue: "a"
      then have "branch (ds1 @ ds2 @ [d]) l" using p_lr Cons(2) branch_inv_Branching by auto
      then have "internal ds1 l" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr atrue by auto
    next
      assume afalse: "~a"
      then have "branch ((ds1) @ ds2 @[d]) r" using p_lr Cons(2) branch_inv_Branching by auto
      then have "internal ds1 r" using Cons(1) by auto
      then show "internal (a # ds1) T" using p_lr afalse by auto
    qed
next
  case (Nil)
  then have "l r. T = Branching l r" using branch_inv_Leaf by (cases T) auto 
  then show ?case by auto
qed


fun parent :: "dir list  dir list" where
  "parent ds = tl ds"


subsection ‹Deleting Nodes›

fun delete :: "dir list  tree  tree" where
  "delete [] T = Leaf"
| "delete (True#ds)  (Branching T1 T2) = Branching (delete ds T1) T2"
| "delete (False#ds) (Branching T1 T2) = Branching T1 (delete ds T2)"
| "delete (a#ds) Leaf = Leaf"

lemma delete_Leaf: "delete T Leaf = Leaf" by (cases T) auto

lemma path_delete: 
  assumes "path p (delete ds T)"
  shows "path p T " (* What a huge proof... But the four cases can be proven shorter *)
using assms proof (induction p arbitrary: T ds)
  case Nil 
  then show ?case by simp
next
  case (Cons a p)
  then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto

  have "dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons by auto
  then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto

  then have "T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *)
        by (cases T; cases ds) auto
  then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto

  {
    assume a_p: "a"
    assume b_p: "¬b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (T1) (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "path p T1" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "path p T2" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "a"
    assume b_p: "b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T1)" using a_p by auto
    then have "path p T1" using Cons by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "¬b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T2)" using a_p by auto
    then have "path p T2" using Cons by auto
    then have ?case using T1T2_p a_p by auto
  }
  ultimately show ?case by blast
qed

lemma branch_delete:
  assumes "branch p (delete ds T)"
  shows "branch p T  p=ds" (* Adapted from above *)
using assms proof (induction p arbitrary: T ds)
  case Nil 
  then have "delete ds T = Leaf" by (cases "delete ds T") auto
  then have "ds = []  T = Leaf" using delete.elims by blast 
  then show ?case by auto
next
  case (Cons a p)
  then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto

  have "dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons branch_is_path by blast
  then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto

  then have "T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *)
        by (cases T; cases ds) auto
  then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto

  {
    assume a_p: "a"
    assume b_p: "¬b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching (T1) (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "branch p T1" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "branch p T2" using a_p by auto
    then have ?case using T1T2_p a_p by auto
  }
  moreover
  {
    assume a_p: "a"
    assume b_p: "b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "branch p (delete ds' T1)" using a_p by auto
    then have "branch p T1  p = ds'" using Cons by metis
    then have ?case using T1T2_p a_p using bds'_p a_p b_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "¬b"
    have "branch (a # p) (delete ds T)" using Cons by -
    then have "branch (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "branch p (delete ds' T2)" using a_p by auto
    then have "branch p T2  p = ds'" using Cons by metis
    then have ?case using T1T2_p a_p using bds'_p a_p b_p by auto
  }
  ultimately show ?case by blast
qed
  

lemma branch_delete_postfix: 
  assumes "path p (delete ds T)"
  shows "¬(c cs. p = ds @ c#cs)" (* Adapted from previous proof *)
using assms proof (induction p arbitrary: T ds)
  case Nil then show ?case by simp
next
  case (Cons a p)
  then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto

  have "dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons by auto
  then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto

  then have "T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *)
        by (cases T; cases ds) auto
  then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto

  {
    assume a_p: "a"
    assume b_p: "¬b"
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "b"
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  moreover
  {
    assume a_p: "a"
    assume b_p: "b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T1)" using a_p by auto
    then have "¬ (c cs. p = ds' @ c # cs)" using Cons by auto
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  moreover
  {
    assume a_p: "¬a"
    assume b_p: "¬b"
    have "path (a # p) (delete ds T)" using Cons by -
    then have "path (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto
    then have "path p (delete ds' T2)" using a_p by auto
    then have "¬ (c cs. p = ds' @ c # cs)" using Cons by auto
    then have ?case using T1T2_p a_p b_p bds'_p by auto
  }
  ultimately show ?case by blast
qed

lemma treezise_delete: 
  assumes "internal p T"
  shows "treesize (delete p T) < treesize T"
using assms proof (induction p arbitrary: T)
  case (Nil)
  then have "T1 T2. T = Branching T1 T2" by (cases T) auto
  then obtain T1 T2 where T1T2_p: "T = Branching T1 T2" by auto 
  then show ?case by auto
next
  case (Cons a p) 
  then have "T1 T2. T = Branching T1 T2" using path_inv_Cons internal_is_path by blast
  then obtain T1 T2 where T1T2_p: "T = Branching T1 T2" by auto
  show ?case
    proof (cases a)
      assume a_p: a
      from a_p have "delete (a#p) T = (Branching (delete p T1) T2)" using T1T2_p by auto
      moreover
      from a_p have "internal p T1" using T1T2_p Cons by auto
      then have "treesize (delete p T1) < treesize T1" using Cons by auto
      ultimately
      show ?thesis using T1T2_p by auto
    next
      assume a_p: "¬a"
      from a_p have "delete (a#p) T = (Branching T1 (delete p T2))" using T1T2_p by auto
      moreover
      from a_p have "internal p T2" using T1T2_p Cons by auto
      then have "treesize (delete p T2) < treesize T2" using Cons by auto
      ultimately
      show ?thesis using T1T2_p by auto
    qed
qed


fun cutoff :: "(dir list  bool)  dir list  tree  tree" where
  "cutoff red ds (Branching T1 T2) = 
     (if red ds then Leaf else Branching (cutoff red (ds@[Left])  T1) (cutoff red (ds@[Right]) T2))"
| "cutoff red ds Leaf = Leaf"
text ‹Initially you should call @{const cutoff} with @{term "ds = []"}.
 If all branches are red, then @{const cutoff} gives a subtree.
 If all branches are red, then so are the ones in @{const cutoff}.
 The internal paths of @{const cutoff} are not red.›

lemma treesize_cutoff: "treesize (cutoff red ds T)  treesize T"
proof (induction T arbitrary: ds)
  case Leaf then show ?case by auto
next
  case (Branching T1 T2) 
  then have "treesize (cutoff red (ds@[Left]) T1) + treesize (cutoff red (ds@[Right]) T2)  treesize T1 + treesize T2" using add_mono by blast
  then show ?case by auto
qed

abbreviation anypath :: "tree  (dir list  bool)  bool" where
  "anypath T P  p. path p T  P p"

abbreviation anybranch :: "tree  (dir list  bool)  bool" where
  "anybranch T P  p. branch p T  P p"

abbreviation anyinternal :: "tree  (dir list  bool)  bool" where
  "anyinternal T P  p. internal p T  P p"

lemma cutoff_branch': 
  assumes "anybranch T (λb. red(ds@b))"
  shows "anybranch (cutoff red ds T) (λb. red(ds@b))"
using assms proof (induction T arbitrary: ds) (* This proof seems a bit excessive for such a simple theorem *)
  case (Leaf) 
  let ?T = "cutoff red ds Leaf"
  {
    fix b
    assume "branch b ?T"
    then have "branch b Leaf" by auto
    then have "red(ds@b)" using Leaf by auto
  }
  then show ?case by simp
next
  case (Branching T1 T2)
  let ?T = "cutoff red ds (Branching T1 T2)"
  from Branching have "p. branch (Left#p) (Branching T1 T2)  red (ds @ (Left#p))" by blast
  then have "p. branch p T1  red (ds @ (Left#p))"  by auto
  then have "anybranch T1 (λp. red ((ds @ [Left]) @ p))" by auto
  then have aa: "anybranch (cutoff red (ds @ [Left]) T1) (λp. red ((ds @ [Left]) @ p)) 
         " using Branching by blast

  from Branching have "p. branch (Right#p) (Branching T1 T2)  red (ds @ (Right#p))" by blast
  then have "p. branch p T2  red (ds @ (Right#p))" by auto
  then have "anybranch T2 (λp. red ((ds @ [Right]) @ p))" by auto
  then have bb: "anybranch (cutoff red (ds @ [Right]) T2) (λp. red ((ds @ [Right]) @ p)) 
         " using Branching by blast
  {           
    fix b
    assume b_p: "branch b ?T"
    have "red ds  ¬red ds" by auto
    then have "red(ds@b)"
      proof
        assume ds_p: "red ds"
        then have "?T = Leaf" by auto
        then have "b = []" using b_p branch_inv_Leaf by auto
        then show "red(ds@b)" using ds_p by auto
      next
        assume ds_p: "¬red ds"
        let ?T1' = "cutoff red (ds@[Left])  T1"
        let ?T2' = "cutoff red (ds@[Right]) T2"
        from ds_p have "?T = Branching ?T1' ?T2'" by auto
        from this b_p obtain a b' where "b = a # b'  (a  branch b' ?T1')  (¬a  branch b' ?T2' )" using branch_inv_Branching[of b ?T1' ?T2'] by auto
        then show "red(ds@b)" using aa bb by (cases a) auto
      qed
  }
  then show ?case by blast
qed

lemma cutoff_branch: 
  assumes "anybranch T (λp. red p)"
  shows "anybranch (cutoff red [] T) (λp. red p)" 
  using assms cutoff_branch'[of T red "[]"] by auto

lemma cutoff_internal': 
  assumes "anybranch T (λb. red(ds@b))" 
  shows "anyinternal (cutoff red ds T) (λb. ¬red(ds@b))"
using assms proof (induction T arbitrary: ds) (* This proof seems a bit excessive for such a simple theorem *)
  case (Leaf) then show ?case using internal_inv_Leaf by simp
next                                                     
  case (Branching T1 T2)
  let ?T = "cutoff red ds (Branching T1 T2)"
  from Branching have "p. branch (Left#p) (Branching T1 T2)  red (ds @ (Left#p))" by blast
  then have "p. branch p T1  red (ds @ (Left#p))" by auto
  then have "anybranch T1 (λp. red ((ds @ [Left]) @ p))" by auto
  then have aa: "anyinternal (cutoff red (ds @ [Left]) T1) (λp. ¬ red ((ds @ [Left]) @ p))" using Branching by blast

  from Branching have "p. branch (Right#p) (Branching T1 T2)  red (ds @ (Right#p))" by blast
  then have "p. branch p T2  red (ds @ (Right#p))" by auto
  then have "anybranch T2 (λp. red ((ds @ [Right]) @ p))" by auto
  then have bb: "anyinternal (cutoff red (ds @ [Right]) T2) (λp. ¬ red ((ds @ [Right]) @ p))" using Branching by blast
  {
    fix p
    assume b_p: "internal p ?T"
    then have ds_p: "¬red ds" using internal_inv_Leaf by auto
    have "p=[]  p[]" by auto
    then have "¬red(ds@p)"
      proof
        assume "p=[]" then show "¬red(ds@p)" using ds_p by auto
      next
        let ?T1' = "cutoff red (ds@[Left])  T1"
        let ?T2' = "cutoff red (ds@[Right]) T2"
        assume "p[]"
        moreover
        have "?T = Branching ?T1' ?T2'" using ds_p by auto
        ultimately
        obtain a p' where b_p: "p = a # p' 
             (a  internal p' (cutoff red (ds @ [Left]) T1)) 
             (¬ a  internal p' (cutoff red (ds @ [Right]) T2))" 
          using b_p internal_inv_Branching[of p ?T1' ?T2'] by auto
        then have "¬red(ds @ [a] @ p')" using aa bb by (cases a) auto
        then show "¬red(ds @ p)" using b_p by simp
      qed
  }
  then show ?case by blast
qed

lemma cutoff_internal:
  assumes  "anybranch T red"
  shows "anyinternal (cutoff red [] T) (λp. ¬red p)" 
  using assms cutoff_internal'[of T red "[]"] by auto

lemma cutoff_branch_internal': 
  assumes "anybranch T red"
  shows "anyinternal (cutoff red [] T) (λp. ¬red p)  anybranch (cutoff red [] T) (λp. red p)" 
  using assms cutoff_internal[of T] cutoff_branch[of T] by blast

lemma cutoff_branch_internal: 
  assumes "anybranch T red"
  shows "T'. anyinternal T' (λp. ¬red p)  anybranch T' (λp. red p)" 
  using assms cutoff_branch_internal' by blast


section ‹Possibly Infinite Trees›
text ‹Possibly infinite trees are of type @{typ "dir list set"}.›

abbreviation wf_tree :: "dir list set  bool" where
  "wf_tree T  (ds d. (ds @ d)  T  ds  T)"

text ‹The subtree in with root r›
fun subtree :: "dir list set  dir list  dir list set" where 
  "subtree T r = {ds  T. ds'. ds = r @ ds'}" 

text ‹A subtree of a tree is either in the left branch, the right branch, or is the tree itself›
lemma subtree_pos: 
  "subtree T ds  subtree T (ds @ [Left])  subtree T (ds @ [Right])  {ds}"
proof (rule subsetI; rule Set.UnCI)
  let ?subtree = "subtree T"
  fix x
  assume asm: "x  ?subtree ds"
  assume "x  {ds}"
  then have "x  ds" by simp
  then have "e d. x = ds @ [d] @ e" using asm list.exhaust by auto
  then have "(e. x = ds @ [Left] @ e)  (e. x = ds @ [Right] @ e)" using bool.exhaust by auto
  then show "x  ?subtree (ds @ [Left])  ?subtree (ds @ [Right])" using asm by auto
qed


subsection ‹Infinite Paths›

abbreviation wf_infpath :: "(nat  'a list)  bool" where
  "wf_infpath f  (f 0 = [])  (n. a. f (Suc n) = (f n) @ [a])"

lemma infpath_length:
  assumes "wf_infpath f"
  shows "length (f n) = n"
using assms proof (induction n)
  case 0 then show ?case by auto
next
  case (Suc n) then show ?case by (metis length_append_singleton)
qed

lemma chain_prefix: 
  assumes "wf_infpath f"
  assumes "n1  n2"
  shows "a. (f n1) @ a = (f n2)"
using assms proof (induction n2)
  case (Suc n2)
  then have "n1  n2  n1 = Suc n2" by auto
  then show ?case
    proof
      assume "n1  n2"
      then obtain a where a: "f n1 @ a = f n2" using Suc by auto
      have b: "b. f (Suc n2) = f n2 @ [b]" using Suc by auto 
      from a b have "b. f n1 @ (a @ [b]) = f (Suc n2)" by auto
      then show "c. f n1 @ c = f (Suc n2)" by blast
    next
      assume "n1 = Suc n2"
      then have "f n1 @ [] = f (Suc n2)" by auto
      then show "a. f n1 @ a = f (Suc n2)" by auto
    qed
qed auto

text ‹If we make a lookup in a list, then looking up in an extension gives us the same value.›
lemma ith_in_extension:
  assumes chain: "wf_infpath f"
  assumes smalli: "i < length (f n1)"
  assumes n1n2: "n1  n2"
  shows "f n1 ! i = f n2 ! i"
proof -
  from chain n1n2 have "a. f n1 @ a = f n2" using chain_prefix by blast
  then obtain a where a_p: "f n1 @ a = f n2" by auto
  have "(f n1 @ a) ! i = f n1 ! i" using smalli by (simp add: nth_append) 
  then show ?thesis using a_p by auto
qed


section ‹König's Lemma›

lemma inf_subs: 
  assumes inf: "¬finite(subtree T ds)"
  shows "¬finite(subtree T (ds @ [Left]))  ¬finite(subtree T (ds @ [Right]))"
proof -
  let ?subtree = "subtree T"
  {
    assume asms: "finite(?subtree(ds @ [Left]))"
                 "finite(?subtree(ds @ [Right]))"
    have "?subtree ds  ?subtree (ds @ [Left] )  ?subtree (ds @ [Right])  {ds} " 
      using subtree_pos by auto
    then have "finite(?subtree (ds))" using asms by (simp add: finite_subset)
  } 
  then show "¬finite(?subtree (ds @ [Left]))  ¬finite(?subtree (ds @ [Right]))" using inf by auto
qed

fun buildchain :: "(dir list  dir list)  nat  dir list" where
  "buildchain next 0 = []"
| "buildchain next (Suc n) = next (buildchain next n)"

lemma konig:
  assumes inf: "¬finite T"
  assumes wellformed: "wf_tree T"
  shows "c. wf_infpath c  (n. (c n)  T)"
proof
  let ?subtree = "subtree T"
  let ?nextnode = "λds. (if ¬finite (?subtree (ds @ [Left])) then ds @ [Left] else ds @ [Right])" 

  let ?c = "buildchain ?nextnode"

  have is_chain: "wf_infpath ?c" by auto

  from wellformed have prefix: "ds d. (ds @ d)  T  ds  T" by blast

  { 
    fix n
    have "(?c n)  T  ¬finite (?subtree (?c n))"
      proof (induction n)
        case 0
        have "ds. ds  T" using inf by (simp add: not_finite_existsD)
        then obtain ds where "ds  T" by auto
        then have "([]@ds)  T" by auto
        then have "[]  T" using prefix by blast 
        then show ?case using inf by auto
      next
        case (Suc n)
        from Suc have next_in:  "(?c n)  T" by auto
        from Suc have next_inf: "¬finite (?subtree (?c n))" by auto

        from next_inf have next_next_inf:
           "¬finite (?subtree (?nextnode (?c n)))" 
              using inf_subs by auto
        then have "ds. ds  ?subtree (?nextnode (?c n))"
          by (simp add: not_finite_existsD)
        then obtain ds where dss: "ds  ?subtree (?nextnode (?c n))" by auto
        then have "ds  T" "suf. ds = (?nextnode (?c n)) @ suf" by auto
        then obtain suf where "ds  T  ds = (?nextnode (?c n)) @ suf" by auto
        then have "(?nextnode (?c n))  T"
          using prefix by blast
              
        then have "(?c (Suc n))  T" by auto
        then show ?case using next_next_inf by auto
      qed
  }
  then show "wf_infpath ?c  (n. (?c n) T) " using is_chain by auto
qed

end

Theory Resolution

section ‹More Terms and Literals›

theory Resolution imports TermsAndLiterals Tree begin

fun complement :: "'t literal  't literal" ("_c" [300] 300) where
  "(Pos P ts)c = Neg P ts"  
| "(Neg P ts)c = Pos P ts"

lemma cancel_comp1: "(lc)c = l" by (cases l) auto   

lemma cancel_comp2:
  assumes asm: "l1c = l2c"
  shows "l1 = l2"
proof -
  from asm have "(l1c)c = (l2c)c" by auto
  then have "l1 = (l2c)c" using cancel_comp1[of l1] by auto
  then show ?thesis using cancel_comp1[of l2] by auto
qed

lemma comp_exi1: "l'. l' = lc" by (cases l) auto 

lemma comp_exi2: "l. l' = lc"
proof
  show "l' = (l'c)c" using cancel_comp1[of l'] by auto
qed

lemma comp_swap: "l1c = l2  l1 = l2c" 
proof -
  have "l1c = l2  l1 = l2c" using cancel_comp1[of l1] by auto
  moreover
  have "l1 = l2c  l1c = l2" using cancel_comp1 by auto
  ultimately
  show ?thesis by auto
qed

lemma sign_comp: "sign l1  sign l2  get_pred l1 = get_pred l2  get_terms l1 = get_terms l2  l2 = l1c"
by (cases l1; cases l2) auto

lemma sign_comp_atom: "sign l1  sign l2  get_atom l1 = get_atom l2  l2 = l1c"
by (cases l1; cases l2) auto


section ‹Clauses›

type_synonym 't clause = "'t literal set"

abbreviation complementls :: "'t literal set  't literal set" ("_C" [300] 300) where 
  "LC  complement ` L"

lemma cancel_compls1: "(LC)C = L"
apply (auto simp add: cancel_comp1)
apply (metis imageI cancel_comp1) 
done

lemma cancel_compls2:
  assumes asm: "L1C = L2C"
  shows "L1 = L2"
proof -
  from asm have "(L1C)C = (L2C)C" by auto
  then show ?thesis using cancel_compls1[of L1] cancel_compls1[of L2] by simp
qed

fun varst  :: "fterm  var_sym set" where
  "varst (Var x) = {x}"
| "varst (Fun f ts) = (t  set ts. varst t)"

abbreviation varsts :: "fterm list  var_sym set" where 
  "varsts ts  (t  set ts. varst t)"

definition varsl :: "fterm literal  var_sym set" where 
  "varsl l = varsts (get_terms l)"

definition varsls :: "fterm literal set  var_sym set" where 
  "varsls L  lL. varsl l"

lemma ground_varst:
  assumes "groundt t"
  shows "varst t = {}" 
using assms by (induction t) auto

lemma groundts_varsts: 
  assumes "groundts ts"
  shows "varsts ts = {}"
using assms ground_varst by auto

lemma groundl_varsl:
  assumes "groundl l"
  shows "varsl l = {}" 
  unfolding varsl_def using assms ground_varst by auto

lemma groundls_varsls: 
  assumes "groundls L"
  shows "varsls L = {}" unfolding varsls_def using assms groundl_varsl by auto

lemma ground_comp: "groundl (lc)  groundl l" by (cases l) auto

lemma  ground_compls: "groundls (LC)  groundls L" using ground_comp by auto

(* Alternative - Collect variables with vars and see if empty set *)


section ‹Semantics›

type_synonym 'u fun_denot  = "fun_sym   'u list  'u"
type_synonym 'u pred_denot = "pred_sym  'u list  bool"
type_synonym 'u var_denot  = "var_sym   'u"

fun evalt  :: "'u var_denot  'u fun_denot  fterm  'u" where
  "evalt E F (Var x) = E x"
| "evalt E F (Fun f ts) = F f (map (evalt E F) ts)"

abbreviation evalts :: "'u var_denot  'u fun_denot  fterm list  'u list" where
  "evalts E F ts  map (evalt E F) ts"

fun evall :: "'u var_denot  'u fun_denot  'u pred_denot  fterm literal  bool" where
  "evall E F G (Pos p ts)   G p (evalts E F ts)"
| "evall E F G (Neg p ts)  ¬G p (evalts E F ts)"

definition evalc :: "'u fun_denot  'u pred_denot  fterm clause  bool" where
  "evalc F G C  (E. l  C. evall E F G l)"

definition evalcs :: "'u fun_denot  'u pred_denot  fterm clause set  bool" where
  "evalcs F G Cs  (C  Cs. evalc F G C)"


subsection ‹Semantics of Ground Terms›

lemma ground_var_denott: 
  assumes "groundt t"
  shows "evalt E F t = evalt E' F t"
using assms proof (induction t)
  case (Var x)
  then have "False" by auto
  then show ?case by auto
next
  case (Fun f ts)
  then have "t  set ts. groundt t" by auto 
  then have "t  set ts. evalt E F t = evalt E' F t" using Fun by auto
  then have "evalts E F ts = evalts E' F ts" by auto
  then have "F f (map (evalt E F) ts) = F f (map (evalt E' F) ts)" by metis
  then show ?case by simp
qed

lemma ground_var_denotts: 
  assumes "groundts ts"
  shows "evalts E F ts = evalts E' F ts"
  using assms ground_var_denott by (metis map_eq_conv)


lemma ground_var_denot: 
  assumes "groundl l"
  shows "evall E F G l = evall E' F G l"
using assms proof (induction l)
  case Pos then show ?case using ground_var_denotts by (metis evall.simps(1) literal.sel(3))
next
  case Neg then show ?case using ground_var_denotts by (metis evall.simps(2) literal.sel(4))
qed


section ‹Substitutions›

type_synonym substitution = "var_sym  fterm" 

fun sub  :: "fterm  substitution  fterm" (infixl "t" 55) where
  "(Var x) t σ = σ x"
| "(Fun f ts) t σ = Fun f (map (λt. t t σ) ts)"

abbreviation subs :: "fterm list  substitution  fterm list" (infixl "ts" 55) where
  "ts ts σ  (map (λt. t t σ) ts)"

fun subl :: "fterm literal  substitution  fterm literal" (infixl "l" 55) where
  "(Pos p ts) l σ = Pos p (ts ts σ)"
| "(Neg p ts) l σ = Neg p (ts ts σ)"

abbreviation subls :: "fterm literal set  substitution  fterm literal set" (infixl "ls" 55) where
  "L ls σ  (λl. l l σ) ` L"

lemma subls_def2: "L ls σ = {l l σ|l. l  L}" by auto

definition instance_oft :: "fterm  fterm  bool" where
  "instance_oft t1 t2  (σ. t1 = t2 t σ)"

definition instance_ofts :: "fterm list  fterm list  bool" where
  "instance_ofts ts1 ts2  (σ. ts1 = ts2 ts σ)"

definition instance_ofl :: "fterm literal  fterm literal  bool" where
  "instance_ofl l1 l2  (σ. l1 = l2 l σ)"

definition instance_ofls :: "fterm clause  fterm clause  bool" where
  "instance_ofls C1 C2  (σ. C1 = C2 ls σ)"

lemma comp_sub: "(lc) l σ=(l l σ)c" 
by (cases l) auto

lemma compls_subls: "(LC) ls σ=(L ls σ)C" 
using comp_sub apply auto
apply (metis image_eqI)
done

lemma subls_union: "(L1  L2) ls σ = (L1 ls σ)  (L2 ls σ)" by auto

(* 
  Alternative: apply a substitution that is a bijection between the set of variables in C1 and some other set.
 *)
definition var_renaming_of :: "fterm clause  fterm clause  bool" where
  "var_renaming_of C1 C2  instance_ofls C1 C2  instance_ofls C2 C1"


subsection ‹The Empty Substitution›

abbreviation ε :: "substitution" where
  "ε  Var"

lemma empty_subt: "(t :: fterm) t ε = t" 
by (induction t) (auto simp add: map_idI)

lemma empty_subts: "ts ts ε = ts" 
using empty_subt by auto

lemma empty_subl: "l l ε = l" 
using empty_subts by (cases l) auto

lemma empty_subls: "L ls ε = L" 
using empty_subl by auto

lemma instance_oft_self: "instance_oft t t"
unfolding instance_oft_def
proof 
  show "t = t t ε" using empty_subt by auto
qed

lemma instance_ofts_self: "instance_ofts ts ts"
unfolding instance_ofts_def
proof 
  show "ts = ts ts ε" using empty_subts by auto
qed

lemma instance_ofl_self: "instance_ofl l l"
unfolding instance_ofl_def
proof 
  show "l = l l ε" using empty_subl by auto
qed

lemma instance_ofls_self: "instance_ofls L L"
unfolding instance_ofls_def
proof
  show "L = L ls ε" using empty_subls by auto
qed


subsection ‹Substitutions and Ground Terms›

lemma ground_sub: 
  assumes "groundt t"
  shows "t t σ = t"
using assms by (induction t) (auto simp add: map_idI)

lemma ground_subs: 
  assumes "groundts ts "
  shows " ts ts σ = ts" 
using assms ground_sub by (simp add: map_idI)

lemma groundl_subs: 
  assumes "groundl l "
  shows " l l σ = l" 
using assms ground_subs by (cases l) auto

lemma groundls_subls:
  assumes ground: "groundls L"
  shows "L ls σ = L"
proof -
  {
    fix l
    assume l_L: "l  L"
    then have "groundl l" using ground by auto
    then have "l = l l σ" using groundl_subs by auto
    moreover
    then have "l l σ  L ls σ" using l_L by auto
    ultimately
    have "l  L ls σ" by auto
  }
  moreover
  {
    fix l
    assume l_L: "l  L ls σ"
    then obtain l' where l'_p: "l'  L  l' l σ = l" by auto
    then have "l' = l" using ground groundl_subs by auto
    from l_L l'_p this have "l  L" by auto
  } 
  ultimately show ?thesis by auto
qed


subsection ‹Composition›

definition composition :: "substitution  substitution  substitution"  (infixl "" 55) where
  "(σ1  σ2) x = (σ1 x) t σ2"

lemma composition_conseq2t:  "(t t σ1) t σ2 = t t (σ1  σ2)" 
proof (induction t)
  case (Var x) 
  have "((Var x) t σ1) t σ2 = (σ1 x) t σ2" by simp
  also have " ... = (σ1  σ2) x" unfolding composition_def by simp
  finally show ?case by auto
next
  case (Fun t ts)
  then show ?case unfolding composition_def by auto
qed

lemma composition_conseq2ts: "(ts ts σ1) ts σ2 = ts ts (σ1  σ2)"
  using composition_conseq2t by auto

lemma composition_conseq2l: "(l l σ1) l σ2 = l l (σ1  σ2)" 
  using composition_conseq2t by (cases l) auto 

lemma composition_conseq2ls: "(L ls σ1) ls σ2 = L ls (σ1  σ2)" 
using composition_conseq2l apply auto
apply (metis imageI) 
done
  

lemma composition_assoc: "σ1  (σ2  σ3) = (σ1  σ2)  σ3" 
proof
  fix x
  show "(σ1  (σ2  σ3)) x = ((σ1  σ2)  σ3) x"
    by (simp only: composition_def composition_conseq2t)
qed

lemma empty_comp1: "(σ  ε) = σ" 
proof
  fix x
  show "(σ  ε) x = σ x" unfolding composition_def using empty_subt by auto 
qed

lemma empty_comp2: "(ε  σ) = σ" 
proof
  fix x
  show "(ε  σ) x = σ x" unfolding composition_def by simp
qed

lemma instance_oft_trans : 
  assumes t12: "instance_oft t1 t2"
  assumes t23: "instance_oft t2 t3"
  shows "instance_oft t1 t3"
proof -
  from t12 obtain σ12 where "t1 = t2 t σ12" 
    unfolding instance_oft_def by auto
  moreover
  from t23 obtain σ23 where "t2 = t3 t σ23" 
    unfolding instance_oft_def by auto
  ultimately
  have "t1 = (t3 t σ23) t σ12" by auto
  then have "t1 = t3 t (σ23  σ12)" using composition_conseq2t by simp
  then show ?thesis unfolding instance_oft_def by auto
qed

lemma instance_ofts_trans : 
  assumes ts12: "instance_ofts ts1 ts2"
  assumes ts23: "instance_ofts ts2 ts3"
  shows "instance_ofts ts1 ts3"
proof -
  from ts12 obtain σ12 where "ts1 = ts2 ts σ12" 
    unfolding instance_ofts_def by auto
  moreover
  from ts23 obtain σ23 where "ts2 = ts3 ts σ23" 
    unfolding instance_ofts_def by auto
  ultimately
  have "ts1 = (ts3 ts σ23) ts σ12" by auto
  then have "ts1 = ts3 ts (σ23  σ12)" using composition_conseq2ts by simp
  then show ?thesis unfolding instance_ofts_def by auto
qed

lemma instance_ofl_trans : 
  assumes l12: "instance_ofl l1 l2"
  assumes l23: "instance_ofl l2 l3"
  shows "instance_ofl l1 l3"
proof -
  from l12 obtain σ12 where "l1 = l2 l σ12" 
    unfolding instance_ofl_def by auto
  moreover
  from l23 obtain σ23 where "l2 = l3 l σ23" 
    unfolding instance_ofl_def by auto
  ultimately
  have "l1 = (l3 l σ23) l σ12" by auto
  then have "l1 = l3 l (σ23  σ12)" using composition_conseq2l by simp
  then show ?thesis unfolding instance_ofl_def by auto
qed

lemma instance_ofls_trans : 
  assumes L12: "instance_ofls L1 L2"
  assumes L23: "instance_ofls L2 L3"
  shows "instance_ofls L1 L3"
proof -
  from L12 obtain σ12 where "L1 = L2 ls σ12" 
    unfolding instance_ofls_def by auto
  moreover
  from L23 obtain σ23 where "L2 = L3 ls σ23" 
    unfolding instance_ofls_def by auto
  ultimately
  have "L1 = (L3 ls σ23) ls σ12" by auto
  then have "L1 = L3 ls (σ23  σ12)" using composition_conseq2ls by simp
  then show ?thesis unfolding instance_ofls_def by auto
qed


subsection ‹Merging substitutions›

lemma project_sub:
  assumes inst_C:"C ls lmbd = C'" 
  assumes L'sub: "L'  C'"
  shows "L  C. L ls lmbd = L'  (C-L) ls lmbd = C' - L'"
proof -
  let ?L = "{l  C. l'  L'. l l lmbd = l'}"
  have "?L  C" by auto
  moreover
  have "?L ls lmbd = L'"
    proof (rule Orderings.order_antisym; rule Set.subsetI)
      fix l'
      assume l'L: "l'  L'"
      from inst_C have "{l l lmbd|l. l  C} = C'" unfolding subls_def2 by -
      then have "l. l' = l l lmbd  l  C  l l lmbd  L'" using L'sub l'L by auto
      then have " l'  {l  C. l l lmbd  L'} ls lmbd" by auto
      then show " l'  {l  C. l'L'. l l lmbd = l'} ls lmbd" by auto
    qed auto
  moreover
  have "(C-?L) ls lmbd = C' - L'" using inst_C by auto
  ultimately show ?thesis
    by blast    
qed

lemma relevant_vars_subt:
  assumes "x  varst t. σ1 x = σ2 x"
  shows " t t σ1 = t t σ2"
using assms proof (induction t)
  case (Fun f ts)
  have f: "t. t  set ts  varst t  varsts ts" by (induction ts) auto
  have "tset ts. t t σ1 = t t σ2" 
    proof
      fix t
      assume tints: "t  set ts"
      then have "x  varst t. σ1 x = σ2 x" using f Fun(2) by auto
      then show "t t σ1 = t t σ2" using Fun tints by auto
    qed
  then have "ts ts σ1 = ts ts σ2" by auto
  then show ?case by auto
qed auto

lemma relevant_vars_subts: (* similar to above proof *)
  assumes asm: "x  varsts ts. σ1 x = σ2 x"
  shows "ts ts σ1 = ts ts σ2" 
proof -
   have f: "t. t  set ts  varst t  varsts ts" by (induction ts) auto
   have "tset ts. t t σ1 = t t σ2" 
    proof
      fix t
      assume tints: "t  set ts"
      then have "x  varst t. σ1 x = σ2 x" using f asm by auto
      then show "t t σ1 = t t σ2" using relevant_vars_subt tints by auto
    qed
  then show ?thesis by auto
qed

lemma relevant_vars_subl:
  assumes "x  varsl l. σ1 x = σ2 x "
  shows "l l σ1 = l l σ2"
using assms proof (induction l)
  case (Pos p ts)
  then show ?case using relevant_vars_subts unfolding varsl_def by auto
next
  case (Neg p ts)
  then show ?case using relevant_vars_subts unfolding varsl_def by auto
qed

lemma relevant_vars_subls: (* in many ways a mirror of relevant_vars_subts  *)
  assumes asm: "x  varsls L. σ1 x = σ2 x"
  shows "L ls σ1 = L ls σ2"
proof -
  have f: "l. l  L  varsl l  varsls L" unfolding varsls_def by auto
  have "l  L. l l σ1 = l l σ2"
    proof
      fix l
      assume linls: "lL"
      then have "xvarsl l. σ1 x = σ2 x" using f asm by auto
      then show "l l σ1 = l l σ2" using relevant_vars_subl linls by auto
    qed
  then show ?thesis by (meson image_cong) 
qed

lemma merge_sub:
  assumes dist: "varsls C  varsls D = {}"
  assumes CC': "C ls lmbd = C'"
  assumes DD': "D ls μ = D'"
  shows "η. C ls η = C'  D ls η = D'"
proof -
  let  = "λx. if x  varsls C then lmbd x else μ x"
  have " xvarsls C.  x = lmbd x" by auto
  then have "C ls  = C ls lmbd" using relevant_vars_subls[of C  lmbd] by auto
  then have "C ls  = C'" using CC' by auto
  moreover
  have " x  varsls D.  x = μ x" using dist by auto
  then have "D ls  = D ls μ" using relevant_vars_subls[of D  μ] by auto
  then have "D ls  = D'" using DD' by auto
  ultimately
  show ?thesis by auto
qed


subsection ‹Standardizing apart›

abbreviation std1 :: "fterm clause  fterm clause" where
  "std1 C  C ls (λx. Var (''1'' @ x))"

abbreviation std2 :: "fterm clause  fterm clause" where
  "std2 C  C ls (λx. Var (''2'' @ x))"

lemma std_apart_apart'': 
  assumes "x  varst  (t t (λx::char list. Var (y @ x)))"
  shows "x'. x = y@x'"
using assms by (induction t) auto

lemma std_apart_apart':
  assumes "x  varsl (l l (λx. Var  (y@x)))" 
  shows "x'. x = y@x'"
using assms unfolding varsl_def using std_apart_apart'' by (cases l) auto

lemma std_apart_apart: "varsls (std1 C1)  varsls (std2 C2) = {}"
proof -
  {
    fix x
    assume xin: "x  varsls (std1 C1)  varsls (std2 C2)"
    from xin have "x  varsls (std1 C1)" by auto
    then have "x'. x=''1'' @ x'" 
      using std_apart_apart'[of x _ "''1''"] unfolding varsls_def by auto
    moreover
    from xin have "x  varsls (std2 C2)" by auto
    then have "x'. x= ''2'' @x' " 
      using std_apart_apart'[of x _ "''2''"] unfolding varsls_def by auto
    ultimately have "False" by auto
    then have "x  {}" by auto
  }
  then show ?thesis by auto 
qed

lemma std_apart_instance_ofls1: "instance_ofls C1 (std1 C1)"
proof -
  have empty: "(λx. Var (''1''@x))  (λx. Var (tl x)) = ε" using composition_def by auto         

  have "C1 ls ε = C1" using empty_subls by auto
  then have "C1 ls ((λx. Var (''1''@x))  (λx. Var (tl x))) = C1" using empty by auto
  then have "(C1 ls (λx. Var (''1''@x))) ls (λx. Var (tl x)) = C1" using composition_conseq2ls by auto
  then have "C1 = (std1 C1) ls (λx. Var (tl x))" by auto
  then show "instance_ofls C1 (std1 C1)" unfolding instance_ofls_def by auto
qed

lemma std_apart_instance_ofls2: "instance_ofls C2 (std2 C2)"  
proof -
  have empty: "(λx. Var (''2''@x))  (λx. Var (tl x)) = ε" using composition_def by auto

  have "C2 ls ε = C2" using empty_subls by auto
  then have "C2 ls ((λx. Var (''2''@x))  (λx. Var (tl x))) = C2" using empty by auto
  then have "(C2 ls (λx. Var (''2''@x))) ls (λx. Var (tl x)) = C2" using composition_conseq2ls by auto
  then have "C2 = (std2 C2) ls (λx. Var (tl x))" by auto
  then show "instance_ofls C2 (std2 C2)" unfolding instance_ofls_def by auto
qed


section ‹Unifiers›

definition unifierts :: "substitution  fterm set  bool" where
  "unifierts σ ts  (t'. t  ts. t t σ = t')"

definition unifierls :: "substitution  fterm literal set  bool" where
  "unifierls σ L  (l'. l  L. l l σ = l')"

lemma unif_sub:
  assumes unif: "unifierls σ L"
  assumes nonempty: "L  {}"
  shows "l. subls L σ = {subl l σ}"
proof -
  from nonempty obtain l where "l  L" by auto
  from unif this have "L ls σ = {l l σ}" unfolding unifierls_def by auto
  then show ?thesis by auto
qed

lemma unifiert_def2: (*  (λt. sub t σ) ` ts could have some nice notation maybe *)
  assumes L_elem: "ts  {}"
  shows "unifierts σ ts  (l. (λt. sub t σ) ` ts ={l})"
proof
  assume unif: "unifierts σ ts"
  from L_elem obtain t where "t  ts" by auto
  then have "(λt. sub t σ) ` ts = {t t σ}" using unif unfolding unifierts_def by auto
  then show "l. (λt. sub t σ) ` ts = {l}" by auto
next
  assume "l. (λt. sub t σ) ` ts ={l}"
  then obtain l where "(λt. sub t σ) ` ts = {l}" by auto
  then have "l'  ts. l' t σ = l" by auto
  then show "unifierts σ ts" unfolding unifierts_def by auto
qed

lemma unifierls_def2: 
  assumes L_elem: "L  {}"
  shows "unifierls σ L  (l. L ls σ = {l})"
proof
  assume unif: "unifierls σ L"
  from L_elem obtain l where "l  L" by auto
  then have "L ls σ = {l l σ}" using unif unfolding unifierls_def by auto
  then show "l. L ls σ = {l}" by auto
next
  assume "l. L ls σ ={l}"
  then obtain l where "L ls σ = {l}" by auto
  then have "l'  L. l' l σ = l" by auto
  then show "unifierls σ L" unfolding unifierls_def by auto
qed

lemma groundls_unif_singleton:
  assumes groundls: "groundls L" 
  assumes unif: "unifierls σ' L"
  assumes empt: "L  {}"
  shows "l. L = {l}"
proof -
  from unif empt have "l. L ls σ' = {l}" using unif_sub by auto
  then show ?thesis using groundls_subls groundls by auto
qed

definition unifiablets :: "fterm set  bool" where
  "unifiablets fs  (σ. unifierts σ fs)"

definition unifiablels :: "fterm literal set  bool" where
  "unifiablels L  (σ. unifierls σ L)"

lemma unifier_comp[simp]: "unifierls σ (LC)  unifierls σ L"
proof
  assume "unifierls σ (LC)" 
  then obtain l'' where l''_p: "l  LC. l l σ = l''" 
    unfolding unifierls_def by auto
  obtain l' where "(l')c = l''" using comp_exi2[of l''] by auto
  from this l''_p have l'_p:"l  LC. l l σ = (l')c" by auto
  have "l  L. l l σ = l'"
    proof
      fix l
      assume "lL"
      then have "lc  LC" by auto
      then have "(lc) l σ = (l')c" using l'_p by auto
      then have "(l l σ)c = (l')c" by (cases l) auto
      then show "l l σ = l'" using cancel_comp2 by blast
    qed
  then show "unifierls σ L" unfolding unifierls_def by auto
next
  assume "unifierls σ L"
  then obtain l' where l'_p: "l  L. l l σ = l'" unfolding unifierls_def by auto
  have "l  LC. l l σ = (l')c"
    proof
      fix l
      assume "l  LC"
      then have "lc  L" using cancel_comp1 by (metis image_iff)
      then show "l l σ = (l')c" using l'_p comp_sub cancel_comp1 by metis
    qed
  then show "unifierls σ (LC)" unfolding unifierls_def by auto
qed

lemma unifier_sub1: 
  assumes "unifierls σ L"
  assumes "L'  L"
  shows "unifierls σ L' " 
  using assms unfolding unifierls_def by auto

lemma unifier_sub2: 
  assumes asm: "unifierls σ (L1  L2)"
  shows "unifierls σ L1  unifierls σ L2 "
proof -
  have "L1  (L1  L2)  L2  (L1  L2)" by simp
  from this asm show ?thesis using unifier_sub1 by auto
qed


subsection ‹Most General Unifiers›

definition mguts :: "substitution  fterm set  bool" where
  "mguts σ ts  unifierts σ ts  (u. unifierts u ts  (i. u = σ  i))"

definition mguls :: "substitution  fterm literal set  bool" where
  "mguls σ L  unifierls σ L  (u. unifierls u L  (i. u = σ  i))"


section ‹Resolution›

definition applicable :: "   fterm clause  fterm clause 
                           fterm literal set  fterm literal set 
                           substitution  bool" where
  "applicable C1 C2 L1 L2 σ  
       C1  {}  C2  {}  L1  {}  L2  {}
      varsls C1  varsls C2 = {} 
      L1  C1  L2  C2 
      mguls σ (L1  L2C)"

definition mresolution :: "   fterm clause  fterm clause 
                           fterm literal set  fterm literal set 
                           substitution  fterm clause" where
  "mresolution C1 C2 L1 L2 σ = ((C1 ls σ)- (L1 ls σ))  ((C2 ls σ) - (L2 ls σ))"

definition resolution :: "   fterm clause  fterm clause 
                           fterm literal set  fterm literal set 
                           substitution  fterm clause" where
  "resolution C1 C2 L1 L2 σ = ((C1 - L1)  (C2 - L2)) ls σ"

inductive mresolution_step :: "fterm clause set  fterm clause set  bool" where
  mresolution_rule:
    "C1  Cs  C2  Cs  applicable C1 C2 L1 L2 σ  
       mresolution_step Cs (Cs  {mresolution C1 C2 L1 L2 σ})"
| standardize_apart:
    "C  Cs  var_renaming_of C C'  mresolution_step Cs (Cs  {C'})"

inductive resolution_step :: "fterm clause set  fterm clause set  bool" where
  resolution_rule: 
    "C1  Cs  C2  Cs  applicable C1 C2 L1 L2 σ  
       resolution_step Cs (Cs  {resolution C1 C2 L1 L2 σ})"
| standardize_apart: (* renaming *)
    "C  Cs  var_renaming_of C C'  resolution_step Cs (Cs  {C'})"

definition mresolution_deriv :: "fterm clause set  fterm clause set  bool" where
  "mresolution_deriv = rtranclp mresolution_step"

definition resolution_deriv :: "fterm clause set  fterm clause set  bool" where
  "resolution_deriv = rtranclp resolution_step"


section ‹Soundness›

definition evalsub :: "'u var_denot  'u fun_denot  substitution  'u var_denot" where
  "evalsub E F σ = evalt E F  σ"

lemma substitutiont: "evalt E F (t t σ) = evalt (evalsub E F σ) F t"
apply (induction t)
 unfolding evalsub_def apply auto
apply (metis (mono_tags, lifting) comp_apply map_cong)
done

lemma substitutionts: "evalts E F (ts ts σ) = evalts (evalsub E F σ) F ts"
using substitutiont by auto

lemma substitution: "evall E F G (l l σ)  evall (evalsub E F σ) F G l"
apply (induction l) 
 using substitutionts apply (metis evall.simps(1) subl.simps(1)) 
using substitutionts apply (metis evall.simps(2) subl.simps(2))
done

lemma subst_sound:
 assumes asm: "evalc F G C"
 shows "evalc F G (C ls σ)"
unfolding evalc_def proof
  fix E
  from asm have "E'. l  C. evall E' F G l" using evalc_def by blast
  then have "l  C. evall (evalsub E F σ) F G l" by auto
  then show "l  C ls σ. evall E F G l" using substitution by blast
qed

lemma simple_resolution_sound:
  assumes C1sat:  "evalc F G C1"
  assumes C2sat:  "evalc F G C2"
  assumes l1inc1: "l1  C1"
  assumes l2inc2: "l2  C2"
  assumes comp: "l1c = l2"
  shows "evalc F G ((C1 - {l1})  (C2 - {l2}))"
proof -
  have "E. l  (((C1 - {l1})  (C2 - {l2}))). evall E F G l"
    proof
      fix E
      have "evall E F G l1  evall E F G l2" using comp by (cases l1) auto
      then show "l  (((C1 - {l1})  (C2 - {l2}))). evall E F G l"
        proof
          assume "evall E F G l1"
          then have "¬evall E F G l2" using comp by (cases l1) auto
          then have "l2' C2. l2'  l2  evall E F G l2'" using l2inc2 C2sat unfolding evalc_def by auto
          then show "l(C1 - {l1})  (C2 - {l2}). evall E F G l" by auto
        next
          assume "evall E F G l2" (* Symmetric *)
          then have "¬evall E F G l1" using comp by (cases l1) auto
          then have "l1' C1. l1'  l1  evall E F G l1'" using l1inc1 C1sat unfolding evalc_def by auto
          then show "l(C1 - {l1})  (C2 - {l2}). evall E F G l" by auto
        qed
    qed
  then show ?thesis unfolding evalc_def by simp
qed

lemma mresolution_sound:
  assumes sat1: "evalc F G C1"
  assumes sat2: "evalc F G C2"
  assumes appl: "applicable C1 C2 L1 L2 σ"
  shows "evalc F G (mresolution C1 C2 L1 L2 σ)"
proof -
  from sat1 have sat1σ: "evalc F G (C1 ls σ)" using subst_sound by blast
  from sat2 have sat2σ: "evalc F G (C2 ls σ)" using subst_sound by blast

  from appl obtain l1 where l1_p: "l1  L1" unfolding applicable_def by auto

  from l1_p appl have "l1  C1" unfolding applicable_def by auto
  then have inc1σ: "l1 l σ  C1 ls σ" by auto
  
  from l1_p have unified1: "l1  (L1  (L2C))" by auto

  from l1_p appl have l1σisl1σ: "{l1 l σ} = L1 ls σ"  
    unfolding mguls_def unifierls_def applicable_def by auto

  from appl obtain l2 where l2_p: "l2  L2" unfolding applicable_def by auto
  
  from l2_p appl have "l2  C2" unfolding applicable_def by auto
  then have inc2σ: "l2 l σ  C2 ls σ" by auto

  from l2_p have unified2: "l2c  (L1  (L2C))" by auto

  from unified1 unified2 appl have "l1 l σ = (l2c) l σ" 
    unfolding mguls_def unifierls_def applicable_def by auto
  then have comp: "(l1 l σ)c = l2 l σ" using comp_sub comp_swap by auto 

  from appl have "unifierls σ (L2C)" 
    using unifier_sub2 unfolding mguls_def applicable_def by blast
  then have "unifierls σ L2" by auto
  from this l2_p have l2σisl2σ: "{l2 l σ} = L2 ls σ" unfolding unifierls_def by auto

  from sat1σ sat2σ inc1σ inc2σ comp have "evalc F G ((C1 ls σ) - {l1 l σ}  ((C2 ls σ) - {l2 l σ}))" using simple_resolution_sound[of F G "C1 ls σ" "C2 ls σ" "l1 l σ" " l2 l σ"]
    by auto
  from this l1σisl1σ l2σisl2σ show ?thesis unfolding mresolution_def by auto
qed

lemma resolution_superset: "mresolution C1 C2 L1 L2 σ  resolution C1 C2 L1 L2 σ"
 unfolding mresolution_def resolution_def by auto

lemma superset_sound:
  assumes sup: "C  C'"
  assumes sat: "evalc F G C"
  shows "evalc F G C'"
proof -
  have "E. l  C'. evall E F G l"
    proof
      fix E
      from sat have "E. l  C. evall E F G l" unfolding evalc_def by -
      then have "l  C . evall E F G l" by auto
      then show "l  C'. evall E F G l" using sup by auto
    qed
  then show "evalc F G C'" unfolding evalc_def by auto
qed
 
theorem resolution_sound:
  assumes sat1: "evalc F G C1"
  assumes sat2: "evalc F G C2"
  assumes appl: "applicable C1 C2 L1 L2 σ"
  shows "evalc F G (resolution C1 C2 L1 L2 σ)"
proof -
  from sat1 sat2 appl have "evalc F G (mresolution C1 C2 L1 L2 σ)" using mresolution_sound by blast
  then show ?thesis using superset_sound resolution_superset by metis
qed

lemma mstep_sound: 
  assumes "mresolution_step Cs Cs'"
  assumes "evalcs F G Cs"
  shows "evalcs F G Cs'"
using assms proof (induction rule: mresolution_step.induct)
  case (mresolution_rule C1 Cs C2 l1 l2 σ)
  then have "evalc F G C1  evalc F G C2" unfolding evalcs_def by auto
  then have "evalc F G (mresolution C1 C2 l1 l2 σ)" 
    using mresolution_sound mresolution_rule by auto
  then show ?case using mresolution_rule unfolding evalcs_def by auto
next
  case (standardize_apart C Cs C')
  then have "evalc F G C" unfolding evalcs_def by auto
  then have "evalc F G C'" using subst_sound standardize_apart unfolding var_renaming_of_def instance_ofls_def by metis
  then show ?case using standardize_apart unfolding evalcs_def by auto
qed

theorem step_sound: 
  assumes "resolution_step Cs Cs'"
  assumes "evalcs F G Cs"
  shows "evalcs F G Cs'"
using assms proof (induction rule: resolution_step.induct)
  case (resolution_rule C1 Cs C2 l1 l2 σ)
  then have "evalc F G C1  evalc F G C2" unfolding evalcs_def by auto
  then have "evalc F G (resolution C1 C2 l1 l2 σ)" 
    using resolution_sound resolution_rule by auto
  then show ?case using resolution_rule unfolding evalcs_def by auto
next
  case (standardize_apart C Cs C')
  then have "evalc F G C" unfolding evalcs_def by auto
  then have "evalc F G C'" using subst_sound standardize_apart unfolding var_renaming_of_def instance_ofls_def by metis
  then show ?case using standardize_apart unfolding evalcs_def by auto
qed

lemma mderivation_sound: 
  assumes "mresolution_deriv Cs Cs'"
  assumes "evalcs F G Cs"
  shows "evalcs F G Cs'" 
using assms unfolding mresolution_deriv_def
proof (induction rule: rtranclp.induct)
  case rtrancl_refl then show ?case by auto
next
  case (rtrancl_into_rtrancl Cs1 Cs2 Cs3) then show ?case using mstep_sound by auto
qed

theorem derivation_sound: 
  assumes "resolution_deriv Cs Cs'"
  assumes "evalcs F G Cs"
  shows"evalcs F G Cs'" 
using assms unfolding resolution_deriv_def
proof (induction rule: rtranclp.induct)
  case rtrancl_refl then show ?case by auto
next
  case (rtrancl_into_rtrancl Cs1 Cs2 Cs3) then show ?case using step_sound by auto
qed
  
theorem derivation_sound_refute: 
  assumes deriv: "resolution_deriv Cs Cs'  {}  Cs'"
  shows "¬evalcs F G Cs"
proof -
  from deriv have "evalcs F G Cs  evalcs F G Cs'" using derivation_sound by auto
  moreover
  from deriv have "evalcs F G Cs'  evalc F G {}" unfolding evalcs_def by auto
  moreover
  then have "evalc F G {}  False" unfolding evalc_def by auto
  ultimately show ?thesis by auto
qed


section ‹Herbrand Interpretations›

text @{const HFun} is the Herbrand function denotation in which terms are mapped to themselves.›
term HFun

lemma eval_groundt: 
  assumes "groundt t"
  shows "(evalt E HFun t) = hterm_of_fterm t"
  using assms by (induction t) auto


lemma eval_groundts: 
  assumes "groundts ts"
  shows "(evalts E HFun ts) = hterms_of_fterms ts" 
  unfolding hterms_of_fterms_def using assms eval_groundt by (induction ts) auto

lemma evall_groundts:
  assumes asm: "groundts ts"
  shows "evall E HFun G (Pos P ts)  G P (hterms_of_fterms ts)"
proof -
  have "evall E HFun G (Pos P ts) = G P (evalts E HFun ts)" by auto
  also have "... = G P (hterms_of_fterms ts)" using asm eval_groundts by simp 
  finally show ?thesis by auto
qed


section ‹Partial Interpretations›

type_synonym partial_pred_denot = "bool list"

definition falsifiesl :: "partial_pred_denot  fterm literal  bool" where
  "falsifiesl G l 
        groundl l
      (let i = nat_of_fatom (get_atom l) in
          i < length G  G ! i = (¬sign l)
        )"

text ‹A ground clause is falsified if it is actually ground and all its literals are falsified.›
abbreviation falsifiesg :: "partial_pred_denot  fterm clause  bool" where
  "falsifiesg G C  groundls C  (l  C. falsifiesl G l)"

abbreviation falsifiesc :: "partial_pred_denot  fterm clause  bool" where
  "falsifiesc G C  (C'. instance_ofls C' C  falsifiesg G C')"

abbreviation falsifiescs :: "partial_pred_denot  fterm clause set  bool" where
  "falsifiescs G Cs  (C  Cs. falsifiesc G C)"  

abbreviation extend :: "(nat  partial_pred_denot)  hterm pred_denot" where
  "extend f P ts  (
     let n = nat_of_hatom (P, ts) in
       f (Suc n) ! n
     )"

fun sub_of_denot :: "hterm var_denot  substitution" where
  "sub_of_denot E = fterm_of_hterm  E"

lemma ground_sub_of_denott: "groundt (t t (sub_of_denot E))" 
  by (induction t) (auto simp add: ground_fterm_of_hterm)


lemma ground_sub_of_denotts: "groundts (ts ts sub_of_denot E)"
using ground_sub_of_denott by simp 


lemma ground_sub_of_denotl: "groundl (l l sub_of_denot E)"
proof -
  have "groundts (subs (get_terms l) (sub_of_denot E))" 
    using ground_sub_of_denotts by auto
  then show ?thesis by (cases l)  auto
qed

lemma sub_of_denot_equivx: "evalt E HFun (sub_of_denot E x) = E x"
proof -
  have "groundt (sub_of_denot E x)" using ground_fterm_of_hterm by simp
  then
  have "evalt E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)"
    using eval_groundt(1) by auto
  also have "... = hterm_of_fterm (fterm_of_hterm (E x))" by auto
  also have "... = E x" by auto
  finally show ?thesis by auto
qed

lemma sub_of_denot_equivt:
    "evalt E HFun (t t (sub_of_denot E)) = evalt E HFun t"
using sub_of_denot_equivx  by (induction t) auto

lemma sub_of_denot_equivts: "evalts E HFun (ts ts (sub_of_denot E)) = evalts E HFun ts"
using sub_of_denot_equivt by simp

lemma sub_of_denot_equivl: "evall E HFun G (l l sub_of_denot E)  evall E HFun G l"
proof (induction l)
  case (Pos p ts)
  have "evall E HFun G ((Pos p ts) l sub_of_denot E)  G p (evalts E HFun (ts ts (sub_of_denot E)))" by auto
  also have " ...  G p (evalts E HFun ts)" using sub_of_denot_equivts[of E ts] by metis
  also have " ...  evall E HFun G (Pos p ts)" by simp
  finally
  show ?case by blast
next
 case (Neg p ts)
  have "evall E HFun G ((Neg p ts) l sub_of_denot E)  ¬G p (evalts E HFun (ts ts (sub_of_denot E)))" by auto
  also have " ...  ¬G p (evalts E HFun ts)" using sub_of_denot_equivts[of E ts] by metis
  also have " ... = evall E HFun G (Neg p ts)" by simp
  finally
  show ?case by blast
qed

text ‹Under an Herbrand interpretation, an environment is equivalent to a substitution.›
lemma sub_of_denot_equiv_ground': 
  "evall E HFun G l = evall E HFun G (l l sub_of_denot E)  groundl (l l sub_of_denot E)"
    using sub_of_denot_equivl ground_sub_of_denotl by auto

text ‹Under an Herbrand interpretation, an environment is similar to a substitution - also for partial interpretations.›
lemma partial_equiv_subst:
  assumes "falsifiesc G (C ls τ)"
  shows "falsifiesc G C"
proof -
  from assms obtain C' where C'_p: "instance_ofls C' (C ls τ)  falsifiesg G C'" by auto
  then have "instance_ofls (C ls τ) C" unfolding instance_ofls_def by auto
  then have "instance_ofls C' C" using C'_p instance_ofls_trans by auto
  then show ?thesis using C'_p by auto
qed

text ‹Under an Herbrand interpretation, an environment is equivalent to a substitution.›
lemma sub_of_denot_equiv_ground:
  "((l  C. evall E HFun G l)  (l  C ls sub_of_denot E. evall E HFun G l))
            groundls (C ls sub_of_denot E)"
  using sub_of_denot_equiv_ground' by auto

lemma std1_falsifies: "falsifiesc G C1  falsifiesc G (std1 C1)"
proof 
  assume asm: "falsifiesc G C1"
  then obtain Cg where "instance_ofls Cg C1   falsifiesg G Cg" by auto
  moreover
  then have "instance_ofls Cg (std1 C1)" using std_apart_instance_ofls1 instance_ofls_trans by blast
  ultimately
  show "falsifiesc G (std1 C1)" by auto
next
  assume asm: "falsifiesc G (std1 C1)"
  then have inst: "instance_ofls (std1 C1) C1" unfolding instance_ofls_def by auto

  from asm obtain Cg where "instance_ofls Cg (std1 C1)   falsifiesg G Cg" by auto
  moreover
  then have "instance_ofls Cg C1" using inst instance_ofls_trans by blast
  ultimately
  show "falsifiesc G C1" by auto
qed

lemma std2_falsifies: "falsifiesc G C2  falsifiesc G (std2 C2)"
proof 
  assume asm: "falsifiesc G C2"
  then obtain Cg where "instance_ofls Cg C2   falsifiesg G Cg" by auto
  moreover
  then have "instance_ofls Cg (std2 C2)" using std_apart_instance_ofls2 instance_ofls_trans by blast
  ultimately
  show "falsifiesc G (std2 C2)" by auto
next
  assume asm: "falsifiesc G (std2 C2)"
  then have inst: "instance_ofls (std2 C2) C2" unfolding instance_ofls_def by auto

  from asm obtain Cg where "instance_ofls Cg (std2 C2)   falsifiesg G Cg" by auto
  moreover
  then have "instance_ofls Cg C2" using inst instance_ofls_trans by blast
  ultimately
  show "falsifiesc G C2" by auto
qed

lemma std1_renames: "var_renaming_of C1 (std1 C1)"
proof -
  have "instance_ofls C1 (std1 C1)" using std_apart_instance_ofls1 by auto
  moreover have "instance_ofls (std1 C1) C1" unfolding instance_ofls_def by auto
  ultimately show "var_renaming_of C1 (std1 C1)" unfolding var_renaming_of_def by auto
qed

lemma std2_renames: "var_renaming_of C2 (std2 C2)"
proof -
  have "instance_ofls C2 (std2 C2)" using std_apart_instance_ofls2 by auto
  moreover have "instance_ofls (std2 C2) C2" unfolding instance_ofls_def by auto
  ultimately show "var_renaming_of C2 (std2 C2)" unfolding var_renaming_of_def by auto
qed


section ‹Semantic Trees›

abbreviation closed_branch :: "partial_pred_denot  tree  fterm clause set  bool" where
  "closed_branch G T Cs  branch G T  falsifiescs G Cs"

abbreviation(input) open_branch :: "partial_pred_denot  tree  fterm clause set  bool" where
  "open_branch G T Cs  branch G T  ¬falsifiescs G Cs"

definition closed_tree :: "tree  fterm clause set  bool" where
  "closed_tree T Cs  anybranch T (λb. closed_branch b T Cs) 
                   anyinternal T (λp. ¬falsifiescs p Cs)" 


section ‹Herbrand's Theorem›

lemma maximum:
  assumes asm: "finite C"
  shows "n :: nat. l  C. f l  n"
proof
  from asm show "lC. f l  (Max (f ` C))" by auto
qed

lemma extend_preserves_model: (* only for ground *)
  assumes f_infpath: "wf_infpath (f :: nat  partial_pred_denot)" 
  assumes C_ground: "groundls C"
  assumes C_sat: "¬falsifiesc (f (Suc n)) C"
  assumes n_max: "lC. nat_of_fatom (get_atom l)  n"
  shows "evalc HFun (extend f) C"
proof -
  let ?F = "HFun" 
  let ?G = "extend f"
  {
    fix E
    from C_sat have "C'. (¬instance_ofls C' C  ¬falsifiesg (f (Suc n)) C')" by auto
    then have "¬falsifiesg (f (Suc n)) C" using instance_ofls_self by auto
    then obtain l where l_p: "lC  ¬falsifiesl (f (Suc n)) l" using C_ground by blast
    let ?i = "nat_of_fatom (get_atom l)"
     
    from l_p have i_n: "?i  n" using n_max by auto
    then have j_n: "?i < length (f (Suc n))" using f_infpath infpath_length[of f] by auto
      
    have "evall E HFun (extend f) l"
      proof (cases l)
        case (Pos P ts)
        from Pos l_p C_ground have ts_ground: "groundts ts" by auto

        have "¬falsifiesl (f (Suc n)) l" using l_p by auto
        then have "f (Suc n) ! ?i = True" 
          using j_n Pos ts_ground empty_subts[of ts] unfolding falsifiesl_def by auto
        moreover have "f (Suc ?i) ! ?i = f (Suc n) ! ?i" 
          using f_infpath i_n j_n infpath_length[of f] ith_in_extension[of f] by simp
        ultimately
        have "f (Suc ?i) ! ?i = True" using Pos by auto
        then have "?G P (hterms_of_fterms ts)" using Pos by (simp add: nat_of_fatom_def) 
        then show ?thesis using evall_groundts[of ts _ ?G P] ts_ground Pos by auto
      next
        case (Neg P ts) (* Symmetric *)
        from Neg l_p C_ground have ts_ground: "groundts ts" by auto

        have "¬falsifiesl (f (Suc n)) l" using l_p by auto  
        then have "f (Suc n) ! ?i = False" 
          using j_n Neg ts_ground empty_subts[of ts] unfolding falsifiesl_def by auto
        moreover have "f (Suc ?i) ! ?i = f (Suc n) ! ?i" 
          using f_infpath i_n j_n infpath_length[of f] ith_in_extension[of f] by simp
        ultimately
        have "f (Suc ?i) ! ?i = False" using Neg by auto
        then have "¬?G P (hterms_of_fterms ts)" using Neg by (simp add: nat_of_fatom_def) 
        then show ?thesis using Neg evall_groundts[of ts _ ?G P] ts_ground by auto
      qed
    then have "l  C. evall E HFun (extend f) l" using l_p by auto
  }
  then have "evalc HFun (extend f) C" unfolding evalc_def by auto
  then show ?thesis using instance_ofls_self by auto
qed

lemma extend_preserves_model2: (* only for ground *)
  assumes f_infpath: "wf_infpath (f :: nat  partial_pred_denot)" 
  assumes C_ground: "groundls C"
  assumes fin_c: "finite C"
  assumes model_C: "n. ¬falsifiesc (f n) C"
  shows C_false: "evalc HFun (extend f) C"
proof -
  ― ‹Since C is finite, C has a largest index of a literal.›
  obtain n where largest: "l  C. nat_of_fatom (get_atom l)  n" using fin_c maximum[of C "λl. nat_of_fatom (get_atom l)"] by blast
  moreover
  then have "¬falsifiesc (f (Suc n)) C" using model_C by auto
  ultimately show ?thesis using model_C f_infpath C_ground extend_preserves_model[of f C n ] by blast
qed

lemma extend_infpath: 
  assumes f_infpath: "wf_infpath (f :: nat  partial_pred_denot)"
  assumes model_c: "n. ¬falsifiesc (f n) C"
  assumes fin_c: "finite C"
  shows "evalc HFun (extend f) C"
unfolding evalc_def proof 
  fix E
  let ?G = "extend f"
  let  = "sub_of_denot E"
  
  from fin_c have fin_cσ: "finite (C ls sub_of_denot E)" by auto
  have groundcσ: "groundls (C ls sub_of_denot E)" using sub_of_denot_equiv_ground by auto

  ― ‹Here starts the proof›
  ― ‹We go from syntactic FO world to syntactic ground world:›
  from model_c have "n. ¬falsifiesc (f n) (C ls )" using partial_equiv_subst by blast
  ― ‹Then from syntactic ground world to semantic ground world:›
  then have "evalc HFun ?G (C ls )" using groundcσ f_infpath fin_cσ extend_preserves_model2[of f "C ls "] by blast
  ― ‹Then from semantic ground world to semantic FO world:›
  then have "E. l  (C ls ). evall E HFun ?G l" unfolding evalc_def by auto
  then have "l  (C ls ). evall E HFun ?G l" by auto
  then show "l  C. evall E HFun ?G l" using sub_of_denot_equiv_ground[of C E "extend f"] by blast
qed

text ‹If we have a infpath of partial models, then we have a model.›
lemma infpath_model:
  assumes f_infpath: "wf_infpath (f :: nat  partial_pred_denot)"
  assumes model_cs: "n. ¬falsifiescs (f n) Cs" 
  assumes fin_cs: "finite Cs"
  assumes fin_c: "C  Cs. finite C"
  shows "evalcs HFun (extend f) Cs"
proof -
  let ?F = "HFun"
    
  have "C  Cs. evalc ?F (extend f) C"  
    proof (rule ballI)
      fix C
      assume asm: "C  Cs"
      then have "n. ¬falsifiesc (f n) C" using model_cs by auto
      then show "evalc ?F (extend f) C" using fin_c asm f_infpath extend_infpath[of f C] by auto
    qed                                                                      
  then show "evalcs ?F (extend f) Cs" unfolding evalcs_def by auto
qed

fun deeptree :: "nat  tree" where
  "deeptree 0 = Leaf"
| "deeptree (Suc n) = Branching (deeptree n) (deeptree n)"

lemma branch_length: 
  assumes "branch b (deeptree n)"
  shows "length b = n"
using assms proof (induction n arbitrary: b)
  case 0 then show ?case using branch_inv_Leaf by auto
next
  case (Suc n)
  then have "branch b (Branching (deeptree n) (deeptree n))" by auto
  then obtain a b' where p: "b = a#b' branch b' (deeptree n)" using branch_inv_Branching[of b] by blast
  then have "length b' = n" using Suc by auto
  then show ?case using p by auto
qed

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

lemma longer_falsifiesl:
  assumes "falsifiesl ds l"
  shows "falsifiesl (ds@d) l"
proof - 
  let ?i = "nat_of_fatom (get_atom l)"
  from assms have i_p: "groundl l   ?i < length ds  ds ! ?i = (¬sign l)" unfolding falsifiesl_def by meson
  moreover
  from i_p have "?i < length (ds@d)" by auto
  moreover
  from i_p have "(ds@d) ! ?i = (¬sign l)" by (simp add: nth_append) 
  ultimately
  show ?thesis unfolding falsifiesl_def by simp
qed

lemma longer_falsifiesg:
  assumes "falsifiesg ds C"
  shows "falsifiesg (ds @ d) C"
proof -
  {
    fix l
    assume "lC"
    then have "falsifiesl (ds @ d) l" using assms longer_falsifiesl by auto
  } then show ?thesis using assms by auto
qed

lemma longer_falsifiesc:
  assumes "falsifiesc ds C"
  shows "falsifiesc (ds @ d) C"
proof -
  from assms obtain C' where "instance_ofls C' C  falsifiesg ds C'" by auto
  moreover
  then have "falsifiesg (ds @ d) C'" using longer_falsifiesg by auto
  ultimately show ?thesis by auto
qed

text ‹We use this so that we can apply König's lemma.›
lemma longer_falsifies:  
  assumes "falsifiescs ds Cs"
  shows "falsifiescs (ds @ d) Cs"
proof -
  from assms obtain C where "C  Cs  falsifiesc ds C" by auto
  moreover
  then have "falsifiesc (ds @ d) C" using longer_falsifiesc[of C ds d] by blast
  ultimately
  show ?thesis by auto
qed

text ‹If all finite semantic trees have an open branch, then the set of clauses has a model.›
theorem herbrand':
  assumes openb: "T. G. open_branch G T Cs"
  assumes finite_cs: "finite Cs" "CCs. finite C"
  shows "G. evalcs HFun G Cs"
proof -
  ― ‹Show T infinite:›
  let ?tree = "{G. ¬falsifiescs G Cs}"
  let ?undiag = length
  let ?diag = "(λl. SOME b. open_branch b (deeptree l) Cs) :: nat  partial_pred_denot"

  from openb have diag_open: "l. open_branch (?diag l) (deeptree l) Cs"
    using someI_ex[of "λb. open_branch b (deeptree _) Cs"] by auto
  then have "n. ?undiag (?diag n) = n" using branch_length by auto
  moreover
  have "n. (?diag n)  ?tree" using diag_open by auto
  ultimately
  have "¬finite ?tree" using infinity[of _ "λn. SOME b. open_branch b (_ n) Cs"] by simp
  ― ‹Get infinite path:›
  moreover 
  have "ds d. ¬falsifiescs (ds @ d) Cs  ¬falsifiescs ds Cs" 
    using longer_falsifies[of Cs] by blast
  then have "(ds d. ds @ d  ?tree  ds  ?tree)" by auto
  ultimately
  have "c. wf_infpath c  (n. c n  ?tree)" using konig[of ?tree] by blast
  then have "G. wf_infpath G  (n. ¬ falsifiescs (G n) Cs)" by auto
  ― ‹Apply above infpath lemma:›
  then show "G. evalcs HFun G Cs" using infpath_model finite_cs by auto
qed

lemma shorter_falsifiesl:
  assumes "falsifiesl (ds@d) l"
  assumes "nat_of_fatom (get_atom l) < length ds"
  shows "falsifiesl ds l"
proof -
  let ?i = "nat_of_fatom (get_atom l)"
  from assms have i_p: "groundl l   ?i < length (ds@d)  (ds@d) ! ?i = (¬sign l)" unfolding falsifiesl_def by meson
  moreover
  then have "?i < length ds" using assms by auto
  moreover
  then have "ds ! ?i = (¬sign l)" using i_p nth_append[of ds d ?i] by auto
  ultimately show ?thesis using assms unfolding falsifiesl_def by simp
qed

theorem herbrand'_contra:
  assumes finite_cs: "finite Cs" "CCs. finite C"
  assumes unsat: "G. ¬evalcs HFun G Cs"
  shows "T. G. branch G T  closed_branch G T Cs"
proof -
  from finite_cs unsat have "(T. G. open_branch G T Cs)  (G. evalcs HFun G Cs)" using herbrand' by blast
  then show ?thesis using unsat by blast 
qed

theorem herbrand:
  assumes unsat: "G. ¬evalcs HFun G Cs"
  assumes finite_cs: "finite Cs" "CCs. finite C"
  shows "T. closed_tree T Cs"
proof -
  from unsat finite_cs obtain T where "anybranch T (λb. closed_branch b T Cs)" using herbrand'_contra[of Cs] by blast
  then have "T. anybranch T (λp. falsifiescs p Cs)  anyinternal T (λp. ¬ falsifiescs p Cs)" 
    using cutoff_branch_internal[of T "λp. falsifiescs p Cs"] by blast
  then show ?thesis unfolding closed_tree_def by auto
qed

end

Theory Completeness

section ‹Lifting Lemma›

theory Completeness imports Resolution begin

locale unification =
  assumes unification: "σ L. finite L  unifierls σ L  θ. mguls θ L"
begin
text ‹
  A proof of this assumption is available in @{file ‹Unification_Theorem.thy›} and used in
  @{file ‹Completeness_Instance.thy›}.
›

lemma lifting:
  assumes fin: "finite C1  finite C2"
  assumes apart: "varsls C1  varsls C2 = {}"
  assumes inst: "instance_ofls C1' C1  instance_ofls C2' C2"
  assumes appl: "applicable C1' C2' L1' L2' σ"
  shows "L1 L2 τ. applicable C1 C2 L1 L2 τ 
                instance_ofls (resolution C1' C2' L1' L2' σ) (resolution C1 C2 L1 L2 τ)"
proof -
  ― ‹Obtaining the subsets we resolve upon:›
  let ?R1' = "C1' - L1'" and ?R2' = "C2' - L2'"

  from inst obtain γ μ where "C1 ls γ = C1'  C2 ls μ = C2'"
    unfolding instance_ofls_def by auto
  then obtain η where η_p: "C1 ls η = C1'  C2 ls η = C2'"
    using apart merge_sub by force

  from η_p obtain L1 where L1_p: "L1  C1  L1 ls η = L1'  (C1 - L1) ls η = ?R1'"
    using appl project_sub using applicable_def by metis
  let ?R1 = "C1 - L1"
  from η_p obtain L2 where L2_p: "L2  C2  L2 ls η = L2'  (C2 - L2) ls η = ?R2'"
    using appl project_sub using applicable_def by metis
  let ?R2 = "C2 - L2"

  ― ‹Obtaining substitutions:›
  from appl have "mguls σ (L1'  L2'C)" using applicable_def by auto
  then have "mguls σ ((L1 ls η)  (L2 ls η)C)" using L1_p L2_p by auto
  then have "mguls σ ((L1   L2C) ls η)" using compls_subls subls_union by auto
  then have "unifierls σ ((L1   L2C) ls η)" using mguls_def by auto
  then have ησuni: "unifierls (η  σ) (L1   L2C)"
    using unifierls_def composition_conseq2l by auto
  then obtain τ where τ_p: "mguls τ (L1   L2C)"
    using unification fin L1_p L2_p by (meson finite_UnI finite_imageI rev_finite_subset)
  then obtain φ where φ_p: "τ  φ = η  σ" using ησuni mguls_def by auto

  ― ‹Showing that we have the desired resolvent:›
  let ?C = "((C1 - L1)   (C2 - L2)) ls τ"
  have "?C ls φ  = (?R1  ?R2 ) ls (τ  φ)"
    using subls_union composition_conseq2ls by auto
  also have "... = (?R1  ?R2 ) ls (η  σ)" using φ_p by auto
  also have "... = ((?R1 ls η)  (?R2 ls η)) ls σ"
    using subls_union composition_conseq2ls by auto
  also have "... = (?R1'  ?R2') ls σ" using η_p L1_p L2_p by auto
  finally have "?C ls φ = ((C1' - L1')  (C2' - L2')) ls σ" by auto
  then have ins: "instance_ofls (resolution C1' C2' L1' L2' σ) (resolution C1 C2 L1 L2 τ)"
    using resolution_def instance_ofls_def by metis

  ― ‹Showing that the resolution rule is applicable:›
  have "C1'  {}  C2'  {}  L1'  {}  L2'  {}"
    using appl applicable_def by auto
  then have "C1  {}  C2  {}  L1  {}  L2  {}" using η_p L1_p L2_p by auto
  then have appli: "applicable C1 C2 L1 L2 τ"
    using apart L1_p L2_p τ_p applicable_def by auto

  from ins appli show ?thesis by auto
qed


section ‹Completeness›

lemma falsifiesg_empty:
  assumes "falsifiesg [] C"
  shows "C = {}"
proof -
  have "l  C. False"
    proof
      fix l
      assume "lC"
      then have "falsifiesl [] l" using assms by auto
      then show False unfolding falsifiesl_def by (cases l) auto
    qed
  then show ?thesis by auto
qed

lemma falsifiescs_empty:
  assumes "falsifiesc [] C"
  shows "C = {}"
proof -
  from assms obtain C' where C'_p: "instance_ofls C' C  falsifiesg [] C'" by auto
  then have "C'= {}" using falsifiesg_empty by auto
  then show "C = {}" using C'_p unfolding instance_ofls_def by auto
qed

lemma complements_do_not_falsify':
  assumes l1C1': "l1  C1'"
  assumes l2C1': "l2  C1'"
  assumes comp: "l1 = l2c"
  assumes falsif: "falsifiesg G C1'"
  shows "False"
proof (cases l1)
  case (Pos p ts)
  let ?i1 = "nat_of_fatom (p, ts)"

  from assms have gr: "groundl l1" unfolding falsifiesl_def by auto
  then have Neg: "l2 = Neg p ts" using comp Pos by (cases l2) auto

  from falsif have "falsifiesl G l1" using l1C1' by auto
  then have "G ! ?i1 = False" using l1C1' Pos unfolding falsifiesl_def by (induction "Pos p ts") auto
  moreover
  let ?i2 = "nat_of_fatom (get_atom l2)"
  from falsif have "falsifiesl G l2" using l2C1' by auto
  then have "G ! ?i2 = (¬sign l2)" unfolding falsifiesl_def by meson
  then have "G ! ?i1 = (¬sign l2)" using Pos Neg comp by simp
  then have "G ! ?i1 = True" using Neg by auto
  ultimately show ?thesis by auto
next
  case (Neg p ts)
  let ?i1 = "nat_of_fatom (p,ts)"

  from assms have gr: "groundl l1" unfolding falsifiesl_def by auto
  then have Pos: "l2 = Pos p ts" using comp Neg by (cases l2) auto

  from falsif have "falsifiesl G l1" using l1C1' by auto
  then have "G ! ?i1 = True" using l1C1' Neg unfolding falsifiesl_def by (metis get_atom.simps(2) literal.disc(2)) 
  moreover
  let ?i2 = "nat_of_fatom (get_atom l2)"
  from falsif have "falsifiesl G l2" using l2C1' by auto
  then have "G ! ?i2 = (¬sign l2)" unfolding falsifiesl_def by meson
  then have "G ! ?i1 = (¬sign l2)" using Pos Neg comp by simp
  then have "G ! ?i1 = False" using Pos using literal.disc(1) by blast
  ultimately show ?thesis by auto
qed

lemma complements_do_not_falsify:
  assumes l1C1': "l1  C1'"
  assumes l2C1': "l2  C1'"
  assumes fals: "falsifiesg G C1'"
  shows "l1  l2c"
using assms complements_do_not_falsify' by blast

lemma other_falsified:
  assumes C1'_p: "groundls C1'  falsifiesg (B@[d]) C1'" 
  assumes l_p: "l  C1'" "nat_of_fatom (get_atom l) = length B"
  assumes other: "lo  C1'" "lo  l"
  shows "falsifiesl B lo"
proof -
  let ?i = "nat_of_fatom (get_atom lo)"
  have ground_l2: "groundl l" using l_p C1'_p by auto
  ― ‹They are, of course, also ground:›
  have ground_lo: "groundl lo" using C1'_p other by auto
  from C1'_p have "falsifiesg (B@[d]) (C1' - {l})" by auto
  ― ‹And indeed, falsified by @{term "B@[d]"}:›
  then have loB2: "falsifiesl (B@[d]) lo" using other by auto
  then have "?i < length (B @ [d])" unfolding falsifiesl_def by meson
  ― ‹And they have numbers in the range of @{term "B@[d]"}, i.e. less than @{term "length B + 1"}:›
  then have "nat_of_fatom (get_atom lo) < length B + 1" using undiag_diag_fatom by (cases lo) auto
  moreover
  have l_lo: "llo" using other by auto
  ― ‹The are not the complement of @{term l }, since then the clause could not be falsified:›
  have lc_lo: "lo  lc" using C1'_p l_p other complements_do_not_falsify[of lo C1' l "(B@[d])"] by auto
  from l_lo lc_lo have "get_atom l  get_atom lo" using sign_comp_atom by metis
  then have "nat_of_fatom (get_atom lo)  nat_of_fatom (get_atom l)" 
    using nat_of_fatom_bij ground_lo ground_l2 groundl_ground_fatom 
    unfolding bij_betw_def inj_on_def by metis
  ― ‹Therefore they have different numbers:›
  then have "nat_of_fatom (get_atom lo)  length B" using l_p by auto
  ultimately 
  ― ‹So their numbers are in the range of @{term B}:›
  have "nat_of_fatom (get_atom lo) < length B" by auto
  ― ‹So we did not need the last index of @{term "B@[d]"} to falsify them, i.e. @{term B} suffices:›
  then show "falsifiesl B lo" using loB2 shorter_falsifiesl by blast
qed

theorem completeness':
  assumes "closed_tree T Cs"
  assumes "CCs. finite C"
  shows "Cs'. resolution_deriv Cs Cs'  {}  Cs'"
using assms proof (induction T arbitrary: Cs rule: measure_induct_rule[of treesize])
  fix T :: tree
  fix Cs :: "fterm clause set"
  assume ih: "T' Cs. treesize T' < treesize T  closed_tree T' Cs  
                            CCs. finite C  Cs'. resolution_deriv Cs Cs'  {}  Cs'"
  assume clo: "closed_tree T Cs"
  assume finite_Cs: "CCs. finite C"
  { ― ‹Base case:›
    assume "treesize T = 0"
    then have "T=Leaf" using treesize_Leaf by auto
    then have "closed_branch [] Leaf Cs" using branch_inv_Leaf clo unfolding closed_tree_def by auto
    then have "falsifiescs [] Cs" by auto
    then have "{}  Cs" using falsifiescs_empty by auto
    then have "Cs'. resolution_deriv Cs Cs'  {}  Cs'" 
      unfolding resolution_deriv_def by auto
  }
  moreover
  { ― ‹Induction case:›
    assume "treesize T > 0"
    then have "l r. T=Branching l r" by (cases T) auto
    
    ― ‹Finding sibling branches and their corresponding clauses:›
    then obtain B where b_p: "internal B T  branch (B@[True]) T  branch (B@[False]) T"
      using internal_branch[of _ "[]" _ T] Branching_Leaf_Leaf_Tree by fastforce 
    let ?B1 = "B@[True]"
    let ?B2 = "B@[False]"

    obtain C1o where C1o_p: "C1o  Cs  falsifiesc ?B1 C1o" using b_p clo unfolding closed_tree_def by metis 
    obtain C2o where C2o_p: "C2o  Cs  falsifiesc ?B2 C2o" using b_p clo unfolding closed_tree_def by metis

    ― ‹Standardizing the clauses apart:›
    let ?C1 = "std1 C1o"
    let ?C2 = "std2 C2o"
    have C1_p: "falsifiesc ?B1 ?C1" using std1_falsifies C1o_p by auto
    have C2_p: "falsifiesc ?B2 ?C2" using std2_falsifies C2o_p by auto

    have fin: "finite ?C1  finite ?C2" using C1o_p C2o_p finite_Cs by auto

    ― ‹We go down to the ground world.›
    ― ‹Finding the falsifying ground instance @{term C1'} of @{term ?C1}, and proving properties about it:›
    
    ― ‹@{term C1'} is falsified by @{term ?B1}:›
    from C1_p  obtain C1' where C1'_p: "groundls C1'  instance_ofls C1' ?C1  falsifiesg ?B1 C1'" by metis

    have "¬falsifiesc B C1o" using C1o_p b_p clo unfolding closed_tree_def by metis
    then have "¬falsifiesc B ?C1" using std1_falsifies using prod.exhaust_sel by blast
    ― ‹@{term C1'} is not falsified by @{term B}:›
    then have l_B: "¬falsifiesg B C1'" using C1'_p by auto

    ― ‹@{term C1'} contains a literal @{term l1} that is falsified by @{term ?B1}, but not @{term B}:›
    from C1'_p l_B obtain l1 where l1_p: "l1  C1'  falsifiesl (B@[True]) l1  ¬(falsifiesl B l1)" by auto
    let ?i = "nat_of_fatom (get_atom l1)"

    ― ‹@{term l1} is of course ground:›
    have ground_l1: "groundl l1" using C1'_p l1_p by auto

    from l1_p have "¬(?i < length B  B ! ?i = (¬sign l1))" using ground_l1 unfolding falsifiesl_def by meson
    then have "¬(?i < length B  (B@[True]) ! ?i = (¬sign l1))" by (metis nth_append) ― ‹Not falsified by @{term B}.›
    moreover
    from l1_p have "?i < length (B @ [True])  (B @ [True]) ! ?i = (¬sign l1)" unfolding falsifiesl_def by meson
    ultimately
    have l1_sign_no: "?i = length B  (B @ [True]) ! ?i = (¬sign l1)" by auto

    ― ‹@{term l1} is negative:›
    from l1_sign_no have l1_sign: "sign l1 = False" by auto
    from l1_sign_no have l1_no: "nat_of_fatom (get_atom l1) = length B" by auto

    ― ‹All the other literals in @{term C1'} must be falsified by B, since they are falsified by @{term ?B1}, but not @{term l1}.›
    from C1'_p l1_no l1_p have B_C1'l1: "falsifiesg B (C1' - {l1})" (* This should be a lemma *)
      using other_falsified by blast

    ― ‹We do the same exercise for @{term ?C2}, @{term C2'}, @{term ?B2}, @{term l2}:›
    from C2_p obtain C2' where C2'_p: "groundls C2'  instance_ofls C2' ?C2  falsifiesg ?B2 C2'" by metis

    have "¬falsifiesc B C2o" using C2o_p b_p clo unfolding closed_tree_def by metis
    then have "¬falsifiesc B ?C2" using std2_falsifies using prod.exhaust_sel by blast
    then have l_B: "¬falsifiesg B C2'" using C2'_p by auto (* I already had something called l_B... I could give it a new name *)
    
    ― ‹@{term C2'} contains a literal @{term l2} that is falsified by @{term ?B2}, but not B:›
    from C2'_p l_B obtain l2 where l2_p: "l2  C2'  falsifiesl (B@[False]) l2  ¬falsifiesl B l2" by auto
    let ?i = "nat_of_fatom (get_atom l2)"

    have ground_l2: "groundl l2" using C2'_p l2_p by auto

    from l2_p have "¬(?i < length B  B ! ?i = (¬sign l2))" using ground_l2 unfolding falsifiesl_def by meson
    then have "¬(?i < length B  (B@[False]) ! ?i = (¬sign l2))" by (metis nth_append) ― ‹Not falsified by @{term B}.›
    moreover
    from l2_p have "?i < length (B @ [False])  (B @ [False]) ! ?i = (¬sign l2)" unfolding falsifiesl_def by meson
    ultimately
    have l2_sign_no: "?i = length B  (B @ [False]) ! ?i = (¬sign l2)" by auto

    ― ‹@{term l2} is negative:›
    from l2_sign_no have l2_sign: "sign l2 = True" by auto
    from l2_sign_no have l2_no: "nat_of_fatom (get_atom l2) = length B" by auto

    ― ‹All the other literals in @{term C2'} must be falsified by B, since they are falsified by 
          @{term ?B2}, but not @{term l2}.›
    from C2'_p l2_no l2_p have B_C2'l2: "falsifiesg B (C2' - {l2})"
      using other_falsified by blast

    ― ‹Proving some properties about @{term C1'} and @{term C2'}, @{term l1} and @{term l2}, as well as 
          the resolvent of @{term C1'} and @{term C2'}:›
    have l2cisl1: "l2c = l1" (* Could perhaps be a lemma *)
      proof -
        from l1_no l2_no ground_l1 ground_l2 have "get_atom l1 = get_atom l2"
              using nat_of_fatom_bij groundl_ground_fatom 
              unfolding bij_betw_def inj_on_def by metis
        then show "l2c = l1" using l1_sign l2_sign using sign_comp_atom by metis 
      qed
    
    have "applicable C1' C2' {l1} {l2} Resolution.ε" unfolding applicable_def
      using l1_p l2_p C1'_p groundls_varsls l2cisl1 empty_comp2 unfolding mguls_def unifierls_def by auto
    ― ‹Lifting to get a resolvent of @{term ?C1} and @{term ?C2}:›
    then obtain L1 L2 τ where L1L2τ_p: "applicable ?C1 ?C2 L1 L2 τ   instance_ofls (resolution C1' C2' {l1} {l2} Resolution.ε) (resolution ?C1 ?C2 L1 L2 τ)"
      using std_apart_apart C1'_p C2'_p lifting[of ?C1 ?C2 C1' C2' "{l1}" "{l2}" Resolution.ε] fin by auto


    ― ‹Defining the clause to be derived, the new clausal form and the new tree:›
    ― ‹We name the resolvent @{term C}.›
    obtain C where C_p: "C = resolution ?C1 ?C2 L1 L2 τ" by auto
    obtain CsNext where CsNext_p: "CsNext = Cs  {?C1, ?C2, C}" by auto
    obtain T'' where T''_p: "T'' = delete B T" by auto 
        ― ‹Here we delete the two branch children @{term ?B1} and @{term ?B2} of @{term B}.›
    
    ― ‹Our new clause is falsified by the branch @{term B} of our new tree:›
    have "falsifiesg B ((C1' - {l1})  (C2' - {l2}))" using B_C1'l1 B_C2'l2 by cases auto
    then have "falsifiesg B (resolution C1' C2' {l1} {l2} Resolution.ε)" unfolding resolution_def empty_subls by auto
    then have falsifies_C: "falsifiesc B C" using C_p L1L2τ_p by auto

    have T''_smaller: "treesize T'' < treesize T" using treezise_delete T''_p b_p by auto
    have T''_bran: "anybranch T'' (λb. closed_branch b T'' CsNext)"
      proof (rule allI; rule impI)
        fix b
        assume br: "branch b T''"
        from br have "b = B  branch b T" using branch_delete T''_p by auto
        then show "closed_branch b T'' CsNext"
          proof
            assume "b=B"
            then show "closed_branch b T'' CsNext" using falsifies_C br CsNext_p by auto
          next
            assume "branch b T"
            then show "closed_branch b T'' CsNext" using clo br T''_p CsNext_p unfolding closed_tree_def by auto
          qed
      qed
    then have T''_bran2: "anybranch T'' (λb. falsifiescs b CsNext)" by auto (* replace T''_bran with this maybe? *)

    ― ‹We cut the tree even smaller to ensure only the branches are falsified, i.e. it is a closed tree:›
    obtain T' where T'_p: "T' = cutoff (λG. falsifiescs G CsNext) [] T''" by auto
    have T'_smaller: "treesize T' < treesize T" using treesize_cutoff[of "λG. falsifiescs G CsNext" "[]" T''] T''_smaller unfolding T'_p by auto

    from T''_bran2 have "anybranch T' (λb. falsifiescs b CsNext)" using cutoff_branch[of T'' "λb. falsifiescs b CsNext"] T'_p by auto
    then have T'_bran: "anybranch T' (λb. closed_branch b T' CsNext)" by auto
    have T'_intr: "anyinternal T' (λp. ¬falsifiescs p CsNext)" using T'_p cutoff_internal[of T'' "λb. falsifiescs b CsNext"] T''_bran2 by blast
    have T'_closed: "closed_tree T' CsNext" using T'_bran T'_intr unfolding closed_tree_def by auto
    have finite_CsNext: "CCsNext. finite C" unfolding CsNext_p C_p resolution_def using finite_Cs fin by auto

    ― ‹By induction hypothesis we get a resolution derivation of @{term "{}"} from our new clausal form:›
    from T'_smaller T'_closed have "Cs''. resolution_deriv CsNext Cs''  {}  Cs''" using ih[of T' CsNext] finite_CsNext by blast
    then obtain Cs'' where Cs''_p: "resolution_deriv CsNext Cs''  {}  Cs''" by auto
    moreover
    { ― ‹Proving that we can actually derive the new clausal form:›
      have "resolution_step Cs (Cs  {?C1})" using std1_renames standardize_apart C1o_p by (metis Un_insert_right)
      moreover
      have "resolution_step (Cs  {?C1}) (Cs  {?C1}  {?C2})" using std2_renames[of C2o] standardize_apart[of C2o _ ?C2] C2o_p by auto 
      then have "resolution_step (Cs  {?C1}) (Cs  {?C1,?C2})" by (simp add: insert_commute)
      moreover
      then have "resolution_step (Cs  {?C1,?C2}) (Cs  {?C1,?C2}  {C})" 
        using L1L2τ_p resolution_rule[of ?C1 "Cs  {?C1,?C2}" ?C2 L1 L2 τ ] using C_p by auto
      then have "resolution_step (Cs  {?C1,?C2}) CsNext" using CsNext_p by (simp add:  Un_commute)
      ultimately
      have "resolution_deriv Cs CsNext"  unfolding resolution_deriv_def by auto
    }
    ― ‹Combining the two derivations, we get the desired derivation from @{term Cs} of @{term "{}"}:›
    ultimately have "resolution_deriv Cs Cs''"  unfolding resolution_deriv_def by auto
    then have "Cs'. resolution_deriv Cs Cs'  {}  Cs'" using Cs''_p by auto
  }
  ultimately show "Cs'. resolution_deriv Cs Cs'  {}  Cs'" by auto
qed

theorem completeness:
  assumes finite_cs: "finite Cs" "CCs. finite C"
  assumes unsat: "(F::hterm fun_denot) (G::hterm pred_denot) . ¬evalcs F G Cs"
  shows "Cs'. resolution_deriv Cs Cs'  {}  Cs'"
proof -
  from unsat have "(G::hterm pred_denot) . ¬evalcs HFun G Cs" by auto
  then obtain T where "closed_tree T Cs" using herbrand assms by blast
  then show "Cs'. resolution_deriv Cs Cs'  {}  Cs'" using completeness' assms by auto
qed 

definition E_conv :: "('a  'b)  'a var_denot  'b var_denot" where
  "E_conv b_of_a E  λx. (b_of_a (E x))"

definition F_conv :: "('a  'b)  'a fun_denot  'b fun_denot" where
  "F_conv b_of_a F  λf bs. b_of_a (F f (map (inv b_of_a) bs))"

definition G_conv :: "('a  'b)  'a pred_denot  'b pred_denot" where
  "G_conv b_of_a G  λp bs. (G p (map (inv b_of_a) bs))"
  
lemma evalt_bij:
  assumes "bij (b_of_a::'a  'b)"
  shows"evalt (E_conv b_of_a E) (F_conv b_of_a F) t = b_of_a (evalt E F t)"
proof (induction t)
  case (Fun f ts)
  then have "map (inv b_of_a  evalt (E_conv b_of_a E) (F_conv b_of_a F)) ts = evalts E F ts"
    unfolding E_conv_def F_conv_def
    using assms bij_is_inj by fastforce
  then have "b_of_a (F f (map (inv b_of_a  evalt (E_conv b_of_a E) ((F_conv b_of_a F))) ts)) = b_of_a (F f (evalts E F ts))" by metis
  then show ?case using assms unfolding E_conv_def F_conv_def by auto
next
  case (Var x)
  then show ?case using assms unfolding E_conv_def by auto
qed

lemma evalts_bij:
  assumes "bij (b_of_a::'a  'b)"
  shows "G_conv b_of_a G p (evalts (E_conv b_of_a E) (F_conv b_of_a F) ts) = G p (evalts E F ts)" 
  using assms using evalt_bij
proof -
  have "map (inv b_of_a  evalt (E_conv b_of_a E) (F_conv b_of_a F)) ts = evalts E F ts"
    using evalt_bij assms bij_is_inj by fastforce
  then show ?thesis
    by (metis (no_types) G_conv_def map_map)
qed
   
  
lemma evall_bij:
  assumes "bij (b_of_a::'a  'b)"
  shows "evall (E_conv b_of_a E) (F_conv b_of_a F) (G_conv b_of_a G) l = evall E F G l"
  using assms evalts_bij 
proof (cases l)
  case (Pos p ts)
  then show ?thesis
    by (simp add: evalts_bij assms) 
next
  case (Neg p ts)
  then show ?thesis
    by (simp add: evalts_bij assms)
qed 
            
lemma evalc_bij:
  assumes "bij (b_of_a::'a  'b)"
  shows "evalc (F_conv b_of_a F) (G_conv b_of_a G) C = evalc F G C"
proof -
  {
    fix E :: "char list  'b"
    assume bij_b_of_a: "bij b_of_a"
    assume C_sat: "E :: char list  'a. lC. evall E F G l" 
    have E_p: "E = E_conv b_of_a (E_conv (inv b_of_a) E)" 
      unfolding E_conv_def using bij_b_of_a
      using bij_betw_inv_into_right by fastforce 
    have "lC. evall (E_conv b_of_a (E_conv (inv b_of_a) E)) (F_conv b_of_a F) (G_conv b_of_a G) l"
      using evall_bij bij_b_of_a C_sat by blast
    then have "lC. evall E (F_conv b_of_a F) (G_conv b_of_a G) l" using E_p by auto 
  }
  then show ?thesis
    by (meson evall_bij assms evalc_def) 
qed

lemma evalcs_bij:
  assumes "bij (b_of_a::'a  'b)"
  shows "evalcs (F_conv b_of_a F) (G_conv b_of_a G) Cs  evalcs F G Cs"
    by (meson evalc_bij assms evalcs_def)
    
lemma countably_inf_bij:
  assumes inf_a_uni: "infinite (UNIV :: ('a ::countable) set)"
  assumes inf_b_uni: "infinite (UNIV :: ('b ::countable) set)"
  shows "b_of_a :: 'a  'b. bij b_of_a"
proof -
  let ?S = "UNIV :: (('a::countable)) set"
  have "countable ?S" by auto
  moreover
  have "infinite ?S" using inf_a_uni by auto
  ultimately
  obtain nat_of_a where QWER: "bij (nat_of_a :: 'a  nat)" using countableE_infinite[of ?S] by blast
      
  let ?T = "UNIV :: (('b::countable)) set"
  have "countable ?T" by auto
  moreover
  have "infinite ?T" using inf_b_uni by auto
  ultimately
  obtain nat_of_b where TYUI: "bij (nat_of_b :: 'b  nat)" using countableE_infinite[of ?T] by blast
      
  let ?b_of_a = "λa. (inv nat_of_b) (nat_of_a a)"
    
  have bij_nat_of_b: "n. nat_of_b (inv nat_of_b n) = n"
    using TYUI bij_betw_inv_into_right by fastforce
  have "a. inv nat_of_a (nat_of_a a) = a"
    by (meson QWER UNIV_I bij_betw_inv_into_left) 
  then have "inj (λa. inv nat_of_b (nat_of_a a))"
    using bij_nat_of_b injI by (metis (no_types))
  moreover
  have "range (λa. inv nat_of_b (nat_of_a a)) = UNIV"
    by (metis QWER TYUI bij_def image_image inj_imp_surj_inv)
  ultimately
  have "bij ?b_of_a"
    unfolding bij_def by auto
      
  then show ?thesis by auto
qed
  
lemma infinite_hterms: "infinite (UNIV :: hterm set)"
proof -
  let ?diago = "λn. HFun (string_of_nat n) []"
  let ?undiago = "λa. nat_of_string (case a of HFun f ts  f)"
  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 :: hterm set)" using infinity[of ?undiago ?diago UNIV] by simp
qed

theorem completeness_countable:
  assumes inf_uni: "infinite (UNIV :: ('u :: countable) set)"
  assumes finite_cs: "finite Cs" "CCs. finite C"
  assumes unsat: "(F::'u fun_denot) (G::'u pred_denot). ¬evalcs F G Cs"
  shows "Cs'. resolution_deriv Cs Cs'  {}  Cs'"
proof -
  have "(F::hterm fun_denot) (G::hterm pred_denot) . ¬evalcs F G Cs"
  proof (rule; rule)
    fix F :: "hterm fun_denot"
    fix G :: "hterm pred_denot"
      
    obtain u_of_hterm :: "hterm  'u" where p_u_of_hterm: "bij u_of_hterm"
      using countably_inf_bij inf_uni infinite_hterms by auto
        
    let ?F = "F_conv u_of_hterm F"
    let ?G = "G_conv u_of_hterm G"
    
    have "¬ evalcs ?F ?G Cs" using unsat by auto
    then show "¬ evalcs F G Cs" using evalcs_bij using p_u_of_hterm by auto
  qed
  then show "Cs'. resolution_deriv Cs Cs'  {}  Cs'" using finite_cs completeness by auto
qed
  
theorem completeness_nat:
  assumes finite_cs: "finite Cs" "CCs. finite C"
  assumes unsat: "(F::nat fun_denot) (G::nat pred_denot) . ¬evalcs F G Cs"
  shows "Cs'. resolution_deriv Cs Cs'  {}  Cs'"
  using assms completeness_countable by blast

end ― ‹unification locale›

end

Theory Examples

section ‹Examples›

theory Examples imports Resolution begin

value "Var ''x''"
value "Fun ''one'' []"
value "Fun ''mul'' [Var ''y'',Var ''y'']"
value "Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''], Fun ''one'' []]"

value "Pos ''greater'' [Var ''x'', Var ''y'']"
value "Neg ''less'' [Var ''x'', Var ''y'']"
value "Pos ''less'' [Var ''x'', Var ''y'']"
value "Pos ''equals''
        [Fun ''add''[Fun ''mul''[Var ''y'',Var ''y''], Fun ''one''[]],Var ''x'']"

fun Fnat :: "nat fun_denot" where
  "Fnat f [n,m] = 
     (if f = ''add'' then n + m else 
      if f = ''mul'' then n * m else 0)"
| "Fnat f [] = 
     (if f = ''one''  then 1 else
      if f = ''zero'' then 0 else 0)"
| "Fnat f us = 0"

fun Gnat :: "nat pred_denot" where
  "Gnat p [x,y] =
     (if p = ''less''  x < y then True else
      if p = ''greater''  x > y then True else 
      if p = ''equals''  x = y then True else False)"
| "Gnat p us = False"

fun Enat :: "nat var_denot" where
  "Enat x =
     (if x = ''x'' then 26 else
      if x = ''y'' then 5 else 0)"

lemma "evalt Enat Fnat (Var ''x'') = 26" 
  by auto
lemma "evalt Enat Fnat (Fun ''one'' []) = 1" 
  by auto
lemma "evalt Enat Fnat (Fun ''mul'' [Var ''y'',Var ''y'']) = 25" 
  by auto
lemma 
  "evalt Enat Fnat (Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''], Fun ''one'' []]) = 26" 
  by auto

lemma "evall Enat Fnat Gnat (Pos ''greater'' [Var ''x'', Var ''y'']) = True" 
  by auto
lemma "evall Enat Fnat Gnat (Neg ''less'' [Var ''x'', Var ''y'']) = True" 
  by auto
lemma "evall Enat Fnat Gnat (Pos ''less'' [Var ''x'', Var ''y'']) = False" 
  by auto

lemma "evall Enat Fnat Gnat 
       (Pos ''equals'' 
         [Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''],Fun ''one'' []]
         ,Var ''x'']
       ) = True" 
  by auto

definition PP :: "fterm literal" where
  "PP = Pos ''P'' [Fun ''c'' []]"

definition PQ :: "fterm literal" where
  "PQ = Pos ''Q'' [Fun ''d'' []]"

definition NP :: "fterm literal" where
  "NP = Neg ''P'' [Fun ''c'' []]"

definition NQ :: "fterm literal" where
  "NQ = Neg ''Q'' [Fun ''d'' []]"

theorem empty_mgu: 
  assumes "unifierls ε L"
  shows "mguls ε L"
using assms unfolding unifierls_def mguls_def apply auto
apply (rule_tac x=u in exI)
using empty_comp1 empty_comp2 apply auto
done

theorem unifier_single: "unifierls σ {l}" 
unfolding unifierls_def by auto

theorem resolution_rule':
  assumes "C1  Cs"
  assumes "C2  Cs"
  assumes "applicable C1 C2 L1 L2 σ"
  assumes "C = {resolution C1 C2 L1 L2 σ}"
  shows "resolution_step Cs (Cs  C)"
  using assms resolution_rule by auto

lemma resolution_example1: 
   "resolution_deriv {{NP,PQ},{NQ},{PP,PQ}} 
                              {{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}}"
proof -
  have "resolution_step 
          {{NP,PQ},{NQ},{PP,PQ}}
         ({{NP,PQ},{NQ},{PP,PQ}}  {{NP}})"
    apply (rule resolution_rule'[of "{NP,PQ}" _ "{NQ}" "{PQ}" "{NQ}" ε])
       unfolding applicable_def varsls_def  varsl_def 
              NQ_def NP_def PQ_def PP_def resolution_def
       using unifier_single empty_mgu using empty_subls
       apply auto 
    done
  then have "resolution_step 
          {{NP,PQ},{NQ},{PP,PQ}}
         ({{NP,PQ},{NQ},{PP,PQ},{NP}})" 
    by (simp add: insert_commute) 
  moreover
  have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP}}  {{PP}})"
    apply (rule resolution_rule'[of "{NQ}" _ "{PP,PQ}" "{NQ}" "{PQ}" ε])
       unfolding applicable_def varsls_def  varsl_def 
              NQ_def NP_def PQ_def PP_def resolution_def
       using unifier_single empty_mgu empty_subls apply auto
    done
  then have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP}})" 
    by (simp add: insert_commute)
  moreover
  have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP},{PP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP}}  {{}})"
    apply (rule resolution_rule'[of "{NP}" _ "{PP}" "{NP}" "{PP}" ε])
       unfolding applicable_def varsls_def  varsl_def 
              NQ_def NP_def PQ_def PP_def resolution_def
       using unifier_single empty_mgu apply auto
    done
  then have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP},{PP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}})" 
    by (simp add: insert_commute)
  ultimately
  have "resolution_deriv {{NP,PQ},{NQ},{PP,PQ}} 
                         {{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}}"
    unfolding resolution_deriv_def by auto 
  then show ?thesis by auto
qed

definition Pa :: "fterm literal" where
  "Pa = Pos ''a'' []"

definition Na :: "fterm literal" where
  "Na = Neg ''a'' []"

definition Pb :: "fterm literal" where
  "Pb = Pos ''b'' []"

definition Nb :: "fterm literal" where
  "Nb = Neg ''b'' []"

definition Paa :: "fterm literal" where
  "Paa = Pos ''a'' [Fun ''a'' []]"

definition Naa :: "fterm literal" where
  "Naa = Neg ''a'' [Fun ''a'' []]"

definition Pax :: "fterm literal" where
  "Pax = Pos ''a'' [Var ''x'']"

definition Nax :: "fterm literal" where
  "Nax = Neg ''a'' [Var ''x'']"

definition mguPaaPax :: substitution where
  "mguPaaPax = (λx. if x = ''x'' then Fun ''a'' [] else Var x)"

lemma mguPaaPax_mgu: "mguls mguPaaPax {Paa,Pax}"
proof -
  let  = "λx. if x = ''x'' then Fun ''a'' [] else Var x"
  have a: "unifierls (λx. if x = ''x'' then Fun ''a'' [] else Var x) {Paa,Pax}" unfolding Paa_def Pax_def unifierls_def by auto
  have b: "u. unifierls u {Paa,Pax}  (i. u =   i)"
    proof (rule;rule)
      fix u
      assume "unifierls u {Paa,Pax}"
      then have uuu: "u ''x'' = Fun ''a'' []" unfolding unifierls_def Paa_def Pax_def by auto
      have "  u = u"
        proof
          fix x
          {
            assume "x=''x''"
            moreover
            have "(  u) ''x'' =  Fun ''a'' []" unfolding composition_def by auto
            ultimately have "(  u) x = u x" using uuu by auto
          }
          moreover
          {
            assume "x''x''"
            then have "(  u) x = (ε x) t u" unfolding composition_def by auto
            then have "(  u) x = u x" by auto
          }
          ultimately show "(  u) x = u x" by auto
        qed
      then have "i.   i = u" by auto
      then show "i. u =   i" by auto
     qed
   from a b show ?thesis unfolding mguls_def unfolding mguPaaPax_def by auto
qed

lemma resolution_example2: 
   "resolution_deriv {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
                              {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}}"
proof -
  have "resolution_step 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}  {{Na,Pb}})"
    apply (rule resolution_rule'[of "{Pax}" _ "{Na,Pb,Naa}" "{Pax}" "{Naa}" mguPaaPax ])
       using mguPaaPax_mgu unfolding applicable_def varsls_def  varsl_def 
          Nb_def Na_def Pax_def Pa_def Pb_def Naa_def Paa_def mguPaaPax_def resolution_def
       apply auto
     apply (rule_tac x=Na in image_eqI)
      unfolding Na_def apply auto
    apply (rule_tac x=Pb in image_eqI)
     unfolding Pb_def apply auto
    done
  then have "resolution_step 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}})" 
    by (simp add: insert_commute)
  moreover
  have "resolution_step 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}}  {{Na}})"
    apply (rule resolution_rule'[of "{Nb,Na}" _ "{Na,Pb}" "{Nb}" "{Pb}" ε])
       unfolding applicable_def varsls_def  varsl_def 
                 Pb_def Nb_def Na_def PP_def resolution_def
       using unifier_single empty_mgu apply auto
    done
  then have "resolution_step 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}})" 
    by (simp add: insert_commute)
  moreover
  have "resolution_step 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}}  {{}})"
    apply (rule resolution_rule'[of "{Na}" _ "{Pa}" "{Na}" "{Pa}" ε])
       unfolding applicable_def varsls_def  varsl_def 
                  Pa_def Nb_def Na_def PP_def resolution_def
       using unifier_single empty_mgu apply auto
    done
  then have "resolution_step 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}})" 
    by (simp add: insert_commute)
  ultimately
  have "resolution_deriv {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} 
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}}"
    unfolding resolution_deriv_def by auto 
  then show ?thesis by auto
qed

lemma resolution_example1_sem: "¬evalcs F G {{NP, PQ}, {NQ}, {PP, PQ}}"
  using resolution_example1 derivation_sound_refute by auto

lemma resolution_example2_sem: "¬evalcs F G {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}"
  using resolution_example2 derivation_sound_refute by auto

end

Theory Unification_Theorem

section ‹The Unification Theorem›

theory Unification_Theorem imports
  First_Order_Terms.Unification Resolution
begin

definition set_to_list :: "'a set  'a list" where
  "set_to_list  inv set"

lemma set_set_to_list: "finite xs  set (set_to_list xs) = xs"
proof (induction rule: finite.induct)
  case (emptyI) 
  have "set [] = {}" by auto
  then show ?case unfolding set_to_list_def inv_into_def by auto
next
  case (insertI A a)
  then have "set (a#set_to_list A) = insert a A" by auto
  then show ?case unfolding set_to_list_def inv_into_def by (metis (mono_tags, lifting) UNIV_I someI) 
qed

fun iterm_to_fterm :: "(fun_sym, var_sym) term  fterm" where
  "iterm_to_fterm (Term.Var x) = Var x"
| "iterm_to_fterm (Term.Fun f ts) = Fun f (map iterm_to_fterm ts)"

fun fterm_to_iterm :: "fterm  (fun_sym, var_sym) term" where
  "fterm_to_iterm (Var x) = Term.Var x"
| "fterm_to_iterm (Fun f ts) = Term.Fun f (map fterm_to_iterm ts)"

lemma iterm_to_fterm_cancel[simp]: "iterm_to_fterm (fterm_to_iterm t) = t"
  by (induction t) (auto simp add: map_idI)

lemma fterm_to_iterm_cancel[simp]: "fterm_to_iterm (iterm_to_fterm t) = t"
  by (induction t) (auto simp add: map_idI)

abbreviation(input) fsub_to_isub :: "substitution  (fun_sym, var_sym) subst" where
  "fsub_to_isub σ  λx. fterm_to_iterm (σ x)"

abbreviation(input) isub_to_fsub :: "(fun_sym, var_sym) subst  substitution" where
  "isub_to_fsub σ  λx. iterm_to_fterm (σ x)"

lemma iterm_to_fterm_subt: "(iterm_to_fterm t1) t σ = iterm_to_fterm (t1  (λx. fterm_to_iterm (σ x)))"
  by (induction t1) auto

lemma unifiert_unifiers:
  assumes "unifierts σ ts"
  shows "fsub_to_isub σ  unifiers (fterm_to_iterm ` ts × fterm_to_iterm ` ts)"
proof -
  have "t1  fterm_to_iterm ` ts. t2  fterm_to_iterm ` ts. t1  (fsub_to_isub σ) = t2  (fsub_to_isub σ)"
    proof (rule ballI;rule ballI)
      fix t1 t2 
      assume t1_p: "t1  fterm_to_iterm ` ts" assume t2_p: "t2  fterm_to_iterm ` ts"
      from t1_p t2_p have "iterm_to_fterm t1  ts  iterm_to_fterm t2  ts" by auto