907 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; |
907 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; |
908 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4"); |
908 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4"); |
909 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2"); |
909 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2"); |
910 |
910 |
911 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
911 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
912 rew_sub ctxt 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
912 rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
913 if rewritten then NONE else SOME "e_errpatID"; |
913 if rewritten then NONE else SOME "e_errpatID"; |
914 |
914 |
915 val norm_res = case rewrite_set_ ctxt false rls res' of |
915 val norm_res = case rewrite_set_ ctxt false rls res' of |
916 NONE => res' |
916 NONE => res' |
917 | SOME (norm_res, _) => norm_res |
917 | SOME (norm_res, _) => norm_res |
955 val rls = norm_diff |
955 val rls = norm_diff |
956 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; |
956 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; |
957 val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)"); |
957 val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)"); |
958 |
958 |
959 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
959 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
960 rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
960 rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
961 if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then () |
961 if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then () |
962 else error "build fun check_for' ?bdv changed 2"; |
962 else error "build fun check_for' ?bdv changed 2"; |
963 |
963 |
964 val norm_res = case rewrite_set_inst_ ctxt false subst rls res' of |
964 val norm_res = case rewrite_set_inst_ ctxt false subst rls res' of |
965 NONE => res' |
965 NONE => res' |
1117 |
1117 |
1118 "~~~~~ fun fill_form, args:"; |
1118 "~~~~~ fun fill_form, args:"; |
1119 val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) = |
1119 val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) = |
1120 (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats); |
1120 (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats); |
1121 val (form', _, _, rewritten) = |
1121 val (form', _, _, rewritten) = |
1122 rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
1122 rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
1123 |
1123 |
1124 if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then () |
1124 if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then () |
1125 else error "find_fill_patterns changed 3"; |
1125 else error "find_fill_patterns changed 3"; |
1126 |
1126 |
1127 "~~~~~ to findFillpatterns return val:"; val (fillpats) = |
1127 "~~~~~ to findFillpatterns return val:"; val (fillpats) = |