114 (writeln o istates2str) (get_obj g_loc pt [4]); |
114 (writeln o istates2str) (get_obj g_loc pt [4]); |
115 |
115 |
116 *) |
116 *) |
117 "----------------------------------------------------------"; |
117 "----------------------------------------------------------"; |
118 |
118 |
119 val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls |
119 val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls |
120 ((#rules o Rule_Set.rep) Test_simplify) |
120 ((#rules o Rule_Set.rep) Test_simplify) |
121 (sqrt_right false (@{theory "Pure"})) NONE |
121 (sqrt_right false (@{theory "Pure"})) NONE |
122 (TermC.str2term "x + 1 + - 1 * 2 = 0"); |
122 (TermC.str2term "x + 1 + - 1 * 2 = 0"); |
123 (writeln o Derive.trtas2str) fod; |
123 (writeln o Derive.trtas2str) fod; |
124 |
124 |
125 val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls |
125 val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls |
126 ((#rules o Rule_Set.rep) Test_simplify) |
126 ((#rules o Rule_Set.rep) Test_simplify) |
127 (sqrt_right false (@{theory "Pure"})) NONE |
127 (sqrt_right false (@{theory "Pure"})) NONE |
128 (TermC.str2term "- 2 * 1 + (1 + x) = 0"); |
128 (TermC.str2term "- 2 * 1 + (1 + x) = 0"); |
129 (writeln o Derive.trtas2str) ifod; |
129 (writeln o Derive.trtas2str) ifod; |
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
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 thy 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
912 rew_sub ctxt 1 [] e_rew_ord 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_ (Isac()) 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 |
918 |
918 |
919 val norm_inf = case rewrite_set_ (Isac()) false rls inf of |
919 val norm_inf = case rewrite_set_ ctxt false rls inf of |
920 NONE => inf |
920 NONE => inf |
921 | SOME (norm_inf, _) => norm_inf; |
921 | SOME (norm_inf, _) => norm_inf; |
922 |
922 |
923 res' = inf; |
923 res' = inf; |
924 norm_res = norm_inf; |
924 norm_res = norm_inf; |
943 then () else error "error patt example3 changed"; |
943 then () else error "error patt example3 changed"; |
944 |
944 |
945 "--------- build fun check_for' ?bdv -------------------------"; |
945 "--------- build fun check_for' ?bdv -------------------------"; |
946 "--------- build fun check_for' ?bdv -------------------------"; |
946 "--------- build fun check_for' ?bdv -------------------------"; |
947 "--------- build fun check_for' ?bdv -------------------------"; |
947 "--------- build fun check_for' ?bdv -------------------------"; |
|
948 val ctxt = Proof_Context.init_global @{theory} |
948 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst; |
949 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst; |
949 val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))"; |
950 val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))"; |
950 val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t; |
951 val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t; |
951 if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then () |
952 if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then () |
952 else error "build fun check_for' ?bdv changed 1"; |
953 else error "build fun check_for' ?bdv changed 1"; |
953 |
954 |
954 val rls = norm_diff |
955 val rls = norm_diff |
955 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)"; |
956 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)"); |
957 |
958 |
958 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*) |
959 rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
960 rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
960 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 () |
961 else error "build fun check_for' ?bdv changed 2"; |
962 else error "build fun check_for' ?bdv changed 2"; |
962 |
963 |
963 val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of |
964 val norm_res = case rewrite_set_inst_ ctxt false subst rls res' of |
964 NONE => res' |
965 NONE => res' |
965 | SOME (norm_res, _) => norm_res; |
966 | SOME (norm_res, _) => norm_res; |
966 if UnparseC.term norm_res = "2 * x + cos (4 * x \<up> 3)" then () |
967 if UnparseC.term norm_res = "2 * x + cos (4 * x \<up> 3)" then () |
967 else error "build fun check_for' ?bdv changed 3"; |
968 else error "build fun check_for' ?bdv changed 3"; |
968 |
969 |
969 val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of |
970 val norm_inf = case rewrite_set_inst_ ctxt false subst rls inf of |
970 NONE => inf |
971 NONE => inf |
971 | SOME (norm_inf, _) => norm_inf; |
972 | SOME (norm_inf, _) => norm_inf; |
972 if UnparseC.term norm_inf = "2 * x + cos (4 * x \<up> 3)" then () |
973 if UnparseC.term norm_inf = "2 * x + cos (4 * x \<up> 3)" then () |
973 else error "build fun check_for' ?bdv changed 4"; |
974 else error "build fun check_for' ?bdv changed 4"; |
974 |
975 |
1116 |
1117 |
1117 "~~~~~ fun fill_form, args:"; |
1118 "~~~~~ fun fill_form, args:"; |
1118 val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) = |
1119 val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) = |
1119 (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats); |
1120 (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats); |
1120 val (form', _, _, rewritten) = |
1121 val (form', _, _, rewritten) = |
1121 rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
1122 rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
1122 |
1123 |
1123 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 () |
1124 else error "find_fill_patterns changed 3"; |
1125 else error "find_fill_patterns changed 3"; |
1125 |
1126 |
1126 "~~~~~ to findFillpatterns return val:"; val (fillpats) = |
1127 "~~~~~ to findFillpatterns return val:"; val (fillpats) = |