neuper@37906: (* SML functions for rational arithmetic
neuper@37906:    WN.22.10.99
neuper@37906:    use"../knowledge/Test.ML";
neuper@37906:    use"IsacKnowledge/Test.ML";
neuper@37906:    use"Test.ML";
neuper@37906:   *)
neuper@37906: 
neuper@37906: 
neuper@37906: (** interface isabelle -- isac **)
neuper@37906: 
neuper@37906: theory' := overwritel (!theory', [("Test.thy",Test.thy)]);
neuper@37906: 
neuper@37906: (** evaluation of numerals and predicates **)
neuper@37906: 
neuper@37906: (*does a term contain a root ?*)
neuper@37906: fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy = 
neuper@37906:   if strip_thy op0 <> "is'_root'_free" 
neuper@37906:     then raise error ("eval_root_free: wrong "^op0)
neuper@37906:   else if const_in (strip_thy op0) arg
neuper@37926: 	 then SOME (mk_thmid thmid "" 
neuper@37906: 		    ((string_of_cterm o cterm_of (sign_of thy)) arg) "", 
neuper@37906: 		    Trueprop $ (mk_equality (t, false_as_term)))
neuper@37926:        else SOME (mk_thmid thmid "" 
neuper@37906: 		  ((string_of_cterm o cterm_of (sign_of thy)) arg) "", 
neuper@37906: 		  Trueprop $ (mk_equality (t, true_as_term)))
neuper@37926:   | eval_root_free _ _ _ _ = NONE; 
neuper@37906: 
neuper@37906: (*does a term contain a root ?*)
neuper@37906: fun eval_contains_root (thmid:string) _ 
neuper@37906: 		       (t as (Const("Test.contains'_root",t0) $ arg)) thy = 
neuper@37930:     if member op = "sqrt"  (ids_of arg)
neuper@37926:     then SOME (mk_thmid thmid "" 
neuper@37906: 			((string_of_cterm o cterm_of (sign_of thy)) arg) "", 
neuper@37906: 	       Trueprop $ (mk_equality (t, true_as_term)))
neuper@37926:     else SOME (mk_thmid thmid "" 
neuper@37906: 			((string_of_cterm o cterm_of (sign_of thy)) arg) "", 
neuper@37906: 	       Trueprop $ (mk_equality (t, false_as_term)))
neuper@37926:   | eval_contains_root _ _ _ _ = NONE; 
neuper@37906:   
neuper@37906: calclist':= overwritel (!calclist', 
neuper@37906:    [("is_root_free", ("Test.is'_root'_free", 
neuper@37906: 		      eval_root_free"#is_root_free_")),
neuper@37906:     ("contains_root", ("Test.contains'_root",
neuper@37906: 		       eval_contains_root"#contains_root_"))
neuper@37906:     ]);
neuper@37906: 
neuper@37906: (** term order **)
neuper@37906: fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
neuper@37906: 
neuper@37906: (** rule sets **)
neuper@37906: 
neuper@37906: val testerls = 
neuper@37906:   Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37906:       erls = e_rls, srls = Erls, 
neuper@37906:       calc = [], 
neuper@37906:       rules = [Thm ("refl",num_str refl),
neuper@37906: 	       Thm ("le_refl",num_str le_refl),
neuper@37906: 	       Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
neuper@37906: 	       Thm ("not_true",num_str not_true),
neuper@37906: 	       Thm ("not_false",num_str not_false),
neuper@37906: 	       Thm ("and_true",and_true),
neuper@37906: 	       Thm ("and_false",and_false),
neuper@37906: 	       Thm ("or_true",or_true),
neuper@37906: 	       Thm ("or_false",or_false),
neuper@37906: 	       Thm ("and_commute",num_str and_commute),
neuper@37906: 	       Thm ("or_commute",num_str or_commute),
neuper@37906: 
neuper@37906: 	       Calc ("Atools.is'_const",eval_const "#is_const_"),
neuper@37906: 	       Calc ("Tools.matches",eval_matches ""),
neuper@37906:     
neuper@37906: 	       Calc ("op +",eval_binop "#add_"),
neuper@37906: 	       Calc ("op *",eval_binop "#mult_"),
neuper@37906: 	       Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37906: 		    
neuper@37906: 	       Calc ("op <",eval_equ "#less_"),
neuper@37906: 	       Calc ("op <=",eval_equ "#less_equal_"),
neuper@37906: 	     	    
neuper@37906: 	       Calc ("Atools.ident",eval_ident "#ident_")],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) 
neuper@37906:       "empty_script")
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: (*.for evaluation of conditions in rewrite rules.*)
neuper@37906: (*FIXXXXXXME 10.8.02: handle like _simplify*)
neuper@37906: val tval_rls =  
neuper@37906:   Rls{id = "tval_rls", preconds = [], 
neuper@37906:       rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy), 
neuper@37906:       erls=testerls,srls = e_rls, 
neuper@37906:       calc=[],
neuper@37906:       rules = [Thm ("refl",num_str refl),
neuper@37906: 	       Thm ("le_refl",num_str le_refl),
neuper@37906: 	       Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
neuper@37906: 	       Thm ("not_true",num_str not_true),
neuper@37906: 	       Thm ("not_false",num_str not_false),
neuper@37906: 	       Thm ("and_true",and_true),
neuper@37906: 	       Thm ("and_false",and_false),
neuper@37906: 	       Thm ("or_true",or_true),
neuper@37906: 	       Thm ("or_false",or_false),
neuper@37906: 	       Thm ("and_commute",num_str and_commute),
neuper@37906: 	       Thm ("or_commute",num_str or_commute),
neuper@37906: 
neuper@37906: 	       Thm ("real_diff_minus",num_str real_diff_minus),
neuper@37906: 
neuper@37906: 	       Thm ("root_ge0",num_str root_ge0),
neuper@37906: 	       Thm ("root_add_ge0",num_str root_add_ge0),
neuper@37906: 	       Thm ("root_ge0_1",num_str root_ge0_1),
neuper@37906: 	       Thm ("root_ge0_2",num_str root_ge0_2),
neuper@37906: 
neuper@37906: 	       Calc ("Atools.is'_const",eval_const "#is_const_"),
neuper@37906: 	       Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),
neuper@37906: 	       Calc ("Tools.matches",eval_matches ""),
neuper@37906: 	       Calc ("Test.contains'_root",
neuper@37906: 		     eval_contains_root"#contains_root_"),
neuper@37906:     
neuper@37906: 	       Calc ("op +",eval_binop "#add_"),
neuper@37906: 	       Calc ("op *",eval_binop "#mult_"),
neuper@37906: 	       Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
neuper@37906: 	       Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37906: 		    
neuper@37906: 	       Calc ("op <",eval_equ "#less_"),
neuper@37906: 	       Calc ("op <=",eval_equ "#less_equal_"),
neuper@37906: 	     	    
neuper@37906: 	       Calc ("Atools.ident",eval_ident "#ident_")],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) 
neuper@37906:       "empty_script")
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: 
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906:   [("testerls", prep_rls testerls)
neuper@37906:    ]);
neuper@37906: 
neuper@37906: 
neuper@37906: (*make () dissappear*)   
neuper@37906: val rearrange_assoc =
neuper@37906:   Rls{id = "rearrange_assoc", preconds = [], 
neuper@37906:       rew_ord = ("e_rew_ord",e_rew_ord), 
neuper@37906:       erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
neuper@37906:       rules = 
neuper@37906:       [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),
neuper@37906:        Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) 
neuper@37906:       "empty_script")
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: val ac_plus_times =
neuper@37906:   Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
neuper@37906:       erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
neuper@37906:       rules = 
neuper@37906:       [Thm ("radd_commute",radd_commute),
neuper@37906:        Thm ("radd_left_commute",radd_left_commute),
neuper@37906:        Thm ("radd_assoc",radd_assoc),
neuper@37906:        Thm ("rmult_commute",rmult_commute),
neuper@37906:        Thm ("rmult_left_commute",rmult_left_commute),
neuper@37906:        Thm ("rmult_assoc",rmult_assoc)],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) 
neuper@37906:       "empty_script")
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: (*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)
neuper@37906: val norm_equation =
neuper@37906:   Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37906:       erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
neuper@37906:       rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)
neuper@37906: 	       ],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) 
neuper@37906:       "empty_script")
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: (** rule sets **)
neuper@37906: 
neuper@37906: val STest_simplify =     (*   vv--- not changed to real by parse*)
neuper@37906:   "Script STest_simplify (t_::'z) =                           \
neuper@37906:   \(Repeat\
neuper@37906:   \    ((Try (Repeat (Rewrite real_diff_minus False))) @@        \
neuper@37906:   \     (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@  \
neuper@37906:   \     (Try (Repeat (Rewrite rdistr_right_assoc False))) @@  \
neuper@37906:   \     (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@\
neuper@37906:   \     (Try (Repeat (Rewrite rdistr_div_right False))) @@    \
neuper@37906:   \     (Try (Repeat (Rewrite rbinom_power_2 False))) @@      \
neuper@37906: 	
neuper@37906:   \     (Try (Repeat (Rewrite radd_commute False))) @@        \
neuper@37906:   \     (Try (Repeat (Rewrite radd_left_commute False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite radd_assoc False))) @@          \
neuper@37906:   \     (Try (Repeat (Rewrite rmult_commute False))) @@       \
neuper@37906:   \     (Try (Repeat (Rewrite rmult_left_commute False))) @@  \
neuper@37906:   \     (Try (Repeat (Rewrite rmult_assoc False))) @@         \
neuper@37906: 	
neuper@37906:   \     (Try (Repeat (Rewrite radd_real_const_eq False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite radd_real_const False))) @@   \
neuper@37906:   \     (Try (Repeat (Calculate plus))) @@   \
neuper@37906:   \     (Try (Repeat (Calculate times))) @@   \
neuper@37906:   \     (Try (Repeat (Calculate divide_))) @@\
neuper@37906:   \     (Try (Repeat (Calculate power_))) @@  \
neuper@37906: 	
neuper@37906:   \     (Try (Repeat (Rewrite rcollect_right False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rcollect_one_left False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@   \
neuper@37906: 	
neuper@37906:   \     (Try (Repeat (Rewrite rshift_nominator False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rcancel_den False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rroot_square_inv False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rroot_times_root False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rsqare False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite power_1 False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rtwo_of_the_same False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@   \
neuper@37906: 	
neuper@37906:   \     (Try (Repeat (Rewrite rmult_1 False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rmult_1_right False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rmult_0 False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite rmult_0_right False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite radd_0 False))) @@   \
neuper@37906:   \     (Try (Repeat (Rewrite radd_0_right False)))) \
neuper@37906:   \ t_)";
neuper@37906: 
neuper@37906: 
neuper@37906: (* expects * distributed over + *)
neuper@37906: val Test_simplify =
neuper@37906:   Rls{id = "Test_simplify", preconds = [], 
neuper@37906:       rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
neuper@37906:       erls = tval_rls, srls = e_rls, 
neuper@37906:       calc=[(*since 040209 filled by prep_rls*)],
neuper@37906:       (*asm_thm = [],*)
neuper@37906:       rules = [
neuper@37906: 	       Thm ("real_diff_minus",num_str real_diff_minus),
neuper@37906: 	       Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),
neuper@37906: 	       Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),
neuper@37906: 	       Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),
neuper@37906: 	       Thm ("rdistr_div_right",num_str rdistr_div_right),
neuper@37906: 	       Thm ("rbinom_power_2",num_str rbinom_power_2),	       
neuper@37906: 
neuper@37906:                Thm ("radd_commute",num_str radd_commute), 
neuper@37906: 	       Thm ("radd_left_commute",num_str radd_left_commute),
neuper@37906: 	       Thm ("radd_assoc",num_str radd_assoc),
neuper@37906: 	       Thm ("rmult_commute",num_str rmult_commute),
neuper@37906: 	       Thm ("rmult_left_commute",num_str rmult_left_commute),
neuper@37906: 	       Thm ("rmult_assoc",num_str rmult_assoc),
neuper@37906: 
neuper@37906: 	       Thm ("radd_real_const_eq",num_str radd_real_const_eq),
neuper@37906: 	       Thm ("radd_real_const",num_str radd_real_const),
neuper@37906: 	       (* these 2 rules are invers to distr_div_right wrt. termination.
neuper@37906: 		  thus they MUST be done IMMEDIATELY before calc *)
neuper@37906: 	       Calc ("op +", eval_binop "#add_"), 
neuper@37906: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37906: 	       Calc ("HOL.divide", eval_cancel "#divide_"),
neuper@37906: 	       Calc ("Atools.pow", eval_binop "#power_"),
neuper@37906: 
neuper@37906: 	       Thm ("rcollect_right",num_str rcollect_right),
neuper@37906: 	       Thm ("rcollect_one_left",num_str rcollect_one_left),
neuper@37906: 	       Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),
neuper@37906: 	       Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),
neuper@37906: 
neuper@37906: 	       Thm ("rshift_nominator",num_str rshift_nominator),
neuper@37906: 	       Thm ("rcancel_den",num_str rcancel_den),
neuper@37906: 	       Thm ("rroot_square_inv",num_str rroot_square_inv),
neuper@37906: 	       Thm ("rroot_times_root",num_str rroot_times_root),
neuper@37906: 	       Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),
neuper@37906: 	       Thm ("rsqare",num_str rsqare),
neuper@37906: 	       Thm ("power_1",num_str power_1),
neuper@37906: 	       Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),
neuper@37906: 	       Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),
neuper@37906: 
neuper@37906: 	       Thm ("rmult_1",num_str rmult_1),
neuper@37906: 	       Thm ("rmult_1_right",num_str rmult_1_right),
neuper@37906: 	       Thm ("rmult_0",num_str rmult_0),
neuper@37906: 	       Thm ("rmult_0_right",num_str rmult_0_right),
neuper@37906: 	       Thm ("radd_0",num_str radd_0),
neuper@37906: 	       Thm ("radd_0_right",num_str radd_0_right)
neuper@37906: 	       ],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37906: 		    (*since 040209 filled by prep_rls: STest_simplify*)
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (** rule sets **)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*isolate the root in a root-equation*)
neuper@37906: val isolate_root =
neuper@37906:   Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), 
neuper@37906:       erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
neuper@37906:       rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),
neuper@37906: 	       Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),
neuper@37906: 	       Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),
neuper@37906: 	       Thm ("risolate_root_add",num_str risolate_root_add),
neuper@37906: 	       Thm ("risolate_root_mult",num_str risolate_root_mult),
neuper@37906: 	       Thm ("risolate_root_div",num_str risolate_root_div)       ],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) 
neuper@37906:       "empty_script")
neuper@37906:       }:rls;
neuper@37906: 
neuper@37906: (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
neuper@37906: val isolate_bdv =
neuper@37906:     Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37906: 	erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
neuper@37906: 	rules = 
neuper@37906: 	[Thm ("risolate_bdv_add",num_str risolate_bdv_add),
neuper@37906: 	 Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),
neuper@37906: 	 Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),
neuper@37906: 	 Thm ("mult_square",num_str mult_square),
neuper@37906: 	 Thm ("constant_square",num_str constant_square),
neuper@37906: 	 Thm ("constant_mult_square",num_str constant_mult_square)
neuper@37906: 	 ],
neuper@37906: 	scr = Script ((term_of o the o (parse thy)) 
neuper@37906: 			  "empty_script")
neuper@37906: 	}:rls;      
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (* association list for calculate_, calculate
neuper@37906:    "op +" etc. not usable in scripts *)
neuper@37906: val calclist = 
neuper@37906:     [
neuper@37906:      (*as Tools.ML*)
neuper@37906:      ("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")),
neuper@37906:      ("matches",("Tools.matches",eval_matches "#matches_")),
neuper@37906:      ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),
neuper@37906:      (*aus Atools.ML*)
neuper@37922:      ("PLUS"    ,("op +"        ,eval_binop "#add_")),
neuper@37922:      ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
neuper@37922:      ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_")),
neuper@37922:      ("POWER"  ,("Atools.pow"  ,eval_binop "#power_")),
neuper@37906:      ("is_const",("Atools.is'_const",eval_const "#is_const_")),
neuper@37906:      ("le"      ,("op <"        ,eval_equ "#less_")),
neuper@37906:      ("leq"     ,("op <="       ,eval_equ "#less_equal_")),
neuper@37906:      ("ident"   ,("Atools.ident",eval_ident "#ident_")),
neuper@37906:      (*von hier (ehem.SqRoot*)
neuper@37906:      ("sqrt"    ,("Root.sqrt"   ,eval_sqrt "#sqrt_")),
neuper@37906:      ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_")),
neuper@37906:      ("Test.contains_root",("contains'_root",
neuper@37906: 			    eval_contains_root"#contains_root_"))
neuper@37906:      ];
neuper@37906: 
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906:   [("Test_simplify", prep_rls Test_simplify),
neuper@37906:    ("tval_rls", prep_rls tval_rls),
neuper@37906:    ("isolate_root", prep_rls isolate_root),
neuper@37906:    ("isolate_bdv", prep_rls isolate_bdv),
neuper@37906:    ("matches", 
neuper@37906:     prep_rls (append_rls "matches" testerls 
neuper@37906: 			 [Calc ("Tools.matches",eval_matches "#matches_")]))
neuper@37906:    ]);
neuper@37906: 
neuper@37906: (** problem types **)
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test" [] e_pblID
neuper@37906:  (["test"],
neuper@37906:   [],
neuper@37926:   e_rls, NONE, []));
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_equ" [] e_pblID
neuper@37906:  (["equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["matches (?a = ?b) e_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:   ],
neuper@37906:   assoc_rls "matches",
neuper@37926:   SOME "solve (e_::bool, v_)", []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni" [] e_pblID
neuper@37906:  (["univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["matches (?a = ?b) e_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:   ],
neuper@37906:   assoc_rls "matches",
neuper@37926:   SOME "solve (e_::bool, v_)", []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_lin" [] e_pblID
neuper@37906:  (["linear","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["(matches (   v_ = 0) e_) | (matches (   ?b*v_ = 0) e_) |\
neuper@37906: 	       \(matches (?a+v_ = 0) e_) | (matches (?a+?b*v_ = 0) e_)  "]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:   ],
neuper@37906:   assoc_rls "matches", 
neuper@37926:   SOME "solve (e_::bool, v_)", [["Test","solve_linear"]]));
neuper@37906: 
neuper@37906: (*25.8.01 ------
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy
neuper@37906:  (["Test.thy"],
neuper@37906:   [("#Given" ,"boolTestGiven g_"),
neuper@37906:    ("#Find"  ,"boolTestFind f_")
neuper@37906:   ],
neuper@37906:   []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy
neuper@37906:  (["testeq","Test.thy"],
neuper@37906:   [("#Given" ,"boolTestGiven g_"),
neuper@37906:    ("#Find"  ,"boolTestFind f_")
neuper@37906:   ],
neuper@37906:   []));
neuper@37906: 
neuper@37906: 
neuper@37906: val ttt = (term_of o the o (parse Isac.thy)) "(matches (   v_ = 0) e_)";
neuper@37906: 
neuper@37906:  ------ 25.8.01*)
neuper@37906: 
neuper@37906: 
neuper@37906: (** methods **)
neuper@37906: store_met
neuper@37906:  (prep_met Diff.thy "met_test" [] e_metID
neuper@37906:  (["Test"],
neuper@37906:    [],
neuper@37906:    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37906:     crls=Atools_erls, nrls=e_rls(*,
neuper@37906:     asm_rls=[],asm_thm=[]*)}, "empty_script"));
neuper@37906: (*
neuper@37906: store_met
neuper@37906:  (prep_met Script.thy
neuper@37906:  (e_metID,(*empty method*)
neuper@37906:    [],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
neuper@37906:     asm_rls=[],asm_thm=[]},
neuper@37906:    "Undef"));*)
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_solvelin" [] e_metID
neuper@37906:  (["Test","solve_linear"]:metID,
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:     ("#Where" ,["matches (?a = ?b) e_"]),
neuper@37906:     ("#Find"  ,["solutions v_i_"])
neuper@37906:     ],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
neuper@37906:     prls=assoc_rls "matches",
neuper@37906:     calc=[],
neuper@37906:     crls=tval_rls, nrls=Test_simplify},
neuper@37906:  "Script Solve_linear (e_::bool) (v_::real)=             \
neuper@37906:  \(let e_ =\
neuper@37906:  \  Repeat\
neuper@37906:  \    (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
neuper@37906:  \      (Rewrite_Set Test_simplify False))) e_\
neuper@37906:  \ in [e_::bool])"
neuper@37906:  )
neuper@37906: (*, prep_met Test.thy (*test for equations*)
neuper@37906:  (["Test","testeq"]:metID,
neuper@37906:   [("#Given" ,["boolTestGiven g_"]),
neuper@37906:    ("#Find"  ,["boolTestFind f_"])
neuper@37906:     ],
neuper@37906:   {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left","")]},
neuper@37906:  "Script Testeq (eq_::bool) =                                         \
neuper@37906:    \Repeat                                                            \
neuper@37906:    \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False eq_));      \
neuper@37906:    \      e_ = Try (Repeat (Rewrite square_equation_left True e_)); \
neuper@37906:    \      e_ = Try (Repeat (Rewrite rmult_0 False e_))                \
neuper@37906:    \   in e_) Until (is_root_free e_)" (*deleted*)
neuper@37906:  )
neuper@37906: , ---------27.4.02*)
neuper@37906: );
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906:   [("norm_equation", prep_rls norm_equation),
neuper@37906:    ("ac_plus_times", prep_rls ac_plus_times),
neuper@37906:    ("rearrange_assoc", prep_rls rearrange_assoc)
neuper@37906:    ]);
neuper@37906: 
neuper@37906: 
neuper@37906: fun bin_o (Const (op_,(Type ("fun",
neuper@37906: 	   [Type (s2,[]),Type ("fun",
neuper@37906: 	    [Type (s4,tl4),Type (s5,tl5)])])))) = 
neuper@37906:     if (s2=s4)andalso(s4=s5)then[op_]else[]
neuper@37906:     | bin_o _                                   = [];
neuper@37906: 
neuper@37930: fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
neuper@37906:   | bin_op t         =  bin_o t;
neuper@37906: fun is_bin_op t = ((bin_op t)<>[]);
neuper@37906: 
neuper@37906: fun bin_op_arg1 ((Const (op_,(Type ("fun",
neuper@37906: 	   [Type (s2,[]),Type ("fun",
neuper@37906: 	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = 
neuper@37906:     arg1;
neuper@37906: fun bin_op_arg2 ((Const (op_,(Type ("fun",
neuper@37906: 	   [Type (s2,[]),Type ("fun",
neuper@37906: 	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = 
neuper@37906:     arg2;
neuper@37906: 
neuper@37906: 
neuper@37906: exception NO_EQUATION_TERM;
neuper@37906: fun is_equation ((Const ("op =",(Type ("fun",
neuper@37906: 		 [Type (_,[]),Type ("fun",
neuper@37906: 		  [Type (_,[]),Type ("bool",[])])])))) $ _ $ _) 
neuper@37906:                   = true
neuper@37906:   | is_equation _ = false;
neuper@37906: fun equ_lhs ((Const ("op =",(Type ("fun",
neuper@37906: 		 [Type (_,[]),Type ("fun",
neuper@37906: 		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r) 
neuper@37906:               = l
neuper@37906:   | equ_lhs _ = raise NO_EQUATION_TERM;
neuper@37906: fun equ_rhs ((Const ("op =",(Type ("fun",
neuper@37906: 		 [Type (_,[]),Type ("fun",
neuper@37906: 		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r) 
neuper@37906:               = r
neuper@37906:   | equ_rhs _ = raise NO_EQUATION_TERM;
neuper@37906: 
neuper@37906: 
neuper@37906: fun atom (Const (_,Type (_,[])))           = true
neuper@37906:   | atom (Free  (_,Type (_,[])))           = true
neuper@37906:   | atom (Var   (_,Type (_,[])))           = true
neuper@37906: (*| atom (_     (_,"?DUMMY"   ))           = true ..ML-error *)
neuper@37906:   | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
neuper@37906:   | atom _                                 = false;
neuper@37906: 
neuper@37906: fun varids (Const  (s,Type (_,[])))         = [strip_thy s]
neuper@37906:   | varids (Free   (s,Type (_,[])))         = if is_no s then []
neuper@37906: 					      else [strip_thy s]
neuper@37906:   | varids (Var((s,_),Type (_,[])))         = [strip_thy s]
neuper@37906: (*| varids (_      (s,"?DUMMY"   ))         =   ..ML-error *)
neuper@37906:   | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
neuper@37930:   | varids (Abs(a,T,t)) = union op = [a] (varids t)
neuper@37930:   | varids (t1 $ t2) = union op = (varids t1) (varids t2)
neuper@37906:   | varids _         = [];
neuper@37906: (*> val t = term_of (hd (parse Diophant.thy "x"));
neuper@37906: val t = Free ("x","?DUMMY") : term
neuper@37906: > varids t;
neuper@37906: val it = [] : string list          [] !!! *)
neuper@37906: 
neuper@37906: 
neuper@37906: fun bin_ops_only ((Const op_) $ t1 $ t2) = 
neuper@37906:     if(is_bin_op (Const op_))
neuper@37906:     then(bin_ops_only t1)andalso(bin_ops_only t2)
neuper@37906:     else false
neuper@37906:   | bin_ops_only t =
neuper@37906:     if atom t then true else bin_ops_only t;
neuper@37906: 
neuper@37906: fun polynomial opl t bdVar = (* bdVar TODO *)
neuper@37934:     subset op = (bin_op t, opl) andalso (bin_ops_only t);
neuper@37906: 
neuper@37906: fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) 
neuper@37906:     andalso polynomial opl (equ_lhs t) bdVar 
neuper@37906:     andalso polynomial opl (equ_rhs t) bdVar
neuper@37934:     andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
neuper@37934:              subset op = (varids bdVar, varids (equ_lhs t)));
neuper@37906: 
neuper@37906: (*fun max is =
neuper@37906:     let fun max_ m [] = m 
neuper@37906: 	  | max_ m (i::is) = if m<i then max_ i is else max_ m is;
neuper@37906:     in max_ (hd is) is end;
neuper@37906: > max [1,5,3,7,4,2];
neuper@37906: val it = 7 : int  *)
neuper@37906: 
neuper@37906: fun max (a,b) = if a < b then b else a;
neuper@37906: 
neuper@37906: fun degree addl mul bdVar t =
neuper@37906: let
neuper@37906: fun deg _ _ v (Const  (s,Type (_,[])))         = if v=strip_thy s then 1 else 0
neuper@37906:   | deg _ _ v (Free   (s,Type (_,[])))         = if v=strip_thy s then 1 else 0
neuper@37906:   | deg _ _ v (Var((s,_),Type (_,[])))         = if v=strip_thy s then 1 else 0
neuper@37906: (*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *) 
neuper@37906:   | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 
neuper@37906:   | deg addl mul v (h $ t1 $ t2) =
neuper@37934:     if subset op = (bin_op h, addl)
neuper@37906:     then max (deg addl mul v t1  ,deg addl mul v t2)
neuper@37906:     else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
neuper@37906: in if polynomial (addl @ [mul]) t bdVar
neuper@37926:    then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)
neuper@37906: end;
neuper@37906: fun degree_ addl mul bdVar t = (* do not export *)
neuper@37926:     let fun opt (SOME i)= i
neuper@37926: 	  | opt  NONE   = 0
neuper@37906: in opt (degree addl mul bdVar t) end;
neuper@37906: 
neuper@37906: 
neuper@37906: fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
neuper@37906: 
neuper@37906: fun linear_equ addl mul bdVar t =
neuper@37906:     if is_equation t 
neuper@37906:     then let val degl = degree_ addl mul bdVar (equ_lhs t);
neuper@37906: 	     val degr = degree_ addl mul bdVar (equ_rhs t)
neuper@37906: 	 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
neuper@37906: 		then true else false
neuper@37906: 	 end
neuper@37906:     else false;
neuper@37906: (* strip_thy op_  before *)
neuper@37906: fun is_div_op (dv,(Const (op_,(Type ("fun",
neuper@37906: 	   [Type (s2,[]),Type ("fun",
neuper@37906: 	    [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
neuper@37906:   | is_div_op _ = false;
neuper@37906: 
neuper@37906: fun is_denom bdVar div_op t =
neuper@37906:     let fun is bool[v]dv (Const  (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
neuper@37906: 	  | is bool[v]dv (Free   (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) 
neuper@37906: 	  | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
neuper@37906: 	  | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
neuper@37906: 	  | is bool[v]dv (h$n$d) = 
neuper@37906: 	      if is_div_op(dv,h) 
neuper@37906: 	      then (is false[v]dv n)orelse(is true[v]dv d)
neuper@37906: 	      else (is bool [v]dv n)orelse(is bool[v]dv d)
neuper@37906: in is false (varids bdVar) (strip_thy div_op) t end;
neuper@37906: 
neuper@37906: 
neuper@37906: fun rational t div_op bdVar = 
neuper@37906:     is_denom bdVar div_op t andalso bin_ops_only t;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (** problem types **)
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_plain2" [] e_pblID
neuper@37906:  (["plain_square","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\
neuper@37906: 	       \(matches (     ?b*v_ ^^^2 = 0) e_) |\
neuper@37906: 	       \(matches (?a +    v_ ^^^2 = 0) e_) |\
neuper@37906: 	       \(matches (        v_ ^^^2 = 0) e_)"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:   ],
neuper@37906:   assoc_rls "matches", 
neuper@37926:   SOME "solve (e_::bool, v_)", [["Test","solve_plain_square"]]));
neuper@37906: (*
neuper@37906:  val e_ = (term_of o the o (parse thy)) "e_::bool";
neuper@37906:  val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
neuper@37906:  val env = [(e_,ve)];
neuper@37906: 
neuper@37906:  val pre = (term_of o the o (parse thy))
neuper@37906: 	      "(matches (a + b*v_ ^^^2 = 0, e_::bool)) |\
neuper@37906: 	      \(matches (    b*v_ ^^^2 = 0, e_::bool)) |\
neuper@37906: 	      \(matches (a +   v_ ^^^2 = 0, e_::bool)) |\
neuper@37906: 	      \(matches (      v_ ^^^2 = 0, e_::bool))";
neuper@37906:  val prei = subst_atomic env pre;
neuper@37906:  val cpre = cterm_of (sign_of thy) prei;
neuper@37906: 
neuper@37926:  val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
neuper@37906: val ct = "True | False | False | False" : cterm 
neuper@37906: 
neuper@37926: > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
neuper@37926: > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
neuper@37926: > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
neuper@37906: val ct = "True" : cterm
neuper@37906: 
neuper@37906: *)
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_poly" [] e_pblID
neuper@37906:  (["polynomial","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
neuper@37906:    ("#Where" ,["False"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37926:   e_rls, SOME "solve (e_::bool, v_)", []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_poly_deg2" [] e_pblID
neuper@37906:  (["degree_two","polynomial","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37926:   e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
neuper@37906:  (["pq_formula","degree_two","polynomial","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37926:   e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
neuper@37906:  (["abc_formula","degree_two","polynomial","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37926:   e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_root" [] e_pblID
neuper@37906:  (["squareroot","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["contains_root (e_::bool)"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37906:   append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
neuper@37906: 			  eval_contains_root "#contains_root_")], 
neuper@37926:   SOME "solve (e_::bool, v_)", [["Test","square_equation"]]));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_norm" [] e_pblID
neuper@37906:  (["normalize","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,[]),
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37926:   e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));
neuper@37906: 
neuper@37906: store_pbt
neuper@37906:  (prep_pbt Test.thy "pbl_test_uni_roottest" [] e_pblID
neuper@37906:  (["sqroot-test","univariate","equation","test"],
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    (*("#Where" ,["contains_root (e_::bool)"]),*)
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:   ],
neuper@37926:   e_rls, SOME "solve (e_::bool, v_)", []));
neuper@37906: 
neuper@37906: (*
neuper@37906: (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
neuper@37906:   *)
neuper@37906: 
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy  "met_test_sqrt" [] e_metID
neuper@37906: (*root-equation, version for tests before 8.01.01*)
neuper@37906:  (["Test","sqrt-equ-test"]:metID,
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["contains_root (e_::bool)"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:    ],
neuper@37906:   {rew_ord'="e_rew_ord",rls'=tval_rls,
neuper@37906:    srls =append_rls "srls_contains_root" e_rls 
neuper@37906: 		    [Calc ("Test.contains'_root",eval_contains_root "")],
neuper@37906:    prls =append_rls "prls_contains_root" e_rls 
neuper@37906: 		    [Calc ("Test.contains'_root",eval_contains_root "")],
neuper@37906:    calc=[],
neuper@37906:    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:  "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:  \(let e_ = \
neuper@37906:  \   ((While (contains_root e_) Do\
neuper@37906:  \      ((Rewrite square_equation_left True) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \       (Try (Rewrite_Set rearrange_assoc False)) @@\
neuper@37906:  \       (Try (Rewrite_Set isolate_root False)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)))) @@\
neuper@37906:  \    (Try (Rewrite_Set norm_equation False)) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \    (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)))\
neuper@37906:  \   e_\
neuper@37906:  \ in [e_::bool])"
neuper@37906:   ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy  "met_test_sqrt2" [] e_metID
neuper@37906: (*root-equation ... for test-*.sml until 8.01*)
neuper@37906:  (["Test","squ-equ-test2"]:metID,
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:    ],
neuper@37906:   {rew_ord'="e_rew_ord",rls'=tval_rls,
neuper@37906:    srls = append_rls "srls_contains_root" e_rls 
neuper@37906: 		     [Calc ("Test.contains'_root",eval_contains_root"")],
neuper@37906:    prls=e_rls,calc=[],
neuper@37906:    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:  "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:  \(let e_ = \
neuper@37906:  \   ((While (contains_root e_) Do\
neuper@37906:  \      ((Rewrite square_equation_left True) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \       (Try (Rewrite_Set rearrange_assoc False)) @@\
neuper@37906:  \       (Try (Rewrite_Set isolate_root False)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)))) @@\
neuper@37906:  \    (Try (Rewrite_Set norm_equation False)) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \    (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)))\
neuper@37906:  \   e_;\
neuper@37906:  \  (L_::bool list) = Tac subproblem_equation_dummy;          \
neuper@37906:  \  L_ = Tac solve_equation_dummy                             \
neuper@37906:  \  in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:   ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_squ_sub" [] e_metID
neuper@37906: (*tests subproblem fixed linear*)
neuper@37906:  (["Test","squ-equ-test-subpbl1"]:metID,
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:    ],
neuper@37906:   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
neuper@37906:     crls=tval_rls, nrls=Test_simplify},
neuper@37906:   "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:    \ (let e_ = ((Try (Rewrite_Set norm_equation False)) @@              \
neuper@37906:    \            (Try (Rewrite_Set Test_simplify False))) e_;              \
neuper@37906:    \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
neuper@37906:    \                    [Test,solve_linear]) [bool_ e_, real_ v_])\
neuper@37906:    \in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:   ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_squ_sub2" [] e_metID
neuper@37906:  (*tests subproblem fixed degree 2*)
neuper@37906:  (["Test","squ-equ-test-subpbl2"]:metID,
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:    ],
neuper@37906:   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
neuper@37906:     crls=tval_rls, nrls=e_rls(*,
neuper@37906:    asm_rls=[],asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:    "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:    \ (let e_ = Try (Rewrite_Set norm_equation False) e_;              \
neuper@37906:    \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
neuper@37906:    \                    [Test,solve_by_pq_formula]) [bool_ e_, real_ v_])\
neuper@37906:    \in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:    )); 
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_squ_nonterm" [] e_metID
neuper@37906:  (*root-equation: see foils..., but notTerminating*)
neuper@37906:  (["Test","square_equation...notTerminating"]:metID,
neuper@37906:   [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:    ("#Find"  ,["solutions v_i_"])
neuper@37906:    ],
neuper@37906:   {rew_ord'="e_rew_ord",rls'=tval_rls,
neuper@37906:    srls = append_rls "srls_contains_root" e_rls 
neuper@37906: 		     [Calc ("Test.contains'_root",eval_contains_root"")],
neuper@37906:    prls=e_rls,calc=[],
neuper@37906:     crls=tval_rls, nrls=e_rls(*,asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:  "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:  \(let e_ = \
neuper@37906:  \   ((While (contains_root e_) Do\
neuper@37906:  \      ((Rewrite square_equation_left True) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \       (Try (Rewrite_Set rearrange_assoc False)) @@\
neuper@37906:  \       (Try (Rewrite_Set isolate_root False)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)))) @@\
neuper@37906:  \    (Try (Rewrite_Set norm_equation False)) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)))\
neuper@37906:  \   e_;\
neuper@37906:  \  (L_::bool list) =                                        \
neuper@37906:  \    (SubProblem (Test_,[linear,univariate,equation,test],\
neuper@37906:  \                 [Test,solve_linear]) [bool_ e_, real_ v_])\
neuper@37906:  \in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:   ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy  "met_test_eq1" [] e_metID
neuper@37906: (*root-equation1:*)
neuper@37906:  (["Test","square_equation1"]:metID,
neuper@37906:    [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:     ("#Find"  ,["solutions v_i_"])
neuper@37906:     ],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,
neuper@37906:    srls = append_rls "srls_contains_root" e_rls 
neuper@37906: 		     [Calc ("Test.contains'_root",eval_contains_root"")],
neuper@37906:    prls=e_rls,calc=[],
neuper@37906:     crls=tval_rls, nrls=e_rls(*,asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:  "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:  \(let e_ = \
neuper@37906:  \   ((While (contains_root e_) Do\
neuper@37906:  \      ((Rewrite square_equation_left True) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \       (Try (Rewrite_Set rearrange_assoc False)) @@\
neuper@37906:  \       (Try (Rewrite_Set isolate_root False)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)))) @@\
neuper@37906:  \    (Try (Rewrite_Set norm_equation False)) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)))\
neuper@37906:  \   e_;\
neuper@37906:  \  (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\
neuper@37906:  \                    [Test,solve_linear]) [bool_ e_, real_ v_])\
neuper@37906:  \  in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:   ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_squ2" [] e_metID
neuper@37906:  (*root-equation2*)
neuper@37906:  (["Test","square_equation2"]:metID,
neuper@37906:    [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:     ("#Find"  ,["solutions v_i_"])
neuper@37906:     ],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,
neuper@37906:    srls = append_rls "srls_contains_root" e_rls 
neuper@37906: 		     [Calc ("Test.contains'_root",eval_contains_root"")],
neuper@37906:    prls=e_rls,calc=[],
neuper@37906:     crls=tval_rls, nrls=e_rls(*,asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:  "Script Solve_root_equation (e_::bool) (v_::real)  =  \
neuper@37906:  \(let e_ = \
neuper@37906:  \   ((While (contains_root e_) Do\
neuper@37906:  \      (((Rewrite square_equation_left True) Or \
neuper@37906:  \        (Rewrite square_equation_right True)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \       (Try (Rewrite_Set rearrange_assoc False)) @@\
neuper@37906:  \       (Try (Rewrite_Set isolate_root False)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)))) @@\
neuper@37906:  \    (Try (Rewrite_Set norm_equation False)) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)))\
neuper@37906:  \   e_;\
neuper@37906:  \  (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test],\
neuper@37906:  \                    [Test,solve_plain_square]) [bool_ e_, real_ v_])\
neuper@37906:  \  in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:   ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_squeq" [] e_metID
neuper@37906:  (*root-equation*)
neuper@37906:  (["Test","square_equation"]:metID,
neuper@37906:    [("#Given" ,["equality e_","solveFor v_"]),
neuper@37906:     ("#Find"  ,["solutions v_i_"])
neuper@37906:     ],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,
neuper@37906:    srls = append_rls "srls_contains_root" e_rls 
neuper@37906: 		     [Calc ("Test.contains'_root",eval_contains_root"")],
neuper@37906:    prls=e_rls,calc=[],
neuper@37906:     crls=tval_rls, nrls=e_rls(*,asm_rls=[],
neuper@37906:    asm_thm=[("square_equation_left",""),
neuper@37906: 	    ("square_equation_right","")]*)},
neuper@37906:  "Script Solve_root_equation (e_::bool) (v_::real) =  \
neuper@37906:  \(let e_ = \
neuper@37906:  \   ((While (contains_root e_) Do\
neuper@37906:  \      (((Rewrite square_equation_left True) Or\
neuper@37906:  \        (Rewrite square_equation_right True)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906:  \       (Try (Rewrite_Set rearrange_assoc False)) @@\
neuper@37906:  \       (Try (Rewrite_Set isolate_root False)) @@\
neuper@37906:  \       (Try (Rewrite_Set Test_simplify False)))) @@\
neuper@37906:  \    (Try (Rewrite_Set norm_equation False)) @@\
neuper@37906:  \    (Try (Rewrite_Set Test_simplify False)))\
neuper@37906:  \   e_;\
neuper@37906:  \  (L_::bool list) = (SubProblem (Test_,[univariate,equation,test],\
neuper@37906:  \                    [no_met]) [bool_ e_, real_ v_])\
neuper@37906:  \  in Check_elementwise L_ {(v_::real). Assumptions})"
neuper@37906:   ) ); (*#######*)
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_eq_plain" [] e_metID
neuper@37906:  (*solve_plain_square*)
neuper@37906:  (["Test","solve_plain_square"]:metID,
neuper@37906:    [("#Given",["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\
neuper@37906: 	       \(matches (     ?b*v_ ^^^2 = 0) e_) |\
neuper@37906: 	       \(matches (?a +    v_ ^^^2 = 0) e_) |\
neuper@37906: 	       \(matches (        v_ ^^^2 = 0) e_)"]), 
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:    ],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
neuper@37906:     prls = assoc_rls "matches",
neuper@37906:     crls=tval_rls, nrls=e_rls(*,
neuper@37906:     asm_rls=[],asm_thm=[]*)},
neuper@37906:   "Script Solve_plain_square (e_::bool) (v_::real) =           \
neuper@37906:    \ (let e_ = ((Try (Rewrite_Set isolate_bdv False)) @@         \
neuper@37906:    \            (Try (Rewrite_Set Test_simplify False)) @@     \
neuper@37906:    \            ((Rewrite square_equality_0 False) Or        \
neuper@37906:    \             (Rewrite square_equality True)) @@            \
neuper@37906:    \            (Try (Rewrite_Set tval_rls False))) e_             \
neuper@37906:    \  in ((Or_to_List e_)::bool list))"
neuper@37906:  ));
neuper@37906: 
neuper@37906: store_met
neuper@37906:  (prep_met Test.thy "met_test_norm_univ" [] e_metID
neuper@37906:  (["Test","norm_univar_equation"]:metID,
neuper@37906:    [("#Given",["equality e_","solveFor v_"]),
neuper@37906:    ("#Where" ,[]), 
neuper@37906:    ("#Find"  ,["solutions v_i_"]) 
neuper@37906:    ],
neuper@37906:    {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
neuper@37906:    calc=[],
neuper@37906:     crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
neuper@37906:   "Script Norm_univar_equation (e_::bool) (v_::real) =      \
neuper@37906:    \ (let e_ = ((Try (Rewrite rnorm_equation_add False)) @@   \
neuper@37906:    \            (Try (Rewrite_Set Test_simplify False))) e_   \
neuper@37906:    \  in (SubProblem (Test_,[univariate,equation,test],         \
neuper@37906:    \                    [no_met]) [bool_ e_, real_ v_]))"
neuper@37906:  ));
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*17.9.02 aus SqRoot.ML------------------------------^^^---*)  
neuper@37906: 
neuper@37906: (*8.4.03  aus Poly.ML--------------------------------vvv---
neuper@37906:   make_polynomial  ---> make_poly
neuper@37906:   ^-- for user          ^-- for systest _ONLY_*)  
neuper@37906: 
neuper@37906: local (*. for make_polytest .*)
neuper@37906: 
neuper@37906: open Term;  (* for type order = EQUAL | LESS | GREATER *)
neuper@37906: 
neuper@37906: fun pr_ord EQUAL = "EQUAL"
neuper@37906:   | pr_ord LESS  = "LESS"
neuper@37906:   | pr_ord GREATER = "GREATER";
neuper@37906: 
neuper@37906: fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)
neuper@37906:   (case a of
neuper@37906:      "Atools.pow" => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)
neuper@37906:    | _ => (((a, 0), T), 0))
neuper@37906:   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
neuper@37906:   | dest_hd' (Var v) = (v, 2)
neuper@37906:   | dest_hd' (Bound i) = ((("", i), dummyT), 3)
neuper@37906:   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
neuper@37906: (* RL *)
neuper@37906: fun get_order_pow (t $ (Free(order,_))) = 
neuper@37906:     	(case int_of_str (order) of
neuper@37926: 	             SOME d => d
neuper@37926: 		   | NONE   => 0)
neuper@37906:   | get_order_pow _ = 0;
neuper@37906: 
neuper@37906: fun size_of_term' (Const(str,_) $ t) =
neuper@37906:   if "Atools.pow"= str then 1000 + size_of_term' t else 1 + size_of_term' t   (*WN*)
neuper@37906:   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
neuper@37906:   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
neuper@37906:   | size_of_term' _ = 1;
neuper@37906: 
neuper@37906: fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
neuper@37906:       (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
neuper@37906:   | term_ord' pr thy (t, u) =
neuper@37906:       (if pr then 
neuper@37906: 	 let
neuper@37906: 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;
neuper@37906: 	   val _=writeln("t= f@ts= \""^
neuper@37906: 	      ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
neuper@37906: 	      (commas(map(string_of_cterm o cterm_of (sign_of thy)) ts))^"]\"");
neuper@37906: 	   val _=writeln("u= g@us= \""^
neuper@37906: 	      ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
neuper@37906: 	      (commas(map(string_of_cterm o cterm_of (sign_of thy)) us))^"]\"");
neuper@37906: 	   val _=writeln("size_of_term(t,u)= ("^
neuper@37906: 	      (string_of_int(size_of_term' t))^", "^
neuper@37906: 	      (string_of_int(size_of_term' u))^")");
neuper@37906: 	   val _=writeln("hd_ord(f,g)      = "^((pr_ord o hd_ord)(f,g)));
neuper@37906: 	   val _=writeln("terms_ord(ts,us) = "^
neuper@37906: 			   ((pr_ord o terms_ord str false)(ts,us)));
neuper@37906: 	   val _=writeln("-------");
neuper@37906: 	 in () end
neuper@37906:        else ();
neuper@37906: 	 case int_ord (size_of_term' t, size_of_term' u) of
neuper@37906: 	   EQUAL =>
neuper@37906: 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
neuper@37906: 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 
neuper@37906: 	     | ord => ord)
neuper@37906: 	     end
neuper@37906: 	 | ord => ord)
neuper@37906: and hd_ord (f, g) =                                        (* ~ term.ML *)
neuper@37906:   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
neuper@37906: and terms_ord str pr (ts, us) = 
neuper@37906:     list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
neuper@37906: in
neuper@37906: 
neuper@37906: fun ord_make_polytest (pr:bool) thy (_:subst) tu = 
neuper@37906:     (term_ord' pr thy(***) tu = LESS );
neuper@37906: 
neuper@37906: end;(*local*)
neuper@37906: 
neuper@37906: rew_ord' := overwritel (!rew_ord',
neuper@37906: [("termlessI", termlessI),
neuper@37906:  ("ord_make_polytest", ord_make_polytest false thy)
neuper@37906:  ]);
neuper@37906: 
neuper@37906: (*WN060510 this was a preparation for prep_rls ...
neuper@37906: val scr_make_polytest = 
neuper@37906: "Script Expand_binomtest t_ =\
neuper@37906: \(Repeat                       \
neuper@37906: \((Try (Repeat (Rewrite real_diff_minus         False))) @@ \ 
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_add_mult_distrib   False))) @@ \	 
neuper@37906: \ (Try (Repeat (Rewrite real_add_mult_distrib2  False))) @@ \	
neuper@37906: \ (Try (Repeat (Rewrite real_diff_mult_distrib  False))) @@ \	
neuper@37906: \ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \	
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_mult_1             False))) @@ \		   
neuper@37906: \ (Try (Repeat (Rewrite real_mult_0             False))) @@ \		   
neuper@37906: \ (Try (Repeat (Rewrite real_add_zero_left      False))) @@ \	 
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_mult_commute       False))) @@ \		
neuper@37906: \ (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ \	
neuper@37906: \ (Try (Repeat (Rewrite real_mult_assoc         False))) @@ \		
neuper@37906: \ (Try (Repeat (Rewrite real_add_commute        False))) @@ \		
neuper@37906: \ (Try (Repeat (Rewrite real_add_left_commute   False))) @@ \	 
neuper@37906: \ (Try (Repeat (Rewrite real_add_assoc          False))) @@ \	 
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ \	 
neuper@37906: \ (Try (Repeat (Rewrite realpow_plus_1          False))) @@ \	 
neuper@37906: \ (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ \		
neuper@37906: \ (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ \		
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_num_collect        False))) @@ \		
neuper@37906: \ (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ \	
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_one_collect        False))) @@ \		
neuper@37906: \ (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ \   
neuper@37906: 
neuper@37906: \ (Try (Repeat (Calculate plus  ))) @@ \
neuper@37906: \ (Try (Repeat (Calculate times ))) @@ \
neuper@37906: \ (Try (Repeat (Calculate power_)))) \  
neuper@37906: \ t_)";
neuper@37906: -----------------------------------------------------*)
neuper@37906: 
neuper@37906: val make_polytest =
neuper@37906:   Rls{id = "make_polytest", preconds = []:term list, rew_ord = ("ord_make_polytest",
neuper@37906: 				ord_make_polytest false Poly.thy),
neuper@37906:       erls = testerls, srls = Erls,
neuper@37922:       calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
neuper@37922: 	      ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37922: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37906: 	      ],
neuper@37906:       (*asm_thm = [],*)
neuper@37906:       rules = [Thm ("real_diff_minus",num_str real_diff_minus),
neuper@37906: 	       (*"a - b = a + (-1) * b"*)
neuper@37906: 	       Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
neuper@37906: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37906: 	       Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
neuper@37906: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37906: 	       Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
neuper@37906: 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
neuper@37906: 	       Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
neuper@37906: 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
neuper@37906: 	       Thm ("real_mult_1",num_str real_mult_1),                 
neuper@37906: 	       (*"1 * z = z"*)
neuper@37906: 	       Thm ("real_mult_0",num_str real_mult_0),        
neuper@37906: 	       (*"0 * z = 0"*)
neuper@37906: 	       Thm ("real_add_zero_left",num_str real_add_zero_left),
neuper@37906: 	       (*"0 + z = z"*)
neuper@37906: 
neuper@37906: 	       (*AC-rewriting*)
neuper@37906: 	       Thm ("real_mult_commute",num_str real_mult_commute),
neuper@37906: 	       (* z * w = w * z *)
neuper@37906: 	       Thm ("real_mult_left_commute",num_str real_mult_left_commute),
neuper@37906: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37906: 	       Thm ("real_mult_assoc",num_str real_mult_assoc),		
neuper@37906: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37906: 	       Thm ("real_add_commute",num_str real_add_commute),	
neuper@37906: 	       (*z + w = w + z*)
neuper@37906: 	       Thm ("real_add_left_commute",num_str real_add_left_commute),
neuper@37906: 	       (*x + (y + z) = y + (x + z)*)
neuper@37906: 	       Thm ("real_add_assoc",num_str real_add_assoc),	               
neuper@37906: 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
neuper@37906: 
neuper@37906: 	       Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),	
neuper@37906: 	       (*"r1 * r1 = r1 ^^^ 2"*)
neuper@37906: 	       Thm ("realpow_plus_1",num_str realpow_plus_1),		
neuper@37906: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
neuper@37906: 	       Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),	
neuper@37906: 	       (*"z1 + z1 = 2 * z1"*)
neuper@37906: 	       Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),	
neuper@37906: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37906: 
neuper@37906: 	       Thm ("real_num_collect",num_str real_num_collect), 
neuper@37906: 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
neuper@37906: 	       Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
neuper@37906: 	       (*"[| l is_const; m is_const |] ==>  
neuper@37906: 				l * n + (m * n + k) =  (l + m) * n + k"*)
neuper@37906: 	       Thm ("real_one_collect",num_str real_one_collect),	
neuper@37906: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37906: 	       Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), 
neuper@37906: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37906: 
neuper@37906: 	       Calc ("op +", eval_binop "#add_"), 
neuper@37906: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37906: 	       Calc ("Atools.pow", eval_binop "#power_")
neuper@37906: 	       ],
neuper@37906:       scr = EmptyScr(*Script ((term_of o the o (parse thy)) 
neuper@37906:       scr_make_polytest)*)
neuper@37906:       }:rls;      
neuper@37906: (*WN060510 this was done before 'fun prep_rls' ...
neuper@37906: val scr_expand_binomtest =
neuper@37906: "Script Expand_binomtest t_ =\
neuper@37906: \(Repeat                       \
neuper@37906: \((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ \
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_mult_1             False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_mult_0             False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_add_zero_left      False))) @@ \
neuper@37906: 
neuper@37906: \ (Try (Repeat (Calculate plus  ))) @@ \
neuper@37906: \ (Try (Repeat (Calculate times ))) @@ \
neuper@37906: \ (Try (Repeat (Calculate power_))) @@ \
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite realpow_plus_1          False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ \
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_num_collect        False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ \
neuper@37906: 
neuper@37906: \ (Try (Repeat (Rewrite real_one_collect        False))) @@ \
neuper@37906: \ (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ \ 
neuper@37906: 
neuper@37906: \ (Try (Repeat (Calculate plus  ))) @@ \
neuper@37906: \ (Try (Repeat (Calculate times ))) @@ \
neuper@37906: \ (Try (Repeat (Calculate power_)))) \  
neuper@37906: \ t_)";
neuper@37906: ------------------------------------------------------*)
neuper@37906: 
neuper@37906: val expand_binomtest =
neuper@37906:   Rls{id = "expand_binomtest", preconds = [], 
neuper@37906:       rew_ord = ("termlessI",termlessI),
neuper@37906:       erls = testerls, srls = Erls,
neuper@37922:       calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
neuper@37922: 	      ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37922: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37906: 	      ],
neuper@37906:       (*asm_thm = [],*)
neuper@37906:       rules = [Thm ("real_plus_binom_pow2"  ,num_str real_plus_binom_pow2),     
neuper@37906: 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
neuper@37906: 	       Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),    
neuper@37906: 	      (*"(a + b)*(a + b) = ...*)
neuper@37906: 	       Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),   
neuper@37906: 	       (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
neuper@37906: 	       Thm ("real_minus_binom_times",num_str real_minus_binom_times),   
neuper@37906: 	       (*"(a - b)*(a - b) = ...*)
neuper@37906: 	       Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),   
neuper@37906: 		(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
neuper@37906: 	       Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),   
neuper@37906: 		(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
neuper@37906: 	       (*RL 020915*)
neuper@37906: 	       Thm ("real_pp_binom_times",num_str real_pp_binom_times), 
neuper@37906: 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
neuper@37906:                Thm ("real_pm_binom_times",num_str real_pm_binom_times), 
neuper@37906: 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
neuper@37906:                Thm ("real_mp_binom_times",num_str real_mp_binom_times), 
neuper@37906: 		(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
neuper@37906:                Thm ("real_mm_binom_times",num_str real_mm_binom_times), 
neuper@37906: 		(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
neuper@37906: 	       Thm ("realpow_multI",num_str realpow_multI),                
neuper@37906: 		(*(a*b)^^^n = a^^^n * b^^^n*)
neuper@37906: 	       Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
neuper@37906: 	        (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
neuper@37906: 	       Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
neuper@37906: 	        (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
neuper@37906: 
neuper@37906: 
neuper@37906:              (*  Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),	
neuper@37906: 		(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37906: 	       Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),	
neuper@37906: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37906: 	       Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),	
neuper@37906: 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
neuper@37906: 	       Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),	
neuper@37906: 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
neuper@37906: 	       *)
neuper@37906: 	       
neuper@37906: 	       Thm ("real_mult_1",num_str real_mult_1),              (*"1 * z = z"*)
neuper@37906: 	       Thm ("real_mult_0",num_str real_mult_0),              (*"0 * z = 0"*)
neuper@37906: 	       Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
neuper@37906: 
neuper@37906: 	       Calc ("op +", eval_binop "#add_"), 
neuper@37906: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37906: 	       Calc ("Atools.pow", eval_binop "#power_"),
neuper@37906:                (*	       
neuper@37906: 	        Thm ("real_mult_commute",num_str real_mult_commute),		(*AC-rewriting*)
neuper@37906: 	       Thm ("real_mult_left_commute",num_str real_mult_left_commute),	(**)
neuper@37906: 	       Thm ("real_mult_assoc",num_str real_mult_assoc),			(**)
neuper@37906: 	       Thm ("real_add_commute",num_str real_add_commute),		(**)
neuper@37906: 	       Thm ("real_add_left_commute",num_str real_add_left_commute),	(**)
neuper@37906: 	       Thm ("real_add_assoc",num_str real_add_assoc),	                (**)
neuper@37906: 	       *)
neuper@37906: 	       
neuper@37906: 	       Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),		
neuper@37906: 	       (*"r1 * r1 = r1 ^^^ 2"*)
neuper@37906: 	       Thm ("realpow_plus_1",num_str realpow_plus_1),			
neuper@37906: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
neuper@37906: 	       (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),		
neuper@37906: 	       (*"z1 + z1 = 2 * z1"*)*)
neuper@37906: 	       Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),		
neuper@37906: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37906: 
neuper@37906: 	       Thm ("real_num_collect",num_str real_num_collect), 
neuper@37906: 	       (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
neuper@37906: 	       Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),	
neuper@37906: 	       (*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
neuper@37906: 	       Thm ("real_one_collect",num_str real_one_collect),		
neuper@37906: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37906: 	       Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), 
neuper@37906: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37906: 
neuper@37906: 	       Calc ("op +", eval_binop "#add_"), 
neuper@37906: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37906: 	       Calc ("Atools.pow", eval_binop "#power_")
neuper@37906: 	       ],
neuper@37906:       scr = EmptyScr
neuper@37906: (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
neuper@37906:       }:rls;      
neuper@37906: 
neuper@37906: 
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906:    [("make_polytest", prep_rls make_polytest),
neuper@37906:     ("expand_binomtest", prep_rls expand_binomtest)
neuper@37906:     ]);
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: