Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Rational.thy
branchisac-update-Isa09-2
changeset 37978 352b7044d4fb
parent 37972 66fc615a1e89
child 37979 4f11d7840684
equal deleted inserted replaced
37977:f93db2ec097a 37978:352b7044d4fb 
    15   is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp") 
    15   is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp") 
    16 
    16 
    17 axioms (*.not contained in Isabelle2002,
 
    17 axioms (*.not contained in Isabelle2002,
 
    18           stated as axioms, TODO?: prove as theorems*)
 
    18           stated as axioms, TODO?: prove as theorems*)
 
    19 
    19 
    20   mult_cross      "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)"
 
    20   mult_cross:      "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)"
 
    21   mult_cross1     "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)"
 
    21   mult_cross1:     "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)"
 
    22   mult_cross2     "           d ~= 0    ==> (a     = c / d) = (a * d =     c)"
 
    22   mult_cross2:     "           d ~= 0    ==> (a     = c / d) = (a * d =     c)"
 
    23                   
    23                   
    24   add_minus       "a + b - b = a"(*RL->Poly.thy*)
 
    24   add_minus:       "a + b - b = a"(*RL->Poly.thy*)
 
    25   add_minus1      "a - b + b = a"(*RL->Poly.thy*)
 
    25   add_minus1:      "a - b + b = a"(*RL->Poly.thy*)
 
    26                   
    26                   
    27   rat_mult        "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) 
    27   rat_mult:        "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) 
    28   rat_mult2       "a / b *  c      = a * c /  b     "(*?Isa02*)
 
    28   rat_mult2:       "a / b *  c      = a * c /  b     "(*?Isa02*)
 
    29 
    29 
    30   rat_mult_poly_l "c is_polyexp ==> c * (a / b) = c * a /  b"
 
    30   rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a /  b"
 
    31   rat_mult_poly_r "c is_polyexp ==> (a / b) * c = a * c /  b"
 
    31   rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c /  b"
 
    32 
    32 
    33 (*real_times_divide1_eq .. Isa02*) 
    33 (*real_times_divide1_eq .. Isa02*) 
    34   real_times_divide_1_eq  "-1    * (c / d) =-1 * c /      d "
 
    34   real_times_divide_1_eq:  "-1    * (c / d) =-1 * c /      d "
 
    35   real_times_divide_num   "a is_const ==> 
    35   real_times_divide_num:   "a is_const ==> 
    36 	          	   a     * (c / d) = a * c /      d "
 
    36 	          	   a     * (c / d) = a * c /      d "
 
    37 
    37 
    38   real_mult_div_cancel2   "k ~= 0 ==> m * k / (n * k) = m / n"
 
    38   real_mult_div_cancel2:   "k ~= 0 ==> m * k / (n * k) = m / n"
 
    39 (*real_mult_div_cancel1   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
 
    39 (*real_mult_div_cancel1:   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
 
    40 			  
    40 			  
    41   real_divide_divide1     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"
 
    41   real_divide_divide1:     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"
 
    42   real_divide_divide1_mg  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"
 
    42   real_divide_divide1_mg:  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"
 
    43 (*real_divide_divide2_eq  "x / y / z = x / (y * z)"..Isa02*)
 
    43 (*real_divide_divide2_eq:  "x / y / z = x / (y * z)"..Isa02*)
 
    44 			  
    44 			  
    45   rat_power               "(a / b)^^^n = (a^^^n) / (b^^^n)"
 
    45   rat_power:               "(a / b)^^^n = (a^^^n) / (b^^^n)"
 
    46 
    46 
    47 
    47 
    48   rat_add         "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    48   rat_add:         "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    49 	           a / c + b / d = (a * d + b * c) / (c * d)"
 
    49 	           a / c + b / d = (a * d + b * c) / (c * d)"
 
    50   rat_add_assoc   "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    50   rat_add_assoc:   "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    51 	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"
 
    51 	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"
 
    52   rat_add1        "[| a is_const; b is_const; c is_const |] ==> 
    52   rat_add1:        "[| a is_const; b is_const; c is_const |] ==> 
    53 	           a / c + b / c = (a + b) / c"
 
    53 	           a / c + b / c = (a + b) / c"
 
    54   rat_add1_assoc   "[| a is_const; b is_const; c is_const |] ==> 
    54   rat_add1_assoc:   "[| a is_const; b is_const; c is_const |] ==> 
    55 	           a / c + (b / c + e) = (a + b) / c + e"
 
    55 	           a / c + (b / c + e) = (a + b) / c + e"
 
    56   rat_add2        "[| a is_const; b is_const; c is_const |] ==> 
    56   rat_add2:        "[| a is_const; b is_const; c is_const |] ==> 
    57 	           a / c + b = (a + b * c) / c"
 
    57 	           a / c + b = (a + b * c) / c"
 
    58   rat_add2_assoc  "[| a is_const; b is_const; c is_const |] ==> 
    58   rat_add2_assoc:  "[| a is_const; b is_const; c is_const |] ==> 
    59 	           a / c + (b + e) = (a + b * c) / c + e"
 
    59 	           a / c + (b + e) = (a + b * c) / c + e"
 
    60   rat_add3        "[| a is_const; b is_const; c is_const |] ==> 
    60   rat_add3:        "[| a is_const; b is_const; c is_const |] ==> 
    61 	           a + b / c = (a * c + b) / c"
 
    61 	           a + b / c = (a * c + b) / c"
 
    62   rat_add3_assoc   "[| a is_const; b is_const; c is_const |] ==> 
    62   rat_add3_assoc:   "[| a is_const; b is_const; c is_const |] ==> 
    63 	           a + (b / c + e) = (a * c + b) / c + e"
 
    63 	           a + (b / c + e) = (a * c + b) / c + e"
 
    64 
    64 
    65 text {*calculate in rationals: gcd, lcm, etc.
 
    65 text {*calculate in rationals: gcd, lcm, etc.
 
    66       (c) Stefan Karnel 2002
 
    66       (c) Stefan Karnel 2002
 
    67       Institute for Mathematics D and Institute for Software Technology, 
    67       Institute for Mathematics D and Institute for Software Technology, 
    85     numerator and nominator in normalform [2] or [3].
 
    85     numerator and nominator in normalform [2] or [3].
 
    86 *}
 
    86 *}
 
    87 
    87 
    88 ML {*
 
    88 ML {*
 
    89 val thy = @{theory};
 
    89 val thy = @{theory};
 
       
    90 val ------------------------------------------------------+ = "11111";
 
    90 
    91 
    91 signature RATIONALI =
 
    92 signature RATIONALI =
 
    92 sig
 
    93 sig
 
    93   type mv_monom
 
    94   type mv_monom
 
    94   type mv_poly 
    95   type mv_poly 
   131   val rational_erls : 
   132   val rational_erls : 
   132       rls             (*.evaluates an arbitrary rational term with numerals.*)
 
   133       rls             (*.evaluates an arbitrary rational term with numerals.*)
 
   133 
   134 
   134 (*WN0210???SK: fehlen Funktionen, die exportiert werden sollen ? *)
 
   135 (*WN0210???SK: fehlen Funktionen, die exportiert werden sollen ? *)
 
   135 end
 
   136 end
 
       
   137 
       
   138 val ------------------------------------------------------++ = "22222";
 
   136 
   139 
   137 (*.**************************************************************************
 
   140 (*.**************************************************************************
 
   138 survey on the functions
 
   141 survey on the functions
 
   139 ~~~~~~~~~~~~~~~~~~~~~~~
 
   142 ~~~~~~~~~~~~~~~~~~~~~~~
 
   140  [2] 'polynomial'   :rls               | [3]'expanded_term':rls
 
   143  [2] 'polynomial'   :rls               | [3]'expanded_term':rls
 
   449 	 !g
 
   452 	 !g
 
   450 	 )
 
   453 	 )
 
   451     end;
 
   454     end;
 
   452 
   455 
   453 (*. calculates the minimum of two real values x and y .*)
 
   456 (*. calculates the minimum of two real values x and y .*)
 
   454 fun uv_mod_r_min(x,y):BasisLibrary.Real.real = if x>y then y else x;
 
   457 fun uv_mod_r_min(x,y):Real.real = if x>y then y else x;
 
   455 
   458 
   456 (*. calculates the minimum of two integer values x and y .*)
 
   459 (*. calculates the minimum of two integer values x and y .*)
 
   457 fun uv_mod_min(x,y) = if x>y then y else x;
 
   460 fun uv_mod_min(x,y) = if x>y then y else x;
 
   458 
   461 
   459 (*. adds the squared values of a integer list .*)
 
   462 (*. adds the squared values of a integer list .*)
 
   460 fun uv_mod_add_qu [] = 0.0 
   463 fun uv_mod_add_qu [] = 0.0 
   461   | uv_mod_add_qu (x::p) =  BasisLibrary.Real.fromInt(x)*BasisLibrary.Real.fromInt(x) + uv_mod_add_qu p;
 
   464   | uv_mod_add_qu (x::p) =  Real.fromInt(x)*Real.fromInt(x) + uv_mod_add_qu p;
 
   462 
   465 
   463 (*. calculates the euklidean norm .*)
 
   466 (*. calculates the euklidean norm .*)
 
   464 fun uv_mod_norm ([]:uv_poly) = 0.0
 
   467 fun uv_mod_norm ([]:uv_poly) = 0.0
 
   465   | uv_mod_norm p = Math.sqrt(uv_mod_add_qu(p));
 
   468   | uv_mod_norm p = Math.sqrt(uv_mod_add_qu(p));
 
   466 
   469 
   578 	 
   581 	 
   579 	d:=gcd_int (uv_mod_lc(!p1)) (uv_mod_lc(!p2));
 
   582 	d:=gcd_int (uv_mod_lc(!p1)) (uv_mod_lc(!p2));
 
   580 	g1:=uv_mod_lc(!p1)*uv_mod_lc(!p2);
 
   583 	g1:=uv_mod_lc(!p1)*uv_mod_lc(!p2);
 
   581 	p:=4;
 
   584 	p:=4;
 
   582 	
   585 	
   583 	m:=BasisLibrary.Real.ceil(2.0 *   
   586 	m:=Real.ceil(2.0 * Real.fromInt(!d) *
 
   584 				  BasisLibrary.Real.fromInt(!d) *
 
   587 	  Real.fromInt(power 2 (uv_mod_min(uv_mod_deg(!p2),uv_mod_deg(!p1)))) *
 
   585 				  BasisLibrary.Real.fromInt(power 2 (uv_mod_min(uv_mod_deg(!p2),uv_mod_deg(!p1)))) *  
   588 	  Real.fromInt(!d) * 
   586 				  BasisLibrary.Real.fromInt(!d) * 
   589 	  uv_mod_r_min(uv_mod_norm(!p1) / Real.fromInt(abs(uv_mod_lc(!p1))),
 
   587 				  uv_mod_r_min(uv_mod_norm(!p1) / BasisLibrary.Real.fromInt(abs(uv_mod_lc(!p1))),
 
   590 	  uv_mod_norm(!p2) / Real.fromInt(abs(uv_mod_lc(!p2))))); 
   588 					uv_mod_norm(!p2) / BasisLibrary.Real.fromInt(abs(uv_mod_lc(!p2))))); 
       
   589 
   591 
   590 	while (!exit=0) do  
   592 	while (!exit=0) do  
   591 	    (
 
   593 	    (
 
   592 	     p:=uv_mod_nextprime(!d,!p);
 
   594 	     p:=uv_mod_nextprime(!d,!p);
 
   593 	     cp:=(uv_mod_gcd_modp (uv_mod_list_modp(!p1) (!p)) (uv_mod_list_modp(!p2) (!p)) (!p)) ;
 
   595 	     cp:=(uv_mod_gcd_modp (uv_mod_list_modp(!p1) (!p)) (uv_mod_list_modp(!p2) (!p)) (!p)) ;
 
   867 	     else raise error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
 
   869 	     else raise error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
 
   868 		 )
 
   870 		 )
 
   869     end;
 
   871     end;
 
   870 
   872 
   871 (*. prints a polynom for (internal use only) .*)
 
   873 (*. prints a polynom for (internal use only) .*)
 
   872 fun mv_print_poly([]:mv_poly)=print("[]\n")
 
   874 fun mv_print_poly([]:mv_poly)=writeln("[]\n")
 
   873   | mv_print_poly((x,y)::[])= print("("^BasisLibrary.Int.toString(x)^","^ints2str(y)^")\n")
 
   875   | mv_print_poly((x,y)::[])= writeln("("^Int.toString(x)^","^ints2str(y)^")\n")
 
   874   | mv_print_poly((x,y)::p1) = (print("("^BasisLibrary.Int.toString(x)^","^ints2str(y)^"),");mv_print_poly(p1));
 
   876   | mv_print_poly((x,y)::p1) = (writeln("("^Int.toString(x)^","^ints2str(y)^"),");mv_print_poly(p1));
 
   875 
   877 
   876 
   878 
   877 (*. division of two multivariate polynomials .*) 
   879 (*. division of two multivariate polynomials .*) 
   878 fun mv_division([]:mv_poly,g:mv_poly,order)=([]:mv_poly,[]:mv_poly)
 
   880 fun mv_division([]:mv_poly,g:mv_poly,order)=([]:mv_poly,[]:mv_poly)
 
   879   | mv_division(f,[],order)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
 
   881   | mv_division(f,[],order)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
 
  2764   Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
  2766   Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
  2765 	 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *)
 
  2767 	 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *)
 
  2766 	 rules = 
  2768 	 rules = 
  2767 	 [Calc ("op =",eval_equal "#equal_"),
 
  2769 	 [Calc ("op =",eval_equal "#equal_"),
 
  2768 	  Calc ("Atools.is'_const",eval_const "#is_const_"),
 
  2770 	  Calc ("Atools.is'_const",eval_const "#is_const_"),
 
  2769 	  Thm ("not_true",num_str @{not_true),
 
  2771 	  Thm ("not_true",num_str @{thm not_true}),
 
  2770 	  Thm ("not_false",num_str @{not_false)
 
  2772 	  Thm ("not_false",num_str @{thm not_false})
 
  2771 	  ], 
  2773 	  ], 
  2772 	 scr = EmptyScr});
 
  2774 	 scr = EmptyScr});
 
  2773 
  2775 
  2774 
  2776 
  2775 (*.simplifies expressions with numerals;
 
  2777 (*.simplifies expressions with numerals;
 
  2782 	      calc = [], 
  2784 	      calc = [], 
  2783 	      rules = 
  2785 	      rules = 
  2784 	      [Calc ("HOL.divide"  ,eval_cancel "#divide_"),
 
  2786 	      [Calc ("HOL.divide"  ,eval_cancel "#divide_"),
 
  2785 	       
  2787 	       
  2786 	       Thm ("minus_divide_left",
 
  2788 	       Thm ("minus_divide_left",
 
  2787 		    num_str (@{thm real_minus_divide_eq} RS @{thm sym})),
 
  2789 		    num_str (@{thm minus_divide_left} RS @{thm sym})),
 
  2788 	       (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)
 
  2790 	       (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)
 
  2789 	       
  2791 	       
  2790 	       Thm ("rat_add",num_str @{thm rat_add}),
 
  2792 	       Thm ("rat_add",num_str @{thm rat_add}),
 
  2791 	       (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
 
  2793 	       (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
 
  2792 		 \"a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
 
  2794 		 \"a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
 
  2822 	       (*"   b ~= 0            ==> (a / b = c    ) = (a     = b * c)*)
 
  2824 	       (*"   b ~= 0            ==> (a / b = c    ) = (a     = b * c)*)
 
  2823 	       Thm ("mult_cross2",num_str @{thm mult_cross2})
 
  2825 	       Thm ("mult_cross2",num_str @{thm mult_cross2})
 
  2824 	       (*"           d ~= 0    ==> (a     = c / d) = (a * d =     c)*)
 
  2826 	       (*"           d ~= 0    ==> (a     = c / d) = (a * d =     c)*)
 
  2825 	       ], scr = EmptyScr})
 
  2827 	       ], scr = EmptyScr})
 
  2826 	calculate_Poly);
 
  2828 	calculate_Poly);
 
       
  2829 val ------------------------------------------------------+++ = "33333";
 
  2827 
  2830 
  2828 
  2831 
  2829 (*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
 
  2832 (*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
 
  2830 fun eval_is_expanded (thmid:string) _ 
  2833 fun eval_is_expanded (thmid:string) _ 
  2831 		       (t as (Const("Rational.is'_expanded", _) $ arg)) thy = 
  2834 		       (t as (Const("Rational.is'_expanded", _) $ arg)) thy = 
  2843 	      (append_rls "is_expanded" Atools_erls 
  2846 	      (append_rls "is_expanded" Atools_erls 
  2844 			  [Calc ("Rational.is'_expanded", eval_is_expanded "")
 
  2847 			  [Calc ("Rational.is'_expanded", eval_is_expanded "")
 
  2845 			   ]);
 
  2848 			   ]);
 
  2846 
  2849 
  2847 
  2850 
  2848 
       
  2849 (*.3 'reverse-rewrite-sets' for symbolic computation on rationals:
 
  2851 (*.3 'reverse-rewrite-sets' for symbolic computation on rationals:
 
  2850  =================================================================
 
  2852  =================================================================
 
  2851  A[2] 'cancel_p': .
 
  2853  A[2] 'cancel_p': .
 
  2852  A[3] 'cancel': .
 
  2854  A[3] 'cancel': .
 
  2853  B[2] 'common_nominator_p': transforms summands in a term [2]
 
  2855  B[2] 'common_nominator_p': transforms summands in a term [2]
 
  2862 The signature of these functions are the same in each 'reverse-rewrite-set' 
  2864 The signature of these functions are the same in each 'reverse-rewrite-set' 
  2863 respectively.*)
 
  2865 respectively.*)
 
  2864 
  2866 
  2865 (* ************************************************************************* *)
 
  2867 (* ************************************************************************* *)
 
  2866 
  2868 
       
  2869 val ------------------------------------------------------++++ = "44444";
 
  2867 
  2870 
  2868 local(*. cancel_p
 
  2871 local(*. cancel_p
 
  2869 ------------------------
 
  2872 ------------------------
 
  2870 cancels a single fraction consisting of two (uni- or multivariate)
 
  2873 cancels a single fraction consisting of two (uni- or multivariate)
 
  2871 polynomials WN0609???SK[2] into another such a fraction; examples:
 
  2874 polynomials WN0609???SK[2] into another such a fraction; examples:
 
  3015 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3018 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3016 		     next_rule   = next_rule thy Atools_erls ro,
 
  3019 		     next_rule   = next_rule thy Atools_erls ro,
 
  3017 		     attach_form = attach_form}}
 
  3020 		     attach_form = attach_form}}
 
  3018 end;(*local*)
 
  3021 end;(*local*)
 
  3019 
  3022 
       
  3023 val ------------------------------------------------------+++++ = "55555";
 
  3020 
  3024 
  3021 local(*.ad (1) 'cancel'
 
  3025 local(*.ad (1) 'cancel'
 
  3022 ------------------------------
 
  3026 ------------------------------
 
  3023 cancels a single fraction consisting of two (uni- or multivariate)
 
  3027 cancels a single fraction consisting of two (uni- or multivariate)
 
  3024 polynomials WN0609???SK[3] into another such a fraction; examples:
 
  3028 polynomials WN0609???SK[3] into another such a fraction; examples:
 
  3097 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3101 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3098 		     next_rule   = next_rule thy Atools_erls ro,
 
  3102 		     next_rule   = next_rule thy Atools_erls ro,
 
  3099 		     attach_form = attach_form}}
 
  3103 		     attach_form = attach_form}}
 
  3100 end;(*local*)
 
  3104 end;(*local*)
 
  3101 
  3105 
       
  3106 val ------------------------------------------------------+++++-+ = "66666";
 
  3102 
  3107 
  3103 
  3108 
  3104 local(*.ad [2] 'common_nominator_p'
 
  3109 local(*.ad [2] 'common_nominator_p'
 
  3105 ---------------------------------
 
  3110 ---------------------------------
 
  3106 FIXME Beschreibung .*)
 
  3111 FIXME Beschreibung .*)
 
  3251 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3256 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3252 		     next_rule   = next_rule thy Atools_erls ro,
 
  3257 		     next_rule   = next_rule thy Atools_erls ro,
 
  3253 		     attach_form = attach_form}}
 
  3258 		     attach_form = attach_form}}
 
  3254 end;(*local*)
 
  3259 end;(*local*)
 
  3255 
  3260 
       
  3261 val ------------------------------------------------------+++++-++ = "77777";
 
  3256 
  3262 
  3257 local(*.ad [2] 'common_nominator'
 
  3263 local(*.ad [2] 'common_nominator'
 
  3258 ---------------------------------
 
  3264 ---------------------------------
 
  3259 FIXME Beschreibung .*)
 
  3265 FIXME Beschreibung .*)
 
  3260 
  3266 
  3267 (*.common_nominator_ = fn : theory -> term -> (term * term list) option
 
  3273 (*.common_nominator_ = fn : theory -> term -> (term * term list) option
 
  3268   as defined above*)
 
  3274   as defined above*)
 
  3269 
  3275 
  3270 (*.init_state = fn : term -> istate
 
  3276 (*.init_state = fn : term -> istate
 
  3271 initialzies the state of the interactive interpreter. The state is:
 
  3277 initialzies the state of the interactive interpreter. The state is:
 
       
  3278 
       
  3279 val ------------------------------------------------------+++++-++++ = "99999";
 
       
  3280 val ------------------------------------------------------+++++-+++++ = "00000";
 
  3272 
  3281 
  3273 type rrlsstate =      (*state for reverse rewriting*)
 
  3282 type rrlsstate =      (*state for reverse rewriting*)
 
  3274      (term *          (*the current formula*)
 
  3283      (term *          (*the current formula*)
 
  3275       term *          (*the final term*)
 
  3284       term *          (*the final term*)
 
  3276       rule list       (*'reverse rule list' (#)*)
 
  3285       rule list       (*'reverse rule list' (#)*)
 
  3291         val rs = (distinct_Thm o (map #1)) der;
 
  3300         val rs = (distinct_Thm o (map #1)) der;
 
  3292 	val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
 
  3301 	val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
 
  3293 				      "sym_real_mult_0",
 
  3302 				      "sym_real_mult_0",
 
  3294 				      "sym_real_mult_1"]) rs;
 
  3303 				      "sym_real_mult_1"]) rs;
 
  3295     in (t,t'',[rs(*here only _ONE_*)],der) end;
 
  3304     in (t,t'',[rs(*here only _ONE_*)],der) end;
 
  3296 
       
  3297 (* use"knowledge/Rational.ML";
 
       
  3298    *)
 
       
  3299 
  3305 
  3300 (*.locate_rule = fn : rule list -> term -> rule
 
  3306 (*.locate_rule = fn : rule list -> term -> rule
 
  3301 		      -> (rule * (term * term list) option) list.
 
  3307 		      -> (rule * (term * term list) option) list.
 
  3302   checks a rule R for being a cancel-rule, and if it is,
 
  3308   checks a rule R for being a cancel-rule, and if it is,
 
  3303   then return the list of rules (+ the terms they are rewriting to)
 
  3309   then return the list of rules (+ the terms they are rewriting to)
 
  3405 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3411 		     locate_rule = locate_rule thy Atools_erls ro,
 
  3406 		     next_rule   = next_rule thy Atools_erls ro,
 
  3412 		     next_rule   = next_rule thy Atools_erls ro,
 
  3407 		     attach_form = attach_form}}
 
  3413 		     attach_form = attach_form}}
 
  3408 
  3414 
  3409 end;(*local*)
 
  3415 end;(*local*)
 
  3410 
       
  3411 
       
  3412 (*##*)
 
       
  3413 end;(*struct*)
 
  3416 end;(*struct*)
 
       
  3417 
       
  3418 val ------------------------------------------------------+++++-+++ = "88888";
 
  3414 
  3419 
  3415 open RationalI;
 
  3420 open RationalI;
 
  3416 (*##*)
 
  3421 (*##*)
 
  3417 
  3422 
  3418 (*.the expression contains + - * ^ / only ?.*)
 
  3423 (*.the expression contains + - * ^ / only ?.*)
 
  3617 val simplify_rational = 
  3622 val simplify_rational = 
  3618     merge_rls "simplify_rational" expand_binoms
 
  3623     merge_rls "simplify_rational" expand_binoms
 
  3619     (append_rls "divide" calculate_Rational
 
  3624     (append_rls "divide" calculate_Rational
 
  3620 		[Thm ("divide_1",num_str @{thm divide_1}),
 
  3625 		[Thm ("divide_1",num_str @{thm divide_1}),
 
  3621 		 (*"?x / 1 = ?x"*)
 
  3626 		 (*"?x / 1 = ?x"*)
 
  3622 		 Thm ("rat_mult",num_str @{thm rat_mult),
 
  3627 		 Thm ("rat_mult",num_str @{thm rat_mult}),
 
  3623 		 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
 
  3628 		 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
 
  3624 		 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
 
  3629 		 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
 
  3625 		 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
 
  3630 		 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
 
  3626 		 otherwise inv.to a / b / c = ...*)
 
  3631 		 otherwise inv.to a / b / c = ...*)
 
  3627 		 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
 
  3632 		 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
 
  3628 		 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
 
  3633 		 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
 
  3629 		 Thm ("add_minus",num_str @{thm add_minus}),
 
  3634 		 Thm ("add_minus",num_str @{thm add_minus}),
 
  3630 		 (*"?a + ?b - ?b = ?a"*)
 
  3635 		 (*"?a + ?b - ?b = ?a"*)
 
  3631 		 Thm ("add_minus1",num_str @{thm add_minus1}),
 
  3636 		 Thm ("add_minus1",num_str @{thm add_minus1}),
 
  3632 		 (*"?a - ?b + ?b = ?a"*)
 
  3637 		 (*"?a - ?b + ?b = ?a"*)
 
  3633 		 Thm ("real_divide_minus1",num_str @{thm real_divide_minus1})
 
  3638 		 Thm ("divide_minus1",num_str @{thm divide_minus1})
 
  3634 		 (*"?x / -1 = - ?x"*)
 
  3639 		 (*"?x / -1 = - ?x"*)
 
  3635 (*
 
  3640 (*
 
  3636 ,
 
  3641 ,
 
  3637 		 Thm ("",num_str @{thm })
 
  3642 		 Thm ("",num_str @{thm })
 
  3638 *)
 
  3643 *)
wneuper/isa