(* theory collecting all knowledge for Root

    created by: 

          date: 

    changed by: rlang

    last change by: rlang

              date: 02.10.21

 *)

 theory Root imports Poly begin

 consts

   (*sqrt   :: "real => real"         Isabelle "NthRoot.sqrt"*)

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

 axiomatization where (*.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 \<up> 2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and

   root_false:		  "b < 0 ==> (a \<up> 2 = b) = False" and

  (* for expand_rootbinom *)

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

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

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

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

   real_plus_binom_pow3:    "(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" and

   real_minus_binom_pow3:   "(a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3" and

   realpow_mul:             "(a*b) \<up> n = a \<up> n * b \<up> n" and

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

   real_plus_binom_times:   "(a + b)*(a + b) = a \<up> 2 + 2*a*b + b \<up> 2" and

   real_minus_binom_times:  "(a - b)*(a - b) = a \<up> 2 - 2*a*b + b \<up> 2" and

   real_plus_binom_pow2:    "(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and

   real_minus_binom_pow2:   "(a - b) \<up> 2 = a \<up> 2 - 2*a*b + b \<up> 2" and

   real_plus_minus_binom1:  "(a + b)*(a - b) = a \<up> 2 - b \<up> 2" and

   real_plus_minus_binom2:  "(a - b)*(a + b) = a \<up> 2 - b \<up> 2" and

   real_root_positive:      "0 <= a ==> (x  \<up>  2 = a) = (x = sqrt a)" and

   real_root_negative:      "a <  0 ==> (x  \<up>  2 = a) = False"

 ML \<open>

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

 (*evaluation square-root over the integers*)

 fun eval_sqrt (_ : string) (_ : string) (t as (Const (op0, _) $ arg)) _(*thy*) = 

     (case arg of 

   	  (Const (\<^const_name>\<open>numeral\<close>, T) $ num) =>

         let val ni = HOLogic.dest_numeral num

         in

     	    if ni < 0 then NONE

     	    else

     		    let val fact = Eval.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),

     			        HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num T 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)) ^ ")",

       		        HOLogic.Trueprop $ TermC.mk_equality 

                     (t, (TermC.mk_factroot op0 T fact (ni div (fact*fact)))))

     	      end

   	    end

     | _ => 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;

 *)

 \<close>

 calculation SQRT (sqrt) = \<open>eval_sqrt "#sqrt_"\<close>

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

 ML \<open>

 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 \<^const_name>\<open>sqrt\<close>  => ((("|||", 0), T), 0)      (*WN greatest *)

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

   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)

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

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

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

   | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";

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

     (case str of \<^const_name>\<open>sqrt\<close>  => (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 => Term_Ord.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 _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^"\" @ \"[" ^

 	                      commas (map UnparseC.term ts) ^ "]\"");

 	     val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^

 	                      commas (map UnparseC.term us) ^ "]\"");

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

 	                      string_of_int(size_of_term' t) ^", " ^

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

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

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

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

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

 	 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 Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord 

             (dest_hd' f, dest_hd' g)

 and terms_ord _(*str*) pr (ts, us) = 

     list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(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) (ts, us) = 

     (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );

 end;

 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',

 [("termlessI", termlessI),

  ("sqrt_right", sqrt_right false @{theory "Pure"})

  ]);

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

 val Root_crls = 

       Rule_Set.append_rules "Root_crls" Atools_erls 

        [\<^rule_thm>\<open>real_unari_minus\<close>,

         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),

         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),

         \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),

         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

         \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),

         \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

         \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_") 

         ];

 val Root_erls = 

       Rule_Set.append_rules "Root_erls" Atools_erls 

        [\<^rule_thm>\<open>real_unari_minus\<close>,

         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),

         \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),

         \<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),

         \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"), 

         \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),

         \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),

         \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_") 

         ];

 \<close>

 rule_set_knowledge Root_erls = Root_erls

 ML \<open>

 val make_rooteq = prep_rls'(

   Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list, 

       rew_ord = ("sqrt_right", sqrt_right false \<^theory>),

       erls = Atools_erls, srls = Rule_Set.Empty,

       calc = [], errpatts = [],

       rules = [\<^rule_thm>\<open>real_diff_minus\<close>,			

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

 	       \<^rule_thm>\<open>distrib_right\<close>,	

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

 	       \<^rule_thm>\<open>distrib_left\<close>,	

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

 	       \<^rule_thm>\<open>left_diff_distrib\<close>,	

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

 	       \<^rule_thm>\<open>right_diff_distrib\<close>,	

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

 	       \<^rule_thm>\<open>mult_1_left\<close>,                         

 	       (*"1 * z = z"*)

 	       \<^rule_thm>\<open>mult_zero_left\<close>,                         

 	       (*"0 * z = 0"*)

 	       \<^rule_thm>\<open>add_0_left\<close>,		

 	       (*"0 + z = z"*)

 	       \<^rule_thm>\<open>mult.commute\<close>,

 		(*AC-rewriting*)

 	       \<^rule_thm>\<open>real_mult_left_commute\<close>,

          	(**)

 	       \<^rule_thm>\<open>mult.assoc\<close>,

 	        (**)

 	       \<^rule_thm>\<open>add.commute\<close>,

 		(**)

 	       \<^rule_thm>\<open>add.left_commute\<close>,

 	        (**)

 	       \<^rule_thm>\<open>add.assoc\<close>,

 	        (**)

 	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,

 	       (*"r1 * r1 = r1  \<up>  2"*)

 	       \<^rule_thm>\<open>realpow_plus_1\<close>,			

 	       (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)

 	       \<^rule_thm_sym>\<open>real_mult_2\<close>,

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

 	       \<^rule_thm>\<open>real_mult_2_assoc\<close>,		

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

 	       \<^rule_thm>\<open>real_num_collect\<close>, 

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

 	       \<^rule_thm>\<open>real_num_collect_assoc\<close>,	

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

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

 	       \<^rule_thm>\<open>real_one_collect\<close>,		

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

 	       \<^rule_thm>\<open>real_one_collect_assoc\<close>, 

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

 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")

 	       ],

       scr = Rule.Empty_Prog

       });      

 \<close>

 rule_set_knowledge make_rooteq = make_rooteq

 ML \<open>

 val prep_rls' = Auto_Prog.prep_rls @{theory};

 val expand_rootbinoms = prep_rls'(

   Rule_Def.Repeat{id = "expand_rootbinoms", preconds = [], 

       rew_ord = ("termlessI",termlessI),

       erls = Atools_erls, srls = Rule_Set.Empty,

       calc = [], errpatts = [],

       rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,     

 	       (*"(a + b)  \<up>  2 = a  \<up>  2 + 2 * a * b + b  \<up>  2"*)

 	       \<^rule_thm>\<open>real_plus_binom_times\<close>,    

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

 	       \<^rule_thm>\<open>real_minus_binom_pow2\<close>,    

 		(*"(a - b)  \<up>  2 = a  \<up>  2 - 2 * a * b + b  \<up>  2"*)

 	       \<^rule_thm>\<open>real_minus_binom_times\<close>,   

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

 	       \<^rule_thm>\<open>real_plus_minus_binom1\<close>,   

 		(*"(a + b) * (a - b) = a  \<up>  2 - b  \<up>  2"*)

 	       \<^rule_thm>\<open>real_plus_minus_binom2\<close>,   

 		(*"(a - b) * (a + b) = a  \<up>  2 - b  \<up>  2"*)

 	       (*RL 020915*)

 	       \<^rule_thm>\<open>real_pp_binom_times\<close>, 

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

                \<^rule_thm>\<open>real_pm_binom_times\<close>, 

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

                \<^rule_thm>\<open>real_mp_binom_times\<close>, 

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

                \<^rule_thm>\<open>real_mm_binom_times\<close>, 

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

 	       \<^rule_thm>\<open>realpow_mul\<close>,                 

 		(*(a*b) \<up> n = a \<up> n * b \<up> n*)

 	       \<^rule_thm>\<open>mult_1_left\<close>,         (*"1 * z = z"*)

 	       \<^rule_thm>\<open>mult_zero_left\<close>,         (*"0 * z = 0"*)

 	       \<^rule_thm>\<open>add_0_left\<close>, 

                  (*"0 + z = z"*)

 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

 	       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 

 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),

 	       \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),

 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),

 	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,

 	       (*"r1 * r1 = r1  \<up>  2"*)

 	       \<^rule_thm>\<open>realpow_plus_1\<close>,			

 	       (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)

 	       \<^rule_thm>\<open>real_mult_2_assoc\<close>,		

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

 	       \<^rule_thm>\<open>real_num_collect\<close>, 

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

 	       \<^rule_thm>\<open>real_num_collect_assoc\<close>,	

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

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

 	       \<^rule_thm>\<open>real_one_collect\<close>,		

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

 	       \<^rule_thm>\<open>real_one_collect_assoc\<close>, 

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

 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

 	       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 

 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),

 	       \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),

 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")

 	       ],

       scr = Rule.Empty_Prog

        });      

 \<close>

 rule_set_knowledge expand_rootbinoms = expand_rootbinoms

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end