(* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt

   author: Walther Neuper 2007

   (c) due to copyright terms

use"../smltest/IsacKnowledge/algein.sml";

use"algein.sml";

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"----------- build method 'Berechnung' 'erstSymbolisch' ----------";

"----------- me 'Berechnung' 'erstNumerisch' ---------------------";

"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

"----------- Widerspruch 3 = 777 ---------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

(*=== inhibit exn ?=============================================================

val thy = AlgEin.thy;

(* use"../smltest/IsacKnowledge/algein.sml";

   *)

"----------- build method 'Berechnung' 'erstSymbolisch' ----------";

"----------- build method 'Berechnung' 'erstSymbolisch' ----------";

"----------- build method 'Berechnung' 'erstSymbolisch' ----------";

val str =

"Script RechnenSymbolScript (k_::bool) (q__::bool) \

\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\

\ (let t_ = (l_ = 1)\

\ in t_)"

;

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

(*---^^^-OK-----------------------------------------------------------------*)

val str =

"Script RechnenSymbolScript (k_::bool) (q__::bool)           \

\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\

\ (let t_ = Take (l_ = Oben + Senkrecht + Unten);            \

\      sum_ = boollist2sum o_;\

\      t_ = Substitute [Oben = sum_] t_;\

\      t_ = Substitute o_ t_;\

\      t_ = Substitute [k_, q__] t_;\

\      t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\

\ in t_)"

;

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

(*---vvv-NOTok--------------------------------------------------------------*)

atomty sc;

atomt sc;

"----------- me 'Berechnung' 'erstNumerisch' ---------------------";

"----------- me 'Berechnung' 'erstNumerisch' ---------------------";

"----------- me 'Berechnung' 'erstNumerisch' ---------------------";

val fmz = 

    ["KantenLaenge (k=10)","Querschnitt (q=1)",

     "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", 

     "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", 

     "KantenOben  [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",

     "GesamtLaenge L"];

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

  ("Isac",["numerischSymbolische", "Berechnung"],

   ["Berechnung","erstNumerisch"]);

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

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);

f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt(**);

if f2str f = "L = 32 + senkrecht + unten" then ()

else error "algein.sml diff.behav. in erstSymbolisch 1";

val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()

else error "algein.sml diff.behav. in erstSymbolisch 99";

"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

states:=[];

CalcTree

[(["KantenLaenge (k=10)","Querschnitt (q=1)",

   "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", 

   "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", 

   "KantenOben  [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",

   "GesamtLaenge L"], 

  ("Isac",["numerischSymbolische", "Berechnung"],

   ["Berechnung","erstSymbolisch"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1; show_pt pt;

if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()

else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";

(*

show_pt pt;

trace_rewrite:=true;

trace_rewrite:=false;

trace_script:=true;

trace_script:=false;

*)

"----------- Widerspruch 3 = 777 ---------------------------------";

"----------- Widerspruch 3 = 777 ---------------------------------";

"----------- Widerspruch 3 = 777 ---------------------------------";

val thy = (theory "Isac"); 

val rew_ord = dummy_ord;

val erls = Erls;

val thm = assoc_thm' thy ("sym_real_mult_0_right","");

val t = str2term "0 = 0";

val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;

term2str t';

(********"0 = ?z1 * 0"*)

(*testing code in ME/appl.sml*)

val sube = ["?z1 = 3"];

val subte = sube2subte sube;

val subst = sube2subst thy sube;

foldl and_ (true, map contains_Var subte);

val t'' = subst_atomic subst t';

term2str t'';

(********"0 = 3 * 0"*)

val thm = assoc_thm' thy ("sym","");

(*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!

val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';

*)

(* use"../smltest/IsacKnowledge/algein.sml";

   *)

===== inhibit exn ?===========================================================*)