1.1 --- a/TODO.md Tue May 24 16:47:31 2022 +0200
1.2 +++ b/TODO.md Thu May 26 12:44:51 2022 +0200
1.3 @@ -59,9 +59,7 @@
1.4 (*1*)val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) );
1.5 (*2*)val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}(**)
1.6
1.7 -* WN: reduce the number of TermC.parse*;
1.8 - + 0d22a6bf1fc6 was too much for 1 changeset
1.9 - + first parse with ctxt in Specify (O_Model.init shall return a context,..) etc
1.10 +* WN: first parse with ctxt in Specify (O_Model.init shall return a context,..) etc
1.11
1.12
1.13 * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue May 24 16:47:31 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Thu May 26 12:44:51 2022 +0200
2.3 @@ -75,7 +75,7 @@
2.4 val parseNEW': Proof.context -> string -> term
2.5 val parseNEW'': theory -> string -> term
2.6 val parse_strict: theory -> string -> term
2.7 - val parse: theory -> string -> cterm option
2.8 +(*val parse: theory -> string -> cterm option*)
2.9
2.10 val parse_patt: theory -> string -> term
2.11 val perm: term -> term -> bool
3.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Tue May 24 16:47:31 2022 +0200
3.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Thu May 26 12:44:51 2022 +0200
3.3 @@ -236,25 +236,25 @@
3.4
3.5 yields p is_prime \<and> n1 < p \<and> \<not> p dvd n2 \<and> (* smallest with these properties... *)
3.6 (\<forall> p'. (p' is_prime \<and> n1 < p' \<and> \<not> p' dvd n2) \<longrightarrow> p \<le> p') *)
3.7 -function next_prime_not_dvd :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "next_prime_not_dvd" 70) where
3.8 -"n1 next_prime_not_dvd n2 =
3.9 +function next_prime_not_dvd :: "nat \<Rightarrow> nat \<Rightarrow> nat" (*infixl "next_prime_not_dvd" 70*) where
3.10 +"next_prime_not_dvd n1 n2 =
3.11 (let
3.12 ps = primes_upto (n1 + 1);
3.13 nxt = last ps
3.14 in
3.15 if n2 mod nxt \<noteq> 0
3.16 then nxt
3.17 - else nxt next_prime_not_dvd n2)"
3.18 + else next_prime_not_dvd nxt n2)"
3.19 by auto \<comment> \<open>simp del: is_prime.simps, make_primes.simps, primes_upto.simps < -- declare*\<close>
3.20 termination sorry (*next_prime_not_dvd: lexicographic_order +PROOF primes? / size_change: Failed*)
3.21
3.22 -value "1 next_prime_not_dvd 15 = 2"
3.23 -value "2 next_prime_not_dvd 15 = 7"
3.24 -value "3 next_prime_not_dvd 15 = 7"
3.25 -value "4 next_prime_not_dvd 15 = 7"
3.26 -value "5 next_prime_not_dvd 15 = 7"
3.27 -value "6 next_prime_not_dvd 15 = 7"
3.28 -value "7 next_prime_not_dvd 15 =11"
3.29 +value "next_prime_not_dvd 1 15 = 2"
3.30 +value "next_prime_not_dvd 2 15 = 7"
3.31 +value "next_prime_not_dvd 3 15 = 7"
3.32 +value "next_prime_not_dvd 4 15 = 7"
3.33 +value "next_prime_not_dvd 5 15 = 7"
3.34 +value "next_prime_not_dvd 6 15 = 7"
3.35 +value "next_prime_not_dvd 7 15 =11"
3.36
3.37 subsection \<open>basic notions for univariate polynomials\<close>
3.38
3.39 @@ -462,11 +462,11 @@
3.40 assume m > 0
3.41 yields up = [p1 mod m, p2 mod m, ..., pk mod m]*)
3.42 definition mod' :: "nat \<Rightarrow> int \<Rightarrow> int" where "mod' m i = i mod (int m)"
3.43 -definition mod_up :: "unipoly \<Rightarrow> nat \<Rightarrow> unipoly" (infixl "mod_up" 70) where
3.44 -"p mod_up m = map (mod' m) p"
3.45 +definition mod_up :: "unipoly \<Rightarrow> nat \<Rightarrow> unipoly" (*infixl "mod_up" 70*) where
3.46 +"mod_up p m = map (mod' m) p"
3.47
3.48 -value "[5, 4, 7, 8, 1] mod_up 5 = [0, 4, 2, 3, 1]"
3.49 -value "[5, 4,-7, 8,-1] mod_up 5 = [0, 4, 3, 3, 4]"
3.50 +value "mod_up [5, 4, 7, 8, 1] 5 = [0, 4, 2, 3, 1]"
3.51 +value "mod_up [5, 4,-7, 8,-1] 5 = [0, 4, 3, 3, 4]"
3.52
3.53 (* euclidean algoritm in Z_p[x/m].
3.54 mod_up_gcd :: unipoly \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> unipoly
3.55 @@ -476,11 +476,11 @@
3.56 function mod_up_gcd :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> unipoly" where
3.57 "mod_up_gcd p1 p2 m =
3.58 (let
3.59 - p1m = p1 mod_up m;
3.60 - p2m = drop_tl_zeros (p2 mod_up m);
3.61 + p1m = mod_up p1 m;
3.62 + p2m = drop_tl_zeros (mod_up p2 m);
3.63 p2n = (replicate (List.length p1 - List.length p2m) 0) @ p2m;
3.64 quot = mod_div (lcoeff_up p1m) (lcoeff_up p2n) m;
3.65 - rest = drop_tl_zeros ((p1m %-% (p2n %* (int quot))) mod_up m)
3.66 + rest = drop_tl_zeros (mod_up (p1m %-% (p2n %* (int quot))) m)
3.67 in
3.68 if rest = [] then p2 else
3.69 if List.length rest < List.length p2
3.70 @@ -539,10 +539,9 @@
3.71 where
3.72 "try_new_prime_up a b d M P g p =
3.73 (if P > M then g else
3.74 - let p = p next_prime_not_dvd d;
3.75 - g_p = centr_up ( ( (normalise (mod_up_gcd a b p) p)
3.76 - %* (int (d mod p)))
3.77 - mod_up p)
3.78 + let p = next_prime_not_dvd p d;
3.79 + g_p = centr_up (mod_up ( (normalise (mod_up_gcd a b p) p)
3.80 + %* (int (d mod p)))p)
3.81 p
3.82 in
3.83 if deg_up g_p < deg_up g
3.84 @@ -552,7 +551,7 @@
3.85 if deg_up g_p \<noteq> deg_up g then try_new_prime_up a b d M P g p else
3.86 let
3.87 P = P * p;
3.88 - g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P
3.89 + g = centr_up (mod_up (chinese_remainder_up (P, p) (g, g_p)) P) P
3.90 in try_new_prime_up a b d M P g p)"
3.91 by pat_completeness auto \<comment> \<open>simp del: centr_up_def normalise.simps mod_up_gcd.simps\<close>
3.92 termination try_new_prime_up (*by lexicographic_order +PROOF primes? / by size_change LOOPS*)
3.93 @@ -569,8 +568,8 @@
3.94 function HENSEL_lifting_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unipoly" where
3.95 "HENSEL_lifting_up a b d M p =
3.96 (let
3.97 - p = p next_prime_not_dvd d;
3.98 - g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (int (d mod p))) mod_up p) p \<comment> \<open>see above\<close>
3.99 + p = next_prime_not_dvd p d;
3.100 + g_p = centr_up (mod_up ((normalise (mod_up_gcd a b p) p) %* (int (d mod p))) p) p \<comment> \<open>see above\<close>
3.101 in
3.102 if deg_up g_p = 0 then [1] else
3.103 (let
4.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Tue May 24 16:47:31 2022 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Thu May 26 12:44:51 2022 +0200
4.3 @@ -88,8 +88,8 @@
4.4 Presently, ISAC uses a slightly different representation for terms (which soon
4.5 will disappear), which does not encode numerals as binary numbers:
4.6 \<close>
4.7 -ML \<open>val SOME t = TermC.parse @{theory "Isac_Knowledge"} "a + b * 3";
4.8 - TermC.atomwy (Thm.term_of t);
4.9 +ML \<open>
4.10 + val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
4.11 \<close>
4.12 text \<open>From the above we see: the internal representation of a term contains
4.13 all the knowledge it is built from, see
4.14 @@ -114,7 +114,8 @@
4.15 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is
4.16 defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
4.17 \<close>
4.18 -ML \<open>TermC.parse @{theory "HOL"} "a + b * 3";
4.19 +ML \<open>
4.20 + val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
4.21 \<close>
4.22 text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see
4.23 \begin{itemize}
5.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Tue May 24 16:47:31 2022 +0200
5.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Thu May 26 12:44:51 2022 +0200
5.3 @@ -22,10 +22,10 @@
5.4 found in $ISABELLE_ISAC/Knowledge/Diff.thy:
5.5 \<close>
5.6 ML \<open>
5.7 -val diff_sum = ThmC.numerals_to_Free @{thm diff_sum};
5.8 -val diff_pow = ThmC.numerals_to_Free @{thm diff_pow};
5.9 -val diff_var = ThmC.numerals_to_Free @{thm diff_var};
5.10 -val diff_const = ThmC.numerals_to_Free @{thm diff_const};
5.11 +val diff_sum = @{thm diff_sum};
5.12 +val diff_pow = @{thm diff_pow};
5.13 +val diff_var = @{thm diff_var};
5.14 +val diff_const = @{thm diff_const};
5.15 \<close>
5.16 text \<open>Looking at the rules (abbreviated by 'thm' above), we see the
5.17 differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound
5.18 @@ -37,10 +37,11 @@
5.19 (*default_print_depth 1;*)
5.20 val (thy, ro, er, inst) =
5.21 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
5.22 +val ctxt = Proof_Context.init_global thy; (*required for parsing*)
5.23 \<close>
5.24 text \<open>... and let us differentiate the term t:\<close>
5.25 ML \<open>
5.26 -val t = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x\<up>2 + x + y)";
5.27 +val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)";
5.28
5.29 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
5.30 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
5.31 @@ -79,10 +80,10 @@
5.32 text \<open>We have already seen conditional rewriting above when we used the rule
5.33 diff_const; let us try:\<close>
5.34 ML \<open>
5.35 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*x*z)";
5.36 +val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)";
5.37 Rewrite.rewrite_inst_ thy ro er true inst diff_const t1;
5.38
5.39 -val t2 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*y*z)";
5.40 +val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)";
5.41 Rewrite.rewrite_inst_ thy ro er true inst diff_const t2;
5.42 \<close>
5.43 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
5.44 @@ -97,7 +98,7 @@
5.45 \<close>
5.46 ML \<open>
5.47 (*show_brackets := true; TODO*)
5.48 -val t0 = (Thm.term_of o the o (TermC.parse thy)) "2*a + 3*b + 4*a"; UnparseC.term t0;
5.49 +val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
5.50 (*show_brackets := false;*)
5.51 \<close>
5.52 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
5.53 @@ -146,11 +147,11 @@
5.54 \<close>
5.55 ML \<open>
5.56 (*show_brackets := false; TODO*)
5.57 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(a - b) * (a\<up>2 + a*b + b\<up>2)";
5.58 +val t1 = TermC.parseNEW' ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
5.59 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; UnparseC.term t;
5.60 \<close>
5.61 ML \<open>
5.62 -val t2 = (Thm.term_of o the o (TermC.parse thy))
5.63 +val t2 = TermC.parseNEW' ctxt
5.64 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
5.65 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
5.66 \<close>
5.67 @@ -186,8 +187,8 @@
5.68
5.69 subsection \<open>What already works\<close>
5.70 ML \<open>
5.71 -val t2 = (Thm.term_of o the o (TermC.parse thy))
5.72 - "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
5.73 +val t2 = TermC.parseNEW' ctxt
5.74 + "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real";
5.75 val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; UnparseC.term t;
5.76 \<close>
5.77 text \<open>Try your own examples !\<close>
5.78 @@ -226,7 +227,7 @@
5.79
5.80 subsection \<open>This does not yet work\<close>
5.81 ML \<open>
5.82 -val t = (Thm.term_of o the o (TermC.parse thy))
5.83 +val t = TermC.parseNEW' ctxt
5.84 "(2*a - 5*b) * (2*a + 5*b)";
5.85 Rewrite.rewrite_set_ thy true rls_p_33 t; UnparseC.term t;
5.86 \<close>
6.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Tue May 24 16:47:31 2022 +0200
6.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Thu May 26 12:44:51 2022 +0200
6.3 @@ -4,6 +4,8 @@
6.4 *)
6.5
6.6 "-----------------------------------------------------------------------------------------------";
6.7 +"This file evaluates, if '-- rat-equ: remove x = 0 from [x = 0, ..' is separated into ML blocks ";
6.8 +"-----------------------------------------------------------------------------------------------";
6.9 "table of contents -----------------------------------------------------------------------------";
6.10 "-----------------------------------------------------------------------------------------------";
6.11 "----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";
7.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Tue May 24 16:47:31 2022 +0200
7.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Thu May 26 12:44:51 2022 +0200
7.3 @@ -354,14 +354,16 @@
7.4 *** Free ( R, RealDef.real)
7.5 *** Free ( R, RealDef.real) *)
7.6 val thy = @{theory "Complex_Main"};
7.7 + val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
7.8 val str = "x + z";
7.9 - TermC.parse thy str;
7.10 + TermC.parseNEW' ctxt str;
7.11 +
7.12 "---------------";
7.13 val str = "x + 2*z";
7.14 val t = Syntax.read_term_global thy str;
7.15 val t = TermC.typ_a2real (Syntax.read_term_global thy str);
7.16 Thm.global_cterm_of thy t;
7.17 - case TermC.parse thy str of
7.18 + case TermC.parseNEW ctxt str of
7.19 SOME t' => t'
7.20 | NONE => error "termC.sml parsing 'x + 2*z' failed";
7.21
7.22 @@ -641,7 +643,7 @@
7.23 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
7.24 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
7.25 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
7.26 -val T = (type_of o Thm.term_of o the) (TermC.parse thy "12::real");
7.27 +val T = type_of (TermC.parseNEW' ctxt "12::real");
7.28 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;
7.29 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
7.30
7.31 @@ -653,7 +655,7 @@
7.32 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
7.33 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
7.34 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
7.35 -val t = (Thm.term_of o the o (TermC.parse thy)) "3 ^ 4";
7.36 +val t = TermC.parseNEW' ctxt "(3::real) ^ 4";
7.37 val hT = type_of (head_of t);
7.38 if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = TermC.dest_binop_typ hT
7.39 then () else error "TermC.dest_binop_typ";
7.40 @@ -661,13 +663,13 @@
7.41 "----------- fun TermC.is_list -----------------------------------------------------------------------";
7.42 "----------- fun TermC.is_list -----------------------------------------------------------------------";
7.43 "----------- fun TermC.is_list -----------------------------------------------------------------------";
7.44 -val (SOME ct) = TermC.parse thy "lll::real list";
7.45 +val (SOME ct) = TermC.parseNEW ctxt "lll::real list";
7.46 val t = TermC.str2term "lll::real list";
7.47 -val ty = (Term.type_of o Thm.term_of) ct;
7.48 +val ty = Term.type_of ct;
7.49 if TermC.is_list t = false then () else error "TermC.is_list lll::real list";
7.50
7.51 val t = TermC.str2term "[a, b, c]";
7.52 -val ty = (Term.type_of o Thm.term_of) ct;
7.53 +val ty = Term.type_of ct;
7.54 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]";
7.55
7.56 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
8.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 24 16:47:31 2022 +0200
8.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu May 26 12:44:51 2022 +0200
8.3 @@ -1026,8 +1026,7 @@
8.4 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
8.5 = (cs', (encode ifo));
8.6 val ctxt = get_ctxt pt pos (*see TODO.thy*)
8.7 - val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
8.8 - val f_in = Thm.term_of f_in
8.9 + val SOME f_in = (*case*) TermC.parseNEW ctxt istr (*of*);
8.10 val pos_pred = lev_back' pos
8.11 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
8.12 (*if*) f_pred = f_in; (*else*)
9.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue May 24 16:47:31 2022 +0200
9.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu May 26 12:44:51 2022 +0200
9.3 @@ -571,8 +571,7 @@
9.4 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
9.5 = (ptp', (encode ifo));
9.6 val SOME f_in =
9.7 - (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
9.8 - val f_in = Thm.term_of f_in
9.9 + (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
9.10 val pos_pred = lev_back(*'*) pos
9.11 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
9.12 val f_succ = Ctree.get_curr_formula (pt, pos);
10.1 --- a/test/Tools/isac/Knowledge/algein.sml Tue May 24 16:47:31 2022 +0200
10.2 +++ b/test/Tools/isac/Knowledge/algein.sml Thu May 26 12:44:51 2022 +0200
10.3 @@ -15,10 +15,7 @@
10.4 "-----------------------------------------------------------------";
10.5
10.6 val thy = @{theory "AlgEin"};
10.7 -
10.8 -
10.9 -(* use"../smltest/IsacKnowledge/algein.sml";
10.10 - *)
10.11 +val ctxt = Proof_Context.init_global thy;
10.12
10.13 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
10.14 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
10.15 @@ -29,7 +26,7 @@
10.16 \ (let t_t = (l_l = 1)\
10.17 \ in t_t)"
10.18 ;
10.19 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
10.20 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
10.21 TermC.atomty sc;
10.22 atomt sc;
10.23
11.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Tue May 24 16:47:31 2022 +0200
11.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Thu May 26 12:44:51 2022 +0200
11.3 @@ -28,7 +28,7 @@
11.4
11.5 val thy = @{theory "Biegelinie"};
11.6 val ctxt = ThyC.id_to_ctxt "Biegelinie";
11.7 -fun str2term str = (Thm.term_of o the o (TermC.parse thy)) str;
11.8 +fun str2term str = TermC.parseNEW' ctxt str;
11.9 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
11.10 fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));
11.11
12.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue May 24 16:47:31 2022 +0200
12.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu May 26 12:44:51 2022 +0200
12.3 @@ -25,6 +25,7 @@
12.4
12.5
12.6 val thy = @{theory "Diff"};
12.7 +val ctxt = Proof_Context.init_global thy;
12.8
12.9 "----------- problemtype --------------------------------";
12.10 "----------- problemtype --------------------------------";
12.11 @@ -34,11 +35,11 @@
12.12 Find =["derivative f_f'"],
12.13 With =[],
12.14 Relate=[]}:string ppc;
12.15 -val chkpbt = ((map (the o (TermC.parse thy))) o P_Model.to_list) pbt;
12.16 +val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt;
12.17
12.18 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))",
12.19 "differentiateFor x", "derivative f_f'"];
12.20 -val chkorg = map (the o (TermC.parse thy)) org;
12.21 +val chkorg = map (TermC.parseNEW' ctxt) org;
12.22
12.23 Problem.from_store ["derivative_of", "function"];
12.24 MethodC.from_store ["diff", "differentiate_on_R"];
12.25 @@ -47,18 +48,18 @@
12.26 "----------- for correction of diff_const ---------------";
12.27 "----------- for correction of diff_const ---------------";
12.28 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
12.29 -val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)";
12.30 +val t = TermC.parseNEW' ctxt "Not (x =!= a)";
12.31 case rewrite_set_ thy false erls_diff t of
12.32 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
12.33 | _ => error "rewrite_set_ Not (x =!= a) changed";
12.34
12.35 -val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_num";
12.36 +val t = TermC.parseNEW' ctxt "2 is_num";
12.37 case rewrite_set_ thy false erls_diff t of
12.38 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
12.39 | _ => error "rewrite_set_ 2 is_num changed";
12.40
12.41 val thm = @{thm diff_const};
12.42 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x";
12.43 +val ct = TermC.parseNEW' ctxt "d_d x x";
12.44 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
12.45 val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
12.46
12.47 @@ -66,10 +67,10 @@
12.48 "----------- for correction of diff_quot ----------------";
12.49 "----------- for correction of diff_quot ----------------";
12.50 val thy = @{theory "Diff"};
12.51 -val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)";
12.52 +val ct = TermC.parseNEW' ctxt "Not (x = 0)";
12.53 rewrite_set_ thy false erls_diff ct;
12.54
12.55 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))";
12.56 +val ct = TermC.parseNEW' ctxt "d_d x ((x+1) / (x - 1))";
12.57 val thm = @{thm diff_quot};
12.58 val SOME (ctt,_) =
12.59 (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
12.60 @@ -78,7 +79,7 @@
12.61 "----------- differentiate by rewrite -------------------";
12.62 "----------- differentiate by rewrite -------------------";
12.63 val thy = @{theory "Diff"};
12.64 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \<up> 2 + 3 * x + 4)";
12.65 +val ct = TermC.parseNEW' ctxt "d_d x (x \<up> 2 + 3 * x + 4)";
12.66 "--- 1 ---";
12.67 val thm = @{thm "diff_sum"};
12.68 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
12.69 @@ -101,7 +102,7 @@
12.70 "--- 7 ---";
12.71 "--- 7 ---";
12.72 val rls = Test_simplify;
12.73 -val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \<up> (2 - 1) + 3 * 1 + 0";
12.74 +val ct = TermC.parseNEW' ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";
12.75 val (ct, _) = the (rewrite_set_ thy true rls ct);
12.76 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
12.77
12.78 @@ -257,7 +258,7 @@
12.79 \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
12.80 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
12.81 ;
12.82 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
12.83 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
12.84
12.85
12.86 "----------- diff_conv, sym_diff_conv -------------------";
13.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Tue May 24 16:47:31 2022 +0200
13.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Thu May 26 12:44:51 2022 +0200
13.3 @@ -94,10 +94,10 @@
13.4 if UnparseC.term t' = "True" then ()
13.5 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
13.6
13.7 -val SOME t = TermC.parse thy "solution LL";
13.8 -TermC.atomty (Thm.term_of t);
13.9 -val SOME t = TermC.parse thy "solution LL";
13.10 -TermC.atomty (Thm.term_of t);
13.11 +val SOME t = TermC.parseNEW ctxt "solution LL";
13.12 +TermC.atomty t;
13.13 +val SOME t = TermC.parseNEW ctxt "solution LL";
13.14 +TermC.atomty t;
13.15
13.16 val t = TermC.str2term
13.17 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
14.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue May 24 16:47:31 2022 +0200
14.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu May 26 12:44:51 2022 +0200
14.3 @@ -255,52 +255,52 @@
14.4 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
14.5 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
14.6
14.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";
14.8 +val t = TermC.parseNEW' ctxt "Integral x D x";
14.9 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.10 if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
14.11
14.12 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
14.13 +val t = TermC.parseNEW' ctxt "Integral c * x \<up> 2 + c_2 D x";
14.14 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.15 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
14.16
14.17 val rls = add_new_c;
14.18 -val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";
14.19 +val t = TermC.parseNEW' ctxt "c * (x \<up> 3 / 3) + c_2 * x";
14.20 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.21 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
14.22 else error "integrate.sml: diff.behav. in add_new_c simpl.";
14.23
14.24 -val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";
14.25 +val t = TermC.parseNEW' ctxt "F x = x \<up> 3 / 3 + x";
14.26 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.27 if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
14.28 else error "integrate.sml: diff.behav. in add_new_c equation";
14.29
14.30 val rls = simplify_Integral;
14.31 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
14.32 -val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
14.33 +val t = TermC.parseNEW' ctxt "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
14.34 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.35 if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
14.36 then () else error "integrate.sml: diff.behav. in simplify_I #1";
14.37
14.38 val rls = integration;
14.39 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
14.40 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
14.41 +val t = TermC.parseNEW' ctxt "Integral c * x \<up> 2 + c_2 D x";
14.42 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.43 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
14.44 then () else error "integrate.sml: diff.behav. in integration #1";
14.45
14.46 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";
14.47 +val t = TermC.parseNEW' ctxt "Integral 3*x \<up> 2 + 2*x + 1 D x";
14.48 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.49 if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
14.50 else error "integrate.sml: diff.behav. in integration #2";
14.51
14.52 -val t = (Thm.term_of o the o (TermC.parse thy))
14.53 +val t = TermC.parseNEW' ctxt
14.54 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
14.55 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.56 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
14.57 if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
14.58 then () else error "integrate.sml: diff.behav. in integration #3";
14.59
14.60 -val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
14.61 +val t = TermC.parseNEW' ctxt ("Integral " ^ UnparseC.term res ^ " D x");
14.62 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
14.63 if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
14.64 then () else error "integrate.sml: diff.behav. in integration #4";
14.65 @@ -330,10 +330,10 @@
14.66 Find =["antiDerivative F_F"],
14.67 With =[],
14.68 Relate=[]}:string ppc;
14.69 -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
14.70 -val t1 = (Thm.term_of o hd) chkmodel;
14.71 -val t2 = (Thm.term_of o hd o tl) chkmodel;
14.72 -val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
14.73 +val chkmodel = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) model;
14.74 +val t1 = (hd) chkmodel;
14.75 +val t2 = (hd o tl) chkmodel;
14.76 +val t3 = (hd o tl o tl) chkmodel;
14.77 case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
14.78 | _ => error "integrate.sml: Integrate.antiDerivative ???";
14.79
14.80 @@ -342,10 +342,10 @@
14.81 Find =["antiDerivativeName F_F"],
14.82 With =[],
14.83 Relate=[]}:string ppc;
14.84 -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
14.85 -val t1 = (Thm.term_of o hd) chkmodel;
14.86 -val t2 = (Thm.term_of o hd o tl) chkmodel;
14.87 -val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
14.88 +val chkmodel = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) model;
14.89 +val t1 = (hd) chkmodel;
14.90 +val t2 = (hd o tl) chkmodel;
14.91 +val t3 = (hd o tl o tl) chkmodel;
14.92 case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
14.93 | _ => error "integrate.sml: Integrate.antiDerivativeName";
14.94
15.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Tue May 24 16:47:31 2022 +0200
15.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Thu May 26 12:44:51 2022 +0200
15.3 @@ -45,135 +45,138 @@
15.4 "-------- fun has_degree_in --------------------------------------------------------------------";
15.5 "-------- fun has_degree_in --------------------------------------------------------------------";
15.6 "-------- fun has_degree_in --------------------------------------------------------------------";
15.7 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.8 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
15.9 +val thy = @{theory}
15.10 +val ctxt = Proof_Context.init_global thy
15.11 +val v = TermC.parseNEW' ctxt "x";
15.12 +val t = TermC.parseNEW' ctxt "1";
15.13 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
15.14
15.15 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.16 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
15.17 +val v = TermC.parseNEW' ctxt "AA";
15.18 +val t = TermC.parseNEW' ctxt "1";
15.19 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
15.20
15.21 (*----------*)
15.22 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.23 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
15.24 +val v = TermC.parseNEW' ctxt "x";
15.25 +val t = TermC.parseNEW' ctxt "a*b+c";
15.26 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
15.27
15.28 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.29 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
15.30 +val v = TermC.parseNEW' ctxt "AA";
15.31 +val t = TermC.parseNEW' ctxt "a*b+c";
15.32 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
15.33
15.34 (*----------*)
15.35 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.36 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
15.37 +val v = TermC.parseNEW' ctxt "x";
15.38 +val t = TermC.parseNEW' ctxt "a*x+c";
15.39 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
15.40
15.41 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.42 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
15.43 +val v = TermC.parseNEW' ctxt "AA";
15.44 +val t = TermC.parseNEW' ctxt "a*AA+c";
15.45 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
15.46
15.47 (*----------*)
15.48 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.49 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
15.50 +val v = TermC.parseNEW' ctxt "x::real";
15.51 +val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \<up> 7";
15.52 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
15.53
15.54 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.55 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
15.56 +val v = TermC.parseNEW' ctxt "AA";
15.57 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
15.58 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
15.59
15.60 (*----------*)
15.61 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.62 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
15.63 +val v = TermC.parseNEW' ctxt "x::real";
15.64 +val t = TermC.parseNEW' ctxt "x \<up> 7";
15.65 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
15.66
15.67 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.68 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
15.69 +val v = TermC.parseNEW' ctxt "AA";
15.70 +val t = TermC.parseNEW' ctxt "AA \<up> 7";
15.71 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
15.72
15.73 (*----------*)
15.74 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.75 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
15.76 +val v = TermC.parseNEW' ctxt "x::real";
15.77 +val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
15.78 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
15.79
15.80 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.81 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
15.82 +val v = TermC.parseNEW' ctxt "AA";
15.83 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
15.84 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
15.85
15.86 (*----------*)
15.87 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.88 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
15.89 +val v = TermC.parseNEW' ctxt "x::real";
15.90 +val t = TermC.parseNEW' ctxt "(a*b+x)*x";
15.91 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
15.92
15.93 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.94 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
15.95 +val v = TermC.parseNEW' ctxt "AA";
15.96 +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
15.97 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
15.98
15.99 (*----------*)
15.100 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.101 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
15.102 +val v = TermC.parseNEW' ctxt "x";
15.103 +val t = TermC.parseNEW' ctxt "x";
15.104 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
15.105
15.106 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.107 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.108 +val v = TermC.parseNEW' ctxt "AA";
15.109 +val t = TermC.parseNEW' ctxt "AA";
15.110 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
15.111
15.112 (*----------*)
15.113 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.114 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
15.115 +val v = TermC.parseNEW' ctxt "x::real";
15.116 +val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)";
15.117 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
15.118
15.119 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.120 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
15.121 +val v = TermC.parseNEW' ctxt "AA";
15.122 +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
15.123 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
15.124
15.125 "-------- fun mono_deg_in ----------------------------------------------------------------------";
15.126 "-------- fun mono_deg_in ----------------------------------------------------------------------";
15.127 "-------- fun mono_deg_in ----------------------------------------------------------------------";
15.128 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
15.129 +val v = TermC.parseNEW' ctxt "x::real";
15.130
15.131 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
15.132 +val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
15.133 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
15.134
15.135 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
15.136 +val t = TermC.parseNEW' ctxt "(x::real) \<up> 7";
15.137 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
15.138
15.139 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
15.140 +val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
15.141 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
15.142
15.143 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
15.144 +val t = TermC.parseNEW' ctxt "(a*b+x)*x";
15.145 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
15.146
15.147 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
15.148 +val t = TermC.parseNEW' ctxt "x::real";
15.149 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
15.150
15.151 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
15.152 +val t = TermC.parseNEW' ctxt "(a*b+c)";
15.153 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
15.154
15.155 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
15.156 +val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
15.157 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
15.158
15.159 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
15.160 val thy = @{theory Partial_Fractions}
15.161 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.162 +val ctxt = Proof_Context.init_global thy
15.163 +val v = TermC.parseNEW' ctxt "AA";
15.164
15.165 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
15.166 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
15.167 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
15.168
15.169 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
15.170 +val t = TermC.parseNEW' ctxt "AA \<up> 7";
15.171 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
15.172
15.173 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
15.174 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
15.175 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
15.176
15.177 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
15.178 +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
15.179 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
15.180
15.181 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
15.182 +val t = TermC.parseNEW' ctxt "AA";
15.183 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
15.184
15.185 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
15.186 +val t = TermC.parseNEW' ctxt "(a*b+c)";
15.187 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
15.188
15.189 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
15.190 +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
15.191 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
15.192
15.193
15.194 @@ -696,6 +699,7 @@
15.195 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
15.196 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
15.197 val thy = @{theory AlgEin};
15.198 +val ctxt = Proof_Context.init_global thy;
15.199
15.200 val SOME (f',_) = rewrite_set_ thy false norm_Poly
15.201 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
15.202 @@ -787,7 +791,7 @@
15.203 else error "poly.sml: diff.behav. in make_polynomial 20";
15.204
15.205 "-----SPO ---";
15.206 -val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
15.207 +val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
15.208 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
15.209 if (UnparseC.term t) = "a \<up> 4" then ()
15.210 else error "poly.sml: diff.behav. in make_polynomial 24";
16.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue May 24 16:47:31 2022 +0200
16.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu May 26 12:44:51 2022 +0200
16.3 @@ -51,55 +51,56 @@
16.4 "----------- tests on predicates in problems ---------------------";
16.5 "----------- tests on predicates in problems ---------------------";
16.6 val thy = @{theory};
16.7 +val ctxt = Proof_Context.init_global thy;
16.8 Rewrite.trace_on:=false; (*true false*)
16.9
16.10 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
16.11 + val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)";
16.12 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
16.13 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
16.14 else error "polyeq.sml: diff.behav. in lhs";
16.15
16.16 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
16.17 + val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x";
16.18 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
16.19 if (UnparseC.term t) = "True" then ()
16.20 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
16.21
16.22 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
16.23 + val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x";
16.24 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
16.25 if (UnparseC.term t) = "False" then ()
16.26 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
16.27
16.28 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
16.29 + val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
16.30 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
16.31 if (UnparseC.term t) = "True" then ()
16.32 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
16.33
16.34 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
16.35 + val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
16.36 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
16.37 if (UnparseC.term t) = "True" then ()
16.38 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
16.39
16.40 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
16.41 + val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
16.42 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
16.43 if (UnparseC.term t) = "True" then ()
16.44 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
16.45
16.46 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
16.47 + val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
16.48 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
16.49 if (UnparseC.term t) = "True" then ()
16.50 else error "polyeq.sml: diff.behav. in has_degree_in_in";
16.51
16.52 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
16.53 + val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2";
16.54 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
16.55 if (UnparseC.term t) = "False" then ()
16.56 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
16.57
16.58 - val t4 = (Thm.term_of o the o (TermC.parse thy))
16.59 + val t4 = TermC.parseNEW' ctxt
16.60 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
16.61 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
16.62 if (UnparseC.term t) = "False" then ()
16.63 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
16.64
16.65 -val t5 = (Thm.term_of o the o (TermC.parse thy))
16.66 +val t5 = TermC.parseNEW' ctxt
16.67 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
16.68 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
16.69 if (UnparseC.term t) = "True" then ()
16.70 @@ -134,7 +135,7 @@
16.71 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
16.72
16.73 (*Aufgabe zum Einstieg in die Arbeit...*)
16.74 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
16.75 + val t = TermC.parseNEW' ctxt "a*b - (a+b)*x + x \<up> 2 = 0";
16.76 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
16.77 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
16.78 UnparseC.term t;
16.79 @@ -164,9 +165,9 @@
16.80 *)
16.81
16.82 "------ 15.11.02 --------------------------";
16.83 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
16.84 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
16.85 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
16.86 + val t = TermC.parseNEW' ctxt "1 + a * x + b * x";
16.87 + val bdv = TermC.parseNEW' ctxt "bdv";
16.88 + val a = TermC.parseNEW' ctxt "a";
16.89
16.90 Rewrite.trace_on := false; (*true false*)
16.91 (* Anwenden einer Regelmenge aus Termorder.ML: *)
16.92 @@ -178,7 +179,7 @@
16.93 UnparseC.term t;
16.94 "1 + b * x + x * a";
16.95
16.96 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
16.97 + val t = TermC.parseNEW' ctxt "1 + a * (x + b * x) + a \<up> 2";
16.98 val SOME (t,_) =
16.99 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
16.100 UnparseC.term t;
16.101 @@ -187,7 +188,7 @@
16.102 UnparseC.term t;
16.103 "1 + (x + b * x) * a + a \<up> 2";
16.104
16.105 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
16.106 + val t = TermC.parseNEW' ctxt "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
16.107 val SOME (t,_) =
16.108 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
16.109 UnparseC.term t;
16.110 @@ -207,7 +208,7 @@
16.111 get_thm Termorder.thy "bdv_n_collect";
16.112 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
16.113 *)
16.114 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
16.115 + val t = TermC.parseNEW' ctxt "a \<up> 2 * x + 7 * a \<up> 2";
16.116 val SOME (t,_) =
16.117 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
16.118 UnparseC.term t;
16.119 @@ -340,14 +341,14 @@
16.120 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
16.121 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
16.122 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
16.123 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
16.124 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
16.125 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
16.126 + val substa = [(TermC.empty, TermC.parseNEW' ctxt "a::real")];
16.127 + val substb = [(TermC.empty, TermC.parseNEW' ctxt "b::real")];
16.128 + val substx = [(TermC.empty, TermC.parseNEW' ctxt "x::real")];
16.129
16.130 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
16.131 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
16.132 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
16.133 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
16.134 + val x1 = TermC.parseNEW' ctxt "a + b + x::real";
16.135 + val x2 = TermC.parseNEW' ctxt "a + x + b::real";
16.136 + val x3 = TermC.parseNEW' ctxt "a + x + b::real";
16.137 + val x4 = TermC.parseNEW' ctxt "x + a + b::real";
16.138
16.139 if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
16.140 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
16.141 @@ -358,22 +359,22 @@
16.142 if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
16.143 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
16.144
16.145 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
16.146 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
16.147 - ord_make_polynomial_in false(*true*) thy substx (aa, bb);
16.148 - true; (* => LESS *)
16.149 + val aa = TermC.parseNEW' ctxt "- 1 * a * x::real";
16.150 + val bb = TermC.parseNEW' ctxt "x \<up> 3::real";
16.151 +if ord_make_polynomial_in false(*true*) thy substx (aa, bb) = true(*LESS *) then ()
16.152 +else error "termorder.sml diff.behav ord_make_polynomial_in #4";
16.153
16.154 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
16.155 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
16.156 - ord_make_polynomial_in false(*true*) thy substa (aa, bb);
16.157 - false; (* => GREATER *)
16.158 + val aa = TermC.parseNEW' ctxt "- 1 * a * x";
16.159 + val bb = TermC.parseNEW' ctxt "x \<up> 3";
16.160 +if ord_make_polynomial_in false(*true*) thy substa (aa, bb) = false(*GREATER*) then ()
16.161 +else error "termorder.sml diff.behav ord_make_polynomial_in #5";
16.162
16.163 (* und nach dem Re-engineering der Termorders in den 'rulesets'
16.164 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
16.165 - val bdv= TermC.str2term "bdv ::real";
16.166 - val x = TermC.str2term "x ::real";
16.167 - val a = TermC.str2term "a ::real";
16.168 - val b = TermC.str2term "b ::real";
16.169 + val bdv= TermC.parseNEW' ctxt "bdv ::real";
16.170 + val x = TermC.parseNEW' ctxt "x ::real";
16.171 + val a = TermC.parseNEW' ctxt "a ::real";
16.172 + val b = TermC.parseNEW' ctxt "b ::real";
16.173 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
16.174 if UnparseC.term t' = "b + x + a" then ()
16.175 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
16.176 @@ -385,13 +386,13 @@
16.177 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
16.178
16.179 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
16.180 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
16.181 + val ppp = TermC.parseNEW' ctxt ppp';
16.182 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
16.183 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
16.184 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
16.185
16.186 val ttt' = "(3*x + 5)/18 ::real";
16.187 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
16.188 + val ttt = TermC.parseNEW' ctxt ttt';
16.189 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
16.190 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
16.191 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
16.192 @@ -1060,7 +1061,7 @@
16.193 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
16.194 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
16.195 "---- test the erls ----";
16.196 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
16.197 + val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \<up> 2 - 1";
16.198 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
16.199 val t' = UnparseC.term t;
16.200 (*if t'= \<^const_name>\<open>True\<close> then ()
17.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue May 24 16:47:31 2022 +0200
17.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu May 26 12:44:51 2022 +0200
17.3 @@ -31,6 +31,7 @@
17.4 "--------------------------------------------------------";
17.5
17.6 val thy = @{theory "PolyMinus"};
17.7 +val ctxt = Proof_Context.init_global thy;
17.8
17.9 "----------- fun identifier --------------------------------------------------------------------";
17.10 "----------- fun identifier --------------------------------------------------------------------";
17.11 @@ -341,7 +342,7 @@
17.12 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
17.13 \ (Try (Rewrite_Set fasse_zusammen False)) #> \
17.14 \ (Try (Rewrite_Set verschoenere False))) t_t)"
17.15 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
17.16 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
17.17 TermC.atomty sc;
17.18
17.19 "----------- me simplification.for_polynomials.with_minus";
17.20 @@ -448,7 +449,7 @@
17.21 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
17.22 \ (Try (Repeat (Calculate ''PLUS''))) #> \
17.23 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
17.24 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
17.25 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
17.26 TermC.atomty sc;
17.27
17.28 "----------- pbl polynom probe -----------------------------------";
18.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue May 24 16:47:31 2022 +0200
18.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu May 26 12:44:51 2022 +0200
18.3 @@ -20,22 +20,22 @@
18.4 "------------ pbl: rational, univariate, equation ----------------";
18.5 "------------ pbl: rational, univariate, equation ----------------";
18.6 "------------ pbl: rational, univariate, equation ----------------";
18.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "(1/b+1/x=1) is_ratequation_in x";
18.8 +val t = TermC.parseNEW' ctxt "(1/b+1/x=1) is_ratequation_in x";
18.9 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
18.10 val result = UnparseC.term t_;
18.11 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
18.12
18.13 -val t = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)=1) is_ratequation_in x";
18.14 +val t = TermC.parseNEW' ctxt "(sqrt(x)=1) is_ratequation_in x";
18.15 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
18.16 val result = UnparseC.term t_;
18.17 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
18.18
18.19 -val t = (Thm.term_of o the o (TermC.parse thy)) "(x=- 1) is_ratequation_in x";
18.20 +val t = TermC.parseNEW' ctxt "(x=- 1) is_ratequation_in x";
18.21 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
18.22 val result = UnparseC.term t_;
18.23 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
18.24
18.25 -val t = (Thm.term_of o the o (TermC.parse thy)) "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
18.26 +val t = TermC.parseNEW' ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
18.27 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
18.28 val result = UnparseC.term t_;
18.29 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
18.30 @@ -61,7 +61,7 @@
18.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.32 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.33
18.34 -case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
18.35 +case nxt of (Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
18.36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.37 (*
18.38 WN120317.TODO dropped rateq: here "x ~= 0 should TermC.sub_at to ctxt, but it does not:
18.39 @@ -92,7 +92,7 @@
18.40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.41 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
18.42 f2str f = "[x = 1 / 5]";
18.43 -case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
18.44 +case nxt of (Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
18.45 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
18.46 val (pt, p) = case Step.by_tactic tac (pt,p) of
18.47 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. Step.by_tactic";
18.48 @@ -198,11 +198,14 @@
18.49 if p = ([4, 3], Pbl) then ()
18.50 else
18.51 (case nxt of
18.52 - ("Add_Given", Add_Given "solveFor x") =>
18.53 + (Add_Given "equality (320 + 128 * x + - 16 * x \<up> 2 = 0)") =>
18.54 (case f of
18.55 - Test_Out.PpcKF (Problem [], {Given = [Incompl "solveFor", Correct "equality (320 + 128 * x + - 16 * x \<up> 2 = 0)"], ...}) => ()
18.56 + Test_Out.PpcKF (Test_Out.Problem [], {
18.57 + Find = [Incompl "solutions []"], Given = [Incompl "equality", Incompl "solveFor"],
18.58 + Relate = [], Where = [False "matches (?a + ?v_ \<up> 2 = 0) e_e \<or>\nmatches (?a + ?b * ?v_ \<up> 2 = 0) e_e"],
18.59 + With = []}) => ()
18.60 | _ => error ("S.68, Bsp.: 40 PblObj changed"))
18.61 - | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string (snd nxt)));
18.62 + | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string (nxt)));
18.63
18.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.65 (* ("Subproblem", Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) *)
18.66 @@ -216,7 +219,7 @@
18.67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.68 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.70 -if p = ([], Res) andalso f2str f = "[]" then ()
18.71 +if p = ([], Res) andalso f2str f = "[x = - 2, x = 10]" then ()
18.72 else error "rateq.sml: new behaviour: [x = - 2, x = 10]";
18.73
18.74 "----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
18.75 @@ -240,11 +243,9 @@
18.76 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)";
18.77
18.78 (*+*)if eq_set op = (Ctree.get_assumptions pt p |> map UnparseC.term,
18.79 -(*+*) ["x \<noteq> 0",
18.80 -(*+*) "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
18.81 -(*+*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"])
18.82 +(*+*) ["x \<noteq> 0", "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0", "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"])
18.83 (*+*)then () else error "assumptions before 1. Subproblem CHANGED";
18.84 -(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
18.85 +(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)"
18.86 (*+*)then
18.87 (*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
18.88 (*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
18.89 @@ -263,7 +264,7 @@
18.90 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18.91 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
18.92
18.93 -if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x \<up> 2 = 0"
18.94 +if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
18.95 then
18.96 ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
18.97 | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
18.98 @@ -286,12 +287,12 @@
18.99
18.100 (* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
18.101 (*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
18.102 -(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
18.103 -(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
18.104 -(*2.pre*) "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
18.105 -(*2.pre*) "lhs (-6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
18.106 +(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
18.107 +(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
18.108 +(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
18.109 +(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
18.110 (*0.asm*) "x \<noteq> 0",
18.111 -(*0.asm*) "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
18.112 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
18.113 (* *)])
18.114 (* *)then () else error "assumptions at end 2. Subproblem CHANGED";
18.115
18.116 @@ -306,12 +307,14 @@
18.117
18.118 (*/-------- final test -----------------------------------------------------------------------\*)
18.119 if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p),
18.120 - ["x = 6 / 5", "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
18.121 - "lhs (-6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
18.122 - "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
18.123 - "x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
18.124 - "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"])
18.125 -then () else error "test CHANGED";
18.126 + ["x = 6 / 5",
18.127 + "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
18.128 + "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
18.129 + "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
18.130 + "x \<noteq> 0",
18.131 + "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
18.132 + "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
18.133 +) then () else error "test CHANGED";
18.134
18.135
18.136 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
18.137 @@ -328,18 +331,18 @@
18.138 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)
18.139
18.140 (*+*)if (get_istate_LI pt p |> Istate.string_of) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
18.141 -(*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [], Rule_Set.empty, NONE, \n??.empty, ORundef, false, true)"
18.142 +(*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
18.143 (*+*)then () else error "rat-eq + subpbl: istate in specify-phase";
18.144
18.145 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
18.146
18.147 (*+*)if (get_istate_LI pt p |> Istate.string_of) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
18.148 -(*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R,R], Rule_Set.empty, SOME e_e, \n5 * x / (x + - 1 * 2) + - 1 * x / (x + 2) = 4, ORundef, true, true)"
18.149 +(*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [R, L, R, L, L, R, R, R], empty, SOME e_e, \n5 * x / (x + - 1 * 2) + - 1 * x / (x + 2) = 4, ORundef, true, true)"
18.150 (*+*)then () else error "rat-eq + subpbl: istate after found_accept";
18.151
18.152 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_eliminate"*)
18.153 (* \<up> 2*05*)
18.154 -\<close> ML \<open>
18.155 +
18.156 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
18.157 (*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Model_Problem*)
18.158
18.159 @@ -353,21 +356,22 @@
18.160 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
18.161 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
18.162
18.163 -(*[4,3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
18.164 -(*[4,3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
18.165 +(*[4,4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Problem ["degree_1", "polynomial", "univariate", "equation"]*)
18.166 +(*[4,4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
18.167 (* \<up> 2*15*)
18.168 -(*[4,3,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
18.169 -(*[4,3,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)
18.170 -(*[4,3,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)
18.171 -(*[4,3,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
18.172 +(*[4,4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
18.173 +(*[4,4,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
18.174 +(*[4,4,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)
18.175 +(*[4,4,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Or_to_List*)
18.176 (* f = Test_Out.FormKF "[x = -4 / 3]" *)
18.177 -(*[4, 3, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
18.178 -(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
18.179 +(*[4,4,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
18.180 +(*[4,4,4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
18.181 +(*[4,4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
18.182 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
18.183 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
18.184 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*)
18.185
18.186 -if p = ([], Res) andalso f2str f = "[x = -4 / 3]"
18.187 +if p = ([], Res) andalso f2str f = "[x = - 4 / 3]"
18.188 then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1"
18.189 else error "rat-eq + subpbl: end CHANGED 2";
18.190
19.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Tue May 24 16:47:31 2022 +0200
19.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Thu May 26 12:44:51 2022 +0200
19.3 @@ -755,7 +755,7 @@
19.4 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
19.5 andalso ThmC.string_of_thm thm =
19.6 (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
19.7 - (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
19.8 + (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
19.9 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
19.10 \---------------------------------------------------------------------------------------/*)
19.11
19.12 @@ -774,7 +774,7 @@
19.13 val SOME (r as (Thm (str, thm))) = nex revsets t;
19.14 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
19.15 ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
19.16 - (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
19.17 + (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
19.18 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
19.19
19.20 (*check the next rule*)
19.21 @@ -1607,7 +1607,8 @@
19.22 "-------- fun eval_get_denominator -------------------------------------------";
19.23 "-------- fun eval_get_denominator -------------------------------------------";
19.24 val thy = @{theory Isac_Knowledge};
19.25 -val t = Thm.term_of (the (TermC.parse thy "get_denominator ((a +x)/b)"));
19.26 +val ctxt = Proof_Context.init_global thy;
19.27 +val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)";
19.28 val SOME (_, t') = eval_get_denominator "" 0 t thy;
19.29 if UnparseC.term t' = "get_denominator ((a + x) / b) = b"
19.30 then () else error "get_denominator ((a + x) / b) = b"
20.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Tue May 24 16:47:31 2022 +0200
20.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu May 26 12:44:51 2022 +0200
20.3 @@ -21,43 +21,44 @@
20.4 (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic
20.5 (b) of this is a case of indeterminism due to something elementary.
20.6
20.7 -*)
20.8 +*)
20.9 val thy = @{theory "RootRatEq"};
20.10 +val ctxt = Proof_Context.init_global thy;
20.11
20.12 "------------ tests on predicates -------------------------------";
20.13 "------------ tests on predicates -------------------------------";
20.14 "------------ tests on predicates -------------------------------";
20.15 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
20.16 +val t1 = TermC.parseNEW' ctxt "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
20.17 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.18 if (UnparseC.term t) = "False" then ()
20.19 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
20.20
20.21 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/x) is_rootRatAddTerm_in x";
20.22 +val t1 = TermC.parseNEW' ctxt "(1/x) is_rootRatAddTerm_in x";
20.23 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.24 if (UnparseC.term t) = "False" then ()
20.25 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
20.26
20.27 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
20.28 +val t1 = TermC.parseNEW' ctxt "(1/sqrt(x)) is_rootRatAddTerm_in x";
20.29 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.30 if (UnparseC.term t) = "False" then ()
20.31 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
20.32
20.33 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
20.34 +val t1 = TermC.parseNEW' ctxt "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
20.35 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.36 if (UnparseC.term t) = "True" then ()
20.37 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
20.38
20.39 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
20.40 +val t1 = TermC.parseNEW' ctxt "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
20.41 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.42 if (UnparseC.term t) = "True" then ()
20.43 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
20.44
20.45 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
20.46 +val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
20.47 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.48 if (UnparseC.term t) = "True" then ()
20.49 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
20.50
20.51 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
20.52 +val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
20.53 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
20.54 if (UnparseC.term t) = "True" then ()
20.55 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
21.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue May 24 16:47:31 2022 +0200
21.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Thu May 26 12:44:51 2022 +0200
21.3 @@ -36,7 +36,7 @@
21.4 val thy = @{theory Complex_Main};
21.5 val ctxt = @{context};
21.6 val thm = @{thm add.commute};
21.7 -val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
21.8 +val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)";
21.9 "----- from old: fun rewrite__";
21.10 val bdv = [];
21.11 val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
21.12 @@ -488,7 +488,7 @@
21.13 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
21.14 val thy = @{theory RatEq};
21.15 val ctxt = Proof_Context.init_global thy;
21.16 -val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
21.17 +val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
21.18 val rls = assoc_rls "RatEq_eliminate"
21.19
21.20 val SOME (t''''', asm''''') =
22.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 24 16:47:31 2022 +0200
22.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 26 12:44:51 2022 +0200
22.3 @@ -299,8 +299,7 @@
22.4 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
22.5 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
22.6 (cs', (encode ifo));
22.7 -val SOME f_in = TermC.parse (ThyC.get_theory "Isac_Knowledge") istr
22.8 - val f_in = Thm.term_of f_in
22.9 +val SOME f_in = TermC.parseNEW (get_ctxt pt pos) istr
22.10 val f_succ = get_curr_formula (pt, pos);
22.11 f_succ = f_in = false;
22.12 val NONE = CAS_Cmd.input f_in
23.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue May 24 16:47:31 2022 +0200
23.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu May 26 12:44:51 2022 +0200
23.3 @@ -95,8 +95,7 @@
23.4 (*case*)
23.5 Step_Solve.by_term ptp (encode ifo) (*of*);
23.6 "~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
23.7 - val SOME f_in =(*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
23.8 - val f_in = Thm.term_of f_in
23.9 + val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
23.10 val pos_pred = lev_back(*'*) pos
23.11 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
23.12 val f_succ = Ctree.get_curr_formula (pt, pos);
24.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Tue May 24 16:47:31 2022 +0200
24.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Thu May 26 12:44:51 2022 +0200
24.3 @@ -131,13 +131,14 @@
24.4
24.5 (*--------------(2): does divide work in Test_simplify ?: ------*)
24.6 val thy = @{theory Test};
24.7 - val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
24.8 + val ctxt = (ThyC.id_to_ctxt "Test")
24.9 + val t = TermC.parseNEW' ctxt "6 / 2";
24.10 val rls = Test_simplify;
24.11 val (t,_) = the (rewrite_set_ thy false rls t);
24.12 (*val t = Free ("3", "Real.real") : term*)
24.13
24.14 (*--------------(3): is_num works ?: -------------------------------------*)
24.15 - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num";
24.16 + val t = TermC.parseNEW' ctxt "2 is_num";
24.17 TermC.atomty t;
24.18 rewrite_set_ @{theory Test} false tval_rls t;
24.19 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
24.20 @@ -153,19 +154,19 @@
24.21 Rewrite.trace_on := false; (*true false*)
24.22 val thy = @{theory Test};
24.23 val rls = Test_simplify;
24.24 - val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
24.25 + val t = TermC.parseNEW' ctxt "(-4) / 2";
24.26
24.27 val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
24.28
24.29 (*--------------(5): reproduce (1) with simpler term: ------------*)
24.30 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
24.31 + val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
24.32 case rewrite_set_ thy false rls t of
24.33 SOME (t', []) =>
24.34 if UnparseC.term t' = "4" then ()
24.35 else error "rewrite_set_ (3+5)/2 changed 1"
24.36 | _ => error "rewrite_set_ (3+5)/2 changed 2";
24.37
24.38 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
24.39 + val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
24.40 case rewrite_set_ thy false rls t of
24.41 SOME (t', _) =>
24.42 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
24.43 @@ -203,7 +204,7 @@
24.44
24.45 (*===================*)
24.46 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
24.47 - val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2";
24.48 + val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
24.49 val SOME (res, []) = rewrite_set_ thy false rls t;
24.50 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
24.51 "x + (-4) / 2";
24.52 @@ -227,17 +228,17 @@
24.53 " ================= evaluate.sml: calculate_ 2002 =================== ";
24.54
24.55 val thy = @{theory Test};
24.56 -val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
24.57 + val t = TermC.parseNEW' ctxt "12 / 3";
24.58 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
24.59 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
24.60 "12 / 3 = 4";
24.61 val thy = @{theory Test};
24.62 -val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
24.63 + val t = TermC.parseNEW' ctxt "4 \<up> 2";
24.64 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
24.65 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
24.66 "4 ^ 2 = 16";
24.67
24.68 - val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
24.69 + val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
24.70 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
24.71 "1 + 2 = 3";
24.72 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
24.73 @@ -262,7 +263,7 @@
24.74 else ();
24.75
24.76 (*13.9.02 *** calc: operator = pow not defined*)
24.77 - val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
24.78 + val t = TermC.parseNEW' ctxt "3 \<up> 2";
24.79 val SOME (thmID,thm) =
24.80 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
24.81 (*** calc: operator = pow not defined*)
25.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Tue May 24 16:47:31 2022 +0200
25.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Thu May 26 12:44:51 2022 +0200
25.3 @@ -89,7 +89,7 @@
25.4 "-------- fun eval_is_num ----------------------------------------------------------------------";
25.5 "-------- fun eval_is_num ----------------------------------------------------------------------";
25.6 "-------- fun eval_is_num ----------------------------------------------------------------------";
25.7 -val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num";
25.8 +val t = TermC.parseNEW' ctxt "2 is_num";
25.9 case rewrite_set_ @{theory Test} false tval_rls t of
25.10 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
25.11 | _ => error "2 is_num CHANGED";
25.12 @@ -201,6 +201,7 @@
25.13 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
25.14 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
25.15 val thy = @{theory}
25.16 +val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
25.17
25.18 val t = TermC.str2term "x = 0";
25.19 val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
25.20 @@ -251,84 +252,84 @@
25.21 "-------- fun eval_occurs_in -------------------------------------------------------------------";
25.22 "-------- fun eval_occurs_in -------------------------------------------------------------------";
25.23 "-------- fun eval_occurs_in -------------------------------------------------------------------";
25.24 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.25 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
25.26 +val v = TermC.parseNEW' ctxt "x";
25.27 +val t = TermC.parseNEW' ctxt "1";
25.28 if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
25.29
25.30 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.31 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
25.32 +val v = TermC.parseNEW' ctxt "AA";
25.33 +val t = TermC.parseNEW' ctxt "1";
25.34 if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
25.35
25.36 (*----------*)
25.37 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.38 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
25.39 +val v = TermC.parseNEW' ctxt "x";
25.40 +val t = TermC.parseNEW' ctxt "a*b+c";
25.41 if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
25.42
25.43 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.44 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
25.45 +val v = TermC.parseNEW' ctxt "AA";
25.46 +val t = TermC.parseNEW' ctxt "a*b+c";
25.47 if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
25.48
25.49 (*----------*)
25.50 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.51 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
25.52 +val v = TermC.parseNEW' ctxt "x";
25.53 +val t = TermC.parseNEW' ctxt "a*x+c";
25.54 if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
25.55
25.56 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.57 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
25.58 +val v = TermC.parseNEW' ctxt "AA";
25.59 +val t = TermC.parseNEW' ctxt "a*AA+c";
25.60 if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
25.61
25.62 (*----------*)
25.63 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.64 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
25.65 +val v = TermC.parseNEW' ctxt "x";
25.66 +val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
25.67 if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \<up> 7) x ..changed";
25.68
25.69 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.70 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
25.71 +val v = TermC.parseNEW' ctxt "AA";
25.72 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
25.73 if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \<up> 7) AA ..changed";
25.74
25.75 (*----------*)
25.76 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.77 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
25.78 +val v = TermC.parseNEW' ctxt "x";
25.79 +val t = TermC.parseNEW' ctxt "x \<up> 7";
25.80 if occurs_in v t then () else error "factor_right_deg (x \<up> 7) x ..changed";
25.81
25.82 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.83 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
25.84 +val v = TermC.parseNEW' ctxt "AA";
25.85 +val t = TermC.parseNEW' ctxt "AA \<up> 7";
25.86 if occurs_in v t then () else error "factor_right_deg (AA \<up> 7) AA ..changed";
25.87
25.88 (*----------*)
25.89 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.90 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
25.91 +val v = TermC.parseNEW' ctxt "x";
25.92 +val t = TermC.parseNEW' ctxt "(a*b+c)*x";
25.93 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
25.94
25.95 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.96 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
25.97 +val v = TermC.parseNEW' ctxt "AA";
25.98 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
25.99 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
25.100
25.101 (*----------*)
25.102 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.103 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
25.104 +val v = TermC.parseNEW' ctxt "x";
25.105 +val t = TermC.parseNEW' ctxt "(a*b+x)*x";
25.106 if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
25.107
25.108 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.109 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
25.110 +val v = TermC.parseNEW' ctxt "AA";
25.111 +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
25.112 if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
25.113
25.114 (*----------*)
25.115 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.116 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
25.117 +val v = TermC.parseNEW' ctxt "x";
25.118 +val t = TermC.parseNEW' ctxt "x";
25.119 if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
25.120
25.121 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.122 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.123 +val v = TermC.parseNEW' ctxt "AA";
25.124 +val t = TermC.parseNEW' ctxt "AA";
25.125 if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
25.126
25.127 (*----------*)
25.128 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
25.129 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
25.130 +val v = TermC.parseNEW' ctxt "x";
25.131 +val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
25.132 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
25.133
25.134 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
25.135 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
25.136 +val v = TermC.parseNEW' ctxt "AA";
25.137 +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
25.138 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
25.139
25.140
25.141 @@ -421,7 +422,7 @@
25.142 "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
25.143 "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
25.144 val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
25.145 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
25.146 +val t = TermC.parseNEW' ctxt "2 * (3::real)";
25.147 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;
25.148 ;
25.149 "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
26.1 --- a/test/Tools/isac/Specify/refine.sml Tue May 24 16:47:31 2022 +0200
26.2 +++ b/test/Tools/isac/Specify/refine.sml Thu May 26 12:44:51 2022 +0200
26.3 @@ -25,20 +25,20 @@
26.4 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
26.5
26.6 (*case 1: no refinement *)
26.7 -val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]");
26.8 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)");
26.9 +val (d1,ts1) = Input_Descript.split (TermC.parseNEW' ctxt "fixedValues [aaa = 0]");
26.10 +val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "errorBound (ddd = 0)");
26.11 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
26.12
26.13 (*case 2: refined to pbt without children *)
26.14 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]");
26.15 +val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "relations [aaa333]");
26.16 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
26.17
26.18 (*case 3: refined to pbt with children *)
26.19 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]");
26.20 +val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "valuesFor [aaa222]");
26.21 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
26.22
26.23 (*case 4: refined to children (without child)*)
26.24 -val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy");
26.25 +val (d3,ts3) = Input_Descript.split (TermC.parseNEW' ctxt "boundVariable aaa222yyy");
26.26 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
26.27
26.28 (*=================================================================
27.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 24 16:47:31 2022 +0200
27.2 +++ b/test/Tools/isac/Test_Isac.thy Thu May 26 12:44:51 2022 +0200
27.3 @@ -50,7 +50,8 @@
27.4 and find out, which ML_file or *.thy causes an error (might be ONLY one).
27.5 Also backup files (#* ) recognised by jEdit cause this trouble *)
27.6 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
27.7 - "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
27.8 +(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
27.9 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
27.10 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
27.11 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
27.12 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
27.13 @@ -62,27 +63,30 @@
27.14 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
27.15 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
27.16 ADDTESTS/------------------------------------------- see end of tests *)
27.17 -(*/--- these work directly from Pure, but create problems here ..
27.18 +(*/~~~ these work directly from Pure, but create problems here ..
27.19 "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
27.20 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
27.21 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
27.22 "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
27.23 "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
27.24 - \--- .. these work independently, but create problems here *)
27.25 -(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Check_Outer_Syntax"
27.26 + \~~~ .. these work independently, but create problems here *)
27.27 (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
27.28 -(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Term"
27.29 +(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
27.30 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
27.31 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
27.32 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
27.33 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
27.34 +(**)
27.35 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
27.36 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
27.37 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
27.38 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
27.39 +(**)
27.40
27.41 begin
27.42
27.43 +declare [[ML_print_depth = 20]]
27.44 +
27.45 ML \<open>open ML_System\<close>
27.46 ML \<open>
27.47 open Kernel;
27.48 @@ -129,51 +133,22 @@
27.49 open Rewrite_Ord
27.50 open UnparseC
27.51 \<close>
27.52 -ML_file "BaseDefinitions/libraryC.sml"
27.53
27.54 -section \<open>code for copy & paste ===============================================================\<close>
27.55 ML \<open>
27.56 "~~~~~ fun xxx , args:"; val () = ();
27.57 "~~~~~ and xxx , args:"; val () = ();
27.58 -"~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
27.59 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
27.60 +"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
27.61 +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
27.62 "xx"
27.63 -^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
27.64 -(*/------------------- step into XXXXX -----------------------------------------------------\*)
27.65 -(*-------------------- stop step into XXXXX -------------------------------------------------*)
27.66 -(*\------------------- step into XXXXX -----------------------------------------------------/*)
27.67 -(*-------------------- contiue step into XXXXX ----------------------------------------------*)
27.68 -(*/------------------- check entry to XXXXX ------------------------------------------------\*)
27.69 -(*\------------------- check entry to XXXXX ------------------------------------------------/*)
27.70 -(*/------------------- check within XXXXX --------------------------------------------------\*)
27.71 -(*\------------------- check within XXXXX --------------------------------------------------/*)
27.72 -(*/------------------- check result of XXXXX -----------------------------------------------\*)
27.73 -(*\------------------- check result of XXXXX -----------------------------------------------/*)
27.74 -(* final test ...*)
27.75 -(*/------------------- build new fun XXXXX -------------------------------------------------\*)
27.76 -(*\------------------- build new fun XXXXX -------------------------------------------------/*)
27.77 +^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
27.78 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
27.79 \<close> ML \<open>
27.80 +\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
27.81 +Rewrite.trace_on := false;
27.82 \<close>
27.83 ML \<open>
27.84 \<close> ML \<open>
27.85 \<close> ML \<open>
27.86 -\<close>
27.87 -text \<open>
27.88 - declare [[show_types]]
27.89 - declare [[show_sorts]]
27.90 - find_theorems "?a <= ?a"
27.91 -
27.92 - print_theorems
27.93 - print_facts
27.94 - print_statement ""
27.95 - print_theory
27.96 - ML_command \<open>Pretty.writeln prt\<close>
27.97 - declare [[ML_print_depth = 999]]
27.98 - declare [[ML_exception_trace]]
27.99 -\<close>
27.100 -
27.101 -section \<open>===================================================================================\<close>
27.102 -ML \<open>
27.103 \<close> ML \<open>
27.104 \<close> ML \<open>
27.105 \<close> ML \<open>
27.106 @@ -189,8 +164,6 @@
27.107 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
27.108 \<close>
27.109
27.110 -(*---------------------- check test file by testfile -------------------------------------------
27.111 - ---------------------- check test file by testfile -------------------------------------------*)
27.112 section \<open>trials with Isabelle's functions\<close>
27.113 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
27.114 ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
27.115 @@ -202,6 +175,7 @@
27.116 section \<open>test ML Code of isac\<close>
27.117 subsection \<open>basic code first\<close>
27.118 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
27.119 + ML_file "BaseDefinitions/base-definitions.sml"
27.120 ML_file "BaseDefinitions/libraryC.sml"
27.121 ML_file "BaseDefinitions/rule-def.sml"
27.122 ML_file "BaseDefinitions/eval-def.sml"
27.123 @@ -216,9 +190,9 @@
27.124 ML_file "BaseDefinitions/calcelems.sml"
27.125 ML_file "BaseDefinitions/termC.sml"
27.126 ML_file "BaseDefinitions/substitution.sml"
27.127 - ML_file "BaseDefinitions/contextC.sml"
27.128 + ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)
27.129 ML_file "BaseDefinitions/environment.sml"
27.130 - ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
27.131 +(** )ML_file "BaseDefinitions/kestore.sml"( *setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
27.132 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
27.133 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
27.134
27.135 @@ -259,7 +233,7 @@
27.136 ML_file "MathEngBasic/thmC.sml"
27.137 ML_file "MathEngBasic/rewrite.sml"
27.138 ML_file "MathEngBasic/tactic.sml"
27.139 - ML_file "MathEngBasic/ctree.sml"
27.140 + ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
27.141 ML_file "MathEngBasic/calculation.sml"
27.142
27.143 ML_file "Specify/formalise.sml"
27.144 @@ -294,7 +268,6 @@
27.145
27.146 ML_file "BridgeLibisabelle/thy-present.sml"
27.147 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
27.148 - ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
27.149 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
27.150 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
27.151 ML_file "BridgeLibisabelle/interface.sml"
27.152 @@ -306,9 +279,9 @@
27.153 ML_file "Knowledge/delete.sml"
27.154 ML_file "Knowledge/descript.sml"
27.155 ML_file "Knowledge/simplify.sml"
27.156 - ML_file "Knowledge/poly.sml"
27.157 ML_file "Knowledge/gcd_poly_ml.sml"
27.158 - ML_file "Knowledge/rational.sml" (*Test_Isac_Short*)
27.159 + ML_file "Knowledge/rational-1.sml"
27.160 + ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)
27.161 ML_file "Knowledge/equation.sml"
27.162 ML_file "Knowledge/root.sml"
27.163 ML_file "Knowledge/lineq.sml"
27.164 @@ -325,7 +298,8 @@
27.165 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
27.166 ML_file "Knowledge/diff.sml"
27.167 ML_file "Knowledge/integrate.sml"
27.168 - ML_file "Knowledge/eqsystem.sml"
27.169 + ML_file "Knowledge/eqsystem-1.sml"
27.170 + ML_file "Knowledge/eqsystem-2.sml"
27.171 ML_file "Knowledge/test.sml"
27.172 ML_file "Knowledge/polyminus.sml"
27.173 ML_file "Knowledge/vect.sml"
28.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue May 24 16:47:31 2022 +0200
28.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu May 26 12:44:51 2022 +0200
28.3 @@ -1,4 +1,4 @@
28.4 -(* Title: All tests on isac (some outcommented since Isabelle2002-->2009- 2)
28.5 +(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
28.6 Author: Walther Neuper 101001
28.7 (c) copyright due to license terms.
28.8
28.9 @@ -166,7 +166,7 @@
28.10
28.11 section \<open>trials with Isabelle's functions\<close>
28.12 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
28.13 - ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
28.14 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
28.15 ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
28.16 ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
28.17 ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
28.18 @@ -190,9 +190,9 @@
28.19 ML_file "BaseDefinitions/calcelems.sml"
28.20 ML_file "BaseDefinitions/termC.sml"
28.21 ML_file "BaseDefinitions/substitution.sml"
28.22 - ML_file "BaseDefinitions/contextC.sml"
28.23 + ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)
28.24 ML_file "BaseDefinitions/environment.sml"
28.25 -(** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
28.26 +(**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
28.27 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
28.28 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
28.29
28.30 @@ -271,7 +271,7 @@
28.31 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
28.32 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
28.33 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
28.34 - ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*)
28.35 + ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
28.36 ML_file "BridgeLibisabelle/interface.sml"
28.37 ML_file "BridgeJEdit/parseC.sml"
28.38 ML_file "BridgeJEdit/preliminary.sml"
28.39 @@ -389,7 +389,7 @@
28.40 migration from "isabelle tty" --> libisabelle
28.41 \<close>
28.42
28.43 -subsection \<open>isac on Isabelle2013- 2\<close>
28.44 +subsection \<open>isac on Isabelle2013-2\<close>
28.45 subsubsection \<open>Summary of development\<close>
28.46 text \<open>
28.47 reactivated context_thy
28.48 @@ -402,17 +402,17 @@
28.49 text \<open>
28.50 TODO
28.51 :
28.52 - : isac on Isablle2013- 2
28.53 + : isac on Isablle2013-2
28.54 :
28.55 Changeset: 55318 (03826ceb24da) merged
28.56 User: Walther Neuper <neuper@ist.tugraz.at>
28.57 - Date: 2013- 12- 12 14:27:37 +0100 (7 minutes)
28.58 + Date: 2013-12-12 14:27:37 +0100 (7 minutes)
28.59 \<close>
28.60
28.61 -subsection \<open>isac on Isabelle2013- 1\<close>
28.62 +subsection \<open>isac on Isabelle2013-1\<close>
28.63 subsubsection \<open>Summary of development\<close>
28.64 text \<open>
28.65 - Isabelle2013- 1 was replaced within a few weeks due to problems with the document model;
28.66 + Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
28.67 no significant development steps for ISAC.
28.68 \<close>
28.69 subsubsection \<open>State of tests\<close>
28.70 @@ -423,13 +423,13 @@
28.71 text \<open>
28.72 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
28.73 User: Walther Neuper <neuper@ist.tugraz.at>
28.74 - Date: 2013- 12-03 18:13:31 +0100 (8 days)
28.75 + Date: 2013-12-03 18:13:31 +0100 (8 days)
28.76 :
28.77 - : isac on Isablle2013- 1
28.78 + : isac on Isablle2013-1
28.79 :
28.80 - Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013- 1: Test_Isac perfect
28.81 + Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
28.82 User: Walther Neuper <neuper@ist.tugraz.at>
28.83 - Date: 2013- 11- 21 18:12:17 +0100 (2 weeks)
28.84 + Date: 2013-11-21 18:12:17 +0100 (2 weeks)
28.85
28.86 \<close>
28.87
28.88 @@ -443,7 +443,7 @@
28.89 \<close>
28.90 subsubsection \<open>Run tests\<close>
28.91 text \<open>
28.92 - Is standard now; this subsection will be discontinued under Isabelle2013- 1
28.93 + Is standard now; this subsection will be discontinued under Isabelle2013-1
28.94 \<close>
28.95 subsubsection \<open>State of tests\<close>
28.96 text \<open>
28.97 @@ -460,7 +460,7 @@
28.98 :
28.99 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
28.100 User: Walther Neuper <neuper@ist.tugraz.at>
28.101 - Date: 2013-07- 15 08:28:50 +0200 (4 weeks)
28.102 + Date: 2013-07-15 08:28:50 +0200 (4 weeks)
28.103 \<close>
28.104
28.105 subsection \<open>isac on Isabelle2012\<close>
28.106 @@ -484,13 +484,13 @@
28.107 in parallel with evaluation.
28.108
28.109 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
28.110 - yields 69 hits, some of which were already present before Isabelle2002-->2009- 2
28.111 + yields 69 hits, some of which were already present before Isabelle2002-->2009-2
28.112 (i.e. on the old notebook from 2002).
28.113
28.114 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
28.115 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
28.116 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
28.117 - # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009- 2 === , most likely go back to 2002
28.118 + # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
28.119 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
28.120
28.121 Some tests have been re-activated (e.g. error patterns, fill patterns).
28.122 @@ -499,17 +499,17 @@
28.123 text \<open>
28.124 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
28.125 User: Walther Neuper <neuper@ist.tugraz.at>
28.126 - Date: 2013-07- 11 16:58:31 +0200 (4 weeks)
28.127 + Date: 2013-07-11 16:58:31 +0200 (4 weeks)
28.128 :
28.129 : isac on Isablle2012
28.130 :
28.131 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
28.132 User: Walther Neuper <neuper@ist.tugraz.at>
28.133 - Date: 2012-09- 24 18:35:13 +0200 (8 months)
28.134 + Date: 2012-09-24 18:35:13 +0200 (8 months)
28.135 ------------------------------------------------------------------------------
28.136 Changeset: 48756 (7443906996a8) merged
28.137 User: Walther Neuper <neuper@ist.tugraz.at>
28.138 - Date: 2012-09- 24 18:15:49 +0200 (8 months)
28.139 + Date: 2012-09-24 18:15:49 +0200 (8 months)
28.140 \<close>
28.141
28.142 subsection \<open>isac on Isabelle2011\<close>
28.143 @@ -547,7 +547,7 @@
28.144
28.145 The list below records TODOs while producing an ISAC kernel for
28.146 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
28.147 - (so to be resumed with Isabelle2013- 1):
28.148 + (so to be resumed with Isabelle2013-1):
28.149 ############## WNxxxxxx.TODO can be found in sources ##############
28.150 --------------------------------------------------------------------------------
28.151 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
28.152 @@ -569,7 +569,7 @@
28.153 --------------------------------------------------------------------------------
28.154 WN120317.TODO changeset 977788dfed26 dropped rateq:
28.155 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
28.156 - # test --- solve (1/x = 5, x) by me --- and --- x / (x \<up> 2 - 6 * x + 9) - ...:
28.157 + # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
28.158 investigation Check_elementwise stopped due to too much effort finding out,
28.159 why Check_elementwise worked in 2002 in spite of the error.
28.160 --------------------------------------------------------------------------------
28.161 @@ -583,11 +583,11 @@
28.162 --------------------------------------------------------------------------------
28.163 WN120320.TODO check-improve rlsthmsNOTisac:
28.164 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
28.165 - DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09- 2.sml .. Isac.thy
28.166 + DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
28.167 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
28.168 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
28.169 --------------------------------------------------------------------------------
28.170 - WN120320.TODO rlsthmsNOTisac: replace twice thms \<up>
28.171 + WN120320.TODO rlsthmsNOTisac: replace twice thms ^
28.172 --------------------------------------------------------------------------------
28.173 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
28.174 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
28.175 @@ -692,18 +692,18 @@
28.176 ------------------------------------------------------------------------------
28.177 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
28.178 User: Walther Neuper <neuper@ist.tugraz.at>
28.179 - Date: 2012-09- 24 16:39:30 +0200 (8 months)
28.180 + Date: 2012-09-24 16:39:30 +0200 (8 months)
28.181 :
28.182 : isac on Isablle2011
28.183 :
28.184 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
28.185 Branch: decompose-isar
28.186 User: Walther Neuper <neuper@ist.tugraz.at>
28.187 - Date: 2011-02- 25 13:04:56 +0100 (2011-02- 25)
28.188 + Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
28.189 ------------------------------------------------------------------------------
28.190 \<close>
28.191
28.192 -subsection \<open>isac on Isabelle2009- 2\<close>
28.193 +subsection \<open>isac on Isabelle2009-2\<close>
28.194 subsubsection \<open>Summary of development\<close>
28.195 text \<open>
28.196 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
28.197 @@ -716,14 +716,14 @@
28.198 WN131021 this is broken by installation of Isabelle2011/12/13,
28.199 because all these write their binaries to ~/.isabelle/heaps/..
28.200
28.201 - $ cd /usr/local/isabisac09- 2/
28.202 + $ cd /usr/local/isabisac09-2/
28.203 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
28.204 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
28.205 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
28.206 \<close>
28.207 subsubsection \<open>State of tests\<close>
28.208 text \<open>
28.209 - Most tests are broken by the update from Isabelle2002 to Isabelle2009- 2.
28.210 + Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
28.211 \<close>
28.212 subsubsection \<open>Changesets of begin and end\<close>
28.213 text \<open>
28.214 @@ -734,12 +734,12 @@
28.215 User: Marco Steger <m.steger@student.tugraz.at>
28.216 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
28.217 :
28.218 - : isac on Isablle2009- 2
28.219 + : isac on Isablle2009-2
28.220 :
28.221 - Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009- 2
28.222 - Branch: isac-from-Isabelle2009- 2
28.223 + Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
28.224 + Branch: isac-from-Isabelle2009-2
28.225 User: Walther Neuper <neuper@ist.tugraz.at>
28.226 - Date: 2010-07- 21 09:59:35 +0200 (2010-07- 21)
28.227 + Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
28.228 ------------------------------------------------------------------------------
28.229 \<close>
28.230