From 9bfefece110938675d23e5297da3b0b90aaba690 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 22 Sep 2020 11:17:37 +0200 Subject: [PATCH] Begin commenting the formal proof --- checker/verified/Checker.thy | 54 ++--- checker/verified/Checker_Codegen.thy | 2 +- checker/verified/Huffman.thy | 264 ++++++++++++++++++--- checker/verified/Sorting_Network.thy | 123 +++++----- checker/verified/Sorting_Network_Bound.thy | 48 ++-- 5 files changed, 349 insertions(+), 142 deletions(-) diff --git a/checker/verified/Checker.thy b/checker/verified/Checker.thy index a54c3e9..c2436d5 100644 --- a/checker/verified/Checker.thy +++ b/checker/verified/Checker.thy @@ -211,7 +211,7 @@ qed (***) -fun list_to_vect :: \bool list \ vect\ where +fun list_to_vect :: \bool list \ bseq\ where \list_to_vect [] i = True\ | \list_to_vect (x # xs) 0 = x\ | \list_to_vect (x # xs) (Suc i) = list_to_vect xs i\ @@ -269,9 +269,9 @@ qed definition is_unsorted_vt :: \nat \ vect_trie \ bool\ where \is_unsorted_vt n A = (length_vt A > Suc n)\ -lemma fixed_width_vect_list_to_vect: - \length xs = n \ fixed_width_vect n (list_to_vect xs)\ - unfolding fixed_width_vect_def list_to_vect_as_nth +lemma fixed_len_bseq_list_to_vect: + \length xs = n \ fixed_len_bseq n (list_to_vect xs)\ + unfolding fixed_len_bseq_def list_to_vect_as_nth by simp lemma is_unsorted_vt_bound: @@ -279,8 +279,8 @@ lemma is_unsorted_vt_bound: shows \pls_bound (list_to_vect ` set_vt A) 1\ proof (rule unsorted_by_card_bound) fix v assume \v \ list_to_vect ` set_vt A\ - thus \fixed_width_vect n v\ - using assms fixed_width_vect_list_to_vect + thus \fixed_len_bseq n v\ + using assms fixed_len_bseq_list_to_vect by blast next show \n + 1 < card (list_to_vect ` set_vt A)\ @@ -404,8 +404,8 @@ definition invert_vt :: \bool \ vect_trie \ vect_t lemma list_to_vect_set_vt_fixed_width: assumes \set_vt A \ {xs. length xs = n}\ - shows \list_to_vect ` set_vt A \ {v. fixed_width_vect n v}\ - by (metis (mono_tags, lifting) Ball_Collect assms fixed_width_vect_list_to_vect image_subsetI + shows \list_to_vect ` set_vt A \ {v. fixed_len_bseq n v}\ + by (metis (mono_tags, lifting) Ball_Collect assms fixed_len_bseq_list_to_vect image_subsetI mem_Collect_eq) lemma invert_vt_bound: @@ -731,7 +731,7 @@ proof - show \\inj_on weight (list_to_vect ` set_vt A)\ using is_unsorted bound_unsorted by blast next - show \\v. v \ list_to_vect ` set_vt A \ fixed_width_vect width v\ + show \\v. v \ list_to_vect ` set_vt A \ fixed_len_bseq width v\ by (metis (full_types) A_lengths Ball_Collect list_to_vect_set_vt_fixed_width) next show \\c. fst c < snd c \ snd c < width \ @@ -787,7 +787,7 @@ lemma remove_nth_as_take_drop: \remove_nth i xs = take i xs @ drop (Suc i) xs\ by (induction i xs rule: remove_nth.induct; simp) -definition prune_nth :: \nat \ vect \ vect\ where +definition prune_nth :: \nat \ bseq \ bseq\ where \prune_nth n v i = (if i \ n then v (Suc i) else v i)\ lemma list_to_vect_remove_nth: @@ -999,10 +999,10 @@ lemma shift_channels_permutes: unshift_shift_inverse) lemma prune_nth_as_perm: - assumes \fixed_width_vect n v\ \v i\ \i < n\ + assumes \fixed_len_bseq n v\ \v i\ \i < n\ shows \prune_nth i v = apply_perm (shift_channels n i) v\ unfolding prune_nth_def shift_channels_def apply_perm_def - using assms fixed_width_vect_def by auto + using assms fixed_len_bseq_def by auto lemma inverted_prune_nth: assumes \i < Suc n\ @@ -1011,11 +1011,11 @@ lemma inverted_prune_nth: using assms by auto lemma prune_nth_as_perm_inverted: - assumes \fixed_width_vect n v\ \\v i\ \i < n\ + assumes \fixed_len_bseq n v\ \\v i\ \i < n\ shows \prune_nth i v = invert_vect (nat.pred n) (apply_perm (shift_channels n i) (invert_vect n v))\ proof - - have \fixed_width_vect n (invert_vect n v)\ + have \fixed_len_bseq n (invert_vect n v)\ by (simp add: assms(1) invert_vect_fixed_width) moreover have \(invert_vect n v) i\ by (simp add: assms(2) assms(3) invert_vect_def) @@ -1030,7 +1030,7 @@ proof - qed lemma prune_nth_as_perm_pol_image: - assumes \\v. v \ V \ fixed_width_vect n v\ \\v. v \ V \ v i = pol\ \i < n\ + assumes \\v. v \ V \ fixed_len_bseq n v\ \\v. v \ V \ v i = pol\ \i < n\ shows \prune_nth i ` V = apply_pol (nat.pred n) pol ` apply_perm (shift_channels n i) ` apply_pol n pol ` V\ @@ -1047,19 +1047,19 @@ proof - obtain n' where n': \n = Suc n'\ using assms less_imp_Suc_add by blast - have f1: \\v. v \ list_to_vect ` {xs \ set_vt A. xs ! i \ pol} \ fixed_width_vect n v\ + have f1: \\v. v \ list_to_vect ` {xs \ set_vt A. xs ! i \ pol} \ fixed_len_bseq n v\ by (metis (mono_tags) Collect_subset assms(3) image_mono in_mono list_to_vect_set_vt_fixed_width mem_Collect_eq) hence \\v. v \ apply_pol n (\ pol) ` list_to_vect ` {xs \ set_vt A. xs ! i \ pol} - \ fixed_width_vect n v\ + \ fixed_len_bseq n v\ using invert_vect_fixed_width by auto hence \\v. v \ apply_perm (shift_channels n i) ` apply_pol n (\ pol) ` list_to_vect ` {xs \ set_vt A. xs ! i \ pol} - \ fixed_width_vect n v\ + \ fixed_len_bseq n v\ by (meson apply_perm_fixed_width_image assms(2) shift_channels_permutes) moreover have \\v. v \ set_vt A \ v ! i \ pol \ @@ -1077,8 +1077,8 @@ proof - ultimately have f2: \\v. v \ apply_perm (shift_channels n i) ` apply_pol n (\ pol) ` list_to_vect ` {xs \ set_vt A. xs ! i \ pol} - \ fixed_width_vect n' v\ - unfolding n' fixed_width_vect_def + \ fixed_len_bseq n' v\ + unfolding n' fixed_len_bseq_def by (metis (no_types, lifting) Suc_leI le_imp_less_or_eq) @@ -1095,7 +1095,7 @@ proof - apply_pol n (\pol) ` list_to_vect ` {xs \ set_vt A. xs ! i \ pol}) b\ by (subst (asm) prune_nth_as_perm_pol_image[where n=n and pol=\\pol\]; - insert assms(2, 3) fixed_width_vect_list_to_vect list_to_vect_as_nth; auto simp add: n') + insert assms(2, 3) fixed_len_bseq_list_to_vect list_to_vect_as_nth; auto simp add: n') hence \pls_bound ( apply_perm (shift_channels n i) ` @@ -1223,7 +1223,7 @@ proof - have \pls_bound (list_to_vect ` set_vt A) (sucmax.value_bound_mset (mset_ran D))\ proof (rule pls_bound_from_pruned_bounds_pol[where n=width and pol=pol and B=D]) fix v assume v: \v \ list_to_vect ` set_vt A\ - thus \fixed_width_vect width v\ + thus \fixed_len_bseq width v\ by (metis A_lengths Ball_Collect v list_to_vect_set_vt_fixed_width) next show \finite (dom D)\ @@ -1449,16 +1449,16 @@ definition check_proof_get_bound :: \proof_cert \ (int \step_checked step\ - shows \lower_size_bound {v. fixed_width_vect (nat (step_width step)) v} (nat (step_bound step))\ + shows \partial_lower_size_bound {v. fixed_len_bseq (nat (step_width step)) v} (nat (step_bound step))\ proof - define A where \A = list_to_vect ` set_vt (vt_list (step_vect_list step))\ hence \pls_bound A (nat (step_bound step))\ using assms step_checked_def by auto - moreover have \A \ {v. fixed_width_vect (nat (step_width step)) v}\ + moreover have \A \ {v. fixed_len_bseq (nat (step_width step)) v}\ by (metis (no_types, lifting) A_def Ball_Collect assms list.pred_set list_to_vect_set_vt_fixed_width set_vt_list step_checked_def) ultimately have - \pls_bound {v. fixed_width_vect (nat (step_width step)) v} (nat (step_bound step))\ + \pls_bound {v. fixed_len_bseq (nat (step_width step)) v} (nat (step_bound step))\ using bound_mono_subset by blast thus ?thesis by (metis (full_types) mem_Collect_eq pls_bound_implies_lower_size_bound) @@ -1466,7 +1466,7 @@ qed lemma check_proof_get_bound_spec: assumes \check_proof_get_bound cert = Some (width, bound)\ - shows \lower_size_bound_for_width (nat width) (nat bound)\ + shows \lower_size_bound (nat width) (nat bound)\ proof - have checked: \check_proof cert \ cert_length cert > 0\ using assms unfolding check_proof_get_bound_def @@ -1479,7 +1479,7 @@ proof - thus ?thesis by (metis Pair_inject assms check_proof_get_bound_def checked last_step_def - option.inject step_checked_bound lower_size_bound_for_width_def) + option.inject step_checked_bound lower_size_bound_def) qed end diff --git a/checker/verified/Checker_Codegen.thy b/checker/verified/Checker_Codegen.thy index 19c56e3..bae5900 100644 --- a/checker/verified/Checker_Codegen.thy +++ b/checker/verified/Checker_Codegen.thy @@ -4,7 +4,7 @@ begin lemma check_proof_get_bound_spec: assumes \check_proof_get_bound cert = Some (width, bound)\ - shows \lower_size_bound_for_width (nat width) (nat bound)\ + shows \lower_size_bound (nat width) (nat bound)\ using assms by (rule Checker.check_proof_get_bound_spec) definition nat_pred_code :: \nat \ nat\ where diff --git a/checker/verified/Huffman.thy b/checker/verified/Huffman.thy index 23eba57..f35cfa4 100644 --- a/checker/verified/Huffman.thy +++ b/checker/verified/Huffman.thy @@ -2,6 +2,13 @@ theory Huffman imports Main "HOL-Library.Multiset" begin +text \In this theory we define Huffman's algorithm and prove its correctness for an arbitrary +Huffman algebra (TODO ref). If you are only interested in the parts specific to sorting networks, +you can skip this theory.\ + + +text \First we state the axioms of a Huffman algebra:\ + class huffman_algebra = fixes combine :: "'a::linorder \ 'a \ 'a" (infix \\\ 70) assumes increasing: \a \ a \ b\ @@ -10,10 +17,18 @@ class huffman_algebra = assumes mono: \a \ b \ a \ c \ b \ c\ assumes assoc_ineq: \a \ c \ (a \ b) \ c \ a \ (b \ c)\ +text \We need some additional lemmas about lists, finite multisets of list elements elements and +sorted lists of multiset elements.\ + +text \Removing the head of a list, removes the corresponding element from a multiset.\ + lemma mset_tl: \xs \ [] \ mset (tl xs) = mset xs - {#hd xs#}\ by (cases xs; simp) +text \The first element of a sorted list of multiset elements is the minimum element of a multiset +if the multiset is nonempty.\ + lemma hd_sorted_list_of_multiset: assumes \A \ {#}\ shows \hd (sorted_list_of_multiset A) = Min_mset A\ @@ -21,16 +36,24 @@ lemma hd_sorted_list_of_multiset: list.set_sel(1) mset.simps(1) mset_sorted_list_of_multiset set_ConsD set_mset_eq_empty_iff set_sorted_list_of_multiset sorted.simps(2) sorted_list_of_multiset_mset sorted_sort) +text \We can remove the smallest element of a nonempty multiset by turning it into a sorted list, +and building a multiset of that lists's tail.\ + lemma mset_tl_sorted_list_of_multiset: assumes \A \ {#}\ shows \mset (tl (sorted_list_of_multiset A)) = A - {#Min_mset A#}\ by (metis assms hd_sorted_list_of_multiset mset.simps(1) mset_sorted_list_of_multiset mset_tl) +text \If we have a sorted list, we can recover it from a multiset of its elements.\ + lemma unique_sorted_list_of_multiset: assumes \mset xs = A\ \sorted xs\ shows \xs = sorted_list_of_multiset A\ using assms(1) assms(2) sorted_sort_id by fastforce +text \The tail of a sorted list of multiset elements is the same as the sorted list of elements +after removing the minimal element.\ + lemma tl_sorted_list_of_multiset: assumes \A \ {#}\ shows \tl (sorted_list_of_multiset A) = sorted_list_of_multiset (A - {#Min_mset A#})\ @@ -41,41 +64,58 @@ proof - by (simp add: assms mset_tl_sorted_list_of_multiset unique_sorted_list_of_multiset) qed +(***) + +text \We also need an alternative characterization of the minimum function.\ + +lemma min_as_logic: + \min (a::'a::linorder) b = c \ (a = c \ a \ b) \ (b = c \ b \ a)\ + \c = min (a::'a::linorder) b \ (a = c \ a \ b) \ (b = c \ b \ a)\ + unfolding min_def by auto (***) +text \Huffman's algorithm repeatedly combines values in a multiset using the Huffman algebra's +operator. To prove that the resulting value is minimal, we need to manipulate syntax trees of +expressions using that operator, which we define here.\ + datatype 'a expr = Val (the_Val: 'a) ("\_\") | Op (left_subexpr: \'a expr\) (right_subexpr: \'a expr\) (infix "\" 70) -fun (in huffman_algebra) value_expr :: \'a expr \ 'a\ where - \value_expr \a\ = a\ | - \value_expr (E \ F) = value_expr E \ value_expr F\ - abbreviation is_Val :: \'a expr \ bool\ where \is_Val E \ \a. E = \a\\ abbreviation is_Op :: \'a expr \ bool\ where \is_Op E \ \L R. E = L \ R\ +text \The set of values in an expression is always non-empty and finite.\ + lemma set_expr_nonempty[simp]: \set_expr E \ {}\ by (induction E; auto) lemma set_expr_finite[simp]: \finite (set_expr E)\ by (induction E; auto) +text \We can recursively evaluate an expression using the Huffman algebra's operator.\ + +fun (in huffman_algebra) value_expr :: \'a expr \ 'a\ where + \value_expr \a\ = a\ | + \value_expr (E \ F) = value_expr E \ value_expr F\ + +text \We can flatten an expression into a nonempty list of contained values.\ + abbreviation list_expr :: \'a expr \ 'a list\ where \list_expr \ rec_expr (\a. [a]) (\_ _. (@))\ lemma list_expr_nonempty[simp]: \list_expr E \ []\ by (induction E; auto) +text \With this we can count the number of values in the expression.\ + abbreviation count_expr :: \'a expr \ nat\ where \count_expr E \ length (list_expr E)\ -lemma count_expr_size: \2 * count_expr E = Suc (size E)\ - by (induction E; auto) - lemma count_expr_ge1[simp]: \count_expr E \ 1\ by (simp add: Suc_leI) @@ -89,48 +129,88 @@ lemma is_Op_by_count: \is_Op E = (count_expr E \ 2)\ lemma expr_from_list: \list_expr E = [e] \ E = \e\\ by (cases E; simp add: append_eq_Cons_conv) +text \The number of values in an expression is also directly related to the size of an expression. +We get the size and several useful of its properties for free whenever we define an algebraic +datatype. With this we get corresponding useful properties also for the number of an expression's +values.\ + +lemma count_expr_size: \2 * count_expr E = Suc (size E)\ + by (induction E; auto) + +text \We define the multiset of an expression's values via the list of values.\ + abbreviation mset_expr :: \'a expr \ 'a multiset\ where \mset_expr E \ mset (list_expr E)\ +text \There is a unique expression containing just one given value.\ + lemma expr_from_mset: \mset_expr E = {# a #} \ E = \a\\ by (simp add: expr_from_list) +text \Ignoring the multiplicity of the multisets's values gives us the same set as the automatically +defined function for the set of values in an expression.\ + lemma set_mset_expr: \set_mset (mset_expr E) = set_expr E\ by (induction E; simp) +text \We define the head of an expression as the leftmost value in the syntax tree, and we do this +via flattening the expression to a list of values.\ + abbreviation hd_expr :: \'a expr \ 'a\ where \hd_expr E \ hd (list_expr E)\ +text \We get the minimum value in an expression as the minimum value of the set of its values.\ + definition Min_expr :: \'a::linorder expr \ 'a\ where \Min_expr E \ Min (set_expr E)\ +text \If the expression contains just one value, the minimum is that value.\ + lemma Min_expr_Val[simp]: \Min_expr \a\ = a\ unfolding Min_expr_def by simp +text \Otherwise the minimum value can be computed recursively.\ + lemma Min_expr_Op: \Min_expr (L \ R) = min (Min_expr L) (Min_expr R)\ unfolding Min_expr_def by (simp add: Min_Un min_def) +text \As the Huffman algebra operator is increasing in both arguments, the minimum value in an +expression is a lower bound for its evaluation.\ + lemma (in huffman_algebra) Min_expr_bound: \Min_expr E \ value_expr E\ by (induction E; simp add: Min_expr_Op; insert increasing min.coboundedI1 order_trans; blast) +text \If two expressions have the same multiset of values they contain the same minimum value.\ + lemma Min_expr_mset_cong: \mset_expr E = mset_expr F \ Min_expr E = Min_expr F\ unfolding Min_expr_def set_mset_expr[symmetric] by simp +text \The minimum value in an expression is also the minimum value of the multiset of its values.\ + lemma Min_expr_from_mset: \Min_expr E = Min_mset (mset_expr E)\ unfolding Min_expr_def by (fold set_mset_expr; simp) +text \We define the tail of an expression as the expression we get by removing the head if that is +possible. This is always possible as long as the expression contains one operator.\ + fun tl_expr :: \'a expr \ 'a expr\ where \tl_expr \a\ = \a\\ | \tl_expr (\l\ \ R) = R\ | \tl_expr ((L \ M) \ R) = tl_expr (L \ M) \ R\ - + +text \If the expression contains an operator, the tail of the list of its values is the same as the +list of values of its tail.\ + lemma list_tl_expr: \is_Op E \ list_expr (tl_expr E) = tl (list_expr E)\ by (induction E rule: tl_expr.induct; simp) +text \If two expressions have the same head and the same multiset of values, their tails also have +the same multiset of values.\ + lemma same_mset_tl_from_same_mset_mset_hd: assumes \hd_expr E = hd_expr F\ \mset_expr E = mset_expr F\ shows \mset_expr (tl_expr E) = mset_expr (tl_expr F)\ @@ -156,6 +236,9 @@ qed (***) +text \Given any property of an expression, we can define a corresponding property that holds if the +given property holds for all subexpressions of an expression (including the expression itself).\ + inductive all_subexpr :: \('a expr \ bool) \ 'a expr \ bool\ where val: \P \a\ \ all_subexpr P \a\\ | op: \\P (L \ R); all_subexpr P L; all_subexpr P R\ \ all_subexpr P (L \ R)\ @@ -170,37 +253,63 @@ lemma all_subexpr_expand: \all_subexpr P (L \ R) = (P (L \ R) (***) +text \An expression has a minimal head, if its head is the minimum of the contained values.\ + abbreviation Min_hd_expr :: \'a::linorder expr \ bool\ where \Min_hd_expr E \ hd_expr E = Min_expr E\ -lemma min_as_logic: - \min (a::'a::linorder) b = c \ (a = c \ a \ b) \ (b = c \ b \ a)\ - \c = min (a::'a::linorder) b \ (a = c \ a \ b) \ (b = c \ b \ a)\ - unfolding min_def by auto +text \If an expression has this property, so does its left subexpression.\ lemma Min_hd_expr_left_subexpr: \Min_hd_expr (L \ R) \ Min_hd_expr L\ by (induction L; auto simp add: Min_expr_Op min_as_logic) +text \In that case the minimum value contained in the left subexpression is at least as small as the +minimum value contained in the right subexpression.\ + lemma Min_hd_expr_subexpr_ord: \Min_hd_expr (L \ R) \ Min_expr L \ Min_expr R\ using Min_hd_expr_left_subexpr min.orderI by (fastforce simp add: Min_expr_Op) +text \Hence to find the minimum value in an minimal head expression, we only need to look at the +left subexpression.\ + lemma Min_hd_expr_left_subexpr_Min: \Min_hd_expr (L \ R) \ Min_expr (L \ R) = Min_expr L\ by (induction L; auto simp add: Min_expr_Op min_as_logic) +text \If two minimal head expressions have the same head they have same minimum contained value.\ + lemma Min_hd_expr_Min_from_hd_cong: assumes \Min_hd_expr E\ \Min_hd_expr F\ \hd_expr E = hd_expr F\ shows \Min_expr E = Min_expr F\ using assms by simp +text \To turn an expression into a minimal head expression without changing the value it evaluates +to, we can swap the sides of every operator where the right subexpression contains a smaller value +than the minimum value on the left.\ + +text \To do this we first define this function which combines two subexpressions such that the +minimum value is on the left.\ + function Min_to_hd_subexpr :: \'a::linorder expr \ 'a::linorder expr \ 'a expr\ where \Min_expr L \ Min_expr R \ Min_to_hd_subexpr L R = L \ R\ | \\(Min_expr L \ Min_expr R) \ Min_to_hd_subexpr L R = R \ L\ by auto termination by lexicographic_order +text \Doing this results in an expression with the same multiset of values as combining them in a +fixed order would result in.\ + lemma Min_to_hd_subexpr_mset: \mset_expr (Min_to_hd_subexpr L R) = mset_expr (L \ R)\ by (cases \(L, R)\ rule: Min_to_hd_subexpr.cases; auto) +text \And does not change the value it evaluates to.\ + +lemma (in huffman_algebra) value_Min_to_hd_subexpr: + \value_expr (Min_to_hd_subexpr L R) = value_expr L \ value_expr R\ + by (metis Min_to_hd_subexpr.simps commutative value_expr.simps(2)) + +text \If we have two expressions, both for which all subexpression have a minimal head, combining +them this way results in an expression where still all subexpressions have a minimal head.\ + lemma Min_to_hd_subexpr_spec: assumes \all_subexpr Min_hd_expr L\ \all_subexpr Min_hd_expr R\ shows \all_subexpr Min_hd_expr (Min_to_hd_subexpr L R)\ @@ -224,6 +333,9 @@ next using assms False by auto qed +text \Thus we can turn any expression into one with only minimal head subexpressions, by recursing +and combining subexpressions with @{term Min_to_hd_subexpr}.\ + fun Min_to_hd_expr :: \'a::linorder expr \ 'a expr\ where \Min_to_hd_expr \a\ = \a\\ | \Min_to_hd_expr (L \ R) = Min_to_hd_subexpr (Min_to_hd_expr L) (Min_to_hd_expr R)\ @@ -234,22 +346,25 @@ lemma Min_to_hd_expr_spec: (subst Min_to_hd_expr.simps; rule Min_to_hd_subexpr_spec)?; auto) +text \This does not change the multiset of values nor what the expression evaluates to.\ + lemma Min_to_hd_expr_mset: \mset_expr (Min_to_hd_expr E) = mset_expr E\ by (induction E rule: Min_to_hd_expr.induct; simp add: Min_to_hd_subexpr_mset) -lemma (in huffman_algebra) value_Min_to_hd_subexpr: - \value_expr (Min_to_hd_subexpr L R) = value_expr L \ value_expr R\ - by (metis Min_to_hd_subexpr.simps commutative value_expr.simps(2)) - lemma (in huffman_algebra) value_Min_to_hd_expr: \value_expr (Min_to_hd_expr E) = value_expr E\ by (induction E rule: Min_to_hd_expr.induct; simp add: value_Min_to_hd_subexpr) (***) +text \We also want an expression's tail to have a minimal head, such that the two smallest values +are the leftmost of an expression.\ + abbreviation tl_Min_hd_expr :: \'a::linorder expr \ bool\ where \tl_Min_hd_expr E \ Min_hd_expr (tl_expr E)\ +text \This property depends only on the list of elements, not on how they are nested.\ + lemma tl_Min_hd_expr_list_expr_cong: assumes \list_expr E = list_expr F\ shows \tl_Min_hd_expr E = tl_Min_hd_expr F\ @@ -262,6 +377,11 @@ proof - by (metis Min_expr_mset_cong) qed +text \By going through several cases, we can rearrange subexpression to ensure that the minimum +value of the tail of an expression is in the left subexpression of an expression. We do this in a +way that the Huffman algebra axioms ensure that the evaluation result is not increased as long as +all subexpressions of the input have a minimal head.\ + function tl_Min_to_hd_subexpr :: \'a::linorder expr \ 'a expr\ where \tl_Min_to_hd_subexpr \a\ = \a\\ | \tl_Min_to_hd_subexpr (\l\ \ R) = \l\ \ R\ | @@ -276,16 +396,23 @@ function tl_Min_to_hd_subexpr :: \'a::linorder expr \ 'a expr\ by (auto, metis tl_expr.cases) termination by lexicographic_order +text \We show that it does not change the size.\ + lemma tl_Min_to_hd_subexpr_size[simp]: \size (tl_Min_to_hd_subexpr E) = size E\ by (induction E rule: tl_Min_to_hd_subexpr.induct; simp) +text \Which allows us to apply it while recursing on the result of that application.\ + fun tl_Min_to_hd_expr :: \'a::linorder expr \ 'a expr\ and helper_tl_Min_to_hd_expr :: \'a::linorder expr \ 'a expr\ where \tl_Min_to_hd_expr E = helper_tl_Min_to_hd_expr (tl_Min_to_hd_subexpr E) \ | \helper_tl_Min_to_hd_expr \a\ = \a\\ | \helper_tl_Min_to_hd_expr (L \ R) = tl_Min_to_hd_expr L \ R\ +text \This recursion also does not change the multiset of values, the minimum value, the head, the +multiset of tail values or the minimum value of the tail.\ + lemma tl_Min_to_hd_expr_mset: \mset_expr (tl_Min_to_hd_expr E) = mset_expr E\ proof (induction \size E\ arbitrary: E rule: less_induct) case less @@ -293,6 +420,7 @@ proof (induction \size E\ arbitrary: E rule: less_induct) by (cases E rule: tl_Min_to_hd_subexpr.cases; simp) qed + lemma tl_Min_to_hd_expr_Min: \Min_expr (tl_Min_to_hd_expr E) = Min_expr E\ using tl_Min_to_hd_expr_mset[of E] unfolding Min_expr_def set_mset_expr[symmetric] @@ -312,45 +440,75 @@ lemma tl_Min_to_hd_expr_mset_tl: \mset_expr (tl_expr (tl_Min_to_hd_expr E) lemma tl_Min_to_hd_expr_Min_tl: \Min_expr (tl_expr (tl_Min_to_hd_expr E)) = Min_expr (tl_expr E)\ using Min_expr_mset_cong tl_Min_to_hd_expr_mset_tl by blast +text \To further analyze @{term tl_Min_to_hd_subexpr}, we need various lemmas about minimum +contained values and minimal head values for expressions and tails of expressions and how they +relate when rearranging subexpressions.\ + +text \Given a minimal head expression, if we rewrite the left subexpression without changing the +minimum value or the head, we still have a minimal head expression.\ + lemma Min_hd_expr_rewrite_left: assumes \Min_hd_expr (L \ R)\ \Min_expr L = Min_expr L'\ \Min_hd_expr L'\ shows \Min_hd_expr (L' \ R)\ by (metis (mono_tags, lifting) Min_expr_Op Min_hd_expr_left_subexpr assms expr.simps(8) hd_append2 list_expr_nonempty) +text \If we have a minimal head expression and exchange the right subexpression with the right +subexpression of the left subexpression, we still have a minimal head expression.\ + lemma Min_hd_expr_exchange_right: assumes \Min_hd_expr ((L \ M) \ R)\ shows \Min_hd_expr ((L \ R) \ M)\ using assms by (simp add: Min_expr_Op; metis min.commute min.assoc) +text \This extends to all minimal head subexpressions.\ + lemma all_subexpr_Min_hd_expr_exchange_right: assumes \all_subexpr Min_hd_expr ((L \ M) \ R)\ shows \all_subexpr Min_hd_expr ((L \ R) \ M)\ by (intro all_subexpr.op; insert assms Min_hd_expr_exchange_right Min_hd_expr_left_subexpr; blast) +text \Combining an expression where the tail has a minimal head with a singleton expression still +has a tail with a minimal head, if that singleton expression is larger than the tail's minimal +head.\ + lemma tl_Min_hd_expr_right_Val: assumes \tl_Min_hd_expr L\ \Min_expr (tl_expr L) \ r\ shows \tl_Min_hd_expr (L \ \r\)\ using assms by (cases L; simp add: Min_expr_Op min_absorb1 dual_order.trans min_def_raw) +text \If we have an upper bound for the minimum value in an expression, combining it with another +expression on the left and then taking the tail of the resulting expression results in an expression +that still has that upper bound, as it still contains all values of our initial expression.\ + lemma Min_expr_tl_bound: assumes \Min_expr M \ r\ shows \Min_expr (tl_expr (L \ M)) \ r\ using assms by (cases L; simp add: Min_expr_Op min_le_iff_disj) +text \If we have a nonsingleton expression whose tail has a minimal head, combining it with another +expression on the right whose minimal value is not smaller than the left expression's tail's minimal +head, is an expression whose tail again has a minimal head.\ + lemma tl_Min_hd_expr_right: assumes \is_Op L\ \tl_Min_hd_expr L\ \Min_expr (tl_expr L) \ Min_expr R\ shows \tl_Min_hd_expr (L \ R)\ using assms by (cases L; simp add: Min_expr_Op min_absorb1 dual_order.trans min_def_raw) +text \Applying @{term tl_Min_to_hd_expr} to a non-singleton expression results in a non-singleton +expression.\ + lemma is_Op_tl_Min_to_hd_expr: \is_Op (tl_Min_to_hd_expr (L \ R))\ unfolding is_Op_by_count by (metis (mono_tags, lifting) count_expr_Op mset_eq_length tl_Min_to_hd_expr_mset) +text \If we have an expression where all subexpressions have a minimal head, applying @{term +tl_Min_to_hd_expr} results in an expression where the tail has a minimal head.\ + lemma tl_Min_to_hd_expr_spec: \all_subexpr Min_hd_expr E \ tl_Min_hd_expr (tl_Min_to_hd_expr E)\ proof (induction \size E\ arbitrary: E rule: less_induct) @@ -426,6 +584,9 @@ case less qed qed +text \If we have an expression where all subexpressions have a minimal head, applying @{term +tl_Min_to_hd_expr} also does not increase the evaluation result.\ + lemma (in huffman_algebra) value_tl_Min_to_hd_expr: \all_subexpr Min_hd_expr E \ value_expr (tl_Min_to_hd_expr E) \ value_expr E\ proof (induction \size E\ arbitrary: E rule: less_induct) @@ -480,12 +641,26 @@ qed (***) +text \At this point we can move the two smallest values of an expression to the very left without +increasing its value. To show that we can always combine the smallest two values, we now need to +make sure that the leftmost nonsingleton subexpression combines two singleton subexpression, i.e.\ +combines two values.\ + +inductive left_nested_expr :: \'a expr \ bool\ where + pair: \left_nested_expr (\l\ \ \r\)\ | + nested: \left_nested_expr L \ left_nested_expr (L \ R)\ + +text \Whenever we have a singleton subexpression on the left, but not on the right, we can perform a +rotation that splits the nonsingleton right subexpression.\ + fun nest_left_subexpr :: \'a::linorder expr \ 'a expr\ where \nest_left_subexpr \a\ = \a\\ | \nest_left_subexpr (\l\ \ \r\) = (\l\ \ \r\)\ | \nest_left_subexpr (\l\ \ (M \ R)) = (\l\ \ M) \ R\ | \nest_left_subexpr ((L \ M) \ R) = ((L \ M) \ R)\ +text \This does not change the expression's size or multiset of values.\ + lemma nest_left_subexpr_size[simp]: \size (nest_left_subexpr E) = size E\ by (induction E rule: nest_left_subexpr.induct; simp) @@ -494,12 +669,16 @@ lemma nest_left_subexpr_mset[simp]: \mset_expr (nest_left_subexpr E) = mset_expr E\ by (induction E rule: nest_left_subexpr.induct; simp) +text \We can perform such rotations and then recurse on the left subexpression of the result. \ + fun nest_left_expr :: \'a::linorder expr \ 'a expr\ and helper_nest_left_expr :: \'a::linorder expr \ 'a expr\ where \nest_left_expr E = helper_nest_left_expr (nest_left_subexpr E) \ | \helper_nest_left_expr \a\ = \a\\ | \helper_nest_left_expr (L \ R) = nest_left_expr L \ R\ +text \Rotations don't change the list order of values.\ + lemma nest_left_expr_list: \list_expr (nest_left_expr E) = list_expr E\ proof (induction \size E\ arbitrary: E rule: less_induct) case less @@ -507,12 +686,11 @@ proof (induction \size E\ arbitrary: E rule: less_induct) by (cases E rule: nest_left_subexpr.cases; simp) qed -inductive left_nested_expr :: \'a expr \ bool\ where - pair: \left_nested_expr (\l\ \ \r\)\ | - nested: \left_nested_expr L \ left_nested_expr (L \ R)\ - declare left_nested_expr.intros[intro] left_nested_expr.cases[elim] +text \Performing these rotations results in an expression that has the wanted property of directly +combining the leftmost value with another value.\ + lemma left_nested_nest_left_expr: \is_Op E \ left_nested_expr (nest_left_expr E)\ proof (induction \size E\ arbitrary: E rule: less_induct) @@ -521,6 +699,9 @@ proof (induction \size E\ arbitrary: E rule: less_induct) by (cases E rule: nest_left_subexpr.cases; auto) qed +text \If the initial expression has a minimal head, these rotations also do not increase the +evaluation result.\ + lemma (in huffman_algebra) value_nest_left_expr: \\Min_hd_expr E\ \ value_expr (nest_left_expr E) \ value_expr E\ proof (induction \size E\ arbitrary: E rule: less_induct) @@ -556,24 +737,20 @@ proof (induction \size E\ arbitrary: E rule: less_induct) qed qed -(***) - -lemma Min_hd_expr_sorted_1: - \Min_hd_expr E \ hd_expr E = hd (sorted_list_of_multiset (mset_expr E))\ - by (metis Min_expr_from_mset hd_sorted_list_of_multiset length_0_conv list_expr_nonempty - mset.simps(1) size_mset) - -lemma Min_hd_expr_sorted_2: - assumes \is_Op E\ \Min_hd_expr E\ \tl_Min_hd_expr E\ - shows \hd_expr (tl_expr E) = hd (tl (sorted_list_of_multiset (mset_expr E)))\ - by (metis Min_expr_from_mset Min_hd_expr_sorted_1 assms list_expr_nonempty - list_tl_expr mset_tl mset_zero_iff tl_sorted_list_of_multiset) (***) +text \We now combine our three rearrangement steps: first we swap left and right subexpressions +whenever the right subexpression contains a smaller value, then we rearrange subexpressions to move +the second smallest value to the second position from the left and finally we perform tree rotations +to pair up the two smallest values.\ + definition rearrange_expr :: \'a::linorder expr \ 'a expr\ where \rearrange_expr E = nest_left_expr (tl_Min_to_hd_expr (Min_to_hd_expr E))\ +text \As intended, the result has the same multiset of values, still has a minimal head and a tail +with minimal head and does have the two leftmost values in the leftmost nonsingleton subexpression.\ + lemma rearrange_expr_mset: \mset_expr (rearrange_expr E) = mset_expr E\ by (metis Min_to_hd_expr_mset nest_left_expr_list rearrange_expr_def tl_Min_to_hd_expr_mset) @@ -598,6 +775,8 @@ proof - using left_nested_nest_left_expr by blast qed +text \All this combined also does not increase the evaluation result.\ + lemma (in huffman_algebra) value_rearrange_expr: \value_expr (rearrange_expr E) \ value_expr E\ unfolding rearrange_expr_def @@ -605,6 +784,27 @@ lemma (in huffman_algebra) value_rearrange_expr: tl_Min_to_hd_expr_Min tl_Min_to_hd_expr_hd value_Min_to_hd_expr value_nest_left_expr value_tl_Min_to_hd_expr) +(***) + +text \For an expression with a minimal head, the head value is the head of the sorted list of its +values.\ + +lemma Min_hd_expr_sorted_1: + \Min_hd_expr E \ hd_expr E = hd (sorted_list_of_multiset (mset_expr E))\ + by (metis Min_expr_from_mset hd_sorted_list_of_multiset length_0_conv list_expr_nonempty + mset.simps(1) size_mset) + +text \For an expression with a minimal head and a tail with minimal head, the head value of its +tail is the second value in the sorted list of its values.\ + +lemma Min_hd_expr_sorted_2: + assumes \is_Op E\ \Min_hd_expr E\ \tl_Min_hd_expr E\ + shows \hd_expr (tl_expr E) = hd (tl (sorted_list_of_multiset (mset_expr E)))\ + by (metis Min_expr_from_mset Min_hd_expr_sorted_1 assms list_expr_nonempty + list_tl_expr mset_tl mset_zero_iff tl_sorted_list_of_multiset) + +(** TODO continue here **) + lemma hd_list_rearrange_expr: \hd (list_expr (rearrange_expr E)) = hd (sorted_list_of_multiset (mset_expr E))\ by (metis Min_expr_from_mset Min_hd_rearrange_expr hd_sorted_list_of_multiset list_expr_nonempty diff --git a/checker/verified/Sorting_Network.thy b/checker/verified/Sorting_Network.thy index 82686e0..9de515a 100644 --- a/checker/verified/Sorting_Network.thy +++ b/checker/verified/Sorting_Network.thy @@ -2,6 +2,9 @@ theory Sorting_Network imports Main Sorting_Network_Bound "HOL-Library.Permutations" "HOL-Library.Multiset" "Huffman" begin +text \Minimum and maximum on Booleans are just conjunction and disjunction, which are often easier +to work with.\ + lemma bool_min_is_conj[simp]: \min a b = (a \ b)\ unfolding min_def by auto @@ -9,34 +12,38 @@ lemma bool_max_is_disj[simp]: \max a b = (a \ b)\ unfolding max_def by auto lemma apply_cmp_logic: - \apply_cmp c v i = (v i \ (i \ fst c \ v (snd c)) \ (i = snd c \ v (fst c)))\ + \apply_cmp c x i = (x i \ (i \ fst c \ x (snd c)) \ (i = snd c \ x (fst c)))\ unfolding apply_cmp_def Let_def case_prod_unfold by auto -lemma apply_cmp_swap_or_id: - \apply_cmp c v = v \ apply_cmp c v = Fun.swap (fst c) (snd c) v\ -proof (cases \v (fst c) \ \v (snd c)\) +text \Applying a comparator to a given sequence is either an exchange or the identity.\ + +lemma apply_cmp_exch_or_id: + \apply_cmp c x = x \ apply_cmp c x = Fun.swap (fst c) (snd c) x\ +proof (cases \x (fst c) \ \x (snd c)\) case True - hence \apply_cmp c v = Fun.swap (fst c) (snd c) v\ + hence \apply_cmp c x = Fun.swap (fst c) (snd c) x\ by (simp add: apply_cmp_def case_prod_beta' swap_def) thus ?thesis.. next case False - hence \apply_cmp c v = v\ + hence \apply_cmp c x = x\ unfolding apply_cmp_logic by blast thus ?thesis.. qed +text \A comparator $(i, i)$ is always the identity.\ + lemma apply_cmp_same_channels: - \fst c = snd c \ apply_cmp c v = v\ - using apply_cmp_swap_or_id by fastforce + \fst c = snd c \ apply_cmp c x = x\ + using apply_cmp_exch_or_id by fastforce lemma apply_cmp_fixed_width_snd_oob: - assumes \fixed_width_vect n v\ \snd c \ n\ + assumes \fixed_len_bseq n v\ \snd c \ n\ shows \apply_cmp c v = v\ using assms - unfolding fixed_width_vect_def apply_cmp_logic + unfolding fixed_len_bseq_def apply_cmp_logic proof (intro impI ext) fix i assume fixed_width: \\i\n. v i = True\ @@ -55,7 +62,7 @@ qed (***) -definition weight :: \vect \ nat\ where +definition weight :: \bseq \ nat\ where \weight v = card (v -` {False})\ lemma \weight (apply_cmp c v) = weight v\ @@ -66,7 +73,7 @@ proof (cases \apply_cmp c v = v\) next case False hence \apply_cmp c v = Fun.swap (fst c) (snd c) v\ - using apply_cmp_swap_or_id by blast + using apply_cmp_exch_or_id by blast hence \apply_cmp c v = v \ Fun.swap (fst c) (snd c) id\ by (simp add: comp_swap) hence \apply_cmp c v -` {False} = (v \ Fun.swap (fst c) (snd c) id) -` {False}\ @@ -78,16 +85,16 @@ next qed lemma fixed_width_false_set: - \fixed_width_vect n v \ (v -` {False}) \ {.. - unfolding fixed_width_vect_def + \fixed_len_bseq n v \ (v -` {False}) \ {.. + unfolding fixed_len_bseq_def using leI by blast lemma fixed_width_weight_bound: - \fixed_width_vect n v \ weight v \ n\ + \fixed_len_bseq n v \ weight v \ n\ by (metis fixed_width_false_set card_lessThan weight_def card_mono finite_lessThan) lemma fixed_width_mono_at_weight: - assumes \fixed_width_vect n v\ \mono v\ \i = weight v\ + assumes \fixed_len_bseq n v\ \mono v\ \i = weight v\ shows \v i = True\ proof (rule ccontr) assume \v i \ True\ @@ -101,7 +108,7 @@ proof (rule ccontr) qed lemma fixed_width_mono_from_weight: - assumes \fixed_width_vect n v\ \mono v\ + assumes \fixed_len_bseq n v\ \mono v\ shows \v i = (i \ weight v)\ proof (cases \i \ weight v\) case True @@ -110,11 +117,11 @@ proof (cases \i \ weight v\) next case False thus ?thesis - by (metis (full_types) assms(2) fixed_width_vect_def fixed_width_weight_bound le_boolD monoD) + by (metis (full_types) assms(2) fixed_len_bseq_def fixed_width_weight_bound le_boolD monoD) qed lemma weight_inj_on_fixed_width_mono: - assumes \\v. v \ V \ mono v \ fixed_width_vect n v\ + assumes \\v. v \ V \ mono v \ fixed_len_bseq n v\ shows \inj_on weight V\ proof (intro inj_onI ext) fix v w i assume vw: \v \ V\ \w \ V\ \weight v = weight w\ @@ -123,19 +130,19 @@ proof (intro inj_onI ext) qed lemma apply_cmp_fixed_width: - assumes \fixed_width_vect n v\ - shows \fixed_width_vect (Suc (max n (max (fst c) (snd c)))) (apply_cmp c v)\ + assumes \fixed_len_bseq n v\ + shows \fixed_len_bseq (Suc (max n (max (fst c) (snd c)))) (apply_cmp c v)\ unfolding apply_cmp_logic - using assms fixed_width_vect_def by auto + using assms fixed_len_bseq_def by auto lemma apply_cmp_fixed_width_in_bounds: - assumes \fixed_width_vect n v\ \fst c < n\ \snd c < n\ - shows \fixed_width_vect n (apply_cmp c v)\ + assumes \fixed_len_bseq n v\ \fst c < n\ \snd c < n\ + shows \fixed_len_bseq n (apply_cmp c v)\ unfolding apply_cmp_logic - using assms fixed_width_vect_def by auto + using assms fixed_len_bseq_def by auto lemma apply_cn_fixed_width: - \fixed_width_vect n v \ \n'. fixed_width_vect n' (fold apply_cmp cn v)\ + \fixed_len_bseq n v \ \n'. fixed_len_bseq n' (fold apply_cmp cn v)\ proof (induction cn arbitrary: n v) case Nil thus ?case @@ -157,13 +164,13 @@ qed (***) -definition pls_bound :: \vect set \ nat \ bool\ where +definition pls_bound :: \bseq set \ nat \ bool\ where \pls_bound V b = (\cn. inj_on weight (fold apply_cmp cn ` V) \ length cn \ b)\ lemma pls_bound_implies_lower_size_bound: - assumes \\v. v \ V \ fixed_width_vect n v\ \pls_bound V b\ - shows \lower_size_bound V b\ - unfolding lower_size_bound_def + assumes \\v. v \ V \ fixed_len_bseq n v\ \pls_bound V b\ + shows \partial_lower_size_bound V b\ + unfolding partial_lower_size_bound_def proof (intro allI impI) fix cn assume cn_sorts: \\v \ V. mono (fold apply_cmp cn v)\ @@ -175,9 +182,9 @@ proof (intro allI impI) hence \mono v \ mono w\ using cn_sorts by auto - moreover obtain n_v where \fixed_width_vect n_v v\ + moreover obtain n_v where \fixed_len_bseq n_v v\ by (metis v_asm apply_cn_fixed_width assms(1) imageE) - moreover obtain n_w where \fixed_width_vect n_w w\ + moreover obtain n_w where \fixed_len_bseq n_w w\ by (metis w_asm apply_cn_fixed_width assms(1) imageE) ultimately have \\i. v i = (i \ weight v)\ \\i. w i = (i \ weight w)\ using fixed_width_mono_from_weight @@ -240,7 +247,7 @@ lemma bound_weaken: (***) lemma unsorted_by_card_bound: - assumes \\v. v \ V \ fixed_width_vect n v\ \card V > n + 1\ + assumes \\v. v \ V \ fixed_len_bseq n v\ \card V > n + 1\ shows \pls_bound V 1\ proof(rule unsorted_bound; rule) assume \inj_on weight V\ @@ -263,7 +270,7 @@ lemma inj_on_invariant_bij_image: (***) -definition apply_perm :: \(nat \ nat) \ vect \ vect\ where +definition apply_perm :: \(nat \ nat) \ bseq \ bseq\ where \apply_perm p v i = v (p i)\ @@ -378,14 +385,14 @@ proof qed lemma apply_perm_fixed_width: - assumes \p permutes {.. \fixed_width_vect n v\ - shows \fixed_width_vect n (apply_perm p v)\ - using assms unfolding fixed_width_vect_def apply_perm_def permutes_def + assumes \p permutes {.. \fixed_len_bseq n v\ + shows \fixed_len_bseq n (apply_perm p v)\ + using assms unfolding fixed_len_bseq_def apply_perm_def permutes_def by simp lemma apply_perm_fixed_width_image: - assumes \p permutes {.. \\v. v \ V \ fixed_width_vect n v\ - shows \\v. v \ apply_perm p ` V \ fixed_width_vect n v\ + assumes \p permutes {.. \\v. v \ V \ fixed_len_bseq n v\ + shows \\v. v \ apply_perm p ` V \ fixed_len_bseq n v\ using apply_perm_fixed_width assms by blast (***) @@ -427,7 +434,7 @@ qed lemma ocmp_suc_bound: assumes unsorted: \\inj_on weight V\ - and fixed_width: \\v. v \ V \ fixed_width_vect n v\ + and fixed_width: \\v. v \ V \ fixed_len_bseq n v\ and suc_bounds: \\c. fst c < snd c \ snd c < n \ pls_bound (apply_cmp c ` V) b \ pls_bound (apply_cmp c ` V) = pls_bound V\ @@ -475,7 +482,7 @@ qed (***) -definition redundant_cmp :: \cmp \ vect set \ bool\ where +definition redundant_cmp :: \cmp \ bseq set \ bool\ where \redundant_cmp c V = (\((\v \ V. v (fst c) \ \v (snd c)) \ (\v \ V. \v (fst c) \ v (snd c))))\ lemma redundant_cmp_id: @@ -529,7 +536,7 @@ lemma redundant_cmp_bound: (***) -definition invert_vect :: \nat \ vect \ vect\ where +definition invert_vect :: \nat \ bseq \ bseq\ where \invert_vect n v i = (v i \ (i < n))\ lemma invert_vect_invol: \invert_vect n \ invert_vect n = id\ @@ -539,12 +546,12 @@ lemma invert_vect_bij: \bij (invert_vect n)\ using invert_vect_invol o_bij by blast lemma invert_vect_fixed_width: - assumes \fixed_width_vect n v\ - shows \fixed_width_vect n (invert_vect n v)\ - using assms fixed_width_vect_def invert_vect_def by auto + assumes \fixed_len_bseq n v\ + shows \fixed_len_bseq n (invert_vect n v)\ + using assms fixed_len_bseq_def invert_vect_def by auto lemma invert_false_set: - assumes \fixed_width_vect n v\ + assumes \fixed_len_bseq n v\ shows \invert_vect n v -` {False} = {.. proof (rule set_eqI) fix i @@ -553,7 +560,7 @@ proof (rule set_eqI) also have \\ = (i < n \ v i)\ by simp also have \\ = (v i = (i < n))\ - using assms fixed_width_vect_def by auto + using assms fixed_len_bseq_def by auto also have \\ = (\invert_vect n v i)\ by (simp add: invert_vect_def) also have \\ = (i \ invert_vect n v -` {False})\ @@ -563,7 +570,7 @@ proof (rule set_eqI) qed lemma invert_vect_weight: - assumes \fixed_width_vect n v\ + assumes \fixed_len_bseq n v\ shows \weight (invert_vect n v) = n - weight v\ unfolding weight_def by (metis assms card_Diff_subset card_lessThan finite_lessThan finite_subset @@ -605,7 +612,7 @@ lemma invert_vect_cmp_comp: by (rule ext; insert assms; simp add: invert_vect_cmp) lemma inverted_bound: - assumes \\v. v \ V \ fixed_width_vect n v\ \pls_bound V b\ + assumes \\v. v \ V \ fixed_len_bseq n v\ \pls_bound V b\ shows \pls_bound (invert_vect n ` V) b\ using assms proof (induction b arbitrary: n V) @@ -628,7 +635,7 @@ next invert_vect_bij invert_vect_weight plus_1_eq_Suc subset_UNIV) next fix v - show \v \ invert_vect n ` V \ fixed_width_vect n v\ + show \v \ invert_vect n ` V \ fixed_len_bseq n v\ using Suc.prems(1) invert_vect_fixed_width by auto next fix c assume \fst c < snd c \ snd c < n\ @@ -650,7 +657,7 @@ qed (***) -definition pruned_bound :: \vect set \ nat \ nat \ bool\ where +definition pruned_bound :: \bseq set \ nat \ nat \ bool\ where \pruned_bound V i b = (((\) i) \ V \ pls_bound {v \ V. \v i} b)\ lemma pls_bound_from_pruned_bound: @@ -765,7 +772,7 @@ qed (***) -definition pruned_bounds :: \vect set \ (nat \ nat) \ bool\ where +definition pruned_bounds :: \bseq set \ (nat \ nat) \ bool\ where \pruned_bounds V B = (\i \ dom B. pruned_bound V i (the (B i)))\ definition combine_bounds :: \nat option \ nat option \ nat option\ where @@ -1297,20 +1304,20 @@ lemma pls_bound_from_pruned_bounds: (***) -abbreviation apply_pol :: \nat \ bool \ vect \ vect\ where +abbreviation apply_pol :: \nat \ bool \ bseq \ bseq\ where \apply_pol n pol v \ (if pol then v else invert_vect n v)\ lemma apply_pol_invol: \apply_pol n pol (apply_pol n pol v) = v\ by (cases pol; simp add: invert_vect_invol pointfree_idE) -definition pruned_bound_pol :: \nat \ bool \ vect set \ nat \ nat \ bool\ where +definition pruned_bound_pol :: \nat \ bool \ bseq set \ nat \ nat \ bool\ where \pruned_bound_pol n pol V i b = pruned_bound (apply_pol n pol ` V) i b\ -definition pruned_bounds_pol :: \nat \ bool \ vect set \ (nat \ nat) \ bool\ where +definition pruned_bounds_pol :: \nat \ bool \ bseq set \ (nat \ nat) \ bool\ where \pruned_bounds_pol n pol V B = (\i \ dom B. pruned_bound_pol n pol V i (the (B i)))\ lemma pls_bound_from_pruned_bounds_pol: - assumes \\v. v \ V \ fixed_width_vect n v\ + assumes \\v. v \ V \ fixed_len_bseq n v\ \pruned_bounds_pol n pol V B\ \finite (dom B)\ \dom B \ {}\ shows \pls_bound V (sucmax.value_bound_mset (mset_ran B))\ proof (cases pol) @@ -1336,13 +1343,13 @@ next qed lemma apply_pol_bound: - assumes \\v. v \ V \ fixed_width_vect n v\ \pls_bound V b\ + assumes \\v. v \ V \ fixed_len_bseq n v\ \pls_bound V b\ shows \pls_bound (apply_pol n pol ` V) b\ using assms by (cases pol; simp add: inverted_bound) lemma apply_pol_bound_iff: - assumes \\v. v \ V \ fixed_width_vect n v\ + assumes \\v. v \ V \ fixed_len_bseq n v\ shows \pls_bound (apply_pol n pol ` V) b = pls_bound V b\ proof assume \pls_bound (apply_pol n pol ` V) b\ diff --git a/checker/verified/Sorting_Network_Bound.thy b/checker/verified/Sorting_Network_Bound.thy index 4d95cda..014e52a 100644 --- a/checker/verified/Sorting_Network_Bound.thy +++ b/checker/verified/Sorting_Network_Bound.thy @@ -2,44 +2,44 @@ theory Sorting_Network_Bound imports Main begin -text \Due to the 0-1-principle we're only concerned with Boolean vectors. While we're interested in -sorting vectors of a given fixed width, it is advantageous to represent them as a function from the -naturals to Boolens.\ +text \Due to the 0-1-principle we're only concerned with Boolean sequences. While we're interested +in sorting vectors of a given fixed width, it is advantageous to represent them as a function from +the naturals to Booleans.\ -type_synonym vect = \nat \ bool\ +type_synonym bseq = \nat \ bool\ -text \To represent vectors of a fixed width, we extend them with True to infinity. This way -monotonicity of a fixed width vector corresponds to monotonicity of our representation.\ +text \To represent Boolean sequences of a fixed length, we extend them with True to infinity. This +way monotonicity of a fixed length sequence corresponds to monotonicity of our representation.\ -definition fixed_width_vect :: \nat \ vect \ bool\ where - \fixed_width_vect n v = (\i \ n. v i = True)\ +definition fixed_len_bseq :: \nat \ bseq \ bool\ where + \fixed_len_bseq n x = (\i \ n. x i = True)\ text \A comparator is represented as an ordered pair of channel indices. Applying a comparator to a -vector will order the values of the two channels so that the channel corresponding to the first +sequence will order the values of the two channels so that the channel corresponding to the first index receives the smaller value.\ type_synonym cmp = \nat \ nat\ -definition apply_cmp :: \cmp \ vect \ vect\ where - \apply_cmp c v = ( - let (a, b) = c - in v( - a := min (v a) (v b), - b := max (v a) (v b) +definition apply_cmp :: \cmp \ bseq \ bseq\ where + \apply_cmp c x = ( + let (i, j) = c + in x( + i := min (x i) (x j), + j := max (x i) (x j) ) )\ -text \A lower size bound for a sorting network on a given set of input vectors is a number of -comparators so that any network that is able to sort every vector of the input set has at least that -number of comparators.\ +text \A lower size bound for a partial sorting network on a given set of input sequences is the +number of comparators required for any comparator network that is able to sort every sequence of the +given set.\ -definition lower_size_bound :: \vect set \ nat \ bool\ where - \lower_size_bound V b = (\cn. (\v \ V. mono (fold apply_cmp cn v)) \ length cn \ b)\ +definition partial_lower_size_bound :: \bseq set \ nat \ bool\ where + \partial_lower_size_bound X k = (\cn. (\x \ X. mono (fold apply_cmp cn x)) \ length cn \ k)\ -text \We are interested in lower size bounds for sorting networks that sort all vectors of a given - width.\ +text \A lower size bound for a sorting network on n channels is the same as a lower size bound for a +partial sorting network on all length n sequences.\ -definition lower_size_bound_for_width :: \nat \ nat \ bool\ where - \lower_size_bound_for_width w b = lower_size_bound {v. fixed_width_vect w v} b\ +definition lower_size_bound :: \nat \ nat \ bool\ where + \lower_size_bound n k = partial_lower_size_bound {x. fixed_len_bseq n x} k\ end \ No newline at end of file