1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Aug 22 14:28:38 2021 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Aug 23 12:33:10 2021 +0200
1.3 @@ -423,9 +423,9 @@
1.4 let
1.5 val (T, _) = HOLogic.dest_number t1;
1.6 val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
1.7 - val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
1.8 + val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
1.9 in
1.10 - if (i1', i2') = (i1, i2) then NONE
1.11 + if abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') then NONE
1.12 else
1.13 let
1.14 val res = TermC.mk_frac T res_int;
2.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 14:28:38 2021 +0200
2.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Mon Aug 23 12:33:10 2021 +0200
2.3 @@ -154,22 +154,18 @@
2.4 end
2.5 | get_pair (*7*)_ _ _ _ = NONE
2.6
2.7 -(* get a thm from an op_ somewhere in the term;
2.8 - apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
2.9 +(* get a thm from an op_ somewhere in a term by use of get_pair *)
2.10 fun adhoc_thm thy (op_, eval_fn) t =
2.11 +((*@{print\<open>tracing\<close>}{a = "adhoc_thm", op_ = op_, t = t, get_p = get_pair thy op_ eval_fn t};*)
2.12 case get_pair thy op_ eval_fn t of
2.13 NONE => NONE
2.14 - | SOME (thmid, t') =>
2.15 - if t = (TermC.rhs o HOLogic.dest_Trueprop) t'
2.16 - then NONE (*..can result from eval_cancel: see test -- fun adhoc_thm + fun eval_cancel --*)
2.17 - else SOME (thmid, Skip_Proof.make_thm thy t');
2.18 + | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t'));
2.19
2.20 -(* get a thm applying an op_ to a term;
2.21 - apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)
2.22 +(* get a thm applying an op_ to a term by direct use of eval_fn *)
2.23 fun adhoc_thm1_ thy (op_, eval_fn) ct =
2.24 case eval_fn op_ ct thy of
2.25 - NONE => NONE
2.26 - | SOME (thmid, t) => SOME (thmid, Skip_Proof.make_thm thy t);
2.27 + NONE => NONE
2.28 + | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t');
2.29
2.30 (** for ordered and conditional rewriting **)
2.31
3.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Sun Aug 22 14:28:38 2021 +0200
3.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Mon Aug 23 12:33:10 2021 +0200
3.3 @@ -123,6 +123,21 @@
3.4 "-------- fun eval_cancel ----------------------------------------------------------------------";
3.5 "-------- fun eval_cancel ----------------------------------------------------------------------";
3.6 "-------- fun eval_cancel ----------------------------------------------------------------------";
3.7 +val t = @{term "- 1 / 2 :: real"};
3.8 +val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t "";
3.9 +"~~~~~ fun eval_cancel , args:"; val (thmid, "Rings.divide_class.divide", (t as (Const _ $ t1 $ t2))) =
3.10 + ("xxx", "Rings.divide_class.divide", t);
3.11 + (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
3.12 + val (T, _) = HOLogic.dest_number t1;
3.13 + val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
3.14 + val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
3.15 +
3.16 +(*+*)val (~1, (1, 2)) = res_int;
3.17 +
3.18 + (*if*) abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') (*then*);
3.19 + NONE (*return value*);
3.20 +
3.21 +"-------- further examples ";
3.22 val t = @{term "3 / 2 :: real"};
3.23 val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t ""
3.24
4.1 --- a/test/Tools/isac/Test_Some.thy Sun Aug 22 14:28:38 2021 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 23 12:33:10 2021 +0200
4.3 @@ -1058,7 +1058,7 @@
4.4 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
4.5 \<close> ML \<open>
4.6 (*EP- 16*)
4.7 -val fmz = ["equality (x + 2*x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
4.8 +val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
4.9 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
4.10 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
4.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.12 @@ -1071,59 +1071,277 @@
4.13 (*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
4.14 (*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
4.15 \<close> ML \<open>
4.16 -\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
4.17 -Rewrite.trace_on := true; (*false true*)
4.18 +Rewrite.trace_on := false; (*false true*)
4.19 +\<close> text \<open> (* *)
4.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
4.21 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
4.22 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
4.23 \<close> ML \<open>
4.24 + val (pt, p) =
4.25 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
4.26 + case Step.by_tactic tac (pt, p) of
4.27 + ("ok", (_, _, ptp)) => ptp
4.28 + | ("unsafe-ok", (_, _, ptp)) => ptp
4.29 + | ("not-applicable",_) => (pt, p)
4.30 + | ("end-of-calculation", (_, _, ptp)) => ptp
4.31 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
4.32 + | _ => raise ERROR "me: uncovered case Step.by_tactic"
4.33 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.34 + (*case*)
4.35 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.36 \<close> ML \<open>
4.37 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
4.38 \<close> ML \<open>
4.39 -\<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml*)
4.40 -fun trace_calc0 str =
4.41 - if ! trace_on then writeln ("### " ^ str) else ()
4.42 -fun trace_calc1 str1 str2 =
4.43 - if ! trace_on then writeln (str1 ^ str2) else ()
4.44 -fun trace_calc2 str term popt =
4.45 - if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
4.46 -fun trace_calc3 str term =
4.47 - if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
4.48 -fun trace_calc4 str t1 t2 =
4.49 - if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
4.50 + (*if*) Pos.on_calc_end ip (*else*);
4.51 \<close> ML \<open>
4.52 -fun get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
4.53 - (trace_calc1 "1.. get_pair: binop = " op_;
4.54 - if op_ = op0 then
4.55 - let
4.56 - val popt = ef op_ t thy
4.57 - val _ = trace_calc2 "2.. get_pair: " t popt
4.58 - in case popt of SOME _ => popt | NONE =>
4.59 - let
4.60 - val popt = get_pair thy op_ ef t1
4.61 - val _ = trace_calc2 "3.. get_pair: " t1 popt
4.62 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
4.63 - end
4.64 - else (* search subterms *)
4.65 - let
4.66 - val popt = get_pair thy op_ ef t1
4.67 - val _ = trace_calc2 "4.. get_pair: " t popt
4.68 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
4.69 - | get_pair _ _ _ _ = NONE
4.70 + val (_, probl_id, _) = Calc.references (pt, p);
4.71 \<close> ML \<open>
4.72 +val _ =
4.73 + (*case*) tacis (*of*);
4.74 \<close> ML \<open>
4.75 -\<close> ML \<open> (* \<longrightarrow> src/../evaluate.sml*)
4.76 -fun adhoc_thm thy (op_, eval_fn) t =
4.77 - case get_pair thy op_ eval_fn t of
4.78 - NONE => NONE
4.79 - | SOME (thmid, t') =>
4.80 - if t = (Prog_Expr.rhs o HOLogic.dest_Trueprop) t'
4.81 - then NONE (*^^^ can result from eval_cancel: see test -- fun adhoc_thm + fun eval_cancel --*)
4.82 - else SOME (thmid, Skip_Proof.make_thm thy t');
4.83 + (*if*) probl_id = Problem.id_empty (*else*);
4.84 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.85 + switch_specify_solve p_ (pt, ip);
4.86 +\<close> ML \<open>
4.87 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.88 +\<close> ML \<open>
4.89 + (*if*) Pos.on_specification ([], state_pos) (*else*);
4.90 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.91 + LI.do_next (pt, input_pos)
4.92 +\<close> ML \<open>
4.93 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
4.94 +\<close> ML \<open>
4.95 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
4.96 +\<close> ML \<open>
4.97 + val thy' = get_obj g_domID pt (par_pblobj pt p);
4.98 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
4.99 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.100 + (*case*)
4.101 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
4.102 +\<close> ML \<open>
4.103 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) =
4.104 + (sc, (pt, pos), ist, ctxt);
4.105 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.106 + (*case*)
4.107 + LI.scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist)
4.108 +\<close> ML \<open>
4.109 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
4.110 + ((prog, (ptp, ctxt)), (Pstate ist));
4.111 +\<close> ML \<open>
4.112 + (*if*) path = [] (*else*);
4.113 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.114 + go_scan_up (prog, cc) (trans_scan_up ist)
4.115 +\<close> ML \<open>
4.116 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
4.117 + ((prog, cc), (trans_scan_up ist));
4.118 +\<close> ML \<open>
4.119 + (*if*) path = [R] (*else*);
4.120 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.121 + scan_up pcc (ist |> path_up) (go_up path sc)
4.122 +\<close> ML \<open>
4.123 +"~~~~~ and scan_up , args:"; val (pcc, ist,(Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ )) =
4.124 + (pcc, (ist |> path_up), (go_up path sc));
4.125 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
4.126 + go_scan_up pcc ist
4.127 +\<close> ML \<open>
4.128 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
4.129 + (pcc, ist);
4.130 +\<close> ML \<open>
4.131 + (*if*) path = [R] (*else*);
4.132 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.133 + scan_up pcc (ist |> path_up) (go_up path sc)
4.134 +\<close> ML \<open>
4.135 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) =
4.136 + (pcc, (ist |> path_up), (go_up path sc));
4.137 +\<close> ML \<open>
4.138 + val e2 = check_Seq_up ist sc;
4.139 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.140 + (*case*)
4.141 + scan_dn cc (ist |> path_up_down [R]) e2 (*of*);
4.142 +\<close> ML \<open>
4.143 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) =
4.144 + (cc, (ist |> path_up_down [R]), e2);
4.145 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.146 + (*case*)
4.147 + scan_dn cc (ist |> path_down [L, R]) e1 (*of*);
4.148 +\<close> ML \<open>
4.149 +"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e)) =
4.150 + (cc, (ist |> path_down [L, R]), e1);
4.151 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.152 + (*case*)
4.153 + scan_dn cc (ist |> path_down [R]) e (*of*);
4.154 +\<close> ML \<open>
4.155 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) =
4.156 + (cc, (ist |> path_down [R]), e);
4.157 +\<close> ML \<open>
4.158 + (*if*) Tactical.contained_in t (*else*);
4.159 +\<close> ML \<open>
4.160 +val (Program.Tac prog_tac, form_arg) = (*case*)
4.161 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
4.162 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.163 + check_tac cc ist (prog_tac, form_arg)
4.164 +\<close> ML \<open>
4.165 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
4.166 + (cc, ist, (prog_tac, form_arg));
4.167 +\<close> ML \<open>
4.168 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
4.169 +\<close> ML \<open>
4.170 +val _ = (*case*) m (*of*);
4.171 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.172 + (*case*)
4.173 +Solve_Step.check m (pt, p) (*of*);
4.174 +\<close> ML \<open>
4.175 +"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, (p, _)))) =
4.176 + (m, (pt, p));
4.177 +\<close> ML \<open>
4.178 + val pp = Ctree.par_pblobj pt p;
4.179 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
4.180 + val f = Calc.current_formula cs;
4.181 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.182 + (*case*)
4.183 + Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f (*of*);
4.184 +\<close> ML \<open>
4.185 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) =
4.186 + ((ThyC.get_theory thy'), false, (assoc_rls rls), f);
4.187 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.188 + rewrite__set_ thy 1 bool [] rls term;
4.189 +\<close> ML \<open>
4.190 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
4.191 + (thy, 1, bool, [], rls, term);
4.192 +\<close> ML \<open>
4.193 +\<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml *)
4.194 +(*//-------------------------------- cp fromewrite.sml-----------------------------------------\\*)
4.195 +\<close> ML \<open>
4.196 +fun msg call thy op_ thmC t =
4.197 + call ^ ": \n" ^
4.198 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
4.199 + "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
4.200 +\<close> ML \<open>
4.201 + (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
4.202 + datatype switch = Appl | Noap;
4.203 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
4.204 + | rew_once ruls asm ct Appl [] =
4.205 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
4.206 + | Rule_Set.Sequence _ => (ct, asm)
4.207 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
4.208 + | rew_once ruls asm ct apno (rul :: thms) =
4.209 + case rul of
4.210 + Rule.Thm (thmid, thm) =>
4.211 + (trace_in1 i "try thm" thmid;
4.212 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.213 + ((#erls o Rule_Set.rep) rls) put_asm thm ct of
4.214 + NONE => rew_once ruls asm ct apno thms
4.215 + | SOME (ct', asm') =>
4.216 + (trace_in2 i "rewrites to" thy ct';
4.217 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
4.218 + (* once again try the same rule, e.g. associativity against "()"*)
4.219 + | Rule.Eval (cc as (op_, _)) =>
4.220 + let val _ = trace_in1 i "try calc" op_;
4.221 + in case Eval.adhoc_thm thy cc ct of
4.222 + NONE => rew_once ruls asm ct apno thms
4.223 + | SOME (_, thm') =>
4.224 + let
4.225 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.226 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
4.227 + val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct)
4.228 + val _ = trace_in3 i "calc. to" thy pairopt;
4.229 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
4.230 + end
4.231 + | Rule.Cal1 (cc as (op_, _)) =>
4.232 + let val _ = trace_in1 i "try cal1" op_;
4.233 + in case Eval.adhoc_thm1_ thy cc ct of
4.234 + NONE => (ct, asm)
4.235 + | SOME (_, thm') =>
4.236 + let
4.237 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.238 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
4.239 + val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
4.240 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
4.241 + val _ = trace_in3 i "cal1. to" thy pairopt;
4.242 + in the pairopt end
4.243 + end
4.244 + | Rule.Rls_ rls' =>
4.245 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
4.246 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
4.247 + | NONE => rew_once ruls asm ct apno thms)
4.248 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
4.249 +(*\\------------------------------- cp from rewrite.sml---------------------------------------//*)
4.250 +\<close> ML \<open>
4.251 + val ruls = (#rules o Rule_Set.rep) rls;
4.252 +\<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.253 +Rewrite.trace_on := false; (*false rew_once-3-isa.txt true*)
4.254 + val (ct', asm') =
4.255 + rew_once ruls [] ct Noap ruls;
4.256 +\<close> ML \<open>
4.257 +(*+*)UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
4.258 +\<close> ML \<open>
4.259 +(*+*)rls;(*val it =
4.260 + Repeat
4.261 + {calc =
4.262 + [("PLUS", ("Groups.plus_class.plus", fn)), ("MINUS", ("Groups.minus_class.minus", fn)), ("TIMES", ("Groups.times_class.times", fn)),
4.263 + ("DIVIDE", ("Rings.divide_class.divide", fn)), ("SQRT", ("NthRoot.sqrt", fn)), ("POWER", ("Transcendental.powr", fn))],
4.264 + ======^^^^^^======
4.265 + erls = ------------------------------ id = "calc_rat_erls" ------------------------------------------------------vvvvvvvvvvvvvvvvvvvv
4.266 + Repeat
4.267 + {calc = [("DIVIDE", ("Rings.divide_class.divide", fn))], erls =
4.268 + ======^^^^^^======
4.269 + Repeat
4.270 + {calc = [("matches", ("Prog_Expr.matches", fn)), ("equal", ("HOL.eq", fn)), ("is_num", ("Prog_Expr.is_num", fn))], erls = Empty, errpatts = [], id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", fn),
4.271 + rules = [Eval ("Prog_Expr.matches", fn), Eval ("HOL.eq", fn), Eval ("Prog_Expr.is_num", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True")], scr = Empty_Prog, srls = Empty},
4.272 + errpatts = [], id = "PolyEq_erls", <<<------------------------------------- "PolyEq_erls"
4.273 + preconds = [], rew_ord = ("dummy_ord", fn), rules =
4.274 + [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Eval ("Transcendental.powr", fn), Eval ("Groups.times_class.times", fn), Eval ("Groups.minus_class.minus", fn), Eval ("Groups.plus_class.plus", fn),
4.275 + Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.occurs_in", fn), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.ident", fn),
4.276 + Eval ("Orderings.ord_class.less_eq", fn), Eval ("Orderings.ord_class.less", fn), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("order_refl", "?x \<le> ?x"), Thm ("refl", "?t = ?t"),
4.277 + Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("not_false", "(\<not> False) = True"),
4.278 + Thm ("not_true", "(\<not> True) = False"), Thm ("mult_cross2", "?d \<noteq> 0 \<Longrightarrow> (?a = ?c / ?d) = (?a * ?d = ?c)"), Thm ("mult_cross1", "?b \<noteq> 0 \<Longrightarrow> (?a / ?b = ?c) = (?a = ?b * ?c)"),
4.279 + Thm ("mult_cross", "?b \<noteq> 0 \<Longrightarrow> ?d \<noteq> 0 \<Longrightarrow> (?a / ?b = ?c / ?d) = (?a * ?d = ?b * ?c)"), Thm ("rat_power", "(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"), Thm ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"),
4.280 + Thm ("real_divide_divide1", "?y \<noteq> 0 \<Longrightarrow> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"), Thm ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"),
4.281 + Thm ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"), Thm ("rat_mult", "?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"),
4.282 + Thm ("rat_add3", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a + ?b / ?c = (?a * ?c + ?b) / ?c"), Thm ("rat_add2", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"),
4.283 + Thm ("rat_add1", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a / ?c + ?b / ?c = (?a + ?b) / ?c"),
4.284 + Thm ("rat_add", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?d is_num \<Longrightarrow> ?a / ?c + ?b / ?d = (?a * ?d + ?b * ?c) / (?c * ?d)"), Thm ("sym_minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
4.285 + Eval ("Rings.divide_class.divide", fn), Eval ("HOL.eq", fn), Thm ("plus_leq", "(0 \<le> ?a + ?b) = (- 1 * ?b \<le> ?a)"), Thm ("minus_leq", "(0 \<le> ?a - ?b) = (?b \<le> ?a)"),
4.286 + ======^^^^^^======
4.287 + Thm ("rat_leq1", "0 \<noteq> ?b \<Longrightarrow> 0 \<noteq> ?d \<Longrightarrow> (?a / ?b \<le> ?c / ?d) = (?a * ?d \<le> ?b * ?c)"), Thm ("rat_leq2", "0 \<noteq> ?d \<Longrightarrow> (?a \<le> ?c / ?d) = (?a * ?d \<le> ?c)"),
4.288 + Thm ("rat_leq3", "0 \<noteq> ?b \<Longrightarrow> (?a / ?b \<le> ?c) = (?a \<le> ?b * ?c)")],
4.289 + scr = Empty_Prog, srls = Empty},
4.290 + errpatts = [], id = "polyeq_simplify", <<<------------------------------- "polyeq_simplify"
4.291 + preconds = [], rew_ord = ("termlessI", fn), rules =
4.292 + [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"),
4.293 + 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),
4.294 + Eval ("Groups.times_class.times", fn), Eval ("Rings.divide_class.divide", fn), Eval ("NthRoot.sqrt", fn), Eval ("Transcendental.powr", fn),
4.295 + ======^^^^^^======
4.296 + Rls_
4.297 + (
4.298 + Repeat
4.299 + {calc = [], erls =
4.300 + Repeat ---------vvvvvvvvvvvvvvvvvvvvvvvvv------------------
4.301 + {calc = [], erls = Empty, errpatts = [], id = "erls_in_reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules =
4.302 + [Eval ("Prog_Expr.is_num", fn), Thm ("not_false", "(\<not> False) = True"), Thm ("not_true", "(\<not> True) = False")], scr = Empty_Prog, srls = Empty},
4.303 + errpatts = [], id = "reduce_012", <<<---------------------------------- "reduce_012"
4.304 + preconds = [], rew_ord = ("dummy_ord", fn), rules =
4.305 + [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"),
4.306 + 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")],
4.307 + scr = Empty_Prog, srls = Empty}
4.308 + )],
4.309 + scr = Empty_Prog, srls = Empty}: id =
4.310 + Rule_Def.rule_set*)
4.311 +\<close> ML \<open>
4.312 +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) =
4.313 + (ruls, [], ct, Noap, ruls);
4.314 +\<close> ML \<open>
4.315 +val Rule.Thm (thmid, thm) =
4.316 + (*case*) rul (*of*);
4.317 +\<close> ML \<open>
4.318 +val NONE = (*case*) rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.319 + ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
4.320 +\<close> ML \<open>
4.321 +(* GOON: find a way to find out, why test -- fun adhoc_thm + fun eval_cancel -- gives
4.322 + Eval.adhoc_thm \<longrightarrow> NONE and above we have ERROR
4.323 +(*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*)
4.324
4.325 -\<close> ML \<open> (* \<longrightarrow> test/../evaluate.sml, BELOW.vv*)
4.326 -"----------- fun adhoc_thm: examples -----------------------------------------------------------";
4.327 -
4.328 -
4.329 -
4.330 + *)
4.331 \<close> ML \<open>
4.332 \<close> ML \<open>
4.333 \<close> ML \<open>
4.334 @@ -1138,6 +1356,125 @@
4.335 \<close> ML \<open>
4.336 \<close> ML \<open>
4.337 \<close> ML \<open>
4.338 +\<close> ML \<open>
4.339 +\<close> ML \<open>
4.340 +\<close> ML \<open>
4.341 +\<close> ML \<open>
4.342 +\<close> ML \<open>
4.343 +\<close> ML \<open>
4.344 +\<close> ML \<open>
4.345 +\<close> ML \<open>
4.346 +\<close> ML \<open>
4.347 +\<close> ML \<open>
4.348 +\<close> ML \<open>
4.349 +\<close> ML \<open>
4.350 +\<close> ML \<open>
4.351 +(*/------------------------------- fun rew_once ITERATED BY HAND -----------------------------\*)
4.352 +\<close> ML \<open>
4.353 +UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
4.354 +\<close> ML \<open>
4.355 +val thm = Rule.thm (nth 1 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
4.356 +\<close> ML \<open>
4.357 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.358 + ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
4.359 +\<close> ML \<open>
4.360 +val thm = Rule.thm (nth 2 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"
4.361 + ATTENTION "real_assoc_1" == "real_assoc_2"*)
4.362 +\<close> ML \<open>
4.363 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.364 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.365 +\<close> ML \<open>
4.366 +val thm = Rule.thm (nth 3 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
4.367 +\<close> ML \<open>
4.368 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.369 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.370 +\<close> ML \<open>
4.371 +UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 - 0)) / (2 * 2)"
4.372 +\<close> ML \<open>
4.373 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.374 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.375 +\<close> ML \<open>
4.376 +UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
4.377 +\<close> ML \<open>
4.378 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.379 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.380 +\<close> ML \<open>
4.381 +UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
4.382 +\<close> ML \<open>
4.383 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.384 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.385 +\<close> ML \<open>
4.386 +val thm = Rule.thm (nth 4 ruls); (* = "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"*)
4.387 +\<close> ML \<open>
4.388 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.389 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.390 +\<close> ML \<open>
4.391 +val thm = Rule.thm (nth 5 ruls); (* = "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"*)
4.392 +\<close> ML \<open>
4.393 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.394 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
4.395 +\<close> ML \<open> (* \<longrightarrow> Rule.*)
4.396 +\<close> ML \<open>
4.397 +val (cc as (op_, _)) = Rule.eval (nth 6 ruls); (* = "Groups.plus_class.plus"*)
4.398 +\<close> ML \<open>
4.399 +val NONE = Eval.adhoc_thm thy cc ct
4.400 +\<close> ML \<open>
4.401 +val (cc as (op_, _)) = Rule.eval (nth 7 ruls); (* = "Groups.minus_class.minus"*)
4.402 +\<close> ML \<open>
4.403 +val NONE = Eval.adhoc_thm thy cc ct
4.404 +\<close> ML \<open>
4.405 +val (cc as (op_, _)) = Rule.eval (nth 8 ruls); (* = "Groups.times_class.times"*)
4.406 +\<close> ML \<open>
4.407 +val SOME (_, thm') = Eval.adhoc_thm thy cc ct
4.408 +\<close> ML \<open>
4.409 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.410 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
4.411 +\<close> ML \<open>
4.412 + "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)";
4.413 +UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
4.414 +\<close> ML \<open>
4.415 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.416 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
4.417 +\<close> ML \<open>
4.418 +UnparseC.term ct = "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
4.419 +\<close> ML \<open>
4.420 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.421 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
4.422 +\<close> ML \<open>
4.423 +val (cc as (op_, _)) = Rule.eval (nth 9 ruls); (* = "Rings.divide_class.divide"*)
4.424 +\<close> ML \<open>
4.425 +val NONE = Eval.adhoc_thm thy cc ct
4.426 +\<close> ML \<open>
4.427 +val (cc as (op_, _)) = Rule.eval (nth 10 ruls); (* = "NthRoot.sqrt"*)
4.428 +\<close> ML \<open>
4.429 +val NONE = Eval.adhoc_thm thy cc ct
4.430 +\<close> ML \<open>
4.431 +val (cc as (op_, _)) = Rule.eval (nth 11 ruls); (* = "Transcendental.powr"*)
4.432 +\<close> ML \<open>
4.433 +val NONE = Eval.adhoc_thm thy cc ct
4.434 +\<close> ML \<open>
4.435 +val rls' = Rule.rls (nth 12 ruls); (* = "reduce_012"*)
4.436 +\<close> ML \<open>
4.437 +val SOME (ct, []) = rewrite__set_ thy (i + 1) put_asm bdv rls' ct
4.438 +\<close> ML \<open>
4.439 + "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)";
4.440 +UnparseC.term ct = "x = (- 1 + sqrt 1) / (2 * 2) \<or> x = (- 1 + - 1 * sqrt 1) / (2 * 2)"
4.441 +\<close> ML \<open>
4.442 +length ruls = 12;
4.443 +(*========== now are further iterations to come, and there is the strange error ===============*)
4.444 +\<close> ML \<open>
4.445 +\<close> ML \<open>
4.446 +\<close> ML \<open>
4.447 +\<close> ML \<open>
4.448 +\<close> ML \<open>
4.449 +\<close> ML \<open>
4.450 +\<close> ML \<open>
4.451 +\<close> ML \<open>
4.452 +\<close> ML \<open>
4.453 +\<close> ML \<open>
4.454 +\<close> ML \<open>
4.455 +\<close> ML \<open>
4.456 +\<close> ML \<open>
4.457 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
4.458 \<close> text \<open>
4.459 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;