# HG changeset patch # User wenzelm # Date 1394009988 -3600 # Node ID c1409c103b77d2d676fb0a522c8df42d0f98a1df # Parent e12a0ab9917cfd901ab720b1f593f630f729db66 proper UTF-8; diff -r e12a0ab9917c -r c1409c103b77 CONTRIBUTORS --- a/CONTRIBUTORS Tue Mar 04 16:16:05 2014 -0800 +++ b/CONTRIBUTORS Wed Mar 05 09:59:48 2014 +0100 @@ -6,13 +6,14 @@ Contributions to this Isabelle version -------------------------------------- -* March 2014: René Thiemann +* March 2014: René Thiemann Improved code generation for multisets. * January 2014: Lars Hupel, TUM An improved, interactive simplifier trace with integration into the Isabelle/jEdit Prover IDE. + Contributions to Isabelle2013-1 ------------------------------- diff -r e12a0ab9917c -r c1409c103b77 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Tue Mar 04 16:16:05 2014 -0800 +++ b/src/HOL/Library/Dlist.thy Wed Mar 05 09:59:48 2014 +0100 @@ -154,23 +154,24 @@ with dxs show "P dxs" by simp qed -lemma dlist_case [case_names empty insert, cases type: dlist]: - assumes empty: "dxs = empty \ P" - assumes insert: "\x dys. \ member dys x \ dxs = insert x dys \ P" - shows P +lemma dlist_case [cases type: dlist]: + obtains (empty) "dxs = empty" + | (insert) x dys where "\ member dys x" and "dxs = insert x dys" proof (cases dxs) case (Abs_dlist xs) then have dxs: "dxs = Dlist xs" and distinct: "distinct xs" by (simp_all add: Dlist_def distinct_remdups_id) - show P proof (cases xs) - case Nil with dxs have "dxs = empty" by (simp add: empty_def) - with empty show P . + show thesis + proof (cases xs) + case Nil with dxs + have "dxs = empty" by (simp add: empty_def) + with empty show ?thesis . next case (Cons x xs) with dxs distinct have "\ member (Dlist xs) x" and "dxs = insert x (Dlist xs)" by (simp_all add: member_def List.member_def insert_def distinct_remdups_id) - with insert show P . + with insert show ?thesis . qed qed diff -r e12a0ab9917c -r c1409c103b77 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue Mar 04 16:16:05 2014 -0800 +++ b/src/HOL/Library/Extended_Real.thy Wed Mar 05 09:59:48 2014 +0100 @@ -71,11 +71,10 @@ lemma inj_ereal[simp]: "inj_on ereal A" unfolding inj_on_def by auto -lemma ereal_cases[case_names real PInf MInf, cases type: ereal]: - assumes "\r. x = ereal r \ P" - assumes "x = \ \ P" - assumes "x = -\ \ P" - shows P +lemma ereal_cases[cases type: ereal]: + obtains (real) r where "x = ereal r" + | (PInf) "x = \" + | (MInf) "x = -\" using assms by (cases x) auto lemmas ereal2_cases = ereal_cases[case_product ereal_cases] diff -r e12a0ab9917c -r c1409c103b77 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Mar 04 16:16:05 2014 -0800 +++ b/src/HOL/Library/Multiset.thy Wed Mar 05 09:59:48 2014 +0100 @@ -647,11 +647,10 @@ lemma multi_nonempty_split: "M \ {#} \ \A a. M = A + {#a#}" by (induct M) auto -lemma multiset_cases [cases type, case_names empty add]: -assumes em: "M = {#} \ P" -assumes add: "\N x. M = N + {#x#} \ P" -shows "P" -using assms by (induct M) simp_all +lemma multiset_cases [cases type]: + obtains (empty) "M = {#}" + | (add) N x where "M = N + {#x#}" + using assms by (induct M) simp_all lemma multi_drop_mem_not_eq: "c \# B \ B - {#c#} \ B" by (cases "B = {#}") (auto dest: multi_member_split)