1 (* Title: "Knowledge/algein.sml"
2 Author: Walther Neuper 2007
4 Note: Unterrichtsversuch IMST-Projekt, Algebra Einf"uhrung
7 "-----------------------------------------------------------------";
8 "table of contents -----------------------------------------------";
9 "-----------------------------------------------------------------";
10 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
11 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
12 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
13 "----------- Widerspruch 3 = 777 ---------------------------------";
14 "-----------------------------------------------------------------";
15 "-----------------------------------------------------------------";
16 "-----------------------------------------------------------------";
18 val thy = @{theory "AlgEin"};
19 val ctxt = Proof_Context.init_global thy;
21 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
22 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
23 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
25 "Program RechnenSymbolScript (k_k::bool) (q__q::bool) \
26 \(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\
27 \ (let t_t = (l_l = 1)\
30 val sc = (inst_abs o (ParseC.parse_test ctxt)) str;
31 TermC.atom_trace_detail @{context} sc;
32 TermC.atom_trace @{context} sc;
34 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
35 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
36 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
38 ["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",
39 "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
40 "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
41 "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
44 ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
45 ["Berechnung", "erstNumerisch"]);
46 val p = e_pos'; val c = [];
47 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Probelm = nxt
48 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenLaenge (k = 10)" = nxt
49 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querschnitt (q = 1)" = nxt
50 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b1 = k - 2 * q]" = nxt
51 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b1 = k - 2 * q, b2 = k - 2 * q]" = nxt
52 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q]" = nxt
53 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b2 = k - 2 * q, b1 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q]" = nxt
54 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v1 = k]" = nxt
55 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v1 = k, v2 = k]" = nxt
56 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v1 = k, v2 = k, v3 = k]" = nxt
57 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v2 = k, v1 = k, v3 = k, v4 = k]" = nxt
58 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t1 = k - 2 * q]" = nxt
59 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t1 = k - 2 * q, t2 = k - 2 * q]" = nxt
60 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t1 = k - 2 * q, t2 = k - 2 * q, t3 = k - 2 * q]" = nxt
61 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t2 = k - 2 * q, t1 = k - 2 * q, t3 = k - 2 * q, t4 = k - 2 * q]" = nxt
62 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "GesamtLaenge L" = nxt
63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Isac_Knowledge" = nxt
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["numerischSymbolische", "Berechnung"] = nxt
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Berechnung", "erstNumerisch"] = nxt
66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Berechnung", "erstNumerisch"] = nxt
67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["oben = t3 + t1 + t2 + t4"] = nxt;
69 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["t3 = k - 2 * q", "t1 = k - 2 * q", "t2 = k - 2 * q", "t4 = k - 2 * q"] = nxt
70 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["k = 10", "q = 1"] = nxt
71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Poly" = nxt
72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["senkrecht = v3 + v1 + v2 + v4"] = nxt;
73 if f2str f = "L = 32 + senkrecht + unten" then ()
74 else error "algein.sml diff.behav. in erstNumerisch 1";
75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
76 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
77 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
78 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
79 val (p,_,f,nxt,_,pt) = me nxt p c pt;
80 if f2str f = "L = 104"
81 then case nxt of End_Proof' => ()
82 | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"
83 else error "algein.sml diff.behav. in erstNumerisch 99 2";
86 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
87 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
88 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
89 (*/------------------- WN230815 test broke since ???, undetected ERROR in autoCalculate ----\\* )
91 [(["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",
92 "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
93 "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
94 "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
96 ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
97 ["Berechnung", "erstSymbolisch"]))];
100 autoCalculate 1 CompleteCalc;
101 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
102 if p = ([], Res) andalso UnparseC.term @{context} (get_obj g_res pt (fst p)) = "L = 104" then()
103 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
104 ( *\------------------- WN230815 test broke since ???, undetected ERROR in autoCalculate ----//*)
106 "----------- Widerspruch 3 = 777 ---------------------------------";
107 "----------- Widerspruch 3 = 777 ---------------------------------";
108 "----------- Widerspruch 3 = 777 ---------------------------------";
109 val thy = @{theory "Isac_Knowledge"};
110 val ctxt = Proof_Context.init_global thy;
111 val rew_ord = Rewrite_Ord.function_empty;
112 val asm_rls = Rule_Set.Empty;
113 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
114 val t = ParseC.parse_test @{context} "0 = (0::real)";
115 val SOME (t',_) = rewrite_ ctxt rew_ord asm_rls false thm t;
116 UnparseC.term @{context} t' = "0 = ?a1 * 0"; (* = true*)
118 val sube = ["?a1 = (3::real)"];
119 (*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1
120 --------------- review together with development of Widerspruch 3 = 77* )
121 val subte = Subst.input_to_terms @{context} sube;
122 UnparseC.terms @{context} subte = "[?a1 = 3]"; (* = true*)
123 val subst = Subst.T_from_string_eqs thy sube;
124 foldl and_ (true, map TermC.contains_Var subte);
126 val t'' = subst_atomic subst t';
127 UnparseC.term @{context} t'' = "0 = 3 * 0"; (* = true*)
129 val thm = ThmC.thm_from_thy thy "sym";
130 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
131 val SOME (t''',_) = rewrite_ thy rew_ord asm_rls false thm t'';
133 ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)