tuned;
authorwenzelm
Mon Apr 28 17:50:03 2014 +0200 (2014-04-28)
changeset 567779c3f0ae99532
parent 56776 309e1a61ee7c
child 56778 cb0929421ca6
tuned;
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Float.thy
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:48:59 2014 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:50:03 2014 +0200
     1.3 @@ -615,19 +615,18 @@
     1.4  begin
     1.5  
     1.6  definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
     1.7 -  "inf_enat \<equiv> min"
     1.8 +  "inf_enat = min"
     1.9  
    1.10  definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
    1.11 -  "sup_enat \<equiv> max"
    1.12 +  "sup_enat = max"
    1.13  
    1.14  definition Inf_enat :: "enat set \<Rightarrow> enat" where
    1.15 -  "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
    1.16 +  "Inf_enat A = (if A = {} then \<infinity> else (LEAST x. x \<in> A))"
    1.17  
    1.18  definition Sup_enat :: "enat set \<Rightarrow> enat" where
    1.19 -  "Sup_enat A \<equiv> if A = {} then 0
    1.20 -    else if finite A then Max A
    1.21 -                     else \<infinity>"
    1.22 -instance proof
    1.23 +  "Sup_enat A = (if A = {} then 0 else if finite A then Max A else \<infinity>)"
    1.24 +instance
    1.25 +proof
    1.26    fix x :: "enat" and A :: "enat set"
    1.27    { assume "x \<in> A" then show "Inf A \<le> x"
    1.28        unfolding Inf_enat_def by (auto intro: Least_le) }
     2.1 --- a/src/HOL/Library/Float.thy	Mon Apr 28 17:48:59 2014 +0200
     2.2 +++ b/src/HOL/Library/Float.thy	Mon Apr 28 17:50:03 2014 +0200
     2.3 @@ -919,7 +919,7 @@
     2.4    show ?thesis
     2.5    proof (cases "0 \<le> l")
     2.6      assume "0 \<le> l"
     2.7 -    def x' == "x * 2 ^ nat l"
     2.8 +    def x' \<equiv> "x * 2 ^ nat l"
     2.9      have "int x * 2 ^ nat l = x'" by (simp add: x'_def int_mult int_power)
    2.10      moreover have "real x * 2 powr real l = real x'"
    2.11        by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
    2.12 @@ -931,7 +931,7 @@
    2.13           (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
    2.14     next
    2.15      assume "\<not> 0 \<le> l"
    2.16 -    def y' == "y * 2 ^ nat (- l)"
    2.17 +    def y' \<equiv> "y * 2 ^ nat (- l)"
    2.18      from `y \<noteq> 0` have "y' \<noteq> 0" by (simp add: y'_def)
    2.19      have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
    2.20      moreover have "real x * real (2::int) powr real l / real y = x / real y'"
    2.21 @@ -959,9 +959,12 @@
    2.22      using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
    2.23  qed
    2.24  
    2.25 -lemma power_aux: assumes "x > 0" shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
    2.26 +lemma power_aux:
    2.27 +  assumes "x > 0"
    2.28 +  shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
    2.29  proof -
    2.30 -  def y \<equiv> "nat (x - 1)" moreover
    2.31 +  def y \<equiv> "nat (x - 1)"
    2.32 +  moreover
    2.33    have "(2::int) ^ y \<le> (2 ^ (y + 1)) - 1" by simp
    2.34    ultimately show ?thesis using assms by simp
    2.35  qed
    2.36 @@ -1103,8 +1106,8 @@
    2.37  
    2.38  lemma lapprox_rat_nonneg:
    2.39    fixes n x y
    2.40 -  defines "p == int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
    2.41 -  assumes "0 \<le> x" "0 < y"
    2.42 +  defines "p \<equiv> int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
    2.43 +  assumes "0 \<le> x" and "0 < y"
    2.44    shows "0 \<le> real (lapprox_rat n x y)"
    2.45  using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    2.46     powr_int[of 2, simplified]
     3.1 --- a/src/HOL/Library/FuncSet.thy	Mon Apr 28 17:48:59 2014 +0200
     3.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Apr 28 17:50:03 2014 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4  abbreviation
     3.5    funcset :: "['a set, 'b set] => ('a => 'b) set"
     3.6      (infixr "->" 60) where
     3.7 -  "A -> B == Pi A (%_. B)"
     3.8 +  "A -> B \<equiv> Pi A (%_. B)"
     3.9  
    3.10  notation (xsymbols)
    3.11    funcset  (infixr "\<rightarrow>" 60)
    3.12 @@ -41,8 +41,8 @@
    3.13    "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    3.14  
    3.15  translations
    3.16 -  "PI x:A. B" == "CONST Pi A (%x. B)"
    3.17 -  "%x:A. f" == "CONST restrict (%x. f) A"
    3.18 +  "PI x:A. B" \<rightleftharpoons> "CONST Pi A (%x. B)"
    3.19 +  "%x:A. f" \<rightleftharpoons> "CONST restrict (%x. f) A"
    3.20  
    3.21  definition
    3.22    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where
    3.23 @@ -352,7 +352,7 @@
    3.24  
    3.25  syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    3.26  
    3.27 -translations "PIE x:A. B" == "CONST Pi\<^sub>E A (%x. B)"
    3.28 +translations "PIE x:A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (%x. B)"
    3.29  
    3.30  abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60) where
    3.31    "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"