1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Sun Aug 22 09:43:43 2021 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Sun Aug 22 11:42:55 2021 +0200
1.3 @@ -79,9 +79,10 @@
1.4 if ! trace_on andalso i < ! depth
1.5 then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
1.6 else();
1.7 -fun msg thy op_ thmC t =
1.8 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
1.9 - "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
1.10 +fun msg call thy op_ thmC t =
1.11 + call ^ ": \n" ^
1.12 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
1.13 + "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
1.14
1.15 fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.16 let
1.17 @@ -177,7 +178,7 @@
1.18 let
1.19 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.20 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.21 - val _ = if pairopt <> NONE then () else raise ERROR (msg thy op_ thm' ct)
1.22 + val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct)
1.23 val _ = trace_in3 i "calc. to" thy pairopt;
1.24 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.25 end
1.26 @@ -281,13 +282,13 @@
1.27 end;
1.28
1.29 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
1.30 -fun calculate_ thy isa_fn ct =
1.31 - case Eval.adhoc_thm thy isa_fn ct of
1.32 +fun calculate_ thy (isa_fn as (id, eval_fn)) t =
1.33 + case Eval.adhoc_thm thy isa_fn t of
1.34 NONE => NONE
1.35 | SOME (thmID, thm) =>
1.36 - (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
1.37 + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
1.38 SOME (rew, _) => rew
1.39 - | NONE => raise ERROR ""
1.40 + | NONE => raise ERROR (msg "calculate_" thy id thm t)
1.41 in SOME (rew, (thmID, thm)) end)
1.42 handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
1.43
2.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 09:43:43 2021 +0200
2.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 11:42:55 2021 +0200
2.3 @@ -110,14 +110,14 @@
2.4 fun trace_calc4 str t1 t2 =
2.5 if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
2.6
2.7 -fun get_pair thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
2.8 +fun get_pair (*1*)thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
2.9 if op_ = op0 then
2.10 let val popt = ef op_ t thy
2.11 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
2.12 else get_pair thy op_ ef arg
2.13 - | get_pair thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
2.14 + | get_pair (*2*)thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
2.15 ef "Prog_Expr.ident" t thy (* not nested *)
2.16 - | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
2.17 + | get_pair (*3*)thy op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
2.18 (trace_calc1 "1.. get_pair: binop = " op_;
2.19 if op_ = op0 then
2.20 let
2.21 @@ -134,7 +134,7 @@
2.22 val popt = get_pair thy op_ ef t1
2.23 val _ = trace_calc2 "4.. get_pair: " t popt
2.24 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
2.25 - | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
2.26 + | get_pair (*4*)thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
2.27 (trace_calc3 "get_pair 4a: t= "t;
2.28 trace_calc1 "get_pair 4a: op_= " op_;
2.29 trace_calc1 "get_pair 4a: op0= " op0;
2.30 @@ -144,15 +144,15 @@
2.31 else
2.32 (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>
2.33 (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))
2.34 - | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
2.35 - | get_pair thy op_ ef (t1 $ t2) =
2.36 + | get_pair (*5*)thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
2.37 + | get_pair (*6*)thy op_ ef (t1 $ t2) =
2.38 let
2.39 val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2;
2.40 val popt = get_pair thy op_ ef t1
2.41 in case popt of SOME _ => popt
2.42 | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2)
2.43 end
2.44 - | get_pair _ _ _ _ = NONE
2.45 + | get_pair (*7*)_ _ _ _ = NONE
2.46
2.47 (* get a thm from an op_ somewhere in the term;
2.48 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
3.1 --- a/test/Tools/isac/Test_Some.thy Sun Aug 22 09:43:43 2021 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Sun Aug 22 11:42:55 2021 +0200
3.3 @@ -1072,154 +1072,10 @@
3.4 (*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
3.5 \<close> ML \<open>
3.6 \<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.7 +Rewrite.trace_on := true; (*false true*)
3.8 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
3.9 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
3.10 \<close> ML \<open>
3.11 - @{theory}; (*Isac_Test.Test_Some:153857*)
3.12 -\<close> ML \<open>
3.13 -d2_polyeq_abcFormula_simplify
3.14 -\<close> ML \<open>
3.15 -val t = TermC.str2term "x + 2 * x \<up> 2 = 0";
3.16 -val subst = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
3.17 -\<close> ML \<open>
3.18 -val SOME (t', []) = rewrite_set_ @{theory} true d2_polyeq_abcFormula_simplify t;
3.19 -\<close> ML \<open>
3.20 -UnparseC.term t' = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
3.21 -(* same as isabisac15 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.22 -\<close> ML \<open>
3.23 -rewrite_set_inst_ @{theory} true subst d2_polyeq_abcFormula_simplify t
3.24 -\<close> ML \<open>
3.25 -UnparseC.term t' = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)"
3.26 -(* same as isabisac15 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.27 -\<close> ML \<open> (*------- BUT THE ERROR COMES FROM Step.do_next WITH ANOTHER REWRITE -----------------*)
3.28 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
3.29 -\<close> ML \<open>
3.30 - val (pt, p) =
3.31 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
3.32 - case Step.by_tactic tac (pt, p) of
3.33 - ("ok", (_, _, ptp)) => ptp
3.34 - | ("unsafe-ok", (_, _, ptp)) => ptp
3.35 - | ("not-applicable",_) => (pt, p)
3.36 - | ("end-of-calculation", (_, _, ptp)) => ptp
3.37 - | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
3.38 - | _ => raise ERROR "me: uncovered case Step.by_tactic"
3.39 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.40 - (*case*)
3.41 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
3.42 -\<close> ML \<open>
3.43 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
3.44 -\<close> ML \<open>
3.45 - (*if*) Pos.on_calc_end ip (*else*);
3.46 -\<close> ML \<open>
3.47 - val (_, probl_id, _) = Calc.references (pt, p);
3.48 -\<close> ML \<open>
3.49 -val _ =
3.50 - (*case*) tacis (*of*);
3.51 -\<close> ML \<open>
3.52 - (*if*) probl_id = Problem.id_empty (*else*);
3.53 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.54 - switch_specify_solve p_ (pt, ip);
3.55 -\<close> ML \<open>
3.56 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
3.57 -\<close> ML \<open>
3.58 - (*if*) Pos.on_specification ([], state_pos) (*else*);
3.59 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.60 - LI.do_next (pt, input_pos)
3.61 -\<close> ML \<open>
3.62 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
3.63 -\<close> ML \<open>
3.64 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
3.65 -\<close> ML \<open>
3.66 - val thy' = get_obj g_domID pt (par_pblobj pt p);
3.67 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
3.68 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.69 - (*case*)
3.70 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
3.71 -\<close> ML \<open>
3.72 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) =
3.73 - (sc, (pt, pos), ist, ctxt);
3.74 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.75 - (*case*)
3.76 - LI.scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist)
3.77 -\<close> ML \<open>
3.78 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
3.79 - ((prog, (ptp, ctxt)), (Pstate ist));
3.80 -\<close> ML \<open>
3.81 - (*if*) path = [] (*else*);
3.82 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.83 - go_scan_up (prog, cc) (trans_scan_up ist)
3.84 -\<close> ML \<open>
3.85 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
3.86 - ((prog, cc), (trans_scan_up ist));
3.87 -\<close> ML \<open>
3.88 - (*if*) path = [R] (*else*);
3.89 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.90 - scan_up pcc (ist |> path_up) (go_up path sc)
3.91 -\<close> ML \<open>
3.92 -"~~~~~ and scan_up , args:"; val (pcc, ist,(Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ )) =
3.93 - (pcc, (ist |> path_up), (go_up path sc));
3.94 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.95 - go_scan_up pcc ist
3.96 -\<close> ML \<open>
3.97 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
3.98 - (pcc, ist);
3.99 -\<close> ML \<open>
3.100 - (*if*) path = [R] (*else*);
3.101 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.102 - scan_up pcc (ist |> path_up) (go_up path sc)
3.103 -\<close> ML \<open>
3.104 -"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) =
3.105 - (pcc, (ist |> path_up), (go_up path sc));
3.106 -\<close> ML \<open>
3.107 - val e2 = check_Seq_up ist sc;
3.108 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.109 - (*case*)
3.110 - scan_dn cc (ist |> path_up_down [R]) e2 (*of*);
3.111 -\<close> ML \<open>
3.112 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) =
3.113 - (cc, (ist |> path_up_down [R]), e2);
3.114 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.115 - (*case*)
3.116 - scan_dn cc (ist |> path_down [L, R]) e1 (*of*);
3.117 -\<close> ML \<open>
3.118 -"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e)) =
3.119 - (cc, (ist |> path_down [L, R]), e1);
3.120 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.121 - (*case*)
3.122 - scan_dn cc (ist |> path_down [R]) e (*of*);
3.123 -\<close> ML \<open>
3.124 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) =
3.125 - (cc, (ist |> path_down [R]), e);
3.126 -\<close> ML \<open>
3.127 - (*if*) Tactical.contained_in t (*else*);
3.128 -\<close> ML \<open>
3.129 -val (Program.Tac prog_tac, form_arg) = (*case*)
3.130 - LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
3.131 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.132 - check_tac cc ist (prog_tac, form_arg)
3.133 -\<close> ML \<open>
3.134 -"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
3.135 - (cc, ist, (prog_tac, form_arg));
3.136 -\<close> ML \<open>
3.137 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
3.138 -\<close> ML \<open>
3.139 -val _ = (*case*) m (*of*);
3.140 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.141 - (*case*)
3.142 -Solve_Step.check m (pt, p) (*of*);
3.143 -\<close> ML \<open>
3.144 -"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, (p, _)))) =
3.145 - (m, (pt, p));
3.146 -\<close> ML \<open>
3.147 - val pp = Ctree.par_pblobj pt p;
3.148 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.149 - val f = Calc.current_formula cs;
3.150 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.151 - (*case*)
3.152 - Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f (*of*);
3.153 -\<close> ML \<open>
3.154 -ThyC.get_theory thy'
3.155 -\<close> ML \<open>
3.156 \<close> ML \<open>
3.157 \<close> ML \<open>
3.158 \<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml*)
3.159 @@ -1261,78 +1117,79 @@
3.160 \<close> ML \<open>
3.161 \<close> ML \<open>
3.162 \<close> ML \<open>
3.163 +"--------------------------------- NEW TEST --> ??? -------------------------------------------";
3.164 +"--------------------------------- NEW TEST --> ??? -------------------------------------------";
3.165 +"--------------------------------- NEW TEST --> ??? -------------------------------------------";
3.166 \<close> ML \<open>
3.167 -UnparseC.term f = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)"
3.168 +(*
3.169 + the sequence of fun calls below is a selection from a longer step-into.
3.170 +
3.171 + ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals
3.172 + given a certain ML_type\<open>eval_fn\<close> and a certain ML\<open>term\<close> ..
3.173 +*)
3.174 \<close> ML \<open>
3.175 -"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) =
3.176 - ((ThyC.get_theory thy'), false, (assoc_rls rls), f);
3.177 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.178 - rewrite__set_ thy 1 bool [] rls term;
3.179 +val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);
3.180 +val t = @{term "- 1 / 2 ::real"};
3.181 \<close> ML \<open>
3.182 -"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
3.183 - (thy, 1, bool, [], rls, term);
3.184 -\<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml *)
3.185 -fun msg thmC t =
3.186 - "rewrite with thm " ^ quote (ThmC.string_of_thm thmC) ^
3.187 - " on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
3.188 +Eval.adhoc_thm @{theory} eval_ t
3.189 \<close> ML \<open>
3.190 \<close> ML \<open>
3.191 +fun msg thy op_ thmC t =
3.192 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
3.193 + "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
3.194 \<close> ML \<open>
3.195 -(*//-------------------------------- cp fromewrite.sml-----------------------------------------\\*)
3.196 - (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
3.197 - datatype switch = Appl | Noap;
3.198 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
3.199 - | rew_once ruls asm ct Appl [] =
3.200 - (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
3.201 - | Rule_Set.Sequence _ => (ct, asm)
3.202 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
3.203 - | rew_once ruls asm ct apno (rul :: thms) =
3.204 - case rul of
3.205 - Rule.Thm (thmid, thm) =>
3.206 - (trace_in1 i "try thm" thmid;
3.207 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.208 - ((#erls o Rule_Set.rep) rls) put_asm thm ct of
3.209 - NONE => rew_once ruls asm ct apno thms
3.210 - | SOME (ct', asm') =>
3.211 - (trace_in2 i "rewrites to" thy ct';
3.212 - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
3.213 - (* once again try the same rule, e.g. associativity against "()"*)
3.214 - | Rule.Eval (cc as (op_, _)) =>
3.215 - let val _ = trace_in1 i "try calc" op_;
3.216 - in case Eval.adhoc_thm thy cc ct of
3.217 - NONE => rew_once ruls asm ct apno thms
3.218 - | SOME (_, thm') =>
3.219 - let
3.220 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.221 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
3.222 - val _ = if pairopt <> NONE then () else raise ERROR (msg thm' ct)
3.223 - val _ = trace_in3 i "calc. to" thy pairopt;
3.224 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
3.225 - end
3.226 - | Rule.Cal1 (cc as (op_, _)) =>
3.227 - let val _ = trace_in1 i "try cal1" op_;
3.228 - in case Eval.adhoc_thm1_ thy cc ct of
3.229 - NONE => (ct, asm)
3.230 - | SOME (_, thm') =>
3.231 - let
3.232 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.233 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
3.234 - val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
3.235 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
3.236 - val _ = trace_in3 i "cal1. to" thy pairopt;
3.237 - in the pairopt end
3.238 - end
3.239 - | Rule.Rls_ rls' =>
3.240 - (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
3.241 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
3.242 - | NONE => rew_once ruls asm ct apno thms)
3.243 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
3.244 -(*\\------------------------------- cp from rewrite.sml---------------------------------------//*)
3.245 +Eval.get_pair;
3.246 +Eval.adhoc_thm
3.247 \<close> ML \<open>
3.248 +fun calculate_ thy (isa_fn as (id, eval_fn)) ct =
3.249 + case Eval.adhoc_thm thy isa_fn ct of
3.250 + NONE => NONE
3.251 + | SOME (thmID, thm) =>
3.252 + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
3.253 + SOME (rew, _) => rew
3.254 + | NONE => raise ERROR "calculate_: "
3.255 + in SOME (rew, (thmID, thm)) end)
3.256 + handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
3.257 \<close> ML \<open>
3.258 -"--------------------------------- NEW TEST --> ??? -------------------------------------------";
3.259 -"--------------------------------- NEW TEST --> ??? -------------------------------------------";
3.260 -"--------------------------------- NEW TEST --> ??? -------------------------------------------";
3.261 +\<close> ML \<open>
3.262 +\<close> ML \<open>
3.263 +\<close> ML \<open>
3.264 +\<close> ML \<open>
3.265 +\<close> ML \<open>
3.266 +
3.267 +val t = @{term "- 1 / 2 ::real"};
3.268 +\<close> ML \<open>
3.269 +val SOME
3.270 + ("#divide_e~1_2", t') =
3.271 + Eval.get_pair @{theory} "Rings.divide_class.divide" (eval_cancel "#divide_e") t
3.272 +\<close> ML \<open>
3.273 +(*
3.274 + get_pair finds two adjacent numerals and does NOT distinguish between divide, plus, etc.
3.275 + So it returns the input Unchanged..
3.276 +*)
3.277 +UnparseC.term t' = "- 1 / 2 = - 1 / 2";
3.278 +\<close> ML \<open>
3.279 +\<close> ML \<open>
3.280 +\<close> ML \<open>
3.281 +\<close> ML \<open>
3.282 +\<close> ML \<open>
3.283 +\<close> ML \<open>
3.284 +\<close> ML \<open>
3.285 +\<close> ML \<open>
3.286 +\<close> ML \<open>
3.287 +\<close> ML \<open>
3.288 +\<close> ML \<open>
3.289 +\<close> ML \<open>
3.290 +\<close> ML \<open>
3.291 +\<close> ML \<open>
3.292 +\<close> ML \<open>
3.293 +"~~~~~ fun get_pair , args:"; val ((*3*)thy, op_, ef, (t as (Const (op0, _) $ t1 $ t2))) =
3.294 + (@{theory}, "Rings.divide_class.divide", (eval_cancel "#divide_e"), t);
3.295 +\<close> ML \<open>
3.296 +\<close> ML \<open>
3.297 +\<close> ML \<open>
3.298 +\<close> ML \<open>
3.299 +\<close> ML \<open>
3.300 \<close> ML \<open>
3.301 "~~~~~ and rewrite__set_ thy , args:"; val ((*3*)thy, i, put_asm, bdv, rls, ct) =
3.302 (@{theory}, 0, true, []: (term * term) list, assoc_rls "reduce_012", @{term "- 1 / 2 :: real"});
3.303 @@ -1361,193 +1218,6 @@
3.304 \<close> ML \<open>
3.305 \<close> ML \<open>
3.306 \<close> ML \<open>
3.307 -\<close> ML \<open>
3.308 -\<close> ML \<open>
3.309 -\<close> ML \<open>
3.310 -\<close> ML \<open>
3.311 -\<close> ML \<open>
3.312 -\<close> ML \<open>
3.313 -\<close> ML \<open>
3.314 -\<close> ML \<open>
3.315 -\<close> ML \<open>
3.316 -\<close> ML \<open>
3.317 -\<close> ML \<open>
3.318 -\<close> ML \<open>
3.319 -\<close> ML \<open>
3.320 -\<close> ML \<open>
3.321 -\<close> ML \<open>
3.322 -\<close> ML \<open>
3.323 -\<close> ML \<open>
3.324 -\<close> ML \<open>
3.325 -\<close> ML \<open>
3.326 -\<close> ML \<open>
3.327 - val ruls = (#rules o Rule_Set.rep) rls;
3.328 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
3.329 -Rewrite.trace_on := true; (*false true*)
3.330 - val (ct', asm') =
3.331 - rew_once ruls [] ct Noap ruls;
3.332 -\<close> ML \<open>
3.333 -(*+*)UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
3.334 -\<close> ML \<open>
3.335 -(*+*)rls
3.336 -\<close> ML \<open>
3.337 -(*+*)ruls(* =
3.338 - [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Thm ("real_assoc_2", "?a * (?b * ?c) = ?a * ?b * ?c"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"),
3.339 - Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Thm ("realpow_multI", "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.minus_class.minus", fn),
3.340 - Eval ("Groups.times_class.times", fn), Eval ("Rings.divide_class.divide", fn), Eval ("NthRoot.sqrt", fn), Eval ("Transcendental.powr", fn),
3.341 - Rls ( Repeat
3.342 - {calc = [], erls =
3.343 - Repeat
3.344 - {calc = [], erls = Empty, errpatts = [], id = "erls_in_reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules =
3.345 - [Eval ("Prog_Expr.is_num", fn), Thm ("not_false", "(\<not> False) = True"), Thm ("not_true", "(\<not> True) = False")], scr = Empty_Prog, srls = Empty},
3.346 - errpatts = [], id = "reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules =
3.347 -------------------------------^^^^^^^^^^^^
3.348 - [Thm ("mult_1_left", "1 * ?a = ?a"), Thm ("real_minus_mult_left", "\<not> (?a is_num) \<Longrightarrow> - ?a * ?b = - (?a * ?b)"), Thm ("mult_zero_left", "0 * ?a = 0"), Thm ("add_0_left", "0 + ?a = ?a"),
3.349 - Thm ("add_0_right", "?a + 0 = ?a"), Thm ("right_minus", "?a + - ?a = 0"), Thm ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), Thm ("real_mult_2_assoc", "?z1.0 + (?z1.0 + ?k) = 2 * ?z1.0 + ?k")],
3.350 - scr = Empty_Prog, srls = Empty}
3.351 - )]*)
3.352 -\<close> ML \<open>
3.353 -"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) =
3.354 - (ruls, [], ct, Noap, ruls);
3.355 -\<close> ML \<open>
3.356 -val Rule.Thm (thmid, thm) =
3.357 - (*case*) rul (*of*);
3.358 -\<close> ML \<open>
3.359 -val NONE = (*case*) rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.360 - ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
3.361 -\<close> ML \<open>
3.362 -\<close> ML \<open>
3.363 -\<close> ML \<open>
3.364 -\<close> ML \<open>
3.365 -\<close> ML \<open>
3.366 -\<close> ML \<open>
3.367 -\<close> ML \<open>
3.368 -\<close> ML \<open>
3.369 -\<close> ML \<open>
3.370 -\<close> ML \<open>
3.371 -\<close> ML \<open>
3.372 -\<close> ML \<open>
3.373 -\<close> ML \<open>
3.374 -\<close> ML \<open>
3.375 -\<close> ML \<open>
3.376 -\<close> ML \<open>
3.377 -\<close> ML \<open>
3.378 -\<close> ML \<open>
3.379 -\<close> ML \<open>
3.380 -\<close> ML \<open>
3.381 -\<close> ML \<open>
3.382 -\<close> ML \<open>
3.383 -\<close> ML \<open>
3.384 -\<close> ML \<open>
3.385 -\<close> ML \<open>
3.386 -\<close> ML \<open>
3.387 -\<close> ML \<open>
3.388 -\<close> ML \<open>
3.389 -(*/------------------------------- fun rew_once ITERATED BY HAND -----------------------------\*)
3.390 -\<close> ML \<open>
3.391 -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
3.392 -\<close> ML \<open>
3.393 -val thm = Rule.thm (nth 1 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
3.394 -\<close> ML \<open>
3.395 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.396 - ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
3.397 -\<close> ML \<open>
3.398 -val thm = Rule.thm (nth 2 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"
3.399 - ATTENTION "real_assoc_1" == "real_assoc_2"*)
3.400 -\<close> ML \<open>
3.401 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.402 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.403 -\<close> ML \<open>
3.404 -val thm = Rule.thm (nth 3 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
3.405 -\<close> ML \<open>
3.406 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.407 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.408 -\<close> ML \<open>
3.409 -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 - 0)) / (2 * 2)"
3.410 -\<close> ML \<open>
3.411 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.412 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.413 -\<close> ML \<open>
3.414 -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
3.415 -\<close> ML \<open>
3.416 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.417 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.418 -\<close> ML \<open>
3.419 -UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
3.420 -\<close> ML \<open>
3.421 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.422 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.423 -\<close> ML \<open>
3.424 -val thm = Rule.thm (nth 4 ruls); (* = "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"*)
3.425 -\<close> ML \<open>
3.426 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.427 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.428 -\<close> ML \<open>
3.429 -val thm = Rule.thm (nth 5 ruls); (* = "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"*)
3.430 -\<close> ML \<open>
3.431 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.432 - ((#erls o Rule_Set.rep) rls) put_asm thm ct
3.433 -\<close> ML \<open> (* \<longrightarrow> Rule.*)
3.434 -\<close> ML \<open>
3.435 -val (cc as (op_, _)) = Rule.eval (nth 6 ruls); (* = "Groups.plus_class.plus"*)
3.436 -\<close> ML \<open>
3.437 -val NONE = Eval.adhoc_thm thy cc ct
3.438 -\<close> ML \<open>
3.439 -val (cc as (op_, _)) = Rule.eval (nth 7 ruls); (* = "Groups.minus_class.minus"*)
3.440 -\<close> ML \<open>
3.441 -val NONE = Eval.adhoc_thm thy cc ct
3.442 -\<close> ML \<open>
3.443 -val (cc as (op_, _)) = Rule.eval (nth 8 ruls); (* = "Groups.times_class.times"*)
3.444 -\<close> ML \<open>
3.445 -val SOME (_, thm') = Eval.adhoc_thm thy cc ct
3.446 -\<close> ML \<open>
3.447 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.448 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
3.449 -\<close> ML \<open>
3.450 - "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)";
3.451 -UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
3.452 -\<close> ML \<open>
3.453 -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.454 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
3.455 -\<close> ML \<open>
3.456 -UnparseC.term ct = "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
3.457 -\<close> ML \<open>
3.458 -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
3.459 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
3.460 -\<close> ML \<open>
3.461 -val (cc as (op_, _)) = Rule.eval (nth 9 ruls); (* = "Rings.divide_class.divide"*)
3.462 -\<close> ML \<open>
3.463 -val NONE = Eval.adhoc_thm thy cc ct
3.464 -\<close> ML \<open>
3.465 -val (cc as (op_, _)) = Rule.eval (nth 10 ruls); (* = "NthRoot.sqrt"*)
3.466 -\<close> ML \<open>
3.467 -val NONE = Eval.adhoc_thm thy cc ct
3.468 -\<close> ML \<open>
3.469 -val (cc as (op_, _)) = Rule.eval (nth 11 ruls); (* = "Transcendental.powr"*)
3.470 -\<close> ML \<open>
3.471 -val NONE = Eval.adhoc_thm thy cc ct
3.472 -\<close> ML \<open>
3.473 -val rls' = Rule.rls (nth 12 ruls); (* = "reduce_012"*)
3.474 -\<close> ML \<open>
3.475 -val SOME (ct, []) = rewrite__set_ thy (i + 1) put_asm bdv rls' ct
3.476 -\<close> ML \<open>
3.477 - "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)";
3.478 -UnparseC.term ct = "x = (- 1 + sqrt 1) / (2 * 2) \<or> x = (- 1 + - 1 * sqrt 1) / (2 * 2)"
3.479 -\<close> ML \<open>
3.480 -length ruls = 12
3.481 -\<close> ML \<open>
3.482 -\<close> ML \<open>
3.483 -\<close> ML \<open>
3.484 -\<close> ML \<open>
3.485 -\<close> ML \<open>
3.486 -\<close> ML \<open>
3.487 -\<close> ML \<open>
3.488 -\<close> ML \<open>
3.489 -\<close> ML \<open>
3.490 -\<close> ML \<open>
3.491 -\<close> ML \<open>
3.492 -\<close> ML \<open>
3.493 -\<close> ML \<open>
3.494 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
3.495 \<close> text \<open>
3.496 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;