Theory HC_Compl_Consistency

theory HC_Compl_Consistency
imports Consistency HC
begin

context begin
private lemma dt: "F ▹ Γ ∪ AX10 ⊢⇩H G ⟹ Γ ∪ AX10 ⊢⇩H F ❙→ G"
  by (metis AX100 Deduction_theorem Un_insert_right sup_left_commute)
lemma sim: "Γ ∪ AX10 ⊢⇩H F ⟹ F ▹ Γ ∪ AX10 ⊢⇩H G ⟹ Γ ∪ AX10 ⊢⇩H G"
  using MP dt by blast
lemma sim_conj: "F ▹ G ▹ Γ ∪ AX10 ⊢⇩H H ⟹ Γ ∪ AX10 ⊢⇩H F ⟹ Γ ∪ AX10 ⊢⇩H G ⟹ Γ ∪ AX10 ⊢⇩H H"
  using MP dt by (metis Un_insert_left)
lemma sim_disj: "⟦F ▹ Γ ∪ AX10 ⊢⇩H H; G ▹ Γ ∪ AX10 ⊢⇩H H; Γ ∪ AX10 ⊢⇩H F ❙∨ G⟧ ⟹ Γ ∪ AX10 ⊢⇩H H"
proof goal_cases
  case 1
  have 2: "Γ ∪ AX10 ⊢⇩H F ❙→ H" by (simp add: 1 dt)
  have 3: "Γ ∪ AX10 ⊢⇩H G ❙→ H" by (simp add: 1 dt)
  have 4: "Γ ∪ AX10 ⊢⇩H (F ❙∨ G) ❙→ H" by (meson 2 3 HC.simps HC_intros(7) HC_mono sup_ge2)
  thus ?case  using 1(3) MP by blast
qed

private lemma someax: "Γ ∪ AX10 ⊢⇩H F ❙→ ❙¬ F ❙→ ⊥"
proof -
  have "F ▹ Γ ∪ AX10 ⊢⇩H ❙¬ F ❙→ F ❙→ ⊥"
    by (meson HC_intros(12) HC_mono subset_insertI sup_ge2)
  then have "❙¬ F ▹ F ▹ Γ ∪ AX10 ⊢⇩H ⊥"
    by (meson HC.simps HC_mono insertI1 subset_insertI)
  then show ?thesis
    by (metis (no_types) Un_insert_left dt)
qed

lemma lem: "Γ ∪ AX10 ⊢⇩H ❙¬ F ❙∨ F"
proof -
  thm HC_intros(7)[of F ⊥ "Not F"]
  have "F ▹ Γ ∪ AX10 ⊢⇩H ( ❙¬ F ❙∨ F)"
    by (metis AX10.intros(3) Ax HC_mono MP Un_commute Un_insert_left insertI1 sup_ge1)
  hence "F ▹ Γ ∪ AX10 ⊢⇩H ❙¬ ( ❙¬ F ❙∨ F) ❙→ ⊥" using someax by (metis HC.simps Un_insert_left)
  hence "❙¬ ( ❙¬ F ❙∨ F) ▹ F ▹ Γ ∪ AX10 ⊢⇩H ⊥" by (meson Ax HC_mono MP insertI1 subset_insertI)
  hence "❙¬ ( ❙¬ F ❙∨ F) ▹ Γ ∪ AX10 ⊢⇩H F ❙→ ⊥"
    by (metis Un_insert_left dt insert_commute)
      
  have "❙¬F ▹ Γ ∪ AX10 ⊢⇩H ( ❙¬ F ❙∨ F)"
    by (metis HC.simps HC_intros(5) HC_mono inf_sup_ord(4) insertI1 insert_is_Un)
  hence "❙¬F ▹ Γ ∪ AX10 ⊢⇩H ❙¬ ( ❙¬ F ❙∨ F) ❙→ ⊥" using someax by (metis HC.simps Un_insert_left)
  hence "❙¬ ( ❙¬ F ❙∨ F) ▹ ❙¬F ▹ Γ ∪ AX10 ⊢⇩H ⊥" by (meson Ax HC_mono MP insertI1 subset_insertI)
  hence "❙¬ ( ❙¬ F ❙∨ F) ▹ Γ ∪ AX10 ⊢⇩H ❙¬F ❙→ ⊥"
    by (metis Un_insert_left dt insert_commute)
  
  hence "Γ ∪ AX10 ⊢⇩H ❙¬ ( ❙¬ F ❙∨ F) ❙→ ⊥"
    by (meson HC_intros(13) HC_mono MP ‹❙¬ (❙¬ F ❙∨ F) ▹ Γ ∪ AX10 ⊢⇩H F ❙→ ⊥› dt subset_insertI sup_ge2)
  thus ?thesis by (meson HC.simps HC_intros(13) HC_mono sup_ge2)
(*    apply(insert HC_mono dt HC_intros(3-)[THEN HC_mono, OF sup_ge2] sim HC.intros)
    sledgehammer[debug,max_facts=50,timeout=120]*)
qed

lemma exchg: "Γ ∪ AX10 ⊢⇩H F ❙∨ G ⟹ Γ ∪ AX10 ⊢⇩H G ❙∨ F"
  by (meson AX10.intros(3) HC.simps HC_intros(5) HC_intros(7) HC_mono sup_ge2)
    
lemma lem2: "Γ ∪ AX10 ⊢⇩H F ❙∨ ❙¬ F" by (simp add: exchg lem)
  
  
lemma imp_sim: "Γ ∪ AX10 ⊢⇩H F ❙→ G ⟹ Γ ∪ AX10 ⊢⇩H ❙¬ F ❙∨ G"
proof goal_cases case 1
  have "Γ ∪ AX10 ⊢⇩H F ❙→ ❙¬ F ❙∨ G"
  proof -
    have f1: "∀F f Fa. ¬ (F ⊢⇩H f) ∨ ¬ F ⊆ Fa ∨ Fa ⊢⇩H f"
      using HC_mono by blast
    then have f2: "F ▹ Γ ∪ AX10 ⊢⇩H F ❙→ G"
      by (metis "1" subset_insertI) (* > 1.0 s, timed out *)
    have "Γ ∪ AX10 ⊢⇩H G ❙→ ❙¬ F ❙∨ G"
      using f1 by blast
    then show ?thesis
      using f2 f1 by (metis (no_types) HC.simps dt insertI1 subset_insertI)
  qed
  moreover have "Γ ∪ AX10 ⊢⇩H ❙¬F ❙→ ❙¬ F ❙∨ G" by (simp add: AX10.intros(2) Ax)
  ultimately show ?case
  proof -
    have "⋀F f fa fb. ¬ (F ⊢⇩H f ❙→ fa) ∨ ¬ (fb ▹ F ⊢⇩H f) ∨ fb ▹ F ⊢⇩H fa"
      by (meson HC_mono MP subset_insertI)
    then show ?thesis
      by (metis Ax ‹Γ ∪ AX10 ⊢⇩H F ❙→ ❙¬ F ❙∨ G› ‹Γ ∪ AX10 ⊢⇩H ❙¬ F ❙→ ❙¬ F ❙∨ G› insertI1 lem sim_disj)
  qed
qed
  
lemma inpcp: "Γ ∪ AX10 ⊢⇩H ⊥ ⟹ Γ ∪ AX10 ⊢⇩H F"
  by (meson HC_intros(13) HC_mono MP dt subset_insertI sup_ge2)
    
lemma HC_case_distinction: "Γ ∪ AX10 ⊢⇩H F ❙→ G ⟹ Γ ∪ AX10 ⊢⇩H ❙¬ F ❙→ G ⟹ Γ ∪ AX10 ⊢⇩H G"
  using HC_intros(7)[of F G "Not F"] lem2
  by (metis (no_types, opaque_lifting) HC.simps HC_mono insertI1 sim_disj subset_insertI)
  
lemma nand_sim: "Γ ∪ AX10 ⊢⇩H ❙¬ (F ❙∧ G) ⟹ Γ ∪ AX10 ⊢⇩H ❙¬ F ❙∨ ❙¬ G"
proof goal_cases case 1
  have "Γ ∪ AX10 ⊢⇩H F ❙→ G ❙→ F ❙∧ G" by (simp add: AX10.intros(7) Ax)
  hence 2: "F ▹ G ▹ Γ ∪ AX10 ⊢⇩H F ❙∧ G"
    by (meson Ax HC_mono MP insertI1 subset_insertI)
  hence 3: "F ▹ G ▹ Γ ∪ AX10 ⊢⇩H ⊥" using 1 by (meson HC_intros(12) HC_mono MP subset_insertI sup_ge2)
  from 2 have "Γ ∪ AX10 ⊢⇩H G ❙→ F ❙→ F ❙∧ G" by (metis Un_insert_left dt)
  have 4: "Γ ∪ AX10 ⊢⇩H ❙¬ F ❙→ ❙¬ F ❙∨ ❙¬ G" by (simp add: AX10.intros(2) Ax)
  have 5: "Γ ∪ AX10 ⊢⇩H ❙¬ G ❙→ F ❙→ ❙¬ F ❙∨ ❙¬ G"
    by (metis (full_types) AX10.intros(3) AX100 Ax HC_mono MP Un_assoc Un_insert_left dt inf_sup_ord(4) insertI1 subset_insertI sup_ge2)
  have 6: "Γ ∪ AX10 ⊢⇩H G ❙→ F ❙→ ❙¬ F ❙∨ ❙¬ G" using 3 inpcp by (metis Un_insert_left dt)
  have 7: "Γ ∪ AX10 ⊢⇩H F ❙→ ❙¬ F ❙∨ ❙¬ G" using 5 6 HC_case_distinction by blast
  show ?case using 4 7 HC_case_distinction by blast
qed
  
lemma HC_contrapos_nn:
  "⟦Γ ∪ AX10 ⊢⇩H ❙¬ F; Γ ∪ AX10 ⊢⇩H G ❙→ F⟧ ⟹ Γ ∪ AX10 ⊢⇩H ❙¬ G"
proof goal_cases case 1
  from 1(1) have "Γ ∪ AX10 ⊢⇩H F ❙→ ⊥" using HC_intros(12) using HC_mono MP by blast
  hence "Γ ∪ AX10 ⊢⇩H G ❙→ ⊥" by (meson 1(2) HC.intros(1) HC_mono MP dt insertI1 subset_insertI)
  thus ?case by(meson HC_intros(11) HC_intros(3) HC_mono MP sup_ge2)
qed
      

lemma nor_sim: 
assumes "Γ ∪ AX10 ⊢⇩H ❙¬ (F ❙∨ G)"
shows "Γ ∪ AX10 ⊢⇩H ❙¬ F" " Γ ∪ AX10 ⊢⇩H ❙¬ G"
  using HC_contrapos_nn assms by (metis HC_intros(5,6) HC_mono sup_ge2)+
    
lemma HC_contrapos_np:
  "⟦Γ ∪ AX10 ⊢⇩H ❙¬ F; Γ ∪ AX10 ⊢⇩H ❙¬ G ❙→ F⟧ ⟹ Γ ∪ AX10 ⊢⇩H G"
    by (meson HC_intros(12) HC_intros(13) HC_mono MP sup_ge2  HC_contrapos_nn[of Γ F "Not G"])    
    
lemma not_imp: "Γ ∪ AX10 ⊢⇩H ❙¬ F ❙→ F ❙→ G"
proof goal_cases case 1
  have "Γ ∪ AX10 ⊢⇩H ❙¬ F ❙→ F ❙→ ⊥" by (simp add: AX10.intros(9) Ax)
  hence "❙¬ F ▹ F ▹ Γ ∪ AX10 ⊢⇩H ⊥" by (meson HC.simps HC_mono insertI1 subset_insertI)
  hence "❙¬ F ▹ F ▹ Γ ∪ AX10 ⊢⇩H G" by (metis (no_types, opaque_lifting) Un_commute Un_insert_right inpcp)
  thus ?case by (metis Un_insert_left dt insert_commute)
qed

lemma HC_consistent:  "pcp {Γ| Γ. ¬(Γ ∪ AX10 ⊢⇩H ⊥)}"
  unfolding pcp_def
  apply(intro ballI conjI; unfold mem_Collect_eq; elim exE conjE; erule contrapos_np; clarsimp)
          subgoal by (simp add: HC.Ax)
         subgoal by (meson Ax HC_intros(12) HC_mono MP Un_upper1 sup_ge2)
        subgoal using sim_conj by (metis (no_types, lifting) Ax HC_intros(8) HC_intros(9) HC_mono MP sup_ge1 sup_ge2)
       subgoal using sim_disj using Ax by blast
      subgoal by (erule (1) sim_disj) (simp add: Ax imp_sim)
     subgoal by (metis Ax HC_contrapos_nn MP Un_iff Un_insert_left dt inpcp someax)  
    subgoal by(erule (1) sim_disj) (simp add: Ax nand_sim)
   subgoal by(erule  sim_conj) (meson Ax Un_iff nor_sim)+
  subgoal for Γ F G apply(erule sim_conj) 
     subgoal by (meson Ax HC_Compl_Consistency.not_imp HC_contrapos_np Un_iff) 
    subgoal by (metis Ax HC_contrapos_nn HC_intros(3) HC_mono sup_ge1 sup_ge2)
  done
done

end

corollary HC_complete: 
  fixes F :: "'a :: countable formula"
  shows "⊨ F ⟹ AX10 ⊢⇩H F"
proof(erule contrapos_pp)
  let ?W = "{Γ| Γ. ¬((Γ :: ('a :: countable) formula set) ∪ AX10 ⊢⇩H ⊥)}"
    note [[show_types]]
  assume ‹¬ (AX10 ⊢⇩H F)›
  hence "¬ (❙¬F ▹ AX10 ⊢⇩H ⊥)"
    by (metis AX100 Deduction_theorem HC_intros(13) MP Un_insert_right)
  hence "{❙¬F} ∈ ?W" by simp
  with pcp_sat HC_consistent have "sat {❙¬ F}" .
  thus "¬ ⊨ F" by (simp add: sat_def)
qed
    

  
end