1 (* Title: Knowledge/eqsystem-1a.sml
2 author: Walther Neuper 050826,
5 "-----------------------------------------------------------------------------------------------";
6 "table of contents -----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
9 "----------- problems -----------------------------------------------------------equsystem-1.sml";
10 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
11 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
12 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
13 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
14 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
15 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
16 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
17 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
18 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
19 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
20 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
21 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
22 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
23 "-----------------------------------------------------------------------------------------------";
24 "-----------------------------------------------------------------------------------------------";
25 "-----------------------------------------------------------------------------------------------";
28 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
29 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
30 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
31 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
32 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
33 "solveForVars [c, c_2]", "solution LL"];
35 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
36 ["EqSystem", "normalise", "2x2"]);
37 val p = e_pos'; val c = [];
38 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
39 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
40 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
41 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
42 val (p,_,f,nxt,_,pt) = me nxt p c pt;
43 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
44 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
46 val (p,_,f,nxt,_,pt) = me nxt p c pt;
47 (*nxt = Apply_Method ["EqSystem", "normalise", "2x2"]*)
48 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f = "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]";
49 (*nxt = Rewrite_Set "norm_Rational" *)
50 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f = "[0 = c_2," ^ " 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
51 (*nxt = Rewrite_Set_Inst (["(''bdv_1'', c)", "(''bdv_2'', c_2)"], "simplify_System_parenthesized")*)
52 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f = "[0 = c_2," ^ " 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
53 (*nxt = Rewrite_Set_Inst (["(''bdv_1'', c)", "(''bdv_2'', c_2)"], "isolate_bdvs")*)
54 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f = "[c_2 = 0," ^ " L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]";
55 (*nxt = Rewrite_Set_Inst (["(''bdv_1'', c)", "(''bdv_2'', c_2)"], "simplify_System_parenthesized")*);
56 (*next in solve_EqSystem:solve_system2: Try (Rewrite_Set ''order_system'') ..is skipped*)
57 val (p''''',_,f''''',nxt''''',_,pt''''') = me nxt p c pt;f2str f = "[c_2 = 0," ^ " L * c + c_2 = q_0 * L \<up> 2 / 2]";
58 (*nxt = Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])*)
60 (*/------------------- step into me -----------------------------------------------------\*)
61 (*+*)val (NONE, SOME (ist, ctxt)) = Ctree.get_obj g_loc pt (fst p);
63 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
65 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
66 case Step.by_tactic tac (pt, p) of
67 ("ok", (_, _, ptp)) => ptp;
69 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
70 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) =
71 (p, ((pt, Pos.e_pos'), []));
72 (*if*) Pos.on_calc_end ip (*else*);
73 val (_, probl_id, _) = Calc.references (pt, p);
74 val _ = (*case*) tacis (*of*);
75 (*if*) probl_id = Problem.id_empty (*else*);
77 switch_specify_solve p_ (pt, ip);
78 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
79 (*if*) Pos.on_specification ([], state_pos) (*else*);
81 LI.do_next (pt, input_pos);
82 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
83 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
84 val thy' = get_obj g_domID pt (par_pblobj pt p);
85 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
87 val Next_Step (Pstate {act_arg = t, ...}, _, _) = (*case*)
88 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
89 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) =
90 (sc, (pt, pos), ist, ctxt);
92 val Accept_Tac ((*tac*)Subproblem' _, _(*ist*), _(*ctxt*)) =
93 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
94 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
95 ((prog, (ptp, ctxt)), (Pstate ist));
96 (*if*) path = [] (*else*);
97 (*+*)path = [R, L, R, L, R, R, R, L, R, R];
99 val Accept_Tac (Subproblem' _, _(*ist*), _(*ctxt*)) =
100 go_scan_up (prog, cc) (trans_scan_up ist);
101 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
102 ((prog, cc), (trans_scan_up ist));
103 (*if*) path = [R] (*else*);
104 (*+*)val [R, L, R, L, R, R, R, L, R, R] = path;
105 val Accept_Tac (Subproblem'
106 (("Biegelinie", ["triangular", "2x2", "LINEAR", "system"], ["EqSystem", "top_down_substitution", "2x2"]), _, _, _, _, _),
108 scan_up pcc (ist |> path_up) (go_up path sc);
109 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _ )) =
110 (pcc, (ist |> path_up), (go_up path sc));
112 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
114 (*if*) path = [R] (*else*);
115 (*+*)val [R, L, R, L, R, R, R, L, R] = path;
116 scan_up pcc (ist |> path_up) (go_up path sc);
117 "~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) =
118 (pcc, (ist |> path_up), (go_up path sc));
119 val e2 = check_Seq_up ist sc
121 (*case*) scan_dn cc (ist |> path_up_down [R]) e2 (*of*);
122 go_scan_up pcc (ist |> path_up |> set_act v |> set_found);
123 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
124 (pcc, (ist |> path_up |> set_act v |> set_found));
125 (*if*) path = [R] (*else*);
126 (*+*)path = [R, L, R, L, R, R, R];
127 scan_up pcc (ist |> path_up) (go_up path sc);
128 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _ )) =
129 (pcc, (ist |> path_up), (go_up path sc));
131 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
133 (*if*) path = [R] (*else*);
134 (*+*)path = [R, L, R, L, R, R];
135 scan_up pcc (ist |> path_up) (go_up path sc);
136 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _ )) =
137 (pcc, (ist |> path_up), (go_up path sc));
139 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
141 (*if*) path = [R] (*else*);
142 (*+*)path = [R, L, R, L, R];
143 scan_up pcc (ist |> path_up) (go_up path sc);
144 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _ )) =
145 (pcc, (ist |> path_up), (go_up path sc));
147 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
149 (*if*) path = [R] (*else*);
150 (*+*)path = [R, L, R, L];
151 scan_up pcc (ist |> path_up) (go_up path sc);
152 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _)) =
153 (pcc, (ist |> path_up), (go_up path sc));
155 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
157 (*if*) path = [R] (*else*);
158 (*+*)path = [R, L, R];
159 scan_up pcc (ist |> path_up) (go_up path sc);
160 "~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _)) =
161 (pcc, (ist |> path_up), (go_up path sc));
162 val (i, body) = check_Let_up ist sc
164 val Accept_Tac _ = (*case*)
165 scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
166 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) =
167 (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
168 (*if*) Tactical.contained_in t (*else*);
169 val (Program.Tac prog_tac, form_arg) =
170 (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
172 check_tac cc ist (prog_tac, form_arg);
173 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
174 (cc, ist, (prog_tac, form_arg));
177 LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac;
178 "~~~~~ fun tac_from_prog , args:"; val (pt, _, (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
179 (pt, (Proof_Context.theory_of ctxt), prog_tac);
180 "~~~~~ from fun tac_from_prog \<longrightarrow>fun check_tac , return:"; val (m) =
182 Sub_Problem.tac_from_prog pt ptac));
183 "~~~~~ fun tac_from_prog , args:"; val (pt, (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags')) =
185 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
186 val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt);;
187 val ctxt = Proof_Context.init_global thy (*BETTER USE user_ctxt ?*)
188 val ags = TermC.isalist2list ags';
189 (*if*) mI = ["no_met"] (*then*);
190 val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags): O_Model.T
192 Refine.refine_ori' ctxt pors pI;
193 val return = (pI', pors (* refinement over models with diff.prec only *),
194 (hd o #met o Problem.from_store ctxt) pI');
195 (*-------------^^ THIS CAUSED THE ERROR Empty*)
197 (*+*)val ["LINEAR", "system"] = pI;
198 (*+*)fun app_ptyp x = Store.apply (get_pbls ()) x; (*redefine locally hidden*)
200 "~~~~~ fun refine_ori' , args:"; val (oris, pblID) = (pors, pI);
201 val SOME ["system", "LINEAR", "2x2", "triangular"] =
202 app_ptyp (Refine.refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
204 "~~~~~ fun app_ptyp , args:"; val () = (); (*considered too expensive for testing*)
205 (*+*)val fmz = ["equalities [c_2 = (0::real), L * c + c_2 = q_0 * L \<up> 2 / 2]",
206 "solveForVars [c, c_2]", "solution LL"];
207 (*+isa<>isa2*)Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];(*
208 *** pass ["system", "LINEAR"]
209 *** pass ["system", "LINEAR", "2x2"]
210 *** pass ["system", "LINEAR", "3x3"]
211 *** pass ["system", "LINEAR", "4x4"]
213 [Matches (["LINEAR", "system"], {Find = [Correct "solution LL"], Given = [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", Correct "solveForVars [c, c_2]"], Relate = [], Where = [], With = []}),
215 (["2x2", "LINEAR", "system"],
216 {Find = [Correct "solution LL"], Given = [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", Correct "solveForVars [c, c_2]"], Relate = [], Where =
217 [Correct "Length [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] = 2", False "Length v_s = 2"], With = []}),
218 -------------------------------------------------------- [c, c_2] NOT SUBSTUTED -----^^^
220 (["3x3", "LINEAR", "system"],
221 {Find = [Correct "solution LL"], Given = [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", Correct "solveForVars [c, c_2]"], Relate = [], Where =
222 [False "Length [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] = 3", False "Length v_s = 3"], With = []}),
223 ------------------------------------------------------ [c, c_2] NOT SUBSTUTED -----^^^
225 (["4x4", "LINEAR", "system"],
226 {Find = [Correct "solution LL"], Given = [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", Correct "solveForVars [c, c_2]"], Relate = [], Where =
227 [False "Length [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] = 4", False "Length v_s = 4"], With = []})]:
228 ------------------------------------------------------ [c, c_2] NOT SUBSTUTED -----^^^
230 (*-------------------- stop step into me -------------------------------------------------*)
231 (*\------------------- step into me -----------------------------------------------------/*)
233 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
234 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
235 val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt''''');
237 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
238 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
239 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
240 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
242 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
243 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
245 val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val PblObj {probl,...} = get_obj I pt [5];
247 (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
249 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
250 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
251 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
253 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
254 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
255 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
256 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
257 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
258 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
259 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
260 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
263 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
264 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
265 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
266 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
267 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
268 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
271 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";