1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Sep 29 19:34:32 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Nov 16 18:26:57 2021 +0100
1.3 @@ -248,10 +248,10 @@
1.4 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
1.5 *)
1.6 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
1.7 - [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionTerm", [t]),
1.8 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
1.9 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivative",
1.10 - [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'"])
1.11 + [((TermC.parseNEW''\<^theory>) "functionTerm", [t]),
1.12 + ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]),
1.13 + ((TermC.parseNEW''\<^theory>) "derivative",
1.14 + [(TermC.parseNEW''\<^theory>) "f_f'"])
1.15 ]
1.16 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
1.17 \<close>
1.18 @@ -394,10 +394,10 @@
1.19 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
1.20 *)
1.21 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
1.22 - [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionEq", [t]),
1.23 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
1.24 - ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivativeEq",
1.25 - [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'::bool"])
1.26 + [((TermC.parseNEW''\<^theory>) "functionEq", [t]),
1.27 + ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]),
1.28 + ((TermC.parseNEW''\<^theory>) "derivativeEq",
1.29 + [(TermC.parseNEW''\<^theory>) "f_f'::bool"])
1.30 ]
1.31 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
1.32 \<close>
2.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Sep 29 19:34:32 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Tue Nov 16 18:26:57 2021 +0100
2.3 @@ -21,7 +21,7 @@
2.4 substitution :: "bool => una"
2.5
2.6 (*the CAS-commands*)
2.7 - solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
2.8 + solve :: "[bool * real] => bool list"(*solveFor ::"real => una"; eg.solve (x+1=2, x)*)
2.9 solveTest :: "[bool * 'a] => bool list" (* for test collection *)
2.10
2.11 text \<open>defines equation and univariate-equation
2.12 @@ -57,10 +57,6 @@
2.13 ML\<open>
2.14 (*.function for handling the cas-input "solve (x+1=2, x)":
2.15 make a model which is already in ctree-internal format.*)
2.16 -(* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
2.17 - val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy))
2.18 - "solveTest (x+1=2, x)");
2.19 - *)
2.20 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =
2.21 [((the o (TermC.parseNEW \<^context>)) "equality", [eq]),
2.22 ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]),
2.23 @@ -76,10 +72,10 @@
2.24 Problem: "univariate/equation"
2.25
2.26 method met_equ : "Equation" =
2.27 - \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
2.28 - errpats = [], nrls = Rule_Set.empty}\<close>
2.29 + \<open>{rew_ord' = "tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.empty,
2.30 + prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
2.31
2.32 ML \<open>
2.33 \<close> ML \<open>
2.34 \<close>
2.35 -end
2.36 \ No newline at end of file
2.37 +end
3.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed Sep 29 19:34:32 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Tue Nov 16 18:26:57 2021 +0100
3.3 @@ -48,9 +48,9 @@
3.4 "Simplify (2*a + 3*a)");
3.5 *)
3.6 fun argl2dtss t =
3.7 - [((Thm.term_of o the o (TermC.parse @{theory})) "Term", t),
3.8 - ((Thm.term_of o the o (TermC.parse @{theory})) "normalform",
3.9 - [(Thm.term_of o the o (TermC.parse @{theory})) "N"])
3.10 + [((TermC.parseNEW''\<^theory>) "Term", t),
3.11 + ((TermC.parseNEW''\<^theory>) "normalform",
3.12 + [(TermC.parseNEW''\<^theory>) "N"])
3.13 ]
3.14 (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
3.15 \<close>
4.1 --- a/src/Tools/isac/MathEngBasic/method.sml Wed Sep 29 19:34:32 2021 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Nov 16 18:26:57 2021 +0100
4.3 @@ -54,7 +54,7 @@
4.4 val gi = (case gi of
4.5 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
4.6 | ((_, gi') :: []) =>
4.7 - (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
4.8 + (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) gi'\<close> of
4.9 SOME x => x
4.10 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
4.11 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
4.12 @@ -64,7 +64,7 @@
4.13 val fi = (case fi of
4.14 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
4.15 | ((_, fi') :: []) =>
4.16 - (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
4.17 + (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) fi'\<close> of
4.18 SOME x => x
4.19 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
4.20 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
4.21 @@ -74,7 +74,7 @@
4.22 val re = (case re of
4.23 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
4.24 | ((_,re') :: []) =>
4.25 - (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
4.26 + (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) re'\<close> of
4.27 SOME x => x
4.28 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
4.29 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
5.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Sep 29 19:34:32 2021 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Tue Nov 16 18:26:57 2021 +0100
5.3 @@ -80,7 +80,7 @@
5.4 val gi = (case gi of
5.5 [] => []
5.6 | ((_, gi') :: []) =>
5.7 - (case \<^try>\<open> map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
5.8 + (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) gi'\<close> of
5.9 SOME x => x
5.10 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Given' of " ^ strs2str pblID))
5.11 | _ => raise ERROR ("prep_input: more than one '#Given' in " ^ strs2str pblID));
5.12 @@ -90,7 +90,7 @@
5.13 val fi = (case fi of
5.14 [] => []
5.15 | ((_, fi') :: []) =>
5.16 - (case \<^try>\<open> map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
5.17 + (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) fi'\<close> of
5.18 SOME x => x
5.19 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))
5.20 | _ => raise ERROR ("prep_input: more than one '#Find' in " ^ strs2str pblID));
5.21 @@ -100,7 +100,7 @@
5.22 val re = (case re of
5.23 [] => []
5.24 | ((_, re') :: []) =>
5.25 - (case \<^try>\<open> map (split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
5.26 + (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) re'\<close> of
5.27 SOME x => x
5.28 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))
5.29 | _ => raise ERROR ("prep_input: more than one '#Relate' in " ^ strs2str pblID));
5.30 @@ -116,7 +116,7 @@
5.31 | _ => raise ERROR ("prep_input: more than one '#Where' in " ^ strs2str pblID));
5.32 in
5.33 ({guh = guh, mathauthors = maa, init = init, thy = thy,
5.34 - cas = Option.map (Thm.term_of o the o TermC.parse thy) ca,
5.35 + cas = Option.map (TermC.parseNEW'' thy) ca,
5.36 prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
5.37 end;
5.38
6.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Sep 29 19:34:32 2021 +0200
6.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Tue Nov 16 18:26:57 2021 +0100
6.3 @@ -55,10 +55,10 @@
6.4
6.5 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
6.6 needs to be here after def. Subproblem in Prog_Tac.thy *)
6.7 -val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
6.8 +val subpbl_t $ (pair_t $ _ $ _) = (TermC.parseNEW'' @{theory Prog_Tac})
6.9 "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"
6.10 val pbl_t $ _ =
6.11 - (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
6.12 + (TermC.parseNEW'' @{theory Prog_Tac}) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
6.13
6.14 fun subpbl domID pblID =
6.15 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
7.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Sep 29 19:34:32 2021 +0200
7.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Nov 16 18:26:57 2021 +0100
7.3 @@ -25,8 +25,8 @@
7.4
7.5 ML \<open>
7.6 \<close> ML \<open>
7.7 -val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
7.8 -val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
7.9 +val UniversalList = TermC.parseNEW''\<^theory> "UniversalList";
7.10 +val EmptyList = TermC.parseNEW''\<^theory> "[]::bool list";
7.11 \<close> ML \<open>
7.12 \<close>
7.13
8.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Sep 29 19:34:32 2021 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Nov 16 18:26:57 2021 +0100
8.3 @@ -92,22 +92,6 @@
8.4 | _ => ls @ [o1, o2])
8.5 | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
8.6 in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
8.7 -(*>val t = @{term True};
8.8 -> val t' = or2list t;
8.9 -> term2str t';
8.10 -"ListC.UniversalList"
8.11 -> val t = @{term False};
8.12 -> val t' = or2list t;
8.13 -> term2str t';
8.14 -"[]"
8.15 -> val t=(Thm.term_of o the o (parse thy)) "x=3";
8.16 -> val t' = or2list t;
8.17 -> term2str t';
8.18 -"[x = 3]"
8.19 -> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
8.20 -> val t' = or2list t;
8.21 -> term2str t';
8.22 -"[x = #3, x = #-3, x = #0]" : string *)
8.23
8.24
8.25 (** evaluation on the meta-level **)
8.26 @@ -125,58 +109,6 @@
8.27 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
8.28 in SOME (UnparseC.term_in_thy thy prop, prop) end
8.29 | eval_matches _ _ _ _ = NONE;
8.30 -(*
8.31 -> val t = (Thm.term_of o the o (parse thy))
8.32 - "matches (?x = 0) (1 * x \<up> 2 = 0)";
8.33 -> eval_matches "/thmid/" "/op_/" t thy;
8.34 -val it =
8.35 - SOME
8.36 - ("matches (x = 0) (1 * x \<up> 2 = 0) = False",
8.37 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
8.38 -
8.39 -> val t = (Thm.term_of o the o (parse thy))
8.40 - "matches (?a = #0) (#1 * x \<up> #2 = #0)";
8.41 -> eval_matches "/thmid/" "/op_/" t thy;
8.42 -val it =
8.43 - SOME
8.44 - ("matches (?a = #0) (#1 * x \<up> #2 = #0) = True",
8.45 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
8.46 -
8.47 -> val t = (Thm.term_of o the o (parse thy))
8.48 - "matches (?a * x = #0) (#1 * x \<up> #2 = #0)";
8.49 -> eval_matches "/thmid/" "/op_/" t thy;
8.50 -val it =
8.51 - SOME
8.52 - ("matches (?a * x = #0) (#1 * x \<up> #2 = #0) = False",
8.53 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
8.54 -
8.55 -> val t = (Thm.term_of o the o (parse thy))
8.56 - "matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0)";
8.57 -> eval_matches "/thmid/" "/op_/" t thy;
8.58 -val it =
8.59 - SOME
8.60 - ("matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0) = True",
8.61 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
8.62 ------ before ?patterns ---:
8.63 -> val t = (Thm.term_of o the o (parse thy))
8.64 - "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";
8.65 -> eval_matches "/thmid/" "/op_/" t thy;
8.66 -SOME
8.67 - ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
8.68 - Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
8.69 - : (string * term) option
8.70 -
8.71 -> val t = (Thm.term_of o the o (parse thy))
8.72 - "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";
8.73 -> eval_matches "/thmid/" "/op_/" t thy;
8.74 -SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
8.75 - Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
8.76 -
8.77 -> val t = (Thm.term_of o the o (parse thy))
8.78 - "matches (a = b) (x + #1 + #-1 * #2 = #0)";
8.79 -> eval_matches "/thmid/" "/op_/" t thy;
8.80 -SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
8.81 -*)
8.82
8.83 (*.does a pattern match some subterm ?.*)
8.84 fun matchsub thy t pat =
9.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Sep 29 19:34:32 2021 +0200
9.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue Nov 16 18:26:57 2021 +0100
9.3 @@ -188,7 +188,7 @@
9.4 | ts_in (Mis _) = []
9.5 | ts_in _ = raise ERROR "ts_in: uncovered case in fun.def.";
9.6
9.7 -val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
9.8 +val unique = TermC.parseNEW'' @{theory "Real"} "UnIqE_tErM";
9.9 fun d_in (Cor ((d ,_), _)) = d
9.10 | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
9.11 | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
10.1 --- a/src/Tools/isac/Specify/p-spec.sml Wed Sep 29 19:34:32 2021 +0200
10.2 +++ b/src/Tools/isac/Specify/p-spec.sml Tue Nov 16 18:26:57 2021 +0100
10.3 @@ -80,13 +80,13 @@
10.4 | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
10.5 | parsitm dI (i, v, b, f, I_Model.Syn str) =
10.6 (case \<^try>\<open>
10.7 - let val _ = (Thm.term_of o the o (TermC.parse dI)) str
10.8 + let val _ = TermC.parseNEW'' dI str
10.9 in (i, v, b ,f, I_Model.Par str) end\<close> of
10.10 SOME x => x
10.11 | NONE => (i, v, b, f, I_Model.Syn str))
10.12 | parsitm dI (i, v, b, f, I_Model.Typ str) =
10.13 (case \<^try>\<open>
10.14 - let val _ = (Thm.term_of o the o (TermC.parse dI)) str
10.15 + let val _ = TermC.parseNEW'' dI str
10.16 in (i, v, b, f, I_Model.Par str) end\<close> of
10.17 SOME x => x
10.18 | NONE => (i, v, b, f, I_Model.Syn str))
11.1 --- a/test/Tools/isac/Test_Some.thy Wed Sep 29 19:34:32 2021 +0200
11.2 +++ b/test/Tools/isac/Test_Some.thy Tue Nov 16 18:26:57 2021 +0100
11.3 @@ -48,7 +48,7 @@
11.4 open Rewrite_Ord
11.5 open UnparseC
11.6 \<close>
11.7 -(*ML_file "BridgeJEdit/parseC.sml"*)
11.8 +(**)ML_file "MathEngBasic/ctree.sml"(**)
11.9
11.10 section \<open>code for copy & paste ===============================================================\<close>
11.11 ML \<open>
11.12 @@ -104,9 +104,143 @@
11.13 \<close> ML \<open>
11.14 \<close>
11.15
11.16 -section \<open>===================================================================================\<close>
11.17 +section \<open>============== new ctree 5 minisubpbl ========================================\<close>
11.18 ML \<open>
11.19 \<close> ML \<open>
11.20 +(*+*) @{term solveFor}
11.21 +\<close> ML \<open>
11.22 +"=====new ctree 5 minisubpbl =====================================";
11.23 +"=====new ctree 5 minisubpbl =====================================";
11.24 +"=====new ctree 5 minisubpbl =====================================";
11.25 +reset_states ();
11.26 +CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
11.27 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
11.28 + ["Test", "squ-equ-test-subpbl1"]))];
11.29 +Iterator 1; moveActiveRoot 1;
11.30 +\<close> ML \<open>
11.31 +(*+*)val ((pt,_),_) = get_calc 1;
11.32 +(*val pt =
11.33 + Nd (PblObj
11.34 + {branch = TransitiveB, ctxt = <context>, fmz =
11.35 + (["equality (x+1=(2::real))", "solveFor x", "solutions L"],
11.36 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
11.37 + ["Test", "squ-equ-test-subpbl1"])),
11.38 + loc =
11.39 + (SOME
11.40 + (Pstate
11.41 + {act_arg = Const ("empty", "??.'a"), assoc = false, env = [], eval =
11.42 + Repeat
11.43 + {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord =
11.44 + ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty},
11.45 + form_arg = NONE, found_accept = false, or = ORundef, path = []},
11.46 + <context>),
11.47 + NONE),
11.48 + meth = [], origin =
11.49 + ([(1, [1], "#Given", Const ("Input_Descript.equality", "bool \<Rightarrow> una"),
11.50 + [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
11.51 + (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $
11.52 + Const ("Groups.one_class.one", "real")) $
11.53 + (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
11.54 + (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))]),
11.55 + (2, [1], "#Given", Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]),
11.56 + (3, [1], "#Find", Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"),
11.57 + [Free ("L", "bool list")])],
11.58 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
11.59 + ["Test", "squ-equ-test-subpbl1"]),
11.60 +--------------------------------------------vvvv headline of calc-head, as calculated initially(!)
11.61 + Const ("Equation.solve", "bool \<times> 'a \<Rightarrow> bool list") $
11.62 + (Const ("Product_Type.Pair", "bool \<Rightarrow> 'a \<Rightarrow> bool \<times> 'a") $
11.63 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
11.64 + (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $
11.65 + Const ("Groups.one_class.one", "real")) $
11.66 + (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
11.67 + (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $
11.68 + Free ("v_v", "'a"))),
11.69 +--------------------^^^^^^^^^^^
11.70 + ostate = Incomplete, probl = [], result = (Const ("empty", "??.'a"), []), spec =
11.71 + ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"])},
11.72 + []):
11.73 + ctree*)
11.74 +\<close> ML \<open>
11.75 +autoCalculate 1 CompleteCalc;
11.76 +val ((pt,_),_) = get_calc 1;
11.77 +\<close> ML \<open>
11.78 +Test_Tool.show_pt pt;
11.79 +
11.80 +\<close> ML \<open>
11.81 +"-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
11.82 +"-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
11.83 +"-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
11.84 +val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract (pt, ([], Frm));
11.85 +\<close> ML \<open>
11.86 +(UnparseC.term form, tac, UnparseC.terms_to_strings asm)
11.87 +(* =("solve (x + 1 = 2, v_v)", Apply_Method ["Test", "squ-equ-test-subpbl1"], [])
11.88 + ||| *)
11.89 +\<close> ML \<open>
11.90 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.91 + ("solve (x + 1 = 2, x)",
11.92 + Apply_Method ["Test", "squ-equ-test-subpbl1"],
11.93 + []) => ()
11.94 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([], Pbl)";
11.95 +
11.96 +\<close> ML \<open>
11.97 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Frm));
11.98 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.99 + ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
11.100 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([1], Frm)";
11.101 +
11.102 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
11.103 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.104 + ("x + 1 + - 1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
11.105 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([1], Res)";
11.106 +
11.107 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
11.108 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.109 + ("- 1 + x = 0",
11.110 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
11.111 + []) => ()
11.112 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([2], Res)";
11.113 +
11.114 +val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Pbl));
11.115 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.116 + ("solve (- 1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
11.117 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3], Pbl)";
11.118 +
11.119 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,1], Frm));
11.120 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.121 + ("- 1 + x = 0", Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), []) => ()
11.122 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,1], Frm)";
11.123 +
11.124 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,1], Res));
11.125 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.126 + ("x = 0 + - 1 * - 1", Rewrite_Set "Test_simplify", []) => ()
11.127 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,1], Res)";
11.128 +
11.129 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,2], Res));
11.130 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.131 + ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],
11.132 + []) => ()
11.133 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,2], Res)";
11.134 +
11.135 +(*========== inhibit exn AK110719 ==============================================
11.136 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Res));
11.137 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.138 + ("[x = 1]", Check_elementwise "Assumptions", []) => ()
11.139 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3], Res)";
11.140 +
11.141 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([4], Res));
11.142 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.143 + ("[x = 1]",
11.144 + Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
11.145 + []) => ()
11.146 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([4], Res)";
11.147 +
11.148 +val (Form form, tac, asm) = ME_Misc.pt_extract (pt, ([], Res));
11.149 +case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
11.150 + ("[x = 1]", NONE, []) => ()
11.151 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([], Res)";
11.152 +========== inhibit exn AK110719 ==============================================*)
11.153 +
11.154 \<close> ML \<open>
11.155 \<close> ML \<open>
11.156 \<close>