Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/ex/NatSum.thy
changeset 76213 e44d86131648
parent 65449 c82e63b11b8b
child 76214 0c18df79b1c8 
--- a/src/ZF/ex/NatSum.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/ex/NatSum.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -12,7 +12,7 @@
   thanks to new simprocs.
 
 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
-  http://www.research.att.com/~njas/sequences/
+  http://www.research.att.com/\<not>njas/sequences/
 *)
 
 
@@ -27,41 +27,41 @@
 declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp]
 
 (*The sum of the first n odd numbers equals n squared.*)
-lemma sum_of_odds: "n \<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n"
+lemma sum_of_odds: "n \<in> nat \<Longrightarrow> sum (%i. i $+ i $+ #1, n) = $#n $* $#n"
 by (induct_tac "n", auto)
 
 (*The sum of the first n odd squares*)
 lemma sum_of_odd_squares:
-     "n \<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) =  
+     "n \<in> nat \<Longrightarrow> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) =  
       $#n $* (#4 $* $#n $* $#n $- #1)"
 by (induct_tac "n", auto)
 
 (*The sum of the first n odd cubes*)
 lemma sum_of_odd_cubes:
      "n \<in> nat  
-      ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) =  
+      \<Longrightarrow> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) =  
           $#n $* $#n $* (#2 $* $#n $* $#n $- #1)"
 by (induct_tac "n", auto)
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
 lemma sum_of_naturals:
-     "n \<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)"
+     "n \<in> nat \<Longrightarrow> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)"
 by (induct_tac "n", auto)
 
 lemma sum_of_squares:
-     "n \<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) =  
+     "n \<in> nat \<Longrightarrow> #6 $* sum (%i. i$*i, succ(n)) =  
                   $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)"
 by (induct_tac "n", auto)
 
 lemma sum_of_cubes:
-     "n \<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) =  
+     "n \<in> nat \<Longrightarrow> #4 $* sum (%i. i$*i$*i, succ(n)) =  
                   $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)"
 by (induct_tac "n", auto)
 
 (** Sum of fourth powers **)
 
 lemma sum_of_fourth_powers:
-     "n \<in> nat ==> #30 $* sum (%i. i$*i$*i$*i, succ(n)) =  
+     "n \<in> nat \<Longrightarrow> #30 $* sum (%i. i$*i$*i$*i, succ(n)) =  
                     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $*  
                     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)"
 by (induct_tac "n", auto)
isabelle