# HG changeset patch # User haftmann # Date 1748584097 -7200 # Node ID 5d5bd00485337d3a2defbb7339f191ebc69ada2c # Parent 92afc125f7cde3c3e7f5da032f408e9b8eb74b83 tuned theory structure diff -r 92afc125f7cd -r 5d5bd0048533 src/HOL/List.thy --- a/src/HOL/List.thy Fri May 30 07:47:03 2025 +0200 +++ b/src/HOL/List.thy Fri May 30 07:48:17 2025 +0200 @@ -7808,29 +7808,10 @@ subsection \Code generation\ -text\Optional tail recursive version of \<^const>\map\. Can avoid -stack overflow in some target languages.\ - -fun map_tailrec_rev :: "('a \ 'b) \ 'a list \ 'b list \ 'b list" where - "map_tailrec_rev f [] bs = bs" | - "map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)" - -lemma map_tailrec_rev: - "map_tailrec_rev f as bs = rev(map f as) @ bs" - by(induction as arbitrary: bs) simp_all - -definition map_tailrec :: "('a \ 'b) \ 'a list \ 'b list" where - "map_tailrec f as = rev (map_tailrec_rev f as [])" - -text\Code equation:\ -lemma map_eq_map_tailrec: "map = map_tailrec" - by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev) - - subsubsection \Counterparts for set-related operations\ -definition member :: "'a list \ 'a \ bool" where -[code_abbrev]: "member xs x \ x \ set xs" +definition member :: \'a list \ 'a \ bool\ + where [code_abbrev]: \member xs x \ x \ set xs\ text \ Use \member\ only for generating executable code. Otherwise use @@ -7838,21 +7819,21 @@ \ lemma member_rec [code]: - "member (x # xs) y \ x = y \ member xs y" - "member [] y \ False" + \member (x # xs) y \ x = y \ member xs y\ + \member [] y \ False\ by (auto simp add: member_def) -lemma in_set_member (* FIXME delete candidate *): - "x \ set xs \ member xs x" - by (simp add: member_def) - -lemmas list_all_iff [code_abbrev] = fun_cong[OF list.pred_set] - -definition list_ex :: "('a \ bool) \ 'a list \ bool" where -list_ex_iff [code_abbrev]: "list_ex P xs \ Bex (set xs) P" - -definition list_ex1 :: "('a \ bool) \ 'a list \ bool" where -list_ex1_iff [code_abbrev]: "list_ex1 P xs \ Set.can_select P (set xs)" +hide_const (open) member + +lemma list_all_iff [code_abbrev]: + \list_all P xs \ Ball (set xs) P\ + by (simp add: list.pred_set) + +definition list_ex :: \('a \ bool) \ 'a list \ bool\ + where list_ex_iff [code_abbrev]: \list_ex P xs \ Bex (set xs) P\ + +definition list_ex1 :: \('a \ bool) \ 'a list \ bool\ + where list_ex1_iff [code_abbrev]: \list_ex1 P xs \ Set.can_select P (set xs)\ text \ Usually you should prefer \\x\set xs\, \\x\set xs\ @@ -7861,108 +7842,103 @@ \ lemma list_all_simps [code]: - "list_all P (x # xs) \ P x \ list_all P xs" - "list_all P [] \ True" + \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" + \list_ex P (x # xs) \ P x \ list_ex P xs\ + \list_ex P [] \ False\ by (simp_all add: list_ex_iff) lemma list_ex1_simps [simp, code]: - "list_ex1 P [] = False" - "list_ex1 P (x # xs) = (if P x then list_all (\y. \ P y \ x = y) xs else list_ex1 P xs)" + \list_ex1 P [] = False\ + \list_ex1 P (x # xs) = (if P x then list_all (\y. \ P y \ x = y) xs else list_ex1 P xs)\ by (auto simp add: list_ex1_iff list_all_iff) -lemma Ball_set_list_all: (* FIXME delete candidate *) - "Ball (set xs) P \ list_all P xs" - by (simp add: list_all_iff) - -lemma Bex_set_list_ex: (* FIXME delete candidate *) - "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" + \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" + \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" + \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" + \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))" + \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))" + \list_ex P xs \ (\n < length xs. P (xs ! n))\ by (auto simp add: list_ex_iff set_conv_nth) -lemmas list_all_cong [fundef_cong] = list.pred_cong +lemma list_all_cong [fundef_cong]: + \list_all f xs = list_all g ys\ + if \xs = ys\ \(\x. x \ set ys \ f x = g x)\ + using that by (rule list.pred_cong) 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 can_select_set_list_ex1 [code]: - "Set.can_select P (set A) = list_ex1 P A" - by (simp add: list_ex1_iff Set.can_select_iff) + \list_ex f xs = list_ex g ys\ + if \xs = ys\ \(\x. x \ set ys \ f x = g x)\ + using that by (simp add: list_ex_iff) text \Executable checks for relations on sets\ -definition listrel1p :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" where -"listrel1p r xs ys = ((xs, ys) \ listrel1 {(x, y). r x y})" +definition listrel1p :: \('a \ 'a \ bool) \ 'a list \ 'a list \ bool\ + where \listrel1p r xs ys \ (xs, ys) \ listrel1 {(x, y). r x y}\ lemma [code_unfold]: - "(xs, ys) \ listrel1 r = listrel1p (\x y. (x, y) \ r) xs ys" -unfolding listrel1p_def by auto + \(xs, ys) \ listrel1 r \ listrel1p (\x y. (x, y) \ r) xs ys\ + by (simp add: listrel1p_def) lemma [code]: - "listrel1p r [] xs = False" - "listrel1p r xs [] = False" - "listrel1p r (x # xs) (y # ys) \ - r x y \ xs = ys \ x = y \ listrel1p r xs ys" -by (simp add: listrel1p_def)+ - -definition - lexordp :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" where - "lexordp r xs ys = ((xs, ys) \ lexord {(x, y). r x y})" + \listrel1p r [] xs \ False\ + \listrel1p r xs [] \ False\ + \listrel1p r (x # xs) (y # ys) \ + r x y \ xs = ys \ x = y \ listrel1p r xs ys\ + by (simp_all add: listrel1p_def) + +definition lexordp :: \('a \ 'a \ bool) \ 'a list \ 'a list \ bool\ + where \lexordp r xs ys \ (xs, ys) \ lexord {(x, y). r x y}\ lemma [code_unfold]: - "(xs, ys) \ lexord r = lexordp (\x y. (x, y) \ r) xs ys" -unfolding lexordp_def by auto + \(xs, ys) \ lexord r = lexordp (\x y. (x, y) \ r) xs ys\ + by (simp add: lexordp_def) lemma [code]: - "lexordp r xs [] = False" - "lexordp r [] (y#ys) = True" - "lexordp r (x # xs) (y # ys) = (r x y \ (x = y \ lexordp r xs ys))" -unfolding lexordp_def by auto - -text \Bounded quantification and summation over nats.\ + \lexordp r xs [] \ False\ + \lexordp r [] (y # ys) \ True\ + \lexordp r (x # xs) (y # ys) \ + r x y \ (x = y \ lexordp r xs ys)\ + by (simp_all add: add: lexordp_def) + + +text \Intervals over \<^typ>\nat\.\ lemma atMost_upto [code_unfold]: - "{..n} = set [0..{..n} = set [0.. by auto lemma atLeast_upt [code_unfold]: - "{..{.. by auto lemma greaterThanLessThan_upt [code_unfold]: - "{n<..{n<.. by auto -lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric] +lemma atLeastLessThan_upt [code_unfold]: + \{i.. + by auto lemma greaterThanAtMost_upt [code_unfold]: "{n<..m} = set [Suc n..Optimized code for \\n:{a.. and similiarly for \\\.\ + +definition all_interval_nat :: \(nat \ bool) \ nat \ nat \ bool\ + where \all_interval_nat P i j \ (\n \ {i.. + +lemma [code]: + \all_interval_nat P i j \ 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\ + using le_less_Suc_eq by fastforce + then show ?thesis + by (auto simp add: all_interval_nat_def) +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) + +hide_const (open) all_interval_nat + lemma all_nat_less_eq [code_unfold]: "(\m (\m \ {0..m\n::nat. P m) \ (\m \ {0..n}. P m)" by auto -text\Bounded \LEAST\ operator:\ - -definition "Bleast S P = (LEAST x. x \ S \ P x)" - -definition "abort_Bleast S P = (LEAST x. x \ S \ P x)" + +text \Intervals over \<^typ>\int\.\ + +lemma greaterThanLessThan_upto [code_unfold]: + \{i<.. + by auto + +lemma atLeastLessThan_upto [code_unfold]: + \{i.. + by auto + +lemma greaterThanAtMost_upto [code_unfold]: + \{i<..j::int} = set [i+1..j]\ + by auto + +lemma atLeastAtMost_upto [code_unfold]: + \{i..j} = set [i..j]\ + by auto + + +text \Optimized code for \\i\{a..b::int}\ and similiarly for \\\.\ + +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\ + by (smt (verit, best) atLeastAtMost_iff) + 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) all_interval_int + + +text \Bounded \LEAST\ operator.\ + +definition Bleast :: \'a::ord set \ ('a \ bool) \ 'a\ + where \Bleast S P = (LEAST x. x \ S \ P x)\ + +declare Bleast_def [symmetric, code_unfold] + +definition abort_Bleast :: \'a::ord set \ ('a \ bool) \ 'a\ + where \abort_Bleast S P = (LEAST x. x \ S \ P x)\ declare [[code abort: abort_Bleast]] lemma Bleast_code [code]: - "Bleast (set xs) P = (case filter P (sort xs) of - x#xs \ x | - [] \ abort_Bleast (set xs) P)" + \Bleast (set xs) P = (case filter P (sort xs) of + x # xs \ x | + [] \ abort_Bleast (set xs) P)\ proof (cases "filter P (sort xs)") case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def) next @@ -8017,134 +8067,223 @@ thus ?thesis using Cons by (simp add: Bleast_def) qed -declare Bleast_def[symmetric, code_unfold] - -text \Summation over ints.\ - -lemma greaterThanLessThan_upto [code_unfold]: - "{i<..Optimizing by rewriting\ - -definition null :: "'a list \ bool" where - [code_abbrev]: "null xs \ xs = []" + +subsubsection \Special implementations\ + +text \ + Optional tail recursive version of \<^const>\map\. Can avoid + stack overflow in some target languages. Do not use for proving. +\ + +fun map_tailrec_rev :: \('a \ 'b) \ 'a list \ 'b list \ 'b list\ + where + \map_tailrec_rev f [] bs = bs\ + | \map_tailrec_rev f (a # as) bs = map_tailrec_rev f as (f a # bs)\ + +lemma map_tailrec_rev: + \map_tailrec_rev f as bs = rev(map f as) @ bs\ + by (induction as arbitrary: bs) simp_all + +definition map_tailrec :: \('a \ 'b) \ 'a list \ 'b list\ + where \map_tailrec f as = rev (map_tailrec_rev f as [])\ + +text\Code equation:\ +lemma map_eq_map_tailrec: + \map = map_tailrec\ + by (simp add: fun_eq_iff map_tailrec_def map_tailrec_rev) + +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 \ + Operation \<^const>\map_filter\ avoids + intermediate lists on execution -- do not use for proving. +\ + +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 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) + +hide_const (open) map_filter + + +subsubsection \Operations for optimization and efficiency\ + +definition null :: \'a list \ bool\ + where [code_abbrev]: \null xs \ xs = []\ text \ Efficient emptyness check is implemented by \<^const>\null\. \ lemma null_rec [code]: - "null (x # xs) \ False" - "null [] \ True" + \null (x # xs) \ False\ + \null [] \ True\ by (simp_all add: null_def) -lemma eq_Nil_null: (* FIXME delete candidate *) - "xs = [] \ null xs" - by (simp add: null_def) - lemma equal_Nil_null [code_unfold]: - "HOL.equal xs [] \ null xs" - "HOL.equal [] = null" + \HOL.equal xs [] \ null xs\ + \HOL.equal [] = null\ by (auto simp add: equal null_def) -definition maps :: "('a \ 'b list) \ 'a list \ 'b list" where - [code_abbrev]: "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)" +hide_const (open) null + + +text \optimized code (tail-recursive) for \<^term>\length\\ + +definition gen_length :: \nat \ 'a list \ nat\ + where \gen_length n xs = n + length xs\ + +lemma gen_length_code [code]: + \gen_length n [] = n\ + \gen_length n (x # xs) = gen_length (Suc n) xs\ + by (simp_all add: gen_length_def) + +lemma length_code [code]: + \length = gen_length 0\ + by (simp add: gen_length_def fun_eq_iff) + +hide_const (open) gen_length + + +definition maps :: \('a \ 'b list) \ 'a list \ 'b list\ + where [code_abbrev]: \maps f xs = concat (map f xs)\ + text \ - Operations \<^const>\maps\ and \<^const>\map_filter\ avoid + Operation \<^const>\maps\ avoids intermediate lists on execution -- do not use for proving. \ lemma maps_simps [code]: - "maps f (x # xs) = f x @ maps f xs" - "maps f [] = []" + \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: (* FIXME delete candidate *) - "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 \\i\{a..b::int}\ and \\n:{a.. -and similiarly for \\\.\ - -definition all_interval_nat :: "(nat \ bool) \ nat \ nat \ bool" where - "all_interval_nat P i j \ (\n \ {i..Implementation of sets by lists\ + +lemma is_empty_set [code]: + "Set.is_empty (set xs) \ List.null xs" + by (simp add: null_def) + +lemma empty_set [code]: + "{} = set []" + by simp + +lemma UNIV_coset [code]: + "UNIV = List.coset []" + by simp + +lemma compl_set [code]: + "- set xs = List.coset xs" + by simp + +lemma compl_coset [code]: + "- List.coset xs = set xs" + by simp lemma [code]: - "all_interval_nat P i j \ 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" - using le_less_Suc_eq by fastforce - 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)" + "x \ set xs \ List.member xs x" + "x \ List.coset xs \ \ List.member xs x" + by (simp_all add: member_def) + +lemma insert_code [code]: + "insert x (set xs) = set (List.insert x xs)" + "insert x (List.coset xs) = List.coset (removeAll x xs)" + by simp_all + +lemma remove_code [code]: + "Set.remove x (set xs) = set (removeAll x xs)" + "Set.remove x (List.coset xs) = List.coset (List.insert x xs)" + by (simp_all add: set_eq_iff ac_simps) + +lemma filter_set [code]: + "Set.filter P (set xs) = set (filter P xs)" + by auto + +lemma image_set [code]: + "image f (set xs) = set (map f xs)" + by simp + +lemma subset_code [code]: + "set xs \ B \ (\x\set xs. x \ B)" + "A \ List.coset ys \ (\y\set ys. y \ A)" + "List.coset [] \ set [] \ False" + by auto + +text \A frequent case -- avoid intermediate sets\ +lemma [code_unfold]: + "set xs \ set ys \ list_all (\x. x \ set ys) xs" + by (auto simp: list_all_iff) + +lemma Ball_set [code]: + "Ball (set xs) P \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set [code]: + "Bex (set xs) P \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma card_set [code]: + "card (set xs) = length (remdups xs)" + by (simp add: length_remdups_card_conv) + +lemma the_elem_set [code]: + "the_elem (set [x]) = x" + by simp + +lemma Pow_set [code]: + "Pow (set []) = {{}}" + "Pow (set (x # xs)) = (let A = Pow (set xs) in A \ insert x ` A)" + by (simp_all add: Pow_insert Let_def) + +definition map_project :: "('a \ 'b option) \ 'a set \ 'b set" where + "map_project f A = {b. \ a \ A. f a = Some b}" 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" - by (smt (verit, best) atLeastAtMost_iff) - 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) - -text \optimized code (tail-recursive) for \<^term>\length\\ - -definition gen_length :: "nat \ 'a list \ nat" -where "gen_length n xs = n + length xs" - -lemma gen_length_code [code]: - "gen_length n [] = n" - "gen_length n (x # xs) = gen_length (Suc n) xs" -by(simp_all add: gen_length_def) - -declare list.size(3-4)[code del] - -lemma length_code [code]: "length = gen_length 0" -by(simp add: gen_length_def fun_eq_iff) - -hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length + "map_project f (set xs) = set (List.map_filter f xs)" + by (auto simp add: map_project_def map_filter_def image_def) + +hide_const (open) map_project + +lemma can_select_set_list_ex1 [code]: + "Set.can_select P (set A) = list_ex1 P A" + by (simp add: list_ex1_iff) + +lemma product_code [code]: + "Product_Type.product (set xs) (set ys) = set [(x, y). x \ xs, y \ ys]" + by (auto simp add: Product_Type.product_def) + +lemma Id_on_set [code]: + "Id_on (set xs) = set [(x, x). x \ xs]" + by (auto simp add: Id_on_def) + +lemma [code]: + "R `` S = List.map_project (\(x, y). if x \ S then Some y else None) R" + unfolding map_project_def by (auto split: prod.split if_split_asm) + +lemma trancl_set_ntrancl [code]: + "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" + by (simp add: finite_trancl_ntranl) + +lemma set_relcomp [code]: + "set xys O set yzs = set ([(fst xy, snd yz). xy \ xys, yz \ yzs, snd xy = fst yz])" + by auto (auto simp add: Bex_def image_def) + +lemma wf_set: + "wf (set xs) = acyclic (set xs)" + by (simp add: wf_iff_acyclic_if_finite) + +lemma wf_code_set[code]: "wf_code (set xs) = acyclic (set xs)" + unfolding wf_code_def using wf_set . subsubsection \Pretty lists\ @@ -8250,123 +8389,6 @@ (Haskell) "any" -subsubsection \Implementation of sets by lists\ - -lemma is_empty_set [code]: - "Set.is_empty (set xs) \ List.null xs" - by (simp add: null_def) - -lemma empty_set [code]: - "{} = set []" - by simp - -lemma UNIV_coset [code]: - "UNIV = List.coset []" - by simp - -lemma compl_set [code]: - "- set xs = List.coset xs" - by simp - -lemma compl_coset [code]: - "- List.coset xs = set xs" - by simp - -lemma [code]: - "x \ set xs \ List.member xs x" - "x \ List.coset xs \ \ List.member xs x" - by (simp_all add: member_def) - -lemma insert_code [code]: - "insert x (set xs) = set (List.insert x xs)" - "insert x (List.coset xs) = List.coset (removeAll x xs)" - by simp_all - -lemma remove_code [code]: - "Set.remove x (set xs) = set (removeAll x xs)" - "Set.remove x (List.coset xs) = List.coset (List.insert x xs)" - by (simp_all add: set_eq_iff ac_simps) - -lemma filter_set [code]: - "Set.filter P (set xs) = set (filter P xs)" - by auto - -lemma image_set [code]: - "image f (set xs) = set (map f xs)" - by simp - -lemma subset_code [code]: - "set xs \ B \ (\x\set xs. x \ B)" - "A \ List.coset ys \ (\y\set ys. y \ A)" - "List.coset [] \ set [] \ False" - by auto - -text \A frequent case -- avoid intermediate sets\ -lemma [code_unfold]: - "set xs \ set ys \ list_all (\x. x \ set ys) xs" - by (auto simp: list_all_iff) - -lemma Ball_set [code]: - "Ball (set xs) P \ list_all P xs" - by (simp add: list_all_iff) - -lemma Bex_set [code]: - "Bex (set xs) P \ list_ex P xs" - by (simp add: list_ex_iff) - -lemma card_set [code]: - "card (set xs) = length (remdups xs)" - by (simp add: length_remdups_card_conv) - -lemma the_elem_set [code]: - "the_elem (set [x]) = x" - by simp - -lemma Pow_set [code]: - "Pow (set []) = {{}}" - "Pow (set (x # xs)) = (let A = Pow (set xs) in A \ insert x ` A)" - by (simp_all add: Pow_insert Let_def) - -definition map_project :: "('a \ 'b option) \ 'a set \ 'b set" where - "map_project f A = {b. \ a \ A. f a = Some b}" - -lemma [code]: - "map_project f (set xs) = set (List.map_filter f xs)" - by (auto simp add: map_project_def map_filter_def image_def) - -hide_const (open) map_project - - -text \Operations on relations\ - -lemma product_code [code]: - "Product_Type.product (set xs) (set ys) = set [(x, y). x \ xs, y \ ys]" - by (auto simp add: Product_Type.product_def) - -lemma Id_on_set [code]: - "Id_on (set xs) = set [(x, x). x \ xs]" - by (auto simp add: Id_on_def) - -lemma [code]: - "R `` S = List.map_project (\(x, y). if x \ S then Some y else None) R" -unfolding map_project_def by (auto split: prod.split if_split_asm) - -lemma trancl_set_ntrancl [code]: - "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" - by (simp add: finite_trancl_ntranl) - -lemma set_relcomp [code]: - "set xys O set yzs = set ([(fst xy, snd yz). xy \ xys, yz \ yzs, snd xy = fst yz])" - by auto (auto simp add: Bex_def image_def) - -lemma wf_set: - "wf (set xs) = acyclic (set xs)" - by (simp add: wf_iff_acyclic_if_finite) - -lemma wf_code_set[code]: "wf_code (set xs) = acyclic (set xs)" - unfolding wf_code_def using wf_set . - - subsection \Setup for Lifting/Transfer\ subsubsection \Transfer rules for the Transfer package\ @@ -8382,9 +8404,6 @@ "(list_all2 A ===> list_all2 A) butlast butlast" by (rule rel_funI, erule list_all2_induct, auto) -lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs" - by (induct xs) auto - lemma append_transfer [transfer_rule]: "(list_all2 A ===> list_all2 A ===> list_all2 A) append append" unfolding List.append_def by transfer_prover @@ -8619,4 +8638,31 @@ end + +subsection \Misc\ + +lemma map_rec: + "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs" + by (induct xs) auto + +lemma in_set_member (* FIXME delete candidate *): + "x \ set xs \ List.member xs x" + by (simp add: member_def) + +lemma eq_Nil_null: (* FIXME delete candidate *) + "xs = [] \ List.null xs" + by (simp add: null_def) + +lemma concat_map_maps: (* FIXME delete candidate *) + "concat (map f xs) = List.maps f xs" + by (simp add: maps_def) + +lemma Ball_set_list_all: (* FIXME delete candidate *) + "Ball (set xs) P \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set_list_ex: (* FIXME delete candidate *) + "Bex (set xs) P \ list_ex P xs" + by (simp add: list_ex_iff) + end