theory Test_Some

  imports Isac.Build_Thydata

  "~~/test/Tools/isac/ProgLang/calculate"    (* setup for calculate.sml*)

begin 

ML \<open>

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)

                      (* these vvv test, if funs are intermediately opened in structure 

                         in case of errors here consider ~~/xtest-to-coding.sh      *)

  open Kernel;

  open Math_Engine;            CalcTreeTEST;

  open Lucin;                  itms2args;

  open Env;

  open Exec;

  open LucinNEW;               scan_dn2;

  open Istate;

  open Inform;                 cas_input;

  open Rtools;                 trtas2str;

  open Chead;                  pt_extract;

  open Generate;               (* NONE *)

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

  open Applicable;             mk_set;

  open Solve;                  (* NONE *)

  open Selem;                  e_fmz;

  open Stool;                  (* NONE *)

  open ContextC;               transfer_asms_from_to;

  open Tactic;                 (* NONE *)

  open Model;                  (* NONE *)

  open Rewrite;                mk_thm;

  open Calc;                   get_pair;

  open TermC;                  atomt;

  open Celem;                  e_pbt;

  open Rule;                   string_of_thm;

(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

\<close>

ML_file "Interpret/lucas-interpreter.sml"

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

ML \<open>

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

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

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

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

"xx"

^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*)

\<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>

ML \<open>

(*========== inhibit exn WN130909 TODO =========================================================

============ inhibit exn WN130909 TODO ========================================================*)

\<close>

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

ML \<open>

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

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

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

\<close>

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

ML \<open>

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

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

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

\<close>

section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>

ML \<open>

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

\<close> ML \<open>

(* waits for finalising ctxt: want result [x = 6 / 5] instead of "[]"*)

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

(*ER-7*) (*Schalk I s.87 Bsp 55b*)

(* peculiarity of this example:

   show_pt_tac pt;

. . . . . . . . . . ("RatEq",["univariate","equation"],["no_met"]);

([], Frm), solve (x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x, x)

                                                                asm ^^^^^ "x \<noteq> 0"

. . . . . . . . . . Subproblem (PolyEq, ["normalise","polynomial","univariate","equation"]),

([4], Pbl), solve ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3), x)

. . . . . . . . . . Subproblem (PolyEq, ["bdv_only","degree_2","polynomial","univariate","equation"]),

([4,4], Pbl), solve (-6 * x + 5 * x ^^^ 2 = 0, x)

([4,4,5], Res), [x = 0, x = 6 / 5]

. . . . . . . . . . Check_Postcond ["bdv_only","degree_2","polynomial","univariate","equation"],

([4,4], Res), [x = 0, x = 6 / 5]

. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],

               ^^^^^ from_subpbl_to_caller must drop "x = 0" due to asm "x \<noteq> 0"

([5], Res), [x = 0, x = 6 / 5]

. . . . . . . . . . Check_Postcond ["rational","univariate","equation"],

([], Res), [x = 6 / 5]

*)

val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",

	   "solveFor x","solutions L"];

val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

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

(*---------solve (x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x, x)*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*[], Met*)val (p,_,f,nxt,_,pt''''') = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)

\<close> ML \<open>

(*+*)if p = ([], Met) andalso fst nxt = "Apply_Method" andalso

(*+*)terms2str (get_assumptions_ pt p) = "[]"

(*+*)then () else error "BEFORE 1 changed";

\<close> ML \<open>

(*//--1 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\

      1 relevant for init_pstate in root-pbl*)

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt''''';

(*\\--1 end step into relevant call ----------------------------------------------------------//*)

\<close> ML \<open>

(*+*)if p = ([1], Frm) andalso fst nxt = "Rewrite_Set" andalso

(*+*)terms2str (get_assumptions_ pt p) = "[\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"

(*+*)then () else error "AFTER 1 changed";

\<close> ML \<open>

(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)

(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "RatEq_eliminate"*)

\<close> ML \<open>

(*+*)if p = ([2], Res) andalso fst nxt = "Rewrite_Set" andalso

(*+*)terms2str (get_assumptions_ pt p) = "[\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"

(*+*)then () else error "BEFORE 2 changed";

\<close> ML \<open>

(*//--2 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\

      2 relevant for preconds like "x \<noteq> 0"                                                     *)

(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]*)

(*---------solve ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3), x)*)

(*\\--2 end step into relevant call ----------------------------------------------------------//*)

\<close> ML \<open>

(*+*)if p = ([3], Res) andalso fst nxt = "Subproblem" andalso

(*+*)terms2str (get_assumptions_ pt p) = "[\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"

(*+*)then () else error "AFTER 2 changed";

\<close> ML \<open>

(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)

(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)

\<close> ML \<open>

(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "normalise_poly"]*)

(*[4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)")*)

(*[4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)

(*---------solve (-6 * x + 5 * x ^^^ 2 = 0, x)*)

\<close> ML \<open>

(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)

(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)

(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)

(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]*)

(*[4, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_bdv_only_simplify")*)

(*[4, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)

(*[4, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)

(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)

(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_elementwise "Assumptions"*)

(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)

\<close> ML \<open>

(*+*)if p = ([4, 4, 5], Res) andalso fst nxt = "Check_Postcond" andalso

(*+*)terms2str (get_assumptions_ pt p) = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]"

(*+*)then () else error "BEFORE 8 changed";

\<close> ML \<open>

(*//--9 begin step into relevant call ----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\

      9 relevant for dropping "x = 0" due to asm "x \<noteq> 0"*)

(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [1] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)

\<close> ML \<open>

val ctxt = get_ctxt pt p;

terms2str (get_assumptions ctxt)

 = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]";

(*     ^^^ NOT evaluated                               ^^^ *)

\<close> ML \<open>

val ctxt = get_ctxt pt''''' p''''';

terms2str (get_assumptions ctxt)

 = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"

(* should formulas from calculation really go into ctxt ?                                                     ^^^^^     ^^^^^^^^^*)

\<close> ML \<open>

"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [1], pt);

\<close> ML \<open>

	    val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt, p) (*of*);

\<close> ML \<open>

val ctxt = get_ctxt (fst ptp''''') (snd ptp''''');

terms2str (get_assumptions ctxt)

 = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"

\<close> ML \<open>

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

\<close> ML \<open>

      val (mI, m) = Solve.mk_tac'_ tac;

\<close> ML \<open>

      val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

\<close> ML \<open>

      (*if*) member op = Solve.specsteps mI (*else*);

\<close> ML \<open>

      val Updated (tacis''''', pos's''''', ptp''''') = loc_solve_ (mI, m) ptp

\<close> ML \<open>

"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);

\<close> ML \<open>

     Solve.solve m (pt, pos);

\<close> ML \<open>

"~~~~~ fun solve , args:"; val (("Check_Postcond", Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))

  = (m, (pt, pos));

\<close> ML \<open>

\<close> ML \<open>

      val pp = par_pblobj pt p

\<close> ML \<open>

(*+*)(p, p_) = ([4, 4, 5], Res);

\<close> ML \<open>

(*+*)pp = [4, 4];

\<close> ML \<open>

(*+*)get_obj I pt (fst pos);

\<close> ML \<open>

PrfObj;

\<close> ML \<open>

      val Check_elementwise "Assumptions" = (*case*) get_obj g_tac pt p (*of*);

(* this   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ should be dropped asap *)

\<close> ML \<open>

show_pt_tac pt

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

(*\\--9 end step into relevant call ----------------------------------------------------------//*)

\<close> ML \<open>

(*+*)if p''''' = ([4, 4], Res) andalso fst nxt''''' = "Check_Postcond" andalso

(*+*)terms2str (get_assumptions_ pt''''' p''''') = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"

(*+*)then () else error "AFTER 8 changed";

\<close> ML \<open>

(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [1] pt''''';(*Check_elementwise "Assumptions"*)

(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)

(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*End_Proof'*)

\<close> ML \<open>

(*+*)if p = ([], Res) andalso f2str f = "[]" (*..must change*)andalso fst nxt = "End_Proof'" andalso

(*+*)terms2str (get_assumptions_ pt p) = "[\"x = 6 / 5\",\"x = 0\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]"

(*+*)then () else error "ERROR CHANGED: rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], End_Proof'";

\<close> ML \<open>

\<close> ML \<open>

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

\<close>

section \<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 xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));

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

"xx"

^ "xxx"   (*+*)

\<close>

end