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