1.1 --- a/src/Tools/isac/Build_Isac.thy Thu Dec 22 10:27:12 2022 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Dec 22 17:06:19 2022 +0100
1.3 @@ -192,264 +192,7 @@
1.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/710-interSteps-short.sml"
1.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
1.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
1.7 -(** )
1.8 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
1.9 -( **)
1.10 -ML \<open>
1.11 -\<close> ML \<open>
1.12 -\<close> ML \<open>
1.13 -(* Title: "Minisubpbl/800-append-on-Frm.sml"
1.14 - Author: Walther Neuper
1.15 - (c) copyright due to lincense terms.
1.16 -*)
1.17 -
1.18 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
1.19 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
1.20 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
1.21 -(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
1.22 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
1.23 -val (dI',pI',mI') =
1.24 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.25 - ["Test", "squ-equ-test-subpbl1"]);
1.26 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];(*Model_Problem*)
1.27 - (*autoCalculate 1 CompleteCalcHead;*)
1.28 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
1.29 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
1.30 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
1.31 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
1.32 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
1.33 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
1.34 - (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
1.35 -
1.36 -\<close> ML \<open>
1.37 - (*autoCalculate 1 (Steps 1);*)
1.38 - (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
1.39 -
1.40 -(*+*)Test_Tool.show_pt_tac pt; (*isa==REP [
1.41 -([], Frm), solve (x + 1 = 2, x)
1.42 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.43 -([1], Frm), x + 1 = 2
1.44 -. . . . . . . . . . Empty_Tac] *)
1.45 -
1.46 - (*appendFormula 1 "2+ - 1 + x = 2";*)
1.47 -"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ - 1 + x = 2");
1.48 - val cs = (*States.get_calc cI*) ((pt, p), []) (*..continue fun me*)
1.49 - val pos = (*States.get_pos cI 1*) p (*..continue fun me*)
1.50 -
1.51 - val ("ok", cs' as (_, _, ptp''''')) = (*case*)
1.52 - Step.do_next pos cs (*of*);
1.53 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
1.54 - val pIopt = Ctree.get_pblID (pt, ip);
1.55 - (*if*) ip = ([], Pos.Res) (*else*);
1.56 - val _ = (*case*) tacis (*of*);
1.57 - val SOME _ = (*case*) pIopt (*of*);
1.58 -
1.59 - Step.switch_specify_solve p_ (pt, ip);
1.60 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.61 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
1.62 -
1.63 - LI.do_next (pt, input_pos);
1.64 -"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
1.65 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.66 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.67 - val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
1.68 -
1.69 -\<close> ML \<open>
1.70 -val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
1.71 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.72 -
1.73 -(*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =
1.74 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
1.75 -"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
1.76 - val pos = next_in_prog' pos;
1.77 -
1.78 - (** )val (pos', c, _, pt) =( **)
1.79 - Step.add tac_ is (pt, pos);
1.80 -"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
1.81 - = (tac_, is, (pt, pos));
1.82 -(*+*)pos = ([1], Frm);
1.83 -
1.84 - (** )val (pt, c) =( **)
1.85 - cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
1.86 - (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;
1.87 -"~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
1.88 - = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
1.89 - (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);
1.90 - (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
1.91 - val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
1.92 - val (pt, cs) = cut_tree(*!*)pt (p, Frm);
1.93 - (** )val pt = ( **)
1.94 - append_atomic p (SOME ic_form, ic_res) f r f' s pt;
1.95 -"~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
1.96 - = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
1.97 - (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);
1.98 - val (iss, f) =
1.99 - ((ic_form, SOME ic_res), f); (*return from if*)
1.100 -
1.101 -\<close> ML \<open>
1.102 - insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
1.103 - result = f', ostate = s}) pt p (*return from append_atomic*);
1.104 -"~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)
1.105 - = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
1.106 - result = f', ostate = s}) pt p);
1.107 -
1.108 -\<close> text \<open>
1.109 -(*/--------------------- step into Deriv.embed -----------------------------------------------\*)
1.110 - val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
1.111 - (*case*)
1.112 -\<close> text \<open>
1.113 -Step_Solve.by_term ptp (encode ifo) (*of*);
1.114 -\<close> ML \<open>
1.115 -"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
1.116 - val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
1.117 - val pos_pred = lev_back(*'*) pos
1.118 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
1.119 - val f_succ = Ctree.get_curr_formula (pt, pos);
1.120 - (*if*) f_succ = f_in (*else*);
1.121 - val NONE =(*case*) CAS_Cmd.input f_in (*of*);
1.122 -
1.123 -\<close> text \<open>
1.124 - (*case*)
1.125 - LI.locate_input_term (pt, pos) f_in (*of*);
1.126 -\<close> ML \<open>
1.127 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
1.128 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.129 - val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);
1.130 -
1.131 -\<close> text \<open>
1.132 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
1.133 -\<close> ML \<open>
1.134 -"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
1.135 - val fo = Calc.current_formula ptp
1.136 - val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
1.137 - val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls
1.138 -
1.139 -\<close> text \<open>
1.140 - val (found, der) =
1.141 - Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
1.142 -\<close> ML \<open> (*//----------- step into Derive.steps ----------------------------------------------\\*)
1.143 -(*//------------------ step into Derive.steps ----------------------------------------------\\*)
1.144 -"~~~~~ fun steps , args:"; val (ctxt, rew_ord, asm_rls, rules, fo, ifo) =
1.145 - (ctxt, rew_ord, asm_rls, rules, fo, ifo);
1.146 -\<close> ML \<open>
1.147 - fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
1.148 - | derivat dt = (#1 o #3 o last_elem) dt
1.149 - fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
1.150 - val fod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo
1.151 - val ifod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo
1.152 -\<close> ML \<open>
1.153 -val (fod, ifod) =
1.154 - (*case*) (fod, ifod) (*of*);
1.155 -\<close> ML \<open>
1.156 - (*if*) derivat fod = derivat ifod (*common normal form found*) (*then*);
1.157 -\<close> ML \<open>
1.158 - val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
1.159 -\<close> ML \<open>
1.160 -(*/--- local to steps ---\*)
1.161 -fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
1.162 -(*\--- local to steps ---/*)
1.163 -\<close> text \<open>
1.164 -val return = (true, fod' @ (map rev_deriv' rifod'))
1.165 -\<close> ML \<open>
1.166 -\<close> ML \<open>
1.167 -\<close> ML \<open>
1.168 -\<close> ML \<open>
1.169 -\<close> ML \<open>
1.170 -\<close> ML \<open>
1.171 -\<close> ML \<open>
1.172 -(*keep for continuing compare_step*)
1.173 -\<close> ML \<open> (*------------- continuing Derive.steps -----------------------------------------------*)
1.174 -(*-------------------- continuing Derive.steps -----------------------------------------------*)
1.175 -(*kept for continuing compare_step*)
1.176 -(*-------------------- stop step into Derive.steps -------------------------------------------*)
1.177 -\<close> ML \<open> (*------------- stop step into Derive.steps -------------------------------------------*)
1.178 -(*\\------------------ step into Derive.steps ----------------------------------------------//*)
1.179 -\<close> text \<open> (*\\----------- step into Derive.steps ----------------------------------------------//*)
1.180 - (*if*) found (*then*);
1.181 - val tacis' = map (State_Steps.make_single rew_ord asm_rls) der;
1.182 -
1.183 - val (c', ptp) =
1.184 - Derive.embed tacis' ptp;
1.185 -"~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
1.186 - val (res, asm) = (State_Steps.result o last_elem) tacis
1.187 - val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
1.188 - (_, SOME (ist, ctxt)) => (ist, ctxt)
1.189 - | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
1.190 - val (f, _) = Ctree.get_obj Ctree.g_result pt p
1.191 - val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
1.192 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
1.193 - (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
1.194 - (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
1.195 - val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
1.196 - val (pt, c, pos as (p, _)) =
1.197 -
1.198 -Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
1.199 -"~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
1.200 -(*+*)length tacis = 8;
1.201 -(*+*)if State_Steps.to_string ctxt tacis = "[\"\n" ^
1.202 - "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^
1.203 - "(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true) ))\", \"\n" ^
1.204 - "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 6], Res), Uistate ))\", \"\n" ^
1.205 - "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 5], Res), Uistate ))\", \"\n" ^
1.206 - "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2, 4], Res), Uistate ))\", \"\n" ^
1.207 - "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 3], Res), Uistate ))\", \"\n" ^
1.208 - "( Rewrite (\"#: 1 + x = - 1 + (2 + x)\", \"1 + x = - 1 + (2 + x)\"), Rewrite' , ( ([2, 2], Res), Uistate ))\", \"\n" ^
1.209 - "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2, 1], Res), Uistate ))\", \"\n" ^
1.210 - "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
1.211 -(*+*)then () else error "Derive.embed CHANGED";
1.212 -
1.213 - val (tacis', (_, tac_, (p, is))) = split_last tacis
1.214 -
1.215 -(*+*)val Begin_Trans' _ = tac_;
1.216 -
1.217 - val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p)
1.218 -(*-------------------- stop step into -------------------------------------------------------*)
1.219 -(*\------------------- end step into -------------------------------------------------------/*)
1.220 -
1.221 -(*/--------------------- final test ----------------------------------------------------------\*)
1.222 -val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
1.223 -;
1.224 -if
1.225 - (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[\"precond_rootmet x\"]"
1.226 - andalso
1.227 - (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[\"precond_rootmet x\"]"
1.228 - andalso
1.229 - Istate.string_of ist_res =
1.230 - "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"
1.231 -then () else error "/800-append-on-Frm.sml CHANGED";
1.232 -
1.233 -Test_Tool.show_pt_tac (fst ptp''''');(*[
1.234 -([], Frm), solve (x + 1 = 2, x)
1.235 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.236 -([1], Frm), x + 1 = 2
1.237 -. . . . . . . . . . Derive Test_simplify,
1.238 -([1,1], Frm), x + 1 = 2
1.239 -. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.240 -([1,1], Res), 1 + x = 2
1.241 -. . . . . . . . . . Rewrite ("#: 1 + x = - 1 + (2 + x)", "1 + x = - 1 + (2 + x)"),
1.242 -([1,2], Res), - 1 + (2 + x) = 2
1.243 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
1.244 -([1,3], Res), - 1 + (x + 2) = 2
1.245 -. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
1.246 -([1,4], Res), x + (- 1 + 2) = 2
1.247 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
1.248 -([1,5], Res), x + (2 + - 1) = 2
1.249 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
1.250 -([1,6], Res), 2 + - 1 + x = 2
1.251 -. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
1.252 -([1], Res), 2 + - 1 + x = 2
1.253 -. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]
1.254 -*)
1.255 -
1.256 -Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
1.257 -
1.258 -
1.259 -\<close> ML \<open>
1.260 -\<close> ML \<open>
1.261 -\<close>
1.262 -(*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
1.263 -(**)\----- outcomment in order to intermediately check with Test_Isac.thy --------------/*)
1.264 -
1.265
1.266 text \<open>
1.267 show theory dependencies using the graph browser,