1.1 --- a/doc-src/isac/jrocnik/Test_Complex.thy	Mon Jul 25 14:19:50 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy	Mon Jul 25 17:44:19 2011 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  *}
     1.5  ML {*
     1.6  @{term "Complex 1 2 + Complex 3 4"};
     1.7 +print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
     1.8 +*}
     1.9 +ML {*
    1.10  @{term "Complex 1 2 * Complex 3 4"};
    1.11  @{term "Complex 1 2 - Complex 3 4"};
    1.12  @{term "Complex 1 2 / Complex 3 4"};
    1.13 @@ -21,7 +24,13 @@
    1.14  
    1.15  ML {*
    1.16  val a = @{term "Complex 1 2"};
    1.17 +atomty a;
    1.18 +val a = str2term "Complex 1 2";
    1.19 +atomty a;
    1.20 +*}
    1.21 +ML {*
    1.22  val b = @{term "Complex 3 4"};
    1.23 +val b = str2term "Complex 3 4";
    1.24  (*a + (b::complex); ERROR: term + term*)
    1.25  *}
    1.26  
    1.27 @@ -33,7 +42,7 @@
    1.28  *}
    1.29  ML {*
    1.30  val thm = @{thm "complex_add"};
    1.31 -val t = @{term "Complex 1 2 + Complex 3 4"};
    1.32 +val t = str2term "Complex 1 2 + Complex 3 4";
    1.33  val SOME _ = rewrite_ thy ro er true thm t;
    1.34  val SOME (t', _) = rewrite_ thy ro er true thm t;
    1.35  "Complex (1 + 3) (2 + 4)" = term2str t';
    1.36 @@ -41,21 +50,30 @@
    1.37  
    1.38  subsection {*example 2*}
    1.39  ML {*
    1.40 -val Simplify_complex = append_rls "Simplify_complex" norm_Poly
    1.41 +val Simplify_complex = append_rls "Simplify_complex" e_rls
    1.42    [ Thm  ("complex_add",num_str @{thm complex_add}),
    1.43 -		    Thm  ("complex_mult",num_str @{thm complex_mult})
    1.44 +		    Thm  ("complex_mult",num_str @{thm complex_mult}),
    1.45 +		    Rls_ norm_Poly
    1.46  		  ];
    1.47  *}
    1.48  ML {*
    1.49 -val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};
    1.50 +val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
    1.51 +term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
    1.52 +atomty t;
    1.53  *}
    1.54  ML {*
    1.55 +trace_rewrite := true;
    1.56  val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    1.57 +trace_rewrite := false;
    1.58 +term2str t = "Complex -12 26";
    1.59 +atomty t;
    1.60  *}
    1.61  ML {*
    1.62 -term2str t
    1.63 +
    1.64  *}
    1.65  ML {*
    1.66 +trace_rewrite := true;
    1.67 +trace_rewrite := false;
    1.68  *}
    1.69  
    1.70  end

     2.1 --- a/doc-src/isac/jrocnik/Test_Z_Transform.thy	Mon Jul 25 14:19:50 2011 +0200
     2.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy	Mon Jul 25 17:44:19 2011 +0200
     2.3 @@ -42,11 +42,9 @@
     2.4  (*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
     2.5  (*definition     "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
     2.6  axioms 
     2.7 -  rule1: "\<forall>x. \<delta>[n] = 1"
     2.8 -  rule3: "1 < || z || ==> z / (z - 1) = -u [-n - 1]"
     2.9 -(*rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha>^n * [n]" 
    2.10 -                            Type unification failed: Clash of types "_ list" and "real"*)
    2.11 -  rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha> * u [n]"
    2.12 +  rule1: "(1::real) = \<delta>[n]"
    2.13 +  rule3: "(1::real) < || z || ==> z / (z - 1) = -u [-n - 1]"
    2.14 +  rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha>^n * u [n]"
    2.15  ML {*
    2.16  @{thm rule1};
    2.17  @{thm rule3};
    2.18 @@ -55,31 +53,43 @@
    2.19  
    2.20  subsection {*apply rules*}
    2.21  ML {*
    2.22 +val inverse_Z = append_rls "inverse_Z" e_rls
    2.23 +  [ Thm  ("rule3",num_str @{thm rule3}),
    2.24 +		    Thm  ("rule4",num_str @{thm rule4}),
    2.25 +    Thm  ("rule1",num_str @{thm rule1})   
    2.26 +		  ];
    2.27 +
    2.28 +val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
    2.29 +val SOME (t', _) = rewrite_set_ thy true inverse_Z t;
    2.30 +term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)
    2.31 +*}
    2.32 +ML {*
    2.33 +val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
    2.34  val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    2.35  *}
    2.36  ML {*
    2.37 -val t = @{term "z / (z - 1) = -u [-n - 1]"};
    2.38 +val SOME (t, _) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
    2.39 +term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
    2.40  *}
    2.41  ML {*
    2.42 -print_depth 999; Pattern.match thy;  print_depth 999
    2.43 +val SOME (t, _) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
    2.44 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^ ?n * ?u [?n] + 1";
    2.45 +*}
    2.46 +ML {*
    2.47 +val SOME (t, _) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
    2.48 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^ ?n * ?u [?n] + ?\<delta> [?n]";
    2.49  *}
    2.50  ML {*
    2.51  *}
    2.52  ML {*
    2.53 -rewrite_ thy ro er true @{thm rule3} t
    2.54  *}
    2.55  ML {*
    2.56  
    2.57  *}
    2.58  ML {*
    2.59 -@{term "LENGTH"};
    2.60 -val t = str2term "LENGTH [x+y=1,y=2] = 2";
    2.61 -
    2.62  *}
    2.63  ML {*
    2.64 -*}
    2.65 -ML {*
    2.66 -@{term "1"};
    2.67 +
    2.68  *}
    2.69  
    2.70  end

     3.1 --- a/test/Tools/isac/Interpret/ctree.sml	Mon Jul 25 14:19:50 2011 +0200
     3.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Mon Jul 25 17:44:19 2011 +0200
     3.3 @@ -17,17 +17,14 @@
     3.4  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
     3.5  "-------------- check positions in miniscript --------------------";
     3.6  "-------------- get_allpos' (from ptree above)--------------------";
     3.7 -(**#####################################################################(**)
     3.8  "-------------- cut_level (from ptree above)----------------------";
     3.9  "-------------- cut_tree (from ptree above)-----------------------";
    3.10  "=====new ptree 1a miniscript with mini-subpbl ===================";
    3.11  "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
    3.12 -(**)#####################################################################**)
    3.13  "=====new ptree 2 miniscript with mini-subpbl ====================";
    3.14  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
    3.15  "-------------- cappend (from ptree above)------------------------";
    3.16  "-------------- cappend minisubpbl -------------------------------";
    3.17 -
    3.18  "=====new ptree 3 ================================================";
    3.19  "-------------- move_dn ------------------------------------------";
    3.20  "-------------- move_dn: Frm -> Res ------------------------------";
    3.21 @@ -35,7 +32,6 @@
    3.22  "------ move into detail -----------------------------------------";
    3.23  "=====new ptree 3a ===============================================";
    3.24  "-------------- move_dn in Incomplete ctree ----------------------";
    3.25 -
    3.26  "=====new ptree 4: crooked by cut_level_'_ =======================";
    3.27  (*############## development stopped 0501 ########################*)
    3.28  (******************************************************************)
    3.29 @@ -46,18 +42,13 @@
    3.30  (*              val get_trace = SAVE_get_trace;                   *)
    3.31  (******************************************************************)
    3.32  (*############## development stopped 0501 ########################*)
    3.33 -
    3.34  "=====new ptree 4 ratequation ====================================";
    3.35  "-------------- pt_extract form, tac, asm<>[] --------------------";
    3.36  "=====new ptree 5 minisubpbl =====================================";
    3.37  "-------------- pt_extract form, tac, asm ------------------------";
    3.38 -
    3.39 -(**#####################################################################(**)
    3.40  "=====new ptree 6 minisubpbl intersteps ==========================";
    3.41  "-------------- get_allpos' new ----------------------------------";
    3.42  "-------------- cut_tree new (from ptree above)-------------------";
    3.43 -(**)#####################################################################**)
    3.44 -
    3.45  "-----------------------------------------------------------------";
    3.46  "-----------------------------------------------------------------";
    3.47  "-----------------------------------------------------------------";
    3.48 @@ -148,8 +139,6 @@
    3.49  
    3.50   show_pt pt;
    3.51  
    3.52 -
    3.53 -
    3.54  "-------------- get_allpos' (from ptree above)--------------------";
    3.55  "-------------- get_allpos' (from ptree above)--------------------";
    3.56  "-------------- get_allpos' (from ptree above)--------------------";
    3.57 @@ -213,8 +202,6 @@
    3.58  then () else error "ctree.sml: diff:behav. in get_allpos' 6";
    3.59  
    3.60  
    3.61 -(**##############################################################(**)
    3.62 -
    3.63  "-------------- cut_level (from ptree above)----------------------";
    3.64  "-------------- cut_level (from ptree above)----------------------";
    3.65  "-------------- cut_level (from ptree above)----------------------";
    3.66 @@ -387,6 +374,9 @@
    3.67   val ((pt,_),_) = get_calc 1;
    3.68   show_pt pt;
    3.69  
    3.70 +if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
    3.71 +else error "mini-subpbl interSteps broken";
    3.72 +
    3.73  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
    3.74  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
    3.75  "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Jul 25 17:44:19 2011 +0200
     4.3 @@ -0,0 +1,71 @@
     4.4 +(* Title: tests for ListC
     4.5 +   Author: Walther Neuper 030501
     4.6 +   (c) copyright due to lincense terms.
     4.7 +*)
     4.8 +
     4.9 +
    4.10 +
    4.11 +"--------------------- nth_ ----------------------------------------------";
    4.12 +"--------------------- nth_ ----------------------------------------------";
    4.13 +"--------------------- nth_ ----------------------------------------------";
    4.14 +val t = str2term "nth_ 3 [a,b,c,d,e]";
    4.15 +atomty t;
    4.16 +val thm = (#prop o rep_thm o num_str) nth_Cons_;
    4.17 +atomty thm;
    4.18 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;
    4.19 +if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
    4.20 +else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
    4.21 +
    4.22 +val t = str2term "nth_ 1 [a,b,c,d,e]";
    4.23 +atomty t;
    4.24 +val thm = (#prop o rep_thm o num_str) nth_Nil_;
    4.25 +atomty thm;
    4.26 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Nil_}) t;
    4.27 +term2str t';
    4.28 +"a";
    4.29 +
    4.30 +val t = str2term "nth_ 3 [a,b,c,d,e]";
    4.31 +atomty t;
    4.32 +trace_rewrite:=true;
    4.33 +val SOME (t',_) = rewrite_set_ thy false list_rls t;
    4.34 +trace_rewrite:=false;
    4.35 +term2str t';
    4.36 +"c";
    4.37 +
    4.38 +(*-------------------------------------------------------------------*)
    4.39 +val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
    4.40 +val ttt = (#prop o rep_thm) thm;
    4.41 +atomty ttt;
    4.42 +(*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)
    4.43 +
    4.44 +
    4.45 +
    4.46 +"--------------------- length_ -------------------------------------------";
    4.47 +"--------------------- length_ -------------------------------------------";
    4.48 +"--------------------- length_ -------------------------------------------";
    4.49 +val thy' = "ListG";
    4.50 +val ct = "length_ [1,1,1]";
    4.51 +val thm = ("length_Cons_","");
    4.52 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    4.53 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    4.54 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    4.55 +val thm = ("length_Nil_","");
    4.56 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    4.57 +if ct="1 + (1 + (1 + 0))"then()
    4.58 +else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
    4.59 +
    4.60 +
    4.61 +val ct = "length_ [1,1,1]";
    4.62 +val rls = "list_rls";
    4.63 +val (ct,asm) = the (rewrite_set thy' false rls ct);
    4.64 +if ct="3"then()
    4.65 +else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
    4.66 +
    4.67 +
    4.68 +val ct = "length_ [1,1,1]";
    4.69 +val t = (term_of o the o (parse ListG.thy)) ct;
    4.70 +val t = eval_listexpr_ ListG.thy list_rls t;
    4.71 +case t of Free ("3",_) => () 
    4.72 +| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
    4.73 +
    4.74 +

     5.1 --- a/test/Tools/isac/ProgLang/listg.sml	Mon Jul 25 14:19:50 2011 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,73 +0,0 @@
     5.4 -(* tests for ListG
     5.5 -   author: Walther Neuper 1.5.03
     5.6 -
     5.7 -use"../smltest/Scripts/listg.sml";
     5.8 -use"listg.sml";
     5.9 -*)
    5.10 -
    5.11 -
    5.12 -
    5.13 -"--------------------- nth_ ----------------------------------------------";
    5.14 -"--------------------- nth_ ----------------------------------------------";
    5.15 -"--------------------- nth_ ----------------------------------------------";
    5.16 -val t = str2term "nth_ 3 [a,b,c,d,e]";
    5.17 -atomty t;
    5.18 -val thm = (#prop o rep_thm o num_str) nth_Cons_;
    5.19 -atomty thm;
    5.20 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;
    5.21 -if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
    5.22 -else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
    5.23 -
    5.24 -val t = str2term "nth_ 1 [a,b,c,d,e]";
    5.25 -atomty t;
    5.26 -val thm = (#prop o rep_thm o num_str) nth_Nil_;
    5.27 -atomty thm;
    5.28 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Nil_}) t;
    5.29 -term2str t';
    5.30 -"a";
    5.31 -
    5.32 -val t = str2term "nth_ 3 [a,b,c,d,e]";
    5.33 -atomty t;
    5.34 -trace_rewrite:=true;
    5.35 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
    5.36 -trace_rewrite:=false;
    5.37 -term2str t';
    5.38 -"c";
    5.39 -
    5.40 -(*-------------------------------------------------------------------*)
    5.41 -val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
    5.42 -val ttt = (#prop o rep_thm) thm;
    5.43 -atomty ttt;
    5.44 -(*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)
    5.45 -
    5.46 -
    5.47 -
    5.48 -"--------------------- length_ -------------------------------------------";
    5.49 -"--------------------- length_ -------------------------------------------";
    5.50 -"--------------------- length_ -------------------------------------------";
    5.51 -val thy' = "ListG";
    5.52 -val ct = "length_ [1,1,1]";
    5.53 -val thm = ("length_Cons_","");
    5.54 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    5.55 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    5.56 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    5.57 -val thm = ("length_Nil_","");
    5.58 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    5.59 -if ct="1 + (1 + (1 + 0))"then()
    5.60 -else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
    5.61 -
    5.62 -
    5.63 -val ct = "length_ [1,1,1]";
    5.64 -val rls = "list_rls";
    5.65 -val (ct,asm) = the (rewrite_set thy' false rls ct);
    5.66 -if ct="3"then()
    5.67 -else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
    5.68 -
    5.69 -
    5.70 -val ct = "length_ [1,1,1]";
    5.71 -val t = (term_of o the o (parse ListG.thy)) ct;
    5.72 -val t = eval_listexpr_ ListG.thy list_rls t;
    5.73 -case t of Free ("3",_) => () 
    5.74 -| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
    5.75 -
    5.76 -

     6.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Jul 25 14:19:50 2011 +0200
     6.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Jul 25 17:44:19 2011 +0200
     6.3 @@ -25,10 +25,10 @@
     6.4  uses 
     6.5    (         "library.sml")
     6.6    (         "calcelems.sml")
     6.7 -  ("ProgLang/termC.sml") 
     6.8 +  ("ProgLang/termC.sml")      
     6.9    ("ProgLang/calculate.sml")
    6.10    ("ProgLang/rewrite.sml")
    6.11 -(*("ProgLang/listg.sml")*)
    6.12 +  ("ProgLang/listg.sml")
    6.13    ("ProgLang/scrtools.sml")
    6.14    ("ProgLang/tools.sml")
    6.15  
    6.16 @@ -78,7 +78,7 @@
    6.17    ("Knowledge/rooteq.sml")
    6.18    ("Knowledge/rateq.sml")
    6.19    ("Knowledge/rootrateq.sml")
    6.20 -(*("Knowledge/polyeq.sml")*)
    6.21 +  ("Knowledge/polyeq.sml")
    6.22    ("Knowledge/calculus.sml")
    6.23    ("Knowledge/trig.sml")
    6.24    ("Knowledge/logexp.sml")
    6.25 @@ -99,10 +99,10 @@
    6.26    ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
    6.27    use          "library.sml"
    6.28    use          "calcelems.sml"
    6.29 -  use "ProgLang/termC.sml
    6.30 +  use "ProgLang/termC.sml"
    6.31    use "ProgLang/calculate.sml"      (*part.*)
    6.32    use "ProgLang/rewrite.sml"        (*part.*)
    6.33 -(*use "ProgLang/listg.sml"            2002*)
    6.34 +(*use "ProgLang/listC.sml"            2002*)
    6.35    use "ProgLang/scrtools.sml"         (*complete*)
    6.36    use "ProgLang/tools.sml"            (*complete*)
    6.37    ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
    6.38 @@ -119,7 +119,7 @@
    6.39    use "Minisubpbl/600-postcond.sml"
    6.40    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
    6.41    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    6.42 -  use "Interpret/mstools.sml"       (*new 2010*)
    6.43 +  use "Interpret/mstools.sml"
    6.44    use "Interpret/ctree.sml"         (*!...!see(25)*)
    6.45    use "Interpret/ptyps.sml"         (*    *)
    6.46  (*use "Interpret/generate.sml"        new 2011*)

     7.1 --- a/test/Tools/isac/Test_Some.thy	Mon Jul 25 14:19:50 2011 +0200
     7.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Jul 25 17:44:19 2011 +0200
     7.3 @@ -11,20 +11,6 @@
     7.4  
     7.5  ML{*
     7.6  
     7.7 -
     7.8 -
     7.9 -
    7.10 -
    7.11 -
    7.12 -
    7.13 -
    7.14 -
    7.15 -
    7.16 -
    7.17 -
    7.18 -
    7.19 -*}
    7.20 -ML{*
    7.21  *}
    7.22  ML{*
    7.23  *}