theory Test_Some

  imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"

begin 

ML \<open>open ML_System\<close>

ML \<open>

  open Kernel;

  open Math_Engine;

  open Test_Code;              CalcTreeTEST;

  open LItool;                 arguments_from_model;

  open Sub_Problem;

  open Fetch_Tacs;

  open Step

  open Env;

  open LI;                     scan_dn;

  open Istate;

  open Error_Pattern;

  open Error_Pattern_Def;

  open Specification;

  open Ctree;                  append_problem;

  open Pos;

  open Program;

  open Prog_Tac;

  open Tactical;

  open Prog_Expr;

  open Auto_Prog;              rule2stac;

  open Input_Descript;

  open Specify;

  open Specify;

  open Step_Specify;

  open Step_Solve;

  open Step;

  open Solve;                  (* NONE *)

  open ContextC;               transfer_asms_from_to;

  open Tactic;                 (* NONE *)

  open I_Model;

  open O_Model;

  open P_Model;                (* NONE *)

  open Rewrite;

  open Eval;                   get_pair;

  open TermC;                  atomt;

  open Rule;

  open Rule_Set;               Sequence;

  open Eval_Def

  open ThyC

  open ThmC_Def

  open ThmC

  open Rewrite_Ord

  open UnparseC

\<close>

(**)ML_file "BridgeJEdit/vscode-example.sml"(**)

section \<open>code for copy & paste ===============================================================\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

"xx"

^ "xxx"   (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)

\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

(*\\------------------ adhoc inserted n ----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

(*//------------------ step into XXXXX -----------------------------------------------------\\*)

(*-------------------- stop step into XXXXX --------------------------------------------------*)

\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

(*\\------------------ step into XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

(*/------------------- check entry to XXXXX -------------------------------------------------\*)

(*\------------------- check entry to XXXXX -------------------------------------------------/*)

(*/------------------- check within XXXXX ---------------------------------------------------\*)

(*\------------------- check within XXXXX ---------------------------------------------------/*)

(*/------------------- check result of XXXXX ------------------------------------------------\*)

(*\------------------- check result of XXXXX ------------------------------------------------/*)

(* final test ... ----------------------------------------------------------------------------*)

\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

(*//------------------ build new fun XXXXX -------------------------------------------------\\*)

(*\\------------------ build new fun XXXXX -------------------------------------------------//*)

\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

\<close> ML \<open>

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

text \<open>

  declare [[show_types]] 

  declare [[show_sorts]]            

  find_theorems "?a <= ?a"

  print_theorems

  print_facts

  print_statement ""

  print_theory

  ML_command \<open>Pretty.writeln prt\<close>

  declare [[ML_print_depth = 999]]

  declare [[ML_exception_trace]]

\<close>

section \<open>===================================================================================\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

section \<open>========= test/../Knowlegde/equsystem-1a.sml ======================================\<close>

ML \<open>

\<close> ML \<open>

"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\

	               \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", 

	   "solveForVars [c, c_2]", "solution LL"];

val (dI',pI',mI') =

  ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],

   ["EqSystem", "normalise", "2x2"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()

	  | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

(*+*)if 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]" then () else error "";

(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) =

   "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)";

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

(*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;

  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)" =

(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

case nxt of

    (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()

  | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

case nxt of

    (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

  | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";

val (p,_,f,nxt,_,pt) = me nxt p c pt;

  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)" =

(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;

(*/------------------- step into me Apply_Method -------------------------------------------\*)

"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);

\<close> ML \<open>

      val (pt'''', p'''') = (* keep for continuation*)

  	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

 case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp;

"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

(*+isa==isa2*)val ([5], Met) = p;

(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);

  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)" =

(*+isa==isa2*)is1 |> Istate.string_of;

  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)" =

(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

  (*case*)

      Step.check tac (pt, p) (*of*);

"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );

(*+*)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)" =

(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);

  (*if*) Tactic.for_specify tac (*else*);

val Applicable.Yes xxx =

Solve_Step.check tac (ctree, pos);

(*+*)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)" =

(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);

"~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);

	    (*if*)  Tactic.for_specify' tac' (*else*);

Step_Solve.by_tactic tac' ptp;;

"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))

  = (tac', ptp);

(*+*)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)" =

(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

        LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;

"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))

  = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);

         val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)

           PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

         val {ppc, ...} = MethodC.from_store ctxt mI;

         val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc

         val srls = LItool.get_simplifier (pt, pos)

         val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of

           (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)

(*+*)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)" =

(*+isa==isa2*)is |> Istate.string_of

        val ini = LItool.implicit_take prog env;

        val pos = start_new_level pos

val NONE =

        (*case*) ini (*of*);

            val (tac''', ist''', ctxt''') = 

   case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of

                Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)

  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)" =

(*+isa==isa2*)ist''' |> Istate.string_of;

"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

  = (prog ,(pt, (lev_dn p, Res)), is, ctxt);

val Accept_Tac

    (Take' ttt, iii, _) =

  (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

(*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term);

  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)" =

(*+isa==isa2*)(Pstate iii |> Istate.string_of);

"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Pstate ist));

  (*if*) path = [] (*then*);

           scan_dn cc (trans_scan_dn ist) (Program.body_of prog);

"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

  = (cc, (trans_scan_dn ist), (Program.body_of prog));

  (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);

"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

  = (cc ,(ist |> path_down [L, R]), e);

  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)" =

(*+isa==isa2*)(Pstate ist |> Istate.string_of);

    (*if*) Tactical.contained_in t (*else*);

      (*case*)

    LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)

  = ("next  ", ctxt, eval, (get_subst ist), t);

    (*case*)

  Prog_Tac.eval_leaf E a v t (*of*);

"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))

  = (E, a, v, t);

val return =

     (Program.Tac (subst_atomic E t), NONE:term option);

"~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;

	        val stac' = Rewrite.eval_prog_expr ctxt srls 

              (subst_atomic (Env.update_opt E (a, v)) stac)

val return =

      (Program.Tac stac', a');

"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;

           check_tac cc ist (prog_tac, form_arg);

"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

  = (cc, ist, (prog_tac, form_arg));

    val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac

val _ =

    (*case*) m (*of*); (*tac as string/input*)

      (*case*)

Solve_Step.check m (pt, p) (*of*);

"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));

val return =

    check_tac cc ist (prog_tac, form_arg)

  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)" =

(*+isa==isa2*)(Pstate ist |> Istate.string_of);

"~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";

       val (Accept_Tac (tac, ist, ctxt)) = return;

  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)" =

(*+isa==isa2*)(Pstate ist |> Istate.string_of)

val return =

      Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);

"~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;

            val (tac', ist', ctxt') = (tac, ist, ctxt)

val Tactic.Take' t =

            (*case*) tac' (*of*);

                  val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');

(*+isa==isa2*)pos; (*from check_tac*)

(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];

  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)" =

(*+isa==isa2*)is1 |> Istate.string_of;

  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)" =

(*+isa==isa2*)(ist' |> Istate.string_of)

(*-------------------- stop step into me Apply_Method ----------------------------------------*)

(*+isa==isa2*)val "c_2 = 0" = f2str f;

  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)" =

(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of)

(*\\------------------- step into me Apply_Method ------------------------------------------//*)

\<close> ML \<open>

val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;

\<close> ML \<open>

(*+isa==isa2*)val ([5, 1], Frm) = p'''';

(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;

(*+isa<>isa2*)val (**)Check_Postcond ["triangular", "2x2", "LINEAR", "system"](** )

                       Substitute ["c_2 = 0"]( **) = nxt'''';

(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');

  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)" =

(*+isa==isa2*)is1 |> Istate.string_of;

  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)" =

(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of;

\<close> ML \<open> (*//----------- step into me Take ---------------------------------------------------\\*)

(*//------------------ step into me Take ---------------------------------------------------\\*)

"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');

\<close> ML \<open>

      val (pt, p) = (* keep for continuation*)

  	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

 case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp;

\<close> ML \<open>

  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)" =

(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of;

\<close> ML \<open>

    (*case*)

      Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

\<close> ML \<open>

"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));

\<close> ML \<open>

  (*if*) Pos.on_calc_end ip (*else*);

\<close> ML \<open>

      val (_, probl_id, _) = Calc.references (pt, p);

\<close> ML \<open>

val _ =

      (*case*) tacis (*of*);

\<close> ML \<open>

        (*if*) probl_id = Problem.id_empty (*else*);

\<close> ML \<open>

           switch_specify_solve p_ (pt, ip);

\<close> ML \<open>

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

\<close> ML \<open>

      (*if*) Pos.on_specification ([], state_pos) (*else*);

\<close> ML \<open>

        LI.do_next (pt, input_pos);

\<close> ML \<open>

"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);

\<close> ML \<open>

    (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);

\<close> ML \<open>

        val thy' = get_obj g_domID pt (par_pblobj pt p);

	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;

\<close> ML \<open>

  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)" =

(*+isa==isa2*)ist |> Istate.string_of;

\<close> ML \<open>

        (*case*) 

        LI.find_next_step sc (pt, pos) ist ctxt (*of*);

\<close> ML \<open>

"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

  = (sc, (pt, pos), ist, ctxt);

\<close> ML \<open>

  (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

\<close> ML \<open>

"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Pstate ist));

\<close> ML \<open>

  (*if*) path = [] (*else*);

\<close> ML \<open>

           go_scan_up (prog, cc) (trans_scan_up ist);

\<close> ML \<open>

"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  = ((prog, cc), (trans_scan_up ist));

\<close> ML \<open>

  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)" =

(*+isa==isa2*)Pstate ist |> Istate.string_of;

(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term;

\<close> ML \<open>

    (*if*) path = [R] (*root of the program body*) (*else*);

\<close> ML \<open>

           scan_up pcc (ist |> path_up) (go_up path sc);

\<close> ML \<open>

"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))

  = (pcc, (ist |> path_up), (go_up path sc));

\<close> ML \<open>

        val (i, body) = check_Let_up ist sc

\<close> ML \<open>

  (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);

\<close> ML \<open>

"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

  = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);

\<close> ML \<open>

val goback =

  (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);

\<close> ML \<open>

"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))

  = (cc, (ist |> path_down [L, R]), e);

\<close> ML \<open>

  (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);

\<close> ML \<open>

"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

  = (cc, (ist |> path_down_form ([L, L, R], a)), e1);

\<close> ML \<open>

        (*if*) Tactical.contained_in t (*else*);

\<close> ML \<open>

      (*case*) 

    LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

\<close> ML \<open>

"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)

  = ("next  ", ctxt, eval, (get_subst ist), t);

\<close> ML \<open>

val (Program.Tac stac, a') =

    (*case*) Prog_Tac.eval_leaf E a v t (*of*);

\<close> ML \<open>

	        val stac' = Rewrite.eval_prog_expr ctxt srls 

              (subst_atomic (Env.update_opt E (a, v)) stac)

\<close> ML \<open>

(*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term;

\<close> ML \<open>

val return =

        (Program.Tac stac', a')

\<close> ML \<open>

"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))

   = (return);

\<close> ML \<open>

           check_tac cc ist (prog_tac, form_arg);

\<close> ML \<open>

"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

  = (cc, ist, (prog_tac, form_arg));

\<close> ML \<open>

    val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac

\<close> ML \<open>

val _ =

    (*case*) m (*of*);

\<close> ML \<open>

      (*case*)

Solve_Step.check m (pt, p) (*of*);

\<close> ML \<open>

"~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))

  = (m, (pt, p));

\<close> ML \<open>

        val pp = Ctree.par_pblobj pt p

        val ctxt = Ctree.get_loc pt pos |> snd

        val thy = Proof_Context.theory_of ctxt

        val f = Calc.current_formula cs;

		    val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)

		    val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)

		    val ro = get_rew_ord ctxt rew_ord'

\<close> ML \<open>

		    (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);

\<close> ML \<open>

(*+isa==isa2*)sube : TermC.as_string list

\<close> ML \<open>

(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term

\<close> ML \<open>

(*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map UnparseC.term

\<close> ML \<open>

val SOME ttt =

		      (*case*) Rewrite.rewrite_terms_ ctxt ro erls subte f (*of*);

\<close> ML \<open>

\<close> ML \<open> (*//----------- build new fun Subst.input_to_terms ----------------------------------\\*)

(*//------------------ build new fun XXXXX -------------------------------------------------\\*)

\<close> ML \<open>

fun input_to_terms ctxt strs = map (TermC.parse ctxt) strs;

\<close> ML \<open>

input_to_terms: Proof.context -> Subst.input -> Subst.as_eqs

\<close> ML \<open>

(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type*)

fun input_to_terms ctxt strs = strs

  |> map (TermC.parse ctxt)

  |> map (Model_Pattern.adapt_term_to_type ctxt)

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

(*\\------------------ build new fun XXXXX -------------------------------------------------//*)

\<close> ML \<open> (*\\----------- build new fun Subst.input_to_terms ----------------------------------//*)

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> text \<open>

"~~~~~ from fun scan_dn \<longrightarrow>fun scan_up , return:"; val (Accept_Tac ict) = (goback);

\<close> text \<open>

"~~~~~ from fun scan_up \<longrightarrow>fun go_scan_up" ^

       " \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:"; val (Accept_Tac (tac, ist, ctxt)) 

  =  (Accept_Tac ict);

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

(*-------------------- stop step into me Take ------------------------------------------------*)

\<close> ML \<open> (*------------- stop step into me Take ------------------------------------------------*)

(*\\------------------ step into me Take ---------------------------------------------------//*)

\<close> ML \<open> (*\\----------- step into me Take ---------------------------------------------------//*)

\<close> ML \<open>

val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

\<close> ML \<open>

(*+*)val (**)"L * c + c_2 = q_0 * L \<up> 2 / 2"(** )

             "[c = L * q_0 / 2, c_2 = 0]"( **) = f2str f;

\<close> ML \<open>

  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)" =

(*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)" =*)

(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of)

\<close> text \<open>

case nxt of

    (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()

  | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

(* final test ... ----------------------------------------------------------------------------*)

if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()

else error "eqsystem.sml me [EqSys...2x2] finished f2str f";

case nxt of

    (End_Proof') => ()

  | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

\<close> ML \<open>

Test_Tool.show_pt pt (*[

(([], Frm), solveSystem

 [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],

  [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]

 [[c], [c_2]]), 

(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]), 

(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]), 

(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]), 

(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]), 

(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]), 

(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),

(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2), 

(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2), 

(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2), 

(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L), 

(([5, 4], Res), c = L * q_0 / 2), 

(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), 

(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), 

(([5], Res), [c = L * q_0 / 2, c_2 = 0]), 

(([], Res), [c = L * q_0 / 2, c_2 = 0])] 

*)

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

section \<open>code for copy & paste ===============================================================\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

"xx"

^ "xxx"   (*+*) (*+++*) (* keep for continuation*) (*+isa<>isa2*) (**)

\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

(*\\------------------ adhoc inserted n ----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

(*//------------------ step into XXXXX -----------------------------------------------------\\*)

(*-------------------- stop step into XXXXX --------------------------------------------------*)

\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

(*\\------------------ step into XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

(*//------------------ build new fun XXXXX -------------------------------------------------\\*)

(*\\------------------ build new fun XXXXX -------------------------------------------------//*)

\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

\<close>

end