wneuper/isac: src/sml/systest/stdinout.sml@90390fecbe74

     1 (* use"test-FE-KE.sml";

     2    W.N.16.4.00

     3    *)

     5 Compiler.Control.Print.printDepth:=4; (*4 default*)

     7 (*#########################################################*)

     8 " _________________ stdin: tutor active_________________ ";

     9 proofs:=[]; dials:=([],[],[]);

    10 (*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*)

    12 StdinSML 0 0 0 0 New_User;

    13 StdinSML 1 0 0 0 New_Proof;

    14 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

    15 	   "solveFor x","errorBound (eps=0)",

    16 	   "solutions L"];

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

    18   ("Script.thy",["sqroot-test","univariate","equation"],

    19    ("Script.thy","sqrt-equ-test"));

    20 "--- s1 ---";

    21 val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 (*@@@@@begin !!!!!*)

    22   (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

    23 "--- s2 ---";

    24 StdinSML 1 1 ~1 ~1 (Command Accept);

    25 (*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*)

    26 "--- s3 ---";

    27 StdinSML 1 1 ~2 ~2 (Command Accept);

    28 (*RuleFK (Add_Given "solveFor x")*)

    29 "--- s4 ---";

    30 StdinSML 1 1 ~3 ~3 (Command Accept);

    31 (*RuleFK (Add_Given "errorBound (eps = #0)")*)

    32 "--- s5 ---";

    33 StdinSML 1 1 ~4 ~4 (Command Accept);

    34 (*RuleFK (Add_Find "solutions L")*)

    35 "--- s6 ---";

    36 StdinSML 1 1 ~5 ~5 (Command Accept);

    37 (*RuleFK (Specify_Domain "Script.thy")*)

    38 "--- s7 ---";

    39 StdinSML 1 1 ~6 ~6 (Command Accept);

    40 (*RuleFK (Specify_Problem ["sqroot-test","univariate","equation"])*)

    41 "--- s8 ---";

    42 StdinSML 1 1 ~7 ~7 (Command Accept);

    43 (*RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))*)

    44 "--- s9 ---";

    45 StdinSML 1 1 ~8 ~8 (Command Accept);

    46 (*RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))*)

    47 "--- 1 ---";

    48 StdinSML 1 1 ~9 ~9 (Command Accept);

    49 (*RuleFK (Rewrite ("square_equation_left",""))*)

    50 "--- 2 ---";

    51 StdinSML 1 1 ~10 ~10 (Command Accept);

    52 (*RuleFK (Rewrite_Set "SqRoot_simplify")*)

    53 "--- 3 ---";

    54 StdinSML 1 1 ~11 ~11 (Command Accept);

    55 (*RuleFK (Rewrite_Set "rearrange_assoc")*)

    56 "--- 4 ---";

    57 StdinSML 1 1 ~12 ~12 (Command Accept);

    58 (*RuleFK (Rewrite_Set "isolate_root")*)

    59 "--- 5 ---";

    60 StdinSML 1 1 ~13 ~13 (Command Accept);

    61 (*RuleFK (Rewrite_Set "SqRoot_simplify")*)

    62 "--- 6 ---";

    63 StdinSML 1 1 ~14 ~14 (Command Accept);

    64 (*RuleFK (Rewrite ("square_equation_left",""))*)

    65 "--- 7 ---";

    66 StdinSML 1 1 ~15 ~15 (Command Accept);

    67 (*RuleFK (Rewrite_Set "SqRoot_simplify")*)

    68 "--- 8 ---";

    69 StdinSML 1 1 ~16 ~16 (Command Accept);

    70 (*RuleFK (Rewrite_Set "norm_equation")*)

    71 "--- 9 ---";

    72 StdinSML 1 1 ~17 ~17 (Command Accept);

    73 (*RuleFK (Rewrite_Set "SqRoot_simplify")*)

    74 "--- 10 ---";

    75 StdinSML 1 1 ~18 ~18 (Command Accept);

    76 (*RuleFK (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))*)

    77 "--- 11 ---";

    78 StdinSML 1 1 ~19 ~19 (Command Accept);

    79 (*RuleFK (Rewrite_Set "SqRoot_simplify")*)

    80 "--- 12 ---";

    81 val (begin,uI,pI,acI,cI,dats,eend) =

    82 StdinSML 1 1 ~20 ~20 (Command Accept);

    83 (*RuleFK (Check_Postcond ("Script.thy","sqrt-equ-test"))*)

    85 if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]"))

    86 then raise error "do_ + msteps input: not finished correctly"

    87 else "roo-equation, do_ + msteps input: OK";

    89 "==========================================================";

    90 writeln (get_history 1 1);

    91 "==========================================================";

    95 (*#########################################################*)

    96 " _________________ stdin: student active_________________ ";

    97 proofs:=[]; dials:=([],[],[]);

    98 (*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*)

   100 StdinSML 0 0 0 0 New_User;

   101 StdinSML 1 0 0 0 New_Proof;

   102 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   103 	   "solveFor x","errorBound (eps=0)",

   104 	   "solutions L"];

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

   106   ("Script.thy",["sqroot-test","univariate","equation"],

   107    ("Script.thy","sqrt-equ-test"));

   108 "--- s1 ---";

   109 val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1

   110   (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   111 "--- s2 ---";

   112 StdinSML 1 1 ~1 2 (RuleFK

   113 (Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"));

   114 "--- s3 ---";

   115 StdinSML 1 1 ~2 3 (RuleFK (Add_Given "solveFor x"));

   116 "--- s4 ---";

   117 StdinSML 1 1 ~3 4 (RuleFK (Add_Given "errorBound (eps = 0)"));

   118 "--- s5 ---";

   119 StdinSML 1 1 ~4 5 (RuleFK (Add_Find "solutions L"));

   120 "--- s6 ---";

   121 StdinSML 1 1 ~5 6 (RuleFK (Specify_Domain "Script.thy"));

   122 "--- s7 ---";

   123 StdinSML 1 1 ~6 7 (RuleFK

   124 (Specify_Problem ["sqroot-test","univariate","equation"]));

   125 "--- s8 ---";

   126 StdinSML 1 1 ~7 8 (RuleFK (Specify_Method ("Script.thy","sqrt-equ-test")));

   127 "--- s9 ---";

   128 StdinSML 1 1 ~8 9 (RuleFK (Apply_Method ("Script.thy","sqrt-equ-test")));

   129 "--- 1 ---";

   130 StdinSML 1 1 ~9 10 (RuleFK

   131 (Rewrite ("square_equation_left","")));

   132 "--- 2 ---";

   133 StdinSML 1 1 ~10 11 (RuleFK (Rewrite_Set "SqRoot_simplify"));

   134 "--- 3 ---";

   135 StdinSML 1 1 ~11 12 (RuleFK (Rewrite_Set "rearrange_assoc"));

   136 "--- 4 ---";

   137 StdinSML 1 1 ~12 13 (RuleFK (Rewrite_Set "isolate_root"));

   138 "--- 5 ---";

   139 StdinSML 1 1 ~13 14 (RuleFK (Rewrite_Set "SqRoot_simplify"));

   140 "--- 6 ---";

   141 StdinSML 1 1 ~14 15 (RuleFK

   142 (Rewrite ("square_equation_left","")));

   143 "--- 7 ---";

   144 StdinSML 1 1 ~15 16 (RuleFK (Rewrite_Set "SqRoot_simplify"));

   145 "--- 8 ---";

   146 StdinSML 1 1 ~16 17 (RuleFK (Rewrite_Set "norm_equation"));

   147 "--- 9 ---";

   148 StdinSML 1 1 ~17 18 (RuleFK (Rewrite_Set "SqRoot_simplify"));

   149 "--- 10 ---";

   150 StdinSML 1 1 ~18 19 (RuleFK

   151 (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv")));

   152 "--- 11 ---";

   153 StdinSML 1 1 ~19 20 (RuleFK (Rewrite_Set "SqRoot_simplify"));

   154 "--- 12 ---";

   155 val (begin,uI,pI,acI,cI,dats,eend) =

   156 StdinSML 1 1 ~20 21 (RuleFK

   157 (Check_Postcond ("Script.thy","sqrt-equ-test")));

   159 if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]"))

   160 then raise error "do_ + msteps input: not finished correctly"

   161 else "roo-equation, do_ + msteps input: OK";

   163 "==========================================================";

   164 writeln (get_history 1 1);

   165 "==========================================================";

   168 (*=========27.4.01===============================================*)

   169    proofs:= []; dials:=([],[],[]);

   170 " _________________ exampel [x=4]: Rules 4.2.01a________________ ";

   171 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;

   172 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;

   173 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   174 	   "solveFor x","errorBound (eps=0)",

   175 	   "solutions L"];

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

   177   ("SqRoot.thy",["sqroot-test","univariate","equation"],

   178    ("SqRoot.thy","squ-equ-test2"));

   179 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   181 StdinSML uI pI ~1 ~1 (Command Accept);

   183 StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "norm_equation"));

author	agriesma
	Thu, 17 Apr 2003 18:01:03 +0200
branch	griesmayer
changeset 338	90390fecbe74
child 809	be2febc29e4f
permissions	-rw-r--r--