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

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 (*. uv polynomial division, result is (quotient, remainder) .*)
 (*. only for uv_mod_divides .*)
 (* FIXME: Division von x^9+x^5+1 durch x-1000 funktioniert nicht,
 integer zu klein  *)
 fun uv_mod_pdiv (p1:uv_poly) ([]:uv_poly) =
-raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
+error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
 | uv_mod_pdiv p1 [x] =
 let
 	val xs= Unsynchronized.ref  [];
 in
 	if x<>0 then
 	    (
 	     xs:=(uv_mod_rem_poly(p1,x));
 	     while length(!xs)>0 andalso hd(!xs)=0 do xs:=tl(!xs)
 	     )
-	else raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero");
+	else error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero");
 	([]:uv_poly,!xs:uv_poly)
 end
 | uv_mod_pdiv p1 p2 =
 let
 	val n= uv_mod_deg(p2);
 	val c= Unsynchronized.ref  0;
 	val output= Unsynchronized.ref  ([],[]);
 in
 	(
 	 if (!m)=0 orelse p2=[0]
-then raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: Division by zero")
+then error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: Division by zero")
 	 else
 	     (
 	      if (!m)<n then
 		  (
 		   output:=([0],p1)
 	val q= Unsynchronized.ref  [];
 	val c= Unsynchronized.ref  0;
 	val output= Unsynchronized.ref  ([],[]);
 in
 	(
-	 if (!m)=0 orelse p2=[0] then raise error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
+	 if (!m)=0 orelse p2=[0] then error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
 	 else
 	     (
 	      if (!m)<n then
 		  (
 		   output:=([0],p1)
 	     !output:uv_poly * uv_poly
 	 )
 end;
 (*. calculates the remainder of p1/p2 .*)
-fun uv_mod_prest (p1:uv_poly) ([]:uv_poly) = raise error("UV_MOD_PREST_EXCEPTION: Division by zero")
+fun uv_mod_prest (p1:uv_poly) ([]:uv_poly) = error("UV_MOD_PREST_EXCEPTION: Division by zero")
 | uv_mod_prest [] p2 = []:uv_poly
 | uv_mod_prest p1 p2 = (#2(uv_mod_pdiv p1 p2));
 (*. calculates the remainder of p1/p2 in Zp .*)
-fun uv_mod_prestp (p1:uv_poly) ([]:uv_poly) p= raise error("UV_MOD_PRESTP_EXCEPTION: Division by zero")
+fun uv_mod_prestp (p1:uv_poly) ([]:uv_poly) p= error("UV_MOD_PRESTP_EXCEPTION: Division by zero")
 | uv_mod_prestp [] p2 p= []:uv_poly
 | uv_mod_prestp p1 p2 p = #2(uv_mod_pdivp p1 p2 p);
 (*. calculates the content of a uv polynomial .*)
 fun uv_mod_cont ([]:uv_poly) = 0
 | uv_mod_cont (x::p)= gcd_int x (uv_mod_cont(p));
 (*. divides each coefficient of a uv polynomial by y .*)
-fun uv_mod_div_list (p:uv_poly,0) = raise error("UV_MOD_DIV_LIST_EXCEPTION: Division by zero")
+fun uv_mod_div_list (p:uv_poly,0) = error("UV_MOD_DIV_LIST_EXCEPTION: Division by zero")
 | uv_mod_div_list ([],y)   = []:uv_poly
 | uv_mod_div_list (x::p,y) = (x div y)::uv_mod_div_list(p,y);
 (*. calculates the primitiv part of a uv polynomial .*)
 fun uv_mod_pp ([]:uv_poly) = []:uv_poly
 	val c= Unsynchronized.ref  0;
 in
 	(
 	 c:=uv_mod_cont(p);
-	 if !c=0 then raise error ("RATIONALS_UV_MOD_PP_EXCEPTION: content is 0")
+	 if !c=0 then error ("RATIONALS_UV_MOD_PP_EXCEPTION: content is 0")
 	 else uv_mod_div_list(p,!c)
 	)
 end;
 (*. gets the leading coefficient of a uv polynomial .*)
 		 );
 	    !exit
 end;
 (*. decides if p1 is a factor of p2 in Zp .*)
-fun uv_mod_dividesp ([]:uv_poly) (p2:uv_poly) p= raise error("UV_MOD_DIVIDESP: Division by zero")
+fun uv_mod_dividesp ([]:uv_poly) (p2:uv_poly) p= error("UV_MOD_DIVIDESP: Division by zero")
 | uv_mod_dividesp p1 p2 p= if uv_mod_prestp p2 p1 p = [] then true else false;
 (*. decides if p1 is a factor of p2 .*)
-fun uv_mod_divides ([]:uv_poly) (p2:uv_poly) = raise error("UV_MOD_DIVIDES: Division by zero")
+fun uv_mod_divides ([]:uv_poly) (p2:uv_poly) = error("UV_MOD_DIVIDES: Division by zero")
 | uv_mod_divides p1 p2 = if uv_mod_prest p2 p1  = [] then true else false;
 (*. chinese remainder algorithm .*)
 fun uv_mod_cra2(r1,r2,m1,m2)=
 let
 	 )
 end;
 (*. applies the chinese remainder algorithmen to the coefficients of x1 and x2 .*)
 fun uv_mod_cra_2 ([],[],m1,m2) = []
-| uv_mod_cra_2 ([],x2,m1,m2) = raise error("UV_MOD_CRA_2_EXCEPTION: invalid call x1")
+| uv_mod_cra_2 ([],x2,m1,m2) = error("UV_MOD_CRA_2_EXCEPTION: invalid call x1")
-| uv_mod_cra_2 (x1,[],m1,m2) = raise error("UV_MOD_CRA_2_EXCEPTION: invalid call x2")
+| uv_mod_cra_2 (x1,[],m1,m2) = error("UV_MOD_CRA_2_EXCEPTION: invalid call x2")
 | uv_mod_cra_2 (x1::x1s,x2::x2s,m1,m2) = (uv_mod_cra2(x1,x2,m1,m2))::(uv_mod_cra_2(x1s,x2s,m1,m2));
 (*. calculates the gcd of two uv polynomials p1' and p2' with the modular algorithm .*)
 fun uv_mod_gcd (p1':uv_poly) (p2':uv_poly) =
 let
 (*. tests if the monomial M1 is greater as the monomial M2 and returns a boolean value .*)
 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)
 fun mv_monom_greater((M1x,M1l):mv_monom,(M2x,M2l):mv_monom,order)=
 if order=LEX_ then
 	(
-	 if length(M1l)<>length(M2l) then raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
+	 if length(M1l)<>length(M2l) then error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
 	 else if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true
 	     )
 else
 	if order=GGO_ then
 	    (
-	     if length(M1l)<>length(M2l) then raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
+	     if length(M1l)<>length(M2l) then error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
 	     else
 		 if mv_addlist(M1l)=mv_addlist(M2l)  then if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true
 		 else if mv_addlist(M1l)>mv_addlist(M2l) then true else false
 	     )
-	else raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Wrong Order");
+	else error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Wrong Order");
 (*. tests if the monomial X is greater as the monomial Y and returns a order value (GREATER,EQUAL,LESS) .*)
 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)
 fun mv_geq order ((x1,x):mv_monom,(x2,y):mv_monom) =
 let
 val temp= Unsynchronized.ref  EQUAL;
 in
 if order=LEX_ then
 	(
 	 if length(x)<>length(y) then
-	     raise error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
+	     error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
 	 else
 	     (
 	      temp:=mv_mg_hlp((map op- (x~~y)));
 	      if !temp=EQUAL then
 		  ( if x1=x2 then EQUAL
 	     )
 else
 	if order=GGO_ then
 	    (
 	     if length(x)<>length(y) then
-	      raise error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
+	      error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
 	     else
 		 if mv_addlist(x)=mv_addlist(y) then
 		     (mv_mg_hlp((map op- (x~~y))))
 		 else if mv_addlist(x)>mv_addlist(y) then GREATER else LESS
 		     )
-	else raise error ("RATIONALS_MV_GEQ_EXCEPTION: Wrong Order")
+	else error ("RATIONALS_MV_GEQ_EXCEPTION: Wrong Order")
 end;
 (*. cuts the first variable from a polynomial .*)
 fun mv_cut([]:mv_poly)=[]:mv_poly
-| mv_cut((x,[])::list) = raise error ("RATIONALS_MV_CUT_EXCEPTION: Invalid list ")
+| mv_cut((x,[])::list) = error ("RATIONALS_MV_CUT_EXCEPTION: Invalid list ")
 | mv_cut((x,y::ys)::list)=(x,ys)::mv_cut(list);
 (*. leading power product .*)
 fun mv_lpp([]:mv_poly,order)  = []
 | mv_lpp([(x,y)],order) = y
 	 while (length(!p1o)>0 andalso hd(#2(hd(!p1o)))=lp) do
 	     (
 	      lc:=hd(mv_cut([hd(!p1o)]))::(!lc);
 	      p1o:=tl(!p1o)
 	      );
-	 if !lc=[] then raise error ("RATIONALS_MV_LC_EXCEPTION: lc is empty") else ();
+	 if !lc=[] then error ("RATIONALS_MV_LC_EXCEPTION: lc is empty") else ();
 	 mv_rev_to(!lc)
 	 )
 end;
 (*. compares two powerproducts .*)
 fun mv_is_negativ([])=false
 | mv_is_negativ(x::xs)=if x<0 then true else mv_is_negativ(xs);
 (*. division of monomials .*)
 fun mv_mdiv((0,[]):mv_monom,_:mv_monom)=(0,[]):mv_monom
-| mv_mdiv(_,(0,[]))= raise error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
+| mv_mdiv(_,(0,[]))= error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
 | mv_mdiv(p1:mv_monom,p2:mv_monom)=
 let
 	val c= Unsynchronized.ref  (#1(p2));
 	val pp= Unsynchronized.ref  [];
 in
 	(
-	 if !c=0 then raise error("MV_MDIV_EXCEPTION Dividing by zero")
+	 if !c=0 then error("MV_MDIV_EXCEPTION Dividing by zero")
 	 else c:=(#1(p1) div #1(p2));
 	     if #1(p2)<>0 then
 		 (
 		  pp:=(#2(mv_mmul((1,#2(p1)),(1,(map mv_minus) (#2(p2))))));
 		  if mv_is_negativ(!pp) then (0,!pp)
 		  else (!c,!pp)
 		      )
-	     else raise error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
+	     else error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
 		 )
 end;
 (*. prints a polynom for (internal use only) .*)
 fun mv_print_poly([]:mv_poly)=tracing("[]\n")
 | mv_print_poly((x,y)::p1) = (tracing("("^Int.toString(x)^","^ints2str(y)^"),");mv_print_poly(p1));
 (*. division of two multivariate polynomials .*)
 fun mv_division([]:mv_poly,g:mv_poly,order)=([]:mv_poly,[]:mv_poly)
-| mv_division(f,[],order)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
+| mv_division(f,[],order)= error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
 | mv_division(f,g,order)=
 let
 	val r= Unsynchronized.ref  [];
 	val q= Unsynchronized.ref  [];
 	val g'= Unsynchronized.ref  ([] : mv_monom list);
 	val m= Unsynchronized.ref  (0,[0]);
 	val exit= Unsynchronized.ref  0;
 in
 	r := rev(sort (mv_geq order) (mv_shorten(f,order)));
 	g':= rev(sort (mv_geq order) (mv_shorten(g,order)));
-	if #1(hd(!g'))=0 then raise error("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero") else ();
+	if #1(hd(!g'))=0 then error("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero") else ();
 	if  (mv_monom_greater (hd(!g'),hd(!r),order)) then ([(0,mv_null2(#2(hd(f))))],(!r))
 	else
 	    (
 	     exit:=0;
 	     while (if (!exit)=0 then not(mv_monom_greater (hd(!g'),hd(!r),order)) else false) do
 		 (
 		  if (#1(mv_lm(!g',order)))<>0 then m:=mv_mdiv(mv_lm(!r,order),mv_lm(!g',order))
-		  else raise error ("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero");
+		  else error ("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero");
 		  if #1(!m)<>0 then
 		      (
 		       q:=(!m)::(!q);
 		       r:=mv_add((!r),mv_minus2(mv_mul(!g',[!m],order)),order)
 		       )
 | mv_correct((x,y)::list,v:int)=(x,v::y)::mv_correct(list,v);
 (*. multivariate case .*)
 (*. decides if x is a factor of y .*)
-fun mv_divides([]:mv_poly,[]:mv_poly)=  raise error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
+fun mv_divides([]:mv_poly,[]:mv_poly)=  error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
-| mv_divides(x,[]) =  raise error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
+| mv_divides(x,[]) =  error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
 | mv_divides(x:mv_poly,y:mv_poly) = #2(mv_division(y,x,LEX_))=[];
 (*. gets the maximum of a and b .*)
 fun mv_max(a,b) = if a>b then a else b;
 	val count= Unsynchronized.ref  0;
 	val max=mv_grad((c1,e1)::others);
 	val help= Unsynchronized.ref  ((c1,e1)::others);
 	val list= Unsynchronized.ref  [];
 in
-	if length(e1)>1 then raise error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
+	if length(e1)>1 then error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
 	else if length(e1)=0 then [c1]
 	     else
 		 (
 		  count:=0;
 		  while (!count)<=max do
 		    val pp= Unsynchronized.ref [];
 		in
 		    cont:=mv_content(p1);
 		    pp:=(#1(mv_division(p1,!cont,LEX_)));
 		    if !pp=[]
-			then raise error("RATIONALS_MV_PP_EXCEPTION: Invalid Content ")
+			then error("RATIONALS_MV_PP_EXCEPTION: Invalid Content ")
 		    else (!pp)
 		end
 (*. calculates the gcd of two multivariate polynomials with a modular approach .*)
 and mv_gcd ([]:mv_poly) ([]:mv_poly) :mv_poly= []:mv_poly
 		   vh:=tl(!vh);
 		   i:=(!i)+1
 		   );
 	      SOME [(1,rev(!vl))] handle _ => NONE
 	      )
-else raise error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
+else error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
 	 )
 end
 | term2coef' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option=
 (
 SOME ((the(term2coef' t1 v)) @ (the(term2coef' t2 v))) handle _ => NONE
 	 )
 | term2coef' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option=
 (
 SOME ((the(term2coef' t1 v)) @ mv_skalar_mul((the(term2coef' t2 v)),1)) handle _ => NONE
 	 )
-| term2coef' (term) v = raise error ("RATIONALS_TERM2COEF_EXCEPTION 2: Invalid term");
+| term2coef' (term) v = error ("RATIONALS_TERM2COEF_EXCEPTION 2: Invalid term");
 (*. checks if all coefficients of a polynomial are positiv (except the first) .*)
 fun check_coeff t = (* erste Koeffizient kann <0 sein !!! *)
 if count_neg(tl(the(term2coef' t (get_vars(t)))))=0 then true
 else false;
 		   vh:=tl(!vh);
 		   i:=(!i)+1
 		   );
 	      SOME [(1,rev(!vl))] handle _ => NONE
 	      )
-else raise error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
+else error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
 	 )
 end
 | term2poly' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option =
 (
 SOME ((the(term2poly' t1 v)) @ (the(term2poly' t2 v))) handle _ => NONE
 	 )
 | term2poly' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option =
 (
 SOME ((the(term2poly' t1 v)) @ mv_skalar_mul((the(term2poly' t2 v)),~1)) handle _ => NONE
 	 )
-| term2poly' (term) v = raise error ("RATIONALS_TERM2POLY_EXCEPTION 2: Invalid term");
+| term2poly' (term) v = error ("RATIONALS_TERM2POLY_EXCEPTION 2: Invalid term");
 (*. translates an Isabelle term into internal representation.
 term2poly
 fn : term ->              (*normalform [2]                    *)
 	 string list ->       (*for ...!!! BITTE DIE ERKLÄRUNG,
 	 mv_monom list        (*internal representation           *)
 		  option      (*the translation may fail with NONE*)
 .*)
 fun term2poly (t:term) v =
 if is_polynomial t then term2poly' t v
-else raise error ("term2poly: invalid = "^(term2str t));
+else error ("term2poly: invalid = "^(term2str t));
 (*. same as term2poly with automatic detection of the variables .*)
 fun term2polyx t = term2poly t (((map free2str) o vars) t);
 (*. checks if the term is in expanded polynomial form and converts it into the internal representation .*)
 fun expanded2poly (t:term) v =
 (*if is_expanded t then*) term2poly' t v
-(*else raise error ("RATIONALS_EXPANDED2POLY_EXCEPTION: Invalid Polynomial")*);
+(*else error ("RATIONALS_EXPANDED2POLY_EXCEPTION: Invalid Polynomial")*);
 (*. same as expanded2poly with automatic detection of the variables .*)
 fun expanded2polyx t = expanded2poly t (((map free2str) o vars) t);
 (*. converts a powerproduct into term representation .*)
 		)
 	       )
 	      )
 	     )
 end
-| step_cancel _ = raise error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
+| step_cancel _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
 (*. same as step_cancel, this time for expanded forms (input+output) .*)
 fun step_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
 let
 		)
 	       )
 	      )
 	     )
 end
-| step_cancel_expanded _ = raise error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
+| step_cancel_expanded _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
 fun direct_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
 let
 	val p1' = Unsynchronized.ref [];
 			    )
 		       )
 		  )
 	     )
 end
-| direct_cancel _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
+| direct_cancel _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
 (*. same es direct_cancel, this time for expanded forms (input+output).*)
 fun direct_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
 let
 	val p1' = Unsynchronized.ref [];
 			    )
 		       )
 		  )
 	     )
 end
-| direct_cancel_expanded _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
+| direct_cancel_expanded _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
 (*. adds two fractions .*)
 fun add_fract ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
 let
 	   poly2term((!den),vars)
 	   )
 	  )
 	 )
 end
-| add_fract (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
+| add_fract (_,_) = error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
 (*. adds two expanded fractions .*)
 fun add_fract_exp ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
 let
 	val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
 	   poly2expanded((!den),vars)
 	   )
 	  )
 	 )
 end
-| add_fract_exp (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXP_EXCEPTION: Invalid add_fraction call");
+| add_fract_exp (_,_) = error ("RATIONALS_ADD_FRACTION_EXP_EXCEPTION: Invalid add_fraction call");
 (*. adds a list of terms .*)
 fun add_list_of_fractions []= (Free("0",HOLogic.realT),[])
 | add_list_of_fractions [x]= direct_cancel x
 | add_list_of_fractions (x::y::xs) =
 	if rest=[] then
 	    (
 	     if last=[(1,mv_null2(vars))] then make_term(factor_list,vars)
 	     else make_term(last::factor_list,vars)
 	     )
-	else raise error ("RATIONALS_FACTORIZE_DEN_EXCEPTION: Invalid factor by division")
+	else error ("RATIONALS_FACTORIZE_DEN_EXCEPTION: Invalid factor by division")
 end;
 (*. 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)
 	if rest=[] then
 	    (
 	     if last=[(1,mv_null2(vars))] then make_exp(factor_list,vars)
 	     else make_exp(last::factor_list,vars)
 	     )
-	else raise error ("RATIONALS_FACTORIZE_DEN_EXP_EXCEPTION: Invalid factor by division")
+	else error ("RATIONALS_FACTORIZE_DEN_EXP_EXCEPTION: Invalid factor by division")
 end;
 (*. calculates the common denominator of all elements of the list and multiplies .*)
 (*. the nominators and denominators with the correct factor .*)
 (*. (polynomial representation) .*)
 fun step_add_list_of_fractions []=(Free("0",HOLogic.realT),[]:term list)
-| step_add_list_of_fractions [x]= raise error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXCEPTION: Nothing to add")
+| step_add_list_of_fractions [x]= error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXCEPTION: Nothing to add")
 | step_add_list_of_fractions (xs) =
 let
 val den_list=termlist2denominators (xs); (* list of denominators *)
 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)
 	val den=factorize_den(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)
 (*. calculates the common denominator of all elements of the list and multiplies .*)
 (*. the nominators and denominators with the correct factor .*)
 (*. (expanded polynomial representation) .*)
 fun step_add_list_of_fractions_exp []  = (Free("0",HOLogic.realT),[]:term list)
-| step_add_list_of_fractions_exp [x] = raise error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXP_EXCEPTION: Nothing to add")
+| step_add_list_of_fractions_exp [x] = error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXP_EXCEPTION: Nothing to add")
 | step_add_list_of_fractions_exp (xs)=
 let
 val den_list=termlist2denominators_exp (xs); (* list of denominators *)
 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)
 	val den=factorize_den_exp(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)
 [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) =
-raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
+error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
-| term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
+| term2list _ = error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
 (*.factors out the gcd of nominator and denominator:
 a/b = (a' * gcd)/(b' * gcd),  a,b,gcd  are poly[2].*)
 fun factout_p_  (thy:theory) t = SOME (step_cancel t,[]:term list);
 fun factout_ (thy:theory) t = SOME (step_cancel_expanded t,[]:term list);
 fun add_fraction_p_ (thy:theory) t =
 (tracing("### add_fraction_p_ called");
 (let val ts = term2list t
 in if 1 < length ts
 	then SOME (add_list_of_fractions ts)
-	else NONE (*raise error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)
+	else NONE (*error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)
 end) handle _ => NONE
 );
 (*.same as add_fraction_p_ but with normalform [3].*)
 (*SOME (step_add_list_of_fractions2(term2list(t))); *)
 fun add_fraction_ (thy:theory) t =
 if length(term2list(t))>1
 then SOME (add_list_of_fractions_exp(term2list(t))) handle _ => NONE
-else (*raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
+else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
 	NONE;
 fun add_fraction_ (thy:theory) t =
 (if 1 < length (term2list t)
 then SOME (add_list_of_fractions_exp (term2list t))
-else (*raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
+else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
 	 NONE) handle _ => NONE;
 (*SOME (step_add_list_of_fractions2_exp(term2list(t))); *)
 (*. brings the term into a normal form .*)
 	      | NONE => (tracing("### locate_rule:  rewrite "^
 				 (id_of_thm r)^" "^(term2str t)^" = NONE");
 			 []) end
 else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])
 | locate_rule _ _ _ _ _ _ =
-raise error ("locate_rule: doesnt match rev-sets in istate");
+error ("locate_rule: doesnt match rev-sets in istate");
 (*.next_rule = fn : rule list -> term -> rule option
 for a given term return the next rules to be done for cancelling.
 arguments:
 rule list     : the reverse rule list
 *)
 	   (_,r,_)::_ => SOME r
 	 | _ => NONE
 end
 | next_rule _ _ _ _ _ =
-raise error ("next_rule: doesnt match rev-sets in istate");
+error ("next_rule: doesnt match rev-sets in istate");
 (*.val attach_form = f : rule list -> term -> term
 			 -> (rule * (term * term list)) list
 checks an input term TI, if it may belong to a current cancellation, by
 trying to derive it from the given term TG.
 	      | NONE => (tracing("### locate_rule:  rewrite "^
 				 (id_of_thm r)^" "^(term2str t)^" = NONE");
 			 []) end
 else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])
 | locate_rule _ _ _ _ _ _ =
-raise error ("locate_rule: doesnt match rev-sets in istate");
+error ("locate_rule: doesnt match rev-sets in istate");
 fun next_rule thy eval_rls ro [rs] t =
 let val der = make_deriv thy eval_rls rs ro NONE t;
 in case der of
 (* val (_,r,_)::_ = der;
 *)
 	   (_,r,_)::_ => SOME r
 	 | _ => NONE
 end
 | next_rule _ _ _ _ _ =
-raise error ("next_rule: doesnt match rev-sets in istate");
+error ("next_rule: doesnt match rev-sets in istate");
 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
 []:(rule * (term * term list)) list;
 val pat = parse_patt thy "?r/?s";
 	      | NONE => (tracing("### locate_rule:  rewrite "^
 				 (id_of_thm r)^" "^(term2str t)^" = NONE");
 			 []) end
 else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])
 | locate_rule _ _ _ _ _ _ =
-raise error ("locate_rule: doesnt match rev-sets in istate");
+error ("locate_rule: doesnt match rev-sets in istate");
 (*.next_rule = fn : rule list -> term -> rule option
 for a given term return the next rules to be done for cancelling.
 arguments:
 rule list     : the reverse rule list
 *)
 	   (_,r,_)::_ => SOME r
 	 | _ => NONE
 end
 | next_rule _ _ _ _ _ =
-raise error ("next_rule: doesnt match rev-sets in istate");
+error ("next_rule: doesnt match rev-sets in istate");
 (*.val attach_form = f : rule list -> term -> term
 			 -> (rule * (term * term list)) list
 checks an input term TI, if it may belong to a current cancellation, by
 trying to derive it from the given term TG.
 	      | NONE => (tracing("### locate_rule:  rewrite "^
 				 (id_of_thm r)^" "^(term2str t)^" = NONE");
 			 []) end
 else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])
 | locate_rule _ _ _ _ _ _ =
-raise error ("locate_rule: doesnt match rev-sets in istate");
+error ("locate_rule: doesnt match rev-sets in istate");
 (*.next_rule = fn : rule list -> term -> rule option
 for a given term return the next rules to be done for cancelling.
 arguments:
 rule list     : the reverse rule list
 *)
 	   (_,r,_)::_ => SOME r
 	 | _ => NONE
 end
 | next_rule _ _ _ _ _ =
-raise error ("next_rule: doesnt match rev-sets in istate");
+error ("next_rule: doesnt match rev-sets in istate");
 (*.val attach_form = f : rule list -> term -> term
 			 -> (rule * (term * term list)) list
 checks an input term TI, if it may belong to a current cancellation, by
 trying to derive it from the given term TG.

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38015	67ba02dffacc
child 38034	928cebc9c4aa