neuper@37906: (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt
neuper@37906:    author: Walther Neuper 2007
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
neuper@37906: "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
neuper@37906: "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
neuper@37906: "----------- Widerspruch 3 = 777 ---------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
t@42166: val thy = @{theory "AlgEin"};
Walther@60424: val ctxt = Proof_Context.init_global thy;
neuper@37906: 
neuper@37906: "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
neuper@37906: "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
neuper@37906: "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
neuper@37906: val str =
wneuper@59585: "Program RechnenSymbolScript (k_k::bool) (q__q::bool) \
neuper@42385: \(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\
neuper@42385: \ (let t_t = (l_l = 1)\
neuper@42385: \ in t_t)"
neuper@37906: ;
Walther@60424: val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
Walther@60650: TermC.atom_trace_detail @{context} sc;
Walther@60650: TermC.atom_trace @{context} sc;
neuper@37906: 
neuper@37906: "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
neuper@37906: "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
neuper@37906: "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
neuper@37906: val fmz = 
walther@59997:     ["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",
neuper@42385:      "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", 
neuper@42385:      "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", 
neuper@42385:      "KantenOben  [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
neuper@37906:      "GesamtLaenge L"];
neuper@37906: val (dI',pI',mI') =
wneuper@59592:   ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
walther@59997:    ["Berechnung", "erstNumerisch"]);
neuper@37906: val p = e_pos'; val c = [];
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);
neuper@37991: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);
neuper@37906: f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
neuper@37906: if f2str f = "L = 32 + senkrecht + unten" then ()
wneuper@59508: else error "algein.sml diff.behav. in erstNumerisch 1";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59253: if f2str f = "L = 104"
walther@59749: then case nxt of End_Proof' => ()
wneuper@59508:   | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"
wneuper@59508: else error "algein.sml diff.behav. in erstNumerisch 99 2";
wneuper@59253: DEconstrCalcTree 1;
neuper@37906: 
neuper@37906: "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
neuper@37906: "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
neuper@37906: "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
Walther@60571: CalcTree @{context}
walther@59997: [(["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",
neuper@42385:      "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", 
neuper@42385:      "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", 
neuper@42385:      "KantenOben  [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
neuper@42385:      "GesamtLaenge L"], 
wneuper@59592:   ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
walther@59997:    ["Berechnung", "erstSymbolisch"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@59868: if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "L = 104" then()
neuper@38031: else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
neuper@42385: 
neuper@37906: "----------- Widerspruch 3 = 777 ---------------------------------";
neuper@37906: "----------- Widerspruch 3 = 777 ---------------------------------";
neuper@37906: "----------- Widerspruch 3 = 777 ---------------------------------";
wneuper@59592: val thy = @{theory "Isac_Knowledge"}; 
Walther@60500: val ctxt = Proof_Context.init_global thy;
Walther@60509: val rew_ord = Rewrite_Ord.function_empty;
Walther@60586: val asm_rls = Rule_Set.Empty;
walther@59876: val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
Walther@60565: val t = TermC.parse_test @{context} "0 = (0::real)";
Walther@60586: val SOME (t',_) = rewrite_ ctxt rew_ord asm_rls false thm t;
walther@59868: UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
neuper@37906: 
neuper@42385: val sube = ["?a1 = (3::real)"];
Walther@60567: (*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1
Walther@60567:   --------------- review together with development of Widerspruch 3 = 77* )
Walther@60567: val subte = Subst.input_to_terms @{context} sube;
walther@59868: UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
walther@59912: val subst = Subst.T_from_string_eqs thy sube;
walther@60230: foldl and_ (true, map TermC.contains_Var subte);
neuper@37906: 
neuper@37906: val t'' = subst_atomic subst t';
walther@59868: UnparseC.term t'' = "0 = 3 * 0"; (* = true*)
neuper@37906: 
walther@59876: val thm = ThmC.thm_from_thy thy "sym";
neuper@41977: (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
Walther@60586: val SOME (t''',_) = rewrite_ thy rew_ord asm_rls false thm t'';
neuper@37906: *)
Walther@60567: ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)