neuper@42164: theory Test_Complex imports Isac begin
neuper@42164: 
neuper@42164: section {*terms and operations*}
neuper@42160: ML {*
jan@42207:   print_depth 999; @{term "Complex 1 (2::real)"};
neuper@42160: *}
neuper@42160: ML {*
neuper@42160: @{term "Complex 1 2 + Complex 3 4"};
Walther@60566: print_depth 999; TermC.parse_test @{context} "Complex 1 2 + Complex 3 4"; print_depth 999;
neuper@42185: *}
neuper@42185: ML {*
neuper@42160: @{term "Complex 1 2 * Complex 3 4"};
neuper@42160: @{term "Complex 1 2 - Complex 3 4"};
neuper@42160: @{term "Complex 1 2 / Complex 3 4"};
neuper@42164: (*@{term "Complex 1 2 ^ Complex 3 4"};
neuper@42164:   Type unification failed: Clash of types "complex" and "nat"
neuper@42164:   Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
neuper@42164:   Operand:   Complex 3 4 :: complex*)
neuper@42160: *}
neuper@42160: ML {*
neuper@42164: term2str @{term "Complex 1 2 + Complex 3 4"};
neuper@42164: term2str @{term "Complex 1 2 / Complex 3 4"};
neuper@42164: *}
neuper@42164: 
neuper@42164: ML {*
neuper@42160: val a = @{term "Complex 1 2"};
Walther@60650: TermC.atom_trace_detail @{context} a;
Walther@60566: val a = TermC.parse_test @{context} "Complex 1 2";
Walther@60650: TermC.atom_trace_detail @{context} a;
neuper@42185: *}
neuper@42185: ML {*
neuper@42160: val b = @{term "Complex 3 4"};
Walther@60566: val b = TermC.parse_test @{context} "Complex 3 4";
neuper@42160: (*a + (b::complex); ERROR: term + term*)
neuper@42160: *}
neuper@42164: 
neuper@42164: section {*use the operations for simplification*}
jan@42207: 
jan@42207: 
jan@42207: 
jan@42207: subsection {*example 1 -- ADD*}
neuper@42160: ML {*
jan@42207:   print_depth 1;
jan@42207:   val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
neuper@42160: *}
neuper@42160: ML {*
jan@42207:   val thm = @{thm "complex_add"};
Walther@60566:   val t = TermC.parse_test @{context} "Complex 1 2 + Complex 3 4";
jan@42207:   val SOME _ = rewrite_ thy ro er true thm t;
jan@42207:   val SOME (t', _) = rewrite_ thy ro er true thm t;
jan@42207:   "Complex (1 + 3) (2 + 4)" = term2str t';
neuper@42164: *}
neuper@42164: 
jan@42207: 
jan@42207: 
jan@42207: 
jan@42207: subsection {*example 2 -- ADD, MULT*}
neuper@42164: ML {*
jan@42207: 
neuper@42185: val Simplify_complex = append_rls "Simplify_complex" e_rls
neuper@42164:   [ Thm  ("complex_add",num_str @{thm complex_add}),
neuper@42185: 		    Thm  ("complex_mult",num_str @{thm complex_mult}),
neuper@42185: 		    Rls_ norm_Poly
neuper@42164: 		  ];
jan@42207: 
neuper@42164: *}
neuper@42164: ML {*
jan@42207: 
Walther@60566: val t = TermC.parse_test @{context} "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
neuper@42185: term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
Walther@60650: TermC.atom_trace_detail @{context} t;
jan@42207: 
jan@42207: *}
jan@42207: ML {*
jan@42207: 
jan@42207: 
jan@42207: val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
jan@42207: 
jan@42207: term2str t = "Complex -12 26";
Walther@60650: TermC.atom_trace_detail @{context} t;
jan@42207: 
jan@42207: *}
jan@42207: 
jan@42207: subsection {*example 3*}
jan@42207: ML {*
jan@42207: val Simplify_complex = append_rls "Simplify_complex" e_rls
jan@42207:   [ Thm  ("complex_mult",num_str @{thm complex_mult}),
jan@42207:     Thm  ("complex_inverse",num_str @{thm complex_inverse}),
jan@42207: 		    Rls_ norm_Poly
jan@42207: 		  ];
jan@42207: *}
jan@42207: ML {*
Walther@60566: val t = TermC.parse_test @{context} "inverse (Complex (2::real) (4::real))";
jan@42207: term2str t = "inverse Complex (2) (4)";
Walther@60650: TermC.atom_trace_detail @{context} t;
neuper@42164: *}
neuper@42164: ML {*
neuper@42185: trace_rewrite := true;
neuper@42164: val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
neuper@42185: trace_rewrite := false;
neuper@42185: term2str t = "Complex -12 26";
Walther@60650: TermC.atom_trace_detail @{context} t;
neuper@42164: *}
neuper@42185: 
jan@42207: 
jan@42207: 
neuper@42164: ML {*
neuper@42185: trace_rewrite := true;
neuper@42185: trace_rewrite := false;
neuper@42160: *}
neuper@42160: 
neuper@42160: end
neuper@42160: