Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/rateq.sml
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 28 Sep 2010 09:06:56 +0200
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37991 028442673981
child 41928 20138d6136cd
permissions -rw-r--r--
tuned error and writeln

# raise error --> error
# writeln in atomtyp, atomty, atomt and xmlsrc 
     1 (* RL 09.02 

     2  testexamples for RatEq, equations with fractions

     3 

     4  Compiler.Control.Print.printDepth:=10; (*4 default*)

     5  Compiler.Control.Print.printDepth:=5; (*4 default*)

     6  trace_rewrite:=true;

     7 

     8  use"kbtest/rateq.sml";

     9  *)

    10 "----------- rateq.sml begin--------";

    11 "---------(1/x=5) ---------------------";

    12 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";

    13 

    14 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in  x";

    15 val SOME(t_, _) = rewrite_set_ RatEq.thy  false RatEq_prls t;

    16 val result = term2str t_;

    17 if result <>  "True"  then error "rateq.sml: new behaviour 1:" else ();

    18 

    19 val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in  x";

    20 val SOME(t_, _) = rewrite_set_ RatEq.thy  false RatEq_prls t;

    21 val result = term2str t_;

    22 if result <>  "False"  then error "rateq.sml: new behaviour 2:" else ();

    23 

    24 val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";

    25 val SOME(t_,_) = rewrite_set_ RatEq.thy  false RatEq_prls t;

    26 val result = term2str t_;

    27 if result <>  "False"  then error "rateq.sml: new behaviour 3:" else ();

    28 

    29 val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";

    30 val SOME(t_,_) = rewrite_set_ RatEq.thy  false RatEq_prls t;

    31 val result = term2str t_;

    32 if result <>  "True"  then error "rateq.sml: new behaviour 4:" else ();

    33 

    34 val result = match_pbl ["equality (x=1)","solveFor x","solutions L"] 

    35                 (get_pbt ["rational","univariate","equation"]); 

    36 case result of NoMatch' _  => ()  | _ => error "rateq.sml: new behaviour: 5";

    37 

    38 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] 

    39                 (get_pbt ["rational","univariate","equation"]); 

    40 case result of Matches' _  => ()  | _ => error "rateq.sml: new behaviour: 6";

    41 

    42 

    43 (*---------rateq---- 23.8.02 ---------------------*)

    44 "---------(1/x=5) ---------------------";

    45 val fmz = ["equality (1/x=5)","solveFor x","solutions L"];

    46 (* refine fmz ["univariate","equation"];

    47    *)

    48 

    49 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

    50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    51 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    52    --------------------------------------- Refine_Tacitly*)

    53 (*  nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)

    54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    59 (* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*)

    60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    61 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    62    --------------------------------------- Refine_Tacitly*)

    63 (*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*) 

    64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    68 (*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)

    69 

    70 (* get_obj g_fmz pt [2];

    71    *)

    72 

    73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    74 (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)

    75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    76 (* val nxt = ("Subproblem",  Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)

    77 

    78 

    79 

    80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    82 (*  ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)

    83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    85 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    90 (* "x = 1 / 5" *)

    91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    92 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then () 

    93 else  error "rateq.sml: new behaviour: [x = 1 / 5]";

    94 

    95 

    96 

    97 (*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)

    98 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";

    99 (*EP Schalk_II_p68_n40*)

   100 val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];

   101 (* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",

   102 	   "solveFor x","solutions L"];*)

   103 

   104 (* refine fmz ["univariate","equation"];

   105 *)

   106 

   107 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

   108 (*val p = e_pos'; 

   109 val c = []; 

   110 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   111 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

   112 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   114 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)

   115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   121 (* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)

   122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   123 (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)

   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   130 (* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)

   131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   132 (* nxt = ("Model_Problem", Model_Problem

   133      ["abcFormula","degree_2","polynomial","univariate","equation"])*)

   134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   141 (* "x = -2, x = 10" *)

   142 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then() 

   143 else  error "rateq.sml: new behaviour: [x = -2, x = 10]";

   144 

   145 "----------- rateq.sml end--------";
wneuper/isa