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"};

@{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"};

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

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

*}

section {*use the operations for simplification*}

subsection {*example 1*}

ML {*

print_depth 1;

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

*}

ML {*

val thm = @{thm "complex_add"};

val t = @{term "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*}

ML {*

val Simplify_complex = append_rls "Simplify_complex" norm_Poly

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

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

		  ];

*}

ML {*

val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};

*}

ML {*

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

*}

ML {*

term2str t

*}

ML {*

*}

end