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; TermC.parse_test @{context} "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"};

TermC.atom_trace_detail @{context} a;

val a = TermC.parse_test @{context} "Complex 1 2";

TermC.atom_trace_detail @{context} a;

*}

ML {*

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

val b = TermC.parse_test @{context} "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 = TermC.parse_test @{context} "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 = TermC.parse_test @{context} "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";

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

TermC.atom_trace_detail @{context} t;

*}

ML {*

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

term2str t = "Complex -12 26";

TermC.atom_trace_detail @{context} 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 = TermC.parse_test @{context} "inverse (Complex (2::real) (4::real))";

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

TermC.atom_trace_detail @{context} t;

*}

ML {*

trace_rewrite := true;

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

trace_rewrite := false;

term2str t = "Complex -12 26";

TermC.atom_trace_detail @{context} t;

*}

ML {*

trace_rewrite := true;

trace_rewrite := false;

*}

end