1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Aug 18 11:35:24 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Aug 18 16:03:08 2021 +0200
1.3 @@ -89,7 +89,7 @@
1.4
1.5 (*real_times_divide1_eq .. Isa02*)
1.6 real_times_divide_1_eq: "-1 * (c / d) = -1 * c / d " and
1.7 - real_times_divide_num: "a is_const ==> a * (c / d) = a * c / d " and
1.8 + real_times_divide_num: "a is_num ==> a * (c / d) = a * c / d " and
1.9
1.10 real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and
1.11 (*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
1.12 @@ -100,21 +100,21 @@
1.13
1.14 rat_power: "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
1.15
1.16 - rat_add: "[| a is_const; b is_const; c is_const; d is_const |] ==>
1.17 + rat_add: "[| a is_num; b is_num; c is_num; d is_num |] ==>
1.18 a / c + b / d = (a * d + b * c) / (c * d)" and
1.19 - rat_add_assoc: "[| a is_const; b is_const; c is_const; d is_const |] ==>
1.20 + rat_add_assoc: "[| a is_num; b is_num; c is_num; d is_num |] ==>
1.21 a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
1.22 - rat_add1: "[| a is_const; b is_const; c is_const |] ==>
1.23 + rat_add1: "[| a is_num; b is_num; c is_num |] ==>
1.24 a / c + b / c = (a + b) / c" and
1.25 - rat_add1_assoc: "[| a is_const; b is_const; c is_const |] ==>
1.26 + rat_add1_assoc: "[| a is_num; b is_num; c is_num |] ==>
1.27 a / c + (b / c + e) = (a + b) / c + e" and
1.28 - rat_add2: "[| a is_const; b is_const; c is_const |] ==>
1.29 + rat_add2: "[| a is_num; b is_num; c is_num |] ==>
1.30 a / c + b = (a + b * c) / c" and
1.31 - rat_add2_assoc: "[| a is_const; b is_const; c is_const |] ==>
1.32 + rat_add2_assoc: "[| a is_num; b is_num; c is_num |] ==>
1.33 a / c + (b + e) = (a + b * c) / c + e" and
1.34 - rat_add3: "[| a is_const; b is_const; c is_const |] ==>
1.35 + rat_add3: "[| a is_num; b is_num; c is_num |] ==>
1.36 a + b / c = (a * c + b) / c" and
1.37 - rat_add3_assoc: "[| a is_const; b is_const; c is_const |] ==>
1.38 + rat_add3_assoc: "[| a is_num; b is_num; c is_num |] ==>
1.39 a + (b / c + e) = (a * c + b) / c + e"
1.40
1.41 section \<open>Cancellation and addition of fractions\<close>
1.42 @@ -414,7 +414,9 @@
1.43 rules = [
1.44 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
1.45 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.46 - \<^rule_eval>\<open>is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.47 +(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
1.48 + \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
1.49 +( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
1.50 \<^rule_thm>\<open>not_true\<close>,
1.51 \<^rule_thm>\<open>not_false\<close>],
1.52 scr = Rule.Empty_Prog});
1.53 @@ -432,10 +434,10 @@
1.54
1.55 \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.56 \<^rule_thm>\<open>rat_add\<close>,
1.57 - (*"[| a is_const; b is_const; c is_const; d is_const |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.58 - \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
1.59 - \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.60 - \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c" *)
1.61 + (*"[| a is_num; b is_num; c is_num; d is_num |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.62 + \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a / c + b / c = (a + b) / c"*)
1.63 + \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_num; ?b is_num; ?c is_num |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.64 + \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a + b / c = (a * c) / c + b / c" *)
1.65
1.66 \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
1.67 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.68 @@ -626,6 +628,7 @@
1.69 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
1.70 scr = Rule.Empty_Prog});
1.71
1.72 +\<close> ML \<open>
1.73 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.74 val rat_mult_divide = prep_rls'(
1.75 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
1.76 @@ -643,6 +646,7 @@
1.77 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.78 scr = Rule.Empty_Prog});
1.79
1.80 +\<close> ML \<open>
1.81 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.82 val reduce_0_1_2 = prep_rls'(
1.83 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.84 @@ -664,15 +668,23 @@
1.85 \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
1.86 scr = Rule.Empty_Prog});
1.87
1.88 +\<close> ML \<open>
1.89 +\<close> ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
1.90 +ML \<open>
1.91 (*erls for calculate_Rational;
1.92 make local with FIXX@ME result:term *term list WN0609???SKMG*)
1.93 val norm_rat_erls = prep_rls'(
1.94 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.95 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.96 rules = [
1.97 - \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
1.98 + \<^rule_thm>\<open>refl\<close> (* ..DELETE, just to avoid ERROR fun #> not applicable to "[]"*)
1.99 +(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
1.100 + \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
1.101 +( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
1.102 +],
1.103 scr = Rule.Empty_Prog});
1.104
1.105 +\<close> ML \<open>
1.106 (* consists of rls containing the absolute minimum of thms *)
1.107 (*
1.108 which is now replaced by MGs version "norm_Rational" below
1.109 @@ -693,6 +705,7 @@
1.110 ],
1.111 scr = Rule.Empty_Prog});
1.112
1.113 +\<close> ML \<open>
1.114 val norm_Rational_parenthesized = prep_rls'(
1.115 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
1.116 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),