# Theory TermsAndLiterals

section ‹Terms and Literals› theory TermsAndLiterals imports Main "HOL-Library.Countable_Set" begin type_synonym var_sym = string type_synonym fun_sym = string type_synonym pred_sym = string datatype fterm = Fun fun_sym (get_sub_terms: "fterm list") | Var var_sym datatype hterm = HFun fun_sym "hterm list" ― ‹Herbrand terms defined as in Berghofer's FOL-Fitting› type_synonym 't atom = "pred_sym * 't list" datatype 't literal = sign: Pos (get_pred: pred_sym) (get_terms: "'t list") | Neg (get_pred: pred_sym) (get_terms: "'t list") fun get_atom :: "'t literal ⇒ 't atom" where "get_atom (Pos p ts) = (p, ts)" | "get_atom (Neg p ts) = (p, ts)" subsection ‹Ground› fun ground⇩_{t}:: "fterm ⇒ bool" where "ground⇩_{t}(Var x) ⟷ False" | "ground⇩_{t}(Fun f ts) ⟷ (∀t ∈ set ts. ground⇩_{t}t)" abbreviation ground⇩_{t}⇩_{s}:: "fterm list ⇒ bool" where "ground⇩_{t}⇩_{s}ts ≡ (∀t ∈ set ts. ground⇩_{t}t)" abbreviation ground⇩_{l}:: "fterm literal ⇒ bool" where "ground⇩_{l}l ≡ ground⇩_{t}⇩_{s}(get_terms l)" abbreviation ground⇩_{l}⇩_{s}:: "fterm literal set ⇒ bool" where "ground⇩_{l}⇩_{s}C ≡ (∀l ∈ C. ground⇩_{l}l)" definition ground_fatoms :: "fterm atom set" where "ground_fatoms ≡ {a. ground⇩_{t}⇩_{s}(snd a)}" lemma ground⇩_{l}_ground_fatom: assumes "ground⇩_{l}l" shows "get_atom l ∈ ground_fatoms" using assms unfolding ground_fatoms_def by (induction l) auto subsection ‹Auxiliary› lemma infinity: assumes inj: "∀n :: nat. undiago (diago n) = n" assumes all_tree: "∀n :: nat. (diago n) ∈ S" shows "¬finite S" proof - from inj all_tree have "∀n. n = undiago (diago n) ∧ (diago n) ∈ S" by auto then have "∀n. ∃ds. n = undiago ds ∧ ds ∈ S" by auto then have "undiago ` S = (UNIV :: nat set)" by auto then show "¬finite S" by (metis finite_imageI infinite_UNIV_nat) qed lemma inv_into_f_f: assumes "bij_betw f A B" assumes "a∈A" shows "(inv_into A f) (f a) = a" using assms bij_betw_inv_into_left by metis lemma f_inv_into_f: assumes "bij_betw f A B" assumes "b∈B" shows "f ((inv_into A f) b) = b" using assms bij_betw_inv_into_right by metis subsection ‹Conversions› subsubsection ‹Conversions - Terms and Herbrand Terms› fun fterm_of_hterm :: "hterm ⇒ fterm" where "fterm_of_hterm (HFun p ts) = Fun p (map fterm_of_hterm ts)" definition fterms_of_hterms :: "hterm list ⇒ fterm list" where "fterms_of_hterms ts ≡ map fterm_of_hterm ts" fun hterm_of_fterm :: "fterm ⇒ hterm" where "hterm_of_fterm (Fun p ts) = HFun p (map hterm_of_fterm ts)" definition hterms_of_fterms :: "fterm list ⇒ hterm list" where "hterms_of_fterms ts ≡ map hterm_of_fterm ts" lemma hterm_of_fterm_fterm_of_hterm[simp]: "hterm_of_fterm (fterm_of_hterm t) = t" by (induction t) (simp add: map_idI) lemma hterms_of_fterms_fterms_of_hterms[simp]: "hterms_of_fterms (fterms_of_hterms ts) = ts" unfolding hterms_of_fterms_def fterms_of_hterms_def by (simp add: map_idI) lemma fterm_of_hterm_hterm_of_fterm[simp]: assumes "ground⇩_{t}t" shows "fterm_of_hterm (hterm_of_fterm t) = t" using assms by (induction t) (auto simp add: map_idI) lemma fterms_of_hterms_hterms_of_fterms[simp]: assumes "ground⇩_{t}⇩_{s}ts" shows "fterms_of_hterms (hterms_of_fterms ts) = ts" using assms unfolding fterms_of_hterms_def hterms_of_fterms_def by (simp add: map_idI) lemma ground_fterm_of_hterm: "ground⇩_{t}(fterm_of_hterm t)" by (induction t) (auto simp add: map_idI) lemma ground_fterms_of_hterms: "ground⇩_{t}⇩_{s}(fterms_of_hterms ts)" unfolding fterms_of_hterms_def using ground_fterm_of_hterm by auto subsubsection ‹Conversions - Literals and Herbrand Literals› fun flit_of_hlit :: "hterm literal ⇒ fterm literal" where "flit_of_hlit (Pos p ts) = Pos p (fterms_of_hterms ts)" | "flit_of_hlit (Neg p ts) = Neg p (fterms_of_hterms ts)" fun hlit_of_flit :: "fterm literal ⇒ hterm literal" where "hlit_of_flit (Pos p ts) = Pos p (hterms_of_fterms ts)" | "hlit_of_flit (Neg p ts) = Neg p (hterms_of_fterms ts)" lemma ground_flit_of_hlit: "ground⇩_{l}(flit_of_hlit l)" by (induction l) (simp add: ground_fterms_of_hterms)+ theorem hlit_of_flit_flit_of_hlit [simp]: "hlit_of_flit (flit_of_hlit l) = l" by (cases l) auto theorem flit_of_hlit_hlit_of_flit [simp]: assumes "ground⇩_{l}l" shows "flit_of_hlit (hlit_of_flit l) = l" using assms by (cases l) auto lemma sign_flit_of_hlit: "sign (flit_of_hlit l) = sign l" by (cases l) auto lemma hlit_of_flit_bij: "bij_betw hlit_of_flit {l. ground⇩_{l}l} UNIV" unfolding bij_betw_def proof show "inj_on hlit_of_flit {l. ground⇩_{l}l}" using inj_on_inverseI flit_of_hlit_hlit_of_flit by (metis (mono_tags, lifting) mem_Collect_eq) next have "∀l. ∃l'. ground⇩_{l}l' ∧ l = hlit_of_flit l'" using ground_flit_of_hlit hlit_of_flit_flit_of_hlit by metis then show "hlit_of_flit ` {l. ground⇩_{l}l} = UNIV" by auto qed lemma flit_of_hlit_bij: "bij_betw flit_of_hlit UNIV {l. ground⇩_{l}l}" unfolding bij_betw_def inj_on_def proof show "∀x∈UNIV. ∀y∈UNIV. flit_of_hlit x = flit_of_hlit y ⟶ x = y" using ground_flit_of_hlit hlit_of_flit_flit_of_hlit by metis next have "∀l. ground⇩_{l}l ⟶ (l = flit_of_hlit (hlit_of_flit l))" using hlit_of_flit_flit_of_hlit by auto then have "{l. ground⇩_{l}l} ⊆ flit_of_hlit ` UNIV " by blast moreover have "∀l. ground⇩_{l}(flit_of_hlit l)" using ground_flit_of_hlit by auto ultimately show "flit_of_hlit ` UNIV = {l. ground⇩_{l}l}" using hlit_of_flit_flit_of_hlit ground_flit_of_hlit by auto qed subsubsection ‹Conversions - Atoms and Herbrand Atoms› fun fatom_of_hatom :: "hterm atom ⇒ fterm atom" where "fatom_of_hatom (p, ts) = (p, fterms_of_hterms ts)" fun hatom_of_fatom :: "fterm atom ⇒ hterm atom" where "hatom_of_fatom (p, ts) = (p, hterms_of_fterms ts)" lemma ground_fatom_of_hatom: "ground⇩_{t}⇩_{s}(snd (fatom_of_hatom a))" by (induction a) (simp add: ground_fterms_of_hterms)+ theorem hatom_of_fatom_fatom_of_hatom [simp]: "hatom_of_fatom (fatom_of_hatom l) = l" by (cases l) auto theorem fatom_of_hatom_hatom_of_fatom [simp]: assumes "ground⇩_{t}⇩_{s}(snd l)" shows "fatom_of_hatom (hatom_of_fatom l) = l" using assms by (cases l) auto lemma hatom_of_fatom_bij: "bij_betw hatom_of_fatom ground_fatoms UNIV" unfolding bij_betw_def proof show "inj_on hatom_of_fatom ground_fatoms" using inj_on_inverseI fatom_of_hatom_hatom_of_fatom unfolding ground_fatoms_def by (metis (mono_tags, lifting) mem_Collect_eq) next have "∀a. ∃a'. ground⇩_{t}⇩_{s}(snd a') ∧ a = hatom_of_fatom a'" using ground_fatom_of_hatom hatom_of_fatom_fatom_of_hatom by metis then show "hatom_of_fatom ` ground_fatoms = UNIV" unfolding ground_fatoms_def by blast qed lemma fatom_of_hatom_bij: "bij_betw fatom_of_hatom UNIV ground_fatoms" unfolding bij_betw_def inj_on_def proof show "∀x∈UNIV. ∀y∈UNIV. fatom_of_hatom x = fatom_of_hatom y ⟶ x = y" using ground_fatom_of_hatom hatom_of_fatom_fatom_of_hatom by metis next have "∀a. ground⇩_{t}⇩_{s}(snd a) ⟶ (a = fatom_of_hatom (hatom_of_fatom a))" using hatom_of_fatom_fatom_of_hatom by auto then have "ground_fatoms ⊆ fatom_of_hatom ` UNIV " unfolding ground_fatoms_def by blast moreover have "∀l. ground⇩_{t}⇩_{s}(snd (fatom_of_hatom l))" using ground_fatom_of_hatom by auto ultimately show "fatom_of_hatom ` UNIV = ground_fatoms" using hatom_of_fatom_fatom_of_hatom ground_fatom_of_hatom unfolding ground_fatoms_def by auto qed subsection ‹Enumerations› subsubsection ‹Enumerating Strings› definition nat_of_string:: "string ⇒ nat" where "nat_of_string ≡ (SOME f. bij f)" definition string_of_nat:: "nat ⇒ string" where "string_of_nat ≡ inv nat_of_string" lemma nat_of_string_bij: "bij nat_of_string" proof - have "countable (UNIV::string set)" by auto moreover have "infinite (UNIV::string set)" using infinite_UNIV_listI by auto ultimately obtain x where "bij (x:: string ⇒ nat)" using countableE_infinite[of UNIV] by blast then show "?thesis" unfolding nat_of_string_def using someI by metis qed lemma string_of_nat_bij: "bij string_of_nat" unfolding string_of_nat_def using nat_of_string_bij bij_betw_inv_into by auto lemma nat_of_string_string_of_nat[simp]: "nat_of_string (string_of_nat n) = n" unfolding string_of_nat_def using nat_of_string_bij f_inv_into_f[of nat_of_string] by simp lemma string_of_nat_nat_of_string[simp]: "string_of_nat (nat_of_string n) = n" unfolding string_of_nat_def using nat_of_string_bij inv_into_f_f[of nat_of_string] by simp subsubsection ‹Enumerating Herbrand Atoms› definition nat_of_hatom:: "hterm atom ⇒ nat" where "nat_of_hatom ≡ (SOME f. bij f)" definition hatom_of_nat:: "nat ⇒ hterm atom" where "hatom_of_nat ≡ inv nat_of_hatom" instantiation hterm :: countable begin instance by countable_datatype end lemma infinite_hatoms: "infinite (UNIV :: ('t atom) set)" proof - let ?diago = "λn. (string_of_nat n,[])" let ?undiago = "λa. nat_of_string (fst a)" have "∀n. ?undiago (?diago n) = n" using nat_of_string_string_of_nat by auto moreover have "∀n. ?diago n ∈ UNIV" by auto ultimately show "infinite (UNIV :: ('t atom) set)" using infinity[of ?undiago ?diago UNIV] by simp qed lemma nat_of_hatom_bij: "bij nat_of_hatom" proof - let ?S = "UNIV :: (('t::countable) atom) set" have "countable ?S" by auto moreover have "infinite ?S" using infinite_hatoms by auto ultimately obtain x where "bij (x :: hterm atom ⇒ nat)" using countableE_infinite[of ?S] by blast then have "bij nat_of_hatom" unfolding nat_of_hatom_def using someI by metis then show "?thesis" unfolding bij_betw_def inj_on_def unfolding nat_of_hatom_def by simp qed lemma hatom_of_nat_bij: "bij hatom_of_nat" unfolding hatom_of_nat_def using nat_of_hatom_bij bij_betw_inv_into by auto lemma nat_of_hatom_hatom_of_nat[simp]: "nat_of_hatom (hatom_of_nat n) = n" unfolding hatom_of_nat_def using nat_of_hatom_bij f_inv_into_f[of nat_of_hatom] by simp lemma hatom_of_nat_nat_of_hatom[simp]: "hatom_of_nat (nat_of_hatom l) = l" unfolding hatom_of_nat_def using nat_of_hatom_bij inv_into_f_f[of nat_of_hatom _ UNIV] by simp subsubsection ‹Enumerating Ground Atoms› definition fatom_of_nat :: "nat ⇒ fterm atom" where "fatom_of_nat = (λn. fatom_of_hatom (hatom_of_nat n))" definition nat_of_fatom :: "fterm atom ⇒ nat" where "nat_of_fatom = (λt. nat_of_hatom (hatom_of_fatom t))" theorem diag_undiag_fatom[simp]: assumes "ground⇩_{t}⇩_{s}ts" shows "fatom_of_nat (nat_of_fatom (p,ts)) = (p,ts)" using assms unfolding fatom_of_nat_def nat_of_fatom_def by auto theorem undiag_diag_fatom[simp]: "nat_of_fatom (fatom_of_nat n) = n" unfolding fatom_of_nat_def nat_of_fatom_def by auto lemma fatom_of_nat_bij: "bij_betw fatom_of_nat UNIV ground_fatoms" using hatom_of_nat_bij bij_betw_trans fatom_of_hatom_bij hatom_of_nat_bij unfolding fatom_of_nat_def comp_def by blast lemma ground_fatom_of_nat: "ground⇩_{t}⇩_{s}(snd (fatom_of_nat x))" unfolding fatom_of_nat_def using ground_fatom_of_hatom by auto lemma nat_of_fatom_bij: "bij_betw nat_of_fatom ground_fatoms UNIV" using nat_of_hatom_bij bij_betw_trans hatom_of_fatom_bij hatom_of_nat_bij unfolding nat_of_fatom_def comp_def by blast end

# Theory Tree

section ‹Trees› theory Tree imports Main begin text ‹Sometimes it is nice to think of @{typ bool}s as directions in a binary tree› hide_const (open) Left Right type_synonym dir = bool definition Left :: bool where "Left = True" definition Right :: bool where "Right = False" declare Left_def [simp] declare Right_def [simp] datatype tree = Leaf | Branching (ltree: tree) (rtree: tree) subsection ‹Sizes› fun treesize :: "tree ⇒ nat" where "treesize Leaf = 0" | "treesize (Branching l r) = 1 + treesize l + treesize r" lemma treesize_Leaf: assumes "treesize T = 0" shows "T = Leaf" using assms by (cases T) auto lemma treesize_Branching: assumes "treesize T = Suc n" shows "∃l r. T = Branching l r" using assms by (cases T) auto subsection ‹Paths› fun path :: "dir list ⇒ tree ⇒ bool" where "path [] T ⟷ True" | "path (d#ds) (Branching T1 T2) ⟷ (if d then path ds T1 else path ds T2)" | "path _ _ ⟷ False" lemma path_inv_Leaf: "path p Leaf ⟷ p = []" by (induction p) auto lemma path_inv_Cons: "path (a#ds) T ⟶ (∃l r. T=Branching l r)" by (cases T) (auto simp add: path_inv_Leaf) lemma path_inv_Branching_Left: "path (Left#p) (Branching l r) ⟷ path p l" using Left_def Right_def path.cases by (induction p) auto lemma path_inv_Branching_Right: "path (Right#p) (Branching l r) ⟷ path p r" using Left_def Right_def path.cases by (induction p) auto lemma path_inv_Branching: "path p (Branching l r) ⟷ (p=[] ∨ (∃a p'. p=a#p'∧ (a ⟶ path p' l) ∧ (¬a ⟶ path p' r)))" (is "?L ⟷ ?R") proof assume ?L then show ?R by (induction p) auto next assume r: ?R then show ?L proof assume "p = []" then show ?L by auto next assume "∃a p'. p=a#p'∧ (a ⟶ path p' l) ∧ (¬a ⟶ path p' r)" then obtain a p' where "p=a#p'∧ (a ⟶ path p' l) ∧ (¬a ⟶ path p' r)" by auto then show ?L by (cases a) auto qed qed lemma path_prefix: assumes "path (ds1@ds2) T" shows "path ds1 T" using assms proof (induction ds1 arbitrary: T) case (Cons a ds1) then have "∃l r. T = Branching l r" using path_inv_Leaf by (cases T) auto then obtain l r where p_lr: "T = Branching l r" by auto show ?case proof (cases a) assume atrue: "a" then have "path ((ds1) @ ds2) l" using p_lr Cons(2) path_inv_Branching by auto then have "path ds1 l" using Cons(1) by auto then show "path (a # ds1) T" using p_lr atrue by auto next assume afalse: "¬a" then have "path ((ds1) @ ds2) r" using p_lr Cons(2) path_inv_Branching by auto then have "path ds1 r" using Cons(1) by auto then show "path (a # ds1) T" using p_lr afalse by auto qed next case (Nil) then show ?case by auto qed subsection ‹Branches› fun branch :: "dir list ⇒ tree ⇒ bool" where "branch [] Leaf ⟷ True" | "branch (d # ds) (Branching l r) ⟷ (if d then branch ds l else branch ds r)" | "branch _ _ ⟷ False" lemma has_branch: "∃b. branch b T" proof (induction T) case (Leaf) have "branch [] Leaf" by auto then show ?case by blast next case (Branching T⇩_{1}T⇩_{2}) then obtain b where "branch b T⇩_{1}" by auto then have "branch (Left#b) (Branching T⇩_{1}T⇩_{2})" by auto then show ?case by blast qed lemma branch_inv_Leaf: "branch b Leaf ⟷ b = []" by (cases b) auto lemma branch_inv_Branching_Left: "branch (Left#b) (Branching l r) ⟷ branch b l" by auto lemma branch_inv_Branching_Right: "branch (Right#b) (Branching l r) ⟷ branch b r" by auto lemma branch_inv_Branching: "branch b (Branching l r) ⟷ (∃a b'. b=a#b'∧ (a ⟶ branch b' l) ∧ (¬a ⟶ branch b' r))" by (induction b) auto lemma branch_inv_Leaf2: "T = Leaf ⟷ (∀b. branch b T ⟶ b = [])" proof - { assume "T=Leaf" then have "∀b. branch b T ⟶ b = []" using branch_inv_Leaf by auto } moreover { assume "∀b. branch b T ⟶ b = []" then have "∀b. branch b T ⟶ ¬(∃a b'. b = a # b')" by auto then have "∀b. branch b T ⟶ ¬(∃l r. branch b (Branching l r))" using branch_inv_Branching by auto then have "T=Leaf" using has_branch[of T] by (metis branch.elims(2)) } ultimately show "T = Leaf ⟷ (∀b. branch b T ⟶ b = [])" by auto qed lemma branch_is_path: assumes"branch ds T" shows "path ds T" using assms proof (induction T arbitrary: ds) case Leaf then have "ds = []" using branch_inv_Leaf by auto then show ?case by auto next case (Branching T⇩_{1}T⇩_{2}) then obtain a b where ds_p: "ds = a # b ∧ (a ⟶ branch b T⇩_{1}) ∧ (¬ a ⟶ branch b T⇩_{2})" using branch_inv_Branching[of ds] by blast then have "(a ⟶ path b T⇩_{1}) ∧ (¬a ⟶ path b T⇩_{2})" using Branching by auto then show "?case" using ds_p by (cases a) auto qed lemma Branching_Leaf_Leaf_Tree: assumes "T = Branching T1 T2" shows "(∃B. branch (B@[True]) T ∧ branch (B@[False]) T)" using assms proof (induction T arbitrary: T1 T2) case Leaf then show ?case by auto next case (Branching T1' T2') { assume "T1'=Leaf ∧ T2'=Leaf" then have "branch ([] @ [True]) (Branching T1' T2') ∧ branch ([] @ [False]) (Branching T1' T2')" by auto then have ?case by metis } moreover { fix T11 T12 assume "T1' = Branching T11 T12" then obtain B where "branch (B @ [True]) T1' ∧ branch (B @ [False]) T1'" using Branching by blast then have "branch (([True] @ B) @ [True]) (Branching T1' T2') ∧ branch (([True] @ B) @ [False]) (Branching T1' T2')" by auto then have ?case by blast } moreover { fix T11 T12 assume "T2' = Branching T11 T12" then obtain B where "branch (B @ [True]) T2' ∧ branch (B @ [False]) T2'" using Branching by blast then have "branch (([False] @ B) @ [True]) (Branching T1' T2') ∧ branch (([False] @ B) @ [False]) (Branching T1' T2')" by auto then have ?case by blast } ultimately show ?case using tree.exhaust by blast qed subsection ‹Internal Paths› fun internal :: "dir list ⇒ tree ⇒ bool" where "internal [] (Branching l r) ⟷ True" | "internal (d#ds) (Branching l r) ⟷ (if d then internal ds l else internal ds r)" | "internal _ _ ⟷ False" lemma internal_inv_Leaf: "¬internal b Leaf" using internal.simps by blast lemma internal_inv_Branching_Left: "internal (Left#b) (Branching l r) ⟷ internal b l" by auto lemma internal_inv_Branching_Right: "internal (Right#b) (Branching l r) ⟷ internal b r" by auto lemma internal_inv_Branching: "internal p (Branching l r) ⟷ (p=[] ∨ (∃a p'. p=a#p'∧ (a ⟶ internal p' l) ∧ (¬a ⟶ internal p' r)))" (is "?L ⟷ ?R") proof assume ?L then show ?R by (metis internal.simps(2) neq_Nil_conv) next assume r: ?R then show ?L proof assume "p = []" then show ?L by auto next assume "∃a p'. p=a#p'∧ (a ⟶ internal p' l) ∧ (¬a ⟶ internal p' r)" then obtain a p' where "p=a#p'∧ (a ⟶ internal p' l) ∧ (¬a ⟶ internal p' r)" by auto then show ?L by (cases a) auto qed qed lemma internal_is_path: assumes "internal ds T" shows "path ds T" using assms proof (induction T arbitrary: ds) case Leaf then have "False" using internal_inv_Leaf by auto then show ?case by auto next case (Branching T⇩_{1}T⇩_{2}) then obtain a b where ds_p: "ds=[] ∨ ds = a # b ∧ (a ⟶ internal b T⇩_{1}) ∧ (¬ a ⟶ internal b T⇩_{2})" using internal_inv_Branching by blast then have "ds = [] ∨ (a ⟶ path b T⇩_{1}) ∧ (¬a ⟶ path b T⇩_{2})" using Branching by auto then show "?case" using ds_p by (cases a) auto qed lemma internal_prefix: assumes "internal (ds1@ds2@[d]) T" shows "internal ds1 T" (* more or less copy paste of path_prefix *) using assms proof (induction ds1 arbitrary: T) case (Cons a ds1) then have "∃l r. T = Branching l r" using internal_inv_Leaf by (cases T) auto then obtain l r where p_lr: "T = Branching l r" by auto show ?case proof (cases a) assume atrue: "a" then have "internal ((ds1) @ ds2 @[d]) l" using p_lr Cons(2) internal_inv_Branching by auto then have "internal ds1 l" using Cons(1) by auto then show "internal (a # ds1) T" using p_lr atrue by auto next assume afalse: "~a" then have "internal ((ds1) @ ds2 @[d]) r" using p_lr Cons(2) internal_inv_Branching by auto then have "internal ds1 r" using Cons(1) by auto then show "internal (a # ds1) T" using p_lr afalse by auto qed next case (Nil) then have "∃l r. T = Branching l r" using internal_inv_Leaf by (cases T) auto then show ?case by auto qed lemma internal_branch: assumes "branch (ds1@ds2@[d]) T" shows "internal ds1 T" (* more or less copy paste of path_prefix *) using assms proof (induction ds1 arbitrary: T) case (Cons a ds1) then have "∃l r. T = Branching l r" using branch_inv_Leaf by (cases T) auto then obtain l r where p_lr: "T = Branching l r" by auto show ?case proof (cases a) assume atrue: "a" then have "branch (ds1 @ ds2 @ [d]) l" using p_lr Cons(2) branch_inv_Branching by auto then have "internal ds1 l" using Cons(1) by auto then show "internal (a # ds1) T" using p_lr atrue by auto next assume afalse: "~a" then have "branch ((ds1) @ ds2 @[d]) r" using p_lr Cons(2) branch_inv_Branching by auto then have "internal ds1 r" using Cons(1) by auto then show "internal (a # ds1) T" using p_lr afalse by auto qed next case (Nil) then have "∃l r. T = Branching l r" using branch_inv_Leaf by (cases T) auto then show ?case by auto qed fun parent :: "dir list ⇒ dir list" where "parent ds = tl ds" subsection ‹Deleting Nodes› fun delete :: "dir list ⇒ tree ⇒ tree" where "delete [] T = Leaf" | "delete (True#ds) (Branching T⇩_{1}T⇩_{2}) = Branching (delete ds T⇩_{1}) T⇩_{2}" | "delete (False#ds) (Branching T⇩_{1}T⇩_{2}) = Branching T⇩_{1}(delete ds T⇩_{2})" | "delete (a#ds) Leaf = Leaf" lemma delete_Leaf: "delete T Leaf = Leaf" by (cases T) auto lemma path_delete: assumes "path p (delete ds T)" shows "path p T " (* What a huge proof... But the four cases can be proven shorter *) using assms proof (induction p arbitrary: T ds) case Nil then show ?case by simp next case (Cons a p) then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto have "∃dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons by auto then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto then have "∃T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *) by (cases T; cases ds) auto then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto { assume a_p: "a" assume b_p: "¬b" have "path (a # p) (delete ds T)" using Cons by - then have "path (a # p) (Branching (T1) (delete ds' T2))" using b_p bds'_p T1T2_p by auto then have "path p T1" using a_p by auto then have ?case using T1T2_p a_p by auto } moreover { assume a_p: "¬a" assume b_p: "b" have "path (a # p) (delete ds T)" using Cons by - then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto then have "path p T2" using a_p by auto then have ?case using T1T2_p a_p by auto } moreover { assume a_p: "a" assume b_p: "b" have "path (a # p) (delete ds T)" using Cons by - then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto then have "path p (delete ds' T1)" using a_p by auto then have "path p T1" using Cons by auto then have ?case using T1T2_p a_p by auto } moreover { assume a_p: "¬a" assume b_p: "¬b" have "path (a # p) (delete ds T)" using Cons by - then have "path (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto then have "path p (delete ds' T2)" using a_p by auto then have "path p T2" using Cons by auto then have ?case using T1T2_p a_p by auto } ultimately show ?case by blast qed lemma branch_delete: assumes "branch p (delete ds T)" shows "branch p T ∨ p=ds" (* Adapted from above *) using assms proof (induction p arbitrary: T ds) case Nil then have "delete ds T = Leaf" by (cases "delete ds T") auto then have "ds = [] ∨ T = Leaf" using delete.elims by blast then show ?case by auto next case (Cons a p) then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto have "∃dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons branch_is_path by blast then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto then have "∃T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *) by (cases T; cases ds) auto then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto { assume a_p: "a" assume b_p: "¬b" have "branch (a # p) (delete ds T)" using Cons by - then have "branch (a # p) (Branching (T1) (delete ds' T2))" using b_p bds'_p T1T2_p by auto then have "branch p T1" using a_p by auto then have ?case using T1T2_p a_p by auto } moreover { assume a_p: "¬a" assume b_p: "b" have "branch (a # p) (delete ds T)" using Cons by - then have "branch (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto then have "branch p T2" using a_p by auto then have ?case using T1T2_p a_p by auto } moreover { assume a_p: "a" assume b_p: "b" have "branch (a # p) (delete ds T)" using Cons by - then have "branch (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto then have "branch p (delete ds' T1)" using a_p by auto then have "branch p T1 ∨ p = ds'" using Cons by metis then have ?case using T1T2_p a_p using bds'_p a_p b_p by auto } moreover { assume a_p: "¬a" assume b_p: "¬b" have "branch (a # p) (delete ds T)" using Cons by - then have "branch (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto then have "branch p (delete ds' T2)" using a_p by auto then have "branch p T2 ∨ p = ds'" using Cons by metis then have ?case using T1T2_p a_p using bds'_p a_p b_p by auto } ultimately show ?case by blast qed lemma branch_delete_postfix: assumes "path p (delete ds T)" shows "¬(∃c cs. p = ds @ c#cs)" (* Adapted from previous proof *) using assms proof (induction p arbitrary: T ds) case Nil then show ?case by simp next case (Cons a p) then obtain b ds' where bds'_p: "ds=b#ds'" by (cases ds) auto have "∃dT1 dT2. delete ds T = Branching dT1 dT2" using Cons path_inv_Cons by auto then obtain dT1 dT2 where "delete ds T = Branching dT1 dT2" by auto then have "∃T1 T2. T=Branching T1 T2" (* Is there a lemma hidden here that I could extract? *) by (cases T; cases ds) auto then obtain T1 T2 where T1T2_p: "T=Branching T1 T2" by auto { assume a_p: "a" assume b_p: "¬b" then have ?case using T1T2_p a_p b_p bds'_p by auto } moreover { assume a_p: "¬a" assume b_p: "b" then have ?case using T1T2_p a_p b_p bds'_p by auto } moreover { assume a_p: "a" assume b_p: "b" have "path (a # p) (delete ds T)" using Cons by - then have "path (a # p) (Branching (delete ds' T1) T2)" using b_p bds'_p T1T2_p by auto then have "path p (delete ds' T1)" using a_p by auto then have "¬ (∃c cs. p = ds' @ c # cs)" using Cons by auto then have ?case using T1T2_p a_p b_p bds'_p by auto } moreover { assume a_p: "¬a" assume b_p: "¬b" have "path (a # p) (delete ds T)" using Cons by - then have "path (a # p) (Branching T1 (delete ds' T2))" using b_p bds'_p T1T2_p by auto then have "path p (delete ds' T2)" using a_p by auto then have "¬ (∃c cs. p = ds' @ c # cs)" using Cons by auto then have ?case using T1T2_p a_p b_p bds'_p by auto } ultimately show ?case by blast qed lemma treezise_delete: assumes "internal p T" shows "treesize (delete p T) < treesize T" using assms proof (induction p arbitrary: T) case (Nil) then have "∃T1 T2. T = Branching T1 T2" by (cases T) auto then obtain T1 T2 where T1T2_p: "T = Branching T1 T2" by auto then show ?case by auto next case (Cons a p) then have "∃T1 T2. T = Branching T1 T2" using path_inv_Cons internal_is_path by blast then obtain T1 T2 where T1T2_p: "T = Branching T1 T2" by auto show ?case proof (cases a) assume a_p: a from a_p have "delete (a#p) T = (Branching (delete p T1) T2)" using T1T2_p by auto moreover from a_p have "internal p T1" using T1T2_p Cons by auto then have "treesize (delete p T1) < treesize T1" using Cons by auto ultimately show ?thesis using T1T2_p by auto next assume a_p: "¬a" from a_p have "delete (a#p) T = (Branching T1 (delete p T2))" using T1T2_p by auto moreover from a_p have "internal p T2" using T1T2_p Cons by auto then have "treesize (delete p T2) < treesize T2" using Cons by auto ultimately show ?thesis using T1T2_p by auto qed qed fun cutoff :: "(dir list ⇒ bool) ⇒ dir list ⇒ tree ⇒ tree" where "cutoff red ds (Branching T⇩_{1}T⇩_{2}) = (if red ds then Leaf else Branching (cutoff red (ds@[Left]) T⇩_{1}) (cutoff red (ds@[Right]) T⇩_{2}))" | "cutoff red ds Leaf = Leaf" text ‹Initially you should call @{const cutoff} with @{term "ds = []"}. If all branches are red, then @{const cutoff} gives a subtree. If all branches are red, then so are the ones in @{const cutoff}. The internal paths of @{const cutoff} are not red.› lemma treesize_cutoff: "treesize (cutoff red ds T) ≤ treesize T" proof (induction T arbitrary: ds) case Leaf then show ?case by auto next case (Branching T1 T2) then have "treesize (cutoff red (ds@[Left]) T1) + treesize (cutoff red (ds@[Right]) T2) ≤ treesize T1 + treesize T2" using add_mono by blast then show ?case by auto qed abbreviation anypath :: "tree ⇒ (dir list ⇒ bool) ⇒ bool" where "anypath T P ≡ ∀p. path p T ⟶ P p" abbreviation anybranch :: "tree ⇒ (dir list ⇒ bool) ⇒ bool" where "anybranch T P ≡ ∀p. branch p T ⟶ P p" abbreviation anyinternal :: "tree ⇒ (dir list ⇒ bool) ⇒ bool" where "anyinternal T P ≡ ∀p. internal p T ⟶ P p" lemma cutoff_branch': assumes "anybranch T (λb. red(ds@b))" shows "anybranch (cutoff red ds T) (λb. red(ds@b))" using assms proof (induction T arbitrary: ds) (* This proof seems a bit excessive for such a simple theorem *) case (Leaf) let ?T = "cutoff red ds Leaf" { fix b assume "branch b ?T" then have "branch b Leaf" by auto then have "red(ds@b)" using Leaf by auto } then show ?case by simp next case (Branching T⇩_{1}T⇩_{2}) let ?T = "cutoff red ds (Branching T⇩_{1}T⇩_{2})" from Branching have "∀p. branch (Left#p) (Branching T⇩_{1}T⇩_{2}) ⟶ red (ds @ (Left#p))" by blast then have "∀p. branch p T⇩_{1}⟶ red (ds @ (Left#p))" by auto then have "anybranch T⇩_{1}(λp. red ((ds @ [Left]) @ p))" by auto then have aa: "anybranch (cutoff red (ds @ [Left]) T⇩_{1}) (λp. red ((ds @ [Left]) @ p)) " using Branching by blast from Branching have "∀p. branch (Right#p) (Branching T⇩_{1}T⇩_{2}) ⟶ red (ds @ (Right#p))" by blast then have "∀p. branch p T⇩_{2}⟶ red (ds @ (Right#p))" by auto then have "anybranch T⇩_{2}(λp. red ((ds @ [Right]) @ p))" by auto then have bb: "anybranch (cutoff red (ds @ [Right]) T⇩_{2}) (λp. red ((ds @ [Right]) @ p)) " using Branching by blast { fix b assume b_p: "branch b ?T" have "red ds ∨ ¬red ds" by auto then have "red(ds@b)" proof assume ds_p: "red ds" then have "?T = Leaf" by auto then have "b = []" using b_p branch_inv_Leaf by auto then show "red(ds@b)" using ds_p by auto next assume ds_p: "¬red ds" let ?T⇩_{1}' = "cutoff red (ds@[Left]) T⇩_{1}" let ?T⇩_{2}' = "cutoff red (ds@[Right]) T⇩_{2}" from ds_p have "?T = Branching ?T⇩_{1}' ?T⇩_{2}'" by auto from this b_p obtain a b' where "b = a # b' ∧ (a ⟶ branch b' ?T⇩_{1}') ∧ (¬a ⟶ branch b' ?T⇩_{2}' )" using branch_inv_Branching[of b ?T⇩_{1}' ?T⇩_{2}'] by auto then show "red(ds@b)" using aa bb by (cases a) auto qed } then show ?case by blast qed lemma cutoff_branch: assumes "anybranch T (λp. red p)" shows "anybranch (cutoff red [] T) (λp. red p)" using assms cutoff_branch'[of T red "[]"] by auto lemma cutoff_internal': assumes "anybranch T (λb. red(ds@b))" shows "anyinternal (cutoff red ds T) (λb. ¬red(ds@b))" using assms proof (induction T arbitrary: ds) (* This proof seems a bit excessive for such a simple theorem *) case (Leaf) then show ?case using internal_inv_Leaf by simp next case (Branching T⇩_{1}T⇩_{2}) let ?T = "cutoff red ds (Branching T⇩_{1}T⇩_{2})" from Branching have "∀p. branch (Left#p) (Branching T⇩_{1}T⇩_{2}) ⟶ red (ds @ (Left#p))" by blast then have "∀p. branch p T⇩_{1}⟶ red (ds @ (Left#p))" by auto then have "anybranch T⇩_{1}(λp. red ((ds @ [Left]) @ p))" by auto then have aa: "anyinternal (cutoff red (ds @ [Left]) T⇩_{1}) (λp. ¬ red ((ds @ [Left]) @ p))" using Branching by blast from Branching have "∀p. branch (Right#p) (Branching T⇩_{1}T⇩_{2}) ⟶ red (ds @ (Right#p))" by blast then have "∀p. branch p T⇩_{2}⟶ red (ds @ (Right#p))" by auto then have "anybranch T⇩_{2}(λp. red ((ds @ [Right]) @ p))" by auto then have bb: "anyinternal (cutoff red (ds @ [Right]) T⇩_{2}) (λp. ¬ red ((ds @ [Right]) @ p))" using Branching by blast { fix p assume b_p: "internal p ?T" then have ds_p: "¬red ds" using internal_inv_Leaf by auto have "p=[] ∨ p≠[]" by auto then have "¬red(ds@p)" proof assume "p=[]" then show "¬red(ds@p)" using ds_p by auto next let ?T⇩_{1}' = "cutoff red (ds@[Left]) T⇩_{1}" let ?T⇩_{2}' = "cutoff red (ds@[Right]) T⇩_{2}" assume "p≠[]" moreover have "?T = Branching ?T⇩_{1}' ?T⇩_{2}'" using ds_p by auto ultimately obtain a p' where b_p: "p = a # p' ∧ (a ⟶ internal p' (cutoff red (ds @ [Left]) T⇩_{1})) ∧ (¬ a ⟶ internal p' (cutoff red (ds @ [Right]) T⇩_{2}))" using b_p internal_inv_Branching[of p ?T⇩_{1}' ?T⇩_{2}'] by auto then have "¬red(ds @ [a] @ p')" using aa bb by (cases a) auto then show "¬red(ds @ p)" using b_p by simp qed } then show ?case by blast qed lemma cutoff_internal: assumes "anybranch T red" shows "anyinternal (cutoff red [] T) (λp. ¬red p)" using assms cutoff_internal'[of T red "[]"] by auto lemma cutoff_branch_internal': assumes "anybranch T red" shows "anyinternal (cutoff red [] T) (λp. ¬red p) ∧ anybranch (cutoff red [] T) (λp. red p)" using assms cutoff_internal[of T] cutoff_branch[of T] by blast lemma cutoff_branch_internal: assumes "anybranch T red" shows "∃T'. anyinternal T' (λp. ¬red p) ∧ anybranch T' (λp. red p)" using assms cutoff_branch_internal' by blast section ‹Possibly Infinite Trees› text ‹Possibly infinite trees are of type @{typ "dir list set"}.› abbreviation wf_tree :: "dir list set ⇒ bool" where "wf_tree T ≡ (∀ds d. (ds @ d) ∈ T ⟶ ds ∈ T)" text ‹The subtree in with root r› fun subtree :: "dir list set ⇒ dir list ⇒ dir list set" where "subtree T r = {ds ∈ T. ∃ds'. ds = r @ ds'}" text ‹A subtree of a tree is either in the left branch, the right branch, or is the tree itself› lemma subtree_pos: "subtree T ds ⊆ subtree T (ds @ [Left]) ∪ subtree T (ds @ [Right]) ∪ {ds}" proof (rule subsetI; rule Set.UnCI) let ?subtree = "subtree T" fix x assume asm: "x ∈ ?subtree ds" assume "x ∉ {ds}" then have "x ≠ ds" by simp then have "∃e d. x = ds @ [d] @ e" using asm list.exhaust by auto then have "(∃e. x = ds @ [Left] @ e) ∨ (∃e. x = ds @ [Right] @ e)" using bool.exhaust by auto then show "x ∈ ?subtree (ds @ [Left]) ∪ ?subtree (ds @ [Right])" using asm by auto qed subsection ‹Infinite Paths› abbreviation wf_infpath :: "(nat ⇒ 'a list) ⇒ bool" where "wf_infpath f ≡ (f 0 = []) ∧ (∀n. ∃a. f (Suc n) = (f n) @ [a])" lemma infpath_length: assumes "wf_infpath f" shows "length (f n) = n" using assms proof (induction n) case 0 then show ?case by auto next case (Suc n) then show ?case by (metis length_append_singleton) qed lemma chain_prefix: assumes "wf_infpath f" assumes "n⇩_{1}≤ n⇩_{2}" shows "∃a. (f n⇩_{1}) @ a = (f n⇩_{2})" using assms proof (induction n⇩_{2}) case (Suc n⇩_{2}) then have "n⇩_{1}≤ n⇩_{2}∨ n⇩_{1}= Suc n⇩_{2}" by auto then show ?case proof assume "n⇩_{1}≤ n⇩_{2}" then obtain a where a: "f n⇩_{1}@ a = f n⇩_{2}" using Suc by auto have b: "∃b. f (Suc n⇩_{2}) = f n⇩_{2}@ [b]" using Suc by auto from a b have "∃b. f n⇩_{1}@ (a @ [b]) = f (Suc n⇩_{2})" by auto then show "∃c. f n⇩_{1}@ c = f (Suc n⇩_{2})" by blast next assume "n⇩_{1}= Suc n⇩_{2}" then have "f n⇩_{1}@ [] = f (Suc n⇩_{2})" by auto then show "∃a. f n⇩_{1}@ a = f (Suc n⇩_{2})" by auto qed qed auto text ‹If we make a lookup in a list, then looking up in an extension gives us the same value.› lemma ith_in_extension: assumes chain: "wf_infpath f" assumes smalli: "i < length (f n⇩_{1})" assumes n⇩_{1}n⇩_{2}: "n⇩_{1}≤ n⇩_{2}" shows "f n⇩_{1}! i = f n⇩_{2}! i" proof - from chain n⇩_{1}n⇩_{2}have "∃a. f n⇩_{1}@ a = f n⇩_{2}" using chain_prefix by blast then obtain a where a_p: "f n⇩_{1}@ a = f n⇩_{2}" by auto have "(f n⇩_{1}@ a) ! i = f n⇩_{1}! i" using smalli by (simp add: nth_append) then show ?thesis using a_p by auto qed section ‹König's Lemma› lemma inf_subs: assumes inf: "¬finite(subtree T ds)" shows "¬finite(subtree T (ds @ [Left])) ∨ ¬finite(subtree T (ds @ [Right]))" proof - let ?subtree = "subtree T" { assume asms: "finite(?subtree(ds @ [Left]))" "finite(?subtree(ds @ [Right]))" have "?subtree ds ⊆ ?subtree (ds @ [Left] ) ∪ ?subtree (ds @ [Right]) ∪ {ds} " using subtree_pos by auto then have "finite(?subtree (ds))" using asms by (simp add: finite_subset) } then show "¬finite(?subtree (ds @ [Left])) ∨ ¬finite(?subtree (ds @ [Right]))" using inf by auto qed fun buildchain :: "(dir list ⇒ dir list) ⇒ nat ⇒ dir list" where "buildchain next 0 = []" | "buildchain next (Suc n) = next (buildchain next n)" lemma konig: assumes inf: "¬finite T" assumes wellformed: "wf_tree T" shows "∃c. wf_infpath c ∧ (∀n. (c n) ∈ T)" proof let ?subtree = "subtree T" let ?nextnode = "λds. (if ¬finite (?subtree (ds @ [Left])) then ds @ [Left] else ds @ [Right])" let ?c = "buildchain ?nextnode" have is_chain: "wf_infpath ?c" by auto from wellformed have prefix: "∀ds d. (ds @ d) ∈ T ⟶ ds ∈ T" by blast { fix n have "(?c n) ∈ T ∧ ¬finite (?subtree (?c n))" proof (induction n) case 0 have "∃ds. ds ∈ T" using inf by (simp add: not_finite_existsD) then obtain ds where "ds ∈ T" by auto then have "([]@ds) ∈ T" by auto then have "[] ∈ T" using prefix by blast then show ?case using inf by auto next case (Suc n) from Suc have next_in: "(?c n) ∈ T" by auto from Suc have next_inf: "¬finite (?subtree (?c n))" by auto from next_inf have next_next_inf: "¬finite (?subtree (?nextnode (?c n)))" using inf_subs by auto then have "∃ds. ds ∈ ?subtree (?nextnode (?c n))" by (simp add: not_finite_existsD) then obtain ds where dss: "ds ∈ ?subtree (?nextnode (?c n))" by auto then have "ds ∈ T" "∃suf. ds = (?nextnode (?c n)) @ suf" by auto then obtain suf where "ds ∈ T ∧ ds = (?nextnode (?c n)) @ suf" by auto then have "(?nextnode (?c n)) ∈ T" using prefix by blast then have "(?c (Suc n)) ∈ T" by auto then show ?case using next_next_inf by auto qed } then show "wf_infpath ?c ∧ (∀n. (?c n)∈ T) " using is_chain by auto qed end

# Theory Resolution

section ‹More Terms and Literals› theory Resolution imports TermsAndLiterals Tree begin fun complement :: "'t literal ⇒ 't literal" ("_⇧^{c}" [300] 300) where "(Pos P ts)⇧^{c}= Neg P ts" | "(Neg P ts)⇧^{c}= Pos P ts" lemma cancel_comp1: "(l⇧^{c})⇧^{c}= l" by (cases l) auto lemma cancel_comp2: assumes asm: "l⇩_{1}⇧^{c}= l⇩_{2}⇧^{c}" shows "l⇩_{1}= l⇩_{2}" proof - from asm have "(l⇩_{1}⇧^{c})⇧^{c}= (l⇩_{2}⇧^{c})⇧^{c}" by auto then have "l⇩_{1}= (l⇩_{2}⇧^{c})⇧^{c}" using cancel_comp1[of l⇩_{1}] by auto then show ?thesis using cancel_comp1[of l⇩_{2}] by auto qed lemma comp_exi1: "∃l'. l' = l⇧^{c}" by (cases l) auto lemma comp_exi2: "∃l. l' = l⇧^{c}" proof show "l' = (l'⇧^{c})⇧^{c}" using cancel_comp1[of l'] by auto qed lemma comp_swap: "l⇩_{1}⇧^{c}= l⇩_{2}⟷ l⇩_{1}= l⇩_{2}⇧^{c}" proof - have "l⇩_{1}⇧^{c}= l⇩_{2}⟶ l⇩_{1}= l⇩_{2}⇧^{c}" using cancel_comp1[of l⇩_{1}] by auto moreover have "l⇩_{1}= l⇩_{2}⇧^{c}⟶ l⇩_{1}⇧^{c}= l⇩_{2}" using cancel_comp1 by auto ultimately show ?thesis by auto qed lemma sign_comp: "sign l⇩_{1}≠ sign l⇩_{2}∧ get_pred l⇩_{1}= get_pred l⇩_{2}∧ get_terms l⇩_{1}= get_terms l⇩_{2}⟷ l⇩_{2}= l⇩_{1}⇧^{c}" by (cases l⇩_{1}; cases l⇩_{2}) auto lemma sign_comp_atom: "sign l⇩_{1}≠ sign l⇩_{2}∧ get_atom l⇩_{1}= get_atom l⇩_{2}⟷ l⇩_{2}= l⇩_{1}⇧^{c}" by (cases l⇩_{1}; cases l⇩_{2}) auto section ‹Clauses› type_synonym 't clause = "'t literal set" abbreviation complementls :: "'t literal set ⇒ 't literal set" ("_⇧^{C}" [300] 300) where "L⇧^{C}≡ complement ` L" lemma cancel_compls1: "(L⇧^{C})⇧^{C}= L" apply (auto simp add: cancel_comp1) apply (metis imageI cancel_comp1) done lemma cancel_compls2: assumes asm: "L⇩_{1}⇧^{C}= L⇩_{2}⇧^{C}" shows "L⇩_{1}= L⇩_{2}" proof - from asm have "(L⇩_{1}⇧^{C})⇧^{C}= (L⇩_{2}⇧^{C})⇧^{C}" by auto then show ?thesis using cancel_compls1[of L⇩_{1}] cancel_compls1[of L⇩_{2}] by simp qed fun vars⇩_{t}:: "fterm ⇒ var_sym set" where "vars⇩_{t}(Var x) = {x}" | "vars⇩_{t}(Fun f ts) = (⋃t ∈ set ts. vars⇩_{t}t)" abbreviation vars⇩_{t}⇩_{s}:: "fterm list ⇒ var_sym set" where "vars⇩_{t}⇩_{s}ts ≡ (⋃t ∈ set ts. vars⇩_{t}t)" definition vars⇩_{l}:: "fterm literal ⇒ var_sym set" where "vars⇩_{l}l = vars⇩_{t}⇩_{s}(get_terms l)" definition vars⇩_{l}⇩_{s}:: "fterm literal set ⇒ var_sym set" where "vars⇩_{l}⇩_{s}L ≡ ⋃l∈L. vars⇩_{l}l" lemma ground_vars⇩_{t}: assumes "ground⇩_{t}t" shows "vars⇩_{t}t = {}" using assms by (induction t) auto lemma ground⇩_{t}⇩_{s}_vars⇩_{t}⇩_{s}: assumes "ground⇩_{t}⇩_{s}ts" shows "vars⇩_{t}⇩_{s}ts = {}" using assms ground_vars⇩_{t}by auto lemma ground⇩_{l}_vars⇩_{l}: assumes "ground⇩_{l}l" shows "vars⇩_{l}l = {}" unfolding vars⇩_{l}_def using assms ground_vars⇩_{t}by auto lemma ground⇩_{l}⇩_{s}_vars⇩_{l}⇩_{s}: assumes "ground⇩_{l}⇩_{s}L" shows "vars⇩_{l}⇩_{s}L = {}" unfolding vars⇩_{l}⇩_{s}_def using assms ground⇩_{l}_vars⇩_{l}by auto lemma ground_comp: "ground⇩_{l}(l⇧^{c}) ⟷ ground⇩_{l}l" by (cases l) auto lemma ground_compls: "ground⇩_{l}⇩_{s}(L⇧^{C}) ⟷ ground⇩_{l}⇩_{s}L" using ground_comp by auto (* Alternative - Collect variables with vars and see if empty set *) section ‹Semantics› type_synonym 'u fun_denot = "fun_sym ⇒ 'u list ⇒ 'u" type_synonym 'u pred_denot = "pred_sym ⇒ 'u list ⇒ bool" type_synonym 'u var_denot = "var_sym ⇒ 'u" fun eval⇩_{t}:: "'u var_denot ⇒ 'u fun_denot ⇒ fterm ⇒ 'u" where "eval⇩_{t}E F (Var x) = E x" | "eval⇩_{t}E F (Fun f ts) = F f (map (eval⇩_{t}E F) ts)" abbreviation eval⇩_{t}⇩_{s}:: "'u var_denot ⇒ 'u fun_denot ⇒ fterm list ⇒ 'u list" where "eval⇩_{t}⇩_{s}E F ts ≡ map (eval⇩_{t}E F) ts" fun eval⇩_{l}:: "'u var_denot ⇒ 'u fun_denot ⇒ 'u pred_denot ⇒ fterm literal ⇒ bool" where "eval⇩_{l}E F G (Pos p ts) ⟷ G p (eval⇩_{t}⇩_{s}E F ts)" | "eval⇩_{l}E F G (Neg p ts) ⟷ ¬G p (eval⇩_{t}⇩_{s}E F ts)" definition eval⇩_{c}:: "'u fun_denot ⇒ 'u pred_denot ⇒ fterm clause ⇒ bool" where "eval⇩_{c}F G C ⟷ (∀E. ∃l ∈ C. eval⇩_{l}E F G l)" definition eval⇩_{c}⇩_{s}:: "'u fun_denot ⇒ 'u pred_denot ⇒ fterm clause set ⇒ bool" where "eval⇩_{c}⇩_{s}F G Cs ⟷ (∀C ∈ Cs. eval⇩_{c}F G C)" subsection ‹Semantics of Ground Terms› lemma ground_var_denott: assumes "ground⇩_{t}t" shows "eval⇩_{t}E F t = eval⇩_{t}E' F t" using assms proof (induction t) case (Var x) then have "False" by auto then show ?case by auto next case (Fun f ts) then have "∀t ∈ set ts. ground⇩_{t}t" by auto then have "∀t ∈ set ts. eval⇩_{t}E F t = eval⇩_{t}E' F t" using Fun by auto then have "eval⇩_{t}⇩_{s}E F ts = eval⇩_{t}⇩_{s}E' F ts" by auto then have "F f (map (eval⇩_{t}E F) ts) = F f (map (eval⇩_{t}E' F) ts)" by metis then show ?case by simp qed lemma ground_var_denotts: assumes "ground⇩_{t}⇩_{s}ts" shows "eval⇩_{t}⇩_{s}E F ts = eval⇩_{t}⇩_{s}E' F ts" using assms ground_var_denott by (metis map_eq_conv) lemma ground_var_denot: assumes "ground⇩_{l}l" shows "eval⇩_{l}E F G l = eval⇩_{l}E' F G l" using assms proof (induction l) case Pos then show ?case using ground_var_denotts by (metis eval⇩_{l}.simps(1) literal.sel(3)) next case Neg then show ?case using ground_var_denotts by (metis eval⇩_{l}.simps(2) literal.sel(4)) qed section ‹Substitutions› type_synonym substitution = "var_sym ⇒ fterm" fun sub :: "fterm ⇒ substitution ⇒ fterm" (infixl "⋅⇩_{t}" 55) where "(Var x) ⋅⇩_{t}σ = σ x" | "(Fun f ts) ⋅⇩_{t}σ = Fun f (map (λt. t ⋅⇩_{t}σ) ts)" abbreviation subs :: "fterm list ⇒ substitution ⇒ fterm list" (infixl "⋅⇩_{t}⇩_{s}" 55) where "ts ⋅⇩_{t}⇩_{s}σ ≡ (map (λt. t ⋅⇩_{t}σ) ts)" fun subl :: "fterm literal ⇒ substitution ⇒ fterm literal" (infixl "⋅⇩_{l}" 55) where "(Pos p ts) ⋅⇩_{l}σ = Pos p (ts ⋅⇩_{t}⇩_{s}σ)" | "(Neg p ts) ⋅⇩_{l}σ = Neg p (ts ⋅⇩_{t}⇩_{s}σ)" abbreviation subls :: "fterm literal set ⇒ substitution ⇒ fterm literal set" (infixl "⋅⇩_{l}⇩_{s}" 55) where "L ⋅⇩_{l}⇩_{s}σ ≡ (λl. l ⋅⇩_{l}σ) ` L" lemma subls_def2: "L ⋅⇩_{l}⇩_{s}σ = {l ⋅⇩_{l}σ|l. l ∈ L}" by auto definition instance_of⇩_{t}:: "fterm ⇒ fterm ⇒ bool" where "instance_of⇩_{t}t⇩_{1}t⇩_{2}⟷ (∃σ. t⇩_{1}= t⇩_{2}⋅⇩_{t}σ)" definition instance_of⇩_{t}⇩_{s}:: "fterm list ⇒ fterm list ⇒ bool" where "instance_of⇩_{t}⇩_{s}ts⇩_{1}ts⇩_{2}⟷ (∃σ. ts⇩_{1}= ts⇩_{2}⋅⇩_{t}⇩_{s}σ)" definition instance_of⇩_{l}:: "fterm literal ⇒ fterm literal ⇒ bool" where "instance_of⇩_{l}l⇩_{1}l⇩_{2}⟷ (∃σ. l⇩_{1}= l⇩_{2}⋅⇩_{l}σ)" definition instance_of⇩_{l}⇩_{s}:: "fterm clause ⇒ fterm clause ⇒ bool" where "instance_of⇩_{l}⇩_{s}C⇩_{1}C⇩_{2}⟷ (∃σ. C⇩_{1}= C⇩_{2}⋅⇩_{l}⇩_{s}σ)" lemma comp_sub: "(l⇧^{c}) ⋅⇩_{l}σ=(l ⋅⇩_{l}σ)⇧^{c}" by (cases l) auto lemma compls_subls: "(L⇧^{C}) ⋅⇩_{l}⇩_{s}σ=(L ⋅⇩_{l}⇩_{s}σ)⇧^{C}" using comp_sub apply auto apply (metis image_eqI) done lemma subls_union: "(L⇩_{1}∪ L⇩_{2}) ⋅⇩_{l}⇩_{s}σ = (L⇩_{1}⋅⇩_{l}⇩_{s}σ) ∪ (L⇩_{2}⋅⇩_{l}⇩_{s}σ)" by auto (* Alternative: apply a substitution that is a bijection between the set of variables in C1 and some other set. *) definition var_renaming_of :: "fterm clause ⇒ fterm clause ⇒ bool" where "var_renaming_of C⇩_{1}C⇩_{2}⟷ instance_of⇩_{l}⇩_{s}C⇩_{1}C⇩_{2}∧ instance_of⇩_{l}⇩_{s}C⇩_{2}C⇩_{1}" subsection ‹The Empty Substitution› abbreviation ε :: "substitution" where "ε ≡ Var" lemma empty_subt: "(t :: fterm) ⋅⇩_{t}ε = t" by (induction t) (auto simp add: map_idI) lemma empty_subts: "ts ⋅⇩_{t}⇩_{s}ε = ts" using empty_subt by auto lemma empty_subl: "l ⋅⇩_{l}ε = l" using empty_subts by (cases l) auto lemma empty_subls: "L ⋅⇩_{l}⇩_{s}ε = L" using empty_subl by auto lemma instance_of⇩_{t}_self: "instance_of⇩_{t}t t" unfolding instance_of⇩_{t}_def proof show "t = t ⋅⇩_{t}ε" using empty_subt by auto qed lemma instance_of⇩_{t}⇩_{s}_self: "instance_of⇩_{t}⇩_{s}ts ts" unfolding instance_of⇩_{t}⇩_{s}_def proof show "ts = ts ⋅⇩_{t}⇩_{s}ε" using empty_subts by auto qed lemma instance_of⇩_{l}_self: "instance_of⇩_{l}l l" unfolding instance_of⇩_{l}_def proof show "l = l ⋅⇩_{l}ε" using empty_subl by auto qed lemma instance_of⇩_{l}⇩_{s}_self: "instance_of⇩_{l}⇩_{s}L L" unfolding instance_of⇩_{l}⇩_{s}_def proof show "L = L ⋅⇩_{l}⇩_{s}ε" using empty_subls by auto qed subsection ‹Substitutions and Ground Terms› lemma ground_sub: assumes "ground⇩_{t}t" shows "t ⋅⇩_{t}σ = t" using assms by (induction t) (auto simp add: map_idI) lemma ground_subs: assumes "ground⇩_{t}⇩_{s}ts " shows " ts ⋅⇩_{t}⇩_{s}σ = ts" using assms ground_sub by (simp add: map_idI) lemma ground⇩_{l}_subs: assumes "ground⇩_{l}l " shows " l ⋅⇩_{l}σ = l" using assms ground_subs by (cases l) auto lemma ground⇩_{l}⇩_{s}_subls: assumes ground: "ground⇩_{l}⇩_{s}L" shows "L ⋅⇩_{l}⇩_{s}σ = L" proof - { fix l assume l_L: "l ∈ L" then have "ground⇩_{l}l" using ground by auto then have "l = l ⋅⇩_{l}σ" using ground⇩_{l}_subs by auto moreover then have "l ⋅⇩_{l}σ ∈ L ⋅⇩_{l}⇩_{s}σ" using l_L by auto ultimately have "l ∈ L ⋅⇩_{l}⇩_{s}σ" by auto } moreover { fix l assume l_L: "l ∈ L ⋅⇩_{l}⇩_{s}σ" then obtain l' where l'_p: "l' ∈ L ∧ l' ⋅⇩_{l}σ = l" by auto then have "l' = l" using ground ground⇩_{l}_subs by auto from l_L l'_p this have "l ∈ L" by auto } ultimately show ?thesis by auto qed subsection ‹Composition› definition composition :: "substitution ⇒ substitution ⇒ substitution" (infixl "⋅" 55) where "(σ⇩_{1}⋅ σ⇩_{2}) x = (σ⇩_{1}x) ⋅⇩_{t}σ⇩_{2}" lemma composition_conseq2t: "(t ⋅⇩_{t}σ⇩_{1}) ⋅⇩_{t}σ⇩_{2}= t ⋅⇩_{t}(σ⇩_{1}⋅ σ⇩_{2})" proof (induction t) case (Var x) have "((Var x) ⋅⇩_{t}σ⇩_{1}) ⋅⇩_{t}σ⇩_{2}= (σ⇩_{1}x) ⋅⇩_{t}σ⇩_{2}" by simp also have " ... = (σ⇩_{1}⋅ σ⇩_{2}) x" unfolding composition_def by simp finally show ?case by auto next case (Fun t ts) then show ?case unfolding composition_def by auto qed lemma composition_conseq2ts: "(ts ⋅⇩_{t}⇩_{s}σ⇩_{1}) ⋅⇩_{t}⇩_{s}σ⇩_{2}= ts ⋅⇩_{t}⇩_{s}(σ⇩_{1}⋅ σ⇩_{2})" using composition_conseq2t by auto lemma composition_conseq2l: "(l ⋅⇩_{l}σ⇩_{1}) ⋅⇩_{l}σ⇩_{2}= l ⋅⇩_{l}(σ⇩_{1}⋅ σ⇩_{2})" using composition_conseq2t by (cases l) auto lemma composition_conseq2ls: "(L ⋅⇩_{l}⇩_{s}σ⇩_{1}) ⋅⇩_{l}⇩_{s}σ⇩_{2}= L ⋅⇩_{l}⇩_{s}(σ⇩_{1}⋅ σ⇩_{2})" using composition_conseq2l apply auto apply (metis imageI) done lemma composition_assoc: "σ⇩_{1}⋅ (σ⇩_{2}⋅ σ⇩_{3}) = (σ⇩_{1}⋅ σ⇩_{2}) ⋅ σ⇩_{3}" proof fix x show "(σ⇩_{1}⋅ (σ⇩_{2}⋅ σ⇩_{3})) x = ((σ⇩_{1}⋅ σ⇩_{2}) ⋅ σ⇩_{3}) x" by (simp only: composition_def composition_conseq2t) qed lemma empty_comp1: "(σ ⋅ ε) = σ" proof fix x show "(σ ⋅ ε) x = σ x" unfolding composition_def using empty_subt by auto qed lemma empty_comp2: "(ε ⋅ σ) = σ" proof fix x show "(ε ⋅ σ) x = σ x" unfolding composition_def by simp qed lemma instance_of⇩_{t}_trans : assumes t⇩_{1}⇩_{2}: "instance_of⇩_{t}t⇩_{1}t⇩_{2}" assumes t⇩_{2}⇩_{3}: "instance_of⇩_{t}t⇩_{2}t⇩_{3}" shows "instance_of⇩_{t}t⇩_{1}t⇩_{3}" proof - from t⇩_{1}⇩_{2}obtain σ⇩_{1}⇩_{2}where "t⇩_{1}= t⇩_{2}⋅⇩_{t}σ⇩_{1}⇩_{2}" unfolding instance_of⇩_{t}_def by auto moreover from t⇩_{2}⇩_{3}obtain σ⇩_{2}⇩_{3}where "t⇩_{2}= t⇩_{3}⋅⇩_{t}σ⇩_{2}⇩_{3}" unfolding instance_of⇩_{t}_def by auto ultimately have "t⇩_{1}= (t⇩_{3}⋅⇩_{t}σ⇩_{2}⇩_{3}) ⋅⇩_{t}σ⇩_{1}⇩_{2}" by auto then have "t⇩_{1}= t⇩_{3}⋅⇩_{t}(σ⇩_{2}⇩_{3}⋅ σ⇩_{1}⇩_{2})" using composition_conseq2t by simp then show ?thesis unfolding instance_of⇩_{t}_def by auto qed lemma instance_of⇩_{t}⇩_{s}_trans : assumes ts⇩_{1}⇩_{2}: "instance_of⇩_{t}⇩_{s}ts⇩_{1}ts⇩_{2}" assumes ts⇩_{2}⇩_{3}: "instance_of⇩_{t}⇩_{s}ts⇩_{2}ts⇩_{3}" shows "instance_of⇩_{t}⇩_{s}ts⇩_{1}ts⇩_{3}" proof - from ts⇩_{1}⇩_{2}obtain σ⇩_{1}⇩_{2}where "ts⇩_{1}= ts⇩_{2}⋅⇩_{t}⇩_{s}σ⇩_{1}⇩_{2}" unfolding instance_of⇩_{t}⇩_{s}_def by auto moreover from ts⇩_{2}⇩_{3}obtain σ⇩_{2}⇩_{3}where "ts⇩_{2}= ts⇩_{3}⋅⇩_{t}⇩_{s}σ⇩_{2}⇩_{3}" unfolding instance_of⇩_{t}⇩_{s}_def by auto ultimately have "ts⇩_{1}= (ts⇩_{3}⋅⇩_{t}⇩_{s}σ⇩_{2}⇩_{3}) ⋅⇩_{t}⇩_{s}σ⇩_{1}⇩_{2}" by auto then have "ts⇩_{1}= ts⇩_{3}⋅⇩_{t}⇩_{s}(σ⇩_{2}⇩_{3}⋅ σ⇩_{1}⇩_{2})" using composition_conseq2ts by simp then show ?thesis unfolding instance_of⇩_{t}⇩_{s}_def by auto qed lemma instance_of⇩_{l}_trans : assumes l⇩_{1}⇩_{2}: "instance_of⇩_{l}l⇩_{1}l⇩_{2}" assumes l⇩_{2}⇩_{3}: "instance_of⇩_{l}l⇩_{2}l⇩_{3}" shows "instance_of⇩_{l}l⇩_{1}l⇩_{3}" proof - from l⇩_{1}⇩_{2}obtain σ⇩_{1}⇩_{2}where "l⇩_{1}= l⇩_{2}⋅⇩_{l}σ⇩_{1}⇩_{2}" unfolding instance_of⇩_{l}_def by auto moreover from l⇩_{2}⇩_{3}obtain σ⇩_{2}⇩_{3}where "l⇩_{2}= l⇩_{3}⋅⇩_{l}σ⇩_{2}⇩_{3}" unfolding instance_of⇩_{l}_def by auto ultimately have "l⇩_{1}= (l⇩_{3}⋅⇩_{l}σ⇩_{2}⇩_{3}) ⋅⇩_{l}σ⇩_{1}⇩_{2}" by auto then have "l⇩_{1}= l⇩_{3}⋅⇩_{l}(σ⇩_{2}⇩_{3}⋅ σ⇩_{1}⇩_{2})" using composition_conseq2l by simp then show ?thesis unfolding instance_of⇩_{l}_def by auto qed lemma instance_of⇩_{l}⇩_{s}_trans : assumes L⇩_{1}⇩_{2}: "instance_of⇩_{l}⇩_{s}L⇩_{1}L⇩_{2}" assumes L⇩_{2}⇩_{3}: "instance_of⇩_{l}⇩_{s}L⇩_{2}L⇩_{3}" shows "instance_of⇩_{l}⇩_{s}L⇩_{1}L⇩_{3}" proof - from L⇩_{1}⇩_{2}obtain σ⇩_{1}⇩_{2}where "L⇩_{1}= L⇩_{2}⋅⇩_{l}⇩_{s}σ⇩_{1}⇩_{2}" unfolding instance_of⇩_{l}⇩_{s}_def by auto moreover from L⇩_{2}⇩_{3}obtain σ⇩_{2}⇩_{3}where "L⇩_{2}= L⇩_{3}⋅⇩_{l}⇩_{s}σ⇩_{2}⇩_{3}" unfolding instance_of⇩_{l}⇩_{s}_def by auto ultimately have "L⇩_{1}= (L⇩_{3}⋅⇩_{l}⇩_{s}σ⇩_{2}⇩_{3}) ⋅⇩_{l}⇩_{s}σ⇩_{1}⇩_{2}" by auto then have "L⇩_{1}= L⇩_{3}⋅⇩_{l}⇩_{s}(σ⇩_{2}⇩_{3}⋅ σ⇩_{1}⇩_{2})" using composition_conseq2ls by simp then show ?thesis unfolding instance_of⇩_{l}⇩_{s}_def by auto qed subsection ‹Merging substitutions› lemma project_sub: assumes inst_C:"C ⋅⇩_{l}⇩_{s}lmbd = C'" assumes L'sub: "L' ⊆ C'" shows "∃L ⊆ C. L ⋅⇩_{l}⇩_{s}lmbd = L' ∧ (C-L) ⋅⇩_{l}⇩_{s}lmbd = C' - L'" proof - let ?L = "{l ∈ C. ∃l' ∈ L'. l ⋅⇩_{l}lmbd = l'}" have "?L ⊆ C" by auto moreover have "?L ⋅⇩_{l}⇩_{s}lmbd = L'" proof (rule Orderings.order_antisym; rule Set.subsetI) fix l' assume l'L: "l' ∈ L'" from inst_C have "{l ⋅⇩_{l}lmbd|l. l ∈ C} = C'" unfolding subls_def2 by - then have "∃l. l' = l ⋅⇩_{l}lmbd ∧ l ∈ C ∧ l ⋅⇩_{l}lmbd ∈ L'" using L'sub l'L by auto then have " l' ∈ {l ∈ C. l ⋅⇩_{l}lmbd ∈ L'} ⋅⇩_{l}⇩_{s}lmbd" by auto then show " l' ∈ {l ∈ C. ∃l'∈L'. l ⋅⇩_{l}lmbd = l'} ⋅⇩_{l}⇩_{s}lmbd" by auto qed auto moreover have "(C-?L) ⋅⇩_{l}⇩_{s}lmbd = C' - L'" using inst_C by auto ultimately show ?thesis by blast qed lemma relevant_vars_subt: assumes "∀x ∈ vars⇩_{t}t. σ⇩_{1}x = σ⇩_{2}x" shows " t ⋅⇩_{t}σ⇩_{1}= t ⋅⇩_{t}σ⇩_{2}" using assms proof (induction t) case (Fun f ts) have f: "∀t. t ∈ set ts ⟶ vars⇩_{t}t ⊆ vars⇩_{t}⇩_{s}ts" by (induction ts) auto have "∀t∈set ts. t ⋅⇩_{t}σ⇩_{1}= t ⋅⇩_{t}σ⇩_{2}" proof fix t assume tints: "t ∈ set ts" then have "∀x ∈ vars⇩_{t}t. σ⇩_{1}x = σ⇩_{2}x" using f Fun(2) by auto then show "t ⋅⇩_{t}σ⇩_{1}= t ⋅⇩_{t}σ⇩_{2}" using Fun tints by auto qed then have "ts ⋅⇩_{t}⇩_{s}σ⇩_{1}= ts ⋅⇩_{t}⇩_{s}σ⇩_{2}" by auto then show ?case by auto qed auto lemma relevant_vars_subts: (* similar to above proof *) assumes asm: "∀x ∈ vars⇩_{t}⇩_{s}ts. σ⇩_{1}x = σ⇩_{2}x" shows "ts ⋅⇩_{t}⇩_{s}σ⇩_{1}= ts ⋅⇩_{t}⇩_{s}σ⇩_{2}" proof - have f: "∀t. t ∈ set ts ⟶ vars⇩_{t}t ⊆ vars⇩_{t}⇩_{s}ts" by (induction ts) auto have "∀t∈set ts. t ⋅⇩_{t}σ⇩_{1}= t ⋅⇩_{t}σ⇩_{2}" proof fix t assume tints: "t ∈ set ts" then have "∀x ∈ vars⇩_{t}t. σ⇩_{1}x = σ⇩_{2}x" using f asm by auto then show "t ⋅⇩_{t}σ⇩_{1}= t ⋅⇩_{t}σ⇩_{2}" using relevant_vars_subt tints by auto qed then show ?thesis by auto qed lemma relevant_vars_subl: assumes "∀x ∈ vars⇩_{l}l. σ⇩_{1}x = σ⇩_{2}x " shows "l ⋅⇩_{l}σ⇩_{1}= l ⋅⇩_{l}σ⇩_{2}" using assms proof (induction l) case (Pos p ts) then show ?case using relevant_vars_subts unfolding vars⇩_{l}_def by auto next case (Neg p ts) then show ?case using relevant_vars_subts unfolding vars⇩_{l}_def by auto qed lemma relevant_vars_subls: (* in many ways a mirror of relevant_vars_subts *) assumes asm: "∀x ∈ vars⇩_{l}⇩_{s}L. σ⇩_{1}x = σ⇩_{2}x" shows "L ⋅⇩_{l}⇩_{s}σ⇩_{1}= L ⋅⇩_{l}⇩_{s}σ⇩_{2}" proof - have f: "∀l. l ∈ L ⟶ vars⇩_{l}l ⊆ vars⇩_{l}⇩_{s}L" unfolding vars⇩_{l}⇩_{s}_def by auto have "∀l ∈ L. l ⋅⇩_{l}σ⇩_{1}= l ⋅⇩_{l}σ⇩_{2}" proof fix l assume linls: "l∈L" then have "∀x∈vars⇩_{l}l. σ⇩_{1}x = σ⇩_{2}x" using f asm by auto then show "l ⋅⇩_{l}σ⇩_{1}= l ⋅⇩_{l}σ⇩_{2}" using relevant_vars_subl linls by auto qed then show ?thesis by (meson image_cong) qed lemma merge_sub: assumes dist: "vars⇩_{l}⇩_{s}C ∩ vars⇩_{l}⇩_{s}D = {}" assumes CC': "C ⋅⇩_{l}⇩_{s}lmbd = C'" assumes DD': "D ⋅⇩_{l}⇩_{s}μ = D'" shows "∃η. C ⋅⇩_{l}⇩_{s}η = C' ∧ D ⋅⇩_{l}⇩_{s}η = D'" proof - let ?η = "λx. if x ∈ vars⇩_{l}⇩_{s}C then lmbd x else μ x" have " ∀x∈vars⇩_{l}⇩_{s}C. ?η x = lmbd x" by auto then have "C ⋅⇩_{l}⇩_{s}?η = C ⋅⇩_{l}⇩_{s}lmbd" using relevant_vars_subls[of C ?η lmbd] by auto then have "C ⋅⇩_{l}⇩_{s}?η = C'" using CC' by auto moreover have " ∀x ∈ vars⇩_{l}⇩_{s}D. ?η x = μ x" using dist by auto then have "D ⋅⇩_{l}⇩_{s}?η = D ⋅⇩_{l}⇩_{s}μ" using relevant_vars_subls[of D ?η μ] by auto then have "D ⋅⇩_{l}⇩_{s}?η = D'" using DD' by auto ultimately show ?thesis by auto qed subsection ‹Standardizing apart› abbreviation std⇩_{1}:: "fterm clause ⇒ fterm clause" where "std⇩_{1}C ≡ C ⋅⇩_{l}⇩_{s}(λx. Var (''1'' @ x))" abbreviation std⇩_{2}:: "fterm clause ⇒ fterm clause" where "std⇩_{2}C ≡ C ⋅⇩_{l}⇩_{s}(λx. Var (''2'' @ x))" lemma std_apart_apart'': assumes "x ∈ vars⇩_{t}(t ⋅⇩_{t}(λx::char list. Var (y @ x)))" shows "∃x'. x = y@x'" using assms by (induction t) auto lemma std_apart_apart': assumes "x ∈ vars⇩_{l}(l ⋅⇩_{l}(λx. Var (y@x)))" shows "∃x'. x = y@x'" using assms unfolding vars⇩_{l}_def using std_apart_apart'' by (cases l) auto lemma std_apart_apart: "vars⇩_{l}⇩_{s}(std⇩_{1}C⇩_{1}) ∩ vars⇩_{l}⇩_{s}(std⇩_{2}C⇩_{2}) = {}" proof - { fix x assume xin: "x ∈ vars⇩_{l}⇩_{s}(std⇩_{1}C⇩_{1}) ∩ vars⇩_{l}⇩_{s}(std⇩_{2}C⇩_{2})" from xin have "x ∈ vars⇩_{l}⇩_{s}(std⇩_{1}C⇩_{1})" by auto then have "∃x'. x=''1'' @ x'" using std_apart_apart'[of x _ "''1''"] unfolding vars⇩_{l}⇩_{s}_def by auto moreover from xin have "x ∈ vars⇩_{l}⇩_{s}(std⇩_{2}C⇩_{2})" by auto then have "∃x'. x= ''2'' @x' " using std_apart_apart'[of x _ "''2''"] unfolding vars⇩_{l}⇩_{s}_def by auto ultimately have "False" by auto then have "x ∈ {}" by auto } then show ?thesis by auto qed lemma std_apart_instance_of⇩_{l}⇩_{s}1: "instance_of⇩_{l}⇩_{s}C⇩_{1}(std⇩_{1}C⇩_{1})" proof - have empty: "(λx. Var (''1''@x)) ⋅ (λx. Var (tl x)) = ε" using composition_def by auto have "C⇩_{1}⋅⇩_{l}⇩_{s}ε = C⇩_{1}" using empty_subls by auto then have "C⇩_{1}⋅⇩_{l}⇩_{s}((λx. Var (''1''@x)) ⋅ (λx. Var (tl x))) = C⇩_{1}" using empty by auto then have "(C⇩_{1}⋅⇩_{l}⇩_{s}(λx. Var (''1''@x))) ⋅⇩_{l}⇩_{s}(λx. Var (tl x)) = C⇩_{1}" using composition_conseq2ls by auto then have "C⇩_{1}= (std⇩_{1}C⇩_{1}) ⋅⇩_{l}⇩_{s}(λx. Var (tl x))" by auto then show "instance_of⇩_{l}⇩_{s}C⇩_{1}(std⇩_{1}C⇩_{1})" unfolding instance_of⇩_{l}⇩_{s}_def by auto qed lemma std_apart_instance_of⇩_{l}⇩_{s}2: "instance_of⇩_{l}⇩_{s}C2 (std⇩_{2}C2)" proof - have empty: "(λx. Var (''2''@x)) ⋅ (λx. Var (tl x)) = ε" using composition_def by auto have "C2 ⋅⇩_{l}⇩_{s}ε = C2" using empty_subls by auto then have "C2 ⋅⇩_{l}⇩_{s}((λx. Var (''2''@x)) ⋅ (λx. Var (tl x))) = C2" using empty by auto then have "(C2 ⋅⇩_{l}⇩_{s}(λx. Var (''2''@x))) ⋅⇩_{l}⇩_{s}(λx. Var (tl x)) = C2" using composition_conseq2ls by auto then have "C2 = (std⇩_{2}C2) ⋅⇩_{l}⇩_{s}(λx. Var (tl x))" by auto then show "instance_of⇩_{l}⇩_{s}C2 (std⇩_{2}C2)" unfolding instance_of⇩_{l}⇩_{s}_def by auto qed section ‹Unifiers› definition unifier⇩_{t}⇩_{s}:: "substitution ⇒ fterm set ⇒ bool" where "unifier⇩_{t}⇩_{s}σ ts ⟷ (∃t'. ∀t ∈ ts. t ⋅⇩_{t}σ = t')" definition unifier⇩_{l}⇩_{s}:: "substitution ⇒ fterm literal set ⇒ bool" where "unifier⇩_{l}⇩_{s}σ L ⟷ (∃l'. ∀l ∈ L. l ⋅⇩_{l}σ = l')" lemma unif_sub: assumes unif: "unifier⇩_{l}⇩_{s}σ L" assumes nonempty: "L ≠ {}" shows "∃l. subls L σ = {subl l σ}" proof - from nonempty obtain l where "l ∈ L" by auto from unif this have "L ⋅⇩_{l}⇩_{s}σ = {l ⋅⇩_{l}σ}" unfolding unifier⇩_{l}⇩_{s}_def by auto then show ?thesis by auto qed lemma unifiert_def2: (* (λt. sub t σ) ` ts could have some nice notation maybe *) assumes L_elem: "ts ≠ {}" shows "unifier⇩_{t}⇩_{s}σ ts ⟷ (∃l. (λt. sub t σ) ` ts ={l})" proof assume unif: "unifier⇩_{t}⇩_{s}σ ts" from L_elem obtain t where "t ∈ ts" by auto then have "(λt. sub t σ) ` ts = {t ⋅⇩_{t}σ}" using unif unfolding unifier⇩_{t}⇩_{s}_def by auto then show "∃l. (λt. sub t σ) ` ts = {l}" by auto next assume "∃l. (λt. sub t σ) ` ts ={l}" then obtain l where "(λt. sub t σ) ` ts = {l}" by auto then have "∀l' ∈ ts. l' ⋅⇩_{t}σ = l" by auto then show "unifier⇩_{t}⇩_{s}σ ts" unfolding unifier⇩_{t}⇩_{s}_def by auto qed lemma unifier⇩_{l}⇩_{s}_def2: assumes L_elem: "L ≠ {}" shows "unifier⇩_{l}⇩_{s}σ L ⟷ (∃l. L ⋅⇩_{l}⇩_{s}σ = {l})" proof assume unif: "unifier⇩_{l}⇩_{s}σ L" from L_elem obtain l where "l ∈ L" by auto then have "L ⋅⇩_{l}⇩_{s}σ = {l ⋅⇩_{l}σ}" using unif unfolding unifier⇩_{l}⇩_{s}_def by auto then show "∃l. L ⋅⇩_{l}⇩_{s}σ = {l}" by auto next assume "∃l. L ⋅⇩_{l}⇩_{s}σ ={l}" then obtain l where "L ⋅⇩_{l}⇩_{s}σ = {l}" by auto then have "∀l' ∈ L. l' ⋅⇩_{l}σ = l" by auto then show "unifier⇩_{l}⇩_{s}σ L" unfolding unifier⇩_{l}⇩_{s}_def by auto qed lemma ground⇩_{l}⇩_{s}_unif_singleton: assumes ground⇩_{l}⇩_{s}: "ground⇩_{l}⇩_{s}L" assumes unif: "unifier⇩_{l}⇩_{s}σ' L" assumes empt: "L ≠ {}" shows "∃l. L = {l}" proof - from unif empt have "∃l. L ⋅⇩_{l}⇩_{s}σ' = {l}" using unif_sub by auto then show ?thesis using ground⇩_{l}⇩_{s}_subls ground⇩_{l}⇩_{s}by auto qed definition unifiablets :: "fterm set ⇒ bool" where "unifiablets fs ⟷ (∃σ. unifier⇩_{t}⇩_{s}σ fs)" definition unifiablels :: "fterm literal set ⇒ bool" where "unifiablels L ⟷ (∃σ. unifier⇩_{l}⇩_{s}σ L)" lemma unifier_comp[simp]: "unifier⇩_{l}⇩_{s}σ (L⇧^{C}) ⟷ unifier⇩_{l}⇩_{s}σ L" proof assume "unifier⇩_{l}⇩_{s}σ (L⇧^{C})" then obtain l'' where l''_p: "∀l ∈ L⇧^{C}. l ⋅⇩_{l}σ = l''" unfolding unifier⇩_{l}⇩_{s}_def by auto obtain l' where "(l')⇧^{c}= l''" using comp_exi2[of l''] by auto from this l''_p have l'_p:"∀l ∈ L⇧^{C}. l ⋅⇩_{l}σ = (l')⇧^{c}" by auto have "∀l ∈ L. l ⋅⇩_{l}σ = l'" proof fix l assume "l∈L" then have "l⇧^{c}∈ L⇧^{C}" by auto then have "(l⇧^{c}) ⋅⇩_{l}σ = (l')⇧^{c}" using l'_p by auto then have "(l ⋅⇩_{l}σ)⇧^{c}= (l')⇧^{c}" by (cases l) auto then show "l ⋅⇩_{l}σ = l'" using cancel_comp2 by blast qed then show "unifier⇩_{l}⇩_{s}σ L" unfolding unifier⇩_{l}⇩_{s}_def by auto next assume "unifier⇩_{l}⇩_{s}σ L" then obtain l' where l'_p: "∀l ∈ L. l ⋅⇩_{l}σ = l'" unfolding unifier⇩_{l}⇩_{s}_def by auto have "∀l ∈ L⇧^{C}. l ⋅⇩_{l}σ = (l')⇧^{c}" proof fix l assume "l ∈ L⇧^{C}" then have "l⇧^{c}∈ L" using cancel_comp1 by (metis image_iff) then show "l ⋅⇩_{l}σ = (l')⇧^{c}" using l'_p comp_sub cancel_comp1 by metis qed then show "unifier⇩_{l}⇩_{s}σ (L⇧^{C})" unfolding unifier⇩_{l}⇩_{s}_def by auto qed lemma unifier_sub1: assumes "unifier⇩_{l}⇩_{s}σ L" assumes "L' ⊆ L" shows "unifier⇩_{l}⇩_{s}σ L' " using assms unfolding unifier⇩_{l}⇩_{s}_def by auto lemma unifier_sub2: assumes asm: "unifier⇩_{l}⇩_{s}σ (L⇩_{1}∪ L⇩_{2})" shows "unifier⇩_{l}⇩_{s}σ L⇩_{1}∧ unifier⇩_{l}⇩_{s}σ L⇩_{2}" proof - have "L⇩_{1}⊆ (L⇩_{1}∪ L⇩_{2}) ∧ L⇩_{2}⊆ (L⇩_{1}∪ L⇩_{2})" by simp from this asm show ?thesis using unifier_sub1 by auto qed subsection ‹Most General Unifiers› definition mgu⇩_{t}⇩_{s}:: "substitution ⇒ fterm set ⇒ bool" where "mgu⇩_{t}⇩_{s}σ ts ⟷ unifier⇩_{t}⇩_{s}σ ts ∧ (∀u. unifier⇩_{t}⇩_{s}u ts ⟶ (∃i. u = σ ⋅ i))" definition mgu⇩_{l}⇩_{s}:: "substitution ⇒ fterm literal set ⇒ bool" where "mgu⇩_{l}⇩_{s}σ L ⟷ unifier⇩_{l}⇩_{s}σ L ∧ (∀u. unifier⇩_{l}⇩_{s}u L ⟶ (∃i. u = σ ⋅ i))" section ‹Resolution› definition applicable :: " fterm clause ⇒ fterm clause ⇒ fterm literal set ⇒ fterm literal set ⇒ substitution ⇒ bool" where "applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ ⟷ C⇩_{1}≠ {} ∧ C⇩_{2}≠ {} ∧ L⇩_{1}≠ {} ∧ L⇩_{2}≠ {} ∧ vars⇩_{l}⇩_{s}C⇩_{1}∩ vars⇩_{l}⇩_{s}C⇩_{2}= {} ∧ L⇩_{1}⊆ C⇩_{1}∧ L⇩_{2}⊆ C⇩_{2}∧ mgu⇩_{l}⇩_{s}σ (L⇩_{1}∪ L⇩_{2}⇧^{C})" definition mresolution :: " fterm clause ⇒ fterm clause ⇒ fterm literal set ⇒ fterm literal set ⇒ substitution ⇒ fterm clause" where "mresolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ = ((C⇩_{1}⋅⇩_{l}⇩_{s}σ)- (L⇩_{1}⋅⇩_{l}⇩_{s}σ)) ∪ ((C⇩_{2}⋅⇩_{l}⇩_{s}σ) - (L⇩_{2}⋅⇩_{l}⇩_{s}σ))" definition resolution :: " fterm clause ⇒ fterm clause ⇒ fterm literal set ⇒ fterm literal set ⇒ substitution ⇒ fterm clause" where "resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ = ((C⇩_{1}- L⇩_{1}) ∪ (C⇩_{2}- L⇩_{2})) ⋅⇩_{l}⇩_{s}σ" inductive mresolution_step :: "fterm clause set ⇒ fterm clause set ⇒ bool" where mresolution_rule: "C⇩_{1}∈ Cs ⟹ C⇩_{2}∈ Cs ⟹ applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ ⟹ mresolution_step Cs (Cs ∪ {mresolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ})" | standardize_apart: "C ∈ Cs ⟹ var_renaming_of C C' ⟹ mresolution_step Cs (Cs ∪ {C'})" inductive resolution_step :: "fterm clause set ⇒ fterm clause set ⇒ bool" where resolution_rule: "C⇩_{1}∈ Cs ⟹ C⇩_{2}∈ Cs ⟹ applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ ⟹ resolution_step Cs (Cs ∪ {resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ})" | standardize_apart: (* renaming *) "C ∈ Cs ⟹ var_renaming_of C C' ⟹ resolution_step Cs (Cs ∪ {C'})" definition mresolution_deriv :: "fterm clause set ⇒ fterm clause set ⇒ bool" where "mresolution_deriv = rtranclp mresolution_step" definition resolution_deriv :: "fterm clause set ⇒ fterm clause set ⇒ bool" where "resolution_deriv = rtranclp resolution_step" section ‹Soundness› definition evalsub :: "'u var_denot ⇒ 'u fun_denot ⇒ substitution ⇒ 'u var_denot" where "evalsub E F σ = eval⇩_{t}E F ∘ σ" lemma substitutiont: "eval⇩_{t}E F (t ⋅⇩_{t}σ) = eval⇩_{t}(evalsub E F σ) F t" apply (induction t) unfolding evalsub_def apply auto apply (metis (mono_tags, lifting) comp_apply map_cong) done lemma substitutionts: "eval⇩_{t}⇩_{s}E F (ts ⋅⇩_{t}⇩_{s}σ) = eval⇩_{t}⇩_{s}(evalsub E F σ) F ts" using substitutiont by auto lemma substitution: "eval⇩_{l}E F G (l ⋅⇩_{l}σ) ⟷ eval⇩_{l}(evalsub E F σ) F G l" apply (induction l) using substitutionts apply (metis eval⇩_{l}.simps(1) subl.simps(1)) using substitutionts apply (metis eval⇩_{l}.simps(2) subl.simps(2)) done lemma subst_sound: assumes asm: "eval⇩_{c}F G C" shows "eval⇩_{c}F G (C ⋅⇩_{l}⇩_{s}σ)" unfolding eval⇩_{c}_def proof fix E from asm have "∀E'. ∃l ∈ C. eval⇩_{l}E' F G l" using eval⇩_{c}_def by blast then have "∃l ∈ C. eval⇩_{l}(evalsub E F σ) F G l" by auto then show "∃l ∈ C ⋅⇩_{l}⇩_{s}σ. eval⇩_{l}E F G l" using substitution by blast qed lemma simple_resolution_sound: assumes C⇩_{1}sat: "eval⇩_{c}F G C⇩_{1}" assumes C⇩_{2}sat: "eval⇩_{c}F G C⇩_{2}" assumes l⇩_{1}inc⇩_{1}: "l⇩_{1}∈ C⇩_{1}" assumes l⇩_{2}inc⇩_{2}: "l⇩_{2}∈ C⇩_{2}" assumes comp: "l⇩_{1}⇧^{c}= l⇩_{2}" shows "eval⇩_{c}F G ((C⇩_{1}- {l⇩_{1}}) ∪ (C⇩_{2}- {l⇩_{2}}))" proof - have "∀E. ∃l ∈ (((C⇩_{1}- {l⇩_{1}}) ∪ (C⇩_{2}- {l⇩_{2}}))). eval⇩_{l}E F G l" proof fix E have "eval⇩_{l}E F G l⇩_{1}∨ eval⇩_{l}E F G l⇩_{2}" using comp by (cases l⇩_{1}) auto then show "∃l ∈ (((C⇩_{1}- {l⇩_{1}}) ∪ (C⇩_{2}- {l⇩_{2}}))). eval⇩_{l}E F G l" proof assume "eval⇩_{l}E F G l⇩_{1}" then have "¬eval⇩_{l}E F G l⇩_{2}" using comp by (cases l⇩_{1}) auto then have "∃l⇩_{2}'∈ C⇩_{2}. l⇩_{2}' ≠ l⇩_{2}∧ eval⇩_{l}E F G l⇩_{2}'" using l⇩_{2}inc⇩_{2}C⇩_{2}sat unfolding eval⇩_{c}_def by auto then show "∃l∈(C⇩_{1}- {l⇩_{1}}) ∪ (C⇩_{2}- {l⇩_{2}}). eval⇩_{l}E F G l" by auto next assume "eval⇩_{l}E F G l⇩_{2}" (* Symmetric *) then have "¬eval⇩_{l}E F G l⇩_{1}" using comp by (cases l⇩_{1}) auto then have "∃l⇩_{1}'∈ C⇩_{1}. l⇩_{1}' ≠ l⇩_{1}∧ eval⇩_{l}E F G l⇩_{1}'" using l⇩_{1}inc⇩_{1}C⇩_{1}sat unfolding eval⇩_{c}_def by auto then show "∃l∈(C⇩_{1}- {l⇩_{1}}) ∪ (C⇩_{2}- {l⇩_{2}}). eval⇩_{l}E F G l" by auto qed qed then show ?thesis unfolding eval⇩_{c}_def by simp qed lemma mresolution_sound: assumes sat⇩_{1}: "eval⇩_{c}F G C⇩_{1}" assumes sat⇩_{2}: "eval⇩_{c}F G C⇩_{2}" assumes appl: "applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ" shows "eval⇩_{c}F G (mresolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ)" proof - from sat⇩_{1}have sat⇩_{1}σ: "eval⇩_{c}F G (C⇩_{1}⋅⇩_{l}⇩_{s}σ)" using subst_sound by blast from sat⇩_{2}have sat⇩_{2}σ: "eval⇩_{c}F G (C⇩_{2}⋅⇩_{l}⇩_{s}σ)" using subst_sound by blast from appl obtain l⇩_{1}where l⇩_{1}_p: "l⇩_{1}∈ L⇩_{1}" unfolding applicable_def by auto from l⇩_{1}_p appl have "l⇩_{1}∈ C⇩_{1}" unfolding applicable_def by auto then have inc⇩_{1}σ: "l⇩_{1}⋅⇩_{l}σ ∈ C⇩_{1}⋅⇩_{l}⇩_{s}σ" by auto from l⇩_{1}_p have unified⇩_{1}: "l⇩_{1}∈ (L⇩_{1}∪ (L⇩_{2}⇧^{C}))" by auto from l⇩_{1}_p appl have l⇩_{1}σisl⇩_{1}σ: "{l⇩_{1}⋅⇩_{l}σ} = L⇩_{1}⋅⇩_{l}⇩_{s}σ" unfolding mgu⇩_{l}⇩_{s}_def unifier⇩_{l}⇩_{s}_def applicable_def by auto from appl obtain l⇩_{2}where l⇩_{2}_p: "l⇩_{2}∈ L⇩_{2}" unfolding applicable_def by auto from l⇩_{2}_p appl have "l⇩_{2}∈ C⇩_{2}" unfolding applicable_def by auto then have inc⇩_{2}σ: "l⇩_{2}⋅⇩_{l}σ ∈ C⇩_{2}⋅⇩_{l}⇩_{s}σ" by auto from l⇩_{2}_p have unified⇩_{2}: "l⇩_{2}⇧^{c}∈ (L⇩_{1}∪ (L⇩_{2}⇧^{C}))" by auto from unified⇩_{1}unified⇩_{2}appl have "l⇩_{1}⋅⇩_{l}σ = (l⇩_{2}⇧^{c}) ⋅⇩_{l}σ" unfolding mgu⇩_{l}⇩_{s}_def unifier⇩_{l}⇩_{s}_def applicable_def by auto then have comp: "(l⇩_{1}⋅⇩_{l}σ)⇧^{c}= l⇩_{2}⋅⇩_{l}σ" using comp_sub comp_swap by auto from appl have "unifier⇩_{l}⇩_{s}σ (L⇩_{2}⇧^{C})" using unifier_sub2 unfolding mgu⇩_{l}⇩_{s}_def applicable_def by blast then have "unifier⇩_{l}⇩_{s}σ L⇩_{2}" by auto from this l⇩_{2}_p have l⇩_{2}σisl⇩_{2}σ: "{l⇩_{2}⋅⇩_{l}σ} = L⇩_{2}⋅⇩_{l}⇩_{s}σ" unfolding unifier⇩_{l}⇩_{s}_def by auto from sat⇩_{1}σ sat⇩_{2}σ inc⇩_{1}σ inc⇩_{2}σ comp have "eval⇩_{c}F G ((C⇩_{1}⋅⇩_{l}⇩_{s}σ) - {l⇩_{1}⋅⇩_{l}σ} ∪ ((C⇩_{2}⋅⇩_{l}⇩_{s}σ) - {l⇩_{2}⋅⇩_{l}σ}))" using simple_resolution_sound[of F G "C⇩_{1}⋅⇩_{l}⇩_{s}σ" "C⇩_{2}⋅⇩_{l}⇩_{s}σ" "l⇩_{1}⋅⇩_{l}σ" " l⇩_{2}⋅⇩_{l}σ"] by auto from this l⇩_{1}σisl⇩_{1}σ l⇩_{2}σisl⇩_{2}σ show ?thesis unfolding mresolution_def by auto qed lemma resolution_superset: "mresolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ ⊆ resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ" unfolding mresolution_def resolution_def by auto lemma superset_sound: assumes sup: "C ⊆ C'" assumes sat: "eval⇩_{c}F G C" shows "eval⇩_{c}F G C'" proof - have "∀E. ∃l ∈ C'. eval⇩_{l}E F G l" proof fix E from sat have "∀E. ∃l ∈ C. eval⇩_{l}E F G l" unfolding eval⇩_{c}_def by - then have "∃l ∈ C . eval⇩_{l}E F G l" by auto then show "∃l ∈ C'. eval⇩_{l}E F G l" using sup by auto qed then show "eval⇩_{c}F G C'" unfolding eval⇩_{c}_def by auto qed theorem resolution_sound: assumes sat⇩_{1}: "eval⇩_{c}F G C⇩_{1}" assumes sat⇩_{2}: "eval⇩_{c}F G C⇩_{2}" assumes appl: "applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ" shows "eval⇩_{c}F G (resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ)" proof - from sat⇩_{1}sat⇩_{2}appl have "eval⇩_{c}F G (mresolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ)" using mresolution_sound by blast then show ?thesis using superset_sound resolution_superset by metis qed lemma mstep_sound: assumes "mresolution_step Cs Cs'" assumes "eval⇩_{c}⇩_{s}F G Cs" shows "eval⇩_{c}⇩_{s}F G Cs'" using assms proof (induction rule: mresolution_step.induct) case (mresolution_rule C⇩_{1}Cs C⇩_{2}l⇩_{1}l⇩_{2}σ) then have "eval⇩_{c}F G C⇩_{1}∧ eval⇩_{c}F G C⇩_{2}" unfolding eval⇩_{c}⇩_{s}_def by auto then have "eval⇩_{c}F G (mresolution C⇩_{1}C⇩_{2}l⇩_{1}l⇩_{2}σ)" using mresolution_sound mresolution_rule by auto then show ?case using mresolution_rule unfolding eval⇩_{c}⇩_{s}_def by auto next case (standardize_apart C Cs C') then have "eval⇩_{c}F G C" unfolding eval⇩_{c}⇩_{s}_def by auto then have "eval⇩_{c}F G C'" using subst_sound standardize_apart unfolding var_renaming_of_def instance_of⇩_{l}⇩_{s}_def by metis then show ?case using standardize_apart unfolding eval⇩_{c}⇩_{s}_def by auto qed theorem step_sound: assumes "resolution_step Cs Cs'" assumes "eval⇩_{c}⇩_{s}F G Cs" shows "eval⇩_{c}⇩_{s}F G Cs'" using assms proof (induction rule: resolution_step.induct) case (resolution_rule C⇩_{1}Cs C⇩_{2}l⇩_{1}l⇩_{2}σ) then have "eval⇩_{c}F G C⇩_{1}∧ eval⇩_{c}F G C⇩_{2}" unfolding eval⇩_{c}⇩_{s}_def by auto then have "eval⇩_{c}F G (resolution C⇩_{1}C⇩_{2}l⇩_{1}l⇩_{2}σ)" using resolution_sound resolution_rule by auto then show ?case using resolution_rule unfolding eval⇩_{c}⇩_{s}_def by auto next case (standardize_apart C Cs C') then have "eval⇩_{c}F G C" unfolding eval⇩_{c}⇩_{s}_def by auto then have "eval⇩_{c}F G C'" using subst_sound standardize_apart unfolding var_renaming_of_def instance_of⇩_{l}⇩_{s}_def by metis then show ?case using standardize_apart unfolding eval⇩_{c}⇩_{s}_def by auto qed lemma mderivation_sound: assumes "mresolution_deriv Cs Cs'" assumes "eval⇩_{c}⇩_{s}F G Cs" shows "eval⇩_{c}⇩_{s}F G Cs'" using assms unfolding mresolution_deriv_def proof (induction rule: rtranclp.induct) case rtrancl_refl then show ?case by auto next case (rtrancl_into_rtrancl Cs⇩_{1}Cs⇩_{2}Cs⇩_{3}) then show ?case using mstep_sound by auto qed theorem derivation_sound: assumes "resolution_deriv Cs Cs'" assumes "eval⇩_{c}⇩_{s}F G Cs" shows"eval⇩_{c}⇩_{s}F G Cs'" using assms unfolding resolution_deriv_def proof (induction rule: rtranclp.induct) case rtrancl_refl then show ?case by auto next case (rtrancl_into_rtrancl Cs⇩_{1}Cs⇩_{2}Cs⇩_{3}) then show ?case using step_sound by auto qed theorem derivation_sound_refute: assumes deriv: "resolution_deriv Cs Cs' ∧ {} ∈ Cs'" shows "¬eval⇩_{c}⇩_{s}F G Cs" proof - from deriv have "eval⇩_{c}⇩_{s}F G Cs ⟶ eval⇩_{c}⇩_{s}F G Cs'" using derivation_sound by auto moreover from deriv have "eval⇩_{c}⇩_{s}F G Cs' ⟶ eval⇩_{c}F G {}" unfolding eval⇩_{c}⇩_{s}_def by auto moreover then have "eval⇩_{c}F G {} ⟶ False" unfolding eval⇩_{c}_def by auto ultimately show ?thesis by auto qed section ‹Herbrand Interpretations› text ‹@{const HFun} is the Herbrand function denotation in which terms are mapped to themselves.› term HFun lemma eval_ground⇩_{t}: assumes "ground⇩_{t}t" shows "(eval⇩_{t}E HFun t) = hterm_of_fterm t" using assms by (induction t) auto lemma eval_ground⇩_{t}⇩_{s}: assumes "ground⇩_{t}⇩_{s}ts" shows "(eval⇩_{t}⇩_{s}E HFun ts) = hterms_of_fterms ts" unfolding hterms_of_fterms_def using assms eval_ground⇩_{t}by (induction ts) auto lemma eval⇩_{l}_ground⇩_{t}⇩_{s}: assumes asm: "ground⇩_{t}⇩_{s}ts" shows "eval⇩_{l}E HFun G (Pos P ts) ⟷ G P (hterms_of_fterms ts)" proof - have "eval⇩_{l}E HFun G (Pos P ts) = G P (eval⇩_{t}⇩_{s}E HFun ts)" by auto also have "... = G P (hterms_of_fterms ts)" using asm eval_ground⇩_{t}⇩_{s}by simp finally show ?thesis by auto qed section ‹Partial Interpretations› type_synonym partial_pred_denot = "bool list" definition falsifies⇩_{l}:: "partial_pred_denot ⇒ fterm literal ⇒ bool" where "falsifies⇩_{l}G l ⟷ ground⇩_{l}l ∧ (let i = nat_of_fatom (get_atom l) in i < length G ∧ G ! i = (¬sign l) )" text ‹A ground clause is falsified if it is actually ground and all its literals are falsified.› abbreviation falsifies⇩_{g}:: "partial_pred_denot ⇒ fterm clause ⇒ bool" where "falsifies⇩_{g}G C ≡ ground⇩_{l}⇩_{s}C ∧ (∀l ∈ C. falsifies⇩_{l}G l)" abbreviation falsifies⇩_{c}:: "partial_pred_denot ⇒ fterm clause ⇒ bool" where "falsifies⇩_{c}G C ≡ (∃C'. instance_of⇩_{l}⇩_{s}C' C ∧ falsifies⇩_{g}G C')" abbreviation falsifies⇩_{c}⇩_{s}:: "partial_pred_denot ⇒ fterm clause set ⇒ bool" where "falsifies⇩_{c}⇩_{s}G Cs ≡ (∃C ∈ Cs. falsifies⇩_{c}G C)" abbreviation extend :: "(nat ⇒ partial_pred_denot) ⇒ hterm pred_denot" where "extend f P ts ≡ ( let n = nat_of_hatom (P, ts) in f (Suc n) ! n )" fun sub_of_denot :: "hterm var_denot ⇒ substitution" where "sub_of_denot E = fterm_of_hterm ∘ E" lemma ground_sub_of_denott: "ground⇩_{t}(t ⋅⇩_{t}(sub_of_denot E))" by (induction t) (auto simp add: ground_fterm_of_hterm) lemma ground_sub_of_denotts: "ground⇩_{t}⇩_{s}(ts ⋅⇩_{t}⇩_{s}sub_of_denot E)" using ground_sub_of_denott by simp lemma ground_sub_of_denotl: "ground⇩_{l}(l ⋅⇩_{l}sub_of_denot E)" proof - have "ground⇩_{t}⇩_{s}(subs (get_terms l) (sub_of_denot E))" using ground_sub_of_denotts by auto then show ?thesis by (cases l) auto qed lemma sub_of_denot_equivx: "eval⇩_{t}E HFun (sub_of_denot E x) = E x" proof - have "ground⇩_{t}(sub_of_denot E x)" using ground_fterm_of_hterm by simp then have "eval⇩_{t}E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)" using eval_ground⇩_{t}(1) by auto also have "... = hterm_of_fterm (fterm_of_hterm (E x))" by auto also have "... = E x" by auto finally show ?thesis by auto qed lemma sub_of_denot_equivt: "eval⇩_{t}E HFun (t ⋅⇩_{t}(sub_of_denot E)) = eval⇩_{t}E HFun t" using sub_of_denot_equivx by (induction t) auto lemma sub_of_denot_equivts: "eval⇩_{t}⇩_{s}E HFun (ts ⋅⇩_{t}⇩_{s}(sub_of_denot E)) = eval⇩_{t}⇩_{s}E HFun ts" using sub_of_denot_equivt by simp lemma sub_of_denot_equivl: "eval⇩_{l}E HFun G (l ⋅⇩_{l}sub_of_denot E) ⟷ eval⇩_{l}E HFun G l" proof (induction l) case (Pos p ts) have "eval⇩_{l}E HFun G ((Pos p ts) ⋅⇩_{l}sub_of_denot E) ⟷ G p (eval⇩_{t}⇩_{s}E HFun (ts ⋅⇩_{t}⇩_{s}(sub_of_denot E)))" by auto also have " ... ⟷ G p (eval⇩_{t}⇩_{s}E HFun ts)" using sub_of_denot_equivts[of E ts] by metis also have " ... ⟷ eval⇩_{l}E HFun G (Pos p ts)" by simp finally show ?case by blast next case (Neg p ts) have "eval⇩_{l}E HFun G ((Neg p ts) ⋅⇩_{l}sub_of_denot E) ⟷ ¬G p (eval⇩_{t}⇩_{s}E HFun (ts ⋅⇩_{t}⇩_{s}(sub_of_denot E)))" by auto also have " ... ⟷ ¬G p (eval⇩_{t}⇩_{s}E HFun ts)" using sub_of_denot_equivts[of E ts] by metis also have " ... = eval⇩_{l}E HFun G (Neg p ts)" by simp finally show ?case by blast qed text ‹Under an Herbrand interpretation, an environment is equivalent to a substitution.› lemma sub_of_denot_equiv_ground': "eval⇩_{l}E HFun G l = eval⇩_{l}E HFun G (l ⋅⇩_{l}sub_of_denot E) ∧ ground⇩_{l}(l ⋅⇩_{l}sub_of_denot E)" using sub_of_denot_equivl ground_sub_of_denotl by auto text ‹Under an Herbrand interpretation, an environment is similar to a substitution - also for partial interpretations.› lemma partial_equiv_subst: assumes "falsifies⇩_{c}G (C ⋅⇩_{l}⇩_{s}τ)" shows "falsifies⇩_{c}G C" proof - from assms obtain C' where C'_p: "instance_of⇩_{l}⇩_{s}C' (C ⋅⇩_{l}⇩_{s}τ) ∧ falsifies⇩_{g}G C'" by auto then have "instance_of⇩_{l}⇩_{s}(C ⋅⇩_{l}⇩_{s}τ) C" unfolding instance_of⇩_{l}⇩_{s}_def by auto then have "instance_of⇩_{l}⇩_{s}C' C" using C'_p instance_of⇩_{l}⇩_{s}_trans by auto then show ?thesis using C'_p by auto qed text ‹Under an Herbrand interpretation, an environment is equivalent to a substitution.› lemma sub_of_denot_equiv_ground: "((∃l ∈ C. eval⇩_{l}E HFun G l) ⟷ (∃l ∈ C ⋅⇩_{l}⇩_{s}sub_of_denot E. eval⇩_{l}E HFun G l)) ∧ ground⇩_{l}⇩_{s}(C ⋅⇩_{l}⇩_{s}sub_of_denot E)" using sub_of_denot_equiv_ground' by auto lemma std⇩_{1}_falsifies: "falsifies⇩_{c}G C⇩_{1}⟷ falsifies⇩_{c}G (std⇩_{1}C⇩_{1})" proof assume asm: "falsifies⇩_{c}G C⇩_{1}" then obtain Cg where "instance_of⇩_{l}⇩_{s}Cg C⇩_{1}∧ falsifies⇩_{g}G Cg" by auto moreover then have "instance_of⇩_{l}⇩_{s}Cg (std⇩_{1}C⇩_{1})" using std_apart_instance_of⇩_{l}⇩_{s}1 instance_of⇩_{l}⇩_{s}_trans by blast ultimately show "falsifies⇩_{c}G (std⇩_{1}C⇩_{1})" by auto next assume asm: "falsifies⇩_{c}G (std⇩_{1}C⇩_{1})" then have inst: "instance_of⇩_{l}⇩_{s}(std⇩_{1}C⇩_{1}) C⇩_{1}" unfolding instance_of⇩_{l}⇩_{s}_def by auto from asm obtain Cg where "instance_of⇩_{l}⇩_{s}Cg (std⇩_{1}C⇩_{1}) ∧ falsifies⇩_{g}G Cg" by auto moreover then have "instance_of⇩_{l}⇩_{s}Cg C⇩_{1}" using inst instance_of⇩_{l}⇩_{s}_trans by blast ultimately show "falsifies⇩_{c}G C⇩_{1}" by auto qed lemma std⇩_{2}_falsifies: "falsifies⇩_{c}G C⇩_{2}⟷ falsifies⇩_{c}G (std⇩_{2}C⇩_{2})" proof assume asm: "falsifies⇩_{c}G C⇩_{2}" then obtain Cg where "instance_of⇩_{l}⇩_{s}Cg C⇩_{2}∧ falsifies⇩_{g}G Cg" by auto moreover then have "instance_of⇩_{l}⇩_{s}Cg (std⇩_{2}C⇩_{2})" using std_apart_instance_of⇩_{l}⇩_{s}2 instance_of⇩_{l}⇩_{s}_trans by blast ultimately show "falsifies⇩_{c}G (std⇩_{2}C⇩_{2})" by auto next assume asm: "falsifies⇩_{c}G (std⇩_{2}C⇩_{2})" then have inst: "instance_of⇩_{l}⇩_{s}(std⇩_{2}C⇩_{2}) C⇩_{2}" unfolding instance_of⇩_{l}⇩_{s}_def by auto from asm obtain Cg where "instance_of⇩_{l}⇩_{s}Cg (std⇩_{2}C⇩_{2}) ∧ falsifies⇩_{g}G Cg" by auto moreover then have "instance_of⇩_{l}⇩_{s}Cg C⇩_{2}" using inst instance_of⇩_{l}⇩_{s}_trans by blast ultimately show "falsifies⇩_{c}G C⇩_{2}" by auto qed lemma std⇩_{1}_renames: "var_renaming_of C⇩_{1}(std⇩_{1}C⇩_{1})" proof - have "instance_of⇩_{l}⇩_{s}C⇩_{1}(std⇩_{1}C⇩_{1})" using std_apart_instance_of⇩_{l}⇩_{s}1 by auto moreover have "instance_of⇩_{l}⇩_{s}(std⇩_{1}C⇩_{1}) C⇩_{1}" unfolding instance_of⇩_{l}⇩_{s}_def by auto ultimately show "var_renaming_of C⇩_{1}(std⇩_{1}C⇩_{1})" unfolding var_renaming_of_def by auto qed lemma std⇩_{2}_renames: "var_renaming_of C⇩_{2}(std⇩_{2}C⇩_{2})" proof - have "instance_of⇩_{l}⇩_{s}C⇩_{2}(std⇩_{2}C⇩_{2})" using std_apart_instance_of⇩_{l}⇩_{s}2 by auto moreover have "instance_of⇩_{l}⇩_{s}(std⇩_{2}C⇩_{2}) C⇩_{2}" unfolding instance_of⇩_{l}⇩_{s}_def by auto ultimately show "var_renaming_of C⇩_{2}(std⇩_{2}C⇩_{2})" unfolding var_renaming_of_def by auto qed section ‹Semantic Trees› abbreviation closed_branch :: "partial_pred_denot ⇒ tree ⇒ fterm clause set ⇒ bool" where "closed_branch G T Cs ≡ branch G T ∧ falsifies⇩_{c}⇩_{s}G Cs" abbreviation(input) open_branch :: "partial_pred_denot ⇒ tree ⇒ fterm clause set ⇒ bool" where "open_branch G T Cs ≡ branch G T ∧ ¬falsifies⇩_{c}⇩_{s}G Cs" definition closed_tree :: "tree ⇒ fterm clause set ⇒ bool" where "closed_tree T Cs ⟷ anybranch T (λb. closed_branch b T Cs) ∧ anyinternal T (λp. ¬falsifies⇩_{c}⇩_{s}p Cs)" section ‹Herbrand's Theorem› lemma maximum: assumes asm: "finite C" shows "∃n :: nat. ∀l ∈ C. f l ≤ n" proof from asm show "∀l∈C. f l ≤ (Max (f ` C))" by auto qed lemma extend_preserves_model: (* only for ground *) assumes f_infpath: "wf_infpath (f :: nat ⇒ partial_pred_denot)" assumes C_ground: "ground⇩_{l}⇩_{s}C" assumes C_sat: "¬falsifies⇩_{c}(f (Suc n)) C" assumes n_max: "∀l∈C. nat_of_fatom (get_atom l) ≤ n" shows "eval⇩_{c}HFun (extend f) C" proof - let ?F = "HFun" let ?G = "extend f" { fix E from C_sat have "∀C'. (¬instance_of⇩_{l}⇩_{s}C' C ∨ ¬falsifies⇩_{g}(f (Suc n)) C')" by auto then have "¬falsifies⇩_{g}(f (Suc n)) C" using instance_of⇩_{l}⇩_{s}_self by auto then obtain l where l_p: "l∈C ∧ ¬falsifies⇩_{l}(f (Suc n)) l" using C_ground by blast let ?i = "nat_of_fatom (get_atom l)" from l_p have i_n: "?i ≤ n" using n_max by auto then have j_n: "?i < length (f (Suc n))" using f_infpath infpath_length[of f] by auto have "eval⇩_{l}E HFun (extend f) l" proof (cases l) case (Pos P ts) from Pos l_p C_ground have ts_ground: "ground⇩_{t}⇩_{s}ts" by auto have "¬falsifies⇩_{l}(f (Suc n)) l" using l_p by auto then have "f (Suc n) ! ?i = True" using j_n Pos ts_ground empty_subts[of ts] unfolding falsifies⇩_{l}_def by auto moreover have "f (Suc ?i) ! ?i = f (Suc n) ! ?i" using f_infpath i_n j_n infpath_length[of f] ith_in_extension[of f] by simp ultimately have "f (Suc ?i) ! ?i = True" using Pos by auto then have "?G P (hterms_of_fterms ts)" using Pos by (simp add: nat_of_fatom_def) then show ?thesis using eval⇩_{l}_ground⇩_{t}⇩_{s}[of ts _ ?G P] ts_ground Pos by auto next case (Neg P ts) (* Symmetric *) from Neg l_p C_ground have ts_ground: "ground⇩_{t}⇩_{s}ts" by auto have "¬falsifies⇩_{l}(f (Suc n)) l" using l_p by auto then have "f (Suc n) ! ?i = False" using j_n Neg ts_ground empty_subts[of ts] unfolding falsifies⇩_{l}_def by auto moreover have "f (Suc ?i) ! ?i = f (Suc n) ! ?i" using f_infpath i_n j_n infpath_length[of f] ith_in_extension[of f] by simp ultimately have "f (Suc ?i) ! ?i = False" using Neg by auto then have "¬?G P (hterms_of_fterms ts)" using Neg by (simp add: nat_of_fatom_def) then show ?thesis using Neg eval⇩_{l}_ground⇩_{t}⇩_{s}[of ts _ ?G P] ts_ground by auto qed then have "∃l ∈ C. eval⇩_{l}E HFun (extend f) l" using l_p by auto } then have "eval⇩_{c}HFun (extend f) C" unfolding eval⇩_{c}_def by auto then show ?thesis using instance_of⇩_{l}⇩_{s}_self by auto qed lemma extend_preserves_model2: (* only for ground *) assumes f_infpath: "wf_infpath (f :: nat ⇒ partial_pred_denot)" assumes C_ground: "ground⇩_{l}⇩_{s}C" assumes fin_c: "finite C" assumes model_C: "∀n. ¬falsifies⇩_{c}(f n) C" shows C_false: "eval⇩_{c}HFun (extend f) C" proof - ― ‹Since C is finite, C has a largest index of a literal.› obtain n where largest: "∀l ∈ C. nat_of_fatom (get_atom l) ≤ n" using fin_c maximum[of C "λl. nat_of_fatom (get_atom l)"] by blast moreover then have "¬falsifies⇩_{c}(f (Suc n)) C" using model_C by auto ultimately show ?thesis using model_C f_infpath C_ground extend_preserves_model[of f C n ] by blast qed lemma extend_infpath: assumes f_infpath: "wf_infpath (f :: nat ⇒ partial_pred_denot)" assumes model_c: "∀n. ¬falsifies⇩_{c}(f n) C" assumes fin_c: "finite C" shows "eval⇩_{c}HFun (extend f) C" unfolding eval⇩_{c}_def proof fix E let ?G = "extend f" let ?σ = "sub_of_denot E" from fin_c have fin_cσ: "finite (C ⋅⇩_{l}⇩_{s}sub_of_denot E)" by auto have groundcσ: "ground⇩_{l}⇩_{s}(C ⋅⇩_{l}⇩_{s}sub_of_denot E)" using sub_of_denot_equiv_ground by auto ― ‹Here starts the proof› ― ‹We go from syntactic FO world to syntactic ground world:› from model_c have "∀n. ¬falsifies⇩_{c}(f n) (C ⋅⇩_{l}⇩_{s}?σ)" using partial_equiv_subst by blast ― ‹Then from syntactic ground world to semantic ground world:› then have "eval⇩_{c}HFun ?G (C ⋅⇩_{l}⇩_{s}?σ)" using groundcσ f_infpath fin_cσ extend_preserves_model2[of f "C ⋅⇩_{l}⇩_{s}?σ"] by blast ― ‹Then from semantic ground world to semantic FO world:› then have "∀E. ∃l ∈ (C ⋅⇩_{l}⇩_{s}?σ). eval⇩_{l}E HFun ?G l" unfolding eval⇩_{c}_def by auto then have "∃l ∈ (C ⋅⇩_{l}⇩_{s}?σ). eval⇩_{l}E HFun ?G l" by auto then show "∃l ∈ C. eval⇩_{l}E HFun ?G l" using sub_of_denot_equiv_ground[of C E "extend f"] by blast qed text ‹If we have a infpath of partial models, then we have a model.› lemma infpath_model: assumes f_infpath: "wf_infpath (f :: nat ⇒ partial_pred_denot)" assumes model_cs: "∀n. ¬falsifies⇩_{c}⇩_{s}(f n) Cs" assumes fin_cs: "finite Cs" assumes fin_c: "∀C ∈ Cs. finite C" shows "eval⇩_{c}⇩_{s}HFun (extend f) Cs" proof - let ?F = "HFun" have "∀C ∈ Cs. eval⇩_{c}?F (extend f) C" proof (rule ballI) fix C assume asm: "C ∈ Cs" then have "∀n. ¬falsifies⇩_{c}(f n) C" using model_cs by auto then show "eval⇩_{c}?F (extend f) C" using fin_c asm f_infpath extend_infpath[of f C] by auto qed then show "eval⇩_{c}⇩_{s}?F (extend f) Cs" unfolding eval⇩_{c}⇩_{s}_def by auto qed fun deeptree :: "nat ⇒ tree" where "deeptree 0 = Leaf" | "deeptree (Suc n) = Branching (deeptree n) (deeptree n)" lemma branch_length: assumes "branch b (deeptree n)" shows "length b = n" using assms proof (induction n arbitrary: b) case 0 then show ?case using branch_inv_Leaf by auto next case (Suc n) then have "branch b (Branching (deeptree n) (deeptree n))" by auto then obtain a b' where p: "b = a#b'∧ branch b' (deeptree n)" using branch_inv_Branching[of b] by blast then have "length b' = n" using Suc by auto then show ?case using p by auto qed lemma infinity: assumes inj: "∀n :: nat. undiago (diago n) = n" assumes all_tree: "∀n :: nat. (diago n) ∈ tree" shows "¬finite tree" proof - from inj all_tree have "∀n. n = undiago (diago n) ∧ (diago n) ∈ tree" by auto then have "∀n. ∃ds. n = undiago ds ∧ ds ∈ tree" by auto then have "undiago ` tree = (UNIV :: nat set)" by auto then have "¬finite tree"by (metis finite_imageI infinite_UNIV_nat) then show ?thesis by auto qed lemma longer_falsifies⇩_{l}: assumes "falsifies⇩_{l}ds l" shows "falsifies⇩_{l}(ds@d) l" proof - let ?i = "nat_of_fatom (get_atom l)" from assms have i_p: "ground⇩_{l}l ∧ ?i < length ds ∧ ds ! ?i = (¬sign l)" unfolding falsifies⇩_{l}_def by meson moreover from i_p have "?i < length (ds@d)" by auto moreover from i_p have "(ds@d) ! ?i = (¬sign l)" by (simp add: nth_append) ultimately show ?thesis unfolding falsifies⇩_{l}_def by simp qed lemma longer_falsifies⇩_{g}: assumes "falsifies⇩_{g}ds C" shows "falsifies⇩_{g}(ds @ d) C" proof - { fix l assume "l∈C" then have "falsifies⇩_{l}(ds @ d) l" using assms longer_falsifies⇩_{l}by auto } then show ?thesis using assms by auto qed lemma longer_falsifies⇩_{c}: assumes "falsifies⇩_{c}ds C" shows "falsifies⇩_{c}(ds @ d) C" proof - from assms obtain C' where "instance_of⇩_{l}⇩_{s}C' C ∧ falsifies⇩_{g}ds C'" by auto moreover then have "falsifies⇩_{g}(ds @ d) C'" using longer_falsifies⇩_{g}by auto ultimately show ?thesis by auto qed text ‹We use this so that we can apply König's lemma.› lemma longer_falsifies: assumes "falsifies⇩_{c}⇩_{s}ds Cs" shows "falsifies⇩_{c}⇩_{s}(ds @ d) Cs" proof - from assms obtain C where "C ∈ Cs ∧ falsifies⇩_{c}ds C" by auto moreover then have "falsifies⇩_{c}(ds @ d) C" using longer_falsifies⇩_{c}[of C ds d] by blast ultimately show ?thesis by auto qed text ‹If all finite semantic trees have an open branch, then the set of clauses has a model.› theorem herbrand': assumes openb: "∀T. ∃G. open_branch G T Cs" assumes finite_cs: "finite Cs" "∀C∈Cs. finite C" shows "∃G. eval⇩_{c}⇩_{s}HFun G Cs" proof - ― ‹Show T infinite:› let ?tree = "{G. ¬falsifies⇩_{c}⇩_{s}G Cs}" let ?undiag = length let ?diag = "(λl. SOME b. open_branch b (deeptree l) Cs) :: nat ⇒ partial_pred_denot" from openb have diag_open: "∀l. open_branch (?diag l) (deeptree l) Cs" using someI_ex[of "λb. open_branch b (deeptree _) Cs"] by auto then have "∀n. ?undiag (?diag n) = n" using branch_length by auto moreover have "∀n. (?diag n) ∈ ?tree" using diag_open by auto ultimately have "¬finite ?tree" using infinity[of _ "λn. SOME b. open_branch b (_ n) Cs"] by simp ― ‹Get infinite path:› moreover have "∀ds d. ¬falsifies⇩_{c}⇩_{s}(ds @ d) Cs ⟶ ¬falsifies⇩_{c}⇩_{s}ds Cs" using longer_falsifies[of Cs] by blast then have "(∀ds d. ds @ d ∈ ?tree ⟶ ds ∈ ?tree)" by auto ultimately have "∃c. wf_infpath c ∧ (∀n. c n ∈ ?tree)" using konig[of ?tree] by blast then have "∃G. wf_infpath G ∧ (∀n. ¬ falsifies⇩_{c}⇩_{s}(G n) Cs)" by auto ― ‹Apply above infpath lemma:› then show "∃G. eval⇩_{c}⇩_{s}HFun G Cs" using infpath_model finite_cs by auto qed lemma shorter_falsifies⇩_{l}: assumes "falsifies⇩_{l}(ds@d) l" assumes "nat_of_fatom (get_atom l) < length ds" shows "falsifies⇩_{l}ds l" proof - let ?i = "nat_of_fatom (get_atom l)" from assms have i_p: "ground⇩_{l}l ∧ ?i < length (ds@d) ∧ (ds@d) ! ?i = (¬sign l)" unfolding falsifies⇩_{l}_def by meson moreover then have "?i < length ds" using assms by auto moreover then have "ds ! ?i = (¬sign l)" using i_p nth_append[of ds d ?i] by auto ultimately show ?thesis using assms unfolding falsifies⇩_{l}_def by simp qed theorem herbrand'_contra: assumes finite_cs: "finite Cs" "∀C∈Cs. finite C" assumes unsat: "∀G. ¬eval⇩_{c}⇩_{s}HFun G Cs" shows "∃T. ∀G. branch G T ⟶ closed_branch G T Cs" proof - from finite_cs unsat have "(∀T. ∃G. open_branch G T Cs) ⟶ (∃G. eval⇩_{c}⇩_{s}HFun G Cs)" using herbrand' by blast then show ?thesis using unsat by blast qed theorem herbrand: assumes unsat: "∀G. ¬eval⇩_{c}⇩_{s}HFun G Cs" assumes finite_cs: "finite Cs" "∀C∈Cs. finite C" shows "∃T. closed_tree T Cs" proof - from unsat finite_cs obtain T where "anybranch T (λb. closed_branch b T Cs)" using herbrand'_contra[of Cs] by blast then have "∃T. anybranch T (λp. falsifies⇩_{c}⇩_{s}p Cs) ∧ anyinternal T (λp. ¬ falsifies⇩_{c}⇩_{s}p Cs)" using cutoff_branch_internal[of T "λp. falsifies⇩_{c}⇩_{s}p Cs"] by blast then show ?thesis unfolding closed_tree_def by auto qed end

# Theory Completeness

section ‹Lifting Lemma› theory Completeness imports Resolution begin locale unification = assumes unification: "⋀σ L. finite L ⟹ unifier⇩_{l}⇩_{s}σ L ⟹ ∃θ. mgu⇩_{l}⇩_{s}θ L" begin text ‹ A proof of this assumption is available in @{file ‹Unification_Theorem.thy›} and used in @{file ‹Completeness_Instance.thy›}. › lemma lifting: assumes fin: "finite C⇩_{1}∧ finite C⇩_{2}" assumes apart: "vars⇩_{l}⇩_{s}C⇩_{1}∩ vars⇩_{l}⇩_{s}C⇩_{2}= {}" assumes inst: "instance_of⇩_{l}⇩_{s}C⇩_{1}' C⇩_{1}∧ instance_of⇩_{l}⇩_{s}C⇩_{2}' C⇩_{2}" assumes appl: "applicable C⇩_{1}' C⇩_{2}' L⇩_{1}' L⇩_{2}' σ" shows "∃L⇩_{1}L⇩_{2}τ. applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}τ ∧ instance_of⇩_{l}⇩_{s}(resolution C⇩_{1}' C⇩_{2}' L⇩_{1}' L⇩_{2}' σ) (resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}τ)" proof - ― ‹Obtaining the subsets we resolve upon:› let ?R⇩_{1}' = "C⇩_{1}' - L⇩_{1}'" and ?R⇩_{2}' = "C⇩_{2}' - L⇩_{2}'" from inst obtain γ μ where "C⇩_{1}⋅⇩_{l}⇩_{s}γ = C⇩_{1}' ∧ C⇩_{2}⋅⇩_{l}⇩_{s}μ = C⇩_{2}'" unfolding instance_of⇩_{l}⇩_{s}_def by auto then obtain η where η_p: "C⇩_{1}⋅⇩_{l}⇩_{s}η = C⇩_{1}' ∧ C⇩_{2}⋅⇩_{l}⇩_{s}η = C⇩_{2}'" using apart merge_sub by force from η_p obtain L⇩_{1}where L⇩_{1}_p: "L⇩_{1}⊆ C⇩_{1}∧ L⇩_{1}⋅⇩_{l}⇩_{s}η = L⇩_{1}' ∧ (C⇩_{1}- L⇩_{1}) ⋅⇩_{l}⇩_{s}η = ?R⇩_{1}'" using appl project_sub using applicable_def by metis let ?R⇩_{1}= "C⇩_{1}- L⇩_{1}" from η_p obtain L⇩_{2}where L⇩_{2}_p: "L⇩_{2}⊆ C⇩_{2}∧ L⇩_{2}⋅⇩_{l}⇩_{s}η = L⇩_{2}' ∧ (C⇩_{2}- L⇩_{2}) ⋅⇩_{l}⇩_{s}η = ?R⇩_{2}'" using appl project_sub using applicable_def by metis let ?R⇩_{2}= "C⇩_{2}- L⇩_{2}" ― ‹Obtaining substitutions:› from appl have "mgu⇩_{l}⇩_{s}σ (L⇩_{1}' ∪ L⇩_{2}'⇧^{C})" using applicable_def by auto then have "mgu⇩_{l}⇩_{s}σ ((L⇩_{1}⋅⇩_{l}⇩_{s}η) ∪ (L⇩_{2}⋅⇩_{l}⇩_{s}η)⇧^{C})" using L⇩_{1}_p L⇩_{2}_p by auto then have "mgu⇩_{l}⇩_{s}σ ((L⇩_{1}∪ L⇩_{2}⇧^{C}) ⋅⇩_{l}⇩_{s}η)" using compls_subls subls_union by auto then have "unifier⇩_{l}⇩_{s}σ ((L⇩_{1}∪ L⇩_{2}⇧^{C}) ⋅⇩_{l}⇩_{s}η)" using mgu⇩_{l}⇩_{s}_def by auto then have ησuni: "unifier⇩_{l}⇩_{s}(η ⋅ σ) (L⇩_{1}∪ L⇩_{2}⇧^{C})" using unifier⇩_{l}⇩_{s}_def composition_conseq2l by auto then obtain τ where τ_p: "mgu⇩_{l}⇩_{s}τ (L⇩_{1}∪ L⇩_{2}⇧^{C})" using unification fin L⇩_{1}_p L⇩_{2}_p by (meson finite_UnI finite_imageI rev_finite_subset) then obtain φ where φ_p: "τ ⋅ φ = η ⋅ σ" using ησuni mgu⇩_{l}⇩_{s}_def by auto ― ‹Showing that we have the desired resolvent:› let ?C = "((C⇩_{1}- L⇩_{1}) ∪ (C⇩_{2}- L⇩_{2})) ⋅⇩_{l}⇩_{s}τ" have "?C ⋅⇩_{l}⇩_{s}φ = (?R⇩_{1}∪ ?R⇩_{2}) ⋅⇩_{l}⇩_{s}(τ ⋅ φ)" using subls_union composition_conseq2ls by auto also have "... = (?R⇩_{1}∪ ?R⇩_{2}) ⋅⇩_{l}⇩_{s}(η ⋅ σ)" using φ_p by auto also have "... = ((?R⇩_{1}⋅⇩_{l}⇩_{s}η) ∪ (?R⇩_{2}⋅⇩_{l}⇩_{s}η)) ⋅⇩_{l}⇩_{s}σ" using subls_union composition_conseq2ls by auto also have "... = (?R⇩_{1}' ∪ ?R⇩_{2}') ⋅⇩_{l}⇩_{s}σ" using η_p L⇩_{1}_p L⇩_{2}_p by auto finally have "?C ⋅⇩_{l}⇩_{s}φ = ((C⇩_{1}' - L⇩_{1}') ∪ (C⇩_{2}' - L⇩_{2}')) ⋅⇩_{l}⇩_{s}σ" by auto then have ins: "instance_of⇩_{l}⇩_{s}(resolution C⇩_{1}' C⇩_{2}' L⇩_{1}' L⇩_{2}' σ) (resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}τ)" using resolution_def instance_of⇩_{l}⇩_{s}_def by metis ― ‹Showing that the resolution rule is applicable:› have "C⇩_{1}' ≠ {} ∧ C⇩_{2}' ≠ {} ∧ L⇩_{1}' ≠ {} ∧ L⇩_{2}' ≠ {}" using appl applicable_def by auto then have "C⇩_{1}≠ {} ∧ C⇩_{2}≠ {} ∧ L⇩_{1}≠ {} ∧ L⇩_{2}≠ {}" using η_p L⇩_{1}_p L⇩_{2}_p by auto then have appli: "applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}τ" using apart L⇩_{1}_p L⇩_{2}_p τ_p applicable_def by auto from ins appli show ?thesis by auto qed section ‹Completeness› lemma falsifies⇩_{g}_empty: assumes "falsifies⇩_{g}[] C" shows "C = {}" proof - have "∀l ∈ C. False" proof fix l assume "l∈C" then have "falsifies⇩_{l}[] l" using assms by auto then show False unfolding falsifies⇩_{l}_def by (cases l) auto qed then show ?thesis by auto qed lemma falsifies⇩_{c}⇩_{s}_empty: assumes "falsifies⇩_{c}[] C" shows "C = {}" proof - from assms obtain C' where C'_p: "instance_of⇩_{l}⇩_{s}C' C ∧ falsifies⇩_{g}[] C'" by auto then have "C'= {}" using falsifies⇩_{g}_empty by auto then show "C = {}" using C'_p unfolding instance_of⇩_{l}⇩_{s}_def by auto qed lemma complements_do_not_falsify': assumes l1C1': "l⇩_{1}∈ C⇩_{1}'" assumes l⇩_{2}C1': "l⇩_{2}∈ C⇩_{1}'" assumes comp: "l⇩_{1}= l⇩_{2}⇧^{c}" assumes falsif: "falsifies⇩_{g}G C⇩_{1}'" shows "False" proof (cases l⇩_{1}) case (Pos p ts) let ?i1 = "nat_of_fatom (p, ts)" from assms have gr: "ground⇩_{l}l⇩_{1}" unfolding falsifies⇩_{l}_def by auto then have Neg: "l⇩_{2}= Neg p ts" using comp Pos by (cases l⇩_{2}) auto from falsif have "falsifies⇩_{l}G l⇩_{1}" using l1C1' by auto then have "G ! ?i1 = False" using l1C1' Pos unfolding falsifies⇩_{l}_def by (induction "Pos p ts") auto moreover let ?i2 = "nat_of_fatom (get_atom l⇩_{2})" from falsif have "falsifies⇩_{l}G l⇩_{2}" using l⇩_{2}C1' by auto then have "G ! ?i2 = (¬sign l⇩_{2})" unfolding falsifies⇩_{l}_def by meson then have "G ! ?i1 = (¬sign l⇩_{2})" using Pos Neg comp by simp then have "G ! ?i1 = True" using Neg by auto ultimately show ?thesis by auto next case (Neg p ts) let ?i1 = "nat_of_fatom (p,ts)" from assms have gr: "ground⇩_{l}l⇩_{1}" unfolding falsifies⇩_{l}_def by auto then have Pos: "l⇩_{2}= Pos p ts" using comp Neg by (cases l⇩_{2}) auto from falsif have "falsifies⇩_{l}G l⇩_{1}" using l1C1' by auto then have "G ! ?i1 = True" using l1C1' Neg unfolding falsifies⇩_{l}_def by (metis get_atom.simps(2) literal.disc(2)) moreover let ?i2 = "nat_of_fatom (get_atom l⇩_{2})" from falsif have "falsifies⇩_{l}G l⇩_{2}" using l⇩_{2}C1' by auto then have "G ! ?i2 = (¬sign l⇩_{2})" unfolding falsifies⇩_{l}_def by meson then have "G ! ?i1 = (¬sign l⇩_{2})" using Pos Neg comp by simp then have "G ! ?i1 = False" using Pos using literal.disc(1) by blast ultimately show ?thesis by auto qed lemma complements_do_not_falsify: assumes l1C1': "l⇩_{1}∈ C⇩_{1}'" assumes l⇩_{2}C1': "l⇩_{2}∈ C⇩_{1}'" assumes fals: "falsifies⇩_{g}G C⇩_{1}'" shows "l⇩_{1}≠ l⇩_{2}⇧^{c}" using assms complements_do_not_falsify' by blast lemma other_falsified: assumes C1'_p: "ground⇩_{l}⇩_{s}C⇩_{1}' ∧ falsifies⇩_{g}(B@[d]) C⇩_{1}'" assumes l_p: "l ∈ C⇩_{1}'" "nat_of_fatom (get_atom l) = length B" assumes other: "lo ∈ C⇩_{1}'" "lo ≠ l" shows "falsifies⇩_{l}B lo" proof - let ?i = "nat_of_fatom (get_atom lo)" have ground_l⇩_{2}: "ground⇩_{l}l" using l_p C1'_p by auto ― ‹They are, of course, also ground:› have ground_lo: "ground⇩_{l}lo" using C1'_p other by auto from C1'_p have "falsifies⇩_{g}(B@[d]) (C⇩_{1}' - {l})" by auto ― ‹And indeed, falsified by @{term "B@[d]"}:› then have loB⇩_{2}: "falsifies⇩_{l}(B@[d]) lo" using other by auto then have "?i < length (B @ [d])" unfolding falsifies⇩_{l}_def by meson ― ‹And they have numbers in the range of @{term "B@[d]"}, i.e. less than @{term "length B + 1"}:› then have "nat_of_fatom (get_atom lo) < length B + 1" using undiag_diag_fatom by (cases lo) auto moreover have l_lo: "l≠lo" using other by auto ― ‹The are not the complement of @{term l }, since then the clause could not be falsified:› have lc_lo: "lo ≠ l⇧^{c}" using C1'_p l_p other complements_do_not_falsify[of lo C⇩_{1}' l "(B@[d])"] by auto from l_lo lc_lo have "get_atom l ≠ get_atom lo" using sign_comp_atom by metis then have "nat_of_fatom (get_atom lo) ≠ nat_of_fatom (get_atom l)" using nat_of_fatom_bij ground_lo ground_l⇩_{2}ground⇩_{l}_ground_fatom unfolding bij_betw_def inj_on_def by metis ― ‹Therefore they have different numbers:› then have "nat_of_fatom (get_atom lo) ≠ length B" using l_p by auto ultimately ― ‹So their numbers are in the range of @{term B}:› have "nat_of_fatom (get_atom lo) < length B" by auto ― ‹So we did not need the last index of @{term "B@[d]"} to falsify them, i.e. @{term B} suffices:› then show "falsifies⇩_{l}B lo" using loB⇩_{2}shorter_falsifies⇩_{l}by blast qed theorem completeness': assumes "closed_tree T Cs" assumes "∀C∈Cs. finite C" shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" using assms proof (induction T arbitrary: Cs rule: measure_induct_rule[of treesize]) fix T :: tree fix Cs :: "fterm clause set" assume ih: "⋀T' Cs. treesize T' < treesize T ⟹ closed_tree T' Cs ⟹ ∀C∈Cs. finite C ⟹ ∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" assume clo: "closed_tree T Cs" assume finite_Cs: "∀C∈Cs. finite C" { ― ‹Base case:› assume "treesize T = 0" then have "T=Leaf" using treesize_Leaf by auto then have "closed_branch [] Leaf Cs" using branch_inv_Leaf clo unfolding closed_tree_def by auto then have "falsifies⇩_{c}⇩_{s}[] Cs" by auto then have "{} ∈ Cs" using falsifies⇩_{c}⇩_{s}_empty by auto then have "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" unfolding resolution_deriv_def by auto } moreover { ― ‹Induction case:› assume "treesize T > 0" then have "∃l r. T=Branching l r" by (cases T) auto ― ‹Finding sibling branches and their corresponding clauses:› then obtain B where b_p: "internal B T ∧ branch (B@[True]) T ∧ branch (B@[False]) T" using internal_branch[of _ "[]" _ T] Branching_Leaf_Leaf_Tree by fastforce let ?B⇩_{1}= "B@[True]" let ?B⇩_{2}= "B@[False]" obtain C⇩_{1}o where C⇩_{1}o_p: "C⇩_{1}o ∈ Cs ∧ falsifies⇩_{c}?B⇩_{1}C⇩_{1}o" using b_p clo unfolding closed_tree_def by metis obtain C⇩_{2}o where C⇩_{2}o_p: "C⇩_{2}o ∈ Cs ∧ falsifies⇩_{c}?B⇩_{2}C⇩_{2}o" using b_p clo unfolding closed_tree_def by metis ― ‹Standardizing the clauses apart:› let ?C⇩_{1}= "std⇩_{1}C⇩_{1}o" let ?C⇩_{2}= "std⇩_{2}C⇩_{2}o" have C⇩_{1}_p: "falsifies⇩_{c}?B⇩_{1}?C⇩_{1}" using std⇩_{1}_falsifies C⇩_{1}o_p by auto have C⇩_{2}_p: "falsifies⇩_{c}?B⇩_{2}?C⇩_{2}" using std⇩_{2}_falsifies C⇩_{2}o_p by auto have fin: "finite ?C⇩_{1}∧ finite ?C⇩_{2}" using C⇩_{1}o_p C⇩_{2}o_p finite_Cs by auto ― ‹We go down to the ground world.› ― ‹Finding the falsifying ground instance @{term C⇩_{1}'} of @{term ?C⇩_{1}}, and proving properties about it:› ― ‹@{term C⇩_{1}'} is falsified by @{term ?B⇩_{1}}:› from C⇩_{1}_p obtain C⇩_{1}' where C⇩_{1}'_p: "ground⇩_{l}⇩_{s}C⇩_{1}' ∧ instance_of⇩_{l}⇩_{s}C⇩_{1}' ?C⇩_{1}∧ falsifies⇩_{g}?B⇩_{1}C⇩_{1}'" by metis have "¬falsifies⇩_{c}B C⇩_{1}o" using C⇩_{1}o_p b_p clo unfolding closed_tree_def by metis then have "¬falsifies⇩_{c}B ?C⇩_{1}" using std⇩_{1}_falsifies using prod.exhaust_sel by blast ― ‹@{term C⇩_{1}'} is not falsified by @{term B}:› then have l_B: "¬falsifies⇩_{g}B C⇩_{1}'" using C⇩_{1}'_p by auto ― ‹@{term C⇩_{1}'} contains a literal @{term l⇩_{1}} that is falsified by @{term ?B⇩_{1}}, but not @{term B}:› from C⇩_{1}'_p l_B obtain l⇩_{1}where l⇩_{1}_p: "l⇩_{1}∈ C⇩_{1}' ∧ falsifies⇩_{l}(B@[True]) l⇩_{1}∧ ¬(falsifies⇩_{l}B l⇩_{1})" by auto let ?i = "nat_of_fatom (get_atom l⇩_{1})" ― ‹@{term l⇩_{1}} is of course ground:› have ground_l⇩_{1}: "ground⇩_{l}l⇩_{1}" using C⇩_{1}'_p l⇩_{1}_p by auto from l⇩_{1}_p have "¬(?i < length B ∧ B ! ?i = (¬sign l⇩_{1}))" using ground_l⇩_{1}unfolding falsifies⇩_{l}_def by meson then have "¬(?i < length B ∧ (B@[True]) ! ?i = (¬sign l⇩_{1}))" by (metis nth_append) ― ‹Not falsified by @{term B}.› moreover from l⇩_{1}_p have "?i < length (B @ [True]) ∧ (B @ [True]) ! ?i = (¬sign l⇩_{1})" unfolding falsifies⇩_{l}_def by meson ultimately have l⇩_{1}_sign_no: "?i = length B ∧ (B @ [True]) ! ?i = (¬sign l⇩_{1})" by auto ― ‹@{term l⇩_{1}} is negative:› from l⇩_{1}_sign_no have l⇩_{1}_sign: "sign l⇩_{1}= False" by auto from l⇩_{1}_sign_no have l⇩_{1}_no: "nat_of_fatom (get_atom l⇩_{1}) = length B" by auto ― ‹All the other literals in @{term C⇩_{1}'} must be falsified by B, since they are falsified by @{term ?B⇩_{1}}, but not @{term l⇩_{1}}.› from C⇩_{1}'_p l⇩_{1}_no l⇩_{1}_p have B_C⇩_{1}'l⇩_{1}: "falsifies⇩_{g}B (C⇩_{1}' - {l⇩_{1}})" (* This should be a lemma *) using other_falsified by blast ― ‹We do the same exercise for @{term ?C⇩_{2}}, @{term C⇩_{2}'}, @{term ?B⇩_{2}}, @{term l⇩_{2}}:› from C⇩_{2}_p obtain C⇩_{2}' where C⇩_{2}'_p: "ground⇩_{l}⇩_{s}C⇩_{2}' ∧ instance_of⇩_{l}⇩_{s}C⇩_{2}' ?C⇩_{2}∧ falsifies⇩_{g}?B⇩_{2}C⇩_{2}'" by metis have "¬falsifies⇩_{c}B C⇩_{2}o" using C⇩_{2}o_p b_p clo unfolding closed_tree_def by metis then have "¬falsifies⇩_{c}B ?C⇩_{2}" using std⇩_{2}_falsifies using prod.exhaust_sel by blast then have l_B: "¬falsifies⇩_{g}B C⇩_{2}'" using C⇩_{2}'_p by auto (* I already had something called l_B... I could give it a new name *) ― ‹@{term C⇩_{2}'} contains a literal @{term l⇩_{2}} that is falsified by @{term ?B⇩_{2}}, but not B:› from C⇩_{2}'_p l_B obtain l⇩_{2}where l⇩_{2}_p: "l⇩_{2}∈ C⇩_{2}' ∧ falsifies⇩_{l}(B@[False]) l⇩_{2}∧ ¬falsifies⇩_{l}B l⇩_{2}" by auto let ?i = "nat_of_fatom (get_atom l⇩_{2})" have ground_l⇩_{2}: "ground⇩_{l}l⇩_{2}" using C⇩_{2}'_p l⇩_{2}_p by auto from l⇩_{2}_p have "¬(?i < length B ∧ B ! ?i = (¬sign l⇩_{2}))" using ground_l⇩_{2}unfolding falsifies⇩_{l}_def by meson then have "¬(?i < length B ∧ (B@[False]) ! ?i = (¬sign l⇩_{2}))" by (metis nth_append) ― ‹Not falsified by @{term B}.› moreover from l⇩_{2}_p have "?i < length (B @ [False]) ∧ (B @ [False]) ! ?i = (¬sign l⇩_{2})" unfolding falsifies⇩_{l}_def by meson ultimately have l⇩_{2}_sign_no: "?i = length B ∧ (B @ [False]) ! ?i = (¬sign l⇩_{2})" by auto ― ‹@{term l⇩_{2}} is negative:› from l⇩_{2}_sign_no have l⇩_{2}_sign: "sign l⇩_{2}= True" by auto from l⇩_{2}_sign_no have l⇩_{2}_no: "nat_of_fatom (get_atom l⇩_{2}) = length B" by auto ― ‹All the other literals in @{term C⇩_{2}'} must be falsified by B, since they are falsified by @{term ?B⇩_{2}}, but not @{term l⇩_{2}}.› from C⇩_{2}'_p l⇩_{2}_no l⇩_{2}_p have B_C⇩_{2}'l⇩_{2}: "falsifies⇩_{g}B (C⇩_{2}' - {l⇩_{2}})" using other_falsified by blast ― ‹Proving some properties about @{term C⇩_{1}'} and @{term C⇩_{2}'}, @{term l⇩_{1}} and @{term l⇩_{2}}, as well as the resolvent of @{term C⇩_{1}'} and @{term C⇩_{2}'}:› have l⇩_{2}cisl⇩_{1}: "l⇩_{2}⇧^{c}= l⇩_{1}" (* Could perhaps be a lemma *) proof - from l⇩_{1}_no l⇩_{2}_no ground_l⇩_{1}ground_l⇩_{2}have "get_atom l⇩_{1}= get_atom l⇩_{2}" using nat_of_fatom_bij ground⇩_{l}_ground_fatom unfolding bij_betw_def inj_on_def by metis then show "l⇩_{2}⇧^{c}= l⇩_{1}" using l⇩_{1}_sign l⇩_{2}_sign using sign_comp_atom by metis qed have "applicable C⇩_{1}' C⇩_{2}' {l⇩_{1}} {l⇩_{2}} Resolution.ε" unfolding applicable_def using l⇩_{1}_p l⇩_{2}_p C⇩_{1}'_p ground⇩_{l}⇩_{s}_vars⇩_{l}⇩_{s}l⇩_{2}cisl⇩_{1}empty_comp2 unfolding mgu⇩_{l}⇩_{s}_def unifier⇩_{l}⇩_{s}_def by auto ― ‹Lifting to get a resolvent of @{term ?C⇩_{1}} and @{term ?C⇩_{2}}:› then obtain L⇩_{1}L⇩_{2}τ where L⇩_{1}L⇩_{2}τ_p: "applicable ?C⇩_{1}?C⇩_{2}L⇩_{1}L⇩_{2}τ ∧ instance_of⇩_{l}⇩_{s}(resolution C⇩_{1}' C⇩_{2}' {l⇩_{1}} {l⇩_{2}} Resolution.ε) (resolution ?C⇩_{1}?C⇩_{2}L⇩_{1}L⇩_{2}τ)" using std_apart_apart C⇩_{1}'_p C⇩_{2}'_p lifting[of ?C⇩_{1}?C⇩_{2}C⇩_{1}' C⇩_{2}' "{l⇩_{1}}" "{l⇩_{2}}" Resolution.ε] fin by auto ― ‹Defining the clause to be derived, the new clausal form and the new tree:› ― ‹We name the resolvent @{term C}.› obtain C where C_p: "C = resolution ?C⇩_{1}?C⇩_{2}L⇩_{1}L⇩_{2}τ" by auto obtain CsNext where CsNext_p: "CsNext = Cs ∪ {?C⇩_{1}, ?C⇩_{2}, C}" by auto obtain T'' where T''_p: "T'' = delete B T" by auto ― ‹Here we delete the two branch children @{term ?B⇩_{1}} and @{term ?B⇩_{2}} of @{term B}.› ― ‹Our new clause is falsified by the branch @{term B} of our new tree:› have "falsifies⇩_{g}B ((C⇩_{1}' - {l⇩_{1}}) ∪ (C⇩_{2}' - {l⇩_{2}}))" using B_C⇩_{1}'l⇩_{1}B_C⇩_{2}'l⇩_{2}by cases auto then have "falsifies⇩_{g}B (resolution C⇩_{1}' C⇩_{2}' {l⇩_{1}} {l⇩_{2}} Resolution.ε)" unfolding resolution_def empty_subls by auto then have falsifies_C: "falsifies⇩_{c}B C" using C_p L⇩_{1}L⇩_{2}τ_p by auto have T''_smaller: "treesize T'' < treesize T" using treezise_delete T''_p b_p by auto have T''_bran: "anybranch T'' (λb. closed_branch b T'' CsNext)" proof (rule allI; rule impI) fix b assume br: "branch b T''" from br have "b = B ∨ branch b T" using branch_delete T''_p by auto then show "closed_branch b T'' CsNext" proof assume "b=B" then show "closed_branch b T'' CsNext" using falsifies_C br CsNext_p by auto next assume "branch b T" then show "closed_branch b T'' CsNext" using clo br T''_p CsNext_p unfolding closed_tree_def by auto qed qed then have T''_bran2: "anybranch T'' (λb. falsifies⇩_{c}⇩_{s}b CsNext)" by auto (* replace T''_bran with this maybe? *) ― ‹We cut the tree even smaller to ensure only the branches are falsified, i.e. it is a closed tree:› obtain T' where T'_p: "T' = cutoff (λG. falsifies⇩_{c}⇩_{s}G CsNext) [] T''" by auto have T'_smaller: "treesize T' < treesize T" using treesize_cutoff[of "λG. falsifies⇩_{c}⇩_{s}G CsNext" "[]" T''] T''_smaller unfolding T'_p by auto from T''_bran2 have "anybranch T' (λb. falsifies⇩_{c}⇩_{s}b CsNext)" using cutoff_branch[of T'' "λb. falsifies⇩_{c}⇩_{s}b CsNext"] T'_p by auto then have T'_bran: "anybranch T' (λb. closed_branch b T' CsNext)" by auto have T'_intr: "anyinternal T' (λp. ¬falsifies⇩_{c}⇩_{s}p CsNext)" using T'_p cutoff_internal[of T'' "λb. falsifies⇩_{c}⇩_{s}b CsNext"] T''_bran2 by blast have T'_closed: "closed_tree T' CsNext" using T'_bran T'_intr unfolding closed_tree_def by auto have finite_CsNext: "∀C∈CsNext. finite C" unfolding CsNext_p C_p resolution_def using finite_Cs fin by auto ― ‹By induction hypothesis we get a resolution derivation of @{term "{}"} from our new clausal form:› from T'_smaller T'_closed have "∃Cs''. resolution_deriv CsNext Cs'' ∧ {} ∈ Cs''" using ih[of T' CsNext] finite_CsNext by blast then obtain Cs'' where Cs''_p: "resolution_deriv CsNext Cs'' ∧ {} ∈ Cs''" by auto moreover { ― ‹Proving that we can actually derive the new clausal form:› have "resolution_step Cs (Cs ∪ {?C⇩_{1}})" using std⇩_{1}_renames standardize_apart C⇩_{1}o_p by (metis Un_insert_right) moreover have "resolution_step (Cs ∪ {?C⇩_{1}}) (Cs ∪ {?C⇩_{1}} ∪ {?C⇩_{2}})" using std⇩_{2}_renames[of C⇩_{2}o] standardize_apart[of C⇩_{2}o _ ?C⇩_{2}] C⇩_{2}o_p by auto then have "resolution_step (Cs ∪ {?C⇩_{1}}) (Cs ∪ {?C⇩_{1},?C⇩_{2}})" by (simp add: insert_commute) moreover then have "resolution_step (Cs ∪ {?C⇩_{1},?C⇩_{2}}) (Cs ∪ {?C⇩_{1},?C⇩_{2}} ∪ {C})" using L⇩_{1}L⇩_{2}τ_p resolution_rule[of ?C⇩_{1}"Cs ∪ {?C⇩_{1},?C⇩_{2}}" ?C⇩_{2}L⇩_{1}L⇩_{2}τ ] using C_p by auto then have "resolution_step (Cs ∪ {?C⇩_{1},?C⇩_{2}}) CsNext" using CsNext_p by (simp add: Un_commute) ultimately have "resolution_deriv Cs CsNext" unfolding resolution_deriv_def by auto } ― ‹Combining the two derivations, we get the desired derivation from @{term Cs} of @{term "{}"}:› ultimately have "resolution_deriv Cs Cs''" unfolding resolution_deriv_def by auto then have "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" using Cs''_p by auto } ultimately show "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" by auto qed theorem completeness: assumes finite_cs: "finite Cs" "∀C∈Cs. finite C" assumes unsat: "∀(F::hterm fun_denot) (G::hterm pred_denot) . ¬eval⇩_{c}⇩_{s}F G Cs" shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" proof - from unsat have "∀(G::hterm pred_denot) . ¬eval⇩_{c}⇩_{s}HFun G Cs" by auto then obtain T where "closed_tree T Cs" using herbrand assms by blast then show "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" using completeness' assms by auto qed definition E_conv :: "('a ⇒ 'b) ⇒ 'a var_denot ⇒ 'b var_denot" where "E_conv b_of_a E ≡ λx. (b_of_a (E x))" definition F_conv :: "('a ⇒ 'b) ⇒ 'a fun_denot ⇒ 'b fun_denot" where "F_conv b_of_a F ≡ λf bs. b_of_a (F f (map (inv b_of_a) bs))" definition G_conv :: "('a ⇒ 'b) ⇒ 'a pred_denot ⇒ 'b pred_denot" where "G_conv b_of_a G ≡ λp bs. (G p (map (inv b_of_a) bs))" lemma eval⇩_{t}_bij: assumes "bij (b_of_a::'a ⇒ 'b)" shows"eval⇩_{t}(E_conv b_of_a E) (F_conv b_of_a F) t = b_of_a (eval⇩_{t}E F t)" proof (induction t) case (Fun f ts) then have "map (inv b_of_a ∘ eval⇩_{t}(E_conv b_of_a E) (F_conv b_of_a F)) ts = eval⇩_{t}⇩_{s}E F ts" unfolding E_conv_def F_conv_def using assms bij_is_inj by fastforce then have "b_of_a (F f (map (inv b_of_a ∘ eval⇩_{t}(E_conv b_of_a E) ((F_conv b_of_a F))) ts)) = b_of_a (F f (eval⇩_{t}⇩_{s}E F ts))" by metis then show ?case using assms unfolding E_conv_def F_conv_def by auto next case (Var x) then show ?case using assms unfolding E_conv_def by auto qed lemma eval⇩_{t}⇩_{s}_bij: assumes "bij (b_of_a::'a ⇒ 'b)" shows "G_conv b_of_a G p (eval⇩_{t}⇩_{s}(E_conv b_of_a E) (F_conv b_of_a F) ts) = G p (eval⇩_{t}⇩_{s}E F ts)" using assms using eval⇩_{t}_bij proof - have "map (inv b_of_a ∘ eval⇩_{t}(E_conv b_of_a E) (F_conv b_of_a F)) ts = eval⇩_{t}⇩_{s}E F ts" using eval⇩_{t}_bij assms bij_is_inj by fastforce then show ?thesis by (metis (no_types) G_conv_def map_map) qed lemma eval⇩_{l}_bij: assumes "bij (b_of_a::'a ⇒ 'b)" shows "eval⇩_{l}(E_conv b_of_a E) (F_conv b_of_a F) (G_conv b_of_a G) l = eval⇩_{l}E F G l" using assms eval⇩_{t}⇩_{s}_bij proof (cases l) case (Pos p ts) then show ?thesis by (simp add: eval⇩_{t}⇩_{s}_bij assms) next case (Neg p ts) then show ?thesis by (simp add: eval⇩_{t}⇩_{s}_bij assms) qed lemma eval⇩_{c}_bij: assumes "bij (b_of_a::'a ⇒ 'b)" shows "eval⇩_{c}(F_conv b_of_a F) (G_conv b_of_a G) C = eval⇩_{c}F G C" proof - { fix E :: "char list ⇒ 'b" assume bij_b_of_a: "bij b_of_a" assume C_sat: "∀E :: char list ⇒ 'a. ∃l∈C. eval⇩_{l}E F G l" have E_p: "E = E_conv b_of_a (E_conv (inv b_of_a) E)" unfolding E_conv_def using bij_b_of_a using bij_betw_inv_into_right by fastforce have "∃l∈C. eval⇩_{l}(E_conv b_of_a (E_conv (inv b_of_a) E)) (F_conv b_of_a F) (G_conv b_of_a G) l" using eval⇩_{l}_bij bij_b_of_a C_sat by blast then have "∃l∈C. eval⇩_{l}E (F_conv b_of_a F) (G_conv b_of_a G) l" using E_p by auto } then show ?thesis by (meson eval⇩_{l}_bij assms eval⇩_{c}_def) qed lemma eval⇩_{c}⇩_{s}_bij: assumes "bij (b_of_a::'a ⇒ 'b)" shows "eval⇩_{c}⇩_{s}(F_conv b_of_a F) (G_conv b_of_a G) Cs ⟷ eval⇩_{c}⇩_{s}F G Cs" by (meson eval⇩_{c}_bij assms eval⇩_{c}⇩_{s}_def) lemma countably_inf_bij: assumes inf_a_uni: "infinite (UNIV :: ('a ::countable) set)" assumes inf_b_uni: "infinite (UNIV :: ('b ::countable) set)" shows "∃b_of_a :: 'a ⇒ 'b. bij b_of_a" proof - let ?S = "UNIV :: (('a::countable)) set" have "countable ?S" by auto moreover have "infinite ?S" using inf_a_uni by auto ultimately obtain nat_of_a where QWER: "bij (nat_of_a :: 'a ⇒ nat)" using countableE_infinite[of ?S] by blast let ?T = "UNIV :: (('b::countable)) set" have "countable ?T" by auto moreover have "infinite ?T" using inf_b_uni by auto ultimately obtain nat_of_b where TYUI: "bij (nat_of_b :: 'b ⇒ nat)" using countableE_infinite[of ?T] by blast let ?b_of_a = "λa. (inv nat_of_b) (nat_of_a a)" have bij_nat_of_b: "∀n. nat_of_b (inv nat_of_b n) = n" using TYUI bij_betw_inv_into_right by fastforce have "∀a. inv nat_of_a (nat_of_a a) = a" by (meson QWER UNIV_I bij_betw_inv_into_left) then have "inj (λa. inv nat_of_b (nat_of_a a))" using bij_nat_of_b injI by (metis (no_types)) moreover have "range (λa. inv nat_of_b (nat_of_a a)) = UNIV" by (metis QWER TYUI bij_def image_image inj_imp_surj_inv) ultimately have "bij ?b_of_a" unfolding bij_def by auto then show ?thesis by auto qed lemma infinite_hterms: "infinite (UNIV :: hterm set)" proof - let ?diago = "λn. HFun (string_of_nat n) []" let ?undiago = "λa. nat_of_string (case a of HFun f ts ⇒ f)" have "∀n. ?undiago (?diago n) = n" using nat_of_string_string_of_nat by auto moreover have "∀n. ?diago n ∈ UNIV" by auto ultimately show "infinite (UNIV :: hterm set)" using infinity[of ?undiago ?diago UNIV] by simp qed theorem completeness_countable: assumes inf_uni: "infinite (UNIV :: ('u :: countable) set)" assumes finite_cs: "finite Cs" "∀C∈Cs. finite C" assumes unsat: "∀(F::'u fun_denot) (G::'u pred_denot). ¬eval⇩_{c}⇩_{s}F G Cs" shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" proof - have "∀(F::hterm fun_denot) (G::hterm pred_denot) . ¬eval⇩_{c}⇩_{s}F G Cs" proof (rule; rule) fix F :: "hterm fun_denot" fix G :: "hterm pred_denot" obtain u_of_hterm :: "hterm ⇒ 'u" where p_u_of_hterm: "bij u_of_hterm" using countably_inf_bij inf_uni infinite_hterms by auto let ?F = "F_conv u_of_hterm F" let ?G = "G_conv u_of_hterm G" have "¬ eval⇩_{c}⇩_{s}?F ?G Cs" using unsat by auto then show "¬ eval⇩_{c}⇩_{s}F G Cs" using eval⇩_{c}⇩_{s}_bij using p_u_of_hterm by auto qed then show "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" using finite_cs completeness by auto qed theorem completeness_nat: assumes finite_cs: "finite Cs" "∀C∈Cs. finite C" assumes unsat: "∀(F::nat fun_denot) (G::nat pred_denot) . ¬eval⇩_{c}⇩_{s}F G Cs" shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'" using assms completeness_countable by blast end ― ‹unification locale› end

# Theory Examples

section ‹Examples› theory Examples imports Resolution begin value "Var ''x''" value "Fun ''one'' []" value "Fun ''mul'' [Var ''y'',Var ''y'']" value "Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''], Fun ''one'' []]" value "Pos ''greater'' [Var ''x'', Var ''y'']" value "Neg ''less'' [Var ''x'', Var ''y'']" value "Pos ''less'' [Var ''x'', Var ''y'']" value "Pos ''equals'' [Fun ''add''[Fun ''mul''[Var ''y'',Var ''y''], Fun ''one''[]],Var ''x'']" fun F⇩_{n}⇩_{a}⇩_{t}:: "nat fun_denot" where "F⇩_{n}⇩_{a}⇩_{t}f [n,m] = (if f = ''add'' then n + m else if f = ''mul'' then n * m else 0)" | "F⇩_{n}⇩_{a}⇩_{t}f [] = (if f = ''one'' then 1 else if f = ''zero'' then 0 else 0)" | "F⇩_{n}⇩_{a}⇩_{t}f us = 0" fun G⇩_{n}⇩_{a}⇩_{t}:: "nat pred_denot" where "G⇩_{n}⇩_{a}⇩_{t}p [x,y] = (if p = ''less'' ∧ x < y then True else if p = ''greater'' ∧ x > y then True else if p = ''equals'' ∧ x = y then True else False)" | "G⇩_{n}⇩_{a}⇩_{t}p us = False" fun E⇩_{n}⇩_{a}⇩_{t}:: "nat var_denot" where "E⇩_{n}⇩_{a}⇩_{t}x = (if x = ''x'' then 26 else if x = ''y'' then 5 else 0)" lemma "eval⇩_{t}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}(Var ''x'') = 26" by auto lemma "eval⇩_{t}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}(Fun ''one'' []) = 1" by auto lemma "eval⇩_{t}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}(Fun ''mul'' [Var ''y'',Var ''y'']) = 25" by auto lemma "eval⇩_{t}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}(Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''], Fun ''one'' []]) = 26" by auto lemma "eval⇩_{l}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}G⇩_{n}⇩_{a}⇩_{t}(Pos ''greater'' [Var ''x'', Var ''y'']) = True" by auto lemma "eval⇩_{l}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}G⇩_{n}⇩_{a}⇩_{t}(Neg ''less'' [Var ''x'', Var ''y'']) = True" by auto lemma "eval⇩_{l}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}G⇩_{n}⇩_{a}⇩_{t}(Pos ''less'' [Var ''x'', Var ''y'']) = False" by auto lemma "eval⇩_{l}E⇩_{n}⇩_{a}⇩_{t}F⇩_{n}⇩_{a}⇩_{t}G⇩_{n}⇩_{a}⇩_{t}(Pos ''equals'' [Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''],Fun ''one'' []] ,Var ''x''] ) = True" by auto definition PP :: "fterm literal" where "PP = Pos ''P'' [Fun ''c'' []]" definition PQ :: "fterm literal" where "PQ = Pos ''Q'' [Fun ''d'' []]" definition NP :: "fterm literal" where "NP = Neg ''P'' [Fun ''c'' []]" definition NQ :: "fterm literal" where "NQ = Neg ''Q'' [Fun ''d'' []]" theorem empty_mgu: assumes "unifier⇩_{l}⇩_{s}ε L" shows "mgu⇩_{l}⇩_{s}ε L" using assms unfolding unifier⇩_{l}⇩_{s}_def mgu⇩_{l}⇩_{s}_def apply auto apply (rule_tac x=u in exI) using empty_comp1 empty_comp2 apply auto done theorem unifier_single: "unifier⇩_{l}⇩_{s}σ {l}" unfolding unifier⇩_{l}⇩_{s}_def by auto theorem resolution_rule': assumes "C⇩_{1}∈ Cs" assumes "C⇩_{2}∈ Cs" assumes "applicable C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ" assumes "C = {resolution C⇩_{1}C⇩_{2}L⇩_{1}L⇩_{2}σ}" shows "resolution_step Cs (Cs ∪ C)" using assms resolution_rule by auto lemma resolution_example1: "resolution_deriv {{NP,PQ},{NQ},{PP,PQ}} {{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}}" proof - have "resolution_step {{NP,PQ},{NQ},{PP,PQ}} ({{NP,PQ},{NQ},{PP,PQ}} ∪ {{NP}})" apply (rule resolution_rule'[of "{NP,PQ}" _ "{NQ}" "{PQ}" "{NQ}" ε]) unfolding applicable_def vars⇩_{l}⇩_{s}_def vars⇩_{l}_def NQ_def NP_def PQ_def PP_def resolution_def using unifier_single empty_mgu using empty_subls apply auto done then have "resolution_step {{NP,PQ},{NQ},{PP,PQ}} ({{NP,PQ},{NQ},{PP,PQ},{NP}})" by (simp add: insert_commute) moreover have "resolution_step {{NP,PQ},{NQ},{PP,PQ},{NP}} ({{NP,PQ},{NQ},{PP,PQ},{NP}} ∪ {{PP}})" apply (rule resolution_rule'[of "{NQ}" _ "{PP,PQ}" "{NQ}" "{PQ}" ε]) unfolding applicable_def vars⇩_{l}⇩_{s}_def vars⇩_{l}_def NQ_def NP_def PQ_def PP_def resolution_def using unifier_single empty_mgu empty_subls apply auto done then have "resolution_step {{NP,PQ},{NQ},{PP,PQ},{NP}} ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP}})" by (simp add: insert_commute) moreover have "resolution_step {{NP,PQ},{NQ},{PP,PQ},{NP},{PP}} ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP}} ∪ {{}})" apply (rule resolution_rule'[of "{NP}" _ "{PP}" "{NP}" "{PP}" ε]) unfolding applicable_def vars⇩_{l}⇩_{s}_def vars⇩_{l}_def NQ_def NP_def PQ_def PP_def resolution_def using unifier_single empty_mgu apply auto done then have "resolution_step {{NP,PQ},{NQ},{PP,PQ},{NP},{PP}} ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}})" by (simp add: insert_commute) ultimately have "resolution_deriv {{NP,PQ},{NQ},{PP,PQ}} {{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}}" unfolding resolution_deriv_def by auto then show ?thesis by auto qed definition Pa :: "fterm literal" where "Pa = Pos ''a'' []" definition Na :: "fterm literal" where "Na = Neg ''a'' []" definition Pb :: "fterm literal" where "Pb = Pos ''b'' []" definition Nb :: "fterm literal" where "Nb = Neg ''b'' []" definition Paa :: "fterm literal" where "Paa = Pos ''a'' [Fun ''a'' []]" definition Naa :: "fterm literal" where "Naa = Neg ''a'' [Fun ''a'' []]" definition Pax :: "fterm literal" where "Pax = Pos ''a'' [Var ''x'']" definition Nax :: "fterm literal" where "Nax = Neg ''a'' [Var ''x'']" definition mguPaaPax :: substitution where "mguPaaPax = (λx. if x = ''x'' then Fun ''a'' [] else Var x)" lemma mguPaaPax_mgu: "mgu⇩_{l}⇩_{s}mguPaaPax {Paa,Pax}" proof - let ?σ = "λx. if x = ''x'' then Fun ''a'' [] else Var x" have a: "unifier⇩_{l}⇩_{s}(λx. if x = ''x'' then Fun ''a'' [] else Var x) {Paa,Pax}" unfolding Paa_def Pax_def unifier⇩_{l}⇩_{s}_def by auto have b: "∀u. unifier⇩_{l}⇩_{s}u {Paa,Pax} ⟶ (∃i. u = ?σ ⋅ i)" proof (rule;rule) fix u assume "unifier⇩_{l}⇩_{s}u {Paa,Pax}" then have uuu: "u ''x'' = Fun ''a'' []" unfolding unifier⇩_{l}⇩_{s}_def Paa_def Pax_def by auto have "?σ ⋅ u = u" proof fix x { assume "x=''x''" moreover have "(?σ ⋅ u) ''x'' = Fun ''a'' []" unfolding composition_def by auto ultimately have "(?σ ⋅ u) x = u x" using uuu by auto } moreover { assume "x≠''x''" then have "(?σ ⋅ u) x = (ε x) ⋅⇩_{t}u" unfolding composition_def by auto then have "(?σ ⋅ u) x = u x" by auto } ultimately show "(?σ ⋅ u) x = u x" by auto qed then have "∃i. ?σ ⋅ i = u" by auto then show "∃i. u = ?σ ⋅ i" by auto qed from a b show ?thesis unfolding mgu⇩_{l}⇩_{s}_def unfolding mguPaaPax_def by auto qed lemma resolution_example2: "resolution_deriv {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}}" proof - have "resolution_step {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} ∪ {{Na,Pb}})" apply (rule resolution_rule'[of "{Pax}" _ "{Na,Pb,Naa}" "{Pax}" "{Naa}" mguPaaPax ]) using mguPaaPax_mgu unfolding applicable_def vars⇩_{l}⇩_{s}_def vars⇩_{l}_def Nb_def Na_def Pax_def Pa_def Pb_def Naa_def Paa_def mguPaaPax_def resolution_def apply auto apply (rule_tac x=Na in image_eqI) unfolding Na_def apply auto apply (rule_tac x=Pb in image_eqI) unfolding Pb_def apply auto done then have "resolution_step {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}})" by (simp add: insert_commute) moreover have "resolution_step {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}} ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}} ∪ {{Na}})" apply (rule resolution_rule'[of "{Nb,Na}" _ "{Na,Pb}" "{Nb}" "{Pb}" ε]) unfolding applicable_def vars⇩_{l}⇩_{s}_def vars⇩_{l}_def Pb_def Nb_def Na_def PP_def resolution_def using unifier_single empty_mgu apply auto done then have "resolution_step {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}} ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}})" by (simp add: insert_commute) moreover have "resolution_step {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}} ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}} ∪ {{}})" apply (rule resolution_rule'[of "{Na}" _ "{Pa}" "{Na}" "{Pa}" ε]) unfolding applicable_def vars⇩_{l}⇩_{s}_def vars⇩_{l}_def Pa_def Nb_def Na_def PP_def resolution_def using unifier_single empty_mgu apply auto done then have "resolution_step {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}} ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}})" by (simp add: insert_commute) ultimately have "resolution_deriv {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}}" unfolding resolution_deriv_def by auto then show ?thesis by auto qed lemma resolution_example1_sem: "¬eval⇩_{c}⇩_{s}F G {{NP, PQ}, {NQ}, {PP, PQ}}" using resolution_example1 derivation_sound_refute by auto lemma resolution_example2_sem: "¬eval⇩_{c}⇩_{s}F G {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}" using resolution_example2 derivation_sound_refute by auto end

# Theory Unification_Theorem

section ‹The Unification Theorem› theory Unification_Theorem imports First_Order_Terms.Unification Resolution begin definition set_to_list :: "'a set ⇒ 'a list" where "set_to_list ≡ inv set" lemma set_set_to_list: "finite xs ⟹ set (set_to_list xs) = xs" proof (induction rule: finite.induct) case (emptyI) have "set [] = {}" by auto then show ?case unfolding set_to_list_def inv_into_def by auto next case (insertI A a) then have "set (a#set_to_list A) = insert a A" by auto then show ?case unfolding set_to_list_def inv_into_def by (metis (mono_tags, lifting) UNIV_I someI) qed fun iterm_to_fterm :: "(fun_sym, var_sym) term ⇒ fterm" where "iterm_to_fterm (Term.Var x) = Var x" | "iterm_to_fterm (Term.Fun f ts) = Fun f (map iterm_to_fterm ts)" fun fterm_to_iterm :: "fterm ⇒ (fun_sym, var_sym) term" where "fterm_to_iterm (Var x) = Term.Var x" | "fterm_to_iterm (Fun f ts) = Term.Fun f (map fterm_to_iterm ts)" lemma iterm_to_fterm_cancel[simp]: "iterm_to_fterm (fterm_to_iterm t) = t" by (induction t) (auto simp add: map_idI) lemma fterm_to_iterm_cancel[simp]: "fterm_to_iterm (iterm_to_fterm t) = t" by (induction t) (auto simp add: map_idI) abbreviation(input) fsub_to_isub :: "substitution ⇒ (fun_sym, var_sym) subst" where "fsub_to_isub σ ≡ λx. fterm_to_iterm (σ x)" abbreviation(input) isub_to_fsub :: "(fun_sym, var_sym) subst ⇒ substitution" where "isub_to_fsub σ ≡ λx. iterm_to_fterm (σ x)" lemma iterm_to_fterm_subt: "(iterm_to_fterm t1) ⋅⇩_{t}σ = iterm_to_fterm (t1 ⋅ (λx. fterm_to_iterm (σ x)))" by (induction t1) auto lemma unifiert_unifiers: assumes "unifier⇩_{t}⇩_{s}σ ts" shows "fsub_to_isub σ ∈ unifiers (fterm_to_iterm ` ts × fterm_to_iterm ` ts)" proof - have "∀t1 ∈ fterm_to_iterm ` ts. ∀t2 ∈ fterm_to_iterm ` ts. t1 ⋅ (fsub_to_isub σ) = t2 ⋅ (fsub_to_isub σ)" proof (rule ballI;rule ballI) fix t1 t2 assume t1_p: "t1 ∈ fterm_to_iterm ` ts" assume t2_p: "t2 ∈ fterm_to_iterm ` ts" from t1_p t2_p have "iterm_to_fterm t1 ∈ ts ∧ iterm_to_fterm t2 ∈ ts" by auto