agriesma@338: (* use"test-FE-KE.sml";
agriesma@338:    W.N.16.4.00
agriesma@338:    *)
agriesma@338: 
agriesma@338: Compiler.Control.Print.printDepth:=4; (*4 default*)
agriesma@338: 
agriesma@338: (*#########################################################*)
agriesma@338: " _________________ stdin: tutor active_________________ ";
agriesma@338: proofs:=[]; dials:=([],[],[]); 
agriesma@338: (*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*)
agriesma@338: 
agriesma@338: StdinSML 0 0 0 0 New_User;
agriesma@338: StdinSML 1 0 0 0 New_Proof;
agriesma@338: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
agriesma@338: 	   "solveFor x","errorBound (eps=0)",
agriesma@338: 	   "solutions L"];
agriesma@338: val (dI',pI',mI') =
agriesma@338:   ("Script.thy",["sqroot-test","univariate","equation"],
agriesma@338:    ("Script.thy","sqrt-equ-test"));
agriesma@338: "--- s1 ---";
agriesma@338: val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 (*@@@@@begin !!!!!*)
agriesma@338:   (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
agriesma@338: "--- s2 ---";
agriesma@338: StdinSML 1 1 ~1 ~1 (Command Accept);
agriesma@338: (*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*)
agriesma@338: "--- s3 ---";
agriesma@338: StdinSML 1 1 ~2 ~2 (Command Accept);
agriesma@338: (*RuleFK (Add_Given "solveFor x")*)
agriesma@338: "--- s4 ---";
agriesma@338: StdinSML 1 1 ~3 ~3 (Command Accept);
agriesma@338: (*RuleFK (Add_Given "errorBound (eps = #0)")*)
agriesma@338: "--- s5 ---";
agriesma@338: StdinSML 1 1 ~4 ~4 (Command Accept);
agriesma@338: (*RuleFK (Add_Find "solutions L")*)
agriesma@338: "--- s6 ---";
agriesma@338: StdinSML 1 1 ~5 ~5 (Command Accept);
agriesma@338: (*RuleFK (Specify_Domain "Script.thy")*)
agriesma@338: "--- s7 ---";
agriesma@338: StdinSML 1 1 ~6 ~6 (Command Accept);
agriesma@338: (*RuleFK (Specify_Problem ["sqroot-test","univariate","equation"])*)
agriesma@338: "--- s8 ---";
agriesma@338: StdinSML 1 1 ~7 ~7 (Command Accept);
agriesma@338: (*RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))*)
agriesma@338: "--- s9 ---";
agriesma@338: StdinSML 1 1 ~8 ~8 (Command Accept);
agriesma@338: (*RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))*)
agriesma@338: "--- 1 ---";
agriesma@338: StdinSML 1 1 ~9 ~9 (Command Accept);
agriesma@338: (*RuleFK (Rewrite ("square_equation_left",""))*)
agriesma@338: "--- 2 ---";
agriesma@338: StdinSML 1 1 ~10 ~10 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "SqRoot_simplify")*)
agriesma@338: "--- 3 ---";
agriesma@338: StdinSML 1 1 ~11 ~11 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "rearrange_assoc")*)
agriesma@338: "--- 4 ---";
agriesma@338: StdinSML 1 1 ~12 ~12 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "isolate_root")*)
agriesma@338: "--- 5 ---";
agriesma@338: StdinSML 1 1 ~13 ~13 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "SqRoot_simplify")*)
agriesma@338: "--- 6 ---";
agriesma@338: StdinSML 1 1 ~14 ~14 (Command Accept);
agriesma@338: (*RuleFK (Rewrite ("square_equation_left",""))*)
agriesma@338: "--- 7 ---";
agriesma@338: StdinSML 1 1 ~15 ~15 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "SqRoot_simplify")*)
agriesma@338: "--- 8 ---";
agriesma@338: StdinSML 1 1 ~16 ~16 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "norm_equation")*)
agriesma@338: "--- 9 ---";
agriesma@338: StdinSML 1 1 ~17 ~17 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "SqRoot_simplify")*)
agriesma@338: "--- 10 ---";
agriesma@338: StdinSML 1 1 ~18 ~18 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))*)
agriesma@338: "--- 11 ---";
agriesma@338: StdinSML 1 1 ~19 ~19 (Command Accept);
agriesma@338: (*RuleFK (Rewrite_Set "SqRoot_simplify")*)
agriesma@338: "--- 12 ---";
agriesma@338: val (begin,uI,pI,acI,cI,dats,eend) = 
agriesma@338: StdinSML 1 1 ~20 ~20 (Command Accept);
agriesma@338: (*RuleFK (Check_Postcond ("Script.thy","sqrt-equ-test"))*)
agriesma@338: 
agriesma@338: if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]"))
agriesma@338: then raise error "do_ + msteps input: not finished correctly"
agriesma@338: else "roo-equation, do_ + msteps input: OK";
agriesma@338: 
agriesma@338: "==========================================================";
agriesma@338: writeln (get_history 1 1);
agriesma@338: "==========================================================";
agriesma@338: 
agriesma@338: 
agriesma@338: 
agriesma@338: (*#########################################################*)
agriesma@338: " _________________ stdin: student active_________________ ";
agriesma@338: proofs:=[]; dials:=([],[],[]); 
agriesma@338: (*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*)
agriesma@338: 
agriesma@338: StdinSML 0 0 0 0 New_User;
agriesma@338: StdinSML 1 0 0 0 New_Proof;
agriesma@338: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
agriesma@338: 	   "solveFor x","errorBound (eps=0)",
agriesma@338: 	   "solutions L"];
agriesma@338: val (dI',pI',mI') =
agriesma@338:   ("Script.thy",["sqroot-test","univariate","equation"],
agriesma@338:    ("Script.thy","sqrt-equ-test"));
agriesma@338: "--- s1 ---";
agriesma@338: val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1
agriesma@338:   (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
agriesma@338: "--- s2 ---";
agriesma@338: StdinSML 1 1 ~1 2 (RuleFK 
agriesma@338: (Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"));
agriesma@338: "--- s3 ---";
agriesma@338: StdinSML 1 1 ~2 3 (RuleFK (Add_Given "solveFor x"));
agriesma@338: "--- s4 ---";
agriesma@338: StdinSML 1 1 ~3 4 (RuleFK (Add_Given "errorBound (eps = 0)"));
agriesma@338: "--- s5 ---";
agriesma@338: StdinSML 1 1 ~4 5 (RuleFK (Add_Find "solutions L"));
agriesma@338: "--- s6 ---";
agriesma@338: StdinSML 1 1 ~5 6 (RuleFK (Specify_Domain "Script.thy"));
agriesma@338: "--- s7 ---";
agriesma@338: StdinSML 1 1 ~6 7 (RuleFK 
agriesma@338: (Specify_Problem ["sqroot-test","univariate","equation"]));
agriesma@338: "--- s8 ---";
agriesma@338: StdinSML 1 1 ~7 8 (RuleFK (Specify_Method ("Script.thy","sqrt-equ-test")));
agriesma@338: "--- s9 ---";
agriesma@338: StdinSML 1 1 ~8 9 (RuleFK (Apply_Method ("Script.thy","sqrt-equ-test")));
agriesma@338: "--- 1 ---";
agriesma@338: StdinSML 1 1 ~9 10 (RuleFK 
agriesma@338: (Rewrite ("square_equation_left","")));
agriesma@338: "--- 2 ---";
agriesma@338: StdinSML 1 1 ~10 11 (RuleFK (Rewrite_Set "SqRoot_simplify"));
agriesma@338: "--- 3 ---";
agriesma@338: StdinSML 1 1 ~11 12 (RuleFK (Rewrite_Set "rearrange_assoc"));
agriesma@338: "--- 4 ---";
agriesma@338: StdinSML 1 1 ~12 13 (RuleFK (Rewrite_Set "isolate_root"));
agriesma@338: "--- 5 ---";
agriesma@338: StdinSML 1 1 ~13 14 (RuleFK (Rewrite_Set "SqRoot_simplify"));
agriesma@338: "--- 6 ---";
agriesma@338: StdinSML 1 1 ~14 15 (RuleFK 
agriesma@338: (Rewrite ("square_equation_left","")));
agriesma@338: "--- 7 ---";
agriesma@338: StdinSML 1 1 ~15 16 (RuleFK (Rewrite_Set "SqRoot_simplify"));
agriesma@338: "--- 8 ---";
agriesma@338: StdinSML 1 1 ~16 17 (RuleFK (Rewrite_Set "norm_equation"));
agriesma@338: "--- 9 ---";
agriesma@338: StdinSML 1 1 ~17 18 (RuleFK (Rewrite_Set "SqRoot_simplify"));
agriesma@338: "--- 10 ---";
agriesma@338: StdinSML 1 1 ~18 19 (RuleFK 
agriesma@338: (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv")));
agriesma@338: "--- 11 ---";
agriesma@338: StdinSML 1 1 ~19 20 (RuleFK (Rewrite_Set "SqRoot_simplify"));
agriesma@338: "--- 12 ---";
agriesma@338: val (begin,uI,pI,acI,cI,dats,eend) = 
agriesma@338: StdinSML 1 1 ~20 21 (RuleFK 
agriesma@338: (Check_Postcond ("Script.thy","sqrt-equ-test")));
agriesma@338: 
agriesma@338: if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]"))
agriesma@338: then raise error "do_ + msteps input: not finished correctly"
agriesma@338: else "roo-equation, do_ + msteps input: OK";
agriesma@338: 
agriesma@338: "==========================================================";
agriesma@338: writeln (get_history 1 1);
agriesma@338: "==========================================================";
agriesma@338: 
agriesma@338: 
agriesma@338: (*=========27.4.01===============================================*)
agriesma@338:    proofs:= []; dials:=([],[],[]); 
agriesma@338: " _________________ exampel [x=4]: Rules 4.2.01a________________ ";
agriesma@338: val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;
agriesma@338: val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;
agriesma@338: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
agriesma@338: 	   "solveFor x","errorBound (eps=0)",
agriesma@338: 	   "solutions L"];
agriesma@338: val (dI',pI',mI') =
agriesma@338:   ("SqRoot.thy",["sqroot-test","univariate","equation"],
agriesma@338:    ("SqRoot.thy","squ-equ-test2"));
agriesma@338: StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
agriesma@338: 
agriesma@338: StdinSML uI pI ~1 ~1 (Command Accept);
agriesma@338: 
agriesma@338: StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "norm_equation"));