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/diff.sml
changeset 60660 c4b24621077e
parent 60650 06ec8abfd3bc
child 60663 2197e3597cba
equal deleted inserted replaced
60659:873f40b097bb 60660:c4b24621077e 
   216 
   216 
   217 "----------- primed id ----------------------------------";
 
   217 "----------- primed id ----------------------------------";
 
   218 "----------- primed id ----------------------------------";
 
   218 "----------- primed id ----------------------------------";
 
   219 "----------- primed id ----------------------------------";
 
   219 "----------- primed id ----------------------------------";
 
   220 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
 
   220 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
 
   221 val f_ = TermC.parse_test @{context} "f_f::bool";
 
   221 val f_ = ParseC.parse_test @{context} "f_f::bool";
 
   222 val f  = TermC.parse_test @{context} "A = s * (a - s)";
 
   222 val f  = ParseC.parse_test @{context} "A = s * (a - s)";
 
   223 val v_ = TermC.parse_test @{context} "v_v";
 
   223 val v_ = ParseC.parse_test @{context} "v_v";
 
   224 val v  = TermC.parse_test @{context} "s";
 
   224 val v  = ParseC.parse_test @{context} "s";
 
   225 val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
 
   225 val screxp0 = ParseC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
 
   226 TermC.atom_trace_detail @{context} screxp0;
 
   226 TermC.atom_trace_detail @{context} screxp0;
 
   227 
   227 
   228 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
 
   228 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
 
   229 UnparseC.term screxp1;
 
   229 UnparseC.term screxp1;
 
   230 TermC.atom_trace_detail @{context} screxp1;
 
   230 TermC.atom_trace_detail @{context} screxp1;
 
   266 
   266 
   267 
   267 
   268 "----------- diff_conv, sym_diff_conv -------------------";
 
   268 "----------- diff_conv, sym_diff_conv -------------------";
 
   269 "----------- diff_conv, sym_diff_conv -------------------";
 
   269 "----------- diff_conv, sym_diff_conv -------------------";
 
   270 "----------- diff_conv, sym_diff_conv -------------------";
 
   270 "----------- diff_conv, sym_diff_conv -------------------";
 
   271 val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
 
   271 val subs = [(ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "x")];
 
   272 val rls = diff_conv;
 
   272 val rls = diff_conv;
 
   273 
   273 
   274 val t = TermC.parse_test @{context} "2/x \<up> 2"; 
   274 val t = ParseC.parse_test @{context} "2/x \<up> 2"; 
   275 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   275 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   276 if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";
 
   276 if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";
 
   277 
   277 
   278 val t = TermC.parse_test @{context} "sqrt (x \<up> 3)";
 
   278 val t = ParseC.parse_test @{context} "sqrt (x \<up> 3)";
 
   279 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   279 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   280 if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";
 
   280 if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";
 
   281 
   281 
   282 val t = TermC.parse_test @{context} "2 / sqrt x \<up> 3";
 
   282 val t = ParseC.parse_test @{context} "2 / sqrt x \<up> 3";
 
   283 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   283 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   284 if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
 
   284 if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
 
   285 
   285 
   286 val rls = diff_sym_conv;
 
   286 val rls = diff_sym_conv;
 
   287 
   287 
   288 val t = TermC.parse_test @{context} "2 * x \<up> - 2";
 
   288 val t = ParseC.parse_test @{context} "2 * x \<up> - 2";
 
   289 val SOME (t, _) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   289 val SOME (t, _) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   290 if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
 
   290 if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
 
   291 
   291 
   292 val t = TermC.parse_test @{context} "x \<up> (3 / 2)";
 
   292 val t = ParseC.parse_test @{context} "x \<up> (3 / 2)";
 
   293 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   293 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   294 if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
 
   294 if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
 
   295 
   295 
   296 val t = TermC.parse_test @{context} "2 * x \<up> (-3 / 2)";
 
   296 val t = ParseC.parse_test @{context} "2 * x \<up> (-3 / 2)";
 
   297 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   297 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
 
   298 if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
 
   298 if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
 
   299 
   299 
   300 
   300 
   301 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
 
   301 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
 
   386 
   386 
   387 "----------- tests for examples -------------------------";
 
   387 "----------- tests for examples -------------------------";
 
   388 "----------- tests for examples -------------------------";
 
   388 "----------- tests for examples -------------------------";
 
   389 "----------- tests for examples -------------------------";
 
   389 "----------- tests for examples -------------------------";
 
   390 "----- TermC.parse errors";
 
   390 "----- TermC.parse errors";
 
   391 (*TermC.parse_test @{context} "F  =  sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
 
   391 (*ParseC.parse_test @{context} "F  =  sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
 
   392 TermC.parse_test @{context} "O";
 
   392 ParseC.parse_test @{context} "O";
 
   393 TermC.parse_test @{context} "OO"; ---errors*)
 
   393 ParseC.parse_test @{context} "OO"; ---errors*)
 
   394 TermC.parse_test @{context} "OOO";
 
   394 ParseC.parse_test @{context} "OOO";
 
   395 
   395 
   396 "----- thm 'diff_prod_const'";
 
   396 "----- thm 'diff_prod_const'";
 
   397 val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "l")];
 
   397 val subs = [(ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "l")];
 
   398 val f = TermC.parse_test @{context} "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
 
   398 val f = ParseC.parse_test @{context} "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
 
   399 
   399 
   400 "------------inform for x \<up> 2+x+1 -------------------------";
 
   400 "------------inform for x \<up> 2+x+1 -------------------------";
 
   401 "------------inform for x \<up> 2+x+1 -------------------------";
 
   401 "------------inform for x \<up> 2+x+1 -------------------------";
 
   402 "------------inform for x \<up> 2+x+1 -------------------------";
 
   402 "------------inform for x \<up> 2+x+1 -------------------------";
 
   403 States.reset ();
 
   403 States.reset ();
wneuper/isa