src/HOL/Complex/ex/BinEx.thy
 changeset 14051 4b61bbb0dcab parent 13966 2160abf7cfe7 child 14373 67a628beb981
```     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.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.91 +                 complex_diff_mult_distrib complex_diff_mult_distrib2
1.92 +
1.93 +lemma "(1 + ii) * (1 - ii) = 2"
1.95 +
1.96 +lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"