Theory Completeness

theory Completeness
imports Unify
theory Completeness imports Unify begin

section {* Lifting Lemma *}

lemma lifting:
  assumes fin: "finite C ∧ finite D "
  assumes apart: "varsls C ∩ varsls D = {}"
  assumes inst1: "instance_ofls C' C"
  assumes inst2: "instance_ofls D' D"
  assumes appl: "applicable C' D' L' M' σ"
  shows "∃L M τ. applicable C D L M τ ∧
                   instance_ofls (resolution C' D' L' M' σ) (resolution C D L M τ)"
proof -
  let ?C'1 = "C' - L'"
  let ?D'1 = "D' - M'"

  from inst1 obtain lmbd where lmbd_p: "C ⋅ls lmbd = C'" unfolding instance_ofls_def by auto
  from inst2 obtain μ where μ_p: "D ⋅ls μ = D'" unfolding instance_ofls_def by auto
  
  from μ_p lmbd_p apart obtain η where η_p: "C ⋅ls η = C' ∧ D ⋅ls η = D'" using merge_sub by force

  from η_p have "∃L ⊆ C. L ⋅ls η = L' ∧ (C - L) ⋅ls η = ?C'1" using appl project_sub[of η C C' L'] unfolding applicable_def by auto
  then obtain L where L_p: "L ⊆ C ∧ L ⋅ls η = L' ∧ (C - L) ⋅ls η = ?C'1" by auto
  let ?C1 = "C - L"

  from η_p have "∃M ⊆ D. M ⋅ls η = M' ∧ (D - M) ⋅ls η = ?D'1" using appl project_sub[of η D D' M'] unfolding applicable_def by auto
  then obtain M where M_p: "M ⊆ D ∧ M ⋅ls η = M' ∧ (D - M) ⋅ls η = ?D'1" by auto
  let ?D1 = "D - M"

  from appl have "mguls σ (L' ∪ M'C)" unfolding applicable_def by auto
  then have "mguls σ ((L ⋅ls η) ∪ (M ⋅ls η)C)" using L_p M_p by auto
  then have "mguls σ ((L  ∪ MC) ⋅ls η)" using compls_subls subls_union by auto
  then have "unifierls σ ((L  ∪ MC) ⋅ls η)" unfolding mguls_def by auto
  then have ησuni: "unifierls (η ⋅ σ) (L  ∪ MC)" 
    unfolding unifierls_def using composition_conseq2l by auto
  then obtain τ where τ_p: "mguls τ (L  ∪ MC)" using unification fin by (meson L_p M_p finite_UnI finite_imageI rev_finite_subset) 
  then obtain φ where φ_p: "τ ⋅ φ = η ⋅ σ" using ησuni unfolding mguls_def by auto
  
  (* Showing that we have the desired resolvent *)
  let ?E = "((C - L)  ∪ (D - M)) ⋅ls τ"
  have "?E ⋅ls φ  = (?C1 ∪ ?D1 ) ⋅ls (τ ⋅ φ)" using subls_union composition_conseq2ls by auto
  also have "... = (?C1 ∪ ?D1 ) ⋅ls (η ⋅ σ)" using φ_p by auto
  also have "... = ((?C1 ⋅ls η) ∪ (?D1 ⋅ls η)) ⋅ls σ" using subls_union composition_conseq2ls by auto
  also have "... = (?C'1 ∪ ?D'1) ⋅ls σ" using η_p L_p M_p by auto
  finally have "?E ⋅ls φ = ((C' - L') ∪ (D' - M')) ⋅ls σ" by auto
  then have inst: "instance_ofls (resolution C' D' L' M' σ) (resolution C D L M τ) "
    unfolding resolution_def instance_ofls_def by blast

  (* Showing that the resolution is applicable: *)
  {
    have "C' ≠ {}" using appl unfolding applicable_def by auto
    then have "C ≠ {}" using η_p by auto
  } moreover {
    have "D' ≠ {}" using appl unfolding applicable_def by auto
    then have "D ≠ {}" using η_p by auto
  } moreover {
    have "L' ≠ {}" using appl unfolding applicable_def by auto
    then have "L ≠ {}" using L_p by auto
  } moreover {
    have "M' ≠ {}" using appl unfolding applicable_def by auto
    then have "M ≠ {}" using M_p by auto
  }
  ultimately have appll: "applicable C D L M τ" 
    using apart L_p M_p τ_p unfolding applicable_def by auto

  from inst appll show ?thesis by auto
qed


section {* Completeness *}

lemma falsifiesg_empty:
  assumes "falsifiesg [] C"
  shows "C = {}"
proof -
  have "∀l ∈ C. False"
    proof
      fix l
      assume "l∈C"
      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:  (* Maybe move to partial interpretation section *)
  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_from_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_from_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_from_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_from_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_from_fatom (get_atom l) = length B"
  assumes other: "lo ∈ C1'" "lo ≠ l"
  shows "falsifiesl B lo"
proof -
  let ?i = "nat_from_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 B2 *)
  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 B2, i.e. less than B + 1*)
  then have "nat_from_fatom (get_atom lo) < length B + 1" using undiag_diag_fatom by (cases lo) auto
  moreover
  have l_lo: "l≠lo" using other by auto
  (* The are not the complement of l2, 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_from_fatom (get_atom lo) ≠ nat_from_fatom (get_atom l)" 
    using nat_from_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_from_fatom (get_atom lo) ≠ length B" using l_p by auto
  ultimately 
  (* So their numbers are in the range of B *)
  have "nat_from_fatom (get_atom lo) < length B" by auto
  (* So we did not need the last index of B2 to falsify them, i.e. B suffices *)
  then show "falsifiesl B lo" using loB2 shorter_falsifiesl by blast
qed


theorem completeness':
  shows "closed_tree T Cs ⟹ ∀C∈Cs. finite C ⟹ ∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'"
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 ⟹ ∀C∈Cs. finite C ⟹
                 ∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs')"
  assume clo: "closed_tree T Cs"
  assume finite_Cs: "∀C∈Cs. 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 C1' of C1, and proving properties about it *)
    
    (* C1' is falsified by 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
    (* C1' is not falsified by B *)
    then have l_B: "¬falsifiesg B C1'" using C1'_p by auto

    (* C1' contains a literal l1 that is falsified by B1, but not 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_from_fatom (get_atom l1)"

    (* l1 is ofcourse 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 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

    (* l1 is negative *)
    from l1_sign_no have l1_sign: "sign l1 = False" by auto
    from l1_sign_no have l1_no: "nat_from_fatom (get_atom l1) = length B" by auto

    (* All the other literals in C1' must be falsified by B, since they are falsified by B1, but not 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 C2, C2', B2, 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 should give it a new name *)
    
    (* C2' contains a literal l2 that is falsified by 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_from_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 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

    (* l2 is negative *)
    from l2_sign_no have l2_sign: "sign l2 = True" by auto
    from l2_sign_no have l2_no: "nat_from_fatom (get_atom l2) = length B" by auto

    (* All the other literals in C2' must be falsified by B, since they are falsified by B2, but not 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 C1' and C2', l1 and l2, as well as the resolvent of C1' and 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_from_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 C1 and 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 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 B1 and B2 of B *)
    
    (* Our new clause is falsified by the branch 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: "∀C∈CsNext. finite C" unfolding CsNext_p C_p resolution_def using finite_Cs fin by auto

    (* By induction hypothesis we get a resolution derivation of {} 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 prod.collapse)
      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 Cs of {} *)
    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" "∀C∈Cs. 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

end