1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Thu Dec 22 10:27:12 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Thu Dec 22 17:06:19 2022 +0100
1.3 @@ -15,6 +15,7 @@
1.4 val id: Rule_Def.rule -> string
1.5 val equal: Rule_Def.rule * Rule_Def.rule -> bool
1.6 val to_string: Rule_Def.rule -> string
1.7 + val to_string_PIDE: Proof.context -> rule -> string
1.8 val to_string_short: Rule_Def.rule -> string
1.9 val s_to_string: rule list -> string
1.10
1.11 @@ -57,16 +58,14 @@
1.12 | equal _ = false;
1.13 fun distinct' rs = distinct equal rs
1.14
1.15 +fun to_string_PIDE _ Rule_Def.Erule = "Erule"
1.16 + | to_string_PIDE ctxt (Rule_Def.Thm (str, thm)) =
1.17 + "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")"
1.18 + | to_string_PIDE _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
1.19 + | to_string_PIDE _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
1.20 + | to_string_PIDE _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
1.21 fun to_string Rule_Def.Erule = "Erule"
1.22 - | to_string (Rule_Def.Thm (str, thm)) =
1.23 -(** )
1.24 - let
1.25 - val thy = Know_Store.get_ref_last_thy () ! ! !Know_Store defined later ! ! !
1.26 - in
1.27 -( **)
1.28 - "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
1.29 -(** )end( **)
1.30 -
1.31 + | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
1.32 | to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
1.33 | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
1.34 | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
2.1 --- a/src/Tools/isac/Build_Isac.thy Thu Dec 22 10:27:12 2022 +0100
2.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Dec 22 17:06:19 2022 +0100
2.3 @@ -192,264 +192,7 @@
2.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/710-interSteps-short.sml"
2.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
2.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
2.7 -(** )
2.8 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
2.9 -( **)
2.10 -ML \<open>
2.11 -\<close> ML \<open>
2.12 -\<close> ML \<open>
2.13 -(* Title: "Minisubpbl/800-append-on-Frm.sml"
2.14 - Author: Walther Neuper
2.15 - (c) copyright due to lincense terms.
2.16 -*)
2.17 -
2.18 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
2.19 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
2.20 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
2.21 -(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
2.22 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
2.23 -val (dI',pI',mI') =
2.24 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
2.25 - ["Test", "squ-equ-test-subpbl1"]);
2.26 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];(*Model_Problem*)
2.27 - (*autoCalculate 1 CompleteCalcHead;*)
2.28 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
2.29 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
2.30 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
2.31 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
2.32 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
2.33 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
2.34 - (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
2.35 -
2.36 -\<close> ML \<open>
2.37 - (*autoCalculate 1 (Steps 1);*)
2.38 - (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
2.39 -
2.40 -(*+*)Test_Tool.show_pt_tac pt; (*isa==REP [
2.41 -([], Frm), solve (x + 1 = 2, x)
2.42 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
2.43 -([1], Frm), x + 1 = 2
2.44 -. . . . . . . . . . Empty_Tac] *)
2.45 -
2.46 - (*appendFormula 1 "2+ - 1 + x = 2";*)
2.47 -"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ - 1 + x = 2");
2.48 - val cs = (*States.get_calc cI*) ((pt, p), []) (*..continue fun me*)
2.49 - val pos = (*States.get_pos cI 1*) p (*..continue fun me*)
2.50 -
2.51 - val ("ok", cs' as (_, _, ptp''''')) = (*case*)
2.52 - Step.do_next pos cs (*of*);
2.53 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
2.54 - val pIopt = Ctree.get_pblID (pt, ip);
2.55 - (*if*) ip = ([], Pos.Res) (*else*);
2.56 - val _ = (*case*) tacis (*of*);
2.57 - val SOME _ = (*case*) pIopt (*of*);
2.58 -
2.59 - Step.switch_specify_solve p_ (pt, ip);
2.60 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
2.61 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
2.62 -
2.63 - LI.do_next (pt, input_pos);
2.64 -"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
2.65 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
2.66 - val thy' = get_obj g_domID pt (par_pblobj pt p);
2.67 - val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
2.68 -
2.69 -\<close> ML \<open>
2.70 -val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
2.71 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
2.72 -
2.73 -(*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =
2.74 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
2.75 -"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
2.76 - val pos = next_in_prog' pos;
2.77 -
2.78 - (** )val (pos', c, _, pt) =( **)
2.79 - Step.add tac_ is (pt, pos);
2.80 -"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
2.81 - = (tac_, is, (pt, pos));
2.82 -(*+*)pos = ([1], Frm);
2.83 -
2.84 - (** )val (pt, c) =( **)
2.85 - cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
2.86 - (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;
2.87 -"~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
2.88 - = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
2.89 - (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);
2.90 - (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
2.91 - val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
2.92 - val (pt, cs) = cut_tree(*!*)pt (p, Frm);
2.93 - (** )val pt = ( **)
2.94 - append_atomic p (SOME ic_form, ic_res) f r f' s pt;
2.95 -"~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
2.96 - = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
2.97 - (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);
2.98 - val (iss, f) =
2.99 - ((ic_form, SOME ic_res), f); (*return from if*)
2.100 -
2.101 -\<close> ML \<open>
2.102 - insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
2.103 - result = f', ostate = s}) pt p (*return from append_atomic*);
2.104 -"~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)
2.105 - = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
2.106 - result = f', ostate = s}) pt p);
2.107 -
2.108 -\<close> text \<open>
2.109 -(*/--------------------- step into Deriv.embed -----------------------------------------------\*)
2.110 - val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
2.111 - (*case*)
2.112 -\<close> text \<open>
2.113 -Step_Solve.by_term ptp (encode ifo) (*of*);
2.114 -\<close> ML \<open>
2.115 -"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
2.116 - val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
2.117 - val pos_pred = lev_back(*'*) pos
2.118 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
2.119 - val f_succ = Ctree.get_curr_formula (pt, pos);
2.120 - (*if*) f_succ = f_in (*else*);
2.121 - val NONE =(*case*) CAS_Cmd.input f_in (*of*);
2.122 -
2.123 -\<close> text \<open>
2.124 - (*case*)
2.125 - LI.locate_input_term (pt, pos) f_in (*of*);
2.126 -\<close> ML \<open>
2.127 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
2.128 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
2.129 - val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);
2.130 -
2.131 -\<close> text \<open>
2.132 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
2.133 -\<close> ML \<open>
2.134 -"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
2.135 - val fo = Calc.current_formula ptp
2.136 - val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
2.137 - val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls
2.138 -
2.139 -\<close> text \<open>
2.140 - val (found, der) =
2.141 - Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
2.142 -\<close> ML \<open> (*//----------- step into Derive.steps ----------------------------------------------\\*)
2.143 -(*//------------------ step into Derive.steps ----------------------------------------------\\*)
2.144 -"~~~~~ fun steps , args:"; val (ctxt, rew_ord, asm_rls, rules, fo, ifo) =
2.145 - (ctxt, rew_ord, asm_rls, rules, fo, ifo);
2.146 -\<close> ML \<open>
2.147 - fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
2.148 - | derivat dt = (#1 o #3 o last_elem) dt
2.149 - fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
2.150 - val fod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo
2.151 - val ifod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo
2.152 -\<close> ML \<open>
2.153 -val (fod, ifod) =
2.154 - (*case*) (fod, ifod) (*of*);
2.155 -\<close> ML \<open>
2.156 - (*if*) derivat fod = derivat ifod (*common normal form found*) (*then*);
2.157 -\<close> ML \<open>
2.158 - val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
2.159 -\<close> ML \<open>
2.160 -(*/--- local to steps ---\*)
2.161 -fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
2.162 -(*\--- local to steps ---/*)
2.163 -\<close> text \<open>
2.164 -val return = (true, fod' @ (map rev_deriv' rifod'))
2.165 -\<close> ML \<open>
2.166 -\<close> ML \<open>
2.167 -\<close> ML \<open>
2.168 -\<close> ML \<open>
2.169 -\<close> ML \<open>
2.170 -\<close> ML \<open>
2.171 -\<close> ML \<open>
2.172 -(*keep for continuing compare_step*)
2.173 -\<close> ML \<open> (*------------- continuing Derive.steps -----------------------------------------------*)
2.174 -(*-------------------- continuing Derive.steps -----------------------------------------------*)
2.175 -(*kept for continuing compare_step*)
2.176 -(*-------------------- stop step into Derive.steps -------------------------------------------*)
2.177 -\<close> ML \<open> (*------------- stop step into Derive.steps -------------------------------------------*)
2.178 -(*\\------------------ step into Derive.steps ----------------------------------------------//*)
2.179 -\<close> text \<open> (*\\----------- step into Derive.steps ----------------------------------------------//*)
2.180 - (*if*) found (*then*);
2.181 - val tacis' = map (State_Steps.make_single rew_ord asm_rls) der;
2.182 -
2.183 - val (c', ptp) =
2.184 - Derive.embed tacis' ptp;
2.185 -"~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
2.186 - val (res, asm) = (State_Steps.result o last_elem) tacis
2.187 - val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
2.188 - (_, SOME (ist, ctxt)) => (ist, ctxt)
2.189 - | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
2.190 - val (f, _) = Ctree.get_obj Ctree.g_result pt p
2.191 - val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
2.192 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
2.193 - (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
2.194 - (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
2.195 - val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
2.196 - val (pt, c, pos as (p, _)) =
2.197 -
2.198 -Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
2.199 -"~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
2.200 -(*+*)length tacis = 8;
2.201 -(*+*)if State_Steps.to_string ctxt tacis = "[\"\n" ^
2.202 - "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^
2.203 - "(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true) ))\", \"\n" ^
2.204 - "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 6], Res), Uistate ))\", \"\n" ^
2.205 - "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 5], Res), Uistate ))\", \"\n" ^
2.206 - "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2, 4], Res), Uistate ))\", \"\n" ^
2.207 - "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 3], Res), Uistate ))\", \"\n" ^
2.208 - "( Rewrite (\"#: 1 + x = - 1 + (2 + x)\", \"1 + x = - 1 + (2 + x)\"), Rewrite' , ( ([2, 2], Res), Uistate ))\", \"\n" ^
2.209 - "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2, 1], Res), Uistate ))\", \"\n" ^
2.210 - "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
2.211 -(*+*)then () else error "Derive.embed CHANGED";
2.212 -
2.213 - val (tacis', (_, tac_, (p, is))) = split_last tacis
2.214 -
2.215 -(*+*)val Begin_Trans' _ = tac_;
2.216 -
2.217 - val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p)
2.218 -(*-------------------- stop step into -------------------------------------------------------*)
2.219 -(*\------------------- end step into -------------------------------------------------------/*)
2.220 -
2.221 -(*/--------------------- final test ----------------------------------------------------------\*)
2.222 -val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
2.223 -;
2.224 -if
2.225 - (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[\"precond_rootmet x\"]"
2.226 - andalso
2.227 - (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[\"precond_rootmet x\"]"
2.228 - andalso
2.229 - Istate.string_of ist_res =
2.230 - "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"
2.231 -then () else error "/800-append-on-Frm.sml CHANGED";
2.232 -
2.233 -Test_Tool.show_pt_tac (fst ptp''''');(*[
2.234 -([], Frm), solve (x + 1 = 2, x)
2.235 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
2.236 -([1], Frm), x + 1 = 2
2.237 -. . . . . . . . . . Derive Test_simplify,
2.238 -([1,1], Frm), x + 1 = 2
2.239 -. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
2.240 -([1,1], Res), 1 + x = 2
2.241 -. . . . . . . . . . Rewrite ("#: 1 + x = - 1 + (2 + x)", "1 + x = - 1 + (2 + x)"),
2.242 -([1,2], Res), - 1 + (2 + x) = 2
2.243 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
2.244 -([1,3], Res), - 1 + (x + 2) = 2
2.245 -. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
2.246 -([1,4], Res), x + (- 1 + 2) = 2
2.247 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
2.248 -([1,5], Res), x + (2 + - 1) = 2
2.249 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
2.250 -([1,6], Res), 2 + - 1 + x = 2
2.251 -. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
2.252 -([1], Res), 2 + - 1 + x = 2
2.253 -. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]
2.254 -*)
2.255 -
2.256 -Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
2.257 -
2.258 -
2.259 -\<close> ML \<open>
2.260 -\<close> ML \<open>
2.261 -\<close>
2.262 -(*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
2.263 -(**)\----- outcomment in order to intermediately check with Test_Isac.thy --------------/*)
2.264 -
2.265
2.266 text \<open>
2.267 show theory dependencies using the graph browser,
3.1 --- a/src/Tools/isac/Interpret/derive.sml Thu Dec 22 10:27:12 2022 +0100
3.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Dec 22 17:06:19 2022 +0100
3.3 @@ -24,7 +24,7 @@
3.4 \<^isac_test>\<open>
3.5 val trtas2str : Proof.context -> (term * Rule.rule * (term * term list)) list -> string
3.6 val deriv2str : Proof.context -> (term * Rule.rule * (term * term list)) list -> string
3.7 - val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
3.8 + val rev_deriv' : Proof.context -> 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
3.9 \<close>
3.10 end
3.11
3.12 @@ -108,17 +108,17 @@
3.13 (** concatenate several steps in revers order **)
3.14
3.15 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
3.16 -fun steps_reverse thy asm_rls rs ro goal t =
3.17 - (rev o (map rev_deriv)) (do_one thy asm_rls rs ro goal t)
3.18 +fun steps_reverse ctxt asm_rls rs ro goal t =
3.19 + (rev o (map rev_deriv)) (do_one ctxt asm_rls rs ro goal t)
3.20
3.21
3.22 (** concatenate several steps **)
3.23
3.24 -fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
3.25 +fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule_PIDE ctxt r, (t, a));
3.26
3.27 (* case fo = ifo excluded already in inform *)
3.28 fun steps ctxt rew_ord asm_rls rules fo ifo =
3.29 - let
3.30 + let
3.31 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
3.32 | derivat dt = (#1 o #3 o last_elem) dt
3.33 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
3.34 @@ -128,12 +128,12 @@
3.35 case (fod, ifod) of
3.36 ([], []) => if fo = ifo then (true, []) else (false, [])
3.37 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
3.38 - | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
3.39 + | ([], ifod) => if fo = derivat ifod then (true, ((map (rev_deriv' ctxt)) o rev) ifod) else (false, [])
3.40 | (fod, ifod) =>
3.41 if derivat fod = derivat ifod (*common normal form found*) then
3.42 let
3.43 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
3.44 - in (true, fod' @ (map rev_deriv' rifod')) end
3.45 + in (true, fod' @ (map (rev_deriv' ctxt) rifod')) end
3.46 else (false, [])
3.47 end
3.48
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 22 10:27:12 2022 +0100
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 22 17:06:19 2022 +0100
4.3 @@ -53,9 +53,10 @@
4.4 val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
4.5 val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
4.6 val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
4.7 + val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Calc.state_post
4.8
4.9 \<^isac_test>\<open>
4.10 - val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Calc.state_post
4.11 +(**)
4.12 \<close>
4.13 end
4.14
5.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Thu Dec 22 10:27:12 2022 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Thu Dec 22 17:06:19 2022 +0100
5.3 @@ -38,6 +38,7 @@
5.4 val string_of_thm_in_thy: theory -> thm -> string
5.5 val id_drop_sym: id -> id
5.6 \<close>
5.7 + val make_sym_rule_PIDE: Proof.context -> Rule.rule -> Rule.rule
5.8 val make_sym_rule: Rule.rule -> Rule.rule
5.9 val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
5.10 val sym_thm: thm -> thm
5.11 @@ -141,6 +142,16 @@
5.12 prepat = prepat, rew_ord = rew_ord}
5.13
5.14 (* toggles sym_* and keeps "#:" for ad-hoc theorems *)
5.15 +fun make_sym_rule_PIDE ctxt (Rule.Thm (thmID, thm)) =
5.16 + let
5.17 + val thm' = sym_thm thm
5.18 + val thmID' = case Symbol.explode thmID of
5.19 + "s" :: "y" :: "m" :: "_" :: id => implode id
5.20 + | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm'
5.21 + | _ => "sym_" ^ thmID
5.22 + in Rule.Thm (thmID', thm') end
5.23 + | make_sym_rule_PIDE _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
5.24 + | make_sym_rule_PIDE ctxt r = raise ERROR ("make_sym_rule: not for " ^ Rule.to_string_PIDE ctxt r)
5.25 fun make_sym_rule (Rule.Thm (thmID, thm)) =
5.26 let
5.27 val thm' = sym_thm thm
6.1 --- a/src/Tools/isac/Specify/specify-step.sml Thu Dec 22 10:27:12 2022 +0100
6.2 +++ b/src/Tools/isac/Specify/specify-step.sml Thu Dec 22 17:06:19 2022 +0100
6.3 @@ -166,14 +166,15 @@
6.4 in
6.5 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
6.6 end
6.7 - | add (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =
6.8 + | add (Tactic.Begin_Trans' t) l (pt, pos as (p, Frm)) =
6.9 let
6.10 val (pt, c) = Ctree.cappend_form pt p l t
6.11 val pt = Ctree.update_branch pt p Ctree.TransitiveB
6.12 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
6.13 val (pt, c') = Ctree.cappend_form pt p l t
6.14 + val ctxt = Ctree.get_ctxt pt pos
6.15 in
6.16 - ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
6.17 + ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt)
6.18 end
6.19 | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
6.20 let
7.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu Dec 22 10:27:12 2022 +0100
7.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu Dec 22 17:06:19 2022 +0100
7.3 @@ -129,7 +129,7 @@
7.4 (writeln o (Derive.trtas2str ctxt)) ifod;
7.5 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
7.6 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
7.7 - val der = fod' @ (map Derive.rev_deriv' rifod');
7.8 + val der = fod' @ (map (Derive.rev_deriv' ctxt) rifod');
7.9 (writeln o (Derive.trtas2str ctxt)) der;
7.10 "----------------------------------------------------------";
7.11 DEconstrCalcTree 1;
8.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu Dec 22 10:27:12 2022 +0100
8.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu Dec 22 17:06:19 2022 +0100
8.3 @@ -113,7 +113,41 @@
8.4 val fo = Calc.current_formula ptp
8.5 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
8.6 val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls
8.7 - val (found, der) = Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
8.8 +
8.9 + val (found, der) =
8.10 + Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
8.11 +(*//------------------ step into Derive.steps ----------------------------------------------\\*)
8.12 +"~~~~~ fun steps , args:"; val (ctxt, rew_ord, asm_rls, rules, fo, ifo) =
8.13 + (ctxt, rew_ord, asm_rls, rules, fo, ifo);
8.14 + fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
8.15 + | derivat dt = (#1 o #3 o last_elem) dt
8.16 + fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
8.17 + val fod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo
8.18 + val ifod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo
8.19 +val (fod, ifod) =
8.20 + (*case*) (fod, ifod) (*of*);
8.21 + (*if*) derivat fod = derivat ifod (*common normal form found*) (*then*);
8.22 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
8.23 +
8.24 +(*/--- local to steps ---\*)
8.25 +fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule_PIDE ctxt r, (t, a));
8.26 +(*\--- local to steps ---/*)
8.27 +val return = (true, fod' @ (map
8.28 + (rev_deriv' ctxt) rifod'));
8.29 +"~~~~~ fun rev_deriv' , args:"; val (ctxt, (t, r, (t', a))) = (ctxt, nth 1 rifod');
8.30 +
8.31 +val return = (t',
8.32 + ThmC.make_sym_rule_PIDE ctxt r, (t, a));
8.33 +"~~~~~ fun make_sym_rule_PIDE , args:"; val (ctxt ,(Rule.Thm (thmID, thm))) = (ctxt, r);
8.34 +open ThmC
8.35 + val thm' = sym_thm thm
8.36 + val thmID' = case Symbol.explode thmID of
8.37 + "s" :: "y" :: "m" :: "_" :: id => implode id
8.38 + | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm'
8.39 + | _ => "sym_" ^ thmID;
8.40 +(*-------------------- stop step into Derive.steps -------------------------------------------*)
8.41 +(*\\------------------ step into Derive.steps ----------------------------------------------//*)
8.42 +
8.43 (*if*) found (*then*);
8.44 val tacis' = map (State_Steps.make_single rew_ord asm_rls) der;
8.45
8.46 @@ -130,8 +164,8 @@
8.47 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
8.48 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
8.49 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
8.50 +
8.51 val (pt, c, pos as (p, _)) =
8.52 -
8.53 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
8.54 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
8.55 (*+*)length tacis = 8;
8.56 @@ -150,18 +184,26 @@
8.57 val (tacis', (_, tac_, (p, is))) = split_last tacis
8.58
8.59 (*+*)val Begin_Trans' _ = tac_;
8.60 -
8.61 - val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p)
8.62 (*-------------------- stop step into -------------------------------------------------------*)
8.63 (*\------------------- end step into -------------------------------------------------------/*)
8.64
8.65 + val (p',c',_,pt') =
8.66 +Specify_Step.add tac_ is (pt, p);
8.67 +"~~~~~ fun add , args:"; val ((Tactic.Begin_Trans' t), l, (pt, (p, Frm))) =
8.68 + (tac_, is, (pt, p));
8.69 + val (pt, c) = Ctree.cappend_form pt p l t
8.70 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
8.71 + val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
8.72 + val (pt, c') = Ctree.cappend_form pt p l t
8.73 +val return = ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt)
8.74 +
8.75 (*/--------------------- final test ----------------------------------------------------------\*)
8.76 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
8.77 ;
8.78 if
8.79 - (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"
8.80 + (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[precond_rootmet x]"
8.81 andalso
8.82 - (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"
8.83 + (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[precond_rootmet x]"
8.84 andalso
8.85 Istate.string_of ist_res =
8.86 "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"
8.87 @@ -190,5 +232,3 @@
8.88 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]
8.89 *)
8.90
8.91 -Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
8.92 -