1629 erls = Rule_Set.Empty, |
1629 erls = Rule_Set.Empty, |
1630 srls = Rule_Set.Empty, calc = [], errpatts = [], |
1630 srls = Rule_Set.Empty, calc = [], errpatts = [], |
1631 rules = [(*for rewriting conditions in Thm's*) |
1631 rules = [(*for rewriting conditions in Thm's*) |
1632 Eval ("Prog_Expr.occurs_in", |
1632 Eval ("Prog_Expr.occurs_in", |
1633 eval_occurs_in "#occurs_in_"), |
1633 eval_occurs_in "#occurs_in_"), |
1634 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), |
1634 Thm ("not_true", @{thm not_true}), |
1635 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})], |
1635 Thm ("not_false", @{thm not_false})], |
1636 scr = Empty_Prog}; |
1636 scr = Empty_Prog}; |
1637 val subs = [(str2t "bdv::real", str2t "x::real")]; |
1637 val subs = [(str2t "bdv::real", str2t "x::real")]; |
1638 \<close> ML \<open> |
1638 \<close> ML \<open> |
1639 fun rewrit thm str = |
1639 fun rewrit thm str = |
1640 fst (the (rewrite_inst_ thy tless_true |
1640 fst (the (rewrite_inst_ thy tless_true |
1801 |
1801 |
1802 "===== test 4"; |
1802 "===== test 4"; |
1803 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; |
1803 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; |
1804 val rls = |
1804 val rls = |
1805 (Rule_Set.append_rules "separate_bdv" collect_bdv |
1805 (Rule_Set.append_rules "separate_bdv" collect_bdv |
1806 [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}), |
1806 [Thm ("separate_bdv", @{thm separate_bdv}), |
1807 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
1807 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
1808 Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), |
1808 Thm ("separate_bdv_n", @{thm separate_bdv_n}), |
1809 (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*) |
1809 (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*) |
1810 Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), |
1810 Thm ("separate_1_bdv", @{thm separate_1_bdv}), |
1811 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
1811 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
1812 Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n}) |
1812 Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n}) |
1813 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*) |
1813 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*) |
1814 ]); |
1814 ]); |
1815 (*show_types := true; --- do we need type-constraint in thms? *) |
1815 (*show_types := true; --- do we need type-constraint in thms? *) |
1816 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*) |
1816 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*) |
1817 @{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*) |
1817 @{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*) |
1818 @{thm separate_1_bdv}; (*::?'a*) |
1818 @{thm separate_1_bdv}; (*::?'a*) |
1819 val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*) |
1819 val xxx = @{thm separate_1_bdv}; (*::?'a*) |
1820 @{thm separate_1_bdv_n}; (*::real ..because of \<up> *) |
1820 @{thm separate_1_bdv_n}; (*::real ..because of \<up> *) |
1821 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*) |
1821 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*) |
1822 |
1822 |
1823 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t; |
1823 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t; |
1824 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then () |
1824 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then () |
2198 "----------- problems --------------------------------------------"; |
2198 "----------- problems --------------------------------------------"; |
2199 "----------- problems --------------------------------------------"; |
2199 "----------- problems --------------------------------------------"; |
2200 val t = TermC.str2term "Length [x+y=1,y=2] = 2"; |
2200 val t = TermC.str2term "Length [x+y=1,y=2] = 2"; |
2201 TermC.atomty t; |
2201 TermC.atomty t; |
2202 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty |
2202 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty |
2203 [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})), |
2203 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})), |
2204 (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})), |
2204 (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})), |
2205 Eval ("Groups.plus_class.plus", eval_binop "#add_"), |
2205 Eval ("Groups.plus_class.plus", eval_binop "#add_"), |
2206 Eval ("HOL.eq",eval_equal "#equal_") |
2206 Eval ("HOL.eq",eval_equal "#equal_") |
2207 ]; |
2207 ]; |
2208 val SOME (t',_) = rewrite_set_ thy false testrls t; |
2208 val SOME (t',_) = rewrite_set_ thy false testrls t; |
2209 if UnparseC.term t' = "True" then () |
2209 if UnparseC.term t' = "True" then () |
2892 val t = TermC.str2term |
2892 val t = TermC.str2term |
2893 ("[L * q_0 = c, " ^ |
2893 ("[L * q_0 = c, " ^ |
2894 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
2894 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
2895 "0 = c_4, " ^ |
2895 "0 = c_4, " ^ |
2896 "0 = c_3]"); |
2896 "0 = c_3]"); |
2897 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t; |
2897 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
2898 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t; |
2898 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
2899 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t; |
2899 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
2900 if UnparseC.term t = |
2900 if UnparseC.term t = |
2901 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" |
2901 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" |
2902 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
2902 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
2903 |
2903 |
2904 \<close> ML \<open> |
2904 \<close> ML \<open> |