1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,158 @@
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 +val thy = AlgEin.thy;
1.12 +
1.13 +"-----------------------------------------------------------------";
1.14 +"table of contents -----------------------------------------------";
1.15 +"-----------------------------------------------------------------";
1.16 +"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
1.17 +"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.18 +"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.19 +"----------- Widerspruch 3 = 777 ---------------------------------";
1.20 +"-----------------------------------------------------------------";
1.21 +"-----------------------------------------------------------------";
1.22 +"-----------------------------------------------------------------";
1.23 +
1.24 +
1.25 +
1.26 +(* use"../smltest/IsacKnowledge/algein.sml";
1.27 + *)
1.28 +
1.29 +"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
1.30 +"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
1.31 +"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
1.32 +val str =
1.33 +"Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.34 +\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.35 +\ (let t_ = (l_ = 1)\
1.36 +\ in t_)"
1.37 +;
1.38 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.39 +(*---^^^-OK-----------------------------------------------------------------*)
1.40 +val str =
1.41 +"Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.42 +\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.43 +\ (let t_ = Take (l_ = Oben + Senkrecht + Unten); \
1.44 +\ sum_ = boollist2sum o_;\
1.45 +\ t_ = Substitute [Oben = sum_] t_;\
1.46 +\ t_ = Substitute o_ t_;\
1.47 +\ t_ = Substitute [k_, q__] t_;\
1.48 +\ t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
1.49 +\ in t_)"
1.50 +;
1.51 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.52 +(*---vvv-NOTok--------------------------------------------------------------*)
1.53 +
1.54 +
1.55 +
1.56 +atomty sc;
1.57 +atomt sc;
1.58 +
1.59 +
1.60 +"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.61 +"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.62 +"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.63 +val fmz =
1.64 + ["KantenLaenge (k=10)","Querschnitt (q=1)",
1.65 + "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
1.66 + "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
1.67 + "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
1.68 + "GesamtLaenge L"];
1.69 +val (dI',pI',mI') =
1.70 + ("Isac.thy",["numerischSymbolische", "Berechnung"],
1.71 + ["Berechnung","erstNumerisch"]);
1.72 +val p = e_pos'; val c = [];
1.73 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
1.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
1.75 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
1.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);
1.77 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);
1.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);
1.79 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);
1.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);
1.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);
1.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);
1.83 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin.thy"*);
1.84 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);
1.85 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);
1.86 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);
1.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);
1.88 +f2str f;
1.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
1.90 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
1.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
1.92 +val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
1.93 +if f2str f = "L = 32 + senkrecht + unten" then ()
1.94 +else raise error "algein.sml diff.behav. in erstSymbolisch 1";
1.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
1.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
1.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
1.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
1.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.100 +if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
1.101 +else raise error "algein.sml diff.behav. in erstSymbolisch 99";
1.102 +
1.103 +
1.104 +"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.105 +"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.106 +"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.107 +states:=[];
1.108 +CalcTree
1.109 +[(["KantenLaenge (k=10)","Querschnitt (q=1)",
1.110 + "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
1.111 + "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
1.112 + "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
1.113 + "GesamtLaenge L"],
1.114 + ("Isac.thy",["numerischSymbolische", "Berechnung"],
1.115 + ["Berechnung","erstSymbolisch"]))];
1.116 +Iterator 1;
1.117 +moveActiveRoot 1;
1.118 +autoCalculate 1 CompleteCalc;
1.119 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.120 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
1.121 +else raise error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
1.122 +
1.123 +(*
1.124 +show_pt pt;
1.125 +trace_rewrite:=true;
1.126 +trace_rewrite:=false;
1.127 +trace_script:=true;
1.128 +trace_script:=false;
1.129 +*)
1.130 +
1.131 +"----------- Widerspruch 3 = 777 ---------------------------------";
1.132 +"----------- Widerspruch 3 = 777 ---------------------------------";
1.133 +"----------- Widerspruch 3 = 777 ---------------------------------";
1.134 +val thy = Isac.thy;
1.135 +val rew_ord = dummy_ord;
1.136 +val erls = Erls;
1.137 +
1.138 +val thm = assoc_thm' thy ("sym_real_mult_0_right","");
1.139 +val t = str2term "0 = 0";
1.140 +val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
1.141 +term2str t';
1.142 +(********"0 = ?z1 * 0"*)
1.143 +
1.144 +(*testing code in ME/appl.sml*)
1.145 +val sube = ["?z1 = 3"];
1.146 +val subte = sube2subte sube;
1.147 +val subst = sube2subst thy sube;
1.148 +foldl and_ (true, map contains_Var subte);
1.149 +
1.150 +val t'' = subst_atomic subst t';
1.151 +term2str t'';
1.152 +(********"0 = 3 * 0"*)
1.153 +
1.154 +val thm = assoc_thm' thy ("sym","");
1.155 +(*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
1.156 +val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
1.157 +*)
1.158 +
1.159 +(* use"../smltest/IsacKnowledge/algein.sml";
1.160 + *)
1.161 +