1.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Mar 05 13:35:44 2012 +0100
1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Mar 06 14:25:08 2012 +0100
1.3 @@ -1,9 +1,6 @@
1.4 (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt
1.5 author: Walther Neuper 2007
1.6 (c) due to copyright terms
1.7 -
1.8 -use"../smltest/IsacKnowledge/algein.sml";
1.9 -use"algein.sml";
1.10 *)
1.11
1.12 "-----------------------------------------------------------------";
1.13 @@ -27,37 +24,28 @@
1.14 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
1.15 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
1.16 val str =
1.17 -"Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.18 -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.19 -\ (let t_ = (l_ = 1)\
1.20 -\ in t_)"
1.21 +"Script RechnenSymbolScript (k_k::bool) (q__q::bool) \
1.22 +\(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\
1.23 +\ (let t_t = (l_l = 1)\
1.24 +\ in t_t)"
1.25 ;
1.26 -(*=== inhibit exn 110722=============================================================
1.27 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.28 -=== inhibit exn 110722=============================================================*)
1.29 -
1.30 -
1.31 -(*=== inhibit exn 110722=============================================================
1.32 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.33 -
1.34 atomty sc;
1.35 atomt sc;
1.36 -=== inhibit exn 110722=============================================================*)
1.37
1.38 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.39 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.40 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.41 val fmz =
1.42 - ["KantenLaenge (k=10)","Querschnitt (q=1)",
1.43 - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
1.44 - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
1.45 - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
1.46 + ["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))",
1.47 + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
1.48 + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
1.49 + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
1.50 "GesamtLaenge L"];
1.51 val (dI',pI',mI') =
1.52 ("Isac",["numerischSymbolische", "Berechnung"],
1.53 ["Berechnung","erstNumerisch"]);
1.54 val p = e_pos'; val c = [];
1.55 -(*=== inhibit exn 110722=============================================================
1.56 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
1.57 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
1.58 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
1.59 @@ -88,63 +76,48 @@
1.60 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
1.61 else error "algein.sml diff.behav. in erstSymbolisch 99";
1.62 DEconstrCalcTree 1;
1.63 -=== inhibit exn 110722=============================================================*)
1.64
1.65 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.66 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.67 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.68 CalcTree
1.69 -[(["KantenLaenge (k=10)","Querschnitt (q=1)",
1.70 - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
1.71 - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
1.72 - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
1.73 - "GesamtLaenge L"],
1.74 +[(["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))",
1.75 + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
1.76 + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
1.77 + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
1.78 + "GesamtLaenge L"],
1.79 ("Isac",["numerischSymbolische", "Berechnung"],
1.80 ["Berechnung","erstSymbolisch"]))];
1.81 Iterator 1;
1.82 moveActiveRoot 1;
1.83 autoCalculate 1 CompleteCalc;
1.84 val ((pt,p),_) = get_calc 1; show_pt pt;
1.85 -(*=== inhibit exn 110722=============================================================
1.86 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
1.87 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
1.88 -===== inhibit exn 110722===========================================================*)
1.89 -(*
1.90 -show_pt pt;
1.91 -trace_rewrite:=true;
1.92 -trace_rewrite:=false;
1.93 -trace_script:=true;
1.94 -trace_script:=false;
1.95 -*)
1.96 +
1.97 "----------- Widerspruch 3 = 777 ---------------------------------";
1.98 "----------- Widerspruch 3 = 777 ---------------------------------";
1.99 "----------- Widerspruch 3 = 777 ---------------------------------";
1.100 val thy = @{theory "Isac"};
1.101 val rew_ord = dummy_ord;
1.102 val erls = Erls;
1.103 -(*===== inhibit exn 110722===========================================================
1.104 -val thm = assoc_thm' thy ("sym_real_mult_0_right","");
1.105 -val t = str2term "0 = 0";
1.106 +val thm = assoc_thm' thy ("sym_mult_zero_right","");
1.107 +val t = str2term "0 = (0::real)";
1.108 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
1.109 -term2str t';
1.110 -(********"0 = ?z1 * 0"*)
1.111 +term2str t' = "0 = ?a1 * 0"; (* = true*)
1.112
1.113 (*testing code in ME/appl.sml*)
1.114 -val sube = ["?z1 = 3"];
1.115 +val sube = ["?a1 = (3::real)"];
1.116 val subte = sube2subte sube;
1.117 +terms2str' subte = "[?a1 = 3]"; (* = true*)
1.118 val subst = sube2subst thy sube;
1.119 foldl and_ (true, map contains_Var subte);
1.120
1.121 val t'' = subst_atomic subst t';
1.122 -term2str t'';
1.123 -(********"0 = 3 * 0"*)
1.124 -===== inhibit exn 110722===========================================================*)
1.125 +term2str t'' = "0 = 3 * 0"; (* = true*)
1.126
1.127 val thm = assoc_thm' thy ("sym","");
1.128 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
1.129 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
1.130 *)
1.131
1.132 -(* use"../smltest/IsacKnowledge/algein.sml";
1.133 - *)
1.134 -