1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 27 12:32:43 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Aug 01 14:39:03 2021 +0200
1.3 @@ -1151,8 +1151,8 @@
1.4
1.5 ML\<open>
1.6
1.7 -(* termorder hacked by MG *)
1.8 -local (*. for make_polynomial_in .*)
1.9 +(* termorder hacked by MG, adapted later by WN *)
1.10 +(**)local (*. for make_polynomial_in .*)
1.11
1.12 open Term; (* for type order = EQUAL | LESS | GREATER *)
1.13
1.14 @@ -1169,59 +1169,82 @@
1.15 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
1.16 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
1.17
1.18 -fun size_of_term' x (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $
1.19 - Free (var, _) $ Const (\<^const_name>\<open>numeral\<close>, _) $ pot) =
1.20 - (case x of (*WN*)
1.21 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
1.22 + Free (var, _) $ Free (pot, _)) =
1.23 + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
1.24 + case x of (*WN*)
1.25 (Free (xstr, _)) =>
1.26 - (if xstr = var then 1000 * (HOLogic.dest_numeral pot) else 3)
1.27 + if xstr = var
1.28 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
1.29 + 1000 * (the (TermC.int_opt_of_string pot)))
1.30 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
1.31 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.32 - | size_of_term' x (Free (subst, _)) =
1.33 - (case x of
1.34 - (Free (xstr, _)) => (if xstr = subst then 1000 else 1)
1.35 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.36 - | size_of_term' x (Abs (_, _, body)) = 1 + size_of_term' x body
1.37 - | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
1.38 - | size_of_term' _ _ = 1;
1.39 + | size_of_term' i pr x (t as Abs (_, _, body)) =
1.40 + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
1.41 + 1 + size_of_term' (i + 1) pr x body)
1.42 + | size_of_term' i pr x (f $ t) =
1.43 + let
1.44 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
1.45 + val s1 = size_of_term' (i + 1) pr x f
1.46 + val s2 = size_of_term' (i + 1) pr x t
1.47 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
1.48 + in (s1 + s2) end
1.49 + | size_of_term' i pr x t =
1.50 + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
1.51 + case t of
1.52 + Free (subst, _) =>
1.53 + (case x of
1.54 + Free (xstr, _) =>
1.55 + if xstr = subst
1.56 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
1.57 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
1.58 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.59 + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
1.60
1.61 -fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.62 - (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1.63 - | term_ord' x pr thy (t, u) =
1.64 - (if pr
1.65 - then
1.66 - let
1.67 - val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.68 - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
1.69 - commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
1.70 - val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
1.71 - commas(map (UnparseC.term_in_thy thy) us) ^ "]\"");
1.72 - val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^
1.73 - string_of_int (size_of_term' x u) ^ ")");
1.74 - val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o (hd_ord x)) (f,g));
1.75 - val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o (terms_ord x) str false) (ts, us));
1.76 - val _ = tracing ("-------");
1.77 - in () end
1.78 - else ();
1.79 - case int_ord (size_of_term' x t, size_of_term' x u) of
1.80 - EQUAL =>
1.81 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u
1.82 - in
1.83 - (case hd_ord x (f, g) of
1.84 - EQUAL => (terms_ord x str pr) (ts, us)
1.85 - | ord => ord)
1.86 - end
1.87 - | ord => ord)
1.88 -and hd_ord x (f, g) = (* ~ term.ML *)
1.89 - prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
1.90 - int_ord (dest_hd' x f, dest_hd' x g)
1.91 -and terms_ord x _ pr (ts, us) =
1.92 - list_ord (term_ord' x pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
1.93 +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.94 + let
1.95 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
1.96 + val ord =
1.97 + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
1.98 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
1.99 + in ord end
1.100 + | term_ord' i pr x _ (t, u) =
1.101 + let
1.102 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
1.103 + val ord =
1.104 + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
1.105 + EQUAL =>
1.106 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
1.107 + in
1.108 + (case hd_ord (i + 1) pr x (f, g) of
1.109 + EQUAL => (terms_ord x (i + 1) pr) (ts, us)
1.110 + | ord => ord)
1.111 + end
1.112 + | ord => ord
1.113 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
1.114 + in ord end
1.115 +and hd_ord i pr x (f, g) = (* ~ term.ML *)
1.116 + let
1.117 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
1.118 + val ord = prod_ord
1.119 + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
1.120 + (dest_hd' x f, dest_hd' x g)
1.121 + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
1.122 + in ord end
1.123 +and terms_ord x i pr (ts, us) =
1.124 + let
1.125 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
1.126 + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
1.127 + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
1.128 + in ord end
1.129
1.130 -in(*local*)
1.131 +(**)in(*local*)
1.132
1.133 fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
1.134 - ((** )tracing ("*** subs variable is: " ^ (Env.subst2str subst)); ( **)
1.135 + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
1.136 case subst of
1.137 - (_, x) :: _ => (term_ord' x pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS)
1.138 + (_, x) :: _ =>
1.139 + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
1.140 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
1.141
1.142 end;(*local*)
2.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Jul 27 12:32:43 2021 +0200
2.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Aug 01 14:39:03 2021 +0200
2.3 @@ -38,8 +38,8 @@
2.4 rules = [(*for rewriting conditions in Thm's*)
2.5 Eval ("Prog_Expr.occurs_in",
2.6 eval_occurs_in "#occurs_in_"),
2.7 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
2.8 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
2.9 + Thm ("not_true", @{thm not_true}),
2.10 + Thm ("not_false", @{thm not_false})],
2.11 scr = Empty_Prog};
2.12 val subs = [(str2t "bdv::real", str2t "x::real")];
2.13 fun rewrit thm str =
2.14 @@ -51,14 +51,14 @@
2.15 "----------- parsing ------------------------------------";
2.16 "----------- parsing ------------------------------------";
2.17 "----------- parsing ------------------------------------";
2.18 -val t = str2t "Integral x D x";
2.19 -val t = str2t "Integral x \<up> 2 D x";
2.20 +val t = TermC.str2term "Integral x D x";
2.21 +val t = TermC.str2term "Integral x \<up> 2 D x";
2.22 case t of
2.23 Const (\<^const_name>\<open>Integral\<close>, _) $
2.24 - (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ Free _) $ Free ("x", _) => ()
2.25 + (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
2.26 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
2.27
2.28 -val t = str2t "ff x is_f_x";
2.29 +val t = TermC.str2term "ff x is_f_x";
2.30 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
2.31 | _ => error "integrate.sml: parsing: ff x is_f_x";
2.32
2.33 @@ -66,26 +66,26 @@
2.34 "----------- integrate by rewriting ---------------------";
2.35 "----------- integrate by rewriting ---------------------";
2.36 "----------- integrate by rewriting ---------------------";
2.37 -val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
2.38 +val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
2.39 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
2.40
2.41 -val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
2.42 +val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral M'/EJ D x");
2.43 if term2s str = "M' / EJ * x" then ()
2.44 else error "Integral M'/EJ D x BY integral_const";
2.45
2.46 -val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
2.47 +val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
2.48 if term2s str = "x \<up> 2 / 2" then ()
2.49 else error "Integral x D x BY integral_var";
2.50
2.51 -val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
2.52 +val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
2.53 if term2s str = "Integral x D x + Integral 1 D x" then ()
2.54 else error "Integral x + 1 D x BY integral_add";
2.55
2.56 -val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x \<up> 3 D x");
2.57 +val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
2.58 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
2.59 else error "Integral M'/EJ * x \<up> 3 D x BY integral_mult";
2.60
2.61 -val str = rewrit @{thm "integral_pow"} (str2t "Integral x \<up> 3 D x");
2.62 +val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
2.63 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
2.64 else error "integrate.sml Integral x \<up> 3 D x";
2.65
2.66 @@ -93,7 +93,7 @@
2.67 "----------- test add_new_c, TermC.is_f_x ---------------------";
2.68 "----------- test add_new_c, TermC.is_f_x ---------------------";
2.69 "----------- test add_new_c, TermC.is_f_x ---------------------";
2.70 -val term = str2t "x \<up> 2 * c + c_2";
2.71 +val term = TermC.str2term "x \<up> 2 * c + c_2";
2.72 val cc = new_c term;
2.73 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
2.74
2.75 @@ -108,7 +108,7 @@
2.76 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
2.77 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
2.78
2.79 -val term = str2t "ff x = x \<up> 2*c + c_2";
2.80 +val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
2.81 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
2.82 if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
2.83 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
2.84 @@ -183,7 +183,7 @@
2.85
2.86 "===== test 2";
2.87 val rls = order_add_mult_in;
2.88 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
2.89 +(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
2.90 assume flawed test setup hidden by "handle _ => ..."
2.91 ERROR ord_make_polynomial_in called with subst = []
2.92 val SOME (t,[]) = rewrite_set_ thy true rls t;
2.93 @@ -193,32 +193,32 @@
2.94
2.95 "===== test 3";
2.96 val rls = discard_parentheses;
2.97 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
2.98 +(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
2.99 assume flawed test setup hidden by "handle _ => ..."
2.100 ERROR ord_make_polynomial_in called with subst = []
2.101 val SOME (t,[]) = rewrite_set_ thy true rls t;
2.102 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
2.103 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
2.104 - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
2.105 + \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*)
2.106
2.107 "===== test 4";
2.108 -val subs = [(str2t "bdv::real", str2t "x::real")];
2.109 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
2.110 val rls =
2.111 (Rule_Set.append_rules "separate_bdv" collect_bdv
2.112 - [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
2.113 + [Thm ("separate_bdv", @{thm separate_bdv}),
2.114 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
2.115 - Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
2.116 + Thm ("separate_bdv_n", @{thm separate_bdv_n}),
2.117 (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)
2.118 - Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
2.119 + Thm ("separate_1_bdv", @{thm separate_1_bdv}),
2.120 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
2.121 - Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})
2.122 + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})
2.123 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
2.124 ]);
2.125 (*show_types := true; --- do we need type-constraint in thms? *)
2.126 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
2.127 @{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*)
2.128 @{thm separate_1_bdv}; (*::?'a*)
2.129 -val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*)
2.130 +val xxx = @{thm separate_1_bdv}; (*::?'a*)
2.131 @{thm separate_1_bdv_n}; (*::real ..because of \<up> *)
2.132 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
2.133
2.134 @@ -227,7 +227,7 @@
2.135 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
2.136
2.137 "===== test 5";
2.138 -val t = str2t "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
2.139 +val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
2.140 val rls = simplify_Integral;
2.141 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
2.142 (* given was: "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
2.143 @@ -237,19 +237,20 @@
2.144 "........... 2nd integral ........................................";
2.145 "........... 2nd integral ........................................";
2.146 "........... 2nd integral ........................................";
2.147 -val t = str2t
2.148 -"Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
2.149 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
2.150 +
2.151 +val thy = @{theory Biegelinie};
2.152 +val t = TermC.str2term
2.153 + "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
2.154 +
2.155 val rls = simplify_Integral;
2.156 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
2.157 -if UnparseC.term t =
2.158 - "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
2.159 +if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
2.160 then () else raise error "integrate.sml, simplify_Integral #198";
2.161
2.162 val rls = integration_rules;
2.163 -val SOME (t,[]) = rewrite_set_ thy true rls t;
2.164 -UnparseC.term t;
2.165 -if UnparseC.term t =
2.166 - "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
2.167 +val SOME (t, []) = rewrite_set_ thy true rls t;
2.168 +if UnparseC.term t = "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
2.169 then () else error "integrate.sml, simplify_Integral #199";
2.170
2.171
2.172 @@ -315,14 +316,13 @@
2.173 "----------- rewrite 3rd integration in 7.27 ------------";
2.174 "----------- rewrite 3rd integration in 7.27 ------------";
2.175 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
2.176 -val t = str2t "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
2.177 -val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;
2.178 +val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
2.179 +val SOME(t, _)= rewrite_set_inst_ thy true subs simplify_Integral t;
2.180 if UnparseC.term t =
2.181 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
2.182 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
2.183
2.184 -val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
2.185 -UnparseC.term t;
2.186 +val SOME(t, _) = rewrite_set_inst_ thy true subs integration t;
2.187 if UnparseC.term t =
2.188 "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
2.189 then () else error "integrate.sml 3rd integration in 7.27, integration";
2.190 @@ -331,6 +331,7 @@
2.191 "----------- check probem type --------------------------";
2.192 "----------- check probem type --------------------------";
2.193 "----------- check probem type --------------------------";
2.194 +val thy = @{theory Integrate};
2.195 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
2.196 Where =[],
2.197 Find =["antiDerivative F_F"],
2.198 @@ -364,14 +365,14 @@
2.199 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
2.200
2.201 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
2.202 - $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
2.203 + $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
2.204 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
2.205 if F1_type = F3_type then ()
2.206 else error "integrate.sml: unequal types in find's";
2.207
2.208 Test_Tool.show_ptyps();
2.209 val pbl = Problem.from_store ["integrate", "function"];
2.210 -case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>,_) $ _) => ()
2.211 +case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
2.212 | _ => error "integrate.sml: Integrate.Integrate ???";
2.213
2.214
2.215 @@ -472,8 +473,7 @@
2.216 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.217 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.218 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.219 -
2.220 -if f2str f = "Q x = c + - 1 * q_0 * x" then()
2.221 +if f2str f = "Q x = c + - q_0 * x" then()
2.222 else error "integrate.sml: method [diff,integration,named] .Q";
2.223
2.224
3.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Jul 27 12:32:43 2021 +0200
3.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sun Aug 01 14:39:03 2021 +0200
3.3 @@ -13,6 +13,7 @@
3.4 "----------- tests on predicates in problems ---------------------";
3.5 "----------- test matching problems ------------------------------";
3.6 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
3.7 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
3.8 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.9 "----------- lin.eq degree_0 -------------------------------------";
3.10 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
3.11 @@ -49,11 +50,11 @@
3.12 "----------- tests on predicates in problems ---------------------";
3.13 "----------- tests on predicates in problems ---------------------";
3.14 "----------- tests on predicates in problems ---------------------";
3.15 -Rewrite.trace_on:=true; (*true false*)
3.16 +Rewrite.trace_on:=false; (*true false*)
3.17
3.18 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
3.19 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
3.20 - if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
3.21 + if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
3.22 else error "polyeq.sml: diff.behav. in lhs";
3.23
3.24 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
3.25 @@ -98,7 +99,7 @@
3.26 if (UnparseC.term t) = "False" then ()
3.27 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
3.28
3.29 - val t5 = (Thm.term_of o the o (TermC.parse thy))
3.30 +val t5 = (Thm.term_of o the o (TermC.parse thy))
3.31 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
3.32 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
3.33 if (UnparseC.term t) = "True" then ()
3.34 @@ -221,6 +222,122 @@
3.35 ##################################################################################*)
3.36
3.37
3.38 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
3.39 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
3.40 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
3.41 +(* termorder hacked by MG, adapted later by WN *)
3.42 +(** )local ( *. for make_polynomial_in .*)
3.43 +
3.44 +open Term; (* for type order = EQUAL | LESS | GREATER *)
3.45 +
3.46 +fun pr_ord EQUAL = "EQUAL"
3.47 + | pr_ord LESS = "LESS"
3.48 + | pr_ord GREATER = "GREATER";
3.49 +
3.50 +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
3.51 + | dest_hd' x (t as Free (a, T)) =
3.52 + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
3.53 + else (((a, 0), T), 1)
3.54 + | dest_hd' _ (Var v) = (v, 2)
3.55 + | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
3.56 + | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
3.57 + | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
3.58 +
3.59 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
3.60 + Free (var, _) $ Free (pot, _)) =
3.61 + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
3.62 + case x of (*WN*)
3.63 + (Free (xstr, _)) =>
3.64 + if xstr = var
3.65 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
3.66 + 1000 * (the (TermC.int_opt_of_string pot)))
3.67 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
3.68 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
3.69 + | size_of_term' i pr x (t as Abs (_, _, body)) =
3.70 + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
3.71 + 1 + size_of_term' (i + 1) pr x body)
3.72 + | size_of_term' i pr x (f $ t) =
3.73 + let
3.74 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
3.75 + val s1 = size_of_term' (i + 1) pr x f
3.76 + val s2 = size_of_term' (i + 1) pr x t
3.77 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
3.78 + in (s1 + s2) end
3.79 + | size_of_term' i pr x t =
3.80 + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
3.81 + case t of
3.82 + Free (subst, _) =>
3.83 + (case x of
3.84 + Free (xstr, _) =>
3.85 + if xstr = subst
3.86 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
3.87 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
3.88 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
3.89 + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
3.90 +
3.91 +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
3.92 + let
3.93 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
3.94 + val ord =
3.95 + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
3.96 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
3.97 + in ord end
3.98 + | term_ord' i pr x _ (t, u) =
3.99 + let
3.100 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
3.101 + val ord =
3.102 + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
3.103 + EQUAL =>
3.104 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
3.105 + in
3.106 + (case hd_ord (i + 1) pr x (f, g) of
3.107 + EQUAL => (terms_ord x (i + 1) pr) (ts, us)
3.108 + | ord => ord)
3.109 + end
3.110 + | ord => ord
3.111 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
3.112 + in ord end
3.113 +and hd_ord i pr x (f, g) = (* ~ term.ML *)
3.114 + let
3.115 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
3.116 + val ord = prod_ord
3.117 + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
3.118 + (dest_hd' x f, dest_hd' x g)
3.119 + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
3.120 + in ord end
3.121 +and terms_ord x i pr (ts, us) =
3.122 + let
3.123 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
3.124 + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
3.125 + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
3.126 + in ord end
3.127 +
3.128 +(** )in( *local*)
3.129 +
3.130 +fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
3.131 + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
3.132 + case subst of
3.133 + (_, x) :: _ =>
3.134 + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
3.135 + | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
3.136 +
3.137 +(** )end;( *local*)
3.138 +
3.139 +\<close> ML \<open>
3.140 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
3.141 +if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
3.142 +
3.143 +val x = TermC.str2term "x ::real";
3.144 +
3.145 +val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
3.146 +if 2006 = size_of_term' 1 true x t1
3.147 +then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
3.148 +
3.149 +val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
3.150 +if 3004 = size_of_term' 1 true x t2
3.151 +then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
3.152 +
3.153 +
3.154 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.155 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.156 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.157 @@ -271,14 +388,14 @@
3.158 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
3.159 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
3.160 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
3.161 -if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
3.162 +if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
3.163 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
3.164
3.165 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
3.166 -if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
3.167 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
3.168 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
3.169
3.170 - val ttt' = "(3*x + 5)/18";
3.171 + val ttt' = "(3*x + 5)/18 ::real";
3.172 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
3.173 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
3.174 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
3.175 @@ -288,7 +405,6 @@
3.176 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
3.177 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
3.178 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
3.179 -============ inhibit exn WN120316 ==============================================*)
3.180
3.181
3.182 "----------- lin.eq degree_0 -------------------------------------";
4.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Jul 27 12:32:43 2021 +0200
4.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Aug 01 14:39:03 2021 +0200
4.3 @@ -302,7 +302,7 @@
4.4 ML_file "Knowledge/trig.sml"
4.5 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
4.6 ML_file "Knowledge/diff.sml"
4.7 -(*ML_file "Knowledge/integrate.sml" rls simplify_Integral broken | in Test_Some.thy*)
4.8 + ML_file "Knowledge/integrate.sml"
4.9 (*ML_file "Knowledge/eqsystem.sml" simplify_System_parenthesized \<longrightarrow> - 0 + c_4 | in Test_Some.thy*)
4.10 ML_file "Knowledge/test.sml"
4.11 ML_file "Knowledge/polyminus.sml"
5.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 27 12:32:43 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Sun Aug 01 14:39:03 2021 +0200
5.3 @@ -108,8 +108,10 @@
5.4 \<close> ML \<open>
5.5 \<close>
5.6
5.7 +(** )ML_file \<open>Knowledge/polyeq-1.sml\<close>( **)
5.8 section \<open>======== check Knowledge/polyeq-1.sml =============================================\<close>
5.9 ML \<open>
5.10 +\<close> text \<open> =======-------------------------vvv polyeq-1.sml-------TOODOO----------------
5.11 \<close> ML \<open>
5.12 (* Title: Knowledge/polyeq-1.sml
5.13 testexamples for PolyEq, poynomial equations and equational systems
5.14 @@ -126,6 +128,7 @@
5.15 "----------- tests on predicates in problems ---------------------";
5.16 "----------- test matching problems ------------------------------";
5.17 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
5.18 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
5.19 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
5.20 "----------- lin.eq degree_0 -------------------------------------";
5.21 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
5.22 @@ -163,6 +166,8 @@
5.23 "----------- tests on predicates in problems ---------------------";
5.24 "----------- tests on predicates in problems ---------------------";
5.25 "----------- tests on predicates in problems ---------------------";
5.26 +Rewrite.trace_on:=false; (*true false*)
5.27 +
5.28 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
5.29 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
5.30 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
5.31 @@ -198,12 +203,9 @@
5.32 if (UnparseC.term t) = "True" then ()
5.33 else error "polyeq.sml: diff.behav. in has_degree_in_in";
5.34
5.35 -\<close> ML \<open>
5.36 +\<close> text \<open> (*TOODOO broken by repair ord_make_polynomial_in*)
5.37 val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
5.38 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
5.39 -\<close> ML \<open>
5.40 -UnparseC.term t = "- 1 = 2";
5.41 -\<close> text \<open> (*"((sqrt(x)) has_degree_in x) = 2" --- = "- 1 = 2" START HERE*)
5.42 + val SOME (t,_) = rewrite_set_ @ {theory PolyEq} false PolyEq_prls t3;
5.43 if (UnparseC.term t) = "False" then ()
5.44 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
5.45
5.46 @@ -276,7 +278,7 @@
5.47 "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
5.48
5.49 (*das rewriting l"asst sich beobachten mit
5.50 -Rewrite.trace_on := false; (*true false*)
5.51 +Rewrite.trace_on := false; (*true false*)
5.52 *)
5.53
5.54 "------ 15.11.02 --------------------------";
5.55 @@ -284,7 +286,7 @@
5.56 val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
5.57 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
5.58
5.59 -Rewrite.trace_on := false; (*true false*)
5.60 +Rewrite.trace_on := false; (*true false*)
5.61 (* Anwenden einer Regelmenge aus Termorder.ML: *)
5.62 val SOME (t,_) =
5.63 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
5.64 @@ -339,6 +341,125 @@
5.65
5.66
5.67 \<close> ML \<open>
5.68 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
5.69 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
5.70 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
5.71 +(* termorder hacked by MG, adapted later by WN *)
5.72 +(** )local ( *. for make_polynomial_in .*)
5.73 +
5.74 +open Term; (* for type order = EQUAL | LESS | GREATER *)
5.75 +
5.76 +fun pr_ord EQUAL = "EQUAL"
5.77 + | pr_ord LESS = "LESS"
5.78 + | pr_ord GREATER = "GREATER";
5.79 +
5.80 +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
5.81 + | dest_hd' x (t as Free (a, T)) =
5.82 + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
5.83 + else (((a, 0), T), 1)
5.84 + | dest_hd' _ (Var v) = (v, 2)
5.85 + | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
5.86 + | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
5.87 + | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
5.88 +
5.89 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
5.90 + Free (var, _) $ Free (pot, _)) =
5.91 + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
5.92 + case x of (*WN*)
5.93 + (Free (xstr, _)) =>
5.94 + if xstr = var
5.95 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
5.96 + 1000 * (the (TermC.int_opt_of_string pot)))
5.97 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
5.98 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
5.99 + | size_of_term' i pr x (t as Abs (_, _, body)) =
5.100 + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
5.101 + 1 + size_of_term' (i + 1) pr x body)
5.102 + | size_of_term' i pr x (f $ t) =
5.103 + let
5.104 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
5.105 + val s1 = size_of_term' (i + 1) pr x f
5.106 + val s2 = size_of_term' (i + 1) pr x t
5.107 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
5.108 + in (s1 + s2) end
5.109 + | size_of_term' i pr x t =
5.110 + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
5.111 + case t of
5.112 + Free (subst, _) =>
5.113 + (case x of
5.114 + Free (xstr, _) =>
5.115 + if xstr = subst
5.116 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
5.117 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
5.118 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
5.119 + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
5.120 +
5.121 +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
5.122 + let
5.123 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
5.124 + val ord =
5.125 + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
5.126 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
5.127 + in ord end
5.128 + | term_ord' i pr x _ (t, u) =
5.129 + let
5.130 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
5.131 + val ord =
5.132 + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
5.133 + EQUAL =>
5.134 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
5.135 + in
5.136 + (case hd_ord (i + 1) pr x (f, g) of
5.137 + EQUAL => (terms_ord x (i + 1) pr) (ts, us)
5.138 + | ord => ord)
5.139 + end
5.140 + | ord => ord
5.141 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
5.142 + in ord end
5.143 +and hd_ord i pr x (f, g) = (* ~ term.ML *)
5.144 + let
5.145 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
5.146 + val ord = prod_ord
5.147 + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
5.148 + (dest_hd' x f, dest_hd' x g)
5.149 + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
5.150 + in ord end
5.151 +and terms_ord x i pr (ts, us) =
5.152 + let
5.153 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
5.154 + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
5.155 + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
5.156 + in ord end
5.157 +
5.158 +(** )in( *local*)
5.159 +
5.160 +fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
5.161 + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
5.162 + case subst of
5.163 + (_, x) :: _ =>
5.164 + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
5.165 + | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
5.166 +
5.167 +(** )end;( *local*)
5.168 +
5.169 +\<close> ML \<open>
5.170 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
5.171 +if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
5.172 +
5.173 +val x = TermC.str2term "x ::real";
5.174 +
5.175 +\<close> ML \<open>
5.176 +val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
5.177 +if 2006 = size_of_term' 1 true x t1
5.178 +then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
5.179 +
5.180 +\<close> ML \<open>
5.181 +val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
5.182 +if 3004 = size_of_term' 1 true x t2
5.183 +then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
5.184 +
5.185 +
5.186 +\<close> ML \<open>
5.187 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
5.188 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
5.189 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
5.190 @@ -351,6 +472,7 @@
5.191 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
5.192 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
5.193
5.194 +\<close> ML \<open>
5.195 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
5.196 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
5.197
5.198 @@ -370,6 +492,7 @@
5.199 ord_make_polynomial_in true thy substa (aa, bb);
5.200 false; (* => GREATER *)
5.201
5.202 +\<close> ML \<open>
5.203 (* und nach dem Re-engineering der Termorders in den 'rulesets'
5.204 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
5.205 val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
5.206 @@ -386,12 +509,13 @@
5.207 if UnparseC.term t' = "a + b + x" then ()
5.208 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
5.209
5.210 +\<close> ML \<open>
5.211 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
5.212 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
5.213 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
5.214 -
5.215 -UnparseC.term t' = "- 6 + - (5 * x) + x \<up> 3 + - (x \<up> 2) + - (x \<up> 3) +\n- (14 * x \<up> 2)"
5.216 -\<close> text \<open> (* TODO.ThmC.numerals_to_Free termorder.sml diff.behav ord_make_polynomial_in*)
5.217 +\<close> ML \<open>
5.218 +UnparseC.term t' = "- 6 + - (5 * x) + - (15 * x \<up> 2) + 0"
5.219 +\<close> text \<open> (*TOODOO broken by repair ord_make_polynomial_in*)
5.220 if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
5.221 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
5.222
5.223 @@ -399,17 +523,17 @@
5.224 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
5.225 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
5.226
5.227 - val ttt' = "(3*x + 5)/18";
5.228 +\<close> ML \<open>
5.229 + val ttt' = "(3*x + 5)/18 ::real";
5.230 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
5.231 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
5.232 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
5.233 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
5.234
5.235 -(*============ inhibit exn WN120316 ==============================================
5.236 +\<close> ML \<open>
5.237 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
5.238 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
5.239 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
5.240 -============ inhibit exn WN120316 ==============================================*)
5.241
5.242
5.243 \<close> ML \<open>
5.244 @@ -449,7 +573,8 @@
5.245 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
5.246 ============ inhibit exn WN110914 ============================================*)
5.247
5.248 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 4 = - 1 / 4" z =
5.249 +\<close> text \<open>
5.250 +(*rewrite_set_, rewrite_ "- 1 / 4 = - 1 / 4" z =
5.251 - 1 * (- 1 / 4 / 2) + sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2 \<or>
5.252 z =
5.253 - 1 * (- 1 / 4 / 2) + - 1 * (sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2) = NONE*)
5.254 @@ -484,6 +609,8 @@
5.255 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
5.256
5.257 \<close> ML \<open>
5.258 +Rewrite.trace_on := false; (*true false*)
5.259 +\<close> ML \<open>
5.260 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
5.261 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
5.262 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
5.263 @@ -532,7 +659,9 @@
5.264 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
5.265
5.266
5.267 -\<close> text \<open> (*see TOODOO.1*)
5.268 +\<close> text \<open> (*see TOODOO.1
5.269 +exception TYPE raised (line 169 of "consts.ML"): Illegal type for constant "HOL.eq" :: real
5.270 + \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool*)
5.271 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
5.272 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
5.273 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
5.274 @@ -1156,534 +1285,10 @@
5.275 *)
5.276
5.277 \<close> ML \<open>
5.278 -\<close> text \<open> (*-------^^^^^ polyeq-1.sml------------vvv diff.sml-------TOODOO----------------*)
5.279 +\<close> text \<open> =======^^^^^ polyeq-1.sml------------vvv eqsystem.sml--------TOODOO-----------
5.280 \<close>
5.281
5.282 -section \<open>======== check Knowledge/integrate.sml ============================================\<close>
5.283 -ML \<open>
5.284 -\<close> ML \<open>
5.285 -(* Title: test/Tools/isac/Knowledge/integrate.sml
5.286 - Author: Walther Neuper 050826
5.287 - (c) due to copyright terms
5.288 -*)
5.289 -"--------------------------------------------------------";
5.290 -"table of contents --------------------------------------";
5.291 -"--------------------------------------------------------";
5.292 -"----------- parsing ------------------------------------";
5.293 -"----------- integrate by rewriting ---------------------";
5.294 -"----------- test add_new_c, TermC.is_f_x ---------------------";
5.295 -"----------- simplify by ruleset reducing make_ratpoly_in";
5.296 -"----------- integrate by ruleset -----------------------";
5.297 -"----------- rewrite 3rd integration in 7.27 ------------";
5.298 -"----------- check probem type --------------------------";
5.299 -"----------- me method [diff,integration] ---------------";
5.300 -"----------- autoCalculate [diff,integration] -----------";
5.301 -"----------- me method [diff,integration,named] ---------";
5.302 -"----------- me met [diff,integration,named] Biegelinie.Q";
5.303 -"----------- method analog to rls 'integration' ---------";
5.304 -"--------------------------------------------------------";
5.305 -"--------------------------------------------------------";
5.306 -"--------------------------------------------------------";
5.307 -
5.308 -(*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
5.309 -they are used several times below; TODO remove duplicates*)
5.310 -val thy = @{theory "Integrate"};
5.311 -val ctxt = ThyC.to_ctxt thy;
5.312 -
5.313 -fun str2t str = parseNEW ctxt str |> the;
5.314 -fun term2s t = UnparseC.term_in_ctxt ctxt t;
5.315 -
5.316 -val conditions_in_integration_rules =
5.317 - Rule_Set.Repeat {id="conditions_in_integration_rules",
5.318 - preconds = [],
5.319 - rew_ord = ("termlessI",termlessI),
5.320 - erls = Rule_Set.Empty,
5.321 - srls = Rule_Set.Empty, calc = [], errpatts = [],
5.322 - rules = [(*for rewriting conditions in Thm's*)
5.323 - Eval ("Prog_Expr.occurs_in",
5.324 - eval_occurs_in "#occurs_in_"),
5.325 - Thm ("not_true", @{thm not_true}),
5.326 - Thm ("not_false", @{thm not_false})],
5.327 - scr = Empty_Prog};
5.328 -val subs = [(str2t "bdv::real", str2t "x::real")];
5.329 -\<close> ML \<open>
5.330 -fun rewrit thm str =
5.331 - fst (the (rewrite_inst_ thy tless_true
5.332 - conditions_in_integration_rules
5.333 - true subs thm str));
5.334 -
5.335 -
5.336 -\<close> ML \<open>
5.337 -"----------- parsing ------------------------------------";
5.338 -"----------- parsing ------------------------------------";
5.339 -"----------- parsing ------------------------------------";
5.340 -val t = TermC.str2term "Integral x D x";
5.341 -val t = TermC.str2term "Integral x \<up> 2 D x";
5.342 -case t of
5.343 - Const (\<^const_name>\<open>Integral\<close>, _) $
5.344 - (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
5.345 - | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
5.346 -
5.347 -val t = TermC.str2term "ff x is_f_x";
5.348 -case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
5.349 - | _ => error "integrate.sml: parsing: ff x is_f_x";
5.350 -
5.351 -
5.352 -\<close> ML \<open>
5.353 -"----------- integrate by rewriting ---------------------";
5.354 -"----------- integrate by rewriting ---------------------";
5.355 -"----------- integrate by rewriting ---------------------";
5.356 -val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
5.357 -if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
5.358 -
5.359 -val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral M'/EJ D x");
5.360 -if term2s str = "M' / EJ * x" then ()
5.361 -else error "Integral M'/EJ D x BY integral_const";
5.362 -
5.363 -val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
5.364 -if term2s str = "x \<up> 2 / 2" then ()
5.365 -else error "Integral x D x BY integral_var";
5.366 -
5.367 -val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
5.368 -if term2s str = "Integral x D x + Integral 1 D x" then ()
5.369 -else error "Integral x + 1 D x BY integral_add";
5.370 -
5.371 -val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
5.372 -if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
5.373 -else error "Integral M'/EJ * x \<up> 3 D x BY integral_mult";
5.374 -
5.375 -val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
5.376 -if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
5.377 -else error "integrate.sml Integral x \<up> 3 D x";
5.378 -
5.379 -
5.380 -\<close> ML \<open>
5.381 -"----------- test add_new_c, TermC.is_f_x ---------------------";
5.382 -"----------- test add_new_c, TermC.is_f_x ---------------------";
5.383 -"----------- test add_new_c, TermC.is_f_x ---------------------";
5.384 -val term = TermC.str2term "x \<up> 2 * c + c_2";
5.385 -val cc = new_c term;
5.386 -if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
5.387 -
5.388 -val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term thy;
5.389 -if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
5.390 -else error "intergrate.sml: diff. eval_add_new_c";
5.391 -
5.392 -val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_");
5.393 -val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
5.394 -
5.395 -val SOME (t',_) = rewrite_set_ thy true add_new_c term;
5.396 -if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
5.397 -else error "intergrate.sml: diff. rewrite_set add_new_c 1";
5.398 -
5.399 -val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
5.400 -val SOME (t',_) = rewrite_set_ thy true add_new_c term;
5.401 -if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
5.402 -else error "intergrate.sml: diff. rewrite_set add_new_c 2";
5.403 -
5.404 -
5.405 -(*WN080222 replace call_new_c with add_new_c----------------------
5.406 -val term = str2t "new_c (c * x \<up> 2 + c_2)";
5.407 -val SOME (_,t') = eval_new_c 0 0 term 0;
5.408 -if term2s t' = "new_c c * x \<up> 2 + c_2 = c_3" then ()
5.409 -else error "integrate.sml: eval_new_c ???";
5.410 -
5.411 -val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2)";
5.412 -val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
5.413 -if term2s t' = "matches (?u + new_c ?v) (x \<up> 2 / 2) = False" then ()
5.414 -else error "integrate.sml: matches new_c = False";
5.415 -
5.416 -val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2)";
5.417 -val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
5.418 -if term2s t'="matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2) = True"
5.419 -then () else error "integrate.sml: matches new_c = True";
5.420 -
5.421 -val t = str2t "ff x TermC.is_f_x";
5.422 -val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
5.423 -if term2s t' = "(ff x TermC.is_f_x) = True" then ()
5.424 -else error "integrate.sml: eval_is_f_x --> true";
5.425 -
5.426 -val t = str2t "q_0/2 * L * x TermC.is_f_x";
5.427 -val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
5.428 -if term2s t' = "(q_0 / 2 * L * x TermC.is_f_x) = False" then ()
5.429 -else error "integrate.sml: eval_is_f_x --> false";
5.430 -
5.431 -val conditions_in_integration =
5.432 -Rule_Set.Repeat {id="conditions_in_integration",
5.433 - preconds = [],
5.434 - rew_ord = ("termlessI",termlessI),
5.435 - erls = Rule_Set.Empty,
5.436 - srls = Rule_Set.Empty, calc = [], errpatts = [],
5.437 - rules = [Eval ("Prog_Expr.matches",eval_matches ""),
5.438 - Eval ("Integrate.is_f_x",
5.439 - eval_is_f_x "is_f_x_"),
5.440 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
5.441 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
5.442 - ],
5.443 - scr = Empty_Prog};
5.444 -fun rewrit thm t =
5.445 - fst (the (rewrite_inst_ thy tless_true
5.446 - conditions_in_integration true subs thm t));
5.447 -val t = rewrit call_for_new_c (str2t "x \<up> 2 / 2"); term2s t;
5.448 -val t = (rewrit call_for_new_c t)
5.449 - handle OPTION => str2t "no_rewrite";
5.450 -
5.451 -val t = rewrit call_for_new_c
5.452 - (str2t "ff x = q_0/2 *L*x"); term2s t;
5.453 -val t = (rewrit call_for_new_c
5.454 - (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
5.455 - handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
5.456 ---------------------------------------------------------------------*)
5.457 -
5.458 -
5.459 -\<close> text \<open>(* broken with repair /sym_/real_mult_minus1+sym *)
5.460 -"----------- simplify by ruleset reducing make_ratpoly_in";
5.461 -"----------- simplify by ruleset reducing make_ratpoly_in";
5.462 -"----------- simplify by ruleset reducing make_ratpoly_in";
5.463 -val thy = @ {theory "Isac_Knowledge"};
5.464 -"===== test 1";
5.465 -val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
5.466 -
5.467 -"----- stepwise from the rulesets in simplify_Integral and below-----";
5.468 -val rls = norm_Rational_noadd_fractions;
5.469 -case rewrite_set_inst_ thy true subs rls t of
5.470 - SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
5.471 - | NONE => ();
5.472 -
5.473 -"===== test 2";
5.474 -val rls = order_add_mult_in;
5.475 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
5.476 - assume flawed test setup hidden by "handle _ => ..."
5.477 - ERROR ord_make_polynomial_in called with subst = []
5.478 -val SOME (t,[]) = rewrite_set_ thy true rls t;
5.479 -if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then()
5.480 -else error "integrate.sml simplify by ruleset order_add_mult_in #2";
5.481 - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
5.482 -
5.483 -"===== test 3";
5.484 -val rls = discard_parentheses;
5.485 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
5.486 - assume flawed test setup hidden by "handle _ => ..."
5.487 - ERROR ord_make_polynomial_in called with subst = []
5.488 -val SOME (t,[]) = rewrite_set_ thy true rls t;
5.489 -if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
5.490 -else error "integrate.sml simplify by ruleset discard_parenth.. #3";
5.491 - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
5.492 -
5.493 -"===== test 4";
5.494 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
5.495 -val rls =
5.496 - (Rule_Set.append_rules "separate_bdv" collect_bdv
5.497 - [Thm ("separate_bdv", @{thm separate_bdv}),
5.498 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
5.499 - Thm ("separate_bdv_n", @{thm separate_bdv_n}),
5.500 - (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)
5.501 - Thm ("separate_1_bdv", @{thm separate_1_bdv}),
5.502 - (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
5.503 - Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})
5.504 - (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
5.505 - ]);
5.506 -(*show_types := true; --- do we need type-constraint in thms? *)
5.507 -@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
5.508 -@{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*)
5.509 -@{thm separate_1_bdv}; (*::?'a*)
5.510 -val xxx = @{thm separate_1_bdv}; (*::?'a*)
5.511 -@{thm separate_1_bdv_n}; (*::real ..because of \<up> *)
5.512 -(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
5.513 -
5.514 -val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
5.515 -if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
5.516 -else error "integrate.sml simplify by ruleset separate_bdv.. #4";
5.517 -
5.518 -"===== test 5";
5.519 -val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
5.520 -val rls = simplify_Integral;
5.521 -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
5.522 -(* given was: "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
5.523 -if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
5.524 -else error "integrate.sml, simplify_Integral #99";
5.525 -
5.526 -\<close> ML \<open>
5.527 -"........... 2nd integral ........................................";
5.528 -"........... 2nd integral ........................................";
5.529 -"........... 2nd integral ........................................";
5.530 -val thy = @{theory Biegelinie};
5.531 -val t = TermC.str2term
5.532 - "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
5.533 -
5.534 -val rls = simplify_Integral;
5.535 -(*TOODOO simplify_Integral broken (required for Biegelinie) ---------------------------------\\
5.536 - "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
5.537 -\<down> "Integral 1 / EI * ((L * q_0 / 4) * x \<up> 2 + (- 1 * q_0 / 6) * x \<up> 3) D x" broken
5.538 -(**)
5.539 -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
5.540 -if UnparseC.term t =
5.541 - "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
5.542 -then () else raise error "integrate.sml, simplify_Integral #198";
5.543 -
5.544 -val rls = integration_rules;
5.545 -val SOME (t,[]) = rewrite_set_ thy true rls t;
5.546 -UnparseC.term t;
5.547 -if UnparseC.term t =
5.548 - "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
5.549 -then () else error "integrate.sml, simplify_Integral #199";
5.550 --------------------------------------------------------------------------------------------//*)
5.551 -
5.552 -
5.553 -\<close> ML \<open>
5.554 -"----------- integrate by ruleset -----------------------";
5.555 -"----------- integrate by ruleset -----------------------";
5.556 -"----------- integrate by ruleset -----------------------";
5.557 -val thy = @{theory "Integrate"};
5.558 -val rls = integration_rules;
5.559 -val subs = [(@{term "bdv::real"}, @{term "x::real"})];
5.560 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.561 -
5.562 -\<close> ML \<open>
5.563 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";
5.564 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.565 -if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
5.566 -
5.567 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
5.568 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.569 -if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
5.570 -
5.571 -\<close> ML \<open>
5.572 -val rls = add_new_c;
5.573 -val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";
5.574 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.575 -if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
5.576 -else error "integrate.sml: diff.behav. in add_new_c simpl.";
5.577 -
5.578 -\<close> ML \<open>
5.579 -val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";
5.580 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.581 -if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
5.582 -else error "integrate.sml: diff.behav. in add_new_c equation";
5.583 -
5.584 -\<close> ML \<open>
5.585 -val rls = simplify_Integral;
5.586 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.587 -val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
5.588 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.589 -if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
5.590 -then () else error "integrate.sml: diff.behav. in simplify_I #1";
5.591 -
5.592 -\<close> ML \<open>
5.593 -val rls = integration;
5.594 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.595 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
5.596 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.597 -if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
5.598 -then () else error "integrate.sml: diff.behav. in integration #1";
5.599 -
5.600 -\<close> ML \<open>
5.601 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";
5.602 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.603 -if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
5.604 -else error "integrate.sml: diff.behav. in integration #2";
5.605 -
5.606 -\<close> text \<open> (*TOODOO rls "integration" does NOT work anymore *)
5.607 -val t = (Thm.term_of o the o (TermC.parse thy))
5.608 - "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
5.609 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.610 -"Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
5.611 -if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
5.612 -then () else error "integrate.sml: diff.behav. in integration #3";
5.613 -
5.614 -\<close> text \<open> (*TOODOO rls "integration" does NOT work anymore *)
5.615 -val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
5.616 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
5.617 -if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
5.618 -then () else error "integrate.sml: diff.behav. in integration #4";
5.619 -
5.620 -\<close> ML \<open>
5.621 -"----------- rewrite 3rd integration in 7.27 ------------";
5.622 -"----------- rewrite 3rd integration in 7.27 ------------";
5.623 -"----------- rewrite 3rd integration in 7.27 ------------";
5.624 -val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
5.625 -val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
5.626 -val SOME(t, _)= rewrite_set_inst_ thy true subs simplify_Integral t;
5.627 -\<close> ML \<open>
5.628 -UnparseC.term t =
5.629 - "Integral 1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2) D x";
5.630 -(*TOODOO simplify_Integral NOW weaker *)
5.631 -\<close> text \<open> (* TOODOO rls simplify_Integral <------------------------------ START HERE *)
5.632 -if UnparseC.term t =
5.633 - "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
5.634 -then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
5.635 -
5.636 -\<close> ML \<open>
5.637 -val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
5.638 -\<close> ML \<open>
5.639 -UnparseC.term t =
5.640 - "c + Integral 1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2) D x";
5.641 -\<close> text \<open> (*TOODOO thus rls "integration" does NOT work anymore *)
5.642 -if UnparseC.term t =
5.643 - "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
5.644 -then () else error "integrate.sml 3rd integration in 7.27, integration";
5.645 -
5.646 -
5.647 -\<close> ML \<open>
5.648 -"----------- check probem type --------------------------";
5.649 -"----------- check probem type --------------------------";
5.650 -"----------- check probem type --------------------------";
5.651 -val thy = @{theory Integrate};
5.652 -val model = {Given =["functionTerm f_f", "integrateBy v_v"],
5.653 - Where =[],
5.654 - Find =["antiDerivative F_F"],
5.655 - With =[],
5.656 - Relate=[]}:string ppc;
5.657 -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
5.658 -val t1 = (Thm.term_of o hd) chkmodel;
5.659 -val t2 = (Thm.term_of o hd o tl) chkmodel;
5.660 -val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
5.661 -case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
5.662 - | _ => error "integrate.sml: Integrate.antiDerivative ???";
5.663 -
5.664 -\<close> ML \<open>
5.665 -val model = {Given =["functionTerm f_f", "integrateBy v_v"],
5.666 - Where =[],
5.667 - Find =["antiDerivativeName F_F"],
5.668 - With =[],
5.669 - Relate=[]}:string ppc;
5.670 -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
5.671 -val t1 = (Thm.term_of o hd) chkmodel;
5.672 -val t2 = (Thm.term_of o hd o tl) chkmodel;
5.673 -val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
5.674 -case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
5.675 - | _ => error "integrate.sml: Integrate.antiDerivativeName";
5.676 -
5.677 -\<close> ML \<open>
5.678 -"----- compare 'Find's from problem, script, formalization -------";
5.679 -val {ppc,...} = Problem.from_store ["named", "integrate", "function"];
5.680 -val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
5.681 - F1_ as Free ("F_F", F1_type))) = last_elem ppc;
5.682 -val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
5.683 -val [_,_, F2_] = formal_args sc;
5.684 -if F1_ = F2_ then () else error "integrate.sml: unequal find's";
5.685 -
5.686 -val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
5.687 - $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
5.688 -if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
5.689 -if F1_type = F3_type then ()
5.690 -else error "integrate.sml: unequal types in find's";
5.691 -
5.692 -Test_Tool.show_ptyps();
5.693 -val pbl = Problem.from_store ["integrate", "function"];
5.694 -case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
5.695 - | _ => error "integrate.sml: Integrate.Integrate ???";
5.696 -
5.697 -
5.698 -\<close> ML \<open>
5.699 -"----------- me method [diff,integration] ---------------";
5.700 -"----------- me method [diff,integration] ---------------";
5.701 -"----------- me method [diff,integration] ---------------";
5.702 -(*exp_CalcInt_No- 1.xml*)
5.703 -val p = e_pos'; val c = [];
5.704 -"----- step 0: returns nxt = Model_Problem ---";
5.705 -val (p,_,f,nxt,_,pt) =
5.706 - CalcTreeTEST
5.707 - [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
5.708 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
5.709 -"----- step 1: returns nxt = Add_Given \"functionTerm (x \<up> 2 + 1)\" ---";
5.710 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
5.711 -"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
5.712 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.713 -"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
5.714 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.715 -"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
5.716 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.717 -"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
5.718 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.719 -"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
5.720 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.721 -"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
5.722 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.723 -case nxt of (Apply_Method ["diff", "integration"]) => ()
5.724 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
5.725 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
5.726 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.727 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.728 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.729 -if f2str f = "c + x + 1 / 3 * x \<up> 3" then ()
5.730 -else error "integrate.sml -- me method [diff,integration] -- end";
5.731 -
5.732 -
5.733 -\<close> ML \<open>
5.734 -"----------- autoCalculate [diff,integration] -----------";
5.735 -"----------- autoCalculate [diff,integration] -----------";
5.736 -"----------- autoCalculate [diff,integration] -----------";
5.737 -reset_states ();
5.738 -CalcTree
5.739 - [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
5.740 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
5.741 -Iterator 1;
5.742 -moveActiveRoot 1;
5.743 -autoCalculate 1 CompleteCalc;
5.744 -val ((pt,p),_) = get_calc 1; @{make_string} p; Test_Tool.show_pt pt;
5.745 -val (Form t,_,_) = ME_Misc.pt_extract (pt, p);
5.746 -if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()
5.747 -else error "integrate.sml -- interSteps [diff,integration] -- result";
5.748 -
5.749 -
5.750 -\<close> ML \<open>
5.751 -"----------- me method [diff,integration,named] ---------";
5.752 -"----------- me method [diff,integration,named] ---------";
5.753 -"----------- me method [diff,integration,named] ---------";
5.754 -(*exp_CalcInt_No- 2.xml*)
5.755 -val fmz = ["functionTerm (x \<up> 2 + (1::real))",
5.756 - "integrateBy x", "antiDerivativeName F"];
5.757 -val (dI',pI',mI') =
5.758 - ("Integrate",["named", "integrate", "function"],
5.759 - ["diff", "integration", "named"]);
5.760 -val p = e_pos'; val c = [];
5.761 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.762 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.763 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.764 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
5.765 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.766 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.767 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.768 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
5.769 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.770 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.771 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.772 -if f2str f = "F x = c + x + 1 / 3 * x \<up> 3" then()
5.773 -else error "integrate.sml: method [diff,integration,named]";
5.774 -
5.775 -
5.776 -\<close> ML \<open>
5.777 -"----------- me met [diff,integration,named] Biegelinie.Q";
5.778 -"----------- me met [diff,integration,named] Biegelinie.Q";
5.779 -"----------- me met [diff,integration,named] Biegelinie.Q";
5.780 -(*exp_CalcInt_No-3.xml*)
5.781 -val fmz = ["functionTerm (- q_0)",
5.782 - "integrateBy x", "antiDerivativeName Q"];
5.783 -val (dI',pI',mI') =
5.784 - ("Biegelinie",["named", "integrate", "function"],
5.785 - ["diff", "integration", "named"]);
5.786 -val p = e_pos'; val c = [];
5.787 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.788 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.789 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.790 -(*Error Tac Q not in ...*)
5.791 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
5.792 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.793 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.794 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.795 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
5.796 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.797 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.798 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.799 -if f2str f = "Q x = c + - q_0 * x" then()
5.800 -else error "integrate.sml: method [diff,integration,named] .Q";
5.801 -
5.802 -
5.803 -\<close> ML \<open>
5.804 -\<close> text \<open> (*-------^^^^^ integrate.sml------------vvv eqsystem.sml--------TOODOO-----------*)
5.805 -\<close>
5.806 -
5.807 +(** )ML_file \<open>Knowledge/eqsystem.sml\<close>( **)
5.808 section \<open>======== check Knowledge/eqsystem.sml =============================================\<close>
5.809 ML \<open>
5.810 \<close> ML \<open>
5.811 @@ -2695,6 +2300,7 @@
5.812 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.813
5.814 ---------------------------------------------------------------------*)
5.815 +\<close> text \<open> =======^^^^^ eqsystem.sml-----------------------------------TOODOO----------------
5.816 \<close> ML \<open>
5.817 \<close> ML \<open>
5.818 \<close>