//reduce the number of TermC.parse*; "//"means: tests broken .
broken tests are outcommented with "reduce the number of TermC.parse*"
1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 18:39:02 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jul 20 14:37:56 2021 +0200
1.3 @@ -68,12 +68,9 @@
1.4 val mk_var_op_num: term -> string -> typ -> typ -> int -> term
1.5
1.6 val matches: theory -> term -> term -> bool
1.7 - val parse: theory -> string -> cterm option
1.8 - val parseN: theory -> string -> cterm option
1.9 val parseNEW: Proof.context -> string -> term option
1.10 val parseNEW': Proof.context -> string -> term
1.11 val parseNEW'': theory -> string -> term
1.12 - val parseold: theory -> string -> cterm option
1.13 val parse_strict: theory -> string -> term
1.14 val parse_patt: theory -> string -> term
1.15 val perm: term -> term -> bool
1.16 @@ -533,21 +530,21 @@
1.17 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
1.18 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
1.19
1.20 -(* TODO clarify parse with Test_Isac *)
1.21 +(* TODO clarify parse with Test_Isac * )
1.22 fun parseold thy str = (* before 2002 *)
1.23 \<^try>\<open>
1.24 let val t = Syntax.read_term_global thy str
1.25 in Thm.global_cterm_of thy t end\<close>;
1.26 fun parseN thy str = (* introduced 2002 *)
1.27 \<^try>\<open>
1.28 - let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
1.29 + let val t = Syntax.read_term_global thy str
1.30 in Thm.global_cterm_of thy t end\<close>;
1.31
1.32 -fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
1.33 fun parse thy str = (* introduced 2010 *)
1.34 \<^try>\<open>
1.35 let val t = parse_strict thy str
1.36 in Thm.global_cterm_of thy t end\<close>;
1.37 +*)
1.38
1.39 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
1.40 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
1.41 @@ -559,6 +556,7 @@
1.42 case parseNEW (ThyC.to_ctxt thy) str of
1.43 SOME t => t
1.44 | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
1.45 +fun parse_strict thy str = (*typ_a2real*) (parseNEW'' thy str);
1.46
1.47 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
1.48 WN130613 probably compare to
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Jul 19 18:39:02 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Jul 20 14:37:56 2021 +0200
2.3 @@ -257,7 +257,7 @@
2.4 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
2.5 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);
2.6
2.7 -val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
2.8 +val e_pblterm = TermC.parseNEW'' @{theory Prog_Tac}
2.9 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");
2.10
2.11 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
3.1 --- a/src/Tools/isac/Interpret/Interpret.thy Mon Jul 19 18:39:02 2021 +0200
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Jul 20 14:37:56 2021 +0200
3.3 @@ -32,5 +32,6 @@
3.4 end
3.5 \<close> ML \<open>
3.6 \<close> ML \<open>
3.7 +\<close> ML \<open>
3.8 \<close>
3.9 end
4.1 --- a/src/Tools/isac/Interpret/step-solve.sml Mon Jul 19 18:39:02 2021 +0200
4.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Tue Jul 20 14:37:56 2021 +0200
4.3 @@ -88,11 +88,10 @@
4.4 *)
4.5 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Calc.state_post) istr =*)
4.6 fun by_term (pt, pos as (p, _)) istr =
4.7 - case TermC.parse (ThyC.get_theory "Isac_Knowledge") istr of
4.8 + case TermC.parseNEW ("Isac_Knowledge" |> ThyC.id_to_ctxt) istr of
4.9 NONE => ("syntax error in '" ^ istr ^ "'", Calc.state_empty_post)
4.10 | SOME f_in =>
4.11 let
4.12 - val f_in = Thm.term_of f_in
4.13 val pos_pred = lev_back(*'*) pos
4.14 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
4.15 val f_succ = Ctree.get_curr_formula (pt, pos);
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Jul 19 18:39:02 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Jul 20 14:37:56 2021 +0200
5.3 @@ -272,10 +272,10 @@
5.4 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
5.5 *)
5.6 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
5.7 - [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionTerm", [t]),
5.8 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
5.9 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivative",
5.10 - [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'"])
5.11 + [(TermC.parseNEW'' \<^theory> "functionTerm", [t]),
5.12 + (TermC.parseNEW'' \<^theory> "differentiateFor", [bdv]),
5.13 + (TermC.parseNEW'' \<^theory> "derivative",
5.14 + [TermC.parseNEW'' \<^theory> "f_f'"])
5.15 ]
5.16 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
5.17 \<close>
5.18 @@ -418,10 +418,10 @@
5.19 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
5.20 *)
5.21 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
5.22 - [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionEq", [t]),
5.23 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
5.24 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivativeEq",
5.25 - [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'::bool"])
5.26 + [(TermC.parseNEW'' \<^theory> "functionEq", [t]),
5.27 + (TermC.parseNEW'' \<^theory> "differentiateFor", [bdv]),
5.28 + (TermC.parseNEW'' \<^theory> "derivativeEq",
5.29 + [TermC.parseNEW'' \<^theory> "f_f'::bool"])
5.30 ]
5.31 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
5.32 \<close>
6.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Mon Jul 19 18:39:02 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Tue Jul 20 14:37:56 2021 +0200
6.3 @@ -48,9 +48,9 @@
6.4 "Simplify (2*a + 3*a)");
6.5 *)
6.6 fun argl2dtss t =
6.7 - [((Thm.term_of o the o (TermC.parse @{theory})) "Term", t),
6.8 - ((Thm.term_of o the o (TermC.parse @{theory})) "normalform",
6.9 - [(Thm.term_of o the o (TermC.parse @{theory})) "N"])
6.10 + [(TermC.parseNEW'' @{theory} "Term", t),
6.11 + (TermC.parseNEW'' @{theory} "normalform",
6.12 + [TermC.parseNEW'' @{theory} "N"])
6.13 ]
6.14 (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
6.15 \<close>
7.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Jul 19 18:39:02 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Jul 20 14:37:56 2021 +0200
7.3 @@ -534,8 +534,7 @@
7.4 \<^rule_thm>\<open>risolate_root_add\<close>,
7.5 \<^rule_thm>\<open>risolate_root_mult\<close>,
7.6 \<^rule_thm>\<open>risolate_root_div\<close> ],
7.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>))
7.8 - "empty_script")
7.9 + scr = Rule.Prog (TermC.parseNEW'' \<^theory> "empty_script")
7.10 };
7.11
7.12 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
7.13 @@ -550,8 +549,7 @@
7.14 \<^rule_thm>\<open>constant_square\<close>,
7.15 \<^rule_thm>\<open>constant_mult_square\<close>
7.16 ],
7.17 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>))
7.18 - "empty_script")
7.19 + scr = Rule.Prog (TermC.parseNEW'' \<^theory> "empty_script")
7.20 };
7.21 \<close>
7.22 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
8.1 --- a/src/Tools/isac/MathEngBasic/method.sml Mon Jul 19 18:39:02 2021 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Jul 20 14:37:56 2021 +0200
8.3 @@ -54,7 +54,7 @@
8.4 val gi = (case gi of
8.5 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
8.6 | ((_, gi') :: []) =>
8.7 - (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
8.8 + (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) gi'\<close> of
8.9 SOME x => x
8.10 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
8.11 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
8.12 @@ -64,7 +64,7 @@
8.13 val fi = (case fi of
8.14 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
8.15 | ((_, fi') :: []) =>
8.16 - (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
8.17 + (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) fi'\<close> of
8.18 SOME x => x
8.19 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
8.20 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
8.21 @@ -74,7 +74,7 @@
8.22 val re = (case re of
8.23 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
8.24 | ((_,re') :: []) =>
8.25 - (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
8.26 + (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) re'\<close> of
8.27 SOME x => x
8.28 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
8.29 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
9.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Mon Jul 19 18:39:02 2021 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Tue Jul 20 14:37:56 2021 +0200
9.3 @@ -80,7 +80,7 @@
9.4 val gi = (case gi of
9.5 [] => []
9.6 | ((_, gi') :: []) =>
9.7 - (case \<^try>\<open> map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
9.8 + (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) gi'\<close> of
9.9 SOME x => x
9.10 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Given' of " ^ strs2str pblID))
9.11 | _ => raise ERROR ("prep_input: more than one '#Given' in " ^ strs2str pblID));
9.12 @@ -90,7 +90,7 @@
9.13 val fi = (case fi of
9.14 [] => []
9.15 | ((_, fi') :: []) =>
9.16 - (case \<^try>\<open> map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
9.17 + (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) fi'\<close> of
9.18 SOME x => x
9.19 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))
9.20 | _ => raise ERROR ("prep_input: more than one '#Find' in " ^ strs2str pblID));
9.21 @@ -100,7 +100,7 @@
9.22 val re = (case re of
9.23 [] => []
9.24 | ((_, re') :: []) =>
9.25 - (case \<^try>\<open> map (split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
9.26 + (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) re'\<close> of
9.27 SOME x => x
9.28 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))
9.29 | _ => raise ERROR ("prep_input: more than one '#Relate' in " ^ strs2str pblID));
9.30 @@ -116,7 +116,7 @@
9.31 | _ => raise ERROR ("prep_input: more than one '#Where' in " ^ strs2str pblID));
9.32 in
9.33 ({guh = guh, mathauthors = maa, init = init, thy = thy,
9.34 - cas = Option.map (Thm.term_of o the o TermC.parse thy) ca,
9.35 + cas = Option.map (TermC.parseNEW'' thy) ca,
9.36 prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
9.37 end;
9.38
10.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Jul 19 18:39:02 2021 +0200
10.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Tue Jul 20 14:37:56 2021 +0200
10.3 @@ -55,10 +55,10 @@
10.4
10.5 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
10.6 needs to be here after def. Subproblem in Prog_Tac.thy *)
10.7 -val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
10.8 +val subpbl_t $ (pair_t $ _ $ _) = TermC.parseNEW'' @{theory Prog_Tac}
10.9 "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"
10.10 -val pbl_t $ _ =
10.11 - (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
10.12 +val pbl_t $ _ = TermC.parseNEW''
10.13 + @{theory Prog_Tac} "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
10.14
10.15 fun subpbl domID pblID =
10.16 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
10.17 @@ -110,24 +110,24 @@
10.18 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
10.19 val (FunID_Term $ _) = Program.prep_program @{thm auto_generated.simps}
10.20 val (FunID_Term_Bdv $ _) = Program.prep_program @{thm auto_generated_inst.simps}
10.21 -val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.22 +val Repeat $ _ = TermC.parseNEW'' @{theory}
10.23 "Repeat (Rewrite ''real_diff_minus'' t)";
10.24 -val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.25 +val Try $ _ = TermC.parseNEW'' @{theory}
10.26 "Try (Rewrite ''real_diff_minus'' t)";
10.27 -val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.28 +val Cal $ _ = TermC.parseNEW'' @{theory}
10.29 "Calculate ''PLUS''";
10.30 -val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.31 +val Ca1 $ _ = TermC.parseNEW'' @{theory}
10.32 "Calculate1 ''PLUS''";
10.33 -val Rew $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.34 +val Rew $ _ $ _ = TermC.parseNEW'' @{theory}
10.35 "Rewrite ''real_diff_minus'' t";
10.36 (*this is specific to FunHead_inst ...*)
10.37 -val Rew_Inst $ Subs $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.38 +val Rew_Inst $ Subs $ _ = TermC.parseNEW'' @{theory}
10.39 "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus''";
10.40 -val Rew_Set $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.41 +val Rew_Set $ _ = TermC.parseNEW'' @{theory}
10.42 "Rewrite_Set ''real_diff_minus''";
10.43 -val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.44 +val Rew_Set_Inst $ _ $ _ = TermC.parseNEW'' @{theory}
10.45 "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
10.46 -val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
10.47 +val SEq $ _ $ _ $ _ = TermC.parseNEW'' @{theory}
10.48 " ((Try (Repeat (Rewrite ''real_diff_minus''))) #> \
10.49 \ (Try (Repeat (Rewrite ''add.commute''))) #> \
10.50 \ (Try (Repeat (Rewrite ''mult_commute'')))) t";
11.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Jul 19 18:39:02 2021 +0200
11.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Jul 20 14:37:56 2021 +0200
11.3 @@ -25,8 +25,8 @@
11.4
11.5 ML \<open>
11.6 \<close> ML \<open>
11.7 -val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
11.8 -val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
11.9 +val UniversalList = TermC.parseNEW'' @{theory} "UniversalList";
11.10 +val EmptyList = TermC.parseNEW'' @{theory} "[]::bool list";
11.11 \<close> ML \<open>
11.12 \<close>
11.13
12.1 --- a/src/Tools/isac/Specify/i-model.sml Mon Jul 19 18:39:02 2021 +0200
12.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue Jul 20 14:37:56 2021 +0200
12.3 @@ -188,7 +188,7 @@
12.4 | ts_in (Mis _) = []
12.5 | ts_in _ = raise ERROR "ts_in: uncovered case in fun.def.";
12.6
12.7 -val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
12.8 +val unique = TermC.parseNEW'' @{theory "Real"} "UnIqE_tErM";
12.9 fun d_in (Cor ((d ,_), _)) = d
12.10 | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
12.11 | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
12.12 @@ -209,7 +209,7 @@
12.13
12.14 fun vars_of itms = itms |> mk_env |> map snd
12.15
12.16 -val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
12.17 +val dsc_unknown = TermC.parseNEW'' @{theory} "unknown::'a => unknow";
12.18
12.19 (* get a term from ori, notyet input in itm.
12.20 the term from ori is thrown back to a string in order to reuse
13.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Jul 19 18:39:02 2021 +0200
13.2 +++ b/src/Tools/isac/Specify/p-spec.sml Tue Jul 20 14:37:56 2021 +0200
13.3 @@ -80,13 +80,13 @@
13.4 | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
13.5 | parsitm dI (i, v, b, f, I_Model.Syn str) =
13.6 (case \<^try>\<open>
13.7 - let val _ = (Thm.term_of o the o (TermC.parse dI)) str
13.8 + let val _ = TermC.parseNEW'' dI str
13.9 in (i, v, b ,f, I_Model.Par str) end\<close> of
13.10 SOME x => x
13.11 | NONE => (i, v, b, f, I_Model.Syn str))
13.12 | parsitm dI (i, v, b, f, I_Model.Typ str) =
13.13 (case \<^try>\<open>
13.14 - let val _ = (Thm.term_of o the o (TermC.parse dI)) str
13.15 + let val _ = TermC.parseNEW'' dI str
13.16 in (i, v, b, f, I_Model.Par str) end\<close> of
13.17 SOME x => x
13.18 | NONE => (i, v, b, f, I_Model.Syn str))
13.19 @@ -157,13 +157,13 @@
13.20 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
13.21 fun fstr2itm_ thy pbt (f, str) =
13.22 let
13.23 - val topt = TermC.parse thy str
13.24 + val topt = TermC.parseNEW (ThyC.to_ctxt thy) str
13.25 in
13.26 case topt of
13.27 NONE => ([], false, f, I_Model.Syn str)
13.28 | SOME ct =>
13.29 let
13.30 - val (d, ts) = (Input_Descript.split o Thm.term_of) ct
13.31 + val (d, ts) = (Input_Descript.split) ct
13.32 val popt = find_first (eq7 (f, d)) pbt
13.33 in
13.34 case popt of
14.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Jul 19 18:39:02 2021 +0200
14.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Tue Jul 20 14:37:56 2021 +0200
14.3 @@ -88,8 +88,8 @@
14.4 Presently, ISAC uses a slightly different representation for terms (which soon
14.5 will disappear), which does not encode numerals as binary numbers:
14.6 \<close>
14.7 -ML \<open>val SOME t = TermC.parse @{theory "Isac_Knowledge"} "a + b * 3";
14.8 - TermC.atomwy (Thm.term_of t);
14.9 +ML \<open>val t = TermC.parseNEW'' @{theory "Isac_Knowledge"} "a + b * 3";
14.10 + TermC.atomwy t;
14.11 \<close>
14.12 text \<open>From the above we see: the internal representation of a term contains
14.13 all the knowledge it is built from, see
14.14 @@ -114,7 +114,9 @@
14.15 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is
14.16 defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
14.17 \<close>
14.18 -ML \<open>TermC.parse @{theory "HOL"} "a + b * 3";
14.19 +ML \<open>
14.20 +\<close> ML \<open>
14.21 +TermC.parseNEW'' @{theory "Real"} "a + b * 3::real";
14.22 \<close>
14.23 text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see
14.24 \begin{itemize}
15.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Jul 19 18:39:02 2021 +0200
15.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Tue Jul 20 14:37:56 2021 +0200
15.3 @@ -40,7 +40,7 @@
15.4 \<close>
15.5 text \<open>... and let us differentiate the term t:\<close>
15.6 ML \<open>
15.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x\<up>2 + x + y)";
15.8 +val t = TermC.parseNEW'' thy "d_d x (x\<up>2 + x + y)";
15.9
15.10 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
15.11 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
15.12 @@ -79,10 +79,10 @@
15.13 text \<open>We have already seen conditional rewriting above when we used the rule
15.14 diff_const; let us try:\<close>
15.15 ML \<open>
15.16 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*x*z)";
15.17 +val t1 = TermC.parseNEW'' thy "d_d x (a*BC*x*z)";
15.18 Rewrite.rewrite_inst_ thy ro er true inst diff_const t1;
15.19
15.20 -val t2 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*y*z)";
15.21 +val t2 = TermC.parseNEW'' thy "d_d x (a*BC*y*z)";
15.22 Rewrite.rewrite_inst_ thy ro er true inst diff_const t2;
15.23 \<close>
15.24 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
15.25 @@ -97,7 +97,7 @@
15.26 \<close>
15.27 ML \<open>
15.28 (*show_brackets := true; TODO*)
15.29 -val t0 = (Thm.term_of o the o (TermC.parse thy)) "2*a + 3*b + 4*a"; UnparseC.term t0;
15.30 +val t0 = TermC.parseNEW'' thy "2*a + 3*b + 4*a"; UnparseC.term t0;
15.31 (*show_brackets := false;*)
15.32 \<close>
15.33 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
15.34 @@ -146,11 +146,11 @@
15.35 \<close>
15.36 ML \<open>
15.37 (*show_brackets := false; TODO*)
15.38 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(a - b) * (a\<up>2 + a*b + b\<up>2)";
15.39 +val t1 = TermC.parseNEW'' thy "(a - b) * (a\<up>2 + a*b + b\<up>2)";
15.40 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; UnparseC.term t;
15.41 \<close>
15.42 ML \<open>
15.43 -val t2 = (Thm.term_of o the o (TermC.parse thy))
15.44 +val t2 = TermC.parseNEW'' thy
15.45 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
15.46 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
15.47 \<close>
15.48 @@ -186,7 +186,7 @@
15.49
15.50 subsection \<open>What already works\<close>
15.51 ML \<open>
15.52 -val t2 = (Thm.term_of o the o (TermC.parse thy))
15.53 +val t2 = TermC.parseNEW'' thy
15.54 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
15.55 val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; UnparseC.term t;
15.56 \<close>
15.57 @@ -226,7 +226,7 @@
15.58
15.59 subsection \<open>This does not yet work\<close>
15.60 ML \<open>
15.61 -val t = (Thm.term_of o the o (TermC.parse thy))
15.62 +val t = TermC.parseNEW'' thy
15.63 "(2*a - 5*b) * (2*a + 5*b)";
15.64 Rewrite.rewrite_set_ thy true rls_p_33 t; UnparseC.term t;
15.65 \<close>
16.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 18:39:02 2021 +0200
16.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue Jul 20 14:37:56 2021 +0200
16.3 @@ -355,15 +355,8 @@
16.4 *** Free ( R, RealDef.real) *)
16.5 val thy = @{theory "Complex_Main"};
16.6 val str = "x + z";
16.7 - TermC.parse thy str;
16.8 + TermC.parseNEW'' thy str;
16.9 "---------------";
16.10 - val str = "x + 2*z";
16.11 - val t = Syntax.read_term_global thy str;
16.12 - val t = TermC.typ_a2real (Syntax.read_term_global thy str);
16.13 - Thm.global_cterm_of thy t;
16.14 - case TermC.parse thy str of
16.15 - SOME t' => t'
16.16 - | NONE => error "termC.sml parsing 'x + 2*z' failed";
16.17
16.18 "===== fun TermC.parse_patt caused error in fun T_a2real ===";
16.19 val thy = @{theory "Poly"};
16.20 @@ -641,7 +634,7 @@
16.21 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
16.22 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
16.23 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
16.24 -val T = (type_of o Thm.term_of o the) (TermC.parse thy "12::real");
16.25 +val T = type_of (TermC.parseNEW'' thy "12::real");
16.26 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;
16.27 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
16.28
16.29 @@ -653,21 +646,21 @@
16.30 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
16.31 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
16.32 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
16.33 -val t = (Thm.term_of o the o (TermC.parse thy)) "3 ^ 4";
16.34 +val t = TermC.parseNEW'' thy "3 \<up> 4";
16.35 val hT = type_of (head_of t);
16.36 -if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = TermC.dest_binop_typ hT
16.37 +if (HOLogic.realT, HOLogic.realT, HOLogic.realT) = TermC.dest_binop_typ hT
16.38 then () else error "TermC.dest_binop_typ";
16.39
16.40 "----------- fun TermC.is_list -----------------------------------------------------------------------";
16.41 "----------- fun TermC.is_list -----------------------------------------------------------------------";
16.42 "----------- fun TermC.is_list -----------------------------------------------------------------------";
16.43 -val (SOME ct) = TermC.parse thy "lll::real list";
16.44 +val ct = TermC.parseNEW'' thy "lll::real list";
16.45 val t = TermC.str2term "lll::real list";
16.46 -val ty = (Term.type_of o Thm.term_of) ct;
16.47 +val ty = Term.type_of ct;
16.48 if TermC.is_list t = false then () else error "TermC.is_list lll::real list";
16.49
16.50 val t = TermC.str2term "[a, b, c]";
16.51 -val ty = (Term.type_of o Thm.term_of) ct;
16.52 +val ty = Term.type_of ct;
16.53 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]";
16.54
16.55 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
17.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Jul 19 18:39:02 2021 +0200
17.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Jul 20 14:37:56 2021 +0200
17.3 @@ -44,6 +44,7 @@
17.4 "-----------------------------------------------------------------";
17.5
17.6
17.7 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.8 "--------- appendFormula: on Res + equ_nrls ----------------------";
17.9 "--------- appendFormula: on Res + equ_nrls ----------------------";
17.10 "--------- appendFormula: on Res + equ_nrls ----------------------";
17.11 @@ -168,6 +169,7 @@
17.12 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
17.13 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
17.14 DEconstrCalcTree 1;
17.15 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.16
17.17 "--------- appendFormula: on Res + NO deriv ----------------------";
17.18 "--------- appendFormula: on Res + NO deriv ----------------------";
17.19 @@ -199,6 +201,7 @@
17.20 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
17.21 DEconstrCalcTree 1;
17.22
17.23 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.24 "--------- appendFormula: on Res + late deriv --------------------";
17.25 "--------- appendFormula: on Res + late deriv --------------------";
17.26 "--------- appendFormula: on Res + late deriv --------------------";
17.27 @@ -255,7 +258,9 @@
17.28 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
17.29 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
17.30 DEconstrCalcTree 1;
17.31 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.32
17.33 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.34 "--------- replaceFormula: on Res + = ----------------------------";
17.35 "--------- replaceFormula: on Res + = ----------------------------";
17.36 "--------- replaceFormula: on Res + = ----------------------------";
17.37 @@ -301,7 +306,9 @@
17.38 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
17.39 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
17.40 DEconstrCalcTree 1;
17.41 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.42
17.43 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.44 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.45 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.46 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.47 @@ -325,6 +332,7 @@
17.48 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
17.49 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
17.50 DEconstrCalcTree 1;
17.51 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.52
17.53 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
17.54 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
17.55 @@ -340,14 +348,18 @@
17.56 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
17.57 val ((pt,_),_) = get_calc 1;
17.58 val str = pr_ctree pr_short pt;
17.59 - writeln str;
17.60 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.61 + str = ". ----- pblobj -----\n1. x + 1 = 2\n";
17.62 +
17.63 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
17.64 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
17.65 autoCalculate 1 CompleteCalc;
17.66 val ((pt,pos as (p,_)),_) = get_calc 1;
17.67 +(**)pos = ([1], Met)
17.68 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
17.69 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
17.70 DEconstrCalcTree 1;
17.71 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.72
17.73 "--------- replaceFormula: cut calculation -----------------------";
17.74 "--------- replaceFormula: cut calculation -----------------------";
17.75 @@ -366,8 +378,11 @@
17.76 val ((pt,p),_) = get_calc 1;
17.77 val str = pr_ctree pr_short pt;
17.78 writeln str;
17.79 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.80 + p = ([], Res)
17.81 if p = ([1], Res) then ()
17.82 else error "inform.sml: diff.behav. cut calculation 2";
17.83 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.84
17.85
17.86 (* 040307 copied from informtest.sml; ... old version
17.87 @@ -471,8 +486,12 @@
17.88 "--------- CAS-command on ([],Pbl) -------------------------------";
17.89 val (p,_,f,nxt,_,pt) =
17.90 CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
17.91 -val ifo = "solve(x+1=2,x)";
17.92 -val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
17.93 +val ifo = "solve (x + 1 = (2::real), x::real)";
17.94 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.95 +ERROR lev_back': called by ([],_)
17.96 +
17.97 +val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve (x + 1 = (2::real), x::real)";
17.98 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.99 (*
17.100 This trick \<up> \<up> \<up> micked input of \<up> \<up> \<up> \<up> \<up> ^^ in the front-end.
17.101 The trick worked in changeset fbaff8cf0179, it does not work in 59c5dd27d589 anymore
17.102 @@ -495,13 +514,17 @@
17.103 CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
17.104 Iterator 1;
17.105 moveActiveRoot 1;
17.106 -replaceFormula 1 "solve(x+1=2,x)";
17.107 +replaceFormula 1 "solve(x + 1 = (2::real), x)";
17.108 autoCalculate 1 CompleteCalc;
17.109 val ((pt,p),_) = get_calc 1;
17.110 Test_Tool.show_pt pt;
17.111 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\
17.112 + p = ([], Pbl)
17.113 +
17.114 if p = ([], Res) then ()
17.115 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
17.116 DEconstrCalcTree 1;
17.117 +----- broken with "reduce the number of TermC.parse*"---------------------------------------//*)
17.118
17.119 "--------- inform [rational,simplification] ----------------------";
17.120 "--------- inform [rational,simplification] ----------------------";
17.121 @@ -551,6 +574,10 @@
17.122 (([2], Res), (a * d + c * b) / (b * d) + e / f)]
17.123 *)
17.124 val ((pt,p),_) = get_calc 1;
17.125 +
17.126 +(*TOODOO broken with "reduce the number of TermC.parse*"------------------------------------\\* )
17.127 + p = ([9], Res)
17.128 +
17.129 if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
17.130 else error ("inform.sml: [rational,simplification] 1");
17.131
17.132 @@ -633,6 +660,7 @@
17.133 (([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
17.134 *)
17.135 DEconstrCalcTree 1;
17.136 +----- broken with "reduce the number of TermC.parse*"------------------------------------//*)
17.137
17.138 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
17.139 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
17.140 @@ -1026,8 +1054,7 @@
17.141 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
17.142 = (cs', (encode ifo));
17.143 val ctxt = get_ctxt pt pos (*see TODO.thy*)
17.144 - val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
17.145 - val f_in = Thm.term_of f_in
17.146 + val SOME f_in = (*case*) TermC.parseNEW (ThyC.id_to_ctxt "Isac_Knowledge") istr (*of*);
17.147 val pos_pred = lev_back' pos
17.148 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
17.149 (*if*) f_pred = f_in; (*else*)
18.1 --- a/test/Tools/isac/Interpret/li-tool.sml Mon Jul 19 18:39:02 2021 +0200
18.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue Jul 20 14:37:56 2021 +0200
18.3 @@ -168,14 +168,14 @@
18.4 "----------- fun go ----------------------------------------------";
18.5 "----------- fun go ----------------------------------------------";
18.6 (*
18.7 -> val t = (Thm.term_of o the o (TermC.parse thy)) "a+b";
18.8 +> val t = TermC.parseNEW'' thy "a+b";
18.9 val it = Const (#,#) $ Free (#,#) $ Free ("b", "RealDef.real") : term
18.10 > val plus_a = TermC.sub_at [L] t;
18.11 > val b = TermC.sub_at [R] t;
18.12 > val plus = TermC.sub_at [L,L] t;
18.13 > val a = TermC.sub_at [L,R] t;
18.14
18.15 -> val t = (Thm.term_of o the o (TermC.parse thy)) "a+b+c";
18.16 +> val t = TermC.parseNEW'' thy "a+b+c";
18.17 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c", "RealDef.real") : term
18.18 > val pl_pl_a_b = TermC.sub_at [L] t;
18.19 > val c = TermC.sub_at [R] t;
18.20 @@ -194,13 +194,13 @@
18.21 "----------- fun dsc_valT ----------------------------------------";
18.22 "----------- fun dsc_valT ----------------------------------------";
18.23 "----------- fun dsc_valT ----------------------------------------";
18.24 -(*> val t = (Thm.term_of o the o (TermC.parse thy)) "equality";
18.25 +(*> val t = TermC.parseNEW'' thy "equality";
18.26 > val T = type_of t;
18.27 val T = "bool => Tools.una" : typ
18.28 > val dsc = dsc_valT t;
18.29 val dsc = "una" : string
18.30
18.31 -> val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues";
18.32 +> val t = TermC.parseNEW'' thy "fixedValues";
18.33 > val T = type_of t;
18.34 val T = "bool List.list => Tools.nam" : typ
18.35 > val dsc = dsc_valT t;
19.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jul 19 18:39:02 2021 +0200
19.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Jul 20 14:37:56 2021 +0200
19.3 @@ -570,6 +570,7 @@
19.4 val ("ok", cs' as (_, _, ptp')) =
19.5 (*case*) Step.do_next pos cs (*of*);
19.6
19.7 +(*TOODOO broken with "reduce the number of TermC.parse---------------------------------------\\*"
19.8 val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
19.9 Step_Solve.by_term ptp' (encode ifo) (*of*);
19.10 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
19.11 @@ -677,3 +678,5 @@
19.12 ([3], Res), [x = 1]
19.13 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
19.14 ([], Res), [x = 1]]*)
19.15 + TOODOObroken with "reduce the number of TermC.parse*"--------------------------------------//*)
19.16 +
20.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Jul 19 18:39:02 2021 +0200
20.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Jul 20 14:37:56 2021 +0200
20.3 @@ -29,7 +29,7 @@
20.4 \ (let t_t = (l_l = 1)\
20.5 \ in t_t)"
20.6 ;
20.7 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
20.8 +val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
20.9 TermC.atomty sc;
20.10 atomt sc;
20.11
21.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Mon Jul 19 18:39:02 2021 +0200
21.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Tue Jul 20 14:37:56 2021 +0200
21.3 @@ -28,7 +28,7 @@
21.4
21.5 val thy = @{theory "Biegelinie"};
21.6 val ctxt = ThyC.id_to_ctxt "Biegelinie";
21.7 -fun str2term str = (Thm.term_of o the o (TermC.parse thy)) str;
21.8 +fun str2term str = TermC.parseNEW'' thy str;
21.9 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
21.10 fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));
21.11
22.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon Jul 19 18:39:02 2021 +0200
22.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Jul 20 14:37:56 2021 +0200
22.3 @@ -47,7 +47,7 @@
22.4 "----------- for correction of diff_const ---------------";
22.5 "----------- for correction of diff_const ---------------";
22.6 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
22.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)";
22.8 +val t = TermC.parseNEW'' thy "Not (x =!= a)";
22.9 case rewrite_set_ thy false erls_diff t of
22.10 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
22.11 | _ => error "rewrite_set_ Not (x =!= a) changed";
22.12 @@ -58,7 +58,7 @@
22.13 | _ => error "rewrite_set_ 2 is_const changed";
22.14
22.15 val thm = @{thm diff_const};
22.16 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x";
22.17 +val ct = TermC.parseNEW'' thy "d_d x x";
22.18 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
22.19 val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
22.20
22.21 @@ -66,10 +66,10 @@
22.22 "----------- for correction of diff_quot ----------------";
22.23 "----------- for correction of diff_quot ----------------";
22.24 val thy = @{theory "Diff"};
22.25 -val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)";
22.26 +val ct = TermC.parseNEW'' thy "Not (x = 0)";
22.27 rewrite_set_ thy false erls_diff ct;
22.28
22.29 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))";
22.30 +val ct = TermC.parseNEW'' thy "d_d x ((x+1) / (x - 1))";
22.31 val thm = @{thm diff_quot};
22.32 val SOME (ctt,_) =
22.33 (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
22.34 @@ -78,7 +78,7 @@
22.35 "----------- differentiate by rewrite -------------------";
22.36 "----------- differentiate by rewrite -------------------";
22.37 val thy = @{theory "Diff"};
22.38 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \<up> 2 + 3 * x + 4)";
22.39 +val ct = TermC.parseNEW'' thy "d_d x (x \<up> 2 + 3 * x + 4)";
22.40 "--- 1 ---";
22.41 val thm = @{thm "diff_sum"};
22.42 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
22.43 @@ -101,7 +101,7 @@
22.44 "--- 7 ---";
22.45 "--- 7 ---";
22.46 val rls = Test_simplify;
22.47 -val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \<up> (2 - 1) + 3 * 1 + 0";
22.48 +val ct = TermC.parseNEW'' thy "2 * x \<up> (2 - 1) + 3 * 1 + 0";
22.49 val (ct, _) = the (rewrite_set_ thy true rls ct);
22.50 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
22.51
22.52 @@ -257,7 +257,7 @@
22.53 \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
22.54 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
22.55 ;
22.56 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
22.57 +val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
22.58
22.59
22.60 "----------- diff_conv, sym_diff_conv -------------------";
23.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Jul 19 18:39:02 2021 +0200
23.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Jul 20 14:37:56 2021 +0200
23.3 @@ -261,40 +261,40 @@
23.4 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
23.5 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
23.6
23.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";
23.8 +val t = TermC.parseNEW'' thy "Integral x D x";
23.9 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.10 if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
23.11
23.12 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
23.13 +val t = TermC.parseNEW'' thy "Integral c * x \<up> 2 + c_2 D x";
23.14 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.15 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
23.16
23.17 val rls = add_new_c;
23.18 -val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";
23.19 +val t = TermC.parseNEW'' thy "c * (x \<up> 3 / 3) + c_2 * x";
23.20 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.21 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
23.22 else error "integrate.sml: diff.behav. in add_new_c simpl.";
23.23
23.24 -val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";
23.25 +val t = TermC.parseNEW'' thy "F x = x \<up> 3 / 3 + x";
23.26 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.27 if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
23.28 else error "integrate.sml: diff.behav. in add_new_c equation";
23.29
23.30 val rls = simplify_Integral;
23.31 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
23.32 -val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
23.33 +val t = TermC.parseNEW'' thy "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
23.34 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.35 if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
23.36 then () else error "integrate.sml: diff.behav. in simplify_I #1";
23.37
23.38 val rls = integration;
23.39 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
23.40 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
23.41 +val t = TermC.parseNEW'' thy "Integral c * x \<up> 2 + c_2 D x";
23.42 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.43 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
23.44 then () else error "integrate.sml: diff.behav. in integration #1";
23.45
23.46 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";
23.47 +val t = TermC.parseNEW'' thy "Integral 3*x \<up> 2 + 2*x + 1 D x";
23.48 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.49 if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
23.50 else error "integrate.sml: diff.behav. in integration #2";
23.51 @@ -306,7 +306,7 @@
23.52 if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
23.53 then () else error "integrate.sml: diff.behav. in integration #3";
23.54
23.55 -val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
23.56 +val t = TermC.parseNEW'' thy ("Integral " ^ UnparseC.term res ^ " D x");
23.57 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
23.58 if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
23.59 then () else error "integrate.sml: diff.behav. in integration #4";
24.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Mon Jul 19 18:39:02 2021 +0200
24.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Tue Jul 20 14:37:56 2021 +0200
24.3 @@ -45,135 +45,135 @@
24.4 "-------- fun has_degree_in --------------------------------------------------------------------";
24.5 "-------- fun has_degree_in --------------------------------------------------------------------";
24.6 "-------- fun has_degree_in --------------------------------------------------------------------";
24.7 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.8 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
24.9 +val v = TermC.parseNEW'' thy "x";
24.10 +val t = TermC.parseNEW'' thy "1";
24.11 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
24.12
24.13 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.14 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
24.15 +val v = TermC.parseNEW'' thy "AA";
24.16 +val t = TermC.parseNEW'' thy "1";
24.17 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
24.18
24.19 (*----------*)
24.20 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.21 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
24.22 +val v = TermC.parseNEW'' thy "x";
24.23 +val t = TermC.parseNEW'' thy "a*b+c";
24.24 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
24.25
24.26 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.27 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
24.28 +val v = TermC.parseNEW'' thy "AA";
24.29 +val t = TermC.parseNEW'' thy "a*b+c";
24.30 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
24.31
24.32 (*----------*)
24.33 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.34 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
24.35 +val v = TermC.parseNEW'' thy "x";
24.36 +val t = TermC.parseNEW'' thy "a*x+c";
24.37 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
24.38
24.39 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.40 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
24.41 +val v = TermC.parseNEW'' thy "AA";
24.42 +val t = TermC.parseNEW'' thy "a*AA+c";
24.43 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
24.44
24.45 (*----------*)
24.46 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.47 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
24.48 +val v = TermC.parseNEW'' thy "x";
24.49 +val t = TermC.parseNEW'' thy "(a*b+c)*x \<up> 7";
24.50 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
24.51
24.52 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.53 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
24.54 +val v = TermC.parseNEW'' thy "AA";
24.55 +val t = TermC.parseNEW'' thy "(a*b+c)*AA \<up> 7";
24.56 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
24.57
24.58 (*----------*)
24.59 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.60 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
24.61 +val v = TermC.parseNEW'' thy "x";
24.62 +val t = TermC.parseNEW'' thy "x \<up> 7";
24.63 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
24.64
24.65 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.66 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
24.67 +val v = TermC.parseNEW'' thy "AA";
24.68 +val t = TermC.parseNEW'' thy "AA \<up> 7";
24.69 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
24.70
24.71 (*----------*)
24.72 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.73 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
24.74 +val v = TermC.parseNEW'' thy "x";
24.75 +val t = TermC.parseNEW'' thy "(a*b+c)*x";
24.76 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
24.77
24.78 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.79 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
24.80 +val v = TermC.parseNEW'' thy "AA";
24.81 +val t = TermC.parseNEW'' thy "(a*b+c)*AA";
24.82 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
24.83
24.84 (*----------*)
24.85 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.86 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
24.87 +val v = TermC.parseNEW'' thy "x";
24.88 +val t = TermC.parseNEW'' thy "(a*b+x)*x";
24.89 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
24.90
24.91 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.92 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
24.93 +val v = TermC.parseNEW'' thy "AA";
24.94 +val t = TermC.parseNEW'' thy "(a*b+AA)*AA";
24.95 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
24.96
24.97 (*----------*)
24.98 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.99 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
24.100 +val v = TermC.parseNEW'' thy "x";
24.101 +val t = TermC.parseNEW'' thy "x";
24.102 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
24.103
24.104 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.105 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.106 +val v = TermC.parseNEW'' thy "AA";
24.107 +val t = TermC.parseNEW'' thy "AA";
24.108 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
24.109
24.110 (*----------*)
24.111 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.112 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
24.113 +val v = TermC.parseNEW'' thy "x";
24.114 +val t = TermC.parseNEW'' thy "ab - (a*b)*x";
24.115 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
24.116
24.117 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.118 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
24.119 +val v = TermC.parseNEW'' thy "AA";
24.120 +val t = TermC.parseNEW'' thy "ab - (a*b)*AA";
24.121 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
24.122
24.123 "-------- fun mono_deg_in ----------------------------------------------------------------------";
24.124 "-------- fun mono_deg_in ----------------------------------------------------------------------";
24.125 "-------- fun mono_deg_in ----------------------------------------------------------------------";
24.126 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
24.127 +val v = TermC.parseNEW'' thy "x";
24.128
24.129 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
24.130 +val t = TermC.parseNEW'' thy "(a*b+c)*x \<up> 7";
24.131 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
24.132
24.133 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
24.134 +val t = TermC.parseNEW'' thy "x \<up> 7";
24.135 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
24.136
24.137 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
24.138 +val t = TermC.parseNEW'' thy "(a*b+c)*x";
24.139 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
24.140
24.141 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
24.142 +val t = TermC.parseNEW'' thy "(a*b+x)*x";
24.143 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
24.144
24.145 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
24.146 +val t = TermC.parseNEW'' thy "x";
24.147 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
24.148
24.149 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
24.150 +val t = TermC.parseNEW'' thy "(a*b+c)";
24.151 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
24.152
24.153 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
24.154 +val t = TermC.parseNEW'' thy "ab - (a*b)*x";
24.155 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
24.156
24.157 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
24.158 val thy = @{theory Partial_Fractions}
24.159 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.160 +val v = TermC.parseNEW'' thy "AA";
24.161
24.162 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
24.163 +val t = TermC.parseNEW'' thy "(a*b+c)*AA \<up> 7";
24.164 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
24.165
24.166 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
24.167 +val t = TermC.parseNEW'' thy "AA \<up> 7";
24.168 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
24.169
24.170 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
24.171 +val t = TermC.parseNEW'' thy "(a*b+c)*AA";
24.172 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
24.173
24.174 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
24.175 +val t = TermC.parseNEW'' thy "(a*b+AA)*AA";
24.176 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
24.177
24.178 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
24.179 +val t = TermC.parseNEW'' thy "AA";
24.180 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
24.181
24.182 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
24.183 +val t = TermC.parseNEW'' thy "(a*b+c)";
24.184 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
24.185
24.186 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
24.187 +val t = TermC.parseNEW'' thy "ab - (a*b)*AA";
24.188 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
24.189
24.190
24.191 @@ -787,7 +787,7 @@
24.192 else error "poly.sml: diff.behav. in make_polynomial 20";
24.193
24.194 "-----SPO ---";
24.195 -val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
24.196 +val t = TermC.parseNEW'' thy "a \<up> 2 * (-a) \<up> 2";
24.197 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
24.198 if (UnparseC.term t) = "a \<up> 4" then ()
24.199 else error "poly.sml: diff.behav. in make_polynomial 24";
25.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Mon Jul 19 18:39:02 2021 +0200
25.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Tue Jul 20 14:37:56 2021 +0200
25.3 @@ -125,36 +125,36 @@
25.4 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
25.5 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
25.6 val thy = @{theory Partial_Fractions}
25.7 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
25.8 +val expr = TermC.parseNEW'' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
25.9 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
25.10
25.11 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
25.12 +val expr = TermC.parseNEW'' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
25.13 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
25.14
25.15 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
25.16 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
25.17 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
25.18 -val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
25.19 +val t = TermC.parseNEW'' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
25.20 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
25.21 if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
25.22 andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
25.23 then () else error "eval_is_expanded_in x ..changed";
25.24
25.25 val thy = @{theory Partial_Fractions}
25.26 -val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
25.27 +val t = TermC.parseNEW'' thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
25.28 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
25.29 if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
25.30 andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
25.31 then () else error "eval_is_expanded_in AA ..changed";
25.32
25.33
25.34 -val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";
25.35 +val t = TermC.parseNEW'' thy "(8 + 2*x + x \<up> 2) is_poly_in x";
25.36 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
25.37 if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
25.38 andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
25.39 then () else error "is_poly_in x ..changed";
25.40
25.41 -val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
25.42 +val t = TermC.parseNEW'' thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
25.43 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
25.44 if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
25.45 andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
25.46 @@ -162,10 +162,10 @@
25.47
25.48
25.49 val thy = @{theory Partial_Fractions}
25.50 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
25.51 +val expr = TermC.parseNEW'' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
25.52 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
25.53
25.54 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
25.55 +val expr = TermC.parseNEW'' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
25.56 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
25.57
25.58 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
25.59 @@ -191,7 +191,7 @@
25.60 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
25.61
25.62
25.63 -val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
25.64 +val t = TermC.parseNEW'' thy "- 1";
25.65 TermC.atomty t;
25.66 (*
25.67 ***
25.68 @@ -205,7 +205,7 @@
25.69 "======= these external values all have the same internal representation";
25.70 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
25.71 (*----------------------------------- vvvvv -------------------------------------------*)
25.72 -val t = (Thm.term_of o the o (TermC.parse thy)) "-x";
25.73 +val t = TermC.parseNEW'' thy "-x";
25.74 TermC.atomty t;
25.75 (**** -------------
25.76 *** Free ( -x, real)*)
25.77 @@ -213,7 +213,7 @@
25.78 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
25.79 | _ => error "internal representation of \"-x\" changed";
25.80 (*----------------------------------- vvvvv -------------------------------------------*)
25.81 -val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
25.82 +val t = TermC.parseNEW'' thy "- x";
25.83 TermC.atomty t;
25.84 (**** -------------
25.85 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
25.86 @@ -221,7 +221,7 @@
25.87 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
25.88 | _ => error "internal representation of \"- x\" changed";
25.89 (*----------------------------------- vvvvvv ------------------------------------------*)
25.90 -val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
25.91 +val t = TermC.parseNEW'' thy "-(x)";
25.92 TermC.atomty t;
25.93 (**** -------------
25.94 *** Free ( -x, real)*)
26.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Jul 19 18:39:02 2021 +0200
26.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Jul 20 14:37:56 2021 +0200
26.3 @@ -51,33 +51,33 @@
26.4 "----------- tests on predicates in problems ---------------------";
26.5 Rewrite.trace_on:=true; (*true false*)
26.6
26.7 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
26.8 + val t1 = TermC.parseNEW'' thy "lhs (-8 - 2*x + x \<up> 2 = 0)";
26.9 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
26.10 if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
26.11 else error "polyeq.sml: diff.behav. in lhs";
26.12
26.13 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
26.14 + val t2 = TermC.parseNEW'' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
26.15 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
26.16 if (UnparseC.term t) = "True" then ()
26.17 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
26.18
26.19 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
26.20 + val t0 = TermC.parseNEW'' thy "(sqrt(x)) is_poly_in x";
26.21 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
26.22 if (UnparseC.term t) = "False" then ()
26.23 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
26.24
26.25 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
26.26 + val t3 = TermC.parseNEW'' thy "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
26.27 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
26.28 if (UnparseC.term t) = "True" then ()
26.29 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
26.30
26.31 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
26.32 + val t4 = TermC.parseNEW'' thy "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
26.33 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
26.34 if (UnparseC.term t) = "True" then ()
26.35 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
26.36
26.37
26.38 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
26.39 + val t6 = TermC.parseNEW'' thy "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
26.40 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
26.41 if (UnparseC.term t) = "True" then ()
26.42 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
26.43 @@ -87,18 +87,18 @@
26.44 if (UnparseC.term t) = "True" then ()
26.45 else error "polyeq.sml: diff.behav. in has_degree_in_in";
26.46
26.47 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
26.48 + val t3 = TermC.parseNEW'' thy "((sqrt(x)) has_degree_in x) = 2";
26.49 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
26.50 if (UnparseC.term t) = "False" then ()
26.51 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
26.52
26.53 - val t4 = (Thm.term_of o the o (TermC.parse thy))
26.54 + val t4 = TermC.parseNEW'' thy
26.55 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
26.56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
26.57 if (UnparseC.term t) = "False" then ()
26.58 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
26.59
26.60 - val t5 = (Thm.term_of o the o (TermC.parse thy))
26.61 + val t5 = TermC.parseNEW'' thy
26.62 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
26.63 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
26.64 if (UnparseC.term t) = "True" then ()
26.65 @@ -133,7 +133,7 @@
26.66 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
26.67
26.68 (*Aufgabe zum Einstieg in die Arbeit...*)
26.69 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
26.70 + val t = TermC.parseNEW'' thy "a*b - (a+b)*x + x \<up> 2 = 0";
26.71 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
26.72 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
26.73 UnparseC.term t;
26.74 @@ -163,9 +163,9 @@
26.75 *)
26.76
26.77 "------ 15.11.02 --------------------------";
26.78 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
26.79 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
26.80 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
26.81 + val t = TermC.parseNEW'' thy "1 + a * x + b * x";
26.82 + val bdv = TermC.parseNEW'' thy "bdv";
26.83 + val a = TermC.parseNEW'' thy "a";
26.84
26.85 Rewrite.trace_on := false; (*true false*)
26.86 (* Anwenden einer Regelmenge aus Termorder.ML: *)
26.87 @@ -177,7 +177,7 @@
26.88 UnparseC.term t;
26.89 "1 + b * x + x * a";
26.90
26.91 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
26.92 + val t = TermC.parseNEW'' thy "1 + a * (x + b * x) + a \<up> 2";
26.93 val SOME (t,_) =
26.94 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.95 UnparseC.term t;
26.96 @@ -186,7 +186,7 @@
26.97 UnparseC.term t;
26.98 "1 + (x + b * x) * a + a \<up> 2";
26.99
26.100 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
26.101 + val t = TermC.parseNEW'' thy "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
26.102 val SOME (t,_) =
26.103 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.104 UnparseC.term t;
26.105 @@ -206,7 +206,7 @@
26.106 get_thm Termorder.thy "bdv_n_collect";
26.107 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
26.108 *)
26.109 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
26.110 + val t = TermC.parseNEW'' thy "a \<up> 2 * x + 7 * a \<up> 2";
26.111 val SOME (t,_) =
26.112 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.113 UnparseC.term t;
26.114 @@ -224,14 +224,14 @@
26.115 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
26.116 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
26.117 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
26.118 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
26.119 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
26.120 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
26.121 + val substa = [(TermC.empty, TermC.parseNEW'' thy "a")];
26.122 + val substb = [(TermC.empty, TermC.parseNEW'' thy "b")];
26.123 + val substx = [(TermC.empty, TermC.parseNEW'' thy "x")];
26.124
26.125 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
26.126 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
26.127 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
26.128 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
26.129 + val x1 = TermC.parseNEW'' thy "a + b + x";
26.130 + val x2 = TermC.parseNEW'' thy "a + x + b";
26.131 + val x3 = TermC.parseNEW'' thy "a + x + b";
26.132 + val x4 = TermC.parseNEW'' thy "x + a + b";
26.133
26.134 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
26.135 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
26.136 @@ -242,22 +242,22 @@
26.137 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
26.138 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
26.139
26.140 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
26.141 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
26.142 + val aa = TermC.parseNEW'' thy "- 1 * a * x";
26.143 + val bb = TermC.parseNEW'' thy "x \<up> 3";
26.144 ord_make_polynomial_in true thy substx (aa, bb);
26.145 true; (* => LESS *)
26.146
26.147 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
26.148 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
26.149 + val aa = TermC.parseNEW'' thy "- 1 * a * x";
26.150 + val bb = TermC.parseNEW'' thy "x \<up> 3";
26.151 ord_make_polynomial_in true thy substa (aa, bb);
26.152 false; (* => GREATER *)
26.153
26.154 (* und nach dem Re-engineering der Termorders in den 'rulesets'
26.155 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
26.156 - val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
26.157 - val x = (Thm.term_of o the o (TermC.parse thy)) "x";
26.158 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
26.159 - val b = (Thm.term_of o the o (TermC.parse thy)) "b";
26.160 + val bdv= TermC.parseNEW'' thy "''bdv''";
26.161 + val x = TermC.parseNEW'' thy "x";
26.162 + val a = TermC.parseNEW'' thy "a";
26.163 + val b = TermC.parseNEW'' thy "b";
26.164 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
26.165 if UnparseC.term t' = "b + x + a" then ()
26.166 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
26.167 @@ -269,7 +269,7 @@
26.168 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
26.169
26.170 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
26.171 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
26.172 + val ppp = TermC.parseNEW'' thy ppp';
26.173 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
26.174 if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
26.175 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
26.176 @@ -279,7 +279,7 @@
26.177 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
26.178
26.179 val ttt' = "(3*x + 5)/18";
26.180 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
26.181 + val ttt = TermC.parseNEW'' thy ttt';
26.182 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
26.183 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
26.184 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
26.185 @@ -940,7 +940,7 @@
26.186 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
26.187 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
26.188 "---- test the erls ----";
26.189 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
26.190 + val t1 = TermC.parseNEW'' thy "0 <= (10/3/2) \<up> 2 - 1";
26.191 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
26.192 val t' = UnparseC.term t;
26.193 (*if t'= \<^const_name>\<open>True\<close> then ()
27.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 18:39:02 2021 +0200
27.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Jul 20 14:37:56 2021 +0200
27.3 @@ -351,7 +351,7 @@
27.4 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
27.5 \ (Try (Rewrite_Set fasse_zusammen False)) #> \
27.6 \ (Try (Rewrite_Set verschoenere False))) t_t)"
27.7 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
27.8 +val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
27.9 TermC.atomty sc;
27.10
27.11 "----------- me simplification.for_polynomials.with_minus";
27.12 @@ -468,7 +468,7 @@
27.13 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
27.14 \ (Try (Repeat (Calculate ''PLUS''))) #> \
27.15 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
27.16 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
27.17 +val sc = (inst_abs o (TermC.parseNEW'' thy)) str;
27.18 TermC.atomty sc;
27.19
27.20 "----------- pbl polynom probe -----------------------------------";
28.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Jul 19 18:39:02 2021 +0200
28.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue Jul 20 14:37:56 2021 +0200
28.3 @@ -20,22 +20,22 @@
28.4 "------------ pbl: rational, univariate, equation ----------------";
28.5 "------------ pbl: rational, univariate, equation ----------------";
28.6 "------------ pbl: rational, univariate, equation ----------------";
28.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "(1/b+1/x=1) is_ratequation_in x";
28.8 +val t = TermC.parseNEW'' thy "(1/b+1/x=1) is_ratequation_in x";
28.9 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
28.10 val result = UnparseC.term t_;
28.11 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
28.12
28.13 -val t = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)=1) is_ratequation_in x";
28.14 +val t = TermC.parseNEW'' thy "(sqrt(x)=1) is_ratequation_in x";
28.15 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
28.16 val result = UnparseC.term t_;
28.17 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
28.18
28.19 -val t = (Thm.term_of o the o (TermC.parse thy)) "(x=- 1) is_ratequation_in x";
28.20 +val t = TermC.parseNEW'' thy "(x=- 1) is_ratequation_in x";
28.21 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
28.22 val result = UnparseC.term t_;
28.23 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
28.24
28.25 -val t = (Thm.term_of o the o (TermC.parse thy)) "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
28.26 +val t = TermC.parseNEW'' thy "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
28.27 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
28.28 val result = UnparseC.term t_;
28.29 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
29.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Mon Jul 19 18:39:02 2021 +0200
29.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Tue Jul 20 14:37:56 2021 +0200
29.3 @@ -784,7 +784,7 @@
29.4 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
29.5 andalso ThmC.string_of_thm thm =
29.6 (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
29.7 - (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
29.8 + (Trueprop $ TermC.parseNEW'' thy "9 = 3 \<up> 2"))) then ()
29.9 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
29.10 \---------------------------------------------------------------------------------------/*)
29.11
29.12 @@ -803,7 +803,7 @@
29.13 val SOME (r as (Thm (str, thm))) = nex revsets t;
29.14 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
29.15 ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
29.16 - (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
29.17 + (Trueprop $ TermC.parseNEW'' thy "9 = 3 \<up> 2"))) then ()
29.18 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
29.19
29.20 (*check the next rule*)
30.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Mon Jul 19 18:39:02 2021 +0200
30.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Tue Jul 20 14:37:56 2021 +0200
30.3 @@ -175,18 +175,18 @@
30.4
30.5 (*
30.6 print("***** TERM2POLY-TESTS *****\n");
30.7 -val t0 = (Thm.term_of o the o (TermC.parse thy)) "3 * 4";
30.8 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "27";
30.9 -val t11= (Thm.term_of o the o (TermC.parse thy)) "27 * c";
30.10 -val t2 = (Thm.term_of o the o (TermC.parse thy)) "b";
30.11 -val t23= (Thm.term_of o the o (TermC.parse thy)) "c \<up> 7";
30.12 -val t24= (Thm.term_of o the o (TermC.parse thy)) "5 * c \<up> 7";
30.13 -val t26= (Thm.term_of o the o (TermC.parse thy)) "a * b";
30.14 -val t3 = (Thm.term_of o the o (TermC.parse thy)) "2 + a";
30.15 -val t4 = (Thm.term_of o the o (TermC.parse thy)) "b + a";
30.16 -val t5 = (Thm.term_of o the o (TermC.parse thy)) "2 + a \<up> 3";*)
30.17 -val t6 = (Thm.term_of o the o (TermC.parse thy)) "5*a \<up> 2*b \<up> 3*c+4*a \<up> 4*b+2*a*c";
30.18 -val t7 = (Thm.term_of o the o (TermC.parse thy)) "a-b";
30.19 +val t0 = TermC.parseNEW'' thy "3 * 4";
30.20 +val t1 = TermC.parseNEW'' thy "27";
30.21 +val t11= TermC.parseNEW'' thy "27 * c";
30.22 +val t2 = TermC.parseNEW'' thy "b";
30.23 +val t23= TermC.parseNEW'' thy "c \<up> 7";
30.24 +val t24= TermC.parseNEW'' thy "5 * c \<up> 7";
30.25 +val t26= TermC.parseNEW'' thy "a * b";
30.26 +val t3 = TermC.parseNEW'' thy "2 + a";
30.27 +val t4 = TermC.parseNEW'' thy "b + a";
30.28 +val t5 = TermC.parseNEW'' thy "2 + a \<up> 3";*)
30.29 +val t6 = TermC.parseNEW'' thy "5*a \<up> 2*b \<up> 3*c+4*a \<up> 4*b+2*a*c";
30.30 +val t7 = TermC.parseNEW'' thy "a-b";
30.31 (*
30.32 (the o term2poly) t0;
30.33 (the o term2poly) t1;
30.34 @@ -204,21 +204,21 @@
30.35
30.36 print("\n\n***** STEP_CANCEL_TESTS: *****\n");
30.37 (*
30.38 -val term2 = (Thm.term_of o the o (TermC.parse thy)) " (9 * a \<up> 2 * b) /// (6 * a * c)";
30.39 +val term2 = TermC.parseNEW'' thy " (9 * a \<up> 2 * b) /// (6 * a * c)";
30.40 val div2 = step_cancel term2;
30.41 atomt div2;
30.42 *)
30.43
30.44 -val term1 = (Thm.term_of o the o (TermC.parse thy)) "(10 * a \<up> 2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b \<up> 2 * c) /// a";
30.45 +val term1 = TermC.parseNEW'' thy "(10 * a \<up> 2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b \<up> 2 * c) /// a";
30.46 val div1 = step_cancel term1;
30.47 -(*if div1 = (Thm.term_of o the o (TermC.parse thy)) "((10 * a * b * c + 14 * b + 3 * c + 20 * b \<up> 2 * c) * a) /// (1 * a)" then () else raise error ("Test failed");*)
30.48 +(*if div1 = TermC.parseNEW'' thy "((10 * a * b * c + 14 * b + 3 * c + 20 * b \<up> 2 * c) * a) /// (1 * a)" then () else raise error ("Test failed");*)
30.49
30.50 -val term2 = (Thm.term_of o the o (TermC.parse thy)) "(10 * a \<up> 2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b \<up> 2 * c) /// (5 * a * b * c + 7 * a \<up> 2 * b * c) ";
30.51 +val term2 = TermC.parseNEW'' thy "(10 * a \<up> 2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b \<up> 2 * c) /// (5 * a * b * c + 7 * a \<up> 2 * b * c) ";
30.52 val div2 = step_cancel term2;
30.53 (*if div2 = ([(10,[1,1,1]),(20,[0,2,1]),(14,[0,1,0]),(3,[0,0,1])],[(1,[1,0,0])],[(7,[1,1,1]),(5,[0,1,1])]) then () else raise error ("Test failed");*)
30.54
30.55
30.56 -val term3 = (Thm.term_of o the o (TermC.parse thy)) "(10 * a \<up> 2 * b * c) /// (1 * x * y * z) ";
30.57 +val term3 = TermC.parseNEW'' thy "(10 * a \<up> 2 * b * c) /// (1 * x * y * z) ";
30.58 val div3 = step_cancel term3;
30.59
30.60
30.61 @@ -237,7 +237,7 @@
30.62
30.63 val thy = Rational.thy;
30.64 val rls = Prls {func=cancel};
30.65 -val t = (Thm.term_of o the o (TermC.parse thy))
30.66 +val t = TermC.parseNEW'' thy
30.67 "(1 + 1 * a \<up> 1)///(- 2 + 2 * a \<up> 2)";
30.68 val (t,asm) = the (rewrite_set_ thy eval_rls false rls t);
30.69
30.70 @@ -261,9 +261,9 @@
30.71 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
30.72
30.73 (*
30.74 -val term2 = (Thm.term_of o the o (TermC.parse thy)) "(a \<up> 2 * b + 2 * a * b + b ) /// ( a \<up> 2 - 1 )";
30.75 +val term2 = TermC.parseNEW'' thy "(a \<up> 2 * b + 2 * a * b + b ) /// ( a \<up> 2 - 1 )";
30.76 val div2 = direct_cancel term2;
30.77 -val t = (Thm.term_of o the o (TermC.parse thy)) "(1 + 1 * a \<up> 1)///(- 2 + 2 * a \<up> 2) = 0";*)
30.78 +val t = TermC.parseNEW'' thy "(1 + 1 * a \<up> 1)///(- 2 + 2 * a \<up> 2) = 0";*)
30.79
30.80
30.81
30.82 @@ -291,7 +291,7 @@
30.83 val e186c'="(144 * a \<up> 2 * b * c) / (12 * a * b * c )";
30.84 val e186c = (the (rewrite_set thy' "rational_erls" false rls' e186c'))
30.85 handle e => OldGoals.print_exn e;
30.86 -val t = (Thm.term_of o the o (TermC.parse thy)) e186c';
30.87 +val t = TermC.parseNEW'' thy e186c';
30.88 atomt t;
30.89
30.90 print("\n\nexample 187:\n");
30.91 @@ -731,8 +731,8 @@
30.92 OK Thm ("real_mult_div_cancel2", "?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n")]
30.93 -------- revset ----------------------------------------------------
30.94
30.95 - val t = (Thm.term_of o the o (TermC.parse thy)) "(-6) * x";
30.96 - val t = (Thm.term_of o the o (TermC.parse thy))
30.97 + val t = TermC.parseNEW'' thy "(-6) * x";
30.98 + val t = TermC.parseNEW'' thy
30.99 "(9 + (- 1)*x \<up> 2) / (9 + ((-6)*x + x \<up> 2))";
30.100 val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)")
30.101 handle e => OldGoals.print_exn e;
30.102 @@ -744,38 +744,38 @@
30.103
30.104 (* SK: Testbeispiele --- WN kopiert Rational.ML -> rational.sml-----
30.105
30.106 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))";
30.107 +val t1 = TermC.parseNEW'' thy "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))";
30.108 val SOME (t1',rest)= cancel_ thy t1;
30.109 val SOME (t1'',_)= factor_out_gcd_ thy t1;
30.110 print(UnparseC.term t1'^" + Einschr\"ankung: "^UnparseC.term (hd(rest)));
30.111 UnparseC.term t1'';
30.112
30.113 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "((-3 * x \<up> 2 + 6 *x - 3) / (2*x - 2))";
30.114 +val t1 = TermC.parseNEW'' thy "((-3 * x \<up> 2 + 6 *x - 3) / (2*x - 2))";
30.115 val SOME (t1',_)= cancel_ thy t1;
30.116 val SOME (t1'',_)= factor_expanded_ thy t1;
30.117 UnparseC.term t1';
30.118 UnparseC.term t1'';
30.119
30.120 -val t2 = (Thm.term_of o the o (TermC.parse thy)) "((x+ (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))";
30.121 +val t2 = TermC.parseNEW'' thy "((x+ (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))";
30.122 val SOME (t2',_) = add_fractions_ thy t2;
30.123 val SOME (t2'',_) = common_nominators_ thy t2;
30.124 UnparseC.term t2';
30.125 UnparseC.term t2'';
30.126
30.127 -val t2 = (Thm.term_of o the o (TermC.parse thy)) "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
30.128 +val t2 = TermC.parseNEW'' thy "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
30.129 val SOME (t2',_) = add_expanded_frac_ thy t2;
30.130 val SOME (t2'',_) = common_expanded_nom_ thy t2;
30.131 UnparseC.term t2';
30.132 UnparseC.term t2'';
30.133
30.134
30.135 -val t3 = (Thm.term_of o the o (TermC.parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x + (- 2))) + ((1) / ( x \<up> 2 + (- 1)))+((1) / (x \<up> 2 + (- 2)*x + 1))";
30.136 +val t3 = TermC.parseNEW'' thy "((1) / (2*x + 2)) + ((1) / (2*x + (- 2))) + ((1) / ( x \<up> 2 + (- 1)))+((1) / (x \<up> 2 + (- 2)*x + 1))";
30.137 val SOME (t3',_) = common_nominators_ thy t3;
30.138 val SOME (t3'',_) = add_fractions_ thy t3;
30.139 (UnparseC.term t3');
30.140 (UnparseC.term t3'');
30.141
30.142 -val t3 = (Thm.term_of o the o (TermC.parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x \<up> 2 - 1))+((1) / (x \<up> 2 - 2 * x + 1))";
30.143 +val t3 = TermC.parseNEW'' thy "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x \<up> 2 - 1))+((1) / (x \<up> 2 - 2 * x + 1))";
30.144 val SOME (t3',_) = common_expanded_nom_ thy t3;
30.145 val SOME (t3'',_) = add_expanded_frac_ thy t3;
30.146 (UnparseC.term t3');
30.147 @@ -787,10 +787,10 @@
30.148 UnparseC.term t4;
30.149 UnparseC.term (hd(t5));*)
30.150
30.151 -(*val test1 = (Thm.term_of o the o (TermC.parse thy)) "1 - x \<up> 2 - 5 * x \<up> 5";
30.152 -val test2 = (Thm.term_of o the o (TermC.parse thy)) "1 + (- 1) * x \<up> 2 + (-5) * x \<up> 5";
30.153 -val test2 = (Thm.term_of o the o (TermC.parse thy)) "1 - x";
30.154 -val test2 = (Thm.term_of o the o (TermC.parse thy)) "1 + (- 1) * x";
30.155 +(*val test1 = TermC.parseNEW'' thy "1 - x \<up> 2 - 5 * x \<up> 5";
30.156 +val test2 = TermC.parseNEW'' thy "1 + (- 1) * x \<up> 2 + (-5) * x \<up> 5";
30.157 +val test2 = TermC.parseNEW'' thy "1 - x";
30.158 +val test2 = TermC.parseNEW'' thy "1 + (- 1) * x";
30.159 UnparseC.term(expanded2term(test1));
30.160 UnparseC.term(term2expanded(test2)); *)
30.161
31.1 --- a/test/Tools/isac/Knowledge/rlang.sml Mon Jul 19 18:39:02 2021 +0200
31.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Tue Jul 20 14:37:56 2021 +0200
31.3 @@ -186,9 +186,9 @@
31.4 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
31.5
31.6 (*WN---v *)
31.7 -val bdv= (Thm.term_of o the o (TermC.parse thy)) "bdv";
31.8 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
31.9 -val t = (Thm.term_of o the o (TermC.parse thy)) "3 * x / 5";
31.10 +val bdv= TermC.parseNEW'' thy "bdv";
31.11 +val v = TermC.parseNEW'' thy "x";
31.12 +val t = TermC.parseNEW'' thy "3 * x / 5";
31.13 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true
31.14 [ (bdv, v) ] make_ratpoly_in t;
31.15 if UnparseC.term t' = "3 / 5 * x" then () else error "rlang.sml: 1";
32.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Jul 19 18:39:02 2021 +0200
32.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Tue Jul 20 14:37:56 2021 +0200
32.3 @@ -27,37 +27,37 @@
32.4 "------------ tests on predicates -------------------------------";
32.5 "------------ tests on predicates -------------------------------";
32.6 "------------ tests on predicates -------------------------------";
32.7 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
32.8 +val t1 = TermC.parseNEW'' thy "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
32.9 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.10 if (UnparseC.term t) = "False" then ()
32.11 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
32.12
32.13 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/x) is_rootRatAddTerm_in x";
32.14 +val t1 = TermC.parseNEW'' thy "(1/x) is_rootRatAddTerm_in x";
32.15 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.16 if (UnparseC.term t) = "False" then ()
32.17 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
32.18
32.19 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
32.20 +val t1 = TermC.parseNEW'' thy "(1/sqrt(x)) is_rootRatAddTerm_in x";
32.21 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.22 if (UnparseC.term t) = "False" then ()
32.23 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
32.24
32.25 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
32.26 +val t1 = TermC.parseNEW'' thy "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
32.27 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.28 if (UnparseC.term t) = "True" then ()
32.29 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
32.30
32.31 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
32.32 +val t1 = TermC.parseNEW'' thy "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
32.33 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.34 if (UnparseC.term t) = "True" then ()
32.35 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
32.36
32.37 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
32.38 +val t1 = TermC.parseNEW'' thy "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
32.39 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.40 if (UnparseC.term t) = "True" then ()
32.41 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
32.42
32.43 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
32.44 +val t1 = TermC.parseNEW'' thy "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
32.45 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32.46 if (UnparseC.term t) = "True" then ()
32.47 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
33.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Mon Jul 19 18:39:02 2021 +0200
33.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue Jul 20 14:37:56 2021 +0200
33.3 @@ -56,20 +56,20 @@
33.4 "solutions L"
33.5
33.6 before 6.5.03:
33.7 -> val t = (Thm.term_of o the o (TermC.parse thy)) "testdscforlist [#1]";
33.8 +> val t = TermC.parseNEW'' thy "testdscforlist [#1]";
33.9 > val (d,ts) = Input_Descript.split t;
33.10 > Input_Descript.join thy (d,ts);
33.11 val it = "testdscforlist [#1]" : cterm
33.12
33.13 -> val t = (Thm.term_of o the o (TermC.parse thy)) "(A::real)";
33.14 +> val t = TermC.parseNEW'' thy "(A::real)";
33.15 > val (d,ts) = Input_Descript.split t;
33.16 val d = Const ("empty", "empty") : term
33.17 val ts = [Free ("A", "RealDef.real")] : term list
33.18 -> val t = (Thm.term_of o the o (TermC.parse thy)) "[R=(R::real)]";
33.19 +> val t = TermC.parseNEW'' thy "[R=(R::real)]";
33.20 > val (d,ts) = Input_Descript.split t;
33.21 val d = Const ("empty", "empty") : term
33.22 val ts = [Const # $ Free # $ Free (#,#)] : term list
33.23 -> val t = (Thm.term_of o the o (TermC.parse thy)) "[#1,#2]";
33.24 +> val t = TermC.parseNEW'' thy "[#1,#2]";
33.25 > val (d,ts) = Input_Descript.split t;
33.26 val ts = [Free ("#1", "'a"),Free ("#2", "'a")] : NOT WANTED
33.27 *)
33.28 @@ -77,13 +77,13 @@
33.29 "----------- type penv -------------------------------------------------------------------------";
33.30 "----------- type penv -------------------------------------------------------------------------";
33.31 (*
33.32 - val e_ = (Thm.term_of o the o (TermC.parse thy)) "e_::bool";
33.33 - val ev = (Thm.term_of o the o (TermC.parse thy)) "#4 + #3 * x \<up> #2 = #0";
33.34 - val v_ = (Thm.term_of o the o (TermC.parse thy)) "v_";
33.35 - val vv = (Thm.term_of o the o (TermC.parse thy)) "x";
33.36 - val r_ = (Thm.term_of o the o (TermC.parse thy)) "err_::bool";
33.37 - val rv1 = (Thm.term_of o the o (TermC.parse thy)) "#0";
33.38 - val rv2 = (Thm.term_of o the o (TermC.parse thy)) "eps";
33.39 + val e_ = TermC.parseNEW'' thy "e_::bool";
33.40 + val ev = TermC.parseNEW'' thy "#4 + #3 * x \<up> #2 = #0";
33.41 + val v_ = TermC.parseNEW'' thy "v_";
33.42 + val vv = TermC.parseNEW'' thy "x";
33.43 + val r_ = TermC.parseNEW'' thy "err_::bool";
33.44 + val rv1 = TermC.parseNEW'' thy "#0";
33.45 + val rv2 = TermC.parseNEW'' thy "eps";
33.46
33.47 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
33.48 map getval penv;
33.49 @@ -108,7 +108,7 @@
33.50 val t as t1 $ t2 = TermC.str2term "antiDerivativeName M_b";
33.51 pbl_ids ctxt t1 t2;
33.52
33.53 - val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues [r=Arbfix]";
33.54 + val t = TermC.parseNEW'' thy "fixedValues [r=Arbfix]";
33.55 val (d,argl) = strip_comb t;
33.56 Input_Descript.is_a d; (*see Input_Descript.split*)
33.57 dest_list (d,argl);
34.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 18:39:02 2021 +0200
34.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Jul 20 14:37:56 2021 +0200
34.3 @@ -36,7 +36,7 @@
34.4 val thy = @{theory Complex_Main};
34.5 val ctxt = @{context};
34.6 val thm = @{thm add.commute};
34.7 -val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
34.8 +val t = TermC.parseNEW'' thy "((r + u) + t) + s";
34.9 "----- from old: fun rewrite__";
34.10 val bdv = [];
34.11 val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
34.12 @@ -52,6 +52,9 @@
34.13 writeln(Syntax.string_of_term ctxt LHS);
34.14 writeln(Syntax.string_of_term ctxt t);
34.15
34.16 +(*broken with "reduce the number of TermC.parse*-------exception MATCH---------------------\\
34.17 +TOODOO ERROR exception MATCH raised (line 284 of "pattern.ML)
34.18 +
34.19 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
34.20 val (rew, RHS) = (Envir.subst_term
34.21 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
34.22 @@ -76,7 +79,7 @@
34.23 (*is displayed on top of <response> buffer...*)
34.24 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
34.25 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
34.26 -(**)
34.27 +--broken with "reduce the number of TermC.parse*------------------------------------------//( **)
34.28
34.29 "----------- test rewriting without Isac's thys ------------------------------------------------";
34.30 "----------- test rewriting without Isac's thys ------------------------------------------------";
35.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Jul 19 18:39:02 2021 +0200
35.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Jul 20 14:37:56 2021 +0200
35.3 @@ -307,8 +307,7 @@
35.4 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
35.5 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
35.6 (cs', (encode ifo));
35.7 -val SOME f_in = TermC.parse (ThyC.get_theory "Isac_Knowledge") istr
35.8 - val f_in = Thm.term_of f_in
35.9 +val SOME f_in = TermC.parseNEW (ThyC.id_to_ctxt "Isac_Knowledge") istr
35.10 val f_succ = get_curr_formula (pt, pos);
35.11 f_succ = f_in = false;
35.12 val NONE = CAS_Cmd.input f_in
36.1 --- a/test/Tools/isac/MathEngine/me-misc.sml Mon Jul 19 18:39:02 2021 +0200
36.2 +++ b/test/Tools/isac/MathEngine/me-misc.sml Tue Jul 20 14:37:56 2021 +0200
36.3 @@ -22,7 +22,7 @@
36.4 moveActiveRoot 1;
36.5 autoCalculate 1 CompleteCalc;
36.6 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
36.7 - replaceFormula 1 "x = 1";
36.8 + replaceFormula 1 "x = (1::real)";
36.9 (*... returns calcChangedEvent with ...*)
36.10 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
36.11 val ((pt,_),_) = get_calc 1;
37.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Mon Jul 19 18:39:02 2021 +0200
37.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Jul 20 14:37:56 2021 +0200
37.3 @@ -7,7 +7,7 @@
37.4 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
37.5 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
37.6 (*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
37.7 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
37.8 +val fmz = ["equality (x+1=(2::real))", "solveFor (x::real)", "solutions (L::bool list)"];
37.9 val (dI',pI',mI') =
37.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
37.11 ["Test", "squ-equ-test-subpbl1"]);
37.12 @@ -90,7 +90,9 @@
37.13 = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
37.14 result = f', ostate = s}) pt p);
37.15
37.16 -(*/--------------------- step into Deriv.embed -----------------------------------------------\*)
37.17 +(*/--------------------- step into Deriv.embed -----------------------------------------------\* )
37.18 +(*broken with "reduce the number of TermC.parse*"
37.19 +TOODOO ERROR: ("no derivation found", ([(Empty_Tac, Empty_Tac_, (([], Und),..*)
37.20 val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
37.21 (*case*)
37.22 Step_Solve.by_term ptp (encode ifo) (*of*);
37.23 @@ -156,8 +158,10 @@
37.24
37.25 (*-------------------- stop step into -------------------------------------------------------*)
37.26 (*\------------------- end step into -------------------------------------------------------/*)
37.27 +----- broken with "reduce the number of TermC.parse*"------------------------------------//*)
37.28
37.29 -(*/--------------------- final test ----------------------------------------------------------\*)
37.30 +(*/--------------------- final test ----------------------------------------------------------\* )
37.31 +(*TOODOO final test*)
37.32 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
37.33 ;
37.34 if
37.35 @@ -191,3 +195,5 @@
37.36 ([1], Res), 2 + - 1 + x = 2
37.37 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]
37.38 *)
37.39 +( *\--------------------- final test ----------------------------------------------------------/*)
37.40 +
38.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Jul 19 18:39:02 2021 +0200
38.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Jul 20 14:37:56 2021 +0200
38.3 @@ -26,7 +26,7 @@
38.4
38.5
38.6 (*
38.7 -> val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";
38.8 +> val t = TermC.parseNEW'' thy "#2 \<up> #3";
38.9 > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
38.10 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
38.11 > Syntax.string_of_term (ThyC.to_ctxt thy) t';
38.12 @@ -131,7 +131,7 @@
38.13 " _________________ rewrite_ x+4_________________ ";
38.14 " _________________ rewrite_ x+4_________________ ";
38.15 " _________________ rewrite_ x+4_________________ ";
38.16 -val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
38.17 +val t = TermC.parseNEW'' thy "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
38.18 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
38.19 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
38.20 val rls = Test_simplify;
38.21 @@ -374,7 +374,7 @@
38.22 *)
38.23
38.24 (*
38.25 -val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
38.26 +val t = TermC.parseNEW'' thy "solutions (L::real set)";
38.27 TermC.atomty t;
38.28 *)
38.29
39.1 --- a/test/Tools/isac/OLDTESTS/script.sml Mon Jul 19 18:39:02 2021 +0200
39.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Tue Jul 20 14:37:56 2021 +0200
39.3 @@ -265,7 +265,7 @@
39.4 val eq_ = (Thm.term_of o the o (TermC.parse thy))"e_::bool";
39.5
39.6 val ct = "0+(sqrt(sqrt(sqrt a)) \<up> 2) \<up> 2=0";
39.7 -val ve0_= (Thm.term_of o the o (TermC.parse thy)) ct;
39.8 +val ve0_= TermC.parseNEW'' thy ct;
39.9 val ets0=[([],(Tac_(Program.thy,"BS", "", ""),[(eq_,ve0_)],[(eq_,ve0_)],
39.10 TermC.empty,TermC.empty,Safe)),
39.11 ([],(User', [], [], TermC.empty, TermC.empty,Sundef))]:ets;
40.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Mon Jul 19 18:39:02 2021 +0200
40.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Tue Jul 20 14:37:56 2021 +0200
40.3 @@ -9,28 +9,28 @@
40.4 (*---------------- 25.7.02 ---------------------*)
40.5
40.6 val thy = (theory "Isac_Knowledge");
40.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "contains_root (sqrt(x)=1)";
40.8 +val t = TermC.parseNEW'' thy "contains_root (sqrt(x)=1)";
40.9 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;
40.10
40.11 -val t = (Thm.term_of o the o (TermC.parse thy)) "is_rootequation_in (sqrt(x)=1) x";
40.12 +val t = TermC.parseNEW'' thy "is_rootequation_in (sqrt(x)=1) x";
40.13 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
40.14
40.15 (*---
40.16 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
40.17 -val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*x)";
40.18 +val v = TermC.parseNEW'' thy "x";
40.19 +val t = TermC.parseNEW'' thy "sqrt(#3+#4*x)";
40.20 scan t v;
40.21 -val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*a)";
40.22 +val t = TermC.parseNEW'' thy "sqrt(#3+#4*a)";
40.23 scan t v;
40.24 -val t = (Thm.term_of o the o (TermC.parse thy)) "#1 + #2*sqrt(#3+#4*x)";
40.25 +val t = TermC.parseNEW'' thy "#1 + #2*sqrt(#3+#4*x)";
40.26 scan t v;
40.27 -val t = (Thm.term_of o the o (TermC.parse thy)) "x + #2*sqrt(#3+#4*a)";
40.28 +val t = TermC.parseNEW'' thy "x + #2*sqrt(#3+#4*a)";
40.29 scan t v;
40.30 ---*)
40.31 -val t = (Thm.term_of o the o (TermC.parse thy))
40.32 +val t = TermC.parseNEW'' thy
40.33 "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";
40.34 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
40.35
40.36 -val t = (Thm.term_of o the o (TermC.parse thy))
40.37 +val t = TermC.parseNEW'' thy
40.38 "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";
40.39 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
40.40
41.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 18:39:02 2021 +0200
41.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Jul 20 14:37:56 2021 +0200
41.3 @@ -129,13 +129,13 @@
41.4
41.5 (*--------------(2): does divide work in Test_simplify ?: ------*)
41.6 val thy = @{theory Test};
41.7 - val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
41.8 + val t = TermC.parseNEW'' thy "6 / 2";
41.9 val rls = Test_simplify;
41.10 val (t,_) = the (rewrite_set_ thy false rls t);
41.11 (*val t = Free ("3", "Real.real") : term*)
41.12
41.13 (*--------------(3): is_const works ?: -------------------------------------*)
41.14 - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
41.15 + val t = TermC.parseNEW'' thy "2 is_const";
41.16 TermC.atomty t;
41.17 rewrite_set_ @{theory Test} false tval_rls t;
41.18 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
41.19 @@ -152,19 +152,19 @@
41.20 Rewrite.trace_on := false; (*true false*)
41.21 val thy = @{theory Test};
41.22 val rls = Test_simplify;
41.23 - val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
41.24 + val t = TermC.parseNEW'' thy "(-4) / 2";
41.25
41.26 val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
41.27
41.28 (*--------------(5): reproduce (1) with simpler term: ------------*)
41.29 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
41.30 + val t = TermC.parseNEW'' thy "(3+5)/2::real";
41.31 case rewrite_set_ thy false rls t of
41.32 SOME (t', []) =>
41.33 if UnparseC.term t' = "4" then ()
41.34 else error "rewrite_set_ (3+5)/2 changed 1"
41.35 | _ => error "rewrite_set_ (3+5)/2 changed 2";
41.36
41.37 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
41.38 + val t = TermC.parseNEW'' thy "(3+1+2*x)/2::real";
41.39 case rewrite_set_ thy false rls t of
41.40 SOME (t', _) => (*WAS "x + 2" WITH OLD numerals TOODOO?*)
41.41 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
41.42 @@ -202,7 +202,7 @@
41.43
41.44 (*===================*)
41.45 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
41.46 - val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2";
41.47 + val t = TermC.parseNEW'' thy "x + (- 1 + -3) / 2::real";
41.48 val SOME (res, []) = rewrite_set_ thy false rls t;
41.49 (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
41.50 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
41.51 @@ -227,17 +227,17 @@
41.52 " ================= evaluate.sml: calculate_ 2002 =================== ";
41.53
41.54 val thy = @{theory Test};
41.55 -val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
41.56 +val t = TermC.parseNEW'' thy "12 / 3";
41.57 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
41.58 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
41.59 "12 / 3 = 4";
41.60 val thy = @{theory Test};
41.61 -val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
41.62 +val t = TermC.parseNEW'' thy "4 \<up> 2";
41.63 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
41.64 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
41.65 "4 ^ 2 = 16";
41.66
41.67 - val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
41.68 + val t = TermC.parseNEW'' thy "((1 + 2) * 4 / 3) \<up> 2";
41.69 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
41.70 "1 + 2 = 3";
41.71 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
41.72 @@ -262,7 +262,7 @@
41.73 else ();
41.74
41.75 (*13.9.02 *** calc: operator = pow not defined*)
41.76 - val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
41.77 + val t = TermC.parseNEW'' thy "3 \<up> 2";
41.78 val SOME (thmID,thm) =
41.79 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
41.80 (*** calc: operator = pow not defined*)
42.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Mon Jul 19 18:39:02 2021 +0200
42.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Tue Jul 20 14:37:56 2021 +0200
42.3 @@ -89,7 +89,7 @@
42.4 "-------- fun eval_const -----------------------------------------------------------------------";
42.5 "-------- fun eval_const -----------------------------------------------------------------------";
42.6 "-------- fun eval_const -----------------------------------------------------------------------";
42.7 -val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
42.8 +val t = TermC.parseNEW'' @{theory Test} "2 is_const";
42.9 case rewrite_set_ @{theory Test} false tval_rls t of
42.10 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
42.11 | _ => error "2 is_const CHANGED";
42.12 @@ -236,84 +236,84 @@
42.13 "-------- fun eval_occurs_in -------------------------------------------------------------------";
42.14 "-------- fun eval_occurs_in -------------------------------------------------------------------";
42.15 "-------- fun eval_occurs_in -------------------------------------------------------------------";
42.16 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.17 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
42.18 +val v = TermC.parseNEW'' thy "x";
42.19 +val t = TermC.parseNEW'' thy "1";
42.20 if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
42.21
42.22 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.23 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
42.24 +val v = TermC.parseNEW'' thy "AA";
42.25 +val t = TermC.parseNEW'' thy "1";
42.26 if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
42.27
42.28 (*----------*)
42.29 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.30 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
42.31 +val v = TermC.parseNEW'' thy "x";
42.32 +val t = TermC.parseNEW'' thy "a*b+c";
42.33 if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
42.34
42.35 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.36 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
42.37 +val v = TermC.parseNEW'' thy "AA";
42.38 +val t = TermC.parseNEW'' thy "a*b+c";
42.39 if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
42.40
42.41 (*----------*)
42.42 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.43 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
42.44 +val v = TermC.parseNEW'' thy "x";
42.45 +val t = TermC.parseNEW'' thy "a*x+c";
42.46 if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
42.47
42.48 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.49 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
42.50 +val v = TermC.parseNEW'' thy "AA";
42.51 +val t = TermC.parseNEW'' thy "a*AA+c";
42.52 if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
42.53
42.54 (*----------*)
42.55 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.56 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
42.57 +val v = TermC.parseNEW'' thy "x";
42.58 +val t = TermC.parseNEW'' thy "(a*b+c)*x \<up> 7";
42.59 if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \<up> 7) x ..changed";
42.60
42.61 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.62 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
42.63 +val v = TermC.parseNEW'' thy "AA";
42.64 +val t = TermC.parseNEW'' thy "(a*b+c)*AA \<up> 7";
42.65 if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \<up> 7) AA ..changed";
42.66
42.67 (*----------*)
42.68 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.69 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
42.70 +val v = TermC.parseNEW'' thy "x";
42.71 +val t = TermC.parseNEW'' thy "x \<up> 7";
42.72 if occurs_in v t then () else error "factor_right_deg (x \<up> 7) x ..changed";
42.73
42.74 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.75 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
42.76 +val v = TermC.parseNEW'' thy "AA";
42.77 +val t = TermC.parseNEW'' thy "AA \<up> 7";
42.78 if occurs_in v t then () else error "factor_right_deg (AA \<up> 7) AA ..changed";
42.79
42.80 (*----------*)
42.81 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.82 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
42.83 +val v = TermC.parseNEW'' thy "x";
42.84 +val t = TermC.parseNEW'' thy "(a*b+c)*x";
42.85 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
42.86
42.87 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.88 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
42.89 +val v = TermC.parseNEW'' thy "AA";
42.90 +val t = TermC.parseNEW'' thy "(a*b+c)*AA";
42.91 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
42.92
42.93 (*----------*)
42.94 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.95 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
42.96 +val v = TermC.parseNEW'' thy "x";
42.97 +val t = TermC.parseNEW'' thy "(a*b+x)*x";
42.98 if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
42.99
42.100 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.101 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
42.102 +val v = TermC.parseNEW'' thy "AA";
42.103 +val t = TermC.parseNEW'' thy "(a*b+AA)*AA";
42.104 if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
42.105
42.106 (*----------*)
42.107 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.108 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
42.109 +val v = TermC.parseNEW'' thy "x";
42.110 +val t = TermC.parseNEW'' thy "x";
42.111 if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
42.112
42.113 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.114 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.115 +val v = TermC.parseNEW'' thy "AA";
42.116 +val t = TermC.parseNEW'' thy "AA";
42.117 if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
42.118
42.119 (*----------*)
42.120 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
42.121 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
42.122 +val v = TermC.parseNEW'' thy "x";
42.123 +val t = TermC.parseNEW'' thy "ab - (a*b)*x";
42.124 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
42.125
42.126 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
42.127 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
42.128 +val v = TermC.parseNEW'' thy "AA";
42.129 +val t = TermC.parseNEW'' thy "ab - (a*b)*AA";
42.130 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
42.131
42.132
42.133 @@ -406,13 +406,13 @@
42.134 "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
42.135 "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
42.136 val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
42.137 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
42.138 +val t = TermC.parseNEW'' thy "2 * 3::real";
42.139 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;
42.140 ;
42.141 "~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
42.142 (thy, op_, ef, t);
42.143 op_ = op0 = true;val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
42.144 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
42.145 +val t = TermC.parseNEW'' thy "2 * 3::real";
42.146
42.147 ef op_ t thy;
42.148 "~~~~~ fun eval_binop , args:"; val ((thmid : string), (op_: string),
43.1 --- a/test/Tools/isac/Specify/refine.sml Mon Jul 19 18:39:02 2021 +0200
43.2 +++ b/test/Tools/isac/Specify/refine.sml Tue Jul 20 14:37:56 2021 +0200
43.3 @@ -25,20 +25,20 @@
43.4 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
43.5
43.6 (*case 1: no refinement *)
43.7 -val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]");
43.8 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)");
43.9 +val (d1,ts1) = Input_Descript.split (TermC.parseNEW'' thy "fixedValues [aaa = 0]");
43.10 +val (d2,ts2) = Input_Descript.split (TermC.parseNEW'' thy "errorBound (ddd = 0)");
43.11 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
43.12
43.13 (*case 2: refined to pbt without children *)
43.14 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]");
43.15 +val (d2,ts2) = Input_Descript.split (TermC.parseNEW'' thy "relations [aaa333]");
43.16 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
43.17
43.18 (*case 3: refined to pbt with children *)
43.19 -val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]");
43.20 +val (d2,ts2) = Input_Descript.split (TermC.parseNEW'' thy "valuesFor [aaa222]");
43.21 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
43.22
43.23 (*case 4: refined to children (without child)*)
43.24 -val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy");
43.25 +val (d3,ts3) = Input_Descript.split (TermC.parseNEW'' thy "boundVariable aaa222yyy");
43.26 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
43.27
43.28 (*=================================================================
44.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 18:39:02 2021 +0200
44.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Jul 20 14:37:56 2021 +0200
44.3 @@ -228,11 +228,11 @@
44.4 ML_file "Minisubpbl/710-interSteps-short.sml"
44.5 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
44.6 ML_file "Minisubpbl/790-complete.sml"
44.7 - ML_file "Minisubpbl/800-append-on-Frm.sml"
44.8 + ML_file "Minisubpbl/800-append-on-Frm.sml"(*STARTbroken with "reduce the number of TermC.parse*"*)
44.9
44.10 subsection \<open>further functionality alongside batch build sequence\<close>
44.11 ML_file "MathEngBasic/thmC.sml"
44.12 - ML_file "MathEngBasic/rewrite.sml"
44.13 + ML_file "MathEngBasic/rewrite.sml"
44.14 ML_file "MathEngBasic/tactic.sml"
44.15 (** )ML_file "MathEngBasic/ctree.sml" ( ** )loops with eliminate ThmC.numerals_to_Free*)
44.16 ML_file "MathEngBasic/calculation.sml"
44.17 @@ -254,16 +254,16 @@
44.18
44.19 ML_file "Interpret/istate.sml"
44.20 ML_file "Interpret/sub-problem.sml"
44.21 - ML_file "Interpret/error-pattern.sml"
44.22 + ML_file "Interpret/error-pattern.sml" (*broken with "reduce the number of TermC.parse*"*)
44.23 ML_file "Interpret/li-tool.sml"
44.24 - ML_file "Interpret/lucas-interpreter.sml"
44.25 + ML_file "Interpret/lucas-interpreter.sml" (*broken with "reduce the number of TermC.parse*"*)
44.26 ML_file "Interpret/step-solve.sml"
44.27
44.28 ML_file "MathEngine/me-misc.sml"
44.29 ML_file "MathEngine/fetch-tactics.sml"
44.30 ML_file "MathEngine/solve.sml"
44.31 ML_file "MathEngine/step.sml"
44.32 - ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
44.33 + ML_file "MathEngine/mathengine-stateless.sml" (*broken with "reduce the number of TermC.parse*"*)
44.34 ML_file "MathEngine/messages.sml"
44.35 ML_file "MathEngine/states.sml"
44.36
44.37 @@ -280,7 +280,7 @@
44.38 ML_file "Knowledge/delete.sml"
44.39 ML_file "Knowledge/descript.sml"
44.40 ML_file "Knowledge/simplify.sml"
44.41 - ML_file "Knowledge/poly-1.sml"
44.42 +(* ML_file "Knowledge/poly-1.sml" broken with "reduce the number of TermC.parse*"*)
44.43 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*)
44.44 ML_file "Knowledge/gcd_poly_ml.sml"
44.45 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
44.46 @@ -322,7 +322,21 @@
44.47 ML_file "Test_Code/test-code.sml"
44.48
44.49 section \<open>further tests additional to src/.. files\<close>
44.50 - ML_file "BridgeLibisabelle/use-cases.sml"
44.51 +(*ML_file "BridgeLibisabelle/use-cases.sml" broken with "reduce the number of TermC.parse*"*)
44.52 +ML \<open>
44.53 +\<close> ML \<open>
44.54 +(*TOODOO broken with "reduce the number of TermC.parse---------------------------------------\\*"
44.55 + TOODOObroken with "reduce the number of TermC.parse*"--------------------------------------//*)
44.56 +\<close> ML \<open>
44.57 +\<close> ML \<open>
44.58 +\<close> ML \<open>
44.59 +\<close> ML \<open>
44.60 +\<close> ML \<open>
44.61 +\<close> ML \<open>
44.62 +\<close> ML \<open>
44.63 +\<close> ML \<open>
44.64 +\<close> ML \<open>
44.65 +\<close>
44.66
44.67 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
44.68 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
45.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 19 18:39:02 2021 +0200
45.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 20 14:37:56 2021 +0200
45.3 @@ -163,43 +163,43 @@
45.4 "----------- tests on predicates in problems ---------------------";
45.5 "----------- tests on predicates in problems ---------------------";
45.6 "----------- tests on predicates in problems ---------------------";
45.7 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
45.8 + val t1 = TermC.parseNEW'' thy "lhs (-8 - 2*x + x \<up> 2 = 0)";
45.9 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
45.10 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
45.11 else error "polyeq.sml: diff.behav. in lhs";
45.12
45.13 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
45.14 + val t2 = TermC.parseNEW'' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
45.15 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
45.16 if (UnparseC.term t) = "True" then ()
45.17 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
45.18
45.19 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
45.20 + val t0 = TermC.parseNEW'' thy "(sqrt(x)) is_poly_in x";
45.21 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
45.22 if (UnparseC.term t) = "False" then ()
45.23 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
45.24
45.25 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
45.26 + val t3 = TermC.parseNEW'' thy "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
45.27 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
45.28 if (UnparseC.term t) = "True" then ()
45.29 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
45.30
45.31 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
45.32 + val t4 = TermC.parseNEW'' thy "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
45.33 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
45.34 if (UnparseC.term t) = "True" then ()
45.35 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
45.36
45.37 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
45.38 + val t6 = TermC.parseNEW'' thy "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
45.39 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
45.40 if (UnparseC.term t) = "True" then ()
45.41 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
45.42
45.43 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
45.44 + val t3 = TermC.parseNEW'' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
45.45 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
45.46 if (UnparseC.term t) = "True" then ()
45.47 else error "polyeq.sml: diff.behav. in has_degree_in_in";
45.48
45.49 \<close> ML \<open>
45.50 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
45.51 + val t3 = TermC.parseNEW'' thy "((sqrt(x)) has_degree_in x) = 2";
45.52 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
45.53 \<close> ML \<open>
45.54 UnparseC.term t = "- 1 = 2";
45.55 @@ -208,14 +208,12 @@
45.56 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
45.57
45.58 \<close> ML \<open>
45.59 - val t4 = (Thm.term_of o the o (TermC.parse thy))
45.60 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
45.61 + val t4 = TermC.parseNEW'' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
45.62 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
45.63 if (UnparseC.term t) = "False" then ()
45.64 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
45.65
45.66 -val t5 = (Thm.term_of o the o (TermC.parse thy))
45.67 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
45.68 +val t5 = TermC.parseNEW'' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
45.69 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
45.70 if (UnparseC.term t) = "True" then ()
45.71 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
45.72 @@ -250,7 +248,7 @@
45.73 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
45.74
45.75 (*Aufgabe zum Einstieg in die Arbeit...*)
45.76 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
45.77 + val t = TermC.parseNEW'' thy "a*b - (a+b)*x + x \<up> 2 = 0";
45.78 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
45.79 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
45.80 UnparseC.term t;
45.81 @@ -280,9 +278,9 @@
45.82 *)
45.83
45.84 "------ 15.11.02 --------------------------";
45.85 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
45.86 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
45.87 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
45.88 + val t = TermC.parseNEW'' thy "1 + a * x + b * x";
45.89 + val bdv = TermC.parseNEW'' thy "bdv";
45.90 + val a = TermC.parseNEW'' thy "a";
45.91
45.92 Rewrite.trace_on := false; (*true false*)
45.93 (* Anwenden einer Regelmenge aus Termorder.ML: *)
45.94 @@ -294,7 +292,7 @@
45.95 UnparseC.term t;
45.96 "1 + b * x + x * a";
45.97
45.98 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
45.99 + val t = TermC.parseNEW'' thy "1 + a * (x + b * x) + a \<up> 2";
45.100 val SOME (t,_) =
45.101 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
45.102 UnparseC.term t;
45.103 @@ -303,7 +301,7 @@
45.104 UnparseC.term t;
45.105 "1 + (x + b * x) * a + a \<up> 2";
45.106
45.107 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
45.108 + val t = TermC.parseNEW'' thy "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
45.109 val SOME (t,_) =
45.110 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
45.111 UnparseC.term t;
45.112 @@ -323,7 +321,7 @@
45.113 get_thm Termorder.thy "bdv_n_collect";
45.114 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
45.115 *)
45.116 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
45.117 + val t = TermC.parseNEW'' thy "a \<up> 2 * x + 7 * a \<up> 2";
45.118 val SOME (t,_) =
45.119 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
45.120 UnparseC.term t;
45.121 @@ -342,14 +340,14 @@
45.122 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
45.123 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
45.124 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
45.125 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
45.126 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
45.127 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
45.128 + val substa = [(TermC.empty, TermC.parseNEW'' thy "a")];
45.129 + val substb = [(TermC.empty, TermC.parseNEW'' thy "b")];
45.130 + val substx = [(TermC.empty, TermC.parseNEW'' thy "x")];
45.131
45.132 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
45.133 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
45.134 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
45.135 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
45.136 + val x1 = TermC.parseNEW'' thy "a + b + x::real";
45.137 + val x2 = TermC.parseNEW'' thy "a + x + b::real";
45.138 + val x3 = TermC.parseNEW'' thy "a + x + b::real";
45.139 + val x4 = TermC.parseNEW'' thy "x + a + b::real";
45.140
45.141 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
45.142 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
45.143 @@ -360,22 +358,22 @@
45.144 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
45.145 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
45.146
45.147 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
45.148 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
45.149 + val aa = TermC.parseNEW'' thy "- 1 * a * x";
45.150 + val bb = TermC.parseNEW'' thy "x \<up> 3";
45.151 ord_make_polynomial_in true thy substx (aa, bb);
45.152 true; (* => LESS *)
45.153
45.154 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
45.155 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
45.156 + val aa = TermC.parseNEW'' thy "- 1 * a * x";
45.157 + val bb = TermC.parseNEW'' thy "x \<up> 3";
45.158 ord_make_polynomial_in true thy substa (aa, bb);
45.159 false; (* => GREATER *)
45.160
45.161 (* und nach dem Re-engineering der Termorders in den 'rulesets'
45.162 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
45.163 - val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
45.164 - val x = (Thm.term_of o the o (TermC.parse thy)) "x";
45.165 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
45.166 - val b = (Thm.term_of o the o (TermC.parse thy)) "b";
45.167 + val bdv= TermC.parseNEW'' thy "''bdv''";
45.168 + val x = TermC.parseNEW'' thy "x";
45.169 + val a = TermC.parseNEW'' thy "a";
45.170 + val b = TermC.parseNEW'' thy "b";
45.171 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
45.172 if UnparseC.term t' = "b + x + a" then ()
45.173 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
45.174 @@ -387,7 +385,7 @@
45.175 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
45.176
45.177 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
45.178 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
45.179 + val ppp = TermC.parseNEW'' thy ppp';
45.180 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
45.181
45.182 UnparseC.term t' = "- 6 + - (5 * x) + x \<up> 3 + - (x \<up> 2) + - (x \<up> 3) +\n- (14 * x \<up> 2)"
45.183 @@ -400,7 +398,7 @@
45.184 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
45.185
45.186 val ttt' = "(3*x + 5)/18";
45.187 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
45.188 + val ttt = TermC.parseNEW'' thy ttt';
45.189 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
45.190 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
45.191 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
45.192 @@ -1096,7 +1094,7 @@
45.193 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
45.194 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
45.195 "---- test the erls ----";
45.196 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
45.197 + val t1 = TermC.parseNEW'' thy "0 <= (10/3/2) \<up> 2 - 1";
45.198 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
45.199 val t' = UnparseC.term t;
45.200 (*if t'= "HOL.True" then ()
45.201 @@ -1198,11 +1196,11 @@
45.202 Find =["derivative f_f'"],
45.203 With =[],
45.204 Relate=[]}:string ppc;
45.205 -val chkpbt = ((map (the o (TermC.parse thy))) o P_Model.to_list) pbt;
45.206 +val chkpbt = ((map (TermC.parseNEW'' thy)) o P_Model.to_list) pbt;
45.207
45.208 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))",
45.209 "differentiateFor x", "derivative f_f'"];
45.210 -val chkorg = map (the o (TermC.parse thy)) org;
45.211 +val chkorg = map (TermC.parseNEW'' thy) org;
45.212
45.213 Problem.from_store ["derivative_of", "function"];
45.214 MethodC.from_store ["diff", "differentiate_on_R"];
45.215 @@ -1211,18 +1209,18 @@
45.216 "----------- for correction of diff_const ---------------";
45.217 "----------- for correction of diff_const ---------------";
45.218 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
45.219 -val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)";
45.220 +val t = TermC.parseNEW'' thy "Not (x =!= a)";
45.221 case rewrite_set_ thy false erls_diff t of
45.222 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
45.223 | _ => error "rewrite_set_ Not (x =!= a) changed";
45.224
45.225 -val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_const";
45.226 +val t = TermC.parseNEW'' thy "2 is_const";
45.227 case rewrite_set_ thy false erls_diff t of
45.228 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
45.229 | _ => error "rewrite_set_ 2 is_const changed";
45.230
45.231 val thm = @{thm diff_const};
45.232 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x";
45.233 +val ct = TermC.parseNEW'' thy "d_d x x";
45.234 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
45.235 val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
45.236
45.237 @@ -1230,10 +1228,10 @@
45.238 "----------- for correction of diff_quot ----------------";
45.239 "----------- for correction of diff_quot ----------------";
45.240 val thy = @{theory "Diff"};
45.241 -val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)";
45.242 +val ct = TermC.parseNEW'' thy "Not (x = 0)";
45.243 rewrite_set_ thy false erls_diff ct;
45.244
45.245 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))";
45.246 +val ct = TermC.parseNEW'' thy "d_d x ((x+1) / (x - 1))";
45.247 val thm = @{thm diff_quot};
45.248 val SOME (ctt,_) =
45.249 (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
45.250 @@ -1242,7 +1240,7 @@
45.251 "----------- differentiate by rewrite -------------------";
45.252 "----------- differentiate by rewrite -------------------";
45.253 val thy = @{theory "Diff"};
45.254 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \<up> 2 + 3 * x + 4)";
45.255 +val ct = TermC.parseNEW'' thy "d_d x (x \<up> 2 + 3 * x + 4)";
45.256 "--- 1 ---";
45.257 val thm = @{thm "diff_sum"};
45.258 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
45.259 @@ -1265,7 +1263,7 @@
45.260 "--- 7 ---";
45.261 "--- 7 ---";
45.262 val rls = Test_simplify;
45.263 -val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \<up> (2 - 1) + 3 * 1 + 0";
45.264 +val ct = TermC.parseNEW'' thy "2 * x \<up> (2 - 1) + 3 * 1 + 0";
45.265 val (ct, _) = the (rewrite_set_ thy true rls ct);
45.266 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
45.267
45.268 @@ -1393,6 +1391,7 @@
45.269 else error "diff.sml: diff.behav. in 'primed'";
45.270 TermC.atomty f'_;
45.271
45.272 +\<close> ML \<open>
45.273 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
45.274 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
45.275 \ in (((Try (Repeat (Rewrite frac_conv))) #> \
45.276 @@ -1421,7 +1420,8 @@
45.277 \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
45.278 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
45.279 ;
45.280 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
45.281 +\<close> ML \<open>
45.282 +val sc = (inst_abs o (TermC.parseNEW'' thy )) str;
45.283
45.284
45.285 \<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
45.286 @@ -1869,23 +1869,23 @@
45.287 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
45.288
45.289 \<close> ML \<open>
45.290 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";
45.291 +val t = TermC.parseNEW'' thy "Integral x D x";
45.292 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.293 if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
45.294
45.295 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
45.296 +val t = TermC.parseNEW'' thy "Integral c * x \<up> 2 + c_2 D x";
45.297 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.298 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
45.299
45.300 \<close> ML \<open>
45.301 val rls = add_new_c;
45.302 -val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";
45.303 +val t = TermC.parseNEW'' thy "c * (x \<up> 3 / 3) + c_2 * x";
45.304 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.305 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
45.306 else error "integrate.sml: diff.behav. in add_new_c simpl.";
45.307
45.308 \<close> ML \<open>
45.309 -val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";
45.310 +val t = TermC.parseNEW'' thy "F x = x \<up> 3 / 3 + x";
45.311 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.312 if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
45.313 else error "integrate.sml: diff.behav. in add_new_c equation";
45.314 @@ -1893,7 +1893,7 @@
45.315 \<close> ML \<open>
45.316 val rls = simplify_Integral;
45.317 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
45.318 -val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
45.319 +val t = TermC.parseNEW'' thy "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
45.320 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.321 if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
45.322 then () else error "integrate.sml: diff.behav. in simplify_I #1";
45.323 @@ -1901,13 +1901,13 @@
45.324 \<close> ML \<open>
45.325 val rls = integration;
45.326 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
45.327 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
45.328 +val t = TermC.parseNEW'' thy "Integral c * x \<up> 2 + c_2 D x";
45.329 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.330 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
45.331 then () else error "integrate.sml: diff.behav. in integration #1";
45.332
45.333 \<close> ML \<open>
45.334 -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";
45.335 +val t = TermC.parseNEW'' thy "Integral 3*x \<up> 2 + 2*x + 1 D x";
45.336 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.337 if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
45.338 else error "integrate.sml: diff.behav. in integration #2";
45.339 @@ -1921,7 +1921,7 @@
45.340 then () else error "integrate.sml: diff.behav. in integration #3";
45.341
45.342 \<close> text \<open> (*TOODOO rls "integration" does NOT work anymore *)
45.343 -val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
45.344 +val t = TermC.parseNEW'' thy ("Integral " ^ UnparseC.term res ^ " D x");
45.345 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
45.346 if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
45.347 then () else error "integrate.sml: diff.behav. in integration #4";
45.348 @@ -1963,23 +1963,27 @@
45.349 Find =["antiDerivative F_F"],
45.350 With =[],
45.351 Relate=[]}:string ppc;
45.352 -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
45.353 -val t1 = (Thm.term_of o hd) chkmodel;
45.354 -val t2 = (Thm.term_of o hd o tl) chkmodel;
45.355 -val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
45.356 +\<close> ML \<open>
45.357 +val chkmodel = (map (TermC.parseNEW'' thy) o P_Model.to_list) model;
45.358 +\<close> ML \<open>
45.359 +val t1 = hd chkmodel;
45.360 +val t2 = (hd o tl) chkmodel;
45.361 +val t3 = (hd o tl o tl) chkmodel;
45.362 case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
45.363 | _ => error "integrate.sml: Integrate.antiDerivative ???";
45.364
45.365 \<close> ML \<open>
45.366 +Thm.term_of: cterm -> term
45.367 +\<close> ML \<open>
45.368 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
45.369 Where =[],
45.370 Find =["antiDerivativeName F_F"],
45.371 With =[],
45.372 Relate=[]}:string ppc;
45.373 -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
45.374 -val t1 = (Thm.term_of o hd) chkmodel;
45.375 -val t2 = (Thm.term_of o hd o tl) chkmodel;
45.376 -val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
45.377 +val chkmodel = (map (TermC.parseNEW'' thy) o P_Model.to_list) model;
45.378 +val t1 = (hd) chkmodel;
45.379 +val t2 = (hd o tl) chkmodel;
45.380 +val t3 = (hd o tl o tl) chkmodel;
45.381 case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
45.382 | _ => error "integrate.sml: Integrate.antiDerivativeName";
45.383
45.384 @@ -2209,10 +2213,10 @@
45.385 if UnparseC.term t' = "True" then ()
45.386 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
45.387
45.388 -val SOME t = TermC.parse thy "solution LL";
45.389 -TermC.atomty (Thm.term_of t);
45.390 -val SOME t = TermC.parse thy "solution LL";
45.391 -TermC.atomty (Thm.term_of t);
45.392 +val t = TermC.parseNEW'' thy "solution LL";
45.393 +TermC.atomty t;
45.394 +val t = TermC.parseNEW'' thy "solution LL";
45.395 +TermC.atomty t;
45.396
45.397 val t = TermC.str2term
45.398 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";