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

equal deleted inserted replaced

-:491b133d154a
+:928cebc9c4aa
 (*. help function for is_polynomial
 checks the order of the operators .*)
 fun test_polynomial (Const ("uminus",_) $ Free (str,_)) _ = true (*WN.13.3.03*)
 | test_polynomial (t as Free(str,_)) v = true
-| test_polynomial (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
+| test_polynomial (t as Const ("Groups.times_class.times",_) $ t1 $ t2) v = if v="^" then false
 						     else (test_polynomial t1 "*") andalso (test_polynomial t2 "*")
 | test_polynomial (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
 							  else (test_polynomial t1 " ") andalso (test_polynomial t2 " ")
 | test_polynomial (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_polynomial t1 "^") andalso (test_polynomial t2 "^")
 | test_polynomial _ v = false;
 fun is_polynomial t = test_polynomial t " ";
 (*. help function for is_expanded
 checks the order of the operators .*)
 fun test_exp (t as Free(str,_)) v = true
-| test_exp (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
+| test_exp (t as Const ("Groups.times_class.times",_) $ t1 $ t2) v = if v="^" then false
 						     else (test_exp t1 "*") andalso (test_exp t2 "*")
 | test_exp (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
 							  else (test_exp t1 " ") andalso (test_exp t2 " ")
 | test_exp (t as Const ("Groups.minus_class.minus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
 							  else (test_exp t1 " ") andalso (test_exp t2 " ")
 		      i:=(!i)+1
 		      );
 		 SOME [(1,rev(!vl))] handle _ => NONE
 	    )
 end
-| term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
+| term2coef' (Const ("Groups.times_class.times",_) $ t1 $ t2) v :mv_poly option=
 let
 	val t1pp= Unsynchronized.ref  [];
 	val t2pp= Unsynchronized.ref  [];
 	val t1c= Unsynchronized.ref  0;
 	val t2c= Unsynchronized.ref  0;
 		      i:=(!i)+1
 		      );
 		 SOME [(1,rev(!vl))] handle _ => NONE
 	    )
 end
-| term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
+| term2poly' (Const ("Groups.times_class.times",_) $ t1 $ t2) v :mv_poly option=
 let
 	val t1pp= Unsynchronized.ref  [];
 	val t2pp= Unsynchronized.ref  [];
 	val t1c= Unsynchronized.ref  0;
 	val t2c= Unsynchronized.ref  0;
 	      )
 	 else
 	     (
 	      if hd(!xss)=1 then
 		  (
-		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   Free(hd(!vv), HOLogic.realT) $
 		   powerproduct2term(tl(!xss),tl(!vv))
 		   )
 	      else
 		  (
-		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   (
 		    Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		    Free(hd(!vv), HOLogic.realT) $  Free(str_of_int (hd(!xss)),HOLogic.realT)
 		    ) $
 		    powerproduct2term(tl(!xss),tl(!vv))
 		  (
 		   powerproduct2term(e,v)
 		   )
 	      else
 		  (
-		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   Free(str_of_int c,HOLogic.realT)  $
 		   powerproduct2term(e,v)
 		   )
 		  )
 	     );*)
 	then Free (str_of_int i, HOLogic.realT)
 	else Const ("uminus", HOLogic.realT --> HOLogic.realT) $
 		   Free ((str_of_int o abs) i, HOLogic.realT)
 else
 	if i > 0
-	then Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
+	then Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
 		   (Free (str_of_int i, HOLogic.realT)) $
 		   powerproduct2term(is, v)
-	else Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
+	else Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
 		   (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
 		   Free ((str_of_int o abs) i, HOLogic.realT)) $
 		   powerproduct2term(is, vs);---------------------------*)
 fun monom2term ((i, is) : mv_monom, vs) =
 if list_is_null is
 then Free (str_of_int i, HOLogic.realT)
 else if i = 1
 then powerproduct2term (is, vs)
-else Const ("op *", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
+else Const ("Groups.times_class.times", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
 	       (Free (str_of_int i, HOLogic.realT)) $
 	       powerproduct2term (is, vs);
 (*. converts the internal polynomial representation into an Isabelle term.*)
 fun poly2term' ([] : mv_poly, vs) = Free(str_of_int 0, HOLogic.realT)
 		  (
 		   powerproduct2term(e,v)
 		   )
 	      else
 		  (
-		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   Free(str_of_int (abs(c)),HOLogic.realT)  $
 		   powerproduct2term(e,v)
 		   )
 		  )
 	     );
 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
 	      (
 	       Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 	       $
 	       (
-		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		poly2term(!p1',vars) $
 		poly2term(!p3,vars)
 		)
 	       $
 	       (
-		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		poly2term(!p2',vars) $
 		poly2term(!p3,vars)
 		)
 	       )
 	      else
 	       p3:=mv_skalar_mul(!p3,~1);
 	       (
 		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		$
 		(
-		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		 poly2term(!p1',vars) $
 		 poly2term(!p3,vars)
 		 )
 		$
 		(
-		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		 poly2term(!p2',vars) $
 		 poly2term(!p3,vars)
 		 )
 		)
 	       )
 	      if #1(hd(sort (mv_geq LEX_) (!p2')))(* mv_lc2(!p2',LEX_)*)>0 then
 	      (
 	       Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 	       $
 	       (
-		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		poly2expanded(!p1',vars) $
 		poly2expanded(!p3,vars)
 		)
 	       $
 	       (
-		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		poly2expanded(!p2',vars) $
 		poly2expanded(!p3,vars)
 		)
 	       )
 	      else
 	       p3:=mv_skalar_mul(!p3,~1);
 	       (
 		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		$
 		(
-		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		 poly2expanded(!p1',vars) $
 		 poly2expanded(!p3,vars)
 		 )
 		$
 		(
-		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		 poly2expanded(!p2',vars) $
 		 poly2expanded(!p3,vars)
 		 )
 		)
 	       )
 		 $
 		 (
 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		  $
 		  (
-		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   poly2term(the (term2poly p1' p1var),p1var) $
 		   poly2term(p3,var)
 		   )
 		  $
 		  (
 	     else
 		 (
 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		  $
 		  (
-		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   poly2term(the (term2poly p1' p1var),p1var) $
 		   poly2term(p3,var)
 		   )
 		  $
 		  den
 		 $
 		 (
 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		  $
 		  (
-		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $
 		   poly2expanded(p3,var)
 		   )
 		  $
 		  (
 	     else
 		 (
 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		  $
 		  (
-		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+		   Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $
 		   poly2expanded(p3,var)
 		   )
 		  $
 		  den
 (*. makes a term out of the elements of the list (polynomial representation) .*)
 fun make_term ([],vars) = Free(str_of_int 0,HOLogic.realT)
 | make_term ((x::xs),vars) = if length(xs)=0 then poly2term(sort (mv_geq LEX_) (x),vars)
 			       else
 				   (
-				    Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+				    Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 				    poly2term(sort (mv_geq LEX_) (x),vars) $
 				    make_term(xs,vars)
 				    );
 (*. factorizes the denominator (polynomial representation) .*)
 (*. makes a term out of the elements of the list (expanded polynomial representation) .*)
 fun make_exp ([],vars) = Free(str_of_int 0,HOLogic.realT)
 | make_exp ((x::xs),vars) = if length(xs)=0 then poly2expanded(sort (mv_geq LEX_) (x),vars)
 			       else
 				   (
-				    Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+				    Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 				    poly2expanded(sort (mv_geq LEX_) (x),vars) $
 				    make_exp(xs,vars)
 				    );
 (*. factorizes the denominator (expanded polynomial representation) .*)
 ]
 | term2list (t as (Free(_,_))) =
 [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 	  t $  Free("1",HOLogic.realT)
 ]
-| term2list (t as (Const("op *",_) $ _ $ _)) =
+| term2list (t as (Const("Groups.times_class.times",_) $ _ $ _)) =
 [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 	  t $ Free("1",HOLogic.realT)
 ]
 | term2list (Const("Groups.plus_class.plus",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
 | term2list (Const("Groups.minus_class.minus",_) $ t1 $ t2) =
 Rrls {id = "cancel_p", prepat=[],
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
-		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
+		  ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  (*asm_thm=[("real_mult_div_cancel2","")],*)
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
 		     normal_form = cancel_p_ thy,
 Rrls {id = "cancel", prepat=prepat,
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
-		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
+		  ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
 		     normal_form = cancel_ thy,
 		     locate_rule = locate_rule thy Atools_erls ro,
 Rrls {id = "common_nominator_p", prepat=prepat,
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
-		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
+		  ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
 		     normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)
 		     locate_rule = locate_rule thy Atools_erls ro,
 Rrls {id = "common_nominator", prepat=prepat,
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
-		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
+		  ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  (*asm_thm=[("real_mult_div_cancel2","")],*)
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
 		     normal_form = add_fraction_ (*NOT common_nominator_*) thy,
 (*.the expression contains + - * ^ / only ?.*)
 fun is_ratpolyexp (Free _) = true
 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
-| is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true
+| is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
 | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
 | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true
 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
-| is_ratpolyexp (Const ("op *",_) $ t1 $ t2) =
+| is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
 | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =
 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
 | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) =
 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

branch	isac-update-Isa09-2
changeset 38034	928cebc9c4aa
parent 38031	460c24a6a6ba
child 38036	02a9b2540eb7