Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/partial_fractions.sml
changeset 42376 9e59542132b3
parent 42359 b9d382f20232
child 42386 3aff35f94465
equal deleted inserted replaced
42373:2450ff84560a 42376:9e59542132b3 
     9 "----------- why helpless here ? ------------------------";
 
     9 "----------- why helpless here ? ------------------------";
 
    10 "----------- why not nxt = Model_Problem here ? ---------";
 
    10 "----------- why not nxt = Model_Problem here ? ---------";
 
    11 "----------- fun factors_from_solution ------------------";
 
    11 "----------- fun factors_from_solution ------------------";
 
    12 "----------- Logic.unvarify_global ----------------------";
 
    12 "----------- Logic.unvarify_global ----------------------";
 
    13 "----------- eval_drop_questionmarks --------------------";
 
    13 "----------- eval_drop_questionmarks --------------------";
 
       
    14 "----------- = me for met_partial_fraction --------------";
 
    14 "--------------------------------------------------------";
 
    15 "--------------------------------------------------------";
 
    15 "--------------------------------------------------------";
 
    16 "--------------------------------------------------------";
 
    16 "--------------------------------------------------------";
 
    17 "--------------------------------------------------------";
 
    17 
    18 
    18 
    19 
    72 "----------- fun factors_from_solution ------------------";
 
    73 "----------- fun factors_from_solution ------------------";
 
    73 val ctxt = ProofContext.init_global @{theory Isac};
 
    74 val ctxt = ProofContext.init_global @{theory Isac};
 
    74 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
 
    75 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
 
    75 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
 
    76 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
 
    76 if term2str t' =
 
    77 if term2str t' =
 
    77  "factors_from_solution [z = 1 / 2, z = -1 / 4] =\n(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
 
    78  "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
 
    78 then () else error "factors_from_solution broken";
 
    79 then () else error "factors_from_solution broken";
 
    79 
    80 
    80 "----------- Logic.unvarify_global ----------------------";
 
    81 "----------- Logic.unvarify_global ----------------------";
 
    81 "----------- Logic.unvarify_global ----------------------";
 
    82 "----------- Logic.unvarify_global ----------------------";
 
    82 "----------- Logic.unvarify_global ----------------------";
 
    83 "----------- Logic.unvarify_global ----------------------";
 
   108 val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
 
   109 val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
 
   109 if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
 
   110 if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
 
   110   "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
 
   111   "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
 
   111 then () else error "eval_drop_questionmarks broken";
 
   112 then () else error "eval_drop_questionmarks broken";
 
   112 
   113 
       
   114 "----------- = me for met_partial_fraction --------------";
 
       
   115 "----------- = me for met_partial_fraction --------------";
 
       
   116 "----------- = me for met_partial_fraction --------------";
 
       
   117   val fmz =                                             
       
   118     ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", 
       
   119       "solveFor z", "decomposedFunction p_p"];
 
       
   120   val (dI',pI',mI') =
 
       
   121     ("Partial_Fractions", 
       
   122       ["partial_fraction", "rational", "simplification"],
 
       
   123       ["simplification","of_rationals","to_partial_fraction"]);
 
       
   124   val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
       
   125   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   126   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   127   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   128   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   129   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   130   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   131   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   132   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   133   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   134   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   135   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   136   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   137   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   138   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   139   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   140   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   141   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   142   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   143   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   144   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   145   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   146   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   147   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   148   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   149   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   150   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   151   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   152   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   153   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   154   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   155   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   156   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   157   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   158   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   159   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   160   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   161   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   162   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   163   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   164   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   165   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   166   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   167   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   168   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   169   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   170   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   171   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   172   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   173   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   174   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   175   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   176   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   177   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   178   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   179   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   180   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   181   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   182   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   183   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   184   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   185   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   186   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   187   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   188   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   189   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   190   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   191   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   192   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   193   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   194   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   195   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   196   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   197   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
       
   198   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   199   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   200   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   201   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   202   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   203   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   204   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   205   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   206   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   207   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   208   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   209   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   210   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   211   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   212   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   213   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   214   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   215   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
       
   216   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
       
   217 
       
   218 show_pt pt;
 
       
   219 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then() 
       
   220 else error "= me .. met_partial_fraction broken";
 
       
   221
wneuper/isa