81 Calc ("Tools.matches",eval_matches ""), |
81 Calc ("Tools.matches",eval_matches ""), |
82 Calc ("Tools.lhs" ,eval_lhs ""), |
82 Calc ("Tools.lhs" ,eval_lhs ""), |
83 Calc ("Tools.rhs" ,eval_rhs ""), |
83 Calc ("Tools.rhs" ,eval_rhs ""), |
84 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""), |
84 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""), |
85 Calc ("op =",eval_equal "#equal_"), |
85 Calc ("op =",eval_equal "#equal_"), |
86 Thm ("not_true",num_str not_true), |
86 Thm ("not_true",num_str @{not_true), |
87 Thm ("not_false",num_str not_false), |
87 Thm ("not_false",num_str @{not_false), |
88 Thm ("and_true",num_str and_true), |
88 Thm ("and_true",num_str @{and_true), |
89 Thm ("and_false",num_str and_false), |
89 Thm ("and_false",num_str @{and_false), |
90 Thm ("or_true",num_str or_true), |
90 Thm ("or_true",num_str @{or_true), |
91 Thm ("or_false",num_str or_false) |
91 Thm ("or_false",num_str @{or_false) |
92 ]; |
92 ]; |
93 |
93 |
94 |
94 |
95 (*rls = merge_rls erls Poly_erls *) |
95 (*rls = merge_rls erls Poly_erls *) |
96 val rateq_erls = |
96 val rateq_erls = |
101 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) |
101 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) |
102 Calc ("RatEq.is'_ratequation'_in", |
102 Calc ("RatEq.is'_ratequation'_in", |
103 eval_is_ratequation_in "") |
103 eval_is_ratequation_in "") |
104 |
104 |
105 ])) |
105 ])) |
106 [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*) |
106 [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*) |
107 Thm ("or_commute",num_str or_commute) (*WN: ein Hack*) |
107 Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*) |
108 ]; |
108 ]; |
109 ruleset' := overwritelthy thy (!ruleset', |
109 ruleset' := overwritelthy thy (!ruleset', |
110 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*) |
110 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*) |
111 ]); |
111 ]); |
112 |
112 |
118 Poly_erls |
118 Poly_erls |
119 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) |
119 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) |
120 Calc ("RatEq.is'_ratequation'_in", |
120 Calc ("RatEq.is'_ratequation'_in", |
121 eval_is_ratequation_in "") |
121 eval_is_ratequation_in "") |
122 ])) |
122 ])) |
123 [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*) |
123 [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*) |
124 Thm ("or_commute",num_str or_commute) (*WN: ein Hack*) |
124 Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*) |
125 ]; |
125 ]; |
126 |
126 |
127 val RatEq_eliminate = prep_rls( |
127 val RatEq_eliminate = prep_rls( |
128 Rls {id = "RatEq_eliminate", preconds = [], |
128 Rls {id = "RatEq_eliminate", preconds = [], |
129 rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls, |
129 rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls, |
130 calc = [], |
130 calc = [], |
131 rules = [ |
131 rules = [ |
132 Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both), |
132 Thm("rat_mult_denominator_both",num_str @{rat_mult_denominator_both), |
133 (* a/b=c/d -> ad=cb *) |
133 (* a/b=c/d -> ad=cb *) |
134 Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left), |
134 Thm("rat_mult_denominator_left",num_str @{rat_mult_denominator_left), |
135 (* a =c/d -> ad=c *) |
135 (* a =c/d -> ad=c *) |
136 Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right) |
136 Thm("rat_mult_denominator_right",num_str @{rat_mult_denominator_right) |
137 (* a/b=c -> a=cb *) |
137 (* a/b=c -> a=cb *) |
138 ], |
138 ], |
139 scr = Script ((term_of o the o (parse thy)) "empty_script") |
139 scr = Script ((term_of o the o (parse thy)) "empty_script") |
140 }:rls); |
140 }:rls); |
141 ruleset' := overwritelthy thy (!ruleset', |
141 ruleset' := overwritelthy thy (!ruleset', |
144 |
144 |
145 val RatEq_simplify = prep_rls( |
145 val RatEq_simplify = prep_rls( |
146 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), |
146 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), |
147 erls = rateq_erls, srls = Erls, calc = [], |
147 erls = rateq_erls, srls = Erls, calc = [], |
148 rules = [ |
148 rules = [ |
149 Thm("real_rat_mult_1",num_str real_rat_mult_1), |
149 Thm("real_rat_mult_1",num_str @{real_rat_mult_1), |
150 (*a*(b/c) = (a*b)/c*) |
150 (*a*(b/c) = (a*b)/c*) |
151 Thm("real_rat_mult_2",num_str real_rat_mult_2), |
151 Thm("real_rat_mult_2",num_str @{real_rat_mult_2), |
152 (*(a/b)*(c/d) = (a*c)/(b*d)*) |
152 (*(a/b)*(c/d) = (a*c)/(b*d)*) |
153 Thm("real_rat_mult_3",num_str real_rat_mult_3), |
153 Thm("real_rat_mult_3",num_str @{real_rat_mult_3), |
154 (* (a/b)*c = (a*c)/b*) |
154 (* (a/b)*c = (a*c)/b*) |
155 Thm("real_rat_pow",num_str real_rat_pow), |
155 Thm("real_rat_pow",num_str @{real_rat_pow), |
156 (*(a/b)^^^2 = a^^^2/b^^^2*) |
156 (*(a/b)^^^2 = a^^^2/b^^^2*) |
157 Thm("real_diff_minus",num_str real_diff_minus), |
157 Thm("real_diff_minus",num_str @{real_diff_minus), |
158 (* a - b = a + (-1) * b *) |
158 (* a - b = a + (-1) * b *) |
159 Thm("rat_double_rat_1",num_str rat_double_rat_1), |
159 Thm("rat_double_rat_1",num_str @{rat_double_rat_1), |
160 (* (a / (c/d) = (a*d) / c) *) |
160 (* (a / (c/d) = (a*d) / c) *) |
161 Thm("rat_double_rat_2",num_str rat_double_rat_2), |
161 Thm("rat_double_rat_2",num_str @{rat_double_rat_2), |
162 (* ((a/b) / (c/d) = (a*d) / (b*c)) *) |
162 (* ((a/b) / (c/d) = (a*d) / (b*c)) *) |
163 Thm("rat_double_rat_3",num_str rat_double_rat_3) |
163 Thm("rat_double_rat_3",num_str @{rat_double_rat_3) |
164 (* ((a/b) / c = a / (b*c) ) *) |
164 (* ((a/b) / c = a / (b*c) ) *) |
165 ], |
165 ], |
166 scr = Script ((term_of o the o (parse thy)) "empty_script") |
166 scr = Script ((term_of o the o (parse thy)) "empty_script") |
167 }:rls); |
167 }:rls); |
168 ruleset' := overwritelthy thy (!ruleset', |
168 ruleset' := overwritelthy thy (!ruleset', |