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 60663 2197e3597cba
parent 60660 c4b24621077e
child 60665 fad0cbfb586d
equal deleted inserted replaced
60662:ba258eeb0826 60663:2197e3597cba 
    33 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
 
    33 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
 
    34 	   Where =[],
 
    34 	   Where =[],
 
    35 	   Find  =["derivative f_f'"],
 
    35 	   Find  =["derivative f_f'"],
 
    36 	   With  =[],
 
    36 	   With  =[],
 
    37 	   Relate=[]}:string model;
 
    37 	   Relate=[]}:string model;
 
    38 val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt;
 
    38 val chkpbt = ((map (ParseC.parse_test ctxt)) o P_Model.to_list) pbt;
 
    39 
    39 
    40 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))", 
    40 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))", 
    41 	   "differentiateFor x", "derivative f_f'"];
 
    41 	   "differentiateFor x", "derivative f_f'"];
 
    42 val chkorg = map (TermC.parseNEW' ctxt) org;
 
    42 val chkorg = map (ParseC.parse_test ctxt) org;
 
    43 
    43 
    44 Problem.from_store @{context} ["derivative_of", "function"];
 
    44 Problem.from_store @{context} ["derivative_of", "function"];
 
    45 MethodC.from_store ctxt ["diff", "differentiate_on_R"];
 
    45 MethodC.from_store ctxt ["diff", "differentiate_on_R"];
 
    46 
    46 
    47 "----------- for correction of diff_const ---------------";
 
    47 "----------- for correction of diff_const ---------------";
 
    48 "----------- for correction of diff_const ---------------";
 
    48 "----------- for correction of diff_const ---------------";
 
    49 "----------- for correction of diff_const ---------------";
 
    49 "----------- for correction of diff_const ---------------";
 
    50 val ctxt = Proof_Context.init_global @{theory};
 
    50 val ctxt = Proof_Context.init_global @{theory};
 
    51 (*re-evaluate this file, otherwise > *** ME_Isa: 'asm_rls' not known*)
 
    51 (*re-evaluate this file, otherwise > *** ME_Isa: 'asm_rls' not known*)
 
    52 val t = TermC.parseNEW' ctxt "Not (x =!= a)";
 
    52 val t = ParseC.parse_test ctxt "Not (x =!= a)";
 
    53 case rewrite_set_ ctxt false erls_diff t of
 
    53 case rewrite_set_ ctxt false erls_diff t of
 
    54   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
 
    54   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
 
    55 | _ => error "rewrite_set_  Not (x =!= a)  changed";
 
    55 | _ => error "rewrite_set_  Not (x =!= a)  changed";
 
    56 
    56 
    57 val t = TermC.parseNEW' ctxt "2 is_num";
 
    57 val t = ParseC.parse_test ctxt "2 is_num";
 
    58 case rewrite_set_ ctxt false erls_diff t of
 
    58 case rewrite_set_ ctxt false erls_diff t of
 
    59   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
 
    59   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
 
    60 | _ => error "rewrite_set_   2 is_num   changed";
 
    60 | _ => error "rewrite_set_   2 is_num   changed";
 
    61 
    61 
    62 val thm = @{thm diff_const};
 
    62 val thm = @{thm diff_const};
 
    63 val ct = TermC.parseNEW' ctxt "d_d x x";
 
    63 val ct = ParseC.parse_test ctxt "d_d x x";
 
    64 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
 
    64 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
 
    65 val NONE = (rewrite_inst_ ctxt tless_true erls_diff false subst thm ct);
 
    65 val NONE = (rewrite_inst_ ctxt tless_true erls_diff false subst thm ct);
 
    66 
    66 
    67 "----------- for correction of diff_quot ----------------";
 
    67 "----------- for correction of diff_quot ----------------";
 
    68 "----------- for correction of diff_quot ----------------";
 
    68 "----------- for correction of diff_quot ----------------";
 
    69 "----------- for correction of diff_quot ----------------";
 
    69 "----------- for correction of diff_quot ----------------";
 
    70 val thy = @{theory "Diff"};
 
    70 val thy = @{theory "Diff"};
 
    71 val ctxt = Proof_Context.init_global thy;
 
    71 val ctxt = Proof_Context.init_global thy;
 
    72 val ct = TermC.parseNEW' ctxt "Not (x = 0)";
 
    72 val ct = ParseC.parse_test ctxt "Not (x = 0)";
 
    73 rewrite_set_ ctxt false erls_diff ct;
 
    73 rewrite_set_ ctxt false erls_diff ct;
 
    74 
    74 
    75 val ct = TermC.parseNEW' ctxt "d_d x ((x+1) / (x - 1))";
 
    75 val ct = ParseC.parse_test ctxt "d_d x ((x+1) / (x - 1))";
 
    76 val thm = @{thm diff_quot};
 
    76 val thm = @{thm diff_quot};
 
    77 val SOME (ctt,_) =
 
    77 val SOME (ctt,_) =
 
    78     (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
 
    78     (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
 
    79 
    79 
    80 "----------- differentiate by rewrite -------------------";
 
    80 "----------- differentiate by rewrite -------------------";
 
    81 "----------- differentiate by rewrite -------------------";
 
    81 "----------- differentiate by rewrite -------------------";
 
    82 "----------- differentiate by rewrite -------------------";
 
    82 "----------- differentiate by rewrite -------------------";
 
    83 val thy = @{theory "Diff"};
 
    83 val thy = @{theory "Diff"};
 
    84 val ctxt = Proof_Context.init_global thy;
 
    84 val ctxt = Proof_Context.init_global thy;
 
    85 val ct = TermC.parseNEW' ctxt "d_d x (x \<up> 2 + 3 * x + 4)";
 
    85 val ct = ParseC.parse_test ctxt "d_d x (x \<up> 2 + 3 * x + 4)";
 
    86 "--- 1 ---";
 
    86 "--- 1 ---";
 
    87 val thm = @{thm "diff_sum"};
 
    87 val thm = @{thm "diff_sum"};
 
    88 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
 
    88 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
 
    89 "--- 2 ---";
 
    89 "--- 2 ---";
 
    90 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
 
    90 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
 
   103 if UnparseC.term ct = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
 
   103 if UnparseC.term ct = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
 
   104 else error "diff.sml diff.behav. in rewrite 1";
 
   104 else error "diff.sml diff.behav. in rewrite 1";
 
   105 "--- 7 ---";
 
   105 "--- 7 ---";
 
   106 "--- 7 ---";
 
   106 "--- 7 ---";
 
   107 val rls = Test_simplify;
 
   107 val rls = Test_simplify;
 
   108 val ct = TermC.parseNEW' ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";
 
   108 val ct = ParseC.parse_test ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";
 
   109 val (ct, _) = the (rewrite_set_ ctxt true rls ct);
 
   109 val (ct, _) = the (rewrite_set_ ctxt true rls ct);
 
   110 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
 
   110 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
 
   111 
   111 
   112 "----------- differentiate: me (*+ tacs input*) ---------";
 
   112 "----------- differentiate: me (*+ tacs input*) ---------";
 
   113 "----------- differentiate: me (*+ tacs input*) ---------";
 
   113 "----------- differentiate: me (*+ tacs input*) ---------";
 
   260  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var        )) Or \
 
   260  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var        )) Or \
 
   261  \    (Repeat (Rewrite_Set             make_polynomial)))) #> \
 
   261  \    (Repeat (Rewrite_Set             make_polynomial)))) #> \
 
   262  \ (Try (Repeat (Rewrite sym_frac_conv))) #>              \
 
   262  \ (Try (Repeat (Rewrite sym_frac_conv))) #>              \
 
   263  \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
 
   263  \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
 
   264 ;
 
   264 ;
 
   265 val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
 
   265 val sc = (inst_abs o (ParseC.parse_test ctxt)) str;
 
   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 -------------------";
wneuper/isa