1.1 --- a/doc-src/isac/jrocnik/Test_Complex.thy	Fri Jul 22 10:26:39 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy	Fri Jul 22 12:10:13 2011 +0200
     1.3 @@ -1,33 +1,61 @@
     1.4 -(* theory Test_Complex imports Isac begin
     1.5 -ERROR TODO                     ^^^^:
     1.6 +theory Test_Complex imports Isac begin
     1.7 +
     1.8 +section {*terms and operations*}
     1.9  ML {*
    1.10 -@{term "Complex 1 2 ^ Complex 3 4"};
    1.11 +print_depth 999; @{term "Complex 1 (2::real)"};
    1.12  *}
    1.13 -Type unification failed: Clash of types "complex" and "nat"
    1.14 -Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
    1.15 -Operand:   Complex 3 4 :: complex
    1.16 -*)
    1.17 -
    1.18 -theory Test_Complex imports Main begin
    1.19 -
    1.20  ML {*
    1.21 -@{term "Complex 1 2"};
    1.22  @{term "Complex 1 2 + Complex 3 4"};
    1.23  @{term "Complex 1 2 * Complex 3 4"};
    1.24  @{term "Complex 1 2 - Complex 3 4"};
    1.25  @{term "Complex 1 2 / Complex 3 4"};
    1.26 -@{term "Complex 1 2 ^ Complex 3 4"};
    1.27 +(*@{term "Complex 1 2 ^ Complex 3 4"};
    1.28 +  Type unification failed: Clash of types "complex" and "nat"
    1.29 +  Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
    1.30 +  Operand:   Complex 3 4 :: complex*)
    1.31  *}
    1.32  ML {*
    1.33 +term2str @{term "Complex 1 2 + Complex 3 4"};
    1.34 +term2str @{term "Complex 1 2 / Complex 3 4"};
    1.35 +*}
    1.36 +
    1.37 +ML {*
    1.38  val a = @{term "Complex 1 2"};
    1.39  val b = @{term "Complex 3 4"};
    1.40  (*a + (b::complex); ERROR: term + term*)
    1.41  *}
    1.42 +
    1.43 +section {*use the operations for simplification*}
    1.44 +subsection {*example 1*}
    1.45  ML {*
    1.46 -@{term "let a = Complex 1 2; b = Complex 3 4 in a + b"};
    1.47 +print_depth 1;
    1.48 +val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    1.49  *}
    1.50  ML {*
    1.51 -(*TODO rules for simplification*)
    1.52 +val thm = @{thm "complex_add"};
    1.53 +val t = @{term "Complex 1 2 + Complex 3 4"};
    1.54 +val SOME _ = rewrite_ thy ro er true thm t;
    1.55 +val SOME (t', _) = rewrite_ thy ro er true thm t;
    1.56 +"Complex (1 + 3) (2 + 4)" = term2str t';
    1.57 +*}
    1.58 +
    1.59 +subsection {*example 2*}
    1.60 +ML {*
    1.61 +val Simplify_complex = append_rls "Simplify_complex" norm_Poly
    1.62 +  [ Thm  ("complex_add",num_str @{thm complex_add}),
    1.63 +		    Thm  ("complex_mult",num_str @{thm complex_mult})
    1.64 +		  ];
    1.65 +*}
    1.66 +ML {*
    1.67 +val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};
    1.68 +*}
    1.69 +ML {*
    1.70 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    1.71 +*}
    1.72 +ML {*
    1.73 +term2str t
    1.74 +*}
    1.75 +ML {*
    1.76  *}
    1.77  
    1.78  end