114 (*HACK.WN080107*) |
114 (*HACK.WN080107*) |
115 fun increase str = |
115 fun increase str = |
116 let val s::ss = explode str |
116 let val s::ss = explode str |
117 in implode ((chr (ord s + 1))::ss) end; |
117 in implode ((chr (ord s + 1))::ss) end; |
118 fun identifier (Free (id,_)) = id (* 2, a *) |
118 fun identifier (Free (id,_)) = id (* 2, a *) |
119 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = |
119 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = |
120 id (* 2*a, a*b *) |
120 id (* 2*a, a*b *) |
121 | identifier (Const ("op *", _) $ (* 3*a*b *) |
121 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
122 (Const ("op *", _) $ |
122 (Const ("Groups.times_class.times", _) $ |
123 Free (num, _) $ Free _) $ Free (id, _)) = |
123 Free (num, _) $ Free _) $ Free (id, _)) = |
124 if is_numeral num then id |
124 if is_numeral num then id |
125 else "|||||||||||||" |
125 else "|||||||||||||" |
126 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = |
126 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = |
127 if is_numeral base then "|||||||||||||" (* a^2 *) |
127 if is_numeral base then "|||||||||||||" (* a^2 *) |
128 else (*increase*) base |
128 else (*increase*) base |
129 | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *) |
129 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
130 (Const ("Atools.pow", _) $ |
130 (Const ("Atools.pow", _) $ |
131 Free (base, _) $ Free (exp, _))) = |
131 Free (base, _) $ Free (exp, _))) = |
132 if is_numeral num andalso not (is_numeral base) then (*increase*) base |
132 if is_numeral num andalso not (is_numeral base) then (*increase*) base |
133 else "|||||||||||||" |
133 else "|||||||||||||" |
134 | identifier _ = "|||||||||||||"(*the "largest" string*); |
134 | identifier _ = "|||||||||||||"(*the "largest" string*); |
153 else SOME ((term2str p) ^ " = False", |
153 else SOME ((term2str p) ^ " = False", |
154 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
154 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
155 | eval_kleiner _ _ _ _ = NONE; |
155 | eval_kleiner _ _ _ _ = NONE; |
156 |
156 |
157 fun ist_monom (Free (id,_)) = true |
157 fun ist_monom (Free (id,_)) = true |
158 | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = |
158 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = |
159 if is_numeral num then true else false |
159 if is_numeral num then true else false |
160 | ist_monom _ = false; |
160 | ist_monom _ = false; |
161 (*. this function only accepts the most simple monoms vvvvvvvvvv .*) |
161 (*. this function only accepts the most simple monoms vvvvvvvvvv .*) |
162 fun ist_monom (Free (id,_)) = true (* 2, a *) |
162 fun ist_monom (Free (id,_)) = true (* 2, a *) |
163 | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) |
163 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) |
164 if is_numeral id then false else true |
164 if is_numeral id then false else true |
165 | ist_monom (Const ("op *", _) $ (* 3*a*b *) |
165 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
166 (Const ("op *", _) $ |
166 (Const ("Groups.times_class.times", _) $ |
167 Free (num, _) $ Free _) $ Free (id, _)) = |
167 Free (num, _) $ Free _) $ Free (id, _)) = |
168 if is_numeral num andalso not (is_numeral id) then true else false |
168 if is_numeral num andalso not (is_numeral id) then true else false |
169 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = |
169 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = |
170 true (* a^2 *) |
170 true (* a^2 *) |
171 | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *) |
171 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
172 (Const ("Atools.pow", _) $ |
172 (Const ("Atools.pow", _) $ |
173 Free (base, _) $ Free (exp, _))) = |
173 Free (base, _) $ Free (exp, _))) = |
174 if is_numeral num then true else false |
174 if is_numeral num then true else false |
175 | ist_monom _ = false; |
175 | ist_monom _ = false; |
176 |
176 |
295 Thm ("vorzeichen_minus_weg3",num_str @{thm vorzeichen_minus_weg3}), |
295 Thm ("vorzeichen_minus_weg3",num_str @{thm vorzeichen_minus_weg3}), |
296 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*) |
296 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*) |
297 Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}), |
297 Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}), |
298 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*) |
298 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*) |
299 |
299 |
300 Calc ("op *", eval_binop "#mult_"), |
300 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
301 |
301 |
302 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), |
302 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), |
303 (*"0 * z = 0"*) |
303 (*"0 * z = 0"*) |
304 Thm ("mult_1_left",num_str @{thm mult_1_left}), |
304 Thm ("mult_1_left",num_str @{thm mult_1_left}), |
305 (*"1 * z = z"*) |
305 (*"1 * z = z"*) |