# HG changeset patch
# User paulson
# Date 1054111700 -7200
# Node ID 4b61bbb0dcab35cb0a34310ea5aa6b51259e9057
# Parent  826037db30cdbfc7ad344fb85415640b99ad02f0
examples now use Complex_Main

diff -r 826037db30cd -r 4b61bbb0dcab src/HOL/Complex/ex/BinEx.thy
--- a/src/HOL/Complex/ex/BinEx.thy	Wed May 28 10:47:54 2003 +0200
+++ b/src/HOL/Complex/ex/BinEx.thy	Wed May 28 10:48:20 2003 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Real/ex/BinEx.thy
+(*  Title:      HOL/Complex/ex/BinEx.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
@@ -6,14 +6,16 @@
 
 header {* Binary arithmetic examples *}
 
-theory BinEx = Real:
+theory BinEx = Complex_Main:
 
 text {*
-  Examples of performing binary arithmetic by simplification This time
+  Examples of performing binary arithmetic by simplification.  This time
   we use the reals, though the representation is just of integers.
 *}
 
-text {* \medskip Addition *}
+subsection{*Real Arithmetic*}
+
+subsubsection {*Addition *}
 
 lemma "(1359::real) + -2468 = -1109"
   by simp
@@ -22,7 +24,7 @@
   by simp
 
 
-text {* \medskip Negation *}
+subsubsection {*Negation *}
 
 lemma "- (65745::real) = -65745"
   by simp
@@ -31,7 +33,7 @@
   by simp
 
 
-text {* \medskip Multiplication *}
+subsubsection {*Multiplication *}
 
 lemma "(-84::real) * 51 = -4284"
   by simp
@@ -43,7 +45,7 @@
   by simp
 
 
-text {* \medskip Inequalities *}
+subsubsection {*Inequalities *}
 
 lemma "(89::real) * 10 \<noteq> 889"
   by simp
@@ -64,7 +66,7 @@
   by simp
 
 
-text {* \medskip Powers *}
+subsubsection {*Powers *}
 
 lemma "2 ^ 15 = (32768::real)"
   by simp
@@ -82,7 +84,7 @@
   by simp
 
 
-text {* \medskip Tests *}
+subsubsection {*Tests *}
 
 lemma "(x + y = x) = (y = (0::real))"
   by arith
@@ -367,4 +369,34 @@
     ==> 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"
   by (tactic "fast_arith_tac 1")
 
+
+subsection{*Complex Arithmetic*}
+
+lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
+  by simp
+
+lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
+  by simp
+
+text{*Multiplication requires distributive laws.  Perhaps versions instantiated
+to literal constants should be added to the simpset.*}
+
+lemmas distrib = complex_add_mult_distrib complex_add_mult_distrib2
+                 complex_diff_mult_distrib complex_diff_mult_distrib2
+
+lemma "(1 + ii) * (1 - ii) = 2"
+by (simp add: distrib)
+
+lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
+by (simp add: distrib)
+
+lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
+by (simp add: distrib)
+
+text{*No inequalities: we have no ordering on the complex numbers.*}
+
+text{*No powers (not supported yet)*}
+
+text{*No linear arithmetic*}
+
 end
diff -r 826037db30cd -r 4b61bbb0dcab src/HOL/Complex/ex/NSPrimes.thy
--- a/src/HOL/Complex/ex/NSPrimes.thy	Wed May 28 10:47:54 2003 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Wed May 28 10:48:20 2003 +0200
@@ -8,7 +8,7 @@
 considering a property of nonstandard sets.
 *)
 
-NSPrimes = Factorization + HSeries +
+NSPrimes = Factorization + Complex_Main +
 
 consts
   hdvd  :: [hypnat, hypnat] => bool       (infixl 50) 
diff -r 826037db30cd -r 4b61bbb0dcab src/HOL/Complex/ex/Sqrt.thy
--- a/src/HOL/Complex/ex/Sqrt.thy	Wed May 28 10:47:54 2003 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy	Wed May 28 10:48:20 2003 +0200
@@ -6,7 +6,7 @@
 
 header {*  Square roots of primes are irrational *}
 
-theory Sqrt = Primes + Hyperreal:
+theory Sqrt = Primes + Complex_Main:
 
 subsection {* Preliminaries *}
 
diff -r 826037db30cd -r 4b61bbb0dcab src/HOL/Complex/ex/Sqrt_Script.thy
--- a/src/HOL/Complex/ex/Sqrt_Script.thy	Wed May 28 10:47:54 2003 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Wed May 28 10:48:20 2003 +0200
@@ -6,7 +6,7 @@
 
 header {* Square roots of primes are irrational (script version) *}
 
-theory Sqrt_Script = Primes + Hyperreal:
+theory Sqrt_Script = Primes + Complex_Main:
 
 text {*
   \medskip Contrast this linear Isabelle/Isar script with Markus