Theory ORD_RES

theory ORD_RES
  imports Background
begin

section ‹ORD-RES›

context simulation_SCLFOL_ground_ordered_resolution begin

lemma "ex_false_clause N ⟷ ¬ (∀C ∈ N. ord_res_Interp N C ⊫ C)"
  unfolding ex_false_clause_def by metis

lemma "¬ ex_false_clause N ⟷ (∀C ∈ N. ord_res_Interp N C ⊫ C)"
  unfolding ex_false_clause_def by metis

definition ord_res_final where
  "ord_res_final N ⟷ {#} |∈| N ∨ ¬ ex_false_clause (fset N)"

inductive ord_res where
  factoring: "{#} |∉| N ⟹ ex_false_clause (fset N) ⟹
    ― ‹Maybe write \<^term>‹¬ ord_res_final N› instead?›
    P |∈| N ⟹ ord_res.ground_factoring P C ⟹
    N' = finsert C N ⟹
    ord_res N N'" |

  resolution: "{#} |∉| N ⟹ ex_false_clause (fset N) ⟹
    P1 |∈| N ⟹ P2 |∈| N ⟹ ord_res.ground_resolution P1 P2 C ⟹
    N' = finsert C N ⟹
    ord_res N N'"

inductive ord_res_load where
  "N ≠ {||} ⟹ ord_res_load N N"

sublocale ord_res_semantics: semantics where
  step = ord_res and
  final = ord_res_final
proof unfold_locales
  fix N :: "'f gterm clause fset"
  assume "ord_res_final N"
  thus "finished ord_res N"
    unfolding ord_res_final_def
  proof (elim disjE)
    show "{#} |∈| N ⟹ finished ord_res N"
      by (simp add: finished_def ord_res.simps)
  next
    show "¬ ex_false_clause (fset N) ⟹ finished ord_res N"
      by (simp add: finished_def ord_res.simps)
  qed
qed

sublocale ord_res_language: language where
  step = ord_res and
  final = ord_res_final and
  load = ord_res_load
  by unfold_locales

end

end