*** empty log message ***
authornipkow
Thu May 24 22:55:53 2007 +0200 (2007-05-24)
changeset 23096423ad2fe9f76
parent 23095 45f10b70e891
child 23097 f4779adcd1a2
*** empty log message ***
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Integ/NatBin.thy
src/HOL/List.thy
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu May 24 16:52:54 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu May 24 22:55:53 2007 +0200
     1.3 @@ -87,14 +87,14 @@
     1.4       "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
     1.5  apply (rule hypreal_sqrt_approx_zero2)
     1.6  apply (rule add_nonneg_nonneg)+
     1.7 -apply (auto simp add: zero_le_square)
     1.8 +apply (auto)
     1.9  done
    1.10  
    1.11  lemma hypreal_sqrt_sum_squares2 [simp]:
    1.12       "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
    1.13  apply (rule hypreal_sqrt_approx_zero2)
    1.14  apply (rule add_nonneg_nonneg)
    1.15 -apply (auto simp add: zero_le_square)
    1.16 +apply (auto)
    1.17  done
    1.18  
    1.19  lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
    1.20 @@ -157,7 +157,7 @@
    1.21       "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
    1.22  apply (rule HFinite_hypreal_sqrt_iff)
    1.23  apply (rule add_nonneg_nonneg)
    1.24 -apply (auto simp add: zero_le_square)
    1.25 +apply (auto)
    1.26  done
    1.27  
    1.28  lemma Infinitesimal_hypreal_sqrt:
    1.29 @@ -184,7 +184,7 @@
    1.30       "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
    1.31  apply (rule Infinitesimal_hypreal_sqrt_iff)
    1.32  apply (rule add_nonneg_nonneg)
    1.33 -apply (auto simp add: zero_le_square)
    1.34 +apply (auto)
    1.35  done
    1.36  
    1.37  lemma HInfinite_hypreal_sqrt:
    1.38 @@ -211,7 +211,7 @@
    1.39       "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
    1.40  apply (rule HInfinite_hypreal_sqrt_iff)
    1.41  apply (rule add_nonneg_nonneg)
    1.42 -apply (auto simp add: zero_le_square)
    1.43 +apply (auto)
    1.44  done
    1.45  
    1.46  lemma HFinite_exp [simp]:
     2.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu May 24 16:52:54 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/NSA.thy	Thu May 24 22:55:53 2007 +0200
     2.3 @@ -1723,13 +1723,13 @@
     2.4       "(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
     2.5  apply (rule Infinitesimal_interval2)
     2.6  apply (rule_tac [3] zero_le_square, assumption)
     2.7 -apply (auto simp add: zero_le_square)
     2.8 +apply (auto)
     2.9  done
    2.10  
    2.11  lemma HFinite_square_cancel [simp]:
    2.12    "(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
    2.13  apply (rule HFinite_bounded, assumption)
    2.14 -apply (auto simp add: zero_le_square)
    2.15 +apply (auto)
    2.16  done
    2.17  
    2.18  lemma Infinitesimal_square_cancel2 [simp]:
    2.19 @@ -1751,7 +1751,7 @@
    2.20  apply (rule Infinitesimal_interval2, assumption)
    2.21  apply (rule_tac [2] zero_le_square, simp)
    2.22  apply (insert zero_le_square [of y]) 
    2.23 -apply (insert zero_le_square [of z], simp)
    2.24 +apply (insert zero_le_square [of z], simp del:zero_le_square)
    2.25  done
    2.26  
    2.27  lemma HFinite_sum_square_cancel [simp]:
    2.28 @@ -1759,7 +1759,7 @@
    2.29  apply (rule HFinite_bounded, assumption)
    2.30  apply (rule_tac [2] zero_le_square)
    2.31  apply (insert zero_le_square [of y]) 
    2.32 -apply (insert zero_le_square [of z], simp)
    2.33 +apply (insert zero_le_square [of z], simp del:zero_le_square)
    2.34  done
    2.35  
    2.36  lemma Infinitesimal_sum_square_cancel2 [simp]:
     3.1 --- a/src/HOL/Integ/NatBin.thy	Thu May 24 16:52:54 2007 +0200
     3.2 +++ b/src/HOL/Integ/NatBin.thy	Thu May 24 22:55:53 2007 +0200
     3.3 @@ -343,7 +343,7 @@
     3.4  
     3.5  lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
     3.6  apply (induct "n")
     3.7 -apply (auto simp add: power_Suc power_add power2_minus)
     3.8 +apply (auto simp add: power_Suc power_add)
     3.9  done
    3.10  
    3.11  lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
    3.12 @@ -366,7 +366,7 @@
    3.13      have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
    3.14        by (simp add: mult_ac power_add power2_eq_square)
    3.15      thus ?case
    3.16 -      by (simp add: prems zero_le_square zero_le_mult_iff)
    3.17 +      by (simp add: prems zero_le_mult_iff)
    3.18  qed
    3.19  
    3.20  lemma odd_power_less_zero:
     4.1 --- a/src/HOL/List.thy	Thu May 24 16:52:54 2007 +0200
     4.2 +++ b/src/HOL/List.thy	Thu May 24 22:55:53 2007 +0200
     4.3 @@ -28,6 +28,7 @@
     4.4    butlast :: "'a list => 'a list"
     4.5    set :: "'a list => 'a set"
     4.6    map :: "('a=>'b) => ('a list => 'b list)"
     4.7 +  listsum ::  "'a list => 'a::monoid_add"
     4.8    nth :: "'a list => nat => 'a"    (infixl "!" 100)
     4.9    list_update :: "'a list => nat => 'a => 'a list"
    4.10    take:: "nat => 'a list => 'a list"
    4.11 @@ -134,6 +135,10 @@
    4.12    "concat(x#xs) = x @ concat(xs)"
    4.13  
    4.14  primrec
    4.15 +"listsum [] = 0"
    4.16 +"listsum (x # xs) = x + listsum xs"
    4.17 +
    4.18 +primrec
    4.19    drop_Nil:"drop n [] = []"
    4.20    drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
    4.21    -- {*Warning: simpset does not contain this definition, but separate
    4.22 @@ -1417,6 +1422,20 @@
    4.23  "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
    4.24  by (induct rule:list_induct2, simp_all)
    4.25  
    4.26 +lemma map_zip_map:
    4.27 + "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
    4.28 +apply(induct xs arbitrary:ys) apply simp
    4.29 +apply(case_tac ys)
    4.30 +apply simp_all
    4.31 +done
    4.32 +
    4.33 +lemma map_zip_map2:
    4.34 + "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
    4.35 +apply(induct xs arbitrary:ys) apply simp
    4.36 +apply(case_tac ys)
    4.37 +apply simp_all
    4.38 +done
    4.39 +
    4.40  lemma nth_zip [simp]:
    4.41  "!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
    4.42  apply (induct ys, simp)
    4.43 @@ -1618,6 +1637,12 @@
    4.44  lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
    4.45  by (induct xs) auto
    4.46  
    4.47 +lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
    4.48 +by(induct xs) simp_all
    4.49 +
    4.50 +lemma foldl_map: "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
    4.51 +by(induct xs arbitrary:a) simp_all
    4.52 +
    4.53  lemma foldl_cong [fundef_cong, recdef_cong]:
    4.54    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
    4.55    ==> foldl f a l = foldl g b k"
    4.56 @@ -1628,6 +1653,19 @@
    4.57    ==> foldr f l a = foldr g k b"
    4.58    by (induct k arbitrary: a b l) simp_all
    4.59  
    4.60 +text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
    4.61 +
    4.62 +lemma foldl_foldr1_lemma:
    4.63 + "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
    4.64 +by (induct xs arbitrary: a) (auto simp:add_assoc)
    4.65 +
    4.66 +corollary foldl_foldr1:
    4.67 + "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
    4.68 +by (simp add:foldl_foldr1_lemma)
    4.69 +
    4.70 +
    4.71 +text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
    4.72 +
    4.73  lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
    4.74  by (induct xs) auto
    4.75  
    4.76 @@ -1649,6 +1687,37 @@
    4.77  "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
    4.78  by (induct ns) auto
    4.79  
    4.80 +subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    4.81 +
    4.82 +lemma listsum_foldr:
    4.83 + "listsum xs = foldr (op +) xs 0"
    4.84 +by(induct xs) auto
    4.85 +
    4.86 +(* for efficient code generation *)
    4.87 +lemma listsum[code]: "listsum xs = foldl (op +) 0 xs"
    4.88 +by(simp add:listsum_foldr foldl_foldr1)
    4.89 +
    4.90 +text{* Some syntactic sugar for summing a function over a list: *}
    4.91 +
    4.92 +syntax
    4.93 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    4.94 +syntax (xsymbols)
    4.95 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    4.96 +syntax (HTML output)
    4.97 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    4.98 +
    4.99 +translations -- {* Beware of argument permutation! *}
   4.100 +  "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
   4.101 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
   4.102 +
   4.103 +lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
   4.104 +by (induct xs) simp_all
   4.105 +
   4.106 +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
   4.107 +lemma uminus_listsum_map:
   4.108 + "- listsum (map f xs) = (listsum (map (uminus o f) xs) :: 'a::ab_group_add)"
   4.109 +by(induct xs) simp_all
   4.110 +
   4.111  
   4.112  subsubsection {* @{text upto} *}
   4.113  
   4.114 @@ -2763,6 +2832,7 @@
   4.115    "map_filter f P (x#xs) =
   4.116       (if P x then f x # map_filter f P xs else map_filter f P xs)"
   4.117  
   4.118 +
   4.119  text {*
   4.120    Only use @{text mem} for generating executable code.  Otherwise use
   4.121    @{prop "x : set xs"} instead --- it is much easier to reason about.
   4.122 @@ -2850,8 +2920,11 @@
   4.123    "map_filter f P xs = map f (filter P xs)"
   4.124    by (induct xs) auto
   4.125  
   4.126 -
   4.127 -text {* code for bounded quantification over nats *}
   4.128 +lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
   4.129 +by(simp add:listsum_foldr foldl_map[symmetric] foldl_foldr1)
   4.130 +
   4.131 +
   4.132 +text {* Code for bounded quantification over nats. *}
   4.133  
   4.134  lemma atMost_upto [code unfold]:
   4.135    "{..n} = set [0..n]"
     5.1 --- a/src/HOL/Real/RealPow.thy	Thu May 24 16:52:54 2007 +0200
     5.2 +++ b/src/HOL/Real/RealPow.thy	Thu May 24 22:55:53 2007 +0200
     5.3 @@ -149,7 +149,7 @@
     5.4  lemma sum_squares_eq_zero_iff:
     5.5    fixes x y :: "'a::ordered_ring_strict"
     5.6    shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
     5.7 -by (simp add: sum_nonneg_eq_zero_iff zero_le_square)
     5.8 +by (simp add: sum_nonneg_eq_zero_iff)
     5.9  
    5.10  lemma sum_squares_le_zero_iff:
    5.11    fixes x y :: "'a::ordered_ring_strict"