neuper@37906: (* collecting all knowledge for Root
neuper@37906:    created by: 
neuper@37906:          date: 
neuper@37906:    changed by: rlang
neuper@37906:    last change by: rlang
neuper@37906:              date: 02.10.24
neuper@37906: *)
neuper@37906: 
neuper@37906: (* use"../knowledge/Root.ML";
neuper@37947:    use"Knowledge/Root.ML";
neuper@37906:    use"Root.ML";
neuper@37906: 
neuper@37906:    remove_thy"Root";
neuper@37947:    use_thy"Knowledge/Isac";
neuper@37906: 
neuper@37906:    use"ROOT.ML";
neuper@37906:    cd"knowledge";
neuper@37906:  *)
neuper@37906: "******* Root.ML begin *******";
neuper@37906: theory' := overwritel (!theory', [("Root.thy",Root.thy)]);                      
neuper@37906: (*-------------------------functions---------------------*)
neuper@37906: (*evaluation square-root over the integers*)
neuper@37906: fun eval_sqrt (thmid:string) (op_:string) (t as 
neuper@37906: 	       (Const(op0,t0) $ arg)) thy = 
neuper@37906:     (case arg of 
neuper@37906: 	Free (n1,t1) =>
neuper@37906: 	(case int_of_str n1 of
neuper@37926: 	     SOME ni => 
neuper@37926: 	     if ni < 0 then NONE
neuper@37906: 	     else
neuper@37906: 		 let val fact = squfact ni;
neuper@37906: 		 in if fact*fact = ni 
neuper@37926: 		    then SOME ("#sqrt #"^(string_of_int ni)^" = #"
neuper@37906: 			       ^(string_of_int (if ni = 0 then 0
neuper@37906: 						else ni div fact)),
neuper@37906: 			       Trueprop $ mk_equality (t, term_of_num t1 fact))
neuper@37926: 		    else if fact = 1 then NONE
neuper@37926: 		    else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
neuper@37906: 			       ^(string_of_int fact)^" * #"
neuper@37906: 			       ^(string_of_int fact)^" * #"
neuper@37906: 			       ^(string_of_int (ni div (fact*fact))^")"),
neuper@37906: 			       Trueprop $ 
neuper@37906: 					(mk_equality 
neuper@37906: 					     (t, 
neuper@37906: 					      (mk_factroot op0 t1 fact 
neuper@37906: 							   (ni div (fact*fact))))))
neuper@37906: 	     end
neuper@37926: 	   | NONE => NONE)
neuper@37926:       | _ => NONE)
neuper@37906: 
neuper@37926:   | eval_sqrt _ _ _ _ = NONE;
neuper@37906: (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");
neuper@37906: > eval_sqrt thmid op_ t thy;
neuper@37906: > val Free (n1,t1) = arg; 
neuper@37926: > val SOME ni = int_of_str n1;
neuper@37906: *)
neuper@37906: 
neuper@37906: calclist':= overwritel (!calclist', 
neuper@37922:    [("SQRT"    ,("Root.sqrt"   ,eval_sqrt "#sqrt_"))
neuper@37906:     (*different types for 'sqrt 4' --- 'Calculate sqrt_'*)
neuper@37906:     ]);
neuper@37906: 
neuper@37906: 
neuper@37906: local (* Vers. 7.10.99.A *)
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 "Root.sqrt"  => ((("|||", 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: fun size_of_term' (Const(str,_) $ t) =
neuper@37906:     (case str of "Root.sqrt"  => (1000 + size_of_term' t)
neuper@37906:                | _ => 1 + size_of_term' t)
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: 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@37938: 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
neuper@37938: 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
neuper@37906: 	   val _=writeln("u= g@us= \""^
neuper@37938: 	      ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
neuper@37938: 	      (commas(map(Syntax.string_of_term (thy2ctxt 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: 
neuper@37906: in
neuper@37906: (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses 
neuper@37906:   by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1 
neuper@37906:      (2) hd_ord: greater to right, 'sqrt' < numerals < variables
neuper@37906:      (3) terms_ord: recurs. on args, greater to right
neuper@37906: *)
neuper@37906: 
neuper@37906: (*args
neuper@37906:    pr: print trace, WN0509 'sqrt_right true' not used anymore
neuper@37906:    thy:
neuper@37906:    subst: no bound variables, only Root.sqrt
neuper@37906:    tu: the terms to compare (t1, t2) ... *)
neuper@37906: fun sqrt_right (pr:bool) thy (_:subst) tu = 
neuper@37906:     (term_ord' pr thy(***) tu = LESS );
neuper@37906: end;
neuper@37906: 
neuper@37906: rew_ord' := overwritel (!rew_ord',
neuper@37906: [("termlessI", termlessI),
neuper@37935:  ("sqrt_right", sqrt_right false (theory "Pure"))
neuper@37906:  ]);
neuper@37906: 
neuper@37906: (*-------------------------rulse-------------------------*)
neuper@37906: val Root_crls = 
neuper@37906:       append_rls "Root_crls" Atools_erls 
neuper@37906:        [Thm  ("real_unari_minus",num_str real_unari_minus),
neuper@37906:         Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
neuper@37906:         Calc ("HOL.divide",eval_cancel "#divide_"),
neuper@37906:         Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37906:         Calc ("op +", eval_binop "#add_"), 
neuper@37906:         Calc ("op -", eval_binop "#sub_"),
neuper@37906:         Calc ("op *", eval_binop "#mult_"),
neuper@37906:         Calc ("op =",eval_equal "#equal_") 
neuper@37906:         ];
neuper@37906: 
neuper@37906: val Root_erls = 
neuper@37906:       append_rls "Root_erls" Atools_erls 
neuper@37906:        [Thm  ("real_unari_minus",num_str real_unari_minus),
neuper@37906:         Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
neuper@37906:         Calc ("HOL.divide",eval_cancel "#divide_"),
neuper@37906:         Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37906:         Calc ("op +", eval_binop "#add_"), 
neuper@37906:         Calc ("op -", eval_binop "#sub_"),
neuper@37906:         Calc ("op *", eval_binop "#mult_"),
neuper@37906:         Calc ("op =",eval_equal "#equal_") 
neuper@37906:         ];
neuper@37906: 
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906: 			[("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) 
neuper@37906: 			 ]);
neuper@37906: 
neuper@37906: val make_rooteq = prep_rls(
neuper@37906:   Rls{id = "make_rooteq", preconds = []:term list, 
neuper@37906:       rew_ord = ("sqrt_right", sqrt_right false Root.thy),
neuper@37906:       erls = Atools_erls, srls = Erls,
neuper@37906:       calc = [],
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: 
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: 	       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: 	       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: 	       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 = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37906:       }:rls);      
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906: 			[("make_rooteq", make_rooteq)
neuper@37906: 			 ]);
neuper@37906: 
neuper@37906: val expand_rootbinoms = prep_rls(
neuper@37906:   Rls{id = "expand_rootbinoms", preconds = [], 
neuper@37906:       rew_ord = ("termlessI",termlessI),
neuper@37906:       erls = Atools_erls, srls = Erls,
neuper@37906:       calc = [],
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_mul",num_str realpow_mul),                 
neuper@37906: 		(*(a*b)^^^n = a^^^n * b^^^n*)
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 "#sub_"), 
neuper@37906: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37906: 	       Calc ("HOL.divide"  ,eval_cancel "#divide_"),
neuper@37906: 	       Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
neuper@37906: 	       Calc ("Atools.pow", eval_binop "#power_"),
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 ("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 "#sub_"), 
neuper@37906: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37906: 	       Calc ("HOL.divide"  ,eval_cancel "#divide_"),
neuper@37906: 	       Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
neuper@37906: 	       Calc ("Atools.pow", eval_binop "#power_")
neuper@37906: 	       ],
neuper@37906:       scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37906:        }:rls);      
neuper@37906: 
neuper@37906: 
neuper@37906: ruleset' := overwritelthy thy (!ruleset',
neuper@37906: 			[("expand_rootbinoms", expand_rootbinoms)
neuper@37906: 			 ]);
neuper@37906: "******* Root.ML end *******";