1.1 --- a/TODO.md Mon Sep 13 15:42:43 2021 +0200
1.2 +++ b/TODO.md Mon Sep 13 16:01:48 2021 +0200
1.3 @@ -53,10 +53,6 @@
1.4 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.5 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.6
1.7 -* WN: eliminate ThmC.numerals_to_Free, check tests marked TOODOO.1
1.8 - + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see
1.9 - https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
1.10 -
1.11 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
1.12 takes only static arguments ----------------^^^^^^^^^^^^^^, not value of "hd_ord (f, g)"
1.13 ? are there better approximations to old output of (*1*) than with (*2*)
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Sep 13 15:42:43 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Sep 13 16:01:48 2021 +0200
2.3 @@ -308,7 +308,7 @@
2.4 fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
2.5 | is_f_x _ = false;
2.6 (* precondition: TermC.is_atom v andalso TermC.is_atom c *)
2.7 -fun is_const (Const _) = true | is_const _ = false; (*TOODOO kept for strange code below*)
2.8 +fun is_const (Const _) = true | is_const _ = false;
2.9 fun variable_constant_pair (v, c) =
2.10 if (is_variable v andalso (is_const c orelse is_num c)) orelse
2.11 (is_variable c andalso (is_const v orelse is_num v))
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Sep 13 15:42:43 2021 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Sep 13 16:01:48 2021 +0200
3.3 @@ -464,7 +464,7 @@
3.4 | goback => goback
3.5 else go_scan_up1 pcct ist
3.6
3.7 - | scan_up1 pcct ist (Const ("If"(*TOODOO*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.8 + | scan_up1 pcct ist (Const (\<^const_name>\<open>If\<close>, _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.9
3.10 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.11 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
4.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Sep 13 15:42:43 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Sep 13 16:01:48 2021 +0200
4.3 @@ -1317,7 +1317,6 @@
4.4 subsubsection \<open>rule-sets\<close>
4.5 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
4.6
4.7 -ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
4.8 rule_set_knowledge
4.9 norm_Poly = \<open>prep_rls' norm_Poly\<close> and
4.10 Poly_erls = \<open>prep_rls' Poly_erls\<close> and
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 13 15:42:43 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 13 16:01:48 2021 +0200
5.3 @@ -667,19 +667,13 @@
5.4 \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
5.5 scr = Rule.Empty_Prog});
5.6
5.7 -\<close> ML \<open>
5.8 -\<close> ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
5.9 -ML \<open>
5.10 (*erls for calculate_Rational;
5.11 make local with FIXX@ME result:term *term list WN0609???SKMG*)
5.12 val norm_rat_erls = prep_rls'(
5.13 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
5.14 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
5.15 rules = [
5.16 - \<^rule_thm>\<open>refl\<close> (* ..DELETE, just to avoid ERROR fun #> not applicable to "[]"*)
5.17 -(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
5.18 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
5.19 -( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
5.20 ],
5.21 scr = Rule.Empty_Prog});
5.22
6.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Mon Sep 13 15:42:43 2021 +0200
6.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Mon Sep 13 16:01:48 2021 +0200
6.3 @@ -2,7 +2,7 @@
6.4 Author: Walther Neuper 000224
6.5 (c) due to copyright terms
6.6
6.7 -TOODOO: rearrange thy dependency such that "Tactical.Chain" etc are known const_name
6.8 +TODO: rearrange thy dependency such that "Tactical.Chain" etc are known const_name
6.9 *)
6.10
6.11 theory Prog_Tac
7.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Sep 13 15:42:43 2021 +0200
7.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Sep 13 16:01:48 2021 +0200
7.3 @@ -732,8 +732,6 @@
7.4 setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
7.5 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
7.6 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
7.7 -(*SINCE eliminate ThmC.numerals_to_Free: TOODOO
7.8 - rewrite_set_, rewrite_ "- 4 / 3 = - 4 / 3" x = - 4 / 3 = NONE---------------------------\\* )
7.9 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
7.10 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
7.11 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
7.12 @@ -753,8 +751,6 @@
7.13 if get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
7.14 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
7.15 DEconstrCalcTree 1;
7.16 -( *SINCE eliminate ThmC.numerals_to_Free:
7.17 - rewrite_set_, rewrite_ "- 4 / 3 = - 4 / 3" x = - 4 / 3 = NONE---------------------------//*)
7.18
7.19
7.20 "--------- tryMatchProblem, tryRefineProblem ------------";
8.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Sep 13 15:42:43 2021 +0200
8.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Sep 13 16:01:48 2021 +0200
8.3 @@ -71,15 +71,8 @@
8.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.7 -(** )
8.8 val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;
8.9 -( **)
8.10 -(*//---------------- adhoc inserted ------------------------------------------------\\* )
8.11 - see TOODOO.1 in test/../evaluate.sml
8.12 -( *\\---------------- adhoc inserted ------------------------------------------------//*)
8.13 -
8.14 -(*//---------------- continue AFTER previous step "me" -----------------------------\\* )
8.15 -"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ continue AFTER previous step "me" ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
8.16 +"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ continue AFTER previous step 'me' ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
8.17 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
8.18 (nxt''''', p''''', [], pt''''');
8.19 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
8.20 @@ -98,7 +91,6 @@
8.21 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
8.22 case tac of Or_to_List' _ => ()
8.23 | _ => error "Or_to_List broken ?"
8.24 -( *\\---------------- continue AFTER previous step "me" -----------------------------//*)
8.25
8.26
8.27 "----------- check thy in CalcTreeTEST ------------------";
9.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Sep 13 15:42:43 2021 +0200
9.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Sep 13 16:01:48 2021 +0200
9.3 @@ -164,7 +164,6 @@
9.4 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
9.5 \<close>
9.6
9.7 -(*--- comments on TOODOO after changeset "eliminate ThmC.numerals_to_Free" ARE AT THE RIGHT MARGIN*)
9.8 section \<open>trials with Isabelle's functions\<close>
9.9 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
9.10 ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"