proper UTF-8;
authorwenzelm
Wed Mar 05 09:59:48 2014 +0100 (2014-03-05)
changeset 55913c1409c103b77
parent 55912 e12a0ab9917c
child 55914 c5b752d549e3
proper UTF-8;
CONTRIBUTORS
src/HOL/Library/Dlist.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/CONTRIBUTORS	Tue Mar 04 16:16:05 2014 -0800
     1.2 +++ b/CONTRIBUTORS	Wed Mar 05 09:59:48 2014 +0100
     1.3 @@ -6,13 +6,14 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 -* March 2014: René Thiemann
     1.8 +* March 2014: René Thiemann
     1.9    Improved code generation for multisets.
    1.10  
    1.11  * January 2014: Lars Hupel, TUM
    1.12    An improved, interactive simplifier trace with integration into the
    1.13    Isabelle/jEdit Prover IDE.
    1.14  
    1.15 +
    1.16  Contributions to Isabelle2013-1
    1.17  -------------------------------
    1.18  
     2.1 --- a/src/HOL/Library/Dlist.thy	Tue Mar 04 16:16:05 2014 -0800
     2.2 +++ b/src/HOL/Library/Dlist.thy	Wed Mar 05 09:59:48 2014 +0100
     2.3 @@ -154,23 +154,24 @@
     2.4    with dxs show "P dxs" by simp
     2.5  qed
     2.6  
     2.7 -lemma dlist_case [case_names empty insert, cases type: dlist]:
     2.8 -  assumes empty: "dxs = empty \<Longrightarrow> P"
     2.9 -  assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P"
    2.10 -  shows P
    2.11 +lemma dlist_case [cases type: dlist]:
    2.12 +  obtains (empty) "dxs = empty"
    2.13 +    | (insert) x dys where "\<not> member dys x" and "dxs = insert x dys"
    2.14  proof (cases dxs)
    2.15    case (Abs_dlist xs)
    2.16    then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
    2.17      by (simp_all add: Dlist_def distinct_remdups_id)
    2.18 -  show P proof (cases xs)
    2.19 -    case Nil with dxs have "dxs = empty" by (simp add: empty_def) 
    2.20 -    with empty show P .
    2.21 +  show thesis
    2.22 +  proof (cases xs)
    2.23 +    case Nil with dxs
    2.24 +    have "dxs = empty" by (simp add: empty_def) 
    2.25 +    with empty show ?thesis .
    2.26    next
    2.27      case (Cons x xs)
    2.28      with dxs distinct have "\<not> member (Dlist xs) x"
    2.29        and "dxs = insert x (Dlist xs)"
    2.30        by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
    2.31 -    with insert show P .
    2.32 +    with insert show ?thesis .
    2.33    qed
    2.34  qed
    2.35  
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 04 16:16:05 2014 -0800
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 05 09:59:48 2014 +0100
     3.3 @@ -71,11 +71,10 @@
     3.4  lemma inj_ereal[simp]: "inj_on ereal A"
     3.5    unfolding inj_on_def by auto
     3.6  
     3.7 -lemma ereal_cases[case_names real PInf MInf, cases type: ereal]:
     3.8 -  assumes "\<And>r. x = ereal r \<Longrightarrow> P"
     3.9 -  assumes "x = \<infinity> \<Longrightarrow> P"
    3.10 -  assumes "x = -\<infinity> \<Longrightarrow> P"
    3.11 -  shows P
    3.12 +lemma ereal_cases[cases type: ereal]:
    3.13 +  obtains (real) r where "x = ereal r"
    3.14 +    | (PInf) "x = \<infinity>"
    3.15 +    | (MInf) "x = -\<infinity>"
    3.16    using assms by (cases x) auto
    3.17  
    3.18  lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
     4.1 --- a/src/HOL/Library/Multiset.thy	Tue Mar 04 16:16:05 2014 -0800
     4.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 05 09:59:48 2014 +0100
     4.3 @@ -647,11 +647,10 @@
     4.4  lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
     4.5  by (induct M) auto
     4.6  
     4.7 -lemma multiset_cases [cases type, case_names empty add]:
     4.8 -assumes em:  "M = {#} \<Longrightarrow> P"
     4.9 -assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
    4.10 -shows "P"
    4.11 -using assms by (induct M) simp_all
    4.12 +lemma multiset_cases [cases type]:
    4.13 +  obtains (empty) "M = {#}"
    4.14 +    | (add) N x where "M = N + {#x#}"
    4.15 +  using assms by (induct M) simp_all
    4.16  
    4.17  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
    4.18  by (cases "B = {#}") (auto dest: multi_member_split)