(* Title: test for rewtools.sml

   authors: Walther Neuper 2000, 2006

*)

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

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

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

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

(*============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! =================

"----------- fun make_isab ------------------------------";

"----------- fun collect_isab_thys ----------------------";

============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ===============*)

"----------- fun thy_containing_rls ---------------------";

"----------- fun thy_containing_cal ---------------------";

(*============ inhibit exn WN120321 ==============================================

"----------- initContext Thy_ Integration-demo ----------";

"----------- initContext..Thy_, fun context_thm ---------";

"----------- initContext..Thy_, fun context_rls ---------";

"----------- checkContext..Thy_, fun context_thy --------";

"----------- checkContext..Thy_, fun context_rls --------";

"----------- checkContext..Thy_ on last formula ---------"; 

"----------- fun guh2theID ------------------------------";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

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

"----------- fun string_of_thmI for_[.]_) ---------------";

"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";

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

"----------- fun filter_appl_rews -----------------------";

"----------- fun is_contained_in ------------------------";

============ inhibit exn WN120321 ==============================================*)

"-------- build fun get_bdv_subst --------------------------------";

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

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

"----------- fun make_isab ------------------------------";

"----------- fun make_isab ------------------------------";

(*============ inhibit exn WN120321 ==============================================

"----------- fun make_isab ------------------------------";

(* rlsthmsNOTisac: contains thms in rls requested from Isabelle ---" *)

map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)

["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",

 "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",

 "sym_real_mult_minus1", "distrib_right", "distrib_left",

 "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",

 "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",

 "add_0_left", "add_0_right", "divide_zero_left", "sym_mult_assoc",

 "order_refl", "minus_minus", "mult_commute", "mult_assoc",

 "add_commute", "add_left_commute", "add_assoc", "minus_mult_left",

 "right_minus", "sym_add_assoc", "left_diff_distrib",

 "right_diff_distrib", "minus_divide_left", "times_divide_eq_right",

 "times_divide_eq_left", "divide_divide_eq_left",

 "divide_divide_eq_right", "divide_1", "add_divide_distrib",

 "sym_rmult_assoc"]; 

if length rlsthmsNOTisac > 34 then () 

else error "rewtools.sml: some rlsthmsNOTisac dropped";

"----- FIXME.WN11xxxx: rlsthmsNOTisac DOES contain thms from isac ---";

map (thmID_of_derivation_name o #1) rlsthmsNOTisac;

"----- FIXME.WN11xxxx: sym_* in rlsthmsNOTisac DOES contain thms from isac ---";

val symthms = [("real_mult_minus1", @{thm real_mult_minus1}),

               ("realpow_twoI", @{thm realpow_twoI}),

               ("realpow_addI", @{thm realpow_addI}),

               ("real_mult_2", @{thm real_mult_2}),

               ("mult_assoc", @{thm mult_assoc}),

               ("add_assoc", @{thm add_assoc}),

               ("rmult_assoc", @{thm rmult_assoc})];

map (Thm.derivation_name o #2) symthms;

"----------- fun collect_isab_thys ----------------------";

"----------- fun collect_isab_thys ----------------------";

"----------- fun collect_isab_thys ----------------------";

val ancestors = Theory.ancestors_of @{theory "Complex_Main"};

val isabthms = (flat o (map Theory.axioms_of)) ancestors;

val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset');

(*thms from rulesets*)

(*=== inhibit exn AK110725 =============================================================

val isacrlsthms = ((map rep_thm_G') o flat o 

		 (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');

length isacrlsthms;

(*takes a few seconds...

val isacrlsthms = gen_distinct eq_thmI isacrlsthms;

length isacrlsthms;

"----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";

print_depth 99; map #1 isacrlsthms; print_depth 3;

"----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";

...*)

(!theory');

map #2 (!theory');

map (PureThy.all_thms_of o #2) (!theory');

val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');

(*takes a few seconds...

val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

length rlsthmsNOTisac;

"----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";

print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;

"----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";

...*)

"----- for 'fun make_isab_thm_thy'";

inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));

inter eq_thmI;

(inter eq_thmI);

(inter eq_thmI) isacrlsthms;

(*takes a few seconds...

curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));

val thy = (nth 52 ancestors);

val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);

length (PureThy.all_thms_of (nth 9 ancestors));

length sec;

...*)

(*takes 1 minute...

print_depth 99; 

map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;

print_depth 3;

*)

(*takes some seconds...

val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))

		       ((#ancestors o rep_theory) first_isac_thy);

print_depth 99; isab_thm_thy; print_depth 3;

*)

=== inhibit exn AK110725 =============================================================*)

============ inhibit exn WN120321 ==============================================*)

"----------- fun thy_containing_rls ---------------------";

"----------- fun thy_containing_rls ---------------------";

"----------- fun thy_containing_rls ---------------------";

infix mem; (*from Isabelle2002*)

fun x mem [] = false

  | x mem (y :: ys) = x = y orelse x mem ys;

val thy' = "Biegelinie";

    val dropthys =

      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

        (rev (!theory'));

(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

if length (!theory') <> length dropthys then ()

else error "thy_containing_rls changed 1";

		    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;

if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"](*, "Biegelinie",..,"Test",.*)

then () else error "thy_containing_rls changed ancestors_rls";

"Isac" mem dropthys';

op mem ("Isac", dropthys');

(op mem) o swap;

((op mem) o swap) (dropthys', "Isac");

curry ((op mem) o swap);

curry ((op mem) o swap) dropthys' "Isac";

		val ancestors_rls = 

		  filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))

		     (rev (!ruleset'));

take (10, map #1 ancestors_rls) = 

  ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", 

   "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)

(* WN120523 popped up again ?!?!?

if length (!ruleset') <> length ancestors_rls then ()

else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";

*)

val rls' = "norm_Poly";

case assoc (ancestors_rls, rls') of

    SOME (thy', _) => thyID2theory' thy'

  | _ => error ("thy_containing_rls : rls '" ^ rls' ^

			  "' not in !rulset' und thy '" ^ thy' ^ "'");

if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly") then ()

else error "thy_containing_rls 3: changed with (Biegelinie, norm_Poly)";

"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie" ,"norm_Poly");

    val rls' = strip_thy rls'

    val thy' = thyID2theory' thy'

    val dropthys =

      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

        (rev (!theory'));

map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*)

    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;

		    val ancestors_rls = 

		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))

		        (rev (!ruleset'));

case assoc (ancestors_rls, rls') of

  SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()

| _ => error "thy_containing_rls changed 2";

============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

"----------- fun thy_containing_cal ---------------------";

"----------- fun thy_containing_cal ---------------------";

"----------- fun thy_containing_cal ---------------------";

val thy' = "Atools";

    val dropthys =

      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

        (rev (!theory'));

length dropthys <> length (!theory');

    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;

(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",

  "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",

  "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",

  "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)

then () else error "thy_containing_cal changed ancestors_rls for Atools";

(rev (!calclist'));

map #1 (rev (!calclist'));

map (#1 : calc -> string) (rev (!calclist'));

    val ancestors_cal =

      filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))

        (rev (!calclist'));

if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus") 

                    (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*)

then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed";

============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

"----------- initContext Thy_ Integration-demo ----------";

"----------- initContext Thy_ Integration-demo ----------";

"----------- initContext Thy_ Integration-demo ----------";

states:=[];

CalcTree

[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"], 

  ("Integrate",["integrate","function"],

  ["diff","integration"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([1],Res);

interSteps 1 ([1,1],Res);

val ((pt,p),_) = get_calc 1; show_pt pt;

if existpt' ([1,1,1], Frm) pt then ()

else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";

initContext  1 Thy_ ([1,1,1], Frm);

"----------- initContext..Thy_, fun context_thm ---------";

"----------- initContext..Thy_, fun context_thm ---------";

"----------- initContext..Thy_, fun context_thm ---------";

states:=[]; (*start of calculation, return No.1*)

CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

"----- no thy-context at result -----";

val p = ([], Res);

initContext 1 Thy_ p;

interSteps 1 ([2], Res);

interSteps 1 ([3,1], Res);

val ((pt,_),_) = get_calc 1; show_pt pt;

val p = ([2,4], Res);

val tac = Rewrite ("radd_left_commute","");

(*============ inhibit exn WN120321 ==============================================

initContext 1 Thy_ p;

(*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0

  --- in initContext..Thy_ ---*)

val ContThm {thm,result,...} = context_thy (pt,p) tac;

(*WN130621: thm = "thy_isac_WN120320: AT Isa2009-2-->11 BROKEN": guh !!!!!!!!!!!!!!!!!!!!!!!!!*)

if thm = "thy_isac_Test-thm-radd_left_commute" 

   andalso term2str result = "-2 + (1 + x) = 0" then ()

else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";

val p = ([3,1,1], Frm);

val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));

initContext 1 Thy_ p;

(*Frm->Res, Rewrite_Inst "risolate_bdv_add"  -1 + x = 0 -> x = 0 + -1 * -1

  --- in initContext..Thy_ ---*)

val ContThmInst {thm,result,...} = context_thy (pt,p) tac;

if thm =  "thy_isac_Test-thm-risolate_bdv_add"

   andalso term2str result = "x = 0 + -1 * -1" then ()

else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

initContext 1 Thy_ ([2,5], Res);

(*Res->Res, Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0

  --- in initContext..Thy_ ---*)

"----------- initContext..Thy_, fun context_rls ---------";

"----------- initContext..Thy_, fun context_rls ---------";

"----------- initContext..Thy_, fun context_rls ---------";

(*using pt from above*)

val p = ([1], Res);

val tac = Rewrite_Set "Test_simplify";

initContext 1 Thy_ p;

(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0

  --- in initContext..Thy_ ---*)

val ContRls {rls,result,...} = context_thy (pt,p) tac;

if rls = "thy_isac_Test-rls-Test_simplify" 

   andalso term2str result = "-1 + x = 0" then ()

else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

val p = ([3,1], Frm);

val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");

initContext 1 Thy_ p;

(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 ->  x = 0 + -1 * -1

  --- in initContext..Thy_ ---*)

val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;

if rls =  "thy_isac_Test-rls-isolate_bdv"

   andalso term2str result = "x = 0 + -1 * -1" then ()

else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

"----------- checkContext..Thy_, fun context_thy --------";

"----------- checkContext..Thy_, fun context_thy --------";

"----------- checkContext..Thy_, fun context_thy --------";

(*using pt from above*)

val p = ([2,4], Res);

val tac = Rewrite ("radd_left_commute","");

checkContext 1 p "thy_Test-thm-radd_left_commute";

(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0

  --- in checkContext..Thy_ ---*)

val ContThm {thm,result,...} = context_thy (pt,p) tac;

if thm =  "thy_isac_Test-thm-radd_left_commute"

   andalso term2str result = "-2 + (1 + x) = 0" then ()

else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";

val p = ([3,1,1], Frm);

val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));

checkContext 1 p "thy_Test-thm-risolate_bdv_add";

(* risolate_bdv_add:  -1 + x = 0 -> x = 0 + -1 * -1

  --- in checkContext..Thy_ ---*)

val ContThmInst {thm,result,...} = context_thy (pt,p) tac;

if thm =  "thy_isac_Test-thm-risolate_bdv_add"

   andalso term2str result = "x = 0 + -1 * -1" then ()

else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";

val p = ([2,5], Res);

val tac = Calculate "plus";

(*checkContext..Thy_ 1 ([2,5], Res);*)

(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)

checkContext 1 p ;

(* Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0

  --- in checkContext..Thy_ ---*)

"----------- checkContext..Thy_, fun context_rls --------";

"----------- checkContext..Thy_, fun context_rls --------";

"----------- checkContext..Thy_, fun context_rls --------";

(*using pt from above*)

show_pt pt;

val p = ([1], Res);

val tac = Rewrite_Set "Test_simplify";

checkContext 1 p "thy_isac_Test-rls-Test_simplify";

(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0

  --- in checkContext..Thy_ ---*)

val ContRls {rls,result,...} = context_thy (pt,p) tac;

if rls = "thy_isac_Test-rls-Test_simplify" 

   andalso term2str result = "-1 + x = 0" then ()

else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";

val p = ([3,1], Frm);

val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");

checkContext 1 p "thy_Test-rls-isolate_bdv";

val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;

if rls = "thy_isac_Test-rls-isolate_bdv" 

   andalso term2str result = "x = 0 + -1 * -1" then ()

else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";

"----------- checkContext..Thy_ on last formula ---------"; 

"----------- checkContext..Thy_ on last formula ---------"; 

"----------- checkContext..Thy_ on last formula ---------"; 

states:=[]; (*start of calculation, return No.1*)

CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

initContext 1 Thy_ ([1], Frm);

checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";

autoCalculate 1 (Step 1);

val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

initContext 1 Thy_ ([1], Res);

checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";

============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

"----------- fun guh2theID ------------------------------";

"----------- fun guh2theID ------------------------------";

"----------- fun guh2theID ------------------------------";

val guh = "thy_scri_ListG-thm-zip_Nil";

print_depth 3; (*999*)

take_fromto 1 4 (Symbol.explode guh);

take_fromto 5 9 (Symbol.explode guh);

val rest = takerest (9,(Symbol.explode guh)); 

separate "-" rest;

space_implode "-" rest;

commas rest;

val delim = "-";

val thyID = takewhile [] (not o (curry op= delim)) rest;

val rest' = dropuntil (curry op= delim) rest;

val setc = take_fromto 1 5 rest';

val xstr = takerest (5, rest');

if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()

else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

"----- initContext -----";

states:=[];

CalcTree 

    [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],

      ("Test",

       ["linear","univariate","equation","test"],

       ["Test","solve_linear"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

if is_curr_endof_calc pt ([1],Frm) then ()

else error "rewtools.sml is_curr_endof_calc ([1],Frm)";

autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

if not (is_curr_endof_calc pt ([1],Frm)) then ()

else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";

if is_curr_endof_calc pt ([1],Res) then ()

else error "rewtools.sml is_curr_endof_calc ([1],Res)";

initContext 1 Thy_ ([1],Res);

"----- checkContext -----";

states:=[];

CalcTree 

    [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],

      ("Test",

       ["linear","univariate","equation","test"],

       ["Test","solve_linear"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([1],Res);

val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";

interSteps 1 ([2],Res);

val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";

checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";

"----------- fun string_of_thmI for_[.]_) ---------------";

"----------- fun string_of_thmI for_[.]_) ---------------";

"----------- fun string_of_thmI for_[.]_) ---------------";

"----- these work ?!?";

(*========== inhibit exn 110718 ================================================

(* ERROR: constructor real_minus_eq_cancel has not been declared *)

val th = sym_thm real_minus_eq_cancel;

val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));

val th'= mk_thm ( @{theory "Isac"} ) ((de_quote o string_of_thm) real_minus_eq_cancel);

val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm) real_minus_eq_cancel);

"----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";

val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;

val Appl (Rewrite' (_,_,_,_,thm',_,_)) =

    applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));

"- compose stac as done in | appy (*leaf*) by handle_leaf";

val (th, sr, E, a, v, t) = 

    ("Biegelinie", 

     (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],

     [(str2term "q__::bool", str2term "q x = q_0")], 

     SOME (str2term "q x = q_0"),

     str2term "q__::bool", 

     str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");

val (a', STac stac) = handle_leaf "next  " th sr E a v t;

term2str stac;

"--- but this \"m\" is already corrupted";

val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;

"- because in assoc_thm'...";

val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));

val "s"::"y"::"m"::"_"::id = explode thmid;

((num_str o (get_thm thy)) (implode id)) RS sym;

((get_thm thy) (implode id)) RS sym;

"... this creates [.]";

((get_thm thy) (implode id));

"... while this has _NO_ [.]";

"----- thus we repair the [.] in string_of_thmI...";

val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;

if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()

else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^

		  " = " ^ string_of_thmI thm);

========== inhibit exn 110718 ================================================*)

"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";

"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";

"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";

states:=[];

CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

	     "RandbedingungenBiegung [y 0 = 0, y L = 0]",

	     "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

	     "FunktionsVariable x"],

	    ("Biegelinie",

	     ["MomentBestimmte","Biegelinien"],

	     ["IntegrierenUndKonstanteBestimmen"]))];

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1) (*Apply_Method*);

autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);

(*========== inhibit exn 110718 ================================================

"--- this was corrupted before 'fun string_of_thmI'";

val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;

if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel", 

				 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()

else error "rewtools.sml: string_of_thmI ?!?";

getTactic 1 ([1],Frm);

"----------- fun filter_appl_rews -----------------------";

"----------- fun filter_appl_rews -----------------------";

"----------- fun filter_appl_rews -----------------------";

val f = str2term "a + z + 2*a + 3*z + 5 + 6";

val thy = assoc_thy "Isac";

val subst = [(*TODO.WN071231 test Rewrite_Inst*)];

val rls = Test_simplify;

(* val rls = rls_p_33;      filter_appl_rews  ---> length 2

   val rls = norm_Poly;     filter_appl_rews  ---> length 1

   *)

if filter_appl_rews thy subst f rls =

   [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),

    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),

    Calculate "plus"] then () 

else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";

============ inhibit exn 110718 ==============================================*)

"----------- fun is_contained_in ------------------------";

"----------- fun is_contained_in ------------------------";

"----------- fun is_contained_in ------------------------";

val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});

if contains_rule r1 Test_simplify then ()

else error "rewtools.sml contains_rule Thm";

val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");

if contains_rule r1 Test_simplify then ()

else error "rewtools.sml contains_rule Calc";

val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");

if not (contains_rule r1 Test_simplify) then ()

else error "rewtools.sml contains_rule Calc";

"-------- build fun get_bdv_subst --------------------------------";

"-------- build fun get_bdv_subst --------------------------------";

"-------- build fun get_bdv_subst --------------------------------";

val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];

val env = [(str2term "v_v", str2term "x")];

subst2str env = "[\"\n(v_v, x)\"]";

"~~~~~ fun get_bdv_subst, args:"; val (prog, env) = (prog, env);

    fun scan (Const _) = NONE

      | scan (Free _) = NONE

      | scan (Var _) = NONE

      | scan (Bound _) = NONE

      | scan (t as Const ("List.list.Cons", _) $

         (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =

           if is_bdv_subst t then SOME t else NONE

      | scan (Abs (_, _, body)) = scan body

      | scan (t1 $ t2) =

          case scan t1 of

            NONE => scan t2

          | SOME subst => SOME subst

val SOME tm = scan prog;

val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair: subst;

if term2str tm = "[(bdv, v_v)]" then () else error "get_bdv_subst changed 1";

if subst2subs subst = ["(bdv, x)"] then () else error "get_bdv_subst changed 2";

case get_bdv_subst prog env of

  (SOME ["(bdv, x)"], [(Free ("bdv", _), Free ("x", _))]: subst) => ()

| _ => error "get_bdv_subst changed 3";

val (SOME subs, _) = get_bdv_subst prog env;

Rewrite_Inst (subs, ("diff_sin_chain","")) (*<<<----- this is the intended usage*)