(* SML functions for rational arithmetic

   WN.22.10.99

   use"../knowledge/Test.ML";

   use"Knowledge/Test.ML";

   use"Test.ML";

  *)

(** interface isabelle -- isac **)

theory' := overwritel (!theory', [("Test.thy",Test.thy)]);

(** evaluation of numerals and predicates **)

(*does a term contain a root ?*)

fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy = 

  if strip_thy op0 <> "is'_root'_free" 

    then raise error ("eval_root_free: wrong "^op0)

  else if const_in (strip_thy op0) arg

	 then SOME (mk_thmid thmid "" 

		    ((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

		    Trueprop $ (mk_equality (t, false_as_term)))

       else SOME (mk_thmid thmid "" 

		  ((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

		  Trueprop $ (mk_equality (t, true_as_term)))

  | eval_root_free _ _ _ _ = NONE; 

(*does a term contain a root ?*)

fun eval_contains_root (thmid:string) _ 

		       (t as (Const("Test.contains'_root",t0) $ arg)) thy = 

    if member op = (ids_of arg) "sqrt"

    then SOME (mk_thmid thmid "" 

			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

	       Trueprop $ (mk_equality (t, true_as_term)))

    else SOME (mk_thmid thmid "" 

			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

	       Trueprop $ (mk_equality (t, false_as_term)))

  | eval_contains_root _ _ _ _ = NONE; 

calclist':= overwritel (!calclist', 

   [("is_root_free", ("Test.is'_root'_free", 

		      eval_root_free"#is_root_free_")),

    ("contains_root", ("Test.contains'_root",

		       eval_contains_root"#contains_root_"))

    ]);

(** term order **)

fun term_order (_:subst) tu = (term_ordI [] tu = LESS);

(** rule sets **)

val testerls = 

  Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 

      erls = e_rls, srls = Erls, 

      calc = [], 

      rules = [Thm ("refl",num_str refl),

	       Thm ("le_refl",num_str le_refl),

	       Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

	       Thm ("not_true",num_str not_true),

	       Thm ("not_false",num_str not_false),

	       Thm ("and_true",and_true),

	       Thm ("and_false",and_false),

	       Thm ("or_true",or_true),

	       Thm ("or_false",or_false),

	       Thm ("and_commute",num_str and_commute),

	       Thm ("or_commute",num_str or_commute),

	       Calc ("Atools.is'_const",eval_const "#is_const_"),

	       Calc ("Tools.matches",eval_matches ""),

	       Calc ("op +",eval_binop "#add_"),

	       Calc ("op *",eval_binop "#mult_"),

	       Calc ("Atools.pow" ,eval_binop "#power_"),

	       Calc ("op <",eval_equ "#less_"),

	       Calc ("op <=",eval_equ "#less_equal_"),

	       Calc ("Atools.ident",eval_ident "#ident_")],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls;      

(*.for evaluation of conditions in rewrite rules.*)

(*FIXXXXXXME 10.8.02: handle like _simplify*)

val tval_rls =  

  Rls{id = "tval_rls", preconds = [], 

      rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")), 

      erls=testerls,srls = e_rls, 

      calc=[],

      rules = [Thm ("refl",num_str refl),

	       Thm ("le_refl",num_str le_refl),

	       Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

	       Thm ("not_true",num_str not_true),

	       Thm ("not_false",num_str not_false),

	       Thm ("and_true",and_true),

	       Thm ("and_false",and_false),

	       Thm ("or_true",or_true),

	       Thm ("or_false",or_false),

	       Thm ("and_commute",num_str and_commute),

	       Thm ("or_commute",num_str or_commute),

	       Thm ("real_diff_minus",num_str real_diff_minus),

	       Thm ("root_ge0",num_str root_ge0),

	       Thm ("root_add_ge0",num_str root_add_ge0),

	       Thm ("root_ge0_1",num_str root_ge0_1),

	       Thm ("root_ge0_2",num_str root_ge0_2),

	       Calc ("Atools.is'_const",eval_const "#is_const_"),

	       Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),

	       Calc ("Tools.matches",eval_matches ""),

	       Calc ("Test.contains'_root",

		     eval_contains_root"#contains_root_"),

	       Calc ("op +",eval_binop "#add_"),

	       Calc ("op *",eval_binop "#mult_"),

	       Calc ("Root.sqrt",eval_sqrt "#sqrt_"),

	       Calc ("Atools.pow" ,eval_binop "#power_"),

	       Calc ("op <",eval_equ "#less_"),

	       Calc ("op <=",eval_equ "#less_equal_"),

	       Calc ("Atools.ident",eval_ident "#ident_")],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls;      

ruleset' := overwritelthy thy (!ruleset',

  [("testerls", prep_rls testerls)

   ]);

(*make () dissappear*)   

val rearrange_assoc =

  Rls{id = "rearrange_assoc", preconds = [], 

      rew_ord = ("e_rew_ord",e_rew_ord), 

      erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

      rules = 

      [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),

       Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls;      

val ac_plus_times =

  Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),

      erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

      rules = 

      [Thm ("radd_commute",radd_commute),

       Thm ("radd_left_commute",radd_left_commute),

       Thm ("radd_assoc",radd_assoc),

       Thm ("rmult_commute",rmult_commute),

       Thm ("rmult_left_commute",rmult_left_commute),

       Thm ("rmult_assoc",rmult_assoc)],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls;      

(*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)

val norm_equation =

  Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),

      erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

      rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)

	       ],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls;      

(** rule sets **)

val STest_simplify =     (*   vv--- not changed to real by parse*)

  "Script STest_simplify (t_::'z) =                           \

  \(Repeat\

  \    ((Try (Repeat (Rewrite real_diff_minus False))) @@        \

  \     (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@  \

  \     (Try (Repeat (Rewrite rdistr_right_assoc False))) @@  \

  \     (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@\

  \     (Try (Repeat (Rewrite rdistr_div_right False))) @@    \

  \     (Try (Repeat (Rewrite rbinom_power_2 False))) @@      \

  \     (Try (Repeat (Rewrite radd_commute False))) @@        \

  \     (Try (Repeat (Rewrite radd_left_commute False))) @@   \

  \     (Try (Repeat (Rewrite radd_assoc False))) @@          \

  \     (Try (Repeat (Rewrite rmult_commute False))) @@       \

  \     (Try (Repeat (Rewrite rmult_left_commute False))) @@  \

  \     (Try (Repeat (Rewrite rmult_assoc False))) @@         \

  \     (Try (Repeat (Rewrite radd_real_const_eq False))) @@   \

  \     (Try (Repeat (Rewrite radd_real_const False))) @@   \

  \     (Try (Repeat (Calculate plus))) @@   \

  \     (Try (Repeat (Calculate times))) @@   \

  \     (Try (Repeat (Calculate divide_))) @@\

  \     (Try (Repeat (Calculate power_))) @@  \

  \     (Try (Repeat (Rewrite rcollect_right False))) @@   \

  \     (Try (Repeat (Rewrite rcollect_one_left False))) @@   \

  \     (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@   \

  \     (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@   \

  \     (Try (Repeat (Rewrite rshift_nominator False))) @@   \

  \     (Try (Repeat (Rewrite rcancel_den False))) @@   \

  \     (Try (Repeat (Rewrite rroot_square_inv False))) @@   \

  \     (Try (Repeat (Rewrite rroot_times_root False))) @@   \

  \     (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@   \

  \     (Try (Repeat (Rewrite rsqare False))) @@   \

  \     (Try (Repeat (Rewrite power_1 False))) @@   \

  \     (Try (Repeat (Rewrite rtwo_of_the_same False))) @@   \

  \     (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@   \

  \     (Try (Repeat (Rewrite rmult_1 False))) @@   \

  \     (Try (Repeat (Rewrite rmult_1_right False))) @@   \

  \     (Try (Repeat (Rewrite rmult_0 False))) @@   \

  \     (Try (Repeat (Rewrite rmult_0_right False))) @@   \

  \     (Try (Repeat (Rewrite radd_0 False))) @@   \

  \     (Try (Repeat (Rewrite radd_0_right False)))) \

  \ t_)";

(* expects * distributed over + *)

val Test_simplify =

  Rls{id = "Test_simplify", preconds = [], 

      rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),

      erls = tval_rls, srls = e_rls, 

      calc=[(*since 040209 filled by prep_rls*)],

      (*asm_thm = [],*)

      rules = [

	       Thm ("real_diff_minus",num_str real_diff_minus),

	       Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),

	       Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),

	       Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),

	       Thm ("rdistr_div_right",num_str rdistr_div_right),

	       Thm ("rbinom_power_2",num_str rbinom_power_2),	       

               Thm ("radd_commute",num_str radd_commute), 

	       Thm ("radd_left_commute",num_str radd_left_commute),

	       Thm ("radd_assoc",num_str radd_assoc),

	       Thm ("rmult_commute",num_str rmult_commute),

	       Thm ("rmult_left_commute",num_str rmult_left_commute),

	       Thm ("rmult_assoc",num_str rmult_assoc),

	       Thm ("radd_real_const_eq",num_str radd_real_const_eq),

	       Thm ("radd_real_const",num_str radd_real_const),

	       (* these 2 rules are invers to distr_div_right wrt. termination.

		  thus they MUST be done IMMEDIATELY before calc *)

	       Calc ("op +", eval_binop "#add_"), 

	       Calc ("op *", eval_binop "#mult_"),

	       Calc ("HOL.divide", eval_cancel "#divide_"),

	       Calc ("Atools.pow", eval_binop "#power_"),

	       Thm ("rcollect_right",num_str rcollect_right),

	       Thm ("rcollect_one_left",num_str rcollect_one_left),

	       Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),

	       Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),

	       Thm ("rshift_nominator",num_str rshift_nominator),

	       Thm ("rcancel_den",num_str rcancel_den),

	       Thm ("rroot_square_inv",num_str rroot_square_inv),

	       Thm ("rroot_times_root",num_str rroot_times_root),

	       Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),

	       Thm ("rsqare",num_str rsqare),

	       Thm ("power_1",num_str power_1),

	       Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),

	       Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),

	       Thm ("rmult_1",num_str rmult_1),

	       Thm ("rmult_1_right",num_str rmult_1_right),

	       Thm ("rmult_0",num_str rmult_0),

	       Thm ("rmult_0_right",num_str rmult_0_right),

	       Thm ("radd_0",num_str radd_0),

	       Thm ("radd_0_right",num_str radd_0_right)

	       ],

      scr = Script ((term_of o the o (parse thy)) "empty_script")

		    (*since 040209 filled by prep_rls: STest_simplify*)

      }:rls;      

(** rule sets **)

(*isolate the root in a root-equation*)

val isolate_root =

  Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), 

      erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)

      rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),

	       Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),

	       Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),

	       Thm ("risolate_root_add",num_str risolate_root_add),

	       Thm ("risolate_root_mult",num_str risolate_root_mult),

	       Thm ("risolate_root_div",num_str risolate_root_div)       ],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls;

(*isolate the bound variable in an equation; 'bdv' is a meta-constant*)

val isolate_bdv =

    Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),

	erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)

	rules = 

	[Thm ("risolate_bdv_add",num_str risolate_bdv_add),

	 Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),

	 Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),

	 Thm ("mult_square",num_str mult_square),

	 Thm ("constant_square",num_str constant_square),

	 Thm ("constant_mult_square",num_str constant_mult_square)

	 ],

	scr = Script ((term_of o the o (parse thy)) 

			  "empty_script")

	}:rls;      

(* association list for calculate_, calculate

   "op +" etc. not usable in scripts *)

val calclist = 

    [

     (*as Tools.ML*)

     ("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")),

     ("matches",("Tools.matches",eval_matches "#matches_")),

     ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),

     (*aus Atools.ML*)

     ("PLUS"    ,("op +"        ,eval_binop "#add_")),

     ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

     ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_")),

     ("POWER"  ,("Atools.pow"  ,eval_binop "#power_")),

     ("is_const",("Atools.is'_const",eval_const "#is_const_")),

     ("le"      ,("op <"        ,eval_equ "#less_")),

     ("leq"     ,("op <="       ,eval_equ "#less_equal_")),

     ("ident"   ,("Atools.ident",eval_ident "#ident_")),

     (*von hier (ehem.SqRoot*)

     ("sqrt"    ,("Root.sqrt"   ,eval_sqrt "#sqrt_")),

     ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_")),

     ("Test.contains_root",("contains'_root",

			    eval_contains_root"#contains_root_"))

     ];

ruleset' := overwritelthy thy (!ruleset',

  [("Test_simplify", prep_rls Test_simplify),

   ("tval_rls", prep_rls tval_rls),

   ("isolate_root", prep_rls isolate_root),

   ("isolate_bdv", prep_rls isolate_bdv),

   ("matches", 

    prep_rls (append_rls "matches" testerls 

			 [Calc ("Tools.matches",eval_matches "#matches_")]))

   ]);

(** problem types **)

store_pbt

 (prep_pbt Test.thy "pbl_test" [] e_pblID

 (["test"],

  [],

  e_rls, NONE, []));

store_pbt

 (prep_pbt Test.thy "pbl_test_equ" [] e_pblID

 (["equation","test"],

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["matches (?a = ?b) e_"]),

   ("#Find"  ,["solutions v_i_"])

  ],

  assoc_rls "matches",

  SOME "solve (e_::bool, v_)", []));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni" [] e_pblID

 (["univariate","equation","test"],

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["matches (?a = ?b) e_"]),

   ("#Find"  ,["solutions v_i_"])

  ],

  assoc_rls "matches",

  SOME "solve (e_::bool, v_)", []));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_lin" [] e_pblID

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

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["(matches (   v_ = 0) e_) | (matches (   ?b*v_ = 0) e_) |\

	       \(matches (?a+v_ = 0) e_) | (matches (?a+?b*v_ = 0) e_)  "]),

   ("#Find"  ,["solutions v_i_"])

  ],

  assoc_rls "matches", 

  SOME "solve (e_::bool, v_)", [["Test","solve_linear"]]));

(*25.8.01 ------

store_pbt

 (prep_pbt Test.thy

 (["Test.thy"],

  [("#Given" ,"boolTestGiven g_"),

   ("#Find"  ,"boolTestFind f_")

  ],

  []));

store_pbt

 (prep_pbt Test.thy

 (["testeq","Test.thy"],

  [("#Given" ,"boolTestGiven g_"),

   ("#Find"  ,"boolTestFind f_")

  ],

  []));

val ttt = (term_of o the o (parse Isac.thy)) "(matches (   v_ = 0) e_)";

 ------ 25.8.01*)

(** methods **)

store_met

 (prep_met Diff.thy "met_test" [] e_metID

 (["Test"],

   [],

   {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

    crls=Atools_erls, nrls=e_rls(*,

    asm_rls=[],asm_thm=[]*)}, "empty_script"));

(*

store_met

 (prep_met Script.thy

 (e_metID,(*empty method*)

   [],

   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

    asm_rls=[],asm_thm=[]},

   "Undef"));*)

store_met

 (prep_met Test.thy "met_test_solvelin" [] e_metID

 (["Test","solve_linear"]:metID,

  [("#Given" ,["equality e_","solveFor v_"]),

    ("#Where" ,["matches (?a = ?b) e_"]),

    ("#Find"  ,["solutions v_i_"])

    ],

   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,

    prls=assoc_rls "matches",

    calc=[],

    crls=tval_rls, nrls=Test_simplify},

 "Script Solve_linear (e_::bool) (v_::real)=             \

 \(let e_ =\

 \  Repeat\

 \    (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\

 \      (Rewrite_Set Test_simplify False))) e_\

 \ in [e_::bool])"

 )

(*, prep_met Test.thy (*test for equations*)

 (["Test","testeq"]:metID,

  [("#Given" ,["boolTestGiven g_"]),

   ("#Find"  ,["boolTestFind f_"])

    ],

  {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],

   asm_thm=[("square_equation_left","")]},

 "Script Testeq (eq_::bool) =                                         \

   \Repeat                                                            \

   \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False eq_));      \

   \      e_ = Try (Repeat (Rewrite square_equation_left True e_)); \

   \      e_ = Try (Repeat (Rewrite rmult_0 False e_))                \

   \   in e_) Until (is_root_free e_)" (*deleted*)

 )

, ---------27.4.02*)

);

ruleset' := overwritelthy thy (!ruleset',

  [("norm_equation", prep_rls norm_equation),

   ("ac_plus_times", prep_rls ac_plus_times),

   ("rearrange_assoc", prep_rls rearrange_assoc)

   ]);

fun bin_o (Const (op_,(Type ("fun",

	   [Type (s2,[]),Type ("fun",

	    [Type (s4,tl4),Type (s5,tl5)])])))) = 

    if (s2=s4)andalso(s4=s5)then[op_]else[]

    | bin_o _                                   = [];

fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)

  | bin_op t         =  bin_o t;

fun is_bin_op t = ((bin_op t)<>[]);

fun bin_op_arg1 ((Const (op_,(Type ("fun",

	   [Type (s2,[]),Type ("fun",

	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = 

    arg1;

fun bin_op_arg2 ((Const (op_,(Type ("fun",

	   [Type (s2,[]),Type ("fun",

	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = 

    arg2;

exception NO_EQUATION_TERM;

fun is_equation ((Const ("op =",(Type ("fun",

		 [Type (_,[]),Type ("fun",

		  [Type (_,[]),Type ("bool",[])])])))) $ _ $ _) 

                  = true

  | is_equation _ = false;

fun equ_lhs ((Const ("op =",(Type ("fun",

		 [Type (_,[]),Type ("fun",

		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r) 

              = l

  | equ_lhs _ = raise NO_EQUATION_TERM;

fun equ_rhs ((Const ("op =",(Type ("fun",

		 [Type (_,[]),Type ("fun",

		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r) 

              = r

  | equ_rhs _ = raise NO_EQUATION_TERM;

fun atom (Const (_,Type (_,[])))           = true

  | atom (Free  (_,Type (_,[])))           = true

  | atom (Var   (_,Type (_,[])))           = true

(*| atom (_     (_,"?DUMMY"   ))           = true ..ML-error *)

  | atom((Const ("Bin.integ_of_bin",_)) $ _) = true

  | atom _                                 = false;

fun varids (Const  (s,Type (_,[])))         = [strip_thy s]

  | varids (Free   (s,Type (_,[])))         = if is_no s then []

					      else [strip_thy s]

  | varids (Var((s,_),Type (_,[])))         = [strip_thy s]

(*| varids (_      (s,"?DUMMY"   ))         =   ..ML-error *)

  | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)

  | varids (Abs(a,T,t)) = union op = [a] (varids t)

  | varids (t1 $ t2) = union op = (varids t1) (varids t2)

  | varids _         = [];

(*> val t = term_of (hd (parse Diophant.thy "x"));

val t = Free ("x","?DUMMY") : term

> varids t;

val it = [] : string list          [] !!! *)

fun bin_ops_only ((Const op_) $ t1 $ t2) = 

    if(is_bin_op (Const op_))

    then(bin_ops_only t1)andalso(bin_ops_only t2)

    else false

  | bin_ops_only t =

    if atom t then true else bin_ops_only t;

fun polynomial opl t bdVar = (* bdVar TODO *)

    subset op = (bin_op t, opl) andalso (bin_ops_only t);

fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) 

    andalso polynomial opl (equ_lhs t) bdVar 

    andalso polynomial opl (equ_rhs t) bdVar

    andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse

             subset op = (varids bdVar, varids (equ_lhs t)));

(*fun max is =

    let fun max_ m [] = m 

	  | max_ m (i::is) = if m<i then max_ i is else max_ m is;

    in max_ (hd is) is end;

> max [1,5,3,7,4,2];

val it = 7 : int  *)

fun max (a,b) = if a < b then b else a;

fun degree addl mul bdVar t =

let

fun deg _ _ v (Const  (s,Type (_,[])))         = if v=strip_thy s then 1 else 0

  | deg _ _ v (Free   (s,Type (_,[])))         = if v=strip_thy s then 1 else 0

  | deg _ _ v (Var((s,_),Type (_,[])))         = if v=strip_thy s then 1 else 0

(*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *) 

  | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 

  | deg addl mul v (h $ t1 $ t2) =

    if subset op = (bin_op h, addl)

    then max (deg addl mul v t1  ,deg addl mul v t2)

    else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)

in if polynomial (addl @ [mul]) t bdVar

   then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)

end;

fun degree_ addl mul bdVar t = (* do not export *)

    let fun opt (SOME i)= i

	  | opt  NONE   = 0

in opt (degree addl mul bdVar t) end;

fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;

fun linear_equ addl mul bdVar t =

    if is_equation t 

    then let val degl = degree_ addl mul bdVar (equ_lhs t);

	     val degr = degree_ addl mul bdVar (equ_rhs t)

	 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2

		then true else false

	 end

    else false;

(* strip_thy op_  before *)

fun is_div_op (dv,(Const (op_,(Type ("fun",

	   [Type (s2,[]),Type ("fun",

	    [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)

  | is_div_op _ = false;

fun is_denom bdVar div_op t =

    let fun is bool[v]dv (Const  (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

	  | is bool[v]dv (Free   (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) 

	  | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

	  | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false

	  | is bool[v]dv (h$n$d) = 

	      if is_div_op(dv,h) 

	      then (is false[v]dv n)orelse(is true[v]dv d)

	      else (is bool [v]dv n)orelse(is bool[v]dv d)

in is false (varids bdVar) (strip_thy div_op) t end;

fun rational t div_op bdVar = 

    is_denom bdVar div_op t andalso bin_ops_only t;

(** problem types **)

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_plain2" [] e_pblID

 (["plain_square","univariate","equation","test"],

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\

	       \(matches (     ?b*v_ ^^^2 = 0) e_) |\

	       \(matches (?a +    v_ ^^^2 = 0) e_) |\

	       \(matches (        v_ ^^^2 = 0) e_)"]),

   ("#Find"  ,["solutions v_i_"])

  ],

  assoc_rls "matches", 

  SOME "solve (e_::bool, v_)", [["Test","solve_plain_square"]]));

(*

 val e_ = (term_of o the o (parse thy)) "e_::bool";

 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";

 val env = [(e_,ve)];

 val pre = (term_of o the o (parse thy))

	      "(matches (a + b*v_ ^^^2 = 0, e_::bool)) |\

	      \(matches (    b*v_ ^^^2 = 0, e_::bool)) |\

	      \(matches (a +   v_ ^^^2 = 0, e_::bool)) |\

	      \(matches (      v_ ^^^2 = 0, e_::bool))";

 val prei = subst_atomic env pre;

 val cpre = (cterm_of thy) prei;

 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;

val ct = "True | False | False | False" : cterm 

> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

> val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

val ct = "True" : cterm

*)

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_poly" [] e_pblID

 (["polynomial","univariate","equation","test"],

  [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),

   ("#Where" ,["False"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  e_rls, SOME "solve (e_::bool, v_)", []));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_poly_deg2" [] e_pblID

 (["degree_two","polynomial","univariate","equation","test"],

  [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_poly_deg2_pq" [] e_pblID

 (["pq_formula","degree_two","polynomial","univariate","equation","test"],

  [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_poly_deg2_abc" [] e_pblID

 (["abc_formula","degree_two","polynomial","univariate","equation","test"],

  [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_root" [] e_pblID

 (["squareroot","univariate","equation","test"],

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["contains_root (e_::bool)"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  append_rls "contains_root" e_rls [Calc ("Test.contains'_root",

			  eval_contains_root "#contains_root_")], 

  SOME "solve (e_::bool, v_)", [["Test","square_equation"]]));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_norm" [] e_pblID

 (["normalize","univariate","equation","test"],

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,[]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));

store_pbt

 (prep_pbt Test.thy "pbl_test_uni_roottest" [] e_pblID

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

  [("#Given" ,["equality e_","solveFor v_"]),

   (*("#Where" ,["contains_root (e_::bool)"]),*)

   ("#Find"  ,["solutions v_i_"]) 

  ],

  e_rls, SOME "solve (e_::bool, v_)", []));

(*

(#ppc o get_pbt) ["sqroot-test","univariate","equation"];

  *)

store_met

 (prep_met Test.thy  "met_test_sqrt" [] e_metID

(*root-equation, version for tests before 8.01.01*)

 (["Test","sqrt-equ-test"]:metID,

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["contains_root (e_::bool)"]),

   ("#Find"  ,["solutions v_i_"])

   ],

  {rew_ord'="e_rew_ord",rls'=tval_rls,

   srls =append_rls "srls_contains_root" e_rls 

		    [Calc ("Test.contains'_root",eval_contains_root "")],

   prls =append_rls "prls_contains_root" e_rls 

		    [Calc ("Test.contains'_root",eval_contains_root "")],

   calc=[],

   crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

 "Script Solve_root_equation (e_::bool) (v_::real) =  \

 \(let e_ = \

 \   ((While (contains_root e_) Do\

 \      ((Rewrite square_equation_left True) @@\

 \       (Try (Rewrite_Set Test_simplify False)) @@\

 \       (Try (Rewrite_Set rearrange_assoc False)) @@\

 \       (Try (Rewrite_Set isolate_root False)) @@\

 \       (Try (Rewrite_Set Test_simplify False)))) @@\

 \    (Try (Rewrite_Set norm_equation False)) @@\

 \    (Try (Rewrite_Set Test_simplify False)) @@\

 \    (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\

 \    (Try (Rewrite_Set Test_simplify False)))\

 \   e_\

 \ in [e_::bool])"

  ));

store_met

 (prep_met Test.thy  "met_test_sqrt2" [] e_metID

(*root-equation ... for test-*.sml until 8.01*)

 (["Test","squ-equ-test2"]:metID,

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"])

   ],

  {rew_ord'="e_rew_ord",rls'=tval_rls,

   srls = append_rls "srls_contains_root" e_rls 

		     [Calc ("Test.contains'_root",eval_contains_root"")],

   prls=e_rls,calc=[],

   crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

 "Script Solve_root_equation (e_::bool) (v_::real) =  \

 \(let e_ = \

 \   ((While (contains_root e_) Do\

 \      ((Rewrite square_equation_left True) @@\

 \       (Try (Rewrite_Set Test_simplify False)) @@\

 \       (Try (Rewrite_Set rearrange_assoc False)) @@\

 \       (Try (Rewrite_Set isolate_root False)) @@\

 \       (Try (Rewrite_Set Test_simplify False)))) @@\

 \    (Try (Rewrite_Set norm_equation False)) @@\

 \    (Try (Rewrite_Set Test_simplify False)) @@\

 \    (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\

 \    (Try (Rewrite_Set Test_simplify False)))\

 \   e_;\

 \  (L_::bool list) = Tac subproblem_equation_dummy;          \

 \  L_ = Tac solve_equation_dummy                             \

 \  in Check_elementwise L_ {(v_::real). Assumptions})"

  ));

store_met

 (prep_met Test.thy "met_test_squ_sub" [] e_metID

(*tests subproblem fixed linear*)

 (["Test","squ-equ-test-subpbl1"]:metID,

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"])

   ],

  {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

    crls=tval_rls, nrls=Test_simplify},

  "Script Solve_root_equation (e_::bool) (v_::real) =  \

   \ (let e_ = ((Try (Rewrite_Set norm_equation False)) @@              \

   \            (Try (Rewrite_Set Test_simplify False))) e_;              \

   \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\

   \                    [Test,solve_linear]) [bool_ e_, real_ v_])\

   \in Check_elementwise L_ {(v_::real). Assumptions})"

  ));

store_met

 (prep_met Test.thy "met_test_squ_sub2" [] e_metID

 (*tests subproblem fixed degree 2*)

 (["Test","squ-equ-test-subpbl2"]:metID,

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"])

   ],

  {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

    crls=tval_rls, nrls=e_rls(*,

   asm_rls=[],asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

   "Script Solve_root_equation (e_::bool) (v_::real) =  \

   \ (let e_ = Try (Rewrite_Set norm_equation False) e_;              \

   \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\

   \                    [Test,solve_by_pq_formula]) [bool_ e_, real_ v_])\

   \in Check_elementwise L_ {(v_::real). Assumptions})"

   )); 

store_met

 (prep_met Test.thy "met_test_squ_nonterm" [] e_metID

 (*root-equation: see foils..., but notTerminating*)

 (["Test","square_equation...notTerminating"]:metID,

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Find"  ,["solutions v_i_"])

   ],

  {rew_ord'="e_rew_ord",rls'=tval_rls,

   srls = append_rls "srls_contains_root" e_rls 

		     [Calc ("Test.contains'_root",eval_contains_root"")],

   prls=e_rls,calc=[],

    crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

 "Script Solve_root_equation (e_::bool) (v_::real) =  \

 \(let e_ = \

 \   ((While (contains_root e_) Do\

 \      ((Rewrite square_equation_left True) @@\

 \       (Try (Rewrite_Set Test_simplify False)) @@\

 \       (Try (Rewrite_Set rearrange_assoc False)) @@\

 \       (Try (Rewrite_Set isolate_root False)) @@\

 \       (Try (Rewrite_Set Test_simplify False)))) @@\

 \    (Try (Rewrite_Set norm_equation False)) @@\

 \    (Try (Rewrite_Set Test_simplify False)))\

 \   e_;\

 \  (L_::bool list) =                                        \

 \    (SubProblem (Test_,[linear,univariate,equation,test],\

 \                 [Test,solve_linear]) [bool_ e_, real_ v_])\

 \in Check_elementwise L_ {(v_::real). Assumptions})"

  ));

store_met

 (prep_met Test.thy  "met_test_eq1" [] e_metID

(*root-equation1:*)

 (["Test","square_equation1"]:metID,

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Find"  ,["solutions v_i_"])

    ],

   {rew_ord'="e_rew_ord",rls'=tval_rls,

   srls = append_rls "srls_contains_root" e_rls 

		     [Calc ("Test.contains'_root",eval_contains_root"")],

   prls=e_rls,calc=[],

    crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

 "Script Solve_root_equation (e_::bool) (v_::real) =  \

 \(let e_ = \

 \   ((While (contains_root e_) Do\

 \      ((Rewrite square_equation_left True) @@\

 \       (Try (Rewrite_Set Test_simplify False)) @@\

 \       (Try (Rewrite_Set rearrange_assoc False)) @@\

 \       (Try (Rewrite_Set isolate_root False)) @@\

 \       (Try (Rewrite_Set Test_simplify False)))) @@\

 \    (Try (Rewrite_Set norm_equation False)) @@\

 \    (Try (Rewrite_Set Test_simplify False)))\

 \   e_;\

 \  (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\

 \                    [Test,solve_linear]) [bool_ e_, real_ v_])\

 \  in Check_elementwise L_ {(v_::real). Assumptions})"

  ));

store_met

 (prep_met Test.thy "met_test_squ2" [] e_metID

 (*root-equation2*)

 (["Test","square_equation2"]:metID,

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Find"  ,["solutions v_i_"])

    ],

   {rew_ord'="e_rew_ord",rls'=tval_rls,

   srls = append_rls "srls_contains_root" e_rls 

		     [Calc ("Test.contains'_root",eval_contains_root"")],

   prls=e_rls,calc=[],

    crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

 "Script Solve_root_equation (e_::bool) (v_::real)  =  \

 \(let e_ = \

 \   ((While (contains_root e_) Do\

 \      (((Rewrite square_equation_left True) Or \

 \        (Rewrite square_equation_right True)) @@\

 \       (Try (Rewrite_Set Test_simplify False)) @@\

 \       (Try (Rewrite_Set rearrange_assoc False)) @@\

 \       (Try (Rewrite_Set isolate_root False)) @@\

 \       (Try (Rewrite_Set Test_simplify False)))) @@\

 \    (Try (Rewrite_Set norm_equation False)) @@\

 \    (Try (Rewrite_Set Test_simplify False)))\

 \   e_;\

 \  (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test],\

 \                    [Test,solve_plain_square]) [bool_ e_, real_ v_])\

 \  in Check_elementwise L_ {(v_::real). Assumptions})"

  ));

store_met

 (prep_met Test.thy "met_test_squeq" [] e_metID

 (*root-equation*)

 (["Test","square_equation"]:metID,

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Find"  ,["solutions v_i_"])

    ],

   {rew_ord'="e_rew_ord",rls'=tval_rls,

   srls = append_rls "srls_contains_root" e_rls 

		     [Calc ("Test.contains'_root",eval_contains_root"")],

   prls=e_rls,calc=[],

    crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   asm_thm=[("square_equation_left",""),

	    ("square_equation_right","")]*)},

 "Script Solve_root_equation (e_::bool) (v_::real) =  \

 \(let e_ = \

 \   ((While (contains_root e_) Do\

 \      (((Rewrite square_equation_left True) Or\

 \        (Rewrite square_equation_right True)) @@\

 \       (Try (Rewrite_Set Test_simplify False)) @@\

 \       (Try (Rewrite_Set rearrange_assoc False)) @@\

 \       (Try (Rewrite_Set isolate_root False)) @@\

 \       (Try (Rewrite_Set Test_simplify False)))) @@\

 \    (Try (Rewrite_Set norm_equation False)) @@\

 \    (Try (Rewrite_Set Test_simplify False)))\

 \   e_;\

 \  (L_::bool list) = (SubProblem (Test_,[univariate,equation,test],\

 \                    [no_met]) [bool_ e_, real_ v_])\

 \  in Check_elementwise L_ {(v_::real). Assumptions})"

  ) ); (*#######*)

store_met

 (prep_met Test.thy "met_test_eq_plain" [] e_metID

 (*solve_plain_square*)

 (["Test","solve_plain_square"]:metID,

   [("#Given",["equality e_","solveFor v_"]),

   ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\

	       \(matches (     ?b*v_ ^^^2 = 0) e_) |\

	       \(matches (?a +    v_ ^^^2 = 0) e_) |\

	       \(matches (        v_ ^^^2 = 0) e_)"]), 

   ("#Find"  ,["solutions v_i_"]) 

   ],

   {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,

    prls = assoc_rls "matches",

    crls=tval_rls, nrls=e_rls(*,

    asm_rls=[],asm_thm=[]*)},

  "Script Solve_plain_square (e_::bool) (v_::real) =           \

   \ (let e_ = ((Try (Rewrite_Set isolate_bdv False)) @@         \

   \            (Try (Rewrite_Set Test_simplify False)) @@     \

   \            ((Rewrite square_equality_0 False) Or        \

   \             (Rewrite square_equality True)) @@            \

   \            (Try (Rewrite_Set tval_rls False))) e_             \

   \  in ((Or_to_List e_)::bool list))"

 ));

store_met

 (prep_met Test.thy "met_test_norm_univ" [] e_metID

 (["Test","norm_univar_equation"]:metID,

   [("#Given",["equality e_","solveFor v_"]),

   ("#Where" ,[]), 

   ("#Find"  ,["solutions v_i_"]) 

   ],

   {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,

   calc=[],

    crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},

  "Script Norm_univar_equation (e_::bool) (v_::real) =      \

   \ (let e_ = ((Try (Rewrite rnorm_equation_add False)) @@   \

   \            (Try (Rewrite_Set Test_simplify False))) e_   \

   \  in (SubProblem (Test_,[univariate,equation,test],         \

   \                    [no_met]) [bool_ e_, real_ v_]))"

 ));

(*17.9.02 aus SqRoot.ML------------------------------^^^---*)  

(*8.4.03  aus Poly.ML--------------------------------vvv---

  make_polynomial  ---> make_poly

  ^-- for user          ^-- for systest _ONLY_*)  

local (*. for make_polytest .*)

open Term;  (* for type order = EQUAL | LESS | GREATER *)

fun pr_ord EQUAL = "EQUAL"

  | pr_ord LESS  = "LESS"