108 val thy = @{theory}; |
108 val thy = @{theory}; |
109 |
109 |
110 (** eval functions **) |
110 (** eval functions **) |
111 |
111 |
112 (*. get the identifier from specific monomials; see fun ist_monom .*) |
112 (*. get the identifier from specific monomials; see fun ist_monom .*) |
113 (*HACK.WN080107*) |
113 fun identifier (Free (id, _)) = id (* //2, a *) |
114 fun increase str = |
114 (*TOODOO*) |
115 let |
115 | identifier (* 3*a*b *) |
116 val (s, ss) = |
116 (Const ("Groups.times_class.times", _) $ (Const ("Groups.times_class.times", _) $ |
117 case Symbol.explode str of |
117 num $ t) $ Free (id, _)) = |
118 s :: ss => (s, ss) |
118 if TermC.is_num num andalso TermC.is_atom t then id |
119 | _ => raise ERROR "PolyMinus.increase: uncovered case" |
|
120 in implode ((chr (ord s + 1))::ss) end; |
|
121 fun identifier (Free (id,_)) = id (* 2 , a *) |
|
122 | identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) = |
|
123 id (* 2*a , a*b *) |
|
124 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
|
125 (Const ("Groups.times_class.times", _) $ |
|
126 Free (num, _) $ Free _) $ Free (id, _)) = |
|
127 if TermC.is_num' num then id |
|
128 else "|||||||||||||" |
119 else "|||||||||||||" |
129 | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) = |
120 |
130 if TermC.is_num' base then "|||||||||||||" (* a^2 *) |
121 | identifier (* 2*a, a*b *) |
131 else (*increase*) base |
122 (Const ("Groups.times_class.times", _) $ num $ Free (id, _)) = |
132 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
123 if TermC.is_atom num then id |
133 (Const ("Transcendental.powr", _) $ |
|
134 Free (base, _) $ Free (_(*exp*), _))) = |
|
135 if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base |
|
136 else "|||||||||||||" |
124 else "|||||||||||||" |
137 | identifier _ = "|||||||||||||"(*the "largest" string*); |
125 |
|
126 | identifier (Const ("Transcendental.powr", _) $ base $ exp) = (* a^2 *) |
|
127 if TermC.is_num base andalso TermC.is_atom exp then "|||||||||||||" |
|
128 else TermC.string_of_atom base |
|
129 |
|
130 | identifier (* 3*a^2 *) |
|
131 (Const ("Groups.times_class.times", _) $ num $ |
|
132 (Const ("Transcendental.powr", _) $ base $ exp )) = |
|
133 if TermC.is_num num andalso not (TermC.is_num base) andalso TermC.is_atom exp |
|
134 then TermC.string_of_atom base |
|
135 else "|||||||||||||" |
|
136 |
|
137 | identifier t = |
|
138 if TermC.is_num t then TermC.string_of_num t (* 2 , //a *) |
|
139 else "|||||||||||||"; (*the "largest" string*) |
138 |
140 |
139 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*) |
141 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*) |
140 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *) |
142 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *) |
141 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ = |
143 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ = |
142 if TermC.is_num b then |
144 if TermC.is_num b then |
143 if TermC.is_num a then (*123 kleiner 32 = True !!!*) |
145 if TermC.is_num a then (*123 kleiner 32 = True !!!*) |
144 if TermC.num_of_term a < TermC.num_of_term b then |
146 if TermC.num_of_term a < TermC.num_of_term b then |
145 SOME ((UnparseC.term p) ^ " = True", |
147 SOME ((UnparseC.term p) ^ " = True", |
146 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
148 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
147 else SOME ((UnparseC.term p) ^ " = False", |
149 else SOME ((UnparseC.term p) ^ " = False", |
148 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
150 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
149 else (* -1 * -2 kleiner 0 *) |
151 else (* -1 * -2 kleiner 0 *) |
150 SOME ((UnparseC.term p) ^ " = False", |
152 SOME ((UnparseC.term p) ^ " = False", |
151 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
153 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
152 else |
154 else |
153 if identifier a < identifier b then |
155 if identifier a < identifier b then |
154 SOME ((UnparseC.term p) ^ " = True", |
156 SOME ((UnparseC.term p) ^ " = True", |
155 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
157 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
156 else SOME ((UnparseC.term p) ^ " = False", |
158 else SOME ((UnparseC.term p) ^ " = False", |
157 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
159 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
158 | eval_kleiner _ _ _ _ = NONE; |
160 | eval_kleiner _ _ _ _ = NONE; |
159 |
161 |
160 fun ist_monom (Free _) = true (* 2, a *) |
162 fun ist_monom t = |
161 | ist_monom (Const ("Groups.times_class.times", _) $ |
163 if TermC.is_atom t then true |
162 (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true |
164 else |
163 | ist_monom (Const ("Groups.times_class.times", _) $ (* 2*a, a*b *) |
165 case t of |
164 Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false |
166 Const ("Groups.times_class.times", _) $ t1 $ t2 => |
165 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
167 ist_monom t1 andalso ist_monom t2 |
166 (Const ("Groups.times_class.times", _) $ |
168 | Const ("Transcendental.powr", _) $ t1 $ t2 => |
167 (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true |
169 ist_monom t1 andalso ist_monom t2 |
168 | ist_monom (Const ("Transcendental.powr", _) $ (* a^2 *) |
170 | _ => false |
169 Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true |
|
170 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a^2 *) |
|
171 (Const ("Num.numeral_class.numeral", _) $ _) $ |
|
172 (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true |
|
173 | ist_monom _ = false; |
|
174 |
171 |
175 (* is this a univariate monomial ? *) |
172 (* is this a univariate monomial ? *) |
176 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*) |
173 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*) |
177 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist_monom",_) $ a)) _ = |
174 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist_monom",_) $ a)) _ = |
178 if ist_monom a then |
175 if ist_monom a then |