# HG changeset patch # User wneuper # Date 1653561891 -7200 # Node ID c3acf9c442ac29b4227bf0867f05e817304d0982 # Parent 6a5f3a2e6d3a405eb28aa4889ca6058950ce4ed4 unify parse 6': TermC.parse eliminated, Test_Isac ok diff -r 6a5f3a2e6d3a -r c3acf9c442ac TODO.md --- a/TODO.md Tue May 24 16:47:31 2022 +0200 +++ b/TODO.md Thu May 26 12:44:51 2022 +0200 @@ -59,9 +59,7 @@ (*1*)val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) ); (*2*)val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}(**) -* WN: reduce the number of TermC.parse*; - + 0d22a6bf1fc6 was too much for 1 changeset - + first parse with ctxt in Specify (O_Model.init shall return a context,..) etc +* WN: first parse with ctxt in Specify (O_Model.init shall return a context,..) etc * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by diff -r 6a5f3a2e6d3a -r c3acf9c442ac src/Tools/isac/BaseDefinitions/termC.sml --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue May 24 16:47:31 2022 +0200 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Thu May 26 12:44:51 2022 +0200 @@ -75,7 +75,7 @@ val parseNEW': Proof.context -> string -> term val parseNEW'': theory -> string -> term val parse_strict: theory -> string -> term - val parse: theory -> string -> cterm option +(*val parse: theory -> string -> cterm option*) val parse_patt: theory -> string -> term val perm: term -> term -> bool diff -r 6a5f3a2e6d3a -r c3acf9c442ac src/Tools/isac/Knowledge/GCD_Poly_FP.thy --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Tue May 24 16:47:31 2022 +0200 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Thu May 26 12:44:51 2022 +0200 @@ -236,25 +236,25 @@ yields p is_prime \ n1 < p \ \ p dvd n2 \ (* smallest with these properties... *) (\ p'. (p' is_prime \ n1 < p' \ \ p' dvd n2) \ p \ p') *) -function next_prime_not_dvd :: "nat \ nat \ nat" (infixl "next_prime_not_dvd" 70) where -"n1 next_prime_not_dvd n2 = +function next_prime_not_dvd :: "nat \ nat \ nat" (*infixl "next_prime_not_dvd" 70*) where +"next_prime_not_dvd n1 n2 = (let ps = primes_upto (n1 + 1); nxt = last ps in if n2 mod nxt \ 0 then nxt - else nxt next_prime_not_dvd n2)" + else next_prime_not_dvd nxt n2)" by auto \ \simp del: is_prime.simps, make_primes.simps, primes_upto.simps < -- declare*\ termination sorry (*next_prime_not_dvd: lexicographic_order +PROOF primes? / size_change: Failed*) -value "1 next_prime_not_dvd 15 = 2" -value "2 next_prime_not_dvd 15 = 7" -value "3 next_prime_not_dvd 15 = 7" -value "4 next_prime_not_dvd 15 = 7" -value "5 next_prime_not_dvd 15 = 7" -value "6 next_prime_not_dvd 15 = 7" -value "7 next_prime_not_dvd 15 =11" +value "next_prime_not_dvd 1 15 = 2" +value "next_prime_not_dvd 2 15 = 7" +value "next_prime_not_dvd 3 15 = 7" +value "next_prime_not_dvd 4 15 = 7" +value "next_prime_not_dvd 5 15 = 7" +value "next_prime_not_dvd 6 15 = 7" +value "next_prime_not_dvd 7 15 =11" subsection \basic notions for univariate polynomials\ @@ -462,11 +462,11 @@ assume m > 0 yields up = [p1 mod m, p2 mod m, ..., pk mod m]*) definition mod' :: "nat \ int \ int" where "mod' m i = i mod (int m)" -definition mod_up :: "unipoly \ nat \ unipoly" (infixl "mod_up" 70) where -"p mod_up m = map (mod' m) p" +definition mod_up :: "unipoly \ nat \ unipoly" (*infixl "mod_up" 70*) where +"mod_up p m = map (mod' m) p" -value "[5, 4, 7, 8, 1] mod_up 5 = [0, 4, 2, 3, 1]" -value "[5, 4,-7, 8,-1] mod_up 5 = [0, 4, 3, 3, 4]" +value "mod_up [5, 4, 7, 8, 1] 5 = [0, 4, 2, 3, 1]" +value "mod_up [5, 4,-7, 8,-1] 5 = [0, 4, 3, 3, 4]" (* euclidean algoritm in Z_p[x/m]. mod_up_gcd :: unipoly \ unipoly \ nat \ unipoly @@ -476,11 +476,11 @@ function mod_up_gcd :: "unipoly \ unipoly \ nat \ unipoly" where "mod_up_gcd p1 p2 m = (let - p1m = p1 mod_up m; - p2m = drop_tl_zeros (p2 mod_up m); + p1m = mod_up p1 m; + p2m = drop_tl_zeros (mod_up p2 m); p2n = (replicate (List.length p1 - List.length p2m) 0) @ p2m; quot = mod_div (lcoeff_up p1m) (lcoeff_up p2n) m; - rest = drop_tl_zeros ((p1m %-% (p2n %* (int quot))) mod_up m) + rest = drop_tl_zeros (mod_up (p1m %-% (p2n %* (int quot))) m) in if rest = [] then p2 else if List.length rest < List.length p2 @@ -539,10 +539,9 @@ where "try_new_prime_up a b d M P g p = (if P > M then g else - let p = p next_prime_not_dvd d; - g_p = centr_up ( ( (normalise (mod_up_gcd a b p) p) - %* (int (d mod p))) - mod_up p) + let p = next_prime_not_dvd p d; + g_p = centr_up (mod_up ( (normalise (mod_up_gcd a b p) p) + %* (int (d mod p)))p) p in if deg_up g_p < deg_up g @@ -552,7 +551,7 @@ if deg_up g_p \ deg_up g then try_new_prime_up a b d M P g p else let P = P * p; - g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P + g = centr_up (mod_up (chinese_remainder_up (P, p) (g, g_p)) P) P in try_new_prime_up a b d M P g p)" by pat_completeness auto \ \simp del: centr_up_def normalise.simps mod_up_gcd.simps\ termination try_new_prime_up (*by lexicographic_order +PROOF primes? / by size_change LOOPS*) @@ -569,8 +568,8 @@ function HENSEL_lifting_up :: "unipoly \ unipoly \ nat \ nat \ nat \ unipoly" where "HENSEL_lifting_up a b d M p = (let - p = p next_prime_not_dvd d; - g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (int (d mod p))) mod_up p) p \ \see above\ + p = next_prime_not_dvd p d; + g_p = centr_up (mod_up ((normalise (mod_up_gcd a b p) p) %* (int (d mod p))) p) p \ \see above\ in if deg_up g_p = 0 then [1] else (let diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Thu May 26 12:44:51 2022 +0200 @@ -88,8 +88,8 @@ Presently, ISAC uses a slightly different representation for terms (which soon will disappear), which does not encode numerals as binary numbers: \ -ML \val SOME t = TermC.parse @{theory "Isac_Knowledge"} "a + b * 3"; - TermC.atomwy (Thm.term_of t); +ML \ + val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; \ text \From the above we see: the internal representation of a term contains all the knowledge it is built from, see @@ -114,7 +114,8 @@ For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is defined ('=' etc), but not yet '+' and '*', so you get 'NONE': \ -ML \TermC.parse @{theory "HOL"} "a + b * 3"; +ML \ + val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; \ text \ISAC uses comparatively few definitions and theorems from Isabelle, see \begin{itemize} diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Thu May 26 12:44:51 2022 +0200 @@ -22,10 +22,10 @@ found in $ISABELLE_ISAC/Knowledge/Diff.thy: \ ML \ -val diff_sum = ThmC.numerals_to_Free @{thm diff_sum}; -val diff_pow = ThmC.numerals_to_Free @{thm diff_pow}; -val diff_var = ThmC.numerals_to_Free @{thm diff_var}; -val diff_const = ThmC.numerals_to_Free @{thm diff_const}; +val diff_sum = @{thm diff_sum}; +val diff_pow = @{thm diff_pow}; +val diff_var = @{thm diff_var}; +val diff_const = @{thm diff_const}; \ text \Looking at the rules (abbreviated by 'thm' above), we see the differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound @@ -37,10 +37,11 @@ (*default_print_depth 1;*) val (thy, ro, er, inst) = (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); +val ctxt = Proof_Context.init_global thy; (*required for parsing*) \ text \... and let us differentiate the term t:\ ML \ -val t = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x\2 + x + y)"; +val t = TermC.parseNEW' ctxt "d_d x (x\2 + x + y)"; val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t; val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t; @@ -79,10 +80,10 @@ text \We have already seen conditional rewriting above when we used the rule diff_const; let us try:\ ML \ -val t1 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*x*z)"; +val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)"; Rewrite.rewrite_inst_ thy ro er true inst diff_const t1; -val t2 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*y*z)"; +val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)"; Rewrite.rewrite_inst_ thy ro er true inst diff_const t2; \ text \For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, @@ -97,7 +98,7 @@ \ ML \ (*show_brackets := true; TODO*) -val t0 = (Thm.term_of o the o (TermC.parse thy)) "2*a + 3*b + 4*a"; UnparseC.term t0; +val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0; (*show_brackets := false;*) \ text \Now we want to bring 4*a close to 2*a in order to get 6*a: @@ -146,11 +147,11 @@ \ ML \ (*show_brackets := false; TODO*) -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(a - b) * (a\2 + a*b + b\2)"; +val t1 = TermC.parseNEW' ctxt "(a - b) * (a\2 + a*b + b\2)"; val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; UnparseC.term t; \ ML \ -val t2 = (Thm.term_of o the o (TermC.parse thy)) +val t2 = TermC.parseNEW' ctxt "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \ 2 - 9))"; val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t; \ @@ -186,8 +187,8 @@ subsection \What already works\ ML \ -val t2 = (Thm.term_of o the o (TermC.parse thy)) - "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; +val t2 = TermC.parseNEW' ctxt + "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real"; val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; UnparseC.term t; \ text \Try your own examples !\ @@ -226,7 +227,7 @@ subsection \This does not yet work\ ML \ -val t = (Thm.term_of o the o (TermC.parse thy)) +val t = TermC.parseNEW' ctxt "(2*a - 5*b) * (2*a + 5*b)"; Rewrite.rewrite_set_ thy true rls_p_33 t; UnparseC.term t; \ diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/BaseDefinitions/contextC.sml --- a/test/Tools/isac/BaseDefinitions/contextC.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Thu May 26 12:44:51 2022 +0200 @@ -4,6 +4,8 @@ *) "-----------------------------------------------------------------------------------------------"; +"This file evaluates, if '-- rat-equ: remove x = 0 from [x = 0, ..' is separated into ML blocks "; +"-----------------------------------------------------------------------------------------------"; "table of contents -----------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; "----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/BaseDefinitions/termC.sml --- a/test/Tools/isac/BaseDefinitions/termC.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Thu May 26 12:44:51 2022 +0200 @@ -354,14 +354,16 @@ *** Free ( R, RealDef.real) *** Free ( R, RealDef.real) *) val thy = @{theory "Complex_Main"}; + val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge") val str = "x + z"; - TermC.parse thy str; + TermC.parseNEW' ctxt str; + "---------------"; val str = "x + 2*z"; val t = Syntax.read_term_global thy str; val t = TermC.typ_a2real (Syntax.read_term_global thy str); Thm.global_cterm_of thy t; - case TermC.parse thy str of + case TermC.parseNEW ctxt str of SOME t' => t' | NONE => error "termC.sml parsing 'x + 2*z' failed"; @@ -641,7 +643,7 @@ "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; -val T = (type_of o Thm.term_of o the) (TermC.parse thy "12::real"); +val T = type_of (TermC.parseNEW' ctxt "12::real"); val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3; if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot"; @@ -653,7 +655,7 @@ "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; -val t = (Thm.term_of o the o (TermC.parse thy)) "3 ^ 4"; +val t = TermC.parseNEW' ctxt "(3::real) ^ 4"; val hT = type_of (head_of t); if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = TermC.dest_binop_typ hT then () else error "TermC.dest_binop_typ"; @@ -661,13 +663,13 @@ "----------- fun TermC.is_list -----------------------------------------------------------------------"; "----------- fun TermC.is_list -----------------------------------------------------------------------"; "----------- fun TermC.is_list -----------------------------------------------------------------------"; -val (SOME ct) = TermC.parse thy "lll::real list"; +val (SOME ct) = TermC.parseNEW ctxt "lll::real list"; val t = TermC.str2term "lll::real list"; -val ty = (Term.type_of o Thm.term_of) ct; +val ty = Term.type_of ct; if TermC.is_list t = false then () else error "TermC.is_list lll::real list"; val t = TermC.str2term "[a, b, c]"; -val ty = (Term.type_of o Thm.term_of) ct; +val ty = Term.type_of ct; if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]"; "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Interpret/error-pattern.sml --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu May 26 12:44:51 2022 +0200 @@ -1026,8 +1026,7 @@ "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr) = (cs', (encode ifo)); val ctxt = get_ctxt pt pos (*see TODO.thy*) - val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*); - val f_in = Thm.term_of f_in + val SOME f_in = (*case*) TermC.parseNEW ctxt istr (*of*); val pos_pred = lev_back' pos val f_pred = Ctree.get_curr_formula (pt, pos_pred); (*if*) f_pred = f_in; (*else*) diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu May 26 12:44:51 2022 +0200 @@ -571,8 +571,7 @@ "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp', (encode ifo)); val SOME f_in = - (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*); - val f_in = Thm.term_of f_in + (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*); val pos_pred = lev_back(*'*) pos val f_pred = Ctree.get_curr_formula (pt, pos_pred); val f_succ = Ctree.get_curr_formula (pt, pos); diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/algein.sml --- a/test/Tools/isac/Knowledge/algein.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/algein.sml Thu May 26 12:44:51 2022 +0200 @@ -15,10 +15,7 @@ "-----------------------------------------------------------------"; val thy = @{theory "AlgEin"}; - - -(* use"../smltest/IsacKnowledge/algein.sml"; - *) +val ctxt = Proof_Context.init_global thy; "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; @@ -29,7 +26,7 @@ \ (let t_t = (l_l = 1)\ \ in t_t)" ; -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; TermC.atomty sc; atomt sc; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/biegelinie-1.sml --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Thu May 26 12:44:51 2022 +0200 @@ -28,7 +28,7 @@ val thy = @{theory "Biegelinie"}; val ctxt = ThyC.id_to_ctxt "Biegelinie"; -fun str2term str = (Thm.term_of o the o (TermC.parse thy)) str; +fun str2term str = TermC.parseNEW' ctxt str; fun term2s t = UnparseC.term_by_thyID "Biegelinie" t; fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str)); diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Thu May 26 12:44:51 2022 +0200 @@ -25,6 +25,7 @@ val thy = @{theory "Diff"}; +val ctxt = Proof_Context.init_global thy; "----------- problemtype --------------------------------"; "----------- problemtype --------------------------------"; @@ -34,11 +35,11 @@ Find =["derivative f_f'"], With =[], Relate=[]}:string ppc; -val chkpbt = ((map (the o (TermC.parse thy))) o P_Model.to_list) pbt; +val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt; val org = ["functionTerm (d_d x (x \ 2 + 3 * x + 4))", "differentiateFor x", "derivative f_f'"]; -val chkorg = map (the o (TermC.parse thy)) org; +val chkorg = map (TermC.parseNEW' ctxt) org; Problem.from_store ["derivative_of", "function"]; MethodC.from_store ["diff", "differentiate_on_R"]; @@ -47,18 +48,18 @@ "----------- for correction of diff_const ---------------"; "----------- for correction of diff_const ---------------"; (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*) -val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)"; +val t = TermC.parseNEW' ctxt "Not (x =!= a)"; case rewrite_set_ thy false erls_diff t of SOME (Const (\<^const_name>\True\, _), []) => () | _ => error "rewrite_set_ Not (x =!= a) changed"; -val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_num"; +val t = TermC.parseNEW' ctxt "2 is_num"; case rewrite_set_ thy false erls_diff t of SOME (Const (\<^const_name>\True\, _), []) => () | _ => error "rewrite_set_ 2 is_num changed"; val thm = @{thm diff_const}; -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x"; +val ct = TermC.parseNEW' ctxt "d_d x x"; val subst = [(@{term "bdv::real"}, @{term "x::real"})]; val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct); @@ -66,10 +67,10 @@ "----------- for correction of diff_quot ----------------"; "----------- for correction of diff_quot ----------------"; val thy = @{theory "Diff"}; -val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)"; +val ct = TermC.parseNEW' ctxt "Not (x = 0)"; rewrite_set_ thy false erls_diff ct; -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))"; +val ct = TermC.parseNEW' ctxt "d_d x ((x+1) / (x - 1))"; val thm = @{thm diff_quot}; val SOME (ctt,_) = (rewrite_inst_ thy tless_true erls_diff true subst thm ct); @@ -78,7 +79,7 @@ "----------- differentiate by rewrite -------------------"; "----------- differentiate by rewrite -------------------"; val thy = @{theory "Diff"}; -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \ 2 + 3 * x + 4)"; +val ct = TermC.parseNEW' ctxt "d_d x (x \ 2 + 3 * x + 4)"; "--- 1 ---"; val thm = @{thm "diff_sum"}; val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); @@ -101,7 +102,7 @@ "--- 7 ---"; "--- 7 ---"; val rls = Test_simplify; -val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \ (2 - 1) + 3 * 1 + 0"; +val ct = TermC.parseNEW' ctxt "2 * x \ (2 - 1) + 3 * 1 + 0"; val (ct, _) = the (rewrite_set_ thy true rls ct); if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed"; @@ -257,7 +258,7 @@ \ (Try (Repeat (Rewrite sym_frac_conv))) #> \ \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')" ; -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; "----------- diff_conv, sym_diff_conv -------------------"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/eqsystem-1.sml --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Thu May 26 12:44:51 2022 +0200 @@ -94,10 +94,10 @@ if UnparseC.term t' = "True" then () else error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; -val SOME t = TermC.parse thy "solution LL"; -TermC.atomty (Thm.term_of t); -val SOME t = TermC.parse thy "solution LL"; -TermC.atomty (Thm.term_of t); +val SOME t = TermC.parseNEW ctxt "solution LL"; +TermC.atomty t; +val SOME t = TermC.parseNEW ctxt "solution LL"; +TermC.atomty t; val t = TermC.str2term "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu May 26 12:44:51 2022 +0200 @@ -255,52 +255,52 @@ val subs = [(@{term "bdv::real"}, @{term "x::real"})]; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x"; +val t = TermC.parseNEW' ctxt "Integral x D x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "x \ 2 / 2" then () else error "Integral x D x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \ 2 + c_2 D x"; +val t = TermC.parseNEW' ctxt "Integral c * x \ 2 + c_2 D x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "c * (x \ 3 / 3) + c_2 * x" then () else error "Integral c * x \ 2 + c_2 D x"; val rls = add_new_c; -val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \ 3 / 3) + c_2 * x"; +val t = TermC.parseNEW' ctxt "c * (x \ 3 / 3) + c_2 * x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "c * (x \ 3 / 3) + c_2 * x + c_3" then () else error "integrate.sml: diff.behav. in add_new_c simpl."; -val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \ 3 / 3 + x"; +val t = TermC.parseNEW' ctxt "F x = x \ 3 / 3 + x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "F x = x \ 3 / 3 + x + c"(*not "F x + c =..."*) then () else error "integrate.sml: diff.behav. in add_new_c equation"; val rls = simplify_Integral; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) -val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \ 2 / 2) + c_2"; +val t = TermC.parseNEW' ctxt "ff x = c * x + - 1 * q_0 * (x \ 2 / 2) + c_2"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \ 2" then () else error "integrate.sml: diff.behav. in simplify_I #1"; val rls = integration; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \ 2 + c_2 D x"; +val t = TermC.parseNEW' ctxt "Integral c * x \ 2 + c_2 D x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \ 3" then () else error "integrate.sml: diff.behav. in integration #1"; -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \ 2 + 2*x + 1 D x"; +val t = TermC.parseNEW' ctxt "Integral 3*x \ 2 + 2*x + 1 D x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "c + x + x \ 2 + x \ 3" then () else error "integrate.sml: diff.behav. in integration #2"; -val t = (Thm.term_of o the o (TermC.parse thy)) +val t = TermC.parseNEW' ctxt "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2) D x"; val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2) D x"; if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \ 2 + - 1 * q_0 / 6 * x \ 3)" then () else error "integrate.sml: diff.behav. in integration #3"; -val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x"); +val t = TermC.parseNEW' ctxt ("Integral " ^ UnparseC.term res ^ " D x"); val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \ 3 + - 1 * q_0 / 24 * x \ 4)" then () else error "integrate.sml: diff.behav. in integration #4"; @@ -330,10 +330,10 @@ Find =["antiDerivative F_F"], With =[], Relate=[]}:string ppc; -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model; -val t1 = (Thm.term_of o hd) chkmodel; -val t2 = (Thm.term_of o hd o tl) chkmodel; -val t3 = (Thm.term_of o hd o tl o tl) chkmodel; +val chkmodel = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) model; +val t1 = (hd) chkmodel; +val t2 = (hd o tl) chkmodel; +val t3 = (hd o tl o tl) chkmodel; case t3 of Const (\<^const_name>\antiDerivative\, _) $ _ => () | _ => error "integrate.sml: Integrate.antiDerivative ???"; @@ -342,10 +342,10 @@ Find =["antiDerivativeName F_F"], With =[], Relate=[]}:string ppc; -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model; -val t1 = (Thm.term_of o hd) chkmodel; -val t2 = (Thm.term_of o hd o tl) chkmodel; -val t3 = (Thm.term_of o hd o tl o tl) chkmodel; +val chkmodel = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) model; +val t1 = (hd) chkmodel; +val t2 = (hd o tl) chkmodel; +val t3 = (hd o tl o tl) chkmodel; case t3 of Const (\<^const_name>\antiDerivativeName\, _) $ _ => () | _ => error "integrate.sml: Integrate.antiDerivativeName"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/poly-1.sml --- a/test/Tools/isac/Knowledge/poly-1.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/poly-1.sml Thu May 26 12:44:51 2022 +0200 @@ -45,135 +45,138 @@ "-------- fun has_degree_in --------------------------------------------------------------------"; "-------- fun has_degree_in --------------------------------------------------------------------"; "-------- fun has_degree_in --------------------------------------------------------------------"; -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "1"; +val thy = @{theory} +val ctxt = Proof_Context.init_global thy +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "1"; if has_degree_in t v = 0 then () else error "has_degree_in (1) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "1"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "1"; if has_degree_in t v = 0 then () else error "has_degree_in (1) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "a*b+c"; if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "a*b+c"; if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "a*x+c"; if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "a*AA+c"; if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \ 7"; +val v = TermC.parseNEW' ctxt "x::real"; +val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \ 7"; if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \ 7) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \ 7"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \ 7"; if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \ 7) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "x \ 7"; +val v = TermC.parseNEW' ctxt "x::real"; +val t = TermC.parseNEW' ctxt "x \ 7"; if has_degree_in t v = 7 then () else error "has_degree_in (x \ 7) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \ 7"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "AA \ 7"; if has_degree_in t v = 7 then () else error "has_degree_in (AA \ 7) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x"; +val v = TermC.parseNEW' ctxt "x::real"; +val t = TermC.parseNEW' ctxt "(a*b+c)*x::real"; if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "(a*b+c)*AA"; if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x"; +val v = TermC.parseNEW' ctxt "x::real"; +val t = TermC.parseNEW' ctxt "(a*b+x)*x"; if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA"; if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "x"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "x"; if has_degree_in t v = 1 then () else error "has_degree_in (x) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "AA"; if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x"; +val v = TermC.parseNEW' ctxt "x::real"; +val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)"; if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA"; if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA"; "-------- fun mono_deg_in ----------------------------------------------------------------------"; "-------- fun mono_deg_in ----------------------------------------------------------------------"; "-------- fun mono_deg_in ----------------------------------------------------------------------"; -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; +val v = TermC.parseNEW' ctxt "x::real"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \ 7"; +val t = TermC.parseNEW' ctxt "(a*b+c)*x \ 7"; if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \ 7) x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "x \ 7"; +val t = TermC.parseNEW' ctxt "(x::real) \ 7"; if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \ 7) x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x"; +val t = TermC.parseNEW' ctxt "(a*b+c)*x::real"; if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x"; +val t = TermC.parseNEW' ctxt "(a*b+x)*x"; if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "x"; +val t = TermC.parseNEW' ctxt "x::real"; if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)"; +val t = TermC.parseNEW' ctxt "(a*b+c)"; if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x"; +val t = TermC.parseNEW' ctxt "ab - (a*b)*x"; if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed"; (*. . . . . . . . . . . . the same with Const (\<^const_name>\AA\, _) . . . . . . . . . . . *) val thy = @{theory Partial_Fractions} -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; +val ctxt = Proof_Context.init_global thy +val v = TermC.parseNEW' ctxt "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \ 7"; +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \ 7"; if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \ 7) AA changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \ 7"; +val t = TermC.parseNEW' ctxt "AA \ 7"; if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \ 7) AA changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA"; +val t = TermC.parseNEW' ctxt "(a*b+c)*AA"; if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA"; +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA"; if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "AA"; +val t = TermC.parseNEW' ctxt "AA"; if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)"; +val t = TermC.parseNEW' ctxt "(a*b+c)"; if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed"; -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA"; +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA"; if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed"; @@ -696,6 +699,7 @@ "-------- norm_Poly with AlgEin ----------------------------------------------------------------"; "-------- norm_Poly with AlgEin ----------------------------------------------------------------"; val thy = @{theory AlgEin}; +val ctxt = Proof_Context.init_global thy; val SOME (f',_) = rewrite_set_ thy false norm_Poly (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben"); @@ -787,7 +791,7 @@ else error "poly.sml: diff.behav. in make_polynomial 20"; "-----SPO ---"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a \ 2 * (-a) \ 2"; +val t = TermC.parseNEW' ctxt "a \ 2 * (-a) \ 2"; val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t; if (UnparseC.term t) = "a \ 4" then () else error "poly.sml: diff.behav. in make_polynomial 24"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/polyeq-1.sml --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu May 26 12:44:51 2022 +0200 @@ -51,55 +51,56 @@ "----------- tests on predicates in problems ---------------------"; "----------- tests on predicates in problems ---------------------"; val thy = @{theory}; +val ctxt = Proof_Context.init_global thy; Rewrite.trace_on:=false; (*true false*) - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \ 2 = 0)"; + val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \ 2 = 0)"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; if ((UnparseC.term t) = "- 8 - 2 * x + x \ 2") then () else error "polyeq.sml: diff.behav. in lhs"; - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \ 2) is_expanded_in x"; + val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \ 2) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. 1 in is_expended_in"; - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x"; + val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0; if (UnparseC.term t) = "False" then () else error "polyeq.sml: diff.behav. 2 in is_poly_in"; - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \ 2) is_poly_in x"; + val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \ 2) is_poly_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. 3 in is_poly_in"; - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \ 2 = 0)) is_expanded_in x"; + val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \ 2 = 0)) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. 4 in is_expended_in"; - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \ 2 = 0)) is_expanded_in x"; + val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \ 2 = 0)) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. 5 in is_expended_in"; - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \ 2) has_degree_in x) = 2"; + val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \ 2) has_degree_in x) = 2"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. in has_degree_in_in"; - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2"; + val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (UnparseC.term t) = "False" then () else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; - val t4 = (Thm.term_of o the o (TermC.parse thy)) + val t4 = TermC.parseNEW' ctxt "((-8 - 2*x + x \ 2) has_degree_in x) = 1"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; if (UnparseC.term t) = "False" then () else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; -val t5 = (Thm.term_of o the o (TermC.parse thy)) +val t5 = TermC.parseNEW' ctxt "((-8 - 2*x + x \ 2) has_degree_in x) = 2"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5; if (UnparseC.term t) = "True" then () @@ -134,7 +135,7 @@ ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy (*Aufgabe zum Einstieg in die Arbeit...*) - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \ 2 = 0"; + val t = TermC.parseNEW' ctxt "a*b - (a+b)*x + x \ 2 = 0"; (*ein 'ruleset' aus Poly.ML wird angewandt...*) val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; UnparseC.term t; @@ -164,9 +165,9 @@ *) "------ 15.11.02 --------------------------"; - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x"; - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv"; - val a = (Thm.term_of o the o (TermC.parse thy)) "a"; + val t = TermC.parseNEW' ctxt "1 + a * x + b * x"; + val bdv = TermC.parseNEW' ctxt "bdv"; + val a = TermC.parseNEW' ctxt "a"; Rewrite.trace_on := false; (*true false*) (* Anwenden einer Regelmenge aus Termorder.ML: *) @@ -178,7 +179,7 @@ UnparseC.term t; "1 + b * x + x * a"; - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \ 2"; + val t = TermC.parseNEW' ctxt "1 + a * (x + b * x) + a \ 2"; val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; UnparseC.term t; @@ -187,7 +188,7 @@ UnparseC.term t; "1 + (x + b * x) * a + a \ 2"; - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \ 2 * x + b * a + 7*a \ 2"; + val t = TermC.parseNEW' ctxt "1 + a \ 2 * x + b * a + 7*a \ 2"; val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; UnparseC.term t; @@ -207,7 +208,7 @@ get_thm Termorder.thy "bdv_n_collect"; get_thm (theory "Isac_Knowledge") "bdv_n_collect"; *) - val t = (Thm.term_of o the o (TermC.parse thy)) "a \ 2 * x + 7 * a \ 2"; + val t = TermC.parseNEW' ctxt "a \ 2 * x + 7 * a \ 2"; val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; UnparseC.term t; @@ -340,14 +341,14 @@ "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")]; - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")]; - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")]; + val substa = [(TermC.empty, TermC.parseNEW' ctxt "a::real")]; + val substb = [(TermC.empty, TermC.parseNEW' ctxt "b::real")]; + val substx = [(TermC.empty, TermC.parseNEW' ctxt "x::real")]; - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x"; - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b"; + val x1 = TermC.parseNEW' ctxt "a + b + x::real"; + val x2 = TermC.parseNEW' ctxt "a + x + b::real"; + val x3 = TermC.parseNEW' ctxt "a + x + b::real"; + val x4 = TermC.parseNEW' ctxt "x + a + b::real"; if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then () else error "termorder.sml diff.behav ord_make_polynomial_in #1"; @@ -358,22 +359,22 @@ if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then () else error "termorder.sml diff.behav ord_make_polynomial_in #3"; - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; - ord_make_polynomial_in false(*true*) thy substx (aa, bb); - true; (* => LESS *) + val aa = TermC.parseNEW' ctxt "- 1 * a * x::real"; + val bb = TermC.parseNEW' ctxt "x \ 3::real"; +if ord_make_polynomial_in false(*true*) thy substx (aa, bb) = true(*LESS *) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #4"; - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; - ord_make_polynomial_in false(*true*) thy substa (aa, bb); - false; (* => GREATER *) + val aa = TermC.parseNEW' ctxt "- 1 * a * x"; + val bb = TermC.parseNEW' ctxt "x \ 3"; +if ord_make_polynomial_in false(*true*) thy substa (aa, bb) = false(*GREATER*) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #5"; (* und nach dem Re-engineering der Termorders in den 'rulesets' kannst Du die 'gr"osste' Variable frei w"ahlen: *) - val bdv= TermC.str2term "bdv ::real"; - val x = TermC.str2term "x ::real"; - val a = TermC.str2term "a ::real"; - val b = TermC.str2term "b ::real"; + val bdv= TermC.parseNEW' ctxt "bdv ::real"; + val x = TermC.parseNEW' ctxt "x ::real"; + val a = TermC.parseNEW' ctxt "a ::real"; + val b = TermC.parseNEW' ctxt "b ::real"; val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; if UnparseC.term t' = "b + x + a" then () else error "termorder.sml diff.behav ord_make_polynomial_in #11"; @@ -385,13 +386,13 @@ else error "termorder.sml diff.behav ord_make_polynomial_in #13"; val ppp' = "-6 + -5*x + x \ 3 + - 1*x \ 2 + - 1*x \ 3 + - 14*x \ 2"; - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp'; + val ppp = TermC.parseNEW' ctxt ppp'; val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \ 2" then () else error "termorder.sml diff.behav ord_make_polynomial_in #15"; val ttt' = "(3*x + 5)/18 ::real"; - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt'; + val ttt = TermC.parseNEW' ctxt ttt'; val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; if UnparseC.term uuu = "(5 + 3 * x) / 18" then () else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; @@ -1060,7 +1061,7 @@ "-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; "-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; "---- test the erls ----"; - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \ 2 - 1"; + val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \ 2 - 1"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1; val t' = UnparseC.term t; (*if t'= \<^const_name>\True\ then () diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu May 26 12:44:51 2022 +0200 @@ -31,6 +31,7 @@ "--------------------------------------------------------"; val thy = @{theory "PolyMinus"}; +val ctxt = Proof_Context.init_global thy; "----------- fun identifier --------------------------------------------------------------------"; "----------- fun identifier --------------------------------------------------------------------"; @@ -341,7 +342,7 @@ \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \ \ (Try (Rewrite_Set fasse_zusammen False)) #> \ \ (Try (Rewrite_Set verschoenere False))) t_t)" -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; TermC.atomty sc; "----------- me simplification.for_polynomials.with_minus"; @@ -448,7 +449,7 @@ \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \ \ (Try (Repeat (Calculate ''PLUS''))) #> \ \ (Try (Repeat (Calculate ''MINUS''))))) e_e)" -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; TermC.atomty sc; "----------- pbl polynom probe -----------------------------------"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu May 26 12:44:51 2022 +0200 @@ -20,22 +20,22 @@ "------------ pbl: rational, univariate, equation ----------------"; "------------ pbl: rational, univariate, equation ----------------"; "------------ pbl: rational, univariate, equation ----------------"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(1/b+1/x=1) is_ratequation_in x"; +val t = TermC.parseNEW' ctxt "(1/b+1/x=1) is_ratequation_in x"; val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t; val result = UnparseC.term t_; if result <> "True" then error "rateq.sml: new behaviour 1:" else (); -val t = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)=1) is_ratequation_in x"; +val t = TermC.parseNEW' ctxt "(sqrt(x)=1) is_ratequation_in x"; val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t; val result = UnparseC.term t_; if result <> "False" then error "rateq.sml: new behaviour 2:" else (); -val t = (Thm.term_of o the o (TermC.parse thy)) "(x=- 1) is_ratequation_in x"; +val t = TermC.parseNEW' ctxt "(x=- 1) is_ratequation_in x"; val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t; val result = UnparseC.term t_; if result <> "False" then error "rateq.sml: new behaviour 3:" else (); -val t = (Thm.term_of o the o (TermC.parse thy)) "(3 + x \ 2 + 1/(x \ 2+3)=1) is_ratequation_in x"; +val t = TermC.parseNEW' ctxt "(3 + x \ 2 + 1/(x \ 2+3)=1) is_ratequation_in x"; val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t; val result = UnparseC.term t_; if result <> "True" then error "rateq.sml: new behaviour 4:" else (); @@ -61,7 +61,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*)); +case nxt of (Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*)); val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* WN120317.TODO dropped rateq: here "x ~= 0 should TermC.sub_at to ctxt, but it does not: @@ -92,7 +92,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt; f2str f = "[x = 1 / 5]"; -case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*)); +case nxt of (Check_elementwise "Assumptions") => () | _ => ((*not checked before*)); "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); val (pt, p) = case Step.by_tactic tac (pt,p) of ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. Step.by_tactic"; @@ -198,11 +198,14 @@ if p = ([4, 3], Pbl) then () else (case nxt of - ("Add_Given", Add_Given "solveFor x") => + (Add_Given "equality (320 + 128 * x + - 16 * x \ 2 = 0)") => (case f of - Test_Out.PpcKF (Problem [], {Given = [Incompl "solveFor", Correct "equality (320 + 128 * x + - 16 * x \ 2 = 0)"], ...}) => () + Test_Out.PpcKF (Test_Out.Problem [], { + Find = [Incompl "solutions []"], Given = [Incompl "equality", Incompl "solveFor"], + Relate = [], Where = [False "matches (?a + ?v_ \ 2 = 0) e_e \\nmatches (?a + ?b * ?v_ \ 2 = 0) e_e"], + With = []}) => () | _ => error ("S.68, Bsp.: 40 PblObj changed")) - | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string (snd nxt))); + | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string (nxt))); val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* ("Subproblem", Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) *) @@ -216,7 +219,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -if p = ([], Res) andalso f2str f = "[]" then () +if p = ([], Res) andalso f2str f = "[x = - 2, x = 10]" then () else error "rateq.sml: new behaviour: [x = - 2, x = 10]"; "----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------"; @@ -240,11 +243,9 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + - 1 * x + x \ 2) * x = 1 * (9 * x + -6 * x \ 2 + x \ 3)"; (*+*)if eq_set op = (Ctree.get_assumptions pt p |> map UnparseC.term, -(*+*) ["x \ 0", -(*+*) "9 * x + -6 * x \ 2 + x \ 3 \ 0", -(*+*) "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) =\n1 / x is_ratequation_in x"]) +(*+*) ["x \ 0", "9 * x + - 6 * x \ 2 + x \ 3 \ 0", "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) =\n1 / x is_ratequation_in x"]) (*+*)then () else error "assumptions before 1. Subproblem CHANGED"; -(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \ 2) * x = 1 * (9 * x + -6 * x \ 2 + x \ 3)" +(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \ 2) * x = 1 * (9 * x + - 6 * x \ 2 + x \ 3)" (*+*)then (*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => () (*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt))) @@ -263,7 +264,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \ 2 = 0"; -if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x \ 2 = 0" +if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \ 2 = 0" then ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => () | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt))) @@ -286,12 +287,12 @@ (* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [ (*0.pre*) "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) =\n1 / x is_ratequation_in x", -(*1.pre*) "\ matches (?a = 0)\n ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + -6 * x \ 2 + x \ 3)) \\n" -(*1.pre*) ^ "\ lhs ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + -6 * x \ 2 + x \ 3)) is_poly_in x", -(*2.pre*) "lhs (-6 * x + 5 * x \ 2 = 0) is_poly_in x", -(*2.pre*) "lhs (-6 * x + 5 * x \ 2 = 0) has_degree_in x = 2", +(*1.pre*) "\ matches (?a = 0)\n ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + - 6 * x \ 2 + x \ 3)) \\n" +(*1.pre*) ^ "\ lhs ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + - 6 * x \ 2 + x \ 3)) is_poly_in x", +(*2.pre*) "lhs (- 6 * x + 5 * x \ 2 = 0) is_poly_in x", +(*2.pre*) "lhs (- 6 * x + 5 * x \ 2 = 0) has_degree_in x = 2", (*0.asm*) "x \ 0", -(*0.asm*) "9 * x + -6 * x \ 2 + x \ 3 \ 0" +(*0.asm*) "9 * x + - 6 * x \ 2 + x \ 3 \ 0" (* *)]) (* *)then () else error "assumptions at end 2. Subproblem CHANGED"; @@ -306,12 +307,14 @@ (*/-------- final test -----------------------------------------------------------------------\*) if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p), - ["x = 6 / 5", "lhs (-6 * x + 5 * x \ 2 = 0) is_poly_in x", - "lhs (-6 * x + 5 * x \ 2 = 0) has_degree_in x = 2", - "\ matches (?a = 0)\n ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + -6 * x \ 2 + x \ 3)) \\n\ lhs ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + -6 * x \ 2 + x \ 3)) is_poly_in x", - "x \ 0", "9 * x + -6 * x \ 2 + x \ 3 \ 0", - "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) =\n1 / x is_ratequation_in x"]) -then () else error "test CHANGED"; + ["x = 6 / 5", + "lhs (- 6 * x + 5 * x \ 2 = 0) is_poly_in x", + "lhs (- 6 * x + 5 * x \ 2 = 0) has_degree_in x = 2", + "\ matches (?a = 0)\n ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + - 6 * x \ 2 + x \ 3)) \\n\ lhs ((3 + - 1 * x + x \ 2) * x =\n 1 * (9 * x + - 6 * x \ 2 + x \ 3)) is_poly_in x", + "x \ 0", + "9 * x + - 6 * x \ 2 + x \ 3 \ 0", + "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) =\n1 / x is_ratequation_in x"] +) then () else error "test CHANGED"; "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------"; @@ -328,18 +331,18 @@ (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*) (*+*)if (get_istate_LI pt p |> Istate.string_of) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*) -(*+*) = "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)" +(*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)" (*+*)then () else error "rat-eq + subpbl: istate in specify-phase"; (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*) (*+*)if (get_istate_LI pt p |> Istate.string_of) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*) -(*+*) = "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)" +(*+*) = "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)" (*+*)then () else error "rat-eq + subpbl: istate after found_accept"; (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_eliminate"*) (* \ 2*05*) -\ ML \ + (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*) (*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Model_Problem*) @@ -353,21 +356,22 @@ (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**) (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**) -(*[4,3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*) -(*[4,3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*) +(*[4,4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Problem ["degree_1", "polynomial", "univariate", "equation"]*) +(*[4,4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*) (* \ 2*15*) -(*[4,3,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*) -(*[4,3,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*) -(*[4,3,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*) -(*[4,3,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*) +(*[4,4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*) +(*[4,4,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*) +(*[4,4,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*) +(*[4,4,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Or_to_List*) (* f = Test_Out.FormKF "[x = -4 / 3]" *) -(*[4, 3, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*) -(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*) +(*[4,4,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*) +(*[4,4,4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*) +(*[4,4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*) (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*) (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*) (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*) -if p = ([], Res) andalso f2str f = "[x = -4 / 3]" +if p = ([], Res) andalso f2str f = "[x = - 4 / 3]" then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1" else error "rat-eq + subpbl: end CHANGED 2"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/rational-2.sml --- a/test/Tools/isac/Knowledge/rational-2.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/rational-2.sml Thu May 26 12:44:51 2022 +0200 @@ -755,7 +755,7 @@ if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso ThmC.string_of_thm thm = (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"} - (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \ 2"))) then () + (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \ 2"))) then () else error "rational.sml next_rule (9 - x \ 2) / (9 - 6 * x + x \ 2)"; \---------------------------------------------------------------------------------------/*) @@ -774,7 +774,7 @@ val SOME (r as (Thm (str, thm))) = nex revsets t; if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"} - (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \ 2"))) then () + (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \ 2"))) then () else error "rational.sml next_rule (9 - x \ 2) / (9 - 6 * x + x \ 2)"; (*check the next rule*) @@ -1607,7 +1607,8 @@ "-------- fun eval_get_denominator -------------------------------------------"; "-------- fun eval_get_denominator -------------------------------------------"; val thy = @{theory Isac_Knowledge}; -val t = Thm.term_of (the (TermC.parse thy "get_denominator ((a +x)/b)")); +val ctxt = Proof_Context.init_global thy; +val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)"; val SOME (_, t') = eval_get_denominator "" 0 t thy; if UnparseC.term t' = "get_denominator ((a + x) / b) = b" then () else error "get_denominator ((a + x) / b) = b" diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu May 26 12:44:51 2022 +0200 @@ -21,43 +21,44 @@ (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic (b) of this is a case of indeterminism due to something elementary. -*) +*) val thy = @{theory "RootRatEq"}; +val ctxt = Proof_Context.init_global thy; "------------ tests on predicates -------------------------------"; "------------ tests on predicates -------------------------------"; "------------ tests on predicates -------------------------------"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - sqrt(x) + x \ 2) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(-8 - sqrt(x) + x \ 2) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "False" then () else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/x) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(1/x) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "False" then () else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(1/sqrt(x)) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "False" then () else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "True" then () else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "True" then () else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "True" then () else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; +val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (UnparseC.term t) = "True" then () else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/MathEngBasic/rewrite.sml --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Thu May 26 12:44:51 2022 +0200 @@ -36,7 +36,7 @@ val thy = @{theory Complex_Main}; val ctxt = @{context}; val thm = @{thm add.commute}; -val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s"); +val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)"; "----- from old: fun rewrite__"; val bdv = []; val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)); @@ -488,7 +488,7 @@ "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------"; val thy = @{theory RatEq}; val ctxt = Proof_Context.init_global thy; -val SOME t = parseNEW ctxt "(3 + -1 * x + x \ 2) / (9 * x + -6 * x \ 2 + x \ 3) = 1 / x"; +val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \ 2) / (9 * x + -6 * x \ 2 + x \ 3) = 1 / x"; val rls = assoc_rls "RatEq_eliminate" val SOME (t''''', asm''''') = diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/MathEngine/mathengine-stateless.sml --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 26 12:44:51 2022 +0200 @@ -299,8 +299,7 @@ (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo); "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) = (cs', (encode ifo)); -val SOME f_in = TermC.parse (ThyC.get_theory "Isac_Knowledge") istr - val f_in = Thm.term_of f_in +val SOME f_in = TermC.parseNEW (get_ctxt pt pos) istr val f_succ = get_curr_formula (pt, pos); f_succ = f_in = false; val NONE = CAS_Cmd.input f_in diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Minisubpbl/800-append-on-Frm.sml --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu May 26 12:44:51 2022 +0200 @@ -95,8 +95,7 @@ (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); "~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo)); - val SOME f_in =(*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*); - val f_in = Thm.term_of f_in + val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*); val pos_pred = lev_back(*'*) pos val f_pred = Ctree.get_curr_formula (pt, pos_pred); val f_succ = Ctree.get_curr_formula (pt, pos); diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Thu May 26 12:44:51 2022 +0200 @@ -131,13 +131,14 @@ (*--------------(2): does divide work in Test_simplify ?: ------*) val thy = @{theory Test}; - val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2"; + val ctxt = (ThyC.id_to_ctxt "Test") + val t = TermC.parseNEW' ctxt "6 / 2"; val rls = Test_simplify; val (t,_) = the (rewrite_set_ thy false rls t); (*val t = Free ("3", "Real.real") : term*) (*--------------(3): is_num works ?: -------------------------------------*) - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num"; + val t = TermC.parseNEW' ctxt "2 is_num"; TermC.atomty t; rewrite_set_ @{theory Test} false tval_rls t; (*val it = SOME (Const (\<^const_name>\True\, "bool"),[]) ... works*) @@ -153,19 +154,19 @@ Rewrite.trace_on := false; (*true false*) val thy = @{theory Test}; val rls = Test_simplify; - val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2"; + val t = TermC.parseNEW' ctxt "(-4) / 2"; val SOME (_, t) = eval_cancel "xxx" \<^const_name>\divide\ t thy; (*--------------(5): reproduce (1) with simpler term: ------------*) - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2"; + val t = TermC.parseNEW' ctxt "(3+5)/(2::real)"; case rewrite_set_ thy false rls t of SOME (t', []) => if UnparseC.term t' = "4" then () else error "rewrite_set_ (3+5)/2 changed 1" | _ => error "rewrite_set_ (3+5)/2 changed 2"; - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2"; + val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)"; case rewrite_set_ thy false rls t of SOME (t', _) => if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1" @@ -203,7 +204,7 @@ (*===================*) Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*) - val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2"; + val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)"; val SOME (res, []) = rewrite_set_ thy false rls t; if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed"; "x + (-4) / 2"; @@ -227,17 +228,17 @@ " ================= evaluate.sml: calculate_ 2002 =================== "; val thy = @{theory Test}; -val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3"; + val t = TermC.parseNEW' ctxt "12 / 3"; val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; "12 / 3 = 4"; val thy = @{theory Test}; -val t = (Thm.term_of o the o (TermC.parse thy)) "4 \ 2"; + val t = TermC.parseNEW' ctxt "4 \ 2"; val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; "4 ^ 2 = 16"; - val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \ 2"; + val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \ 2"; val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; "1 + 2 = 3"; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; @@ -262,7 +263,7 @@ else (); (*13.9.02 *** calc: operator = pow not defined*) - val t = (Thm.term_of o the o (TermC.parse thy)) "3 \ 2"; + val t = TermC.parseNEW' ctxt "3 \ 2"; val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; (*** calc: operator = pow not defined*) diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/ProgLang/prog_expr.sml --- a/test/Tools/isac/ProgLang/prog_expr.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Thu May 26 12:44:51 2022 +0200 @@ -89,7 +89,7 @@ "-------- fun eval_is_num ----------------------------------------------------------------------"; "-------- fun eval_is_num ----------------------------------------------------------------------"; "-------- fun eval_is_num ----------------------------------------------------------------------"; -val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num"; +val t = TermC.parseNEW' ctxt "2 is_num"; case rewrite_set_ @{theory Test} false tval_rls t of SOME (Const (\<^const_name>\True\, _), []) => () | _ => error "2 is_num CHANGED"; @@ -201,6 +201,7 @@ "-------- fun eval_equal for x \ 0: \ indetermined, NOT \ 'True' -----------------------------"; "-------- fun eval_equal for x \ 0: \ indetermined, NOT \ 'True' -----------------------------"; val thy = @{theory} +val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge") val t = TermC.str2term "x = 0"; val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\HOL.eq\ t thy; @@ -251,84 +252,84 @@ "-------- fun eval_occurs_in -------------------------------------------------------------------"; "-------- fun eval_occurs_in -------------------------------------------------------------------"; "-------- fun eval_occurs_in -------------------------------------------------------------------"; -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "1"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "1"; if occurs_in v t then error "factor_right_deg (1) x ..changed" else (); -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "1"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "1"; if occurs_in v t then error "factor_right_deg (1) AA ..changed" else (); (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "a*b+c"; if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else (); -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "a*b+c"; if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else (); (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "a*x+c"; if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "a*AA+c"; if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \ 7"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "(a*b+c)*x \ 7"; if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \ 7) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \ 7"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \ 7"; if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \ 7) AA ..changed"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "x \ 7"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "x \ 7"; if occurs_in v t then () else error "factor_right_deg (x \ 7) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \ 7"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "AA \ 7"; if occurs_in v t then () else error "factor_right_deg (AA \ 7) AA ..changed"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "(a*b+c)*x"; if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "(a*b+c)*AA"; if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "(a*b+x)*x"; if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA"; if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "x"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "x"; if occurs_in v t then () else error "factor_right_deg (x) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "AA"; if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed"; (*----------*) -val v = (Thm.term_of o the o (TermC.parse thy)) "x"; -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x"; +val v = TermC.parseNEW' ctxt "x"; +val t = TermC.parseNEW' ctxt "ab - (a*b)*x"; if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed"; -val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA"; +val v = TermC.parseNEW' ctxt "AA"; +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA"; if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed"; @@ -421,7 +422,7 @@ "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------"; "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------"; val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES")); -val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3"; +val t = TermC.parseNEW' ctxt "2 * (3::real)"; (*val SOME (thmid,t') = *)get_pair thy op_ ef t; ; "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) = diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Specify/refine.sml --- a/test/Tools/isac/Specify/refine.sml Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Specify/refine.sml Thu May 26 12:44:51 2022 +0200 @@ -25,20 +25,20 @@ val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}; (*case 1: no refinement *) -val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]"); -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)"); +val (d1,ts1) = Input_Descript.split (TermC.parseNEW' ctxt "fixedValues [aaa = 0]"); +val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "errorBound (ddd = 0)"); val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T; (*case 2: refined to pbt without children *) -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]"); +val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "relations [aaa333]"); val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T; (*case 3: refined to pbt with children *) -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]"); +val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "valuesFor [aaa222]"); val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T; (*case 4: refined to children (without child)*) -val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy"); +val (d3,ts3) = Input_Descript.split (TermC.parseNEW' ctxt "boundVariable aaa222yyy"); val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T; (*================================================================= diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Test_Isac.thy Thu May 26 12:44:51 2022 +0200 @@ -50,7 +50,8 @@ and find out, which ML_file or *.thy causes an error (might be ONLY one). Also backup files (#* ) recognised by jEdit cause this trouble *) (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) - "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All" +(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*) +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter" (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt" (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test" (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt" @@ -62,27 +63,30 @@ (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo" (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" ADDTESTS/------------------------------------------- see end of tests *) -(*/--- these work directly from Pure, but create problems here .. +(*/~~~ these work directly from Pure, but create problems here .. "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *) "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *) "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *) "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *) "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *) - \--- .. these work independently, but create problems here *) -(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Check_Outer_Syntax" + \~~~ .. these work independently, but create problems here *) (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers" -(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Term" +(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer" (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *) "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *) "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*) +(**) (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) +(**) begin +declare [[ML_print_depth = 20]] + ML \open ML_System\ ML \ open Kernel; @@ -129,51 +133,22 @@ open Rewrite_Ord open UnparseC \ -ML_file "BaseDefinitions/libraryC.sml" -section \code for copy & paste ===============================================================\ ML \ "~~~~~ fun xxx , args:"; val () = (); "~~~~~ and xxx , args:"; val () = (); -"~~~~~ fun xxx \fun yyy \fun zzz , return:"; val () = (); -(*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*); +"~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); "xx" -^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**) -(*/------------------- step into XXXXX -----------------------------------------------------\*) -(*-------------------- stop step into XXXXX -------------------------------------------------*) -(*\------------------- step into XXXXX -----------------------------------------------------/*) -(*-------------------- contiue step into XXXXX ----------------------------------------------*) -(*/------------------- check entry to XXXXX ------------------------------------------------\*) -(*\------------------- check entry to XXXXX ------------------------------------------------/*) -(*/------------------- check within XXXXX --------------------------------------------------\*) -(*\------------------- check within XXXXX --------------------------------------------------/*) -(*/------------------- check result of XXXXX -----------------------------------------------\*) -(*\------------------- check result of XXXXX -----------------------------------------------/*) -(* final test ...*) -(*/------------------- build new fun XXXXX -------------------------------------------------\*) -(*\------------------- build new fun XXXXX -------------------------------------------------/*) +^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) +\ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) \ ML \ +\ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) +Rewrite.trace_on := false; \ ML \ \ ML \ \ ML \ -\ -text \ - declare [[show_types]] - declare [[show_sorts]] - find_theorems "?a <= ?a" - - print_theorems - print_facts - print_statement "" - print_theory - ML_command \Pretty.writeln prt\ - declare [[ML_print_depth = 999]] - declare [[ML_exception_trace]] -\ - -section \===================================================================================\ -ML \ \ ML \ \ ML \ \ ML \ @@ -189,8 +164,6 @@ (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); \ -(*---------------------- check test file by testfile ------------------------------------------- - ---------------------- check test file by testfile -------------------------------------------*) section \trials with Isabelle's functions\ ML \"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\ ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML" @@ -202,6 +175,7 @@ section \test ML Code of isac\ subsection \basic code first\ ML \"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\ + ML_file "BaseDefinitions/base-definitions.sml" ML_file "BaseDefinitions/libraryC.sml" ML_file "BaseDefinitions/rule-def.sml" ML_file "BaseDefinitions/eval-def.sml" @@ -216,9 +190,9 @@ ML_file "BaseDefinitions/calcelems.sml" ML_file "BaseDefinitions/termC.sml" ML_file "BaseDefinitions/substitution.sml" - ML_file "BaseDefinitions/contextC.sml" + ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*) ML_file "BaseDefinitions/environment.sml" - ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) +(** )ML_file "BaseDefinitions/kestore.sml"( *setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) @@ -259,7 +233,7 @@ ML_file "MathEngBasic/thmC.sml" ML_file "MathEngBasic/rewrite.sml" ML_file "MathEngBasic/tactic.sml" - ML_file "MathEngBasic/ctree.sml" + ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*) ML_file "MathEngBasic/calculation.sml" ML_file "Specify/formalise.sml" @@ -294,7 +268,6 @@ ML_file "BridgeLibisabelle/thy-present.sml" ML_file "BridgeLibisabelle/mathml.sml" (*part.*) - ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*) ML_file "BridgeLibisabelle/thy-hierarchy.sml" ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) ML_file "BridgeLibisabelle/interface.sml" @@ -306,9 +279,9 @@ ML_file "Knowledge/delete.sml" ML_file "Knowledge/descript.sml" ML_file "Knowledge/simplify.sml" - ML_file "Knowledge/poly.sml" ML_file "Knowledge/gcd_poly_ml.sml" - ML_file "Knowledge/rational.sml" (*Test_Isac_Short*) + ML_file "Knowledge/rational-1.sml" + ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*) ML_file "Knowledge/equation.sml" ML_file "Knowledge/root.sml" ML_file "Knowledge/lineq.sml" @@ -325,7 +298,8 @@ (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) ML_file "Knowledge/diff.sml" ML_file "Knowledge/integrate.sml" - ML_file "Knowledge/eqsystem.sml" + ML_file "Knowledge/eqsystem-1.sml" + ML_file "Knowledge/eqsystem-2.sml" ML_file "Knowledge/test.sml" ML_file "Knowledge/polyminus.sml" ML_file "Knowledge/vect.sml" diff -r 6a5f3a2e6d3a -r c3acf9c442ac test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Tue May 24 16:47:31 2022 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu May 26 12:44:51 2022 +0200 @@ -1,4 +1,4 @@ -(* Title: All tests on isac (some outcommented since Isabelle2002-->2009- 2) +(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) Author: Walther Neuper 101001 (c) copyright due to license terms. @@ -166,7 +166,7 @@ section \trials with Isabelle's functions\ ML \"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\ - ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML" + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML" ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML" ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML" ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML" @@ -190,9 +190,9 @@ ML_file "BaseDefinitions/calcelems.sml" ML_file "BaseDefinitions/termC.sml" ML_file "BaseDefinitions/substitution.sml" - ML_file "BaseDefinitions/contextC.sml" + ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*) ML_file "BaseDefinitions/environment.sml" -(** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) +(**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) @@ -271,7 +271,7 @@ ML_file "BridgeLibisabelle/mathml.sml" (*part.*) ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml" ML_file "BridgeLibisabelle/thy-hierarchy.sml" - ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*) + ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) ML_file "BridgeLibisabelle/interface.sml" ML_file "BridgeJEdit/parseC.sml" ML_file "BridgeJEdit/preliminary.sml" @@ -389,7 +389,7 @@ migration from "isabelle tty" --> libisabelle \ -subsection \isac on Isabelle2013- 2\ +subsection \isac on Isabelle2013-2\ subsubsection \Summary of development\ text \ reactivated context_thy @@ -402,17 +402,17 @@ text \ TODO : - : isac on Isablle2013- 2 + : isac on Isablle2013-2 : Changeset: 55318 (03826ceb24da) merged User: Walther Neuper - Date: 2013- 12- 12 14:27:37 +0100 (7 minutes) + Date: 2013-12-12 14:27:37 +0100 (7 minutes) \ -subsection \isac on Isabelle2013- 1\ +subsection \isac on Isabelle2013-1\ subsubsection \Summary of development\ text \ - Isabelle2013- 1 was replaced within a few weeks due to problems with the document model; + Isabelle2013-1 was replaced within a few weeks due to problems with the document model; no significant development steps for ISAC. \ subsubsection \State of tests\ @@ -423,13 +423,13 @@ text \ Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy User: Walther Neuper - Date: 2013- 12-03 18:13:31 +0100 (8 days) + Date: 2013-12-03 18:13:31 +0100 (8 days) : - : isac on Isablle2013- 1 + : isac on Isablle2013-1 : - Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013- 1: Test_Isac perfect + Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect User: Walther Neuper - Date: 2013- 11- 21 18:12:17 +0100 (2 weeks) + Date: 2013-11-21 18:12:17 +0100 (2 weeks) \ @@ -443,7 +443,7 @@ \ subsubsection \Run tests\ text \ - Is standard now; this subsection will be discontinued under Isabelle2013- 1 + Is standard now; this subsection will be discontinued under Isabelle2013-1 \ subsubsection \State of tests\ text \ @@ -460,7 +460,7 @@ : Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013 User: Walther Neuper - Date: 2013-07- 15 08:28:50 +0200 (4 weeks) + Date: 2013-07-15 08:28:50 +0200 (4 weeks) \ subsection \isac on Isabelle2012\ @@ -484,13 +484,13 @@ in parallel with evaluation. Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant) - yields 69 hits, some of which were already present before Isabelle2002-->2009- 2 + yields 69 hits, some of which were already present before Isabelle2002-->2009-2 (i.e. on the old notebook from 2002). Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin: # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002 - # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009- 2 === , most likely go back to 2002 + # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml. Some tests have been re-activated (e.g. error patterns, fill patterns). @@ -499,17 +499,17 @@ text \ Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012 User: Walther Neuper - Date: 2013-07- 11 16:58:31 +0200 (4 weeks) + Date: 2013-07-11 16:58:31 +0200 (4 weeks) : : isac on Isablle2012 : Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012 User: Walther Neuper - Date: 2012-09- 24 18:35:13 +0200 (8 months) + Date: 2012-09-24 18:35:13 +0200 (8 months) ------------------------------------------------------------------------------ Changeset: 48756 (7443906996a8) merged User: Walther Neuper - Date: 2012-09- 24 18:15:49 +0200 (8 months) + Date: 2012-09-24 18:15:49 +0200 (8 months) \ subsection \isac on Isabelle2011\ @@ -547,7 +547,7 @@ The list below records TODOs while producing an ISAC kernel for gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING - (so to be resumed with Isabelle2013- 1): + (so to be resumed with Isabelle2013-1): ############## WNxxxxxx.TODO can be found in sources ############## -------------------------------------------------------------------------------- WN111013.TODO: lots of cleanup/removal in test/../Test.thy @@ -569,7 +569,7 @@ -------------------------------------------------------------------------------- WN120317.TODO changeset 977788dfed26 dropped rateq: # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002 - # test --- solve (1/x = 5, x) by me --- and --- x / (x \ 2 - 6 * x + 9) - ...: + # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...: investigation Check_elementwise stopped due to too much effort finding out, why Check_elementwise worked in 2002 in spite of the error. -------------------------------------------------------------------------------- @@ -583,11 +583,11 @@ -------------------------------------------------------------------------------- WN120320.TODO check-improve rlsthmsNOTisac: DONE make test --- old compute rlsthmsNOTisac by eq_thmI' - DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09- 2.sml .. Isac.thy + DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab # mark twice thms (in isac + (later) in Isabelle) in Isac.thy -------------------------------------------------------------------------------- - WN120320.TODO rlsthmsNOTisac: replace twice thms \ + WN120320.TODO rlsthmsNOTisac: replace twice thms ^ -------------------------------------------------------------------------------- WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac. @@ -692,18 +692,18 @@ ------------------------------------------------------------------------------ Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files User: Walther Neuper - Date: 2012-09- 24 16:39:30 +0200 (8 months) + Date: 2012-09-24 16:39:30 +0200 (8 months) : : isac on Isablle2011 : Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011 Branch: decompose-isar User: Walther Neuper - Date: 2011-02- 25 13:04:56 +0100 (2011-02- 25) + Date: 2011-02-25 13:04:56 +0100 (2011-02-25) ------------------------------------------------------------------------------ \ -subsection \isac on Isabelle2009- 2\ +subsection \isac on Isabelle2009-2\ subsubsection \Summary of development\ text \ In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg. @@ -716,14 +716,14 @@ WN131021 this is broken by installation of Isabelle2011/12/13, because all these write their binaries to ~/.isabelle/heaps/.. - $ cd /usr/local/isabisac09- 2/ + $ cd /usr/local/isabisac09-2/ $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!! \ subsubsection \State of tests\ text \ - Most tests are broken by the update from Isabelle2002 to Isabelle2009- 2. + Most tests are broken by the update from Isabelle2002 to Isabelle2009-2. \ subsubsection \Changesets of begin and end\ text \ @@ -734,12 +734,12 @@ User: Marco Steger Date: 2011-02-06 18:30:28 +0100 (2011-02-06) : - : isac on Isablle2009- 2 + : isac on Isablle2009-2 : - Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009- 2 - Branch: isac-from-Isabelle2009- 2 + Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2 + Branch: isac-from-Isabelle2009-2 User: Walther Neuper - Date: 2010-07- 21 09:59:35 +0200 (2010-07- 21) + Date: 2010-07-21 09:59:35 +0200 (2010-07-21) ------------------------------------------------------------------------------ \