wneuper/isa: comparison src/Tools/isac/IsacKnowledge/Poly.ML

equal deleted inserted replaced

-:d957275620d4
+:e6fc98fbcb85
 	finddivide t v
 end;
 fun eval_is_polyrat_in _ _ (p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _  =
 if is_polyrat_in t v then
-	Some ((term2str p) ^ " = True",
+	SOME ((term2str p) ^ " = True",
 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
-else Some ((term2str p) ^ " = True",
+else SOME ((term2str p) ^ " = True",
 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
-| eval_is_polyrat_in _ _ _ _ = ((*writeln"### nichts matcht";*) None);
+| eval_is_polyrat_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
 local
 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
 fun coeff_in c v = not (v mem (vars c));
 if (1) then degree 0
 if (2) then v is a factor on the very right, ev. with exponent.*)
 fun factor_right_deg (*case 2*)
 	    (t as Const ("op *",_) $ t1 $
 	       (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
-	if ((vv = v) andalso (coeff_in t1 v)) then Some (int_of_str' d) else None
+	if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
 | factor_right_deg
 	    (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
-	if (vv = v) then Some (int_of_str' d) else None
+	if (vv = v) then SOME (int_of_str' d) else NONE
 | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v =
-	if ((vv = v) andalso (coeff_in t1 v))then Some 1 else None
+	if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
 | factor_right_deg vv v =
-	if (vv = v) then Some 1 else None;
+	if (vv = v) then SOME 1 else NONE;
 fun mono_deg_in m v =
-	if coeff_in m v then (*case 1*) Some 0
+	if coeff_in m v then (*case 1*) SOME 0
 	else factor_right_deg m v;
 (*
 val v = (term_of o the o (parse thy)) "x";
 val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";
 mono_deg_in t v;
-(*val it = Some 7*)
+(*val it = SOME 7*)
 val t = (term_of o the o (parse thy)) "x^^^7";
 mono_deg_in t v;
-(*val it = Some 7*)
+(*val it = SOME 7*)
 val t = (term_of o the o (parse thy)) "(a*b+c)*x";
 mono_deg_in t v;
-(*val it = Some 1*)
+(*val it = SOME 1*)
 val t = (term_of o the o (parse thy)) "(a*b+x)*x";
 mono_deg_in t v;
-(*val it = None*)
+(*val it = NONE*)
 val t = (term_of o the o (parse thy)) "x";
 mono_deg_in t v;
-(*val it = Some 1*)
+(*val it = SOME 1*)
 val t = (term_of o the o (parse thy)) "(a*b+c)";
 mono_deg_in t v;
-(*val it = Some 0*)
+(*val it = SOME 0*)
 val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
 mono_deg_in t v;
-(*val it = None*)
+(*val it = NONE*)
 *)
 fun expand_deg_in t v =
 	let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
 		(case mono_deg_in t2 v of (* $ is left associative*)
-		     Some d' => edi d' d' t1
+		     SOME d' => edi d' d' t1
-		   | None => None)
+		   | NONE => NONE)
 	      | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
 		(case mono_deg_in t2 v of
-		     Some d' => edi d' d' t1
+		     SOME d' => edi d' d' t1
-		   | None => None)
+		   | NONE => NONE)
 	      | edi d dmax (Const ("op -",_) $ t1 $ t2) =
 		(case mono_deg_in t2 v of
 		     (*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4  +x*)
-		     Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
+		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else NONE
-		   | None => None)
+		   | NONE => NONE)
 	      | edi d dmax (Const ("op +",_) $ t1 $ t2) =
 		(case mono_deg_in t2 v of
 		     (*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4  +x*)
-		     Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
+		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else NONE
-		   | None => None)
+		   | NONE => NONE)
 	      | edi ~1 ~1 t =
 		(case mono_deg_in t v of
-		     d as Some _ => d
+		     d as SOME _ => d
-		   | None => None)
+		   | NONE => NONE)
 	      | edi d dmax t = (*basecase last*)
 		(case mono_deg_in t v of
-		     Some d' => if ((d > d') orelse ((d=0) andalso (d'=0)))  then Some dmax else None
+		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))  then SOME dmax else NONE
-		   | None => None)
+		   | NONE => NONE)
 	in edi ~1 ~1 t end;
 (*
 val v = (term_of o the o (parse thy)) "x";
 val t = (term_of o the o (parse thy)) "a+b";
 expand_deg_in t v;
-(*val it = Some 0*)
+(*val it = SOME 0*)
 val t = (term_of o the o (parse thy)) "(a+b)*x";
 expand_deg_in t v;
-(*Some 1*)
+(*SOME 1*)
 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
 expand_deg_in t v;
-(*Some 1*)
+(*SOME 1*)
 val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
 expand_deg_in t v;
-(*Some 1*)
+(*SOME 1*)
 val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
 expand_deg_in t v;
 *)
 fun poly_deg_in t v =
 	let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
 		(case mono_deg_in t2 v of (* $ is left associative*)
-		     Some d' => edi d' d' t1
+		     SOME d' => edi d' d' t1
-		   | None => None)
+		   | NONE => NONE)
 	      | edi d dmax (Const ("op +",_) $ t1 $ t2) =
 		(case mono_deg_in t2 v of
 		     (*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4  +x*)
-		     Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
+		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else NONE
-		   | None => None)
+		   | NONE => NONE)
 	      | edi ~1 ~1 t =
 		(case mono_deg_in t v of
-		     d as Some _ => d
+		     d as SOME _ => d
-		   | None => None)
+		   | NONE => NONE)
 	      | edi d dmax t = (*basecase last*)
 		(case mono_deg_in t v of
-		     Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then Some dmax else None
+		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then SOME dmax else NONE
-		   | None => None)
+		   | NONE => NONE)
 	in edi ~1 ~1 t end;
 in
 fun is_expanded_in t v =
-case expand_deg_in t v of Some _ => true | None => false;
+case expand_deg_in t v of SOME _ => true | NONE => false;
 fun is_poly_in t v =
-case poly_deg_in t v of Some _ => true | None => false;
+case poly_deg_in t v of SOME _ => true | NONE => false;
 fun has_degree_in t v =
-case expand_deg_in t v of Some d => d | None => ~1;
+case expand_deg_in t v of SOME d => d | NONE => ~1;
 end;
 (*
 val v = (term_of o the o (parse thy)) "x";
 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
 has_degree_in t v;
 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
 fun eval_is_expanded_in _ _
 	     (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
 if is_expanded_in t v
-then Some ((term2str p) ^ " = True",
+then SOME ((term2str p) ^ " = True",
 	  Trueprop $ (mk_equality (p, HOLogic.true_const)))
-else Some ((term2str p) ^ " = True",
+else SOME ((term2str p) ^ " = True",
 	  Trueprop $ (mk_equality (p, HOLogic.false_const)))
-| eval_is_expanded_in _ _ _ _ = None;
+| eval_is_expanded_in _ _ _ _ = NONE;
 (*
 val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
-val Some (id, t') = eval_is_expanded_in 0 0 t 0;
+val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
 term2str t';
 (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
 *)
 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
 fun eval_is_poly_in _ _
 	     (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
 if is_poly_in t v
-then Some ((term2str p) ^ " = True",
+then SOME ((term2str p) ^ " = True",
 	  Trueprop $ (mk_equality (p, HOLogic.true_const)))
-else Some ((term2str p) ^ " = True",
+else SOME ((term2str p) ^ " = True",
 	  Trueprop $ (mk_equality (p, HOLogic.false_const)))
-| eval_is_poly_in _ _ _ _ = None;
+| eval_is_poly_in _ _ _ _ = NONE;
 (*
 val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
-val Some (id, t') = eval_is_poly_in 0 0 t 0;
+val SOME (id, t') = eval_is_poly_in 0 0 t 0;
 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
 term2str t';
 (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
 *)
 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
 fun eval_has_degree_in _ _
 	     (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
 let val d = has_degree_in t v
 	val d' = term_of_num HOLogic.realT d
-in Some ((term2str p) ^ " = " ^ (string_of_int d),
+in SOME ((term2str p) ^ " = " ^ (string_of_int d),
 	  Trueprop $ (mk_equality (p, d')))
 end
-| eval_has_degree_in _ _ _ _ = None;
+| eval_has_degree_in _ _ _ _ = NONE;
 (*
 > val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
-> val Some (id, t') = eval_has_degree_in 0 0 t 0;
+> val SOME (id, t') = eval_has_degree_in 0 0 t 0;
 val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
 > term2str t';
 val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
 *)
 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
 fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
 	(case int_of_str (order) of
-	             Some d => d
+	             SOME d => d
-		   | None   => 0)
+		   | NONE   => 0)
 | get_order_pow _ = 0;
 fun size_of_term' (Const(str,_) $ t) =
 if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
 fun eval_is_polyexp (thmid:string) _
 		       (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
 if is_polyexp arg
-then Some (mk_thmid thmid ""
+then SOME (mk_thmid thmid ""
 			((string_of_cterm o cterm_of (sign_of thy)) arg) "",
 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))
-else Some (mk_thmid thmid ""
+else SOME (mk_thmid thmid ""
 			((string_of_cterm o cterm_of (sign_of thy)) arg) "",
 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))
-| eval_is_polyexp _ _ _ _ = None;
+| eval_is_polyexp _ _ _ _ = NONE;
 val expand_poly_rat_ =
 Rls{id = "expand_poly_rat_", preconds = [],
 rew_ord = ("dummy_ord", dummy_ord),
 erls =  append_rls "e_rls-is_polyexp" e_rls
 	    ((monom_degree xs, xs), (monom_degree ys, ys));
 fun hd_str str = substring (str, 0, 1);
 fun tl_str str = substring (str, 1, (size str) - 1);
-(* liefert nummerischen Koeffizienten eines Monoms oder None *)
+(* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
 fun get_koeff_of_mon [] =  raise error("get_koeff_of_mon: called with l = []")
-| get_koeff_of_mon (l as x::xs) = if is_nums x then Some x
+| get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
-				    else None;
+				    else NONE;
 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
-fun koeff2ordStr (Some x) = (case x of
+fun koeff2ordStr (SOME x) = (case x of
 				 (Free (str, T)) =>
 				     if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
 				     else str
 			       | _ => "aaa") (* "num.Ausdruck" --> gross *)
-| koeff2ordStr None = "---"; (* "kein Koeff" --> kleinste *)
+| koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
 (* Order zum Vergleich von Koeffizienten (strings):
 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
 fun compare_koeff_ord (xs, ys) =
 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
 fun eval_is_multUnordered (thmid:string) _
 		       (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
 if is_multUnordered arg
-then Some (mk_thmid thmid ""
+then SOME (mk_thmid thmid ""
 			((string_of_cterm o cterm_of (sign_of thy)) arg) "",
 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))
-else Some (mk_thmid thmid ""
+else SOME (mk_thmid thmid ""
 			((string_of_cterm o cterm_of (sign_of thy)) arg) "",
 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))
-| eval_is_multUnordered _ _ _ _ = None;
+| eval_is_multUnordered _ _ _ _ = NONE;
 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
 []:(rule * (term * term list)) list;
 fun init_state (_:term) = e_rrlsstate;
 fun locate_rule (_:rule list list) (_:term) (_:rule) =
 ([]:(rule * (term * term list)) list);
-fun next_rule (_:rule list list) (_:term) = (None:rule option);
+fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
-fun normal_form t = Some (sort_variables t,[]:term list);
+fun normal_form t = SOME (sort_variables t,[]:term list);
 val order_mult_ =
 Rrls {id = "order_mult_",
 	  prepat =
 	  [([(term_of o the o (parse thy)) "p is_multUnordered"],
 (*WN.18.6.03 *)
 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
 fun eval_is_addUnordered (thmid:string) _
 		       (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
 if is_addUnordered arg
-then Some (mk_thmid thmid ""
+then SOME (mk_thmid thmid ""
 			((string_of_cterm o cterm_of (sign_of thy)) arg) "",
 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))
-else Some (mk_thmid thmid ""
+else SOME (mk_thmid thmid ""
 			((string_of_cterm o cterm_of (sign_of thy)) arg) "",
 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))
-| eval_is_addUnordered _ _ _ _ = None;
+| eval_is_addUnordered _ _ _ _ = NONE;
 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
 []:(rule * (term * term list)) list;
 fun init_state (_:term) = e_rrlsstate;
 fun locate_rule (_:rule list list) (_:term) (_:rule) =
 ([]:(rule * (term * term list)) list);
-fun next_rule (_:rule list list) (_:term) = (None:rule option);
+fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
-fun normal_form t = Some (sort_monoms t,[]:term list);
+fun normal_form t = SOME (sort_monoms t,[]:term list);
 val order_add_ =
 Rrls {id = "order_add_",
 	  prepat = (*WN.18.6.03 Preconditions und Pattern,
 		    die beide passen muessen, damit das Rrls angewandt wird*)
 ("#Where" ,["t_ is_polyexp"]),
 ("#Find"  ,["normalform n_"])
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)
 			    Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
-Some "Simplify t_",
+SOME "Simplify t_",
 [["simplification","for_polynomials"]]));
 (** methods **)

branch	isac-update-Isa09-2
changeset 37926	e6fc98fbcb85
parent 37922	30eff896074c
child 37930	f2b8d1b3fcc2