1.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Jul 28 17:06:16 2014 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Jul 31 14:15:41 2014 +0200
1.3 @@ -521,7 +521,7 @@
1.4 > *** dropwhile': did not start with equal elements*)
1.5
1.6 (*040214: version for concat_deriv*)
1.7 -fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
1.8 +fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
1.9
1.10 fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
1.11 (Rewrite (rule2thm' r),
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Jul 28 17:06:16 2014 +0200
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Jul 31 14:15:41 2014 +0200
2.3 @@ -233,12 +233,20 @@
2.4 Rrls {id="sym_"^id, scr=scr, calc=calc, errpatts=errpatts, erls=erls, prepat=prepat,
2.5 rew_ord=rew_ord};
2.6
2.7 -fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
2.8 - | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
2.9 - | sym_Thm r = error ("sym_Thm: not for "^(rule2str r));
2.10 +(* toggles sym_* and keeps "#:" for ad-hoc calculations *)
2.11 +fun sym_rule (Thm (thmID, thm)) =
2.12 + let
2.13 + val thm' = sym_thm thm
2.14 + val thmID' = case Symbol.explode thmID of
2.15 + "s"::"y"::"m"::"_"::id => implode id
2.16 + | "#"::":":: _ => "#: " ^ string_of_thmI thm'
2.17 + | _ => "sym_" ^ thmID
2.18 + in Thm (thmID', thm') end
2.19 + | sym_rule (Rls_ rls) = Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
2.20 + | sym_rule r = error ("sym_rule: not for " ^ (rule2str r));
2.21 (*
2.22 val th = Thm ("real_one_collect",num_str @{thm real_one_collect});
2.23 - sym_Thm th;
2.24 + sym_rule th;
2.25 val th =
2.26 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
2.27 : rule
2.28 @@ -247,7 +255,7 @@
2.29
2.30
2.31 (*version for reverse rewrite used before 040214*)
2.32 -fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
2.33 +fun rev_deriv (t, r, (t', a)) = (sym_rule r, (t, a));
2.34 (* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');
2.35 *)
2.36 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Mon Jul 28 17:06:16 2014 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Jul 31 14:15:41 2014 +0200
3.3 @@ -259,7 +259,7 @@
3.4 (*WN071229 "Fields.inverse_class.divide" never tried*)
3.5 val rhs = var_op_float v op_ t0 T1 res
3.6 val prop = Trueprop $ (mk_equality (t, rhs))
3.7 - in SOME (mk_thmid_f thmid n1 n2, prop) end
3.8 + in SOME ("#: " ^ term2str prop, prop) end
3.9 | _ => NONE
3.10 else NONE
3.11 | eval_binop (thmid:string) (op_:string)
3.12 @@ -275,7 +275,7 @@
3.13 val res = calc op0 n1 n2
3.14 val rhs = float_op_var v op_ t0 T1 res
3.15 val prop = Trueprop $ (mk_equality (t, rhs))
3.16 - in SOME (mk_thmid_f thmid n1 n2, prop) end
3.17 + in SOME ("#: " ^ term2str prop, prop) end
3.18 | _ => NONE
3.19 else NONE
3.20
3.21 @@ -287,7 +287,7 @@
3.22 val res = calc op0 n1 n2;
3.23 val rhs = term_of_float Trange res;
3.24 val prop = Trueprop $ (mk_equality (t, rhs));
3.25 - in SOME (mk_thmid_f thmid n1 n2, prop) end
3.26 + in SOME ("#: " ^ term2str prop, prop) end
3.27 | _ => NONE)
3.28 | eval_binop _ _ _ _ = NONE;
3.29 (*
4.1 --- a/src/Tools/isac/calcelems.sml Mon Jul 28 17:06:16 2014 +0200
4.2 +++ b/src/Tools/isac/calcelems.sml Thu Jul 31 14:15:41 2014 +0200
4.3 @@ -536,7 +536,8 @@
4.4
4.5 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
4.6 TODO (a): thehier does not contain sym_thmID theorems
4.7 -TODO (b): lookup to thehier for sym_thmID creates response using sym_thm
4.8 + (b): lookup for sym_thmID directly from Isabelle using sym_thm
4.9 + (within math-engine NO lookup in thehier -- within java in *.xml only!)
4.10 TODO (c): export from thehier to xml
4.11 TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
4.12 TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
5.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Jul 28 17:06:16 2014 +0200
5.2 +++ b/test/Tools/isac/Knowledge/rational.sml Thu Jul 31 14:15:41 2014 +0200
5.3 @@ -691,14 +691,12 @@
5.4 then () else error "first element of revset changed";
5.5 if
5.6 (revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso
5.7 -(revsets |> nth 1 |> nth 2 |> rule2str) =
5.8 - "Thm (\"sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))\",9 = 3 ^^^ 2)" andalso
5.9 -(revsets |> nth 1 |> nth 3 |> rule2str) =
5.10 - "Thm (\"sym_#mult_Float ((2,0), (0,0)) __ ((3,0), (0,0))\",6 * x = 2 * (3 * x))" andalso
5.11 -(revsets |> nth 1 |> nth 4 |> rule2str) =
5.12 - "Thm (\"sym_#mult_Float ((~1,0), (0,0)) __ ((3,0), (0,0))\",-3 * x = -1 * (3 * x))" andalso
5.13 -(revsets |> nth 1 |> nth 5 |> rule2str) =
5.14 - "Thm (\"sym_#mult_Float ((3,0), (0,0)) __ ((3,0), (0,0))\",9 = 3 * 3)" andalso
5.15 +(revsets |> nth 1 |> nth 2 |> rule2str) = "Thm (\"#: 9 = 3 ^^^ 2\",9 = 3 ^^^ 2)" andalso
5.16 +(revsets |> nth 1 |> nth 3 |> rule2str) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
5.17 +andalso
5.18 +(revsets |> nth 1 |> nth 4 |> rule2str) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))"
5.19 +andalso
5.20 +(revsets |> nth 1 |> nth 5 |> rule2str) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
5.21 (revsets |> nth 1 |> nth 6 |> rule2str) = "Rls_ (\"sym_order_mult_rls_\")" andalso
5.22 (revsets |> nth 1 |> nth 7 |> rule2str) =
5.23 "Thm (\"sym_mult_assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"