1.1 --- a/doc-src/isac/jrocnik/Test_Complex.thy	Tue Jul 26 09:53:53 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy	Wed Jul 27 08:00:24 2011 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  
     1.5  section {*terms and operations*}
     1.6  ML {*
     1.7 -print_depth 999; @{term "Complex 1 (2::real)"};
     1.8 +  print_depth 999; @{term "Complex 1 (2::real)"};
     1.9  *}
    1.10  ML {*
    1.11  @{term "Complex 1 2 + Complex 3 4"};
    1.12 @@ -35,31 +35,64 @@
    1.13  *}
    1.14  
    1.15  section {*use the operations for simplification*}
    1.16 -subsection {*example 1*}
    1.17 +
    1.18 +
    1.19 +
    1.20 +subsection {*example 1 -- ADD*}
    1.21  ML {*
    1.22 -print_depth 1;
    1.23 -val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    1.24 +  print_depth 1;
    1.25 +  val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    1.26  *}
    1.27  ML {*
    1.28 -val thm = @{thm "complex_add"};
    1.29 -val t = str2term "Complex 1 2 + Complex 3 4";
    1.30 -val SOME _ = rewrite_ thy ro er true thm t;
    1.31 -val SOME (t', _) = rewrite_ thy ro er true thm t;
    1.32 -"Complex (1 + 3) (2 + 4)" = term2str t';
    1.33 +  val thm = @{thm "complex_add"};
    1.34 +  val t = str2term "Complex 1 2 + Complex 3 4";
    1.35 +  val SOME _ = rewrite_ thy ro er true thm t;
    1.36 +  val SOME (t', _) = rewrite_ thy ro er true thm t;
    1.37 +  "Complex (1 + 3) (2 + 4)" = term2str t';
    1.38  *}
    1.39  
    1.40 -subsection {*example 2*}
    1.41 +
    1.42 +
    1.43 +
    1.44 +subsection {*example 2 -- ADD, MULT*}
    1.45  ML {*
    1.46 +
    1.47  val Simplify_complex = append_rls "Simplify_complex" e_rls
    1.48    [ Thm  ("complex_add",num_str @{thm complex_add}),
    1.49  		    Thm  ("complex_mult",num_str @{thm complex_mult}),
    1.50  		    Rls_ norm_Poly
    1.51  		  ];
    1.52 +
    1.53  *}
    1.54  ML {*
    1.55 +
    1.56  val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
    1.57  term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
    1.58  atomty t;
    1.59 +
    1.60 +*}
    1.61 +ML {*
    1.62 +
    1.63 +
    1.64 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    1.65 +
    1.66 +term2str t = "Complex -12 26";
    1.67 +atomty t;
    1.68 +
    1.69 +*}
    1.70 +
    1.71 +subsection {*example 3*}
    1.72 +ML {*
    1.73 +val Simplify_complex = append_rls "Simplify_complex" e_rls
    1.74 +  [ Thm  ("complex_mult",num_str @{thm complex_mult}),
    1.75 +    Thm  ("complex_inverse",num_str @{thm complex_inverse}),
    1.76 +		    Rls_ norm_Poly
    1.77 +		  ];
    1.78 +*}
    1.79 +ML {*
    1.80 +val t = str2term "inverse (Complex (2::real) (4::real))";
    1.81 +term2str t = "inverse Complex (2) (4)";
    1.82 +atomty t;
    1.83  *}
    1.84  ML {*
    1.85  trace_rewrite := true;
    1.86 @@ -68,9 +101,9 @@
    1.87  term2str t = "Complex -12 26";
    1.88  atomty t;
    1.89  *}
    1.90 -ML {*
    1.91  
    1.92 -*}
    1.93 +
    1.94 +
    1.95  ML {*
    1.96  trace_rewrite := true;
    1.97  trace_rewrite := false;