wneuper/isa: comparison test/Tools/isac/Knowledge/diffapp.sml

equal deleted inserted replaced

-:03bfbc480107
+:972a73d7c50b
 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
 \      (v_::real) (itv_::real set) (err_::bool) =          \
 \ (let e_e = (hd o (filterVar m_)) rs_;              \
 \      t_ = (if 1 < length_ rs_                            \
 \           then (SubProblem (Reals_,[make,function],[no_met])\
-\                     [real_ m_, real_ v_v, bool_list_ rs_])\
+\                     [REAL m_, REAL v_v, BOOL_LIST rs_])\
 \           else (hd rs_));                                \
 \      (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
 \                                [Isac,maximum_on_interval])\
-\                               [bool_ t_, real_ v_v, real_set_ itv_]\
+\                               [BOOL t_, REAL v_v, REAL_SET itv_]\
 \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values])   \
-\      [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_,     \
+\      [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_,     \
-\       bool_list_ (dropWhile (ident e_e) rs_)])::bool list))";
+\       BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))";
 val fix_ = (str2term "fix_::bool list",
 	    str2term "[r=Arbfix]");
 val m_   = (str2term "m_::real",
 	    str2term "A");
 (*--- 2.line in script ---*)
 val t = str2term
 	    "(if 1 < length_ rs_                            \
 \           then (SubProblem (Reals_,[make,function],[no_met])\
-\                     [real_ m_, real_ v_v, bool_list_ rs_])\
+\                     [REAL m_, REAL v_v, BOOL_LIST rs_])\
 \           else (hd rs_))";
 val s = subst_atomic env t;
 term2str s;
 "if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\
 \then SubProblem (Reals_, [make, function], [no_met])\
-\      [real_ A, real_ b,\
+\      [REAL A, REAL b,\
-\       bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\
+\       BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\
 \else hd [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
 val SOME (s',_) = rewrite_set_ thy false list_rls s;
 val s'' = term2str s';
 if s'' =
 "SubProblem (Reals_, [make, function], [no_met])\n\
-\ [real_ A, real_ b,\n\
+\ [REAL A, REAL b,\n\
-\  bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
+\  BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
 else raise error "new behaviour with list_rls 1.3.";
 val env = env @ [(str2term "t_::bool",
 		  str2term "A = (2*sqrt(r^^^2-(b/2)^^^2)) * b")];
 \ (let h_  = (hd o (filterVar f_)) eqs_;                   \
 \      e_1 = hd (dropWhile (ident h_) eqs_);               \
 \      vs_ = dropWhile (ident f_) (Vars h_);                \
 \      v_1 = hd (dropWhile (ident v_v) vs_);                \
 \      (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
-\                          [bool_ e_1, real_ v_1])\
+\                          [BOOL e_1, REAL v_1])\
 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
 val f_ = (str2term "f_::real",
 	  str2term "A");
 val v_v = (str2term "v_::real",
 	  str2term "b");
 if s' = "a" then () else raise error "new behaviour with list_rls 2.4.";
 val env = env @ [(str2term "v_1::real", str2term s')];
 (*--- 5.line in script ---*)
 val t = str2term "(SubProblem(Reals_,[univar,equation],[no_met])\
-		 \           [bool_ e_1, real_ v_1])";
+		 \           [BOOL e_1, REAL v_1])";
 val s = subst_atomic env t;
 term2str s;
 "SubProblem (Reals_, [univar, equation], [no_met])\n\
-\ [bool_ ((a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2), real_ a]";
+\ [BOOL ((a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2), REAL a]";
 val env = env @ [(str2term "s_1::bool list",
 		  str2term "[a = 2 * sqrt (r^^^2 - (b/2)^^^2)]")];
 (*--- 6.line in script ---*)
 val t = str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_::bool)";
 \     v_1 = nth_ 1 vs_;                                   \
 \     v_2 = nth_ 2 vs_;                                   \
 \     e_1 = (hd o (filterVar v_1)) es_;            \
 \     e_2 = (hd o (filterVar v_2)) es_;            \
 \  (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
-\                    [bool_ e_1, real_ v_1]);\
+\                    [BOOL e_1, REAL v_1]);\
 \  (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
-\                    [bool_ e_2, real_ v_2])\
+\                    [BOOL e_2, REAL v_2])\
 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
 val f_ = (str2term "f_::real",
 	  str2term "A");
 val v_v = (str2term "v_::real",
 	  str2term "alpha");
 else raise error "new behaviour with list_rls 3.7.";
 val env = env @ [(str2term "e_2::bool", str2term s')];
 (*--- 8.line in script ---*)
 val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
-		 \            [bool_ e_1, real_ v_1])";
+		 \            [BOOL e_1, REAL v_1])";
 val s = subst_atomic env t;
 term2str s;
 "SubProblem (Reals_, [univar, equation], [no_met])\
-	    \ [bool_ (a / 2 = r * sin alpha), real_ a]";
+	    \ [BOOL (a / 2 = r * sin alpha), REAL a]";
 val s_1 = str2term "[a = 2*r*sin alpha]";
 val env = env @ [(str2term "s_1::bool list", s_1)];
 (*--- 9.line in script ---*)
 val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
-\                    [bool_ e_2, real_ v_2])";
+\                    [BOOL e_2, REAL v_2])";
 val s = subst_atomic env t;
 term2str s;
 "SubProblem (Reals_, [univar, equation], [no_met])\
-	    \ [bool_ (b / 2 = r * cos alpha), real_ b]";
+	    \ [BOOL (b / 2 = r * cos alpha), REAL b]";
 val s_2 = str2term "[b = 2*r*cos alpha]";
 val env = env @ [(str2term "s_2::bool list", s_2)];
 (*--- 10.line in script ---*)
 val t = str2term

branch	isac-update-Isa09-2
changeset 37984	972a73d7c50b
parent 37981	b2877b9d455a
child 37991	028442673981