diff --git a/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy b/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy new file mode 100644 --- /dev/null +++ b/thys/Functional_Ordered_Resolution_Prover/Executable_FO_Ordered_Resolution_Prover.thy @@ -0,0 +1,263 @@ +(* Title: An Executable Simple Ordered Resolution Prover for First-Order Clauses + Author: Dmitriy Traytel , 2017, 2018 + Author: Anders Schlichtkrull , 2018 + Maintainer: Anders Schlichtkrull +*) + +section \An Executable Simple Ordered Resolution Prover for First-Order Clauses\ + +text \ +This theory provides an executable functional implementation of the +\deterministic_RP\ prover, building on the \textsf{IsaFoR} library +for the notion of terms and on the Knuth--Bendix order. +\ + +theory Executable_FO_Ordered_Resolution_Prover + imports + Deterministic_FO_Ordered_Resolution_Prover + Executable_Subsumption + "HOL-Library.Code_Target_Nat" + Show.Show_Instances + IsaFoR_Term_KBO +begin + +global_interpretation RP: deterministic_FO_resolution_prover where + S = "\_. {#}" and + subst_atm = "(\)" and + id_subst = "Var :: _ \ ('f :: {weighted, compare_order}, nat) term" and + comp_subst = "(\\<^sub>s)" and + renamings_apart = renamings_apart and + atm_of_atms = "Fun undefined" and + mgu = mgu_sets and + less_atm = less_kbo and + size_atm = size and + timestamp_factor = 1 and + size_factor = 1 + defines deterministic_RP = RP.deterministic_RP + and deterministic_RP_step = RP.deterministic_RP_step + and is_final_dstate = RP.is_final_dstate + and is_reducible_lit = RP.is_reducible_lit + and is_tautology = RP.is_tautology + and maximal_wrt = RP.maximal_wrt + and reduce = RP.reduce + and reduce_all = RP.reduce_all + and reduce_all2 = RP.reduce_all2 + and remdups_clss = RP.remdups_clss + and resolve = RP.resolve + and resolve_on = RP.resolve_on + and resolvable = RP.resolvable + and resolvent = RP.resolvent + and resolve_rename = RP.resolve_rename + and resolve_rename_either_way = RP.resolve_rename_either_way + and select_min_weight_clause = RP.select_min_weight_clause + and strictly_maximal_wrt = RP.strictly_maximal_wrt + and strictly_subsume = RP.strictly_subsume + and subsume = RP.subsume + and weight = RP.weight + and St0 = RP.St0 + and sorted_list_of_set = "linorder.sorted_list_of_set (le_of_comp compare)" + and sort_key = "linorder.sort_key (le_of_comp compare)" + and insort_key = "linorder.insort_key (le_of_comp compare)" + by (unfold_locales) + (auto simp: less_kbo_subst is_ground_atm_ground less_kbo_less intro: ground_less_less_kbo) + +declare + RP.deterministic_RP.simps[code] + RP.deterministic_RP_step.simps[code] + RP.is_final_dstate.simps[code] + RP.is_tautology_def[code] + RP.reduce.simps[code] + RP.reduce_all_def[code] + RP.reduce_all2.simps[code] + RP.resolve_rename_def[code] + RP.resolve_rename_either_way_def[code] + RP.select_min_weight_clause.simps[code] + RP.weight.simps[code] + St0_def[code] + substitution_ops.strictly_subsumes_def[code] + substitution_ops.subst_cls_lists_def[code] + substitution_ops.subst_lit_def[code] + substitution_ops.subst_cls_def[code] + +lemma remove1_mset_subset_eq: "remove1_mset a A \# B \ A \# add_mset a B" + by (metis add_mset_add_single subset_eq_diff_conv) + +lemma Bex_cong: "(\b. b \ B \ P b = Q b) \ Bex B P = Bex B Q" + by auto + +lemma is_reducible_lit_code[code]: "RP.is_reducible_lit Ds C L = + (\D \ set Ds. (\L' \ set D. + if is_pos L' = is_neg L then + (case match_term_list [(atm_of L', atm_of L)] Map.empty of + None \ False + | Some \ \ subsumes_list (remove1 L' D) C \) + else False))" + unfolding RP.is_reducible_lit_def subsumes_list_alt subsumes_modulo_def + apply (rule Bex_cong)+ + subgoal for D L' + apply (split if_splits option.splits)+ + apply safe + subgoal for \ + using term_subst_eq[of _ "subst_of_map Var (\x. if x \ vars_lit L' then Some (\ x) else None)" \] + by (cases L; cases L'; + auto simp add: subst_lit_def subst_of_map_def + dest!: match_term_list_complete[of _ _ "\x. if x \ vars_lit L' then Some (\ x) else None"]) + subgoal for \ + using term_subst_eq[of _ "subst_of_map Var (\x. if x \ vars_lit L' then Some (\ x) else None)" \] + by (cases L; cases L'; + auto simp add: subst_lit_def subst_of_map_def + dest!: match_term_list_complete[of _ _ "\x. if x \ vars_lit L' then Some (\ x) else None"]) + subgoal for \ + by (cases L; cases L'; simp add: subst_lit_def) + subgoal for \ + by (cases L; cases L'; simp add: subst_lit_def) + subgoal for \ \ + using same_on_vars_clause[of "mset (remove1 L' D)" "subst_of_map Var + (\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None)" \] + apply (cases L; cases L'; auto simp add: subst_lit_def dom_def subst_of_map_def + dest!: match_term_list_sound split: option.splits if_splits + intro!: exI[of _ "\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None"]) + by (auto 0 4 simp: extends_subst_def subst_of_map_def split: option.splits dest!: term_subst_eq_rev) + subgoal for \ \ + by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def extends_subst_def + dest!: match_term_list_sound intro!: exI[of _ "subst_of_map Var \"] term_subst_eq) + subgoal for \ \ + using same_on_vars_clause[of "mset (remove1 L' D)" "subst_of_map Var + (\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None)" \] + apply (cases L; cases L'; auto simp add: subst_lit_def dom_def subst_of_map_def + dest!: match_term_list_sound split: option.splits if_splits + intro!: exI[of _ "\x. if x \ vars_clause (remove1_mset L' (mset D)) \ dom \ then Some (\ x) else None"]) + by (auto 0 4 simp: extends_subst_def subst_of_map_def split: option.splits dest!: term_subst_eq_rev) + subgoal for \ \ + by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def extends_subst_def + dest!: match_term_list_sound intro!: exI[of _ "subst_of_map Var \"] term_subst_eq) + subgoal for \ \ + by (cases L; cases L'; simp add: subst_lit_def) + subgoal for \ \ + by (cases L; cases L'; simp add: subst_lit_def) + done + done + +declare + Pairs_def[folded sorted_list_of_set_def, code] + linorder.sorted_list_of_set_sort_remdups[OF class_linorder_compare, + folded sorted_list_of_set_def sort_key_def, code] + linorder.sort_key_def[OF class_linorder_compare, folded sort_key_def insort_key_def, code] + linorder.insort_key.simps[OF class_linorder_compare, folded insort_key_def, code] + +export_code St0 in SML +export_code deterministic_RP in SML module_name RP + +(*arbitrary*) +instantiation nat :: weighted begin +definition weights_nat :: "nat weights" where "weights_nat = + \w = Suc \ prod_encode, w0 = 1, pr_strict = \(f, n) (g, m). f > g \ f = g \ n > m, least = \n. n = 0, scf = \_ _. 1\" + +instance + by (intro_classes, unfold_locales) + (auto simp: weights_nat_def SN_iff_wf asymp.simps irreflp_def prod_encode_def + intro!: wf_subset[OF wf_lex_prod]) +end + +definition prover :: "((nat, nat) Term.term literal list \ nat) list \ bool" where + "prover N = (case deterministic_RP (St0 N 0) of + None \ True + | Some R \ [] \ set R)" + +theorem prover_complete_refutation: "prover N \ satisfiable (RP.grounded_N0 N)" + unfolding prover_def St0_def + using RP.deterministic_RP_complete[of N 0] RP.deterministic_RP_refutation[of N 0] + by (force simp: grounding_of_clss_def grounding_of_cls_def ex_ground_subst + split: option.splits if_splits) + +definition string_literal_of_nat :: "nat \ String.literal" where + "string_literal_of_nat n = String.implode (show n)" + +export_code prover Fun Var Pos Neg string_literal_of_nat "0::nat" "Suc" in SML module_name RPx + +abbreviation "\ \ Fun 42" +abbreviation "\ \ Fun 0 []" +abbreviation "\ \ Fun 1 []" +abbreviation "\ \ Fun 2 []" +abbreviation "X \ Var 0" +abbreviation "Y \ Var 1" +abbreviation "Z \ Var 2" + +value "prover + ([([Neg (\[X,Y,Z]), Pos (\[Y,Z,X])], 1), + ([Pos (\[\,\,\])], 1), + ([Neg (\[\,\,\])], 1)] + :: ((nat, nat) Term.term literal list \ nat) list)" + +value "prover + ([([Pos (\[X,Y])], 1), ([Neg (\[X,X])], 1)] + :: ((nat, nat) Term.term literal list \ nat) list)" + +value "prover ([([Neg (\[X,Y,Z]), Pos (\[Y,Z,X])], 1)] + :: ((nat, nat) Term.term literal list \ nat) list)" + +definition mk_MSC015_1 :: "nat \ ((nat, nat) Term.term literal list \ nat) list" where + "mk_MSC015_1 n = + (let + init = ([Pos (\ (replicate n \))], 1); + rules = map (\i. ([Neg (\ (map Var [0 ..< n - i - 1] @ \ # replicate i \)), + Pos (\ (map Var [0 ..< n - i - 1] @ \ # replicate i \))], 1)) [0 ..< n]; + goal = ([Neg (\ (replicate n \))], 1) + in init # rules @ [goal])" + +value "prover (mk_MSC015_1 1)" +value "prover (mk_MSC015_1 2)" +value "prover (mk_MSC015_1 3)" +value "prover (mk_MSC015_1 4)" +value "prover (mk_MSC015_1 5)" +value "prover (mk_MSC015_1 10)" + +lemma + assumes + "p a a a a a a a a a a a a a a" + "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13. + \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 a \ + p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 b)" + "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12. + \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 a b \ + p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 b a)" + "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11. + \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 a b b \ + p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 b a a)" + "(\x1 x2 x3 x4 x5 x6 x7 x8 x9 x10. + \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 a b b b \ + p x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 b a a a)" + "(\x1 x2 x3 x4 x5 x6 x7 x8 x9. + \ p x1 x2 x3 x4 x5 x6 x7 x8 x9 a b b b b \ + p x1 x2 x3 x4 x5 x6 x7 x8 x9 b a a a a)" + "(\x1 x2 x3 x4 x5 x6 x7 x8. + \ p x1 x2 x3 x4 x5 x6 x7 x8 a b b b b b \ + p x1 x2 x3 x4 x5 x6 x7 x8 b a a a a a)" + "(\x1 x2 x3 x4 x5 x6 x7. + \ p x1 x2 x3 x4 x5 x6 x7 a b b b b b b \ + p x1 x2 x3 x4 x5 x6 x7 b a a a a a a)" + "(\x1 x2 x3 x4 x5 x6. + \ p x1 x2 x3 x4 x5 x6 a b b b b b b b \ + p x1 x2 x3 x4 x5 x6 b a a a a a a a)" + "(\x1 x2 x3 x4 x5. + \ p x1 x2 x3 x4 x5 a b b b b b b b b \ + p x1 x2 x3 x4 x5 b a a a a a a a a)" + "(\x1 x2 x3 x4. + \ p x1 x2 x3 x4 a b b b b b b b b b \ + p x1 x2 x3 x4 b a a a a a a a a a)" + "(\x1 x2 x3. + \ p x1 x2 x3 a b b b b b b b b b b \ + p x1 x2 x3 b a a a a a a a a a a)" + "(\x1 x2. + \ p x1 x2 a b b b b b b b b b b b \ + p x1 x2 b a a a a a a a a a a a)" + "(\x1. + \ p x1 a b b b b b b b b b b b b \ + p x1 b a a a a a a a a a a a a)" + "(\ p a b b b b b b b b b b b b b \ + p b a a a a a a a a a a a a a)" + "\ p b b b b b b b b b b b b b b" + shows False + using assms by metis + +end diff --git a/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy b/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy --- a/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy +++ b/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy @@ -1,363 +1,365 @@ (* Title: An Executable Algorithm for Clause Subsumption Author: Dmitriy Traytel , 2017 Maintainer: Anders Schlichtkrull *) section \An Executable Algorithm for Clause Subsumption\ text \ -This theory provides a functional implementation of clause subsumption, building -on the \textsf{IsaFoR} library (part of the AFP entry \First_Order_Terms\). +This theory provides an executable functional implementation of clause +subsumption, building on the \textsf{IsaFoR} library. \ theory Executable_Subsumption - imports IsaFoR_Term First_Order_Terms.Matching + imports + IsaFoR_Term + First_Order_Terms.Matching begin subsection \Naive Implementation of Clause Subsumption\ fun subsumes_list where "subsumes_list [] Ks \ = True" | "subsumes_list (L # Ls) Ks \ = (\K \ set Ks. is_pos K = is_pos L \ (case match_term_list [(atm_of L, atm_of K)] \ of None \ False | Some \ \ subsumes_list Ls (remove1 K Ks) \))" lemma atm_of_map_literal[simp]: "atm_of (map_literal f l) = f (atm_of l)" by (cases l; simp) definition "extends_subst \ \ = (\x \ dom \. \ x = \ x)" lemma extends_subst_refl[simp]: "extends_subst \ \" unfolding extends_subst_def by auto lemma extends_subst_trans: "extends_subst \ \ \ extends_subst \ \ \ extends_subst \ \" unfolding extends_subst_def dom_def by (metis mem_Collect_eq) lemma extends_subst_dom: "extends_subst \ \ \ dom \ \ dom \" unfolding extends_subst_def dom_def by auto lemma extends_subst_extends: "extends_subst \ \ \ x \ dom \ \ \ x = \ x" unfolding extends_subst_def dom_def by auto lemma extends_subst_fun_upd_new: "\ x = None \ extends_subst (\(x \ t)) \ \ extends_subst \ \ \ \ x = Some t" unfolding extends_subst_def dom_fun_upd subst_of_map_def by (force simp add: dom_def split: option.splits) lemma extends_subst_fun_upd_matching: "\ x = Some t \ extends_subst (\(x \ t)) \ \ extends_subst \ \" unfolding extends_subst_def dom_fun_upd subst_of_map_def by (auto simp add: dom_def split: option.splits) lemma extends_subst_empty[simp]: "extends_subst Map.empty \" unfolding extends_subst_def by auto lemma extends_subst_cong_term: "extends_subst \ \ \ vars_term t \ dom \ \ t \ subst_of_map Var \ = t \ subst_of_map Var \" by (force simp: extends_subst_def subst_of_map_def split: option.splits intro!: term_subst_eq) lemma extends_subst_cong_lit: "extends_subst \ \ \ vars_lit L \ dom \ \ L \lit subst_of_map Var \ = L \lit subst_of_map Var \" by (cases L) (auto simp: extends_subst_cong_term) definition "subsumes_modulo C D \ = (\\. dom \ = vars_clause C \ dom \ \ extends_subst \ \ \ subst_cls C (subst_of_map Var \) \# D)" abbreviation subsumes_list_modulo where "subsumes_list_modulo Ls Ks \ \ subsumes_modulo (mset Ls) (mset Ks) \" lemma vars_clause_add_mset[simp]: "vars_clause (add_mset L C) = vars_lit L \ vars_clause C" unfolding vars_clause_def by auto lemma subsumes_list_modulo_Cons: "subsumes_list_modulo (L # Ls) Ks \ \ (\K \ set Ks. \\. extends_subst \ \ \ dom \ = vars_lit L \ dom \ \ L \lit (subst_of_map Var \) = K \ subsumes_list_modulo Ls (remove1 K Ks) \)" unfolding subsumes_modulo_def proof (safe, goal_cases left_right right_left) case (left_right \) then show ?case by (intro bexI[of _ "L \lit subst_of_map Var \"] exI[of _ "\x. if x \ vars_lit L \ dom \ then \ x else None"], intro conjI exI[of _ \]) (auto 0 3 simp: extends_subst_def dom_def split: if_splits simp: insert_subset_eq_iff subst_lit_def intro!: extends_subst_cong_lit) next case (right_left K \ \') then show ?case by (intro bexI[of _ "L \lit subst_of_map Var \"] exI[of _ \'], intro conjI exI[of _ \]) (auto simp: insert_subset_eq_iff subst_lit_def extends_subst_cong_lit intro: extends_subst_trans) qed lemma decompose_Some_var_terms: "decompose (Fun f ss) (Fun g ts) = Some eqs \ f = g \ length ss = length ts \ eqs = zip ss ts \ (\(t, u)\set ((Fun f ss, Fun g ts) # P). vars_term t) = (\(t, u)\set (eqs @ P). vars_term t)" by (drule decompose_Some) (fastforce simp: in_set_zip in_set_conv_nth Bex_def image_iff) lemma match_term_list_sound: "match_term_list tus \ = Some \ \ extends_subst \ \ \ dom \ = (\(t, u)\set tus. vars_term t) \ dom \ \ (\(t,u)\set tus. t \ subst_of_map Var \ = u)" proof (induct tus \ rule: match_term_list.induct) case (2 x t P \) then show ?case by (auto 0 3 simp: extends_subst_fun_upd_new extends_subst_fun_upd_matching subst_of_map_def dest: extends_subst_extends simp del: fun_upd_apply split: if_splits option.splits) next case (3 f ss g ts P \) from 3(2) obtain eqs where "decompose (Fun f ss) (Fun g ts) = Some eqs" "match_term_list (eqs @ P) \ = Some \" by (auto split: option.splits) with 3(1)[OF this] show ?case proof (elim decompose_Some_var_terms[where P = P, elim_format] conjE, intro conjI, goal_cases extend dom subst) case subst from subst(3,5,6,7) show ?case by (auto 0 6 simp: in_set_conv_nth list_eq_iff_nth_eq Ball_def) qed auto qed auto lemma match_term_list_complete: "match_term_list tus \ = None \ extends_subst \ \ \ dom \ = (\(t, u)\set tus. vars_term t) \ dom \ \ (\(t,u)\set tus. t \ subst_of_map Var \ \ u)" proof (induct tus \ arbitrary: \ rule: match_term_list.induct) case (2 x t P \) then show ?case by (auto simp: extends_subst_fun_upd_new extends_subst_fun_upd_matching subst_of_map_def dest: extends_subst_extends simp del: fun_upd_apply split: if_splits option.splits) next case (3 f ss g ts P \) show ?case proof (cases "decompose (Fun f ss) (Fun g ts) = None") case False with 3(2) obtain eqs where "decompose (Fun f ss) (Fun g ts) = Some eqs" "match_term_list (eqs @ P) \ = None" by (auto split: option.splits) with 3(1)[OF this 3(3) trans[OF 3(4) arg_cong[of _ _ "\x. x \ dom \"]]] show ?thesis proof (elim decompose_Some_var_terms[where P = P, elim_format] conjE, goal_cases subst) case subst from subst(1)[OF subst(6)] subst(4,5) show ?case by (auto 0 3 simp: in_set_conv_nth list_eq_iff_nth_eq Ball_def) qed qed auto qed auto lemma unique_extends_subst: assumes extends: "extends_subst \ \" "extends_subst \ \" and dom: "dom \ = vars_term t \ dom \" "dom \ = vars_term t \ dom \" and eq: "t \ subst_of_map Var \ = t \ subst_of_map Var \" shows "\ = \" proof fix x consider (a) "x \ dom \" | (b) "x \ vars_term t" | (c) "x \ dom \" using assms by auto then show "\ x = \ x" proof cases case a then show ?thesis using extends unfolding extends_subst_def by auto next case b with eq show ?thesis proof (induct t) case (Var x) with trans[OF dom(1) dom(2)[symmetric]] show ?case by (auto simp: subst_of_map_def split: option.splits) qed auto next case c then have "\ x = None" "\ x = None" using dom by auto then show ?thesis by simp qed qed lemma subsumes_list_alt: "subsumes_list Ls Ks \ \ subsumes_list_modulo Ls Ks \" proof (induction Ls Ks \ rule: subsumes_list.induct[case_names Nil Cons]) case (Cons L Ls Ks \) show ?case unfolding subsumes_list_modulo_Cons subsumes_list.simps proof ((intro bex_cong[OF refl] ext iffI; elim exE conjE), goal_cases LR RL) case (LR K) show ?case by (insert LR; cases K; cases L; auto simp: Cons.IH split: option.splits dest!: match_term_list_sound) next case (RL K \) then show ?case proof (cases "match_term_list [(atm_of L, atm_of K)] \") case None with RL show ?thesis by (auto simp: Cons.IH dest!: match_term_list_complete) next case (Some \') with RL show ?thesis using unique_extends_subst[of \ \ \' "atm_of L"] by (auto simp: Cons.IH dest!: match_term_list_sound) qed qed qed (auto simp: subsumes_modulo_def subst_cls_def vars_clause_def intro: extends_subst_refl) lemma subsumes_subsumes_list[code_unfold]: "subsumes (mset Ls) (mset Ks) = subsumes_list Ls Ks Map.empty" unfolding subsumes_list_alt[of Ls Ks Map.empty] proof assume "subsumes (mset Ls) (mset Ks)" then obtain \ where "subst_cls (mset Ls) \ \# mset Ks" unfolding subsumes_def by blast moreover define \ where "\ = (\x. if x \ vars_clause (mset Ls) then Some (\ x) else None)" ultimately show "subsumes_list_modulo Ls Ks Map.empty" unfolding subsumes_modulo_def by (subst (asm) same_on_vars_clause[of _ \ "subst_of_map Var \"]) (auto intro!: exI[of _ \] simp: subst_of_map_def[abs_def] split: if_splits) qed (auto simp: subsumes_modulo_def subst_lit_def subsumes_def) lemma strictly_subsumes_subsumes_list[code_unfold]: "strictly_subsumes (mset Ls) (mset Ks) = (subsumes_list Ls Ks Map.empty \ \ subsumes_list Ks Ls Map.empty)" unfolding strictly_subsumes_def subsumes_subsumes_list by simp lemma subsumes_list_filterD: "subsumes_list Ls (filter P Ks) \ \ subsumes_list Ls Ks \" proof (induction Ls arbitrary: Ks \) case (Cons L Ls) from Cons.prems show ?case by (auto dest!: Cons.IH simp: filter_remove1[symmetric] split: option.splits) qed simp lemma subsumes_list_filterI: assumes match: "(\L K \ \. L \ set Ls \ match_term_list [(atm_of L, atm_of K)] \ = Some \ \ is_pos L = is_pos K \ P K)" shows "subsumes_list Ls Ks \ \ subsumes_list Ls (filter P Ks) \" using assms proof (induction Ls Ks \ rule: subsumes_list.induct[case_names Nil Cons]) case (Cons L Ls Ks \) from Cons.prems show ?case unfolding subsumes_list.simps set_filter bex_simps conj_assoc by (elim bexE conjE) (rule exI, rule conjI, assumption, auto split: option.splits simp: filter_remove1[symmetric] intro!: Cons.IH) qed simp lemma subsumes_list_Cons_filter_iff: assumes sorted_wrt: "sorted_wrt leq (L # Ls)" and trans: "transp leq" and match: "(\L K \ \. match_term_list [(atm_of L, atm_of K)] \ = Some \ \ is_pos L = is_pos K \ leq L K)" shows "subsumes_list (L # Ls) (filter (leq L) Ks) \ \ subsumes_list (L # Ls) Ks \" apply (rule iffI[OF subsumes_list_filterD subsumes_list_filterI]; assumption?) unfolding list.set insert_iff apply (elim disjE) subgoal by (auto split: option.splits elim!: match) subgoal for L K \ \ using sorted_wrt unfolding List.sorted_wrt.simps(2) apply (elim conjE) apply (drule bspec, assumption) apply (erule transpD[OF trans]) apply (erule match) by auto done definition leq_head :: "('f::linorder, 'v) term \ ('f, 'v) term \ bool" where "leq_head t u = (case (root t, root u) of (None, _) \ True | (_, None) \ False | (Some f, Some g) \ f \ g)" definition "leq_lit L K = (case (K, L) of (Neg _, Pos _) \ True | (Pos _, Neg _) \ False | _ \ leq_head (atm_of L) (atm_of K))" lemma transp_leq_lit[simp]: "transp leq_lit" unfolding transp_def leq_lit_def leq_head_def by (force split: option.splits literal.splits) lemma reflp_leq_lit[simp]: "reflp_on leq_lit A" unfolding reflp_on_def leq_lit_def leq_head_def by (auto split: option.splits literal.splits) lemma total_leq_lit[simp]: "total_on leq_lit A" unfolding total_on_def leq_lit_def leq_head_def by (auto split: option.splits literal.splits) lemma leq_head_subst[simp]: "leq_head t (t \ \)" by (induct t) (auto simp: leq_head_def) lemma leq_lit_match: fixes L K :: "('f :: linorder, 'v) term literal" shows "match_term_list [(atm_of L, atm_of K)] \ = Some \ \ is_pos L = is_pos K \ leq_lit L K" by (cases L; cases K) (auto simp: leq_lit_def dest!: match_term_list_sound split: option.splits) subsection \Optimized Implementation of Clause Subsumption\ fun subsumes_list_filter where "subsumes_list_filter [] Ks \ = True" | "subsumes_list_filter (L # Ls) Ks \ = (let Ks = filter (leq_lit L) Ks in (\K \ set Ks. is_pos K = is_pos L \ (case match_term_list [(atm_of L, atm_of K)] \ of None \ False | Some \ \ subsumes_list_filter Ls (remove1 K Ks) \)))" lemma sorted_wrt_subsumes_list_subsumes_list_filter: "sorted_wrt leq_lit Ls \ subsumes_list Ls Ks \ = subsumes_list_filter Ls Ks \" proof (induction Ls arbitrary: Ks \) case (Cons L Ls) from Cons.prems have "subsumes_list (L # Ls) Ks \ = subsumes_list (L # Ls) (filter (leq_lit L) Ks) \" by (intro subsumes_list_Cons_filter_iff[symmetric]) (auto dest: leq_lit_match) also have "subsumes_list (L # Ls) (filter (leq_lit L) Ks) \ = subsumes_list_filter (L # Ls) Ks \" using Cons.prems by (auto simp: Cons.IH split: option.splits) finally show ?case . qed simp subsection \Definition of Deterministic QuickSort\ text \ This is the functional description of the standard variant of deterministic QuickSort that always chooses the first list element as the pivot as given by Hoare in 1962. For a list that is already sorted, this leads to $n(n-1)$ comparisons, but as is well known, the average case is much better. The code below is adapted from Manuel Eberl's \Quick_Sort_Cost\ AFP entry, but without invoking probability theory and using a predicate instead of a set. \ fun quicksort :: "('a \ 'a \ bool) \ 'a list \ 'a list" where "quicksort _ [] = []" | "quicksort R (x # xs) = quicksort R (filter (\y. R y x) xs) @ [x] @ quicksort R (filter (\y. \ R y x) xs)" text \ We can easily show that this QuickSort is correct: \ theorem mset_quicksort [simp]: "mset (quicksort R xs) = mset xs" by (induction R xs rule: quicksort.induct) simp_all corollary set_quicksort [simp]: "set (quicksort R xs) = set xs" by (induction R xs rule: quicksort.induct) auto theorem sorted_wrt_quicksort: assumes "transp R" and "total_on R (set xs)" and "reflp_on R (set xs)" shows "sorted_wrt R (quicksort R xs)" using assms proof (induction R xs rule: quicksort.induct) case (2 R x xs) have total: "R a b" if "\ R b a" "a \ set (x#xs)" "b \ set (x#xs)" for a b using "2.prems" that unfolding total_on_def reflp_on_def by (cases "a = b") auto have "sorted_wrt R (quicksort R (filter (\y. R y x) xs))" "sorted_wrt R (quicksort R (filter (\y. \ R y x) xs))" using "2.prems" by (intro "2.IH"; auto simp: total_on_def reflp_on_def)+ then show ?case by (auto simp: sorted_wrt_append \transp R\ intro: transpD[OF \transp R\] dest!: total) qed auto text \ End of the material adapted from Eberl's \Quick_Sort_Cost\. \ lemma subsumes_list_subsumes_list_filter[abs_def, code_unfold]: "subsumes_list Ls Ks \ = subsumes_list_filter (quicksort leq_lit Ls) Ks \" by (rule trans[OF box_equals[OF _ subsumes_list_alt[symmetric] subsumes_list_alt[symmetric]] sorted_wrt_subsumes_list_subsumes_list_filter]) (auto simp: sorted_wrt_quicksort) end diff --git a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy --- a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy +++ b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy @@ -1,634 +1,634 @@ (* Title: Integration of IsaFoR Terms Author: Dmitriy Traytel , 2014 Author: Anders Schlichtkrull , 2017 Maintainer: Anders Schlichtkrull *) section \Integration of \textsf{IsaFoR} Terms\ text \ This theory implements the abstract interface for atoms and substitutions using -the \textsf{IsaFoR} library (part of the AFP entry \First_Order_Terms\). +the \textsf{IsaFoR} library. \ theory IsaFoR_Term imports Deriving.Derive Ordered_Resolution_Prover.Abstract_Substitution First_Order_Terms.Unification First_Order_Terms.Subsumption "HOL-Cardinals.Wellorder_Extension" Open_Induction.Restricted_Predicates begin hide_const (open) mgu abbreviation subst_apply_literal :: "('f, 'v) term literal \ ('f, 'v, 'w) gsubst \ ('f, 'w) term literal" (infixl "\lit" 60) where "L \lit \ \ map_literal (\A. A \ \) L" definition subst_apply_clause :: "('f, 'v) term clause \ ('f, 'v, 'w) gsubst \ ('f, 'w) term clause" (infixl "\cls" 60) where "C \cls \ = image_mset (\L. L \lit \) C" abbreviation vars_lit :: "('f, 'v) term literal \ 'v set" where "vars_lit L \ vars_term (atm_of L)" definition vars_clause :: "('f, 'v) term clause \ 'v set" where "vars_clause C = Union (set_mset (image_mset vars_lit C))" definition vars_clause_list :: "('f, 'v) term clause list \ 'v set" where "vars_clause_list Cs = Union (vars_clause ` set Cs) " definition vars_partitioned :: "('f,'v) term clause list \ bool" where "vars_partitioned Cs \ (\i < length Cs. \j < length Cs. i \ j \ (vars_clause (Cs ! i) \ vars_clause (Cs ! j)) = {})" lemma vars_clause_mono: "S \# C \ vars_clause S \ vars_clause C" unfolding vars_clause_def by auto interpretation substitution_ops "(\)" Var "(\\<^sub>s)" . lemma is_ground_atm_is_ground_on_var: assumes "is_ground_atm (A \ \)" and "v \ vars_term A" shows "is_ground_atm (\ v)" using assms proof (induction A) case (Var x) then show ?case by auto next case (Fun f ts) then show ?case unfolding is_ground_atm_def by auto qed lemma is_ground_lit_is_ground_on_var: assumes ground_lit: "is_ground_lit (subst_lit L \)" and v_in_L: "v \ vars_lit L" shows "is_ground_atm (\ v)" proof - let ?A = "atm_of L" from v_in_L have A_p: "v \ vars_term ?A" by auto then have "is_ground_atm (?A \ \)" using ground_lit unfolding is_ground_lit_def by auto then show ?thesis using A_p is_ground_atm_is_ground_on_var by metis qed lemma is_ground_cls_is_ground_on_var: assumes ground_clause: "is_ground_cls (subst_cls C \)" and v_in_C: "v \ vars_clause C" shows "is_ground_atm (\ v)" proof - from v_in_C obtain L where L_p: "L \# C" "v \ vars_lit L" unfolding vars_clause_def by auto then have "is_ground_lit (subst_lit L \)" using ground_clause unfolding is_ground_cls_def subst_cls_def by auto then show ?thesis using L_p is_ground_lit_is_ground_on_var by metis qed lemma is_ground_cls_list_is_ground_on_var: assumes ground_list: "is_ground_cls_list (subst_cls_list Cs \)" and v_in_Cs: "v \ vars_clause_list Cs" shows "is_ground_atm (\ v)" proof - from v_in_Cs obtain C where C_p: "C \ set Cs" "v \ vars_clause C" unfolding vars_clause_list_def by auto then have "is_ground_cls (subst_cls C \)" using ground_list unfolding is_ground_cls_list_def subst_cls_list_def by auto then show ?thesis using C_p is_ground_cls_is_ground_on_var by metis qed lemma same_on_vars_lit: assumes "\v \ vars_lit L. \ v = \ v" shows "subst_lit L \ = subst_lit L \" using assms proof (induction L) case (Pos x) then have "\v \ vars_term x. \ v = \ v \ subst_atm_abbrev x \ = subst_atm_abbrev x \" using term_subst_eq by metis+ then show ?case unfolding subst_lit_def using Pos by auto next case (Neg x) then have "\v \ vars_term x. \ v = \ v \ subst_atm_abbrev x \ = subst_atm_abbrev x \" using term_subst_eq by metis+ then show ?case unfolding subst_lit_def using Neg by auto qed lemma in_list_of_mset_in_S: assumes "i < length (list_of_mset S)" shows "list_of_mset S ! i \# S" proof - from assms have "list_of_mset S ! i \ set (list_of_mset S)" by auto then have "list_of_mset S ! i \# mset (list_of_mset S)" by (meson in_multiset_in_set) then show ?thesis by auto qed lemma same_on_vars_clause: assumes "\v \ vars_clause S. \ v = \ v" shows "subst_cls S \ = subst_cls S \" by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset subst_cls_def vars_clause_def) lemma vars_partitioned_var_disjoint: assumes "vars_partitioned Cs" shows "var_disjoint Cs" unfolding var_disjoint_def proof (intro allI impI) fix \s :: \('b \ ('a, 'b) term) list\ assume "length \s = length Cs" with assms[unfolded vars_partitioned_def] Fun_More.fun_merge[of "map vars_clause Cs" "nth \s"] obtain \ where \_p: "\i < length (map vars_clause Cs). \x \ map vars_clause Cs ! i. \ x = (\s ! i) x" by auto have "\i < length Cs. \S. S \# Cs ! i \ subst_cls S (\s ! i) = subst_cls S \" proof (rule, rule, rule, rule) fix i :: nat and S :: "('a, 'b) term literal multiset" assume "i < length Cs" and "S \# Cs ! i" then have "\v \ vars_clause S. (\s ! i) v = \ v" using vars_clause_mono[of S "Cs ! i"] \_p by auto then show "subst_cls S (\s ! i) = subst_cls S \" using same_on_vars_clause by auto qed then show "\\. \iS. S \# Cs ! i \ subst_cls S (\s ! i) = subst_cls S \" by auto qed lemma vars_in_instance_in_range_term: "vars_term (subst_atm_abbrev A \) \ Union (image vars_term (range \))" by (induction A) auto lemma vars_in_instance_in_range_lit: "vars_lit (subst_lit L \) \ Union (image vars_term (range \))" proof (induction L) case (Pos A) have "vars_term (A \ \) \ Union (image vars_term (range \))" using vars_in_instance_in_range_term[of A \] by blast then show ?case by auto next case (Neg A) have "vars_term (A \ \) \ Union (image vars_term (range \))" using vars_in_instance_in_range_term[of A \] by blast then show ?case by auto qed lemma vars_in_instance_in_range_cls: "vars_clause (subst_cls C \) \ Union (image vars_term (range \))" unfolding vars_clause_def subst_cls_def using vars_in_instance_in_range_lit[of _ \] by auto primrec renamings_apart :: "('f, nat) term clause list \ (('f, nat) subst) list" where "renamings_apart [] = []" | "renamings_apart (C # Cs) = (let \s = renamings_apart Cs in (\v. Var (v + Max (vars_clause_list (subst_cls_lists Cs \s) \ {0}) + 1)) # \s)" definition var_map_of_subst :: "('f, nat) subst \ nat \ nat" where "var_map_of_subst \ v = the_Var (\ v)" lemma len_renamings_apart: "length (renamings_apart Cs) = length Cs" by (induction Cs) (auto simp: Let_def) lemma renamings_apart_is_Var: "\\ \ set (renamings_apart Cs). \x. is_Var (\ x)" by (induction Cs) (auto simp: Let_def) lemma renamings_apart_inj: "\\ \ set (renamings_apart Cs). inj \" proof (induction Cs) case (Cons a Cs) then have "inj (\v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \ {0}))))" by (meson add_right_imp_eq injI nat.inject term.inject(1)) then show ?case using Cons by (auto simp: Let_def) qed auto lemma finite_vars_clause[simp]: "finite (vars_clause x)" unfolding vars_clause_def by auto lemma finite_vars_clause_list[simp]: "finite (vars_clause_list Cs)" unfolding vars_clause_list_def by (induction Cs) auto lemma Suc_Max_notin_set: "finite X \ Suc (v + Max (insert 0 X)) \ X" by (metis Max.boundedE Suc_n_not_le_n empty_iff finite.insertI le_add2 vimageE vimageI vimage_Suc_insert_0) lemma vars_partitioned_Nil[simp]: "vars_partitioned []" unfolding vars_partitioned_def by auto lemma subst_cls_lists_Nil[simp]: "subst_cls_lists Cs [] = []" unfolding subst_cls_lists_def by auto lemma vars_clause_hd_partitioned_from_tl: assumes "Cs \[]" shows "vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \ vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}" using assms proof (induction Cs) case (Cons C Cs) define \' :: "nat \ nat" where "\' = (\v. (Suc (v + Max ((vars_clause_list (subst_cls_lists Cs (renamings_apart Cs))) \ {0}))))" define \ :: "nat \ ('a, nat) term" where "\ = (\v. Var (\' v))" have "vars_clause (subst_cls C \) \ \ (vars_term ` range \)" using vars_in_instance_in_range_cls[of C "hd (renamings_apart (C # Cs))"] \_def \'_def by (auto simp: Let_def) moreover have "\ (vars_term ` range \) \ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}" proof - have "range \' \ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}" unfolding \'_def using Suc_Max_notin_set by auto then show ?thesis unfolding \_def \'_def by auto qed ultimately have "vars_clause (subst_cls C \) \ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}" by auto then show ?case unfolding \_def \'_def unfolding subst_cls_lists_def by (simp add: Let_def subst_cls_lists_def) qed auto lemma vars_partitioned_renamings_apart: "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))" proof (induction Cs) case (Cons C Cs) { fix i :: nat and j :: nat assume ij: "i < Suc (length Cs)" "j < i" have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" proof (cases i; cases j) fix j' :: nat assume i'j': "i = 0" "j = Suc j'" then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" using ij by auto next fix i' :: nat assume i'j': "i = Suc i'" "j = 0" have disjoin_C_Cs: "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \ vars_clause_list ((subst_cls_lists Cs (renamings_apart Cs))) = {}" using vars_clause_hd_partitioned_from_tl[of "C # Cs"] by (simp add: Let_def subst_cls_lists_def) { fix x assume asm: "x \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')" then have "(subst_cls_lists Cs (renamings_apart Cs) ! i') \ set (subst_cls_lists Cs (renamings_apart Cs))" using i'j' ij unfolding subst_cls_lists_def by (metis Suc_less_SucD length_map len_renamings_apart length_zip min_less_iff_conj nth_mem) moreover from asm have "x \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')" using i'j' ij unfolding subst_cls_lists_def by simp ultimately have "\D \ set (subst_cls_lists Cs (renamings_apart Cs)). x \ vars_clause D" by auto } then have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \ Union (set (map vars_clause ((subst_cls_lists Cs (renamings_apart Cs)))))" by auto then have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}" using disjoin_C_Cs unfolding vars_clause_list_def by auto moreover have "subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i" using i'j' ij unfolding subst_cls_lists_def by (simp add: Let_def) ultimately show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" using i'j' by (simp add: Int_commute) next fix i' :: nat and j' :: nat assume i'j': "i = Suc i'" "j = Suc j'" have "i' j'" using \i = Suc i'\ \j = Suc j'\ ij by blast ultimately have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}" using Cons unfolding vars_partitioned_def by auto then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}" unfolding i'j' by (simp add: subst_cls_lists_def Let_def) next assume \i = 0\ and \j = 0\ then show \vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \ vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}\ using ij by auto qed } then show ?case unfolding vars_partitioned_def by (metis (no_types, lifting) Int_commute Suc_lessI len_renamings_apart length_map length_nth_simps(2) length_zip min.idem nat.inject not_less_eq subst_cls_lists_def) qed auto interpretation substitution "(\)" "Var :: _ \ ('f, nat) term" "(\\<^sub>s)" renamings_apart "Fun undefined" proof (standard) show "\A. A \ Var = A" by auto next show "\A \ \. A \ \ \\<^sub>s \ = A \ \ \ \" by auto next show "\\ \. (\A. A \ \ = A \ \) \ \ = \" by (simp add: subst_term_eqI) next fix C :: "('f, nat) term clause" fix \ assume "is_ground_cls (subst_cls C \)" then have ground_atms_\: "\v. v \ vars_clause C \ is_ground_atm (\ v)" by (meson is_ground_cls_is_ground_on_var) define some_ground_trm :: "('f, nat) term" where "some_ground_trm = (Fun undefined [])" have ground_trm: "is_ground_atm some_ground_trm" unfolding is_ground_atm_def some_ground_trm_def by auto define \ where "\ = (\v. if v \ vars_clause C then \ v else some_ground_trm)" then have \_\: "\v \ vars_clause C. \ v = \ v" unfolding \_def by auto have all_ground_\: "is_ground_atm (\ v)" for v proof (cases "v \ vars_clause C") case True then show ?thesis using ground_atms_\ \_\ by auto next case False then show ?thesis unfolding \_def using ground_trm by auto qed have "is_ground_subst \" unfolding is_ground_subst_def proof fix A show "is_ground_atm (subst_atm_abbrev A \)" proof (induction A) case (Var v) then show ?case using all_ground_\ by auto next case (Fun f As) then show ?case using all_ground_\ by (simp add: is_ground_atm_def) qed qed moreover have "\v \ vars_clause C. \ v = \ v" using \_\ unfolding vars_clause_list_def by blast then have "subst_cls C \ = subst_cls C \" using same_on_vars_clause by auto ultimately show "\\. is_ground_subst \ \ subst_cls C \ = subst_cls C \" by auto next fix Cs :: "('f, nat) term clause list" show "length (renamings_apart Cs) = length Cs" using len_renamings_apart by auto next fix Cs :: "('f, nat) term clause list" fix \ :: "nat \ ('f, nat) Term.term" assume \_renaming: "\ \ set (renamings_apart Cs)" { have inj_is_renaming: "\\ :: ('f, nat) subst. (\x. is_Var (\ x)) \ inj \ \ is_renaming \" proof - fix \ :: "('f, nat) subst" fix x assume is_var_\: "\x. is_Var (\ x)" assume inj_\: "inj \" define \' where "\' = var_map_of_subst \" have \: "\ = Var \ \'" unfolding \'_def var_map_of_subst_def using is_var_\ by auto from is_var_\ inj_\ have "inj \'" unfolding is_renaming_def unfolding subst_domain_def inj_on_def \'_def var_map_of_subst_def by (metis term.collapse(1)) then have "inv \' \ \' = id" using inv_o_cancel[of \'] by simp then have "Var \ (inv \' \ \') = Var" by simp then have "\x. (Var \ (inv \' \ \')) x = Var x" by metis then have "\x. ((Var \ \') \\<^sub>s (Var \ (inv \'))) x = Var x" unfolding subst_compose_def by auto then have "\ \\<^sub>s (Var \ (inv \')) = Var" using \ by auto then show "is_renaming \" unfolding is_renaming_def by blast qed then have "\\ \ (set (renamings_apart Cs)). is_renaming \" using renamings_apart_is_Var renamings_apart_inj by blast } then show "is_renaming \" using \_renaming by auto next fix Cs :: "('f, nat) term clause list" have "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))" using vars_partitioned_renamings_apart by auto then show "var_disjoint (subst_cls_lists Cs (renamings_apart Cs))" using vars_partitioned_var_disjoint by auto next show "\\ As Bs. Fun undefined As \ \ = Fun undefined Bs \ map (\A. A \ \) As = Bs" by simp next show "wfP (strictly_generalizes_atm :: ('f, 'v) term \ _ \ _)" unfolding wfP_def by (rule wf_subset[OF wf_subsumes]) (auto simp: strictly_generalizes_atm_def generalizes_atm_def term_subsumable.subsumes_def subsumeseq_term.simps) qed fun pairs :: "'a list \ ('a \ 'a) list" where "pairs (x # y # xs) = (x, y) # pairs (y # xs)" | "pairs _ = []" derive compare "term" derive compare "literal" lemma class_linorder_compare: "class.linorder (le_of_comp compare) (lt_of_comp compare)" apply standard apply (simp_all add: lt_of_comp_def le_of_comp_def split: order.splits) apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5)) apply (metis comparator_compare comparator_def order.distinct(5)) apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5)) by (metis comparator.sym comparator_compare invert_order.simps(2) order.distinct(5)) context begin interpretation compare_linorder: linorder "le_of_comp compare" "lt_of_comp compare" by (rule class_linorder_compare) definition Pairs where "Pairs AAA = concat (compare_linorder.sorted_list_of_set ((pairs \ compare_linorder.sorted_list_of_set) ` AAA))" lemma unifies_all_pairs_iff: "(\p \ set (pairs xs). fst p \ \ = snd p \ \) \ (\a \ set xs. \b \ set xs. a \ \ = b \ \)" proof (induct xs rule: pairs.induct) case (1 x y xs) then show ?case unfolding pairs.simps list.set ball_Un ball_simps simp_thms fst_conv snd_conv by metis qed simp_all lemma in_pair_in_set: assumes "(A,B) \ set ((pairs As))" shows "A \ set As \ B \ set As" using assms proof (induction As) case (Cons A As) note Cons_outer = this show ?case proof (cases As) case Nil then show ?thesis using Cons_outer by auto next case (Cons B As') then show ?thesis using Cons_outer by auto qed qed auto lemma in_pairs_sorted_list_of_set_in_set: assumes "finite AAA" "\AA \ AAA. finite AA" "AB_pairs \ (pairs \ compare_linorder.sorted_list_of_set) ` AAA" and "(A :: _ :: compare, B) \ set AB_pairs" shows "\AA. AA \ AAA \ A \ AA \ B \ AA" proof - from assms have "AB_pairs \ (pairs \ compare_linorder.sorted_list_of_set) ` AAA" by auto then obtain AA where AA_p: "AA \ AAA \ (pairs \ compare_linorder.sorted_list_of_set) AA = AB_pairs" by auto have "(A, B) \ set (pairs (compare_linorder.sorted_list_of_set AA))" using AA_p[] assms(4) by auto then have "A \ set (compare_linorder.sorted_list_of_set AA)" and "B \ set (compare_linorder.sorted_list_of_set AA)" using in_pair_in_set[of A] by auto then show ?thesis using assms(2) AA_p by auto qed lemma unifiers_Pairs: assumes "finite AAA" and "\AA \ AAA. finite AA" shows "unifiers (set (Pairs AAA)) = {\. is_unifiers \ AAA}" proof (rule; rule) fix \ :: "('a, 'b) subst" assume asm: "\ \ unifiers (set (Pairs AAA))" have "\AA. AA \ AAA \ card (AA \\<^sub>s\<^sub>e\<^sub>t \) \ Suc 0" proof - fix AA :: "('a, 'b) term set" assume asm': "AA \ AAA" then have "\p \ set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \ = subst_atm_abbrev (snd p) \" using assms asm unfolding Pairs_def by auto then have "\A \ AA. \B \ AA. subst_atm_abbrev A \ = subst_atm_abbrev B \" using assms asm' unfolding unifies_all_pairs_iff using compare_linorder.sorted_list_of_set by blast then show "card (AA \\<^sub>s\<^sub>e\<^sub>t \) \ Suc 0" by (smt imageE card.empty card_Suc_eq card_mono finite.intros(1) finite_insert le_SucI singletonI subsetI) qed then show "\ \ {\. is_unifiers \ AAA}" using assms by (auto simp: is_unifiers_def is_unifier_def subst_atms_def) next fix \ :: "('a, 'b) subst" assume asm: "\ \ {\. is_unifiers \ AAA}" { fix AB_pairs A B assume "AB_pairs \ set (compare_linorder.sorted_list_of_set ((pairs \ compare_linorder.sorted_list_of_set) ` AAA))" and "(A, B) \ set AB_pairs" then have "\AA. AA \ AAA \ A \ AA \ B \ AA" using assms by (simp add: in_pairs_sorted_list_of_set_in_set) then obtain AA where a: "AA \ AAA" "A \ AA" "B \ AA" by blast from a assms asm have card_AA_\: "card (AA \\<^sub>s\<^sub>e\<^sub>t \) \ Suc 0" unfolding is_unifiers_def is_unifier_def subst_atms_def by auto have "subst_atm_abbrev A \ = subst_atm_abbrev B \" proof (cases "card (AA \\<^sub>s\<^sub>e\<^sub>t \) = Suc 0") case True moreover have "subst_atm_abbrev A \ \ AA \\<^sub>s\<^sub>e\<^sub>t \" using a assms asm card_AA_\ by auto moreover have "subst_atm_abbrev B \ \ AA \\<^sub>s\<^sub>e\<^sub>t \" using a assms asm card_AA_\ by auto ultimately show ?thesis using a assms asm card_AA_\ by (metis (no_types, lifting) card_Suc_eq singletonD) next case False then have "card (AA \\<^sub>s\<^sub>e\<^sub>t \) = 0" using a assms asm card_AA_\ by arith then show ?thesis using a assms asm card_AA_\ by auto qed } then show "\ \ unifiers (set (Pairs AAA))" unfolding Pairs_def unifiers_def by auto qed end definition "mgu_sets AAA = map_option subst_of (unify (Pairs AAA) [])" interpretation mgu "(\)" "Var :: _ \ ('f :: compare, nat) term" "(\\<^sub>s)" "Fun undefined" renamings_apart mgu_sets proof fix AAA :: "('a :: compare, nat) term set set" and \ :: "('a, nat) subst" assume fin: "finite AAA" "\AA \ AAA. finite AA" and "mgu_sets AAA = Some \" then have "is_imgu \ (set (Pairs AAA))" using unify_sound unfolding mgu_sets_def by blast then show "is_mgu \ AAA" unfolding is_imgu_def is_mgu_def unifiers_Pairs[OF fin] by auto next fix AAA :: "('a :: compare, nat) term set set" and \ :: "('a, nat) subst" assume fin: "finite AAA" "\AA \ AAA. finite AA" and "is_unifiers \ AAA" then have "\ \ unifiers (set (Pairs AAA))" unfolding is_mgu_def unifiers_Pairs[OF fin] by auto then show "\\. mgu_sets AAA = Some \" using unify_complete unfolding mgu_sets_def by blast qed derive linorder prod derive linorder list end diff --git a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term_KBO.thy b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term_KBO.thy new file mode 100644 --- /dev/null +++ b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term_KBO.thy @@ -0,0 +1,161 @@ +(* Title: A Well-Order on Terms that Extends IsaFoR's KBO + Author: Dmitriy Traytel , 2014 + Author: Anders Schlichtkrull , 2017 + Maintainer: Anders Schlichtkrull +*) + +section \A Well-Order on Terms that Extends \textsf{IsaFoR}'s KBO\ + +text \ +This theory extends and integrates and the Knuth--Bendix order defined in the +\textsf{IsaFoR} library. +\ + +theory IsaFoR_Term_KBO +imports + IsaFoR_Term + Knuth_Bendix_Order.KBO +begin + +record 'f weights = + w :: "'f \ nat \ nat" + w0 :: nat + pr_strict :: "'f \ nat \ 'f \ nat \ bool" + least :: "'f \ bool" + scf :: "'f \ nat \ nat \ nat" + +class weighted = + fixes weights :: "'a weights" + assumes weights_adm: + "admissible_kbo + (w weights) (w0 weights) (pr_strict weights) ((pr_strict weights)\<^sup>=\<^sup>=) (least weights) (scf weights)" + and pr_strict_total: "fi = gj \ pr_strict weights fi gj \ pr_strict weights gj fi" + and pr_strict_asymp: "asymp (pr_strict weights)" + and scf_ok: "i < n \ scf weights (f, n) i \ 1" + +instantiation unit :: weighted begin + +definition weights_unit :: "unit weights" where "weights_unit = + \w = Suc \ snd, w0 = 1, pr_strict = \(_, n) (_, m). n > m, least = \_. True, scf = \_ _. 1\" + +instance + by (intro_classes, unfold_locales) (auto simp: weights_unit_def SN_iff_wf asymp.simps irreflp_def + intro!: wf_subset[OF wf_inv_image[OF wf], of _ snd]) +end + +global_interpretation KBO: + admissible_kbo + "w (weights :: 'f :: weighted weights)" "w0 (weights :: 'f :: weighted weights)" + "pr_strict weights" "((pr_strict weights)\<^sup>=\<^sup>=)" "least weights" "scf weights" + defines weight = KBO.weight + and kbo = KBO.kbo + by (simp add: weights_adm) + +lemma kbo_code[code]: "kbo s t = + (let wt = weight t; ws = weight s in + if vars_term_ms (KBO.SCF t) \# vars_term_ms (KBO.SCF s) \ wt \ ws + then + (if wt < ws then (True, True) + else + (case s of + Var y \ (False, case t of Var x \ True | Fun g ts \ ts = [] \ least weights g) + | Fun f ss \ + (case t of + Var x \ (True, True) + | Fun g ts \ + if pr_strict weights (f, length ss) (g, length ts) then (True, True) + else if (f, length ss) = (g, length ts) then lex_ext_unbounded kbo ss ts + else (False, False)))) + else (False, False))" + by (subst KBO.kbo.simps) (auto simp: Let_def split: term.splits) + +definition "less_kbo s t = fst (kbo t s)" + +lemma less_kbo_gtotal: "ground s \ ground t \ s = t \ less_kbo s t \ less_kbo t s" + unfolding less_kbo_def using KBO.S_ground_total by (metis pr_strict_total subset_UNIV) + +lemma less_kbo_subst: + fixes \ :: "('f :: weighted, 'v) subst" + shows "less_kbo s t \ less_kbo (s \ \) (t \ \)" + unfolding less_kbo_def by (rule KBO.S_subst) + +lemma wfP_less_kbo: "wfP less_kbo" +proof - + have "SN {(x, y). fst (kbo x y)}" + using pr_strict_asymp by (fastforce simp: asymp.simps irreflp_def intro!: KBO.S_SN scf_ok) + then show ?thesis + unfolding SN_iff_wf wfP_def by (rule wf_subset) (auto simp: less_kbo_def) +qed + +instantiation "term" :: (weighted, type) linorder begin + +definition "leq_term = (SOME leq. {(s,t). less_kbo s t} \ leq \ Well_order leq \ Field leq = UNIV)" + +lemma less_trm_extension: "{(s,t). less_kbo s t} \ leq_term" + unfolding leq_term_def + by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto + +lemma less_trm_well_order: "well_order leq_term" + unfolding leq_term_def + by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto + +definition less_eq_term :: "('a :: weighted, 'b) term \ _ \ bool" where + "less_eq_term = in_rel leq_term" +definition less_term :: "('a :: weighted, 'b) term \ _ \ bool" where + "less_term s t = strict (\) s t" + +lemma leq_term_minus_Id: "leq_term - Id = {(x,y). x < y}" + using less_trm_well_order + unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def less_term_def less_eq_term_def + by auto + +lemma less_term_alt: "(<) = in_rel (leq_term - Id)" + by (simp add: in_rel_Collect_case_prod_eq leq_term_minus_Id) + +instance +proof (standard, goal_cases less_less_eq refl trans antisym total) + case (less_less_eq x y) + then show ?case unfolding less_term_def .. +next +case (refl x) + then show ?case using less_trm_well_order + unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def + less_eq_term_def by auto +next +case (trans x y z) + then show ?case using less_trm_well_order + unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def trans_def + less_eq_term_def by auto +next + case (antisym x y) + then show ?case using less_trm_well_order + unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def + less_eq_term_def by auto +next + case (total x y) + then show ?case using less_trm_well_order + unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def + Relation.total_on_def less_eq_term_def by (cases "x = y") auto +qed + +end + +instantiation "term" :: (weighted, type) wellorder begin +instance + using less_trm_well_order[unfolded well_order_on_def wf_def leq_term_minus_Id, THEN conjunct2] + by intro_classes (atomize, auto) +end + +lemma ground_less_less_kbo: "ground s \ ground t \ s < t \ less_kbo s t" + using less_kbo_gtotal[of s t] less_trm_extension + by (auto simp: less_term_def less_eq_term_def) + +lemma less_kbo_less: "less_kbo s t \ s < t" + using less_trm_extension + by (auto simp: less_term_alt less_kbo_def KBO.S_irrefl) + +lemma is_ground_atm_ground: "is_ground_atm t \ ground t" + unfolding is_ground_atm_def + by (induct t) (fastforce simp: in_set_conv_nth list_eq_iff_nth_eq)+ + +end diff --git a/thys/Functional_Ordered_Resolution_Prover/ROOT b/thys/Functional_Ordered_Resolution_Prover/ROOT --- a/thys/Functional_Ordered_Resolution_Prover/ROOT +++ b/thys/Functional_Ordered_Resolution_Prover/ROOT @@ -1,17 +1,15 @@ chapter AFP -session Functional_Ordered_Resolution_Prover (AFP) = "HOL-Library" + +session Functional_Ordered_Resolution_Prover (AFP) = Ordered_Resolution_Prover + options [timeout = 600] sessions First_Order_Terms + Knuth_Bendix_Order Lambda_Free_RPOs Nested_Multisets_Ordinals Open_Induction - Ordered_Resolution_Prover Polynomial_Factorization theories - Deterministic_FO_Ordered_Resolution_Prover - IsaFoR_Term - Executable_Subsumption + Executable_FO_Ordered_Resolution_Prover document_files "root.tex" diff --git a/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy b/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy --- a/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy +++ b/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy @@ -1,836 +1,833 @@ (* Title: A Fair Ordered Resolution Prover for First-Order Clauses with Weights Author: Anders Schlichtkrull , 2017 Author: Jasmin Blanchette , 2017 Maintainer: Anders Schlichtkrull *) section \A Fair Ordered Resolution Prover for First-Order Clauses with Weights\ text \ The \weighted_RP\ prover introduced below operates on finite multisets of clauses and organizes the multiset of processed clauses as a priority queue to ensure that inferences are performed in a fair manner, to guarantee completeness. \ theory Weighted_FO_Ordered_Resolution_Prover imports Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover begin - -subsection \Prover\ - type_synonym 'a wclause = "'a clause \ nat" type_synonym 'a wstate = "'a wclause multiset \ 'a wclause multiset \ 'a wclause multiset \ nat" fun state_of_wstate :: "'a wstate \ 'a state" where "state_of_wstate (N, P, Q, n) = (set_mset (image_mset fst N), set_mset (image_mset fst P), set_mset (image_mset fst Q))" locale weighted_FO_resolution_prover = FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm for S :: "('a :: wellorder) clause \ 'a clause" and subst_atm :: "'a \ 's \ 'a" and id_subst :: "'s" and comp_subst :: "'s \ 's \ 's" and renamings_apart :: "'a clause list \ 's list" and atm_of_atms :: "'a list \ 'a" and mgu :: "'a set set \ 's option" and less_atm :: "'a \ 'a \ bool" + fixes weight :: "'a clause \ nat \ nat" assumes weight_mono: "i < j \ weight (C, i) < weight (C, j)" begin abbreviation clss_of_wstate :: "'a wstate \ 'a clause set" where "clss_of_wstate St \ clss_of_state (state_of_wstate St)" abbreviation N_of_wstate :: "'a wstate \ 'a clause set" where "N_of_wstate St \ N_of_state (state_of_wstate St)" abbreviation P_of_wstate :: "'a wstate \ 'a clause set" where "P_of_wstate St \ P_of_state (state_of_wstate St)" abbreviation Q_of_wstate :: "'a wstate \ 'a clause set" where "Q_of_wstate St \ Q_of_state (state_of_wstate St)" fun wN_of_wstate :: "'a wstate \ 'a wclause multiset" where "wN_of_wstate (N, P, Q, n) = N" fun wP_of_wstate :: "'a wstate \ 'a wclause multiset" where "wP_of_wstate (N, P, Q, n) = P" fun wQ_of_wstate :: "'a wstate \ 'a wclause multiset" where "wQ_of_wstate (N, P, Q, n) = Q" fun n_of_wstate :: "'a wstate \ nat" where "n_of_wstate (N, P, Q, n) = n" lemma of_wstate_split[simp]: "(wN_of_wstate St, wP_of_wstate St, wQ_of_wstate St, n_of_wstate St) = St" by (cases St) auto abbreviation grounding_of_wstate :: "'a wstate \ 'a clause set" where "grounding_of_wstate St \ grounding_of_state (state_of_wstate St)" abbreviation Liminf_wstate :: "'a wstate llist \ 'a state" where "Liminf_wstate Sts \ Liminf_state (lmap state_of_wstate Sts)" lemma timestamp_le_weight: "n \ weight (C, n)" by (induct n, simp, metis weight_mono[of k "Suc k" for k] Suc_le_eq le_less le_trans) inductive weighted_RP :: "'a wstate \ 'a wstate \ bool" (infix "\\<^sub>w" 50) where tautology_deletion: "Neg A \# C \ Pos A \# C \ (N + {#(C, i)#}, P, Q, n) \\<^sub>w (N, P, Q, n)" | forward_subsumption: "D \# image_mset fst (P + Q) \ subsumes D C \ (N + {#(C, i)#}, P, Q, n) \\<^sub>w (N, P, Q, n)" | backward_subsumption_P: "D \# image_mset fst N \ C \# image_mset fst P \ strictly_subsumes D C \ (N, P, Q, n) \\<^sub>w (N, {#(E, k) \# P. E \ C#}, Q, n)" | backward_subsumption_Q: "D \# image_mset fst N \ strictly_subsumes D C \ (N, P, Q + {#(C, i)#}, n) \\<^sub>w (N, P, Q, n)" | forward_reduction: "D + {#L'#} \# image_mset fst (P + Q) \ - L = L' \l \ \ D \ \ \# C \ (N + {#(C + {#L#}, i)#}, P, Q, n) \\<^sub>w (N + {#(C, i)#}, P, Q, n)" | backward_reduction_P: "D + {#L'#} \# image_mset fst N \ - L = L' \l \ \ D \ \ \# C \ (\j. (C + {#L#}, j) \# P \ j \ i) \ (N, P + {#(C + {#L#}, i)#}, Q, n) \\<^sub>w (N, P + {#(C, i)#}, Q, n)" | backward_reduction_Q: "D + {#L'#} \# image_mset fst N \ - L = L' \l \ \ D \ \ \# C \ (N, P, Q + {#(C + {#L#}, i)#}, n) \\<^sub>w (N, P + {#(C, i)#}, Q, n)" | clause_processing: "(N + {#(C, i)#}, P, Q, n) \\<^sub>w (N, P + {#(C, i)#}, Q, n)" | inference_computation: "(\(D, j) \# P. weight (C, i) \ weight (D, j)) \ N = mset_set ((\D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\ S) (set_mset (image_mset fst Q)) C)) \ ({#}, P + {#(C, i)#}, Q, n) \\<^sub>w (N, {#(D, j) \# P. D \ C#}, Q + {#(C, i)#}, Suc n)" lemma weighted_RP_imp_RP: "St \\<^sub>w St' \ state_of_wstate St \ state_of_wstate St'" proof (induction rule: weighted_RP.induct) case (backward_subsumption_P D N C P Q n) show ?case by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\)", OF _ _ RP.backward_subsumption_P[of D "fst ` set_mset N" C "fst ` set_mset P - {C}" "fst ` set_mset Q"]]) (use backward_subsumption_P in auto) next case (inference_computation P C i N n Q) show ?case by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\)", OF _ _ RP.inference_computation[of "fst ` set_mset N" "fst ` set_mset Q" C "fst ` set_mset P - {C}"]], use inference_computation(2) finite_ord_FO_resolution_inferences_between in \auto simp: comp_def image_comp inference_system.inferences_between_def\) qed (use RP.intros in simp_all) lemma final_weighted_RP: "\ ({#}, {#}, Q, n) \\<^sub>w St" by (auto elim: weighted_RP.cases) context fixes Sts :: "'a wstate llist" assumes full_deriv: "full_chain (\\<^sub>w) Sts" and empty_P0: "P_of_wstate (lhd Sts) = {}" and empty_Q0: "Q_of_wstate (lhd Sts) = {}" begin lemma finite_Sts0: "finite (clss_of_wstate (lhd Sts))" by (cases "lhd Sts") auto lemmas deriv = full_chain_imp_chain[OF full_deriv] lemmas lhd_lmap_Sts = llist.map_sel(1)[OF chain_not_lnull[OF deriv]] lemma deriv_RP: "chain (\) (lmap state_of_wstate Sts)" using deriv weighted_RP_imp_RP by (metis chain_lmap) lemma finite_Sts0_RP: "finite (clss_of_state (lhd (lmap state_of_wstate Sts)))" using finite_Sts0 chain_length_pos[OF deriv] by auto lemma empty_P0_RP: "P_of_state (lhd (lmap state_of_wstate Sts)) = {}" using empty_P0 chain_length_pos[OF deriv] by auto lemma empty_Q0_RP: "Q_of_state (lhd (lmap state_of_wstate Sts)) = {}" using empty_Q0 chain_length_pos[OF deriv] by auto lemmas Sts_thms = deriv_RP finite_Sts0_RP empty_P0_RP empty_Q0_RP theorem weighted_RP_model: "St \\<^sub>w St' \ I \s grounding_of_wstate St' \ I \s grounding_of_wstate St" using RP_model Sts_thms weighted_RP_imp_RP by (simp only: comp_def) abbreviation S_gQ :: "'a clause \ 'a clause" where "S_gQ \ S_Q (lmap state_of_wstate Sts)" interpretation sq: selection S_gQ unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms by unfold_locales auto interpretation gd: ground_resolution_with_selection S_gQ by unfold_locales interpretation src: standard_redundancy_criterion_reductive gd.ord_\ by unfold_locales interpretation src: standard_redundancy_criterion_counterex_reducing gd.ord_\ "ground_resolution_with_selection.INTERP S_gQ" by unfold_locales lemmas ord_\_saturated_upto_def = src.saturated_upto_def lemmas ord_\_saturated_upto_complete = src.saturated_upto_complete lemmas ord_\_contradiction_Rf = src.contradiction_Rf theorem weighted_RP_sound: assumes "{#} \ clss_of_state (Liminf_wstate Sts)" shows "\ satisfiable (grounding_of_wstate (lhd Sts))" by (rule RP_sound[OF deriv_RP assms, unfolded lhd_lmap_Sts]) abbreviation RP_filtered_measure :: "('a wclause \ bool) \ 'a wstate \ nat \ nat \ nat" where "RP_filtered_measure \ \p (N, P, Q, n). (sum_mset (image_mset (\(C, i). Suc (size C)) {#Di \# N + P + Q. p Di#}), size {#Di \# N. p Di#}, size {#Di \# P. p Di#})" abbreviation RP_combined_measure :: "nat \ 'a wstate \ nat \ (nat \ nat \ nat) \ (nat \ nat \ nat)" where "RP_combined_measure \ \w St. (w + 1 - n_of_wstate St, RP_filtered_measure (\(C, i). i \ w) St, RP_filtered_measure (\Ci. True) St)" abbreviation (input) RP_filtered_relation :: "((nat \ nat \ nat) \ (nat \ nat \ nat)) set" where "RP_filtered_relation \ natLess <*lex*> natLess <*lex*> natLess" abbreviation (input) RP_combined_relation :: "((nat \ ((nat \ nat \ nat) \ (nat \ nat \ nat))) \ (nat \ ((nat \ nat \ nat) \ (nat \ nat \ nat)))) set" where "RP_combined_relation \ natLess <*lex*> RP_filtered_relation <*lex*> RP_filtered_relation" abbreviation "(fst3 :: 'b * 'c * 'd \ 'b) \ fst" abbreviation "(snd3 :: 'b * 'c * 'd \ 'c) \ \x. fst (snd x)" abbreviation "(trd3 :: 'b * 'c * 'd \ 'd) \ \x. snd (snd x)" lemma wf_RP_filtered_relation: "wf RP_filtered_relation" and wf_RP_combined_relation: "wf RP_combined_relation" unfolding natLess_def using wf_less wf_mult by auto lemma multiset_sum_of_Suc_f_monotone: "N \# M \ (\x \# N. Suc (f x)) < (\x \# M. Suc (f x))" proof (induction N arbitrary: M) case empty then obtain y where "y \# M" by force then have "(\x \# M. 1) = (\x \# M - {#y#} + {#y#}. 1)" by auto also have "... = (\x \# M - {#y#}. 1) + (\x \# {#y#}. 1)" by (metis image_mset_union sum_mset.union) also have "... > (0 :: nat)" by auto finally have "0 < (\x \# M. Suc (f x))" by (fastforce intro: gr_zeroI) then show ?case using empty by auto next case (add x N) from this(2) have "(\y \# N. Suc (f y)) < (\y \# M - {#x#}. Suc (f y))" using add(1)[of "M - {#x#}"] by (simp add: insert_union_subset_iff) moreover have "add_mset x (remove1_mset x M) = M" by (meson add.prems add_mset_remove_trivial_If mset_subset_insertD) ultimately show ?case by (metis (no_types) add.commute add_less_cancel_right sum_mset.insert) qed lemma multiset_sum_monotone_f': assumes "CC \# DD" shows "(\(C, i) \# CC. Suc (f C)) < (\(C, i) \# DD. Suc (f C))" using multiset_sum_of_Suc_f_monotone[OF assms, of "f \ fst"] by (metis (mono_tags) comp_apply image_mset_cong2 split_beta) lemma filter_mset_strict_subset: assumes "x \# M" and "\ p x" shows "{#y \# M. p y#} \# M" proof - have subseteq: "{#E \# M. p E#} \# M" by auto have "count {#E \# M. p E#} x = 0" using assms by auto moreover have "0 < count M x" using assms by auto ultimately have lt_count: "count {#y \# M. p y#} x < count M x" by auto then show ?thesis using subseteq by (metis less_not_refl2 subset_mset.le_neq_trans) qed lemma weighted_RP_measure_decreasing_N: assumes "St \\<^sub>w St'" and "(C, l) \# wN_of_wstate St" shows "(RP_filtered_measure (\Ci. True) St', RP_filtered_measure (\Ci. True) St) \ RP_filtered_relation" using assms proof (induction rule: weighted_RP.induct) case (backward_subsumption_P D N C' P Q n) then obtain i' where "(C', i') \# P" by auto then have "{#(E, k) \# P. E \ C'#} \# P" using filter_mset_strict_subset[of "(C', i')" P "\X. \fst X = C'"] by (metis (mono_tags, lifting) filter_mset_cong fst_conv prod.case_eq_if) then have "(\(C, i) \# {#(E, k) \# P. E \ C'#}. Suc (size C)) < (\(C, i) \# P. Suc (size C))" using multiset_sum_monotone_f'[of "{#(E, k) \# P. E \ C'#}" P size] by metis then show ?case unfolding natLess_def by auto qed (auto simp: natLess_def) lemma weighted_RP_measure_decreasing_P: assumes "St \\<^sub>w St'" and "(C, i) \# wP_of_wstate St" shows "(RP_combined_measure (weight (C, i)) St', RP_combined_measure (weight (C, i)) St) \ RP_combined_relation" using assms proof (induction rule: weighted_RP.induct) case (backward_subsumption_P D N C' P Q n) define St where "St = (N, P, Q, n)" define P' where "P' = {#(E, k) \# P. E \ C'#}" define St' where "St' = (N, P', Q, n)" from backward_subsumption_P obtain i' where "(C', i') \# P" by auto then have P'_sub_P: "P' \# P" unfolding P'_def using filter_mset_strict_subset[of "(C', i')" P "\Dj. fst Dj \ C'"] by (metis (no_types, lifting) filter_mset_cong fst_conv prod.case_eq_if) have P'_subeq_P_filter: "{#(Ca, ia) \# P'. ia \ weight (C, i)#} \# {#(Ca, ia) \# P. ia \ weight (C, i)#}" using P'_sub_P by (auto intro: multiset_filter_mono) have "fst3 (RP_combined_measure (weight (C, i)) St') \ fst3 (RP_combined_measure (weight (C, i)) St)" unfolding St'_def St_def by auto moreover have "(\(C, i) \# {#(Ca, ia) \# P'. ia \ weight (C, i)#}. Suc (size C)) \ (\x \# {#(Ca, ia) \# P. ia \ weight (C, i)#}. case x of (C, i) \ Suc (size C))" using P'_subeq_P_filter by (rule sum_image_mset_mono) then have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St')) \ fst3 (snd3 (RP_combined_measure (weight (C, i)) St))" unfolding St'_def St_def by auto moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St')) \ snd3 (snd3 (RP_combined_measure (weight (C, i)) St))" unfolding St'_def St_def by auto moreover from P'_subeq_P_filter have "size {#(Ca, ia) \# P'. ia \ weight (C, i)#} \ size {#(Ca, ia) \# P. ia \ weight (C, i)#}" by (simp add: size_mset_mono) then have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St')) \ trd3 (snd3 (RP_combined_measure (weight (C, i)) St))" unfolding St'_def St_def unfolding fst_def snd_def by auto moreover from P'_sub_P have "(\(C, i) \# P'. Suc (size C)) < (\(C, i) \# P. Suc (size C))" using multiset_sum_monotone_f'[of "{#(E, k) \# P. E \ C'#}" P size] unfolding P'_def by metis then have "fst3 (trd3 (RP_combined_measure (weight (C, i)) St')) < fst3 (trd3 (RP_combined_measure (weight (C, i)) St))" unfolding P'_def St'_def St_def by auto ultimately show ?case unfolding natLess_def P'_def St'_def St_def by auto next case (inference_computation P C' i' N n Q) then show ?case proof (cases "n \ weight (C, i)") case True then have "weight (C, i) + 1 - n > weight (C, i) + 1 - Suc n" by auto then show ?thesis unfolding natLess_def by auto next case n_nle_w: False define St :: "'a wstate" where "St = ({#}, P + {#(C', i')#}, Q, n)" define St' :: "'a wstate" where "St' = (N, {#(D, j) \# P. D \ C'#}, Q + {#(C', i')#}, Suc n)" define concls :: "'a wclause set" where "concls = (\D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\ S) (fst ` set_mset Q) C')" have fin: "finite concls" unfolding concls_def using finite_ord_FO_resolution_inferences_between by auto have "{(D, ia) \ concls. ia \ weight (C, i)} = {}" unfolding concls_def using n_nle_w by auto then have "{#(D, ia) \# mset_set concls. ia \ weight (C, i)#} = {#}" using fin filter_mset_empty_if_finite_and_filter_set_empty[of concls] by auto then have n_low_weight_empty: "{#(D, ia) \# N. ia \ weight (C, i)#} = {#}" unfolding inference_computation unfolding concls_def by auto have "weight (C', i') \ weight (C, i)" using inference_computation by auto then have i'_le_w_Ci: "i' \ weight (C, i)" using timestamp_le_weight[of i' C'] by auto have subs: "{#(D, ia) \# N + {#(D, j) \# P. D \ C'#} + (Q + {#(C', i')#}). ia \ weight (C, i)#} \# {#(D, ia) \# {#} + (P + {#(C', i')#}) + Q. ia \ weight (C, i)#}" using n_low_weight_empty by (auto simp: multiset_filter_mono) have "fst3 (RP_combined_measure (weight (C, i)) St') \ fst3 (RP_combined_measure (weight (C, i)) St)" unfolding St'_def St_def by auto moreover have "fst (RP_filtered_measure ((\(D, ia). ia \ weight (C, i))) St') = (\(C, i) \# {#(D, ia) \# N + {#(D, j) \# P. D \ C'#} + (Q + {#(C', i')#}). ia \ weight (C, i)#}. Suc (size C))" unfolding St'_def by auto also have "... \ (\(C, i) \# {#(D, ia) \# {#} + (P + {#(C', i')#}) + Q. ia \ weight (C, i)#}. Suc (size C))" using subs sum_image_mset_mono by blast also have "... = fst (RP_filtered_measure (\(D, ia). ia \ weight (C, i)) St)" unfolding St_def by auto finally have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St')) \ fst3 (snd3 (RP_combined_measure (weight (C, i)) St))" by auto moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St')) = snd3 (snd3 (RP_combined_measure (weight (C, i)) St))" unfolding St_def St'_def using n_low_weight_empty by auto moreover have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St')) < trd3 (snd3 (RP_combined_measure (weight (C, i)) St))" unfolding St_def St'_def using i'_le_w_Ci by (simp add: le_imp_less_Suc multiset_filter_mono size_mset_mono) ultimately show ?thesis unfolding natLess_def St'_def St_def lex_prod_def by force qed qed (auto simp: natLess_def) lemma preserve_min_or_delete_completely: assumes "St \\<^sub>w St'" "(C, i) \# wP_of_wstate St" "\k. (C, k) \# wP_of_wstate St \ i \ k" shows "(C, i) \# wP_of_wstate St' \ (\j. (C, j) \# wP_of_wstate St')" using assms proof (induction rule: weighted_RP.induct) case (backward_reduction_P D L' N L \ C' P i' Q n) show ?case proof (cases "C = C' + {#L#}") case True_outer: True then have C_i_in: "(C, i) \# P + {#(C, i')#}" using backward_reduction_P by auto then have max: "\k. (C, k) \# P + {#(C, i')#} \ k \ i'" using backward_reduction_P unfolding True_outer[symmetric] by auto then have "count (P + {#(C, i')#}) (C, i') \ 1" by auto moreover { assume asm: "count (P + {#(C, i')#}) (C, i') = 1" then have nin_P: "(C, i') \# P" using not_in_iff by force have ?thesis proof (cases "(C, i) = (C, i')") case True then have "i = i'" by auto then have "\j. (C, j) \# P + {#(C, i')#} \ j = i'" using max backward_reduction_P(6) unfolding True_outer[symmetric] by force then show ?thesis using True_outer[symmetric] nin_P by auto next case False then show ?thesis using C_i_in by auto qed } moreover { assume "count (P + {#(C, i')#}) (C, i') > 1" then have ?thesis using C_i_in by auto } ultimately show ?thesis by (cases "count (P + {#(C, i')#}) (C, i') = 1") auto next case False then show ?thesis using backward_reduction_P by auto qed qed auto lemma preserve_min_P: assumes "St \\<^sub>w St'" "(C, j) \# wP_of_wstate St'" and "(C, i) \# wP_of_wstate St" and "\k. (C, k) \# wP_of_wstate St \ i \ k" shows "(C, i) \# wP_of_wstate St'" using assms preserve_min_or_delete_completely by blast lemma preserve_min_P_Sts: assumes "enat (Suc k) < llength Sts" and "(C, i) \# wP_of_wstate (lnth Sts k)" and "(C, j) \# wP_of_wstate (lnth Sts (Suc k))" and "\j. (C, j) \# wP_of_wstate (lnth Sts k) \ i \ j" shows "(C, i) \# wP_of_wstate (lnth Sts (Suc k))" using deriv assms chain_lnth_rel preserve_min_P by metis lemma in_lnth_in_Supremum_ldrop: assumes "i < llength xs" and "x \# (lnth xs i)" shows "x \ Sup_llist (lmap set_mset (ldrop (enat i) xs))" using assms by (metis (no_types) ldrop_eq_LConsD ldropn_0 llist.simps(13) contra_subsetD ldrop_enat ldropn_Suc_conv_ldropn lnth_0 lnth_lmap lnth_subset_Sup_llist) lemma persistent_wclause_in_P_if_persistent_clause_in_P: assumes "C \ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))" shows "\i. (C, i) \ Liminf_llist (lmap (set_mset \ wP_of_wstate) Sts)" proof - obtain t_C where t_C_p: "enat t_C < llength Sts" "\t. t_C \ t \ t < llength Sts \ C \ P_of_state (state_of_wstate (lnth Sts t))" using assms unfolding Liminf_llist_def by auto then obtain i where i_p: "(C, i) \# wP_of_wstate (lnth Sts t_C)" using t_C_p by (cases "lnth Sts t_C") force have Ci_in_nth_wP: "\i. (C, i) \# wP_of_wstate (lnth Sts (t_C + t))" if "t_C + t < llength Sts" for t using that t_C_p(2)[of "t_C + _"] by (cases "lnth Sts (t_C + t)") force define in_Sup_wP :: "nat \ bool" where "in_Sup_wP = (\i. (C, i) \ Sup_llist (lmap (set_mset \ wP_of_wstate) (ldrop t_C Sts)))" have "in_Sup_wP i" using i_p assms(1) in_lnth_in_Supremum_ldrop[of t_C "lmap wP_of_wstate Sts" "(C, i)"] t_C_p by (simp add: in_Sup_wP_def llist.map_comp) then obtain j where j_p: "is_least in_Sup_wP j" unfolding in_Sup_wP_def[symmetric] using least_exists by metis then have "\i. (C, i) \ Sup_llist (lmap (set_mset \ wP_of_wstate) (ldrop t_C Sts)) \ j \ i" unfolding is_least_def in_Sup_wP_def using not_less by blast then have j_smallest: "\i t. enat (t_C + t) < llength Sts \ (C, i) \# wP_of_wstate (lnth Sts (t_C + t)) \ j \ i" unfolding comp_def by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn plus_enat_simps(1) lnth_ldropn Sup_llist_def UN_I ldrop_lmap llength_lmap lnth_lmap mem_Collect_eq) from j_p have "\t_Cj. t_Cj < llength (ldrop (enat t_C) Sts) \ (C, j) \# wP_of_wstate (lnth (ldrop t_C Sts) t_Cj)" unfolding in_Sup_wP_def Sup_llist_def is_least_def by simp then obtain t_Cj where j_p: "(C,j) \# wP_of_wstate (lnth Sts (t_C + t_Cj))" "enat (t_C + t_Cj) < llength Sts" by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn plus_enat_simps(1) lhd_ldropn) have Ci_stays: "t_C + t_Cj + t < llength Sts \ (C,j) \# wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for t proof (induction t) case 0 then show ?case using j_p by (simp add: add.commute) next case (Suc t) have any_Ck_in_wP: "j \ k" if "(C, k) \# wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for k using that j_p j_smallest Suc by (smt Suc_ile_eq add.commute add.left_commute add_Suc less_imp_le plus_enat_simps(1) the_enat.simps) from Suc have Cj_in_wP: "(C, j) \# wP_of_wstate (lnth Sts (t_C + t_Cj + t))" by (metis (no_types, hide_lams) Suc_ile_eq add.commute add_Suc_right less_imp_le) moreover have "C \ P_of_state (state_of_wstate (lnth Sts (Suc (t_C + t_Cj + t))))" using t_C_p(2) Suc.prems by auto then have "\k. (C, k) \# wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))" by (smt Suc.prems Ci_in_nth_wP add.commute add.left_commute add_Suc_right enat_ord_code(4)) ultimately have "(C, j) \# wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))" using preserve_min_P_Sts Cj_in_wP any_Ck_in_wP Suc.prems by force then have "(C, j) \# lnth (lmap wP_of_wstate Sts) (Suc (t_C + t_Cj + t))" using Suc.prems by auto then show ?case by (smt Suc.prems add.commute add_Suc_right lnth_lmap) qed then have "(\t. t_C + t_Cj \ t \ t < llength (lmap (set_mset \ wP_of_wstate) Sts) \ (C, j) \# wP_of_wstate (lnth Sts t))" using Ci_stays[of "_ - (t_C + t_Cj)"] by (metis le_add_diff_inverse llength_lmap) then have "(C, j) \ Liminf_llist (lmap (set_mset \ wP_of_wstate) Sts)" unfolding Liminf_llist_def using j_p by auto then show "\i. (C, i) \ Liminf_llist (lmap (set_mset \ wP_of_wstate) Sts)" by auto qed lemma lfinite_not_LNil_nth_llast: assumes "lfinite Sts" and "Sts \ LNil" shows "\i < llength Sts. lnth Sts i = llast Sts \ (\j < llength Sts. j \ i)" using assms proof (induction rule: lfinite.induct) case (lfinite_LConsI xs x) then show ?case proof (cases "xs = LNil") case True show ?thesis using True zero_enat_def by auto next case False then obtain i where i_p: "enat i < llength xs \ lnth xs i = llast xs \ (\j < llength xs. j \ enat i)" using lfinite_LConsI by auto then have "enat (Suc i) < llength (LCons x xs)" by (simp add: Suc_ile_eq) moreover from i_p have "lnth (LCons x xs) (Suc i) = llast (LCons x xs)" by (metis gr_implies_not_zero llast_LCons llength_lnull lnth_Suc_LCons) moreover from i_p have "\j < llength (LCons x xs). j \ enat (Suc i)" by (metis antisym_conv2 eSuc_enat eSuc_ile_mono ileI1 iless_Suc_eq llength_LCons) ultimately show ?thesis by auto qed qed auto lemma fair_if_finite: assumes fin: "lfinite Sts" shows "fair_state_seq (lmap state_of_wstate Sts)" proof (rule ccontr) assume unfair: "\ fair_state_seq (lmap state_of_wstate Sts)" have no_inf_from_last: "\y. \ llast Sts \\<^sub>w y" using fin full_chain_iff_chain[of "(\\<^sub>w)" Sts] full_deriv by auto from unfair obtain C where "C \ Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts)) \ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))" unfolding fair_state_seq_def Liminf_state_def by auto then obtain i where i_p: "enat i < llength Sts" "\j. i \ j \ enat j < llength Sts \ C \ N_of_state (state_of_wstate (lnth Sts j)) \ P_of_state (state_of_wstate (lnth Sts j))" unfolding Liminf_llist_def by auto have C_in_llast: "C \ N_of_state (state_of_wstate (llast Sts)) \ P_of_state (state_of_wstate (llast Sts))" proof - obtain l where l_p: "enat l < llength Sts \ lnth Sts l = llast Sts \ (\j < llength Sts. j \ enat l)" using fin lfinite_not_LNil_nth_llast i_p(1) by fastforce then have "C \ N_of_state (state_of_wstate (lnth Sts l)) \ P_of_state (state_of_wstate (lnth Sts l))" using i_p(1) i_p(2)[of l] by auto then show ?thesis using l_p by auto qed define N :: "'a wclause multiset" where "N = wN_of_wstate (llast Sts)" define P :: "'a wclause multiset" where "P = wP_of_wstate (llast Sts)" define Q :: "'a wclause multiset" where "Q = wQ_of_wstate (llast Sts)" define n :: nat where "n = n_of_wstate (llast Sts)" { assume "N_of_state (state_of_wstate (llast Sts)) \ {}" then obtain D j where "(D, j) \# N" unfolding N_def by (cases "llast Sts") auto then have "llast Sts \\<^sub>w (N - {#(D, j)#}, P + {#(D, j)#}, Q, n)" using weighted_RP.clause_processing[of "N - {#(D, j)#}" D j P Q n] unfolding N_def P_def Q_def n_def by auto then have "\St'. llast Sts \\<^sub>w St'" by auto } moreover { assume a: "N_of_state (state_of_wstate (llast Sts)) = {}" then have b: "N = {#}" unfolding N_def by (cases "llast Sts") auto from a have "C \ P_of_state (state_of_wstate (llast Sts))" using C_in_llast by auto then obtain D j where "(D, j) \# P" unfolding P_def by (cases "llast Sts") auto then have "weight (D, j) \ weight ` set_mset P" by auto then have "\w. is_least (\w. w \ (weight ` set_mset P)) w" using least_exists by auto then have "\D j. (\(D', j') \# P. weight (D, j) \ weight (D', j')) \ (D, j) \# P" using assms linorder_not_less unfolding is_least_def by (auto 6 0) then obtain D j where min: "(\(D', j') \# P. weight (D, j) \ weight (D', j'))" and Dj_in_p: "(D, j) \# P" by auto from min have min: "(\(D', j') \# P - {#(D, j)#}. weight (D, j) \ weight (D', j'))" using mset_subset_diff_self[OF Dj_in_p] by auto define N' where "N' = mset_set ((\D'. (D', n)) ` concls_of (inference_system.inferences_between (ord_FO_\ S) (set_mset (image_mset fst Q)) D))" have "llast Sts \\<^sub>w (N', {#(D', j') \# P - {#(D, j)#}. D' \ D#}, Q + {#(D,j)#}, Suc n)" using weighted_RP.inference_computation[of "P - {#(D, j)#}" D j N' n Q, OF min N'_def] of_wstate_split[symmetric, of "llast Sts"] Dj_in_p unfolding N_def[symmetric] P_def[symmetric] Q_def[symmetric] n_def[symmetric] b by auto then have "\St'. llast Sts \\<^sub>w St'" by auto } ultimately have "\St'. llast Sts \\<^sub>w St'" by auto then show False using no_inf_from_last by metis qed lemma N_of_state_state_of_wstate_wN_of_wstate: assumes "C \ N_of_state (state_of_wstate St)" shows "\i. (C, i) \# wN_of_wstate St" by (smt N_of_state.elims assms eq_fst_iff fstI fst_conv image_iff of_wstate_split set_image_mset state_of_wstate.simps) lemma in_wN_of_wstate_in_N_of_wstate: "(C, i) \# wN_of_wstate St \ C \ N_of_wstate St" by (metis (mono_guards_query_query) N_of_state.simps fst_conv image_eqI of_wstate_split set_image_mset state_of_wstate.simps) lemma in_wP_of_wstate_in_P_of_wstate: "(C, i) \# wP_of_wstate St \ C \ P_of_wstate St" by (metis (mono_guards_query_query) P_of_state.simps fst_conv image_eqI of_wstate_split set_image_mset state_of_wstate.simps) lemma in_wQ_of_wstate_in_Q_of_wstate: "(C, i) \# wQ_of_wstate St \ C \ Q_of_wstate St" by (metis (mono_guards_query_query) Q_of_state.simps fst_conv image_eqI of_wstate_split set_image_mset state_of_wstate.simps) lemma n_of_wstate_weighted_RP_increasing: "St \\<^sub>w St' \ n_of_wstate St \ n_of_wstate St'" by (induction rule: weighted_RP.induct) auto lemma nth_of_wstate_monotonic: assumes "j < llength Sts" and "i \ j" shows "n_of_wstate (lnth Sts i) \ n_of_wstate (lnth Sts j)" using assms proof (induction "j - i" arbitrary: i) case (Suc x) then have "x = j - (i + 1)" by auto then have "n_of_wstate (lnth Sts (i + 1)) \ n_of_wstate (lnth Sts j)" using Suc by auto moreover have "i < j" using Suc by auto then have "Suc i < llength Sts" using Suc by (metis enat_ord_simps(2) le_less_Suc_eq less_le_trans not_le) then have "lnth Sts i \\<^sub>w lnth Sts (Suc i)" using deriv chain_lnth_rel[of "(\\<^sub>w)" Sts i] by auto then have "n_of_wstate (lnth Sts i) \ n_of_wstate (lnth Sts (i + 1))" using n_of_wstate_weighted_RP_increasing[of "lnth Sts i" "lnth Sts (i + 1)"] by auto ultimately show ?case by auto qed auto lemma infinite_chain_relation_measure: assumes measure_decreasing: "\St St'. P St \ R St St' \ (m St', m St) \ mR" and non_infer_chain: "chain R (ldrop (enat k) Sts)" and inf: "llength Sts = \" and P: "\i. P (lnth (ldrop (enat k) Sts) i)" shows "chain (\x y. (x, y) \ mR)\\ (lmap m (ldrop (enat k) Sts))" proof (rule lnth_rel_chain) show "\ lnull (lmap m (ldrop (enat k) Sts))" using assms by auto next from inf have ldrop_inf: "llength (ldrop (enat k) Sts) = \ \ \ lfinite (ldrop (enat k) Sts)" using inf by (auto simp: llength_eq_infty_conv_lfinite) { fix j :: "nat" define St where "St = lnth (ldrop (enat k) Sts) j" define St' where "St' = lnth (ldrop (enat k) Sts) (j + 1)" have P': "P St \ P St'" unfolding St_def St'_def using P by auto from ldrop_inf have "R St St'" unfolding St_def St'_def using non_infer_chain infinite_chain_lnth_rel[of "ldrop (enat k) Sts" R j] by auto then have "(m St', m St) \ mR" using measure_decreasing P' by auto then have "(lnth (lmap m (ldrop (enat k) Sts)) (j + 1), lnth (lmap m (ldrop (enat k) Sts)) j) \ mR" unfolding St_def St'_def using lnth_lmap by (smt enat.distinct(1) enat_add_left_cancel enat_ord_simps(4) inf ldrop_lmap llength_lmap lnth_ldrop plus_enat_simps(3)) } then show "\j. enat (j + 1) < llength (lmap m (ldrop (enat k) Sts)) \ (\x y. (x, y) \ mR)\\ (lnth (lmap m (ldrop (enat k) Sts)) j) (lnth (lmap m (ldrop (enat k) Sts)) (j + 1))" by blast qed theorem weighted_RP_fair: "fair_state_seq (lmap state_of_wstate Sts)" proof (rule ccontr) assume asm: "\ fair_state_seq (lmap state_of_wstate Sts)" then have inff: "\ lfinite Sts" using fair_if_finite by auto then have inf: "llength Sts = \" using llength_eq_infty_conv_lfinite by auto from asm obtain C where "C \ Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts)) \ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))" unfolding fair_state_seq_def Liminf_state_def by auto then show False proof assume "C \ Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))" then obtain x where "enat x < llength Sts" "\xa. x \ xa \ enat xa < llength Sts \ C \ N_of_state (state_of_wstate (lnth Sts xa))" unfolding Liminf_llist_def by auto then have "\k. \j. k \ j \ (\i. (C, i) \# wN_of_wstate (lnth Sts j))" unfolding Liminf_llist_def by (force simp add: inf N_of_state_state_of_wstate_wN_of_wstate) then obtain k where k_p: "\j. k \ j \ \i. (C, i) \# wN_of_wstate (lnth Sts j)" unfolding Liminf_llist_def by auto have chain_drop_Sts: "chain (\\<^sub>w) (ldrop k Sts)" using deriv inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat) have in_N_j: "\j. \i. (C, i) \# wN_of_wstate (lnth (ldrop k Sts) j)" using k_p by (simp add: add.commute inf) then have "chain (\x y. (x, y) \ RP_filtered_relation)\\ (lmap (RP_filtered_measure (\Ci. True)) (ldrop k Sts))" using inff inf weighted_RP_measure_decreasing_N chain_drop_Sts infinite_chain_relation_measure[of "\St. \i. (C, i) \# wN_of_wstate St" "(\\<^sub>w)"] by blast then show False using wfP_iff_no_infinite_down_chain_llist[of "\x y. (x, y) \ RP_filtered_relation"] wf_RP_filtered_relation inff by (metis (no_types, lifting) inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist lfinite_lmap wfPUNIVI wf_induct_rule) next assume asm: "C \ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))" from asm obtain i where i_p: "enat i < llength Sts" "\j. i \ j \ enat j < llength Sts \ C \ P_of_state (state_of_wstate (lnth Sts j))" unfolding Liminf_llist_def by auto then obtain i where "(C, i) \ Liminf_llist (lmap (set_mset \ wP_of_wstate) Sts)" using persistent_wclause_in_P_if_persistent_clause_in_P[of C] using asm inf by auto then have "\l. \k \ l. (C, i) \ (set_mset \ wP_of_wstate) (lnth Sts k)" unfolding Liminf_llist_def using inff inf by auto then obtain k where k_p: "(\k'\k. (C, i) \ (set_mset \ wP_of_wstate) (lnth Sts k'))" by blast have Ci_in: "\k'. (C, i) \ (set_mset \ wP_of_wstate) (lnth (ldrop k Sts) k')" using k_p lnth_ldrop[of k _ Sts] inf inff by force then have Ci_inn: "\k'. (C, i) \# (wP_of_wstate) (lnth (ldrop k Sts) k')" by auto have "chain (\\<^sub>w) (ldrop k Sts)" using deriv inf_chain_ldropn_chain inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat) then have "chain (\x y. (x, y) \ RP_combined_relation)\\ (lmap (RP_combined_measure (weight (C, i))) (ldrop k Sts))" using inff inf Ci_in weighted_RP_measure_decreasing_P infinite_chain_relation_measure[of "\St. (C, i) \# wP_of_wstate St" "(\\<^sub>w)" "RP_combined_measure (weight (C, i))" ] by auto then show False using wfP_iff_no_infinite_down_chain_llist[of "\x y. (x, y) \ RP_combined_relation"] wf_RP_combined_relation inff by (smt inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist lfinite_lmap wfPUNIVI wf_induct_rule) qed qed corollary weighted_RP_saturated: "src.saturated_upto (Liminf_llist (lmap grounding_of_wstate Sts))" using RP_saturated_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, unfolded llist.map_comp] by simp corollary weighted_RP_complete: "\ satisfiable (grounding_of_wstate (lhd Sts)) \ {#} \ Q_of_state (Liminf_wstate Sts)" using RP_complete_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, simplified lhd_lmap_Sts] . end end locale weighted_FO_resolution_prover_with_size_timestamp_factors = FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm for S :: "('a :: wellorder) clause \ 'a clause" and subst_atm :: "'a \ 's \ 'a" and id_subst :: "'s" and comp_subst :: "'s \ 's \ 's" and renamings_apart :: "'a literal multiset list \ 's list" and atm_of_atms :: "'a list \ 'a" and mgu :: "'a set set \ 's option" and less_atm :: "'a \ 'a \ bool" + fixes size_atm :: "'a \ nat" and size_factor :: nat and timestamp_factor :: nat assumes timestamp_factor_pos: "timestamp_factor > 0" begin fun weight :: "'a wclause \ nat" where "weight (C, i) = size_factor * size_multiset (size_literal size_atm) C + timestamp_factor * i" lemma weight_mono: "i < j \ weight (C, i) < weight (C, j)" using timestamp_factor_pos by simp declare weight.simps [simp del] sublocale wrp: weighted_FO_resolution_prover _ _ _ _ _ _ _ _ weight by unfold_locales (rule weight_mono) notation wrp.weighted_RP (infix "\\<^sub>w" 50) end end diff --git a/thys/Functional_Ordered_Resolution_Prover/document/root.tex b/thys/Functional_Ordered_Resolution_Prover/document/root.tex --- a/thys/Functional_Ordered_Resolution_Prover/document/root.tex +++ b/thys/Functional_Ordered_Resolution_Prover/document/root.tex @@ -1,79 +1,72 @@ \documentclass[10pt,a4paper]{article} \usepackage{amssymb} \usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} \usepackage{graphicx} \usepackage{isabelle} \usepackage{isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{pdfsetup} \urlstyle{tt} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \renewcommand{\isacharunderscore}{\_} \begin{document} \title{A Verified Functional Implementation of \\ Bachmair and Ganzinger's Ordered Resolution Prover} \author{Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel} \maketitle \begin{abstract} \noindent This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section~4.3 of Bachmair and Ganzinger's ``Resolution Theorem Proving'' chapter in the \emph{Handbook of Automated Reasoning}. The result is a functional implementation of a first-order prover. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt \parskip 0.5ex \section{Introduction} Bachmair and Ganzinger's ``Resolution Theorem Proving'' chapter %\cite{bachmair-ganzinger-2001} in the \emph{Handbook of Automated Reasoning} is the standard reference on the topic. It defines a general framework for propositional and first-order resolution-based theorem proving. Resolution forms the basis for superposition, the calculus implemented in many popular automatic theorem provers. \medskip This Isabelle/HOL formalization starts from an existing formalization of Bachmair and Ganzinger's chapter, up to and including Section 4.3. It refines the abstract ordered resolution prover presented in Section~4.3 to obtain an executable, functional implementation of a first-order prover. Figure~\ref{fig:thys} shows the corresponding Isabelle theory structure. -\medskip - -Due to a dependency on the Knuth--Bendix order from the \textsf{IsaFoR} -library, which has not yet been moved to the AFP, the final part of our -development is currently hosted in the IsaFoL repository.% -\footnote{\url{https://bitbucket.org/isafol/isafol/src/master/Functional_Ordered_Resolution_Prover/}} - \begin{figure} \begin{center} \includegraphics[width=0.75\textwidth,keepaspectratio]{session_graph} \end{center} \caption{Theory dependency graph} \label{fig:thys} \end{figure} % generated text of all theories \input{session} % optional bibliography % \bibliographystyle{abbrv} % \bibliography{bib} \end{document}