diff --git a/thys/Efficient-Mergesort/Natural_Mergesort.thy b/thys/Efficient-Mergesort/Natural_Mergesort.thy --- a/thys/Efficient-Mergesort/Natural_Mergesort.thy +++ b/thys/Efficient-Mergesort/Natural_Mergesort.thy @@ -1,163 +1,163 @@ (* Author: Christian Sternagel *) theory Natural_Mergesort imports "HOL-Data_Structures.Sorting" begin subsection \Auxiliary Results\ lemma C_merge_adj': "C_merge_adj xss \ length (concat xss)" proof (induct xss rule: C_merge_adj.induct) case (3 xs ys zss) then show ?case using C_merge_ub [of xs ys] by simp qed simp_all lemma length_concat_merge_adj: "length (concat (merge_adj xss)) = length (concat xss)" by (induct xss rule: merge_adj.induct) (simp_all add: length_merge) lemma C_merge_all': "C_merge_all xss \ length (concat xss) * \log 2 (length xss)\" proof (induction xss rule: C_merge_all.induct) case (3 xs ys zss) let ?xss = "xs # ys # zss" let ?m = "length (concat ?xss)" have *: "\log 2 (real n + 2)\ = \log 2 (Suc n div 2 + 1)\ + 1" for n :: nat using ceiling_log2_div2 [of "n + 2"] by (simp add: algebra_simps) have "C_merge_all ?xss = C_merge_adj ?xss + C_merge_all (merge_adj ?xss)" by simp also have "\ \ ?m + C_merge_all (merge_adj ?xss)" using C_merge_adj' [of ?xss] by auto also have "\ \ ?m + length (concat (merge_adj ?xss)) * \log 2 (length (merge_adj ?xss))\" using "3.IH" by simp also have "\ = ?m + ?m * \log 2 (length (merge_adj ?xss))\" by (simp only: length_concat_merge_adj) also have "\ \ ?m * \log 2 (length ?xss)\" by (auto simp: * algebra_simps) finally show ?case by simp qed simp_all subsection \Definition of Natural Mergesort\ text \ Partition input into ascending and descending subsequences. (The latter are reverted on the fly.) \ fun runs :: "('a::linorder) list \ 'a list list" and asc :: "'a \ ('a list \ 'a list) \ 'a list \ 'a list list" and desc :: "'a \ 'a list \ 'a list \ 'a list list" where "runs (a # b # xs) = (if a > b then desc b [a] xs else asc b ((#) a) xs)" | "runs [x] = [[x]]" | "runs [] = []" | "asc a as (b # bs) = (if \ a > b then asc b (as \ (#) a) bs else as [a] # runs (b # bs))" | "asc a as [] = [as [a]]" | "desc a as (b # bs) = (if a > b then desc b (a # as) bs else (a # as) # runs (b # bs))" | "desc a as [] = [a # as]" definition nmsort :: "('a::linorder) list \ 'a list" where "nmsort xs = merge_all (runs xs)" subsection \Functional Correctness\ definition "ascP f = (\xs ys. f (xs @ ys) = f xs @ ys)" lemma ascP_Cons [simp]: "ascP ((#) x)" by (simp add: ascP_def) lemma ascP_comp_Cons [simp]: "ascP f \ ascP (f \ (#) x)" by (auto simp: ascP_def simp flip: append_Cons) lemma ascP_simp [simp]: assumes "ascP f" shows "f [x] = f [] @ [x]" using assms [unfolded ascP_def, THEN spec, THEN spec, of "[]" "[x]"] by simp lemma - shows mset_runs: "\# (image_mset mset (mset (runs xs))) = mset xs" - and mset_asc: "ascP f \ \# (image_mset mset (mset (asc x f ys))) = {#x#} + mset (f []) + mset ys" - and mset_desc: "\# (image_mset mset (mset (desc x xs ys))) = {#x#} + mset xs + mset ys" + shows mset_runs: "\\<^sub># (image_mset mset (mset (runs xs))) = mset xs" + and mset_asc: "ascP f \ \\<^sub># (image_mset mset (mset (asc x f ys))) = {#x#} + mset (f []) + mset ys" + and mset_desc: "\\<^sub># (image_mset mset (mset (desc x xs ys))) = {#x#} + mset xs + mset ys" by (induct xs and x f ys and x xs ys rule: runs_asc_desc.induct) auto lemma mset_nmsort: "mset (nmsort xs) = mset xs" by (auto simp: mset_merge_all nmsort_def mset_runs) lemma shows sorted_runs: "\x\set (runs xs). sorted x" and sorted_asc: "ascP f \ sorted (f []) \ \x\set (f []). x \ a \ \x\set (asc a f ys). sorted x" and sorted_desc: "sorted xs \ \x\set xs. a \ x \ \x\set (desc a xs ys). sorted x" by (induct xs and a f ys and a xs ys rule: runs_asc_desc.induct) (auto simp: sorted_append not_less dest: order_trans, fastforce) lemma sorted_nmsort: "sorted (nmsort xs)" by (auto intro: sorted_merge_all simp: nmsort_def sorted_runs) subsection \Running Time Analysis\ fun C_runs :: "('a::linorder) list \ nat" and C_asc :: "('a::linorder) \ 'a list \ nat" and C_desc :: "('a::linorder) \ 'a list \ nat" where "C_runs (a # b # xs) = 1 + (if a > b then C_desc b xs else C_asc b xs)" | "C_runs xs = 0" | "C_asc a (b # bs) = 1 + (if \ a > b then C_asc b bs else C_runs (b # bs))" | "C_asc a [] = 0" | "C_desc a (b # bs) = 1 + (if a > b then C_desc b bs else C_runs (b # bs))" | "C_desc a [] = 0" fun C_nmsort :: "('a::linorder) list \ nat" where "C_nmsort xs = C_runs xs + C_merge_all (runs xs)" lemma fixes a :: "'a::linorder" and xs ys :: "'a list" shows C_runs: "C_runs xs \ length xs - 1" and C_asc: "C_asc a ys \ length ys" and C_desc: "C_desc a ys \ length ys" by (induct xs and a ys and a ys rule: C_runs_C_asc_C_desc.induct) auto lemma shows length_runs: "length (runs xs) \ length xs" and length_asc: "ascP f \ length (asc a f ys) \ 1 + length ys" and length_desc: "length (desc a xs ys) \ 1 + length ys" by (induct xs and a f ys and a xs ys rule: runs_asc_desc.induct) auto lemma shows length_concat_runs [simp]: "length (concat (runs xs)) = length xs" and length_concat_asc: "ascP f \ length (concat (asc a f ys)) = 1 + length (f []) + length ys" and length_concat_desc: "length (concat (desc a xs ys)) = 1 + length xs + length ys" by (induct xs and a f ys and a xs ys rule: runs_asc_desc.induct) auto lemma log2_mono: "x > 0 \ x \ y \ log 2 x \ log 2 y" by auto lemma shows runs_ne: "xs \ [] \ runs xs \ []" and "ascP f \ asc a f ys \ []" and "desc a xs ys \ []" by (induct xs and a f ys and a xs ys rule: runs_asc_desc.induct) simp_all lemma C_nmsort: assumes [simp]: "length xs = n" shows "C_nmsort xs \ n + n * \log 2 n\" proof - have [simp]: "xs = [] \ length xs = 0" by blast have "int (C_merge_all (runs xs)) \ int n * \log 2 (length (runs xs))\" using C_merge_all' [of "runs xs"] by simp also have "\ \ int n * \log 2 n\" using length_runs [of xs] by (cases n) (auto intro!: runs_ne mult_mono ceiling_mono log2_mono) finally have "int (C_merge_all (runs xs)) \ int n * \log 2 n\" . moreover have "C_runs xs \ n" using C_runs [of xs] by auto ultimately show ?thesis by (auto intro: add_mono) qed end diff --git a/thys/Knuth_Bendix_Order/KBO.thy b/thys/Knuth_Bendix_Order/KBO.thy --- a/thys/Knuth_Bendix_Order/KBO.thy +++ b/thys/Knuth_Bendix_Order/KBO.thy @@ -1,1227 +1,1227 @@ section \KBO\ text \ Below, we formalize a variant of KBO that includes subterm coefficient functions. A more standard definition is obtained by setting all subterm coefficients to 1. For this special case it would be possible to define more efficient code-equations that do not have to evaluate subterm coefficients at all. \ theory KBO imports Lexicographic_Extension Term_Aux Polynomial_Factorization.Missing_List begin subsection \Subterm Coefficient Functions\ text \ Given a function @{term scf}, associating positions with subterm coefficients, and a list @{term xs}, the function @{term scf_list} yields an expanded list where each element of @{term xs} is replicated a number of times according to its subterm coefficient. \ definition scf_list :: "(nat \ nat) \ 'a list \ 'a list" where "scf_list scf xs = concat (map (\(x, i). replicate (scf i) x) (zip xs [0 ..< length xs]))" lemma set_scf_list [simp]: assumes "\i < length xs. scf i > 0" shows "set (scf_list scf xs) = set xs" using assms by (auto simp: scf_list_def set_zip set_conv_nth[of xs]) lemma scf_list_subset: "set (scf_list scf xs) \ set xs" by (auto simp: scf_list_def set_zip) lemma scf_list_empty [simp]: "scf_list scf [] = []" by (auto simp: scf_list_def) lemma scf_list_bef_i_aft [simp]: "scf_list scf (bef @ i # aft) = scf_list scf bef @ replicate (scf (length bef)) i @ scf_list (\ i. scf (Suc (length bef + i))) aft" unfolding scf_list_def proof (induct aft rule: List.rev_induct) case (snoc a aft) define bia where "bia = bef @ i # aft" have bia: "bef @ i # aft @ [a] = bia @ [a]" by (simp add: bia_def) have zip: "zip (bia @ [a]) [0..(x, i). replicate (scf i) x) (zip bia [0..(x, i). replicate (scf i) x) (zip bia [0.. The function @{term scf_term} replicates each argument a number of times according to its subterm coefficient function. \ fun scf_term :: "('f \ nat \ nat \ nat) \ ('f, 'v) term \ ('f, 'v) term" where "scf_term scf (Var x) = (Var x)" | "scf_term scf (Fun f ts) = Fun f (scf_list (scf (f, length ts)) (map (scf_term scf) ts))" lemma vars_term_scf_subset: "vars_term (scf_term scf s) \ vars_term s" proof (induct s) case (Fun f ss) have "vars_term (scf_term scf (Fun f ss)) = (\x\set (scf_list (scf (f, length ss)) ss). vars_term (scf_term scf x))" by auto also have "\ \ (\x\set ss. vars_term (scf_term scf x))" using scf_list_subset [of _ ss] by blast also have "\ \ (\x\set ss. vars_term x)" using Fun by auto finally show ?case by auto qed auto lemma scf_term_subst: "scf_term scf (t \ \) = scf_term scf t \ (\ x. scf_term scf (\ x))" proof (induct t) case (Fun f ts) { fix t assume "t \ set (scf_list (scf (f, length ts)) ts)" with scf_list_subset [of _ ts] have "t \ set ts" by auto then have "scf_term scf (t \ \) = scf_term scf t \ (\x. scf_term scf (\ x))" by (rule Fun) } then show ?case by auto qed auto subsection \Weight Functions\ locale weight_fun = fixes w :: "'f \ nat \ nat" and w0 :: nat and scf :: "'f \ nat \ nat \ nat" begin text \ The \<^emph>\weight\ of a term is computed recursively, where variables have weight @{term w0} and the weight of a compound term is computed by adding the weight of its root symbol @{term "w (f, n)"} to the weighted sum where weights of arguments are multiplied according to their subterm coefficients. \ fun weight :: "('f, 'v) term \ nat" where "weight (Var x) = w0" | "weight (Fun f ts) = (let n = length ts; scff = scf (f, n) in w (f, n) + sum_list (map (\ (ti, i). weight ti * scff i) (zip ts [0 ..< n])))" text \ Alternatively, we can replicate arguments via @{const scf_list}. The advantage is that then both @{const weight} and @{const scf_term} are defined via @{const scf_list}. \ lemma weight_simp [simp]: "weight (Fun f ts) = w (f, length ts) + sum_list (map weight (scf_list (scf (f, length ts)) ts))" proof - define scff where "scff = (scf (f, length ts) :: nat \ nat)" have "(\(ti, i) \ zip ts [0.. scf_term scf" lemma sum_list_scf_list: assumes "\ i. i < length ts \ f i > 0" shows "sum_list (map weight ts) \ sum_list (map weight (scf_list f ts))" using assms unfolding scf_list_def proof (induct ts rule: List.rev_induct) case (snoc t ts) have "sum_list (map weight ts) \ sum_list (map weight (concat (map (\(x, i). replicate (f i) x) (zip ts [0..Definition of KBO\ text \ The precedence is given by three parameters: \<^item> a predicate @{term pr_strict} for strict decrease between two function symbols, \<^item> a predicate @{term pr_weak} for weak decrease between two function symbols, and \<^item> a function indicating whether a symbol is least in the precedence. \ locale kbo = weight_fun w w0 scf for w w0 and scf :: "'f \ nat \ nat \ nat" + fixes least :: "'f \ bool" and pr_strict :: "'f \ nat \ 'f \ nat \ bool" and pr_weak :: "'f \ nat \ 'f \ nat \ bool" begin text \ The result of @{term kbo} is a pair of Booleans encoding strict/weak decrease. Interestingly, the bound on the lengths of the lists in the lexicographic extension is not required for KBO. \ fun kbo :: "('f, 'v) term \ ('f, 'v) term \ bool \ bool" where "kbo s t = (if (vars_term_ms (SCF t) \# vars_term_ms (SCF s) \ weight t \ weight s) then if (weight t < weight s) then (True, True) else (case s of Var y \ (False, (case t of Var x \ x = y | Fun g ts \ ts = [] \ least g)) | Fun f ss \ (case t of Var x \ (True, True) | Fun g ts \ if pr_strict (f, length ss) (g, length ts) then (True, True) else if pr_weak (f, length ss) (g, length ts) then lex_ext_unbounded kbo ss ts else (False, False))) else (False, False))" text \Abbreviations for strict (S) and nonstrict (NS) KBO.\ abbreviation "S \ \ s t. fst (kbo s t)" abbreviation "NS \ \ s t. snd (kbo s t)" text \ For code-generation we do not compute the weights of @{term s} and @{term t} repeatedly. \ lemma kbo_code: "kbo s t = (let wt = weight t; ws = weight s in if (vars_term_ms (SCF t) \# vars_term_ms (SCF s) \ wt \ ws) then if wt < ws then (True, True) else (case s of Var y \ (False, (case t of Var x \ True | Fun g ts \ ts = [] \ least g)) | Fun f ss \ (case t of Var x \ (True, True) | Fun g ts \ let ff = (f, length ss); gg = (g, length ts) in if pr_strict ff gg then (True, True) else if pr_weak ff gg then lex_ext_unbounded kbo ss ts else (False, False))) else (False, False))" unfolding kbo.simps[of s t] Let_def by (auto simp del: kbo.simps split: term.splits) end declare kbo.kbo_code[code] declare weight_fun.weight.simps[code] lemma mset_replicate_mono: assumes "m1 \# m2" - shows "\# (mset (replicate n m1)) \# \# (mset (replicate n m2))" + shows "\\<^sub># (mset (replicate n m1)) \# \\<^sub># (mset (replicate n m2))" proof (induct n) case (Suc n) - have "\# (mset (replicate (Suc n) m1)) = - \# (mset (replicate n m1)) + m1" by simp - also have "\ \# \# (mset (replicate n m1)) + m2" using \m1 \# m2\ by auto - also have "\ \# \# (mset (replicate n m2)) + m2" using Suc by auto + have "\\<^sub># (mset (replicate (Suc n) m1)) = + \\<^sub># (mset (replicate n m1)) + m1" by simp + also have "\ \# \\<^sub># (mset (replicate n m1)) + m2" using \m1 \# m2\ by auto + also have "\ \# \\<^sub># (mset (replicate n m2)) + m2" using Suc by auto finally show ?case by (simp add: union_commute) qed simp text \ While the locale @{locale kbo} only fixes its parameters, we now demand that these parameters are sensible, e.g., encoding a well-founded precedence, etc. \ locale admissible_kbo = kbo w w0 scf least pr_strict pr_weak for w w0 pr_strict pr_weak and least :: "'f \ bool" and scf + assumes w0: "w (f, 0) \ w0" "w0 > 0" and adm: "w (f, 1) = 0 \ pr_weak (f, 1) (g, n)" and least: "least f = (w (f, 0) = w0 \ (\ g. w (g, 0) = w0 \ pr_weak (g, 0) (f, 0)))" and scf: "i < n \ scf (f, n) i > 0" and pr_weak_refl [simp]: "pr_weak fn fn" and pr_weak_trans: "pr_weak fn gm \ pr_weak gm hk \ pr_weak fn hk" and pr_strict: "pr_strict fn gm \ pr_weak fn gm \ \ pr_weak gm fn" and pr_SN: "SN {(fn, gm). pr_strict fn gm}" begin lemma weight_w0: "weight t \ w0" proof (induct t) case (Fun f ts) show ?case proof (cases ts) case Nil with w0(1) have "w0 \ w (f, length ts)" by auto then show ?thesis by auto next case (Cons s ss) then obtain i where i: "i < length ts" by auto from scf[OF this] have scf: "0 < scf (f, length ts) i" by auto then obtain n where scf: "scf (f, length ts) i = Suc n" by (auto elim: lessE) from id_take_nth_drop[OF i] i obtain bef aft where ts: "ts = bef @ ts ! i # aft" and ii: "length bef = i" by auto define tsi where "tsi = ts ! i" note ts = ts[folded tsi_def] from i have tsi: "tsi \ set ts" unfolding tsi_def by auto from Fun[OF this] have w0: "w0 \ weight tsi" . show ?thesis using scf ii w0 unfolding ts by simp qed qed simp lemma weight_gt_0: "weight t > 0" using weight_w0 [of t] and w0 by arith lemma weight_0 [iff]: "weight t = 0 \ False" using weight_gt_0 [of t] by auto lemma not_S_Var: "\ S (Var x) t" using weight_w0[of t] by (cases t, auto) lemma S_imp_NS: "S s t \ NS s t" proof (induct s t rule: kbo.induct) case (1 s t) from 1(2) have S: "S s t" . from S have w: "vars_term_ms (SCF t) \# vars_term_ms (SCF s) \ weight t \ weight s" by (auto split: if_splits) note S = S w note IH = 1(1)[OF w] show ?case proof (cases "weight t < weight s") case True with S show ?thesis by simp next case False note IH = IH[OF False] note S = S False from not_S_Var[of _ t] S obtain f ss where s: "s = Fun f ss" by (cases s, auto) note IH = IH[OF s] show ?thesis proof (cases t) case (Var x) from S show ?thesis by (auto, insert Var s, auto) next case (Fun g ts) note IH = IH[OF Fun] let ?f = "(f, length ss)" let ?g = "(g, length ts)" let ?lex = "lex_ext_unbounded kbo ss ts" from S[simplified, unfolded s Fun] have disj: "pr_strict ?f ?g \ pr_weak ?f ?g \ fst ?lex" by (auto split: if_splits) show ?thesis proof (cases "pr_strict ?f ?g") case True then show ?thesis using S s Fun by auto next case False with disj have fg: "pr_weak ?f ?g" and lex: "fst ?lex" by auto note IH = IH[OF False fg] from lex have "fst (lex_ext kbo (length ss + length ts) ss ts)" unfolding lex_ext_def Let_def by auto from lex_ext_stri_imp_nstri[OF this] have lex: "snd ?lex" unfolding lex_ext_def Let_def by auto with False fg S s Fun show ?thesis by auto qed qed qed qed subsection \Reflexivity and Irreflexivity\ lemma NS_refl: "NS s s" proof (induct s) case (Fun f ss) have "snd (lex_ext kbo (length ss) ss ss)" by (rule all_nstri_imp_lex_nstri, insert Fun[unfolded set_conv_nth], auto) then have "snd (lex_ext_unbounded kbo ss ss)" unfolding lex_ext_def Let_def by simp then show ?case by auto qed simp lemma pr_strict_irrefl: "\ pr_strict fn fn" unfolding pr_strict by auto lemma S_irrefl: "\ S t t" proof (induct t) case (Var x) then show ?case by (rule not_S_Var) next case (Fun f ts) from pr_strict_irrefl have "\ pr_strict (f, length ts) (f, length ts)" . moreover { assume "fst (lex_ext_unbounded kbo ts ts)" then obtain i where "i < length ts" and "S (ts ! i) (ts ! i)" unfolding lex_ext_unbounded_iff by auto with Fun have False by auto } ultimately show ?case by auto qed subsection \Monotonicity (a.k.a. Closure under Contexts)\ lemma S_mono_one: assumes S: "S s t" shows "S (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))" proof - let ?ss = "ss1 @ s # ss2" let ?ts = "ss1 @ t # ss2" let ?s = "Fun f ?ss" let ?t = "Fun f ?ts" from S have w: "weight t \ weight s" and v: "vars_term_ms (SCF t) \# vars_term_ms (SCF s)" by (auto split: if_splits) have v': "vars_term_ms (SCF ?t) \# vars_term_ms (SCF ?s)" using mset_replicate_mono[OF v] by simp have w': "weight ?t \ weight ?s" using sum_list_replicate_mono[OF w] by simp have lex: "fst (lex_ext_unbounded kbo ?ss ?ts)" unfolding lex_ext_unbounded_iff fst_conv by (rule disjI1, rule exI[of _ "length ss1"], insert S NS_refl, auto simp del: kbo.simps simp: nth_append) show ?thesis using v' w' lex by simp qed lemma S_ctxt: "S s t \ S (C\s\) (C\t\)" by (induct C, auto simp del: kbo.simps intro: S_mono_one) lemma NS_mono_one: assumes NS: "NS s t" shows "NS (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))" proof - let ?ss = "ss1 @ s # ss2" let ?ts = "ss1 @ t # ss2" let ?s = "Fun f ?ss" let ?t = "Fun f ?ts" from NS have w: "weight t \ weight s" and v: "vars_term_ms (SCF t) \# vars_term_ms (SCF s)" by (auto split: if_splits) have v': "vars_term_ms (SCF ?t) \# vars_term_ms (SCF ?s)" using mset_replicate_mono[OF v] by simp have w': "weight ?t \ weight ?s" using sum_list_replicate_mono[OF w] by simp have lex: "snd (lex_ext_unbounded kbo ?ss ?ts)" unfolding lex_ext_unbounded_iff snd_conv proof (intro disjI2 conjI allI impI) fix i assume "i < length (ss1 @ t # ss2)" then show "NS (?ss ! i) (?ts ! i)" using NS NS_refl by (cases "i = length ss1", auto simp del: kbo.simps simp: nth_append) qed simp show ?thesis using v' w' lex by simp qed lemma NS_ctxt: "NS s t \ NS (C\s\) (C\t\)" by (induct C, auto simp del: kbo.simps intro: NS_mono_one) subsection \The Subterm Property\ lemma NS_Var_imp_eq_least: "NS (Var x) t \ t = Var x \ (\ f. t = Fun f [] \ least f)" by (cases t, insert weight_w0[of t], auto split: if_splits) lemma kbo_supt_one: "NS s (t :: ('f, 'v) term) \ S (Fun f (bef @ s # aft)) t" proof (induct t arbitrary: f s bef aft) case (Var x) note NS = this let ?ss = "bef @ s # aft" let ?t = "Var x" have "length bef < length ?ss" by auto from scf[OF this, of f] obtain n where scf:"scf (f, length ?ss) (length bef) = Suc n" by (auto elim: lessE) obtain X where "vars_term_ms (SCF (Fun f ?ss)) = vars_term_ms (SCF s) + X" by (simp add: o_def scf[simplified]) then have vs: "vars_term_ms (SCF s) \# vars_term_ms (SCF (Fun f ?ss))" by simp from NS have vt: "vars_term_ms (SCF ?t) \# vars_term_ms (SCF s)" by (auto split: if_splits) from vt vs have v: "vars_term_ms (SCF ?t) \# vars_term_ms (SCF (Fun f ?ss))" by (rule subset_mset.order_trans) from weight_w0[of "Fun f ?ss"] v show ?case by simp next case (Fun g ts f s bef aft) let ?t = "Fun g ts" let ?ss = "bef @ s # aft" note NS = Fun(2) note IH = Fun(1) have "length bef < length ?ss" by auto from scf[OF this, of f] obtain n where scff:"scf (f, length ?ss) (length bef) = Suc n" by (auto elim: lessE) note scff = scff[simplified] obtain X where "vars_term_ms (SCF (Fun f ?ss)) = vars_term_ms (SCF s) + X" by (simp add: o_def scff) then have vs: "vars_term_ms (SCF s) \# vars_term_ms (SCF (Fun f ?ss))" by simp have ws: "weight s \ sum_list (map weight (scf_list (scf (f, length ?ss)) ?ss))" by (simp add: scff) from NS have wt: "weight ?t \ weight s" and vt: "vars_term_ms (SCF ?t) \# vars_term_ms (SCF s)" by (auto split: if_splits) from ws wt have w: "weight ?t \ sum_list (map weight (scf_list (scf (f, length ?ss)) ?ss))" by simp from vt vs have v: "vars_term_ms (SCF ?t) \# vars_term_ms (SCF (Fun f ?ss))" by auto then have v': "(vars_term_ms (SCF ?t) \# vars_term_ms (SCF (Fun f ?ss))) = True" by simp show ?case proof (cases "weight ?t = weight (Fun f ?ss)") case False with w v show ?thesis by auto next case True from wt[unfolded True] weight_gt_0[of s] have wf: "w (f, length ?ss) = 0" and lsum: "sum_list (map weight (scf_list (scf (f, length ?ss)) bef)) = 0" "sum_list (map weight (scf_list (\ i. (scf (f, length ?ss) (Suc (length bef) + i))) aft)) = 0" and n: "n = 0" by (auto simp: scff) have "sum_list (map weight bef) \ sum_list (map weight (scf_list (scf (f, length ?ss)) bef))" by (rule sum_list_scf_list, rule scf, auto) with lsum(1) have "sum_list (map weight bef) = 0" by arith then have bef: "bef = []" using weight_gt_0[of "hd bef"] by (cases bef, auto) have "sum_list (map weight aft) \ sum_list (map weight (scf_list (\ i. (scf (f, length ?ss) (Suc (length bef) + i))) aft))" by (rule sum_list_scf_list, rule scf, auto) with lsum(2) have "sum_list (map weight aft) = 0" by arith then have aft: "aft = []" using weight_gt_0[of "hd aft"] by (cases aft, auto) note scff = scff[unfolded bef aft n, simplified] from bef aft have ba: "bef @ s # aft = [s]" by simp with wf have wf: "w (f, 1) = 0" by auto from wf have wst: "weight s = weight ?t" using scff unfolding True[unfolded ba] by (simp add: scf_list_def) let ?g = "(g, length ts)" let ?f = "(f, 1)" show ?thesis proof (cases "pr_strict ?f ?g") case True with w v show ?thesis unfolding ba by simp next case False note admf = adm[OF wf] from admf have pg: "pr_weak ?f ?g" . from pg False[unfolded pr_strict] have "pr_weak ?g ?f" by auto from pr_weak_trans[OF this admf] have g: "\ h k. pr_weak ?g (h, k)" . show ?thesis proof (cases ts) case Nil have "fst (lex_ext_unbounded kbo [s] ts)" unfolding Nil lex_ext_unbounded_iff by auto with pg w v show ?thesis unfolding ba by simp next case (Cons t tts) { fix x assume s: "s = Var x" from NS_Var_imp_eq_least[OF NS[unfolded s Cons]] have False by auto } then obtain h ss where s: "s = Fun h ss" by (cases s, auto) from NS wst g[of h "length ss"] pr_strict[of "(h, length ss)" "(g, length ts)"] have lex: "snd (lex_ext_unbounded kbo ss ts)" unfolding s by (auto split: if_splits) from lex obtain s0 sss where ss: "ss = s0 # sss" unfolding Cons lex_ext_unbounded_iff snd_conv by (cases ss, auto) from lex[unfolded ss Cons] have "S s0 t \ NS s0 t" by (cases "kbo s0 t", simp add: lex_ext_unbounded.simps del: kbo.simps split: if_splits) with S_imp_NS[of s0 t] have "NS s0 t" by blast from IH[OF _ this, of h Nil sss] have S: "S s t" unfolding Cons s ss by simp have "fst (lex_ext_unbounded kbo [s] ts)" unfolding Cons unfolding lex_ext_unbounded_iff fst_conv by (rule disjI1[OF exI[of _ 0]], insert S, auto simp del: kbo.simps) then have lex: "fst (lex_ext_unbounded kbo [s] ts) = True" by simp note all = lex wst[symmetric] S pg scff v' note all = all[unfolded ba, unfolded s ss Cons] have w: "weight (Fun f [t]) = weight (t :: ('f, 'v) term)" for t using wf scff by (simp add: scf_list_def) show ?thesis unfolding ba unfolding s ss Cons unfolding kbo.simps[of "Fun f [Fun h (s0 # sss)]"] unfolding all w using all by simp qed qed qed qed lemma S_supt: assumes supt: "s \ t" shows "S s t" proof - from supt obtain C where s: "s = C\t\" and C: "C \ \" by auto show ?thesis unfolding s using C proof (induct C arbitrary: t) case (More f bef C aft t) show ?case proof (cases "C = \") case True from kbo_supt_one[OF NS_refl, of f bef t aft] show ?thesis unfolding True by simp next case False from kbo_supt_one[OF S_imp_NS[OF More(1)[OF False]], of f bef t aft] show ?thesis by simp qed qed simp qed lemma NS_supteq: assumes "s \ t" shows "NS s t" using S_imp_NS[OF S_supt[of s t]] NS_refl[of s] using assms[unfolded subterm.le_less] by blast subsection \Least Elements\ lemma NS_all_least: assumes l: "least f" shows "NS t (Fun f [])" proof (induct t) case (Var x) show ?case using l[unfolded least] l by auto next case (Fun g ts) show ?case proof (cases ts) case (Cons s ss) with Fun[of s] have "NS s (Fun f [])" by auto from S_imp_NS[OF kbo_supt_one[OF this, of g Nil ss]] show ?thesis unfolding Cons by simp next case Nil from weight_w0[of "Fun g []"] have w: "weight (Fun g []) \ weight (Fun f [])" using l[unfolded least] by auto from lex_ext_least_1 have "snd (lex_ext kbo 0 [] [])" . then have lex: "snd (lex_ext_unbounded kbo [] [])" unfolding lex_ext_def Let_def by simp then show ?thesis using w l[unfolded least] unfolding Fun Nil by (auto simp: empty_le) qed qed lemma not_S_least: assumes l: "least f" shows "\ S (Fun f []) t" proof (cases t) case (Fun g ts) show ?thesis unfolding Fun proof assume S: "S (Fun f []) (Fun g ts)" from S[unfolded Fun, simplified] have w: "w (g, length ts) + sum_list (map weight (scf_list (scf (g, length ts)) ts)) \ weight (Fun f [])" by (auto split: if_splits) show False proof (cases ts) case Nil with w have "w (g, 0) \ weight (Fun f [])" by simp also have "weight (Fun f []) \ w0" using l[unfolded least] by simp finally have g: "w (g, 0) = w0" using w0(1)[of g] by auto with w Nil l[unfolded least] have gf: "w (g, 0) = w (f, 0)" by simp with S have p: "pr_weak (f, 0) (g, 0)" unfolding Nil by (simp split: if_splits add: pr_strict) with l[unfolded least, THEN conjunct2, rule_format, OF g] have p2: "pr_weak (g, 0) (f, 0)" by auto from p p2 gf S have "fst (lex_ext_unbounded kbo [] ts)" unfolding Nil by (auto simp: pr_strict) then show False unfolding lex_ext_unbounded_iff by auto next case (Cons s ss) then have ts: "ts = [] @ s # ss" by auto from scf[of 0 "length ts" g] obtain n where scff: "scf (g, length ts) 0 = Suc n" unfolding Cons by (auto elim: lessE) let ?e = "sum_list (map weight ( scf_list (\i. scf (g, Suc (length ss)) (Suc i)) ss ))" have "w0 + sum_list (map weight (replicate n s)) \ weight s + sum_list (map weight (replicate n s))" using weight_w0[of s] by auto also have "\ = sum_list (map weight (replicate (scf (g, length ts) 0) s))" unfolding scff by simp also have "w (g, length ts) + \ + ?e \ w0" using w l[unfolded least] unfolding ts scf_list_bef_i_aft by auto finally have "w0 + sum_list (map weight (replicate n s)) + w (g, length ts) + ?e \ w0" by arith then have wg: "w (g, length ts) = 0" and null: "?e = 0" "sum_list (map weight (replicate n s)) = 0" by auto from null(2) weight_gt_0[of s] have n: "n = 0" by (cases n, auto) have "sum_list (map weight ss) \ ?e" by (rule sum_list_scf_list, rule scf, auto) from this[unfolded null] weight_gt_0[of "hd ss"] have ss: "ss = []" by (cases ss, auto) with Cons have ts: "ts = [s]" by simp note scff = scff[unfolded ts n, simplified] from wg ts have wg: "w (g, 1) = 0" by auto from adm[OF wg, rule_format, of f] have "pr_weak (g, 1) (f, 0)" by auto with S[unfolded Fun ts] l[unfolded least] weight_w0[of s] scff have "fst (lex_ext_unbounded kbo [] [s])" by (auto split: if_splits simp: scf_list_def pr_strict) then show ?thesis unfolding lex_ext_unbounded_iff by auto qed qed qed simp lemma NS_least_least: assumes l: "least f" and NS: "NS (Fun f []) t" shows "\ g. t = Fun g [] \ least g" proof (cases t) case (Var x) show ?thesis using NS unfolding Var by simp next case (Fun g ts) from NS[unfolded Fun, simplified] have w: "w (g, length ts) + sum_list (map weight (scf_list (scf (g, length ts)) ts)) \ weight (Fun f [])" by (auto split: if_splits) show ?thesis proof (cases ts) case Nil with w have "w (g, 0) \ weight (Fun f [])" by simp also have "weight (Fun f []) \ w0" using l[unfolded least] by simp finally have g: "w (g, 0) = w0" using w0(1)[of g] by auto with w Nil l[unfolded least] have gf: "w (g, 0) = w (f, 0)" by simp with NS[unfolded Fun] have p: "pr_weak (f, 0) (g, 0)" unfolding Nil by (simp split: if_splits add: pr_strict) have least: "least g" unfolding least proof (rule conjI[OF g], intro allI) fix h from l[unfolded least] have "w (h, 0) = w0 \ pr_weak (h, 0) (f, 0)" by blast with pr_weak_trans p show "w (h, 0) = w0 \ pr_weak (h, 0) (g, 0)" by blast qed show ?thesis by (rule exI[of _ g], unfold Fun Nil, insert least, auto) next case (Cons s ss) then have ts: "ts = [] @ s # ss" by auto from scf[of 0 "length ts" g] obtain n where scff: "scf (g, length ts) 0 = Suc n" unfolding Cons by (auto elim: lessE) let ?e = "sum_list (map weight ( scf_list (\i. scf (g, Suc (length ss)) (Suc i)) ss ))" have "w0 + sum_list (map weight (replicate n s)) \ weight s + sum_list (map weight (replicate n s))" using weight_w0[of s] by auto also have "\ = sum_list (map weight (replicate (scf (g, length ts) 0) s))" unfolding scff by simp also have "w (g, length ts) + \ + ?e \ w0" using w l[unfolded least] unfolding ts scf_list_bef_i_aft by auto finally have "w0 + sum_list (map weight (replicate n s)) + w (g, length ts) + ?e \ w0" by arith then have wg: "w (g, length ts) = 0" and null: "?e = 0" "sum_list (map weight (replicate n s)) = 0" by auto from null(2) weight_gt_0[of s] have n: "n = 0" by (cases n, auto) have "sum_list (map weight ss) \ ?e" by (rule sum_list_scf_list, rule scf, auto) from this[unfolded null] weight_gt_0[of "hd ss"] have ss: "ss = []" by (cases ss, auto) with Cons have ts: "ts = [s]" by simp note scff = scff[unfolded ts n, simplified] from wg ts have wg: "w (g, 1) = 0" by auto from adm[OF wg, rule_format, of f] have "pr_weak (g, 1) (f, 0)" by auto with NS[unfolded Fun ts] l[unfolded least] weight_w0[of s] scff have "snd (lex_ext_unbounded kbo [] [s])" by (auto split: if_splits simp: scf_list_def pr_strict) then show ?thesis unfolding lex_ext_unbounded_iff snd_conv by auto qed qed subsection \Stability (a.k.a. Closure under Substitutions\ lemma weight_subst: "weight (t \ \) = weight t + sum_mset (image_mset (\ x. weight (\ x) - w0) (vars_term_ms (SCF t)))" proof (induct t) case (Var x) show ?case using weight_w0[of "\ x"] by auto next case (Fun f ts) let ?ts = "scf_list (scf (f, length ts)) ts" define sts where "sts = ?ts" have id: "map (\ t. weight (t \ \)) ?ts = map (\ t. weight t + sum_mset (image_mset (\ x. weight (\ x) - w0) (vars_term_ms (scf_term scf t)))) ?ts" by (rule map_cong[OF refl Fun], insert scf_list_subset[of _ ts], auto) show ?case by (simp add: o_def id, unfold sts_def[symmetric], induct sts, auto) qed lemma weight_stable_le: assumes ws: "weight s \ weight t" and vs: "vars_term_ms (SCF s) \# vars_term_ms (SCF t)" shows "weight (s \ \) \ weight (t \ \)" proof - from vs[unfolded mset_subset_eq_exists_conv] obtain u where vt: "vars_term_ms (SCF t) = vars_term_ms (SCF s) + u" .. show ?thesis unfolding weight_subst vt using ws by auto qed lemma weight_stable_lt: assumes ws: "weight s < weight t" and vs: "vars_term_ms (SCF s) \# vars_term_ms (SCF t)" shows "weight (s \ \) < weight (t \ \)" proof - from vs[unfolded mset_subset_eq_exists_conv] obtain u where vt: "vars_term_ms (SCF t) = vars_term_ms (SCF s) + u" .. show ?thesis unfolding weight_subst vt using ws by auto qed text \KBO is stable, i.e., closed under substitutions.\ lemma kbo_stable: fixes \ :: "('f, 'v) subst" assumes "NS s t" shows "(S s t \ S (s \ \) (t \ \)) \ NS (s \ \) (t \ \)" (is "?P s t") using assms proof (induct s arbitrary: t) case (Var y t) then have not: "\ S (Var y) t" using not_S_Var[of y t] by auto from NS_Var_imp_eq_least[OF Var] have "t = Var y \ (\ f. t = Fun f [] \ least f)" by simp then obtain f where "t = Var y \ t = Fun f [] \ least f" by auto then have "NS (Var y \ \) (t \ \)" proof assume "t = Var y" then show ?thesis using NS_refl[of "t \ \"] by auto next assume "t = Fun f [] \ least f" with NS_all_least[of f "Var y \ \"] show ?thesis by auto qed with not show ?case by blast next case (Fun f ss t) note NS = Fun(2) note IH = Fun(1) let ?s = "Fun f ss" define s where "s = ?s" let ?ss = "map (\ s. s \ \) ss" from NS have v: "vars_term_ms (SCF t) \# vars_term_ms (SCF ?s)" and w: "weight t \ weight ?s" by (auto split: if_splits) from weight_stable_le[OF w v] have w\: "weight (t \ \) \ weight (?s \ \)" by auto from vars_term_ms_subst_mono[OF v, of "\ x. SCF (\ x)"] have v\: "vars_term_ms (SCF (t \ \)) \# vars_term_ms (SCF (?s \ \))" unfolding scf_term_subst . show ?case proof (cases "weight (t \ \) < weight (?s \ \)") case True with v\ show ?thesis by auto next case False with weight_stable_lt[OF _ v, of \] w have w: "weight t = weight ?s" by arith show ?thesis proof (cases t) case (Var y) from set_mset_mono[OF v, folded s_def] have "y \ vars_term (SCF s)" unfolding Var by (auto simp: o_def) also have "\ \ vars_term s" by (rule vars_term_scf_subset) finally have "y \ vars_term s" by auto from supteq_Var[OF this] have "?s \ Var y" unfolding s_def Fun by auto from S_supt[OF supt_subst[OF this]] have S: "S (?s \ \) (t \ \)" unfolding Var . from S_imp_NS[OF S] S show ?thesis by auto next case (Fun g ts) note t = this let ?f = "(f, length ss)" let ?g = "(g, length ts)" let ?ts = "map (\ s. s \ \) ts" show ?thesis proof (cases "pr_strict ?f ?g") case True then have S: "S (?s \ \) (t \ \)" using w\ v\ unfolding t by simp from S S_imp_NS[OF S] show ?thesis by simp next case False note prec = this show ?thesis proof (cases "pr_weak ?f ?g") case False with v w prec have "\ NS ?s t" unfolding t by (auto simp del: vars_term_ms.simps) with NS show ?thesis by blast next case True from v w have "vars_term_ms (SCF t) \# vars_term_ms (SCF ?s) \ weight t \ weight ?s" "\ weight t < weight ?s" by auto { fix i assume i: "i < length ss" "i < length ts" and S: "S (ss ! i) (ts ! i)" have "S (map (\s. s \ \) ss ! i) (map (\s. s \ \) ts ! i)" using IH[OF _ S_imp_NS[OF S]] S i unfolding set_conv_nth by (force simp del: kbo.simps) } note IH_S = this { fix i assume i: "i < length ss" "i < length ts" and NS: "NS (ss ! i) (ts ! i)" have "NS (map (\s. s \ \) ss ! i) (map (\s. s \ \) ts ! i)" using IH[OF _ NS] i unfolding set_conv_nth by (force simp del: kbo.simps) } note IH_NS = this { assume "S ?s t" with prec v w True have lex: "fst (lex_ext_unbounded kbo ss ts)" unfolding s_def t by simp have "fst (lex_ext_unbounded kbo ?ss ?ts)" by (rule lex_ext_unbounded_map_S[OF _ _ lex], insert IH_NS IH_S, blast+) with v\ w\ prec True have "S (?s \ \) (t \ \)" unfolding t by auto } moreover { from NS prec v w True have lex: "snd (lex_ext_unbounded kbo ss ts)" unfolding t by simp have "snd (lex_ext_unbounded kbo ?ss ?ts)" by (rule lex_ext_unbounded_map_NS[OF _ _ lex], insert IH_S IH_NS, blast) with v\ w\ prec True have "NS (?s \ \) (t \ \)" unfolding t by auto } ultimately show ?thesis by auto qed qed qed qed qed lemma S_subst: "S s t \ S (s \ (\ :: ('f, 'v) subst)) (t \ \)" using kbo_stable[OF S_imp_NS, of s t \] by auto lemma NS_subst: "NS s t \ NS (s \ (\ :: ('f, 'v) subst)) (t \ \)" using kbo_stable[of s t \] by auto subsection \Transitivity and Compatibility\ lemma kbo_trans: "(S s t \ NS t u \ S s u) \ (NS s t \ S t u \ S s u) \ (NS s t \ NS t u \ NS s u)" (is "?P s t u") proof (induct s arbitrary: t u) case (Var x t u) from not_S_Var[of x t] have nS: "\ S (Var x) t" . show ?case proof (cases "NS (Var x) t") case False with nS show ?thesis by blast next case True from NS_Var_imp_eq_least[OF this] obtain f where "t = Var x \ t = Fun f [] \ least f" by blast then show ?thesis proof assume "t = Var x" then show ?thesis using nS by blast next assume "t = Fun f [] \ least f" then have t: "t = Fun f []" and least: "least f" by auto from not_S_least[OF least] have nS': "\ S t u" unfolding t . show ?thesis proof (cases "NS t u") case True with NS_least_least[OF least, of u] t obtain h where u: "u = Fun h []" and least: "least h" by auto from NS_all_least[OF least] have NS: "NS (Var x) u" unfolding u . with nS nS' show ?thesis by blast next case False with S_imp_NS[of t u] show ?thesis by blast qed qed qed next case (Fun f ss t u) note IH = this let ?s = "Fun f ss" show ?case proof (cases "NS ?s t") case False with S_imp_NS[of ?s t] show ?thesis by blast next case True note st = this then have vst: "vars_term_ms (SCF t) \# vars_term_ms (SCF ?s)" and wst: "weight t \ weight ?s" by (auto split: if_splits) show ?thesis proof (cases "NS t u") case False with S_imp_NS[of t u] show ?thesis by blast next case True note tu = this then have vtu: "vars_term_ms (SCF u) \# vars_term_ms (SCF t)" and wtu: "weight u \ weight t" by (auto split: if_splits) from vst vtu have v: "vars_term_ms (SCF u) \# vars_term_ms (SCF ?s)" by simp from wst wtu have w: "weight u \ weight ?s" by simp show ?thesis proof (cases "weight u < weight ?s") case True with v show ?thesis by auto next case False with wst wtu have wst: "weight t = weight ?s" and wtu: "weight u = weight t" and w: "weight u = weight ?s" by arith+ show ?thesis proof (cases u) case (Var z) with v w show ?thesis by auto next case (Fun h us) note u = this show ?thesis proof (cases t) case (Fun g ts) note t = this let ?f = "(f, length ss)" let ?g = "(g, length ts)" let ?h = "(h, length us)" from st t wst have fg: "pr_weak ?f ?g" by (simp split: if_splits add: pr_strict) from tu t u wtu have gh: "pr_weak ?g ?h" by (simp split: if_splits add: pr_strict) from pr_weak_trans[OF fg gh] have fh: "pr_weak ?f ?h" . show ?thesis proof (cases "pr_strict ?f ?h") case True with w v u show ?thesis by auto next case False let ?lex = "lex_ext_unbounded kbo" from False fh have hf: "pr_weak ?h ?f" unfolding pr_strict by auto from pr_weak_trans[OF hf fg] have hg: "pr_weak ?h ?g" . from hg have gh2: "\ pr_strict ?g ?h" unfolding pr_strict by auto from pr_weak_trans[OF gh hf] have gf: "pr_weak ?g ?f" . from gf have fg2: "\ pr_strict ?f ?g" unfolding pr_strict by auto from st t wst fg2 have st: "snd (?lex ss ts)" by (auto split: if_splits) from tu t u wtu gh2 have tu: "snd (?lex ts us)" by (auto split: if_splits) { fix s t u assume "s \ set ss" from IH[OF this, of t u] have "(NS s t \ S t u \ S s u) \ (S s t \ NS t u \ S s u) \ (NS s t \ NS t u \ NS s u) \ (S s t \ S t u \ S s u)" using S_imp_NS[of s t] by blast } note IH = this let ?b = "length ss + length ts + length us" note lex = lex_ext_compat[of ss ts us kbo ?b, OF IH] let ?lexb = "lex_ext kbo ?b" note conv = lex_ext_def Let_def from st have st: "snd (?lexb ss ts)" unfolding conv by simp from tu have tu: "snd (?lexb ts us)" unfolding conv by simp from lex st tu have su: "snd (?lexb ss us)" by blast then have su: "snd (?lex ss us)" unfolding conv by simp from w v u su fh have NS: "NS ?s u" by simp { assume st: "S ?s t" with t wst fg fg2 have st: "fst (?lex ss ts)" by (auto split: if_splits) then have st: "fst (?lexb ss ts)" unfolding conv by simp from lex st tu have su: "fst (?lexb ss us)" by blast then have su: "fst (?lex ss us)" unfolding conv by simp from w v u su fh have S: "S ?s u" by simp } note S_left = this { assume tu: "S t u" with t u wtu gh2 have tu: "fst (?lex ts us)" by (auto split: if_splits) then have tu: "fst (?lexb ts us)" unfolding conv by simp from lex st tu have su: "fst (?lexb ss us)" by blast then have su: "fst (?lex ss us)" unfolding conv by simp from w v u su fh have S: "S ?s u" by simp } note S_right = this from NS S_left S_right show ?thesis by blast qed next case (Var x) note t = this from tu weight_w0[of u] have least: "least h" and u: "u = Fun h []" unfolding t u by (auto split: if_splits) from NS_all_least[OF least] have NS: "NS ?s u" unfolding u . from not_S_Var have nS': "\ S t u" unfolding t . show ?thesis proof (cases "S ?s t") case False with nS' NS show ?thesis by blast next case True then have "vars_term_ms (SCF t) \# vars_term_ms (SCF ?s)" by (auto split: if_splits) from set_mset_mono[OF this, unfolded set_mset_vars_term_ms t] have "x \ vars_term (SCF ?s)" by simp also have "\ \ vars_term ?s" by (rule vars_term_scf_subset) finally obtain s sss where ss: "ss = s # sss" by (cases ss, auto) from kbo_supt_one[OF NS_all_least[OF least, of s], of f Nil sss] have "S ?s u" unfolding ss u by simp with NS show ?thesis by blast qed qed qed qed qed qed qed lemma S_trans: "S s t \ S t u \ S s u" using S_imp_NS[of s t] kbo_trans[of s t u] by blast lemma NS_trans: "NS s t \ NS t u \ NS s u" using kbo_trans[of s t u] by blast lemma NS_S_compat: "NS s t \ S t u \ S s u" using kbo_trans[of s t u] by blast lemma S_NS_compat: "S s t \ NS t u \ S s u" using kbo_trans[of s t u] by blast subsection \Strong Normalization (a.k.a. Well-Foundedness)\ lemma kbo_strongly_normalizing: fixes s :: "('f, 'v) term" shows "SN_on {(s, t). S s t} {s}" proof - let ?SN = "\ t :: ('f, 'v) term. SN_on {(s, t). S s t} {t}" let ?m1 = "\ (f, ss). weight (Fun f ss)" let ?m2 = "\ (f, ss). (f, length ss)" let ?rel' = "lex_two {(fss, gts). ?m1 fss > ?m1 gts} {(fss, gts). ?m1 fss \ ?m1 gts} {(fss, gts). pr_strict (?m2 fss) (?m2 gts)}" let ?rel = "inv_image ?rel' (\ x. (x, x))" have SN_rel: "SN ?rel" by (rule SN_inv_image, rule lex_two, insert SN_inv_image[OF pr_SN, of ?m2] SN_inv_image[OF SN_nat_gt, of ?m1], auto simp: inv_image_def) note conv = SN_on_all_reducts_SN_on_conv show "?SN s" proof (induct s) case (Var x) show ?case unfolding conv[of _ "Var x"] using not_S_Var[of x] by auto next case (Fun f ss) then have subset: "set ss \ {s. ?SN s}" by blast let ?P = "\ (f, ss). set ss \ {s. ?SN s} \ ?SN (Fun f ss)" { fix fss have "?P fss" proof (induct fss rule: SN_induct[OF SN_rel]) case (1 fss) obtain f ss where fss: "fss = (f, ss)" by force { fix g ts assume "?m1 (f, ss) > ?m1 (g, ts) \ ?m1 (f, ss) \ ?m1 (g, ts) \ pr_strict (?m2 (f, ss)) (?m2 (g, ts))" and "set ts \ {s. ?SN s}" then have "?SN (Fun g ts)" using 1[rule_format, of "(g, ts)", unfolded fss split] by auto } note IH = this[unfolded split] show ?case unfolding fss split proof assume SN_s: "set ss \ {s. ?SN s}" let ?f = "(f, length ss)" let ?s = "Fun f ss" let ?SNt = "\ g ts. ?SN (Fun g ts)" let ?sym = "\ g ts. (g, length ts)" let ?lex = "lex_ext kbo (weight ?s)" let ?lexu = "lex_ext_unbounded kbo" let ?lex_SN = "{(ys, xs). (\ y \ set ys. ?SN y) \ fst (?lex ys xs)}" from lex_ext_SN[of kbo "weight ?s", OF NS_S_compat] have SN: "SN ?lex_SN" . { fix g and ts :: "('f, 'v) term list" assume "pr_weak ?f (?sym g ts) \ weight (Fun g ts) \ weight ?s \ set ts \ {s. ?SN s}" then have "?SNt g ts" proof (induct ts arbitrary: g rule: SN_induct[OF SN]) case (1 ts g) note inner_IH = 1(1) let ?g = "(g, length ts)" let ?t = "Fun g ts" from 1(2) have fg: "pr_weak ?f ?g" and w: "weight ?t \ weight ?s" and SN: "set ts \ {s. ?SN s}" by auto show "?SNt g ts" unfolding conv[of _ ?t] proof (intro allI impI) fix u assume "(?t, u) \ {(s, t). S s t}" then have tu: "S ?t u" by auto then show "?SN u" proof (induct u) case (Var x) then show ?case using not_S_Var[of x] unfolding conv[of _ "Var x"] by auto next case (Fun h us) let ?h = "(h, length us)" let ?u = "Fun h us" note tu = Fun(2) { fix u assume u: "u \ set us" then have "?u \ u" by auto from S_trans[OF tu S_supt[OF this]] have "S ?t u" by auto from Fun(1)[OF u this] have "?SN u" . } then have SNu: "set us \ {s . ?SN s}" by blast note IH = IH[OF _ this] from tu have wut: "weight ?u \ weight ?t" by (simp split: if_splits) show ?case proof (cases "?m1 (f, ss) > ?m1 (h, us) \ ?m1 (f, ss) \ ?m1 (h, us) \ pr_strict (?m2 (f, ss)) (?m2 (h, us))") case True from IH[OF True[unfolded split]] show ?thesis by simp next case False with wut w have wut: "weight ?t = weight ?u" "weight ?s = weight ?u" by auto note False = False[unfolded split wut] note tu = tu[unfolded kbo.simps[of ?t] wut, unfolded Fun term.simps, simplified] from tu have gh: "pr_weak ?g ?h" unfolding pr_strict by (auto split: if_splits) from pr_weak_trans[OF fg gh] have fh: "pr_weak ?f ?h" . from False wut fh have "\ pr_strict ?f ?h" unfolding pr_strict by auto with fh have hf: "pr_weak ?h ?f" unfolding pr_strict by auto from pr_weak_trans[OF hf fg] have hg: "pr_weak ?h ?g" . from hg have gh2: "\ pr_strict ?g ?h" unfolding pr_strict by auto from tu gh2 have lex: "fst (?lexu ts us)" by (auto split: if_splits) from fh wut SNu have "pr_weak ?f ?h \ weight ?u \ weight ?s \ set us \ {s. ?SN s}" by auto note inner_IH = inner_IH[OF _ this] show ?thesis proof (rule inner_IH, rule, unfold split, intro conjI ballI) have "fst (?lexu ts us)" by (rule lex) moreover have "length us \ weight ?s" proof - have "length us \ sum_list (map weight us)" proof (induct us) case (Cons u us) from Cons have "length (u # us) \ Suc (sum_list (map weight us))" by auto also have "... \ sum_list (map weight (u # us))" using weight_gt_0[of u] by auto finally show ?case . qed simp also have "\ \ sum_list (map weight (scf_list (scf (h, length us)) us))" by (rule sum_list_scf_list[OF scf]) also have "... \ weight ?s" using wut by simp finally show ?thesis . qed ultimately show "fst (?lex ts us)" unfolding lex_ext_def Let_def by auto qed (insert SN, blast) qed qed qed qed } from this[of f ss] SN_s show "?SN ?s" by auto qed qed } from this[of "(f, ss)", unfolded split] show ?case using Fun by blast qed qed lemma S_SN: "SN {(x, y). S x y}" using kbo_strongly_normalizing unfolding SN_defs by blast subsection \Ground Totality\ lemma ground_SCF [simp]: "ground (SCF t) = ground t" proof - have *: "\i 0" for f :: 'f and xs :: "('f, 'v) term list" using scf by simp show ?thesis by (induct t) (auto simp: set_scf_list [OF *]) qed declare kbo.simps[simp del] lemma ground_vars_term_ms: "ground t \ vars_term_ms t = {#}" by (induct t) auto context fixes F :: "('f \ nat) set" assumes pr_weak: "pr_weak = pr_strict\<^sup>=\<^sup>=" and pr_gtotal: "\f g. f \ F \ g \ F \ f = g \ pr_strict f g \ pr_strict g f" begin lemma S_ground_total: assumes "funas_term s \ F" and "ground s" and "funas_term t \ F" and "ground t" shows "s = t \ S s t \ S t s" using assms proof (induct s arbitrary: t) case IH: (Fun f ss) note [simp] = ground_vars_term_ms let ?s = "Fun f ss" have *: "(vars_term_ms (SCF t) \# vars_term_ms (SCF ?s)) = True" "(vars_term_ms (SCF ?s) \# vars_term_ms (SCF t)) = True" using \ground ?s\ and \ground t\ by (auto simp: scf) from IH(5) obtain g ts where t[simp]: "t = Fun g ts" by (cases t, auto) let ?t = "Fun g ts" let ?f = "(f, length ss)" let ?g = "(g, length ts)" from IH have f: "?f \ F" and g: "?g \ F" by auto { assume "\ ?case" note contra = this[unfolded kbo.simps[of ?s] kbo.simps[of t] *, unfolded t term.simps] from pr_gtotal[OF f g] contra have fg: "?f = ?g" by (auto split: if_splits) have IH: "\(s, t)\set (zip ss ts). s = t \ S s t \ S t s" using IH by (auto elim!: in_set_zipE) blast from fg have len: "length ss = length ts" by auto from lex_ext_unbounded_total[OF IH NS_refl len] contra fg have False by (auto split: if_splits) } then show ?case by blast qed auto end subsection \Summary\ text \ At this point we have shown well-foundedness @{thm [source] S_SN}, transitivity and compatibility @{thm [source] S_trans NS_trans NS_S_compat S_NS_compat}, closure under substitutions @{thm [source] S_subst NS_subst}, closure under contexts @{thm [source] S_ctxt NS_ctxt}, the subterm property @{thm [source] S_supt NS_supteq}, reflexivity of the weak @{thm [source] NS_refl} and irreflexivity of the strict part @{thm [source] S_irrefl}, and ground-totality @{thm [source] S_ground_total}. In particular, this allows us to show that KBO is an instance of strongly normalizing order pairs (@{locale SN_order_pair}). \ sublocale SN_order_pair "{(x, y). S x y}" "{(x, y). NS x y}" by (unfold_locales, insert NS_refl NS_trans S_trans S_SN NS_S_compat S_NS_compat) (auto simp: refl_on_def trans_def, blast+) end end diff --git a/thys/Knuth_Bendix_Order/Term_Aux.thy b/thys/Knuth_Bendix_Order/Term_Aux.thy --- a/thys/Knuth_Bendix_Order/Term_Aux.thy +++ b/thys/Knuth_Bendix_Order/Term_Aux.thy @@ -1,119 +1,119 @@ section \Auxiliaries\ theory Term_Aux imports Subterm_and_Context "HOL-Library.Multiset" begin text \ This theory contains material about terms that is required for KBO, but does not belong to @{theory Knuth_Bendix_Order.Subterm_and_Context}. We plan to merge this material into the theory @{theory First_Order_Terms.Term} at some point. \ text \The variables of a term as multiset.\ fun vars_term_ms :: "('f, 'v) term \ 'v multiset" where "vars_term_ms (Var x) = {#x#}" | - "vars_term_ms (Fun f ts) = \# (mset (map vars_term_ms ts))" + "vars_term_ms (Fun f ts) = \\<^sub># (mset (map vars_term_ms ts))" lemma vars_term_ms_subst [simp]: "vars_term_ms (t \ \) = - \# (image_mset (\ x. vars_term_ms (\ x)) (vars_term_ms t))" (is "_ = ?V t") + \\<^sub># (image_mset (\ x. vars_term_ms (\ x)) (vars_term_ms t))" (is "_ = ?V t") proof (induct t) case (Fun f ts) have IH: "map (\ t. vars_term_ms (t \ \)) ts = map (\ t. ?V t) ts" by (rule map_cong[OF refl Fun]) show ?case by (simp add: o_def IH, induct ts, auto) qed simp lemma vars_term_ms_subst_mono: assumes "vars_term_ms s \# vars_term_ms t" shows "vars_term_ms (s \ \) \# vars_term_ms (t \ \)" proof - from assms[unfolded mset_subset_eq_exists_conv] obtain u where t: "vars_term_ms t = vars_term_ms s + u" by auto show ?thesis unfolding vars_term_ms_subst unfolding t by auto qed lemma set_mset_vars_term_ms [simp]: "set_mset (vars_term_ms t) = vars_term t" by (induct t) auto text \A term is called \<^emph>\ground\ if it does not contain any variables.\ fun ground :: "('f, 'v) term \ bool" where "ground (Var x) \ False" | "ground (Fun f ts) \ (\t \ set ts. ground t)" lemma ground_vars_term_empty: "ground t \ vars_term t = {}" by (induct t) simp_all lemma ground_subst [simp]: "ground (t \ \) \ (\x \ vars_term t. ground (\ x))" by (induct t) simp_all lemma ground_subst_apply: assumes "ground t" shows "t \ \ = t" proof - have "t = t \ Var" by simp also have "\ = t \ \" by (rule term_subst_eq, insert assms[unfolded ground_vars_term_empty], auto) finally show ?thesis by simp qed text \ A \<^emph>\signature\ is a set of function symbol/arity pairs, where the arity of a function symbol, denotes the number of arguments it expects. \ type_synonym 'f sig = "('f \ nat) set" text \The set of all function symbol/ arity pairs occurring in a term.\ fun funas_term :: "('f, 'v) term \ 'f sig" where "funas_term (Var _) = {}" | "funas_term (Fun f ts) = {(f, length ts)} \ \(set (map funas_term ts))" lemma supt_imp_funas_term_subset: assumes "s \ t" shows "funas_term t \ funas_term s" using assms by (induct) auto lemma supteq_imp_funas_term_subset[simp]: assumes "s \ t" shows "funas_term t \ funas_term s" using assms by (induct) auto text \The set of all function symbol/arity pairs occurring in a context.\ fun funas_ctxt :: "('f, 'v) ctxt \ 'f sig" where "funas_ctxt Hole = {}" | "funas_ctxt (More f ss1 D ss2) = {(f, Suc (length (ss1 @ ss2)))} \ funas_ctxt D \ \(set (map funas_term (ss1 @ ss2)))" lemma funas_term_ctxt_apply [simp]: "funas_term (C\t\) = funas_ctxt C \ funas_term t" proof (induct t) case (Var x) show ?case by (induct C) auto next case (Fun f ts) show ?case by (induct C arbitrary: f ts) auto qed lemma funas_term_subst: "funas_term (t \ \) = funas_term t \ \(funas_term ` \ ` vars_term t)" by (induct t) auto lemma funas_ctxt_compose [simp]: "funas_ctxt (C \\<^sub>c D) = funas_ctxt C \ funas_ctxt D" by (induct C) auto lemma funas_ctxt_subst [simp]: "funas_ctxt (C \\<^sub>c \) = funas_ctxt C \ \(funas_term ` \ ` vars_ctxt C)" by (induct C, auto simp: funas_term_subst) end diff --git a/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy b/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy --- a/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy +++ b/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy @@ -1,599 +1,599 @@ (* Title: Lambda-Free Higher-Order Terms Author: Jasmin Blanchette , 2016 Maintainer: Jasmin Blanchette *) section \Lambda-Free Higher-Order Terms\ theory Lambda_Free_Term imports Lambda_Free_Util abbrevs ">s" = ">\<^sub>s" and ">h" = ">\<^sub>h\<^sub>d" and "\\h" = "\\\<^sub>h\<^sub>d" begin text \ This theory defines \\\-free higher-order terms and related locales. \ subsection \Precedence on Symbols\ locale gt_sym = fixes gt_sym :: "'s \ 's \ bool" (infix ">\<^sub>s" 50) assumes gt_sym_irrefl: "\ f >\<^sub>s f" and gt_sym_trans: "h >\<^sub>s g \ g >\<^sub>s f \ h >\<^sub>s f" and gt_sym_total: "f >\<^sub>s g \ g >\<^sub>s f \ g = f" and gt_sym_wf: "wfP (\f g. g >\<^sub>s f)" begin lemma gt_sym_antisym: "f >\<^sub>s g \ \ g >\<^sub>s f" by (metis gt_sym_irrefl gt_sym_trans) end subsection \Heads\ datatype (plugins del: size) (syms_hd: 's, vars_hd: 'v) hd = is_Var: Var (var: 'v) | Sym (sym: 's) abbreviation is_Sym :: "('s, 'v) hd \ bool" where "is_Sym \ \ \ is_Var \" lemma finite_vars_hd[simp]: "finite (vars_hd \)" by (cases \) auto lemma finite_syms_hd[simp]: "finite (syms_hd \)" by (cases \) auto subsection \Terms\ consts head0 :: 'a datatype (syms: 's, vars: 'v) tm = is_Hd: Hd (head: "('s, 'v) hd") | App ("fun": "('s, 'v) tm") (arg: "('s, 'v) tm") where "head (App s _) = head0 s" | "fun (Hd \) = Hd \" | "arg (Hd \) = Hd \" overloading head0 \ "head0 :: ('s, 'v) tm \ ('s, 'v) hd" begin primrec head0 :: "('s, 'v) tm \ ('s, 'v) hd" where "head0 (Hd \) = \" | "head0 (App s _) = head0 s" end lemma head_App[simp]: "head (App s t) = head s" by (cases s) auto declare tm.sel(2)[simp del] lemma head_fun[simp]: "head (fun s) = head s" by (cases s) auto abbreviation ground :: "('s, 'v) tm \ bool" where "ground t \ vars t = {}" abbreviation is_App :: "('s, 'v) tm \ bool" where "is_App s \ \ is_Hd s" lemma size_fun_lt: "is_App s \ size (fun s) < size s" and size_arg_lt: "is_App s \ size (arg s) < size s" by (cases s; simp)+ lemma finite_vars[simp]: "finite (vars s)" and finite_syms[simp]: "finite (syms s)" by (induct s) auto lemma vars_head_subseteq: "vars_hd (head s) \ vars s" and syms_head_subseteq: "syms_hd (head s) \ syms s" by (induct s) auto fun args :: "('s, 'v) tm \ ('s, 'v) tm list" where "args (Hd _) = []" | "args (App s t) = args s @ [t]" lemma set_args_fun: "set (args (fun s)) \ set (args s)" by (cases s) auto lemma arg_in_args: "is_App s \ arg s \ set (args s)" by (cases s rule: tm.exhaust) auto lemma vars_args_subseteq: "si \ set (args s) \ vars si \ vars s" and syms_args_subseteq: "si \ set (args s) \ syms si \ syms s" by (induct s) auto lemma args_Nil_iff_is_Hd: "args s = [] \ is_Hd s" by (cases s) auto abbreviation num_args :: "('s, 'v) tm \ nat" where "num_args s \ length (args s)" lemma size_ge_num_args: "size s \ num_args s" by (induct s) auto lemma Hd_head_id: "num_args s = 0 \ Hd (head s) = s" by (metis args.cases args.simps(2) length_0_conv snoc_eq_iff_butlast tm.collapse(1) tm.disc(1)) lemma one_arg_imp_Hd: "num_args s = 1 \ s = App t u \ t = Hd (head t)" by (simp add: Hd_head_id) lemma size_in_args: "s \ set (args t) \ size s < size t" by (induct t) auto primrec apps :: "('s, 'v) tm \ ('s, 'v) tm list \ ('s, 'v) tm" where "apps s [] = s" | "apps s (t # ts) = apps (App s t) ts" lemma vars_apps[simp]: "vars (apps s ss) = vars s \ (\s \ set ss. vars s)" and syms_apps[simp]: "syms (apps s ss) = syms s \ (\s \ set ss. syms s)" and head_apps[simp]: "head (apps s ss) = head s" and args_apps[simp]: "args (apps s ss) = args s @ ss" and is_App_apps[simp]: "is_App (apps s ss) \ args (apps s ss) \ []" and fun_apps_Nil[simp]: "fun (apps s []) = fun s" and fun_apps_Cons[simp]: "fun (apps (App s sa) ss) = apps s (butlast (sa # ss))" and arg_apps_Nil[simp]: "arg (apps s []) = arg s" and arg_apps_Cons[simp]: "arg (apps (App s sa) ss) = last (sa # ss)" by (induct ss arbitrary: s sa) (auto simp: args_Nil_iff_is_Hd) lemma apps_append[simp]: "apps s (ss @ ts) = apps (apps s ss) ts" by (induct ss arbitrary: s ts) auto lemma App_apps: "App (apps s ts) t = apps s (ts @ [t])" by simp lemma tm_inject_apps[iff, induct_simp]: "apps (Hd \) ss = apps (Hd \) ts \ \ = \ \ ss = ts" by (metis args_apps head_apps same_append_eq tm.sel(1)) lemma tm_collapse_apps[simp]: "apps (Hd (head s)) (args s) = s" by (induct s) auto lemma tm_expand_apps: "head s = head t \ args s = args t \ s = t" by (metis tm_collapse_apps) lemma tm_exhaust_apps_sel[case_names apps]: "(s = apps (Hd (head s)) (args s) \ P) \ P" by (atomize_elim, induct s) auto lemma tm_exhaust_apps[case_names apps]: "(\\ ss. s = apps (Hd \) ss \ P) \ P" by (metis tm_collapse_apps) lemma tm_induct_apps[case_names apps]: assumes "\\ ss. (\s. s \ set ss \ P s) \ P (apps (Hd \) ss)" shows "P s" using assms by (induct s taking: size rule: measure_induct_rule) (metis size_in_args tm_collapse_apps) lemma ground_fun: "ground s \ ground (fun s)" and ground_arg: "ground s \ ground (arg s)" by (induct s) auto lemma ground_head: "ground s \ is_Sym (head s)" by (cases s rule: tm_exhaust_apps) (auto simp: is_Var_def) lemma ground_args: "t \ set (args s) \ ground s \ ground t" by (induct s rule: tm_induct_apps) auto primrec vars_mset :: "('s, 'v) tm \ 'v multiset" where "vars_mset (Hd \) = mset_set (vars_hd \)" | "vars_mset (App s t) = vars_mset s + vars_mset t" lemma set_vars_mset[simp]: "set_mset (vars_mset t) = vars t" by (induct t) auto lemma vars_mset_empty_iff[iff]: "vars_mset s = {#} \ ground s" by (induct s) (auto simp: mset_set_empty_iff) lemma vars_mset_fun[intro]: "vars_mset (fun t) \# vars_mset t" by (cases t) auto lemma vars_mset_arg[intro]: "vars_mset (arg t) \# vars_mset t" by (cases t) auto subsection \hsize\ text \The hsize of a term is the number of heads (Syms or Vars) in the term.\ primrec hsize :: "('s, 'v) tm \ nat" where "hsize (Hd \) = 1" | "hsize (App s t) = hsize s + hsize t" lemma hsize_size: "hsize t * 2 = size t + 1" by (induct t) auto lemma hsize_pos[simp]: "hsize t > 0" by (induction t; simp) lemma hsize_fun_lt: "is_App s \ hsize (fun s) < hsize s" by (cases s; simp) lemma hsize_arg_lt: "is_App s \ hsize (arg s) < hsize s" by (cases s; simp) lemma hsize_ge_num_args: "hsize s \ hsize s" by (induct s) auto lemma hsize_in_args: "s \ set (args t) \ hsize s < hsize t" by (induct t) auto lemma hsize_apps: "hsize (apps t ts) = hsize t + sum_list (map hsize ts)" by (induct ts arbitrary:t; simp) lemma hsize_args: "1 + sum_list (map hsize (args t)) = hsize t" by (metis hsize.simps(1) hsize_apps tm_collapse_apps) subsection \Substitutions\ primrec subst :: "('v \ ('s, 'v) tm) \ ('s, 'v) tm \ ('s, 'v) tm" where "subst \ (Hd \) = (case \ of Var x \ \ x | Sym f \ Hd (Sym f))" | "subst \ (App s t) = App (subst \ s) (subst \ t)" lemma subst_apps[simp]: "subst \ (apps s ts) = apps (subst \ s) (map (subst \) ts)" by (induct ts arbitrary: s) auto lemma head_subst[simp]: "head (subst \ s) = head (subst \ (Hd (head s)))" by (cases s rule: tm_exhaust_apps) (auto split: hd.split) lemma args_subst[simp]: "args (subst \ s) = (case head s of Var x \ args (\ x) | Sym f \ []) @ map (subst \) (args s)" by (cases s rule: tm_exhaust_apps) (auto split: hd.split) lemma ground_imp_subst_iden: "ground s \ subst \ s = s" by (induct s) (auto split: hd.split) -lemma vars_mset_subst[simp]: "vars_mset (subst \ s) = (\# {#vars_mset (\ x). x \# vars_mset s#})" +lemma vars_mset_subst[simp]: "vars_mset (subst \ s) = (\\<^sub># {#vars_mset (\ x). x \# vars_mset s#})" proof (induct s) case (Hd \) show ?case by (cases \) auto qed auto lemma vars_mset_subst_subseteq: "vars_mset t \# vars_mset s \ vars_mset (subst \ t) \# vars_mset (subst \ s)" unfolding vars_mset_subst by (metis (no_types) add_diff_cancel_right' diff_subset_eq_self image_mset_union sum_mset.union subset_mset.add_diff_inverse) lemma vars_subst_subseteq: "vars t \ vars s \ vars (subst \ t) \ vars (subst \ s)" unfolding set_vars_mset[symmetric] vars_mset_subst by auto subsection \Subterms\ inductive sub :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where sub_refl: "sub s s" | sub_fun: "sub s t \ sub s (App u t)" | sub_arg: "sub s t \ sub s (App t u)" inductive_cases sub_HdE[simplified, elim]: "sub s (Hd \)" inductive_cases sub_AppE[simplified, elim]: "sub s (App t u)" inductive_cases sub_Hd_HdE[simplified, elim]: "sub (Hd \) (Hd \)" inductive_cases sub_Hd_AppE[simplified, elim]: "sub (Hd \) (App t u)" lemma in_vars_imp_sub: "x \ vars s \ sub (Hd (Var x)) s" by induct (auto intro: sub.intros elim: hd.set_cases(2)) lemma sub_args: "s \ set (args t) \ sub s t" by (induct t) (auto intro: sub.intros) lemma sub_size: "sub s t \ size s \ size t" by induct auto lemma sub_subst: "sub s t \ sub (subst \ s) (subst \ t)" proof (induct t) case (Hd \) thus ?case by (cases \; blast intro: sub.intros) qed (auto intro: sub.intros del: sub_AppE elim!: sub_AppE) abbreviation proper_sub :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where "proper_sub s t \ sub s t \ s \ t" lemma proper_sub_Hd[simp]: "\ proper_sub s (Hd \)" using sub.cases by blast lemma proper_sub_subst: assumes psub: "proper_sub s t" shows "proper_sub (subst \ s) (subst \ t)" proof (cases t) case Hd thus ?thesis using psub by simp next case t: (App t1 t2) have "sub s t1 \ sub s t2" using t psub by blast hence "sub (subst \ s) (subst \ t1) \ sub (subst \ s) (subst \ t2)" using sub_subst by blast thus ?thesis unfolding t by (auto intro: sub.intros dest: sub_size) qed subsection \Maximum Arities\ locale arity = fixes arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" begin primrec arity_hd :: "('s, 'v) hd \ enat" where "arity_hd (Var x) = arity_var x" | "arity_hd (Sym f) = arity_sym f" definition arity :: "('s, 'v) tm \ enat" where "arity s = arity_hd (head s) - num_args s" lemma arity_simps[simp]: "arity (Hd \) = arity_hd \" "arity (App s t) = arity s - 1" by (auto simp: arity_def enat_diff_diff_eq add.commute eSuc_enat plus_1_eSuc(1)) lemma arity_apps[simp]: "arity (apps s ts) = arity s - length ts" proof (induct ts arbitrary: s) case (Cons t ts) thus ?case by (case_tac "arity s"; simp add: one_enat_def) qed simp inductive wary :: "('s, 'v) tm \ bool" where wary_Hd[intro]: "wary (Hd \)" | wary_App[intro]: "wary s \ wary t \ num_args s < arity_hd (head s) \ wary (App s t)" inductive_cases wary_HdE: "wary (Hd \)" inductive_cases wary_AppE: "wary (App s t)" inductive_cases wary_binaryE[simplified]: "wary (App (App s t) u)" lemma wary_fun[intro]: "wary t \ wary (fun t)" by (cases t) (auto elim: wary.cases) lemma wary_arg[intro]: "wary t \ wary (arg t)" by (cases t) (auto elim: wary.cases) lemma wary_args: "s \ set (args t) \ wary t \ wary s" by (induct t arbitrary: s, simp) (metis Un_iff args.simps(2) wary.cases insert_iff length_pos_if_in_set less_numeral_extra(3) list.set(2) list.size(3) set_append tm.distinct(1) tm.inject(2)) lemma wary_sub: "sub s t \ wary t \ wary s" by (induct rule: sub.induct) (auto elim: wary.cases) lemma wary_inf_ary: "(\\. arity_hd \ = \) \ wary s" by induct auto lemma wary_num_args_le_arity_head: "wary s \ num_args s \ arity_hd (head s)" by (induct rule: wary.induct) (auto simp: zero_enat_def[symmetric] Suc_ile_eq) lemma wary_apps: "wary s \ (\sa. sa \ set ss \ wary sa) \ length ss \ arity s \ wary (apps s ss)" proof (induct ss arbitrary: s) case (Cons sa ss) note ih = this(1) and wary_s = this(2) and wary_ss = this(3) and nargs_s_sa_ss = this(4) show ?case unfolding apps.simps proof (rule ih) have "wary sa" using wary_ss by simp moreover have " enat (num_args s) < arity_hd (head s)" by (metis (mono_tags) One_nat_def add.comm_neutral arity_def diff_add_zero enat_ord_simps(1) idiff_enat_enat less_one list.size(4) nargs_s_sa_ss not_add_less2 order.not_eq_order_implies_strict wary_num_args_le_arity_head wary_s) ultimately show "wary (App s sa)" by (rule wary_App[OF wary_s]) next show "\sa. sa \ set ss \ wary sa" using wary_ss by simp next show "length ss \ arity (App s sa)" proof (cases "arity s") case enat thus ?thesis using nargs_s_sa_ss by (simp add: one_enat_def) qed simp qed qed simp lemma wary_cases_apps[consumes 1, case_names apps]: assumes wary_t: "wary t" and apps: "\\ ss. t = apps (Hd \) ss \ (\sa. sa \ set ss \ wary sa) \ length ss \ arity_hd \ \ P" shows P using apps proof (atomize_elim, cases t rule: tm_exhaust_apps) case t: (apps \ ss) show "\\ ss. t = apps (Hd \) ss \ (\sa. sa \ set ss \ wary sa) \ enat (length ss) \ arity_hd \" by (rule exI[of _ \], rule exI[of _ ss]) (auto simp: t wary_args[OF _ wary_t] wary_num_args_le_arity_head[OF wary_t, unfolded t, simplified]) qed lemma arity_hd_head: "wary s \ arity_hd (head s) = arity s + num_args s" by (simp add: arity_def enat_sub_add_same wary_num_args_le_arity_head) lemma arity_head_ge: "arity_hd (head s) \ arity s" by (induct s) (auto intro: enat_le_imp_minus_le) inductive wary_fo :: "('s, 'v) tm \ bool" where wary_foI[intro]: "is_Hd s \ is_Sym (head s) \ length (args s) = arity_hd (head s) \ (\t \ set (args s). wary_fo t) \ wary_fo s" lemma wary_fo_args: "s \ set (args t) \ wary_fo t \ wary_fo s" by (induct t arbitrary: s rule: tm_induct_apps, simp) (metis args.simps(1) args_apps self_append_conv2 wary_fo.cases) lemma wary_fo_arg: "wary_fo (App s t) \ wary_fo t" by (erule wary_fo.cases) auto end subsection \Potential Heads of Ground Instances of Variables\ locale ground_heads = gt_sym "(>\<^sub>s)" + arity arity_sym arity_var for gt_sym :: "'s \ 's \ bool" (infix ">\<^sub>s" 50) and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" + fixes ground_heads_var :: "'v \ 's set" assumes ground_heads_var_arity: "f \ ground_heads_var x \ arity_sym f \ arity_var x" and ground_heads_var_nonempty: "ground_heads_var x \ {}" begin primrec ground_heads :: "('s, 'v) hd \ 's set" where "ground_heads (Var x) = ground_heads_var x" | "ground_heads (Sym f) = {f}" lemma ground_heads_arity: "f \ ground_heads \ \ arity_sym f \ arity_hd \" by (cases \) (auto simp: ground_heads_var_arity) lemma ground_heads_nonempty[simp]: "ground_heads \ \ {}" by (cases \) (auto simp: ground_heads_var_nonempty) lemma sym_in_ground_heads: "is_Sym \ \ sym \ \ ground_heads \" by (metis ground_heads.simps(2) hd.collapse(2) hd.set_sel(1) hd.simps(16)) lemma ground_hd_in_ground_heads: "ground s \ sym (head s) \ ground_heads (head s)" by (simp add: ground_head sym_in_ground_heads) lemma some_ground_head_arity: "arity_sym (SOME f. f \ ground_heads (Var x)) \ arity_var x" by (simp add: ground_heads_var_arity ground_heads_var_nonempty some_in_eq) definition wary_subst :: "('v \ ('s, 'v) tm) \ bool" where "wary_subst \ \ (\x. wary (\ x) \ arity (\ x) \ arity_var x \ ground_heads (head (\ x)) \ ground_heads_var x)" definition strict_wary_subst :: "('v \ ('s, 'v) tm) \ bool" where "strict_wary_subst \ \ (\x. wary (\ x) \ arity (\ x) \ {arity_var x, \} \ ground_heads (head (\ x)) \ ground_heads_var x)" lemma strict_imp_wary_subst: "strict_wary_subst \ \ wary_subst \" unfolding strict_wary_subst_def wary_subst_def using eq_iff by force lemma wary_subst_wary: assumes wary_\: "wary_subst \" and wary_s: "wary s" shows "wary (subst \ s)" using wary_s proof (induct s rule: tm.induct) case (App s t) note wary_st = this(3) from wary_st have wary_s: "wary s" by (rule wary_AppE) from wary_st have wary_t: "wary t" by (rule wary_AppE) from wary_st have nargs_s_lt: "num_args s < arity_hd (head s)" by (rule wary_AppE) note wary_\s = App(1)[OF wary_s] note wary_\t = App(2)[OF wary_t] note wary_\x = wary_\[unfolded wary_subst_def, rule_format, THEN conjunct1] note ary_\x = wary_\[unfolded wary_subst_def, rule_format, THEN conjunct2] have "num_args (\ x) + num_args s < arity_hd (head (\ x))" if hd_s: "head s = Var x" for x proof - have ary_hd_s: "arity_hd (head s) = arity_var x" using hd_s arity_hd.simps(1) by presburger hence "num_args s \ arity (\ x)" by (metis (no_types) wary_num_args_le_arity_head ary_\x dual_order.trans wary_s) hence "num_args s + num_args (\ x) \ arity_hd (head (\ x))" by (metis (no_types) arity_hd_head[OF wary_\x] add_right_mono plus_enat_simps(1)) thus ?thesis using ary_hd_s by (metis (no_types) add.commute add_diff_cancel_left' ary_\x arity_def idiff_enat_enat leD nargs_s_lt order.not_eq_order_implies_strict) qed hence nargs_\s: "num_args (subst \ s) < arity_hd (head (subst \ s))" using nargs_s_lt by (auto split: hd.split) show ?case by simp (rule wary_App[OF wary_\s wary_\t nargs_\s]) qed (auto simp: wary_\[unfolded wary_subst_def] split: hd.split) lemmas strict_wary_subst_wary = wary_subst_wary[OF strict_imp_wary_subst] lemma wary_subst_ground_heads: assumes wary_\: "wary_subst \" shows "ground_heads (head (subst \ s)) \ ground_heads (head s)" proof (induct s rule: tm_induct_apps) case (apps \ ss) show ?case proof (cases \) case x: (Var x) thus ?thesis using wary_\ wary_subst_def x by auto qed auto qed lemmas strict_wary_subst_ground_heads = wary_subst_ground_heads[OF strict_imp_wary_subst] definition grounding_\ :: "'v \ ('s, 'v) tm" where "grounding_\ x = (let s = Hd (Sym (SOME f. f \ ground_heads_var x)) in apps s (replicate (the_enat (arity s - arity_var x)) s))" lemma ground_grounding_\: "ground (subst grounding_\ s)" by (induct s) (auto simp: Let_def grounding_\_def elim: hd.set_cases(2) split: hd.split) lemma strict_wary_grounding_\: "strict_wary_subst grounding_\" unfolding strict_wary_subst_def proof (intro allI conjI) fix x define f where "f = (SOME f. f \ ground_heads_var x)" define s :: "('s, 'v) tm" where "s = Hd (Sym f)" have wary_s: "wary s" unfolding s_def by (rule wary_Hd) have ary_s_ge_x: "arity s \ arity_var x" unfolding s_def f_def using some_ground_head_arity by simp have gr\_x: "grounding_\ x = apps s (replicate (the_enat (arity s - arity_var x)) s)" unfolding grounding_\_def Let_def f_def[symmetric] s_def[symmetric] by (rule refl) show "wary (grounding_\ x)" unfolding gr\_x by (auto intro!: wary_s wary_apps[OF wary_s] enat_the_enat_minus_le) show "arity (grounding_\ x) \ {arity_var x, \}" unfolding gr\_x using ary_s_ge_x by (cases "arity s"; cases "arity_var x"; simp) show "ground_heads (head (grounding_\ x)) \ ground_heads_var x" unfolding gr\_x s_def f_def by (simp add: some_in_eq ground_heads_var_nonempty) qed lemmas wary_grounding_\ = strict_wary_grounding_\[THEN strict_imp_wary_subst] definition gt_hd :: "('s, 'v) hd \ ('s, 'v) hd \ bool" (infix ">\<^sub>h\<^sub>d" 50) where "\ >\<^sub>h\<^sub>d \ \ (\g \ ground_heads \. \f \ ground_heads \. g >\<^sub>s f)" definition comp_hd :: "('s, 'v) hd \ ('s, 'v) hd \ bool" (infix "\\\<^sub>h\<^sub>d" 50) where "\ \\\<^sub>h\<^sub>d \ \ \ = \ \ \ >\<^sub>h\<^sub>d \ \ \ >\<^sub>h\<^sub>d \" lemma gt_hd_irrefl: "\ \ >\<^sub>h\<^sub>d \" unfolding gt_hd_def using gt_sym_irrefl by (meson ex_in_conv ground_heads_nonempty) lemma gt_hd_trans: "\ >\<^sub>h\<^sub>d \ \ \ >\<^sub>h\<^sub>d \ \ \ >\<^sub>h\<^sub>d \" unfolding gt_hd_def using gt_sym_trans by (meson ex_in_conv ground_heads_nonempty) lemma gt_sym_imp_hd: "g >\<^sub>s f \ Sym g >\<^sub>h\<^sub>d Sym f" unfolding gt_hd_def by simp lemma not_comp_hd_imp_Var: "\ \ \\\<^sub>h\<^sub>d \ \ is_Var \ \ is_Var \" using gt_sym_total by (cases \; cases \; auto simp: comp_hd_def gt_hd_def) end end diff --git a/thys/Nested_Multisets_Ordinals/Multiset_More.thy b/thys/Nested_Multisets_Ordinals/Multiset_More.thy --- a/thys/Nested_Multisets_Ordinals/Multiset_More.thy +++ b/thys/Nested_Multisets_Ordinals/Multiset_More.thy @@ -1,1032 +1,1032 @@ (* Title: More about Multisets Author: Mathias Fleury , 2015 Author: Jasmin Blanchette , 2014, 2015 Author: Anders Schlichtkrull , 2017 Author: Dmitriy Traytel , 2014 Maintainer: Mathias Fleury *) section \More about Multisets\ theory Multiset_More imports "HOL-Library.Multiset_Order" "HOL-Library.Sublist" begin text \ Isabelle's theory of finite multisets is not as developed as other areas, such as lists and sets. The present theory introduces some missing concepts and lemmas. Some of it is expected to move to Isabelle's library. \ subsection \Basic Setup\ declare diff_single_trivial [simp] in_image_mset [iff] image_mset.compositionality [simp] (*To have the same rules as the set counter-part*) mset_subset_eqD[dest, intro?] (*@{thm subsetD}*) Multiset.in_multiset_in_set[simp] inter_add_left1[simp] inter_add_left2[simp] inter_add_right1[simp] inter_add_right2[simp] sum_mset_sum_list[simp] subsection \Lemmas about Intersection, Union and Pointwise Inclusion\ lemma subset_mset_imp_subset_add_mset: "A \# B \ A \# add_mset x B" by (metis add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def subset_mset.inf.absorb2) lemma subset_add_mset_notin_subset_mset: \A \# add_mset b B \ b \# A \ A \# B\ by (simp add: subset_mset.le_iff_sup) lemma subset_msetE: "\A \# B; \A \# B; \ B \# A\ \ R\ \ R" by (simp add: subset_mset.less_le_not_le) lemma Diff_triv_mset: "M \# N = {#} \ M - N = M" by (metis diff_intersect_left_idem diff_zero) lemma diff_intersect_sym_diff: "(A - B) \# (B - A) = {#}" unfolding multiset_inter_def proof - have "A - (B - (B - A)) = A - B" by (metis diff_intersect_right_idem multiset_inter_def) then show "A - B - (A - B - (B - A)) = {#}" by (metis diff_add diff_cancel diff_subset_eq_self subset_mset.diff_add) qed declare subset_msetE [elim!] lemma subseq_mset_subseteq_mset: "subseq xs ys \ mset xs \# mset ys" proof (induct xs arbitrary: ys) case (Cons x xs) note Outer_Cons = this then show ?case proof (induct ys) case (Cons y ys) have "subseq xs ys" by (metis Cons.prems(2) subseq_Cons' subseq_Cons2_iff) then show ?case using Cons by (metis mset.simps(2) mset_subset_eq_add_mset_cancel subseq_Cons2_iff subset_mset_imp_subset_add_mset) qed simp qed simp subsection \Lemmas about Filter and Image\ lemma count_image_mset_ge_count: "count (image_mset f A) (f b) \ count A b" by (induction A) auto lemma count_image_mset_inj: assumes \inj f\ shows \count (image_mset f M) (f x) = count M x\ by (induct M) (use assms in \auto simp: inj_on_def\) lemma count_image_mset_le_count_inj_on: "inj_on f (set_mset M) \ count (image_mset f M) y \ count M (inv_into (set_mset M) f y)" proof (induct M) case (add x M) note ih = this(1) and inj_xM = this(2) have inj_M: "inj_on f (set_mset M)" using inj_xM by simp show ?case proof (cases "x \# M") case x_in_M: True show ?thesis proof (cases "y = f x") case y_eq_fx: True show ?thesis using x_in_M ih[OF inj_M] unfolding y_eq_fx by (simp add: inj_M insert_absorb) next case y_ne_fx: False show ?thesis using x_in_M ih[OF inj_M] y_ne_fx insert_absorb by fastforce qed next case x_ni_M: False show ?thesis proof (cases "y = f x") case y_eq_fx: True have "f x \# image_mset f M" using x_ni_M inj_xM by force thus ?thesis unfolding y_eq_fx by (metis (no_types) inj_xM count_add_mset count_greater_eq_Suc_zero_iff count_inI image_mset_add_mset inv_into_f_f union_single_eq_member) next case y_ne_fx: False show ?thesis proof (rule ccontr) assume neg_conj: "\ count (image_mset f (add_mset x M)) y \ count (add_mset x M) (inv_into (set_mset (add_mset x M)) f y)" have cnt_y: "count (add_mset (f x) (image_mset f M)) y = count (image_mset f M) y" using y_ne_fx by simp have "inv_into (set_mset M) f y \# add_mset x M \ inv_into (set_mset (add_mset x M)) f (f (inv_into (set_mset M) f y)) = inv_into (set_mset M) f y" by (meson inj_xM inv_into_f_f) hence "0 < count (image_mset f (add_mset x M)) y \ count M (inv_into (set_mset M) f y) = 0 \ x = inv_into (set_mset M) f y" using neg_conj cnt_y ih[OF inj_M] by (metis (no_types) count_add_mset count_greater_zero_iff count_inI f_inv_into_f image_mset_add_mset set_image_mset) thus False using neg_conj cnt_y x_ni_M ih[OF inj_M] by (metis (no_types) count_greater_zero_iff count_inI eq_iff image_mset_add_mset less_imp_le) qed qed qed qed simp lemma mset_filter_compl: "mset (filter p xs) + mset (filter (Not \ p) xs) = mset xs" by (induction xs) (auto simp: ac_simps) text \Near duplicate of @{thm [source] filter_eq_replicate_mset}: @{thm filter_eq_replicate_mset}.\ lemma filter_mset_eq: "filter_mset ((=) L) A = replicate_mset (count A L) L" by (auto simp: multiset_eq_iff) lemma filter_mset_cong[fundef_cong]: assumes "M = M'" "\a. a \# M \ P a = Q a" shows "filter_mset P M = filter_mset Q M" proof - have "M - filter_mset Q M = filter_mset (\a. \Q a) M" by (metis multiset_partition add_diff_cancel_left') then show ?thesis by (auto simp: filter_mset_eq_conv assms) qed lemma image_mset_filter_swap: "image_mset f {# x \# M. P (f x)#} = {# x \# image_mset f M. P x#}" by (induction M) auto lemma image_mset_cong2: "(\x. x \# M \ f x = g x) \ M = N \ image_mset f M = image_mset g N" by (hypsubst, rule image_mset_cong) lemma filter_mset_empty_conv: \(filter_mset P M = {#}) = (\L\#M. \ P L)\ by (induction M) auto lemma multiset_filter_mono2: \filter_mset P A \# filter_mset Q A \ (\a\#A. P a \ Q a)\ by (induction A) (auto intro: subset_mset.order.trans) lemma image_filter_cong: assumes \\C. C \# M \ P C \ f C = g C\ shows \{#f C. C \# {#C \# M. P C#}#} = {#g C | C\# M. P C#}\ using assms by (induction M) auto lemma image_mset_filter_swap2: \{#C \# {#P x. x \# D#}. Q C #} = {#P x. x \# {#C| C \# D. Q (P C)#}#}\ by (simp add: image_mset_filter_swap) declare image_mset_cong2 [cong] lemma filter_mset_empty_if_finite_and_filter_set_empty: assumes "{x \ X. P x} = {}" and "finite X" shows "{#x \# mset_set X. P x#} = {#}" proof - have empty_empty: "\Y. set_mset Y = {} \ Y = {#}" by auto from assms have "set_mset {#x \# mset_set X. P x#} = {}" by auto then show ?thesis by (rule empty_empty) qed subsection \Lemmas about Sum\ lemma sum_image_mset_sum_map[simp]: "sum_mset (image_mset f (mset xs)) = sum_list (map f xs)" by (metis mset_map sum_mset_sum_list) lemma sum_image_mset_mono: fixes f :: "'a \ 'b::canonically_ordered_monoid_add" assumes sub: "A \# B" shows "(\m \# A. f m) \ (\m \# B. f m)" by (metis image_mset_union le_iff_add sub subset_mset.add_diff_inverse sum_mset.union) lemma sum_image_mset_mono_mem: "n \# M \ f n \ (\m \# M. f m)" for f :: "'a \ 'b::canonically_ordered_monoid_add" using le_iff_add multi_member_split by fastforce lemma count_sum_mset_if_1_0: \count M a = (\x\#M. if x = a then 1 else 0)\ by (induction M) auto lemma sum_mset_dvd: fixes k :: "'a::comm_semiring_1_cancel" assumes "\m \# M. k dvd f m" shows "k dvd (\m \# M. f m)" using assms by (induct M) auto lemma sum_mset_distrib_div_if_dvd: fixes k :: "'a::unique_euclidean_semiring" assumes "\m \# M. k dvd f m" shows "(\m \# M. f m) div k = (\m \# M. f m div k)" using assms by (induct M) (auto simp: div_plus_div_distrib_dvd_left) subsection \Lemmas about Remove\ lemma set_mset_minus_replicate_mset[simp]: "n \ count A a \ set_mset (A - replicate_mset n a) = set_mset A - {a}" "n < count A a \ set_mset (A - replicate_mset n a) = set_mset A" unfolding set_mset_def by (auto split: if_split simp: not_in_iff) abbreviation removeAll_mset :: "'a \ 'a multiset \ 'a multiset" where "removeAll_mset C M \ M - replicate_mset (count M C) C" lemma mset_removeAll[simp, code]: "removeAll_mset C (mset L) = mset (removeAll C L)" by (induction L) (auto simp: ac_simps multiset_eq_iff split: if_split_asm) lemma removeAll_mset_filter_mset: "removeAll_mset C M = filter_mset ((\) C) M" by (induction M) (auto simp: ac_simps multiset_eq_iff) abbreviation remove1_mset :: "'a \ 'a multiset \ 'a multiset" where "remove1_mset C M \ M - {#C#}" lemma removeAll_subseteq_remove1_mset: "removeAll_mset x M \# remove1_mset x M" by (auto simp: subseteq_mset_def) lemma in_remove1_mset_neq: assumes ab: "a \ b" shows "a \# remove1_mset b C \ a \# C" by (metis assms diff_single_trivial in_diffD insert_DiffM insert_noteq_member) lemma size_mset_removeAll_mset_le_iff: "size (removeAll_mset x M) < size M \ x \# M" by (auto intro: count_inI mset_subset_size simp: subset_mset_def multiset_eq_iff) lemma size_remove1_mset_If: \size (remove1_mset x M) = size M - (if x \# M then 1 else 0)\ by (auto simp: size_Diff_subset_Int) lemma size_mset_remove1_mset_le_iff: "size (remove1_mset x M) < size M \ x \# M" using less_irrefl by (fastforce intro!: mset_subset_size elim: in_countE simp: subset_mset_def multiset_eq_iff) lemma remove_1_mset_id_iff_notin: "remove1_mset a M = M \ a \# M" by (meson diff_single_trivial multi_drop_mem_not_eq) lemma id_remove_1_mset_iff_notin: "M = remove1_mset a M \ a \# M" using remove_1_mset_id_iff_notin by metis lemma remove1_mset_eqE: "remove1_mset L x1 = M \ (L \# x1 \ x1 = M + {#L#} \ P) \ (L \# x1 \ x1 = M \ P) \ P" by (cases "L \# x1") auto lemma image_filter_ne_mset[simp]: "image_mset f {#x \# M. f x \ y#} = removeAll_mset y (image_mset f M)" by (induction M) simp_all lemma image_mset_remove1_mset_if: "image_mset f (remove1_mset a M) = (if a \# M then remove1_mset (f a) (image_mset f M) else image_mset f M)" by (auto simp: image_mset_Diff) lemma filter_mset_neq: "{#x \# M. x \ y#} = removeAll_mset y M" by (metis add_diff_cancel_left' filter_eq_replicate_mset multiset_partition) lemma filter_mset_neq_cond: "{#x \# M. P x \ x \ y#} = removeAll_mset y {# x\#M. P x#}" by (metis filter_filter_mset filter_mset_neq) lemma remove1_mset_add_mset_If: "remove1_mset L (add_mset L' C) = (if L = L' then C else remove1_mset L C + {#L'#})" by (auto simp: multiset_eq_iff) lemma minus_remove1_mset_if: "A - remove1_mset b B = (if b \# B \ b \# A \ count A b \ count B b then {#b#} + (A - B) else A - B)" by (auto simp: multiset_eq_iff count_greater_zero_iff[symmetric] simp del: count_greater_zero_iff) lemma add_mset_eq_add_mset_ne: "a \ b \ add_mset a A = add_mset b B \ a \# B \ b \# A \ A = add_mset b (B - {#a#})" by (metis (no_types, lifting) diff_single_eq_union diff_union_swap multi_self_add_other_not_self remove_1_mset_id_iff_notin union_single_eq_diff) lemma add_mset_eq_add_mset: \add_mset a M = add_mset b M' \ (a = b \ M = M') \ (a \ b \ b \# M \ add_mset a (M - {#b#}) = M')\ by (metis add_mset_eq_add_mset_ne add_mset_remove_trivial union_single_eq_member) (* TODO move to Multiset: could replace add_mset_remove_trivial_eq? *) lemma add_mset_remove_trivial_iff: \N = add_mset a (N - {#b#}) \ a \# N \ a = b\ by (metis add_left_cancel add_mset_remove_trivial insert_DiffM2 single_eq_single size_mset_remove1_mset_le_iff union_single_eq_member) lemma trivial_add_mset_remove_iff: \add_mset a (N - {#b#}) = N \ a \# N \ a = b\ by (subst eq_commute) (fact add_mset_remove_trivial_iff) lemma remove1_single_empty_iff[simp]: \remove1_mset L {#L'#} = {#} \ L = L'\ using add_mset_remove_trivial_iff by fastforce lemma add_mset_less_imp_less_remove1_mset: assumes xM_lt_N: "add_mset x M < N" shows "M < remove1_mset x N" proof - have "M < N" using assms le_multiset_right_total mset_le_trans by blast then show ?thesis by (metis add_less_cancel_right add_mset_add_single diff_single_trivial insert_DiffM2 xM_lt_N) qed subsection \Lemmas about Replicate\ lemma replicate_mset_minus_replicate_mset_same[simp]: "replicate_mset m x - replicate_mset n x = replicate_mset (m - n) x" by (induct m arbitrary: n, simp, metis left_diff_repeat_mset_distrib' repeat_mset_replicate_mset) lemma replicate_mset_subset_iff_lt[simp]: "replicate_mset m x \# replicate_mset n x \ m < n" by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI) lemma replicate_mset_subseteq_iff_le[simp]: "replicate_mset m x \# replicate_mset n x \ m \ n" by (induct n m rule: diff_induct) auto lemma replicate_mset_lt_iff_lt[simp]: "replicate_mset m x < replicate_mset n x \ m < n" by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI gr_zeroI) lemma replicate_mset_le_iff_le[simp]: "replicate_mset m x \ replicate_mset n x \ m \ n" by (induct n m rule: diff_induct) auto lemma replicate_mset_eq_iff[simp]: "replicate_mset m x = replicate_mset n y \ m = n \ (m \ 0 \ x = y)" by (cases m; cases n; simp) (metis in_replicate_mset insert_noteq_member size_replicate_mset union_single_eq_diff) lemma replicate_mset_plus: "replicate_mset (a + b) C = replicate_mset a C + replicate_mset b C" by (induct a) (auto simp: ac_simps) lemma mset_replicate_replicate_mset: "mset (replicate n L) = replicate_mset n L" by (induction n) auto lemma set_mset_single_iff_replicate_mset: "set_mset U = {a} \ (\n > 0. U = replicate_mset n a)" by (rule, metis count_greater_zero_iff count_replicate_mset insertI1 multi_count_eq singletonD zero_less_iff_neq_zero, force) lemma ex_replicate_mset_if_all_elems_eq: assumes "\x \# M. x = y" shows "\n. M = replicate_mset n y" using assms by (metis count_replicate_mset mem_Collect_eq multiset_eqI neq0_conv set_mset_def) subsection \Multiset and Set Conversions\ lemma count_mset_set_if: "count (mset_set A) a = (if a \ A \ finite A then 1 else 0)" by auto lemma mset_set_set_mset_empty_mempty[iff]: "mset_set (set_mset D) = {#} \ D = {#}" by (simp add: mset_set_empty_iff) lemma count_mset_set_le_one: "count (mset_set A) x \ 1" by (simp add: count_mset_set_if) lemma mset_set_set_mset_subseteq[simp]: "mset_set (set_mset A) \# A" by (simp add: mset_set_set_mset_msubset) lemma mset_sorted_list_of_set[simp]: "mset (sorted_list_of_set A) = mset_set A" by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set) lemma sorted_sorted_list_of_multiset[simp]: "sorted (sorted_list_of_multiset (M :: 'a::linorder multiset))" by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_mset sorted_sort) lemma mset_take_subseteq: "mset (take n xs) \# mset xs" apply (induct xs arbitrary: n) apply simp by (case_tac n) simp_all lemma sorted_list_of_multiset_eq_Nil[simp]: "sorted_list_of_multiset M = [] \ M = {#}" by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_empty) subsection \Duplicate Removal\ (* TODO: use abbreviation? *) definition remdups_mset :: "'v multiset \ 'v multiset" where "remdups_mset S = mset_set (set_mset S)" lemma set_mset_remdups_mset[simp]: \set_mset (remdups_mset A) = set_mset A\ unfolding remdups_mset_def by auto lemma count_remdups_mset_eq_1: "a \# remdups_mset A \ count (remdups_mset A) a = 1" unfolding remdups_mset_def by (auto simp: count_eq_zero_iff intro: count_inI) lemma remdups_mset_empty[simp]: "remdups_mset {#} = {#}" unfolding remdups_mset_def by auto lemma remdups_mset_singleton[simp]: "remdups_mset {#a#} = {#a#}" unfolding remdups_mset_def by auto lemma remdups_mset_eq_empty[iff]: "remdups_mset D = {#} \ D = {#}" unfolding remdups_mset_def by blast lemma remdups_mset_singleton_sum[simp]: "remdups_mset (add_mset a A) = (if a \# A then remdups_mset A else add_mset a (remdups_mset A))" unfolding remdups_mset_def by (simp_all add: insert_absorb) lemma mset_remdups_remdups_mset[simp]: "mset (remdups D) = remdups_mset (mset D)" by (induction D) (auto simp add: ac_simps) declare mset_remdups_remdups_mset[symmetric, code] definition distinct_mset :: "'a multiset \ bool" where "distinct_mset S \ (\a. a \# S \ count S a = 1)" lemma distinct_mset_count_less_1: "distinct_mset S \ (\a. count S a \ 1)" using eq_iff nat_le_linear unfolding distinct_mset_def by fastforce lemma distinct_mset_empty[simp]: "distinct_mset {#}" unfolding distinct_mset_def by auto lemma distinct_mset_singleton: "distinct_mset {#a#}" unfolding distinct_mset_def by auto lemma distinct_mset_union: assumes dist: "distinct_mset (A + B)" shows "distinct_mset A" unfolding distinct_mset_count_less_1 proof (rule allI) fix a have \count A a \ count (A + B) a\ by auto moreover have \count (A + B) a \ 1\ using dist unfolding distinct_mset_count_less_1 by auto ultimately show \count A a \ 1\ by simp qed lemma distinct_mset_minus[simp]: "distinct_mset A \ distinct_mset (A - B)" by (metis diff_subset_eq_self mset_subset_eq_exists_conv distinct_mset_union) lemma count_remdups_mset_If: \count (remdups_mset A) a = (if a \# A then 1 else 0)\ unfolding remdups_mset_def by auto lemma distinct_mset_rempdups_union_mset: assumes "distinct_mset A" and "distinct_mset B" shows "A \# B = remdups_mset (A + B)" using assms nat_le_linear unfolding remdups_mset_def by (force simp add: multiset_eq_iff max_def count_mset_set_if distinct_mset_def not_in_iff) lemma distinct_mset_add_mset[simp]: "distinct_mset (add_mset a L) \ a \# L \ distinct_mset L" unfolding distinct_mset_def apply (rule iffI) apply (auto split: if_split_asm; fail)[] by (auto simp: not_in_iff; fail) lemma distinct_mset_size_eq_card: "distinct_mset C \ size C = card (set_mset C)" by (induction C) auto lemma distinct_mset_add: "distinct_mset (L + L') \ distinct_mset L \ distinct_mset L' \ L \# L' = {#}" by (induction L arbitrary: L') auto lemma distinct_mset_set_mset_ident[simp]: "distinct_mset M \ mset_set (set_mset M) = M" by (induction M) auto lemma distinct_finite_set_mset_subseteq_iff[iff]: assumes "distinct_mset M" "finite N" shows "set_mset M \ N \ M \# mset_set N" by (metis assms distinct_mset_set_mset_ident finite_set_mset msubset_mset_set_iff) lemma distinct_mem_diff_mset: assumes dist: "distinct_mset M" and mem: "x \ set_mset (M - N)" shows "x \ set_mset N" proof - have "count M x = 1" using dist mem by (meson distinct_mset_def in_diffD) then show ?thesis using mem by (metis count_greater_eq_one_iff in_diff_count not_less) qed lemma distinct_set_mset_eq: assumes "distinct_mset M" "distinct_mset N" "set_mset M = set_mset N" shows "M = N" using assms distinct_mset_set_mset_ident by fastforce lemma distinct_mset_union_mset[simp]: \distinct_mset (D \# C) \ distinct_mset D \ distinct_mset C\ unfolding distinct_mset_count_less_1 by force lemma distinct_mset_inter_mset: "distinct_mset C \ distinct_mset (C \# D)" "distinct_mset D \ distinct_mset (C \# D)" by (simp_all add: multiset_inter_def, metis distinct_mset_minus multiset_inter_commute multiset_inter_def) lemma distinct_mset_remove1_All: "distinct_mset C \ remove1_mset L C = removeAll_mset L C" by (auto simp: multiset_eq_iff distinct_mset_count_less_1) lemma distinct_mset_size_2: "distinct_mset {#a, b#} \ a \ b" by auto lemma distinct_mset_filter: "distinct_mset M \ distinct_mset {# L \# M. P L#}" by (simp add: distinct_mset_def) lemma distinct_mset_mset_distinct[simp]: \distinct_mset (mset xs) = distinct xs\ by (induction xs) auto lemma distinct_image_mset_inj: \inj_on f (set_mset M) \ distinct_mset (image_mset f M) \ distinct_mset M\ by (induction M) (auto simp: inj_on_def) subsection \Repeat Operation\ lemma repeat_mset_compower: "repeat_mset n A = (((+) A) ^^ n) {#}" by (induction n) auto lemma repeat_mset_prod: "repeat_mset (m * n) A = (((+) (repeat_mset n A)) ^^ m) {#}" by (induction m) (auto simp: repeat_mset_distrib) subsection \Cartesian Product\ text \Definition of the cartesian products over multisets. The construction mimics of the cartesian product on sets and use the same theorem names (adding only the suffix \_mset\ to Sigma and Times). See file @{file \~~/src/HOL/Product_Type.thy\}\ definition Sigma_mset :: "'a multiset \ ('a \ 'b multiset) \ ('a \ 'b) multiset" where - "Sigma_mset A B \ \# {#{#(a, b). b \# B a#}. a \# A #}" + "Sigma_mset A B \ \\<^sub># {#{#(a, b). b \# B a#}. a \# A #}" abbreviation Times_mset :: "'a multiset \ 'b multiset \ ('a \ 'b) multiset" (infixr "\#" 80) where "Times_mset A B \ Sigma_mset A (\_. B)" hide_const (open) Times_mset text \Contrary to the set version @{term \SIGMA x:A. B\}, we use the non-ASCII symbol \\#\.\ syntax "_Sigma_mset" :: "[pttrn, 'a multiset, 'b multiset] => ('a * 'b) multiset" ("(3SIGMAMSET _\#_./ _)" [0, 0, 10] 10) translations "SIGMAMSET x\#A. B" == "CONST Sigma_mset A (\x. B)" text \Link between the multiset and the set cartesian product:\ lemma Times_mset_Times: "set_mset (A \# B) = set_mset A \ set_mset B" unfolding Sigma_mset_def by auto lemma Sigma_msetI [intro!]: "\a \# A; b \# B a\ \ (a, b) \# Sigma_mset A B" by (unfold Sigma_mset_def) auto lemma Sigma_msetE[elim!]: "\c \# Sigma_mset A B; \x y. \x \# A; y \# B x; c = (x, y)\ \ P\ \ P" by (unfold Sigma_mset_def) auto text \Elimination of @{term "(a, b) \# A \# B"} -- introduces no eigenvariables.\ lemma Sigma_msetD1: "(a, b) \# Sigma_mset A B \ a \# A" by blast lemma Sigma_msetD2: "(a, b) \# Sigma_mset A B \ b \# B a" by blast lemma Sigma_msetE2: "\(a, b) \# Sigma_mset A B; \a \# A; b \# B a\ \ P\ \ P" by blast lemma Sigma_mset_cong: "\A = B; \x. x \# B \ C x = D x\ \ (SIGMAMSET x \# A. C x) = (SIGMAMSET x \# B. D x)" by (metis (mono_tags, lifting) Sigma_mset_def image_mset_cong) -lemma count_sum_mset: "count (\# M) b = (\P \# M. count P b)" +lemma count_sum_mset: "count (\\<^sub># M) b = (\P \# M. count P b)" by (induction M) auto lemma Sigma_mset_plus_distrib1[simp]: "Sigma_mset (A + B) C = Sigma_mset A C + Sigma_mset B C" unfolding Sigma_mset_def by auto lemma Sigma_mset_plus_distrib2[simp]: "Sigma_mset A (\i. B i + C i) = Sigma_mset A B + Sigma_mset A C" unfolding Sigma_mset_def by (induction A) (auto simp: multiset_eq_iff) lemma Times_mset_single_left: "{#a#} \# B = image_mset (Pair a) B" unfolding Sigma_mset_def by auto lemma Times_mset_single_right: "A \# {#b#} = image_mset (\a. Pair a b) A" unfolding Sigma_mset_def by (induction A) auto lemma Times_mset_single_single[simp]: "{#a#} \# {#b#} = {#(a, b)#}" unfolding Sigma_mset_def by simp lemma count_image_mset_Pair: "count (image_mset (Pair a) B) (x, b) = (if x = a then count B b else 0)" by (induction B) auto lemma count_Sigma_mset: "count (Sigma_mset A B) (a, b) = count A a * count (B a) b" by (induction A) (auto simp: Sigma_mset_def count_image_mset_Pair) lemma Sigma_mset_empty1[simp]: "Sigma_mset {#} B = {#}" unfolding Sigma_mset_def by auto lemma Sigma_mset_empty2[simp]: "A \# {#} = {#}" by (auto simp: multiset_eq_iff count_Sigma_mset) lemma Sigma_mset_mono: assumes "A \# C" and "\x. x \# A \ B x \# D x" shows "Sigma_mset A B \# Sigma_mset C D" proof - have "count A a * count (B a) b \ count C a * count (D a) b" for a b using assms unfolding subseteq_mset_def by (metis count_inI eq_iff mult_eq_0_iff mult_le_mono) then show ?thesis by (auto simp: subseteq_mset_def count_Sigma_mset) qed lemma mem_Sigma_mset_iff[iff]: "((a,b) \# Sigma_mset A B) = (a \# A \ b \# B a)" by blast lemma mem_Times_mset_iff: "x \# A \# B \ fst x \# A \ snd x \# B" by (induct x) simp lemma Sigma_mset_empty_iff: "(SIGMAMSET i\#I. X i) = {#} \ (\i\#I. X i = {#})" by (auto simp: Sigma_mset_def) lemma Times_mset_subset_mset_cancel1: "x \# A \ (A \# B \# A \# C) = (B \# C)" by (auto simp: subseteq_mset_def count_Sigma_mset) lemma Times_mset_subset_mset_cancel2: "x \# C \ (A \# C \# B \# C) = (A \# B)" by (auto simp: subseteq_mset_def count_Sigma_mset) lemma Times_mset_eq_cancel2: "x \# C \ (A \# C = B \# C) = (A = B)" by (auto simp: multiset_eq_iff count_Sigma_mset dest!: in_countE) lemma split_paired_Ball_mset_Sigma_mset[simp]: "(\z\#Sigma_mset A B. P z) \ (\x\#A. \y\#B x. P (x, y))" by blast lemma split_paired_Bex_mset_Sigma_mset[simp]: "(\z\#Sigma_mset A B. P z) \ (\x\#A. \y\#B x. P (x, y))" by blast lemma sum_mset_if_eq_constant: "(\x\#M. if a = x then (f x) else 0) = (((+) (f a)) ^^ (count M a)) 0" by (induction M) (auto simp: ac_simps) lemma iterate_op_plus: "(((+) k) ^^ m) 0 = k * m" by (induction m) auto lemma untion_image_mset_Pair_distribute: - "\#{#image_mset (Pair x) (C x). x \# J - I#} = - \# {#image_mset (Pair x) (C x). x \# J#} - \#{#image_mset (Pair x) (C x). x \# I#}" + "\\<^sub>#{#image_mset (Pair x) (C x). x \# J - I#} = + \\<^sub># {#image_mset (Pair x) (C x). x \# J#} - \\<^sub>#{#image_mset (Pair x) (C x). x \# I#}" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant iterate_op_plus diff_mult_distrib2) lemma Sigma_mset_Un_distrib1: "Sigma_mset (I \# J) C = Sigma_mset I C \# Sigma_mset J C" by (auto simp: Sigma_mset_def sup_subset_mset_def untion_image_mset_Pair_distribute) lemma Sigma_mset_Un_distrib2: "(SIGMAMSET i\#I. A i \# B i) = Sigma_mset I A \# Sigma_mset I B" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant Sigma_mset_def diff_mult_distrib2 iterate_op_plus max_def not_in_iff) lemma Sigma_mset_Int_distrib1: "Sigma_mset (I \# J) C = Sigma_mset I C \# Sigma_mset J C" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant Sigma_mset_def iterate_op_plus min_def not_in_iff) lemma Sigma_mset_Int_distrib2: "(SIGMAMSET i\#I. A i \# B i) = Sigma_mset I A \# Sigma_mset I B" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant Sigma_mset_def iterate_op_plus min_def not_in_iff) lemma Sigma_mset_Diff_distrib1: "Sigma_mset (I - J) C = Sigma_mset I C - Sigma_mset J C" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib2) lemma Sigma_mset_Diff_distrib2: "(SIGMAMSET i\#I. A i - B i) = Sigma_mset I A - Sigma_mset I B" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib) -lemma Sigma_mset_Union: "Sigma_mset (\#X) B = (\# (image_mset (\A. Sigma_mset A B) X))" +lemma Sigma_mset_Union: "Sigma_mset (\\<^sub>#X) B = (\\<^sub># (image_mset (\A. Sigma_mset A B) X))" by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant Sigma_mset_def iterate_op_plus min_def not_in_iff sum_mset_distrib_left) lemma Times_mset_Un_distrib1: "(A \# B) \# C = A \# C \# B \# C" by (fact Sigma_mset_Un_distrib1) lemma Times_mset_Int_distrib1: "(A \# B) \# C = A \# C \# B \# C" by (fact Sigma_mset_Int_distrib1) lemma Times_mset_Diff_distrib1: "(A - B) \# C = A \# C - B \# C" by (fact Sigma_mset_Diff_distrib1) lemma Times_mset_empty[simp]: "A \# B = {#} \ A = {#} \ B = {#}" by (auto simp: Sigma_mset_empty_iff) lemma Times_insert_left: "A \# add_mset x B = A \# B + image_mset (\a. Pair a x) A" unfolding add_mset_add_single[of x B] Sigma_mset_plus_distrib2 by (simp add: Times_mset_single_right) lemma Times_insert_right: "add_mset a A \# B = A \# B + image_mset (Pair a) B" unfolding add_mset_add_single[of a A] Sigma_mset_plus_distrib1 by (simp add: Times_mset_single_left) lemma fst_image_mset_times_mset [simp]: "image_mset fst (A \# B) = (if B = {#} then {#} else repeat_mset (size B) A)" by (induct B) (auto simp: Times_mset_single_right ac_simps Times_insert_left) lemma snd_image_mset_times_mset [simp]: "image_mset snd (A \# B) = (if A = {#} then {#} else repeat_mset (size A) B)" by (induct B) (auto simp add: Times_mset_single_right Times_insert_left image_mset_const_eq) lemma product_swap_mset: "image_mset prod.swap (A \# B) = B \# A" by (induction A) (auto simp add: Times_mset_single_left Times_mset_single_right Times_insert_right Times_insert_left) context begin qualified definition product_mset :: "'a multiset \ 'b multiset \ ('a \ 'b) multiset" where [code_abbrev]: "product_mset A B = A \# B" lemma member_product_mset: "x \# product_mset A B \ x \# A \# B" by (simp add: Multiset_More.product_mset_def) end lemma count_Sigma_mset_abs_def: "count (Sigma_mset A B) = (\(a, b) \ count A a * count (B a) b)" by (auto simp: fun_eq_iff count_Sigma_mset) lemma Times_mset_image_mset1: "image_mset f A \# B = image_mset (\(a, b). (f a, b)) (A \# B)" by (induct B) (auto simp: Times_insert_left) lemma Times_mset_image_mset2: "A \# image_mset f B = image_mset (\(a, b). (a, f b)) (A \# B)" by (induct A) (auto simp: Times_insert_right) lemma sum_le_singleton: "A \ {x} \ sum f A = (if x \ A then f x else 0)" by (auto simp: subset_singleton_iff elim: finite_subset) lemma Times_mset_assoc: "(A \# B) \# C = image_mset (\(a, b, c). ((a, b), c)) (A \# B \# C)" by (auto simp: multiset_eq_iff count_Sigma_mset count_image_mset vimage_def Times_mset_Times Int_commute count_eq_zero_iff intro!: trans[OF _ sym[OF sum_le_singleton[of _ "(_, _, _)"]]] cong: sum.cong if_cong) subsection \Transfer Rules\ lemma plus_multiset_transfer[transfer_rule]: "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (+) (+)" by (unfold rel_fun_def rel_mset_def) (force dest: list_all2_appendI intro: exI[of _ "_ @ _"] conjI[rotated]) lemma minus_multiset_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique R" shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (-) (-)" proof (unfold rel_fun_def rel_mset_def, safe) fix xs ys xs' ys' assume [transfer_rule]: "list_all2 R xs ys" "list_all2 R xs' ys'" have "list_all2 R (fold remove1 xs' xs) (fold remove1 ys' ys)" by transfer_prover moreover have "mset (fold remove1 xs' xs) = mset xs - mset xs'" by (induct xs' arbitrary: xs) auto moreover have "mset (fold remove1 ys' ys) = mset ys - mset ys'" by (induct ys' arbitrary: ys) auto ultimately show "\xs'' ys''. mset xs'' = mset xs - mset xs' \ mset ys'' = mset ys - mset ys' \ list_all2 R xs'' ys''" by blast qed declare rel_mset_Zero[transfer_rule] lemma count_transfer[transfer_rule]: assumes "bi_unique R" shows "(rel_fun (rel_mset R) (rel_fun R (=))) count count" unfolding rel_fun_def rel_mset_def proof safe fix x y xs ys assume "list_all2 R xs ys" "R x y" then show "count (mset xs) x = count (mset ys) y" proof (induct xs ys rule: list.rel_induct) case (Cons x' xs y' ys) then show ?case using assms unfolding bi_unique_alt_def2 by (auto simp: rel_fun_def) qed simp qed lemma subseteq_multiset_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique R" "right_total R" shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (=))) (\M N. filter_mset (Domainp R) M \# filter_mset (Domainp R) N) (\#)" proof - have count_filter_mset_less: "(\a. count (filter_mset (Domainp R) M) a \ count (filter_mset (Domainp R) N) a) \ (\a \ {x. Domainp R x}. count M a \ count N a)" for M and N by auto show ?thesis unfolding subseteq_mset_def count_filter_mset_less by transfer_prover qed lemma sum_mset_transfer[transfer_rule]: "R 0 0 \ rel_fun R (rel_fun R R) (+) (+) \ (rel_fun (rel_mset R) R) sum_mset sum_mset" using sum_list_transfer[of R] unfolding rel_fun_def rel_mset_def by auto lemma Sigma_mset_transfer[transfer_rule]: "(rel_fun (rel_mset R) (rel_fun (rel_fun R (rel_mset S)) (rel_mset (rel_prod R S)))) Sigma_mset Sigma_mset" by (unfold Sigma_mset_def) transfer_prover subsection \Even More about Multisets\ subsubsection \Multisets and Functions\ lemma range_image_mset: assumes "set_mset Ds \ range f" shows "Ds \ range (image_mset f)" proof - have "\D. D \# Ds \ (\C. f C = D)" using assms by blast then obtain f_i where f_p: "\D. D \# Ds \ (f (f_i D) = D)" by metis define Cs where "Cs \ image_mset f_i Ds" from f_p Cs_def have "image_mset f Cs = Ds" by auto then show ?thesis by blast qed subsubsection \Multisets and Lists\ lemma length_sorted_list_of_multiset[simp]: "length (sorted_list_of_multiset A) = size A" by (metis mset_sorted_list_of_multiset size_mset) definition list_of_mset :: "'a multiset \ 'a list" where "list_of_mset m = (SOME l. m = mset l)" lemma list_of_mset_exi: "\l. m = mset l" using ex_mset by metis lemma mset_list_of_mset[simp]: "mset (list_of_mset m) = m" by (metis (mono_tags, lifting) ex_mset list_of_mset_def someI_ex) lemma length_list_of_mset[simp]: "length (list_of_mset A) = size A" unfolding list_of_mset_def by (metis (mono_tags) ex_mset size_mset someI_ex) lemma range_mset_map: assumes "set_mset Ds \ range f" shows "Ds \ range (\Cl. mset (map f Cl))" proof - have "Ds \ range (image_mset f)" by (simp add: assms range_image_mset) then obtain Cs where Cs_p: "image_mset f Cs = Ds" by auto define Cl where "Cl = list_of_mset Cs" then have "mset Cl = Cs" by auto then have "image_mset f (mset Cl) = Ds" using Cs_p by auto then have "mset (map f Cl) = Ds" by auto then show ?thesis by auto qed lemma list_of_mset_empty[iff]: "list_of_mset m = [] \ m = {#}" by (metis (mono_tags, lifting) ex_mset list_of_mset_def mset_zero_iff_right someI_ex) lemma in_mset_conv_nth: "(x \# mset xs) = (\i# LL" assumes "LL \ set Ci" shows "L \# sum_list Ci" using assms by (induction Ci) auto lemma in_mset_sum_list2: assumes "L \# sum_list Ci" obtains LL where "LL \ set Ci" "L \# LL" using assms by (induction Ci) auto (* TODO: Make [simp]. *) lemma in_mset_sum_list_iff: "a \# sum_list \ \ (\A \ set \. a \# A)" by (metis in_mset_sum_list in_mset_sum_list2) lemma subseteq_list_Union_mset: assumes "length Ci = n" assumes "length CAi = n" assumes "\i# CAi ! i " - shows "\# (mset Ci) \# \# (mset CAi)" + shows "\\<^sub># (mset Ci) \# \\<^sub># (mset CAi)" using assms proof (induction n arbitrary: Ci CAi) case 0 then show ?case by auto next case (Suc n) from Suc have "\i# tl CAi ! i" by (simp add: nth_tl) - hence "\#(mset (tl Ci)) \# \#(mset (tl CAi))" using Suc by auto + hence "\\<^sub>#(mset (tl Ci)) \# \\<^sub>#(mset (tl CAi))" using Suc by auto moreover have "hd Ci \# hd CAi" using Suc by (metis hd_conv_nth length_greater_0_conv zero_less_Suc) ultimately - show "\#(mset Ci) \# \#(mset CAi)" + show "\\<^sub>#(mset Ci) \# \\<^sub>#(mset CAi)" using Suc by (cases Ci; cases CAi) (auto intro: subset_mset.add_mono) qed subsubsection \More on Multisets and Functions\ lemma subseteq_mset_size_eql: "X \# Y \ size Y = size X \ X = Y" using mset_subset_size subset_mset_def by fastforce lemma image_mset_of_subset_list: assumes "image_mset \ C' = mset lC" shows "\qC'. map \ qC' = lC \ mset qC' = C'" using assms apply (induction lC arbitrary: C') subgoal by simp subgoal by (fastforce dest!: msed_map_invR intro: exI[of _ \_ # _\]) done lemma image_mset_of_subset: assumes "A \# image_mset \ C'" shows "\A'. image_mset \ A' = A \ A' \# C'" proof - define C where "C = image_mset \ C'" define lA where "lA = list_of_mset A" define lD where "lD = list_of_mset (C-A)" define lC where "lC = lA @ lD" have "mset lC = C" using C_def assms unfolding lD_def lC_def lA_def by auto then have "\qC'. map \ qC' = lC \ mset qC' = C'" using assms image_mset_of_subset_list unfolding C_def by metis then obtain qC' where qC'_p: "map \ qC' = lC \ mset qC' = C'" by auto let ?lA' = "take (length lA) qC'" have m: "map \ ?lA' = lA" using qC'_p lC_def by (metis append_eq_conv_conj take_map) let ?A' = "mset ?lA'" have "image_mset \ ?A' = A" using m using lA_def by (metis (full_types) ex_mset list_of_mset_def mset_map someI_ex) moreover have "?A' \# C'" using qC'_p unfolding lA_def using mset_take_subseteq by blast ultimately show ?thesis by blast qed lemma all_the_same: "\x \# X. x = y \ card (set_mset X) \ Suc 0" by (metis card.empty card.insert card_mono finite.intros(1) finite_insert le_SucI singletonI subsetI) lemma Melem_subseteq_Union_mset[simp]: assumes "x \# T" - shows "x \# \#T" + shows "x \# \\<^sub>#T" using assms sum_mset.remove by force lemma Melem_subset_eq_sum_list[simp]: assumes "x \# mset T" shows "x \# sum_list T" using assms by (metis mset_subset_eq_add_left sum_mset.remove sum_mset_sum_list) lemma less_subset_eq_Union_mset[simp]: assumes "i < length CAi" - shows "CAi ! i \# \#(mset CAi)" + shows "CAi ! i \# \\<^sub>#(mset CAi)" proof - from assms have "CAi ! i \# mset CAi" by auto then show ?thesis by auto qed lemma less_subset_eq_sum_list[simp]: assumes "i < length CAi" shows "CAi ! i \# sum_list CAi" proof - from assms have "CAi ! i \# mset CAi" by auto then show ?thesis by auto qed subsubsection \More on Multiset Order\ lemma less_multiset_doubletons: assumes "y < t \ y < s" "x < t \ x < s" shows "{#y, x#} < {#t, s#}" unfolding less_multiset\<^sub>D\<^sub>M proof (intro exI) let ?X = "{#t, s#}" let ?Y = "{#y, x#}" show "?X \ {#} \ ?X \# {#t, s#} \ {#y, x#} = {#t, s#} - ?X + ?Y \ (\k. k \# ?Y \ (\a. a \# ?X \ k < a))" using add_eq_conv_diff assms by auto qed end diff --git a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy --- a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy +++ b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy @@ -1,1412 +1,1412 @@ (* Title: First-Order Ordered Resolution Calculus with Selection Author: Anders Schlichtkrull , 2016, 2017 Author: Jasmin Blanchette , 2014, 2017 Author: Dmitriy Traytel , 2014 Author: Sophie Tourret , 2020 Maintainer: Anders Schlichtkrull *) section \First-Order Ordered Resolution Calculus with Selection\ theory FO_Ordered_Resolution imports Abstract_Substitution Ordered_Ground_Resolution Standard_Redundancy begin text \ This material is based on Section 4.3 (``A Simple Resolution Prover for First-Order Clauses'') of Bachmair and Ganzinger's chapter. Specifically, it formalizes the ordered resolution calculus for first-order standard clauses presented in Figure 4 and its related lemmas and theorems, including soundness and Lemma 4.12 (the lifting lemma). The following corresponds to pages 41--42 of Section 4.3, until Figure 5 and its explanation. \ locale FO_resolution = mgu subst_atm id_subst comp_subst atm_of_atms renamings_apart mgu for subst_atm :: "'a :: wellorder \ 's \ 'a" and id_subst :: "'s" and comp_subst :: "'s \ 's \ 's" and renamings_apart :: "'a literal multiset list \ 's list" and atm_of_atms :: "'a list \ 'a" and mgu :: "'a set set \ 's option" + fixes less_atm :: "'a \ 'a \ bool" assumes less_atm_stable: "less_atm A B \ less_atm (A \a \) (B \a \)" and less_atm_ground: "is_ground_atm A \ is_ground_atm B \ less_atm A B \ A < B" begin subsection \Library\ lemma Bex_cartesian_product: "(\xy \ A \ B. P xy) \ (\x \ A. \y \ B. P (x, y))" by simp lemma eql_map_neg_lit_eql_atm: assumes "map (\L. L \l \) (map Neg As') = map Neg As" shows "As' \al \ = As" using assms by (induction As' arbitrary: As) auto lemma instance_list: assumes "negs (mset As) = SDA' \ \" shows "\As'. negs (mset As') = SDA' \ As' \al \ = As" proof - from assms have negL: "\L \# SDA'. is_neg L" using Melem_subst_cls subst_lit_in_negs_is_neg by metis from assms have "{#L \l \. L \# SDA'#} = mset (map Neg As)" using subst_cls_def by auto then have "\NAs'. map (\L. L \l \) NAs' = map Neg As \ mset NAs' = SDA'" using image_mset_of_subset_list[of "\L. L \l \" SDA' "map Neg As"] by auto then obtain As' where As'_p: "map (\L. L \l \) (map Neg As') = map Neg As \ mset (map Neg As') = SDA'" by (metis (no_types, lifting) Neg_atm_of_iff negL ex_map_conv set_mset_mset) have "negs (mset As') = SDA'" using As'_p by auto moreover have "map (\L. L \l \) (map Neg As') = map Neg As" using As'_p by auto then have "As' \al \ = As" using eql_map_neg_lit_eql_atm by auto ultimately show ?thesis by blast qed lemma map2_add_mset_map: assumes "length AAs' = n" and "length As' = n" shows "map2 add_mset (As' \al \) (AAs' \aml \) = map2 add_mset As' AAs' \aml \" using assms proof (induction n arbitrary: AAs' As') case (Suc n) then have "map2 add_mset (tl (As' \al \)) (tl (AAs' \aml \)) = map2 add_mset (tl As') (tl AAs') \aml \" by simp moreover have Succ: "length (As' \al \) = Suc n" "length (AAs' \aml \) = Suc n" using Suc(3) Suc(2) by auto then have "length (tl (As' \al \)) = n" "length (tl (AAs' \aml \)) = n" by auto then have "length (map2 add_mset (tl (As' \al \)) (tl (AAs' \aml \))) = n" "length (map2 add_mset (tl As') (tl AAs') \aml \) = n" using Suc(2,3) by auto ultimately have "\i < n. tl (map2 add_mset ( (As' \al \)) ((AAs' \aml \))) ! i = tl (map2 add_mset (As') (AAs') \aml \) ! i" using Suc(2,3) Succ by (simp add: map2_tl map_tl subst_atm_mset_list_def del: subst_atm_list_tl) moreover have nn: "length (map2 add_mset ((As' \al \)) ((AAs' \aml \))) = Suc n" "length (map2 add_mset (As') (AAs') \aml \) = Suc n" using Succ Suc by auto ultimately have "\i. i < Suc n \ i > 0 \ map2 add_mset (As' \al \) (AAs' \aml \) ! i = (map2 add_mset As' AAs' \aml \) ! i" by (auto simp: subst_atm_mset_list_def gr0_conv_Suc subst_atm_mset_def) moreover have "add_mset (hd As' \a \) (hd AAs' \am \) = add_mset (hd As') (hd AAs') \am \" unfolding subst_atm_mset_def by auto then have "(map2 add_mset (As' \al \) (AAs' \aml \)) ! 0 = (map2 add_mset (As') (AAs') \aml \) ! 0" using Suc by (simp add: Succ(2) subst_atm_mset_def) ultimately have "\i < Suc n. (map2 add_mset (As' \al \) (AAs' \aml \)) ! i = (map2 add_mset (As') (AAs') \aml \) ! i" using Suc by auto then show ?case using nn list_eq_iff_nth_eq by metis qed auto context fixes S :: "'a clause \ 'a clause" begin subsection \Calculus\ text \ The following corresponds to Figure 4. \ definition maximal_wrt :: "'a \ 'a literal multiset \ bool" where "maximal_wrt A C \ (\B \ atms_of C. \ less_atm A B)" definition strictly_maximal_wrt :: "'a \ 'a literal multiset \ bool" where "strictly_maximal_wrt A C \ \B \ atms_of C. A \ B \ \ less_atm A B" lemma strictly_maximal_wrt_maximal_wrt: "strictly_maximal_wrt A C \ maximal_wrt A C" unfolding maximal_wrt_def strictly_maximal_wrt_def by auto lemma maximal_wrt_subst: "maximal_wrt (A \a \) (C \ \) \ maximal_wrt A C" unfolding maximal_wrt_def using in_atms_of_subst less_atm_stable by blast lemma strictly_maximal_wrt_subst: "strictly_maximal_wrt (A \a \) (C \ \) \ strictly_maximal_wrt A C" unfolding strictly_maximal_wrt_def using in_atms_of_subst less_atm_stable by blast inductive eligible :: "'s \ 'a list \ 'a clause \ bool" where eligible: "S DA = negs (mset As) \ S DA = {#} \ length As = 1 \ maximal_wrt (As ! 0 \a \) (DA \ \) \ eligible \ As DA" inductive ord_resolve :: "'a clause list \ 'a clause \ 'a multiset list \ 'a list \ 's \ 'a clause \ bool" where ord_resolve: "length CAs = n \ length Cs = n \ length AAs = n \ length As = n \ n \ 0 \ (\i < n. CAs ! i = Cs ! i + poss (AAs ! i)) \ (\i < n. AAs ! i \ {#}) \ Some \ = mgu (set_mset ` set (map2 add_mset As AAs)) \ eligible \ As (D + negs (mset As)) \ (\i < n. strictly_maximal_wrt (As ! i \a \) (Cs ! i \ \)) \ (\i < n. S (CAs ! i) = {#}) \ - ord_resolve CAs (D + negs (mset As)) AAs As \ ((\# (mset Cs) + D) \ \)" + ord_resolve CAs (D + negs (mset As)) AAs As \ ((\\<^sub># (mset Cs) + D) \ \)" inductive ord_resolve_rename :: "'a clause list \ 'a clause \ 'a multiset list \ 'a list \ 's \ 'a clause \ bool" where ord_resolve_rename: "length CAs = n \ length AAs = n \ length As = n \ (\i < n. poss (AAs ! i) \# CAs ! i) \ negs (mset As) \# DA \ \ = hd (renamings_apart (DA # CAs)) \ \s = tl (renamings_apart (DA # CAs)) \ ord_resolve (CAs \\cl \s) (DA \ \) (AAs \\aml \s) (As \al \) \ E \ ord_resolve_rename CAs DA AAs As \ E" lemma ord_resolve_empty_main_prem: "\ ord_resolve Cs {#} AAs As \ E" by (simp add: ord_resolve.simps) lemma ord_resolve_rename_empty_main_prem: "\ ord_resolve_rename Cs {#} AAs As \ E" by (simp add: ord_resolve_empty_main_prem ord_resolve_rename.simps) subsection \Soundness\ text \ Soundness is not discussed in the chapter, but it is an important property. \ lemma ord_resolve_ground_inst_sound: assumes res_e: "ord_resolve CAs DA AAs As \ E" and cc_inst_true: "I \m mset CAs \cm \ \cm \" and d_inst_true: "I \ DA \ \ \ \" and ground_subst_\: "is_ground_subst \" shows "I \ E \ \" using res_e proof (cases rule: ord_resolve.cases) case (ord_resolve n Cs D) note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10) and len = this(1) have len: "length CAs = length As" using as_len cas_len by auto have "is_ground_subst (\ \ \)" using ground_subst_\ by (rule is_ground_comp_subst) then have cc_true: "I \m mset CAs \cm \ \cm \" and d_true: "I \ DA \ \ \ \" using cc_inst_true d_inst_true by auto from mgu have unif: "\i < n. \A\#AAs ! i. A \a \ = As ! i \a \" using mgu_unifier as_len aas_len by blast show "I \ E \ \" proof (cases "\A \ set As. A \a \ \a \ \ I") case True then have "\ I \ negs (mset As) \ \ \ \" unfolding true_cls_def[of I] by auto then have "I \ D \ \ \ \" using d_true da by auto then show ?thesis unfolding e by auto next case False then obtain i where a_in_aa: "i < length CAs" and a_false: "(As ! i) \a \ \a \ \ I" using da len by (metis in_set_conv_nth) define C where "C \ Cs ! i" define BB where "BB \ AAs ! i" - have c_cf': "C \# \# (mset CAs)" + have c_cf': "C \# \\<^sub># (mset CAs)" unfolding C_def using a_in_aa cas cas_len by (metis less_subset_eq_Union_mset mset_subset_eq_add_left subset_mset.order.trans) have c_in_cc: "C + poss BB \# mset CAs" using C_def BB_def a_in_aa cas_len in_set_conv_nth cas by fastforce { fix B assume "B \# BB" then have "B \a \ = (As ! i) \a \" using unif a_in_aa cas_len unfolding BB_def by auto } then have "\ I \ poss BB \ \ \ \" using a_false by (auto simp: true_cls_def) moreover have "I \ (C + poss BB) \ \ \ \" using c_in_cc cc_true true_cls_mset_true_cls[of I "mset CAs \cm \ \cm \"] by force ultimately have "I \ C \ \ \ \" by simp then show ?thesis unfolding e subst_cls_union using c_cf' C_def a_in_aa cas_len cs_len by (metis (no_types, lifting) mset_subset_eq_add_left nth_mem_mset set_mset_mono sum_mset.remove true_cls_mono subst_cls_mono) qed qed text \ The previous lemma is not only used to prove soundness, but also the following lemma which is used to prove Lemma 4.10. \ lemma ord_resolve_rename_ground_inst_sound: assumes "ord_resolve_rename CAs DA AAs As \ E" and "\s = tl (renamings_apart (DA # CAs))" and "\ = hd (renamings_apart (DA # CAs))" and "I \m (mset (CAs \\cl \s)) \cm \ \cm \" and "I \ DA \ \ \ \ \ \" and "is_ground_subst \" shows "I \ E \ \" using assms by (cases rule: ord_resolve_rename.cases) (fast intro: ord_resolve_ground_inst_sound) text \ Here follows the soundness theorem for the resolution rule. \ theorem ord_resolve_sound: assumes res_e: "ord_resolve CAs DA AAs As \ E" and cc_d_true: "\\. is_ground_subst \ \ I \m (mset CAs + {#DA#}) \cm \" and ground_subst_\: "is_ground_subst \" shows "I \ E \ \" proof (use res_e in \cases rule: ord_resolve.cases\) case (ord_resolve n Cs D) note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10) have ground_subst_\_\: "is_ground_subst (\ \ \)" using ground_subst_\ by (rule is_ground_comp_subst) have cas_true: "I \m mset CAs \cm \ \cm \" using cc_d_true ground_subst_\_\ by fastforce have da_true: "I \ DA \ \ \ \" using cc_d_true ground_subst_\_\ by fastforce show "I \ E \ \" using ord_resolve_ground_inst_sound[OF res_e cas_true da_true] ground_subst_\ by auto qed lemma subst_sound: assumes "\\. is_ground_subst \ \ I \ C \ \" and "is_ground_subst \" shows "I \ C \ \ \ \" using assms is_ground_comp_subst subst_cls_comp_subst by metis lemma subst_sound_scl: assumes len: "length P = length CAs" and true_cas: "\\. is_ground_subst \ \ I \m mset CAs \cm \" and ground_subst_\: "is_ground_subst \" shows "I \m mset (CAs \\cl P) \cm \" proof - from true_cas have "\CA. CA\# mset CAs \ (\\. is_ground_subst \ \ I \ CA \ \)" unfolding true_cls_mset_def by force then have "\i < length CAs. \\. is_ground_subst \ \ (I \ CAs ! i \ \)" using in_set_conv_nth by auto then have true_cp: "\i < length CAs. \\. is_ground_subst \ \ I \ CAs ! i \ P ! i \ \" using subst_sound len by auto { fix CA assume "CA \# mset (CAs \\cl P)" then obtain i where i_x: "i < length (CAs \\cl P)" "CA = (CAs \\cl P) ! i" by (metis in_mset_conv_nth) then have "\\. is_ground_subst \ \ I \ CA \ \" using true_cp unfolding subst_cls_lists_def by (simp add: len) } then show ?thesis using assms unfolding true_cls_mset_def by auto qed text \ Here follows the soundness theorem for the resolution rule with renaming. \ lemma ord_resolve_rename_sound: assumes res_e: "ord_resolve_rename CAs DA AAs As \ E" and cc_d_true: "\\. is_ground_subst \ \ I \m ((mset CAs) + {#DA#}) \cm \" and ground_subst_\: "is_ground_subst \" shows "I \ E \ \" using res_e proof (cases rule: ord_resolve_rename.cases) case (ord_resolve_rename n \ \s) note \s = this(7) and res = this(8) have len: "length \s = length CAs" using \s renamings_apart_length by auto have "\\. is_ground_subst \ \ I \m (mset (CAs \\cl \s) + {#DA \ \#}) \cm \" using subst_sound_scl[OF len, of I] subst_sound cc_d_true by auto then show "I \ E \ \" using ground_subst_\ ord_resolve_sound[OF res] by simp qed subsection \Other Basic Properties\ lemma ord_resolve_unique: assumes "ord_resolve CAs DA AAs As \ E" and "ord_resolve CAs DA AAs As \' E'" shows "\ = \' \ E = E'" using assms proof (cases rule: ord_resolve.cases[case_product ord_resolve.cases], intro conjI) case (ord_resolve_ord_resolve CAs n Cs AAs As \'' DA CAs' n' Cs' AAs' As' \''' DA') note res = this(1-17) and res' = this(18-34) show \: "\ = \'" using res(3-5,14) res'(3-5,14) by (metis option.inject) have "Cs = Cs'" using res(1,3,7,8,12) res'(1,3,7,8,12) by (metis add_right_imp_eq nth_equalityI) moreover have "DA = DA'" using res(2,4) res'(2,4) by fastforce ultimately show "E = E'" using res(5,6) res'(5,6) \ by blast qed lemma ord_resolve_rename_unique: assumes "ord_resolve_rename CAs DA AAs As \ E" and "ord_resolve_rename CAs DA AAs As \' E'" shows "\ = \' \ E = E'" using assms unfolding ord_resolve_rename.simps using ord_resolve_unique by meson lemma ord_resolve_max_side_prems: "ord_resolve CAs DA AAs As \ E \ length CAs \ size DA" by (auto elim!: ord_resolve.cases) lemma ord_resolve_rename_max_side_prems: "ord_resolve_rename CAs DA AAs As \ E \ length CAs \ size DA" by (elim ord_resolve_rename.cases, drule ord_resolve_max_side_prems, simp add: renamings_apart_length) subsection \Inference System\ definition ord_FO_\ :: "'a inference set" where "ord_FO_\ = {Infer (mset CAs) DA E | CAs DA AAs As \ E. ord_resolve_rename CAs DA AAs As \ E}" interpretation ord_FO_resolution: inference_system ord_FO_\ . lemma finite_ord_FO_resolution_inferences_between: assumes fin_cc: "finite CC" shows "finite (ord_FO_resolution.inferences_between CC C)" proof - let ?CCC = "CC \ {C}" define all_AA where "all_AA = (\D \ ?CCC. atms_of D)" define max_ary where "max_ary = Max (size ` ?CCC)" define CAS where "CAS = {CAs. CAs \ lists ?CCC \ length CAs \ max_ary}" define AS where "AS = {As. As \ lists all_AA \ length As \ max_ary}" define AAS where "AAS = {AAs. AAs \ lists (mset ` AS) \ length AAs \ max_ary}" note defs = all_AA_def max_ary_def CAS_def AS_def AAS_def let ?infer_of = "\CAs DA AAs As. Infer (mset CAs) DA (THE E. \\. ord_resolve_rename CAs DA AAs As \ E)" let ?Z = "{\ | CAs DA AAs As \ E \. \ = Infer (mset CAs) DA E \ ord_resolve_rename CAs DA AAs As \ E \ infer_from ?CCC \ \ C \# prems_of \}" let ?Y = "{Infer (mset CAs) DA E | CAs DA AAs As \ E. ord_resolve_rename CAs DA AAs As \ E \ set CAs \ {DA} \ ?CCC}" let ?X = "{?infer_of CAs DA AAs As | CAs DA AAs As. CAs \ CAS \ DA \ ?CCC \ AAs \ AAS \ As \ AS}" let ?W = "CAS \ ?CCC \ AAS \ AS" have fin_w: "finite ?W" unfolding defs using fin_cc by (simp add: finite_lists_length_le lists_eq_set) have "?Z \ ?Y" by (force simp: infer_from_def) also have "\ \ ?X" proof - { fix CAs DA AAs As \ E assume res_e: "ord_resolve_rename CAs DA AAs As \ E" and da_in: "DA \ ?CCC" and cas_sub: "set CAs \ ?CCC" have "E = (THE E. \\. ord_resolve_rename CAs DA AAs As \ E) \ CAs \ CAS \ AAs \ AAS \ As \ AS" (is "?e \ ?cas \ ?aas \ ?as") proof (intro conjI) show ?e using res_e ord_resolve_rename_unique by (blast intro: the_equality[symmetric]) next show ?cas unfolding CAS_def max_ary_def using cas_sub ord_resolve_rename_max_side_prems[OF res_e] da_in fin_cc by (auto simp add: Max_ge_iff) next show ?aas using res_e proof (cases rule: ord_resolve_rename.cases) case (ord_resolve_rename n \ \s) note len_cas = this(1) and len_aas = this(2) and len_as = this(3) and aas_sub = this(4) and as_sub = this(5) and res_e' = this(8) show ?thesis unfolding AAS_def proof (clarify, intro conjI) show "AAs \ lists (mset ` AS)" unfolding AS_def image_def proof clarsimp fix AA assume "AA \ set AAs" then obtain i where i_lt: "i < n" and aa: "AA = AAs ! i" by (metis in_set_conv_nth len_aas) have casi_in: "CAs ! i \ ?CCC" using i_lt len_cas cas_sub nth_mem by blast have pos_aa_sub: "poss AA \# CAs ! i" using aa aas_sub i_lt by blast then have "set_mset AA \ atms_of (CAs ! i)" by (metis atms_of_poss lits_subseteq_imp_atms_subseteq set_mset_mono) also have aa_sub: "\ \ all_AA" unfolding all_AA_def using casi_in by force finally have aa_sub: "set_mset AA \ all_AA" . have "size AA = size (poss AA)" by simp also have "\ \ size (CAs ! i)" by (rule size_mset_mono[OF pos_aa_sub]) also have "\ \ max_ary" unfolding max_ary_def using fin_cc casi_in by auto finally have sz_aa: "size AA \ max_ary" . let ?As' = "sorted_list_of_multiset AA" have "?As' \ lists all_AA" using aa_sub by auto moreover have "length ?As' \ max_ary" using sz_aa by simp moreover have "AA = mset ?As'" by simp ultimately show "\xa. xa \ lists all_AA \ length xa \ max_ary \ AA = mset xa" by blast qed next have "length AAs = length As" unfolding len_aas len_as .. also have "\ \ size DA" using as_sub size_mset_mono by fastforce also have "\ \ max_ary" unfolding max_ary_def using fin_cc da_in by auto finally show "length AAs \ max_ary" . qed qed next show ?as unfolding AS_def proof (clarify, intro conjI) have "set As \ atms_of DA" using res_e[simplified ord_resolve_rename.simps] by (metis atms_of_negs lits_subseteq_imp_atms_subseteq set_mset_mono set_mset_mset) also have "\ \ all_AA" unfolding all_AA_def using da_in by blast finally show "As \ lists all_AA" unfolding lists_eq_set by simp next have "length As \ size DA" using res_e[simplified ord_resolve_rename.simps] ord_resolve_rename_max_side_prems[OF res_e] by auto also have "size DA \ max_ary" unfolding max_ary_def using fin_cc da_in by auto finally show "length As \ max_ary" . qed qed } then show ?thesis by simp fast qed also have "\ \ (\(CAs, DA, AAs, As). ?infer_of CAs DA AAs As) ` ?W" unfolding image_def Bex_cartesian_product by fast finally show ?thesis unfolding inference_system.inferences_between_def ord_FO_\_def mem_Collect_eq by (fast intro: rev_finite_subset[OF finite_imageI[OF fin_w]]) qed lemma ord_FO_resolution_inferences_between_empty_empty: "ord_FO_resolution.inferences_between {} {#} = {}" unfolding ord_FO_resolution.inferences_between_def inference_system.inferences_between_def infer_from_def ord_FO_\_def using ord_resolve_rename_empty_main_prem by auto subsection \Lifting\ text \ The following corresponds to the passage between Lemmas 4.11 and 4.12. \ context fixes M :: "'a clause set" assumes select: "selection S" begin interpretation selection by (rule select) definition S_M :: "'a literal multiset \ 'a literal multiset" where "S_M C = (if C \ grounding_of_clss M then (SOME C'. \D \. D \ M \ C = D \ \ \ C' = S D \ \ \ is_ground_subst \) else S C)" lemma S_M_grounding_of_clss: assumes "C \ grounding_of_clss M" obtains D \ where "D \ M \ C = D \ \ \ S_M C = S D \ \ \ is_ground_subst \" proof (atomize_elim, unfold S_M_def eqTrueI[OF assms] if_True, rule someI_ex) from assms show "\C' D \. D \ M \ C = D \ \ \ C' = S D \ \ \ is_ground_subst \" by (auto simp: grounding_of_clss_def grounding_of_cls_def) qed lemma S_M_not_grounding_of_clss: "C \ grounding_of_clss M \ S_M C = S C" unfolding S_M_def by simp lemma S_M_selects_subseteq: "S_M C \# C" by (metis S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_subseteq subst_cls_mono_mset) lemma S_M_selects_neg_lits: "L \# S_M C \ is_neg L" by (metis Melem_subst_cls S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_neg_lits subst_lit_is_neg) end end text \ The following corresponds to Lemma 4.12: \ lemma ground_resolvent_subset: assumes gr_cas: "is_ground_cls_list CAs" and gr_da: "is_ground_cls DA" and res_e: "ord_resolve S CAs DA AAs As \ E" - shows "E \# \# (mset CAs) + DA" + shows "E \# \\<^sub># (mset CAs) + DA" using res_e proof (cases rule: ord_resolve.cases) case (ord_resolve n Cs D) note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10) - then have cs_sub_cas: "\# (mset Cs) \# \# (mset CAs)" + then have cs_sub_cas: "\\<^sub># (mset Cs) \# \\<^sub># (mset CAs)" using subseteq_list_Union_mset cas_len cs_len by force - then have cs_sub_cas: "\# (mset Cs) \# \# (mset CAs)" + then have cs_sub_cas: "\\<^sub># (mset Cs) \# \\<^sub># (mset CAs)" using subseteq_list_Union_mset cas_len cs_len by force then have gr_cs: "is_ground_cls_list Cs" using gr_cas by simp have d_sub_da: "D \# DA" by (simp add: da) then have gr_d: "is_ground_cls D" using gr_da is_ground_cls_mono by auto - have "is_ground_cls (\# (mset Cs) + D)" + have "is_ground_cls (\\<^sub># (mset Cs) + D)" using gr_cs gr_d by auto - with e have "E = \# (mset Cs) + D" + with e have "E = \\<^sub># (mset Cs) + D" by auto then show ?thesis using cs_sub_cas d_sub_da by (auto simp: subset_mset.add_mono) qed lemma ord_resolve_obtain_clauses: assumes res_e: "ord_resolve (S_M S M) CAs DA AAs As \ E" and select: "selection S" and grounding: "{DA} \ set CAs \ grounding_of_clss M" and n: "length CAs = n" and d: "DA = D + negs (mset As)" and c: "(\i < n. CAs ! i = Cs ! i + poss (AAs ! i))" "length Cs = n" "length AAs = n" obtains DA0 \0 CAs0 \s0 As0 AAs0 D0 Cs0 where "length CAs0 = n" "length \s0 = n" "DA0 \ M" "DA0 \ \0 = DA" "S DA0 \ \0 = S_M S M DA" "\CA0 \ set CAs0. CA0 \ M" "CAs0 \\cl \s0 = CAs" "map S CAs0 \\cl \s0 = map (S_M S M) CAs" "is_ground_subst \0" "is_ground_subst_list \s0" "As0 \al \0 = As" "AAs0 \\aml \s0 = AAs" "length As0 = n" "D0 \ \0 = D" "DA0 = D0 + (negs (mset As0))" "S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0" "length Cs0 = n" "Cs0 \\cl \s0 = Cs" "\i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" "length AAs0 = n" using res_e proof (cases rule: ord_resolve.cases) case (ord_resolve n_twin Cs_twins D_twin) note da = this(1) and e = this(2) and cas = this(8) and mgu = this(10) and eligible = this(11) from ord_resolve have "n_twin = n" "D_twin = D" using n d by auto moreover have "Cs_twins = Cs" using c cas n calculation(1) \length Cs_twins = n_twin\ by (auto simp add: nth_equalityI) ultimately have nz: "n \ 0" and cs_len: "length Cs = n" and aas_len: "length AAs = n" and as_len: "length As = n" and da: "DA = D + negs (mset As)" and eligible: "eligible (S_M S M) \ As (D + negs (mset As))" and cas: "\in \ 0\ \length CAs = n\ \length Cs = n\ \length AAs = n\ \length As = n\ interpret S: selection S by (rule select) \ \Obtain FO side premises\ have "\CA \ set CAs. \CA0 \c0. CA0 \ M \ CA0 \ \c0 = CA \ S CA0 \ \c0 = S_M S M CA \ is_ground_subst \c0" using grounding S_M_grounding_of_clss select by (metis (no_types) le_supE subset_iff) then have "\i < n. \CA0 \c0. CA0 \ M \ CA0 \ \c0 = (CAs ! i) \ S CA0 \ \c0 = S_M S M (CAs ! i) \ is_ground_subst \c0" using n by force then obtain \s0f CAs0f where f_p: "\i < n. CAs0f i \ M" "\i < n. (CAs0f i) \ (\s0f i) = (CAs ! i)" "\i < n. S (CAs0f i) \ (\s0f i) = S_M S M (CAs ! i)" "\i < n. is_ground_subst (\s0f i)" using n by (metis (no_types)) define \s0 where "\s0 = map \s0f [0 ..s0 = n" "length CAs0 = n" unfolding \s0_def CAs0_def by auto note n = \length \s0 = n\ \length CAs0 = n\ n \ \The properties we need of the FO side premises\ have CAs0_in_M: "\CA0 \ set CAs0. CA0 \ M" unfolding CAs0_def using f_p(1) by auto have CAs0_to_CAs: "CAs0 \\cl \s0 = CAs" unfolding CAs0_def \s0_def using f_p(2) by (auto simp: n intro: nth_equalityI) have SCAs0_to_SMCAs: "(map S CAs0) \\cl \s0 = map (S_M S M) CAs" unfolding CAs0_def \s0_def using f_p(3) n by (force intro: nth_equalityI) have sub_ground: "\\c0 \ set \s0. is_ground_subst \c0" unfolding \s0_def using f_p n by force then have "is_ground_subst_list \s0" using n unfolding is_ground_subst_list_def by auto \ \Split side premises CAs0 into Cs0 and AAs0\ obtain AAs0 Cs0 where AAs0_Cs0_p: "AAs0 \\aml \s0 = AAs" "length Cs0 = n" "Cs0 \\cl \s0 = Cs" "\i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" "length AAs0 = n" proof - have "\i < n. \AA0. AA0 \am \s0 ! i = AAs ! i \ poss AA0 \# CAs0 ! i" proof (rule, rule) fix i assume "i < n" have "CAs0 ! i \ \s0 ! i = CAs ! i" using \i < n\ \CAs0 \\cl \s0 = CAs\ n by force moreover have "poss (AAs ! i) \# CAs !i" using \i < n\ cas by auto ultimately obtain poss_AA0 where nn: "poss_AA0 \ \s0 ! i = poss (AAs ! i) \ poss_AA0 \# CAs0 ! i" using cas image_mset_of_subset unfolding subst_cls_def by metis then have l: "\L \# poss_AA0. is_pos L" unfolding subst_cls_def by (metis Melem_subst_cls imageE literal.disc(1) literal.map_disc_iff set_image_mset subst_cls_def subst_lit_def) define AA0 where "AA0 = image_mset atm_of poss_AA0" have na: "poss AA0 = poss_AA0" using l unfolding AA0_def by auto then have "AA0 \am \s0 ! i = AAs ! i" using nn by (metis (mono_tags) literal.inject(1) multiset.inj_map_strong subst_cls_poss) moreover have "poss AA0 \# CAs0 ! i" using na nn by auto ultimately show "\AA0. AA0 \am \s0 ! i = AAs ! i \ poss AA0 \# CAs0 ! i" by blast qed then obtain AAs0f where AAs0f_p: "\i < n. AAs0f i \am \s0 ! i = AAs ! i \ (poss (AAs0f i)) \# CAs0 ! i" by metis define AAs0 where "AAs0 = map AAs0f [0 ..length AAs0 = n\ from AAs0_def have "\i < n. AAs0 ! i \am \s0 ! i = AAs ! i" using AAs0f_p by auto then have AAs0_AAs: "AAs0 \\aml \s0 = AAs" using n by (auto intro: nth_equalityI) from AAs0_def have AAs0_in_CAs0: "\i < n. poss (AAs0 ! i) \# CAs0 ! i" using AAs0f_p by auto define Cs0 where "Cs0 = map2 (-) CAs0 (map poss AAs0)" have "length Cs0 = n" using Cs0_def n by auto note n = n \length Cs0 = n\ have "\i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" using AAs0_in_CAs0 Cs0_def n by auto then have "Cs0 \\cl \s0 = Cs" using \CAs0 \\cl \s0 = CAs\ AAs0_AAs cas n by (auto intro: nth_equalityI) show ?thesis using that \AAs0 \\aml \s0 = AAs\ \Cs0 \\cl \s0 = Cs\ \\i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)\ \length AAs0 = n\ \length Cs0 = n\ by blast qed \ \Obtain FO main premise\ have "\DA0 \0. DA0 \ M \ DA = DA0 \ \0 \ S DA0 \ \0 = S_M S M DA \ is_ground_subst \0" using grounding S_M_grounding_of_clss select by (metis le_supE singletonI subsetCE) then obtain DA0 \0 where DA0_\0_p: "DA0 \ M \ DA = DA0 \ \0 \ S DA0 \ \0 = S_M S M DA \ is_ground_subst \0" by auto \ \The properties we need of the FO main premise\ have DA0_in_M: "DA0 \ M" using DA0_\0_p by auto have DA0_to_DA: "DA0 \ \0 = DA" using DA0_\0_p by auto have SDA0_to_SMDA: "S DA0 \ \0 = S_M S M DA" using DA0_\0_p by auto have "is_ground_subst \0" using DA0_\0_p by auto \ \Split main premise DA0 into D0 and As0\ obtain D0 As0 where D0As0_p: "As0 \al \0 = As" "length As0 = n" "D0 \ \0 = D" "DA0 = D0 + (negs (mset As0))" "S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0" proof - { assume a: "S_M S M (D + negs (mset As)) = {#} \ length As = (Suc 0) \ maximal_wrt (As ! 0 \a \) ((D + negs (mset As)) \ \)" then have as: "mset As = {#As ! 0#}" by (auto intro: nth_equalityI) then have "negs (mset As) = {#Neg (As ! 0)#}" by (simp add: \mset As = {#As ! 0#}\) then have "DA = D + {#Neg (As ! 0)#}" using da by auto then obtain L where "L \# DA0 \ L \l \0 = Neg (As ! 0)" using DA0_to_DA by (metis Melem_subst_cls mset_subset_eq_add_right single_subset_iff) then have "Neg (atm_of L) \# DA0 \ Neg (atm_of L) \l \0 = Neg (As ! 0)" by (metis Neg_atm_of_iff literal.sel(2) subst_lit_is_pos) then have "[atm_of L] \al \0 = As \ negs (mset [atm_of L]) \# DA0" using as subst_lit_def by auto then have "\As0. As0 \al \0 = As \ negs (mset As0) \# DA0 \ (S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0)" using a by blast } moreover { assume "S_M S M (D + negs (mset As)) = negs (mset As)" then have "negs (mset As) = S DA0 \ \0" using da \S DA0 \ \0 = S_M S M DA\ by auto then have "\As0. negs (mset As0) = S DA0 \ As0 \al \0 = As" using instance_list[of As "S DA0" \0] S.S_selects_neg_lits by auto then have "\As0. As0 \al \0 = As \ negs (mset As0) \# DA0 \ (S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0)" using S.S_selects_subseteq by auto } ultimately have "\As0. As0 \al \0 = As \ (negs (mset As0)) \# DA0 \ (S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0)" using eligible unfolding eligible.simps by auto then obtain As0 where As0_p: "As0 \al \0 = As \ negs (mset As0) \# DA0 \ (S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0)" by blast then have "length As0 = n" using as_len by auto note n = n this have "As0 \al \0 = As" using As0_p by auto define D0 where "D0 = DA0 - negs (mset As0)" then have "DA0 = D0 + negs (mset As0)" using As0_p by auto then have "D0 \ \0 = D" using DA0_to_DA da As0_p by auto have "S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0" using As0_p by blast then show ?thesis using that \As0 \al \0 = As\ \D0 \ \0= D\ \DA0 = D0 + (negs (mset As0))\ \length As0 = n\ by metis qed show ?thesis using that[OF n(2,1) DA0_in_M DA0_to_DA SDA0_to_SMDA CAs0_in_M CAs0_to_CAs SCAs0_to_SMCAs \is_ground_subst \0\ \is_ground_subst_list \s0\ \As0 \al \0 = As\ \AAs0 \\aml \s0 = AAs\ \length As0 = n\ \D0 \ \0 = D\ \DA0 = D0 + (negs (mset As0))\ \S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0\ \length Cs0 = n\ \Cs0 \\cl \s0 = Cs\ \\i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)\ \length AAs0 = n\] by auto qed lemma ord_resolve_rename_lifting: assumes sel_stable: "\\ C. is_renaming \ \ S (C \ \) = S C \ \" and res_e: "ord_resolve (S_M S M) CAs DA AAs As \ E" and select: "selection S" and grounding: "{DA} \ set CAs \ grounding_of_clss M" obtains \s \ \2 CAs0 DA0 AAs0 As0 E0 \ where "is_ground_subst \" "is_ground_subst_list \s" "is_ground_subst \2" "ord_resolve_rename S CAs0 DA0 AAs0 As0 \ E0" "CAs0 \\cl \s = CAs" "DA0 \ \ = DA" "E0 \ \2 = E" "{DA0} \ set CAs0 \ M" "length CAs0 = length CAs" "length \s = length CAs" using res_e proof (cases rule: ord_resolve.cases) case (ord_resolve n Cs D) note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and aas_len = this(5) and as_len = this(6) and nz = this(7) and cas = this(8) and aas_not_empt = this(9) and mgu = this(10) and eligible = this(11) and str_max = this(12) and sel_empt = this(13) have sel_ren_list_inv: "\\s Cs. length \s = length Cs \ is_renaming_list \s \ map S (Cs \\cl \s) = map S Cs \\cl \s" using sel_stable unfolding is_renaming_list_def by (auto intro: nth_equalityI) note n = \n \ 0\ \length CAs = n\ \length Cs = n\ \length AAs = n\ \length As = n\ interpret S: selection S by (rule select) obtain DA0 \0 CAs0 \s0 As0 AAs0 D0 Cs0 where as0: "length CAs0 = n" "length \s0 = n" "DA0 \ M" "DA0 \ \0 = DA" "S DA0 \ \0 = S_M S M DA" "\CA0 \ set CAs0. CA0 \ M" "CAs0 \\cl \s0 = CAs" "map S CAs0 \\cl \s0 = map (S_M S M) CAs" "is_ground_subst \0" "is_ground_subst_list \s0" "As0 \al \0 = As" "AAs0 \\aml \s0 = AAs" "length As0 = n" "D0 \ \0 = D" "DA0 = D0 + (negs (mset As0))" "S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0) = S DA0" "length Cs0 = n" "Cs0 \\cl \s0 = Cs" "\i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" "length AAs0 = n" using ord_resolve_obtain_clauses[of S M CAs DA, OF res_e select grounding n(2) \DA = D + negs (mset As)\ \\i \length Cs = n\ \length AAs = n\, of thesis] by blast note n = \length CAs0 = n\ \length \s0 = n\ \length As0 = n\ \length AAs0 = n\ \length Cs0 = n\ n have "length (renamings_apart (DA0 # CAs0)) = Suc n" using n renamings_apart_length by auto note n = this n define \ where "\ = hd (renamings_apart (DA0 # CAs0))" define \s where "\s = tl (renamings_apart (DA0 # CAs0))" define DA0' where "DA0' = DA0 \ \" define D0' where "D0' = D0 \ \" define As0' where "As0' = As0 \al \" define CAs0' where "CAs0' = CAs0 \\cl \s" define Cs0' where "Cs0' = Cs0 \\cl \s" define AAs0' where "AAs0' = AAs0 \\aml \s" define \0' where "\0' = inv_renaming \ \ \0" define \s0' where "\s0' = map inv_renaming \s \s \s0" have renames_DA0: "is_renaming \" using renamings_apart_length renamings_apart_renaming unfolding \_def by (metis length_greater_0_conv list.exhaust_sel list.set_intros(1) list.simps(3)) have renames_CAs0: "is_renaming_list \s" using renamings_apart_length renamings_apart_renaming unfolding \s_def by (metis is_renaming_list_def length_greater_0_conv list.set_sel(2) list.simps(3)) have "length \s = n" unfolding \s_def using n by auto note n = n \length \s = n\ have "length As0' = n" unfolding As0'_def using n by auto have "length CAs0' = n" using as0(1) n unfolding CAs0'_def by auto have "length Cs0' = n" unfolding Cs0'_def using n by auto have "length AAs0' = n" unfolding AAs0'_def using n by auto have "length \s0' = n" using as0(2) n unfolding \s0'_def by auto note n = \length CAs0' = n\ \length \s0' = n\ \length As0' = n\ \length AAs0' = n\ \length Cs0' = n\ n have DA0'_DA: "DA0' \ \0' = DA" using as0(4) unfolding \0'_def DA0'_def using renames_DA0 by simp have D0'_D: "D0' \ \0' = D" using as0(14) unfolding \0'_def D0'_def using renames_DA0 by simp have As0'_As: "As0' \al \0' = As" using as0(11) unfolding \0'_def As0'_def using renames_DA0 by auto have "S DA0' \ \0' = S_M S M DA" using as0(5) unfolding \0'_def DA0'_def using renames_DA0 sel_stable by auto have CAs0'_CAs: "CAs0' \\cl \s0' = CAs" using as0(7) unfolding CAs0'_def \s0'_def using renames_CAs0 n by auto have Cs0'_Cs: "Cs0' \\cl \s0' = Cs" using as0(18) unfolding Cs0'_def \s0'_def using renames_CAs0 n by auto have AAs0'_AAs: "AAs0' \\aml \s0' = AAs" using as0(12) unfolding \s0'_def AAs0'_def using renames_CAs0 using n by auto have "map S CAs0' \\cl \s0' = map (S_M S M) CAs" unfolding CAs0'_def \s0'_def using as0(8) n renames_CAs0 sel_ren_list_inv by auto have DA0'_split: "DA0' = D0' + negs (mset As0')" using as0(15) DA0'_def D0'_def As0'_def by auto then have D0'_subset_DA0': "D0' \# DA0'" by auto from DA0'_split have negs_As0'_subset_DA0': "negs (mset As0') \# DA0'" by auto have CAs0'_split: "\ii# CAs0' ! i" by auto from CAs0'_split have poss_AAs0'_subset_CAs0': "\i# CAs0' ! i" by auto then have AAs0'_in_atms_of_CAs0': "\i < n. \A\#AAs0' ! i. A \ atms_of (CAs0' ! i)" by (auto simp add: atm_iff_pos_or_neg_lit) have as0': "S_M S M (D + negs (mset As)) \ {#} \ negs (mset As0') = S DA0'" proof - assume a: "S_M S M (D + negs (mset As)) \ {#}" then have "negs (mset As0) \ \ = S DA0 \ \" using as0(16) unfolding \_def by metis then show "negs (mset As0') = S DA0'" using As0'_def DA0'_def using sel_stable[of \ DA0] renames_DA0 by auto qed have vd: "var_disjoint (DA0' # CAs0')" unfolding DA0'_def CAs0'_def using renamings_apart_var_disjoint unfolding \_def \s_def by (metis length_greater_0_conv list.exhaust_sel n(6) substitution.subst_cls_lists_Cons substitution_axioms zero_less_Suc) \ \Introduce ground substitution\ from vd DA0'_DA CAs0'_CAs have "\\. \i < Suc n. \S. S \# (DA0' # CAs0') ! i \ S \ (\0'#\s0') ! i = S \ \" unfolding var_disjoint_def using n by auto then obtain \ where \_p: "\i < Suc n. \S. S \# (DA0' # CAs0') ! i \ S \ (\0'#\s0') ! i = S \ \" by auto have \_p_lit: "\i < Suc n. \L. L \# (DA0' # CAs0') ! i \ L \l (\0'#\s0') ! i = L \l \" proof (rule, rule, rule, rule) fix i :: "nat" and L :: "'a literal" assume a: "i < Suc n" "L \# (DA0' # CAs0') ! i" then have "\S. S \# (DA0' # CAs0') ! i \ S \ (\0' # \s0') ! i = S \ \" using \_p by auto then have "{# L #} \ (\0' # \s0') ! i = {# L #} \ \" using a by (meson single_subset_iff) then show "L \l (\0' # \s0') ! i = L \l \" by auto qed have \_p_atm: "\i < Suc n. \A. A \ atms_of ((DA0' # CAs0') ! i) \ A \a (\0'#\s0') ! i = A \a \" proof (rule, rule, rule, rule) fix i :: "nat" and A :: "'a" assume a: "i < Suc n" "A \ atms_of ((DA0' # CAs0') ! i)" then obtain L where L_p: "atm_of L = A \ L \# (DA0' # CAs0') ! i" unfolding atms_of_def by auto then have "L \l (\0'#\s0') ! i = L \l \" using \_p_lit a by auto then show "A \a (\0' # \s0') ! i = A \a \" using L_p unfolding subst_lit_def by (cases L) auto qed have DA0'_DA: "DA0' \ \ = DA" using DA0'_DA \_p by auto have "D0' \ \ = D" using \_p D0'_D n D0'_subset_DA0' by auto have "As0' \al \ = As" proof (rule nth_equalityI) show "length (As0' \al \) = length As" using n by auto next fix i show "ial \) \ (As0' \al \) ! i = As ! i" proof - assume a: "i < length (As0' \al \)" have A_eq: "\A. A \ atms_of DA0' \ A \a \0' = A \a \" using \_p_atm n by force have "As0' ! i \ atms_of DA0'" using negs_As0'_subset_DA0' unfolding atms_of_def using a n by force then have "As0' ! i \a \0' = As0' ! i \a \" using A_eq by simp then show "(As0' \al \) ! i = As ! i" using As0'_As \length As0' = n\ a by auto qed qed interpret selection by (rule select) have "S DA0' \ \ = S_M S M DA" using \S DA0' \ \0' = S_M S M DA\ \_p S.S_selects_subseteq by auto from \_p have \_p_CAs0': "\i < n. (CAs0' ! i) \ (\s0' ! i) = (CAs0'! i) \ \" using n by auto then have "CAs0' \\cl \s0' = CAs0' \cl \" using n by (auto intro: nth_equalityI) then have CAs0'_\_fo_CAs: "CAs0' \cl \ = CAs" using CAs0'_CAs \_p n by auto from \_p have "\i < n. S (CAs0' ! i) \ \s0' ! i = S (CAs0' ! i) \ \" using S.S_selects_subseteq n by auto then have "map S CAs0' \\cl \s0' = map S CAs0' \cl \" using n by (auto intro: nth_equalityI) then have SCAs0'_\_fo_SMCAs: "map S CAs0' \cl \ = map (S_M S M) CAs" using \map S CAs0' \\cl \s0' = map (S_M S M) CAs\ by auto have "Cs0' \cl \ = Cs" proof (rule nth_equalityI) show "length (Cs0' \cl \) = length Cs" using n by auto next fix i show "icl \) \ (Cs0' \cl \) ! i = Cs ! i" proof - assume "i < length (Cs0' \cl \)" then have a: "i < n" using n by force have "(Cs0' \\cl \s0') ! i = Cs ! i" using Cs0'_Cs a n by force moreover have \_p_CAs0': "\S. S \# CAs0' ! i \ S \ \s0' ! i = S \ \" using \_p a by force have "Cs0' ! i \ \s0' ! i = (Cs0' \cl \) ! i" using \_p_CAs0' \\i# CAs0' ! i\ a n by force then have "(Cs0' \\cl \s0') ! i = (Cs0' \cl \) ! i " using a n by force ultimately show "(Cs0' \cl \) ! i = Cs ! i" by auto qed qed have AAs0'_AAs: "AAs0' \aml \ = AAs" proof (rule nth_equalityI) show "length (AAs0' \aml \) = length AAs" using n by auto next fix i show "iaml \) \ (AAs0' \aml \) ! i = AAs ! i" proof - assume a: "i < length (AAs0' \aml \)" then have "i < n" using n by force then have "\A. A \ atms_of ((DA0' # CAs0') ! Suc i) \ A \a (\0' # \s0') ! Suc i = A \a \" using \_p_atm n by force then have A_eq: "\A. A \ atms_of (CAs0' ! i) \ A \a \s0' ! i = A \a \" by auto have AAs_CAs0': "\A \# AAs0' ! i. A \ atms_of (CAs0' ! i)" using AAs0'_in_atms_of_CAs0' unfolding atms_of_def using a n by force then have "AAs0' ! i \am \s0' ! i = AAs0' ! i \am \" unfolding subst_atm_mset_def using A_eq unfolding subst_atm_mset_def by auto then show "(AAs0' \aml \) ! i = AAs ! i" using AAs0'_AAs \length AAs0' = n\ \length \s0' = n\ a by auto qed qed \ \Obtain MGU and substitution\ obtain \ \ where \\: "Some \ = mgu (set_mset ` set (map2 add_mset As0' AAs0'))" "\ \ \ = \ \ \" proof - have uu: "is_unifiers \ (set_mset ` set (map2 add_mset (As0' \al \) (AAs0' \aml \)))" using mgu mgu_sound is_mgu_def unfolding \AAs0' \aml \ = AAs\ using \As0' \al \ = As\ by auto have \\uni: "is_unifiers (\ \ \) (set_mset ` set (map2 add_mset As0' AAs0'))" proof - have "set_mset ` set (map2 add_mset As0' AAs0' \aml \) = set_mset ` set (map2 add_mset As0' AAs0') \ass \" unfolding subst_atmss_def subst_atm_mset_list_def using subst_atm_mset_def subst_atms_def by (simp add: image_image subst_atm_mset_def subst_atms_def) then have "is_unifiers \ (set_mset ` set (map2 add_mset As0' AAs0') \ass \)" using uu by (auto simp: n map2_add_mset_map) then show ?thesis using is_unifiers_comp by auto qed then obtain \ where \_p: "Some \ = mgu (set_mset ` set (map2 add_mset As0' AAs0'))" using mgu_complete by (metis (mono_tags, hide_lams) List.finite_set finite_imageI finite_set_mset image_iff) moreover then obtain \ where \_p: "\ \ \ = \ \ \" by (metis (mono_tags, hide_lams) finite_set \\uni finite_imageI finite_set_mset image_iff mgu_sound set_mset_mset substitution_ops.is_mgu_def) (* should be simpler *) ultimately show thesis using that by auto qed \ \Lifting eligibility\ have eligible0': "eligible S \ As0' (D0' + negs (mset As0'))" proof - have "S_M S M (D + negs (mset As)) = negs (mset As) \ S_M S M (D + negs (mset As)) = {#} \ length As = 1 \ maximal_wrt (As ! 0 \a \) ((D + negs (mset As)) \ \)" using eligible unfolding eligible.simps by auto then show ?thesis proof assume "S_M S M (D + negs (mset As)) = negs (mset As)" then have "S_M S M (D + negs (mset As)) \ {#}" using n by force then have "S (D0' + negs (mset As0')) = negs (mset As0')" using as0' DA0'_split by auto then show ?thesis unfolding eligible.simps[simplified] by auto next assume asm: "S_M S M (D + negs (mset As)) = {#} \ length As = 1 \ maximal_wrt (As ! 0 \a \) ((D + negs (mset As)) \ \)" then have "S (D0' + negs (mset As0')) = {#}" using \D0' \ \ = D\[symmetric] \As0' \al \ = As\[symmetric] \S (DA0') \ \ = S_M S M (DA)\ da DA0'_split subst_cls_empty_iff by metis moreover from asm have l: "length As0' = 1" using \As0' \al \ = As\ by auto moreover from asm have "maximal_wrt (As0' ! 0 \a (\ \ \)) ((D0' + negs (mset As0')) \ (\ \ \))" using \As0' \al \ = As\ \D0' \ \ = D\ using l \\ by auto then have "maximal_wrt (As0' ! 0 \a \ \a \) ((D0' + negs (mset As0')) \ \ \ \)" by auto then have "maximal_wrt (As0' ! 0 \a \) ((D0' + negs (mset As0')) \ \)" using maximal_wrt_subst by blast ultimately show ?thesis unfolding eligible.simps[simplified] by auto qed qed \ \Lifting maximality\ have maximality: "\i < n. strictly_maximal_wrt (As0' ! i \a \) (Cs0' ! i \ \)" (* Reformulate in list notation? *) proof - from str_max have "\i < n. strictly_maximal_wrt ((As0' \al \) ! i \a \) ((Cs0' \cl \) ! i \ \)" using \As0' \al \ = As\ \Cs0' \cl \ = Cs\ by simp then have "\i < n. strictly_maximal_wrt (As0' ! i \a (\ \ \)) (Cs0' ! i \ (\ \ \))" using n \\ by simp then have "\i < n. strictly_maximal_wrt (As0' ! i \a \ \a \) (Cs0' ! i \ \ \ \)" by auto then show "\i < n. strictly_maximal_wrt (As0' ! i \a \) (Cs0' ! i \ \)" using strictly_maximal_wrt_subst \\ by blast qed \ \Lifting nothing being selected\ have nothing_selected: "\i < n. S (CAs0' ! i) = {#}" proof - have "\i < n. (map S CAs0' \cl \) ! i = map (S_M S M) CAs ! i" by (simp add: \map S CAs0' \cl \ = map (S_M S M) CAs\) then have "\i < n. S (CAs0' ! i) \ \ = S_M S M (CAs ! i)" using n by auto then have "\i < n. S (CAs0' ! i) \ \ = {#}" using sel_empt \\i < n. S (CAs0' ! i) \ \ = S_M S M (CAs ! i)\ by auto then show "\i < n. S (CAs0' ! i) = {#}" using subst_cls_empty_iff by blast qed \ \Lifting AAs0's non-emptiness\ have "\i < n. AAs0' ! i \ {#}" using n aas_not_empt \AAs0' \aml \ = AAs\ by auto \ \Resolve the lifted clauses\ define E0' where - "E0' = ((\# (mset Cs0')) + D0') \ \" + "E0' = ((\\<^sub># (mset Cs0')) + D0') \ \" have res_e0': "ord_resolve S CAs0' DA0' AAs0' As0' \ E0'" using ord_resolve.intros[of CAs0' n Cs0' AAs0' As0' \ S D0', OF _ _ _ _ _ _ \\i < n. AAs0' ! i \ {#}\ \\(1) eligible0' \\i < n. strictly_maximal_wrt (As0' ! i \a \) (Cs0' ! i \ \)\ \\i < n. S (CAs0' ! i) = {#}\] unfolding E0'_def using DA0'_split n \\i by blast \ \Prove resolvent instantiates to ground resolvent\ have e0'\e: "E0' \ \ = E" proof - - have "E0' \ \ = ((\# (mset Cs0')) + D0') \ (\ \ \)" + have "E0' \ \ = ((\\<^sub># (mset Cs0')) + D0') \ (\ \ \)" unfolding E0'_def by auto - also have "\ = (\# (mset Cs0') + D0') \ (\ \ \)" + also have "\ = (\\<^sub># (mset Cs0') + D0') \ (\ \ \)" using \\ by auto - also have "\ = (\# (mset Cs) + D) \ \" + also have "\ = (\\<^sub># (mset Cs) + D) \ \" using \Cs0' \cl \ = Cs\ \D0' \ \ = D\ by auto also have "\ = E" using e by auto finally show e0'\e: "E0' \ \ = E" . qed \ \Replace @{term \} with a true ground substitution\ obtain \2 where ground_\2: "is_ground_subst \2" "E0' \ \2 = E" proof - have "is_ground_cls_list CAs" "is_ground_cls DA" using grounding grounding_ground unfolding is_ground_cls_list_def by auto then have "is_ground_cls E" using res_e ground_resolvent_subset by (force intro: is_ground_cls_mono) then show thesis using that e0'\e make_ground_subst by auto qed have \length CAs0 = length CAs\ using n by simp have \length \s0 = length CAs\ using n by simp \ \Wrap up the proof\ have "ord_resolve S (CAs0 \\cl \s) (DA0 \ \) (AAs0 \\aml \s) (As0 \al \) \ E0'" using res_e0' As0'_def \_def AAs0'_def \s_def DA0'_def \_def CAs0'_def \s_def by simp moreover have "\i# CAs0 ! i" using as0(19) by auto moreover have "negs (mset As0) \# DA0" using local.as0(15) by auto ultimately have "ord_resolve_rename S CAs0 DA0 AAs0 As0 \ E0'" using ord_resolve_rename[of CAs0 n AAs0 As0 DA0 \ \s S \ E0'] \_def \s_def n by auto then show thesis using that[of \0 \s0 \2 CAs0 DA0] \is_ground_subst \0\ \is_ground_subst_list \s0\ \is_ground_subst \2\ \CAs0 \\cl \s0 = CAs\ \DA0 \ \0 = DA\ \E0' \ \2 = E\ \DA0 \ M\ \\CA \ set CAs0. CA \ M\ \length CAs0 = length CAs\ \length \s0 = length CAs\ by blast qed lemma ground_ord_resolve_ground: assumes select: "selection S" and CAs_p: "ground_resolution_with_selection.ord_resolve S CAs DA AAs As E" and ground_cas: "is_ground_cls_list CAs" and ground_da: "is_ground_cls DA" shows "is_ground_cls E" proof - have a1: "atms_of E \ (\CA \ set CAs. atms_of CA) \ atms_of DA" using ground_resolution_with_selection.ord_resolve_atms_of_concl_subset[OF _ CAs_p] ground_resolution_with_selection.intro[OF select] by blast { fix L :: "'a literal" assume "L \# E" then have "atm_of L \ atms_of E" by (meson atm_of_lit_in_atms_of) then have "is_ground_atm (atm_of L)" using a1 ground_cas ground_da is_ground_cls_imp_is_ground_atm is_ground_cls_list_def by auto } then show ?thesis unfolding is_ground_cls_def is_ground_lit_def by simp qed lemma ground_ord_resolve_imp_ord_resolve: assumes ground_da: \is_ground_cls DA\ and ground_cas: \is_ground_cls_list CAs\ and gr: "ground_resolution_with_selection S_G" and gr_res: \ground_resolution_with_selection.ord_resolve S_G CAs DA AAs As E\ shows \\\. ord_resolve S_G CAs DA AAs As \ E\ proof (cases rule: ground_resolution_with_selection.ord_resolve.cases[OF gr gr_res]) case (1 CAs n Cs AAs As D) note cas = this(1) and da = this(2) and aas = this(3) and as = this(4) and e = this(5) and cas_len = this(6) and cs_len = this(7) and aas_len = this(8) and as_len = this(9) and nz = this(10) and casi = this(11) and aas_not_empt = this(12) and as_aas = this(13) and eligibility = this(14) and str_max = this(15) and sel_empt = this(16) have len_aas_len_as: "length AAs = length As" using aas_len as_len by auto from as_aas have "\i < n. \A \# add_mset (As ! i) (AAs ! i). A = As ! i" by simp then have "\i < n. card (set_mset (add_mset (As ! i) (AAs ! i))) \ Suc 0" using all_the_same by metis then have "\i < length AAs. card (set_mset (add_mset (As ! i) (AAs ! i))) \ Suc 0" using aas_len by auto then have "\AA \ set (map2 add_mset As AAs). card (set_mset AA) \ Suc 0" using set_map2_ex[of AAs As add_mset, OF len_aas_len_as] by auto then have "is_unifiers id_subst (set_mset ` set (map2 add_mset As AAs))" unfolding is_unifiers_def is_unifier_def by auto moreover have "finite (set_mset ` set (map2 add_mset As AAs))" by auto moreover have "\AA \ set_mset ` set (map2 add_mset As AAs). finite AA" by auto ultimately obtain \ where \_p: "Some \ = mgu (set_mset ` set (map2 add_mset As AAs))" using mgu_complete by metis have ground_elig: "ground_resolution_with_selection.eligible S_G As (D + negs (mset As))" using eligibility by simp have ground_cs: "\i < n. is_ground_cls (Cs ! i)" using cas cas_len cs_len casi ground_cas nth_mem unfolding is_ground_cls_list_def by force have ground_set_as: "is_ground_atms (set As)" using da ground_da by (metis atms_of_negs is_ground_cls_is_ground_atms_atms_of is_ground_cls_union set_mset_mset) then have ground_mset_as: "is_ground_atm_mset (mset As)" unfolding is_ground_atm_mset_def is_ground_atms_def by auto have ground_as: "is_ground_atm_list As" using ground_set_as is_ground_atm_list_def is_ground_atms_def by auto have ground_d: "is_ground_cls D" using ground_da da by simp from as_len nz have atms: "atms_of D \ set As \ {}" "finite (atms_of D \ set As)" by auto then have "Max (atms_of D \ set As) \ atms_of D \ set As" using Max_in by metis then have is_ground_Max: "is_ground_atm (Max (atms_of D \ set As))" using ground_d ground_mset_as is_ground_cls_imp_is_ground_atm unfolding is_ground_atm_mset_def by auto have "maximal_wrt (Max (atms_of D \ set As)) (D + negs (mset As))" unfolding maximal_wrt_def by clarsimp (metis atms Max_less_iff UnCI ground_d ground_set_as infinite_growing is_ground_Max is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground) moreover have "Max (atms_of D \ set As) \a \ = Max (atms_of D \ set As)" and "D \ \ + negs (mset As \am \) = D + negs (mset As)" using ground_elig is_ground_Max ground_mset_as ground_d by auto ultimately have fo_elig: "eligible S_G \ As (D + negs (mset As))" using ground_elig unfolding ground_resolution_with_selection.eligible.simps[OF gr] ground_resolution_with_selection.maximal_wrt_def[OF gr] eligible.simps by auto have "\i < n. strictly_maximal_wrt (As ! i) (Cs ! i)" using str_max[unfolded ground_resolution_with_selection.strictly_maximal_wrt_def[OF gr]] ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground unfolding strictly_maximal_wrt_def by clarsimp (fastforce simp: is_ground_cls_as_atms)+ then have ll: "\i < n. strictly_maximal_wrt (As ! i \a \) (Cs ! i \ \)" by (simp add: ground_as ground_cs as_len) have ground_e: "is_ground_cls E" using ground_d ground_cs cs_len unfolding e is_ground_cls_def by simp (metis in_mset_sum_list2 in_set_conv_nth) show ?thesis using cas da aas as e ground_e ord_resolve.intros[OF cas_len cs_len aas_len as_len nz casi aas_not_empt \_p fo_elig ll sel_empt] by auto qed end end diff --git a/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy b/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy --- a/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy +++ b/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy @@ -1,143 +1,143 @@ (* Title: Herbrand Interpretation Author: Jasmin Blanchette , 2014, 2017 Author: Dmitriy Traytel , 2014 Maintainer: Jasmin Blanchette *) section \Herbrand Intepretation\ theory Herbrand_Interpretation imports Clausal_Logic begin text \ The material formalized here corresponds roughly to Sections 2.2 (``Herbrand Interpretations'') of Bachmair and Ganzinger, excluding the formula and term syntax. A Herbrand interpretation is a set of ground atoms that are to be considered true. \ type_synonym 'a interp = "'a set" definition true_lit :: "'a interp \ 'a literal \ bool" (infix "\l" 50) where "I \l L \ (if is_pos L then (\P. P) else Not) (atm_of L \ I)" lemma true_lit_simps[simp]: "I \l Pos A \ A \ I" "I \l Neg A \ A \ I" unfolding true_lit_def by auto lemma true_lit_iff[iff]: "I \l L \ (\A. L = Pos A \ A \ I \ L = Neg A \ A \ I)" by (cases L) simp+ definition true_cls :: "'a interp \ 'a clause \ bool" (infix "\" 50) where "I \ C \ (\L \# C. I \l L)" lemma true_cls_empty[iff]: "\ I \ {#}" unfolding true_cls_def by simp lemma true_cls_singleton[iff]: "I \ {#L#} \ I \l L" unfolding true_cls_def by simp lemma true_cls_add_mset[iff]: "I \ add_mset C D \ I \l C \ I \ D" unfolding true_cls_def by auto lemma true_cls_union[iff]: "I \ C + D \ I \ C \ I \ D" unfolding true_cls_def by auto lemma true_cls_mono: "set_mset C \ set_mset D \ I \ C \ I \ D" unfolding true_cls_def subset_eq by metis lemma assumes "I \ J" shows false_to_true_imp_ex_pos: "\ I \ C \ J \ C \ \A \ J. Pos A \# C" and true_to_false_imp_ex_neg: "I \ C \ \ J \ C \ \A \ J. Neg A \# C" using assms unfolding subset_iff true_cls_def by (metis literal.collapse true_lit_simps)+ lemma true_cls_replicate_mset[iff]: "I \ replicate_mset n L \ n \ 0 \ I \l L" by (simp add: true_cls_def) lemma pos_literal_in_imp_true_cls[intro]: "Pos A \# C \ A \ I \ I \ C" using true_cls_def by blast lemma neg_literal_notin_imp_true_cls[intro]: "Neg A \# C \ A \ I \ I \ C" using true_cls_def by blast lemma pos_neg_in_imp_true: "Pos A \# C \ Neg A \# C \ I \ C" using true_cls_def by blast definition true_clss :: "'a interp \ 'a clause set \ bool" (infix "\s" 50) where "I \s CC \ (\C \ CC. I \ C)" lemma true_clss_empty[iff]: "I \s {}" by (simp add: true_clss_def) lemma true_clss_singleton[iff]: "I \s {C} \ I \ C" unfolding true_clss_def by blast lemma true_clss_insert[iff]: "I \s insert C DD \ I \ C \ I \s DD" unfolding true_clss_def by blast lemma true_clss_union[iff]: "I \s CC \ DD \ I \s CC \ I \s DD" unfolding true_clss_def by blast lemma true_clss_Union[iff]: "I \s \ CCC \ (\CC \ CCC. I \s CC)" unfolding true_clss_def by simp lemma true_clss_mono: "DD \ CC \ I \s CC \ I \s DD" by (simp add: subsetD true_clss_def) lemma true_clss_mono_strong: "(\D \ DD. \C \ CC. C \# D) \ I \s CC \ I \s DD" unfolding true_clss_def true_cls_def true_lit_def by (meson mset_subset_eqD) lemma true_clss_subclause: "C \# D \ I \s {C} \ I \s {D}" by (rule true_clss_mono_strong[of _ "{C}"]) auto abbreviation satisfiable :: "'a clause set \ bool" where "satisfiable CC \ \I. I \s CC" lemma satisfiable_antimono: "CC \ DD \ satisfiable DD \ satisfiable CC" using true_clss_mono by blast lemma unsatisfiable_mono: "CC \ DD \ \ satisfiable CC \ \ satisfiable DD" using satisfiable_antimono by blast definition true_cls_mset :: "'a interp \ 'a clause multiset \ bool" (infix "\m" 50) where "I \m CC \ (\C \# CC. I \ C)" lemma true_cls_mset_empty[iff]: "I \m {#}" unfolding true_cls_mset_def by auto lemma true_cls_mset_singleton[iff]: "I \m {#C#} \ I \ C" by (simp add: true_cls_mset_def) lemma true_cls_mset_union[iff]: "I \m CC + DD \ I \m CC \ I \m DD" unfolding true_cls_mset_def by auto -lemma true_cls_mset_Union[iff]: "I \m \# CCC \ (\CC \# CCC. I \m CC)" +lemma true_cls_mset_Union[iff]: "I \m \\<^sub># CCC \ (\CC \# CCC. I \m CC)" unfolding true_cls_mset_def by simp lemma true_cls_mset_add_mset[iff]: "I \m add_mset C CC \ I \ C \ I \m CC" unfolding true_cls_mset_def by auto lemma true_cls_mset_image_mset[iff]: "I \m image_mset f A \ (\x \# A. I \ f x)" unfolding true_cls_mset_def by auto lemma true_cls_mset_mono: "set_mset DD \ set_mset CC \ I \m CC \ I \m DD" unfolding true_cls_mset_def subset_iff by auto lemma true_cls_mset_mono_strong: "(\D \# DD. \C \# CC. C \# D) \ I \m CC \ I \m DD" unfolding true_cls_mset_def true_cls_def true_lit_def by (meson mset_subset_eqD) lemma true_clss_set_mset[iff]: "I \s set_mset CC \ I \m CC" unfolding true_clss_def true_cls_mset_def by auto lemma true_clss_mset_set[simp]: "finite CC \ I \m mset_set CC \ I \s CC" unfolding true_clss_def true_cls_mset_def by auto lemma true_cls_mset_true_cls: "I \m CC \ C \# CC \ I \ C" using true_cls_mset_def by auto end diff --git a/thys/Ordered_Resolution_Prover/Ordered_Ground_Resolution.thy b/thys/Ordered_Resolution_Prover/Ordered_Ground_Resolution.thy --- a/thys/Ordered_Resolution_Prover/Ordered_Ground_Resolution.thy +++ b/thys/Ordered_Resolution_Prover/Ordered_Ground_Resolution.thy @@ -1,468 +1,468 @@ (* Title: Ground Ordered Resolution Calculus with Selection Author: Anders Schlichtkrull , 2016, 2017 Author: Jasmin Blanchette , 2014, 2017 Author: Dmitriy Traytel , 2014 Maintainer: Anders Schlichtkrull *) section \Ground Ordered Resolution Calculus with Selection\ theory Ordered_Ground_Resolution imports Inference_System Ground_Resolution_Model begin text \ Ordered ground resolution with selection is the second inference system studied in Section~3 (``Standard Resolution'') of Bachmair and Ganzinger's chapter. \ subsection \Inference Rule\ text \ Ordered ground resolution consists of a single rule, called \ord_resolve\ below. Like \unord_resolve\, the rule is sound and counterexample-reducing. In addition, it is reductive. \ context ground_resolution_with_selection begin text \ The following inductive definition corresponds to Figure 2. \ definition maximal_wrt :: "'a \ 'a literal multiset \ bool" where "maximal_wrt A DA \ DA = {#} \ A = Max (atms_of DA)" definition strictly_maximal_wrt :: "'a \ 'a literal multiset \ bool" where "strictly_maximal_wrt A CA \ (\B \ atms_of CA. B < A)" inductive eligible :: "'a list \ 'a clause \ bool" where eligible: "(S DA = negs (mset As)) \ (S DA = {#} \ length As = 1 \ maximal_wrt (As ! 0) DA) \ eligible As DA" lemma "(S DA = negs (mset As) \ S DA = {#} \ length As = 1 \ maximal_wrt (As ! 0) DA) \ eligible As DA" using eligible.intros ground_resolution_with_selection.eligible.cases ground_resolution_with_selection_axioms by blast inductive ord_resolve :: "'a clause list \ 'a clause \ 'a multiset list \ 'a list \ 'a clause \ bool" where ord_resolve: "length CAs = n \ length Cs = n \ length AAs = n \ length As = n \ n \ 0 \ (\i < n. CAs ! i = Cs ! i + poss (AAs ! i)) \ (\i < n. AAs ! i \ {#}) \ (\i < n. \A \# AAs ! i. A = As ! i) \ eligible As (D + negs (mset As)) \ (\i < n. strictly_maximal_wrt (As ! i) (Cs ! i)) \ (\i < n. S (CAs ! i) = {#}) \ - ord_resolve CAs (D + negs (mset As)) AAs As (\# (mset Cs) + D)" + ord_resolve CAs (D + negs (mset As)) AAs As (\\<^sub># (mset Cs) + D)" lemma ord_resolve_sound: assumes res_e: "ord_resolve CAs DA AAs As E" and cc_true: "I \m mset CAs" and d_true: "I \ DA" shows "I \ E" using res_e proof (cases rule: ord_resolve.cases) case (ord_resolve n Cs D) note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and as_len = this(6) and cas = this(8) and aas_ne = this(9) and a_eq = this(10) show ?thesis proof (cases "\A \ set As. A \ I") case True then have "\ I \ negs (mset As)" unfolding true_cls_def by fastforce then have "I \ D" using d_true DA by fast then show ?thesis unfolding e by blast next case False then obtain i where a_in_aa: "i < n" and a_false: "As ! i \ I" using cas_len as_len by (metis in_set_conv_nth) have "\ I \ poss (AAs ! i)" using a_false a_eq aas_ne a_in_aa unfolding true_cls_def by auto moreover have "I \ CAs ! i" using a_in_aa cc_true unfolding true_cls_mset_def using cas_len by auto ultimately have "I \ Cs ! i" using cas a_in_aa by auto then show ?thesis using a_in_aa cs_len unfolding e true_cls_def by (meson in_Union_mset_iff nth_mem_mset union_iff) qed qed lemma filter_neg_atm_of_S: "{#Neg (atm_of L). L \# S C#} = S C" by (simp add: S_selects_neg_lits) text \ This corresponds to Lemma 3.13: \ lemma ord_resolve_reductive: assumes "ord_resolve CAs DA AAs As E" shows "E < DA" using assms proof (cases rule: ord_resolve.cases) case (ord_resolve n Cs D) note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and ai_len = this(6) and nz = this(7) and cas = this(8) and maxim = this(12) show ?thesis - proof (cases "\# (mset Cs) = {#}") + proof (cases "\\<^sub># (mset Cs) = {#}") case True have "negs (mset As) \ {#}" using nz ai_len by auto then show ?thesis unfolding True e DA by auto next case False define max_A_of_Cs where - "max_A_of_Cs = Max (atms_of (\# (mset Cs)))" + "max_A_of_Cs = Max (atms_of (\\<^sub># (mset Cs)))" have - mc_in: "max_A_of_Cs \ atms_of (\# (mset Cs))" and - mc_max: "\B. B \ atms_of (\# (mset Cs)) \ B \ max_A_of_Cs" + mc_in: "max_A_of_Cs \ atms_of (\\<^sub># (mset Cs))" and + mc_max: "\B. B \ atms_of (\\<^sub># (mset Cs)) \ B \ max_A_of_Cs" using max_A_of_Cs_def False by auto then have "\C_max \ set Cs. max_A_of_Cs \ atms_of (C_max)" by (metis atm_imp_pos_or_neg_lit in_Union_mset_iff neg_lit_in_atms_of pos_lit_in_atms_of set_mset_mset) then obtain max_i where cm_in_cas: "max_i < length CAs" and mc_in_cm: "max_A_of_Cs \ atms_of (Cs ! max_i)" using in_set_conv_nth[of _ CAs] by (metis cas_len cs_len in_set_conv_nth) define CA_max where "CA_max = CAs ! max_i" define A_max where "A_max = As ! max_i" define C_max where "C_max = Cs ! max_i" have mc_lt_ma: "max_A_of_Cs < A_max" using maxim cm_in_cas mc_in_cm cas_len unfolding strictly_maximal_wrt_def A_max_def by auto - then have ucas_ne_neg_aa: "\# (mset Cs) \ negs (mset As)" + then have ucas_ne_neg_aa: "\\<^sub># (mset Cs) \ negs (mset As)" using mc_in mc_max mc_lt_ma cm_in_cas cas_len ai_len unfolding A_max_def by (metis atms_of_negs nth_mem set_mset_mset leD) - moreover have ucas_lt_ma: "\B \ atms_of (\# (mset Cs)). B < A_max" + moreover have ucas_lt_ma: "\B \ atms_of (\\<^sub># (mset Cs)). B < A_max" using mc_max mc_lt_ma by fastforce - moreover have "\ Neg A_max \# \# (mset Cs)" - using ucas_lt_ma neg_lit_in_atms_of[of A_max "\# (mset Cs)"] by auto + moreover have "\ Neg A_max \# \\<^sub># (mset Cs)" + using ucas_lt_ma neg_lit_in_atms_of[of A_max "\\<^sub># (mset Cs)"] by auto moreover have "Neg A_max \# negs (mset As)" using cm_in_cas cas_len ai_len A_max_def by auto - ultimately have "\# (mset Cs) < negs (mset As)" + ultimately have "\\<^sub># (mset Cs) < negs (mset As)" unfolding less_multiset\<^sub>H\<^sub>O by (metis (no_types) atms_less_eq_imp_lit_less_eq_neg count_greater_zero_iff count_inI le_imp_less_or_eq less_imp_not_less not_le) then show ?thesis unfolding e DA by auto qed qed text \ This corresponds to Theorem 3.15: \ theorem ord_resolve_counterex_reducing: assumes ec_ni_n: "{#} \ N" and d_in_n: "DA \ N" and d_cex: "\ INTERP N \ DA" and d_min: "\C. C \ N \ \ INTERP N \ C \ DA \ C" obtains CAs AAs As E where "set CAs \ N" "INTERP N \m mset CAs" "\CA. CA \ set CAs \ productive N CA" "ord_resolve CAs DA AAs As E" "\ INTERP N \ E" "E < DA" proof - have d_ne: "DA \ {#}" using d_in_n ec_ni_n by blast have "\As. As \ [] \ negs (mset As) \# DA \ eligible As DA" proof (cases "S DA = {#}") assume s_d_e: "S DA = {#}" define A where "A = Max (atms_of DA)" define As where "As = [A]" define D where "D = DA-{#Neg A #}" have na_in_d: "Neg A \# DA" unfolding A_def using s_d_e d_ne d_in_n d_cex d_min by (metis Max_in_lits Max_lit_eq_pos_or_neg_Max_atm max_pos_imp_Interp Interp_imp_INTERP) then have das: "DA = D + negs (mset As)" unfolding D_def As_def by auto moreover from na_in_d have "negs (mset As) \# DA" by (simp add: As_def) moreover have hd: "As ! 0 = Max (atms_of (D + negs (mset As)))" using A_def As_def das by auto then have "eligible As DA" using eligible s_d_e As_def das maximal_wrt_def by auto ultimately show ?thesis using As_def by blast next assume s_d_e: "S DA \ {#}" define As :: "'a list" where "As = list_of_mset {#atm_of L. L \# S DA#}" define D :: "'a clause" where "D = DA - negs {#atm_of L. L \# S DA#}" have "As \ []" unfolding As_def using s_d_e by (metis image_mset_is_empty_iff list_of_mset_empty) moreover have da_sub_as: "negs {#atm_of L. L \# S DA#} \# DA" using S_selects_subseteq by (auto simp: filter_neg_atm_of_S) then have "negs (mset As) \# DA" unfolding As_def by auto moreover have das: "DA = D + negs (mset As)" using da_sub_as unfolding D_def As_def by auto moreover have "S DA = negs {#atm_of L. L \# S DA#}" by (auto simp: filter_neg_atm_of_S) then have "S DA = negs (mset As)" unfolding As_def by auto then have "eligible As DA" unfolding das using eligible by auto ultimately show ?thesis by blast qed then obtain As :: "'a list" where as_ne: "As \ []" and negs_as_le_d: "negs (mset As) \# DA" and s_d: "eligible As DA" by blast define D :: "'a clause" where "D = DA - negs (mset As)" have "set As \ INTERP N" using d_cex negs_as_le_d by force then have prod_ex: "\A \ set As. \D. produces N D A" unfolding INTERP_def by (metis (no_types, lifting) INTERP_def subsetCE UN_E not_produces_imp_notin_production) then have "\A. \D. produces N D A \ A \ set As" using ec_ni_n by (auto intro: productive_in_N) then have "\A. \D. produces N D A \ A \ set As" using prod_ex by blast then obtain CA_of where c_of0: "\A. produces N (CA_of A) A \ A \ set As" by metis then have prod_c0: "\A \ set As. produces N (CA_of A) A" by blast define C_of where "\A. C_of A = {#L \# CA_of A. L \ Pos A#}" define Aj_of where "\A. Aj_of A = image_mset atm_of {#L \# CA_of A. L = Pos A#}" have pospos: "\LL A. {#Pos (atm_of x). x \# {#L \# LL. L = Pos A#}#} = {#L \# LL. L = Pos A#}" by (metis (mono_tags, lifting) image_filter_cong literal.sel(1) multiset.map_ident) have ca_of_c_of_aj_of: "\A. CA_of A = C_of A + poss (Aj_of A)" using pospos[of _ "CA_of _"] by (simp add: C_of_def Aj_of_def) define n :: nat where "n = length As" define Cs :: "'a clause list" where "Cs = map C_of As" define AAs :: "'a multiset list" where "AAs = map Aj_of As" define CAs :: "'a literal multiset list" where "CAs = map CA_of As" have m_nz: "\A. A \ set As \ Aj_of A \ {#}" unfolding Aj_of_def using prod_c0 produces_imp_Pos_in_lits by (metis (full_types) filter_mset_empty_conv image_mset_is_empty_iff) have prod_c: "productive N CA" if ca_in: "CA \ set CAs" for CA proof - obtain i where i_p: "i < length CAs" "CAs ! i = CA" using ca_in by (meson in_set_conv_nth) have "production N (CA_of (As ! i)) = {As ! i}" using i_p CAs_def prod_c0 by auto then show "productive N CA" using i_p CAs_def by auto qed then have cs_subs_n: "set CAs \ N" using productive_in_N by auto have cs_true: "INTERP N \m mset CAs" unfolding true_cls_mset_def using prod_c productive_imp_INTERP by auto have "\A. A \ set As \ \ Neg A \# CA_of A" using prod_c0 produces_imp_neg_notin_lits by auto then have a_ni_c': "\A. A \ set As \ A \ atms_of (C_of A)" unfolding C_of_def using atm_imp_pos_or_neg_lit by force have c'_le_c: "\A. C_of A \ CA_of A" unfolding C_of_def by (auto intro: subset_eq_imp_le_multiset) have a_max_c: "\A. A \ set As \ A = Max (atms_of (CA_of A))" using prod_c0 productive_imp_produces_Max_atom[of N] by auto then have "\A. A \ set As \ C_of A \ {#} \ Max (atms_of (C_of A)) \ A" using c'_le_c by (metis less_eq_Max_atms_of) moreover have "\A. A \ set As \ C_of A \ {#} \ Max (atms_of (C_of A)) \ A" using a_ni_c' Max_in by (metis (no_types) atms_empty_iff_empty finite_atms_of) ultimately have max_c'_lt_a: "\A. A \ set As \ C_of A \ {#} \ Max (atms_of (C_of A)) < A" by (metis order.strict_iff_order) have le_cs_as: "length CAs = length As" unfolding CAs_def by simp have "length CAs = n" by (simp add: le_cs_as n_def) moreover have "length Cs = n" by (simp add: Cs_def n_def) moreover have "length AAs = n" by (simp add: AAs_def n_def) moreover have "length As = n" using n_def by auto moreover have "n \ 0" by (simp add: as_ne n_def) moreover have " \i. i < length AAs \ (\A \# AAs ! i. A = As ! i)" using AAs_def Aj_of_def by auto have "\x B. production N (CA_of x) = {x} \ B \# CA_of x \ B \ Pos x \ atm_of B < x" by (metis atm_of_lit_in_atms_of insert_not_empty le_imp_less_or_eq Pos_atm_of_iff Neg_atm_of_iff pos_neg_in_imp_true produces_imp_Pos_in_lits produces_imp_atms_leq productive_imp_not_interp) then have "\B A. A\set As \ B \# CA_of A \ B \ Pos A \ atm_of B < A" using prod_c0 by auto have "\i. i < length AAs \ AAs ! i \ {#}" unfolding AAs_def using m_nz by simp have "\i < n. CAs ! i = Cs ! i + poss (AAs ! i)" unfolding CAs_def Cs_def AAs_def using ca_of_c_of_aj_of by (simp add: n_def) moreover have "\i < n. AAs ! i \ {#}" using \\i < length AAs. AAs ! i \ {#}\ calculation(3) by blast moreover have "\i < n. \A \# AAs ! i. A = As ! i" by (simp add: \\i < length AAs. \A \# AAs ! i. A = As ! i\ calculation(3)) moreover have "eligible As DA" using s_d by auto then have "eligible As (D + negs (mset As))" using D_def negs_as_le_d by auto moreover have "\i. i < length AAs \ strictly_maximal_wrt (As ! i) ((Cs ! i))" by (simp add: C_of_def Cs_def \\x B. \production N (CA_of x) = {x}; B \# CA_of x; B \ Pos x\ \ atm_of B < x\ atms_of_def calculation(3) n_def prod_c0 strictly_maximal_wrt_def) have "\i < n. strictly_maximal_wrt (As ! i) (Cs ! i)" by (simp add: \\i. i < length AAs \ strictly_maximal_wrt (As ! i) (Cs ! i)\ calculation(3)) moreover have "\CA \ set CAs. S CA = {#}" using prod_c producesD productive_imp_produces_Max_literal by blast have "\CA\set CAs. S CA = {#}" using \\CA\set CAs. S CA = {#}\ by simp then have "\i < n. S (CAs ! i) = {#}" using \length CAs = n\ nth_mem by blast - ultimately have res_e: "ord_resolve CAs (D + negs (mset As)) AAs As (\# (mset Cs) + D)" + ultimately have res_e: "ord_resolve CAs (D + negs (mset As)) AAs As (\\<^sub># (mset Cs) + D)" using ord_resolve by auto have "\A. A \ set As \ \ interp N (CA_of A) \ CA_of A" by (simp add: prod_c0 producesD) then have "\A. A \ set As \ \ Interp N (CA_of A) \ C_of A" unfolding prod_c0 C_of_def Interp_def true_cls_def using true_lit_def not_gr_zero prod_c0 by auto then have c'_at_n: "\A. A \ set As \ \ INTERP N \ C_of A" using a_max_c c'_le_c max_c'_lt_a not_Interp_imp_not_INTERP unfolding true_cls_def by (metis true_cls_def true_cls_empty) - have "\ INTERP N \ \# (mset Cs)" + have "\ INTERP N \ \\<^sub># (mset Cs)" unfolding Cs_def true_cls_def using c'_at_n by fastforce moreover have "\ INTERP N \ D" using d_cex by (metis D_def add_diff_cancel_right' negs_as_le_d subset_mset.add_diff_assoc2 true_cls_def union_iff) - ultimately have e_cex: "\ INTERP N \ \# (mset Cs) + D" + ultimately have e_cex: "\ INTERP N \ \\<^sub># (mset Cs) + D" by simp have "set CAs \ N" by (simp add: cs_subs_n) moreover have "INTERP N \m mset CAs" by (simp add: cs_true) moreover have "\CA. CA \ set CAs \ productive N CA" by (simp add: prod_c) - moreover have "ord_resolve CAs DA AAs As (\# (mset Cs) + D)" + moreover have "ord_resolve CAs DA AAs As (\\<^sub># (mset Cs) + D)" using D_def negs_as_le_d res_e by auto - moreover have "\ INTERP N \ \# (mset Cs) + D" + moreover have "\ INTERP N \ \\<^sub># (mset Cs) + D" using e_cex by simp - moreover have "\# (mset Cs) + D < DA" + moreover have "\\<^sub># (mset Cs) + D < DA" using calculation(4) ord_resolve_reductive by auto ultimately show thesis .. qed lemma ord_resolve_atms_of_concl_subset: assumes "ord_resolve CAs DA AAs As E" shows "atms_of E \ (\C \ set CAs. atms_of C) \ atms_of DA" using assms proof (cases rule: ord_resolve.cases) case (ord_resolve n Cs D) note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and cas = this(8) have "\i < n. set_mset (Cs ! i) \ set_mset (CAs ! i)" using cas by auto - then have "\i < n. Cs ! i \# \# (mset CAs)" + then have "\i < n. Cs ! i \# \\<^sub># (mset CAs)" by (metis cas cas_len mset_subset_eq_add_left nth_mem_mset sum_mset.remove union_assoc) - then have "\C \ set Cs. C \# \# (mset CAs)" + then have "\C \ set Cs. C \# \\<^sub># (mset CAs)" using cs_len in_set_conv_nth[of _ Cs] by auto - then have "set_mset (\# (mset Cs)) \ set_mset (\# (mset CAs))" + then have "set_mset (\\<^sub># (mset Cs)) \ set_mset (\\<^sub># (mset CAs))" by auto (meson in_mset_sum_list2 mset_subset_eqD) - then have "atms_of (\# (mset Cs)) \ atms_of (\# (mset CAs))" + then have "atms_of (\\<^sub># (mset Cs)) \ atms_of (\\<^sub># (mset CAs))" by (meson lits_subseteq_imp_atms_subseteq mset_subset_eqD subsetI) - moreover have "atms_of (\# (mset CAs)) = (\CA \ set CAs. atms_of CA)" + moreover have "atms_of (\\<^sub># (mset CAs)) = (\CA \ set CAs. atms_of CA)" by (intro set_eqI iffI, simp_all, metis in_mset_sum_list2 atm_imp_pos_or_neg_lit neg_lit_in_atms_of pos_lit_in_atms_of, metis in_mset_sum_list atm_imp_pos_or_neg_lit neg_lit_in_atms_of pos_lit_in_atms_of) - ultimately have "atms_of (\# (mset Cs)) \ (\CA \ set CAs. atms_of CA)" + ultimately have "atms_of (\\<^sub># (mset Cs)) \ (\CA \ set CAs. atms_of CA)" by auto moreover have "atms_of D \ atms_of DA" using DA by auto ultimately show ?thesis unfolding e by auto qed subsection \Inference System\ text \ Theorem 3.16 is subsumed in the counterexample-reducing inference system framework, which is instantiated below. Unlike its unordered cousin, ordered resolution is additionally a reductive inference system. \ definition ord_\ :: "'a inference set" where "ord_\ = {Infer (mset CAs) DA E | CAs DA AAs As E. ord_resolve CAs DA AAs As E}" sublocale ord_\_sound_counterex_reducing?: sound_counterex_reducing_inference_system "ground_resolution_with_selection.ord_\ S" "ground_resolution_with_selection.INTERP S" + reductive_inference_system "ground_resolution_with_selection.ord_\ S" proof unfold_locales fix N :: "'a clause set" and DA :: "'a clause" assume "{#} \ N" and "DA \ N" and "\ INTERP N \ DA" and "\C. C \ N \ \ INTERP N \ C \ DA \ C" then obtain CAs AAs As E where dd_sset_n: "set CAs \ N" and dd_true: "INTERP N \m mset CAs" and res_e: "ord_resolve CAs DA AAs As E" and e_cex: "\ INTERP N \ E" and e_lt_c: "E < DA" using ord_resolve_counterex_reducing[of N DA thesis] by auto have "Infer (mset CAs) DA E \ ord_\" using res_e unfolding ord_\_def by (metis (mono_tags, lifting) mem_Collect_eq) then show "\CC E. set_mset CC \ N \ INTERP N \m CC \ Infer CC DA E \ ord_\ \ \ INTERP N \ E \ E < DA" using dd_sset_n dd_true e_cex e_lt_c by (metis set_mset_mset) qed (auto simp: ord_\_def intro: ord_resolve_sound ord_resolve_reductive) lemmas clausal_logic_compact = ord_\_sound_counterex_reducing.clausal_logic_compact end text \ A second proof of Theorem 3.12, compactness of clausal logic: \ lemmas clausal_logic_compact = ground_resolution_with_selection.clausal_logic_compact end diff --git a/thys/PAC_Checker/PAC_Polynomials.thy b/thys/PAC_Checker/PAC_Polynomials.thy --- a/thys/PAC_Checker/PAC_Polynomials.thy +++ b/thys/PAC_Checker/PAC_Polynomials.thy @@ -1,489 +1,489 @@ theory PAC_Polynomials imports PAC_Specification Finite_Map_Multiset begin section \Polynomials of strings\ text \ Isabelle's definition of polynomials only work with variables of type \<^typ>\nat\. Therefore, we introduce a version that uses strings by using an injective function that converts a string to a natural number. It exists because strings are countable. Remark that the whole development is independent of the function. \ subsection \Polynomials and Variables\ lemma poly_embed_EX: \\\. bij (\ :: string \ nat)\ by (rule countableE_infinite[of \UNIV :: string set\]) (auto intro!: infinite_UNIV_listI) text \Using a multiset instead of a list has some advantage from an abstract point of view. First, we can have monomials that appear several times and the coefficient can also be zero. Basically, we can represent un-normalised polynomials, which is very useful to talk about intermediate states in our program. \ type_synonym term_poly = \string multiset\ type_synonym mset_polynomial = \(term_poly * int) multiset\ definition normalized_poly :: \mset_polynomial \ bool\ where \normalized_poly p \ distinct_mset (fst `# p) \ 0 \# snd `# p\ lemma normalized_poly_simps[simp]: \normalized_poly {#}\ \normalized_poly (add_mset t p) \ snd t \ 0 \ fst t \# fst `# p \ normalized_poly p\ by (auto simp: normalized_poly_def) lemma normalized_poly_mono: \normalized_poly B \ A \# B \ normalized_poly A\ unfolding normalized_poly_def by (auto intro: distinct_mset_mono image_mset_subseteq_mono) definition mult_poly_by_monom :: \term_poly * int \ mset_polynomial \ mset_polynomial\ where \mult_poly_by_monom = (\ys q. image_mset (\xs. (fst xs + fst ys, snd ys * snd xs)) q)\ definition mult_poly_raw :: \mset_polynomial \ mset_polynomial \ mset_polynomial\ where \mult_poly_raw p q = (sum_mset ((\y. mult_poly_by_monom y q) `# p))\ definition remove_powers :: \mset_polynomial \ mset_polynomial\ where \remove_powers xs = image_mset (apfst remdups_mset) xs\ definition all_vars_mset :: \mset_polynomial \ string multiset\ where - \all_vars_mset p = \# (fst `# p)\ + \all_vars_mset p = \\<^sub># (fst `# p)\ abbreviation all_vars :: \mset_polynomial \ string set\ where \all_vars p \ set_mset (all_vars_mset p)\ definition add_to_coefficient :: \_ \ mset_polynomial \ mset_polynomial\ where \add_to_coefficient = (\(a, n) b. {#(a', _) \# b. a' \ a#} + (if n + sum_mset (snd `# {#(a', _) \# b. a' = a#}) = 0 then {#} else {#(a, n + sum_mset (snd `# {#(a', _) \# b. a' = a#}))#}))\ definition normalize_poly :: \mset_polynomial \ mset_polynomial\ where \normalize_poly p = fold_mset add_to_coefficient {#} p\ lemma add_to_coefficient_simps: \n + sum_mset (snd `# {#(a', _) \# b. a' = a#}) \ 0 \ add_to_coefficient (a, n) b = {#(a', _) \# b. a' \ a#} + {#(a, n + sum_mset (snd `# {#(a', _) \# b. a' = a#}))#}\ \n + sum_mset (snd `# {#(a', _) \# b. a' = a#}) = 0 \ add_to_coefficient (a, n) b = {#(a', _) \# b. a' \ a#}\ and add_to_coefficient_simps_If: \add_to_coefficient (a, n) b = {#(a', _) \# b. a' \ a#} + (if n + sum_mset (snd `# {#(a', _) \# b. a' = a#}) = 0 then {#} else {#(a, n + sum_mset (snd `# {#(a', _) \# b. a' = a#}))#})\ by (auto simp: add_to_coefficient_def) interpretation comp_fun_commute \add_to_coefficient\ proof - have [iff]: \a \ aa \ ((case x of (a', _) \ a' = a) \ (case x of (a', _) \ a' \ aa)) \ (case x of (a', _) \ a' = a)\ for a' aa a x by auto show \comp_fun_commute add_to_coefficient\ unfolding add_to_coefficient_def by standard (auto intro!: ext simp: filter_filter_mset ac_simps add_eq_0_iff) qed lemma normalized_poly_normalize_poly[simp]: \normalized_poly (normalize_poly p)\ unfolding normalize_poly_def apply (induction p) subgoal by auto subgoal for x p by (cases x) (auto simp: add_to_coefficient_simps_If intro: normalized_poly_mono) done subsection \Addition\ inductive add_poly_p :: \mset_polynomial \ mset_polynomial \ mset_polynomial \ mset_polynomial \ mset_polynomial \ mset_polynomial \ bool\ where add_new_coeff_r: \add_poly_p (p, add_mset x q, r) (p, q, add_mset x r)\ | add_new_coeff_l: \add_poly_p (add_mset x p, q, r) (p, q, add_mset x r)\ | add_same_coeff_l: \add_poly_p (add_mset (x, n) p, q, add_mset (x, m) r) (p, q, add_mset (x, n + m) r)\ | add_same_coeff_r: \add_poly_p (p, add_mset (x, n) q, add_mset (x, m) r) (p, q, add_mset (x, n + m) r)\ | rem_0_coeff: \add_poly_p (p, q, add_mset (x, 0) r) (p, q, r)\ inductive_cases add_poly_pE: \add_poly_p S T\ lemmas add_poly_p_induct = add_poly_p.induct[split_format(complete)] lemma add_poly_p_empty_l: \add_poly_p\<^sup>*\<^sup>* (p, q, r) ({#}, q, p + r)\ apply (induction p arbitrary: r) subgoal by auto subgoal by (metis (no_types, lifting) add_new_coeff_l r_into_rtranclp rtranclp_trans union_mset_add_mset_left union_mset_add_mset_right) done lemma add_poly_p_empty_r: \add_poly_p\<^sup>*\<^sup>* (p, q, r) (p, {#}, q + r)\ apply (induction q arbitrary: r) subgoal by auto subgoal by (metis (no_types, lifting) add_new_coeff_r r_into_rtranclp rtranclp_trans union_mset_add_mset_left union_mset_add_mset_right) done lemma add_poly_p_sym: \add_poly_p (p, q, r) (p', q', r') \ add_poly_p (q, p, r) (q', p', r')\ apply (rule iffI) subgoal by (cases rule: add_poly_p.cases, assumption) (auto intro: add_poly_p.intros) subgoal by (cases rule: add_poly_p.cases, assumption) (auto intro: add_poly_p.intros) done lemma wf_if_measure_in_wf: \wf R \ (\a b. (a, b) \ S \ (\ a, \ b)\R) \ wf S\ by (metis in_inv_image wfE_min wfI_min wf_inv_image) lemma lexn_n: \n > 0 \ (x # xs, y # ys) \ lexn r n \ (length xs = n-1 \ length ys = n-1) \ ((x, y) \ r \ (x = y \ (xs, ys) \ lexn r (n - 1)))\ apply (cases n) apply simp by (auto simp: map_prod_def image_iff lex_prod_def) lemma wf_add_poly_p: \wf {(x, y). add_poly_p y x}\ by (rule wf_if_measure_in_wf[where R = \lexn less_than 3\ and \ = \\(a,b,c). [size a , size b, size c]\]) (auto simp: add_poly_p.simps wf_lexn simp: lexn_n simp del: lexn.simps(2)) lemma mult_poly_by_monom_simps[simp]: \mult_poly_by_monom t {#} = {#}\ \mult_poly_by_monom t (ps + qs) = mult_poly_by_monom t ps + mult_poly_by_monom t qs\ \mult_poly_by_monom a (add_mset p ps) = add_mset (fst a + fst p, snd a * snd p) (mult_poly_by_monom a ps)\ proof - interpret comp_fun_commute \(\xs. add_mset (xs + t))\ for t by standard auto show \mult_poly_by_monom t (ps + qs) = mult_poly_by_monom t ps + mult_poly_by_monom t qs\ for t by (induction ps) (auto simp: mult_poly_by_monom_def) show \mult_poly_by_monom a (add_mset p ps) = add_mset (fst a + fst p, snd a * snd p) (mult_poly_by_monom a ps)\ \mult_poly_by_monom t {#} = {#}\for t by (auto simp: mult_poly_by_monom_def) qed inductive mult_poly_p :: \mset_polynomial \ mset_polynomial \ mset_polynomial \ mset_polynomial \ mset_polynomial \ bool\ for q :: mset_polynomial where mult_step: \mult_poly_p q (add_mset (xs, n) p, r) (p, (\(ys, m). (remdups_mset (xs + ys), n * m)) `# q + r)\ lemmas mult_poly_p_induct = mult_poly_p.induct[split_format(complete)] subsection \Normalisation\ inductive normalize_poly_p :: \mset_polynomial \ mset_polynomial \ bool\where rem_0_coeff[simp, intro]: \normalize_poly_p p q \ normalize_poly_p (add_mset (xs, 0) p) q\ | merge_dup_coeff[simp, intro]: \normalize_poly_p p q \ normalize_poly_p (add_mset (xs, m) (add_mset (xs, n) p)) (add_mset (xs, m + n) q)\ | same[simp, intro]: \normalize_poly_p p p\ | keep_coeff[simp, intro]: \normalize_poly_p p q \ normalize_poly_p (add_mset x p) (add_mset x q)\ subsection \Correctness\ text \ This locales maps string polynomials to real polynomials. \ locale poly_embed = fixes \ :: \string \ nat\ assumes \_inj: \inj \\ begin definition poly_of_vars :: "term_poly \ ('a :: {comm_semiring_1}) mpoly" where \poly_of_vars xs = fold_mset (\a b. Var (\ a) * b) (1 :: 'a mpoly) xs\ lemma poly_of_vars_simps[simp]: shows \poly_of_vars (add_mset x xs) = Var (\ x) * (poly_of_vars xs :: ('a :: {comm_semiring_1}) mpoly)\ (is ?A) and \poly_of_vars (xs + ys) = poly_of_vars xs * (poly_of_vars ys :: ('a :: {comm_semiring_1}) mpoly)\ (is ?B) proof - interpret comp_fun_commute \(\a b. (b :: 'a :: {comm_semiring_1} mpoly) * Var (\ a))\ by standard (auto simp: algebra_simps ac_simps Var_def times_monomial_monomial intro!: ext) show ?A by (auto simp: poly_of_vars_def comp_fun_commute_axioms fold_mset_fusion ac_simps) show ?B apply (auto simp: poly_of_vars_def ac_simps) by (simp add: local.comp_fun_commute_axioms local.fold_mset_fusion semiring_normalization_rules(18)) qed definition mononom_of_vars where \mononom_of_vars \ (\(xs, n). (+) (Const n * poly_of_vars xs))\ interpretation comp_fun_commute \mononom_of_vars\ by standard (auto simp: algebra_simps ac_simps mononom_of_vars_def Var_def times_monomial_monomial intro!: ext) lemma [simp]: \poly_of_vars {#} = 1\ by (auto simp: poly_of_vars_def) lemma mononom_of_vars_add[simp]: \NO_MATCH 0 b \ mononom_of_vars xs b = Const (snd xs) * poly_of_vars (fst xs) + b\ by (cases xs) (auto simp: ac_simps mononom_of_vars_def) definition polynomial_of_mset :: \mset_polynomial \ _\ where \polynomial_of_mset p = sum_mset (mononom_of_vars `# p) 0\ lemma polynomial_of_mset_append[simp]: \polynomial_of_mset (xs + ys) = polynomial_of_mset xs + polynomial_of_mset ys\ by (auto simp: ac_simps Const_def polynomial_of_mset_def) lemma polynomial_of_mset_Cons[simp]: \polynomial_of_mset (add_mset x ys) = Const (snd x) * poly_of_vars (fst x) + polynomial_of_mset ys\ by (cases x) (auto simp: ac_simps polynomial_of_mset_def mononom_of_vars_def) lemma polynomial_of_mset_empty[simp]: \polynomial_of_mset {#} = 0\ by (auto simp: polynomial_of_mset_def) lemma polynomial_of_mset_mult_poly_by_monom[simp]: \polynomial_of_mset (mult_poly_by_monom x ys) = (Const (snd x) * poly_of_vars (fst x) * polynomial_of_mset ys)\ by (induction ys) (auto simp: Const_mult algebra_simps) lemma polynomial_of_mset_mult_poly_raw[simp]: \polynomial_of_mset (mult_poly_raw xs ys) = polynomial_of_mset xs * polynomial_of_mset ys\ unfolding mult_poly_raw_def by (induction xs arbitrary: ys) (auto simp: Const_mult algebra_simps) lemma polynomial_of_mset_uminus: \polynomial_of_mset {#case x of (a, b) \ (a, - b). x \# za#} = - polynomial_of_mset za\ by (induction za) auto lemma X2_X_polynomial_bool_mult_in: \Var (x1) * (Var (x1) * p) - Var (x1) * p \ More_Modules.ideal polynomial_bool\ using ideal_mult_right_in[OF X2_X_in_pac_ideal[of x1 \{}\, unfolded pac_ideal_def], of p] by (auto simp: right_diff_distrib ac_simps power2_eq_square) lemma polynomial_of_list_remove_powers_polynomial_bool: \(polynomial_of_mset xs) - polynomial_of_mset (remove_powers xs) \ ideal polynomial_bool\ proof (induction xs) case empty then show \?case\ by (auto simp: remove_powers_def ideal.span_zero) next case (add x xs) have H1: \x1 \# x2 \ Var (\ x1) * poly_of_vars x2 - p \ More_Modules.ideal polynomial_bool \ poly_of_vars x2 - p \ More_Modules.ideal polynomial_bool \ for x1 x2 p apply (subst (2) ideal.span_add_eq[symmetric, of \Var (\ x1) * poly_of_vars x2 - poly_of_vars x2\]) apply (drule multi_member_split) apply (auto simp: X2_X_polynomial_bool_mult_in) done have diff: \poly_of_vars (x) - poly_of_vars (remdups_mset (x)) \ ideal polynomial_bool\ for x by (induction x) (auto simp: remove_powers_def ideal.span_zero H1 simp flip: right_diff_distrib intro!: ideal.span_scale) have [simp]: \polynomial_of_mset xs - polynomial_of_mset (apfst remdups_mset `# xs) \ More_Modules.ideal polynomial_bool \ poly_of_vars ys * poly_of_vars ys - poly_of_vars ys * poly_of_vars (remdups_mset ys) \ More_Modules.ideal polynomial_bool \ polynomial_of_mset xs + Const y * poly_of_vars ys - (polynomial_of_mset (apfst remdups_mset `# xs) + Const y * poly_of_vars (remdups_mset ys)) \ More_Modules.ideal polynomial_bool\ for y ys by (metis add_diff_add diff ideal.scale_right_diff_distrib ideal.span_add ideal.span_scale) show ?case using add apply (cases x) subgoal for ys y using ideal_mult_right_in2[OF diff, of \poly_of_vars ys\ ys] by (auto simp: remove_powers_def right_diff_distrib ideal.span_diff ideal.span_add field_simps) done qed lemma add_poly_p_polynomial_of_mset: \add_poly_p (p, q, r) (p', q', r') \ polynomial_of_mset r + (polynomial_of_mset p + polynomial_of_mset q) = polynomial_of_mset r' + (polynomial_of_mset p' + polynomial_of_mset q')\ apply (induction rule: add_poly_p_induct) subgoal by auto subgoal by auto subgoal by (auto simp: algebra_simps Const_add) subgoal by (auto simp: algebra_simps Const_add) subgoal by (auto simp: algebra_simps Const_add) done lemma rtranclp_add_poly_p_polynomial_of_mset: \add_poly_p\<^sup>*\<^sup>* (p, q, r) (p', q', r') \ polynomial_of_mset r + (polynomial_of_mset p + polynomial_of_mset q) = polynomial_of_mset r' + (polynomial_of_mset p' + polynomial_of_mset q')\ by (induction rule: rtranclp_induct[of add_poly_p \(_, _, _)\ \(_, _, _)\, split_format(complete), of for r]) (auto dest: add_poly_p_polynomial_of_mset) lemma rtranclp_add_poly_p_polynomial_of_mset_full: \add_poly_p\<^sup>*\<^sup>* (p, q, {#}) ({#}, {#}, r') \ polynomial_of_mset r' = (polynomial_of_mset p + polynomial_of_mset q)\ by (drule rtranclp_add_poly_p_polynomial_of_mset) (auto simp: ac_simps add_eq_0_iff) lemma poly_of_vars_remdups_mset: \poly_of_vars (remdups_mset (xs)) - (poly_of_vars xs) \ More_Modules.ideal polynomial_bool\ apply (induction xs) subgoal by (auto simp: ideal.span_zero) subgoal for x xs apply (cases \x \# xs\) apply (metis (no_types, lifting) X2_X_polynomial_bool_mult_in diff_add_cancel diff_diff_eq2 ideal.span_diff insert_DiffM poly_of_vars_simps(1) remdups_mset_singleton_sum) by (metis (no_types, lifting) ideal.span_scale poly_of_vars_simps(1) remdups_mset_singleton_sum right_diff_distrib) done lemma polynomial_of_mset_mult_map: \polynomial_of_mset {#case x of (ys, n) \ (remdups_mset (ys + xs), n * m). x \# q#} - Const m * (poly_of_vars xs * polynomial_of_mset q) \ More_Modules.ideal polynomial_bool\ (is \?P q \ _\) proof (induction q) case empty then show ?case by (auto simp: algebra_simps ideal.span_zero) next case (add x q) then have uP: \-?P q \ More_Modules.ideal polynomial_bool\ using ideal.span_neg by blast have \ Const b * (Const m * poly_of_vars (remdups_mset (a + xs))) - Const b * (Const m * (poly_of_vars a * poly_of_vars xs)) \ More_Modules.ideal polynomial_bool\ for a b by (auto simp: Const_mult simp flip: right_diff_distrib' poly_of_vars_simps intro!: ideal.span_scale poly_of_vars_remdups_mset) then show ?case apply (subst ideal.span_add_eq2[symmetric, OF uP]) apply (cases x) apply (auto simp: field_simps Const_mult simp flip: intro!: ideal.span_scale poly_of_vars_remdups_mset) done qed lemma mult_poly_p_mult_ideal: \mult_poly_p q (p, r) (p', r') \ (polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r) \ ideal polynomial_bool\ proof (induction rule: mult_poly_p_induct) case (mult_step xs n p r) show ?case by (auto simp: algebra_simps polynomial_of_mset_mult_map) qed lemma rtranclp_mult_poly_p_mult_ideal: \(mult_poly_p q)\<^sup>*\<^sup>* (p, r) (p', r') \ (polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r) \ ideal polynomial_bool\ apply (induction p' r' rule: rtranclp_induct[of \mult_poly_p q\ \(p, r)\ \(p', q')\ for p' q', split_format(complete)]) subgoal by (auto simp: ideal.span_zero) subgoal for a b aa ba apply (drule mult_poly_p_mult_ideal) apply (drule ideal.span_add) apply assumption by (auto simp: group_add_class.diff_add_eq_diff_diff_swap add.inverse_distrib_swap ac_simps add_diff_eq simp flip: diff_add_eq_diff_diff_swap) done lemma rtranclp_mult_poly_p_mult_ideal_final: \(mult_poly_p q)\<^sup>*\<^sup>* (p, {#}) ({#}, r) \ (polynomial_of_mset r) - (polynomial_of_mset p * polynomial_of_mset q) \ ideal polynomial_bool\ by (drule rtranclp_mult_poly_p_mult_ideal) auto lemma normalize_poly_p_poly_of_mset: \normalize_poly_p p q \ polynomial_of_mset p = polynomial_of_mset q\ apply (induction rule: normalize_poly_p.induct) apply (auto simp: Const_add algebra_simps) done lemma rtranclp_normalize_poly_p_poly_of_mset: \normalize_poly_p\<^sup>*\<^sup>* p q \ polynomial_of_mset p = polynomial_of_mset q\ by (induction rule: rtranclp_induct) (auto simp: normalize_poly_p_poly_of_mset) end text \It would be nice to have the property in the other direction too, but this requires a deep dive into the definitions of polynomials.\ locale poly_embed_bij = poly_embed + fixes V N assumes \_bij: \bij_betw \ V N\ begin definition \' :: \nat \ string\ where \\' = the_inv_into V \\ lemma \'_\[simp]: \x \ V \ \' (\ x) = x\ using \_bij unfolding \'_def by (meson bij_betw_imp_inj_on the_inv_into_f_f) lemma \_\'[simp]: \x \ N \ \ (\' x) = x\ using \_bij unfolding \'_def by (meson f_the_inv_into_f_bij_betw) end end