Theory Resolution

theory Resolution
imports TermsAndLiterals Tree
theory Resolution imports TermsAndLiterals Tree begin

section {* Terms and literals *}

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 ≡ ⋃l∈L. varsl l"

lemma ground_varst: "groundt t ⟹ varst t = {}" 
by (induction t) auto

lemma groundts_varsts: "groundts ts ⟹ varsts ts = {}"
using ground_varst by auto

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

lemma groundls_varsls: "groundls L ⟹ varsls L = {}" unfolding varsls_def using 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: "groundt t ⟹ (evalt E F t = evalt E' F t)"
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: "groundts ts ⟹ (evalts E F ts = evalts E' F ts)"
  using ground_var_denott by (metis map_eq_conv)


lemma ground_var_denot: "groundl l ⟹ (evall E F G l = evall E' F G l)"
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: "groundt t ⟹ t ⋅t σ = t"
by (induction t) (auto simp add: map_idI)

lemma ground_subs: "groundts ts ⟹ ts ⋅ts σ = ts" 
using ground_sub by (simp add: map_idI)

lemma groundl_subs: "groundl l ⟹ l ⋅l σ = l" 
using 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" unfolding composition_def using composition_conseq2t by simp
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
  moreover
  ultimately show ?thesis by auto
qed

lemma relevant_vars_subt:
  "∀x ∈ varst t. σ1 x = σ2 x ⟹ t ⋅t σ1 = t ⋅t σ2"
proof (induction t)
  case (Fun f ts)
  have f: "⋀t. t ∈ set ts ⟹ varst t ⊆ varsts ts" by (induction ts) auto
  have "∀t∈set 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 "∀t∈set 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:
  "∀x ∈ varsl l. σ1 x = σ2 x ⟹ l ⋅l σ1 = l ⋅l σ2"
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: "l∈L"
      then have "∀x∈varsl 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 " ∀x∈varsls 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'': 
  "x ∈ varst  (t ⋅t (λx::char list. Var (y @ x))) ⟹ ∃x'. x = y@x'"
by (induction t) auto


lemma std_apart_apart': "x ∈ varsl (l ⋅l (λx. Var  (y@x))) ⟹ ∃x'. x = y@x'"
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 should 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 "l∈L"
      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: "unifierls σ L ⟹ L' ⊆ L ⟹ unifierls σ L' " 
  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: (* rename *)
    "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 *}
(* Proving instantiation sound *)

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 σ)"
proof - 
 have "∀E. ∃l ∈ C ⋅ls σ. evall E F G l"
  proof
   fix E
   from asm have "∀E. ∃l ∈ C. evall E F G l" unfolding evalc_def by auto
   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
 then show "evalc F G (C ⋅ls σ)" unfolding evalc_def by auto
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
 

lemma 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 sound_step: "mresolution_step Cs Cs' ⟹ evalcs F G Cs ⟹ evalcs F G Cs'"
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

lemma lsound_step: "resolution_step Cs Cs' ⟹ evalcs F G Cs ⟹ evalcs F G Cs'"
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 sound_derivation: 
  "mresolution_deriv Cs Cs' ⟹ evalcs F G Cs ⟹ evalcs F G Cs'" 
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 sound_step by auto
qed

lemma lsound_derivation: 
  "resolution_deriv Cs Cs' ⟹ evalcs F G Cs ⟹ evalcs F G Cs'" 
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 lsound_step by auto
qed

section {* Herbrand Interpretations *}

(* HFun is the Herbrand function denotation in which terms are mapped to themselves  *)
term HFun

lemma eval_groundt: "groundt t ⟹ (evalt E HFun t) = hterm_of_fterm t"
  by (induction t) auto


lemma eval_groundts: "groundts ts ⟹ (evalts E HFun ts) = hterms_of_fterms ts" 
  unfolding hterms_of_fterms_def using 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_from_fatom (get_atom l) in
          i < length G ∧ G ! i = (¬sign l)
        )"

(* A groundt clause is falsified if it is actually groundt 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_from_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

(* 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

(* Under an Herbrand interpretation, an environment is "equivalent" 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

(* 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 asm 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 assms 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 asm 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 assms 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 assms by auto
  moreover have "instance_ofls (std1 C1) C1" using assms 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 assms by auto
  moreover have "instance_ofls (std2 C2) C2" using assms unfolding instance_ofls_def by auto
  ultimately show "var_renaming_of C2 (std2 C2)" unfolding var_renaming_of_def by auto
qed

subsection {* 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 "∀l∈C. f l ≤ (Max (f ` C))" by auto
qed

lemma extend_preserves_model: (* only for groundt *)
  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: "∀l∈C. nat_from_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: "l∈C ∧ ¬falsifiesl (f (Suc n)) l" using C_ground by blast
    let ?i = "nat_from_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_from_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_from_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 groundt *)
  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 {sub_of_denot E}ls has a largest index of a literal.  *)
  obtain n where largest: "∀l ∈ C. nat_from_fatom (get_atom l) ≤ n" using fin_c maximum[of C "λl. nat_from_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 groundt world: *)
  from model_c have "∀n. ¬falsifiesc (f n) (C ⋅ls ?σ)" using partial_equiv_subst by blast
  (* Then from syntactic groundt world to semantic groundt 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 groundt 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

(* 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: "branch b (deeptree n) ⟹ length b = n"
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_from_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 "l∈C"
    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

(* 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

(* "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" "∀C∈Cs. 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_from_fatom (get_atom l) < length ds"
  shows "falsifiesl ds l"
proof -
  let ?i = "nat_from_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" "∀C∈Cs. 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" "∀C∈Cs. 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