(* Title: Knowledge/eqsystem-1a.sml

   author: Walther Neuper 050826,

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";

"----------- problems -----------------------------------------------------------equsystem-1.sml";

"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";

"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";

"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";

"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";

"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";

"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";

"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";

"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";

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

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

"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";

"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";

"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.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";

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

(*nxt = Apply_Method ["EqSystem", "normalise", "2x2"]*)

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

(*nxt = Rewrite_Set "norm_Rational" *)

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

(*nxt = Rewrite_Set_Inst (["(''bdv_1'', c)", "(''bdv_2'', c_2)"], "simplify_System_parenthesized")*)

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

(*nxt = Rewrite_Set_Inst (["(''bdv_1'', c)", "(''bdv_2'', c_2)"], "isolate_bdvs")*)

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

(*nxt = Rewrite_Set_Inst (["(''bdv_1'', c)", "(''bdv_2'', c_2)"], "simplify_System_parenthesized")*);

(*next in solve_EqSystem:solve_system2: Try (Rewrite_Set ''order_system'') ..is skipped*)

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

(*nxt = Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])*)

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

(*+*)val (NONE, SOME (ist, ctxt)) = Ctree.get_obj g_loc pt (fst p);

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

      val (pt, p) = 

  	    (*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;

      (*case*) 

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

"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) = 

  (p, ((pt, Pos.e_pos'), []));

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

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

val _ = (*case*) tacis (*of*);

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

           switch_specify_solve p_ (pt, ip);

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

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

        LI.do_next (pt, input_pos);

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

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

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

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

val Next_Step (Pstate {act_arg = t, ...}, _, _) = (*case*)

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

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

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

val Accept_Tac ((*tac*)Subproblem' _, _(*ist*), _(*ctxt*)) =

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

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

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

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

(*+*)path = [R, L, R, L, R, R, R, L, R, R];

val Accept_Tac (Subproblem' _, _(*ist*), _(*ctxt*)) =

           go_scan_up (prog, cc) (trans_scan_up ist);

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

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

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

(*+*)val [R, L, R, L, R, R, R, L, R, R] = path;

val Accept_Tac (Subproblem'

  (("Biegelinie", ["triangular", "2x2", "LINEAR", "system"], ["EqSystem", "top_down_substitution", "2x2"]), _, _, _, _, _), 

  istist, _) =

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

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _ )) = 

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

           go_scan_up pcc ist;

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

  (pcc, ist);

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

(*+*)val [R, L, R, L, R, R, R, L, R] = path;

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

"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) =

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

        val e2 = check_Seq_up ist sc

val Term_Val v =

        (*case*) scan_dn cc (ist |> path_up_down [R]) e2 (*of*);

           go_scan_up pcc (ist |> path_up |> set_act v |> set_found);

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

  (pcc, (ist |> path_up |> set_act v |> set_found));

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

(*+*)path = [R, L, R, L, R, R, R];

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

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _ )) = 

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

           go_scan_up pcc ist;

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

  (pcc, ist);

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

(*+*)path = [R, L, R, L, R, R];

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

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _ )) =

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

           go_scan_up pcc ist;

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

  (pcc, ist);

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

(*+*)path = [R, L, R, L, R];

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

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _ )) = 

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

          go_scan_up pcc ist;

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

  (pcc, ist);

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

(*+*)path = [R, L, R, L];

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

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _)) = 

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

          go_scan_up pcc ist;

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

  (pcc, ist);

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

(*+*)path = [R, L, R];

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

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

        val (i, body) = check_Let_up ist sc

val Accept_Tac _ = (*case*)

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

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

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

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

val (Program.Tac prog_tac, form_arg) =

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

           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;

"~~~~~ fun tac_from_prog , args:"; val (pt, _, (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =

  (pt, (Proof_Context.theory_of ctxt), prog_tac);

"~~~~~ from fun tac_from_prog \<longrightarrow>fun check_tac , return:"; val (m) =

  (fst (

Sub_Problem.tac_from_prog pt ptac));

"~~~~~ fun tac_from_prog , args:"; val (pt, (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags')) =

  (pt, ptac);

      val (dI, pI, mI) = Prog_Tac.dest_spec spec'

      val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt);;

      val ctxt = Proof_Context.init_global thy (*BETTER USE user_ctxt ?*)

	    val ags = TermC.isalist2list ags';

	      (*if*) mI = ["no_met"] (*then*);

            val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags): O_Model.T

		        val pI' = 

    Refine.refine_ori' ctxt pors pI;

val return = (pI', pors (* refinement over models with diff.prec only *), 

		          (hd o #met o Problem.from_store ctxt) pI');

(*-------------^^ THIS CAUSED THE ERROR Empty*)

(*+*)val ["LINEAR", "system"] = pI;

(*+*)fun app_ptyp x = Store.apply (get_pbls ()) x; (*redefine locally hidden*)

"~~~~~ fun refine_ori' , args:"; val (oris, pblID) = (pors, pI);

val SOME ["system", "LINEAR", "2x2", "triangular"] = 

           app_ptyp (Refine.refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);

"~~~~~ fun app_ptyp , args:"; val () = (); (*considered too expensive for testing*)

(*+*)val fmz = ["equalities [c_2 = (0::real), L * c + c_2 = q_0 * L \<up> 2 / 2]", 

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

(*+isa<>isa2*)Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];(*

*** pass ["system", "LINEAR"] 

*** pass ["system", "LINEAR", "2x2"] 

*** pass ["system", "LINEAR", "3x3"] 

*** pass ["system", "LINEAR", "4x4"] 

val it =

   [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 = []}),

    NoMatch

     (["2x2", "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 =

       [Correct "Length [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] = 2", False "Length v_s = 2"], With = []}),

-------------------------------------------------------- [c, c_2] NOT SUBSTUTED -----^^^

    NoMatch

     (["3x3", "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 =

       [False "Length [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] = 3", False "Length v_s = 3"], With = []}),

------------------------------------------------------ [c, c_2] NOT SUBSTUTED -----^^^

    NoMatch

     (["4x4", "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 =

       [False "Length [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] = 4", False "Length v_s = 4"], With = []})]:

------------------------------------------------------ [c, c_2] NOT SUBSTUTED -----^^^

   M_Match.T list*)

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

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

case nxt''''' of

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

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

val (p,f,nxt,pt) = (p''''',f''''',nxt''''',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;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 PblObj {probl,...} = get_obj I pt [5];

    (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;

(*[

(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]])),

(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),

(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]

*)

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;

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

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

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;

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