diff --git a/thys/Affine_Arithmetic/Affine_Form.thy b/thys/Affine_Arithmetic/Affine_Form.thy --- a/thys/Affine_Arithmetic/Affine_Form.thy +++ b/thys/Affine_Arithmetic/Affine_Form.thy @@ -1,1989 +1,2005 @@ section \Affine Form\ theory Affine_Form imports "HOL-Analysis.Multivariate_Analysis" "HOL-Combinatorics.List_Permutation" Affine_Arithmetic_Auxiliarities Executable_Euclidean_Space begin subsection \Auxiliary developments\ lemma sum_list_mono: fixes xs ys::"'a::ordered_ab_group_add list" shows "length xs = length ys \ (\x y. (x, y) \ set (zip xs ys) \ x \ y) \ sum_list xs \ sum_list ys" by (induct xs ys rule: list_induct2) (auto simp: algebra_simps intro: add_mono) lemma fixes xs::"'a::ordered_comm_monoid_add list" shows sum_list_nonneg: "(\x. x \ set xs \ x \ 0) \ sum_list xs \ 0" by (induct xs) (auto intro!: add_nonneg_nonneg) lemma map_filter: "map f (filter (\x. P (f x)) xs) = filter P (map f xs)" by (induct xs) simp_all lemma map_of_zip_upto2_length_eq_nth: assumes "distinct B" assumes "i < length B" shows "(map_of (zip B [0.. (i, a) \ set xs \ (i, b) \ set xs \ a = b" by (metis (lifting) map_of_is_SomeI option.inject) lemma length_filter_snd_zip: "length ys = length xs \ length (filter (p \ snd) (zip ys xs)) = length (filter p xs)" by (induct ys xs rule: list_induct2) (auto ) lemma filter_snd_nth: "length ys = length xs \ n < length (filter p xs) \ snd (filter (p \ snd) (zip ys xs) ! n) = filter p xs ! n" by (induct ys xs arbitrary: n rule: list_induct2) (auto simp: o_def nth_Cons split: nat.split) lemma distinct_map_snd_fst_eqD: "distinct (map snd xs) \ (i, a) \ set xs \ (j, a) \ set xs \ i = j" by (metis Pair_inject inj_on_contraD snd_conv distinct_map) lemma map_of_mapk_inj_on_SomeI: "inj_on f (fst ` (set t)) \ map_of t k = Some x \ map_of (map (case_prod (\k. Pair (f k))) t) (f k) = Some x" by (induct t) (auto simp add: inj_on_def dest!: map_of_SomeD split: if_split_asm) lemma map_abs_nonneg[simp]: fixes xs::"'a::ordered_ab_group_add_abs list" shows "list_all (\x. x \ 0) xs \ map abs xs = xs" by (induct xs) auto lemma the_inv_into_image_eq: "inj_on f A \ Y \ f ` A \ the_inv_into A f ` Y = f -` Y \ A" using f_the_inv_into_f the_inv_into_f_f[where f = f and A = A] by force lemma image_fst_zip: "length ys = length xs \ fst ` set (zip ys xs) = set ys" by (metis dom_map_of_conv_image_fst dom_map_of_zip) lemma inj_on_fst_set_zip_distinct[simp]: "distinct xs \ length xs = length ys \ inj_on fst (set (zip xs ys))" by (force simp add: in_set_zip distinct_conv_nth intro!: inj_onI) lemma mem_greaterThanLessThan_absI: fixes x::real assumes "abs x < 1" shows "x \ {-1 <..< 1}" using assms by (auto simp: abs_real_def split: if_split_asm) lemma minus_one_less_divideI: "b > 0 \ -b < a \ -1 < a / (b::real)" by (auto simp: field_simps) lemma divide_less_oneI: "b > 0 \ b > a \ a / (b::real) < 1" by (auto simp: field_simps) lemma closed_segment_real: fixes a b::real shows "closed_segment a b = (if a \ b then {a .. b} else {b .. a})" (is "_ = ?if") proof safe fix x assume "x \ closed_segment a b" from segment_bound[OF this] show "x \ ?if" by (auto simp: abs_real_def split: if_split_asm) next fix x assume "x \ ?if" thus "x \ closed_segment a b" by (auto simp: closed_segment_def intro!: exI[where x="(x - a)/(b - a)"] simp: divide_simps algebra_simps) qed subsection \Partial Deviations\ typedef (overloaded) 'a pdevs = "{x::nat \ 'a::zero. finite {i. x i \ 0}}" \ \TODO: unify with polynomials\ morphisms pdevs_apply Abs_pdev by (auto intro!: exI[where x="\x. 0"]) setup_lifting type_definition_pdevs lemma pdevs_eqI: "(\i. pdevs_apply x i = pdevs_apply y i) \ x = y" by transfer auto definition pdevs_val :: "(nat \ real) \ 'a::real_normed_vector pdevs \ 'a" where "pdevs_val e x = (\i. e i *\<^sub>R pdevs_apply x i)" definition valuate:: "((nat \ real) \ 'a) \ 'a set" where "valuate x = x ` (UNIV \ {-1 .. 1})" lemma valuate_ex: "x \ valuate f \ (\e. (\i. e i \ {-1 .. 1}) \ x = f e)" unfolding valuate_def by (auto simp add: valuate_def Pi_iff) blast instantiation pdevs :: (equal) equal begin definition equal_pdevs::"'a pdevs \ 'a pdevs \ bool" where "equal_pdevs a b \ a = b" instance proof qed (simp add: equal_pdevs_def) end subsection \Affine Forms\ text \The data structure of affine forms represents particular sets, zonotopes\ type_synonym 'a aform = "'a \ 'a pdevs" subsection \Evaluation, Range, Joint Range\ definition aform_val :: "(nat \ real) \ 'a::real_normed_vector aform \ 'a" where "aform_val e X = fst X + pdevs_val e (snd X)" definition Affine :: "'a::real_normed_vector aform \ 'a set" where "Affine X = valuate (\e. aform_val e X)" definition Joints :: "'a::real_normed_vector aform list \ 'a list set" where "Joints XS = valuate (\e. map (aform_val e) XS)" lemma Joints_nthE: assumes "zs \ Joints ZS" obtains e where "\i. i < length zs \ zs ! i = aform_val e (ZS ! i)" "\i. e i \ {-1..1}" using assms by atomize_elim (auto simp: Joints_def Pi_iff valuate_ex) lemma Joints_mapE: assumes "ys \ Joints YS" obtains e where "ys = map (\x. aform_val e x) YS" "\i. e i \ {-1 .. 1}" using assms by (force simp: Joints_def valuate_def) lemma zipped_subset_mapped_Elem: assumes "xs = map (aform_val e) XS" assumes e: "\i. e i \ {-1 .. 1}" assumes [simp]: "length xs = length XS" assumes [simp]: "length ys = length YS" assumes "set (zip ys YS) \ set (zip xs XS)" shows "ys = map (aform_val e) YS" proof - from assms have ys: "\i. i < length xs \ xs ! i = aform_val e (XS ! i)" by auto from assms have set_eq: "{(ys ! i, YS ! i) |i. i < length ys \ i < length YS} \ {(xs ! i, XS ! i) |i. i < length xs \ i < length XS}" using assms(2) by (auto simp: set_zip) hence "\ij YS ! i = XS ! j" by auto then obtain j where j: "\i. i < length YS \ ys ! i = xs ! (j i)" "\i. i < length YS \ YS ! i = XS ! (j i)" "\i. i < length YS \ j i < length XS" by metis show ?thesis using assms by (auto simp: Joints_def j ys intro!: exI[where x=e] nth_equalityI) qed lemma Joints_set_zip_subset: assumes "xs \ Joints XS" assumes "length xs = length XS" assumes "length ys = length YS" assumes "set (zip ys YS) \ set (zip xs XS)" shows "ys \ Joints YS" proof - from Joints_mapE assms obtain e where ys: "xs = map (\x. aform_val e x) XS" and e: "\i. e i \ {-1 .. 1}" by blast show "ys \ Joints YS" using e zipped_subset_mapped_Elem[OF ys e assms(2-4)] by (auto simp: Joints_def valuate_def intro!: exI[where x=e]) qed lemma Joints_set_zip: assumes "ys \ Joints YS" assumes "length xs = length XS" assumes "length YS = length XS" assumes sets_eq: "set (zip xs XS) = set (zip ys YS)" shows "xs \ Joints XS" proof - from assms have "length ys = length YS" by (auto simp: Joints_def valuate_def) from assms(1) this assms(2) show ?thesis by (rule Joints_set_zip_subset) (simp add: assms) qed definition Joints2 :: "'a::real_normed_vector aform list \'b::real_normed_vector aform \ ('a list \ 'b) set" where "Joints2 XS Y = valuate (\e. (map (aform_val e) XS, aform_val e Y))" lemma Joints2E: assumes "zs_y \ Joints2 ZS Y" obtains e where "\i. i < length (fst zs_y) \ (fst zs_y) ! i = aform_val e (ZS ! i)" "snd (zs_y) = aform_val e Y" "\i. e i \ {-1..1}" using assms by atomize_elim (auto simp: Joints2_def Pi_iff valuate_ex) lemma nth_in_AffineI: assumes "xs \ Joints XS" assumes "i < length XS" shows "xs ! i \ Affine (XS ! i)" using assms by (force simp: Affine_def Joints_def valuate_def) lemma Cons_nth_in_Joints1: assumes "xs \ Joints XS" assumes "i < length XS" shows "((xs ! i) # xs) \ Joints ((XS ! i) # XS)" using assms by (force simp: Joints_def valuate_def) lemma Cons_nth_in_Joints2: assumes "xs \ Joints XS" assumes "i < length XS" assumes "j < length XS" shows "((xs ! i) #(xs ! j) # xs) \ Joints ((XS ! i)#(XS ! j) # XS)" using assms by (force simp: Joints_def valuate_def) lemma Joints_swap: "x#y#xs\Joints (X#Y#XS) \ y#x#xs \ Joints (Y#X#XS)" by (force simp: Joints_def valuate_def) lemma Joints_swap_Cons_append: "length xs = length XS \ x#ys@xs\Joints (X#YS@XS) \ ys@x#xs \ Joints (YS@X#XS)" by (auto simp: Joints_def valuate_def) lemma Joints_ConsD: "x#xs\Joints (X#XS) \ xs \ Joints XS" by (force simp: Joints_def valuate_def) lemma Joints_appendD1: "ys@xs\Joints (YS@XS) \ length xs = length XS \ xs \ Joints XS" by (force simp: Joints_def valuate_def) lemma Joints_appendD2: "ys@xs\Joints (YS@XS) \ length ys = length YS \ ys \ Joints YS" by (force simp: Joints_def valuate_def) lemma Joints_imp_length_eq: "xs \ Joints XS \ length xs = length XS" by (auto simp: Joints_def valuate_def) lemma Joints_rotate[simp]: "xs@[x] \ Joints (XS @[X]) \ x#xs \ Joints (X#XS)" by (auto simp: Joints_def valuate_def) subsection \Domain\ definition "pdevs_domain x = {i. pdevs_apply x i \ 0}" lemma finite_pdevs_domain[intro, simp]: "finite (pdevs_domain x)" unfolding pdevs_domain_def by transfer lemma in_pdevs_domain[simp]: "i \ pdevs_domain x \ pdevs_apply x i \ 0" by (auto simp: pdevs_domain_def) subsection \Least Fresh Index\ definition degree::"'a::real_vector pdevs \ nat" where "degree x = (LEAST i. \j\i. pdevs_apply x j = 0)" lemma degree[rule_format, intro, simp]: shows "\j\degree x. pdevs_apply x j = 0" unfolding degree_def proof (rule LeastI_ex) have "\j. j > Max (pdevs_domain x) \ j \ (pdevs_domain x)" by (metis Max_less_iff all_not_in_conv less_irrefl_nat finite_pdevs_domain) then show "\xa. \j\xa. pdevs_apply x j = 0" by (auto intro!: exI[where x="Max (pdevs_domain x) + 1"]) qed lemma degree_le: assumes d: "\j \ d. pdevs_apply x j = 0" shows "degree x \ d" unfolding degree_def by (rule Least_le) (rule d) lemma degree_gt: "pdevs_apply x j \ 0 \ degree x > j" by auto lemma pdevs_val_pdevs_domain: "pdevs_val e X = (\i\pdevs_domain X. e i *\<^sub>R pdevs_apply X i)" by (auto simp: pdevs_val_def intro!: suminf_finite) lemma pdevs_val_sum_le: "degree X \ d \ pdevs_val e X = (\i < d. e i *\<^sub>R pdevs_apply X i)" by (force intro!: degree_gt sum.mono_neutral_cong_left simp: pdevs_val_pdevs_domain) lemmas pdevs_val_sum = pdevs_val_sum_le[OF order_refl] lemma pdevs_val_zero[simp]: "pdevs_val (\_. 0) x = 0" by (auto simp: pdevs_val_sum) lemma degree_eqI: assumes "pdevs_apply x d \ 0" assumes "\j. j > d \ pdevs_apply x j = 0" shows "degree x = Suc d" unfolding eq_iff by (auto intro!: degree_gt degree_le assms simp: Suc_le_eq) lemma finite_degree_nonzero[intro, simp]: "finite {i. pdevs_apply x i \ 0}" by transfer (auto simp: vimage_def Collect_neg_eq) lemma degree_eq_Suc_max: "degree x = (if (\i. pdevs_apply x i = 0) then 0 else Suc (Max {i. pdevs_apply x i \ 0}))" proof - { assume "\i. pdevs_apply x i = 0" hence ?thesis by auto (metis degree_le le_0_eq) } moreover { fix i assume "pdevs_apply x i \ 0" hence ?thesis using Max_in[OF finite_degree_nonzero, of x] by (auto intro!: degree_eqI) (metis Max.coboundedI[OF finite_degree_nonzero] in_pdevs_domain le_eq_less_or_eq less_asym pdevs_domain_def) } ultimately show ?thesis by blast qed lemma pdevs_val_degree_cong: assumes "b = d" assumes "\i. i < degree b \ a i = c i" shows "pdevs_val a b = pdevs_val c d" using assms by (auto simp: pdevs_val_sum) abbreviation degree_aform::"'a::real_vector aform \ nat" where "degree_aform X \ degree (snd X)" lemma degree_cong: "(\i. (pdevs_apply x i = 0) = (pdevs_apply y i = 0)) \ degree x = degree y" unfolding degree_def by auto lemma Least_True_nat[intro, simp]: "(LEAST i::nat. True) = 0" by (metis (lifting) One_nat_def less_one not_less_Least not_less_eq) lemma sorted_list_of_pdevs_domain_eq: "sorted_list_of_set (pdevs_domain X) = filter ((\) 0 o pdevs_apply X) [0..x. x", simplified]) subsection \Total Deviation\ definition tdev::"'a::ordered_euclidean_space pdevs \ 'a" where "tdev x = (\ipdevs_apply x i\)" lemma abs_pdevs_val_le_tdev: "e \ UNIV \ {-1 .. 1} \ \pdevs_val e x\ \ tdev x" by (force simp: pdevs_val_sum tdev_def abs_scaleR Pi_iff intro!: order_trans[OF sum_abs] sum_mono scaleR_left_le_one_le intro: abs_leI) subsection \Binary Pointwise Operations\ definition binop_pdevs_raw::"('a::zero \ 'b::zero \ 'c::zero) \ (nat \ 'a) \ (nat \ 'b) \ nat \ 'c" where "binop_pdevs_raw f x y i = (if x i = 0 \ y i = 0 then 0 else f (x i) (y i))" lemma nonzeros_binop_pdevs_subset: "{i. binop_pdevs_raw f x y i \ 0} \ {i. x i \ 0} \ {i. y i \ 0}" by (auto simp: binop_pdevs_raw_def) lift_definition binop_pdevs:: "('a \ 'b \ 'c) \ 'a::zero pdevs \ 'b::zero pdevs \ 'c::zero pdevs" is binop_pdevs_raw using nonzeros_binop_pdevs_subset by (rule finite_subset) auto lemma pdevs_apply_binop_pdevs[simp]: "pdevs_apply (binop_pdevs f x y) i = (if pdevs_apply x i = 0 \ pdevs_apply y i = 0 then 0 else f (pdevs_apply x i) (pdevs_apply y i))" by transfer (auto simp: binop_pdevs_raw_def) subsection \Addition\ definition add_pdevs::"'a::real_vector pdevs \ 'a pdevs \ 'a pdevs" where "add_pdevs = binop_pdevs (+)" lemma pdevs_apply_add_pdevs[simp]: "pdevs_apply (add_pdevs X Y) n = pdevs_apply X n + pdevs_apply Y n" by (auto simp: add_pdevs_def) lemma pdevs_val_add_pdevs[simp]: fixes x y::"'a::euclidean_space" shows "pdevs_val e (add_pdevs X Y) = pdevs_val e X + pdevs_val e Y" proof - let ?sum = "\m X. \i < m. e i *\<^sub>R pdevs_apply X i" let ?m = "max (degree X) (degree Y)" have "pdevs_val e X + pdevs_val e Y = ?sum (degree X) X + ?sum (degree Y) Y" by (simp add: pdevs_val_sum) also have "?sum (degree X) X = ?sum ?m X" by (rule sum.mono_neutral_cong_left) auto also have "?sum (degree Y) Y = ?sum ?m Y" by (rule sum.mono_neutral_cong_left) auto also have "?sum ?m X + ?sum ?m Y = (\i < ?m. e i *\<^sub>R (pdevs_apply X i + pdevs_apply Y i))" by (simp add: scaleR_right_distrib sum.distrib) also have "\ = (\i. e i *\<^sub>R (pdevs_apply X i + pdevs_apply Y i))" by (rule suminf_finite[symmetric]) auto also have "\ = pdevs_val e (add_pdevs X Y)" by (simp add: pdevs_val_def) finally show "pdevs_val e (add_pdevs X Y) = pdevs_val e X + pdevs_val e Y" by simp qed subsection \Total Deviation\ lemma tdev_eq_zero_iff: fixes X::"real pdevs" shows "tdev X = 0 \ (\e. pdevs_val e X = 0)" by (force simp add: pdevs_val_sum tdev_def sum_nonneg_eq_0_iff dest!: spec[where x="\i. if pdevs_apply X i \ 0 then 1 else -1"] split: if_split_asm) lemma tdev_nonneg[intro, simp]: "tdev X \ 0" by (auto simp: tdev_def) lemma tdev_nonpos_iff[simp]: "tdev X \ 0 \ tdev X = 0" by (auto simp: order.antisym) subsection \Unary Operations\ definition unop_pdevs_raw:: "('a::zero \ 'b::zero) \ (nat \ 'a) \ nat \ 'b" where "unop_pdevs_raw f x i = (if x i = 0 then 0 else f (x i))" lemma nonzeros_unop_pdevs_subset: "{i. unop_pdevs_raw f x i \ 0} \ {i. x i \ 0}" by (auto simp: unop_pdevs_raw_def) lift_definition unop_pdevs:: "('a \ 'b) \ 'a::zero pdevs \ 'b::zero pdevs" is unop_pdevs_raw using nonzeros_unop_pdevs_subset by (rule finite_subset) auto lemma pdevs_apply_unop_pdevs[simp]: "pdevs_apply (unop_pdevs f x) i = (if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i))" by transfer (auto simp: unop_pdevs_raw_def) lemma pdevs_domain_unop_linear: assumes "linear f" shows "pdevs_domain (unop_pdevs f x) \ pdevs_domain x" proof - interpret f: linear f by fact show ?thesis by (auto simp: f.zero) qed lemma pdevs_val_unop_linear: assumes "linear f" shows "pdevs_val e (unop_pdevs f x) = f (pdevs_val e x)" proof - interpret f: linear f by fact have *: "\i. (if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i)) = f (pdevs_apply x i)" by (auto simp: f.zero) have "pdevs_val e (unop_pdevs f x) = (\i\pdevs_domain (unop_pdevs f x). e i *\<^sub>R f (pdevs_apply x i))" by (auto simp add: pdevs_val_pdevs_domain *) also have "\ = (\xa\pdevs_domain x. e xa *\<^sub>R f (pdevs_apply x xa))" by (auto intro!: sum.mono_neutral_cong_left) also have "\ = f (pdevs_val e x)" by (auto simp add: pdevs_val_pdevs_domain f.sum f.scaleR) finally show ?thesis . qed subsection \Pointwise Scaling of Partial Deviations\ definition scaleR_pdevs::"real \ 'a::real_vector pdevs \ 'a pdevs" where "scaleR_pdevs r x = unop_pdevs ((*\<^sub>R) r) x" lemma pdevs_apply_scaleR_pdevs[simp]: "pdevs_apply (scaleR_pdevs x Y) n = x *\<^sub>R pdevs_apply Y n" by (auto simp: scaleR_pdevs_def) lemma degree_scaleR_pdevs[simp]: "degree (scaleR_pdevs r x) = (if r = 0 then 0 else degree x)" unfolding degree_def by auto lemma pdevs_val_scaleR_pdevs[simp]: fixes x::real and Y::"'a::real_normed_vector pdevs" shows "pdevs_val e (scaleR_pdevs x Y) = x *\<^sub>R pdevs_val e Y" by (auto simp: pdevs_val_sum scaleR_sum_right ac_simps) subsection \Partial Deviations Scale Pointwise\ definition pdevs_scaleR::"real pdevs \ 'a::real_vector \ 'a pdevs" where "pdevs_scaleR r x = unop_pdevs (\r. r *\<^sub>R x) r" lemma pdevs_apply_pdevs_scaleR[simp]: "pdevs_apply (pdevs_scaleR X y) n = pdevs_apply X n *\<^sub>R y" by (auto simp: pdevs_scaleR_def) lemma degree_pdevs_scaleR[simp]: "degree (pdevs_scaleR r x) = (if x = 0 then 0 else degree r)" unfolding degree_def by auto lemma pdevs_val_pdevs_scaleR[simp]: fixes X::"real pdevs" and y::"'a::real_normed_vector" shows "pdevs_val e (pdevs_scaleR X y) = pdevs_val e X *\<^sub>R y" by (auto simp: pdevs_val_sum scaleR_sum_left) subsection \Pointwise Unary Minus\ definition uminus_pdevs::"'a::real_vector pdevs \ 'a pdevs" where "uminus_pdevs = unop_pdevs uminus" lemma pdevs_apply_uminus_pdevs[simp]: "pdevs_apply (uminus_pdevs x) = - pdevs_apply x" by (auto simp: uminus_pdevs_def) lemma degree_uminus_pdevs[simp]: "degree (uminus_pdevs x) = degree x" by (rule degree_cong) simp lemma pdevs_val_uminus_pdevs[simp]: "pdevs_val e (uminus_pdevs x) = - pdevs_val e x" unfolding pdevs_val_sum by (auto simp: sum_negf) definition "uminus_aform X = (- fst X, uminus_pdevs (snd X))" lemma fst_uminus_aform[simp]: "fst (uminus_aform Y) = - fst Y" by (simp add: uminus_aform_def) lemma aform_val_uminus_aform[simp]: "aform_val e (uminus_aform X) = - aform_val e X" by (auto simp: uminus_aform_def aform_val_def) subsection \Constant\ lift_definition zero_pdevs::"'a::zero pdevs" is "\_. 0" by simp lemma pdevs_apply_zero_pdevs[simp]: "pdevs_apply zero_pdevs i = 0" by transfer simp lemma pdevs_val_zero_pdevs[simp]: "pdevs_val e zero_pdevs = 0" by (auto simp: pdevs_val_def) definition "num_aform f = (f, zero_pdevs)" subsection \Inner Product\ definition pdevs_inner::"'a::euclidean_space pdevs \ 'a \ real pdevs" where "pdevs_inner x b = unop_pdevs (\x. x \ b) x" lemma pdevs_apply_pdevs_inner[simp]: "pdevs_apply (pdevs_inner p a) i = pdevs_apply p i \ a" by (simp add: pdevs_inner_def) lemma pdevs_val_pdevs_inner[simp]: "pdevs_val e (pdevs_inner p a) = pdevs_val e p \ a" by (auto simp add: inner_sum_left pdevs_val_pdevs_domain intro!: sum.mono_neutral_cong_left) definition inner_aform::"'a::euclidean_space aform \ 'a \ real aform" where "inner_aform X b = (fst X \ b, pdevs_inner (snd X) b)" subsection \Inner Product Pair\ definition inner2::"'a::euclidean_space \ 'a \ 'a \ real*real" where "inner2 x n l = (x \ n, x \ l)" definition pdevs_inner2::"'a::euclidean_space pdevs \ 'a \ 'a \ (real*real) pdevs" where "pdevs_inner2 X n l = unop_pdevs (\x. inner2 x n l) X" lemma pdevs_apply_pdevs_inner2[simp]: "pdevs_apply (pdevs_inner2 p a b) i = (pdevs_apply p i \ a, pdevs_apply p i \ b)" by (simp add: pdevs_inner2_def inner2_def zero_prod_def) definition inner2_aform::"'a::euclidean_space aform \ 'a \ 'a \ (real*real) aform" where "inner2_aform X a b = (inner2 (fst X) a b, pdevs_inner2 (snd X) a b)" lemma linear_inner2[intro, simp]: "linear (\x. inner2 x n i)" by unfold_locales (auto simp: inner2_def algebra_simps) lemma aform_val_inner2_aform[simp]: "aform_val e (inner2_aform Z n i) = inner2 (aform_val e Z) n i" proof - have "aform_val e (inner2_aform Z n i) = inner2 (fst Z) n i + inner2 (pdevs_val e (snd Z)) n i" by (auto simp: aform_val_def inner2_aform_def pdevs_inner2_def pdevs_val_unop_linear) also have "\ = inner2 (aform_val e Z) n i" by (simp add: inner2_def algebra_simps aform_val_def) finally show ?thesis . qed subsection \Update\ lemma pdevs_val_upd[simp]: "pdevs_val (e(n := e')) X = pdevs_val e X - e n * pdevs_apply X n + e' * pdevs_apply X n" unfolding pdevs_val_def by (subst suminf_finite[OF finite.insertI[OF finite_degree_nonzero], of n X], auto simp: pdevs_val_def sum.insert_remove)+ lemma nonzeros_fun_upd: "{i. (f(n := a)) i \ 0} \ {i. f i \ 0} \ {n}" by (auto split: if_split_asm) lift_definition pdev_upd::"'a::real_vector pdevs \ nat \ 'a \ 'a pdevs" is "\x n a. x(n:=a)" by (rule finite_subset[OF nonzeros_fun_upd]) simp lemma pdevs_apply_pdev_upd[simp]: "pdevs_apply (pdev_upd X n x) = (pdevs_apply X)(n:=x)" by transfer simp lemma pdevs_val_pdev_upd[simp]: "pdevs_val e (pdev_upd X n x) = pdevs_val e X + e n *\<^sub>R x - e n *\<^sub>R pdevs_apply X n" unfolding pdevs_val_def by (subst suminf_finite[OF finite.insertI[OF finite_degree_nonzero], of n X], auto simp: pdevs_val_def sum.insert_remove)+ lemma degree_pdev_upd: assumes "x = 0 \ pdevs_apply X n = 0" shows "degree (pdev_upd X n x) = degree X" using assms by (auto intro!: degree_cong split: if_split_asm) lemma degree_pdev_upd_le: assumes "degree X \ n" shows "degree (pdev_upd X n x) \ Suc n" using assms by (auto intro!: degree_le) subsection \Inf/Sup\ definition "Inf_aform X = fst X - tdev (snd X)" definition "Sup_aform X = fst X + tdev (snd X)" lemma Inf_aform: assumes "e \ UNIV \ {-1 .. 1}" shows "Inf_aform X \ aform_val e X" using order_trans[OF abs_ge_minus_self abs_pdevs_val_le_tdev[OF assms]] by (auto simp: Inf_aform_def aform_val_def minus_le_iff) lemma Sup_aform: assumes "e \ UNIV \ {-1 .. 1}" shows "aform_val e X \ Sup_aform X" using order_trans[OF abs_ge_self abs_pdevs_val_le_tdev[OF assms]] by (auto simp: Sup_aform_def aform_val_def) subsection \Minkowski Sum\ definition msum_pdevs_raw::"nat\(nat \ 'a::real_vector)\(nat \ 'a)\(nat\'a)" where "msum_pdevs_raw n x y i = (if i < n then x i else y (i - n))" lemma nonzeros_msum_pdevs_raw: "{i. msum_pdevs_raw n f g i \ 0} = ({0.. {i. f i \ 0}) \ (+) n ` ({i. g i \ 0})" by (force simp: msum_pdevs_raw_def not_less split: if_split_asm) lift_definition msum_pdevs::"nat\'a::real_vector pdevs\'a pdevs\'a pdevs" is msum_pdevs_raw unfolding nonzeros_msum_pdevs_raw by simp lemma pdevs_apply_msum_pdevs: "pdevs_apply (msum_pdevs n f g) i = (if i < n then pdevs_apply f i else pdevs_apply g (i - n))" by transfer (auto simp: msum_pdevs_raw_def) lemma degree_least_nonzero: assumes "degree f \ 0" shows "pdevs_apply f (degree f - 1) \ 0" proof assume H: "pdevs_apply f (degree f - 1) = 0" { fix j assume "j\degree f - 1" with H have "pdevs_apply f j = 0" by (cases "degree f - 1 = j") auto } from degree_le[rule_format, OF this] have "degree f \ degree f - 1" by blast with assms show False by simp qed lemma degree_leI: assumes "(\i. pdevs_apply y i = 0 \ pdevs_apply x i = 0)" shows "degree x \ degree y" proof cases assume "degree x \ 0" from degree_least_nonzero[OF this] have "pdevs_apply y (degree x - 1) \ 0" by (auto simp: assms split: if_split_asm) from degree_gt[OF this] show ?thesis by simp qed simp lemma degree_msum_pdevs_ge1: shows "degree f \ n \ degree f \ degree (msum_pdevs n f g)" by (rule degree_leI) (auto simp: pdevs_apply_msum_pdevs split: if_split_asm) lemma degree_msum_pdevs_ge2: assumes "degree f \ n" shows "degree g \ degree (msum_pdevs n f g) - n" proof cases assume "degree g \ 0" hence "pdevs_apply g (degree g - 1) \ 0" by (rule degree_least_nonzero) hence "pdevs_apply (msum_pdevs n f g) (n + degree g - 1) \ 0" using assms by (auto simp: pdevs_apply_msum_pdevs) from degree_gt[OF this] show ?thesis by simp qed simp lemma degree_msum_pdevs_le: shows "degree (msum_pdevs n f g) \ n + degree g" by (auto intro!: degree_le simp: pdevs_apply_msum_pdevs) lemma sum_msum_pdevs_cases: assumes "degree f \ n" assumes [simp]: "\i. e i 0 = 0" shows "(\i i i i\{.. {i. i < n}. e i (pdevs_apply f i)) + (\i\{.. - {i. i < n}. e i (pdevs_apply g (i - n)))" (is "_ = ?sum_f + ?sum_g") by (simp add: sum.If_cases if_distrib) also have "?sum_f = (\i = 0..i\{0 + n.. = (\i = 0.. = (\i = 0.. n \ tdev (msum_pdevs n f g) = tdev f + tdev g" by (auto simp: tdev_def pdevs_apply_msum_pdevs intro!: sum_msum_pdevs_cases) lemma pdevs_val_msum_pdevs: "degree f \ n \ pdevs_val e (msum_pdevs n f g) = pdevs_val e f + pdevs_val (\i. e (i + n)) g" by (auto simp: pdevs_val_sum pdevs_apply_msum_pdevs intro!: sum_msum_pdevs_cases) definition msum_aform::"nat \ 'a::real_vector aform \ 'a aform \ 'a aform" where "msum_aform n f g = (fst f + fst g, msum_pdevs n (snd f) (snd g))" lemma fst_msum_aform[simp]: "fst (msum_aform n f g) = fst f + fst g" by (simp add: msum_aform_def) lemma snd_msum_aform[simp]: "snd (msum_aform n f g) = msum_pdevs n (snd f) (snd g)" by (simp add: msum_aform_def) lemma finite_nonzero_summable: "finite {i. f i \ 0} \ summable f" by (auto intro!: sums_summable sums_finite) lemma aform_val_msum_aform: assumes "degree_aform f \ n" shows "aform_val e (msum_aform n f g) = aform_val e f + aform_val (\i. e (i + n)) g" using assms by (auto simp: pdevs_val_msum_pdevs aform_val_def) lemma Inf_aform_msum_aform: "degree_aform X \ n \ Inf_aform (msum_aform n X Y) = Inf_aform X + Inf_aform Y" by (simp add: Inf_aform_def tdev_msum_pdevs) lemma Sup_aform_msum_aform: "degree_aform X \ n \ Sup_aform (msum_aform n X Y) = Sup_aform X + Sup_aform Y" by (simp add: Sup_aform_def tdev_msum_pdevs) definition "independent_from d Y = msum_aform d (0, zero_pdevs) Y" definition "independent_aform X Y = independent_from (degree_aform X) Y" lemma degree_zero_pdevs[simp]: "degree zero_pdevs = 0" by (metis degree_least_nonzero pdevs_apply_zero_pdevs) lemma independent_aform_Joints: assumes "x \ Affine X" assumes "y \ Affine Y" shows "[x, y] \ Joints [X, independent_aform X Y]" using assms unfolding Affine_def valuate_def Joints_def apply safe subgoal premises prems for e ea using prems by (intro image_eqI[where x="\i. if i < degree_aform X then e i else ea (i - degree_aform X)"]) (auto simp: aform_val_def pdevs_val_msum_pdevs Pi_iff independent_aform_def independent_from_def intro!: pdevs_val_degree_cong) done lemma msum_aform_Joints: assumes "d \ degree_aform X" assumes "\X. X \ set XS \ d \ degree_aform X" assumes "(x#xs) \ Joints (X#XS)" assumes "y \ Affine Y" shows "((x + y)#x#xs) \ Joints (msum_aform d X Y#X#XS)" using assms unfolding Joints_def valuate_def Affine_def proof (safe, goal_cases) case (1 e ea a b zs) then show ?case by (intro image_eqI[where x = "\i. if i < d then e i else ea (i - d)"]) (force simp: aform_val_def pdevs_val_msum_pdevs intro!: intro!: pdevs_val_degree_cong)+ qed lemma Joints_msum_aform: assumes "d \ degree_aform X" assumes "\Y. Y \ set YS \ d \ degree_aform Y" shows "Joints (msum_aform d X Y#YS) = {((x + y)#ys) |x y ys. y \ Affine Y \ x#ys \ Joints (X#YS)}" unfolding Affine_def valuate_def Joints_def proof (safe, goal_cases) case (1 x e) thus ?case using assms by (intro exI[where x = "aform_val e X"] exI[where x = "aform_val ((\i. e (i + d))) Y"]) (auto simp add: aform_val_def pdevs_val_msum_pdevs) next case (2 x xa y ys e ea) thus ?case using assms by (intro image_eqI[where x="\i. if i < d then ea i else e (i - d)"]) (force simp: aform_val_def pdevs_val_msum_pdevs Pi_iff intro!: pdevs_val_degree_cong)+ qed lemma Joints_singleton_image: "Joints [x] = (\x. [x]) ` Affine x" by (auto simp: Joints_def Affine_def valuate_def) lemma Collect_extract_image: "{g (f x y) |x y. P x y} = g ` {f x y |x y. P x y}" by auto lemma inj_Cons: "inj (\x. x#xs)" by (auto intro!: injI) lemma Joints_Nil[simp]: "Joints [] = {[]}" by (force simp: Joints_def valuate_def) lemma msum_pdevs_zero_ident[simp]: "msum_pdevs 0 zero_pdevs x = x" by transfer (auto simp: msum_pdevs_raw_def) lemma msum_aform_zero_ident[simp]: "msum_aform 0 (0, zero_pdevs) x = x" by (simp add: msum_aform_def) lemma mem_Joints_singleton: "(x \ Joints [X]) = (\y. x = [y] \ y \ Affine X)" by (auto simp: Affine_def valuate_def Joints_def) lemma singleton_mem_Joints[simp]: "[x] \ Joints [X] \ x \ Affine X" by (auto simp: mem_Joints_singleton) lemma msum_aform_Joints_without_first: assumes "d \ degree_aform X" assumes "\X. X \ set XS \ d \ degree_aform X" assumes "(x#xs) \ Joints (X#XS)" assumes "y \ Affine Y" assumes "z = x + y" shows "z#xs \ Joints (msum_aform d X Y#XS)" unfolding \z = x + y\ using msum_aform_Joints[OF assms(1-4)] by (force simp: Joints_def valuate_def) lemma Affine_msum_aform: assumes "d \ degree_aform X" shows "Affine (msum_aform d X Y) = {x + y |x y. x \ Affine X \ y \ Affine Y}" using Joints_msum_aform[OF assms, of Nil Y, simplified, unfolded mem_Joints_singleton] by (auto simp add: Joints_singleton_image Collect_extract_image[where g="\x. [x]"] inj_image_eq_iff[OF inj_Cons] ) lemma Affine_zero_pdevs[simp]: "Affine (0, zero_pdevs) = {0}" by (force simp: Affine_def valuate_def aform_val_def) lemma Affine_independent_aform: "Affine (independent_aform X Y) = Affine Y" by (auto simp: independent_aform_def independent_from_def Affine_msum_aform) lemma abs_diff_eq1: fixes l u::"'a::ordered_euclidean_space" shows "l \ u \ \u - l\ = u - l" by (metis abs_of_nonneg diff_add_cancel le_add_same_cancel2) lemma compact_sum: fixes f :: "'a \ 'b::topological_space \ 'c::real_normed_vector" assumes "finite I" assumes "\i. i \ I \ compact (S i)" assumes "\i. i \ I \ continuous_on (S i) (f i)" assumes "I \ J" shows "compact {\i\I. f i (x i) | x. x \ Pi J S}" using assms proof (induct I) case empty thus ?case proof (cases "\x. x \ Pi J S") case False hence *: "{\i\{}. f i (x i) |x. x \ Pi J S} = {}" by (auto simp: Pi_iff) show ?thesis unfolding * by simp qed auto next case (insert a I) hence "{\i\insert a I. f i (xa i) |xa. xa \ Pi J S} = {x + y |x y. x \ f a ` S a \ y \ {\i\I. f i (x i) |x. x \ Pi J S}}" proof safe fix s x assume "s \ S a" "x \ Pi J S" thus "\xa. f a s + (\i\I. f i (x i)) = (\i\insert a I. f i (xa i)) \ xa \ Pi J S" using insert by (auto intro!: exI[where x="x(a:=s)"] sum.cong) qed force also have "compact \" using insert by (intro compact_sums) (auto intro!: compact_continuous_image) finally show ?case . qed lemma compact_Affine: fixes X::"'a::ordered_euclidean_space aform" shows "compact (Affine X)" proof - have "Affine X = {x + y|x y. x \ {fst X} \ y \ {(\i \ {0..R pdevs_apply (snd X) i) | e. e \ UNIV \ {-1 .. 1}}}" by (auto simp: Affine_def valuate_def aform_val_def pdevs_val_sum atLeast0LessThan) also have "compact \" by (rule compact_sums) (auto intro!: compact_sum continuous_intros) finally show ?thesis . qed lemma Joints2_JointsI: "(xs, x) \ Joints2 XS X \ x#xs \ Joints (X#XS)" by (auto simp: Joints_def Joints2_def valuate_def) subsection \Splitting\ definition "split_aform X i = (let xi = pdevs_apply (snd X) i /\<^sub>R 2 in ((fst X - xi, pdev_upd (snd X) i xi), (fst X + xi, pdev_upd (snd X) i xi)))" lemma split_aformE: assumes "e \ UNIV \ {-1 .. 1}" assumes "x = aform_val e X" obtains err where "x = aform_val (e(i:=err)) (fst (split_aform X i))" "err \ {-1 .. 1}" | err where "x = aform_val (e(i:=err)) (snd (split_aform X i))" "err \ {-1 .. 1}" proof (atomize_elim) let ?thesis = "(\err. x = aform_val (e(i := err)) (fst (split_aform X i)) \ err \ {- 1..1}) \ (\err. x = aform_val (e(i := err)) (snd (split_aform X i)) \ err \ {- 1..1})" { assume "pdevs_apply (snd X) i = 0" hence "X = fst (split_aform X i)" by (auto simp: split_aform_def intro!: prod_eqI pdevs_eqI) with assms have ?thesis by (auto intro!: exI[where x="e i"]) } moreover { assume "pdevs_apply (snd X) i \ 0" hence [simp]: "degree_aform X > i" by (rule degree_gt) note assms(2) also have "aform_val e X = fst X + (\iR pdevs_apply (snd X) i)" by (simp add: aform_val_def pdevs_val_sum) also have rewr: "{.. {i}" by auto have "(\iR pdevs_apply (snd X) i) = (\i \ {0..R pdevs_apply (snd X) i) + e i *\<^sub>R pdevs_apply (snd X) i" by (subst rewr, subst sum.union_disjoint) auto finally have "x = fst X + \" . hence "x = aform_val (e(i:=2 * e i - 1)) (snd (split_aform X i))" "x = aform_val (e(i:=2 * e i + 1)) (fst (split_aform X i))" by (auto simp: aform_val_def split_aform_def Let_def pdevs_val_sum atLeast0LessThan Diff_eq degree_pdev_upd if_distrib sum.If_cases field_simps scaleR_left_distrib[symmetric]) moreover have "2 * e i - 1 \ {-1 .. 1} \ 2 * e i + 1 \ {-1 .. 1}" using assms by (auto simp: not_le Pi_iff dest!: spec[where x=i]) ultimately have ?thesis by blast } ultimately show ?thesis by blast qed lemma pdevs_val_add: "pdevs_val (\i. e i + f i) xs = pdevs_val e xs + pdevs_val f xs" by (auto simp: pdevs_val_pdevs_domain algebra_simps sum.distrib) lemma pdevs_val_minus: "pdevs_val (\i. e i - f i) xs = pdevs_val e xs - pdevs_val f xs" by (auto simp: pdevs_val_pdevs_domain algebra_simps sum_subtractf) lemma pdevs_val_cmul: "pdevs_val (\i. u * e i) xs = u *\<^sub>R pdevs_val e xs" by (auto simp: pdevs_val_pdevs_domain scaleR_sum_right) lemma atLeastAtMost_absI: "- a \ a \ \x::real\ \ \a\ \ x \ atLeastAtMost (- a) a" by auto lemma divide_atLeastAtMost_1_absI: "\x::real\ \ \a\ \ x/a \ {-1 .. 1}" by (intro atLeastAtMost_absI) (auto simp: divide_le_eq_1) lemma convex_scaleR_aux: "u + v = 1 \ u *\<^sub>R x + v *\<^sub>R x = (x::'a::real_vector)" by (metis scaleR_add_left scaleR_one) lemma convex_mult_aux: "u + v = 1 \ u * x + v * x = (x::real)" using convex_scaleR_aux[of u v x] by simp lemma convex_Affine: "convex (Affine X)" proof (rule convexI) fix x y::'a and u v::real assume "x \ Affine X" "y \ Affine X" and convex: "0 \ u" "0 \ v" "u + v = 1" then obtain e f where x: "x = aform_val e X" "e \ UNIV \ {-1 .. 1}" and y: "y = aform_val f X" "f \ UNIV \ {-1 .. 1}" by (auto simp: Affine_def valuate_def) let ?conv = "\i. u * e i + v * f i" { fix i have "\?conv i\ \ u * \e i\ + v * \f i\" using convex by (intro order_trans[OF abs_triangle_ineq]) (simp add: abs_mult) also have "\ \ 1" using convex x y by (intro convex_bound_le) (auto simp: Pi_iff abs_real_def) finally have "?conv i \ 1" "-1 \ ?conv i" by (auto simp: abs_real_def split: if_split_asm) } thus "u *\<^sub>R x + v *\<^sub>R y \ Affine X" using convex x y by (auto simp: Affine_def valuate_def aform_val_def pdevs_val_add pdevs_val_cmul algebra_simps convex_scaleR_aux intro!: image_eqI[where x="?conv"]) qed lemma segment_in_aform_val: assumes "e \ UNIV \ {-1 .. 1}" assumes "f \ UNIV \ {-1 .. 1}" shows "closed_segment (aform_val e X) (aform_val f X) \ Affine X" proof - have "aform_val e X \ Affine X" "aform_val f X \ Affine X" using assms by (auto simp: Affine_def valuate_def) with convex_Affine[of X, simplified convex_contains_segment] show ?thesis by simp qed subsection \From List of Generators\ lift_definition pdevs_of_list::"'a::zero list \ 'a pdevs" is "\xs i. if i < length xs then xs ! i else 0" by auto lemma pdevs_apply_pdevs_of_list: "pdevs_apply (pdevs_of_list xs) i = (if i < length xs then xs ! i else 0)" by transfer simp lemma pdevs_apply_pdevs_of_list_Nil[simp]: "pdevs_apply (pdevs_of_list []) i = 0" by transfer auto lemma pdevs_apply_pdevs_of_list_Cons: "pdevs_apply (pdevs_of_list (x # xs)) i = (if i = 0 then x else pdevs_apply (pdevs_of_list xs) (i - 1))" by transfer auto lemma pdevs_domain_pdevs_of_list_Cons[simp]: "pdevs_domain (pdevs_of_list (x # xs)) = (if x = 0 then {} else {0}) \ (+) 1 ` pdevs_domain (pdevs_of_list xs)" by (force simp: pdevs_apply_pdevs_of_list_Cons split: if_split_asm) lemma pdevs_val_pdevs_of_list_eq[simp]: "pdevs_val e (pdevs_of_list (x # xs)) = e 0 *\<^sub>R x + pdevs_val (e o (+) 1) (pdevs_of_list xs)" proof - have "pdevs_val e (pdevs_of_list (x # xs)) = (\i\pdevs_domain (pdevs_of_list (x # xs)) \ {0}. e i *\<^sub>R x) + (\i\pdevs_domain (pdevs_of_list (x # xs)) \ - {0}. e i *\<^sub>R pdevs_apply (pdevs_of_list xs) (i - Suc 0))" (is "_ = ?l + ?r") by (simp add: pdevs_val_pdevs_domain if_distrib sum.If_cases pdevs_apply_pdevs_of_list_Cons) also have "?r = (\i\pdevs_domain (pdevs_of_list xs). e (Suc i) *\<^sub>R pdevs_apply (pdevs_of_list xs) i)" by (rule sum.reindex_cong[of "\i. i + 1"]) auto also have "\ = pdevs_val (e o (+) 1) (pdevs_of_list xs)" by (simp add: pdevs_val_pdevs_domain ) also have "?l = (\i\{0}. e i *\<^sub>R x)" by (rule sum.mono_neutral_cong_left) auto also have "\ = e 0 *\<^sub>R x" by simp finally show ?thesis . qed lemma less_degree_pdevs_of_list_imp_less_length: assumes "i < degree (pdevs_of_list xs)" shows "i < length xs" proof - from assms have "pdevs_apply (pdevs_of_list xs) (degree (pdevs_of_list xs) - 1) \ 0" by (metis degree_least_nonzero less_nat_zero_code) hence "degree (pdevs_of_list xs) - 1 < length xs" by (simp add: pdevs_apply_pdevs_of_list split: if_split_asm) with assms show ?thesis by simp qed lemma tdev_pdevs_of_list[simp]: "tdev (pdevs_of_list xs) = sum_list (map abs xs)" by (auto simp: tdev_def pdevs_apply_pdevs_of_list sum_list_sum_nth less_degree_pdevs_of_list_imp_less_length intro!: sum.mono_neutral_cong_left degree_gt) lemma pdevs_of_list_Nil[simp]: "pdevs_of_list [] = zero_pdevs" by (auto intro!: pdevs_eqI) lemma pdevs_val_inj_sumI: fixes K::"'a set" and g::"'a \ nat" assumes "finite K" assumes "inj_on g K" assumes "pdevs_domain x \ g ` K" assumes "\i. i \ K \ g i \ pdevs_domain x \ f i = 0" assumes "\i. i \ K \ g i \ pdevs_domain x \ f i = e (g i) *\<^sub>R pdevs_apply x (g i)" shows "pdevs_val e x = (\i\K. f i)" proof - have [simp]: "inj_on (the_inv_into K g) (pdevs_domain x)" using assms by (auto simp: intro!: subset_inj_on[OF inj_on_the_inv_into]) { fix y assume y: "y \ pdevs_domain x" have g_inv: "g (the_inv_into K g y) = y" by (meson assms(2) assms(3) y f_the_inv_into_f subset_eq) have inv_in: "the_inv_into K g y \ K" by (meson assms(2) assms(3) y subset_iff in_pdevs_domain the_inv_into_into) have inv3: "the_inv_into (pdevs_domain x) (the_inv_into K g) (the_inv_into K g y) = g (the_inv_into K g y)" using assms y by (subst the_inv_into_f_f) (auto simp: f_the_inv_into_f[OF assms(2)]) note g_inv inv_in inv3 } note this[simp] have "pdevs_val e x = (\i\pdevs_domain x. e i *\<^sub>R pdevs_apply x i)" by (simp add: pdevs_val_pdevs_domain) also have "\ = (\i \ the_inv_into K g ` pdevs_domain x. e (g i) *\<^sub>R pdevs_apply x (g i))" by (rule sum.reindex_cong[OF inj_on_the_inv_into]) auto also have "\ = (\i\K. f i)" using assms by (intro sum.mono_neutral_cong_left) (auto simp: the_inv_into_image_eq) finally show ?thesis . qed lemma pdevs_domain_pdevs_of_list_le: "pdevs_domain (pdevs_of_list xs) \ {0..(i,x)\zip [0..R x)" by (auto simp: sum_list_distinct_conv_sum_set in_set_zip image_fst_zip pdevs_apply_pdevs_of_list distinct_zipI1 intro!: pdevs_val_inj_sumI[of _ fst] split: if_split_asm) +lemma pdevs_val_map: + \pdevs_val e (pdevs_of_list xs) + = (\n\[0..R xs ! n)\ +proof - + have \map2 (\i. (*\<^sub>R) (e i)) [0..n. e n *\<^sub>R xs ! n) [0.. + by (rule nth_equalityI) simp_all + then show ?thesis + by (simp add: pdevs_val_zip) +qed + lemma scaleR_sum_list: fixes xs::"'a::real_vector list" shows "a *\<^sub>R sum_list xs = sum_list (map (scaleR a) xs)" by (induct xs) (auto simp: algebra_simps) lemma pdevs_val_const_pdevs_of_list: "pdevs_val (\_. c) (pdevs_of_list xs) = c *\<^sub>R sum_list xs" unfolding pdevs_val_zip split_beta' scaleR_sum_list by (rule arg_cong) (auto intro!: nth_equalityI) lemma pdevs_val_partition: assumes "e \ UNIV \ I" obtains f g where "pdevs_val e (pdevs_of_list xs) = pdevs_val f (pdevs_of_list (filter p xs)) + pdevs_val g (pdevs_of_list (filter (Not o p) xs))" "f \ UNIV \ I" "g \ UNIV \ I" proof - obtain i where i: "i \ I" by (metis assms funcset_mem iso_tuple_UNIV_I) let ?zip = "zip [0.. snd) ?zip" let ?f = "(\n. if n < degree (pdevs_of_list (filter p xs)) then e (map fst (fst part) ! n) else i)" let ?g = "(\n. if n < degree (pdevs_of_list (filter (Not \ p) xs)) then e (map fst (snd part) ! n) else i)" show ?thesis proof have "pdevs_val e (pdevs_of_list xs) = (\(i,x)\?zip. e i *\<^sub>R x)" by (rule pdevs_val_zip) also have "\ = (\(i, x)\set ?zip. e i *\<^sub>R x)" by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1) also have [simp]: "set (fst part) \ set (snd part) = {}" by (auto simp: part_def) from partition_set[of "p o snd" ?zip "fst part" "snd part"] have "set ?zip = set (fst part) \ set (snd part)" by (auto simp: part_def) also have "(\a\set (fst part) \ set (snd part). case a of (i, x) \ e i *\<^sub>R x) = (\(i, x)\set (fst part). e i *\<^sub>R x) + (\(i, x)\set (snd part). e i *\<^sub>R x)" by (auto simp: split_beta sum_Un) also have "(\(i, x)\set (fst part). e i *\<^sub>R x) = (\(i, x)\(fst part). e i *\<^sub>R x)" by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1 part_def) also have "\ = (\i e i *\<^sub>R x)" by (subst sum_list_sum_nth) (simp add: split_beta' atLeast0LessThan) also have "\ = pdevs_val (\n. e (map fst (fst part) ! n)) (pdevs_of_list (map snd (fst part)))" by (force simp: pdevs_val_zip sum_list_distinct_conv_sum_set distinct_zipI1 split_beta' in_set_zip intro!: sum.reindex_cong[where l=fst] image_eqI[where x = "(x, map snd (fst part) ! x)" for x]) also have "(\(i, x)\set (snd part). e i *\<^sub>R x) = (\(i, x)\(snd part). e i *\<^sub>R x)" by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1 part_def) also have "\ = (\i e i *\<^sub>R x)" by (subst sum_list_sum_nth) (simp add: split_beta' atLeast0LessThan) also have "\ = pdevs_val (\n. e (map fst (snd part) ! n)) (pdevs_of_list (map snd (snd part)))" by (force simp: pdevs_val_zip sum_list_distinct_conv_sum_set distinct_zipI1 split_beta' in_set_zip intro!: sum.reindex_cong[where l=fst] image_eqI[where x = "(x, map snd (snd part) ! x)" for x]) also have "pdevs_val (\n. e (map fst (fst part) ! n)) (pdevs_of_list (map snd (fst part))) = pdevs_val (\n. if n < degree (pdevs_of_list (map snd (fst part))) then e (map fst (fst part) ! n) else i) (pdevs_of_list (map snd (fst part)))" by (rule pdevs_val_degree_cong) simp_all also have "pdevs_val (\n. e (map fst (snd part) ! n)) (pdevs_of_list (map snd (snd part))) = pdevs_val (\n. if n < degree (pdevs_of_list (map snd (snd part))) then e (map fst (snd part) ! n) else i) (pdevs_of_list (map snd (snd part)))" by (rule pdevs_val_degree_cong) simp_all also have "map snd (snd part) = filter (Not o p) xs" by (simp add: part_def filter_map[symmetric] o_assoc) also have "map snd (fst part) = filter p xs" by (simp add: part_def filter_map[symmetric]) finally show "pdevs_val e (pdevs_of_list xs) = pdevs_val ?f (pdevs_of_list (filter p xs)) + pdevs_val ?g (pdevs_of_list (filter (Not \ p) xs))" . show "?f \ UNIV \ I" "?g \ UNIV \ I" using assms \i\I\ by (auto simp: Pi_iff) qed qed lemma pdevs_apply_pdevs_of_list_append: "pdevs_apply (pdevs_of_list (xs @ zs)) i = (if i < length xs then pdevs_apply (pdevs_of_list xs) i else pdevs_apply (pdevs_of_list zs) (i - length xs))" by (auto simp: pdevs_apply_pdevs_of_list nth_append) lemma degree_pdevs_of_list_le_length[intro, simp]: "degree (pdevs_of_list xs) \ length xs" by (metis less_irrefl_nat le_less_linear less_degree_pdevs_of_list_imp_less_length) lemma degree_pdevs_of_list_append: "degree (pdevs_of_list (xs @ ys)) \ length xs + degree (pdevs_of_list ys)" by (rule degree_le) (auto simp: pdevs_apply_pdevs_of_list_append) lemma pdevs_val_pdevs_of_list_append: assumes "f \ UNIV \ I" assumes "g \ UNIV \ I" obtains e where "pdevs_val f (pdevs_of_list xs) + pdevs_val g (pdevs_of_list ys) = pdevs_val e (pdevs_of_list (xs @ ys))" "e \ UNIV \ I" proof let ?e = "(\i. if i < length xs then f i else g (i - length xs))" have f: "pdevs_val f (pdevs_of_list xs) = (\i\{..R pdevs_apply (pdevs_of_list (xs @ ys)) i)" by (auto simp: pdevs_val_sum degree_gt pdevs_apply_pdevs_of_list_append intro: sum.mono_neutral_cong_left) have g: "pdevs_val g (pdevs_of_list ys) = (\i=length xs ..R pdevs_apply (pdevs_of_list (xs @ ys)) i)" (is "_ = ?sg") by (auto simp: pdevs_val_sum pdevs_apply_pdevs_of_list_append intro!: inj_onI image_eqI[where x="length xs + x" for x] sum.reindex_cong[where l="\i. i - length xs"]) show "pdevs_val f (pdevs_of_list xs) + pdevs_val g (pdevs_of_list ys) = pdevs_val ?e (pdevs_of_list (xs @ ys))" unfolding f g by (subst sum.union_disjoint[symmetric]) (force simp: pdevs_val_sum ivl_disj_un degree_pdevs_of_list_append intro!: sum.mono_neutral_cong_right split: if_split_asm)+ show "?e \ UNIV \ I" using assms by (auto simp: Pi_iff) qed lemma sum_general_mono: fixes f::"'a\('b::ordered_ab_group_add)" assumes [simp,intro]: "finite s" "finite t" assumes f: "\x. x \ s - t \ f x \ 0" assumes g: "\x. x \ t - s \ g x \ 0" assumes fg: "\x. x \ s \ t \ f x \ g x" shows "(\x \ s. f x) \ (\x \ t. g x)" proof - have "s = (s - t) \ (s \ t)" and [intro, simp]: "(s - t) \ (s \ t) = {}" by auto hence "(\x \ s. f x) = (\x \ s - t \ s \ t. f x)" using assms by simp also have "\ = (\x \ s - t. f x) + (\x \ s \ t. f x)" by (simp add: sum_Un) also have "(\x \ s - t. f x) \ 0" by (auto intro!: sum_nonpos f) also have "0 \ (\x \ t - s. g x)" by (auto intro!: sum_nonneg g) also have "(\x \ s \ t. f x) \ (\x \ s \ t. g x)" by (auto intro!: sum_mono fg) also have [intro, simp]: "(t - s) \ (s \ t) = {}" by auto hence "sum g (t - s) + sum g (s \ t) = sum g ((t - s) \ (s \ t))" by (simp add: sum_Un) also have "\ = sum g t" by (auto intro!: sum.cong) finally show ?thesis by simp qed +lemma degree_pdevs_of_list_eq': + \degree (pdevs_of_list xs) = Min {n. n \ length xs \ (\m. n \ m \ m < length xs \ xs ! m = 0)}\ + apply (simp add: degree_def pdevs_apply_pdevs_of_list) + apply (rule Least_equality) + apply auto + apply (subst (asm) Min_le_iff) + apply auto + apply (subst Min_le_iff) + apply auto + apply (metis le_cases not_less) + done + +lemma pdevs_val_permuted: + \pdevs_val (e \ p) (pdevs_of_list (permute_list p xs)) = pdevs_val e (pdevs_of_list xs)\ (is \?r = ?s\) + if perm: \p permutes {.. +proof - + from that have \image_mset p (mset_set {0.. + by (simp add: permutes_image_mset lessThan_atLeast0) + moreover have \map (\n. e (p n) *\<^sub>R permute_list p xs ! n) [0..n. e n *\<^sub>R xs ! n) (map p [0.. + using that by (simp add: permute_list_nth) + ultimately show ?thesis + using that by (simp add: pdevs_apply_pdevs_of_list pdevs_val_map + flip: map_map sum_mset_sum_list) +qed + lemma pdevs_val_perm_ex: assumes "xs <~~> ys" assumes mem: "e \ UNIV \ I" shows "\e'. e' \ UNIV \ I \ pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)" - using assms -proof (induct arbitrary: e) - case Nil - thus ?case - by auto -next - case (Cons xs ys z) - hence "(e \ (+) (Suc 0)) \ UNIV \ I" by auto - from Cons(2)[OF this] obtain e' where "e' \ UNIV \ I" - "pdevs_val (e \ (+) (Suc 0)) (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)" - by metis - thus ?case using Cons - by (auto intro!: exI[where x="\x. if x = 0 then e 0 else e' (x - 1)"] simp: o_def Pi_iff) -next - case (trans xs ys zs) - thus ?case by metis -next - case (swap y x l) - thus ?case - by (auto intro!: exI[where x="\i. if i = 0 then e 1 else if i = 1 then e 0 else e i"] - simp: o_def Pi_iff) +proof - + from \mset xs = mset ys\ + have \mset ys = mset xs\ .. + then obtain p where \p permutes {.. \permute_list p xs = ys\ + by (rule mset_eq_permutation) + moreover define e' where \e' = e \ p\ + ultimately have \e' \ UNIV \ I\ \pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)\ + using mem by (auto simp add: pdevs_val_permuted) + then show ?thesis by blast qed lemma pdevs_val_perm: assumes "xs <~~> ys" assumes mem: "e \ UNIV \ I" obtains e' where "e' \ UNIV \ I" "pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list ys)" using assms by (metis pdevs_val_perm_ex) lemma set_distinct_permI: "set xs = set ys \ distinct xs \ distinct ys \ xs <~~> ys" by (metis eq_set_perm_remdups remdups_id_iff_distinct) lemmas pdevs_val_permute = pdevs_val_perm[OF set_distinct_permI] lemma partition_permI: "filter p xs @ filter (Not o p) xs <~~> xs" -proof (induct xs) - case (Cons x xs) - have swap_app_Cons: "filter p xs @ x # [a\xs . \ p a] <~~> x # filter p xs @ [a\xs . \ p a]" - by (metis perm_sym perm_append_Cons) - also have "\ <~~> x#xs" - using Cons by auto - finally (trans) - show ?case using Cons - by simp -qed simp + by simp lemma pdevs_val_eqI: assumes "\i. i \ pdevs_domain y \ i \ pdevs_domain x \ e i *\<^sub>R pdevs_apply x i = f i *\<^sub>R pdevs_apply y i" assumes "\i. i \ pdevs_domain y \ i \ pdevs_domain x \ f i *\<^sub>R pdevs_apply y i = 0" assumes "\i. i \ pdevs_domain x \ i \ pdevs_domain y \ e i *\<^sub>R pdevs_apply x i = 0" shows "pdevs_val e x = pdevs_val f y" using assms by (force simp: pdevs_val_pdevs_domain intro!: sum.reindex_bij_witness_not_neutral[where i=id and j = id and S'="pdevs_domain x - pdevs_domain y" and T'="pdevs_domain y - pdevs_domain x"]) definition filter_pdevs_raw::"(nat \ 'a \ bool) \ (nat \ 'a::real_vector) \ (nat \ 'a)" where "filter_pdevs_raw I X = (\i. if I i (X i) then X i else 0)" lemma filter_pdevs_raw_nonzeros: "{i. filter_pdevs_raw s f i \ 0} = {i. f i \ 0} \ {x. s x (f x)}" by (auto simp: filter_pdevs_raw_def) lift_definition filter_pdevs::"(nat \ 'a \ bool) \ 'a::real_vector pdevs \ 'a pdevs" is filter_pdevs_raw by (simp add: filter_pdevs_raw_nonzeros) lemma pdevs_apply_filter_pdevs[simp]: "pdevs_apply (filter_pdevs I x) i = (if I i (pdevs_apply x i) then pdevs_apply x i else 0)" by transfer (auto simp: filter_pdevs_raw_def) lemma degree_filter_pdevs_le: "degree (filter_pdevs I x) \ degree x" by (rule degree_leI) (simp split: if_split_asm) lemma pdevs_val_filter_pdevs: "pdevs_val e (filter_pdevs I x) = (\i \ {.. {i. I i (pdevs_apply x i)}. e i *\<^sub>R pdevs_apply x i)" by (auto simp: pdevs_val_sum if_distrib sum.inter_restrict degree_filter_pdevs_le degree_gt intro!: sum.mono_neutral_cong_left split: if_split_asm) lemma pdevs_val_filter_pdevs_dom: "pdevs_val e (filter_pdevs I x) = (\i \ pdevs_domain x \ {i. I i (pdevs_apply x i)}. e i *\<^sub>R pdevs_apply x i)" by (auto simp: pdevs_val_pdevs_domain if_distrib sum.inter_restrict degree_filter_pdevs_le degree_gt intro!: sum.mono_neutral_cong_left split: if_split_asm) lemma pdevs_val_filter_pdevs_eval: "pdevs_val e (filter_pdevs p x) = pdevs_val (\i. if p i (pdevs_apply x i) then e i else 0) x" by (auto split: if_split_asm intro!: pdevs_val_eqI) definition "pdevs_applys X i = map (\x. pdevs_apply x i) X" definition "pdevs_vals e X = map (pdevs_val e) X" definition "aform_vals e X = map (aform_val e) X" definition "filter_pdevs_list I X = map (filter_pdevs (\i _. I i (pdevs_applys X i))) X" lemma pdevs_applys_filter_pdevs_list[simp]: "pdevs_applys (filter_pdevs_list I X) i = (if I i (pdevs_applys X i) then pdevs_applys X i else map (\_. 0) X)" by (auto simp: filter_pdevs_list_def o_def pdevs_applys_def) definition "degrees X = Max (insert 0 (degree ` set X))" abbreviation "degree_aforms X \ degrees (map snd X)" lemma degrees_leI: assumes "\x. x \ set X \ degree x \ K" shows "degrees X \ K" using assms by (auto simp: degrees_def intro!: Max.boundedI) lemma degrees_leD: assumes "degrees X \ K" shows "\x. x \ set X \ degree x \ K" using assms by (auto simp: degrees_def intro!: Max.boundedI) lemma degree_filter_pdevs_list_le: "degrees (filter_pdevs_list I x) \ degrees x" by (rule degrees_leI) (auto simp: filter_pdevs_list_def intro!: degree_le dest!: degrees_leD) definition "dense_list_of_pdevs x = map (\i. pdevs_apply x i) [0..(reverse) ordered coefficients as list\ definition "list_of_pdevs x = map (\i. (i, pdevs_apply x i)) (rev (sorted_list_of_set (pdevs_domain x)))" lemma list_of_pdevs_zero_pdevs[simp]: "list_of_pdevs zero_pdevs = []" by (auto simp: list_of_pdevs_def) lemma sum_list_list_of_pdevs: "sum_list (map snd (list_of_pdevs x)) = sum_list (dense_list_of_pdevs x)" by (auto intro!: sum.mono_neutral_cong_left simp add: degree_gt sum_list_distinct_conv_sum_set dense_list_of_pdevs_def list_of_pdevs_def) lemma sum_list_filter_dense_list_of_pdevs[symmetric]: "sum_list (map snd (filter (p o snd) (list_of_pdevs x))) = sum_list (filter p (dense_list_of_pdevs x))" by (auto intro!: sum.mono_neutral_cong_left simp add: degree_gt sum_list_distinct_conv_sum_set dense_list_of_pdevs_def list_of_pdevs_def o_def filter_map) lemma pdevs_of_list_dense_list_of_pdevs: "pdevs_of_list (dense_list_of_pdevs x) = x" by (auto simp: pdevs_apply_pdevs_of_list dense_list_of_pdevs_def pdevs_eqI) lemma pdevs_val_sum_list: "pdevs_val (\_. c) X = c *\<^sub>R sum_list (map snd (list_of_pdevs X))" by (auto simp: pdevs_val_sum sum_list_list_of_pdevs pdevs_val_const_pdevs_of_list[symmetric] pdevs_of_list_dense_list_of_pdevs) lemma list_of_pdevs_all_nonzero: "list_all (\x. x \ 0) (map snd (list_of_pdevs xs))" by (auto simp: list_of_pdevs_def list_all_iff) lemma list_of_pdevs_nonzero: "x \ set (map snd (list_of_pdevs xs)) \ x \ 0" by (auto simp: list_of_pdevs_def) lemma pdevs_of_list_scaleR_0[simp]: fixes xs::"'a::real_vector list" shows "pdevs_of_list (map ((*\<^sub>R) 0) xs) = zero_pdevs" by (auto simp: pdevs_apply_pdevs_of_list intro!: pdevs_eqI) lemma degree_pdevs_of_list_scaleR: "degree (pdevs_of_list (map ((*\<^sub>R) c) xs)) = (if c \ 0 then degree (pdevs_of_list xs) else 0)" by (auto simp: pdevs_apply_pdevs_of_list intro!: degree_cong) lemma list_of_pdevs_eq: "rev (list_of_pdevs X) = (filter ((\) 0 o snd) (map (\i. (i, pdevs_apply X i)) [0..i. if i < d then 1 else 0) (pdevs_of_list xs)" proof - have "sum_list (take d xs) = 1 *\<^sub>R sum_list (take d xs)" by simp also note pdevs_val_const_pdevs_of_list[symmetric] also have "pdevs_val (\_. 1) (pdevs_of_list (take d xs)) = pdevs_val (\i. if i < d then 1 else 0) (pdevs_of_list xs)" by (auto simp: pdevs_apply_pdevs_of_list split: if_split_asm intro!: pdevs_val_eqI) finally show ?thesis . qed lemma zero_in_range_pdevs_apply[intro, simp]: fixes X::"'a::real_vector pdevs" shows "0 \ range (pdevs_apply X)" by (metis degree_gt less_irrefl rangeI) lemma dense_list_in_range: "x \ set (dense_list_of_pdevs X) \ x \ range (pdevs_apply X)" by (auto simp: dense_list_of_pdevs_def) lemma not_in_dense_list_zeroD: assumes "pdevs_apply X i \ set (dense_list_of_pdevs X)" shows "pdevs_apply X i = 0" proof (rule ccontr) assume "pdevs_apply X i \ 0" hence "i < degree X" by (rule degree_gt) thus False using assms by (auto simp: dense_list_of_pdevs_def) qed lemma list_all_list_of_pdevsI: assumes "\i. i \ pdevs_domain X \ P (pdevs_apply X i)" shows "list_all (\x. P x) (map snd (list_of_pdevs X))" using assms by (auto simp: list_all_iff list_of_pdevs_def) lemma pdevs_of_list_map_scaleR: "pdevs_of_list (map (scaleR r) xs) = scaleR_pdevs r (pdevs_of_list xs)" by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list) lemma map_permI: assumes "xs <~~> ys" shows "map f xs <~~> map f ys" using assms by induct auto lemma rev_perm: "rev xs <~~> ys \ xs <~~> ys" - by (metis perm.trans perm_rev rev_rev_ident) + by simp lemma list_of_pdevs_perm_filter_nonzero: "map snd (list_of_pdevs X) <~~> (filter ((\) 0) (dense_list_of_pdevs X))" proof - have zip_map: "zip [0..i. (i, pdevs_apply X i)) [0.. filter ((\) 0 o snd) (zip [0.. map snd (filter ((\) 0 \ snd) (zip [0..) 0 \ snd) (zip [0..) 0) (dense_list_of_pdevs X)" using map_filter[of snd "(\) 0" "(zip [0.. UNIV \ I" assumes "0 \ I" obtains e' where "pdevs_val e (pdevs_of_list (filter p xs)) = pdevs_val e' (pdevs_of_list xs)" "e' \ UNIV \ I" unfolding pdevs_val_filter_pdevs_eval proof - have "(\_::nat. 0) \ UNIV \ I" using assms by simp have "pdevs_val e (pdevs_of_list (filter p xs)) = pdevs_val e (pdevs_of_list (filter p xs)) + pdevs_val (\_. 0) (pdevs_of_list (filter (Not o p) xs))" by (simp add: pdevs_val_sum) also from pdevs_val_pdevs_of_list_append[OF \e \ _\ \(\_. 0) \ _\] obtain e' where "e' \ UNIV \ I" "\ = pdevs_val e' (pdevs_of_list (filter p xs @ filter (Not o p) xs))" by metis note this(2) also from pdevs_val_perm[OF partition_permI \e' \ _\] obtain e'' where "\ = pdevs_val e'' (pdevs_of_list xs)" "e'' \ UNIV \ I" by metis note this(1) finally show ?thesis using \e'' \ _\ .. qed lemma pdevs_val_of_list_of_pdevs: assumes "e \ UNIV \ I" assumes "0 \ I" obtains e' where "pdevs_val e (pdevs_of_list (map snd (list_of_pdevs X))) = pdevs_val e' X" "e' \ UNIV \ I" proof - obtain e' where "e' \ UNIV \ I" and "pdevs_val e (pdevs_of_list (map snd (list_of_pdevs X))) = pdevs_val e' (pdevs_of_list (filter ((\) 0) (dense_list_of_pdevs X)))" by (rule pdevs_val_perm[OF list_of_pdevs_perm_filter_nonzero assms(1)]) note this(2) also from pdevs_val_filter[OF \e' \ _\ \0 \ I\, of "(\) 0" "dense_list_of_pdevs X"] obtain e'' where "e'' \ UNIV \ I" and "\ = pdevs_val e'' (pdevs_of_list (dense_list_of_pdevs X))" by metis note this(2) also have "\ = pdevs_val e'' X" by (simp add: pdevs_of_list_dense_list_of_pdevs) finally show ?thesis using \e'' \ UNIV \ I\ .. qed lemma pdevs_val_of_list_of_pdevs2: assumes "e \ UNIV \ I" obtains e' where "pdevs_val e X = pdevs_val e' (pdevs_of_list (map snd (list_of_pdevs X)))" "e' \ UNIV \ I" proof - from list_of_pdevs_perm_filter_nonzero[of X] have perm: "(filter ((\) 0) (dense_list_of_pdevs X)) <~~> map snd (list_of_pdevs X)" - by (simp add: perm_sym) + by simp have "pdevs_val e X = pdevs_val e (pdevs_of_list (dense_list_of_pdevs X))" by (simp add: pdevs_of_list_dense_list_of_pdevs) also from pdevs_val_partition[OF \e \ _\, of "dense_list_of_pdevs X" "(\) 0"] obtain f g where "f \ UNIV \ I" "g \ UNIV \ I" "\ = pdevs_val f (pdevs_of_list (filter ((\) 0) (dense_list_of_pdevs X))) + pdevs_val g (pdevs_of_list (filter (Not \ (\) 0) (dense_list_of_pdevs X)))" (is "_ = ?f + ?g") by metis note this(3) also have "pdevs_of_list [x\dense_list_of_pdevs X . x = 0] = zero_pdevs" by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list dest!: nth_mem) hence "?g = 0" by (auto simp: o_def ) also obtain e' where "e' \ UNIV \ I" and "?f = pdevs_val e' (pdevs_of_list (map snd (list_of_pdevs X)))" by (rule pdevs_val_perm[OF perm \f \ _\]) note this(2) finally show ?thesis using \e' \ UNIV \ I\ by (auto intro!: that) qed lemma dense_list_of_pdevs_scaleR: "r \ 0 \ map ((*\<^sub>R) r) (dense_list_of_pdevs x) = dense_list_of_pdevs (scaleR_pdevs r x)" by (auto simp: dense_list_of_pdevs_def) lemma degree_pdevs_of_list_eq: "(\x. x \ set xs \ x \ 0) \ degree (pdevs_of_list xs) = length xs" by (cases xs) (auto simp add: pdevs_apply_pdevs_of_list nth_Cons intro!: degree_eqI split: nat.split) lemma dense_list_of_pdevs_pdevs_of_list: "(\x. x \ set xs \ x \ 0) \ dense_list_of_pdevs (pdevs_of_list xs) = xs" by (auto simp: dense_list_of_pdevs_def degree_pdevs_of_list_eq pdevs_apply_pdevs_of_list intro!: nth_equalityI) lemma pdevs_of_list_sum: assumes "distinct xs" assumes "e \ UNIV \ I" obtains f where "f \ UNIV \ I" "pdevs_val e (pdevs_of_list xs) = (\P\set xs. f P *\<^sub>R P)" proof - define f where "f X = e (the (map_of (zip xs [0.. UNIV \ I" by (auto simp: f_def) moreover have "pdevs_val e (pdevs_of_list xs) = (\P\set xs. f P *\<^sub>R P)" by (auto simp add: pdevs_val_zip f_def assms sum_list_distinct_conv_sum_set[symmetric] in_set_zip map_of_zip_upto2_length_eq_nth intro!: sum_list_nth_eqI) ultimately show ?thesis .. qed lemma pdevs_domain_eq_pdevs_of_list: assumes nz: "\x. x \ set (xs) \ x \ 0" shows "pdevs_domain (pdevs_of_list xs) = {0..x. x \ set xs \ x \ 0" shows "length (list_of_pdevs (pdevs_of_list xs)) = length xs" using nz by (auto simp: list_of_pdevs_def pdevs_domain_eq_pdevs_of_list) lemma nth_list_of_pdevs_pdevs_of_list: assumes nz: "\x. x \ set xs \ x \ 0" assumes l: "n < length xs" shows "list_of_pdevs (pdevs_of_list xs) ! n = ((length xs - Suc n), xs ! (length xs - Suc n))" using nz l by (auto simp: list_of_pdevs_def pdevs_domain_eq_pdevs_of_list rev_nth pdevs_apply_pdevs_of_list) lemma list_of_pdevs_pdevs_of_list_eq: "(\x. x \ set xs \ x \ 0) \ list_of_pdevs (pdevs_of_list xs) = zip (rev [0..x. x \ set xs \ x \ 0" shows "sum_list (filter p (map snd (list_of_pdevs (pdevs_of_list xs)))) = sum_list (filter p xs)" using assms by (auto simp: list_of_pdevs_pdevs_of_list_eq rev_filter[symmetric]) lemma sum_list_partition: fixes xs::"'a::comm_monoid_add list" shows "sum_list (filter p xs) + sum_list (filter (Not o p) xs) = sum_list xs" by (induct xs) (auto simp: ac_simps) subsection \2d zonotopes\ definition "prod_of_pdevs x y = binop_pdevs Pair x y" lemma apply_pdevs_prod_of_pdevs[simp]: "pdevs_apply (prod_of_pdevs x y) i = (pdevs_apply x i, pdevs_apply y i)" unfolding prod_of_pdevs_def by (simp add: zero_prod_def) lemma pdevs_domain_prod_of_pdevs[simp]: "pdevs_domain (prod_of_pdevs x y) = pdevs_domain x \ pdevs_domain y" by (auto simp: zero_prod_def) lemma pdevs_val_prod_of_pdevs[simp]: "pdevs_val e (prod_of_pdevs x y) = (pdevs_val e x, pdevs_val e y)" proof - have "pdevs_val e x = (\i\pdevs_domain x \ pdevs_domain y. e i *\<^sub>R pdevs_apply x i)" (is "_ = ?x") unfolding pdevs_val_pdevs_domain by (rule sum.mono_neutral_cong_left) auto moreover have "pdevs_val e y = (\i\pdevs_domain x \ pdevs_domain y. e i *\<^sub>R pdevs_apply y i)" (is "_ = ?y") unfolding pdevs_val_pdevs_domain by (rule sum.mono_neutral_cong_left) auto ultimately have "(pdevs_val e x, pdevs_val e y) = (?x, ?y)" by auto also have "\ = pdevs_val e (prod_of_pdevs x y)" by (simp add: sum_prod pdevs_val_pdevs_domain) finally show ?thesis by simp qed definition prod_of_aforms (infixr "\\<^sub>a" 80) where "prod_of_aforms x y = ((fst x, fst y), prod_of_pdevs (snd x) (snd y))" subsection \Intervals\ definition One_pdevs_raw::"nat \ 'a::executable_euclidean_space" where "One_pdevs_raw i = (if i < length (Basis_list::'a list) then Basis_list ! i else 0)" lemma zeros_One_pdevs_raw: "One_pdevs_raw -` {0::'a::executable_euclidean_space} = {length (Basis_list::'a list)..}" by (auto simp: One_pdevs_raw_def nonzero_Basis split: if_split_asm dest!: nth_mem) lemma nonzeros_One_pdevs_raw: "{i. One_pdevs_raw i \ (0::'a::executable_euclidean_space)} = - {length (Basis_list::'a list)..}" using zeros_One_pdevs_raw by blast lift_definition One_pdevs::"'a::executable_euclidean_space pdevs" is One_pdevs_raw by (auto simp: nonzeros_One_pdevs_raw) lemma pdevs_apply_One_pdevs[simp]: "pdevs_apply One_pdevs i = (if i < length (Basis_list::'a::executable_euclidean_space list) then Basis_list ! i else 0::'a)" by transfer (simp add: One_pdevs_raw_def) lemma Max_Collect_less_nat: "Max {i::nat. i < k} = (if k = 0 then Max {} else k - 1)" by (auto intro!: Max_eqI) lemma degree_One_pdevs[simp]: "degree (One_pdevs::'a pdevs) = length (Basis_list::'a::executable_euclidean_space list)" by (auto simp: degree_eq_Suc_max Basis_list_nth_nonzero Max_Collect_less_nat intro!: Max_eqI DIM_positive) definition inner_scaleR_pdevs::"'a::euclidean_space \ 'a pdevs \ 'a pdevs" where "inner_scaleR_pdevs b x = unop_pdevs (\x. (b \ x) *\<^sub>R x) x" lemma pdevs_apply_inner_scaleR_pdevs[simp]: "pdevs_apply (inner_scaleR_pdevs a x) i = (a \ (pdevs_apply x i)) *\<^sub>R (pdevs_apply x i)" by (simp add: inner_scaleR_pdevs_def) lemma degree_inner_scaleR_pdevs_le: "degree (inner_scaleR_pdevs (l::'a::executable_euclidean_space) One_pdevs) \ degree (One_pdevs::'a pdevs)" by (rule degree_leI) (auto simp: inner_scaleR_pdevs_def One_pdevs_raw_def) definition "pdevs_of_ivl l u = scaleR_pdevs (1/2) (inner_scaleR_pdevs (u - l) One_pdevs)" lemma degree_pdevs_of_ivl_le: "degree (pdevs_of_ivl l u::'a::executable_euclidean_space pdevs) \ DIM('a)" using degree_inner_scaleR_pdevs_le by (simp add: pdevs_of_ivl_def) lemma pdevs_apply_pdevs_of_ivl: defines "B \ Basis_list::'a::executable_euclidean_space list" shows "pdevs_apply (pdevs_of_ivl l u) i = (if i < length B then ((u - l)\(B!i)/2)*\<^sub>R(B!i) else 0)" by (auto simp: pdevs_of_ivl_def B_def) lemma deg_length_less_imp[simp]: "k < degree (pdevs_of_ivl l u::'a::executable_euclidean_space pdevs) \ k < length (Basis_list::'a list)" by (metis (no_types, hide_lams) degree_One_pdevs degree_inner_scaleR_pdevs_le degree_scaleR_pdevs dual_order.strict_trans length_Basis_list_pos nat_neq_iff not_le pdevs_of_ivl_def) lemma tdev_pdevs_of_ivl: "tdev (pdevs_of_ivl l u) = \u - l\ /\<^sub>R 2" proof - have "tdev (pdevs_of_ivl l u) = (\i pdevs_apply (pdevs_of_ivl l u) i\)" by (auto simp: tdev_def) also have "\ = (\i = 0..pdevs_apply (pdevs_of_ivl l u) i\)" using degree_pdevs_of_ivl_le[of l u] by (intro sum.mono_neutral_cong_left) auto also have "\ = (\i = 0..((u - l) \ Basis_list ! i / 2) *\<^sub>R Basis_list ! i\)" by (auto simp: pdevs_apply_pdevs_of_ivl) also have "\ = (\b \ Basis_list. \((u - l) \ b / 2) *\<^sub>R b\)" by (auto simp: sum_list_sum_nth) also have "\ = (\b\Basis. \((u - l) \ b / 2) *\<^sub>R b\)" by (auto simp: sum_list_distinct_conv_sum_set) also have "\ = \u - l\ /\<^sub>R 2" by (subst euclidean_representation[symmetric, of "\u - l\ /\<^sub>R 2"]) (simp add: abs_inner abs_scaleR) finally show ?thesis . qed definition "aform_of_ivl l u = ((l + u)/\<^sub>R2, pdevs_of_ivl l u)" definition "aform_of_point x = aform_of_ivl x x" lemma Elem_affine_of_ivl_le: assumes "e \ UNIV \ {-1 .. 1}" assumes "l \ u" shows "l \ aform_val e (aform_of_ivl l u)" proof - have "l = (1 / 2) *\<^sub>R l + (1 / 2) *\<^sub>R l" by (simp add: scaleR_left_distrib[symmetric]) also have "\ = (l + u)/\<^sub>R2 - tdev (pdevs_of_ivl l u)" by (auto simp: assms tdev_pdevs_of_ivl algebra_simps) also have "\ \ aform_val e (aform_of_ivl l u)" using abs_pdevs_val_le_tdev[OF assms(1), of "pdevs_of_ivl l u"] by (auto simp: aform_val_def aform_of_ivl_def minus_le_iff dest!: abs_le_D2) finally show ?thesis . qed lemma Elem_affine_of_ivl_ge: assumes "e \ UNIV \ {-1 .. 1}" assumes "l \ u" shows "aform_val e (aform_of_ivl l u) \ u" proof - have "aform_val e (aform_of_ivl l u) \ (l + u)/\<^sub>R2 + tdev (pdevs_of_ivl l u)" using abs_pdevs_val_le_tdev[OF assms(1), of "pdevs_of_ivl l u"] by (auto simp: aform_val_def aform_of_ivl_def minus_le_iff dest!: abs_le_D1) also have "\ = (1 / 2) *\<^sub>R u + (1 / 2) *\<^sub>R u" by (auto simp: assms tdev_pdevs_of_ivl algebra_simps) also have "\ = u" by (simp add: scaleR_left_distrib[symmetric]) finally show ?thesis . qed lemma map_of_zip_upto_length_eq_nth: assumes "i < length B" assumes "d = length B" shows "(map_of (zip [0.. {l .. u}" obtains e where "e \ UNIV \ {-1 .. 1}" "k = aform_val e (aform_of_ivl l u)" proof atomize_elim define e where [abs_def]: "e i = (let b = if i R 2) \ b) / (((u - l) /\<^sub>R 2) \ b))" for i let ?B = "Basis_list::'a list" have "k = (1 / 2) *\<^sub>R (l + u) + (\b \ Basis. (if (u - l) \ b = 0 then 0 else ((k - (1 / 2) *\<^sub>R (l + u)) \ b)) *\<^sub>R b)" (is "_ = _ + ?dots") using assms by (force simp add: algebra_simps eucl_le[where 'a='a] intro!: euclidean_eqI[where 'a='a]) also have "?dots = (\b \ Basis. (if (u - l) \ b = 0 then 0 else ((k - (1 / 2) *\<^sub>R (l + u)) \ b) *\<^sub>R b))" by (auto intro!: sum.cong) also have "\ = (\b \ ?B. (if (u - l) \ b = 0 then 0 else ((k - (1 / 2) *\<^sub>R (l + u)) \ b) *\<^sub>R b))" by (auto simp: sum_list_distinct_conv_sum_set) also have "\ = (\i = 0.. ?B ! i = 0 then 0 else ((k - (1 / 2) *\<^sub>R (l + u)) \ ?B ! i) *\<^sub>R ?B ! i))" by (auto simp: sum_list_sum_nth) also have "\ = (\i = 0.. Basis_list ! i = 0 then 0 else ((k - (1 / 2) *\<^sub>R (l + u)) \ Basis_list ! i) *\<^sub>R Basis_list ! i))" using degree_inner_scaleR_pdevs_le[of "u - l"] by (intro sum.mono_neutral_cong_right) (auto dest!: degree) also have "(1 / 2) *\<^sub>R (l + u) + (\i = 0.. Basis_list ! i = 0 then 0 else ((k - (1 / 2) *\<^sub>R (l + u)) \ Basis_list ! i) *\<^sub>R Basis_list ! i)) = aform_val e (aform_of_ivl l u)" using degree_inner_scaleR_pdevs_le[of "u - l"] by (auto simp: aform_val_def aform_of_ivl_def pdevs_of_ivl_def map_of_zip_upto_length_eq_nth e_def Let_def pdevs_val_sum intro!: sum.cong) finally have "k = aform_val e (aform_of_ivl l u)" . moreover { fix k l u::real assume *: "l \ k" "k \ u" let ?m = "l / 2 + u / 2" have "\k - ?m\ \ \if k \ ?m then ?m - l else u - ?m\" using * by auto also have "\ \ \u / 2 - l / 2\" by (auto simp: abs_real_def) finally have "\k - (l / 2 + u / 2)\ \ \u / 2 - l/2\" . } note midpoint_abs = this have "e \ UNIV \ {- 1..1}" using assms unfolding e_def Let_def by (intro Pi_I divide_atLeastAtMost_1_absI) (auto simp: map_of_zip_upto_length_eq_nth eucl_le[where 'a='a] divide_le_eq_1 not_less inner_Basis algebra_simps intro!: midpoint_abs dest!: nth_mem) ultimately show "\e. e \ UNIV \ {- 1..1} \ k = aform_val e (aform_of_ivl l u)" by blast qed lemma Inf_aform_aform_of_ivl: assumes "l \ u" shows "Inf_aform (aform_of_ivl l u) = l" using assms by (auto simp: Inf_aform_def aform_of_ivl_def tdev_pdevs_of_ivl abs_diff_eq1 algebra_simps) (metis field_sum_of_halves scaleR_add_left scaleR_one) lemma Sup_aform_aform_of_ivl: assumes "l \ u" shows "Sup_aform (aform_of_ivl l u) = u" using assms by (auto simp: Sup_aform_def aform_of_ivl_def tdev_pdevs_of_ivl abs_diff_eq1 algebra_simps) (metis field_sum_of_halves scaleR_add_left scaleR_one) lemma Affine_aform_of_ivl: "a \ b \ Affine (aform_of_ivl a b) = {a .. b}" by (force simp: Affine_def valuate_def intro!: Elem_affine_of_ivl_ge Elem_affine_of_ivl_le elim!: in_ivl_affine_of_ivlE) end diff --git a/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy b/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy --- a/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy +++ b/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy @@ -1,971 +1,971 @@ theory Unique_Factorization imports Polynomial_Interpolation.Ring_Hom_Poly Polynomial_Factorization.Polynomial_Divisibility "HOL-Combinatorics.Permutations" "HOL-Computational_Algebra.Euclidean_Algorithm" Containers.Containers_Auxiliary (* only for a lemma *) More_Missing_Multiset "HOL-Algebra.Divisibility" begin hide_const(open) Divisibility.prime Divisibility.irreducible hide_fact(open) Divisibility.irreducible_def Divisibility.irreducibleI Divisibility.irreducibleD Divisibility.irreducibleE hide_const (open) Rings.coprime lemma irreducible_uminus [simp]: fixes a::"'a::idom" shows "irreducible (-a) \ irreducible a" using irreducible_mult_unit_left[of "-1::'a"] by auto context comm_monoid_mult begin definition coprime :: "'a \ 'a \ bool" where coprime_def': "coprime p q \ \r. r dvd p \ r dvd q \ r dvd 1" lemma coprimeI: assumes "\r. r dvd p \ r dvd q \ r dvd 1" shows "coprime p q" using assms by (auto simp: coprime_def') lemma coprimeE: assumes "coprime p q" and "(\r. r dvd p \ r dvd q \ r dvd 1) \ thesis" shows thesis using assms by (auto simp: coprime_def') lemma coprime_commute [ac_simps]: "coprime p q \ coprime q p" by (auto simp add: coprime_def') lemma not_coprime_iff_common_factor: "\ coprime p q \ (\r. r dvd p \ r dvd q \ \ r dvd 1)" by (auto simp add: coprime_def') end lemma (in algebraic_semidom) coprime_iff_coprime [simp, code]: "coprime = Rings.coprime" by (simp add: fun_eq_iff coprime_def coprime_def') lemma (in comm_semiring_1) coprime_0 [simp]: "coprime p 0 \ p dvd 1" "coprime 0 p \ p dvd 1" by (auto intro: coprimeI elim: coprimeE dest: dvd_trans) (**** until here ****) (* TODO: move or...? *) lemma dvd_rewrites: "dvd.dvd ((*)) = (dvd)" by (unfold dvd.dvd_def dvd_def, rule) subsection \Interfacing UFD properties\ hide_const (open) Divisibility.irreducible context comm_monoid_mult_isom begin lemma coprime_hom[simp]: "coprime (hom x) y' \ coprime x (Hilbert_Choice.inv hom y')" proof- show ?thesis by (unfold coprime_def', fold ball_UNIV, subst surj[symmetric], simp) qed lemma coprime_inv_hom[simp]: "coprime (Hilbert_Choice.inv hom x') y \ coprime x' (hom y)" proof- interpret inv: comm_monoid_mult_isom "Hilbert_Choice.inv hom".. show ?thesis by simp qed end subsubsection \Original part\ lemma dvd_dvd_imp_smult: fixes p q :: "'a :: idom poly" assumes pq: "p dvd q" and qp: "q dvd p" shows "\c. p = smult c q" proof (cases "p = 0") case True then show ?thesis by auto next case False from qp obtain r where r: "p = q * r" by (elim dvdE, auto) with False qp have r0: "r \ 0" and q0: "q \ 0" by auto with divides_degree[OF pq] divides_degree[OF qp] False have "degree p = degree q" by auto with r degree_mult_eq[OF q0 r0] have "degree r = 0" by auto from degree_0_id[OF this] obtain c where "r = [:c:]" by metis from r[unfolded this] show ?thesis by auto qed lemma dvd_const: assumes pq: "(p::'a::semidom poly) dvd q" and q0: "q \ 0" and degq: "degree q = 0" shows "degree p = 0" proof- from dvdE[OF pq] obtain r where *: "q = p * r". with q0 have "p \ 0" "r \ 0" by auto from degree_mult_eq[OF this] degq * show "degree p = 0" by auto qed context Rings.dvd begin abbreviation ddvd (infix "ddvd" 40) where "x ddvd y \ x dvd y \ y dvd x" lemma ddvd_sym[sym]: "x ddvd y \ y ddvd x" by auto end context comm_monoid_mult begin lemma ddvd_trans[trans]: "x ddvd y \ y ddvd z \ x ddvd z" using dvd_trans by auto lemma ddvd_transp: "transp (ddvd)" by (intro transpI, fact ddvd_trans) end context comm_semiring_1 begin definition mset_factors where "mset_factors F p \ F \ {#} \ (\f. f \# F \ irreducible f) \ p = prod_mset F" lemma mset_factorsI[intro!]: assumes "\f. f \# F \ irreducible f" and "F \ {#}" and "prod_mset F = p" shows "mset_factors F p" unfolding mset_factors_def using assms by auto lemma mset_factorsD: assumes "mset_factors F p" shows "f \# F \ irreducible f" and "F \ {#}" and "prod_mset F = p" using assms[unfolded mset_factors_def] by auto lemma mset_factorsE[elim]: assumes "mset_factors F p" and "(\f. f \# F \ irreducible f) \ F \ {#} \ prod_mset F = p \ thesis" shows thesis using assms[unfolded mset_factors_def] by auto lemma mset_factors_imp_not_is_unit: assumes "mset_factors F p" shows "\ p dvd 1" proof(cases F) case empty with assms show ?thesis by auto next case (add f F) with assms have "\ f dvd 1" "p = f * prod_mset F" by (auto intro!: irreducible_not_unit) then show ?thesis by auto qed definition primitive_poly where "primitive_poly f \ \d. (\i. d dvd coeff f i) \ d dvd 1" end lemma(in semidom) mset_factors_imp_nonzero: assumes "mset_factors F p" shows "p \ 0" proof assume "p = 0" moreover from assms have "prod_mset F = p" by auto ultimately obtain f where "f \# F" "f = 0" by auto with assms show False by auto qed class ufd = idom + assumes mset_factors_exist: "\x. x \ 0 \ \ x dvd 1 \ \F. mset_factors F x" and mset_factors_unique: "\x F G. mset_factors F x \ mset_factors G x \ rel_mset (ddvd) F G" subsubsection \Connecting to HOL/Divisibility\ context comm_semiring_1 begin abbreviation "mk_monoid \ \carrier = UNIV - {0}, mult = (*), one = 1\" lemma carrier_0[simp]: "x \ carrier mk_monoid \ x \ 0" by auto lemmas mk_monoid_simps = carrier_0 monoid.simps abbreviation irred where "irred \ Divisibility.irreducible mk_monoid" abbreviation factor where "factor \ Divisibility.factor mk_monoid" abbreviation factors where "factors \ Divisibility.factors mk_monoid" abbreviation properfactor where "properfactor \ Divisibility.properfactor mk_monoid" lemma factors: "factors fs y \ prod_list fs = y \ Ball (set fs) irred" proof - have "prod_list fs = foldr (*) fs 1" by (induct fs, auto) thus ?thesis unfolding factors_def by auto qed lemma factor: "factor x y \ (\z. z \ 0 \ x * z = y)" unfolding factor_def by auto lemma properfactor_nz: shows "(y :: 'a) \ 0 \ properfactor x y \ x dvd y \ \ y dvd x" by (auto simp: properfactor_def factor_def dvd_def) lemma mem_Units[simp]: "y \ Units mk_monoid \ y dvd 1" unfolding dvd_def Units_def by (auto simp: ac_simps) end context idom begin lemma irred_0[simp]: "irred (0::'a)" by (unfold Divisibility.irreducible_def, auto simp: factor properfactor_def) lemma factor_idom[simp]: "factor (x::'a) y \ (if y = 0 then x = 0 else x dvd y)" by (cases "y = 0"; auto intro: exI[of _ 1] elim: dvdE simp: factor) lemma associated_connect[simp]: "(\\<^bsub>mk_monoid\<^esub>) = (ddvd)" by (intro ext, unfold associated_def, auto) lemma essentially_equal_connect[simp]: "essentially_equal mk_monoid fs gs \ rel_mset (ddvd) (mset fs) (mset gs)" - by (auto simp: essentially_equal_def rel_mset_via_perm perm_iff_eq_mset) + by (auto simp: essentially_equal_def rel_mset_via_perm) lemma irred_idom_nz: assumes x0: "(x::'a) \ 0" shows "irred x \ irreducible x" using x0 by (auto simp: irreducible_altdef Divisibility.irreducible_def properfactor_nz) lemma dvd_dvd_imp_unit_mult: assumes xy: "x dvd y" and yx: "y dvd x" shows "\z. z dvd 1 \ y = x * z" proof(cases "x = 0") case True with xy show ?thesis by (auto intro: exI[of _ 1]) next case x0: False from xy obtain z where z: "y = x * z" by (elim dvdE, auto) from yx obtain w where w: "x = y * w" by (elim dvdE, auto) from z w have "x * (z * w) = x" by (auto simp: ac_simps) then have "z * w = 1" using x0 by auto with z show ?thesis by (auto intro: exI[of _ z]) qed lemma irred_inner_nz: assumes x0: "x \ 0" shows "(\b. b dvd x \ \ x dvd b \ b dvd 1) \ (\a b. x = a * b \ a dvd 1 \ b dvd 1)" (is "?l \ ?r") proof (intro iffI allI impI) assume l: ?l fix a b assume xab: "x = a * b" then have ax: "a dvd x" and bx: "b dvd x" by auto { assume a1: "\ a dvd 1" with l ax have xa: "x dvd a" by auto from dvd_dvd_imp_unit_mult[OF ax xa] obtain z where z1: "z dvd 1" and xaz: "x = a * z" by auto from xab x0 have "a \ 0" by auto with xab xaz have "b = z" by auto with z1 have "b dvd 1" by auto } then show "a dvd 1 \ b dvd 1" by auto next assume r: ?r fix b assume bx: "b dvd x" and xb: "\ x dvd b" then obtain a where xab: "x = a * b" by (elim dvdE, auto simp: ac_simps) with r consider "a dvd 1" | "b dvd 1" by auto then show "b dvd 1" proof(cases) case 2 then show ?thesis by auto next case 1 then obtain c where ac1: "a * c = 1" by (elim dvdE, auto) from xab have "x * c = b * (a * c)" by (auto simp: ac_simps) with ac1 have "x * c = b" by auto then have "x dvd b" by auto with xb show ?thesis by auto qed qed lemma irred_idom[simp]: "irred x \ x = 0 \ irreducible x" by (cases "x = 0"; simp add: irred_idom_nz irred_inner_nz irreducible_def) lemma assumes "x \ 0" and "factors fs x" and "f \ set fs" shows "f \ 0" using assms by (auto simp: factors) lemma factors_as_mset_factors: assumes x0: "x \ 0" and x1: "x \ 1" shows "factors fs x \ mset_factors (mset fs) x" using assms by (auto simp: factors prod_mset_prod_list) end context ufd begin interpretation comm_monoid_cancel: comm_monoid_cancel "mk_monoid::'a monoid" apply (unfold_locales) apply simp_all using mult_left_cancel apply (auto simp: ac_simps) done lemma factors_exist: assumes "a \ 0" and "\ a dvd 1" shows "\fs. set fs \ UNIV - {0} \ factors fs a" proof- from mset_factors_exist[OF assms] obtain F where "mset_factors F a" by auto also from ex_mset obtain fs where "F = mset fs" by metis finally have fs: "mset_factors (mset fs) a". then have "factors fs a" using assms by (subst factors_as_mset_factors, auto) moreover have "set fs \ UNIV - {0}" using fs by (auto elim!: mset_factorsE) ultimately show ?thesis by auto qed lemma factors_unique: assumes fs: "factors fs a" and gs: "factors gs a" and a0: "a \ 0" and a1: "\ a dvd 1" shows "rel_mset (ddvd) (mset fs) (mset gs)" proof- from a1 have "a \ 1" by auto with a0 fs gs have "mset_factors (mset fs) a" "mset_factors (mset gs) a" by (unfold factors_as_mset_factors) from mset_factors_unique[OF this] show ?thesis. qed lemma factorial_monoid: "factorial_monoid (mk_monoid :: 'a monoid)" by (unfold_locales; auto simp add: factors_exist factors_unique) end lemma (in idom) factorial_monoid_imp_ufd: assumes "factorial_monoid (mk_monoid :: 'a monoid)" shows "class.ufd ((*) :: 'a \ _) 1 (+) 0 (-) uminus" proof (unfold_locales) interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact assms) { fix x assume x: "x \ 0" "\ x dvd 1" note * = factors_exist[simplified, OF this] with x show "\F. mset_factors F x" by (subst(asm) factors_as_mset_factors, auto) } fix x F G assume FG: "mset_factors F x" "mset_factors G x" with mset_factors_imp_not_is_unit have x1: "\ x dvd 1" by auto from FG(1) have x0: "x \ 0" by (rule mset_factors_imp_nonzero) obtain fs gs where fsgs: "F = mset fs" "G = mset gs" using ex_mset by metis note FG = FG[unfolded this] then have 0: "0 \ set fs" "0 \ set gs" by (auto elim!: mset_factorsE) from x1 have "x \ 1" by auto note FG[folded factors_as_mset_factors[OF x0 this]] from factors_unique[OF this, simplified, OF x0 x1, folded fsgs] 0 show "rel_mset (ddvd) F G" by auto qed subsection \Preservation of Irreducibility\ locale comm_semiring_1_hom = comm_monoid_mult_hom hom + zero_hom hom for hom :: "'a :: comm_semiring_1 \ 'b :: comm_semiring_1" locale irreducibility_hom = comm_semiring_1_hom + assumes irreducible_imp_irreducible_hom: "irreducible a \ irreducible (hom a)" begin lemma hom_mset_factors: assumes F: "mset_factors F p" shows "mset_factors (image_mset hom F) (hom p)" proof (unfold mset_factors_def, intro conjI allI impI) from F show "hom p = prod_mset (image_mset hom F)" "image_mset hom F \ {#}" by (auto simp: hom_distribs) fix f' assume "f' \# image_mset hom F" then obtain f where f: "f \# F" and f'f: "f' = hom f" by auto with F irreducible_imp_irreducible_hom show "irreducible f'" unfolding f'f by auto qed end locale unit_preserving_hom = comm_semiring_1_hom + assumes is_unit_hom_if: "\x. hom x dvd 1 \ x dvd 1" begin lemma is_unit_hom_iff[simp]: "hom x dvd 1 \ x dvd 1" using is_unit_hom_if hom_dvd by force lemma irreducible_hom_imp_irreducible: assumes irr: "irreducible (hom a)" shows "irreducible a" proof (intro irreducibleI) from irr show "a \ 0" by auto from irr show "\ a dvd 1" by (auto dest: irreducible_not_unit) fix b c assume "a = b * c" then have "hom a = hom b * hom c" by (simp add: hom_distribs) with irr have "hom b dvd 1 \ hom c dvd 1" by (auto dest: irreducibleD) then show "b dvd 1 \ c dvd 1" by simp qed end locale factor_preserving_hom = unit_preserving_hom + irreducibility_hom begin lemma irreducible_hom[simp]: "irreducible (hom a) \ irreducible a" using irreducible_hom_imp_irreducible irreducible_imp_irreducible_hom by metis end lemma factor_preserving_hom_comp: assumes f: "factor_preserving_hom f" and g: "factor_preserving_hom g" shows "factor_preserving_hom (f o g)" proof- interpret f: factor_preserving_hom f by (rule f) interpret g: factor_preserving_hom g by (rule g) show ?thesis by (unfold_locales, auto simp: hom_distribs) qed context comm_semiring_isom begin sublocale unit_preserving_hom by (unfold_locales, auto) sublocale factor_preserving_hom proof (standard) fix a :: 'a assume "irreducible a" note a = this[unfolded irreducible_def] show "irreducible (hom a)" proof (rule ccontr) assume "\ irreducible (hom a)" from this[unfolded Factorial_Ring.irreducible_def,simplified] a obtain hb hc where eq: "hom a = hb * hc" and nu: "\ hb dvd 1" "\ hc dvd 1" by auto from bij obtain b where hb: "hb = hom b" by (elim bij_pointE) from bij obtain c where hc: "hc = hom c" by (elim bij_pointE) from eq[unfolded hb hc, folded hom_mult] have "a = b * c" by auto with nu hb hc have "a = b * c" "\ b dvd 1" "\ c dvd 1" by auto with a show False by auto qed qed end subsubsection\Back to divisibility\ lemma(in comm_semiring_1) mset_factors_mult: assumes F: "mset_factors F a" and G: "mset_factors G b" shows "mset_factors (F+G) (a*b)" proof(intro mset_factorsI) fix f assume "f \# F + G" then consider "f \# F" | "f \# G" by auto then show "irreducible f" by(cases, insert F G, auto) qed (insert F G, auto) lemma(in ufd) dvd_imp_subset_factors: assumes ab: "a dvd b" and F: "mset_factors F a" and G: "mset_factors G b" shows "\G'. G' \# G \ rel_mset (ddvd) F G'" proof- from F G have a0: "a \ 0" and b0: "b \ 0" by (simp_all add: mset_factors_imp_nonzero) from ab obtain c where c: "b = a * c" by (elim dvdE, auto) with b0 have c0: "c \ 0" by auto show ?thesis proof(cases "c dvd 1") case True show ?thesis proof(cases F) case empty with F show ?thesis by auto next case (add f F') with F have a: "f * prod_mset F' = a" and F': "\f. f \# F' \ irreducible f" and irrf: "irreducible f" by auto from irrf have f0: "f \ 0" and f1: "\f dvd 1" by (auto dest: irreducible_not_unit) from a c have "(f * c) * prod_mset F' = b" by (auto simp: ac_simps) moreover { have "irreducible (f * c)" using True irrf by (subst irreducible_mult_unit_right) with F' irrf have "\f'. f' \# F' + {#f * c#} \ irreducible f'" by auto } ultimately have "mset_factors (F' + {#f * c#}) b" by (intro mset_factorsI, auto) from mset_factors_unique[OF this G] have F'G: "rel_mset (ddvd) (F' + {#f * c#}) G". from True add have FF': "rel_mset (ddvd) F (F' + {#f * c#})" by (auto simp add: multiset.rel_refl intro!: rel_mset_Plus) have "rel_mset (ddvd) F G" apply(rule transpD[OF multiset.rel_transp[OF transpI] FF' F'G]) using ddvd_trans. then show ?thesis by auto qed next case False from mset_factors_exist[OF c0 this] obtain H where H: "mset_factors H c" by auto from c mset_factors_mult[OF F H] have "mset_factors (F + H) b" by auto note mset_factors_unique[OF this G] from rel_mset_split[OF this] obtain G1 G2 where "G = G1 + G2" "rel_mset (ddvd) F G1" "rel_mset (ddvd) H G2" by auto then show ?thesis by (intro exI[of _ "G1"], auto) qed qed lemma(in idom) irreducible_factor_singleton: assumes a: "irreducible a" shows "mset_factors F a \ F = {#a#}" proof(cases F) case empty with mset_factorsD show ?thesis by auto next case (add f F') show ?thesis proof assume F: "mset_factors F a" from add mset_factorsD[OF F] have *: "a = f * prod_mset F'" by auto then have fa: "f dvd a" by auto from * a have f0: "f \ 0" by auto from add have "f \# F" by auto with F have f: "irreducible f" by auto from add have "F' \# F" by auto then have unitemp: "prod_mset F' dvd 1 \ F' = {#}" proof(induct F') case empty then show ?case by auto next case (add f F') from add have "f \# F" by (simp add: mset_subset_eq_insertD) with F irreducible_not_unit have "\ f dvd 1" by auto then have "\ (prod_mset F' * f) dvd 1" by simp with add show ?case by auto qed show "F = {#a#}" proof(cases "a dvd f") case True then obtain r where "f = a * r" by (elim dvdE, auto) with * have "f = (r * prod_mset F') * f" by (auto simp: ac_simps) with f0 have "r * prod_mset F' = 1" by auto then have "prod_mset F' dvd 1" by (metis dvd_triv_right) with unitemp * add show ?thesis by auto next case False with fa a f show ?thesis by (auto simp: irreducible_altdef) qed qed (insert a, auto) qed lemma(in ufd) irreducible_dvd_imp_factor: assumes ab: "a dvd b" and a: "irreducible a" and G: "mset_factors G b" shows "\g \# G. a ddvd g" proof- from a have "mset_factors {#a#} a" by auto from dvd_imp_subset_factors[OF ab this G] obtain G' where G'G: "G' \# G" and rel: "rel_mset (ddvd) {#a#} G'" by auto with rel_mset_size size_1_singleton_mset size_single obtain g where gG': "G' = {#g#}" by fastforce from rel[unfolded this rel_mset_def] have "a ddvd g" by auto with gG' G'G show ?thesis by auto qed lemma(in idom) prod_mset_remove_units: "prod_mset F ddvd prod_mset {# f \# F. \f dvd 1 #}" proof(induct F) case (add f F) then show ?case by (cases "f = 0", auto) qed auto lemma(in comm_semiring_1) mset_factors_imp_dvd: assumes "mset_factors F x" and "f \# F" shows "f dvd x" using assms by (simp add: dvd_prod_mset mset_factors_def) lemma(in ufd) prime_elem_iff_irreducible[iff]: "prime_elem x \ irreducible x" proof (intro iffI, fact prime_elem_imp_irreducible, rule prime_elemI) assume r: "irreducible x" then show x0: "x \ 0" and x1: "\ x dvd 1" by (auto dest: irreducible_not_unit) from irreducible_factor_singleton[OF r] have *: "mset_factors {#x#} x" by auto fix a b assume "x dvd a * b" then obtain c where abxc: "a * b = x * c" by (elim dvdE, auto) show "x dvd a \ x dvd b" proof(cases "c = 0 \ a = 0 \ b = 0") case True with abxc show ?thesis by auto next case False then have a0: "a \ 0" and b0: "b \ 0" and c0: "c \ 0" by auto from x0 c0 have xc0: "x * c \ 0" by auto from x1 have xc1: "\ x * c dvd 1" by auto show ?thesis proof (cases "a dvd 1 \ b dvd 1") case False then have a1: "\ a dvd 1" and b1: "\ b dvd 1" by auto from mset_factors_exist[OF a0 a1] obtain F where Fa: "mset_factors F a" by auto then have F0: "F \ {#}" by auto from mset_factors_exist[OF b0 b1] obtain G where Gb: "mset_factors G b" by auto then have G0: "G \ {#}" by auto from mset_factors_mult[OF Fa Gb] have FGxc: "mset_factors (F + G) (x * c)" by (simp add: abxc) show ?thesis proof (cases "c dvd 1") case True from r irreducible_mult_unit_right[OF this] have "irreducible (x*c)" by simp note irreducible_factor_singleton[OF this] FGxc with F0 G0 have False by (cases F; cases G; auto) then show ?thesis by auto next case False from mset_factors_exist[OF c0 this] obtain H where "mset_factors H c" by auto with * have xHxc: "mset_factors (add_mset x H) (x * c)" by force note rel = mset_factors_unique[OF this FGxc] obtain hs where "mset hs = H" using ex_mset by auto then have "mset (x#hs) = add_mset x H" by auto from rel_mset_free[OF rel this] obtain jjs where jjsGH: "mset jjs = F + G" and rel: "list_all2 (ddvd) (x # hs) jjs" by auto then obtain j js where jjs: "jjs = j # js" by (cases jjs, auto) with rel have xj: "x ddvd j" by auto from jjs jjsGH have j: "j \ set_mset (F + G)" by (intro union_single_eq_member, auto) from j consider "j \# F" | "j \# G" by auto then show ?thesis proof(cases) case 1 with Fa have "j dvd a" by (auto intro: mset_factors_imp_dvd) with xj dvd_trans have "x dvd a" by auto then show ?thesis by auto next case 2 with Gb have "j dvd b" by (auto intro: mset_factors_imp_dvd) with xj dvd_trans have "x dvd b" by auto then show ?thesis by auto qed qed next case True then consider "a dvd 1" | "b dvd 1" by auto then show ?thesis proof(cases) case 1 then obtain d where ad: "a * d = 1" by (elim dvdE, auto) from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps) also have "... = a * d * b" by (auto simp: ac_simps) finally have "x dvd b" by (intro dvdI, auto simp: ad) then show ?thesis by auto next case 2 then obtain d where bd: "b * d = 1" by (elim dvdE, auto) from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps) also have "... = (b * d) * a" by (auto simp: ac_simps) finally have "x dvd a" by (intro dvdI, auto simp:bd) then show ?thesis by auto qed qed qed qed subsection\Results for GCDs etc.\ lemma prod_list_remove1: "(x :: 'b :: comm_monoid_mult) \ set xs \ prod_list (remove1 x xs) * x = prod_list xs" by (induct xs, auto simp: ac_simps) (* Isabelle 2015-style and generalized gcd-class without normalization and factors *) class comm_monoid_gcd = gcd + comm_semiring_1 + assumes gcd_dvd1[iff]: "gcd a b dvd a" and gcd_dvd2[iff]: "gcd a b dvd b" and gcd_greatest: "c dvd a \ c dvd b \ c dvd gcd a b" begin lemma gcd_0_0[simp]: "gcd 0 0 = 0" using gcd_greatest[OF dvd_0_right dvd_0_right, of 0] by auto lemma gcd_zero_iff[simp]: "gcd a b = 0 \ a = 0 \ b = 0" proof assume "gcd a b = 0" from gcd_dvd1[of a b, unfolded this] gcd_dvd2[of a b, unfolded this] show "a = 0 \ b = 0" by auto qed auto lemma gcd_zero_iff'[simp]: "0 = gcd a b \ a = 0 \ b = 0" using gcd_zero_iff by metis lemma dvd_gcd_0_iff[simp]: shows "x dvd gcd 0 a \ x dvd a" (is ?g1) and "x dvd gcd a 0 \ x dvd a" (is ?g2) proof- have "a dvd gcd a 0" "a dvd gcd 0 a" by (auto intro: gcd_greatest) with dvd_refl show ?g1 ?g2 by (auto dest: dvd_trans) qed lemma gcd_dvd_1[simp]: "gcd a b dvd 1 \ coprime a b" using dvd_trans[OF gcd_greatest[of _ a b], of _ 1] by (cases "a = 0 \ b = 0") (auto intro!: coprimeI elim: coprimeE) lemma dvd_imp_gcd_dvd_gcd: "b dvd c \ gcd a b dvd gcd a c" by (meson gcd_dvd1 gcd_dvd2 gcd_greatest dvd_trans) definition listgcd :: "'a list \ 'a" where "listgcd xs = foldr gcd xs 0" lemma listgcd_simps[simp]: "listgcd [] = 0" "listgcd (x # xs) = gcd x (listgcd xs)" by (auto simp: listgcd_def) lemma listgcd: "x \ set xs \ listgcd xs dvd x" proof (induct xs) case (Cons y ys) show ?case proof (cases "x = y") case False with Cons have dvd: "listgcd ys dvd x" by auto thus ?thesis unfolding listgcd_simps using dvd_trans by blast next case True thus ?thesis unfolding listgcd_simps using dvd_trans by blast qed qed simp lemma listgcd_greatest: "(\ x. x \ set xs \ y dvd x) \ y dvd listgcd xs" by (induct xs arbitrary:y, auto intro: gcd_greatest) end context Rings.dvd begin definition "is_gcd x a b \ x dvd a \ x dvd b \ (\y. y dvd a \ y dvd b \ y dvd x)" definition "some_gcd a b \ SOME x. is_gcd x a b" lemma is_gcdI[intro!]: assumes "x dvd a" "x dvd b" "\y. y dvd a \ y dvd b \ y dvd x" shows "is_gcd x a b" by (insert assms, auto simp: is_gcd_def) lemma is_gcdE[elim!]: assumes "is_gcd x a b" and "x dvd a \ x dvd b \ (\y. y dvd a \ y dvd b \ y dvd x) \ thesis" shows thesis by (insert assms, auto simp: is_gcd_def) lemma is_gcd_some_gcdI: assumes "\x. is_gcd x a b" shows "is_gcd (some_gcd a b) a b" by (unfold some_gcd_def, rule someI_ex[OF assms]) end context comm_semiring_1 begin lemma some_gcd_0[intro!]: "is_gcd (some_gcd a 0) a 0" "is_gcd (some_gcd 0 b) 0 b" by (auto intro!: is_gcd_some_gcdI intro: exI[of _ a] exI[of _ b]) lemma some_gcd_0_dvd[intro!]: "some_gcd a 0 dvd a" "some_gcd 0 b dvd b" using some_gcd_0 by auto lemma dvd_some_gcd_0[intro!]: "a dvd some_gcd a 0" "b dvd some_gcd 0 b" using some_gcd_0[of a] some_gcd_0[of b] by auto end context idom begin lemma is_gcd_connect: assumes "a \ 0" "b \ 0" shows "isgcd mk_monoid x a b \ is_gcd x a b" using assms by (force simp: isgcd_def) lemma some_gcd_connect: assumes "a \ 0" and "b \ 0" shows "somegcd mk_monoid a b = some_gcd a b" using assms by (auto intro!: arg_cong[of _ _ Eps] simp: is_gcd_connect some_gcd_def somegcd_def) end context comm_monoid_gcd begin lemma is_gcd_gcd: "is_gcd (gcd a b) a b" using gcd_greatest by auto lemma is_gcd_some_gcd: "is_gcd (some_gcd a b) a b" by (insert is_gcd_gcd, auto intro!: is_gcd_some_gcdI) lemma gcd_dvd_some_gcd: "gcd a b dvd some_gcd a b" using is_gcd_some_gcd by auto lemma some_gcd_dvd_gcd: "some_gcd a b dvd gcd a b" using is_gcd_some_gcd by (auto intro: gcd_greatest) lemma some_gcd_ddvd_gcd: "some_gcd a b ddvd gcd a b" by (auto intro: gcd_dvd_some_gcd some_gcd_dvd_gcd) lemma some_gcd_dvd: "some_gcd a b dvd d \ gcd a b dvd d" "d dvd some_gcd a b \ d dvd gcd a b" using some_gcd_ddvd_gcd[of a b] by (auto dest:dvd_trans) end class idom_gcd = comm_monoid_gcd + idom begin interpretation raw: comm_monoid_cancel "mk_monoid :: 'a monoid" by (unfold_locales, auto intro: mult_commute mult_assoc) interpretation raw: gcd_condition_monoid "mk_monoid :: 'a monoid" by (unfold_locales, auto simp: is_gcd_connect intro!: exI[of _ "gcd _ _"] dest: gcd_greatest) lemma gcd_mult_ddvd: "d * gcd a b ddvd gcd (d * a) (d * b)" proof (cases "d = 0") case True then show ?thesis by auto next case d0: False show ?thesis proof (cases "a = 0 \ b = 0") case False note some_gcd_ddvd_gcd[of a b] with d0 have "d * gcd a b ddvd d * some_gcd a b" by auto also have "d * some_gcd a b ddvd some_gcd (d * a) (d * b)" using False d0 raw.gcd_mult by (simp add: some_gcd_connect) also note some_gcd_ddvd_gcd finally show ?thesis. next case True with d0 show ?thesis apply (elim disjE) apply (rule ddvd_trans[of _ "d * b"]; force) apply (rule ddvd_trans[of _ "d * a"]; force) done qed qed lemma gcd_greatest_mult: assumes cad: "c dvd a * d" and cbd: "c dvd b * d" shows "c dvd gcd a b * d" proof- from gcd_greatest[OF assms] have c: "c dvd gcd (d * a) (d * b)" by (auto simp: ac_simps) note gcd_mult_ddvd[of d a b] then have "gcd (d * a) (d * b) dvd gcd a b * d" by (auto simp: ac_simps) from dvd_trans[OF c this] show ?thesis . qed lemma listgcd_greatest_mult: "(\ x :: 'a. x \ set xs \ y dvd x * z) \ y dvd listgcd xs * z" proof (induct xs) case (Cons x xs) from Cons have "y dvd x * z" "y dvd listgcd xs * z" by auto thus ?case unfolding listgcd_simps by (rule gcd_greatest_mult) qed (simp) lemma dvd_factor_mult_gcd: assumes dvd: "k dvd p * q" "k dvd p * r" and q0: "q \ 0" and r0: "r \ 0" shows "k dvd p * gcd q r" proof - from dvd gcd_greatest[of k "p * q" "p * r"] have "k dvd gcd (p * q) (p * r)" by simp also from gcd_mult_ddvd[of p q r] have "... dvd (p * gcd q r)" by auto finally show ?thesis . qed lemma coprime_mult_cross_dvd: assumes coprime: "coprime p q" and eq: "p' * p = q' * q" shows "p dvd q'" (is ?g1) and "q dvd p'" (is ?g2) proof (atomize(full), cases "p = 0 \ q = 0") case True then show "?g1 \ ?g2" proof assume p0: "p = 0" with coprime have "q dvd 1" by auto with eq p0 show ?thesis by auto next assume q0: "q = 0" with coprime have "p dvd 1" by auto with eq q0 show ?thesis by auto qed next case False { fix p q r p' q' :: 'a assume cop: "coprime p q" and eq: "p' * p = q' * q" and p: "p \ 0" and q: "q \ 0" and r: "r dvd p" "r dvd q" let ?gcd = "gcd q p" from eq have "p' * p dvd q' * q" by auto hence d1: "p dvd q' * q" by (rule dvd_mult_right) have d2: "p dvd q' * p" by auto from dvd_factor_mult_gcd[OF d1 d2 q p] have 1: "p dvd q' * ?gcd" . from q p have 2: "?gcd dvd q" by auto from q p have 3: "?gcd dvd p" by auto from cop[unfolded coprime_def', rule_format, OF 3 2] have "?gcd dvd 1" . from 1 dvd_mult_unit_iff[OF this] have "p dvd q'" by auto } note main = this from main[OF coprime eq,of 1] False coprime coprime_commute main[OF _ eq[symmetric], of 1] show "?g1 \ ?g2" by auto qed end subclass (in ring_gcd) idom_gcd by (unfold_locales, auto) lemma coprime_rewrites: "comm_monoid_mult.coprime ((*)) 1 = coprime" apply (intro ext) apply (subst comm_monoid_mult.coprime_def') apply (unfold_locales) apply (unfold dvd_rewrites) apply (fold coprime_def') .. (* TODO: incorporate into the default class hierarchy *) locale gcd_condition = fixes ty :: "'a :: idom itself" assumes gcd_exists: "\a b :: 'a. \x. is_gcd x a b" begin sublocale idom_gcd "(*)" "1 :: 'a" "(+)" 0 "(-)" uminus some_gcd rewrites "dvd.dvd ((*)) = (dvd)" and "comm_monoid_mult.coprime ((*) ) 1 = Unique_Factorization.coprime" proof- have "is_gcd (some_gcd a b) a b" for a b :: 'a by (intro is_gcd_some_gcdI gcd_exists) from this[unfolded is_gcd_def] show "class.idom_gcd (*) (1 :: 'a) (+) 0 (-) uminus some_gcd" by (unfold_locales, auto simp: dvd_rewrites) qed (simp_all add: dvd_rewrites coprime_rewrites) end instance semiring_gcd \ comm_monoid_gcd by (intro_classes, auto) lemma listgcd_connect: "listgcd = gcd_list" proof (intro ext) fix xs :: "'a list" show "listgcd xs = gcd_list xs" by(induct xs, auto) qed interpretation some_gcd: gcd_condition "TYPE('a::ufd)" proof(unfold_locales, intro exI) interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact factorial_monoid) note d = dvd.dvd_def some_gcd_def carrier_0 fix a b :: 'a show "is_gcd (some_gcd a b) a b" proof (cases "a = 0 \ b = 0") case True thus ?thesis using some_gcd_0 by auto next case False with gcdof_exists[of a b] show ?thesis by (auto intro!: is_gcd_some_gcdI simp add: is_gcd_connect some_gcd_connect) qed qed lemma some_gcd_listgcd_dvd_listgcd: "some_gcd.listgcd xs dvd listgcd xs" by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd) lemma listgcd_dvd_some_gcd_listgcd: "listgcd xs dvd some_gcd.listgcd xs" by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd) context factorial_ring_gcd begin text \Do not declare the following as subclass, to avoid conflict in \field \ gcd_condition\ vs. \factorial_ring_gcd \ gcd_condition\. \ sublocale as_ufd: ufd proof(unfold_locales, goal_cases) case (1 x) from prime_factorization_exists[OF \x \ 0\] obtain F where f: "\f. f \# F \ prime_elem f" and Fx: "normalize (prod_mset F) = normalize x" by auto from associatedE2[OF Fx] obtain u where u: "is_unit u" "x = u * prod_mset F" by blast from \\ is_unit x\ Fx have "F \ {#}" by auto then obtain g G where F: "F = add_mset g G" by (cases F, auto) then have "g \# F" by auto with f[OF this]prime_elem_iff_irreducible irreducible_mult_unit_left[OF unit_factor_is_unit[OF \x \ 0\]] have g: "irreducible (u * g)" using u(1) by (subst irreducible_mult_unit_left) simp_all show ?case proof (intro exI conjI mset_factorsI) show "prod_mset (add_mset (u * g) G) = x" using \x \ 0\ by (simp add: F ac_simps u) fix f assume "f \# add_mset (u * g) G" with f[unfolded F] g prime_elem_iff_irreducible show "irreducible f" by auto qed auto next case (2 x F G) note transpD[OF multiset.rel_transp[OF ddvd_transp],trans] obtain fs where F: "F = mset fs" by (metis ex_mset) have "list_all2 (ddvd) fs (map normalize fs)" by (intro list_all2_all_nthI, auto) then have FH: "rel_mset (ddvd) F (image_mset normalize F)" by (unfold rel_mset_def F, force) also have FG: "image_mset normalize F = image_mset normalize G" proof (intro prime_factorization_unique'') from 2 have xF: "x = prod_mset F" and xG: "x = prod_mset G" by auto from xF have "normalize x = normalize (prod_mset (image_mset normalize F))" by (simp add: normalize_prod_mset_normalize) with xG have nFG: "\ = normalize (prod_mset (image_mset normalize G))" by (simp_all add: normalize_prod_mset_normalize) then show "normalize (\i\#image_mset normalize F. i) = normalize (\i\#image_mset normalize G. i)" by auto next from 2 prime_elem_iff_irreducible have "f \# F \ prime_elem f" "g \# G \ prime_elem g" for f g by (auto intro: prime_elemI) then show " Multiset.Ball (image_mset normalize F) prime" "Multiset.Ball (image_mset normalize G) prime" by auto qed also obtain gs where G: "G = mset gs" by (metis ex_mset) have "list_all2 ((ddvd)\\) gs (map normalize gs)" by (intro list_all2_all_nthI, auto) then have "rel_mset (ddvd) (image_mset normalize G) G" by (subst multiset.rel_flip[symmetric], unfold rel_mset_def G, force) finally show ?case. qed end instance int :: ufd by (intro class.ufd.of_class.intro as_ufd.ufd_axioms) instance int :: idom_gcd by (intro_classes, auto) instance field \ ufd by (intro_classes, auto simp: dvd_field_iff) end diff --git a/thys/CakeML/generated/LemExtraDefs.thy b/thys/CakeML/generated/LemExtraDefs.thy --- a/thys/CakeML/generated/LemExtraDefs.thy +++ b/thys/CakeML/generated/LemExtraDefs.thy @@ -1,1257 +1,1241 @@ (*========================================================================*) (* Lem *) (* *) (* Dominic Mulligan, University of Cambridge *) (* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) (* Gabriel Kerneis, University of Cambridge *) (* Kathy Gray, University of Cambridge *) (* Peter Boehm, University of Cambridge (while working on Lem) *) (* Peter Sewell, University of Cambridge *) (* Scott Owens, University of Kent *) (* Thomas Tuerk, University of Cambridge *) (* Brian Campbell, University of Edinburgh *) (* Shaked Flur, University of Cambridge *) (* Thomas Bauereiss, University of Cambridge *) (* Stephen Kell, University of Cambridge *) (* Thomas Williams *) (* Lars Hupel *) (* Basile Clement *) (* *) (* The Lem sources are copyright 2010-2018 *) (* by the authors above and Institut National de Recherche en *) (* Informatique et en Automatique (INRIA). *) (* *) (* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) (* are distributed under the license below. The former are distributed *) (* under the LGPLv2, as in the LICENSE file. *) (* *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in the *) (* documentation and/or other materials provided with the distribution. *) (* 3. The names of the authors may not be used to endorse or promote *) (* products derived from this software without specific prior written *) (* permission. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) (* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) (* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) (* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) (* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) (* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) (* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) (* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) (* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) (* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (*========================================================================*) chapter \Auxiliary Definitions needed by Lem\ theory "LemExtraDefs" imports Main "HOL-Combinatorics.List_Permutation" "HOL-Library.While_Combinator" begin hide_const (open) sign subsection \General\ consts failwith :: " 'a \ 'b" subsection \Lists\ fun index :: " 'a list \ nat \ 'a option " where "index [] n = None" | "index (x # xs) 0 = Some x" | "index (x # xs) (Suc n) = index xs n" lemma index_eq_some [simp]: "index l n = Some x \ (n < length l \ (x = l ! n))" proof (induct l arbitrary: n x) case Nil thus ?case by simp next case (Cons e es n x) note ind_hyp = this show ?case proof (cases n) case 0 thus ?thesis by auto next case (Suc n') with ind_hyp show ?thesis by simp qed qed lemma index_eq_none [simp]: "index l n = None \ length l \ n" by (rule iffD1[OF Not_eq_iff]) auto lemma index_simps [simp]: "length l \ n \ index l n = None" "n < length l \ index l n = Some (l ! n)" by (simp_all) fun find_indices :: "('a \ bool) \ 'a list \ nat list" where "find_indices P [] = []" | "find_indices P (x # xs) = (if P x then 0 # (map Suc (find_indices P xs)) else (map Suc (find_indices P xs)))" lemma length_find_indices : "length (find_indices P l) \ length l" by (induct l) auto lemma sorted_map_suc : "sorted l \ sorted (map Suc l)" by (induct l) (simp_all) lemma sorted_find_indices : "sorted (find_indices P xs)" proof (induct xs) case Nil thus ?case by simp next case (Cons x xs) from sorted_map_suc[OF this] show ?case by (simp) qed lemma find_indices_set [simp] : "set (find_indices P l) = {i. i < length l \ P (l ! i)}" proof (intro set_eqI) fix i show "i \ set (find_indices P l) \ (i \ {i. i < length l \ P (l ! i)})" proof (induct l arbitrary: i) case Nil thus ?case by simp next case (Cons x l' i) note ind_hyp = this show ?case proof (cases i) case 0 thus ?thesis by auto next case (Suc i') with ind_hyp[of i'] show ?thesis by auto qed qed qed definition find_index where "find_index P xs = (case find_indices P xs of [] \ None | i # _ \ Some i)" lemma find_index_eq_some [simp] : "(find_index P xs = Some ii) \ (ii < length xs \ P (xs ! ii) \ (\i' < ii. \(P (xs ! i'))))" (is "?lhs = ?rhs") proof (cases "find_indices P xs") case Nil with find_indices_set[of P xs] show ?thesis unfolding find_index_def by auto next case (Cons i il) note find_indices_eq = this from sorted_find_indices[of P xs] find_indices_eq have "sorted (i # il)" by simp hence i_leq: "\i'. i' \ set (i # il) \ i \ i'" by auto from find_indices_set[of P xs, unfolded find_indices_eq] have set_i_il_eq:"\i'. i' \ set (i # il) = (i' < length xs \ P (xs ! i'))" by simp have lhs_eq: "find_index P xs = Some i" unfolding find_index_def find_indices_eq by simp show ?thesis proof (intro iffI) assume ?lhs with lhs_eq have ii_eq[simp]: "ii = i" by simp from set_i_il_eq[of i] i_leq[unfolded set_i_il_eq] show ?rhs by auto (metis leD less_trans) next assume ?rhs with set_i_il_eq[of ii] have "ii \ set (i # il) \ (ii \ i)" by (metis leI length_pos_if_in_set nth_Cons_0 nth_mem set_i_il_eq) with i_leq [of ii] have "i = ii" by simp thus ?lhs unfolding lhs_eq by simp qed qed lemma find_index_eq_none [simp] : "(find_index P xs = None) \ (\x \ set xs. \(P x))" (is "?lhs = ?rhs") proof (rule iffD1[OF Not_eq_iff], intro iffI) assume "\ ?lhs" then obtain i where "find_index P xs = Some i" by auto hence "i < length xs \ P (xs ! i)" by simp thus "\ ?rhs" by auto next let ?p = "(\i. i < length xs \ P(xs ! i))" assume "\ ?rhs" then obtain i where "?p i" by (metis in_set_conv_nth) from LeastI [of ?p, OF \?p i\] have "?p (Least ?p)" . hence "find_index P xs = Some (Least ?p)" by (subst find_index_eq_some) (metis (mono_tags) less_trans not_less_Least) thus "\ ?lhs" by blast qed definition genlist where "genlist f n = map f (upt 0 n)" lemma genlist_length [simp] : "length (genlist f n) = n" unfolding genlist_def by simp lemma genlist_simps [simp]: "genlist f 0 = []" "genlist f (Suc n) = genlist f n @ [f n]" unfolding genlist_def by auto definition split_at where "split_at n l = (take n l, drop n l)" fun delete_first :: "('a \ bool) \ 'a list \ ('a list) option " where "delete_first P [] = None" | "delete_first P (x # xs) = (if (P x) then Some xs else map_option (\xs'. x # xs') (delete_first P xs))" declare delete_first.simps [simp del] lemma delete_first_simps [simp] : "delete_first P [] = None" "P x \ delete_first P (x # xs) = Some xs" "\(P x) \ delete_first P (x # xs) = map_option (\xs'. x # xs') (delete_first P xs)" unfolding delete_first.simps by auto lemmas delete_first_unroll = delete_first.simps(2) lemma delete_first_eq_none [simp] : "delete_first P l = None \ (\x \ set l. \ (P x))" by (induct l) (auto simp add: delete_first_unroll) lemma delete_first_eq_some : "delete_first P l = (Some l') \ (\l1 x l2. P x \ (\x \ set l1. \(P x)) \ (l = l1 @ (x # l2)) \ (l' = l1 @ l2))" (is "?lhs l l' = (\l1 x l2. ?rhs_body l1 x l2 l l')") proof (induct l arbitrary: l') case Nil thus ?case by simp next case (Cons e l l') note ind_hyp = this show ?case proof (cases "P e") case True show ?thesis proof (rule iffI) assume "?lhs (e # l) l'" with \P e\ have "l = l'" by simp with \P e\ have "?rhs_body [] e l' (e # l) l'" by simp thus "\l1 x l2. ?rhs_body l1 x l2 (e # l) l'" by blast next assume "\l1 x l2. ?rhs_body l1 x l2 (e # l) l'" then obtain l1 x l2 where body_ok: "?rhs_body l1 x l2 (e # l) l'" by blast from body_ok \P e\ have l1_eq[simp]: "l = l'" by (cases l1) (simp_all) with \P e\ show "?lhs (e # l) l'" by simp qed next case False define rhs_pred where "rhs_pred \ \l1 x l2 l l'. ?rhs_body l1 x l2 l l'" have rhs_fold: "\l1 x l2 l l'. ?rhs_body l1 x l2 l l' = rhs_pred l1 x l2 l l'" unfolding rhs_pred_def by simp have "(\z l1 x l2. rhs_pred l1 x l2 l z \ e # z = l') = (\l1 x l2. rhs_pred l1 x l2 (e # l) l')" proof (intro iffI) assume "\z l1 x l2. rhs_pred l1 x l2 l z \ e # z = l'" then obtain z l1 x l2 where "rhs_pred l1 x l2 l z" and l'_eq: "l' = e # z" by auto with \\(P e)\ have "rhs_pred (e # l1) x l2 (e # l) l'" unfolding rhs_pred_def by simp thus "\l1 x l2. rhs_pred l1 x l2 (e # l) l'" by blast next assume "\l1 x l2. rhs_pred l1 x l2 (e # l) l'" then obtain l1 x l2 where "rhs_pred l1 x l2 (e # l) l'" by blast with \\ (P e)\ obtain l1' where l1_eq[simp]: "l1 = e # l1'" unfolding rhs_pred_def by (cases l1) (auto) with \rhs_pred l1 x l2 (e # l) l'\ have "rhs_pred l1' x l2 l (l1' @ l2) \ e # (l1' @ l2) = l'" unfolding rhs_pred_def by (simp) thus "\z l1 x l2. rhs_pred l1 x l2 l z \ e # z = l'" by blast qed with \\ P e\ show ?thesis unfolding rhs_fold by (simp add: ind_hyp[unfolded rhs_fold]) qed qed lemma perm_eval [code] : "perm [] l \ l = []" (is ?g1) "perm (x # xs) l \ (case delete_first (\e. e = x) l of None => False | Some l' => perm xs l')" (is ?g2) proof - show ?g1 by auto next show ?g2 proof (cases "delete_first (\e. e = x) l") case None note del_eq = this hence "x \ set l" by auto with perm_set_eq [of "x # xs" l] have "\ perm (x # xs) l" by auto thus ?thesis unfolding del_eq by simp next case (Some l') note del_eq = this from del_eq[unfolded delete_first_eq_some] obtain l1 l2 where l_eq: "l = l1 @ [x] @ l2" and l'_eq: "l' = l1 @ l2" by auto have "(x # xs <~~> l1 @ x # l2) = (xs <~~> l1 @ l2)" proof - from perm_append_swap [of l1 "[x]"] perm_append2 [of "l1 @ [x]" "x # l1" l2] have "l1 @ x # l2 <~~> x # (l1 @ l2)" by simp hence "x # xs <~~> l1 @ x # l2 \ x # xs <~~> x # (l1 @ l2)" - by (metis perm.trans perm_sym) + by simp thus ?thesis by simp qed with del_eq l_eq l'_eq show ?thesis by simp qed qed fun sorted_by :: "('a \ 'a \ bool)\ 'a list \ bool " where "sorted_by cmp [] = True" | "sorted_by cmp [_] = True" | "sorted_by cmp (x1 # x2 # xs) = ((cmp x1 x2) \ sorted_by cmp (x2 # xs))" lemma sorted_by_lesseq [simp] : "sorted_by ((\) :: ('a::{linorder}) => 'a => bool) = sorted" proof (rule ext) fix l :: "'a list" show "sorted_by (\) l = sorted l" proof (induct l) case Nil thus ?case by simp next case (Cons x xs) thus ?case by (cases xs) (simp_all del: sorted.simps(2) add: sorted2_simps) qed qed lemma sorted_by_cons_imp : "sorted_by cmp (x # xs) \ sorted_by cmp xs" by (cases xs) simp_all lemma sorted_by_cons_trans : assumes trans_cmp: "transp cmp" shows "sorted_by cmp (x # xs) = ((\x' \ set xs . cmp x x') \ sorted_by cmp xs)" proof (induct xs arbitrary: x) case Nil thus ?case by simp next case (Cons x2 xs x1) note ind_hyp = this from trans_cmp show ?case by (auto simp add: ind_hyp transp_def) qed fun insert_sort_insert_by :: "('a \ 'a \ bool)\ 'a \ 'a list \ 'a list " where "insert_sort_insert_by cmp e ([]) = ( [e])" | "insert_sort_insert_by cmp e (x # xs) = ( if cmp e x then (e # (x # xs)) else x # (insert_sort_insert_by cmp e xs))" lemma insert_sort_insert_by_length [simp] : "length (insert_sort_insert_by cmp e l) = Suc (length l)" by (induct l) auto lemma insert_sort_insert_by_set [simp] : "set (insert_sort_insert_by cmp e l) = insert e (set l)" by (induct l) auto lemma insert_sort_insert_by_perm : "(insert_sort_insert_by cmp e l) <~~> (e # l)" -proof (induct l) - case Nil thus ?case by simp -next - case (Cons e2 l') - note ind_hyp = this - - have "e2 # e # l' <~~> e # e2 # l'" by (rule perm.swap) - hence "e2 # insert_sort_insert_by cmp e l' <~~> e # e2 # l'" - using ind_hyp by (metis cons_perm_eq perm.trans) - thus ?case by simp -qed + by (induction l) simp_all lemma insert_sort_insert_by_sorted_by : assumes cmp_cases: "\y. y \ set l \ \ (cmp e y) \ cmp y e" assumes cmp_trans: "transp cmp" shows "sorted_by cmp l \ sorted_by cmp (insert_sort_insert_by cmp e l)" using cmp_cases proof (induct l) case Nil thus ?case by simp next case (Cons x1 l') note ind_hyp = Cons(1) note sorted_x1_l' = Cons(2) note cmp_cases = Cons(3) show ?case proof (cases l') case Nil with cmp_cases show ?thesis by simp next case (Cons x2 l'') note l'_eq = this from l'_eq sorted_x1_l' have "cmp x1 x2" "sorted_by cmp l'" by simp_all show ?thesis proof (cases "cmp e x1") case True with \cmp x1 x2\ \sorted_by cmp l'\ have "sorted_by cmp (x1 # l')" unfolding l'_eq by (simp) with \cmp e x1\ show ?thesis by simp next case False with cmp_cases have "cmp x1 e" by simp have "\x'. x' \ set l' \ cmp x1 x'" proof - fix x' assume "x' \ set l'" hence "x' = x2 \ cmp x2 x'" using \sorted_by cmp l'\ l'_eq sorted_by_cons_trans [OF cmp_trans, of x2 l''] by auto with transpD[OF cmp_trans, of x1 x2 x'] \cmp x1 x2\ show "cmp x1 x'" by blast qed hence "sorted_by cmp (x1 # insert_sort_insert_by cmp e l')" using ind_hyp [OF \sorted_by cmp l'\] \cmp x1 e\ cmp_cases unfolding sorted_by_cons_trans[OF cmp_trans] by simp with \\(cmp e x1)\ show ?thesis by simp qed qed qed fun insert_sort_by :: "('a \ 'a \ bool) \ 'a list \ 'a list " where "insert_sort_by cmp [] = []" | "insert_sort_by cmp (x # xs) = insert_sort_insert_by cmp x (insert_sort_by cmp xs)" lemma insert_sort_by_perm : "(insert_sort_by cmp l) <~~> l" -proof (induct l) - case Nil thus ?case by simp -next - case (Cons x l) - thus ?case - by simp (metis cons_perm_eq insert_sort_insert_by_perm perm.trans) -qed + by (induction l) (simp_all add: insert_sort_insert_by_perm) lemma insert_sort_by_length [simp]: "length (insert_sort_by cmp l) = length l" by (induct l) auto lemma insert_sort_by_set [simp]: "set (insert_sort_by cmp l) = set l" by (induct l) auto definition sort_by where "sort_by = insert_sort_by" lemma sort_by_simps [simp]: "length (sort_by cmp l) = length l" "set (sort_by cmp l) = set l" unfolding sort_by_def by simp_all lemma sort_by_perm : "sort_by cmp l <~~> l" unfolding sort_by_def by (simp add: insert_sort_by_perm) subsection \Maps\ definition map_image :: "('v \ 'w) \ ('k, 'v) map \ ('k, 'w) map" where "map_image f m = (\k. map_option f (m k))" definition map_domain_image :: "('k \ 'v \ 'w) \ ('k, 'v) map \ ('k, 'w) map" where "map_domain_image f m = (\k. map_option (f k) (m k))" lemma map_image_simps [simp]: "(map_image f m) k = None \ m k = None" "(map_image f m) k = Some x \ (\x'. (m k = Some x') \ (x = f x'))" "(map_image f Map.empty) = Map.empty" "(map_image f (m (k \ v)) = (map_image f m) (k \ f v))" unfolding map_image_def by auto lemma map_image_dom_ran [simp]: "dom (map_image f m) = dom m" "ran (map_image f m) = f ` (ran m)" unfolding dom_def ran_def by auto definition map_to_set :: "('k, 'v) map \ ('k * 'v) set" where "map_to_set m = { (k, v) . m k = Some v }" lemma map_to_set_simps [simp] : "map_to_set Map.empty = {}" (is ?g1) "map_to_set (m ((k::'k) \ (v::'v))) = (insert (k, v) (map_to_set (m |` (- {k}))))" (is ?g2) proof - show ?g1 unfolding map_to_set_def by simp next show ?g2 proof (rule set_eqI) fix kv :: "('k * 'v)" obtain k' v' where kv_eq[simp]: "kv = (k', v')" by (rule prod.exhaust) show "(kv \ map_to_set (m(k \ v))) = (kv \ insert (k, v) (map_to_set (m |` (- {k}))))" by (auto simp add: map_to_set_def) qed qed subsection \Sets\ definition "set_choose s \ (SOME x. (x \ s))" definition without_trans_edges :: "('a \ 'a) set \ ('a \ 'a) set" where "without_trans_edges S \ let ts = trancl S in { (x, y) \ S. \z \ snd ` S. x \ z \ y \ z \ \ ((x, z) \ ts \ (z, y) \ ts)}" definition unbounded_lfp :: "'a set \ ('a set \ 'a set) \ 'a set" where "unbounded_lfp S f \ while (\x. x \ S) f S" definition unbounded_gfp :: "'a set \ ('a set \ 'a set) \ 'a set" where "unbounded_gfp S f \ while (\x. S \ x) f S" lemma set_choose_thm[simp]: "s \ {} \ (set_choose s) \ s" unfolding set_choose_def by (rule someI_ex) auto lemma set_choose_sing [simp]: "set_choose {x} = x" unfolding set_choose_def by auto lemma set_choose_code [code]: "set_choose (set [x]) = x" by auto lemma set_choose_in [intro] : assumes "s \ {}" shows "set_choose s \ s" proof - from \s \ {}\ obtain x where "x \ s" by auto thus ?thesis unfolding set_choose_def by (rule someI) qed definition set_case where "set_case s c_empty c_sing c_else = (if (s = {}) then c_empty else (if (card s = 1) then c_sing (set_choose s) else c_else))" lemma set_case_simps [simp] : "set_case {} c_empty c_sing c_else = c_empty" "set_case {x} c_empty c_sing c_else = c_sing x" "card s > 1 \ set_case s c_empty c_sing c_else = c_else" "\(finite s) \ set_case s c_empty c_sing c_else = c_else" unfolding set_case_def by auto lemma set_case_simp_insert2 [simp] : assumes x12_neq: "x1 \ x2" shows "set_case (insert x1 (insert x2 xs)) c_empty c_sing c_else = c_else" proof (cases "finite xs") case False thus ?thesis by (simp) next case True note fin_xs = this have "card {x1,x2} \ card (insert x1 (insert x2 xs))" by (rule card_mono) (auto simp add: fin_xs) with x12_neq have "1 < card (insert x1 (insert x2 xs))" by simp thus ?thesis by auto qed lemma set_case_code [code] : "set_case (set []) c_empty c_sing c_else = c_empty" "set_case (set [x]) c_empty c_sing c_else = c_sing x" "set_case (set (x1 # x2 # xs)) c_empty c_sing c_else = (if (x1 = x2) then set_case (set (x2 # xs)) c_empty c_sing c_else else c_else)" by auto definition set_lfp:: "'a set \ ('a set \ 'a set) \ 'a set" where "set_lfp s f = lfp (\s'. f s' \ s)" lemma set_lfp_tail_rec_def : assumes mono_f: "mono f" shows "set_lfp s f = (if (f s) \ s then s else (set_lfp (s \ f s) f))" (is "?ls = ?rs") proof (cases "f s \ s") case True note fs_sub_s = this from fs_sub_s have "\{u. f u \ s \ u} = s" by auto hence "?ls = s" unfolding set_lfp_def lfp_def . with fs_sub_s show "?ls = ?rs" by simp next case False note not_fs_sub_s = this from mono_f have mono_f': "mono (\s'. f s' \ s)" unfolding mono_def by auto have "\{u. f u \ s \ u} = \{u. f u \ (s \ f s) \ u}" (is "\?S1 = \?S2") proof have "?S2 \ ?S1" by auto thus "\?S1 \ \?S2" by (rule Inf_superset_mono) next { fix e assume "e \ \?S2" hence S2_prop: "\s'. f s' \ s' \ s \ s' \ f s \ s' \ e \ s'" by simp { fix s' assume "f s' \ s'" "s \ s'" from mono_f \s \ s'\ have "f s \ f s'" unfolding mono_def by simp with \f s' \ s'\ have "f s \ s'" by simp with \f s' \ s'\ \s \ s'\ S2_prop have "e \ s'" by simp } hence "e \ \?S1" by simp } thus "\?S2 \ \?S1" by auto qed hence "?ls = (set_lfp (s \ f s) f)" unfolding set_lfp_def lfp_def . with not_fs_sub_s show "?ls = ?rs" by simp qed lemma set_lfp_simps [simp] : "mono f \ f s \ s \ set_lfp s f = s" "mono f \ \(f s \ s) \ set_lfp s f = (set_lfp (s \ f s) f)" by (metis set_lfp_tail_rec_def)+ fun insert_in_list_at_arbitrary_pos where "insert_in_list_at_arbitrary_pos x [] = {[x]}" | "insert_in_list_at_arbitrary_pos x (y # ys) = insert (x # y # ys) ((\l. y # l) ` (insert_in_list_at_arbitrary_pos x ys))" lemma insert_in_list_at_arbitrary_pos_thm : "xl \ insert_in_list_at_arbitrary_pos x l \ (\l1 l2. l = l1 @ l2 \ xl = l1 @ [x] @ l2)" proof (induct l arbitrary: xl) case Nil thus ?case by simp next case (Cons y l xyl) note ind_hyp = this show ?case proof (rule iffI) assume xyl_in: "xyl \ insert_in_list_at_arbitrary_pos x (y # l)" show "\l1 l2. y # l = l1 @ l2 \ xyl = l1 @ [x] @ l2" proof (cases "xyl = x # y # l") case True hence "y # l = [] @ (y # l) \ xyl = [] @ [x] @ (y # l)" by simp thus ?thesis by blast next case False with xyl_in have "xyl \ (#) y ` insert_in_list_at_arbitrary_pos x l" by simp with ind_hyp obtain l1 l2 where "l = l1 @ l2 \ xyl = y # l1 @ x # l2" by (auto simp add: image_def Bex_def) hence "y # l = (y # l1) @ l2 \ xyl = (y # l1) @ [x] @ l2" by simp thus ?thesis by blast qed next assume "\l1 l2. y # l = l1 @ l2 \ xyl = l1 @ [x] @ l2" then obtain l1 l2 where yl_eq: "y # l = l1 @ l2" and xyl_eq: "xyl = l1 @ [x] @ l2" by blast show "xyl \ insert_in_list_at_arbitrary_pos x (y # l)" proof (cases l1) case Nil with yl_eq xyl_eq have "xyl = x # y # l" by simp thus ?thesis by simp next case (Cons y' l1') with yl_eq have l1_eq: "l1 = y # l1'" and l_eq: "l = l1' @ l2" by simp_all have "\l1'' l2''. l = l1'' @ l2'' \ l1' @ [x] @ l2 = l1'' @ [x] @ l2''" apply (rule_tac exI[where x = l1']) apply (rule_tac exI [where x = l2]) apply (simp add: l_eq) done hence "(l1' @ [x] @ l2) \ insert_in_list_at_arbitrary_pos x l" unfolding ind_hyp by blast hence "\l'. l' \ insert_in_list_at_arbitrary_pos x l \ l1 @ x # l2 = y # l'" by (rule_tac exI [where x = "l1' @ [x] @ l2"]) (simp add: l1_eq) thus ?thesis by (simp add: image_def Bex_def xyl_eq) qed qed qed definition list_of_set_set :: "'a set \ ('a list) set" where "list_of_set_set s = { l . (set l = s) \ distinct l }" lemma list_of_set_set_empty [simp]: "list_of_set_set {} = {[]}" unfolding list_of_set_set_def by auto lemma list_of_set_set_insert [simp] : "list_of_set_set (insert x s) = \ ((insert_in_list_at_arbitrary_pos x) ` (list_of_set_set (s - {x})))" (is "?lhs = ?rhs") proof (intro set_eqI) fix l have "(set l = insert x s \ distinct l) \ (\l1 l2. set (l1 @ l2) = s - {x} \ distinct (l1 @ l2) \ l = l1 @ x # l2)" proof (intro iffI) assume "set l = insert x s \ distinct l" hence set_l_eq: "set l = insert x s" and "distinct l" by simp_all from \set l = insert x s\ have "x \ set l" by simp then obtain l1 l2 where l_eq: "l = l1 @ x # l2" unfolding in_set_conv_decomp by blast from \distinct l\ l_eq have "distinct (l1 @ l2)" and x_nin: "x \ set (l1 @ l2)" by auto from x_nin set_l_eq[unfolded l_eq] have set_l12_eq: "set (l1 @ l2) = s - {x}" by auto from \distinct (l1 @ l2)\ l_eq set_l12_eq show "\l1 l2. set (l1 @ l2) = s - {x} \ distinct (l1 @ l2) \ l = l1 @ x # l2" by blast next assume "\l1 l2. set (l1 @ l2) = s - {x} \ distinct (l1 @ l2) \ l = l1 @ x # l2" then obtain l1 l2 where "set (l1 @ l2) = s - {x}" "distinct (l1 @ l2)" "l = l1 @ x # l2" by blast thus "set l = insert x s \ distinct l" by auto qed thus "l \ list_of_set_set (insert x s) \ l \ (\ ((insert_in_list_at_arbitrary_pos x) ` (list_of_set_set (s - {x}))))" unfolding list_of_set_set_def by (simp add: insert_in_list_at_arbitrary_pos_thm ex_simps[symmetric] del: ex_simps) qed lemma list_of_set_set_code [code]: "list_of_set_set (set []) = {[]}" "list_of_set_set (set (x # xs)) = \ ((insert_in_list_at_arbitrary_pos x) ` (list_of_set_set ((set xs) - {x})))" by simp_all lemma list_of_set_set_is_empty : "list_of_set_set s = {} \ \ (finite s)" proof - have "finite s \ (\l. set l = s \ distinct l)" proof (rule iffI) assume "\l. set l = s \ distinct l" then obtain l where "s = set l" by blast thus "finite s" by simp next assume "finite s" thus "\l. set l = s \ distinct l" proof (induct s) case empty show ?case by auto next case (insert e s) note e_nin_s = insert(2) from insert(3) obtain l where set_l: "set l = s" and dist_l: "distinct l" by blast from set_l have set_el: "set (e # l) = insert e s" by auto from dist_l set_l e_nin_s have dist_el: "distinct (e # l)" by simp from set_el dist_el show ?case by blast qed qed thus ?thesis unfolding list_of_set_set_def by simp qed definition list_of_set :: "'a set \ 'a list" where "list_of_set s = set_choose (list_of_set_set s)" lemma list_of_set [simp] : assumes fin_s: "finite s" shows "set (list_of_set s) = s" "distinct (list_of_set s)" proof - from fin_s list_of_set_set_is_empty[of s] have "\ (list_of_set_set s = {})" by simp hence "list_of_set s \ list_of_set_set s" unfolding list_of_set_def by (rule set_choose_thm) thus "set (list_of_set s) = s" "distinct (list_of_set s)" unfolding list_of_set_set_def by simp_all qed lemma list_of_set_in: "finite s \ list_of_set s \ list_of_set_set s" unfolding list_of_set_def by (metis list_of_set_set_is_empty set_choose_thm) definition ordered_list_of_set where "ordered_list_of_set cmp s = set_choose (sort_by cmp ` list_of_set_set s)" subsection \sum\ find_consts "'a list => ('a list * _)" fun sum_partition :: "('a + 'b) list \ 'a list * 'b list" where "sum_partition [] = ([], [])" | "sum_partition ((Inl l) # lrs) = (let (ll, rl) = sum_partition lrs in (l # ll, rl))" | "sum_partition ((Inr r) # lrs) = (let (ll, rl) = sum_partition lrs in (ll, r # rl))" lemma sum_partition_length : "List.length lrs = List.length (fst (sum_partition lrs)) + List.length (snd (sum_partition lrs))" proof (induct lrs) case Nil thus ?case by simp next case (Cons lr lrs) thus ?case by (cases lr) (auto split: prod.split) qed subsection \sorting\ subsection \Strings\ declare String.literal.explode_inverse [simp] subsection \num to string conversions\ definition nat_list_to_string :: "nat list \ string" where "nat_list_to_string nl = map char_of nl" definition is_digit where "is_digit (n::nat) = (n < 10)" lemma is_digit_simps[simp] : "n < 10 \ is_digit n" "\(n < 10) \ \(is_digit n)" unfolding is_digit_def by simp_all lemma is_digit_expand : "is_digit n \ (n = 0) \ (n = 1) \ (n = 2) \ (n = 3) \ (n = 4) \ (n = 5) \ (n = 6) \ (n = 7) \ (n = 8) \ (n = 9)" unfolding is_digit_def by auto lemmas is_digitE = is_digit_expand[THEN iffD1,elim_format] lemmas is_digitI = is_digit_expand[THEN iffD2,rule_format] definition is_digit_char where "is_digit_char c \ (c = CHR ''0'') \ (c = CHR ''5'') \ (c = CHR ''1'') \ (c = CHR ''6'') \ (c = CHR ''2'') \ (c = CHR ''7'') \ (c = CHR ''3'') \ (c = CHR ''8'') \ (c = CHR ''4'') \ (c = CHR ''9'')" lemma is_digit_char_simps[simp] : "is_digit_char (CHR ''0'')" "is_digit_char (CHR ''1'')" "is_digit_char (CHR ''2'')" "is_digit_char (CHR ''3'')" "is_digit_char (CHR ''4'')" "is_digit_char (CHR ''5'')" "is_digit_char (CHR ''6'')" "is_digit_char (CHR ''7'')" "is_digit_char (CHR ''8'')" "is_digit_char (CHR ''9'')" unfolding is_digit_char_def by simp_all lemmas is_digit_charE = is_digit_char_def[THEN iffD1,elim_format] lemmas is_digit_charI = is_digit_char_def[THEN iffD2,rule_format] definition digit_to_char :: "nat \ char" where "digit_to_char n = ( if n = 0 then CHR ''0'' else if n = 1 then CHR ''1'' else if n = 2 then CHR ''2'' else if n = 3 then CHR ''3'' else if n = 4 then CHR ''4'' else if n = 5 then CHR ''5'' else if n = 6 then CHR ''6'' else if n = 7 then CHR ''7'' else if n = 8 then CHR ''8'' else if n = 9 then CHR ''9'' else CHR ''X'')" lemma digit_to_char_simps [simp]: "digit_to_char 0 = CHR ''0''" "digit_to_char (Suc 0) = CHR ''1''" "digit_to_char 2 = CHR ''2''" "digit_to_char 3 = CHR ''3''" "digit_to_char 4 = CHR ''4''" "digit_to_char 5 = CHR ''5''" "digit_to_char 6 = CHR ''6''" "digit_to_char 7 = CHR ''7''" "digit_to_char 8 = CHR ''8''" "digit_to_char 9 = CHR ''9''" "n > 9 \ digit_to_char n = CHR ''X''" unfolding digit_to_char_def by simp_all definition char_to_digit :: "char \ nat" where "char_to_digit c = ( if c = CHR ''0'' then 0 else if c = CHR ''1'' then 1 else if c = CHR ''2'' then 2 else if c = CHR ''3'' then 3 else if c = CHR ''4'' then 4 else if c = CHR ''5'' then 5 else if c = CHR ''6'' then 6 else if c = CHR ''7'' then 7 else if c = CHR ''8'' then 8 else if c = CHR ''9'' then 9 else 10)" lemma char_to_digit_simps [simp]: "char_to_digit (CHR ''0'') = 0" "char_to_digit (CHR ''1'') = 1" "char_to_digit (CHR ''2'') = 2" "char_to_digit (CHR ''3'') = 3" "char_to_digit (CHR ''4'') = 4" "char_to_digit (CHR ''5'') = 5" "char_to_digit (CHR ''6'') = 6" "char_to_digit (CHR ''7'') = 7" "char_to_digit (CHR ''8'') = 8" "char_to_digit (CHR ''9'') = 9" unfolding char_to_digit_def by simp_all lemma diget_to_char_inv[simp]: assumes is_digit: "is_digit n" shows "char_to_digit (digit_to_char n) = n" using is_digit unfolding is_digit_expand by auto lemma char_to_diget_inv[simp]: assumes is_digit: "is_digit_char c" shows "digit_to_char (char_to_digit c) = c" using is_digit unfolding char_to_digit_def is_digit_char_def by auto lemma char_to_digit_div_mod [simp]: assumes is_digit: "is_digit_char c" shows "char_to_digit c < 10" using is_digit unfolding char_to_digit_def is_digit_char_def by auto lemma is_digit_char_intro[simp]: "is_digit (char_to_digit c) = is_digit_char c" unfolding char_to_digit_def is_digit_char_def is_digit_expand by auto lemma is_digit_intro[simp]: "is_digit_char (digit_to_char n) = is_digit n" unfolding digit_to_char_def is_digit_char_def is_digit_expand by auto lemma digit_to_char_11: "digit_to_char n1 = digit_to_char n2 \ (is_digit n1 = is_digit n2) \ (is_digit n1 \ (n1 = n2))" by (metis diget_to_char_inv is_digit_intro) lemma char_to_digit_11: "char_to_digit c1 = char_to_digit c2 \ (is_digit_char c1 = is_digit_char c2) \ (is_digit_char c1 \ (c1 = c2))" by (metis char_to_diget_inv is_digit_char_intro) function nat_to_string :: "nat \ string" where "nat_to_string n = (if (is_digit n) then [digit_to_char n] else nat_to_string (n div 10) @ [digit_to_char (n mod 10)])" by auto termination by (relation "measure id") (auto simp add: is_digit_def) definition int_to_string :: "int \ string" where "int_to_string i \ if i < 0 then ''-'' @ nat_to_string (nat (abs i)) else nat_to_string (nat i)" lemma nat_to_string_simps[simp]: "is_digit n \ nat_to_string n = [digit_to_char n]" "\(is_digit n) \ nat_to_string n = nat_to_string (n div 10) @ [digit_to_char (n mod 10)]" by simp_all declare nat_to_string.simps[simp del] lemma nat_to_string_neq_nil[simp]: "nat_to_string n \ []" by (cases "is_digit n") simp_all lemmas nat_to_string_neq_nil2[simp] = nat_to_string_neq_nil[symmetric] lemma nat_to_string_char_to_digit [simp]: "is_digit_char c \ nat_to_string (char_to_digit c) = [c]" by auto lemma nat_to_string_11[simp] : "(nat_to_string n1 = nat_to_string n2) \ n1 = n2" proof (rule iffI) assume "n1 = n2" thus "nat_to_string n1 = nat_to_string n2" by simp next assume "nat_to_string n1 = nat_to_string n2" thus "n1 = n2" proof (induct n2 arbitrary: n1 rule: less_induct) case (less n2') note ind_hyp = this(1) note n2s_eq = less(2) have is_dig_eq: "is_digit n2' = is_digit n1" using n2s_eq apply (cases "is_digit n2'") apply (case_tac [!] "is_digit n1") apply (simp_all) done show ?case proof (cases "is_digit n2'") case True with n2s_eq is_dig_eq show ?thesis by simp (metis digit_to_char_11) next case False with is_dig_eq have not_digs : "\ (is_digit n1)" "\ (is_digit n2')" by simp_all from not_digs(2) have "n2' div 10 < n2'" unfolding is_digit_def by auto note ind_hyp' = ind_hyp [OF this, of "n1 div 10"] from not_digs n2s_eq ind_hyp' digit_to_char_11[of "n1 mod 10" "n2' mod 10"] have "(n1 mod 10) = (n2' mod 10)" "n1 div 10 = n2' div 10" by simp_all thus "n1 = n2'" by (metis div_mult_mod_eq) qed qed qed definition "is_nat_string s \ (\c\set s. is_digit_char c)" definition "is_strong_nat_string s \ is_nat_string s \ (s \ []) \ (hd s = CHR ''0'' \ length s = 1)" lemma is_nat_string_simps[simp]: "is_nat_string []" "is_nat_string (c # s) \ is_digit_char c \ is_nat_string s" unfolding is_nat_string_def by simp_all lemma is_strong_nat_string_simps[simp]: "\(is_strong_nat_string [])" "is_strong_nat_string (c # s) \ is_digit_char c \ is_nat_string s \ (c = CHR ''0'' \ s = [])" unfolding is_strong_nat_string_def by simp_all fun string_to_nat_aux :: "nat \ string \ nat" where "string_to_nat_aux n [] = n" | "string_to_nat_aux n (d#ds) = string_to_nat_aux (n*10 + char_to_digit d) ds" definition string_to_nat :: "string \ nat option" where "string_to_nat s \ (if is_nat_string s then Some (string_to_nat_aux 0 s) else None)" definition string_to_nat' :: "string \ nat" where "string_to_nat' s \ the (string_to_nat s)" lemma string_to_nat_aux_inv : assumes "is_nat_string s" assumes "n > 0 \ is_strong_nat_string s" shows "nat_to_string (string_to_nat_aux n s) = (if n = 0 then '''' else nat_to_string n) @ s" using assms proof (induct s arbitrary: n) case Nil thus ?case by (simp add: is_strong_nat_string_def) next case (Cons c s n) from Cons(2) have "is_digit_char c" "is_nat_string s" by simp_all note cs_ok = Cons(3) let ?m = "n*10 + char_to_digit c" note ind_hyp = Cons(1)[OF \is_nat_string s\, of ?m] from \is_digit_char c\ have m_div: "?m div 10 = n" and m_mod: "?m mod 10 = char_to_digit c" unfolding is_digit_char_def by auto show ?case proof (cases "?m = 0") case True with \is_digit_char c\ have "n = 0" "c = CHR ''0''" unfolding is_digit_char_def by auto moreover with cs_ok have "s = []" by simp ultimately show ?thesis by simp next case False note m_neq_0 = this with ind_hyp have ind_hyp': "nat_to_string (string_to_nat_aux ?m s) = (nat_to_string ?m) @ s" by auto hence "nat_to_string (string_to_nat_aux n (c # s)) = (nat_to_string ?m) @ s" by simp with \is_digit_char c\ m_div show ?thesis by simp qed qed lemma string_to_nat_inv : assumes strong_nat_s: "is_strong_nat_string s" assumes s2n_s: "string_to_nat s = Some n" shows "nat_to_string n = s" proof - from strong_nat_s have nat_s: "is_nat_string s" unfolding is_strong_nat_string_def by simp with s2n_s have n_eq: "n = string_to_nat_aux 0 s" unfolding string_to_nat_def by simp from string_to_nat_aux_inv[of s 0, folded n_eq] nat_s strong_nat_s show ?thesis by simp qed lemma nat_to_string_induct [case_names "digit" "non_digit"]: assumes digit: "\d. is_digit d \ P d" assumes not_digit: "\n. \(is_digit n) \ P (n div 10) \ P (n mod 10) \ P n" shows "P n" proof (induct n rule: less_induct) case (less n) note ind_hyp = this show ?case proof (cases "is_digit n") case True with digit show ?thesis by simp next case False note not_dig = this hence "n div 10 < n" "n mod 10 < n" unfolding is_digit_def by auto with not_dig ind_hyp not_digit show ?thesis by simp qed qed lemma nat_to_string___is_nat_string [simp]: "is_nat_string (nat_to_string n)" unfolding is_nat_string_def proof (induct n rule: nat_to_string_induct) case (digit d) thus ?case by simp next case (non_digit n) thus ?case by simp qed lemma nat_to_string___eq_0 [simp]: "(nat_to_string n = (CHR ''0'')#s) \ (n = 0 \ s = [])" unfolding is_nat_string_def proof (induct n arbitrary: s rule: nat_to_string_induct) case (digit d) thus ?case unfolding is_digit_expand by auto next case (non_digit n) obtain c s' where ns_eq: "nat_to_string (n div 10) = c # s'" by (cases "nat_to_string (n div 10)") auto from non_digit(1) have "n div 10 \ 0" unfolding is_digit_def by auto with non_digit(2) ns_eq have c_neq: "c \ CHR ''0''" by auto from \\ (is_digit n)\ c_neq ns_eq show ?case by auto qed lemma nat_to_string___is_strong_nat_string: "is_strong_nat_string (nat_to_string n)" proof (cases "is_digit n") case True thus ?thesis by simp next case False note not_digit = this obtain c s' where ns_eq: "nat_to_string n = c # s'" by (cases "nat_to_string n") auto from not_digit have "0 < n" unfolding is_digit_def by simp with ns_eq have c_neq: "c \ CHR ''0''" by auto hence "hd (nat_to_string n) \ CHR ''0''" unfolding ns_eq by simp thus ?thesis unfolding is_strong_nat_string_def by simp qed lemma nat_to_string_inv : "string_to_nat (nat_to_string n) = Some n" by (metis nat_to_string_11 nat_to_string___is_nat_string nat_to_string___is_strong_nat_string string_to_nat_def string_to_nat_inv) definition The_opt where "The_opt p = (if (\!x. p x) then Some (The p) else None)" lemma The_opt_eq_some [simp] : "((The_opt p) = (Some x)) \ ((p x) \ ((\ y. p y \ (x = y))))" (is "?lhs = ?rhs") proof (cases "\!x. p x") case True note exists_unique = this then obtain x where p_x: "p x" by auto from the1_equality[of p x] exists_unique p_x have the_opt_eq: "The_opt p = Some x" unfolding The_opt_def by simp from exists_unique the_opt_eq p_x show ?thesis by auto next case False note not_unique = this hence "The_opt p = None" unfolding The_opt_def by simp with not_unique show ?thesis by auto qed lemma The_opt_eq_none [simp] : "((The_opt p) = None) \ \(\!x. p x)" unfolding The_opt_def by auto end diff --git a/thys/PAC_Checker/PAC_Polynomials_Operations.thy b/thys/PAC_Checker/PAC_Polynomials_Operations.thy --- a/thys/PAC_Checker/PAC_Polynomials_Operations.thy +++ b/thys/PAC_Checker/PAC_Polynomials_Operations.thy @@ -1,1261 +1,1272 @@ theory PAC_Polynomials_Operations imports PAC_Polynomials_Term PAC_Checker_Specification begin subsection \Addition\ text \In this section, we refine the polynomials to list. These lists will be used in our checker to represent the polynomials and execute operations. There is one \<^emph>\key\ difference between the list representation and the usual representation: in the former, coefficients can be zero and monomials can appear several times. This makes it easier to reason on intermediate representation where this has not yet been sanitized. \ fun add_poly_l' :: \llist_polynomial \ llist_polynomial \ llist_polynomial\ where \add_poly_l' (p, []) = p\ | \add_poly_l' ([], q) = q\ | \add_poly_l' ((xs, n) # p, (ys, m) # q) = (if xs = ys then if n + m = 0 then add_poly_l' (p, q) else let pq = add_poly_l' (p, q) in ((xs, n + m) # pq) else if (xs, ys) \ term_order_rel then let pq = add_poly_l' (p, (ys, m) # q) in ((xs, n) # pq) else let pq = add_poly_l' ((xs, n) # p, q) in ((ys, m) # pq) )\ definition add_poly_l :: \llist_polynomial \ llist_polynomial \ llist_polynomial nres\ where \add_poly_l = REC\<^sub>T (\add_poly_l (p, q). case (p,q) of (p, []) \ RETURN p | ([], q) \ RETURN q | ((xs, n) # p, (ys, m) # q) \ (if xs = ys then if n + m = 0 then add_poly_l (p, q) else do { pq \ add_poly_l (p, q); RETURN ((xs, n + m) # pq) } else if (xs, ys) \ term_order_rel then do { pq \ add_poly_l (p, (ys, m) # q); RETURN ((xs, n) # pq) } else do { pq \ add_poly_l ((xs, n) # p, q); RETURN ((ys, m) # pq) }))\ definition nonzero_coeffs where \nonzero_coeffs a \ 0 \# snd `# a\ lemma nonzero_coeffs_simps[simp]: \nonzero_coeffs {#}\ \nonzero_coeffs (add_mset (xs, n) a) \ nonzero_coeffs a \ n \ 0\ by (auto simp: nonzero_coeffs_def) lemma nonzero_coeffsD: \nonzero_coeffs a \ (x, n) \# a \ n \ 0\ by (auto simp: nonzero_coeffs_def) lemma sorted_poly_list_rel_ConsD: \((ys, n) # p, a) \ sorted_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ ys \ set (map fst p) \ n \ 0 \ nonzero_coeffs a\ unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (subst (asm) list.rel_sel) apply (intro conjI) apply (rename_tac y, rule_tac b = \tl y\ in relcompI) apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list.tl_def term_poly_list_rel_def nonzero_coeffs_def split: list.splits) done lemma sorted_poly_list_rel_Cons_iff: \((ys, n) # p, a) \ sorted_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ ys \ set (map fst p) \ n \ 0 \ nonzero_coeffs a\ apply (rule iffI) subgoal by (auto dest!: sorted_poly_list_rel_ConsD) subgoal unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (intro conjI) apply (rename_tac y; rule_tac b = \(mset ys, n) # y\ in relcompI) by (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ \mset _\] nonzero_coeffs_def dest!: multi_member_split) done lemma sorted_repeat_poly_list_rel_ConsD: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ n \ 0 \ nonzero_coeffs a\ unfolding sorted_repeat_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (subst (asm) list.rel_sel) apply (intro conjI) apply (rename_tac y, rule_tac b = \tl y\ in relcompI) apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list.tl_def term_poly_list_rel_def nonzero_coeffs_def split: list.splits) done lemma sorted_repeat_poly_list_rel_Cons_iff: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ n \ 0 \ nonzero_coeffs a\ apply (rule iffI) subgoal by (auto dest!: sorted_repeat_poly_list_rel_ConsD) subgoal unfolding sorted_repeat_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (intro conjI) apply (rename_tac y, rule_tac b = \(mset ys, n) # y\ in relcompI) by (auto simp: sorted_repeat_poly_list_rel_wrt_def list_mset_rel_def br_def term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ \mset _\] nonzero_coeffs_def dest!: multi_member_split) done lemma add_poly_p_add_mset_sum_0: \n + m = 0 \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (add_mset (mset ys, n) A, add_mset (mset ys, m) Aa, {#}) ({#}, {#}, r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_r) apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_same_coeff_l) apply (rule converse_rtranclp_into_rtranclp) apply (auto intro: add_poly_p.rem_0_coeff) done lemma monoms_add_poly_l'D: \(aa, ba) \ set (add_poly_l' x) \ aa \ fst ` set (fst x) \ aa \ fst ` set (snd x)\ by (induction x rule: add_poly_l'.induct) (auto split: if_splits) lemma add_poly_p_add_to_result: \add_poly_p\<^sup>*\<^sup>* (A, B, r) (A', B', r') \ add_poly_p\<^sup>*\<^sup>* (A, B, p + r) (A', B', p + r')\ apply (induction rule: rtranclp_induct[of add_poly_p \(_, _, _)\ \(_, _, _)\, split_format(complete), of for r]) subgoal by auto by (elim add_poly_pE) (metis (no_types, lifting) Pair_inject add_poly_p.intros rtranclp.simps union_mset_add_mset_right)+ lemma add_poly_p_add_mset_comb: \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (add_mset (xs, n) A, Aa, {#}) ({#}, {#}, add_mset (xs, n) r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_l) using add_poly_p_add_to_result[of A Aa \{#}\ \{#}\ \{#}\ r \{#(xs, n)#}\] by auto lemma add_poly_p_add_mset_comb2: \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (add_mset (ys, n) A, add_mset (ys, m) Aa, {#}) ({#}, {#}, add_mset (ys, n + m) r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_r) apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_same_coeff_l) using add_poly_p_add_to_result[of A Aa \{#}\ \{#}\ \{#}\ r \{#(ys, n+m)#}\] by auto lemma add_poly_p_add_mset_comb3: \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (A, add_mset (ys, m) Aa, {#}) ({#}, {#}, add_mset (ys, m) r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_r) using add_poly_p_add_to_result[of A Aa \{#}\ \{#}\ \{#}\ r \{#(ys, m)#}\] by auto lemma total_on_lexord: \Relation.total_on UNIV R \ Relation.total_on UNIV (lexord R)\ apply (auto simp: Relation.total_on_def) by (meson lexord_linear) lemma antisym_lexord: \antisym R \ irrefl R \ antisym (lexord R)\ by (auto simp: antisym_def lexord_def irrefl_def elim!: list_match_lel_lel) lemma less_than_char_linear: \(a, b) \ less_than_char \ a = b \ (b, a) \ less_than_char\ by (auto simp: less_than_char_def) lemma total_on_lexord_less_than_char_linear: \xs \ ys \ (xs, ys) \ lexord (lexord less_than_char) \ (ys, xs) \ lexord (lexord less_than_char)\ using lexord_linear[of \lexord less_than_char\ xs ys] using lexord_linear[of \less_than_char\] less_than_char_linear using lexord_irrefl[OF irrefl_less_than_char] antisym_lexord[OF antisym_lexord[OF antisym_less_than_char irrefl_less_than_char]] apply (auto simp: antisym_def Relation.total_on_def) done lemma sorted_poly_list_rel_nonzeroD: \(p, r) \ sorted_poly_list_rel term_order \ nonzero_coeffs (r)\ \(p, r) \ sorted_poly_list_rel (rel2p (lexord (lexord less_than_char))) \ nonzero_coeffs (r)\ by (auto simp: sorted_poly_list_rel_wrt_def nonzero_coeffs_def) lemma add_poly_l'_add_poly_p: assumes \(pq, pq') \ sorted_poly_rel \\<^sub>r sorted_poly_rel\ shows \\r. (add_poly_l' pq, r) \ sorted_poly_rel \ add_poly_p\<^sup>*\<^sup>* (fst pq', snd pq', {#}) ({#}, {#}, r)\ supply [[goals_limit=1]] using assms apply (induction \pq\ arbitrary: pq' rule: add_poly_l'.induct) subgoal for p pq' using add_poly_p_empty_l[of \fst pq'\ \{#}\ \{#}\] by (cases pq') (auto intro!: exI[of _ \fst pq'\]) subgoal for x p pq' using add_poly_p_empty_r[of \{#}\ \snd pq'\ \{#}\] by (cases pq') (auto intro!: exI[of _ \snd pq'\]) subgoal premises p for xs n p ys m q pq' apply (cases pq') \ \Isabelle does a completely stupid case distinction here\ apply (cases \xs = ys\) subgoal apply (cases \n + m = 0\) subgoal using p(1)[of \(remove1_mset (mset xs, n) (fst pq'), remove1_mset (mset ys, m) (snd pq'))\] p(5-) apply (auto dest!: sorted_poly_list_rel_ConsD multi_member_split ) using add_poly_p_add_mset_sum_0 by blast subgoal using p(2)[of \(remove1_mset (mset xs, n) (fst pq'), remove1_mset (mset ys, m) (snd pq'))\] p(5-) apply (auto dest!: sorted_poly_list_rel_ConsD multi_member_split) apply (rule_tac x = \add_mset (mset ys, n + m) r\ in exI) apply (fastforce dest!: monoms_add_poly_l'D simp: sorted_poly_list_rel_Cons_iff rel2p_def sorted_poly_list_rel_nonzeroD var_order_rel_def intro: add_poly_p_add_mset_comb2) done done subgoal apply (cases \(xs, ys) \ term_order_rel\) subgoal using p(3)[of \(remove1_mset (mset xs, n) (fst pq'), (snd pq'))\] p(5-) apply (auto dest!: multi_member_split simp: sorted_poly_list_rel_Cons_iff rel2p_def) apply (rule_tac x = \add_mset (mset xs, n) r\ in exI) apply (auto dest!: monoms_add_poly_l'D) apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI var_order_rel_def) apply (rule lexord_trans) apply assumption apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI sorted_poly_list_rel_nonzeroD var_order_rel_def) using total_on_lexord_less_than_char_linear by fastforce subgoal using p(4)[of \(fst pq', remove1_mset (mset ys, m) (snd pq'))\] p(5-) apply (auto dest!: multi_member_split simp: sorted_poly_list_rel_Cons_iff rel2p_def var_order_rel_def) apply (rule_tac x = \add_mset (mset ys, m) r\ in exI) apply (auto dest!: monoms_add_poly_l'D simp: total_on_lexord_less_than_char_linear) apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI total_on_lexord_less_than_char_linear var_order_rel_def) apply (rule lexord_trans) apply assumption apply (auto intro: lexord_trans add_poly_p_add_mset_comb3 simp: lexord_transI sorted_poly_list_rel_nonzeroD var_order_rel_def) using total_on_lexord_less_than_char_linear by fastforce done done done lemma add_poly_l_add_poly: \add_poly_l x = RETURN (add_poly_l' x)\ unfolding add_poly_l_def by (induction x rule: add_poly_l'.induct) (solves \subst RECT_unfold, refine_mono, simp split: list.split\)+ lemma add_poly_l_spec: \(add_poly_l, uncurry (\p q. SPEC(\r. add_poly_p\<^sup>*\<^sup>* (p, q, {#}) ({#}, {#}, r)))) \ sorted_poly_rel \\<^sub>r sorted_poly_rel \\<^sub>f \sorted_poly_rel\nres_rel\ unfolding add_poly_l_add_poly apply (intro nres_relI frefI) apply (drule add_poly_l'_add_poly_p) apply (auto simp: conc_fun_RES) done definition sort_poly_spec :: \llist_polynomial \ llist_polynomial nres\ where \sort_poly_spec p = SPEC(\p'. mset p = mset p' \ sorted_wrt (rel2p (Id \ term_order_rel)) (map fst p'))\ lemma sort_poly_spec_id: assumes \(p, p') \ unsorted_poly_rel\ shows \sort_poly_spec p \ \ (sorted_repeat_poly_rel) (RETURN p')\ proof - obtain y where py: \(p, y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and p'_y: \p' = mset y\ and zero: \0 \# snd `# p'\ using assms unfolding sort_poly_spec_def poly_list_rel_def sorted_poly_list_rel_wrt_def by (auto simp: list_mset_rel_def br_def) then have [simp]: \length y = length p\ by (auto simp: list_rel_def list_all2_conv_all_nth) have H: \(x, p') \ \term_poly_list_rel \\<^sub>r int_rel\list_rel O list_mset_rel\ if px: \mset p = mset x\ and \sorted_wrt (rel2p (Id \ lexord var_order_rel)) (map fst x)\ for x :: \llist_polynomial\ proof - - obtain f where - f: \bij_betw f {.. and - [simp]: \\i. i x ! i = p ! (f i)\ - using px apply - apply (subst (asm)(2) eq_commute) unfolding mset_eq_perm - by (auto dest!: permutation_Ex_bij) + from px have \length x = length p\ + by (metis size_mset) + from px have \mset x = mset p\ + by simp + then obtain f where \f permutes {.. \permute_list f p = x\ + by (rule mset_eq_permutation) + with \length x = length p\ have f: \bij_betw f {.. + by (simp add: permutes_imp_bij) + from \f permutes {.. \permute_list f p = x\ [symmetric] + have [simp]: \\i. i < length x \ x ! i = p ! (f i)\ + by (simp add: permute_list_nth) let ?y = \map (\i. y ! f i) [0 ..< length x]\ have \i < length y \ (p ! f i, y ! f i) \ term_poly_list_rel \\<^sub>r int_rel\ for i using list_all2_nthD[of _ p y \f i\, OF py[unfolded list_rel_def mem_Collect_eq prod.case]] mset_eq_length[OF px] f by (auto simp: list_rel_def list_all2_conv_all_nth bij_betw_def) then have \(x, ?y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and xy: \length x = length y\ using py list_all2_nthD[of \rel2p (term_poly_list_rel \\<^sub>r int_rel)\ p y \f i\ for i, simplified] mset_eq_length[OF px] by (auto simp: list_rel_def list_all2_conv_all_nth) moreover { have f: \mset_set {0.. using f mset_eq_length[OF px] by (auto simp: bij_betw_def lessThan_atLeast0 image_mset_mset_set) have \mset y = {#y ! f x. x \# mset_set {0.. by (subst drop_0[symmetric], subst mset_drop_upto, subst xy[symmetric], subst f) auto then have \(?y, p') \ list_mset_rel\ by (auto simp: list_mset_rel_def br_def p'_y) } ultimately show ?thesis by (auto intro!: relcompI[of _ ?y]) qed show ?thesis using zero unfolding sort_poly_spec_def poly_list_rel_def sorted_repeat_poly_list_rel_wrt_def by refine_rcg (auto intro: H) qed subsection \Multiplication\ fun mult_monoms :: \term_poly_list \ term_poly_list \ term_poly_list\ where \mult_monoms p [] = p\ | \mult_monoms [] p = p\ | \mult_monoms (x # p) (y # q) = (if x = y then x # mult_monoms p q else if (x, y) \ var_order_rel then x # mult_monoms p (y # q) else y # mult_monoms (x # p) q)\ lemma term_poly_list_rel_empty_iff[simp]: \([], q') \ term_poly_list_rel \ q' = {#}\ by (auto simp: term_poly_list_rel_def) lemma mset_eqD_set_mset: \mset xs = A \ set xs = set_mset A\ by auto lemma term_poly_list_rel_Cons_iff: \(y # p, p') \ term_poly_list_rel \ (p, remove1_mset y p') \ term_poly_list_rel \ y \# p' \ y \ set p \ y \# remove1_mset y p' \ (\x\#mset p. (y, x) \ var_order_rel)\ by (auto simp: term_poly_list_rel_def rel2p_def dest!: multi_member_split mset_eqD_set_mset) lemma var_order_rel_antisym[simp]: \(y, y) \ var_order_rel\ by (simp add: less_than_char_def lexord_irreflexive var_order_rel_def) lemma term_poly_list_rel_remdups_mset: \(p, p') \ term_poly_list_rel \ (p, remdups_mset p') \ term_poly_list_rel\ by (auto simp: term_poly_list_rel_def distinct_mset_remdups_mset_id simp flip: distinct_mset_mset_distinct) lemma var_notin_notin_mult_monomsD: \y \ set (mult_monoms p q) \ y \ set p \ y \ set q\ by (induction p q arbitrary: p' q' rule: mult_monoms.induct) (auto split: if_splits) lemma term_poly_list_rel_set_mset: \(p, q) \ term_poly_list_rel \ set p = set_mset q\ by (auto simp: term_poly_list_rel_def) lemma mult_monoms_spec: \(mult_monoms, (\a b. remdups_mset (a + b))) \ term_poly_list_rel \ term_poly_list_rel \ term_poly_list_rel\ proof - have [dest]: \remdups_mset (A + Aa) = add_mset y Ab \ y \# A \ y \# Aa \ False\ for Aa Ab y A by (metis set_mset_remdups_mset union_iff union_single_eq_member) show ?thesis apply (intro fun_relI) apply (rename_tac p p' q q') subgoal for p p' q q' apply (induction p q arbitrary: p' q' rule: mult_monoms.induct) subgoal by (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_remdups_mset) subgoal for x p p' q' by (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_remdups_mset dest!: multi_member_split[of _ q']) subgoal premises p for x p y q p' q' apply (cases \x = y\) subgoal using p(1)[of \remove1_mset y p'\ \remove1_mset y q'\] p(4-) by (auto simp: term_poly_list_rel_Cons_iff rel2p_def dest!: var_notin_notin_mult_monomsD dest!: multi_member_split) apply (cases \(x, y) \ var_order_rel\) subgoal using p(2)[of \remove1_mset x p'\ \q'\] p(4-) apply (auto simp: term_poly_list_rel_Cons_iff term_poly_list_rel_set_mset rel2p_def var_order_rel_def dest!: multi_member_split[of _ p'] multi_member_split[of _ q'] var_notin_notin_mult_monomsD split: if_splits) apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) using lexord_trans trans_less_than_char var_order_rel_antisym unfolding var_order_rel_def apply blast+ done subgoal using p(3)[of \p'\ \remove1_mset y q'\] p(4-) apply (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_set_mset rel2p_def var_order_rel_antisym dest!: multi_member_split[of _ p'] multi_member_split[of _ q'] var_notin_notin_mult_monomsD split: if_splits) using lexord_trans trans_less_than_char var_order_rel_antisym unfolding var_order_rel_def apply blast apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) by (meson less_than_char_linear lexord_linear lexord_trans trans_less_than_char) done done done qed definition mult_monomials :: \term_poly_list \ int \ term_poly_list \ int \ term_poly_list \ int\ where \mult_monomials = (\(x, a) (y, b). (mult_monoms x y, a * b))\ definition mult_poly_raw :: \llist_polynomial \ llist_polynomial \ llist_polynomial\ where \mult_poly_raw p q = foldl (\b x. map (mult_monomials x) q @ b) [] p\ fun map_append where \map_append f b [] = b\ | \map_append f b (x # xs) = f x # map_append f b xs\ lemma map_append_alt_def: \map_append f b xs = map f xs @ b\ by (induction f b xs rule: map_append.induct) auto lemma foldl_append_empty: \NO_MATCH [] xs \ foldl (\b x. f x @ b) xs p = foldl (\b x. f x @ b) [] p @ xs\ apply (induction p arbitrary: xs) apply simp by (metis (mono_tags, lifting) NO_MATCH_def append.assoc append_self_conv foldl_Cons) lemma poly_list_rel_empty_iff[simp]: \([], r) \ poly_list_rel R \ r = {#}\ by (auto simp: poly_list_rel_def list_mset_rel_def br_def) lemma mult_poly_raw_simp[simp]: \mult_poly_raw [] q = []\ \mult_poly_raw (x # p) q = mult_poly_raw p q @ map (mult_monomials x) q\ subgoal by (auto simp: mult_poly_raw_def) subgoal by (induction p) (auto simp: mult_poly_raw_def foldl_append_empty) done lemma sorted_poly_list_relD: \(q, q') \ sorted_poly_list_rel R \ q' = (\(a, b). (mset a, b)) `# mset q\ apply (induction q arbitrary: q') apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list_rel_split_right_iff) apply (subst (asm)(2) term_poly_list_rel_def) apply (simp add: relcomp.relcompI) done lemma list_all2_in_set_ExD: \list_all2 R p q \ x \ set p \ \y \ set q. R x y\ by (induction p q rule: list_all2_induct) auto inductive_cases mult_poly_p_elim: \mult_poly_p q (A, r) (B, r')\ lemma mult_poly_p_add_mset_same: \(mult_poly_p q')\<^sup>*\<^sup>* (A, r) (B, r') \ (mult_poly_p q')\<^sup>*\<^sup>* (add_mset x A, r) (add_mset x B, r')\ apply (induction rule: rtranclp_induct[of \mult_poly_p q'\ \(_, r)\ \(p', q'')\ for p' q'', split_format(complete)]) subgoal by simp apply (rule rtranclp.rtrancl_into_rtrancl) apply assumption by (auto elim!: mult_poly_p_elim intro: mult_poly_p.intros intro: rtranclp.rtrancl_into_rtrancl simp: add_mset_commute[of x]) lemma mult_poly_raw_mult_poly_p: assumes \(p, p') \ sorted_poly_rel\ and \(q, q') \ sorted_poly_rel\ shows \\r. (mult_poly_raw p q, r) \ unsorted_poly_rel \ (mult_poly_p q')\<^sup>*\<^sup>* (p', {#}) ({#}, r)\ proof - have H: \(q, q') \ sorted_poly_list_rel term_order \ n < length q \ distinct aa \ sorted_wrt var_order aa \ (mult_monoms aa (fst (q ! n)), mset (mult_monoms aa (fst (q ! n)))) \ term_poly_list_rel\ for aa n using mult_monoms_spec[unfolded fun_rel_def, simplified] apply - apply (drule bspec[of _ _ \(aa, (mset aa))\]) apply (auto simp: term_poly_list_rel_def)[] unfolding prod.case sorted_poly_list_rel_wrt_def apply clarsimp subgoal for y apply (drule bspec[of _ _ \(fst (q ! n), mset (fst (q ! n)))\]) apply (cases \q ! n\; cases \y ! n\) using param_nth[of n y n q \term_poly_list_rel \\<^sub>r int_rel\] by (auto simp: list_rel_imp_same_length term_poly_list_rel_def) done have H': \(q, q') \ sorted_poly_list_rel term_order \ distinct aa \ sorted_wrt var_order aa \ (ab, ba) \ set q \ remdups_mset (mset aa + mset ab) = mset (mult_monoms aa ab)\ for aa n ab ba using mult_monoms_spec[unfolded fun_rel_def, simplified] apply - apply (drule bspec[of _ _ \(aa, (mset aa))\]) apply (auto simp: term_poly_list_rel_def)[] unfolding prod.case sorted_poly_list_rel_wrt_def apply clarsimp subgoal for y apply (drule bspec[of _ _ \(ab, mset ab)\]) apply (auto simp: list_rel_imp_same_length term_poly_list_rel_def list_rel_def dest: list_all2_in_set_ExD) done done have H: \(q, q') \ sorted_poly_list_rel term_order \ a = (aa, b) \ (pq, r) \ unsorted_poly_rel \ p' = add_mset (mset aa, b) A \ \x\set p. term_order aa (fst x) \ sorted_wrt var_order aa \ distinct aa \ b\ 0 \ (\aaa. (aaa, 0) \# q') \ (pq @ map (mult_monomials (aa, b)) q, {#case x of (ys, n) \ (remdups_mset (mset aa + ys), n * b) . x \# q'#} + r) \ unsorted_poly_rel\ for a p p' pq aa b r apply (auto simp: poly_list_rel_def) apply (rule_tac b = \y @ map (\(a,b). (mset a, b)) (map (mult_monomials (aa, b)) q)\ in relcompI) apply (auto simp: list_rel_def list_all2_append list_all2_lengthD H list_mset_rel_def br_def mult_monomials_def case_prod_beta intro!: list_all2_all_nthI simp: sorted_poly_list_relD) apply (subst sorted_poly_list_relD[of q q' term_order]) apply (auto simp: case_prod_beta H' intro!: image_mset_cong) done show ?thesis using assms apply (induction p arbitrary: p') subgoal by auto subgoal premises p for a p p' using p(1)[of \remove1_mset (mset (fst a), snd a) p'\] p(2-) apply (cases a) apply (auto simp: sorted_poly_list_rel_Cons_iff dest!: multi_member_split) apply (rule_tac x = \(\(ys, n). (remdups_mset (mset (fst a) + ys), n * snd a)) `# q' + r\ in exI) apply (auto 5 3 intro: mult_poly_p.intros simp: intro!: H dest: sorted_poly_list_rel_nonzeroD nonzero_coeffsD) apply (rule rtranclp_trans) apply (rule mult_poly_p_add_mset_same) apply assumption apply (rule converse_rtranclp_into_rtranclp) apply (auto intro!: mult_poly_p.intros simp: ac_simps) done done qed fun merge_coeffs :: \llist_polynomial \ llist_polynomial\ where \merge_coeffs [] = []\ | \merge_coeffs [(xs, n)] = [(xs, n)]\ | \merge_coeffs ((xs, n) # (ys, m) # p) = (if xs = ys then if n + m \ 0 then merge_coeffs ((xs, n + m) # p) else merge_coeffs p else (xs, n) # merge_coeffs ((ys, m) # p))\ abbreviation (in -)mononoms :: \llist_polynomial \ term_poly_list set\ where \mononoms p \ fst `set p\ lemma fst_normalize_polynomial_subset: \mononoms (merge_coeffs p) \ mononoms p\ by (induction p rule: merge_coeffs.induct) auto lemma fst_normalize_polynomial_subsetD: \(a, b) \ set (merge_coeffs p) \ a \ mononoms p\ apply (induction p rule: merge_coeffs.induct) subgoal by auto subgoal by auto subgoal by (auto split: if_splits) done lemma distinct_merge_coeffs: assumes \sorted_wrt R (map fst xs)\ and \transp R\ \antisymp R\ shows \distinct (map fst (merge_coeffs xs))\ using assms by (induction xs rule: merge_coeffs.induct) (auto 5 4 dest: antisympD dest!: fst_normalize_polynomial_subsetD) lemma in_set_merge_coeffsD: \(a, b) \ set (merge_coeffs p) \\b. (a, b) \ set p\ by (auto dest!: fst_normalize_polynomial_subsetD) lemma rtranclp_normalize_poly_add_mset: \normalize_poly_p\<^sup>*\<^sup>* A r \ normalize_poly_p\<^sup>*\<^sup>* (add_mset x A) (add_mset x r)\ by (induction rule: rtranclp_induct) (auto dest: normalize_poly_p.keep_coeff[of _ _ x]) lemma nonzero_coeffs_diff: \nonzero_coeffs A \ nonzero_coeffs (A - B)\ by (auto simp: nonzero_coeffs_def dest: in_diffD) lemma merge_coeffs_is_normalize_poly_p: \(xs, ys) \ sorted_repeat_poly_rel \ \r. (merge_coeffs xs, r) \ sorted_poly_rel \ normalize_poly_p\<^sup>*\<^sup>* ys r\ apply (induction xs arbitrary: ys rule: merge_coeffs.induct) subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def) subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def) subgoal premises p for xs n ys m p ysa apply (cases \xs = ys\, cases \m+n \ 0\) subgoal using p(1)[of \add_mset (mset ys, m+n) ysa - {#(mset ys, m), (mset ys, n)#}\] p(4-) apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (auto dest!: multi_member_split simp del: normalize_poly_p.merge_dup_coeff simp: add_mset_commute intro: converse_rtranclp_into_rtranclp) subgoal using p(2)[of \ysa - {#(mset ys, m), (mset ys, n)#}\] p(4-) apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.rem_0_coeff[of \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\] using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (force intro: add_mset_commute[of \(mset ys, n)\ \(mset ys, -n)\] converse_rtranclp_into_rtranclp dest!: multi_member_split simp del: normalize_poly_p.rem_0_coeff simp: add_eq_0_iff2 intro: normalize_poly_p.rem_0_coeff) subgoal using p(3)[of \add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}\] p(4-) apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \add_mset (mset xs, n) r\ in exI) apply (auto dest!: in_set_merge_coeffsD) apply (auto intro: normalize_poly_p.intros rtranclp_normalize_poly_add_mset simp: rel2p_def var_order_rel_def dest!: multi_member_split dest: sorted_poly_list_rel_nonzeroD) using total_on_lexord_less_than_char_linear apply fastforce using total_on_lexord_less_than_char_linear apply fastforce done done done subsection \Normalisation\ definition normalize_poly where \normalize_poly p = do { p \ sort_poly_spec p; RETURN (merge_coeffs p) }\ definition sort_coeff :: \string list \ string list nres\ where \sort_coeff ys = SPEC(\xs. mset xs = mset ys \ sorted_wrt (rel2p (Id \ var_order_rel)) xs)\ lemma distinct_var_order_Id_var_order: \distinct a \ sorted_wrt (rel2p (Id \ var_order_rel)) a \ sorted_wrt var_order a\ by (induction a) (auto simp: rel2p_def) definition sort_all_coeffs :: \llist_polynomial \ llist_polynomial nres\ where \sort_all_coeffs xs = monadic_nfoldli xs (\_. RETURN True) (\(a, n) b. do {a \ sort_coeff a; RETURN ((a, n) # b)}) []\ lemma sort_all_coeffs_gen: assumes \(\xs \ mononoms xs'. sorted_wrt (rel2p (var_order_rel)) xs)\ and \\x \ mononoms (xs @ xs'). distinct x\ shows \monadic_nfoldli xs (\_. RETURN True) (\(a, n) b. do {a \ sort_coeff a; RETURN ((a, n) # b)}) xs' \ \Id (SPEC(\ys. map (\(a,b). (mset a, b)) (rev xs @ xs') = map (\(a,b). (mset a, b)) (ys) \ (\xs \ mononoms ys. sorted_wrt (rel2p (var_order_rel)) xs)))\ proof - have H: \ \x\set xs'. sorted_wrt var_order (fst x) \ sorted_wrt (rel2p (Id \ var_order_rel)) x \ (aaa, ba) \ set xs' \ sorted_wrt (rel2p (Id \ var_order_rel)) aaa\ for xs xs' ba aa b x aaa by (metis UnCI fst_eqD rel2p_def sorted_wrt_mono_rel) show ?thesis using assms unfolding sort_all_coeffs_def sort_coeff_def apply (induction xs arbitrary: xs') subgoal using assms by auto subgoal premises p for a xs using p(2-) apply (cases a, simp only: monadic_nfoldli_simp bind_to_let_conv Let_def if_True Refine_Basic.nres_monad3 intro_spec_refine_iff prod.case) by (auto 5 3 simp: intro_spec_refine_iff image_Un dest: same_mset_distinct_iff intro!: p(1)[THEN order_trans] distinct_var_order_Id_var_order simp: H) done qed definition shuffle_coefficients where \shuffle_coefficients xs = (SPEC(\ys. map (\(a,b). (mset a, b)) (rev xs) = map (\(a,b). (mset a, b)) ys \ (\xs \ mononoms ys. sorted_wrt (rel2p (var_order_rel)) xs)))\ lemma sort_all_coeffs: \\x \ mononoms xs. distinct x \ sort_all_coeffs xs \ \ Id (shuffle_coefficients xs)\ unfolding sort_all_coeffs_def shuffle_coefficients_def by (rule sort_all_coeffs_gen[THEN order_trans]) auto lemma unsorted_term_poly_list_rel_mset: \(ys, aa) \ unsorted_term_poly_list_rel \ mset ys = aa\ by (auto simp: unsorted_term_poly_list_rel_def) lemma RETURN_map_alt_def: \RETURN o (map f) = REC\<^sub>T (\g xs. case xs of [] \ RETURN [] | x # xs \ do {xs \ g xs; RETURN (f x # xs)})\ unfolding comp_def apply (subst eq_commute) apply (intro ext) apply (induct_tac x) subgoal apply (subst RECT_unfold) apply refine_mono apply auto done subgoal apply (subst RECT_unfold) apply refine_mono apply auto done done lemma fully_unsorted_poly_rel_Cons_iff: \((ys, n) # p, a) \ fully_unsorted_poly_rel \ (p, remove1_mset (mset ys, n) a) \ fully_unsorted_poly_rel \ (mset ys, n) \# a \ distinct ys\ apply (auto simp: poly_list_rel_def list_rel_split_right_iff list_mset_rel_def br_def unsorted_term_poly_list_rel_def nonzero_coeffs_def fully_unsorted_poly_list_rel_def dest!: multi_member_split) apply blast apply (rule_tac b = \(mset ys, n) # y\ in relcompI) apply auto done lemma map_mset_unsorted_term_poly_list_rel: \(\a. a \ mononoms s \ distinct a) \ \x \ mononoms s. distinct x \ (\xs \ mononoms s. sorted_wrt (rel2p (Id \ var_order_rel)) xs) \ (s, map (\(a, y). (mset a, y)) s) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ by (induction s) (auto simp: term_poly_list_rel_def distinct_var_order_Id_var_order) lemma list_rel_unsorted_term_poly_list_relD: \(p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ mset y = (\(a, y). (mset a, y)) `# mset p \ (\x \ mononoms p. distinct x)\ by (induction p arbitrary: y) (auto simp: list_rel_split_right_iff unsorted_term_poly_list_rel_def) lemma shuffle_terms_distinct_iff: assumes \map (\(a, y). (mset a, y)) p = map (\(a, y). (mset a, y)) s\ shows \(\x\set p. distinct (fst x)) \ (\x\set s. distinct (fst x))\ proof - have \\x\set s. distinct (fst x)\ if m: \map (\(a, y). (mset a, y)) p = map (\(a, y). (mset a, y)) s\ and dist: \\x\set p. distinct (fst x)\ for s p proof standard+ fix x assume x: \x \ set s\ obtain v n where [simp]: \x = (v, n)\ by (cases x) then have \(mset v, n) \ set (map (\(a, y). (mset a, y)) p)\ using x unfolding m by auto then obtain v' where \(v', n) \ set p\ and \mset v' = mset v\ by (auto simp: image_iff) then show \distinct (fst x)\ using dist by (metis \x = (v, n)\ distinct_mset_mset_distinct fst_conv) qed from this[of p s] this[of s p] show \?thesis\ unfolding assms by blast qed lemma \(p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ (a, b) \ set p \ distinct a\ using list_rel_unsorted_term_poly_list_relD by fastforce lemma sort_all_coeffs_unsorted_poly_rel_with0: assumes \(p, p') \ fully_unsorted_poly_rel\ shows \sort_all_coeffs p \ \ (unsorted_poly_rel_with0) (RETURN p')\ proof - have H: \(map (\(a, y). (mset a, y)) (rev p)) = map (\(a, y). (mset a, y)) s \ (map (\(a, y). (mset a, y)) p) = map (\(a, y). (mset a, y)) (rev s)\ for s by (auto simp flip: rev_map simp: eq_commute[of \rev (map _ _)\ \map _ _\]) have 1: \\s y. (p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ p' = mset y \ map (\(a, y). (mset a, y)) (rev p) = map (\(a, y). (mset a, y)) s \ \x\set s. sorted_wrt var_order (fst x) \ (s, map (\(a, y). (mset a, y)) s) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ by (auto 4 4 simp: rel2p_def dest!: list_rel_unsorted_term_poly_list_relD dest: shuffle_terms_distinct_iff["THEN" iffD1] intro!: map_mset_unsorted_term_poly_list_rel sorted_wrt_mono_rel[of _ \rel2p (var_order_rel)\ \rel2p (Id \ var_order_rel)\]) have 2: \\s y. (p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ p' = mset y \ map (\(a, y). (mset a, y)) (rev p) = map (\(a, y). (mset a, y)) s \ \x\set s. sorted_wrt var_order (fst x) \ mset y = {#case x of (a, x) \ (mset a, x). x \# mset s#}\ by (metis (no_types, lifting) list_rel_unsorted_term_poly_list_relD mset_map mset_rev) show ?thesis apply (rule sort_all_coeffs[THEN order_trans]) using assms by (auto simp: shuffle_coefficients_def poly_list_rel_def RETURN_def fully_unsorted_poly_list_rel_def list_mset_rel_def br_def dest: list_rel_unsorted_term_poly_list_relD intro!: RES_refine relcompI[of _ \map (\(a, y). (mset a, y)) (rev p)\] 1 2) qed lemma sort_poly_spec_id': assumes \(p, p') \ unsorted_poly_rel_with0\ shows \sort_poly_spec p \ \ (sorted_repeat_poly_rel_with0) (RETURN p')\ proof - obtain y where py: \(p, y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and p'_y: \p' = mset y\ using assms unfolding fully_unsorted_poly_list_rel_def poly_list_rel_def sorted_poly_list_rel_wrt_def by (auto simp: list_mset_rel_def br_def) then have [simp]: \length y = length p\ by (auto simp: list_rel_def list_all2_conv_all_nth) have H: \(x, p') \ \term_poly_list_rel \\<^sub>r int_rel\list_rel O list_mset_rel\ if px: \mset p = mset x\ and \sorted_wrt (rel2p (Id \ lexord var_order_rel)) (map fst x)\ for x :: \llist_polynomial\ proof - - obtain f where - f: \bij_betw f {.. and - [simp]: \\i. i x ! i = p ! (f i)\ - using px apply - apply (subst (asm)(2) eq_commute) unfolding mset_eq_perm - by (auto dest!: permutation_Ex_bij) + from px have \length x = length p\ + by (metis size_mset) + from px have \mset x = mset p\ + by simp + then obtain f where \f permutes {.. \permute_list f p = x\ + by (rule mset_eq_permutation) + with \length x = length p\ have f: \bij_betw f {.. + by (simp add: permutes_imp_bij) + from \f permutes {.. \permute_list f p = x\ [symmetric] + have [simp]: \\i. i < length x \ x ! i = p ! (f i)\ + by (simp add: permute_list_nth) let ?y = \map (\i. y ! f i) [0 ..< length x]\ have \i < length y \ (p ! f i, y ! f i) \ term_poly_list_rel \\<^sub>r int_rel\ for i using list_all2_nthD[of _ p y \f i\, OF py[unfolded list_rel_def mem_Collect_eq prod.case]] mset_eq_length[OF px] f by (auto simp: list_rel_def list_all2_conv_all_nth bij_betw_def) then have \(x, ?y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and xy: \length x = length y\ using py list_all2_nthD[of \rel2p (term_poly_list_rel \\<^sub>r int_rel)\ p y \f i\ for i, simplified] mset_eq_length[OF px] by (auto simp: list_rel_def list_all2_conv_all_nth) moreover { have f: \mset_set {0.. using f mset_eq_length[OF px] by (auto simp: bij_betw_def lessThan_atLeast0 image_mset_mset_set) have \mset y = {#y ! f x. x \# mset_set {0.. by (subst drop_0[symmetric], subst mset_drop_upto, subst xy[symmetric], subst f) auto then have \(?y, p') \ list_mset_rel\ by (auto simp: list_mset_rel_def br_def p'_y) } ultimately show ?thesis by (auto intro!: relcompI[of _ ?y]) qed show ?thesis unfolding sort_poly_spec_def poly_list_rel_def sorted_repeat_poly_list_rel_with0_wrt_def by refine_rcg (auto intro: H) qed fun merge_coeffs0 :: \llist_polynomial \ llist_polynomial\ where \merge_coeffs0 [] = []\ | \merge_coeffs0 [(xs, n)] = (if n = 0 then [] else [(xs, n)])\ | \merge_coeffs0 ((xs, n) # (ys, m) # p) = (if xs = ys then if n + m \ 0 then merge_coeffs0 ((xs, n + m) # p) else merge_coeffs0 p else if n = 0 then merge_coeffs0 ((ys, m) # p) else(xs, n) # merge_coeffs0 ((ys, m) # p))\ lemma sorted_repeat_poly_list_rel_with0_wrt_ConsD: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys\ unfolding sorted_repeat_poly_list_rel_with0_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (subst (asm) list.rel_sel) apply (intro conjI) apply (rule_tac b = \tl y\ in relcompI) apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) done lemma sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys\ apply (rule iffI) subgoal by (auto dest!: sorted_repeat_poly_list_rel_with0_wrt_ConsD) subgoal unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def sorted_repeat_poly_list_rel_with0_wrt_def apply (clarsimp) apply (rule_tac b = \(mset ys, n) # y\ in relcompI) by (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ \mset _\] nonzero_coeffs_def dest!: multi_member_split) done lemma fst_normalize0_polynomial_subsetD: \(a, b) \ set (merge_coeffs0 p) \ a \ mononoms p\ apply (induction p rule: merge_coeffs0.induct) subgoal by auto subgoal by (auto split: if_splits) subgoal by (auto split: if_splits) done lemma in_set_merge_coeffs0D: \(a, b) \ set (merge_coeffs0 p) \\b. (a, b) \ set p\ by (auto dest!: fst_normalize0_polynomial_subsetD) lemma merge_coeffs0_is_normalize_poly_p: \(xs, ys) \ sorted_repeat_poly_rel_with0 \ \r. (merge_coeffs0 xs, r) \ sorted_poly_rel \ normalize_poly_p\<^sup>*\<^sup>* ys r\ apply (induction xs arbitrary: ys rule: merge_coeffs0.induct) subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def sorted_repeat_poly_list_rel_with0_wrt_def list_mset_rel_def br_def) subgoal for xs n ys by (force simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def sorted_repeat_poly_list_rel_with0_wrt_def list_mset_rel_def br_def list_rel_split_right_iff) subgoal premises p for xs n ys m p ysa apply (cases \xs = ys\, cases \m+n \ 0\) subgoal using p(1)[of \add_mset (mset ys, m+n) ysa - {#(mset ys, m), (mset ys, n)#}\] p(5-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (auto intro: normalize_poly_p.intros add_mset_commute add_mset_commute converse_rtranclp_into_rtranclp dest!: multi_member_split simp del: normalize_poly_p.merge_dup_coeff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (auto intro: normalize_poly_p.intros converse_rtranclp_into_rtranclp dest!: multi_member_split simp: add_mset_commute[of \(mset ys, n)\ \(mset ys, m)\] simp del: normalize_poly_p.merge_dup_coeff) subgoal using p(2)[of \ysa - {#(mset ys, m), (mset ys, n)#}\] p(5-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.rem_0_coeff[of \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\] using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (force intro: normalize_poly_p.intros converse_rtranclp_into_rtranclp dest!: multi_member_split simp del: normalize_poly_p.rem_0_coeff simp: add_mset_commute[of \(mset ys, n)\ \(mset ys, m)\]) apply (cases \n = 0\) subgoal using p(3)[of \add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}\] p(4-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) apply (auto dest!: in_set_merge_coeffsD) by (force intro: rtranclp_normalize_poly_add_mset converse_rtranclp_into_rtranclp simp: rel2p_def var_order_rel_def sorted_poly_list_rel_Cons_iff dest!: multi_member_split dest: sorted_poly_list_rel_nonzeroD) subgoal using p(4)[of \add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}\] p(5-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \add_mset (mset xs, n) r\ in exI) apply (auto dest!: in_set_merge_coeffs0D) apply (auto intro: normalize_poly_p.intros rtranclp_normalize_poly_add_mset simp: rel2p_def var_order_rel_def sorted_poly_list_rel_Cons_iff dest!: multi_member_split dest: sorted_poly_list_rel_nonzeroD) using in_set_merge_coeffs0D total_on_lexord_less_than_char_linear apply fastforce using in_set_merge_coeffs0D total_on_lexord_less_than_char_linear apply fastforce done done done definition full_normalize_poly where \full_normalize_poly p = do { p \ sort_all_coeffs p; p \ sort_poly_spec p; RETURN (merge_coeffs0 p) }\ fun sorted_remdups where \sorted_remdups (x # y # zs) = (if x = y then sorted_remdups (y # zs) else x # sorted_remdups (y # zs))\ | \sorted_remdups zs = zs\ lemma set_sorted_remdups[simp]: \set (sorted_remdups xs) = set xs\ by (induction xs rule: sorted_remdups.induct) auto lemma distinct_sorted_remdups: \sorted_wrt R xs \ transp R \ Restricted_Predicates.total_on R UNIV \ antisymp R \ distinct (sorted_remdups xs)\ by (induction xs rule: sorted_remdups.induct) (auto dest: antisympD) lemma full_normalize_poly_normalize_poly_p: assumes \(p, p') \ fully_unsorted_poly_rel\ shows \full_normalize_poly p \ \ (sorted_poly_rel) (SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r))\ (is \?A \ \ ?R ?B\) proof - have 1: \?B = do { p' \ RETURN p'; p' \ RETURN p'; SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r) }\ by auto have [refine0]: \sort_all_coeffs p \ SPEC(\p. (p, p') \ unsorted_poly_rel_with0)\ by (rule sort_all_coeffs_unsorted_poly_rel_with0[OF assms, THEN order_trans]) (auto simp: conc_fun_RES RETURN_def) have [refine0]: \sort_poly_spec p \ SPEC (\c. (c, p') \ sorted_repeat_poly_rel_with0)\ if \(p, p') \ unsorted_poly_rel_with0\ for p p' by (rule sort_poly_spec_id'[THEN order_trans, OF that]) (auto simp: conc_fun_RES RETURN_def) show ?thesis apply (subst 1) unfolding full_normalize_poly_def by (refine_rcg) (auto intro!: RES_refine dest!: merge_coeffs0_is_normalize_poly_p simp: RETURN_def) qed definition mult_poly_full :: \_\ where \mult_poly_full p q = do { let pq = mult_poly_raw p q; normalize_poly pq }\ lemma normalize_poly_normalize_poly_p: assumes \(p, p') \ unsorted_poly_rel\ shows \normalize_poly p \ \ (sorted_poly_rel) (SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r))\ proof - have 1: \SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r) = do { p' \ RETURN p'; SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r) }\ by auto show ?thesis unfolding normalize_poly_def apply (subst 1) apply (refine_rcg sort_poly_spec_id[OF assms] merge_coeffs_is_normalize_poly_p) subgoal by (drule merge_coeffs_is_normalize_poly_p) (auto intro!: RES_refine simp: RETURN_def) done qed subsection \Multiplication and normalisation\ definition mult_poly_p' :: \_\ where \mult_poly_p' p' q' = do { pq \ SPEC(\r. (mult_poly_p q')\<^sup>*\<^sup>* (p', {#}) ({#}, r)); SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* pq r) }\ lemma unsorted_poly_rel_fully_unsorted_poly_rel: \unsorted_poly_rel \ fully_unsorted_poly_rel\ proof - have \term_poly_list_rel \\<^sub>r int_rel \ unsorted_term_poly_list_rel \\<^sub>r int_rel\ by (auto simp: unsorted_term_poly_list_rel_def term_poly_list_rel_def) from list_rel_mono[OF this] show ?thesis unfolding poly_list_rel_def fully_unsorted_poly_list_rel_def by (auto simp:) qed lemma mult_poly_full_mult_poly_p': assumes \(p, p') \ sorted_poly_rel\ \(q, q') \ sorted_poly_rel\ shows \mult_poly_full p q \ \ (sorted_poly_rel) (mult_poly_p' p' q')\ unfolding mult_poly_full_def mult_poly_p'_def apply (refine_rcg full_normalize_poly_normalize_poly_p normalize_poly_normalize_poly_p) apply (subst RETURN_RES_refine_iff) apply (subst Bex_def) apply (subst mem_Collect_eq) apply (subst conj_commute) apply (rule mult_poly_raw_mult_poly_p[OF assms(1,2)]) subgoal by blast done definition add_poly_spec :: \_\ where \add_poly_spec p q = SPEC (\r. p + q - r \ ideal polynomial_bool)\ definition add_poly_p' :: \_\ where \add_poly_p' p q = SPEC(\r. add_poly_p\<^sup>*\<^sup>* (p, q, {#}) ({#}, {#}, r))\ lemma add_poly_l_add_poly_p': assumes \(p, p') \ sorted_poly_rel\ \(q, q') \ sorted_poly_rel\ shows \add_poly_l (p, q) \ \ (sorted_poly_rel) (add_poly_p' p' q')\ unfolding add_poly_p'_def apply (refine_rcg add_poly_l_spec[THEN fref_to_Down_curry_right, THEN order_trans, of _ p' q']) subgoal by auto subgoal using assms by auto subgoal by auto done subsection \Correctness\ context poly_embed begin definition mset_poly_rel where \mset_poly_rel = {(a, b). b = polynomial_of_mset a}\ definition var_rel where \var_rel = br \ (\_. True)\ lemma normalize_poly_p_normalize_poly_spec: \(p, p') \ mset_poly_rel \ SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p r) \ \mset_poly_rel (normalize_poly_spec p')\ by (auto simp: mset_poly_rel_def rtranclp_normalize_poly_p_poly_of_mset ideal.span_zero normalize_poly_spec_def intro!: RES_refine) lemma mult_poly_p'_mult_poly_spec: \(p, p') \ mset_poly_rel \ (q, q') \ mset_poly_rel \ mult_poly_p' p q \ \mset_poly_rel (mult_poly_spec p' q')\ unfolding mult_poly_p'_def mult_poly_spec_def apply refine_rcg apply (auto simp: mset_poly_rel_def dest!: rtranclp_mult_poly_p_mult_ideal_final) apply (intro RES_refine) using ideal.span_add_eq2 ideal.span_zero by (fastforce dest!: rtranclp_normalize_poly_p_poly_of_mset intro: ideal.span_add_eq2) lemma add_poly_p'_add_poly_spec: \(p, p') \ mset_poly_rel \ (q, q') \ mset_poly_rel \ add_poly_p' p q \ \mset_poly_rel (add_poly_spec p' q')\ unfolding add_poly_p'_def add_poly_spec_def apply (auto simp: mset_poly_rel_def dest!: rtranclp_add_poly_p_polynomial_of_mset_full) apply (intro RES_refine) apply (auto simp: rtranclp_add_poly_p_polynomial_of_mset_full ideal.span_zero) done end definition weak_equality_l :: \llist_polynomial \ llist_polynomial \ bool nres\ where \weak_equality_l p q = RETURN (p = q)\ definition weak_equality :: \int mpoly \ int mpoly \ bool nres\ where \weak_equality p q = SPEC (\r. r \ p = q)\ definition weak_equality_spec :: \mset_polynomial \ mset_polynomial \ bool nres\ where \weak_equality_spec p q = SPEC (\r. r \ p = q)\ lemma term_poly_list_rel_same_rightD: \(a, aa) \ term_poly_list_rel \ (a, ab) \ term_poly_list_rel \ aa = ab\ by (auto simp: term_poly_list_rel_def) lemma list_rel_term_poly_list_rel_same_rightD: \(xa, y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ (xa, ya) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ y = ya\ by (induction xa arbitrary: y ya) (auto simp: list_rel_split_right_iff dest: term_poly_list_rel_same_rightD) lemma weak_equality_l_weak_equality_spec: \(uncurry weak_equality_l, uncurry weak_equality_spec) \ sorted_poly_rel \\<^sub>r sorted_poly_rel \\<^sub>f \bool_rel\nres_rel\ by (intro frefI nres_relI) (auto simp: weak_equality_l_def weak_equality_spec_def sorted_poly_list_rel_wrt_def list_mset_rel_def br_def dest: list_rel_term_poly_list_rel_same_rightD) end -