(* theory collecting all knowledge for Root

    created by: 

          date: 

    changed by: rlang

    last change by: rlang

              date: 02.10.21

 *)

 theory Root imports Simplify begin

 consts

   sqrt   :: "real => real"         (*"(sqrt _ )" [80] 80*)

   nroot  :: "[real, real] => real"

 axioms (*.not contained in Isabelle2002,

          stated as axioms, TODO: prove as theorems;

          theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)

   root_plus_minus         "0 <= b ==> 

 			   (a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))"

   root_false		  "b < 0 ==> (a^^^2 = b) = False"

  (* for expand_rootbinom *)

   real_pp_binom_times     "(a + b)*(c + d) = a*c + a*d + b*c + b*d"

   real_pm_binom_times     "(a + b)*(c - d) = a*c - a*d + b*c - b*d"

   real_mp_binom_times     "(a - b)*(c + d) = a*c + a*d - b*c - b*d"

   real_mm_binom_times     "(a - b)*(c - d) = a*c - a*d - b*c + b*d"

   real_plus_binom_pow3    "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"

   real_minus_binom_pow3   "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"

   realpow_mul             "(a*b)^^^n = a^^^n * b^^^n"

   real_diff_minus         "a - b = a + (-1) * b"

   real_plus_binom_times   "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"

   real_minus_binom_times  "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"

   real_plus_binom_pow2    "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"

   real_minus_binom_pow2   "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"

   real_plus_minus_binom1  "(a + b)*(a - b) = a^^^2 - b^^^2"

   real_plus_minus_binom2  "(a - b)*(a + b) = a^^^2 - b^^^2"

   real_root_positive      "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)"

   real_root_negative      "a <  0 ==> (x ^^^ 2 = a) = False"

 ML {*

 (*-------------------------functions---------------------*)

 (*evaluation square-root over the integers*)

 fun eval_sqrt (thmid:string) (op_:string) (t as 

 	       (Const(op0,t0) $ arg)) thy = 

     (case arg of 

 	Free (n1,t1) =>

 	(case int_of_str n1 of

 	     SOME ni => 

 	     if ni < 0 then NONE

 	     else

 		 let val fact = squfact ni;

 		 in if fact*fact = ni 

 		    then SOME ("#sqrt #"^(string_of_int ni)^" = #"

 			       ^(string_of_int (if ni = 0 then 0

 						else ni div fact)),

 			       Trueprop $ mk_equality (t, term_of_num t1 fact))

 		    else if fact = 1 then NONE

 		    else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"

 			       ^(string_of_int fact)^" * #"

 			       ^(string_of_int fact)^" * #"

 			       ^(string_of_int (ni div (fact*fact))^")"),

 			       Trueprop $ 

 					(mk_equality 

 					     (t, 

 					      (mk_factroot op0 t1 fact 

 						(ni div (fact*fact))))))

 	         end

 	   | NONE => NONE)

       | _ => NONE)

   | eval_sqrt _ _ _ _ = NONE;

 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");

 > eval_sqrt thmid op_ t thy;

 > val Free (n1,t1) = arg; 

 > val SOME ni = int_of_str n1;

 *)

 calclist':= overwritel (!calclist', 

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

     (*different types for 'sqrt 4' --- 'Calculate sqrt_'*)

     ]);

 local (* Vers. 7.10.99.A *)

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

 fun pr_ord EQUAL = "EQUAL"

   | pr_ord LESS  = "LESS"

   | pr_ord GREATER = "GREATER";

 fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)

   (case a of "Root.sqrt"  => ((("|||", 0), T), 0)      (*WN greatest *)

 	   | _ => (((a, 0), T), 0))

   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)

   | dest_hd' (Var v) = (v, 2)

   | dest_hd' (Bound i) = ((("", i), dummyT), 3)

   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);

 fun size_of_term' (Const(str,_) $ t) =

     (case str of "Root.sqrt"  => (1000 + size_of_term' t)

                | _ => 1 + size_of_term' t)

   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body

   | size_of_term' (f $ t) = size_of_term' f  +  size_of_term' t

   | size_of_term' _ = 1;

 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

       (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)

   | term_ord' pr thy (t, u) =

       (if pr then 

 	 let

 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;

 	   val _=writeln("t= f@ts= \""^

 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^

 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");

 	   val _=writeln("u= g@us= \""^

 	      ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^

 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");

 	   val _=writeln("size_of_term(t,u)= ("^

 	      (string_of_int(size_of_term' t))^", "^

 	      (string_of_int(size_of_term' u))^")");

 	   val _=writeln("hd_ord(f,g)      = "^((pr_ord o hd_ord)(f,g)));

 	   val _=writeln("terms_ord(ts,us) = "^

 			   ((pr_ord o terms_ord str false)(ts,us)));

 	   val _=writeln("-------");

 	 in () end

        else ();

 	 case int_ord (size_of_term' t, size_of_term' u) of

 	   EQUAL =>

 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in

 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 

 	     | ord => ord)

 	     end

 	 | ord => ord)

 and hd_ord (f, g) =                                        (* ~ term.ML *)

   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)

 and terms_ord str pr (ts, us) = 

     list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);

 in

 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses 

   by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1 

      (2) hd_ord: greater to right, 'sqrt' < numerals < variables

      (3) terms_ord: recurs. on args, greater to right

 *)

 (*args

    pr: print trace, WN0509 'sqrt_right true' not used anymore

    thy:

    subst: no bound variables, only Root.sqrt

    tu: the terms to compare (t1, t2) ... *)

 fun sqrt_right (pr:bool) thy (_:subst) tu = 

     (term_ord' pr thy(***) tu = LESS );

 end;

 rew_ord' := overwritel (!rew_ord',

 [("termlessI", termlessI),

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

  ]);

 (*-------------------------rulse-------------------------*)

 val Root_crls = 

       append_rls "Root_crls" Atools_erls 

        [Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),

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

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

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

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

         Calc ("op -", eval_binop "#sub_"),

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

         Calc ("op =",eval_equal "#equal_") 

         ];

 val Root_erls = 

       append_rls "Root_erls" Atools_erls 

        [Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),

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

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

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

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

         Calc ("op -", eval_binop "#sub_"),

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

         Calc ("op =",eval_equal "#equal_") 

         ];

 ruleset' := overwritelthy @{theory} (!ruleset',

 			[("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) 

 			 ]);

 val make_rooteq = prep_rls(

   Rls{id = "make_rooteq", preconds = []:term list, 

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

       erls = Atools_erls, srls = Erls,

       calc = [],

       (*asm_thm = [],*)

       rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),			

 	       (*"a - b = a + (-1) * b"*)

 	       Thm ("left_distrib" ,num_str @{thm left_distrib}),	

 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

 	       Thm ("left_distrib2",num_str @{thm left_distrib2}),	

 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

 	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),	

 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

 	       Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib2}),	

 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

 	       Thm ("mult_1_left",num_str @{thm mult_1_left}),                         

 	       (*"1 * z = z"*)

 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),                         

 	       (*"0 * z = 0"*)

 	       Thm ("add_0_left",num_str @{thm add_0_left}),		

 	       (*"0 + z = z"*)

 	       Thm ("real_mult_commute",num_str @{thm real_mult_commute}),

 		(*AC-rewriting*)

 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),

          	(**)

 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),

 	        (**)

 	       Thm ("add_commute",num_str @{thm add_commute}),

 		(**)

 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),

 	        (**)

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

 	        (**)

 	       Thm ("sym_realpow_twoI",

                      num_str (@{thm realpow_twoI} RS @{thm sym})),

 	       (*"r1 * r1 = r1 ^^^ 2"*)

 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),			

 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

 	       Thm ("sym_real_mult_2",

                      num_str (@{thm real_mult_2} RS @{thm sym})),

 	       (*"z1 + z1 = 2 * z1"*)

 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),		

 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

 	       Thm ("real_num_collect",num_str @{thm real_num_collect}), 

 	       (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)

 	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),	

 	       (*"[| l is_const; m is_const |] ==>  

                                    l * n + (m * n + k) =  (l + m) * n + k"*)

 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),		

 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)

 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 

 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

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

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

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

 	       ],

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

       }:rls);      

 ruleset' := overwritelthy @{theory} (!ruleset',

 			[("make_rooteq", make_rooteq)

 			 ]);

 val expand_rootbinoms = prep_rls(

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

       rew_ord = ("termlessI",termlessI),

       erls = Atools_erls, srls = Erls,

       calc = [],

       (*asm_thm = [],*)

       rules = [Thm ("real_plus_binom_pow2"  ,num_str @{thm real_plus_binom_pow2}),     

 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)

 	       Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),    

 	       (*"(a + b)*(a + b) = ...*)

 	       Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),    

 		(*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)

 	       Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),   

 	       (*"(a - b)*(a - b) = ...*)

 	       Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),   

 		(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)

 	       Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),   

 		(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)

 	       (*RL 020915*)

 	       Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), 

 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)

                Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), 

 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)

                Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), 

 		(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)

                Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), 

 		(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)

 	       Thm ("realpow_mul",num_str @{thm realpow_mul}),                 

 		(*(a*b)^^^n = a^^^n * b^^^n*)

 	       Thm ("mult_1_left",num_str @{thm mult_1_left}),         (*"1 * z = z"*)

 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),         (*"0 * z = 0"*)

 	       Thm ("add_0_left",num_str @{thm add_0_left}), 

                  (*"0 + z = z"*)

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

 	       Calc ("op -", eval_binop "#sub_"), 

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

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

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

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

 	       Thm ("sym_realpow_twoI",

                      num_str (@{thm realpow_twoI} RS @{thm sym})),

 	       (*"r1 * r1 = r1 ^^^ 2"*)

 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),			

 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),		

 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

 	       Thm ("real_num_collect",num_str @{thm real_num_collect}), 

 	       (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)

 	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),	

 	       (*"[| l is_const; m is_const |] ==>

                   l * n + (m * n + k) =  (l + m) * n + k"*)

 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),		

 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)

 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 

 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

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

 	       Calc ("op -", eval_binop "#sub_"), 

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

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

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

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

 	       ],

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

        }:rls);      

 ruleset' := overwritelthy @{theory} (!ruleset',

 			[("expand_rootbinoms", expand_rootbinoms)

 			 ]);

 *}

 end