1 (* theory collecting all knowledge for Root
9 theory Root imports Poly begin
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"
45 (*-------------------------functions---------------------*)
46 (*evaluation square-root over the integers*)
47 fun eval_sqrt (_ : string) (_ : string) t (_: Proof.context) =
49 Const (op0, _) $ num =>
50 (case try HOLogic.dest_number num of
54 let val fact = Eval.squfact ni;
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
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)))))
72 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", TermC.parse_test @{context} "sqrt 0");
73 > eval_sqrt thmid op_ t thy;
74 > val Free (n1,t1) = arg;
75 > val SOME ni = int_of_str n1;
79 calculation SQRT (sqrt) = \<open>eval_sqrt "#sqrt_"\<close>
80 (*different types for 'sqrt 4' --- 'Calculate SQRT'*)
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)
107 | term_ord' pr _(*thy*) (t, u) =
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("-------");
124 case int_ord (size_of_term' t, size_of_term' u) of
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)
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);
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
145 pr: print trace, WN0509 'sqrt_right true' not used anymore
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 );
154 setup \<open>KEStore_Elems.add_rew_ords [
155 ("termlessI", termlessI),
156 ("sqrt_right", sqrt_right false @{theory "Pure"})]\<close>
159 (*------------------------- rules -------------------------*)
161 Rule_Set.append_rules "Root_crls" Atools_erls [
162 \<^rule_thm>\<open>real_unari_minus\<close>,
163 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
164 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
165 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
166 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
167 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
168 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
169 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
172 Rule_Set.append_rules "Root_erls" Atools_erls [
173 \<^rule_thm>\<open>real_unari_minus\<close>,
174 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
175 \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
176 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
177 \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(Calc_Binop.numeric "#add_"),
178 \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(Calc_Binop.numeric "#sub_"),
179 \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(Calc_Binop.numeric "#mult_"),
180 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
182 Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [
183 \<^rule_thm>\<open>not_false\<close>,
184 \<^rule_thm>\<open>not_true\<close>,
185 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];
187 rule_set_knowledge Root_erls = Root_erls
190 val make_rooteq = prep_rls'(
191 Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list,
192 rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
193 erls = Atools_erls, srls = Rule_Set.Empty,
194 calc = [], errpatts = [],
196 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
198 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
199 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
200 \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
201 \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
203 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
204 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
205 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
208 \<^rule_thm>\<open>mult.commute\<close>,
209 \<^rule_thm>\<open>real_mult_left_commute\<close>,
210 \<^rule_thm>\<open>mult.assoc\<close>,
211 \<^rule_thm>\<open>add.commute\<close>,
212 \<^rule_thm>\<open>add.left_commute\<close>,
213 \<^rule_thm>\<open>add.assoc\<close>,
215 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
216 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
217 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
218 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
220 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==> l * n + m * n = (l + m) * n"*)
221 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
222 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
223 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
225 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
226 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
227 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
228 scr = Rule.Empty_Prog});
230 rule_set_knowledge make_rooteq = make_rooteq
233 val prep_rls' = Auto_Prog.prep_rls @{theory};
235 val expand_rootbinoms = prep_rls'(
237 id = "expand_rootbinoms", preconds = [], rew_ord = ("termlessI",termlessI),
238 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
240 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
241 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
242 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
243 \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)
244 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
245 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
247 \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
248 \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
249 \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
250 \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
251 \<^rule_thm>\<open>realpow_mul\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
253 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
254 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
255 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
257 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
258 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
259 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
260 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
261 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
262 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
264 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
265 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
266 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
268 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*)
269 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
270 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
271 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
273 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
274 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
275 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
276 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
277 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
278 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
279 scr = Rule.Empty_Prog});
281 rule_set_knowledge expand_rootbinoms = expand_rootbinoms