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