1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri Mar 02 14:19:59 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Fri Mar 02 16:19:02 2018 +0100
1.3 @@ -121,15 +121,15 @@
1.4 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.5 (Const ("Groups.times_class.times", _) $
1.6 Free (num, _) $ Free _) $ Free (id, _)) =
1.7 - if TermC.is_numeral num then id
1.8 + if TermC.is_num' num then id
1.9 else "|||||||||||||"
1.10 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.11 - if TermC.is_numeral base then "|||||||||||||" (* a^2 *)
1.12 + if TermC.is_num' base then "|||||||||||||" (* a^2 *)
1.13 else (*increase*) base
1.14 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
1.15 (Const ("Atools.pow", _) $
1.16 Free (base, _) $ Free (exp, _))) =
1.17 - if TermC.is_numeral num andalso not (TermC.is_numeral base) then (*increase*) base
1.18 + if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
1.19 else "|||||||||||||"
1.20 | identifier _ = "|||||||||||||"(*the "largest" string*);
1.21
1.22 @@ -140,38 +140,38 @@
1.23 if TermC.is_num a then (*123 kleiner 32 = True !!!*)
1.24 if TermC.int_of_Free a < TermC.int_of_Free b then
1.25 SOME ((term2str p) ^ " = True",
1.26 - TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.27 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.28 else SOME ((term2str p) ^ " = False",
1.29 - TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.30 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.31 else (* -1 * -2 kleiner 0 *)
1.32 SOME ((term2str p) ^ " = False",
1.33 - TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.34 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.35 else
1.36 if identifier a < identifier b then
1.37 SOME ((term2str p) ^ " = True",
1.38 - TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.39 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.40 else SOME ((term2str p) ^ " = False",
1.41 - TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.42 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.43 | eval_kleiner _ _ _ _ = NONE;
1.44
1.45 fun ist_monom (Free (id,_)) = true
1.46 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
1.47 - if TermC.is_numeral num then true else false
1.48 + if TermC.is_num' num then true else false
1.49 | ist_monom _ = false;
1.50 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
1.51 fun ist_monom (Free (id,_)) = true (* 2, a *)
1.52 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
1.53 - if TermC.is_numeral id then false else true
1.54 + if TermC.is_num' id then false else true
1.55 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.56 (Const ("Groups.times_class.times", _) $
1.57 Free (num, _) $ Free _) $ Free (id, _)) =
1.58 - if TermC.is_numeral num andalso not (TermC.is_numeral id) then true else false
1.59 + if TermC.is_num' num andalso not (TermC.is_num' id) then true else false
1.60 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.61 true (* a^2 *)
1.62 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
1.63 (Const ("Atools.pow", _) $
1.64 Free (base, _) $ Free (exp, _))) =
1.65 - if TermC.is_numeral num then true else false
1.66 + if TermC.is_num' num then true else false
1.67 | ist_monom _ = false;
1.68
1.69 (* is this a univariate monomial ? *)
1.70 @@ -179,9 +179,9 @@
1.71 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
1.72 if ist_monom a then
1.73 SOME ((term2str p) ^ " = True",
1.74 - TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.75 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.76 else SOME ((term2str p) ^ " = False",
1.77 - TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.78 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.79 | eval_ist_monom _ _ _ _ = NONE;
1.80
1.81