1.1 --- a/src/Tools/isac/BaseDefinitions/KEStore.thy Tue Apr 14 12:39:26 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/KEStore.thy Tue Apr 14 15:56:15 2020 +0200
1.3 @@ -17,7 +17,7 @@
1.4 ML_file theoryC.sml (*rename identifiers by use of struct.id*)
1.5 ML_file unparseC.sml
1.6 ML_file "rule-def.sml"
1.7 -ML_file "thmC-def.sml" (*rename identifiers by use of struct.id*)
1.8 +ML_file "thmC-def.sml"
1.9 ML_file "exec-def.sml" (*rename identifiers by use of struct.id*)
1.10 ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
1.11 ML_file rule.sml
2.1 --- a/src/Tools/isac/BaseDefinitions/error-fill-def.sml Tue Apr 14 12:39:26 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/error-fill-def.sml Tue Apr 14 15:56:15 2020 +0200
2.3 @@ -33,7 +33,7 @@
2.4 do not match (which reflects student's error).
2.5 fillpatterns are stored with these thms. *)
2.6 fun errpat2str (id, tms, thms) =
2.7 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.thms2str thms
2.8 + "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
2.9 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
2.10
2.11 (* for (at least) 2 kinds of access:
3.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Tue Apr 14 12:39:26 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Tue Apr 14 15:56:15 2020 +0200
3.3 @@ -52,7 +52,7 @@
3.4 | equal _ = false;
3.5
3.6 fun to_string Rule_Def.Erule = "Erule"
3.7 - | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")"
3.8 + | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thm thm ^ ")"
3.9 | to_string (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
3.10 | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
3.11 | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
4.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue Apr 14 12:39:26 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Apr 14 15:56:15 2020 +0200
4.3 @@ -28,9 +28,9 @@
4.4
4.5 val term_of_num: typ -> int -> term
4.6 val num_of_term: term -> int
4.7 - val int_of_str_opt: string -> int option
4.8 val int_of_str: string -> int
4.9 val isastr_of_int: int -> string
4.10 + val int_opt_of_string: string -> int option (* belongs to TermC *)
4.11
4.12 val isalist2list: term -> term list
4.13 val list2isalist: typ -> term list -> term
4.14 @@ -235,13 +235,13 @@
4.15 else string_of_int n;
4.16 val int_of_str = Value.parse_int;
4.17
4.18 -val int_of_str_opt = ThmC_Def.int_of_str_opt
4.19 +val int_opt_of_string = ThmC_Def.int_opt_of_string
4.20
4.21 -fun is_num' str = case int_of_str_opt str of SOME _ => true | NONE => false;
4.22 +fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
4.23 fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false;
4.24 fun term_of_num ntyp n = Free (str_of_int n, ntyp);
4.25 fun num_of_term (t as (Free (istr, _))) =
4.26 - (case int_of_str_opt istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
4.27 + (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
4.28 | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
4.29
4.30 fun is_const (Const _) = true | is_const _ = false;
4.31 @@ -437,7 +437,7 @@
4.32 end;
4.33
4.34 (** transform binary numeralsstrings **)
4.35 -val numbers_to_string = ThmC_Def.numbers_to_string
4.36 +val numbers_to_string = ThmC_Def.num_to_Free
4.37 val uminus_to_string = ThmC_Def.uminus_to_string
4.38
4.39 fun mk_Free (s,T) = Free (s, T);
4.40 @@ -507,11 +507,11 @@
4.41 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
4.42 WN130613 probably compare to
4.43 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
4.44 -fun parse_patt thy str =
4.45 - (thy, str) |>> ThyC.thy2ctxt
4.46 - |-> Proof_Context.read_term_pattern
4.47 - |> numbers_to_string (*TODO drop*)
4.48 - |> typ_a2real; (*TODO drop*)
4.49 +fun parse_patt thy str = (thy, str)
4.50 + |>> ThyC.thy2ctxt
4.51 + |-> Proof_Context.read_term_pattern
4.52 + |> numbers_to_string (*TODO drop*)
4.53 + |> typ_a2real; (*TODO drop*)
4.54 fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str
4.55
4.56 (* TODO decide with Test_Isac *)
5.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Tue Apr 14 12:39:26 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Tue Apr 14 15:56:15 2020 +0200
5.3 @@ -9,16 +9,16 @@
5.4 type T
5.5 eqtype id
5.6
5.7 - val string_of_thmI: thm -> string
5.8 - val thms2str : thm list -> string
5.9 + val make_thm: theory -> term -> thm (* required for Calculate.thy *)
5.10
5.11 -(* required for ProgLang/ListC BEFORE definition in ------vvv *)
5.12 - val int_of_str_opt: string -> int option (* belongs to TermC *)
5.13 - val numerals_to_Free: thm -> thm (* belongs to ThmC *)
5.14 - val numbers_to_string: term -> term (* belongs to TermC *)
5.15 - val uminus_to_string: term -> term (* belongs to TermC *)
5.16 + val string_of_thm: thm -> string
5.17 + val string_of_thms: thm list -> string
5.18
5.19 - val make_thm: theory -> term -> thm
5.20 +(* required in ProgLang BEFORE definition in ---------------vvv *)
5.21 + val int_opt_of_string: string -> int option (* belongs to TermC *)
5.22 + val numerals_to_Free: thm -> thm (* belongs to ThmC *)
5.23 + val num_to_Free: term -> term (* belongs to TermC *)
5.24 + val uminus_to_string: term -> term (* belongs to TermC *)
5.25
5.26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.27 (*NONE*)
5.28 @@ -35,28 +35,17 @@
5.29 type id = string; (* key into KEStore, without point *)
5.30 type T = id * Thm.thm;
5.31
5.32 +fun make_thm thy t = Thm.make_thm (Thm.global_cterm_of thy t);
5.33
5.34 -fun string_of_thm thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
5.35 -(*check for [.] as caused by "fun assoc_thm'"*)
5.36 -fun string_of_thmI thm =
5.37 - let
5.38 - val str = (de_quote o string_of_thm) thm
5.39 - val (a, b) = split_nlast (5, Symbol.explode str)
5.40 - in
5.41 - case b of
5.42 - [" ", " ","[", ".", "]"] => implode a
5.43 - | _ => str
5.44 - end
5.45 -
5.46 -fun thm2str thm =
5.47 +fun string_of_thm thm =
5.48 let
5.49 val t = Thm.prop_of thm
5.50 val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
5.51 val ctxt' = Config.put show_markup false ctxt
5.52 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
5.53 -fun thms2str thms = (strs2str o (map thm2str)) thms
5.54 +fun string_of_thms thms = (strs2str o (map string_of_thm)) thms
5.55
5.56 -fun int_of_str_opt str =
5.57 +fun int_opt_of_string str =
5.58 let
5.59 val ss = Symbol.explode str
5.60 val ss' = case ss of "(" :: s => drop_last s | _ => ss
5.61 @@ -68,7 +57,7 @@
5.62
5.63 (** transform Isabelle's binary numerals to "Free (string, T)" **)
5.64
5.65 -val numbers_to_string = (* Makarius 100308 *)
5.66 +val num_to_Free = (* Makarius 100308 *)
5.67 let
5.68 fun dest_num t =
5.69 (case try HOLogic.dest_number t of
5.70 @@ -79,12 +68,13 @@
5.71 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
5.72 | to_str t = perhaps dest_num t;
5.73 in to_str end
5.74 +
5.75 val uminus_to_string =
5.76 let
5.77 fun dest_num t =
5.78 case t of
5.79 (Const ("Groups.uminus_class.uminus", _) $ Free (s, T)) =>
5.80 - (case int_of_str_opt s of
5.81 + (case int_opt_of_string s of
5.82 SOME i => SOME (Free (signed_string_of_int (~1 * i), T))
5.83 | NONE => NONE)
5.84 | _ => NONE;
5.85 @@ -93,14 +83,13 @@
5.86 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
5.87 | to_str t = perhaps dest_num t;
5.88 in to_str end;
5.89 +
5.90 fun numerals_to_Free thm =
5.91 let
5.92 val (deriv,
5.93 {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps,
5.94 hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm
5.95 - val prop' = numbers_to_string prop;
5.96 + val prop' = num_to_Free prop;
5.97 in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end;
5.98
5.99 -fun make_thm thy t = Thm.make_thm (Thm.global_cterm_of thy t);
5.100 -
5.101 (**)end(**)
6.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 14 12:39:26 2020 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 14 15:56:15 2020 +0200
6.3 @@ -307,7 +307,7 @@
6.4 XML.Elem (("INTLIST", []), map xml_of_int is)
6.5
6.6 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
6.7 - (case TermC.int_of_str_opt i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
6.8 + (case TermC.int_opt_of_string i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
6.9 | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
6.10 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
6.11 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
6.12 @@ -330,7 +330,7 @@
6.13 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
6.14 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
6.15 fun xml_to_auto (XML.Elem (("AUTO", []), [
6.16 - XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Steps (TermC.int_of_str_opt i |> the)
6.17 + XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Steps (TermC.int_opt_of_string i |> the)
6.18 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel
6.19 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = Solve.CompleteCalcHead
6.20 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = Solve.CompleteToSubpbl
7.1 --- a/src/Tools/isac/Build_Isac.thy Tue Apr 14 12:39:26 2020 +0200
7.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Apr 14 15:56:15 2020 +0200
7.3 @@ -16,9 +16,9 @@
7.4 (* theory KEStore imports Complex_Main
7.5 ML_file libraryC.sml
7.6 ML_file theoryC.sml
7.7 - ML_file unparseC.sml
7.8 + ML_file unparseC.sml
7.9 ML_file "rule-def.sml"
7.10 - ML_file thmC.sml
7.11 + ML_file "thmC-def.sml"
7.12 ML_file "exec-def.sml"
7.13 ML_file "rewrite-order.sml"
7.14 ML_file rule.sml
7.15 @@ -45,6 +45,7 @@
7.16 (*
7.17 theory MathEngBasic imports
7.18 "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
7.19 + ML_file thmC.sml
7.20 ML_file rewrite.sml
7.21 ML_file "calc-tree-elem.sml"
7.22 ML_file model.sml
8.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Tue Apr 14 12:39:26 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Tue Apr 14 15:56:15 2020 +0200
8.3 @@ -228,7 +228,7 @@
8.4 do not match (which reflects student's error).
8.5 fillpatterns are stored with these thms. *)
8.6 fun errpat2str (id, tms, thms) =
8.7 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.thms2str thms
8.8 + "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC.string_of_thms thms
8.9 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
8.10
8.11 (**)end(**)
8.12 \ No newline at end of file
9.1 --- a/src/Tools/isac/Isac_Protocol.thy Tue Apr 14 12:39:26 2020 +0200
9.2 +++ b/src/Tools/isac/Isac_Protocol.thy Tue Apr 14 15:56:15 2020 +0200
9.3 @@ -25,7 +25,7 @@
9.4 XML.Elem (("AUTOCALC", []), [
9.5 XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
9.6 | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
9.7 - val SOME calcid = TermC.int_of_str_opt ci
9.8 + val SOME calcid = TermC.int_opt_of_string ci
9.9 val auto = xml_to_auto a
9.10 val result = Kernel.autoCalculate calcid auto
9.11 in result end)
9.12 @@ -518,7 +518,7 @@
9.13 XML.Elem (("CALCID", []), [XML.Text ci]), p])
9.14 => (ci, p)
9.15 | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
9.16 - val SOME calcid = TermC.int_of_str_opt ci
9.17 + val SOME calcid = TermC.int_opt_of_string ci
9.18 val pos = xml_to_pos p
9.19 val result = Kernel.refFormula calcid pos
9.20 in result end)
10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Apr 14 12:39:26 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Apr 14 15:56:15 2020 +0200
10.3 @@ -52,12 +52,12 @@
10.4 let fun selc var =
10.5 case (Symbol.explode o id_of) var of
10.6 "c"::[] => true
10.7 - | "c"::"_"::is => (case (TermC.int_of_str_opt o implode) is of
10.8 + | "c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
10.9 SOME _ => true
10.10 | NONE => false)
10.11 | _ => false;
10.12 fun get_coeff c = case (Symbol.explode o id_of) c of
10.13 - "c"::"_"::is => (the o TermC.int_of_str_opt o implode) is
10.14 + "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
10.15 | _ => 0;
10.16 val cs = filter selc (TermC.vars term);
10.17 in
11.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Apr 14 12:39:26 2020 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Apr 14 15:56:15 2020 +0200
11.3 @@ -332,7 +332,7 @@
11.4 (case x of
11.5 (Const ("Prog_Expr.pow", _) $ Free _ $ Free (str_h, T)) =>
11.6 if (is_nums (Free (str_h, T))) then
11.7 - counter (n + (the (TermC.int_of_str_opt str_h)), xs)
11.8 + counter (n + (the (TermC.int_opt_of_string str_h)), xs)
11.9 else counter (n + 1000, xs) (*FIXME.MG?!*)
11.10 | (Const ("Prog_Expr.pow", _) $ Free _ $ _ ) =>
11.11 counter (n + 1000, xs) (*FIXME.MG?!*)
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Apr 14 12:39:26 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Apr 14 15:56:15 2020 +0200
12.3 @@ -1171,7 +1171,7 @@
12.4 fun size_of_term' x (Const ("Prog_Expr.pow",_) $ Free (var,_) $ Free (pot,_)) =
12.5 (case x of (*WN*)
12.6 (Free (xstr,_)) =>
12.7 - (if xstr = var then 1000*(the (TermC.int_of_str_opt pot)) else 3)
12.8 + (if xstr = var then 1000*(the (TermC.int_opt_of_string pot)) else 3)
12.9 | _ => error ("size_of_term' called with subst = "^
12.10 (UnparseC.term x)))
12.11 | size_of_term' x (Free (subst,_)) =
13.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Apr 14 12:39:26 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Tue Apr 14 15:56:15 2020 +0200
13.3 @@ -209,7 +209,7 @@
13.4 rls put_asm thm' ct;
13.5 val _ = if pairopt <> NONE then ()
13.6 else error("rewrite_set_, rewrite_ \""^
13.7 - (ThmC_Def.string_of_thmI thm')^"\" \""^
13.8 + (ThmC.string_of_thm thm')^"\" \""^
13.9 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
13.10 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
13.11 val ruls = (#rules o Rule_Set.rep) ruless;
13.12 @@ -245,7 +245,7 @@
13.13 rls put_asm thm' ct;
13.14 val _ = if pairopt <> NONE then ()
13.15 else error("rewrite_set_, rewrite_ \""^
13.16 - (ThmC_Def.string_of_thmI thm')^"\" \""^
13.17 + (ThmC.string_of_thm thm')^"\" \""^
13.18 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
13.19 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
13.20 val ruls = (#rules o Rule_Set.rep) ruless;
14.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Apr 14 12:39:26 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Apr 14 15:56:15 2020 +0200
14.3 @@ -125,10 +125,10 @@
14.4 (c, list_update es (find_index (curry op = t) vs) 1)
14.5 | monom_of_term vs (c, es) (t as Free (id, _)) =
14.6 if TermC.is_num' id
14.7 - then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*)
14.8 + then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
14.9 else (c, list_update es (find_index (curry op = t) vs) 1)
14.10 | monom_of_term vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =
14.11 - (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_of_str_opt e)))
14.12 + (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
14.13 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
14.14 let val (c', es') = monom_of_term vs (c, es) m1
14.15 in monom_of_term vs (c', es') m2 end
15.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Apr 14 12:39:26 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Apr 14 15:56:15 2020 +0200
15.3 @@ -50,7 +50,7 @@
15.4 (Const(op0,t0) $ arg)) thy =
15.5 (case arg of
15.6 Free (n1,t1) =>
15.7 - (case TermC.int_of_str_opt n1 of
15.8 + (case TermC.int_opt_of_string n1 of
15.9 SOME ni =>
15.10 if ni < 0 then NONE
15.11 else
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Apr 14 12:39:26 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Apr 14 15:56:15 2020 +0200
16.3 @@ -303,7 +303,7 @@
16.4 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
16.5 (* RL *)
16.6 fun get_order_pow (t $ (Free(order,_))) =
16.7 - (case TermC.int_of_str_opt (order) of
16.8 + (case TermC.int_opt_of_string order of
16.9 SOME d => d
16.10 | NONE => 0)
16.11 | get_order_pow _ = 0;
17.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 12:39:26 2020 +0200
17.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 15:56:15 2020 +0200
17.3 @@ -155,7 +155,7 @@
17.4 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
17.5 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
17.6 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
17.7 - ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
17.8 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
17.9 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
17.10 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
17.11 end
17.12 @@ -169,7 +169,7 @@
17.13 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
17.14 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
17.15 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
17.16 - ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
17.17 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
17.18 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
17.19 in the pairopt end
17.20 end
18.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Tue Apr 14 12:39:26 2020 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Tue Apr 14 15:56:15 2020 +0200
18.3 @@ -8,10 +8,10 @@
18.4 sig
18.5 type T = ThmC_Def.T
18.6 type id = ThmC_Def.id;
18.7 +
18.8 val numerals_to_Free: thm -> thm
18.9
18.10 val id_of_thm: Rule_Def.rule -> string
18.11 - val string_of_thmI: thm -> string
18.12 val thmID_of_derivation_name: string -> string
18.13 val thmID_of_derivation_name': thm -> string
18.14 val thm''_of_thm: thm -> T
18.15 @@ -31,6 +31,7 @@
18.16 val thms2str : thm list -> string
18.17 val string_of_thm': theory -> thm -> string
18.18 val string_of_thm: thm -> string
18.19 + val string_of_thms: thm list -> string
18.20 (** )
18.21 val mk_thm: theory -> string -> thm
18.22 ( **)
18.23 @@ -48,6 +49,9 @@
18.24 type id = ThmC_Def.id;
18.25 type thm' = id * TermC.as_string;
18.26
18.27 +val string_of_thm = ThmC_Def.string_of_thm
18.28 +val string_of_thms = ThmC_Def.string_of_thms
18.29 +
18.30 val numerals_to_Free = ThmC_Def.numerals_to_Free
18.31
18.32
18.33 @@ -60,9 +64,7 @@
18.34 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
18.35 fun thms2str thms = (strs2str o (map thm2str)) thms
18.36
18.37 -fun string_of_thm thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
18.38 fun string_of_thm' thy thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt thy) (Thm.prop_of thm)
18.39 -val string_of_thmI = ThmC_Def.string_of_thmI
18.40
18.41 fun id_of_thm (Rule_Def.Thm (id, _)) = id
18.42 | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ to_string r *))
18.43 @@ -91,7 +93,7 @@
18.44
18.45 (* get the theorem associated with the xstring-identifier;
18.46 if the identifier starts with "sym_" then swap lhs = rhs around =
18.47 - (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
18.48 + (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC.string_of_thm);
18.49 identifiers starting with "#" come from Num_Calc and
18.50 get a hand-made theorem (containing numerals only) *)
18.51 fun assoc_thm'' thy thmid =
18.52 @@ -141,7 +143,7 @@
18.53 val thm' = sym_thm thm
18.54 val thmID' = case Symbol.explode thmID of
18.55 "s" :: "y" :: "m" :: "_" :: id => implode id
18.56 - | "#" :: ":" :: _ => "#: " ^ ThmC_Def.string_of_thmI thm'
18.57 + | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'
18.58 | _ => "sym_" ^ thmID
18.59 in Rule.Thm (thmID', thm') end
18.60 | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
19.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Apr 14 12:39:26 2020 +0200
19.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Apr 14 15:56:15 2020 +0200
19.3 @@ -300,7 +300,7 @@
19.4 (t as (Const _ $ arg)) _ =
19.5 (case arg of
19.6 Free (n,_) =>
19.7 - (case ThmC_Def.int_of_str_opt n of
19.8 + (case ThmC_Def.int_opt_of_string n of
19.9 SOME i =>
19.10 if even i then SOME (TermC.mk_thmid thmid n "",
19.11 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
19.12 @@ -344,7 +344,7 @@
19.13 ("leq" ,("Orderings.ord_class.less_eq" , Prog_Expr.eval_equ "#less_equal_"))*)
19.14 fun eval_equ (thmid:string) (_(*op_*)) (t as
19.15 (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
19.16 - (case (ThmC_Def.int_of_str_opt n1, ThmC_Def.int_of_str_opt n2) of
19.17 + (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
19.18 (SOME n1', SOME n2') =>
19.19 if Num_Calc.calc_equ (strip_thy op0) (n1', n2')
19.20 then SOME (TermC.mk_thmid thmid n1 n2,
19.21 @@ -437,7 +437,7 @@
19.22 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
19.23 fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
19.24 (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
19.25 - (case (ThmC_Def.int_of_str_opt n1, ThmC_Def.int_of_str_opt n2) of
19.26 + (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
19.27 (SOME n1', SOME n2') =>
19.28 let
19.29 val sg = Num_Calc.sign_mult n1' n2';
20.1 --- a/src/Tools/isac/ProgLang/Program.thy Tue Apr 14 12:39:26 2020 +0200
20.2 +++ b/src/Tools/isac/ProgLang/Program.thy Tue Apr 14 15:56:15 2020 +0200
20.3 @@ -73,7 +73,7 @@
20.4 |> HOLogic.dest_Trueprop
20.5 |> Logic.unvarify_global
20.6 |> TermC.inst_abs
20.7 - |> ThmC_Def.numbers_to_string (*for numbers in the program*))
20.8 + |> ThmC_Def.num_to_Free (*for numbers in the program*))
20.9 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
20.10
20.11 (* get identifier of partial_function *)
21.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Apr 14 12:39:26 2020 +0200
21.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Apr 14 15:56:15 2020 +0200
21.3 @@ -191,14 +191,14 @@
21.4
21.5 (* convert int and float to internal floatingpoint prepresentation.*)
21.6 fun numeral (Free (str, _)) =
21.7 - (case ThmC_Def.int_of_str_opt str of
21.8 + (case ThmC_Def.int_opt_of_string str of
21.9 SOME i => SOME ((i, 0), (0, 0))
21.10 | NONE => NONE)
21.11 | numeral (Const ("Float.Float", _) $
21.12 (Const ("Product_Type.Pair", _) $
21.13 (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
21.14 (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
21.15 - (case (ThmC_Def.int_of_str_opt v1, ThmC_Def.int_of_str_opt v2, ThmC_Def.int_of_str_opt p1, ThmC_Def.int_of_str_opt p2) of
21.16 + (case (ThmC_Def.int_opt_of_string v1, ThmC_Def.int_opt_of_string v2, ThmC_Def.int_opt_of_string p1, ThmC_Def.int_opt_of_string p2) of
21.17 (SOME v1', SOME v2', SOME p1', SOME p2') =>
21.18 SOME ((v1', v2'), (p1', p2'))
21.19 | _ => NONE)
22.1 --- a/src/Tools/isac/TODO.thy Tue Apr 14 12:39:26 2020 +0200
22.2 +++ b/src/Tools/isac/TODO.thy Tue Apr 14 15:56:15 2020 +0200
22.3 @@ -43,10 +43,9 @@
22.4 \<close>
22.5 subsection \<open>Postponed from current changeset\<close>
22.6 text \<open>
22.7 - \item see "TODO CLEANUP Thm" in code
22.8 + \item "TODO CLEANUP Thm"
22.9 (* TODO CLEANUP Thm:
22.10 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
22.11 - (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC_Def.string_of_thmI
22.12 thmID : type for data from user input + program
22.13 thmDeriv : type for thy_hierarchy ONLY
22.14 obsolete types : thm' (SEE "ad thm'"), thm''.
23.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Tue Apr 14 12:39:26 2020 +0200
23.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Tue Apr 14 15:56:15 2020 +0200
23.3 @@ -149,10 +149,10 @@
23.4 XML.Elem (("INT", []), [XML.Text level]),
23.5 XML.Elem (("BOOL", []), [XML.Text rules])]) => (calcid, from, to, level, rules)
23.6 | tree => error ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
23.7 - val SOME calcid = int_of_str_opt calcid
23.8 + val SOME calcid = ThmC_Def.int_opt_of_string calcid
23.9 val from = xml_to_pos from
23.10 val to = xml_to_pos to
23.11 - val SOME level = (*xml_to_int*) int_of_str_opt level
23.12 + val SOME level = (*xml_to_int*) ThmC_Def.int_opt_of_string level
23.13 val rules = (*xml_to_bool*) string_to_bool rules
23.14 val out = getFormulaeFromTo calcid from to level rules (* <-------------------- *)
23.15 ;
23.16 @@ -215,7 +215,7 @@
23.17 XML.Elem (("CALCID", []), [XML.Text ci]),
23.18 p]) => (ci, p)
23.19 | _ => error "operation_setup refformula intree changed"
23.20 - val SOME calcid = int_of_str_opt ci
23.21 + val SOME calcid = ThmC_Def.int_opt_of_string ci
23.22 val pos = xml_to_pos p
23.23 ;
23.24 if calcid = 1 andalso pos = ([], Pbl) then () else error "--- step 6: intree changed";
24.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 14 12:39:26 2020 +0200
24.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 14 15:56:15 2020 +0200
24.3 @@ -65,7 +65,7 @@
24.4
24.5 term "(1.24444) :: real"
24.6
24.7 - numbers_to_string @{term "%x. (-9993::int) + x + 1"}
24.8 + ThmC_Def.num_to_Free @{term "%x. (-9993::int) + x + 1"}
24.9
24.10 Toplevel.debug := true;
24.11
24.12 @@ -81,7 +81,7 @@
24.13 "===== extend parse to string with markup===";
24.14 (*
24.15 fun parse thy str =
24.16 - (let val t = (typ_a2real o numbers_to_string)
24.17 + (let val t = (typ_a2real o ThmC_Def.num_to_Free)
24.18 (Syntax.read_term_global thy str)
24.19 in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
24.20 handle _ => NONE;
25.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Tue Apr 14 12:39:26 2020 +0200
25.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue Apr 14 15:56:15 2020 +0200
25.3 @@ -20,7 +20,7 @@
25.4 "----------- fun str_of_int --------------------------------------------------------------------";
25.5 "----------- fun scala_of_term -----------------------------------------------------------------";
25.6 "----------- fun contains_Var ------------------------------------------------------------------";
25.7 -"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
25.8 +"----------- fun ThmC_Def.int_opt_of_string, fun is_num ----------------------------------------------------";
25.9 "----------- fun is_f_x ------------------------------------------------------------------------";
25.10 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
25.11 "----------- fun strip_imp_prems' --------------------------------------------------------------";
25.12 @@ -29,7 +29,7 @@
25.13 "----------- fun dest_binop_typ ----------------------------------------------------------------";
25.14 "----------- fun is_list -----------------------------------------------------------------------";
25.15 "----------- fun inst_abs ----------------------------------------------------------------------";
25.16 -"----------- fun numbers_to_string -------------------------------------------------------------";
25.17 +"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
25.18 "--------------------------------------------------------";
25.19 "--------------------------------------------------------";
25.20
25.21 @@ -367,8 +367,8 @@
25.22 "---------------";
25.23 val str = "x + 2*z";
25.24 val t = (Syntax.read_term_global thy str);
25.25 - val t = numbers_to_string (Syntax.read_term_global thy str);
25.26 - val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
25.27 + val t = ThmC_Def.num_to_Free (Syntax.read_term_global thy str);
25.28 + val t = (typ_a2real o ThmC_Def.num_to_Free) (Syntax.read_term_global thy str);
25.29 Thm.global_cterm_of thy t;
25.30 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
25.31
25.32 @@ -382,8 +382,8 @@
25.33 "---------------";
25.34 val str = "x + 2*z";
25.35 val t = (Syntax.read_term_global thy str);
25.36 - val t = numbers_to_string (Syntax.read_term_global thy str);
25.37 - val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
25.38 + val t = ThmC_Def.num_to_Free (Syntax.read_term_global thy str);
25.39 + val t = (typ_a2real o ThmC_Def.num_to_Free) (Syntax.read_term_global thy str);
25.40 Thm.global_cterm_of thy t;
25.41 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
25.42
25.43 @@ -434,8 +434,8 @@
25.44 "----------- uminus_to_string ---------------------------";
25.45 "----------- uminus_to_string ---------------------------";
25.46 "----------- uminus_to_string ---------------------------";
25.47 - val t1 = numbers_to_string @{term "-2::real"};
25.48 - val t2 = numbers_to_string @{term "- 2::real"};
25.49 + val t1 = ThmC_Def.num_to_Free @{term "-2::real"};
25.50 + val t2 = ThmC_Def.num_to_Free @{term "- 2::real"};
25.51 if uminus_to_string t2 = t1
25.52 then ()
25.53 else error "termC.sml diff.behav. in uminus_to_string";
25.54 @@ -447,7 +447,7 @@
25.55 val str = "?a";
25.56 val t = (thy, str) |>> thy2ctxt
25.57 |-> Proof_Context.read_term_pattern
25.58 - |> numbers_to_string;
25.59 + |> ThmC_Def.num_to_Free;
25.60 val Var (("a", 0), ty) = t;
25.61 val TVar ((str, i), srt) = ty;
25.62 if str = "'a" andalso i = 1 andalso srt = []
25.63 @@ -458,7 +458,7 @@
25.64 val str = "?a :: real";
25.65 val t = (thy, str) |>> thy2ctxt
25.66 |-> Proof_Context.read_term_pattern
25.67 - |> numbers_to_string;
25.68 + |> ThmC_Def.num_to_Free;
25.69 val Var (("a", 0), ty) = t;
25.70 val Type (str, tys) = ty;
25.71 if str = "Real.real" andalso tys = [] andalso ty = HOLogic.realT
25.72 @@ -475,7 +475,7 @@
25.73 "----- read_term_pattern ---";
25.74 val t = (thy, str) |>> thy2ctxt
25.75 |-> Proof_Context.read_term_pattern
25.76 - |> numbers_to_string;
25.77 + |> ThmC_Def.num_to_Free;
25.78 val t_real = typ_a2real t;
25.79 if UnparseC.term_in_ctxt ctxt t_real =
25.80 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n "
25.81 @@ -596,17 +596,17 @@
25.82 val t = parse_patt @{theory} "z = 3";
25.83 if contains_Var t = false then () else error "contains_Var ?z = 3";
25.84
25.85 -"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
25.86 -"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
25.87 -"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";
25.88 -case int_of_str_opt "123" of
25.89 - SOME 123 => () | _ => raise error "int_of_str_opt 123 changed";
25.90 -case int_of_str_opt "(-123)" of
25.91 - SOME ~123 => () | _ => raise error "int_of_str_opt (-123) changed";
25.92 -case int_of_str_opt "#123" of
25.93 - NONE => () | _ => raise error "int_of_str_opt #123 changed";
25.94 -case int_of_str_opt "-123" of
25.95 - SOME ~123 => () | _ => raise error "int_of_str_opt -123 changed";
25.96 +"----------- fun ThmC_Def.int_opt_of_string, fun is_num ----------------------------------------------------";
25.97 +"----------- fun ThmC_Def.int_opt_of_string, fun is_num ----------------------------------------------------";
25.98 +"----------- fun ThmC_Def.int_opt_of_string, fun is_num ----------------------------------------------------";
25.99 +case ThmC_Def.int_opt_of_string "123" of
25.100 + SOME 123 => () | _ => raise error "ThmC_Def.int_opt_of_string 123 changed";
25.101 +case ThmC_Def.int_opt_of_string "(-123)" of
25.102 + SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string (-123) changed";
25.103 +case ThmC_Def.int_opt_of_string "#123" of
25.104 + NONE => () | _ => raise error "ThmC_Def.int_opt_of_string #123 changed";
25.105 +case ThmC_Def.int_opt_of_string "-123" of
25.106 + SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string -123 changed";
25.107
25.108 val t = str2term "1";
25.109 if is_num t = true then () else error "is_num 1";
25.110 @@ -699,12 +699,12 @@
25.111 val ty = (Term.type_of o Thm.term_of) ct;
25.112 if is_list t = true then () else error "is_list [a, b, c]";
25.113
25.114 -"----------- fun numbers_to_string -------------------------------------------------------------";
25.115 -"----------- fun numbers_to_string -------------------------------------------------------------";
25.116 -"----------- fun numbers_to_string -------------------------------------------------------------";
25.117 -if numbers_to_string @{term "123::real"} = Free ("123", HOLogic.realT)
25.118 -then () else error "numbers_to_string '123' changed";
25.119 -if numbers_to_string @{term "1::real"} = Free ("1", HOLogic.realT)
25.120 -then () else error "numbers_to_string '1' changed";
25.121 -if numbers_to_string @{term "0::real"} = Free ("0", HOLogic.realT)
25.122 -then () else error "numbers_to_string '0' changed";
25.123 +"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
25.124 +"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
25.125 +"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
25.126 +if ThmC_Def.num_to_Free @{term "123::real"} = Free ("123", HOLogic.realT)
25.127 +then () else error "ThmC_Def.num_to_Free '123' changed";
25.128 +if ThmC_Def.num_to_Free @{term "1::real"} = Free ("1", HOLogic.realT)
25.129 +then () else error "ThmC_Def.num_to_Free '1' changed";
25.130 +if ThmC_Def.num_to_Free @{term "0::real"} = Free ("0", HOLogic.realT)
25.131 +then () else error "ThmC_Def.num_to_Free '0' changed";
26.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 14 12:39:26 2020 +0200
26.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 14 15:56:15 2020 +0200
26.3 @@ -175,13 +175,13 @@
26.4 val (Thm (thmID, thm)) = ThmC.revert_sym thy
26.5 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
26.6 ;
26.7 -if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
26.8 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
26.9 then () else error "fun revert_sym changed 1";
26.10
26.11 val (Thm (thmID, thm)) = ThmC.revert_sym thy
26.12 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
26.13 ;
26.14 -if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
26.15 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
26.16 then () else error "fun revert_sym changed 2"
26.17
26.18 "----------- fun thms_of_rlss ------------------------------------";
27.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Apr 14 12:39:26 2020 +0200
27.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Apr 14 15:56:15 2020 +0200
27.3 @@ -839,7 +839,7 @@
27.4 Thm ("sym_#mult_2_3", "6 = 2 * 3")
27.5 ### Isabelle2009-2 for cancel_ (not cancel_p_):
27.6 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
27.7 - andalso string_of_thm thm =
27.8 + andalso ThmC.string_of_thm thm =
27.9 (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
27.10 (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2"))) then ()
27.11 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
27.12 @@ -859,7 +859,7 @@
27.13 (* find the next rule to apply *)
27.14 val SOME (r as (Thm (str, thm))) = nex revsets t;
27.15 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
27.16 - string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
27.17 + ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
27.18 (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2"))) then ()
27.19 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
27.20
28.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 12:39:26 2020 +0200
28.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 15:56:15 2020 +0200
28.3 @@ -552,7 +552,7 @@
28.4 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
28.5 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
28.6 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
28.7 - Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
28.8 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
28.9 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
28.10 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
28.11 end
28.12 @@ -566,7 +566,7 @@
28.13 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
28.14 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
28.15 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
28.16 - Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
28.17 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
28.18 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
28.19 in the pairopt end
28.20 end
29.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Apr 14 12:39:26 2020 +0200
29.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Apr 14 15:56:15 2020 +0200
29.3 @@ -15,7 +15,7 @@
29.4 "----------- tryrefine ----------------------------------";
29.5 "----------- search for Or_to_List ----------------------";
29.6 "----------- check thy in CalcTreeTEST ------------------";
29.7 -"----------- identified error in fun getTactic, string_of_thmI ---------------";
29.8 +"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
29.9 "----------- improved fun getTactic for interSteps and numeral calculations --";
29.10 "--------------------------------------------------------";
29.11 "--------------------------------------------------------";
29.12 @@ -171,9 +171,9 @@
29.13 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
29.14 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
29.15
29.16 -"----------- identified error in fun getTactic, string_of_thmI ---------------";
29.17 -"----------- identified error in fun getTactic, string_of_thmI ---------------";
29.18 -"----------- identified error in fun getTactic, string_of_thmI ---------------";
29.19 +"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
29.20 +"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
29.21 +"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
29.22 reset_states ();
29.23 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.24 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
29.25 @@ -234,9 +234,9 @@
29.26 BUT WE FIND IN THE CODE ABOVE IN find_next_step:*)
29.27 ;
29.28 (*----------------------------------------------------------------------------------------------*)
29.29 -if string_of_thmI @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
29.30 -then () else error "string_of_thmI changed";
29.31 -if string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
29.32 +if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
29.33 +then () else error "ThmC.string_of_thm changed";
29.34 +if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
29.35 then () else error "string_of_thm changed";
29.36 (*----------------------------------------------------------------------------------------------*)
29.37 ;
30.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Apr 14 12:39:26 2020 +0200
30.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Apr 14 15:56:15 2020 +0200
30.3 @@ -116,7 +116,7 @@
30.4 *)
30.5 val thy = @{theory "Test"};
30.6 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
30.7 - val ct = numbers_to_string @{term
30.8 + val ct = ThmC_Def.num_to_Free @{term
30.9 "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
30.10 case calculate_ thy op_ ct of
30.11 SOME _ => ()
31.1 --- a/test/Tools/isac/Test_Some_meld.thy Tue Apr 14 12:39:26 2020 +0200
31.2 +++ b/test/Tools/isac/Test_Some_meld.thy Tue Apr 14 15:56:15 2020 +0200
31.3 @@ -34,7 +34,7 @@
31.4 open Num_Calc; get_pair;
31.5 open TermC; atomt;
31.6 open Celem; e_pbt;
31.7 - open Rule; string_of_thm;
31.8 + open Rule; ThmC.string_of_thm;
31.9 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31.10 \<close>
31.11 ML_file "Calcelements/libraryC.sml"