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

   author: Walther Neuper 2007

   (c) due to copyright terms

*)

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

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

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

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

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

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

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

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

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

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

val thy = @{theory "AlgEin"};

val ctxt = Proof_Context.init_global thy;

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

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

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

val str =

"Program RechnenSymbolScript (k_k::bool) (q__q::bool) \

\(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\

\ (let t_t = (l_l = 1)\

\ in t_t)"

;

val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;

TermC.atom_trace_detail @{context} sc;

TermC.atom_trace @{context} sc;

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

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

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

val fmz = 

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

     "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", 

     "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", 

     "KantenOben  [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",

     "GesamtLaenge L"];

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

  ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],

   ["Berechnung", "erstNumerisch"]);

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

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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 erstNumerisch 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"

then case nxt of End_Proof' => ()

  | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"

else error "algein.sml diff.behav. in erstNumerisch 99 2";

DEconstrCalcTree 1;

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

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

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

CalcTree @{context}

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

     "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", 

     "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", 

     "KantenOben  [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",

     "GesamtLaenge L"], 

  ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

val thy = @{theory "Isac_Knowledge"}; 

val ctxt = Proof_Context.init_global thy;

val rew_ord = Rewrite_Ord.function_empty;

val asm_rls = Rule_Set.Empty;

val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";

val t = TermC.parse_test @{context} "0 = (0::real)";

val SOME (t',_) = rewrite_ ctxt rew_ord asm_rls false thm t;

UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)

val sube = ["?a1 = (3::real)"];

(*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1

  --------------- review together with development of Widerspruch 3 = 77* )

val subte = Subst.input_to_terms @{context} sube;

UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)

val subst = Subst.T_from_string_eqs thy sube;

foldl and_ (true, map TermC.contains_Var subte);

val t'' = subst_atomic subst t';

UnparseC.term t'' = "0 = 3 * 0"; (* = true*)

val thm = ThmC.thm_from_thy thy "sym";

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

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

*)

( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)