1.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Mar 13 10:46:34 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Mar 13 14:41:02 2018 +0100
1.3 @@ -168,17 +168,6 @@
1.4
1.5 (** evaluation of numerals and predicates **)
1.6
1.7 -(*does a term contain a root ? WN110518 seems incorrect, compare contains_root*)
1.8 -fun eval_root_free (thmid:string) _ (t as (Const (op0, t0) $ arg)) thy =
1.9 - if strip_thy op0 <> "is'_root'_free"
1.10 - then error ("eval_root_free: wrong " ^ op0)
1.11 - else if TermC.const_in (strip_thy op0) arg
1.12 - then SOME (TermC.mk_thmid thmid (term_to_string''' thy arg)"",
1.13 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.14 - else SOME (TermC.mk_thmid thmid (term_to_string''' thy arg)"",
1.15 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.16 -| eval_root_free _ _ _ _ = NONE;
1.17 -
1.18 (*does a term contain a root ?*)
1.19 fun eval_contains_root (thmid:string) _
1.20 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
1.21 @@ -202,8 +191,7 @@
1.22 | eval_precond_rootpbl _ _ _ _ = NONE;
1.23 *}
1.24 setup {* KEStore_Elems.add_calcs
1.25 - [("is_root_free", ("Test.is'_root'_free", eval_root_free"#is_root_free_e")),
1.26 - ("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
1.27 + [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
1.28 ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
1.29 ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
1.30 eval_precond_rootpbl"#Test.precond_rootpbl_"))] *}
1.31 @@ -271,7 +259,7 @@
1.32 Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}),
1.33
1.34 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.35 - Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_e"),
1.36 + Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),
1.37 Calc ("Tools.matches",eval_matches ""),
1.38 Calc ("Test.contains'_root",
1.39 eval_contains_root"#contains_root_"),
1.40 @@ -489,7 +477,7 @@
1.41 ("ident" ,("Atools.ident",eval_ident "#ident_")),
1.42 (*von hier (ehem.SqRoot*)
1.43 ("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
1.44 - ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")),
1.45 + ("Test.contains_root",("contains'_root", eval_contains_root "#contains'_root")),
1.46 ("Test.contains_root",("contains'_root",
1.47 eval_contains_root"#contains_root_"))
1.48 ];
2.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Mar 13 10:46:34 2018 +0100
2.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Mar 13 14:41:02 2018 +0100
2.3 @@ -19,6 +19,8 @@
2.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.5 val get_pair: theory -> string -> eval_fn -> term -> (string * term) option
2.6 val mk_rule: term list * term * term -> term
2.7 + val divisors: int -> int list
2.8 + val doubles: int list -> int list
2.9 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.10 end
2.11
3.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Mar 13 10:46:34 2018 +0100
3.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Mar 13 14:41:02 2018 +0100
3.3 @@ -5,7 +5,6 @@
3.4
3.5 signature TERMC =
3.6 sig
3.7 - val const_in: string -> term -> bool
3.8 val contains_Var: term -> bool
3.9 val dest_binop_typ: typ -> typ * typ * typ
3.10 val dest_equals: term -> term * term
3.11 @@ -283,7 +282,7 @@
3.12 let
3.13 fun get es (Const("List.list.Cons", _) $ t $ ls) = get (t :: es) ls
3.14 | get es (Const("List.list.Nil", _)) = es
3.15 - | get _ t = error ("isalist2list applied to NON-list '"^term2str t^"'")
3.16 + | get _ t = raise TERM ("isalist2list applied to NON-list: ", [t])
3.17 in (rev o (get [])) ls end;
3.18
3.19 fun is_list ((Const ("List.list.Cons", _)) $ _ $ _) = true
3.20 @@ -301,17 +300,17 @@
3.21 | strip_trueprop t = t;
3.22
3.23 (* (A1==>...An==>B) goes to (A1==>...An==>) Pure/logic.ML: term -> term list*)
3.24 -fun strip_imp_prems' (Const ("==>", _) $ A $ t) =
3.25 +fun strip_imp_prems' (Const ("Pure.imp", _) $ A $ t) =
3.26 let
3.27 - fun coll_prems As (Const("==>", _) $ A $ t) =
3.28 + fun coll_prems As (Const("Pure.imp", _) $ A $ t) =
3.29 coll_prems (As $ (Logic.implies $ A)) t
3.30 | coll_prems As _ = SOME As
3.31 in coll_prems (Logic.implies $ A) t end
3.32 | strip_imp_prems' _ = NONE; (* *)
3.33
3.34 (* (A1==>...An==>) (B) goes to (A1==>...An==>B), where B is lowest branch, 2002 Pure/thm.ML *)
3.35 -fun ins_concl (Const ("==>", _) $ A $ t) B = Logic.implies $ A $ (ins_concl t B)
3.36 - | ins_concl (Const ("==>", _) $ A ) B = Logic.implies $ A $ B
3.37 +fun ins_concl (Const ("Pure.imp", _) $ A $ t) B = Logic.implies $ A $ (ins_concl t B)
3.38 + | ins_concl (Const ("Pure.imp", _) $ A ) B = Logic.implies $ A $ B
3.39 | ins_concl t B = raise TERM ("ins_concl", [t, B]);
3.40
3.41 fun vperm (Var _, Var _) = true (* 2002 Pure/thm.ML *)
3.42 @@ -378,17 +377,6 @@
3.43 else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
3.44 end;
3.45
3.46 -fun const_in _ (Const _) = false
3.47 - | const_in str (Free (s, _)) = if strip_thy s = str then true else false
3.48 - | const_in _ (Bound _) = false
3.49 - | const_in _ (Var _) = false
3.50 - | const_in str (Abs (_, _, body)) = const_in str body
3.51 - | const_in str (f $ u) = const_in str f orelse const_in str u;
3.52 -
3.53 -
3.54 -
3.55 -
3.56 -
3.57 (** transform binary numeralsstrings **)
3.58 (*Makarius 100308, hacked by WN*)
3.59 val numbers_to_string =
4.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Mar 13 10:46:34 2018 +0100
4.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Mar 13 14:41:02 2018 +0100
4.3 @@ -19,6 +19,9 @@
4.4 "----------- calculate (2 * x is_const) -----------------";
4.5 "----------- fun get_pair: examples ------------------------------------------------------------";
4.6 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
4.7 +"----------- fun power -------------------------------------------------------------------------";
4.8 +"----------- fun divisors ----------------------------------------------------------------------";
4.9 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
4.10 "--------------------------------------------------------";
4.11 "--------------------------------------------------------";
4.12 "--------------------------------------------------------";
4.13 @@ -420,3 +423,30 @@
4.14 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
4.15 if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso thm2str thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
4.16 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
4.17 +
4.18 +"----------- fun power -------------------------------------------------------------------------";
4.19 +"----------- fun power -------------------------------------------------------------------------";
4.20 +"----------- fun power -------------------------------------------------------------------------";
4.21 +if power 2 3 = 8 then () else error "power 2 3 = 8";
4.22 +if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
4.23 +if power ~3 2 = 9 then () else error "power ~3 2 = 9";
4.24 +(power 3 ~2; error "power 3 ~2: should raise an exn") handle _ => 000;
4.25 +
4.26 +"----------- fun divisors ----------------------------------------------------------------------";
4.27 +"----------- fun divisors ----------------------------------------------------------------------";
4.28 +"----------- fun divisors ----------------------------------------------------------------------";
4.29 +if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";
4.30 +if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";
4.31 +if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";
4.32 +if divisors 11 = [11] then () else error "divisors 11 = [11]";
4.33 +
4.34 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
4.35 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
4.36 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
4.37 +if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";
4.38 +if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";
4.39 +
4.40 +if squfact 30 = 1 then () else error "squfact 30 changed";
4.41 +if squfact 32 = 4 then () else error "squfact 32 changed";
4.42 +if squfact 60 = 2 then () else error "squfact 60 changed";
4.43 +if squfact 11 = 1 then () else error "squfact 11 changed";
5.1 --- a/test/Tools/isac/ProgLang/termC.sml Tue Mar 13 10:46:34 2018 +0100
5.2 +++ b/test/Tools/isac/ProgLang/termC.sml Tue Mar 13 14:41:02 2018 +0100
5.3 @@ -15,7 +15,19 @@
5.4 "----------- uminus_to_string ---------------------------";
5.5 "----------- *** prep_pbt: syntax error in '#Where' of [v";
5.6 "----------- check writeln, tracing for string markup ---";
5.7 -"-------- build fun is_bdv_subst ---------------------------------";
5.8 +"----------- build fun is_bdv_subst ------------------------------------------------------------";
5.9 +"----------- fun str_of_int --------------------------------------------------------------------";
5.10 +"----------- fun scala_of_term -----------------------------------------------------------------";
5.11 +"----------- fun contains_Var ------------------------------------------------------------------";
5.12 +"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
5.13 +"----------- fun is_f_x ------------------------------------------------------------------------";
5.14 +"----------- fun list2isalist, fun isalist2list ------------------------------------------------";
5.15 +"----------- fun strip_imp_prems' --------------------------------------------------------------";
5.16 +"----------- fun ins_concl ---------------------------------------------------------------------";
5.17 +"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
5.18 +"----------- fun dest_binop_typ ----------------------------------------------------------------";
5.19 +"----------- fun is_list -----------------------------------------------------------------------";
5.20 +"----------- fun inst_abs ----------------------------------------------------------------------";
5.21 "--------------------------------------------------------";
5.22 "--------------------------------------------------------";
5.23
5.24 @@ -533,9 +545,9 @@
5.25 tracing "----------------DIFFERENT output----";
5.26 *)
5.27
5.28 -"-------- build fun is_bdv_subst ---------------------------------";
5.29 -"-------- build fun is_bdv_subst ---------------------------------";
5.30 -"-------- build fun is_bdv_subst ---------------------------------";
5.31 +"----------- build fun is_bdv_subst ------------------------------------------------------------";
5.32 +"----------- build fun is_bdv_subst ------------------------------------------------------------";
5.33 +"----------- build fun is_bdv_subst ------------------------------------------------------------";
5.34 fun is_bdv_subst (Const ("List.list.Cons", _) $
5.35 (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str
5.36 | is_bdv_subst _ = false;
5.37 @@ -546,62 +558,32 @@
5.38 if is_bdv_subst (str2term "[(bdv_1, v_s1),(bdv_2, v_s2)]") then ()
5.39 else error "is_bdv_subst canged 2";
5.40
5.41 -"----------- fun str_of_int ---------------------------------------------------------------------";
5.42 -"----------- fun str_of_int ---------------------------------------------------------------------";
5.43 -"----------- fun str_of_int ---------------------------------------------------------------------";
5.44 -(*
5.45 -> str_of_int 1;
5.46 -val it = "1" : string
5.47 -> str_of_int ~1;
5.48 -val it = "-1" : string
5.49 -*)
5.50 +"----------- fun str_of_int --------------------------------------------------------------------";
5.51 +"----------- fun str_of_int --------------------------------------------------------------------";
5.52 +"----------- fun str_of_int --------------------------------------------------------------------";
5.53 +if str_of_int 1 = "1" then () else error "str_of_int 1";
5.54 +if str_of_int ~1 = "-1" then () else error "str_of_int -1";
5.55
5.56 +"----------- fun scala_of_term -----------------------------------------------------------------";
5.57 +"----------- fun scala_of_term -----------------------------------------------------------------";
5.58 +"----------- fun scala_of_term -----------------------------------------------------------------";
5.59 +val t = @{term "aaa::real"};
5.60 +if scala_of_term t = "Free(\"aaa\", Type(\"Real.real\", List()))"
5.61 +then () else error "scala_of_term aaa::real";
5.62
5.63 -"----------- fun power -------------------------------------------------------------------------";
5.64 -"----------- fun power -------------------------------------------------------------------------";
5.65 -"----------- fun power -------------------------------------------------------------------------";
5.66 -(*
5.67 -> power 2 3;
5.68 -val it = 8 : int
5.69 -> power ~2 3;
5.70 -val it = ~8 : int
5.71 -> power ~3 2;
5.72 -val it = 9 : int
5.73 -> power 3 ~2;
5.74 -*)
5.75 -"----------- fun divisors ----------------------------------------------------------------------";
5.76 -"----------- fun divisors ----------------------------------------------------------------------";
5.77 -"----------- fun divisors ----------------------------------------------------------------------";
5.78 -(*
5.79 -divisors 30;
5.80 -divisors 32;
5.81 -divisors 60;
5.82 -divisors 11;
5.83 -*)
5.84 -"----------- fun scala_of_term -----------------------------------------------------------------";
5.85 -"----------- fun scala_of_term -----------------------------------------------------------------";
5.86 -"----------- fun scala_of_term -----------------------------------------------------------------";
5.87 -(*TODO*)
5.88 -"----------- fun atom_typ ----------------------------------------------------------------------";
5.89 -"----------- fun atom_typ ----------------------------------------------------------------------";
5.90 -"----------- fun atom_typ ----------------------------------------------------------------------";
5.91 -(*
5.92 -> val T = (type_of o Thm.term_of o the o (parse thy)) "a::[real,int] => nat";
5.93 -> atomtyp T;
5.94 -*** Type (fun,[
5.95 -*** Type (RealDef.real,[])
5.96 -*** Type (fun,[
5.97 -*** Type (IntDef.int,[])
5.98 -*** Type (nat,[])
5.99 -*** ]
5.100 -*** ]
5.101 -*)
5.102 +val t = @{term "aaa + bbb"};
5.103 +if scala_of_term t = "App(App(Const(\"Groups.plus_class.plus\", Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")),Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")),TFree(\"'a\", List(\"Groups.plus\"))))))), Free(\"aaa\", TFree(\"'a\", List(\"Groups.plus\")))), Free(\"bbb\", TFree(\"'a\", List(\"Groups.plus\"))))"
5.104 +then () else error "scala_of_term aaa + bbb";
5.105 +
5.106 "----------- fun contains_Var ------------------------------------------------------------------";
5.107 "----------- fun contains_Var ------------------------------------------------------------------";
5.108 "----------- fun contains_Var ------------------------------------------------------------------";
5.109 -(* contains_Var (str2term "?z = 3") (*true*);
5.110 - contains_Var (str2term "z = 3") (*false*);
5.111 - *)
5.112 +val t = parse_patt @{theory} "?z = 3";
5.113 +if contains_Var t = true then () else error "contains_Var ?z = 3";
5.114 +
5.115 +val t = parse_patt @{theory} "z = 3";
5.116 +if contains_Var t = false then () else error "contains_Var ?z = 3";
5.117 +
5.118 "----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
5.119 "----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
5.120 "----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
5.121 @@ -613,381 +595,135 @@
5.122 NONE => () | _ => raise error "int_of_str_opt #123 changed";
5.123 case int_of_str_opt "-123" of
5.124 SOME ~123 => () | _ => raise error "int_of_str_opt -123 changed";
5.125 -(*>
5.126 -> is_num ((Thm.term_of o the o (parse thy)) "#1");
5.127 -val it = true : bool
5.128 -> is_num ((Thm.term_of o the o (parse thy)) "#-1");
5.129 -val it = true : bool
5.130 -> is_num ((Thm.term_of o the o (parse thy)) "a123");
5.131 -val it = false : bool
5.132 -*)
5.133 +
5.134 +val t = str2term "1";
5.135 +if is_num t = true then () else error "is_num 1";
5.136 +
5.137 +val t = str2term "-1";
5.138 +if is_num t = true then () else error "is_num -1";
5.139 +
5.140 +val t = str2term "a123";
5.141 +if is_num t = false then () else error "is_num a123";
5.142 +
5.143 "----------- fun is_f_x ------------------------------------------------------------------------";
5.144 "----------- fun is_f_x ------------------------------------------------------------------------";
5.145 "----------- fun is_f_x ------------------------------------------------------------------------";
5.146 -(* is_f_x (str2term "q_0/2 * L * x") (*false*);
5.147 - is_f_x (str2term "M_b x") (*true*);
5.148 - *)
5.149 +val t = str2term "q_0/2 * L * x";
5.150 +if is_f_x t = false then () else error "is_f_x q_0/2 * L * x";
5.151 +
5.152 +val t = str2term "M_b x";
5.153 +if is_f_x t = true then () else error "M_b x";
5.154 +
5.155 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
5.156 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
5.157 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
5.158 -(*
5.159 -> val tt = (Thm.term_of o the o (parse thy)) "R=(R::real)";
5.160 -> val TT = type_of tt;
5.161 -> val ss = list2isalist TT [tt,tt,tt];
5.162 -> (Thm.global_cterm_of thy) ss;
5.163 -val it = "[R = R, R = R, R = R]" : cterm
5.164 -*)
5.165 -(*
5.166 -> val il = str2term "[a=b,c=d,e=f]";
5.167 -> val l = isalist2list il;
5.168 -> (tracing o terms2str) l;
5.169 -["a = b","c = d","e = f"]
5.170 +val t = str2term "R=(R::real)";
5.171 +val T = type_of t;
5.172 +val ss = list2isalist T [t,t,t];
5.173 +if term2str ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";
5.174
5.175 -> val il = str2term "ss___::bool list";
5.176 -> val l = isalist2list il;
5.177 -[Free ("ss___", "bool List.list")]
5.178 -*)
5.179 -"----------- fun strip_imp_prems' --------------------------------------------------------------";
5.180 -"----------- fun strip_imp_prems' --------------------------------------------------------------";
5.181 -"----------- fun strip_imp_prems' --------------------------------------------------------------";
5.182 -(*
5.183 - val thm = real_mult_div_cancel2;
5.184 - val prop = (#prop o rep_thm) thm;
5.185 - atomt prop;
5.186 -*** -------------
5.187 -*** Const ( ==>)
5.188 -*** . Const ( Trueprop)
5.189 -*** . . Const ( Not)
5.190 -*** . . . Const ( op =)
5.191 -*** . . . . Var ((k, 0), )
5.192 -*** . . . . Const ( 0)
5.193 -*** . Const ( Trueprop)
5.194 -*** . . Const ( op =) *** .............
5.195 - val SOME t = strip_imp_prems' ((#prop o rep_thm) thm);
5.196 - atomt t;
5.197 -*** -------------
5.198 -*** Const ( ==>)
5.199 -*** . Const ( Trueprop)
5.200 -*** . . Const ( Not)
5.201 -*** . . . Const ( op =)
5.202 -*** . . . . Var ((k, 0), )
5.203 -*** . . . . Const ( 0)
5.204 +val t = str2term "[a=b,c=d,e=f]";
5.205 +val il = isalist2list t;
5.206 +if terms2str il = "[\"a = b\",\"c = d\",\"e = f\"]" then () else error "isalist2list 2";
5.207
5.208 - val thm = real_le_anti_sym;
5.209 - val prop = (#prop o rep_thm) thm;
5.210 - atomt prop;
5.211 -*** -------------
5.212 -*** Const ( ==>)
5.213 -*** . Const ( Trueprop)
5.214 -*** . . Const ( op <=)
5.215 -*** . . . Var ((z, 0), )
5.216 -*** . . . Var ((w, 0), )
5.217 -*** . Const ( ==>)
5.218 -*** . . Const ( Trueprop)
5.219 -*** . . . Const ( op <=)
5.220 -*** . . . . Var ((w, 0), )
5.221 -*** . . . . Var ((z, 0), )
5.222 -*** . . Const ( Trueprop)
5.223 -*** . . . Const ( op =)
5.224 -*** .............
5.225 - val SOME t = strip_imp_prems' ((#prop o rep_thm) thm);
5.226 - atomt t;
5.227 -*** -------------
5.228 -*** Const ( ==>)
5.229 -*** . Const ( Trueprop)
5.230 -*** . . Const ( op <=)
5.231 -*** . . . Var ((z, 0), )
5.232 -*** . . . Var ((w, 0), )
5.233 -*** . Const ( ==>)
5.234 -*** . . Const ( Trueprop)
5.235 -*** . . . Const ( op <=)
5.236 -*** . . . . Var ((w, 0), )
5.237 -*** . . . . Var ((z, 0), )
5.238 -*)
5.239 -"----------- fun ins_concl ---------------------------------------------------------------------";
5.240 -"----------- fun ins_concl ---------------------------------------------------------------------";
5.241 -"----------- fun ins_concl ---------------------------------------------------------------------";
5.242 -(*
5.243 - val thm = real_le_anti_sym;
5.244 - val prop = (#prop o rep_thm) thm;
5.245 - val concl = Logic.strip_imp_concl prop;
5.246 - val SOME prems = strip_imp_prems' prop;
5.247 - val prop' = ins_concl prems concl;
5.248 - prop = prop';
5.249 - atomt prop;
5.250 - atomt prop';
5.251 -*)
5.252 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
5.253 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
5.254 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
5.255 -(*> doubles [2,3,4];
5.256 -val it = [] : int list
5.257 -> doubles [2,3,3,5,5,7];
5.258 -val it = [5,3] : int list*)
5.259 +val t = str2term "[a=b,c=d,e=f]";
5.260 +val il = isalist2list t;
5.261 +if terms2str il = "[\"a = b\",\"c = d\",\"e = f\"]" then () else error "isalist2list 2";
5.262
5.263 -(*> squfact 30;
5.264 -val it = 1 : int
5.265 -> squfact 32;
5.266 -val it = 4 : int
5.267 -> squfact 60;
5.268 -val it = 2 : int
5.269 -> squfact 11;
5.270 -val it = 1 : int*)
5.271 -"----------- fun pairT, fun PairT, fun pairt ---------------------------------------------------";
5.272 -"----------- fun pairT, fun PairT, fun pairt ---------------------------------------------------";
5.273 -"----------- fun pairT, fun PairT, fun pairt ---------------------------------------------------";
5.274 -(*> val t = str2term "(1,2)";
5.275 -> type_of t = pairT HOLogic.realT HOLogic.realT;
5.276 -val it = true : bool
5.277 -*)
5.278 +val t = str2term "ss___s::bool list";
5.279 +(isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>();
5.280
5.281 -(*> val t = str2term "(1,2)";
5.282 -> val Const ("Product_Type.Pair",pT) $ _ $ _ = t;
5.283 -> pT = PairT HOLogic.realT HOLogic.realT;
5.284 -val it = true : bool
5.285 -*)
5.286 +"----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";
5.287 +"----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";
5.288 +"----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";
5.289 +val prop = (#prop o Thm.rep_thm) @{thm real_mult_div_cancel2};
5.290 +term2str prop = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
5.291 +val t as Const ("Pure.imp", _) $
5.292 + (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Const ("Groups.zero_class.zero", _)))) $
5.293 + (Const ("HOL.Trueprop", _) $
5.294 + (Const ("HOL.eq", _) $
5.295 + (Const ("Rings.divide_class.divide", _) $ (Const ("Groups.times_class.times", _) $ Var (("m", 0), _) $ Var (("k", 0), _)) $
5.296 + (Const ("Groups.times_class.times", _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $
5.297 + (Const ("Rings.divide_class.divide", _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop;
5.298 +val SOME t' = strip_imp_prems' t;
5.299 +if term2str t' = "op \<Longrightarrow> (?k \<noteq> 0)" then () else error "strip_imp_prems' changed";
5.300 +
5.301 +val thm = TermC.num_str @{thm frac_sym_conv};
5.302 +val prop = (#prop o Thm.rep_thm) thm;
5.303 +val concl = Logic.strip_imp_concl prop;
5.304 +val SOME prems = strip_imp_prems' prop;
5.305 +val prop' = ins_concl prems concl;
5.306 +if prop = prop' then () else error "ins_concl o strip_imp_concl";
5.307 +
5.308 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
5.309 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
5.310 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
5.311 -(*
5.312 -val T = (type_of o Thm.term_of o the) (parse thy "#12::real");
5.313 +val T = (type_of o Thm.term_of o the) (parse thy "12::real");
5.314 val t = mk_factroot "SqRoot.sqrt" T 2 3;
5.315 -(Thm.global_cterm_of thy) t;
5.316 -val it = "#2 * sqrt #3 " : cterm
5.317 -*)
5.318 -(*
5.319 -> val t = mk_num_op_num "Int" 3 4;
5.320 -> atomty t;
5.321 -> string_of_cterm ((Thm.global_cterm_of thy) t);
5.322 -*)
5.323 -"----------- fun const_in ----------------------------------------------------------------------";
5.324 -"----------- fun const_in ----------------------------------------------------------------------";
5.325 -"----------- fun const_in ----------------------------------------------------------------------";
5.326 -(*
5.327 -> val t = (Thm.term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
5.328 -> const_in "sqrt" t;
5.329 -val it = true : bool
5.330 -> val t = (Thm.term_of o the o (parse thy)) "6 + 5 * 4 + 3";
5.331 -> const_in "sqrt" t;
5.332 -val it = false : bool
5.333 -*)
5.334 +if term2str t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
5.335 +
5.336 +val t = str2term "aaa + bbb";
5.337 +val op_ as Const ("Groups.plus_class.plus", Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;
5.338 +val t' = mk_num_op_num T1 T2 ("Groups.plus_class.plus", Top) 2 3;
5.339 +if term2str t' = "2 + 3" then () else error "mk_num_op_num";
5.340 +
5.341 "----------- fun dest_binop_typ ----------------------------------------------------------------";
5.342 "----------- fun dest_binop_typ ----------------------------------------------------------------";
5.343 "----------- fun dest_binop_typ ----------------------------------------------------------------";
5.344 -(* -----
5.345 -> val t = (Thm.term_of o the o (parse thy)) "#3^#4";
5.346 -> val hT = type_of (head_of t);
5.347 -> dest_binop_typ hT;
5.348 -val it = ("'a","nat","'a") : typ * typ * typ
5.349 - ----- *)
5.350 +val t = (Thm.term_of o the o (parse thy)) "3 ^ 4";
5.351 +val hT = type_of (head_of t);
5.352 +if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = dest_binop_typ hT
5.353 +then () else error "dest_binop_typ";
5.354 +
5.355 "----------- fun is_list -----------------------------------------------------------------------";
5.356 "----------- fun is_list -----------------------------------------------------------------------";
5.357 "----------- fun is_list -----------------------------------------------------------------------";
5.358 -(* val (SOME ct) = parse thy "lll::real list";
5.359 -> val ty = (#t o rep_cterm) ct;
5.360 -> is_list ty;
5.361 -val it = false : bool
5.362 -> val (SOME ct) = parse thy "[lll]";
5.363 -> val ty = (#t o rep_cterm) ct;
5.364 -> is_list ty;
5.365 -val it = true : bool *)
5.366 +val (SOME ct) = parse thy "lll::real list";
5.367 +val t = str2term "lll::real list";
5.368 +val ty = (Term.type_of o Thm.term_of) ct;
5.369 +if is_list t = false then () else error "is_list lll::real list";
5.370 +
5.371 +val t = str2term "[a, b, c]";
5.372 +val ty = (Term.type_of o Thm.term_of) ct;
5.373 +if is_list t = true then () else error "is_list [a, b, c]";
5.374 +
5.375 "----------- fun inst_abs ----------------------------------------------------------------------";
5.376 "----------- fun inst_abs ----------------------------------------------------------------------";
5.377 "----------- fun inst_abs ----------------------------------------------------------------------";
5.378 -(*val scr =
5.379 - "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
5.380 - \ (let h_ = (hd o (filterVar f_)) eqs_; \
5.381 - \ e_1 = hd (dropWhile (ident h_) eqs_); \
5.382 - \ vs_ = dropWhile (ident f_) (Vars h_); \
5.383 - \ v_1 = hd (dropWhile (ident v_) vs_); \
5.384 - \ (s_1::bool list)=(SubProblem(DiffApp_,[univar,equation],[no_met])\
5.385 - \ [BOOL e_1, REAL v_1])\
5.386 - \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
5.387 -> val ttt = (Thm.term_of o the o (parse thy)) scr;
5.388 -> tracing(term2str ttt);
5.389 -> atomt ttt;
5.390 -*** -------------
5.391 -*** Const ( DiffApp.Make'_fun'_by'_explicit)
5.392 -*** . Free ( f_, )
5.393 -*** . Free ( v_, )
5.394 -*** . Free ( eqs_, )
5.395 -*** . Const ( Let)
5.396 -*** . . Const ( Fun.op o)
5.397 -*** . . . Const ( List.hd)
5.398 -*** . . . Const ( DiffApp.filterVar)
5.399 -*** . . . . Free ( f_, )
5.400 -*** . . . Free ( eqs_, )
5.401 -*** . . Abs( h_,..
5.402 -*** . . . Const ( Let)
5.403 -*** . . . . Const ( List.hd)
5.404 -*** . . . . . Const ( List.dropWhile)
5.405 -*** . . . . . . Const ( Atools.ident)
5.406 -*** . . . . . . . Bound 0 <---- Free ( h_, )
5.407 -*** . . . . . . Free ( eqs_, )
5.408 -*** . . . . Abs( e_1,..
5.409 -*** . . . . . Const ( Let)
5.410 -*** . . . . . . Const ( List.dropWhile)
5.411 -*** . . . . . . . Const ( Atools.ident)
5.412 -*** . . . . . . . . Free ( f_, )
5.413 -*** . . . . . . . Const ( Tools.Vars)
5.414 -*** . . . . . . . . Bound 1 <---- Free ( h_, )
5.415 -*** . . . . . . Abs( vs_,..
5.416 -*** . . . . . . . Const ( Let)
5.417 -*** . . . . . . . . Const ( List.hd)
5.418 -*** . . . . . . . . . Const ( List.dropWhile)
5.419 -*** . . . . . . . . . . Const ( Atools.ident)
5.420 -*** . . . . . . . . . . . Free ( v_, )
5.421 -*** . . . . . . . . . . Bound 0 <---- Free ( vs_, )
5.422 -*** . . . . . . . . Abs( v_1,..
5.423 -*** . . . . . . . . . Const ( Let)
5.424 -*** . . . . . . . . . . Const ( Script.SubProblem)
5.425 -*** . . . . . . . . . . . Const ( Pair)
5.426 -*** . . . . . . . . . . . . Free ( DiffApp_, )
5.427 -*** . . . . . . . . . . . . Const ( Pair)
5.428 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.429 -*** . . . . . . . . . . . . . . Free ( univar, )
5.430 -*** . . . . . . . . . . . . . . Const ( List.list.Cons)
5.431 -*** . . . . . . . . . . . . . . . Free ( equation, )
5.432 -*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
5.433 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.434 -*** . . . . . . . . . . . . . . Free ( no_met, )
5.435 -*** . . . . . . . . . . . . . . Const ( List.list.Nil)
5.436 -*** . . . . . . . . . . . Const ( List.list.Cons)
5.437 -*** . . . . . . . . . . . . Const ( Script.BOOL)
5.438 -*** . . . . . . . . . . . . . Bound 2 <----- Free ( e_1, )
5.439 -*** . . . . . . . . . . . . Const ( List.list.Cons)
5.440 -*** . . . . . . . . . . . . . Const ( Script.real_)
5.441 -*** . . . . . . . . . . . . . . Bound 0 <----- Free ( v_1, )
5.442 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.443 -*** . . . . . . . . . . Abs( s_1,..
5.444 -*** . . . . . . . . . . . Const ( Script.Substitute)
5.445 -*** . . . . . . . . . . . . Const ( List.list.Cons)
5.446 -*** . . . . . . . . . . . . . Const ( Pair)
5.447 -*** . . . . . . . . . . . . . . Bound 1 <----- Free ( v_1, )
5.448 -*** . . . . . . . . . . . . . . Const ( Fun.op o)
5.449 -*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
5.450 -*** . . . . . . . . . . . . . . . Const ( List.hd)
5.451 -*** . . . . . . . . . . . . . . . Bound 0 <----- Free ( s_1, )
5.452 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.453 -*** . . . . . . . . . . . . Bound 4 <----- Free ( h_, )
5.454 +(* cp from Biegelinie.thy*)
5.455 +val scr = str2term
5.456 + ("Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
5.457 + " (let fu_n = Take fu_n; " ^
5.458 + " bd_v = argument_in (lhs fu_n); " ^
5.459 + " va_l = argument_in (lhs su_b); " ^
5.460 + " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
5.461 + " eq_u = (Substitute [su_b]) eq_u " ^
5.462 + " in (Rewrite_Set norm_Rational False) eq_u) ")
5.463 +val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $
5.464 + (Const ("HOL.Let", _) $ (Const ("Script.Take", _) $ Free ("fu_n", _)) $
5.465 + Abs ("fu_n", _, (* <-- ID taken from here ------------------------------*)
5.466 + Const ("HOL.Let", _) $
5.467 + (Const ("Atools.argument'_in", _) $ (Const ("Tools.lhs", _) $
5.468 + Bound 0)) $ (* difference --vvv ------------------------------------*)
5.469 + Abs _)) = scr;
5.470
5.471 -> val ttt' = inst_abs thy ttt;
5.472 -> tracing(term2str ttt');
5.473 -Script Make_fun_by_explicit f_ v_ eqs_ =
5.474 - ... as above ...
5.475 -> atomt ttt';
5.476 -*** -------------
5.477 -*** Const ( DiffApp.Make'_fun'_by'_explicit)
5.478 -*** . Free ( f_, )
5.479 -*** . Free ( v_, )
5.480 -*** . Free ( eqs_, )
5.481 -*** . Const ( Let)
5.482 -*** . . Const ( Fun.op o)
5.483 -*** . . . Const ( List.hd)
5.484 -*** . . . Const ( DiffApp.filterVar)
5.485 -*** . . . . Free ( f_, )
5.486 -*** . . . Free ( eqs_, )
5.487 -*** . . Abs( h_,..
5.488 -*** . . . Const ( Let)
5.489 -*** . . . . Const ( List.hd)
5.490 -*** . . . . . Const ( List.dropWhile)
5.491 -*** . . . . . . Const ( Atools.ident)
5.492 -*** . . . . . . . Free ( h_, ) <---- Bound 0
5.493 -*** . . . . . . Free ( eqs_, )
5.494 -*** . . . . Abs( e_1,..
5.495 -*** . . . . . Const ( Let)
5.496 -*** . . . . . . Const ( List.dropWhile)
5.497 -*** . . . . . . . Const ( Atools.ident)
5.498 -*** . . . . . . . . Free ( f_, )
5.499 -*** . . . . . . . Const ( Tools.Vars)
5.500 -*** . . . . . . . . Free ( h_, ) <---- Bound 1
5.501 -*** . . . . . . Abs( vs_,..
5.502 -*** . . . . . . . Const ( Let)
5.503 -*** . . . . . . . . Const ( List.hd)
5.504 -*** . . . . . . . . . Const ( List.dropWhile)
5.505 -*** . . . . . . . . . . Const ( Atools.ident)
5.506 -*** . . . . . . . . . . . Free ( v_, )
5.507 -*** . . . . . . . . . . Free ( vs_, ) <---- Bound 0
5.508 -*** . . . . . . . . Abs( v_1,..
5.509 -*** . . . . . . . . . Const ( Let)
5.510 -*** . . . . . . . . . . Const ( Script.SubProblem)
5.511 -*** . . . . . . . . . . . Const ( Pair)
5.512 -*** . . . . . . . . . . . . Free ( DiffApp_, )
5.513 -*** . . . . . . . . . . . . Const ( Pair)
5.514 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.515 -*** . . . . . . . . . . . . . . Free ( univar, )
5.516 -*** . . . . . . . . . . . . . . Const ( List.list.Cons)
5.517 -*** . . . . . . . . . . . . . . . Free ( equation, )
5.518 -*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
5.519 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.520 -*** . . . . . . . . . . . . . . Free ( no_met, )
5.521 -*** . . . . . . . . . . . . . . Const ( List.list.Nil)
5.522 -*** . . . . . . . . . . . Const ( List.list.Cons)
5.523 -*** . . . . . . . . . . . . Const ( Script.BOOL)
5.524 -*** . . . . . . . . . . . . . Free ( e_1, ) <----- Bound 2
5.525 -*** . . . . . . . . . . . . Const ( List.list.Cons)
5.526 -*** . . . . . . . . . . . . . Const ( Script.real_)
5.527 -*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 0
5.528 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.529 -*** . . . . . . . . . . Abs( s_1,..
5.530 -*** . . . . . . . . . . . Const ( Script.Substitute)
5.531 -*** . . . . . . . . . . . . Const ( List.list.Cons)
5.532 -*** . . . . . . . . . . . . . Const ( Pair)
5.533 -*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 1
5.534 -*** . . . . . . . . . . . . . . Const ( Fun.op o)
5.535 -*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
5.536 -*** . . . . . . . . . . . . . . . Const ( List.hd)
5.537 -*** . . . . . . . . . . . . . . . Free ( s_1, ) <----- Bound 0
5.538 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.539 -*** . . . . . . . . . . . . Free ( h_, ) <----- Bound 4
5.540 +val scr' = inst_abs scr;
5.541 +val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $
5.542 + (Const ("HOL.Let", _) $ (Const ("Script.Take", _) $ Free ("fu_n", _)) $
5.543 + Abs ("fu_n", _,
5.544 + Const ("HOL.Let", _) $
5.545 + (Const ("Atools.argument'_in", _) $ (Const ("Tools.lhs", _) $
5.546 + Free ("fu_n", _))) $ (* difference --^^^ -----------------------------------*)
5.547 + Abs _)) = scr';
5.548 +if term2str scr' = (* see the ugly IDs ...*)
5.549 + ("Script Function2Equality fu_n su_b =\n " ^
5.550 + "let fu_na = Take fu_n; " ^
5.551 + "bd_va = argument_in lhs fu_n;\n " ^
5.552 + "va_la = argument_in lhs su_b; " ^
5.553 + "eq_ua = Substitute [bd_v = va_l] fu_n;\n " ^
5.554 + "eq_ua = Substitute [su_b] eq_u\n " ^
5.555 + "in (Rewrite_Set norm_Rational False) eq_u")
5.556 + then () else error "inst_abs changed";
5.557
5.558 -Note numbering of de Bruijn indexes !
5.559 -
5.560 -Script Make_fun_by_explicit f_ v_ eqs_ =
5.561 - let h_ = (hd o filterVar f_) eqs_;
5.562 - e_1 = hd (dropWhile (ident h_ BOUND_0) eqs_);
5.563 - vs_ = dropWhile (ident f_) (Vars h_ BOUND_1);
5.564 - v_1 = hd (dropWhile (ident v_) vs_ BOUND_0);
5.565 - s_1 =
5.566 - SubProblem (DiffApp_, [univar, equation], [no_met])
5.567 - [BOOL e_1 BOUND_2, REAL v_1 BOUND_0]
5.568 - in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4
5.569 -*)
5.570 -"----------- fun is_atom -----------------------------------------------------------------------";
5.571 -"----------- fun is_atom -----------------------------------------------------------------------";
5.572 -"----------- fun is_atom -----------------------------------------------------------------------";
5.573 -(* val t = str2term "q_0/2 * L * x";
5.574 -
5.575 -
5.576 -*)
5.577 -(*val t = str2term "Float ((1,2),(0,0))";
5.578 -> is_atom t;
5.579 -val it = true : bool
5.580 -> val t = str2term "Float ((1,2),(0,0)) * I__";
5.581 -> is_atom t;
5.582 -val it = true : bool
5.583 -> val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
5.584 -> is_atom t;
5.585 -val it = true : bool
5.586 -> val t = str2term "1 + 2*I__";
5.587 -> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
5.588 -*)
5.589 -
5.590 -
5.591 -
5.592 -
5.593 -
5.594 -
5.595 -
5.596 -
5.597 -
5.598 -
5.599 -
5.600 -
5.601 -
5.602 -
5.603 -
5.604 -
5.605 -
5.606 -
5.607 -
5.608 +val {scr = Prog original, ...} = get_met ["Equation","fromFunction"];
5.609 +if scr' = original then () else error "inst_abs changed";
6.1 --- a/test/Tools/isac/Test_Isac.thy Tue Mar 13 10:46:34 2018 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Mar 13 14:41:02 2018 +0100
6.3 @@ -179,78 +179,6 @@
6.4 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
6.5 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
6.6 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
6.7 -ML {*
6.8 -"----------- fun autoCalculate -----------------------------------";
6.9 -reset_states ();
6.10 -CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
6.11 - [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
6.12 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
6.13 -Iterator 1;
6.14 -moveActiveRoot 1;
6.15 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
6.16 -modeling is skipped FIXME
6.17 -see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
6.18 - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
6.19 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
6.20 -
6.21 - fetchProposedTactic 1;
6.22 - setNextTactic 1 (Add_Given "solveFor x");
6.23 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.24 -
6.25 - fetchProposedTactic 1;
6.26 - setNextTactic 1 (Add_Find "solutions L");
6.27 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.28 -
6.29 - fetchProposedTactic 1;
6.30 - setNextTactic 1 (Specify_Theory "Test");
6.31 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.32 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
6.33 -autoCalculate 1 (Step 1);
6.34 -"----- step 1 ---";
6.35 -autoCalculate 1 (Step 1);
6.36 -"----- step 2 ---";
6.37 -autoCalculate 1 (Step 1);
6.38 -"----- step 3 ---";
6.39 -autoCalculate 1 (Step 1);
6.40 -*} ML {*
6.41 -"----- step 4 ---";
6.42 -autoCalculate 1 (Step 1);
6.43 -val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
6.44 -*} ML {*
6.45 -term2str t = "c + x + 1 / (2 + 1) * x ^^^ (2 + 1)";
6.46 -*} ML {*
6.47 -"----- step 5 ---";
6.48 -autoCalculate 1 (Step 1);
6.49 -val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
6.50 -*} ML {*
6.51 -term2str t;
6.52 -*} ML {*
6.53 -"----- step 6 ---";
6.54 -autoCalculate 1 (Step 1);
6.55 -val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
6.56 -*} ML {*
6.57 -term2str t;
6.58 -*} ML {*
6.59 -"----- step 7 ---";
6.60 -autoCalculate 1 (Step 1);
6.61 -val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
6.62 -*} ML {*
6.63 -term2str t;
6.64 -*} ML {*
6.65 -"----- step 8 ---";
6.66 -autoCalculate 1 (Step 1);
6.67 -val (ptp as (_, p), _) = get_calc 1;
6.68 -val (Form t,_,_) = pt_extract ptp;
6.69 -
6.70 -*} ML {*
6.71 -*} ML {*
6.72 -term2str t = "c + x + 1 / (2 + 1) * x ^^^ (2 + 1)"
6.73 -*} ML {*
6.74 -if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
6.75 -else error "mathengine.sml -- fun autoCalculate -- end";
6.76 -*} ML {*
6.77 -*} ML {*
6.78 -*}
6.79 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
6.80 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
6.81 ML_file "xmlsrc/mathml.sml" (*part.*)