(* 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^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and

  root_false:		  "b < 0 ==> (a^^^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)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and

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

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

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

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

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

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

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

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

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

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

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

ML {*

val thy = @{theory};

(*-------------------------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 TermC.int_of_str_opt n1 of

	     SOME ni => 

	     if ni < 0 then NONE

	     else

		 let val fact = Calc.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 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))^")"),

			       HOLogic.Trueprop $ 

					(TermC.mk_equality 

					     (t, 

					      (TermC.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;

*)

*}

setup {* KEStore_Elems.add_calcs

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

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

ML {*

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 "NthRoot.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 "NthRoot.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 => 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= \"" ^ Celem.term2str f ^"\" @ \"[" ^

	                      commas (map Celem.term2str ts) ^ "]\"");

	     val _ = tracing ("u= g@us= \"" ^ Celem.term2str g ^"\" @ \"[" ^

	                      commas (map Celem.term2str 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 (Celem.assoc_thy "Isac"))(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 (_: Celem.subst) tu = 

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

end;

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

[("termlessI", termlessI),

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

 ]);

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

val Root_crls = 

      Celem.append_rls "Root_crls" Atools_erls 

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

        Celem.Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),

        Celem.Calc ("Rings.divide_class.divide",eval_cancel "#divide_e"),

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

        Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

        Celem.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),

        Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),

        Celem.Calc ("HOL.eq",eval_equal "#equal_") 

        ];

val Root_erls = 

      Celem.append_rls "Root_erls" Atools_erls 

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

        Celem.Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),

        Celem.Calc ("Rings.divide_class.divide",eval_cancel "#divide_e"),

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

        Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

        Celem.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),

        Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),

        Celem.Calc ("HOL.eq",eval_equal "#equal_") 

        ];

*}

setup {* KEStore_Elems.add_rlss [("Root_erls", (Context.theory_name @{theory}, Root_erls))] *}

ML {*

val make_rooteq = prep_rls'(

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

      rew_ord = ("sqrt_right", sqrt_right false thy),

      erls = Atools_erls, srls = Celem.Erls,

      calc = [], errpatts = [],

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

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

	       Celem.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),	

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

	       Celem.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),	

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

	       Celem.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),	

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

	       Celem.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),	

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

	       Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),                         

	       (*"1 * z = z"*)

	       Celem.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),                         

	       (*"0 * z = 0"*)

	       Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),		

	       (*"0 + z = z"*)

	       Celem.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),

		(*AC-rewriting*)

	       Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),

         	(**)

	       Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),

	        (**)

	       Celem.Thm ("add_commute",TermC.num_str @{thm add.commute}),

		(**)

	       Celem.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),

	        (**)

	       Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),

	        (**)

	       Celem.Thm ("sym_realpow_twoI",

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

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

	       Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),			

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

	       Celem.Thm ("sym_real_mult_2",

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

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

	       Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),		

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

	       Celem.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 

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

	       Celem.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),	

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

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

	       Celem.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),		

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

	       Celem.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 

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

	       Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

	       Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),

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

	       ],

      scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

      });      

*}

setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}

ML {*

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

val expand_rootbinoms = prep_rls'(

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

      rew_ord = ("termlessI",termlessI),

      erls = Atools_erls, srls = Celem.Erls,

      calc = [], errpatts = [],

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

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

	       Celem.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),    

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

	       Celem.Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),    

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

	       Celem.Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),   

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

	       Celem.Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),   

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

	       Celem.Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),   

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

	       (*RL 020915*)

	       Celem.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}), 

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

               Celem.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}), 

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

               Celem.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}), 

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

               Celem.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}), 

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

	       Celem.Thm ("realpow_mul",TermC.num_str @{thm realpow_mul}),                 

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

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

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

	       Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}), 

                 (*"0 + z = z"*)

	       Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

	       Celem.Calc ("Groups.minus_class.minus", eval_binop "#sub_"), 

	       Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),

	       Celem.Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e"),

	       Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),

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

	       Celem.Thm ("sym_realpow_twoI",

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

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

	       Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),			

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

	       Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),		

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

	       Celem.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 

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

	       Celem.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),	

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

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

	       Celem.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),		

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

	       Celem.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 

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

	       Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

	       Celem.Calc ("Groups.minus_class.minus", eval_binop "#sub_"), 

	       Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),

	       Celem.Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e"),

	       Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),

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

	       ],

      scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

       });      

*}

setup {* KEStore_Elems.add_rlss

  [("expand_rootbinoms", (Context.theory_name @{theory}, expand_rootbinoms))] *}

end