1.1 --- a/test/Tools/isac/Test_Some.thy Sun Oct 09 09:01:29 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Wed Oct 19 10:43:04 2022 +0200
1.3 @@ -57,30 +57,31 @@
1.4 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
1.6 "xx"
1.7 -^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
1.8 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
1.9 -\<close> ML \<open>
1.10 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
1.11 -\<close> ML \<open> (*//---------------- adhoc copied up -----------------------------------------------\\*)
1.12 -\<close> ML \<open>
1.13 -\<close> ML \<open> (*\\---------------- adhoc copied up -----------------------------------------------//*)
1.14 -(*/------------------- step into XXXXX -----------------------------------------------------\*)
1.15 -(*-------------------- stop step into XXXXX -------------------------------------------------*)
1.16 -(*\------------------- step into XXXXX -----------------------------------------------------/*)
1.17 -(*-------------------- contiue step into XXXXX ----------------------------------------------*)
1.18 -(*/------------------- check entry to XXXXX ------------------------------------------------\*)
1.19 -(*\------------------- check entry to XXXXX ------------------------------------------------/*)
1.20 -(*/------------------- check within XXXXX --------------------------------------------------\*)
1.21 -(*\------------------- check within XXXXX --------------------------------------------------/*)
1.22 -(*/------------------- check result of XXXXX -----------------------------------------------\*)
1.23 -(*\------------------- check result of XXXXX -----------------------------------------------/*)
1.24 -(* final test ...*)
1.25 -(*/------------------- build new fun XXXXX -------------------------------------------------\*)
1.26 -(*\------------------- build new fun XXXXX -------------------------------------------------/*)
1.27 -(**** chapter ############################################################################ ****)
1.28 -(*** section ============================================================================== ***)
1.29 -(** subsection ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ **)
1.30 -(* subsubsection ............................................................................ *)
1.31 +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)
1.32 +\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
1.33 + (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
1.34 +(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
1.35 +\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
1.36 +
1.37 +\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
1.38 +(*//------------------ step into XXXXX -----------------------------------------------------\\*)
1.39 +(*-------------------- stop step into XXXXX --------------------------------------------------*)
1.40 +\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
1.41 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
1.42 +\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
1.43 +
1.44 +(*/------------------- check entry to XXXXX -------------------------------------------------\*)
1.45 +(*\------------------- check entry to XXXXX -------------------------------------------------/*)
1.46 +(*/------------------- check within XXXXX ---------------------------------------------------\*)
1.47 +(*\------------------- check within XXXXX ---------------------------------------------------/*)
1.48 +(*/------------------- check result of XXXXX ------------------------------------------------\*)
1.49 +(*\------------------- check result of XXXXX ------------------------------------------------/*)
1.50 +(* final test ... ----------------------------------------------------------------------------*)
1.51 +
1.52 +\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
1.53 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
1.54 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
1.55 +\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
1.56 \<close> ML \<open>
1.57 \<close>
1.58 ML \<open>
1.59 @@ -108,10 +109,476 @@
1.60 \<close> ML \<open>
1.61 \<close>
1.62
1.63 -section \<open>===================================================================================\<close>
1.64 +section \<open>========= test/../Knowlegde/equsystem-1a.sml ======================================\<close>
1.65 ML \<open>
1.66 \<close> ML \<open>
1.67 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
1.68 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
1.69 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
1.70 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.71 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.72 + "solveForVars [c, c_2]", "solution LL"];
1.73 +val (dI',pI',mI') =
1.74 + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
1.75 + ["EqSystem", "normalise", "2x2"]);
1.76 +val p = e_pos'; val c = [];
1.77 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.79 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.82 +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
1.83 + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
1.84 +
1.85 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.86 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.87 +
1.88 +(*+*)if f2str f =
1.89 + "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^
1.90 + " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";
1.91 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) =
1.92 + "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)";
1.93 +
1.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.98 +
1.99 +(*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;
1.100 + val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)" =
1.101 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
1.102 +
1.103 +case nxt of
1.104 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
1.105 + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
1.106 +
1.107 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.109 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.111 +case nxt of
1.112 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
1.113 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
1.114 +
1.115 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.116 +
1.117 + val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.118 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
1.119 +
1.120 +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;
1.121 +(*/------------------- step into me Apply_Method -------------------------------------------\*)
1.122 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
1.123 \<close> ML \<open>
1.124 + val (pt'''', p'''') = (* keep for continuation*)
1.125 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1.126 +
1.127 + case Step.by_tactic tac (pt, p) of
1.128 + ("ok", (_, _, ptp)) => ptp;
1.129 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.130 +
1.131 +(*+isa==isa2*)val ([5], Met) = p;
1.132 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);
1.133 + val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.134 +(*+isa==isa2*)is1 |> Istate.string_of;
1.135 + val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.136 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
1.137 +
1.138 + (*case*)
1.139 + Step.check tac (pt, p) (*of*);
1.140 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );
1.141 +
1.142 +(*+*)val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.143 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);
1.144 +
1.145 + (*if*) Tactic.for_specify tac (*else*);
1.146 +val Applicable.Yes xxx =
1.147 +
1.148 +Solve_Step.check tac (ctree, pos);
1.149 +
1.150 +(*+*)val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.151 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);
1.152 +
1.153 +"~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);
1.154 + (*if*) Tactic.for_specify' tac' (*else*);
1.155 +
1.156 +Step_Solve.by_tactic tac' ptp;;
1.157 +"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))
1.158 + = (tac', ptp);
1.159 +
1.160 +(*+*)val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.161 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
1.162 +
1.163 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
1.164 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
1.165 + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
1.166 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
1.167 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.168 + val {ppc, ...} = MethodC.from_store ctxt mI;
1.169 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
1.170 + val srls = LItool.get_simplifier (pt, pos)
1.171 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
1.172 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
1.173 +
1.174 +(*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =
1.175 +(*+isa==isa2*)is |> Istate.string_of
1.176 +
1.177 + val ini = LItool.implicit_take prog env;
1.178 + val pos = start_new_level pos
1.179 +val NONE =
1.180 + (*case*) ini (*of*);
1.181 + val (tac''', ist''', ctxt''') =
1.182 + case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
1.183 + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
1.184 +
1.185 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
1.186 +(*+isa==isa2*)ist''' |> Istate.string_of;
1.187 +
1.188 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
1.189 + = (prog ,(pt, (lev_dn p, Res)), is, ctxt);
1.190 +val Accept_Tac
1.191 + (Take' ttt, iii, _) =
1.192 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
1.193 +
1.194 +(*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term);
1.195 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
1.196 +(*+isa==isa2*)(Pstate iii |> Istate.string_of);
1.197 +
1.198 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
1.199 + = ((prog, (ptp, ctxt)), (Pstate ist));
1.200 + (*if*) path = [] (*then*);
1.201 +
1.202 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
1.203 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
1.204 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
1.205 +
1.206 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
1.207 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
1.208 + = (cc ,(ist |> path_down [L, R]), e);
1.209 +
1.210 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
1.211 +(*+isa==isa2*)(Pstate ist |> Istate.string_of);
1.212 +
1.213 + (*if*) Tactical.contained_in t (*else*);
1.214 +
1.215 + (*case*)
1.216 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
1.217 +"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)
1.218 + = ("next ", ctxt, eval, (get_subst ist), t);
1.219 +
1.220 + (*case*)
1.221 + Prog_Tac.eval_leaf E a v t (*of*);
1.222 +"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))
1.223 + = (E, a, v, t);
1.224 +
1.225 +val return =
1.226 + (Program.Tac (subst_atomic E t), NONE:term option);
1.227 +"~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;
1.228 + val stac' = Rewrite.eval_prog_expr ctxt srls
1.229 + (subst_atomic (Env.update_opt E (a, v)) stac)
1.230 +
1.231 +val return =
1.232 + (Program.Tac stac', a');
1.233 +"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;
1.234 +
1.235 + check_tac cc ist (prog_tac, form_arg);
1.236 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
1.237 + = (cc, ist, (prog_tac, form_arg));
1.238 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
1.239 +val _ =
1.240 + (*case*) m (*of*); (*tac as string/input*)
1.241 +
1.242 + (*case*)
1.243 +Solve_Step.check m (pt, p) (*of*);
1.244 +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));
1.245 +
1.246 +val return =
1.247 + check_tac cc ist (prog_tac, form_arg)
1.248 +
1.249 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
1.250 +(*+isa==isa2*)(Pstate ist |> Istate.string_of);
1.251 +
1.252 +"~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";
1.253 + val (Accept_Tac (tac, ist, ctxt)) = return;
1.254 +
1.255 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
1.256 +(*+isa==isa2*)(Pstate ist |> Istate.string_of)
1.257 +
1.258 +val return =
1.259 + Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);
1.260 +"~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;
1.261 + val (tac', ist', ctxt') = (tac, ist, ctxt)
1.262 +val Tactic.Take' t =
1.263 + (*case*) tac' (*of*);
1.264 + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
1.265 +
1.266 +(*+isa==isa2*)pos; (*from check_tac*)
1.267 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];
1.268 + val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
1.269 +(*+isa==isa2*)is1 |> Istate.string_of;
1.270 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
1.271 +(*+isa==isa2*)(ist' |> Istate.string_of)
1.272 +(*-------------------- stop step into me Apply_Method ----------------------------------------*)
1.273 +(*+isa==isa2*)val "c_2 = 0" = f2str f;
1.274 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
1.275 +(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of)
1.276 +(*\\------------------- step into me Apply_Method ------------------------------------------//*)
1.277 +
1.278 +\<close> ML \<open>
1.279 +val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;
1.280 +\<close> ML \<open>
1.281 +(*+isa==isa2*)val ([5, 1], Frm) = p'''';
1.282 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;
1.283 +(*+isa<>isa2*)val (**)Check_Postcond ["triangular", "2x2", "LINEAR", "system"](** )
1.284 + Substitute ["c_2 = 0"]( **) = nxt'''';
1.285 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');
1.286 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
1.287 +(*+isa==isa2*)is1 |> Istate.string_of;
1.288 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
1.289 +(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of;
1.290 +\<close> ML \<open> (*//----------- step into me Take ---------------------------------------------------\\*)
1.291 +(*//------------------ step into me Take ---------------------------------------------------\\*)
1.292 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
1.293 +\<close> ML \<open>
1.294 + val (pt, p) = (* keep for continuation*)
1.295 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1.296 +
1.297 + case Step.by_tactic tac (pt, p) of
1.298 + ("ok", (_, _, ptp)) => ptp;
1.299 +\<close> ML \<open>
1.300 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
1.301 +(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of;
1.302 +\<close> ML \<open>
1.303 + (*case*)
1.304 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.305 +\<close> ML \<open>
1.306 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
1.307 +\<close> ML \<open>
1.308 + (*if*) Pos.on_calc_end ip (*else*);
1.309 +\<close> ML \<open>
1.310 + val (_, probl_id, _) = Calc.references (pt, p);
1.311 +\<close> ML \<open>
1.312 +val _ =
1.313 + (*case*) tacis (*of*);
1.314 +\<close> ML \<open>
1.315 + (*if*) probl_id = Problem.id_empty (*else*);
1.316 +\<close> ML \<open>
1.317 + switch_specify_solve p_ (pt, ip);
1.318 +\<close> ML \<open>
1.319 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.320 +\<close> ML \<open>
1.321 + (*if*) Pos.on_specification ([], state_pos) (*else*);
1.322 +\<close> ML \<open>
1.323 + LI.do_next (pt, input_pos);
1.324 +\<close> ML \<open>
1.325 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
1.326 +\<close> ML \<open>
1.327 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.328 +\<close> ML \<open>
1.329 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.330 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
1.331 +\<close> ML \<open>
1.332 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
1.333 +(*+isa==isa2*)ist |> Istate.string_of;
1.334 +\<close> ML \<open>
1.335 + (*case*)
1.336 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.337 +\<close> ML \<open>
1.338 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
1.339 + = (sc, (pt, pos), ist, ctxt);
1.340 +\<close> ML \<open>
1.341 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
1.342 +\<close> ML \<open>
1.343 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
1.344 + = ((prog, (ptp, ctxt)), (Pstate ist));
1.345 +\<close> ML \<open>
1.346 + (*if*) path = [] (*else*);
1.347 +\<close> ML \<open>
1.348 + go_scan_up (prog, cc) (trans_scan_up ist);
1.349 +\<close> ML \<open>
1.350 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
1.351 + = ((prog, cc), (trans_scan_up ist));
1.352 +\<close> ML \<open>
1.353 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" =
1.354 +(*+isa==isa2*)Pstate ist |> Istate.string_of;
1.355 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term;
1.356 +\<close> ML \<open>
1.357 + (*if*) path = [R] (*root of the program body*) (*else*);
1.358 +\<close> ML \<open>
1.359 + scan_up pcc (ist |> path_up) (go_up path sc);
1.360 +\<close> ML \<open>
1.361 +"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
1.362 + = (pcc, (ist |> path_up), (go_up path sc));
1.363 +\<close> ML \<open>
1.364 + val (i, body) = check_Let_up ist sc
1.365 +\<close> ML \<open>
1.366 + (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
1.367 +\<close> ML \<open>
1.368 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
1.369 + = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
1.370 +\<close> ML \<open>
1.371 +val goback =
1.372 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
1.373 +\<close> ML \<open>
1.374 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))
1.375 + = (cc, (ist |> path_down [L, R]), e);
1.376 +\<close> ML \<open>
1.377 + (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
1.378 +\<close> ML \<open>
1.379 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
1.380 + = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
1.381 +\<close> ML \<open>
1.382 + (*if*) Tactical.contained_in t (*else*);
1.383 +\<close> ML \<open>
1.384 + (*case*)
1.385 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
1.386 +\<close> ML \<open>
1.387 +"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)
1.388 + = ("next ", ctxt, eval, (get_subst ist), t);
1.389 +\<close> ML \<open>
1.390 +val (Program.Tac stac, a') =
1.391 + (*case*) Prog_Tac.eval_leaf E a v t (*of*);
1.392 +\<close> ML \<open>
1.393 + val stac' = Rewrite.eval_prog_expr ctxt srls
1.394 + (subst_atomic (Env.update_opt E (a, v)) stac)
1.395 +\<close> ML \<open>
1.396 +(*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term;
1.397 +\<close> ML \<open>
1.398 +val return =
1.399 + (Program.Tac stac', a')
1.400 +\<close> ML \<open>
1.401 +"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))
1.402 + = (return);
1.403 +\<close> ML \<open>
1.404 + check_tac cc ist (prog_tac, form_arg);
1.405 +\<close> ML \<open>
1.406 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
1.407 + = (cc, ist, (prog_tac, form_arg));
1.408 +\<close> ML \<open>
1.409 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
1.410 +\<close> ML \<open>
1.411 +val _ =
1.412 + (*case*) m (*of*);
1.413 +\<close> ML \<open>
1.414 + (*case*)
1.415 +Solve_Step.check m (pt, p) (*of*);
1.416 +\<close> ML \<open>
1.417 +"~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))
1.418 + = (m, (pt, p));
1.419 +\<close> ML \<open>
1.420 + val pp = Ctree.par_pblobj pt p
1.421 + val ctxt = Ctree.get_loc pt pos |> snd
1.422 + val thy = Proof_Context.theory_of ctxt
1.423 + val f = Calc.current_formula cs;
1.424 + val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
1.425 + val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)
1.426 + val ro = get_rew_ord ctxt rew_ord'
1.427 +\<close> ML \<open>
1.428 + (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);
1.429 +\<close> ML \<open>
1.430 +(*+isa==isa2*)sube : TermC.as_string list
1.431 +\<close> ML \<open>
1.432 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term
1.433 +\<close> ML \<open>
1.434 +(*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map UnparseC.term
1.435 +\<close> ML \<open>
1.436 +val SOME ttt =
1.437 + (*case*) Rewrite.rewrite_terms_ ctxt ro erls subte f (*of*);
1.438 +\<close> ML \<open>
1.439 +\<close> ML \<open> (*//----------- build new fun Subst.input_to_terms ----------------------------------\\*)
1.440 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
1.441 +\<close> ML \<open>
1.442 +fun input_to_terms ctxt strs = map (TermC.parse ctxt) strs;
1.443 +\<close> ML \<open>
1.444 +input_to_terms: Proof.context -> Subst.input -> Subst.as_eqs
1.445 +\<close> ML \<open>
1.446 +(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type*)
1.447 +fun input_to_terms ctxt strs = strs
1.448 + |> map (TermC.parse ctxt)
1.449 + |> map (Model_Pattern.adapt_term_to_type ctxt)
1.450 +\<close> ML \<open>
1.451 +\<close> ML \<open>
1.452 +\<close> ML \<open>
1.453 +\<close> ML \<open>
1.454 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
1.455 +\<close> ML \<open> (*\\----------- build new fun Subst.input_to_terms ----------------------------------//*)
1.456 +\<close> ML \<open>
1.457 +\<close> ML \<open>
1.458 +\<close> ML \<open>
1.459 +\<close> ML \<open>
1.460 +\<close> ML \<open>
1.461 +\<close> ML \<open>
1.462 +\<close> ML \<open>
1.463 +\<close> ML \<open>
1.464 +\<close> text \<open>
1.465 +"~~~~~ from fun scan_dn \<longrightarrow>fun scan_up , return:"; val (Accept_Tac ict) = (goback);
1.466 +\<close> text \<open>
1.467 +"~~~~~ from fun scan_up \<longrightarrow>fun go_scan_up" ^
1.468 + " \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:"; val (Accept_Tac (tac, ist, ctxt))
1.469 + = (Accept_Tac ict);
1.470 +\<close> ML \<open>
1.471 +\<close> ML \<open>
1.472 +\<close> ML \<open>
1.473 +\<close> ML \<open>
1.474 +\<close> ML \<open>
1.475 +\<close> ML \<open>
1.476 +\<close> ML \<open>
1.477 +\<close> ML \<open>
1.478 +(*-------------------- stop step into me Take ------------------------------------------------*)
1.479 +\<close> ML \<open> (*------------- stop step into me Take ------------------------------------------------*)
1.480 +(*\\------------------ step into me Take ---------------------------------------------------//*)
1.481 +\<close> ML \<open> (*\\----------- step into me Take ---------------------------------------------------//*)
1.482 +\<close> ML \<open>
1.483 +val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f;
1.484 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.485 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.486 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.487 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.488 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.489 +\<close> ML \<open>
1.490 +(*+*)val (**)"L * c + c_2 = q_0 * L \<up> 2 / 2"(** )
1.491 + "[c = L * q_0 / 2, c_2 = 0]"( **) = f2str f;
1.492 +\<close> ML \<open>
1.493 + val "Pstate ([\"\n(e_s, [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])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
1.494 +(*val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =*)
1.495 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of)
1.496 +\<close> text \<open>
1.497 +case nxt of
1.498 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
1.499 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
1.500 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.501 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.502 +
1.503 +(* final test ... ----------------------------------------------------------------------------*)
1.504 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
1.505 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
1.506 +
1.507 +case nxt of
1.508 + (End_Proof') => ()
1.509 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
1.510 +\<close> ML \<open>
1.511 +Test_Tool.show_pt pt (*[
1.512 +(([], Frm), solveSystem
1.513 + [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
1.514 + [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
1.515 + [[c], [c_2]]),
1.516 +(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
1.517 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
1.518 +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
1.519 +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
1.520 +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
1.521 +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
1.522 +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
1.523 +(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
1.524 +
1.525 +(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
1.526 +(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
1.527 +(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
1.528 +(([5, 4], Res), c = L * q_0 / 2),
1.529 +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
1.530 +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.531 +(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.532 +(([], Res), [c = L * q_0 / 2, c_2 = 0])]
1.533 +*)
1.534 \<close> ML \<open>
1.535 \<close>
1.536
1.537 @@ -125,10 +592,26 @@
1.538 section \<open>code for copy & paste ===============================================================\<close>
1.539 ML \<open>
1.540 "~~~~~ fun xxx , args:"; val () = ();
1.541 -"~~~~~ and xxx , args:"; val () = ();
1.542 -"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
1.543 +"~~~~~ and xxx , args:"; val () = ();
1.544 +"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.545 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
1.546 "xx"
1.547 -^ "xxx" (*+*)
1.548 +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*+isa<>isa2*) (**)
1.549 +\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
1.550 + (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
1.551 +(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
1.552 +\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
1.553 +
1.554 +\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
1.555 +(*//------------------ step into XXXXX -----------------------------------------------------\\*)
1.556 +(*-------------------- stop step into XXXXX --------------------------------------------------*)
1.557 +\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
1.558 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
1.559 +\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
1.560 +
1.561 +\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
1.562 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
1.563 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
1.564 +\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
1.565 \<close>
1.566 end