1.1 --- a/src/HOL/Complex/ex/BinEx.thy	Wed May 28 10:47:54 2003 +0200
     1.2 +++ b/src/HOL/Complex/ex/BinEx.thy	Wed May 28 10:48:20 2003 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Real/ex/BinEx.thy
     1.5 +(*  Title:      HOL/Complex/ex/BinEx.thy
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1999  University of Cambridge
     1.9 @@ -6,14 +6,16 @@
    1.10  
    1.11  header {* Binary arithmetic examples *}
    1.12  
    1.13 -theory BinEx = Real:
    1.14 +theory BinEx = Complex_Main:
    1.15  
    1.16  text {*
    1.17 -  Examples of performing binary arithmetic by simplification This time
    1.18 +  Examples of performing binary arithmetic by simplification.  This time
    1.19    we use the reals, though the representation is just of integers.
    1.20  *}
    1.21  
    1.22 -text {* \medskip Addition *}
    1.23 +subsection{*Real Arithmetic*}
    1.24 +
    1.25 +subsubsection {*Addition *}
    1.26  
    1.27  lemma "(1359::real) + -2468 = -1109"
    1.28    by simp
    1.29 @@ -22,7 +24,7 @@
    1.30    by simp
    1.31  
    1.32  
    1.33 -text {* \medskip Negation *}
    1.34 +subsubsection {*Negation *}
    1.35  
    1.36  lemma "- (65745::real) = -65745"
    1.37    by simp
    1.38 @@ -31,7 +33,7 @@
    1.39    by simp
    1.40  
    1.41  
    1.42 -text {* \medskip Multiplication *}
    1.43 +subsubsection {*Multiplication *}
    1.44  
    1.45  lemma "(-84::real) * 51 = -4284"
    1.46    by simp
    1.47 @@ -43,7 +45,7 @@
    1.48    by simp
    1.49  
    1.50  
    1.51 -text {* \medskip Inequalities *}
    1.52 +subsubsection {*Inequalities *}
    1.53  
    1.54  lemma "(89::real) * 10 \<noteq> 889"
    1.55    by simp
    1.56 @@ -64,7 +66,7 @@
    1.57    by simp
    1.58  
    1.59  
    1.60 -text {* \medskip Powers *}
    1.61 +subsubsection {*Powers *}
    1.62  
    1.63  lemma "2 ^ 15 = (32768::real)"
    1.64    by simp
    1.65 @@ -82,7 +84,7 @@
    1.66    by simp
    1.67  
    1.68  
    1.69 -text {* \medskip Tests *}
    1.70 +subsubsection {*Tests *}
    1.71  
    1.72  lemma "(x + y = x) = (y = (0::real))"
    1.73    by arith
    1.74 @@ -367,4 +369,34 @@
    1.75      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
    1.76    by (tactic "fast_arith_tac 1")
    1.77  
    1.78 +
    1.79 +subsection{*Complex Arithmetic*}
    1.80 +
    1.81 +lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
    1.82 +  by simp
    1.83 +
    1.84 +lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
    1.85 +  by simp
    1.86 +
    1.87 +text{*Multiplication requires distributive laws.  Perhaps versions instantiated
    1.88 +to literal constants should be added to the simpset.*}
    1.89 +
    1.90 +lemmas distrib = complex_add_mult_distrib complex_add_mult_distrib2
    1.91 +                 complex_diff_mult_distrib complex_diff_mult_distrib2
    1.92 +
    1.93 +lemma "(1 + ii) * (1 - ii) = 2"
    1.94 +by (simp add: distrib)
    1.95 +
    1.96 +lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
    1.97 +by (simp add: distrib)
    1.98 +
    1.99 +lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
   1.100 +by (simp add: distrib)
   1.101 +
   1.102 +text{*No inequalities: we have no ordering on the complex numbers.*}
   1.103 +
   1.104 +text{*No powers (not supported yet)*}
   1.105 +
   1.106 +text{*No linear arithmetic*}
   1.107 +
   1.108  end

     2.1 --- a/src/HOL/Complex/ex/NSPrimes.thy	Wed May 28 10:47:54 2003 +0200
     2.2 +++ b/src/HOL/Complex/ex/NSPrimes.thy	Wed May 28 10:48:20 2003 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  considering a property of nonstandard sets.
     2.5  *)
     2.6  
     2.7 -NSPrimes = Factorization + HSeries +
     2.8 +NSPrimes = Factorization + Complex_Main +
     2.9  
    2.10  consts
    2.11    hdvd  :: [hypnat, hypnat] => bool       (infixl 50) 

     3.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Wed May 28 10:47:54 2003 +0200
     3.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Wed May 28 10:48:20 2003 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  header {*  Square roots of primes are irrational *}
     3.6  
     3.7 -theory Sqrt = Primes + Hyperreal:
     3.8 +theory Sqrt = Primes + Complex_Main:
     3.9  
    3.10  subsection {* Preliminaries *}
    3.11  

     4.1 --- a/src/HOL/Complex/ex/Sqrt_Script.thy	Wed May 28 10:47:54 2003 +0200
     4.2 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Wed May 28 10:48:20 2003 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  header {* Square roots of primes are irrational (script version) *}
     4.6  
     4.7 -theory Sqrt_Script = Primes + Hyperreal:
     4.8 +theory Sqrt_Script = Primes + Complex_Main:
     4.9  
    4.10  text {*
    4.11    \medskip Contrast this linear Isabelle/Isar script with Markus