1.1 --- a/src/Tools/isac/IsacKnowledge/Rational-WN.sml Wed Aug 18 13:53:15 2010 +0200
1.2 +++ b/src/Tools/isac/IsacKnowledge/Rational-WN.sml Wed Aug 18 13:55:23 2010 +0200
1.3 @@ -69,14 +69,14 @@
1.4 | poly t v g = mono t v g;
1.5
1.6 fun term2poly (t as Free (s, _)) v =
1.7 - if t = v then Some ([0,1] : poly) else (Some [(the o int_of_str) s]
1.8 - handle _ => None)
1.9 + if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]
1.10 + handle _ => NONE)
1.11 | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
1.12 - if t = v then Some [0, (the o int_of_str) s1] else None
1.13 + if t = v then SOME [0, (the o int_of_str) s1] else NONE
1.14 | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v =
1.15 - Some ([(the o int_of_str) s1] @ (poly t v 1))
1.16 + SOME ([(the o int_of_str) s1] @ (poly t v 1))
1.17 | term2poly t v =
1.18 - Some (poly t v 0) handle _ => None;
1.19 + SOME (poly t v 0) handle _ => NONE;
1.20
1.21 (*tests*)
1.22 val v = (term_of o the o (parse thy)) "x::real";
1.23 @@ -105,7 +105,7 @@
1.24
1.25
1.26 fun is_polynomial_in t v =
1.27 - case term2poly t v of Some _ => true | None => false;
1.28 + case term2poly t v of SOME _ => true | NONE => false;
1.29
1.30 (* transform the internal polynomial p into an Isabelle term t
1.31 where t meets the preconditions of term2poly
1.32 @@ -196,25 +196,25 @@
1.33 Thm (thmid, thm) =>
1.34 (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.35 rls put_asm (thm_of_thm rul) ct of
1.36 - None => rew_once ruls asm ct apno thms
1.37 - | Some (ct',asm') =>
1.38 + NONE => rew_once ruls asm ct apno thms
1.39 + | SOME (ct',asm') =>
1.40 rew_once ruls (asm union asm') ct' Appl (rul::thms))
1.41 | Calc (cc as (op_,_)) =>
1.42 (case get_calculation_ thy cc ct of
1.43 - None => rew_once ruls asm ct apno thms
1.44 - | Some (thmid, thm') =>
1.45 + NONE => rew_once ruls asm ct apno thms
1.46 + | SOME (thmid, thm') =>
1.47 let
1.48 val pairopt =
1.49 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.50 rls put_asm thm' ct;
1.51 - val _ = if pairopt <> None then ()
1.52 + val _ = if pairopt <> NONE then ()
1.53 else raise error("rewrite_set_, rewrite_ \""^
1.54 (string_of_thmI thm')^"\" \""^
1.55 - (Sign.string_of_term (sign_of thy) ct)^"\" = None")
1.56 + (Sign.string_of_term (sign_of thy) ct)^"\" = NONE")
1.57 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
1.58 val ruls = (#rules o rep_rls) ruless;
1.59 val (ct',asm') = rew_once ruls [] ct Noap ruls;
1.60 - in if ct = ct' then None else Some (ct',asm') end;
1.61 + in if ct = ct' then NONE else SOME (ct',asm') end;
1.62
1.63 (*
1.64 fun reverse_rewrite t1 t2 rls =
1.65 @@ -232,25 +232,25 @@
1.66 Thm (thmid, thm) =>
1.67 (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.68 rls put_asm (thm_of_thm rul) ct of
1.69 - None => rew_once ruls asm ct apno thms
1.70 - | Some (ct',asm') =>
1.71 + NONE => rew_once ruls asm ct apno thms
1.72 + | SOME (ct',asm') =>
1.73 rew_once ruls (asm union asm') ct' Appl (rul::thms))
1.74 | Calc (cc as (op_,_)) =>
1.75 (case get_calculation_ thy cc ct of
1.76 - None => rew_once ruls asm ct apno thms
1.77 - | Some (thmid, thm') =>
1.78 + NONE => rew_once ruls asm ct apno thms
1.79 + | SOME (thmid, thm') =>
1.80 let
1.81 val pairopt =
1.82 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.83 rls put_asm thm' ct;
1.84 - val _ = if pairopt <> None then ()
1.85 + val _ = if pairopt <> NONE then ()
1.86 else raise error("rewrite_set_, rewrite_ \""^
1.87 (string_of_thmI thm')^"\" \""^
1.88 - (Sign.string_of_term (sign_of thy) ct)^"\" = None")
1.89 + (Sign.string_of_term (sign_of thy) ct)^"\" = NONE")
1.90 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
1.91 val ruls = (#rules o rep_rls) ruless;
1.92 val (ct',asm') = rew_once ruls [] ct Noap ruls;
1.93 - in if ct = ct' then None else Some (ct',asm') end;
1.94 + in if ct = ct' then NONE else SOME (ct',asm') end;
1.95
1.96 realpow_two;
1.97 real_mult_div_cancel1;