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 "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:
  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: "l≠lo" 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 "∀C∈Cs. 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 ⟹ 
                            ∀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 @{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: "∀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 @{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" "∀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 

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. ∃l∈C. 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 "∃l∈C. 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 "∃l∈C. 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" "∀C∈Cs. 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" "∀C∈Cs. 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