Mercurial Mercurial > wneuper > isac / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/sml/systest/details.sml
author agriesma
Thu, 17 Apr 2003 18:01:03 +0200
branchgriesmayer
changeset 338 90390fecbe74
child 708 7d3338563b8c
permissions -rw-r--r--
neues cvs-verzeichnis 
     1 (* use"../systest/details.sml";

     2    use"systest/details.sml";

     3    use"details.sml";

     4 

     5 ########################################################

     6 is NOT dependent on Test, but on other thys:

     7 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

     8 uses from Rational.ML: Rrls cancel_p, Rrls cancel

     9 which in turn

    10 uses from Poly.ML: Rls make_polynomial, Rls expand_binom 

    11 ######################################################## 

    12 *)

    13 "-------- cancel, without detail ------------------------------";

    14 "-------- cancel, detail rev-rew (cancel) afterwards ----------";

    15 "-------------- cancel_p, without detail ------------------------------";

    16 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

    17 

    18 store_pbt

    19  (prep_pbt Test.thy

    20  (["test"],

    21   [],

    22   e_rls, None, []));

    23 store_pbt

    24  (prep_pbt Test.thy

    25  (["detail","test"],

    26   [("#Given" ,["realTestGiven t_"]),

    27    ("#Find"  ,["realTestFind s_"])

    28    ],

    29   e_rls, None, [("Test.thy","test_detail")]));

    30 

    31 methods:= overwritel (!methods,

    32 [

    33  prep_met

    34  (("Test.thy","test_detail_binom"):metID,

    35   [("#Given" ,["realTestGiven t_"]),

    36    ("#Find"  ,["realTestFind s_"])

    37    ],

    38   {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,

    39    asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]},

    40  "Script Testterm (g_::real) =   \

    41  \(((Rewrite_Set expand_binoms False) @@\

    42  \  (Rewrite_Set cancel False)) g_)"

    43  ),

    44  prep_met

    45  (("Test.thy","test_detail_poly"):metID,

    46   [("#Given" ,["realTestGiven t_"]),

    47    ("#Find"  ,["realTestFind s_"])

    48    ],

    49   {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,

    50    asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]},

    51  "Script Testterm (g_::real) =   \

    52  \(((Rewrite_Set make_polynomial False) @@\

    53  \  (Rewrite_Set cancel_p False)) g_)"

    54  )]);

    55 

    56 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)

    57 

    58 "-------- cancel, without detail ------------------------------";

    59 "-------- cancel, without detail ------------------------------";

    60 "-------- cancel, without detail ------------------------------";

    61 val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",

    62 	   "realTestFind s"];

    63 val (dI',pI',mI') =

    64   ("Test.thy",["detail","test"],("Test.thy","test_detail_binom"));

    65 

    66 val p = e_pos'; val c = [];

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

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

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

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

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

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

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

    74 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

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

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

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

    79 (*"(3 + -1 * x) / (3 + x)"*)

    80 if nxt = ("End_Proof'",End_Proof') then ()

    81 else raise error "details.sml, changed behaviour in: without detail";

    82 

    83 

    84 "-------- cancel, detail rev-rew (cancel) afterwards ----------";

    85 "-------- cancel, detail rev-rew (cancel) afterwards ----------";

    86 "-------- cancel, detail rev-rew (cancel) afterwards ----------";

    87  val p = e_pos'; val c = [];

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

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

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

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

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

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

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

    95  (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

    97  (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)

    98  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

    99  val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

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

   105  (*val nxt = ("End_Detail",End_Detail)*)

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

   107  (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)

   108  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

   109  val nxt = ("Detail",Detail);"----------------------";

   110  val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

   112 (*15.10.02*)

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

   114 (*

   115 rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","")

   116 	"3 ^^^ 2 - x ^^^ 2";

   117 *)

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

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

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

   121  val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

   123 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))

   124    andalso nxt = ("End_Proof'",End_Proof') then ()

   125 else raise error "new behaviour in details.sml, \

   126 		 \cancel, rev-rew (cancel) afterwards";

   127 

   128 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)

   129 

   130 "-------------- cancel_p, without detail ------------------------------";

   131 "-------------- cancel_p, without detail ------------------------------";

   132 "-------------- cancel_p, without detail ------------------------------";

   133 val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",

   134 	   "realTestFind s"];

   135 val (dI',pI',mI') =

   136   ("Test.thy",["detail","test"],("Test.thy","test_detail_poly"));

   137 

   138 val p = e_pos'; val c = [];

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

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

   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 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

   148 "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";

   149 

   150  (*14.3.03*)

   151  val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";

   152  val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   153  "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";

   154  val Some (t,_) = rewrite_set_ thy false cancel_p t; term2str t;

   155  cancel_p_ thy t;

   156 

   157  val t = str2term "(3 + x) * (3 + -1 * x)";

   158  val Some (t,_) = rewrite_set_ thy false expand_poly t; term2str t;

   159  "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";

   160  val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;

   161  "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";

   162  val Some (t,_) = rewrite_set_ thy false simplify_power t; term2str t;

   163  "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";

   164  val Some (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;

   165  "9 + (0 * x + -1 * x ^^^ 2)";

   166  val Some (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;

   167  "9 + - (x ^^^ 2)"; 

   168  (*14.3.03*)

   169 

   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 (*"(3 + -1 * x) / (3 + x)"*)

   174 if nxt = ("End_Proof'",End_Proof') then ()

   175 else raise error "details.sml, changed behaviour in: cancel_p, without detail";

   176 

   177 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

   178 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

   179 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

   180  val p = e_pos'; val c = [];

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

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

   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  (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

   190  (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)

   191  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

   192 

   193 (*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:

   194   fun make_deriv ...  Rls_ not yet impl. (| Thm | Calc) 

   195   Rls_ needed for make_polynomial ----------------------

   196  val nxt = ("Detail",Detail);"----------------------";

   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  val (p,_,f,nxt,_,pt) = me nxt p [] pt;

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

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

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

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

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

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

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

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

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

   227  if nxt = ("End_Detail",End_Detail) then ()

   228  else raise error "details.sml: new behav. in Detail make_polynomial";

   229 ----------------------------------------------------------------------*)

   230 

   231 (*---------------

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

   233  (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)

   234  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

   235  val nxt = ("Detail",Detail);"----------------------";

   236  val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

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

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

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

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

   242  val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

   244 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))

   245    andalso nxt = ("End_Proof'",End_Proof') then ()

   246 else raise error "new behaviour in details.sml, cancel_p afterwards";

   247 

   248 ----------------*)

   249 

   250 

   251 

   252 

   253 

   254 val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",

   255 	   "realTestFind s"];

   256 val (dI',pI',mI') =

   257   ("Test.thy",["detail","test"],("Test.thy","test_detail_poly"));

   258 

   259  val p = e_pos'; val c = [];

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

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

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

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

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

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

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

   267  (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

   269 (*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------

   270  (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)

   271  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

   272  val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

   277 -------------------------------------------------------------------------*)

   278 

   279 

   280
wneuper/isac