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/system.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37991 028442673981
child 55276 ce872d7781d2
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba 
    22 val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
 
    22 val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
 
    23 		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
 
    23 		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
 
    24 val SOME (t,_) = rewrite_set_ thy false norm_Poly t;
 
    24 val SOME (t,_) = rewrite_set_ thy false norm_Poly t;
 
    25 if term2str t = 
    25 if term2str t = 
    26 "[0 = -1 * q_0 * (0 / 2) + c_2, 0 = L * c + -1 * q_0 * (L ^^^ 2 / 2) + c_2]"
 
    26 "[0 = -1 * q_0 * (0 / 2) + c_2, 0 = L * c + -1 * q_0 * (L ^^^ 2 / 2) + c_2]"
 
    27 then () else raise error "system.sml, diff.behav. in norm_Poly";
 
    27 then () else error "system.sml, diff.behav. in norm_Poly";
 
    28 
    28 
    29 val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
 
    29 val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
 
    30 		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
 
    30 		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
 
    31 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 
    31 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 
    32 if term2str t = 
    32 if term2str t = 
    33 "[0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
 
    33 "[0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
 
    34 then () else raise error "system.sml, diff.behav. in norm_Rational";
 
    34 then () else error "system.sml, diff.behav. in norm_Rational";
 
    35 
    35 
    36 
    36 
    37 val t = str2term "nth_ 1 [0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
 
    37 val t = str2term "nth_ 1 [0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\
 
    38 		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
 
    38 		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";
 
    39 val SOME (t,_) = rewrite_set_ thy false list_rls t;
 
    39 val SOME (t,_) = rewrite_set_ thy false list_rls t;
 
    40 if term2str t = "0 = c * 0 + -1 * q_0 * (0 ^^^ 2 / 2) + c_2"
 
    40 if term2str t = "0 = c * 0 + -1 * q_0 * (0 ^^^ 2 / 2) + c_2"
 
    41 then () else raise error "system.sml, list_rls";
 
    41 then () else error "system.sml, list_rls";
 
    42 
    42 
    43 
    43 
    44 "----------- me --------------------------------------------------";
 
    44 "----------- me --------------------------------------------------";
 
    45 "----------- me --------------------------------------------------";
 
    45 "----------- me --------------------------------------------------";
 
    46 "----------- me --------------------------------------------------";
 
    46 "----------- me --------------------------------------------------";
 
    53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    57 case nxt of (_, Specify_Theory "Biegelinie") => ()
 
    57 case nxt of (_, Specify_Theory "Biegelinie") => ()
 
    58 	  | _ => raise error "system.sml diff.behav.in me --1";
 
    58 	  | _ => error "system.sml diff.behav.in me --1";
 
    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    62 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
 
    62 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
 
    63 	  | _ => raise error "system.sml diff.behav.in me --2";
 
    63 	  | _ => error "system.sml diff.behav.in me --2";
 
    64 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    64 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    65 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    65 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    66 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    66 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    67 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    67 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    68 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    68 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    69 
    69 
    70 case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2", 
    70 case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2", 
    71 					       "linear", "system"])) => ()
 
    71 					       "linear", "system"])) => ()
 
    72 	  | _ => raise error "system.sml diff.behav.in me --3";
 
    72 	  | _ => error "system.sml diff.behav.in me --3";
 
    73 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    73 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    76 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    76 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    77 case nxt of (_, Specify_Theory "Biegelinie") => ()
 
    77 case nxt of (_, Specify_Theory "Biegelinie") => ()
 
    78 	  | _ => raise error "system.sml diff.behav.in me --1";
 
    78 	  | _ => error "system.sml diff.behav.in me --1";
 
    79 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    79 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    80 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    80 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    82 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
 
    82 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
 
    83 	  | _ => raise error "system.sml diff.behav.in me --2";
 
    83 	  | _ => error "system.sml diff.behav.in me --2";
 
    84 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    84 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    85 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    85 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    86 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    86 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    87 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    87 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    88 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    88 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
    90 
    90 
    91 (*---
 
    91 (*---
 
    92 WN060421 stopped as soon as exp_IsacCore_Equ_Sys_Lin_No-1.xml worked ...
 
    92 WN060421 stopped as soon as exp_IsacCore_Equ_Sys_Lin_No-1.xml worked ...
 
    93 
    93 
    94 if f2str f = "" then ()
 
    94 if f2str f = "" then ()
 
    95 else raise error  "system.sml diff.behav.in me --99";
 
    95 else error  "system.sml diff.behav.in me --99";
 
    96 case nxt of ("End_Proof'", End_Proof') => ()
 
    96 case nxt of ("End_Proof'", End_Proof') => ()
 
    97 	  | _ => raise error  "system.sml diff.behav.in me --99";
 
    97 	  | _ => error  "system.sml diff.behav.in me --99";
 
    98 
    98 
    99 print_depth 11;nxt;print_depth 3;
 
    99 print_depth 11;nxt;print_depth 3;
 
   100 ---*)
 
   100 ---*)
 
   101 (*
 
   101 (*
 
   102 use"../smltest/IsacKnowledge/system.sml";
 
   102 use"../smltest/IsacKnowledge/system.sml";
wneuper/isa