32 (b - a) = (-a + b)" and |
32 (b - a) = (-a + b)" and |
33 tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==> |
33 tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==> |
34 (- b + a) = (a - b)" and |
34 (- b + a) = (a - b)" and |
35 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==> |
35 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==> |
36 (- b - a) = (-a - b)" and |
36 (- b - a) = (-a - b)" and |
|
37 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*) |
37 tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and |
38 tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and |
38 tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and |
39 tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and |
39 tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and |
40 tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and |
40 tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and |
41 tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and |
|
42 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*) |
41 |
43 |
42 (*commute with invariant (a.b).c -association*) |
44 (*commute with invariant (a.b).c -association*) |
43 tausche_mal: "[| b is_atom; a kleiner b |] ==> |
45 tausche_mal: "[| b is_atom; a kleiner b |] ==> |
44 (b * a) = (a * b)" and |
46 (b * a) = (a * b)" and |
45 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==> |
47 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==> |
85 subtrahiere_vor_minus: "[| l is_const; m is_const |] ==> |
87 subtrahiere_vor_minus: "[| l is_const; m is_const |] ==> |
86 - (l * v) - m * v = (-l - m) * v" and |
88 - (l * v) - m * v = (-l - m) * v" and |
87 subtrahiere_eins_vor_minus:"[| m is_const |] ==> |
89 subtrahiere_eins_vor_minus:"[| m is_const |] ==> |
88 - v - m * v = (-1 - m) * v" and |
90 - v - m * v = (-1 - m) * v" and |
89 |
91 |
|
92 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*) |
90 vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and |
93 vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and |
91 vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and |
94 vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and |
92 vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and |
95 vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and |
93 vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and |
96 vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and |
|
97 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*) |
94 |
98 |
95 (*klammer_plus_plus = (add.assoc RS sym)*) |
99 (*klammer_plus_plus = (add.assoc RS sym)*) |
96 klammer_plus_minus: "a + (b - c) = (a + b) - c" and |
100 klammer_plus_minus: "a + (b - c) = (a + b) - c" and |
97 klammer_minus_plus: "a - (b + c) = (a - b) - c" and |
101 klammer_minus_plus: "a - (b + c) = (a - b) - c" and |
98 klammer_minus_minus: "a - (b - c) = (a - b) + c" and |
102 klammer_minus_minus: "a - (b - c) = (a - b) + c" and |
106 (** eval functions **) |
110 (** eval functions **) |
107 |
111 |
108 (*. get the identifier from specific monomials; see fun ist_monom .*) |
112 (*. get the identifier from specific monomials; see fun ist_monom .*) |
109 (*HACK.WN080107*) |
113 (*HACK.WN080107*) |
110 fun increase str = |
114 fun increase str = |
111 let val s::ss = Symbol.explode str |
115 let |
112 in implode ((chr (ord s + 1))::ss) end; |
116 val (s, ss) = |
113 fun identifier (Free (id,_)) = id (* 2, a *) |
117 case Symbol.explode str of |
114 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = |
118 s :: ss => (s, ss) |
115 id (* 2*a, a*b *) |
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 *) |
116 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
124 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
117 (Const ("Groups.times_class.times", _) $ |
125 (Const ("Groups.times_class.times", _) $ |
118 Free (num, _) $ Free _) $ Free (id, _)) = |
126 Free (num, _) $ Free _) $ Free (id, _)) = |
119 if TermC.is_num' num then id |
127 if TermC.is_num' num then id |
120 else "|||||||||||||" |
128 else "|||||||||||||" |
121 | identifier (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (exp, _)) = |
129 | identifier (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (_(*exp*), _)) = |
122 if TermC.is_num' base then "|||||||||||||" (* a^2 *) |
130 if TermC.is_num' base then "|||||||||||||" (* a^2 *) |
123 else (*increase*) base |
131 else (*increase*) base |
124 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
132 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
125 (Const ("Prog_Expr.pow", _) $ |
133 (Const ("Prog_Expr.pow", _) $ |
126 Free (base, _) $ Free (exp, _))) = |
134 Free (base, _) $ Free (_(*exp*), _))) = |
127 if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base |
135 if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base |
128 else "|||||||||||||" |
136 else "|||||||||||||" |
129 | identifier _ = "|||||||||||||"(*the "largest" string*); |
137 | identifier _ = "|||||||||||||"(*the "largest" string*); |
130 |
138 |
131 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*) |
139 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*) |
147 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
155 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
148 else SOME ((UnparseC.term p) ^ " = False", |
156 else SOME ((UnparseC.term p) ^ " = False", |
149 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
157 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
150 | eval_kleiner _ _ _ _ = NONE; |
158 | eval_kleiner _ _ _ _ = NONE; |
151 |
159 |
152 fun ist_monom (Free (id,_)) = true |
160 fun ist_monom (Free _) = true |
153 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = |
161 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) = |
154 if TermC.is_num' num then true else false |
162 if TermC.is_num' num then true else false |
155 | ist_monom _ = false; |
163 | ist_monom _ = false; |
156 (*. this function only accepts the most simple monoms vvvvvvvvvv .*) |
164 (*. this function only accepts the most simple monoms vvvvvvvvvv .*) |
157 fun ist_monom (Free (id,_)) = true (* 2, a *) |
165 fun ist_monom (Free _) = true (* 2, a *) |
158 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) |
166 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) |
159 if TermC.is_num' id then false else true |
167 if TermC.is_num' id then false else true |
160 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
168 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *) |
161 (Const ("Groups.times_class.times", _) $ |
169 (Const ("Groups.times_class.times", _) $ |
162 Free (num, _) $ Free _) $ Free (id, _)) = |
170 Free (num, _) $ Free _) $ Free (id, _)) = |
163 if TermC.is_num' num andalso not (TermC.is_num' id) then true else false |
171 if TermC.is_num' num andalso not (TermC.is_num' id) then true else false |
164 | ist_monom (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (exp, _)) = |
172 | ist_monom (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) = |
165 true (* a^2 *) |
173 true (* a^2 *) |
166 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
174 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) |
167 (Const ("Prog_Expr.pow", _) $ |
175 (Const ("Prog_Expr.pow", _) $ |
168 Free (base, _) $ Free (exp, _))) = |
176 Free _ $ Free _)) = |
169 if TermC.is_num' num then true else false |
177 if TermC.is_num' num then true else false |
170 | ist_monom _ = false; |
178 | ist_monom _ = false; |
171 |
179 |
172 (* is this a univariate monomial ? *) |
180 (* is this a univariate monomial ? *) |
173 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*) |
181 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*) |