wneuper/isa: src/Tools/isac/Knowledge/Root.thy@d3a3cc2f0382

     1 (* theory collecting all knowledge for Root

     2    created by:

     3          date:

     4    changed by: rlang

     5    last change by: rlang

     6              date: 02.10.21

     7 *)

     9 theory Root imports Poly begin

    11 consts

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

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

    16 axiomatization where (*.not contained in Isabelle2002,

    17          stated as axioms, TODO: prove as theorems;

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

    20   root_plus_minus:         "0 <= b ==>

    21 			   (a \<up> 2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and

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

    24  (* for expand_rootbinom *)

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

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

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

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

    29   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

    30   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

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

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

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

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

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

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

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

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

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

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

    44 ML \<open>

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

    46 (*evaluation square-root over the integers*)

    47 fun eval_sqrt (_ : string) (_ : string) t (_: theory) =

    48   (case t of

    49     Const (op0, _) $ num =>

    50       (case try HOLogic.dest_number num of

    51         SOME (T, ni)=>

    52           if ni < 0 then NONE

    53           else

    54             let val fact = Eval.squfact ni;

    55             in

    56               if fact * fact = ni

    57               then

    58                 SOME ("#sqrt #" ^ string_of_int ni ^ " = #"

    59                     ^ string_of_int (if ni = 0 then 0 else ni div fact),

    60                   HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num T fact))

    61               else if fact = 1 then NONE

    62               else

    63                 SOME ("#sqrt #" ^ string_of_int ni ^ " = sqrt (#"

    64                     ^ string_of_int fact ^ " * #" ^ string_of_int fact ^ " * #"

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

    66                   HOLogic.Trueprop $ TermC.mk_equality

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

    68             end

    69         | NONE => NONE)

    70   | _ => NONE);

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

    73 > eval_sqrt thmid op_ t thy;

    74 > val Free (n1,t1) = arg;

    75 > val SOME ni = int_of_str n1;

    76 *)

    77 \<close>

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

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

    81 ML \<open>

    82 local (* Vers. 7.10.99.A *)

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

    86 fun pr_ord EQUAL = "EQUAL"

    87   | pr_ord LESS  = "LESS"

    88   | pr_ord GREATER = "GREATER";

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

    91   (case a of \<^const_name>\<open>sqrt\<close>  => ((("|||", 0), T), 0)      (*WN greatest *)

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

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

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

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

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

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

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

    99     (case str of \<^const_name>\<open>sqrt\<close>  => (1000 + size_of_term' t)

   100                | _ => 1 + size_of_term' t)

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

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

   103   | size_of_term' _ = 1;

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

   105     (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)

   106                                    | ord => ord)

   107   | term_ord' pr _(*thy*) (t, u) =

   108     (if pr then

   109 	 let

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

   111 	     val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^"\" @ \"[" ^

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

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

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

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

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

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

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

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

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

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

   122 	 in () end

   123      else ();

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

   125 	 EQUAL =>

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

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

   128 	                          | ord => ord)

   129 	 end

   130        | ord => ord)

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

   132   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord

   133             (dest_hd' f, dest_hd' g)

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

   135     list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);

   137 in

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

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

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

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

   142 *)

   144 (*args

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

   146    thy:

   147    subst: no bound variables, only Root.sqrt

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

   149 fun sqrt_right (pr:bool) thy (_: subst) (ts, us) =

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

   151 end;

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

   154 [("termlessI", termlessI),

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

   156  ]);

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

   159 val Root_crls =

   160   Rule_Set.append_rules "Root_crls" Atools_erls [

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

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

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

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

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

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

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

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

   170 val Root_erls =

   171   Rule_Set.append_rules "Root_erls" Atools_erls [

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

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

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

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

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

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

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

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

   180 val Root_erls =

   181   Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [

   182     \<^rule_thm>\<open>not_false\<close>,

   183     \<^rule_thm>\<open>not_true\<close>,

   184     \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];

   185 \<close>

   186 rule_set_knowledge Root_erls = Root_erls

   187 ML \<open>

   189 val make_rooteq = prep_rls'(

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

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

   192     erls = Atools_erls, srls = Rule_Set.Empty,

   193     calc = [], errpatts = [],

   194     rules = [

   195       \<^rule_thm>\<open>real_diff_minus\<close>,	 (*"a - b = a + (-1) * b"*)

   197       \<^rule_thm>\<open>distrib_right\<close>,	 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

   198       \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

   199       \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

   200       \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

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

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

   204       \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)

   206        (*AC-rewriting*)

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

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

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

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

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

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

   214       \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1  \<up>  2"*)

   215       \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)

   216       \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)

   217       \<^rule_thm>\<open>real_mult_2_assoc\<close>,	(*"z1 + (z1 + k) = 2 * z1 + k"*)

   219       \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==> l * n + m * n = (l + m) * n"*)

   220       \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)

   221       \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)

   222       \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)

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

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

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

   227     scr = Rule.Empty_Prog});

   228 \<close>

   229 rule_set_knowledge make_rooteq = make_rooteq

   230 ML \<open>

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

   234 val expand_rootbinoms = prep_rls'(

   235   Rule_Def.Repeat {

   236     id = "expand_rootbinoms", preconds = [], rew_ord = ("termlessI",termlessI),

   237     erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],

   238     rules = [

   239        \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b)  \<up>  2 = a  \<up>  2 + 2 * a * b + b  \<up>  2"*)

   240        \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)

   241        \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b)  \<up>  2 = a  \<up>  2 - 2 * a * b + b  \<up>  2"*)

   242        \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)

   243        \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a  \<up>  2 - b  \<up>  2"*)

   244        \<^rule_thm>\<open>real_plus_minus_binom2\<close>,  (*"(a - b) * (a + b) = a  \<up>  2 - b  \<up>  2"*)

   245        (*RL 020915*)

   246        \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)

   247        \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)

   248        \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)

   249        \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)

   250        \<^rule_thm>\<open>realpow_mul\<close>,  (*(a*b) \<up> n = a \<up> n * b \<up> n*)

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

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

   254        \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)

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

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

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

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

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

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

   263        \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1  \<up>  2"*)

   264        \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)

   265        \<^rule_thm>\<open>real_mult_2_assoc\<close>,	 (*"z1 + (z1 + k) = 2 * z1 + k"*)

   267        \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*)

   268        \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)

   269        \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)

   270        \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)

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

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

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

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

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

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

   278     scr = Rule.Empty_Prog});

   279 \<close>

   280 rule_set_knowledge expand_rootbinoms = expand_rootbinoms

   281 ML \<open>

   282 \<close> ML \<open>

   283 \<close> ML \<open>

   284 \<close>

   285 end

author	wneuper <walther.neuper@jku.at>
	Wed, 18 Aug 2021 16:03:08 +0200
changeset 60385	d3a3cc2f0382
parent 60384	2b6e73df4e5d
child 60405	d4ebe139100d
permissions	-rw-r--r--