theory Test_Complex imports Isac begin

 section {*terms and operations*}

 ML {*

   print_depth 999; @{term "Complex 1 (2::real)"};

 *}

 ML {*

 @{term "Complex 1 2 + Complex 3 4"};

 print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;

 *}

 ML {*

 @{term "Complex 1 2 * Complex 3 4"};

 @{term "Complex 1 2 - Complex 3 4"};

 @{term "Complex 1 2 / Complex 3 4"};

 (*@{term "Complex 1 2 ^ Complex 3 4"};

   Type unification failed: Clash of types "complex" and "nat"

   Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex

   Operand:   Complex 3 4 :: complex*)

 *}

 ML {*

 term2str @{term "Complex 1 2 + Complex 3 4"};

 term2str @{term "Complex 1 2 / Complex 3 4"};

 *}

 ML {*

 val a = @{term "Complex 1 2"};

 atomty a;

 val a = str2term "Complex 1 2";

 atomty a;

 *}

 ML {*

 val b = @{term "Complex 3 4"};

 val b = str2term "Complex 3 4";

 (*a + (b::complex); ERROR: term + term*)

 *}

 section {*use the operations for simplification*}

 subsection {*example 1 -- ADD*}

 ML {*

   print_depth 1;

   val (thy, ro, er) = (@{theory}, tless_true, eval_rls);

 *}

 ML {*

   val thm = @{thm "complex_add"};

   val t = str2term "Complex 1 2 + Complex 3 4";

   val SOME _ = rewrite_ thy ro er true thm t;

   val SOME (t', _) = rewrite_ thy ro er true thm t;

   "Complex (1 + 3) (2 + 4)" = term2str t';

 *}

 subsection {*example 2 -- ADD, MULT*}

 ML {*

 val Simplify_complex = append_rls "Simplify_complex" e_rls

   [ Thm  ("complex_add",num_str @{thm complex_add}),

 		    Thm  ("complex_mult",num_str @{thm complex_mult}),

 		    Rls_ norm_Poly

 		  ];

 *}

 ML {*

 val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";

 term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";

 atomty t;

 *}

 ML {*

 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;

 term2str t = "Complex -12 26";

 atomty t;

 *}

 subsection {*example 3*}

 ML {*

 val Simplify_complex = append_rls "Simplify_complex" e_rls

   [ Thm  ("complex_mult",num_str @{thm complex_mult}),

     Thm  ("complex_inverse",num_str @{thm complex_inverse}),

 		    Rls_ norm_Poly

 		  ];

 *}

 ML {*

 val t = str2term "inverse (Complex (2::real) (4::real))";

 term2str t = "inverse Complex (2) (4)";

 atomty t;

 *}

 ML {*

 trace_rewrite := true;

 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;

 trace_rewrite := false;

 term2str t = "Complex -12 26";

 atomty t;

 *}

 ML {*

 trace_rewrite := true;

 trace_rewrite := false;

 *}

 end