1.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Mar 07 17:22:20 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Mar 07 17:29:30 2019 +0100
1.3 @@ -48,9 +48,11 @@
1.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.5 val vals_of_oris : Model.ori list -> term list
1.6 val is_error : Model.itm_ -> bool
1.7 + val is_copy_named_idstr : string -> bool
1.8 + val is_copy_named_generating_idstr : string -> bool
1.9 + val is_copy_named_generating : 'a * ('b * term) -> bool
1.10 val is_copy_named : 'a * ('b * term) -> bool
1.11 val ori2Coritm : Celem.pat list -> Model.ori -> Model.itm
1.12 - val is_copy_named_idstr : string -> bool
1.13 val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
1.14 val mtc : theory -> Celem.pat -> term -> Model.preori option
1.15 val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori
1.16 @@ -246,9 +248,9 @@
1.17 end
1.18 | nxt_add thy oris _ itms =
1.19 let
1.20 - fun testr_vt v ori = member op= (#2 ori) v andalso (#3 ori) <> "#undef"
1.21 - fun testi_vt v itm = member op= (#2 itm) v
1.22 - fun test_id ids r = member op= ids (#1 r)
1.23 + fun testr_vt v ori = member op= (#2 (ori : Model.ori)) v andalso (#3 ori) <> "#undef"
1.24 + fun testi_vt v itm = member op= (#2 (itm : Model.itm)) v
1.25 + fun test_id ids r = member op= ids (#1 (r : Model.ori))
1.26 fun test_subset itm (_, _, _, d, ts) =
1.27 (Model.d_in (#5 (itm: Model.itm))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
1.28 fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false
1.29 @@ -543,9 +545,9 @@
1.30 let fun sel (_,_,d,ts) = Model.comp_ts (d, ts)
1.31 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
1.32 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
1.33 - val vars' = map (TermC.free2str o snd o snd) pbt (*cpy-nam filtered_out*)
1.34 + val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
1.35 val vals = map sel oris
1.36 - val cy_ext = (TermC.free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
1.37 + val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
1.38 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
1.39 else ([1], field, dsc, [t])
1.40 ) handle _ => error ("cpy_nam: for "^ Rule.term2str t)
2.1 --- a/src/Tools/isac/Interpret/script.sml Thu Mar 07 17:22:20 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Mar 07 17:29:30 2019 +0100
2.3 @@ -1023,7 +1023,7 @@
2.4 (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
2.5 | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)
2.6 nstep_up thy ptp scr E l ay a v
2.7 - | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq",_) $ _) a v = (*comes from e1*)
2.8 + | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)
2.9 if ay = Napp_
2.10 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
2.11 else (*Skip_*)
3.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 07 17:22:20 2019 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 07 17:29:30 2019 +0100
3.3 @@ -141,7 +141,7 @@
3.4 (denom::real) = get_denominator funterm; \<comment> \<open>get_denominator\<close>
3.5 (num::real) = get_numerator funterm; \<comment> \<open>get_numerator\<close>
3.6 (equ::bool) = (denom = (0::real));
3.7 - (L_L::bool list) = (SubProblem (''PolyEq'',
3.8 + (L_L::bool list) = (SubProblem (''Partial_Fractions'',
3.9 [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''],
3.10 [''no_met''])
3.11 [BOOL equ, REAL zzz]);
3.12 @@ -199,7 +199,7 @@
3.13 " (num::real) = get_numerator funterm; "^
3.14 (*get_numerator*)
3.15 " (equ::bool) = (denom = (0::real)); "^
3.16 - " (L_L::bool list) = (SubProblem (''PolyEq'', "^
3.17 + " (L_L::bool list) = (SubProblem (''Partial_Fractions'', "^
3.18 " [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], "^
3.19 " [''no_met'']) "^
3.20 " [BOOL equ, REAL zzz]); "^
4.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Mar 07 17:22:20 2019 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Mar 07 17:29:30 2019 +0100
4.3 @@ -202,7 +202,7 @@
4.4 denom = get_denominator f_f; \<comment> \<open>equ = -1 + -2 * z + 8 * z ^^^ 2 = 0\<close>
4.5 equ = denom = (0::real);
4.6 \<comment> \<open>----- ([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)\<close>
4.7 - L_L = SubProblem (''PolyEq'', \<comment> \<open>([2], Res), [z = 1 / 2, z = -1 / 4\<close>
4.8 + L_L = SubProblem (''Partial_Fractions'', \<comment> \<open>([2], Res), [z = 1 / 2, z = -1 / 4\<close>
4.9 [''abcFormula'', ''degree_2'', ''polynomial'', ''univariate'', ''equation''],
4.10 [''no_met'']) [BOOL equ, REAL zzz]; \<comment> \<open>facs: (z - 1 / 2) * (z - -1 / 4)\<close>
4.11 facs = factors_from_solution L_L; \<comment> \<open>([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4))\<close>
4.12 @@ -257,7 +257,7 @@
4.13 " (equ::bool) = (denom = (0::real)); " ^
4.14
4.15 (*([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
4.16 - " (L_L::bool list) = (SubProblem (''PolyEq'', " ^
4.17 + " (L_L::bool list) = (SubProblem (''Partial_Fractions'', " ^
4.18 " [''abcFormula'', ''degree_2'', ''polynomial'', ''univariate'', ''equation''], " ^
4.19 (*([2], Res), [z = 1 / 2, z = -1 / 4]*)
4.20 " [''no_met'']) [BOOL equ, REAL zzz]); " ^
5.1 --- a/src/Tools/isac/TODO.thy Thu Mar 07 17:22:20 2019 +0100
5.2 +++ b/src/Tools/isac/TODO.thy Thu Mar 07 17:29:30 2019 +0100
5.3 @@ -57,8 +57,45 @@
5.4 Notes in ~~/xmldata/TODO.txt.
5.5 \<close>
5.6
5.7 +section \<open>new tools for checking tests\<close>
5.8 +text\<open>
5.9 +\begin{itemize}
5.10 +\item fun show_pt_tac: show (pos, formula, tactic); this would speed up investigations like
5.11 + isabisacREP WORKING isabisac NOT working
5.12 + (([], Frm), Problem (''Partial_Fractions'', =
5.13 + [''partial_fraction'', ''rational'', ''simplification''])), = WN190301: here is an ERROR with ??.<const>String.char.Char
5.14 + (([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), =
5.15 + (([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)), =
5.16 + (([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)), =
5.17 + (([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0), =
5.18 + (([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or> =
5.19 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)), =
5.20 + (([2,2], Res), z = 1 / 2 \<or> z = -1 / 4), =
5.21 + (([2,3], Res), [z = 1 / 2, z = -1 / 4]), =
5.22 + (([2,4], Res), [z = 1 / 2, z = -1 / 4]), =
5.23 + (([2], Res), [z = 1 / 2, z = -1 / 4]), =
5.24 + ("Take", Take "3 / ((z - 1 / 2) * (z - -1 / 4))")
5.25 + (([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))), =
5.26 + ("Rewrite_Set", Rewrite_Set "ansatz_rls")
5.27 + (([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)), (([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)),
5.28 + ("Take", Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)")
5.29 + (([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)), (([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)),
5.30 + ("Rewrite_Set", Rewrite_Set "equival_trans")
5.31 + (([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)), (([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)),
5.32 + ("Substitute", Substitute ["z = 1 / 2"])
5.33 + (([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)), (([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)),
5.34 + ("Rewrite_Set", Rewrite_Set "norm_Rational")
5.35 + (([6], Res), 3 = 3 * A / 4)] (([6], Res), 3 = AA * 3 / 4)]
5.36 + val it = (): unit val it = (): unit *)
5.37 +\item
5.38 +\end{itemize}
5.39 +\<close>
5.40 section \<open>\<close>
5.41 subsection \<open>\<close>
5.42 subsubsection \<open>\<close>
5.43 -text \<open>\<close>
5.44 +text\<open>
5.45 +\begin{itemize}
5.46 +\item
5.47 +\end{itemize}
5.48 +\<close>
5.49 end