wneuper/isa: comparison src/Tools/isac/Knowledge/Poly.thy

equal deleted inserted replaced

-:2b6e73df4e5d
+:d3a3cc2f0382
 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
 			    (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
 real_minus_binom_pow3_p: "(a + -1 * b) \<up> 3 = a \<up> 3 + -3*a \<up> 2*b + 3*a*b \<up> 2 +
 -1*b \<up> 3" and
-(* real_plus_binom_pow:        "[| n is_const;  3 < n |] ==>
+(* real_plus_binom_pow:        "[| n is_num;  3 < n |] ==>
 			       (a + b) \<up> n = (a + b) * (a + b)\<up>(n - 1)" *)
 real_plus_binom_pow4:   "(a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
 *(a + b)" and
 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
 			   (a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
 real_plus_minus_binom2_p:   "(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2" and
 real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2" and
 real_plus_binom_times1:     "(a +  1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2" and
 real_plus_binom_times2:     "(a + -1*b)*(a +  1*b) = a \<up> 2 + -1*b \<up> 2" and
-real_num_collect:           "[| l is_const; m is_const |] ==>
+real_num_collect:           "[| l is_num; m is_num |] ==>
 			      l * n + m * n = (l + m) * n" and
 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
 	by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
-real_num_collect_assoc:     "[| l is_const; m is_const |] ==>
+real_num_collect_assoc:     "[| l is_num; m is_num |] ==>
 			      l * n + (m * n + k) = (l + m) * n + k" and
-real_num_collect_assoc_l:   "[| l is_const; m is_const |] ==>
+real_num_collect_assoc_l:   "[| l is_num; m is_num |] ==>
 			      l * n + (m * n + k) = (l + m)
 				* n + k" and
-real_num_collect_assoc_r:   "[| l is_const; m is_const |] ==>
+real_num_collect_assoc_r:   "[| l is_num; m is_num |] ==>
 			      (k + m * n) + l * n = k + (l + m) * n" and
-real_one_collect:           "m is_const ==> n + m * n = (1 + m) * n" and
+real_one_collect:           "m is_num ==> n + m * n = (1 + m) * n" and
 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
 	by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
-real_one_collect_assoc:     "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
+real_one_collect_assoc:     "m is_num ==> n + (m * n + k) = (1 + m)* n + k" and
-real_one_collect_assoc_l:   "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
+real_one_collect_assoc_l:   "m is_num ==> n + (m * n + k) = (1 + m) * n + k" and
-real_one_collect_assoc_r:  "m is_const ==> (k + n) +  m * n = k + (1 + m) * n" and
+real_one_collect_assoc_r:  "m is_num ==> (k + n) +  m * n = k + (1 + m) * n" and
 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
 	by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
 real_mult_2_assoc:          "z1 + (z1 + k) = 2 * z1 + k" and
 real_mult_2_assoc_l:        "z1 + (z1 + k) = 2 * z1 + k" and
 rules = [
 \<^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"*)],
 scr = Rule.Empty_Prog};
+\<close> ML \<open>
+\<close> ML \<open>@{term "1 is_num"}\<close>
+ML \<open>
 (* erls for calculate_Rational + etc *)
 val powers_erls =
 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [
 val discard_minus =
 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [
 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
-\<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
+\<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)],
 	    scr = Rule.Empty_Prog};
 val expand_poly_ =
 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
 erls = Atools_erls, srls = Rule_Set.Empty,
 calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
 	      ], errpatts = [],
 rules = [
-\<^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\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
 	      \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,
-	        (*"[| l is_const; m is_const |] ==> (k + m * n) + l * n = k + (l + m)*n"*)
+	        (*"[| l is_num; m is_num |] ==> (k + m * n) + l * n = k + (l + m)*n"*)
-\<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
+\<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
-\<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
+\<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
 	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
 		       (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
 \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>, (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
 \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>, (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
 \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?z) = ?z"*),
 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
-\<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
+\<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)
 	       (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*) (*"- (?x + ?y) = - ?x + - ?y"*)
 	       (*\<^rule_thm>\<open>real_diff_plus\<close>*) (*"a - b = a + -b"*)],
 scr = Rule.Empty_Prog};
 calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
 	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
 	      ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))
 	      ], errpatts = [],
 rules =[
-\<^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\<close>, (*"[| l is_num; m is_num |]==>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"*)
+(*"[| l is_num; m is_num |] ==> 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\<close>,	 (*"m is_num ==> 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_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> 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};
 val reduce_012 =
 	     \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
 	     \<^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\<close>,  (*"[| l is_num; m is_num |]==>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_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> 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\<close>, (*"m is_num ==> 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_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
 	     \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
 	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
 	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
 	     \<^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\<close>, (*"[| l is_num; m is_num |] ==>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_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> 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\<close>, (*"m is_num ==> 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_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> 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.Prog (Program.prep_program @{thm expand_binoms_2.simps})};
 subsection \<open>add to Know_Store\<close>
 subsubsection \<open>rule-sets\<close>
 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
+ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
 rule_set_knowledge
-norm_Poly = \<open>prep_rls' norm_Poly\<close> and
+norm_Poly = \<open>prep_rls' norm_Poly\<close>
-Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) and
+(*/---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------\* )
+and
+Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*)
+( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
+and
 expand = \<open>prep_rls' expand\<close> and
 expand_poly = \<open>prep_rls' expand_poly\<close> and
 simplify_power = \<open>prep_rls' simplify_power\<close> and
 order_add_mult = \<open>prep_rls' order_add_mult\<close> and
 crls = Rule_Set.empty, errpats = [], nrls = norm_Poly}\<close>
 Program: simplify.simps
 Given: "Term t_t"
 Where: "t_t is_polyexp"
 Find: "normalform n_n"
 ML \<open>
 \<close> ML \<open>
 \<close>
 end

changeset 60385	d3a3cc2f0382
parent 60384	2b6e73df4e5d
child 60386	b7ea87559ad5