intermed. test/../integrate.sml in -- me method [diff,integration] --
removed last error by
find . -type f -exec sed -i s/"\"Isac.thy\""/"\"Isac\""/g {} \;
find . -type f -exec sed -i s/" Isac.thy"/" (theory \"Isac\")"/g {} \;
1 (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt
2 author: Walther Neuper 2007
3 (c) due to copyright terms
5 use"../smltest/IsacKnowledge/algein.sml";
10 "-----------------------------------------------------------------";
11 "table of contents -----------------------------------------------";
12 "-----------------------------------------------------------------";
13 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
14 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
15 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
16 "----------- Widerspruch 3 = 777 ---------------------------------";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
23 (* use"../smltest/IsacKnowledge/algein.sml";
26 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
27 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
28 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
30 "Script RechnenSymbolScript (k_::bool) (q__::bool) \
31 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
35 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
36 (*---^^^-OK-----------------------------------------------------------------*)
38 "Script RechnenSymbolScript (k_::bool) (q__::bool) \
39 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
40 \ (let t_ = Take (l_ = Oben + Senkrecht + Unten); \
41 \ sum_ = boollist2sum o_;\
42 \ t_ = Substitute [Oben = sum_] t_;\
43 \ t_ = Substitute o_ t_;\
44 \ t_ = Substitute [k_, q__] t_;\
45 \ t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
48 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
49 (*---vvv-NOTok--------------------------------------------------------------*)
57 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
58 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
59 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
61 ["KantenLaenge (k=10)","Querschnitt (q=1)",
62 "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
63 "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
64 "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
67 ("Isac",["numerischSymbolische", "Berechnung"],
68 ["Berechnung","erstNumerisch"]);
69 val p = e_pos'; val c = [];
70 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
71 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
72 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
73 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);
74 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);
75 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);
76 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);
77 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);
78 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);
79 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);
80 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*);
81 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);
82 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);
83 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);
84 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);
86 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
87 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
88 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
89 val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
90 if f2str f = "L = 32 + senkrecht + unten" then ()
91 else error "algein.sml diff.behav. in erstSymbolisch 1";
92 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
93 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
97 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
98 else error "algein.sml diff.behav. in erstSymbolisch 99";
101 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
102 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
103 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
106 [(["KantenLaenge (k=10)","Querschnitt (q=1)",
107 "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
108 "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
109 "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
111 ("Isac",["numerischSymbolische", "Berechnung"],
112 ["Berechnung","erstSymbolisch"]))];
115 autoCalculate 1 CompleteCalc;
116 val ((pt,p),_) = get_calc 1; show_pt pt;
117 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
118 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
123 trace_rewrite:=false;
128 "----------- Widerspruch 3 = 777 ---------------------------------";
129 "----------- Widerspruch 3 = 777 ---------------------------------";
130 "----------- Widerspruch 3 = 777 ---------------------------------";
131 val thy = (theory "Isac");
132 val rew_ord = dummy_ord;
135 val thm = assoc_thm' thy ("sym_real_mult_0_right","");
136 val t = str2term "0 = 0";
137 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
139 (********"0 = ?z1 * 0"*)
141 (*testing code in ME/appl.sml*)
142 val sube = ["?z1 = 3"];
143 val subte = sube2subte sube;
144 val subst = sube2subst thy sube;
145 foldl and_ (true, map contains_Var subte);
147 val t'' = subst_atomic subst t';
149 (********"0 = 3 * 0"*)
151 val thm = assoc_thm' thy ("sym","");
152 (*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
153 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
156 (* use"../smltest/IsacKnowledge/algein.sml";