summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 05 Mar 2014 09:59:48 +0100 | |

changeset 55913 | c1409c103b77 |

parent 55912 | e12a0ab9917c |

child 55914 | c5b752d549e3 |

proper UTF-8;

--- 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 -------------------------------

--- 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 \<Longrightarrow> P" - assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P" - shows P +lemma dlist_case [cases type: dlist]: + obtains (empty) "dxs = empty" + | (insert) x dys where "\<not> 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 "\<not> 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

--- 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 "\<And>r. x = ereal r \<Longrightarrow> P" - assumes "x = \<infinity> \<Longrightarrow> P" - assumes "x = -\<infinity> \<Longrightarrow> P" - shows P +lemma ereal_cases[cases type: ereal]: + obtains (real) r where "x = ereal r" + | (PInf) "x = \<infinity>" + | (MInf) "x = -\<infinity>" using assms by (cases x) auto lemmas ereal2_cases = ereal_cases[case_product ereal_cases]

--- 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 \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}" by (induct M) auto -lemma multiset_cases [cases type, case_names empty add]: -assumes em: "M = {#} \<Longrightarrow> P" -assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> 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 \<in># B \<Longrightarrow> B - {#c#} \<noteq> B" by (cases "B = {#}") (auto dest: multi_member_split)