126 Rule.Thm("rat_mult_denominator_left",TermC.num_str @{thm rat_mult_denominator_left}), |
126 Rule.Thm("rat_mult_denominator_left",TermC.num_str @{thm rat_mult_denominator_left}), |
127 (* a =c/d -> ad=c *) |
127 (* a =c/d -> ad=c *) |
128 Rule.Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right}) |
128 Rule.Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right}) |
129 (* a/b=c -> a=cb *) |
129 (* a/b=c -> a=cb *) |
130 ], |
130 ], |
131 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")}); |
131 scr = Rule.EmptyScr}); |
132 |
132 |
133 \<close> ML \<open> |
133 \<close> ML \<open> |
134 val RatEq_simplify = prep_rls'( |
134 val RatEq_simplify = prep_rls'( |
135 Rule.Rls |
135 Rule.Rls |
136 {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls, |
136 {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls, |
150 (* (a / (c/d) = (a*d) / c) *) |
150 (* (a / (c/d) = (a*d) / c) *) |
151 Rule.Thm("rat_double_rat_2",TermC.num_str @{thm rat_double_rat_2}), |
151 Rule.Thm("rat_double_rat_2",TermC.num_str @{thm rat_double_rat_2}), |
152 (* ((a/b) / (c/d) = (a*d) / (b*c)) *) |
152 (* ((a/b) / (c/d) = (a*d) / (b*c)) *) |
153 Rule.Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3}) |
153 Rule.Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3}) |
154 (* ((a/b) / c = a / (b*c) ) *)], |
154 (* ((a/b) / c = a / (b*c) ) *)], |
155 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")}); |
155 scr = Rule.EmptyScr}); |
156 \<close> |
156 \<close> |
157 setup \<open>KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))]\<close> |
157 setup \<open>KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))]\<close> |
158 setup \<open>KEStore_Elems.add_rlss [("RatEq_eliminate", (Context.theory_name @{theory}, RatEq_eliminate))]\<close> |
158 setup \<open>KEStore_Elems.add_rlss [("RatEq_eliminate", (Context.theory_name @{theory}, RatEq_eliminate))]\<close> |
159 setup \<open>KEStore_Elems.add_rlss [("RatEq_simplify", (Context.theory_name @{theory}, RatEq_simplify))]\<close> |
159 setup \<open>KEStore_Elems.add_rlss [("RatEq_simplify", (Context.theory_name @{theory}, RatEq_simplify))]\<close> |
160 |
160 |