# HG changeset patch # User blanchet # Date 1360924594 -3600 # Node ID 43502299c9350167002f82ad8d1b0a3aee48bf5c # Parent 4f0147ed8bcb35449e995576377589e4a46a9cab# Parent cc7423ce677414aee2043166012450013fb64917 merge diff -r 4f0147ed8bcb -r 43502299c935 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Fri Feb 15 11:27:15 2013 +0100 +++ b/src/HOL/BNF/Examples/Stream.thy Fri Feb 15 11:36:34 2013 +0100 @@ -16,25 +16,33 @@ (* TODO: Provide by the package*) theorem stream_set_induct: - "\\s. P (shd s) s; \s y. \y \ stream_set (stl s); P y (stl s)\ \ P y s\ \ - \y \ stream_set s. P y s" -by (rule stream.dtor_set_induct) - (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) + "\\s. P (shd s) s; \s y. \y \ stream_set (stl s); P y (stl s)\ \ P y s\ \ + \y \ stream_set s. P y s" + by (rule stream.dtor_set_induct) + (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) + +lemma stream_map_simps[simp]: + "shd (stream_map f s) = f (shd s)" "stl (stream_map f s) = stream_map f (stl s)" + unfolding shd_def stl_def stream_case_def stream_map_def stream.dtor_unfold + by (case_tac [!] s) (auto simp: Stream_def stream.dtor_ctor) + +lemma stream_map_Stream[simp]: "stream_map f (x ## s) = f x ## stream_map f s" + by (metis stream.exhaust stream.sels stream_map_simps) theorem shd_stream_set: "shd s \ stream_set s" -by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) - (metis UnCI fsts_def insertI1 stream.dtor_set) + by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) + (metis UnCI fsts_def insertI1 stream.dtor_set) theorem stl_stream_set: "y \ stream_set (stl s) \ y \ stream_set s" -by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) - (metis insertI1 set_mp snds_def stream.dtor_set_set_incl) + by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) + (metis insertI1 set_mp snds_def stream.dtor_set_set_incl) (* only for the non-mutual case: *) theorem stream_set_induct1[consumes 1, case_names shd stl, induct set: "stream_set"]: assumes "y \ stream_set s" and "\s. P (shd s) s" and "\s y. \y \ stream_set (stl s); P y (stl s)\ \ P y s" shows "P y s" -using assms stream_set_induct by blast + using assms stream_set_induct by blast (* end TODO *) @@ -45,39 +53,18 @@ | "shift (x # xs) s = x ## shift xs s" lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s" -by (induct xs) auto + by (induct xs) auto lemma shift_simps[simp]: "shd (xs @- s) = (if xs = [] then shd s else hd xs)" "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)" -by (induct xs) auto - - -subsection {* recurring stream out of a list *} + by (induct xs) auto -definition cycle :: "'a list \ 'a stream" where - "cycle = stream_unfold hd (\xs. tl xs @ [hd xs])" - -lemma cycle_simps[simp]: - "shd (cycle u) = hd u" - "stl (cycle u) = cycle (tl u @ [hd u])" -by (auto simp: cycle_def) +lemma stream_set_shift[simp]: "stream_set (xs @- s) = set xs \ stream_set s" + by (induct xs) auto -lemma cycle_decomp: "u \ [] \ cycle u = u @- cycle u" -proof (coinduct rule: stream.coinduct[of "\s1 s2. \u. s1 = cycle u \ s2 = u @- cycle u \ u \ []"]) - case (2 s1 s2) - then obtain u where "s1 = cycle u \ s2 = u @- cycle u \ u \ []" by blast - thus ?case using stream.unfold[of hd "\xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def) -qed auto - -lemma cycle_Cons: "cycle (x # xs) = x ## cycle (xs @ [x])" -proof (coinduct rule: stream.coinduct[of "\s1 s2. \x xs. s1 = cycle (x # xs) \ s2 = x ## cycle (xs @ [x])"]) - case (2 s1 s2) - then obtain x xs where "s1 = cycle (x # xs) \ s2 = x ## cycle (xs @ [x])" by blast - thus ?case - by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold) -qed auto +subsection {* set of streams with elements in some fixes set *} coinductive_set streams :: "'a set => 'a stream set" @@ -86,7 +73,7 @@ Stream[intro!, simp, no_atp]: "\a \ A; s \ streams A\ \ a ## s \ streams A" lemma shift_streams: "\w \ lists A; s \ streams A\ \ w @- s \ streams A" -by (induct w) auto + by (induct w) auto lemma stream_set_streams: assumes "stream_set s \ A" @@ -110,52 +97,137 @@ lemma flat_simps[simp]: "shd (flat ws) = hd (shd ws)" "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)" -unfolding flat_def by auto + unfolding flat_def by auto lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)" -unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto + unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto lemma flat_Stream[simp]: "xs \ [] \ flat (xs ## ws) = xs @- flat ws" -by (induct xs) auto + by (induct xs) auto lemma flat_unfold: "shd ws \ [] \ flat ws = shd ws @- flat (stl ws)" -by (cases ws) auto + by (cases ws) auto -subsection {* take, drop, nth for streams *} +subsection {* nth, take, drop for streams *} + +primrec snth :: "'a stream \ nat \ 'a" (infixl "!!" 100) where + "s !! 0 = shd s" +| "s !! Suc n = stl s !! n" + +lemma snth_stream_map[simp]: "stream_map f s !! n = f (s !! n)" + by (induct n arbitrary: s) auto + +lemma shift_snth_less[simp]: "p < length xs \ (xs @- s) !! p = xs ! p" + by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl) + +lemma shift_snth_ge[simp]: "p \ length xs \ (xs @- s) !! p = s !! (p - length xs)" + by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred) + +lemma snth_stream_set[simp]: "s !! n \ stream_set s" + by (induct n arbitrary: s) (auto intro: shd_stream_set stl_stream_set) + +lemma stream_set_range: "stream_set s = range (snth s)" +proof (intro equalityI subsetI) + fix x assume "x \ stream_set s" + thus "x \ range (snth s)" + proof (induct s) + case (stl s x) + then obtain n where "x = stl s !! n" by auto + thus ?case by (auto intro: range_eqI[of _ _ "Suc n"]) + qed (auto intro: range_eqI[of _ _ 0]) +qed auto primrec stake :: "nat \ 'a stream \ 'a list" where "stake 0 s = []" | "stake (Suc n) s = shd s # stake n (stl s)" +lemma length_stake[simp]: "length (stake n s) = n" + by (induct n arbitrary: s) auto + +lemma stake_stream_map[simp]: "stake n (stream_map f s) = map f (stake n s)" + by (induct n arbitrary: s) auto + primrec sdrop :: "nat \ 'a stream \ 'a stream" where "sdrop 0 s = s" | "sdrop (Suc n) s = sdrop n (stl s)" -primrec snth :: "'a stream \ nat \ 'a" (infixl "!!" 100) where - "s !! 0 = shd s" -| "s !! Suc n = stl s !! n" +lemma sdrop_simps[simp]: + "shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s" + by (induct n arbitrary: s) auto + +lemma sdrop_stream_map[simp]: "sdrop n (stream_map f s) = stream_map f (sdrop n s)" + by (induct n arbitrary: s) auto lemma stake_sdrop: "stake n s @- sdrop n s = s" -by (induct n arbitrary: s) auto + by (induct n arbitrary: s) auto + +lemma id_stake_snth_sdrop: + "s = stake i s @- s !! i ## sdrop (Suc i) s" + by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse) -lemma stake_empty: "stake n s = [] \ n = 0" -by (cases n) auto +lemma stream_map_alt: "stream_map f s = s' \ (\n. f (s !! n) = s' !! n)" (is "?L = ?R") +proof + assume ?R + thus ?L + by (coinduct rule: stream.coinduct[of "\s1 s2. \n. s1 = stream_map f (sdrop n s) \ s2 = sdrop n s'"]) + (auto intro: exI[of _ 0] simp del: sdrop.simps(2)) +qed auto + +lemma stake_invert_Nil[iff]: "stake n s = [] \ n = 0" + by (induct n) auto lemma sdrop_shift: "\s = w @- s'; length w = n\ \ sdrop n s = s'" -by (induct n arbitrary: w s) auto + by (induct n arbitrary: w s) auto lemma stake_shift: "\s = w @- s'; length w = n\ \ stake n s = w" -by (induct n arbitrary: w s) auto + by (induct n arbitrary: w s) auto lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s" -by (induct m arbitrary: s) auto + by (induct m arbitrary: s) auto lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s" -by (induct m arbitrary: s) auto + by (induct m arbitrary: s) auto + + +subsection {* unary predicates lifted to streams *} + +definition "stream_all P s = (\p. P (s !! p))" + +lemma stream_all_iff[iff]: "stream_all P s \ Ball (stream_set s) P" + unfolding stream_all_def stream_set_range by auto + +lemma stream_all_shift[simp]: "stream_all P (xs @- s) = (list_all P xs \ stream_all P s)" + unfolding stream_all_iff list_all_iff by auto + + +subsection {* recurring stream out of a list *} + +definition cycle :: "'a list \ 'a stream" where + "cycle = stream_unfold hd (\xs. tl xs @ [hd xs])" + +lemma cycle_simps[simp]: + "shd (cycle u) = hd u" + "stl (cycle u) = cycle (tl u @ [hd u])" + by (auto simp: cycle_def) + +lemma cycle_decomp: "u \ [] \ cycle u = u @- cycle u" +proof (coinduct rule: stream.coinduct[of "\s1 s2. \u. s1 = cycle u \ s2 = u @- cycle u \ u \ []"]) + case (2 s1 s2) + then obtain u where "s1 = cycle u \ s2 = u @- cycle u \ u \ []" by blast + thus ?case using stream.unfold[of hd "\xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def) +qed auto + +lemma cycle_Cons: "cycle (x # xs) = x ## cycle (xs @ [x])" +proof (coinduct rule: stream.coinduct[of "\s1 s2. \x xs. s1 = cycle (x # xs) \ s2 = x ## cycle (xs @ [x])"]) + case (2 s1 s2) + then obtain x xs where "s1 = cycle (x # xs) \ s2 = x ## cycle (xs @ [x])" by blast + thus ?case + by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold) +qed auto lemma cycle_rotated: "\v \ []; cycle u = v @- s\ \ cycle (tl u @ [hd u]) = tl v @- s" -by (auto dest: arg_cong[of _ _ stl]) + by (auto dest: arg_cong[of _ _ stl]) lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s" proof (induct n arbitrary: u) @@ -166,27 +238,105 @@ assumes "u \ []" "n < length u" shows "stake n (cycle u) = take n u" using min_absorb2[OF less_imp_le_nat[OF assms(2)]] -by (subst cycle_decomp[OF assms(1)], subst stake_append) auto + by (subst cycle_decomp[OF assms(1)], subst stake_append) auto lemma stake_cycle_eq[simp]: "u \ [] \ stake (length u) (cycle u) = u" -by (metis cycle_decomp stake_shift) + by (metis cycle_decomp stake_shift) lemma sdrop_cycle_eq[simp]: "u \ [] \ sdrop (length u) (cycle u) = cycle u" -by (metis cycle_decomp sdrop_shift) + by (metis cycle_decomp sdrop_shift) lemma stake_cycle_eq_mod_0[simp]: "\u \ []; n mod length u = 0\ \ stake n (cycle u) = concat (replicate (n div length u) u)" -by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric]) + by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric]) lemma sdrop_cycle_eq_mod_0[simp]: "\u \ []; n mod length u = 0\ \ sdrop n (cycle u) = cycle u" -by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric]) + by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric]) lemma stake_cycle: "u \ [] \ stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u" -by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto + by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto lemma sdrop_cycle: "u \ [] \ sdrop n (cycle u) = cycle (rotate (n mod length u) u)" -by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric]) + by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric]) + + +subsection {* stream repeating a single element *} + +definition "same x = stream_unfold (\_. x) id ()" + +lemma same_simps[simp]: "shd (same x) = x" "stl (same x) = same x" + unfolding same_def by auto + +lemma same_unfold: "same x = Stream x (same x)" + by (metis same_simps stream.collapse) + +lemma snth_same[simp]: "same x !! n = x" + unfolding same_def by (induct n) auto + +lemma stake_same[simp]: "stake n (same x) = replicate n x" + unfolding same_def by (induct n) (auto simp: upt_rec) + +lemma sdrop_same[simp]: "sdrop n (same x) = same x" + unfolding same_def by (induct n) auto + +lemma shift_replicate_same[simp]: "replicate n x @- same x = same x" + by (metis sdrop_same stake_same stake_sdrop) + +lemma stream_all_same[simp]: "stream_all P (same x) \ P x" + unfolding stream_all_def by auto + +lemma same_cycle: "same x = cycle [x]" + by (coinduct rule: stream.coinduct[of "\s1 s2. s1 = same x \ s2 = cycle [x]"]) auto + + +subsection {* stream of natural numbers *} + +definition "fromN n = stream_unfold id Suc n" + +lemma fromN_simps[simp]: "shd (fromN n) = n" "stl (fromN n) = fromN (Suc n)" + unfolding fromN_def by auto + +lemma snth_fromN[simp]: "fromN n !! m = n + m" + unfolding fromN_def by (induct m arbitrary: n) auto + +lemma stake_fromN[simp]: "stake m (fromN n) = [n ..< m + n]" + unfolding fromN_def by (induct m arbitrary: n) (auto simp: upt_rec) + +lemma sdrop_fromN[simp]: "sdrop m (fromN n) = fromN (n + m)" + unfolding fromN_def by (induct m arbitrary: n) auto + +abbreviation "nats \ fromN 0" + + +subsection {* zip *} + +definition "szip s1 s2 = + stream_unfold (map_pair shd shd) (map_pair stl stl) (s1, s2)" + +lemma szip_simps[simp]: + "shd (szip s1 s2) = (shd s1, shd s2)" "stl (szip s1 s2) = szip (stl s1) (stl s2)" + unfolding szip_def by auto + +lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)" + by (induct n arbitrary: s1 s2) auto + + +subsection {* zip via function *} + +definition "stream_map2 f s1 s2 = + stream_unfold (\(s1,s2). f (shd s1) (shd s2)) (map_pair stl stl) (s1, s2)" + +lemma stream_map2_simps[simp]: + "shd (stream_map2 f s1 s2) = f (shd s1) (shd s2)" + "stl (stream_map2 f s1 s2) = stream_map2 f (stl s1) (stl s2)" + unfolding stream_map2_def by auto + +lemma stream_map2_szip: + "stream_map2 f s1 s2 = stream_map (split f) (szip s1 s2)" + by (coinduct rule: stream.coinduct[of + "\s1 s2. \s1' s2'. s1 = stream_map2 f s1' s2' \ s2 = stream_map (split f) (szip s1' s2')"]) + fastforce+ end diff -r 4f0147ed8bcb -r 43502299c935 src/HOL/Codegenerator_Test/RBT_Set_Test.thy --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Fri Feb 15 11:27:15 2013 +0100 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Fri Feb 15 11:36:34 2013 +0100 @@ -25,9 +25,17 @@ lemma [code, code del]: "acc = acc" .. -lemmas [code del] = - finite_set_code finite_coset_code - equal_set_code +lemma [code, code del]: + "Cardinality.card' = Cardinality.card'" .. + +lemma [code, code del]: + "Cardinality.finite' = Cardinality.finite'" .. + +lemma [code, code del]: + "Cardinality.subset' = Cardinality.subset'" .. + +lemma [code, code del]: + "Cardinality.eq_set = Cardinality.eq_set" .. (* If the code generation ends with an exception with the following message: diff -r 4f0147ed8bcb -r 43502299c935 src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Fri Feb 15 11:27:15 2013 +0100 +++ b/src/HOL/Library/Cardinality.thy Fri Feb 15 11:36:34 2013 +0100 @@ -388,65 +388,133 @@ subsection {* Code setup for sets *} text {* - Implement operations @{term "finite"}, @{term "card"}, @{term "op \"}, and @{term "op ="} - for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}. + Implement @{term "CARD('a)"} via @{term card_UNIV} and provide + implementations for @{term "finite"}, @{term "card"}, @{term "op \"}, + and @{term "op ="}if the calling context already provides @{class finite_UNIV} + and @{class card_UNIV} instances. If we implemented the latter + always via @{term card_UNIV}, we would require instances of essentially all + element types, i.e., a lot of instantiation proofs and -- at run time -- + possibly slow dictionary constructions. *} +definition card_UNIV' :: "'a card_UNIV" +where [code del]: "card_UNIV' = Phantom('a) CARD('a)" + +lemma CARD_code [code_unfold]: + "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)" +by(simp add: card_UNIV'_def) + +lemma card_UNIV'_code [code]: + "card_UNIV' = card_UNIV" +by(simp add: card_UNIV card_UNIV'_def) + +hide_const (open) card_UNIV' + lemma card_Compl: "finite A \ card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)" by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) -lemma card_coset_code [code]: - fixes xs :: "'a :: card_UNIV list" - shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" -by(simp add: List.card_set card_Compl card_UNIV) - -lemma [code, code del]: "finite = finite" .. +context fixes xs :: "'a :: finite_UNIV list" +begin -lemma [code]: - fixes xs :: "'a :: card_UNIV list" - shows finite_set_code: - "finite (set xs) = True" - and finite_coset_code: - "finite (List.coset xs) \ of_phantom (finite_UNIV :: 'a finite_UNIV)" +definition finite' :: "'a set \ bool" +where [simp, code del, code_abbrev]: "finite' = finite" + +lemma finite'_code [code]: + "finite' (set xs) \ True" + "finite' (List.coset xs) \ of_phantom (finite_UNIV :: 'a finite_UNIV)" by(simp_all add: card_gt_0_iff finite_UNIV) -lemma coset_subset_code [code]: - fixes xs :: "'a list" shows - "List.coset xs \ set ys \ (let n = CARD('a) in n > 0 \ card (set (xs @ ys)) = n)" +end + +context fixes xs :: "'a :: card_UNIV list" +begin + +definition card' :: "'a set \ nat" +where [simp, code del, code_abbrev]: "card' = card" + +lemma card'_code [code]: + "card' (set xs) = length (remdups xs)" + "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" +by(simp_all add: List.card_set card_Compl card_UNIV) + + +definition subset' :: "'a set \ 'a set \ bool" +where [simp, code del, code_abbrev]: "subset' = op \" + +lemma subset'_code [code]: + "subset' A (List.coset ys) \ (\y \ set ys. y \ A)" + "subset' (set ys) B \ (\y \ set ys. y \ B)" + "subset' (List.coset xs) (set ys) \ (let n = CARD('a) in n > 0 \ card(set (xs @ ys)) = n)" by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) (metis finite_compl finite_set rev_finite_subset) -lemma equal_set_code [code]: - fixes xs ys :: "'a :: equal list" +definition eq_set :: "'a set \ 'a set \ bool" +where [simp, code del, code_abbrev]: "eq_set = op =" + +lemma eq_set_code [code]: + fixes ys defines "rhs \ let n = CARD('a) in if n = 0 then False else let xs' = remdups xs; ys' = remdups ys in length xs' + length ys' = n \ (\x \ set xs'. x \ set ys') \ (\y \ set ys'. y \ set xs')" - shows "equal_class.equal (List.coset xs) (set ys) \ rhs" (is ?thesis1) - and "equal_class.equal (set ys) (List.coset xs) \ rhs" (is ?thesis2) - and "equal_class.equal (set xs) (set ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis3) - and "equal_class.equal (List.coset xs) (List.coset ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis4) + shows "eq_set (List.coset xs) (set ys) \ rhs" (is ?thesis1) + and "eq_set (set ys) (List.coset xs) \ rhs" (is ?thesis2) + and "eq_set (set xs) (set ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis3) + and "eq_set (List.coset xs) (List.coset ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis4) proof - show ?thesis1 (is "?lhs \ ?rhs") proof assume ?lhs thus ?rhs - by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) + by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) next assume ?rhs moreover have "\ \y\set xs. y \ set ys; \x\set ys. x \ set xs \ \ set xs \ set ys = {}" by blast ultimately show ?lhs - by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm) + by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm) qed - thus ?thesis2 unfolding equal_eq by blast - show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+ + thus ?thesis2 unfolding eq_set_def by blast + show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+ qed -notepad begin (* test code setup *) -have "List.coset [True] = set [False] \ List.coset [] \ List.set [True, False] \ finite (List.coset [True])" +end + +text {* + Provide more informative exceptions than Match for non-rewritten cases. + If generated code raises one these exceptions, then a code equation calls + the mentioned operator for an element type that is not an instance of + @{class card_UNIV} and is therefore not implemented via @{term card_UNIV}. + Constrain the element type with sort @{class card_UNIV} to change this. +*} + +definition card_coset_requires_card_UNIV :: "'a list \ nat" +where [code del, simp]: "card_coset_requires_card_UNIV xs = card (List.coset xs)" + +code_abort card_coset_requires_card_UNIV + +lemma card_coset_error [code]: + "card (List.coset xs) = card_coset_requires_card_UNIV xs" +by(simp) + +definition coset_subseteq_set_requires_card_UNIV :: "'a list \ 'a list \ bool" +where [code del, simp]: "coset_subseteq_set_requires_card_UNIV xs ys \ List.coset xs \ set ys" + +code_abort coset_subseteq_set_requires_card_UNIV + +lemma coset_subseteq_set_code [code]: + "List.coset xs \ set ys \ + (if xs = [] \ ys = [] then False else coset_subseteq_set_requires_card_UNIV xs ys)" +by simp + +notepad begin -- "test code setup" +have "List.coset [True] = set [False] \ + List.coset [] \ List.set [True, False] \ + finite (List.coset [True])" by eval end +hide_const (open) card' finite' subset' eq_set + end