1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Aug 04 17:34:47 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Aug 05 18:05:28 2021 +0200
1.3 @@ -110,19 +110,35 @@
1.4 (** eval functions **)
1.5
1.6 (*. get the identifier from specific monomials; see fun ist_monom .*)
1.7 -fun identifier (Free (id, _)) = id (* //2, a *)
1.8 -(*TOODOO*)
1.9 - | identifier (* 3*a*b *)
1.10 - (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $
1.11 - num $ t) $ Free (id, _)) =
1.12 - if TermC.is_num num andalso TermC.is_atom t then id
1.13 +fun Free_to_string (Free (str, _)) = str
1.14 + | Free_to_string t =
1.15 + if TermC.is_num t then TermC.string_of_num t else "|||||||||||||"(*the "largest" string*);
1.16 +
1.17 +(* quick and dirty solution just before a field test *)
1.18 +fun identifier (Free (id,_)) = id (* _a_ *)
1.19 + | identifier (Const (\<^const_name>\<open>times\<close>, _) $ t1 $ t2) = (* 2*_a_, a*_b_, 3*a*_b_ *)
1.20 + if TermC.is_atom t2
1.21 + then Free_to_string t2
1.22 + else
1.23 + (case t1 of
1.24 + Const (\<^const_name>\<open>times\<close>, _) $ num $ t1' => (* 3*_a_ \<up> 2 *)
1.25 + if TermC.is_atom num andalso TermC.is_atom t1' then Free_to_string t2
1.26 + else "|||||||||||||"
1.27 + | _ =>
1.28 + (case t2 of
1.29 + Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp =>
1.30 + if TermC.is_atom base andalso TermC.is_atom exp then
1.31 + if TermC.is_num base then "|||||||||||||"
1.32 + else Free_to_string base
1.33 + else "|||||||||||||"
1.34 + | _ => "|||||||||||||"))
1.35 + | identifier (Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp) = (* _a_\<up>2, _3_^2 *)
1.36 + if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base
1.37 else "|||||||||||||"
1.38 -
1.39 - | identifier (* 2*a, a*b *)
1.40 - (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ num $ Free (id, _)) =
1.41 - if TermC.is_atom num then id
1.42 - else "|||||||||||||"
1.43 - | identifier _ = "|||||||||||||"(*the "largest" string*);
1.44 + | identifier t = (* 12 *)
1.45 + if TermC.is_num t
1.46 + then TermC.string_of_num t
1.47 + else "|||||||||||||" (*the "largest" string*);
1.48
1.49 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
1.50 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
2.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Aug 04 17:34:47 2021 +0200
2.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 05 18:05:28 2021 +0200
2.3 @@ -254,37 +254,33 @@
2.4
2.5 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
2.6
2.7 -(*+*)val Test_Out.FormKF "??.empty" = f;
2.8 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
2.9 -(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
2.10 -
2.11 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
2.12 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
2.13 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
2.14 -(*this is new since ThmC.numerals_to_Free..*)
2.15 +(*this is new since ThmC.numerals_to_Free.-----\\*)
2.16 "Calculate PLUS"]
2.17 - then () else error "specific_from_prog ([1], Res) CHANGED"; (*GOON*)
2.18 + then () else error "specific_from_prog ([1], Res) 1 CHANGED"; (*GOON*)
2.19 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
2.20
2.21 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
2.22 - ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
2.23 - "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
2.24 + ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
2.25 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
2.26 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
2.27 - "Calculate PLUS", (*..this is new since ThmC.numerals_to_Free*)
2.28 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
2.29 +(*this is new since ThmC.numerals_to_Free.-----\\*)
2.30 + "Calculate PLUS",
2.31 +(*this is new since ThmC.numerals_to_Free.-----//*)
2.32 "Calculate MINUS"]
2.33 - then () else error "specific_from_prog ([1], Res) CHANGED";
2.34 -
2.35 + then () else error "specific_from_prog ([1], Res) 2 CHANGED";
2.36 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
2.37
2.38 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
2.39 -(** )val ("ok", ([(Rewrite ("tausche_minus_plus", _), _, _)], _, _)) = ( *isa*)
2.40 +(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
2.41 Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
2.42 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
2.43 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
2.44 (*if*) Tactic.for_specify' m; (*false*)
2.45
2.46 -(** )val ("ok", ([(Rewrite ("tausche_minus_plus", _), _, _)], _, _)) = ( *isa*)
2.47 +(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
2.48 Step_Solve.by_tactic m (pt, p);
2.49 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
2.50 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
2.51 @@ -378,8 +374,8 @@
2.52 then () else error "locate_input_tactic Helpless, but applicable CHANGED";
2.53 ( *\----- original before child of 7e314dd233fd -------------------------------------------------/*)
2.54
2.55 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = Rewrite_Set "fasse_zusammen"*)
2.56 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
2.57 +val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
2.58 +val ([3], Res) = p;
2.59
2.60
2.61 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
3.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Aug 04 17:34:47 2021 +0200
3.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Aug 05 18:05:28 2021 +0200
3.3 @@ -35,19 +35,16 @@
3.4 "----------- fun identifier --------------------------------------------------------------------";
3.5 "----------- fun identifier --------------------------------------------------------------------";
3.6 "----------- fun identifier --------------------------------------------------------------------";
3.7 -(*+*)identifier (TermC.str2term "12 ::real") = "|||||||||||||";
3.8 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
3.9 if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1";
3.10 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
3.11 +if identifier (TermC.str2term
3.12 + "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g ::real") = "|||||||||||||"
3.13 + then () else error "identifier 1a";
3.14
3.15 if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2";
3.16 if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3";
3.17
3.18 -(*+*)identifier (TermC.str2term "a \<up> 2 ::real") = "|||||||||||||";(*TOODOO <-- START HERE*)
3.19 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
3.20 if identifier (TermC.str2term "a \<up> 2 ::real") = "a" then () else error "identifier 4";
3.21 if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
3.22 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
3.23 if identifier (TermC.str2term "a * b ::real") = "b" then () else error "identifier 5b";
3.24
3.25 (*these are strange (see "specific monomials" in comment to fun.def.)..*)
3.26 @@ -67,8 +64,6 @@
3.27 TermC.str2term "aaa";
3.28 TermC.str2term "222 * aaa";
3.29
3.30 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
3.31 -(*TOODOO eval_kleiner *)
3.32 case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
3.33 SOME ("123 kleiner 32 = False", _) => ()
3.34 | _ => error "polyminus.sml: 12 kleiner 9 = False";
3.35 @@ -95,7 +90,7 @@
3.36 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
3.37 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
3.38 eval_kleiner "aaa" "bbb" t "ccc";
3.39 -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>",_) $ a $ b)), _) =
3.40 +"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>,_) $ a $ b)), _) =
3.41 ("aaa", "bbb", t, "ccc");
3.42 (*if*) TermC.is_num b (*else*);
3.43
3.44 @@ -105,7 +100,6 @@
3.45 Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $
3.46 (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
3.47 | _ => error "eval_kleiner CHANGED"; (*isa*)
3.48 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
3.49
3.50
3.51 "----------- fun ist_monom ---------------------------------------------------------------------";
3.52 @@ -372,20 +366,11 @@
3.53 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.54
3.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.56 - f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; (*isa == isa2*)
3.57 -val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt;
3.58 - val Check_Postcond ["plus_minus", "polynom", "vereinfachen"] = nxt;
3.59 -nxt;
3.60 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
3.61 - val (*TOODOO*) Rewrite_Set "ordne_alphabetisch" = nxt;
3.62 - f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; (*isa2*)
3.63 -val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
3.64 - f2str f = "3 + - 2 * e + 2 * f + 2 * g"; (*isa2*)
3.65 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.66 - f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
3.67 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.68 - f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
3.69 -if f2str f = "3 - 2 * e + 2 * f + 2 * g" (*isa2*)
3.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.72 +if f2str f = "3 - 2 * e + 2 * f + 2 * g"
3.73 then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1"
3.74 else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
3.75
3.76 @@ -417,7 +402,6 @@
3.77 if p = ([], Res) andalso
3.78 UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
3.79 then () else error "polyminus.sml: Vereinfache 140 d)";
3.80 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
3.81
3.82 "======= 139 c ---";
3.83 reset_states ();