# HG changeset patch # User haftmann # Date 1277731946 -7200 # Node ID 625bc011768a817a0bd2ff8b10283eec023533d4 # Parent 1840dc0265da89461a605b40e8f51821a4a9cf69 put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem diff -r 1840dc0265da -r 625bc011768a src/HOL/List.thy --- a/src/HOL/List.thy Mon Jun 28 15:32:25 2010 +0200 +++ b/src/HOL/List.thy Mon Jun 28 15:32:26 2010 +0200 @@ -2352,6 +2352,22 @@ case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) qed +lemma rev_foldl_cons [code]: + "rev xs = foldl (\xs x. x # xs) [] xs" +proof (induct xs) + case Nil then show ?case by simp +next + case Cons + { + fix x xs ys + have "foldl (\xs x. x # xs) ys xs @ [x] + = foldl (\xs x. x # xs) (ys @ [x]) xs" + by (induct xs arbitrary: ys) auto + } + note aux = this + show ?case by (induct xs) (auto simp add: Cons aux) +qed + text{* The ``First Duality Theorem'' in Bird \& Wadler: *} @@ -2509,120 +2525,6 @@ by (simp add: sup_commute) -subsubsection {* List summation: @{const listsum} and @{text"\"}*} - -lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" -by (induct xs) (simp_all add:add_assoc) - -lemma listsum_rev [simp]: - fixes xs :: "'a\comm_monoid_add list" - shows "listsum (rev xs) = listsum xs" -by (induct xs) (simp_all add:add_ac) - -lemma listsum_map_remove1: -fixes f :: "'a \ ('b::comm_monoid_add)" -shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))" -by (induct xs)(auto simp add:add_ac) - -lemma list_size_conv_listsum: - "list_size f xs = listsum (map f xs) + size xs" -by(induct xs) auto - -lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" -by (induct xs) auto - -lemma length_concat: "length (concat xss) = listsum (map length xss)" -by (induct xss) simp_all - -lemma listsum_map_filter: - fixes f :: "'a \ 'b \ comm_monoid_add" - assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" - shows "listsum (map f (filter P xs)) = listsum (map f xs)" -using assms by (induct xs) auto - -text{* For efficient code generation --- - @{const listsum} is not tail recursive but @{const foldl} is. *} -lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" -by(simp add:listsum_foldr foldl_foldr1) - -lemma distinct_listsum_conv_Setsum: - "distinct xs \ listsum xs = Setsum(set xs)" -by (induct xs) simp_all - -lemma listsum_eq_0_nat_iff_nat[simp]: - "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" -by(simp add: listsum) - -lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" -apply(induct ns arbitrary: k) - apply simp -apply(fastsimp simp add:nth_Cons split: nat.split) -done - -lemma listsum_update_nat: "k - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" -apply(induct ns arbitrary:k) - apply (auto split:nat.split) -apply(drule elem_le_listsum_nat) -apply arith -done - -text{* Some syntactic sugar for summing a function over a list: *} - -syntax - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) -syntax (xsymbols) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) -syntax (HTML output) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) - -translations -- {* Beware of argument permutation! *} - "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" - "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" - -lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" - by (induct xs) (simp_all add: left_distrib) - -lemma listsum_0 [simp]: "(\x\xs. 0) = 0" - by (induct xs) (simp_all add: left_distrib) - -text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} -lemma uminus_listsum_map: - fixes f :: "'a \ 'b\ab_group_add" - shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" -by (induct xs) simp_all - -lemma listsum_addf: - fixes f g :: "'a \ 'b::comm_monoid_add" - shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" -by (induct xs) (simp_all add: algebra_simps) - -lemma listsum_subtractf: - fixes f g :: "'a \ 'b::ab_group_add" - shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" -by (induct xs) simp_all - -lemma listsum_const_mult: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. c * f x) = c * (\x\xs. f x)" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_mult_const: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. f x * c) = (\x\xs. f x) * c" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_abs: - fixes xs :: "'a::ordered_ab_group_add_abs list" - shows "\listsum xs\ \ listsum (map abs xs)" -by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) - -lemma listsum_mono: - fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" - shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" -by (induct xs, simp, simp add: add_mono) - - subsubsection {* @{text upt} *} lemma upt_rec[code]: "[i.."}*} + +lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" +by (induct xs) (simp_all add:add_assoc) + +lemma listsum_rev [simp]: + fixes xs :: "'a\comm_monoid_add list" + shows "listsum (rev xs) = listsum xs" +by (induct xs) (simp_all add:add_ac) + +lemma listsum_map_remove1: +fixes f :: "'a \ ('b::comm_monoid_add)" +shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))" +by (induct xs)(auto simp add:add_ac) + +lemma list_size_conv_listsum: + "list_size f xs = listsum (map f xs) + size xs" +by(induct xs) auto + +lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" +by (induct xs) auto + +lemma length_concat: "length (concat xss) = listsum (map length xss)" +by (induct xss) simp_all + +lemma listsum_map_filter: + fixes f :: "'a \ 'b \ comm_monoid_add" + assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" + shows "listsum (map f (filter P xs)) = listsum (map f xs)" +using assms by (induct xs) auto + +text{* For efficient code generation --- + @{const listsum} is not tail recursive but @{const foldl} is. *} +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" +by(simp add:listsum_foldr foldl_foldr1) + +lemma distinct_listsum_conv_Setsum: + "distinct xs \ listsum xs = Setsum(set xs)" +by (induct xs) simp_all + +lemma listsum_eq_0_nat_iff_nat[simp]: + "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" +by(simp add: listsum) + +lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" +apply(induct ns arbitrary: k) + apply simp +apply(fastsimp simp add:nth_Cons split: nat.split) +done + +lemma listsum_update_nat: "k + listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" +apply(induct ns arbitrary:k) + apply (auto split:nat.split) +apply(drule elem_le_listsum_nat) +apply arith +done + +text{* Some syntactic sugar for summing a function over a list: *} + +syntax + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) +syntax (xsymbols) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) +syntax (HTML output) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) + +translations -- {* Beware of argument permutation! *} + "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" + "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" + +lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" + by (induct xs) (simp_all add: left_distrib) + +lemma listsum_0 [simp]: "(\x\xs. 0) = 0" + by (induct xs) (simp_all add: left_distrib) + +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} +lemma uminus_listsum_map: + fixes f :: "'a \ 'b\ab_group_add" + shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" +by (induct xs) simp_all + +lemma listsum_addf: + fixes f g :: "'a \ 'b::comm_monoid_add" + shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" +by (induct xs) (simp_all add: algebra_simps) + +lemma listsum_subtractf: + fixes f g :: "'a \ 'b::ab_group_add" + shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" +by (induct xs) simp_all + +lemma listsum_const_mult: + fixes f :: "'a \ 'b::semiring_0" + shows "(\x\xs. c * f x) = c * (\x\xs. f x)" +by (induct xs, simp_all add: algebra_simps) + +lemma listsum_mult_const: + fixes f :: "'a \ 'b::semiring_0" + shows "(\x\xs. f x * c) = (\x\xs. f x) * c" +by (induct xs, simp_all add: algebra_simps) + +lemma listsum_abs: + fixes xs :: "'a::ordered_ab_group_add_abs list" + shows "\listsum xs\ \ listsum (map abs xs)" +by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) + +lemma listsum_mono: + fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" + shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" +by (induct xs, simp, simp add: add_mono) + +lemma listsum_distinct_conv_setsum_set: + "distinct xs \ listsum (map f xs) = setsum f (set xs)" + by (induct xs) simp_all + +lemma interv_listsum_conv_setsum_set_nat: + "listsum (map f [m.. i = 0 ..< length xs. xs ! i)" + using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) + + subsubsection {* @{const insert} *} lemma in_set_insert [simp]: @@ -4513,9 +4546,266 @@ *) -subsection {* Code generator *} - -subsubsection {* Setup *} +subsection {* Code generation *} + +subsubsection {* Counterparts for set-related operations *} + +definition member :: "'a list \ 'a \ bool" where + [code_post]: "member xs x \ x \ set xs" + +text {* + Only use @{text member} for generating executable code. Otherwise use + @{prop "x \ set xs"} instead --- it is much easier to reason about. +*} + +lemma member_set: + "member = set" + by (simp add: expand_fun_eq member_def mem_def) + +lemma member_rec [code]: + "member (x # xs) y \ x = y \ member xs y" + "member [] y \ False" + by (auto simp add: member_def) + +lemma in_set_member [code_unfold]: + "x \ set xs \ member xs x" + by (simp add: member_def) + +declare INFI_def [code_unfold] +declare SUPR_def [code_unfold] + +declare set_map [symmetric, code_unfold] + +definition list_all :: "('a \ bool) \ 'a list \ bool" where + list_all_iff [code_post]: "list_all P xs \ (\x \ set xs. P x)" + +definition list_ex :: "('a \ bool) \ 'a list \ bool" where + list_ex_iff [code_post]: "list_ex P xs \ (\x \ set xs. P x)" + +text {* + Usually you should prefer @{text "\x\set xs"} and @{text "\x\set xs"} + over @{const list_all} and @{const list_ex} in specifications. +*} + +lemma list_all_simps [simp, code]: + "list_all P (x # xs) \ P x \ list_all P xs" + "list_all P [] \ True" + by (simp_all add: list_all_iff) + +lemma list_ex_simps [simp, code]: + "list_ex P (x # xs) \ P x \ list_ex P xs" + "list_ex P [] \ False" + by (simp_all add: list_ex_iff) + +lemma Ball_set_list_all [code_unfold]: + "Ball (set xs) P \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set_list_ex [code_unfold]: + "Bex (set xs) P \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma list_all_append [simp]: + "list_all P (xs @ ys) \ list_all P xs \ list_all P ys" + by (auto simp add: list_all_iff) + +lemma list_ex_append [simp]: + "list_ex P (xs @ ys) \ list_ex P xs \ list_ex P ys" + by (auto simp add: list_ex_iff) + +lemma list_all_rev [simp]: + "list_all P (rev xs) \ list_all P xs" + by (simp add: list_all_iff) + +lemma list_ex_rev [simp]: + "list_ex P (rev xs) \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma list_all_length: + "list_all P xs \ (\n < length xs. P (xs ! n))" + by (auto simp add: list_all_iff set_conv_nth) + +lemma list_ex_length: + "list_ex P xs \ (\n < length xs. P (xs ! n))" + by (auto simp add: list_ex_iff set_conv_nth) + +lemma list_all_cong [fundef_cong]: + "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_all f xs = list_all g ys" + by (simp add: list_all_iff) + +lemma list_any_cong [fundef_cong]: + "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_ex f xs = list_ex g ys" + by (simp add: list_ex_iff) + +text {* Bounded quantification and summation over nats. *} + +lemma atMost_upto [code_unfold]: + "{..n} = set [0..mnat. P m) \ (\m \ {0..mnat. P m) \ (\m \ {0..m\n\nat. P m) \ (\m \ {0..n}. P m)" + by auto + +lemma ex_nat_less [code_unfold]: + "(\m\n\nat. P m) \ (\m \ {0..n}. P m)" + by auto + +lemma setsum_set_upt_conv_listsum_nat [code_unfold]: + "setsum f (set [m.. bool" where + [code_post]: "null xs \ xs = []" + +text {* + Efficient emptyness check is implemented by @{const null}. +*} + +lemma null_rec [code]: + "null (x # xs) \ False" + "null [] \ True" + by (simp_all add: null_def) + +lemma eq_Nil_null [code_unfold]: + "xs = [] \ null xs" + by (simp add: null_def) + +lemma equal_Nil_null [code_unfold]: + "eq_class.eq xs [] \ null xs" + by (simp add: eq eq_Nil_null) + +definition maps :: "('a \ 'b list) \ 'a list \ 'b list" where + [code_post]: "maps f xs = concat (map f xs)" + +definition map_filter :: "('a \ 'b option) \ 'a list \ 'b list" where + [code_post]: "map_filter f xs = map (the \ f) (filter (\x. f x \ None) xs)" + +text {* + Operations @{const maps} and @{const map_filter} avoid + intermediate lists on execution -- do not use for proving. +*} + +lemma maps_simps [code]: + "maps f (x # xs) = f x @ maps f xs" + "maps f [] = []" + by (simp_all add: maps_def) + +lemma map_filter_simps [code]: + "map_filter f (x # xs) = (case f x of None \ map_filter f xs | Some y \ y # map_filter f xs)" + "map_filter f [] = []" + by (simp_all add: map_filter_def split: option.split) + +lemma concat_map_maps [code_unfold]: + "concat (map f xs) = maps f xs" + by (simp add: maps_def) + +lemma map_filter_map_filter [code_unfold]: + "map f (filter P xs) = map_filter (\x. if P x then Some (f x) else None) xs" + by (simp add: map_filter_def) + +text {* Optimized code for @{text"\i\{a..b::int}"} and @{text"\n:{a.."}. *} + +definition all_interval_nat :: "(nat \ bool) \ nat \ nat \ bool" where + "all_interval_nat P i j \ (\n \ {i.. i \ j \ P i \ all_interval_nat P (Suc i) j" +proof - + have *: "\n. P i \ \n\{Suc i.. i \ n \ n < j \ P n" + proof - + fix n + assume "P i" "\n\{Suc i.. n" "n < j" + then show "P n" by (cases "n = i") simp_all + qed + show ?thesis by (auto simp add: all_interval_nat_def intro: *) +qed + +lemma list_all_iff_all_interval_nat [code_unfold]: + "list_all P [i.. all_interval_nat P i j" + by (simp add: list_all_iff all_interval_nat_def) + +lemma list_ex_iff_not_all_inverval_nat [code_unfold]: + "list_ex P [i.. \ (all_interval_nat (Not \ P) i j)" + by (simp add: list_ex_iff all_interval_nat_def) + +definition all_interval_int :: "(int \ bool) \ int \ int \ bool" where + "all_interval_int P i j \ (\k \ {i..j}. P k)" + +lemma [code]: + "all_interval_int P i j \ i > j \ P i \ all_interval_int P (i + 1) j" +proof - + have *: "\k. P i \ \k\{i+1..j}. P k \ i \ k \ k \ j \ P k" + proof - + fix k + assume "P i" "\k\{i+1..j}. P k" "i \ k" "k \ j" + then show "P k" by (cases "k = i") simp_all + qed + show ?thesis by (auto simp add: all_interval_int_def intro: *) +qed + +lemma list_all_iff_all_interval_int [code_unfold]: + "list_all P [i..j] \ all_interval_int P i j" + by (simp add: list_all_iff all_interval_int_def) + +lemma list_ex_iff_not_all_inverval_int [code_unfold]: + "list_ex P [i..j] \ \ (all_interval_int (Not \ P) i j)" + by (simp add: list_ex_iff all_interval_int_def) + +hide_const (open) member null maps map_filter all_interval_nat all_interval_int + + +subsubsection {* Pretty lists *} use "Tools/list_code.ML" @@ -4578,374 +4868,6 @@ *} -subsubsection {* Generation of efficient code *} - -definition member :: "'a list \ 'a \ bool" where - mem_iff [code_post]: "member xs x \ x \ set xs" - -primrec - null:: "'a list \ bool" -where - "null [] = True" - | "null (x#xs) = False" - -primrec - list_inter :: "'a list \ 'a list \ 'a list" -where - "list_inter [] bs = []" - | "list_inter (a#as) bs = - (if a \ set bs then a # list_inter as bs else list_inter as bs)" - -primrec - list_all :: "('a \ bool) \ ('a list \ bool)" -where - "list_all P [] = True" - | "list_all P (x#xs) = (P x \ list_all P xs)" - -primrec - list_ex :: "('a \ bool) \ 'a list \ bool" -where - "list_ex P [] = False" - | "list_ex P (x#xs) = (P x \ list_ex P xs)" - -primrec - filtermap :: "('a \ 'b option) \ 'a list \ 'b list" -where - "filtermap f [] = []" - | "filtermap f (x#xs) = - (case f x of None \ filtermap f xs - | Some y \ y # filtermap f xs)" - -primrec - map_filter :: "('a \ 'b) \ ('a \ bool) \ 'a list \ 'b list" -where - "map_filter f P [] = []" - | "map_filter f P (x#xs) = - (if P x then f x # map_filter f P xs else map_filter f P xs)" - -primrec - length_unique :: "'a list \ nat" -where - "length_unique [] = 0" - | "length_unique (x#xs) = - (if x \ set xs then length_unique xs else Suc (length_unique xs))" - -primrec - concat_map :: "('a => 'b list) => 'a list => 'b list" -where - "concat_map f [] = []" - | "concat_map f (x#xs) = f x @ concat_map f xs" - -text {* - Only use @{text member} for generating executable code. Otherwise use - @{prop "x : set xs"} instead --- it is much easier to reason about. - The same is true for @{const list_all} and @{const list_ex}: write - @{text "\x\set xs"} and @{text "\x\set xs"} instead because the HOL - quantifiers are aleady known to the automatic provers. In fact, the - declarations in the code subsection make sure that @{text "\"}, - @{text "\x\set xs"} and @{text "\x\set xs"} are implemented - efficiently. - - Efficient emptyness check is implemented by @{const null}. - - The functions @{const filtermap} and @{const map_filter} are just - there to generate efficient code. Do not use - them for modelling and proving. -*} - -lemma rev_foldl_cons [code]: - "rev xs = foldl (\xs x. x # xs) [] xs" -proof (induct xs) - case Nil then show ?case by simp -next - case Cons - { - fix x xs ys - have "foldl (\xs x. x # xs) ys xs @ [x] - = foldl (\xs x. x # xs) (ys @ [x]) xs" - by (induct xs arbitrary: ys) auto - } - note aux = this - show ?case by (induct xs) (auto simp add: Cons aux) -qed - -lemmas in_set_code [code_unfold] = mem_iff [symmetric] - -lemma member_simps [simp, code]: - "member (x # xs) y \ x = y \ member xs y" - "member [] y \ False" - by (auto simp add: mem_iff) - -lemma member_set: - "member = set" - by (simp add: expand_fun_eq mem_iff mem_def) - -abbreviation (input) mem :: "'a \ 'a list \ bool" (infixl "mem" 55) where - "x mem xs \ member xs x" -- "for backward compatibility" - -lemma empty_null: - "xs = [] \ null xs" -by (cases xs) simp_all - -lemma [code_unfold]: - "eq_class.eq xs [] \ null xs" -by (simp add: eq empty_null) - -lemmas null_empty [code_post] = - empty_null [symmetric] - -lemma list_inter_conv: - "set (list_inter xs ys) = set xs \ set ys" -by (induct xs) auto - -lemma list_all_iff [code_post]: - "list_all P xs \ (\x \ set xs. P x)" -by (induct xs) auto - -lemmas list_ball_code [code_unfold] = list_all_iff [symmetric] - -lemma list_all_append [simp]: - "list_all P (xs @ ys) \ (list_all P xs \ list_all P ys)" -by (induct xs) auto - -lemma list_all_rev [simp]: - "list_all P (rev xs) \ list_all P xs" -by (simp add: list_all_iff) - -lemma list_all_length: - "list_all P xs \ (\n < length xs. P (xs ! n))" -unfolding list_all_iff by (auto intro: all_nth_imp_all_set) - -lemma list_all_cong[fundef_cong]: - "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_all f xs = list_all g ys" -by (simp add: list_all_iff) - -lemma list_ex_iff [code_post]: - "list_ex P xs \ (\x \ set xs. P x)" -by (induct xs) simp_all - -lemmas list_bex_code [code_unfold] = - list_ex_iff [symmetric] - -lemma list_ex_length: - "list_ex P xs \ (\n < length xs. P (xs ! n))" -unfolding list_ex_iff set_conv_nth by auto - -lemma list_ex_cong[fundef_cong]: - "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_ex f xs = list_ex g ys" -by (simp add: list_ex_iff) - -lemma filtermap_conv: - "filtermap f xs = map (\x. the (f x)) (filter (\x. f x \ None) xs)" -by (induct xs) (simp_all split: option.split) - -lemma map_filter_conv [simp]: - "map_filter f P xs = map f (filter P xs)" -by (induct xs) auto - -lemma length_remdups_length_unique [code_unfold]: - "length (remdups xs) = length_unique xs" -by (induct xs) simp_all - -lemma concat_map_code[code_unfold]: - "concat(map f xs) = concat_map f xs" -by (induct xs) simp_all - -declare INFI_def [code_unfold] -declare SUPR_def [code_unfold] - -declare set_map [symmetric, code_unfold] - -hide_const (open) length_unique - - -text {* Code for bounded quantification and summation over nats. *} - -lemma atMost_upto [code_unfold]: - "{..n} = set [0..mnat. P m) \ (\m \ {0..mnat. P m) \ (\m \ {0..m\n\nat. P m) \ (\m \ {0..n}. P m)" -by auto - -lemma ex_nat_less [code_unfold]: - "(\m\n\nat. P m) \ (\m \ {0..n}. P m)" -by auto - -lemma setsum_set_distinct_conv_listsum: - "distinct xs \ setsum f (set xs) = listsum (map f xs)" -by (induct xs) simp_all - -lemma setsum_set_upt_conv_listsum [code_unfold]: - "setsum f (set [m.. i = 0 ..< length xs. xs ! i)" -using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"] -by (simp add: map_nth) - -text {* Code for summation over ints. *} - -lemma greaterThanLessThan_upto [code_unfold]: - "{i<..i\{a..b::int}"} and @{text"\n:{a.."}. *} - -function all_from_to_nat :: "(nat \ bool) \ nat \ nat \ bool" where -"all_from_to_nat P i j = - (if i < j then if P i then all_from_to_nat P (i+1) j else False - else True)" -by auto -termination -by (relation "measure(%(P,i,j). j - i)") auto - -declare all_from_to_nat.simps[simp del] - -lemma all_from_to_nat_iff_ball: - "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)" -proof(induct P i j rule:all_from_to_nat.induct) - case (1 P i j) - let ?yes = "i < j & P i" - show ?case - proof (cases) - assume ?yes - hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)" - by(simp add: all_from_to_nat.simps) - also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp - also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R") - proof - assume L: ?L - show ?R - proof clarify - fix n assume n: "n : {i.. bool) \ int \ int \ bool" where -"all_from_to_int P i j = - (if i <= j then if P i then all_from_to_int P (i+1) j else False - else True)" -by auto -termination -by (relation "measure(%(P,i,j). nat(j - i + 1))") auto - -declare all_from_to_int.simps[simp del] - -lemma all_from_to_int_iff_ball: - "all_from_to_int P i j = (ALL n : {i .. j}. P n)" -proof(induct P i j rule:all_from_to_int.induct) - case (1 P i j) - let ?yes = "i <= j & P i" - show ?case - proof (cases) - assume ?yes - hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)" - by(simp add: all_from_to_int.simps) - also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp - also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R") - proof - assume L: ?L - show ?R - proof clarify - fix n assume n: "n : {i..j}" - show "P n" - proof cases - assume "n = i" thus "P n" using L by simp - next - assume "n ~= i" - hence "i+1 <= n" using n by auto - thus "P n" using L n by simp - qed - qed - next - assume R: ?R thus ?L using `?yes` 1 by auto - qed - finally show ?thesis . - next - assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps) - qed -qed - -lemma list_all_iff_all_from_to_int[code_unfold]: - "list_all P [i..j] = all_from_to_int P i j" -by(simp add: all_from_to_int_iff_ball list_all_iff) - -lemma list_ex_iff_not_all_from_to_not_int[code_unfold]: - "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)" -by(simp add: all_from_to_int_iff_ball list_ex_iff) - - subsubsection {* Use convenient predefined operations *} code_const "op @" @@ -4963,12 +4885,18 @@ code_const concat (Haskell "concat") +code_const List.maps + (Haskell "concatMap") + code_const rev (Haskell "reverse") code_const zip (Haskell "zip") +code_const List.null + (Haskell "null") + code_const takeWhile (Haskell "takeWhile") @@ -4981,4 +4909,10 @@ code_const last (Haskell "last") +code_const list_all + (Haskell "all") + +code_const list_ex + (Haskell "any") + end