wneuper/isa: comparison src/Tools/isac/Knowledge/EqSystem.thy

equal deleted inserted replaced

-:eb7d9cbaa3ef
+:8721c71fe3a3
 author: Walther Neuper
 050826,
 (c) due to copyright terms
 *)
-theory EqSystem imports Rational Root begin
+theory EqSystem imports Integrate Rational Root begin
 consts
 occur'_exactly'_in ::
 "[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _")
 (*descriptions in the related problems*)
-solveForVars       :: real list => toreall
+solveForVars       :: "real list => toreall"
-solution           :: bool list => toreall
+solution           :: "bool list => toreall"
 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
 solveSystem        :: "[bool list, real list] => bool list"
 (*Script-names*)
 | _ => 1)
 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
 | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
 | size_of_term' _ = 1;
-fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
+fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
-(case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
+(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
-| Term_Ord.term_ord' pr thy (t, u) =
+| term_ord' pr thy (t, u) =
 (if pr then
 	 let
 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;
 	   val _=writeln("t= f@ts= \""^
 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
 end;
 (**)
 rew_ord' := overwritel (!rew_ord',
 [("ord_simplify_System", ord_simplify_System false thy)
 ]);
+*}
+ML {*
 (** rulesets **)
 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
 val order_add_mult_System =
 Rls{id = "order_add_mult_System", preconds = [],
 	       (*x + (y + z) = y + (x + z)*)
 	       Thm ("add_assoc",num_str @{thm add_assoc})
 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
 	       ],
 scr = EmptyScr}:rls;
+*}
+ML {*
 (*.adapted from 'norm_Rational' by
 #1 using 'ord_simplify_System' in 'order_add_mult_System'
 #2 NOT using common_nominator_p                          .*)
 val norm_System_noadd_fractions =
 Rls {id = "norm_System_noadd_fractions", preconds = [],
 		Rls_ cancel_p
 		],
 scr = Script ((term_of o the o (parse thy))
 			 "empty_script")
 }:rls;
+*}
+ML {*
 (*.adapted from 'norm_Rational' by
 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
 val norm_System =
 Rls {id = "norm_System", preconds = [],
 rew_ord = ("dummy_ord",dummy_ord),
 		Rls_ cancel_p
 		],
 scr = Script ((term_of o the o (parse thy))
 			 "empty_script")
 }:rls;
+*}
+ML {*
 (*.simplify an equational system BEFORE solving it such that parentheses are
 ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) )
 ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION
 This is a copy from 'make_ratpoly_in' with respective reductions:
 *0* expand the term, ie. distribute * and / over +
 	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
 	       Rls_ separate_bdv2,
 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
 	       ],
 scr = EmptyScr}:rls;
+*}
+ML {*
 (*.simplify an equational system AFTER solving it;
 This is a copy of 'make_ratpoly_in' with the differences
 *1* ord_simplify_System instead of termlessI           .*)
 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
 val simplify_System =
 val simplify_System =
 append_rls "simplify_System" simplify_System_parenthesized
 	       [Thm ("sym_add_assoc",
 num_str (@{thm add_assoc} RS @{thm sym}))];
 *)
+*}
+ML {*
 val isolate_bdvs =
 Rls {id="isolate_bdvs", preconds = [],
 	 rew_ord = ("e_rew_ord", e_rew_ord),
 	 erls = append_rls "erls_isolate_bdvs" e_rls
 			   [(Calc ("EqSystem.occur'_exactly'_in",
 				   eval_occur_exactly_in
 				       "#eval_occur_exactly_in_"))
 			    ],
 			   srls = Erls, calc = [],
-	      rules = [Thm ("commute_0_equality",
+	      rules =
-			    num_str @{commute_0_equality),
+[Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
-		       Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}),
+	      Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}),
-		       Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})],
+	      Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})],
 	      scr = EmptyScr};
+*}
+ML {*
 val isolate_bdvs_4x4 =
 Rls {id="isolate_bdvs_4x4", preconds = [],
 	 rew_ord = ("e_rew_ord", e_rew_ord),
 	 erls = append_rls
 		    "erls_isolate_bdvs_4x4" e_rls
 			   eval_some_occur_in "#some_occur_in_"),
 Thm ("not_true",num_str @{thm not_true}),
 		     Thm ("not_false",num_str @{thm not_false})
 			    ],
 	 srls = Erls, calc = [],
-	 rules = [Thm ("commute_0_equality",
+	 rules = [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
-		       num_str @{commute_0_equality),
 		  Thm ("separate_bdvs0", num_str @{thm separate_bdvs0}),
 		  Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add1}),
 		  Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add2}),
 		  Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})
 ], scr = EmptyScr};
+*}
+ML {*
 (*.order the equations in a system such, that a triangular system (if any)
 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
 val order_system =
 Rls {id="order_system", preconds = [],
 Rls {id="prls_triangular", preconds = [],
 	 rew_ord = ("e_rew_ord", e_rew_ord),
 	 erls = Rls {id="erls_prls_triangular", preconds = [],
 		     rew_ord = ("e_rew_ord", e_rew_ord),
 		     erls = Erls, srls = Erls, calc = [],
-		     rules = [(*for precond nth_Cons_ ...*)
+		     rules = [(*for precond NTH_CONS ...*)
 			      Calc ("op <",eval_equ "#less_"),
 			      Calc ("op +", eval_binop "#add_")
 			      (*immediately repeated rewrite pushes
 					    '+' into precondition !*)
 			      ],
 		     scr = EmptyScr},
 	 srls = Erls, calc = [],
-	 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
+	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
 		  Calc ("op +", eval_binop "#add_"),
-		  Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
+		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
 		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
 		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
 		  Calc ("EqSystem.occur'_exactly'_in",
 			eval_occur_exactly_in
 			    "#eval_occur_exactly_in_")
 		  ],
 	 scr = EmptyScr};
+*}
+ML {*
 (*WN060914 quickly created for 4x4;
 more similarity to prls_triangular desirable*)
 val prls_triangular4 =
 Rls {id="prls_triangular4", preconds = [],
 	 rew_ord = ("e_rew_ord", e_rew_ord),
 	 erls = Rls {id="erls_prls_triangular4", preconds = [],
 		     rew_ord = ("e_rew_ord", e_rew_ord),
 		     erls = Erls, srls = Erls, calc = [],
-		     rules = [(*for precond nth_Cons_ ...*)
+		     rules = [(*for precond NTH_CONS ...*)
 			      Calc ("op <",eval_equ "#less_"),
 			      Calc ("op +", eval_binop "#add_")
 			      (*immediately repeated rewrite pushes
 					    '+' into precondition !*)
 			      ],
 		     scr = EmptyScr},
 	 srls = Erls, calc = [],
-	 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
+	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
 		  Calc ("op +", eval_binop "#add_"),
-		  Thm ("nth_Nil_",num_str @{thm thm nth_Nil_}),
+		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
 		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
 		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
 		  Calc ("EqSystem.occur'_exactly'_in",
 			eval_occur_exactly_in
 			    "#eval_occur_exactly_in_")
 		  ],
 	 scr = EmptyScr};
+*}
+ML {*
 ruleset' :=
 overwritelthy @{theory}
 	      (!ruleset',
 [("simplify_System_parenthesized", prep_rls simplify_System_parenthesized),
 ("order_system", prep_rls order_system),
 ("order_add_mult_System", prep_rls order_add_mult_System),
 ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions),
 ("norm_System", prep_rls norm_System)
 ]);
+*}
+ML {*
 (** problems **)
 store_pbt
 (prep_pbt thy "pbl_equsys" [] e_pblID
 (["system"],
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
-("#Find"  ,["solution ss___"](*___ is copy-named*))
+("#Find"  ,["solution ss'''"](*''' is copy-named*))
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 []));
 store_pbt
 (prep_pbt thy "pbl_equsys_lin" [] e_pblID
 (["linear", "system"],
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
 (*TODO.WN050929 check linearity*)
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 []));
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
 (["2x2", "linear", "system"],
 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
-("#Where"  ,["length_ (es_:: bool list) = 2", "length_ v_s = 2"]),
+("#Where"  ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "prls_2x2_linear_system" e_rls
-			     [Thm ("length_Cons_",num_str @{thm length_Cons_}),
+			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
-			      Thm ("length_Nil_",num_str @{thm length_Nil_}),
+			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
 			      Calc ("op +", eval_binop "#add_"),
 			      Calc ("op =",eval_equal "#equal_")
 			      ],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 []));
+*}
+ML {*
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
 (["triangular", "2x2", "linear", "system"],
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
 ("#Where"  ,
-["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
+["(tl v_s) from_ v_s occur_exactly_in (NTH 1 (e_s::bool list))",
-"    v_s  from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
+"    v_s  from_ v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 prls_triangular,
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 [["EqSystem","top_down_substitution","2x2"]]));
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
 (["normalize", "2x2", "linear", "system"],
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 [["EqSystem","normalize","2x2"]]));
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
 (["3x3", "linear", "system"],
 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
-("#Where"  ,["length_ (es_:: bool list) = 3", "length_ v_s = 3"]),
+("#Where"  ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "prls_3x3_linear_system" e_rls
-			     [Thm ("length_Cons_",num_str @{thm length_Cons_}),
+			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
-			      Thm ("length_Nil_",num_str @{thm length_Nil_}),
+			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
 			      Calc ("op +", eval_binop "#add_"),
 			      Calc ("op =",eval_equal "#equal_")
 			      ],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 []));
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
 (["4x4", "linear", "system"],
 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
-("#Where"  ,["length_ (es_:: bool list) = 4", "length_ v_s = 4"]),
+("#Where"  ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "prls_4x4_linear_system" e_rls
-			     [Thm ("length_Cons_",num_str @{thm length_Cons_}),
+			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
-			      Thm ("length_Nil_",num_str @{thm length_Nil_}),
+			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
 			      Calc ("op +", eval_binop "#add_"),
 			      Calc ("op =",eval_equal "#equal_")
 			      ],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 []));
+*}
+ML {*
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
 (["triangular", "4x4", "linear", "system"],
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
 ("#Where" , (*accepts missing variables up to diagional form*)
-["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
+["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
-"(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
+"(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
-"(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
+"(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
-"(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
+"(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
 ]),
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "prls_tri_4x4_lin_sys" prls_triangular
 	     [Calc ("Atools.occurs'_in",eval_occurs_in "")],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 [["EqSystem","top_down_substitution","4x4"]]));
+*}
+ML {*
 store_pbt
 (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
 (["normalize", "4x4", "linear", "system"],
-[("#Given" ,["equalities es_", "solveForVars v_s"]),
+[("#Given" ,["equalities e_s", "solveForVars v_s"]),
-(*length_ is checked 1 level above*)
+(*LENGTH is checked 1 level above*)
-("#Find"  ,["solution ss___"])
+("#Find"  ,["solution ss'''"])
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
-SOME "solveSystem es_ v_s",
+SOME "solveSystem e_s v_s",
 [["EqSystem","normalize","4x4"]]));
 (* show_ptyps();
 *)
+*}
+ML {*
 (** methods **)
 store_met
 (prep_met thy "met_eqsys" [] e_metID
 	      (["EqSystem"],
 	       [],
 	       {rew_ord'="tless_true", rls' = Erls, calc = [],
 		srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
 	       "empty_script"
 	       ));
+*}
+ML {*
 store_met
 (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
 	 (["EqSystem","top_down_substitution","2x2"],
-	  [("#Given" ,["equalities es_", "solveForVars v_s"]),
+	  [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	   ("#Where"  ,
-	    ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
+	    ["(tl v_s) from_ v_s occur_exactly_in (NTH 1 (e_s::bool list))",
-	     "    v_s  from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
+	     "    v_s  from_ v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
-	   ("#Find"  ,["solution ss___"])
+	   ("#Find"  ,["solution ss'''"])
 	   ],
 	  {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
 	   srls = append_rls "srls_top_down_2x2" e_rls
 				  [Thm ("hd_thm",num_str @{thm hd_thm}),
 				   Thm ("tl_Cons",num_str @{thm tl_Cons}),
 				   Thm ("tl_Nil",num_str @{thm tl_Nil})
 				   ],
 	   prls = prls_triangular, crls = Erls, nrls = Erls},
-"Script SolveSystemScript (es_::bool list) (v_s::real list) =                " ^
+"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
-"  (let e1__ = Take (hd es_);                                                " ^
+"  (let e_1 = Take (hd e_s);                                                " ^
-"       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
+"       e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                  isolate_bdvs False))     @@               " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
-"                                  simplify_System False))) e1__;            " ^
+"                                  simplify_System False))) e_1;            " ^
-"       e2__ = Take (hd (tl es_));                                           " ^
+"       e_2 = Take (hd (tl e_s));                                           " ^
-"       e2__ = ((Substitute [e1__]) @@                                       " ^
+"       e_2 = ((Substitute [e_1]) @@                                       " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                  simplify_System_parenthesized False)) @@  " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                  isolate_bdvs False))     @@               " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
-"                                  simplify_System False))) e2__;            " ^
+"                                  simplify_System False))) e_2;            " ^
-"       es__ = Take [e1__, e2__]                                             " ^
+"       e__s = Take [e_1, e_2]                                             " ^
-"   in (Try (Rewrite_Set order_system False)) es__)"
+"   in (Try (Rewrite_Set order_system False)) e__s)"
 (*---------------------------------------------------------------------------
-this script does NOT separate the equations as abolve,
+this script does NOT separate the equations as above,
 but it does not yet work due to preliminary script-interpreter,
 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
-"Script SolveSystemScript (es_::bool list) (v_s::real list) =         " ^
+"Script SolveSystemScript (e_s::bool list) (v_s::real list) =         " ^
-"  (let es__ = Take es_;                                              " ^
+"  (let e__s = Take e_s;                                              " ^
-"       e1__ = hd es__;                                               " ^
+"       e_1 = hd e__s;                                               " ^
-"       e2__ = hd (tl es__);                                          " ^
+"       e_2 = hd (tl e__s);                                          " ^
-"       es__ = [e1__, Substitute [e1__] e2__]                         " ^
+"       e__s = [e_1, Substitute [e_1] e_2]                         " ^
 "   in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                  simplify_System_parenthesized False)) @@ " ^
 "       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
 "                              isolate_bdvs False))              @@   " ^
 "       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
-"                                  simplify_System False))) es__)"
+"                                  simplify_System False))) e__s)"
 ---------------------------------------------------------------------------*)
 	  ));
+*}
+ML {*
 store_met
 (prep_met thy "met_eqsys_norm" [] e_metID
 	      (["EqSystem","normalize"],
 	       [],
 	       {rew_ord'="tless_true", rls' = Erls, calc = [],
 	       "empty_script"
 	       ));
 store_met
 (prep_met thy "met_eqsys_norm_2x2" [] e_metID
 	      (["EqSystem","normalize","2x2"],
-	       [("#Given" ,["equalities es_", "solveForVars v_s"]),
+	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
-		("#Find"  ,["solution ss___"])],
+		("#Find"  ,["solution ss'''"])],
 	       {rew_ord'="tless_true", rls' = Erls, calc = [],
 		srls = append_rls "srls_normalize_2x2" e_rls
 				  [Thm ("hd_thm",num_str @{thm hd_thm}),
 				   Thm ("tl_Cons",num_str @{thm tl_Cons}),
 				   Thm ("tl_Nil",num_str @{thm tl_Nil})
 				   ],
 		prls = Erls, crls = Erls, nrls = Erls},
-"Script SolveSystemScript (es_::bool list) (v_s::real list) =                " ^
+"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
-"  (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@                   " ^
+"  (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@                   " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                  simplify_System_parenthesized False)) @@  " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                                    isolate_bdvs False)) @@ " ^
 "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
 "                                  simplify_System_parenthesized False)) @@  " ^
-"               (Try (Rewrite_Set order_system False))) es_                  " ^
+"               (Try (Rewrite_Set order_system False))) e_s                  " ^
 "   in (SubProblem (EqSystem_,[linear,system],[no_met])                      " ^
-"                  [BOOL_LIST es__, REAL_LIST v_s]))"
+"                  [BOOL_LIST e__s, REAL_LIST v_s]))"
 	       ));
-(*this is for nth_ only*)
+(*this is for NTH only*)
 val srls = Rls {id="srls_normalize_4x4",
 		preconds = [],
 		rew_ord = ("termlessI",termlessI),
 		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
-				  [(*for asm in nth_Cons_ ...*)
+				  [(*for asm in NTH_CONS ...*)
 				   Calc ("op <",eval_equ "#less_"),
-				   (*2nd nth_Cons_ pushes n+-1 into asms*)
+				   (*2nd NTH_CONS pushes n+-1 into asms*)
 				   Calc("op +", eval_binop "#add_")
 				   ],
 		srls = Erls, calc = [],
-		rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
+		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
 			 Calc("op +", eval_binop "#add_"),
-			 Thm ("nth_Nil_",num_str @{thm nth_Nil_})],
+			 Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
 		scr = EmptyScr};
 store_met
 (prep_met thy "met_eqsys_norm_4x4" [] e_metID
 	      (["EqSystem","normalize","4x4"],
-	       [("#Given" ,["equalities es_", "solveForVars v_s"]),
+	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
-		("#Find"  ,["solution ss___"])],
+		("#Find"  ,["solution ss'''"])],
 	       {rew_ord'="tless_true", rls' = Erls, calc = [],
 		srls = append_rls "srls_normalize_4x4" srls
 				  [Thm ("hd_thm",num_str @{thm hd_thm}),
 				   Thm ("tl_Cons",num_str @{thm tl_Cons}),
 				   Thm ("tl_Nil",num_str @{thm tl_Nil})
 				   ],
 		prls = Erls, crls = Erls, nrls = Erls},
 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
-"Script SolveSystemScript (es_::bool list) (v_s::real list) =                " ^
+"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
-"  (let es__ =                                                               " ^
+"  (let e__s =                                                               " ^
 "     ((Try (Rewrite_Set norm_Rational False)) @@                            " ^
 "      (Repeat (Rewrite commute_0_equality False)) @@                        " ^
-"      (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ),     " ^
+"      (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ),     " ^
-"                              (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )]     " ^
+"                              (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )]     " ^
 "                             simplify_System_parenthesized False))    @@    " ^
-"      (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ),     " ^
+"      (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ),     " ^
-"                              (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )]     " ^
+"                              (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )]     " ^
 "                             isolate_bdvs_4x4 False))                 @@    " ^
-"      (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ),     " ^
+"      (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ),     " ^
-"                              (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )]     " ^
+"                              (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )]     " ^
 "                             simplify_System_parenthesized False))    @@    " ^
-"      (Try (Rewrite_Set order_system False)))                           es_ " ^
+"      (Try (Rewrite_Set order_system False)))                           e_s " ^
 "   in (SubProblem (EqSystem_,[linear,system],[no_met])                      " ^
-"                  [BOOL_LIST es__, REAL_LIST v_s]))"
+"                  [BOOL_LIST e__s, REAL_LIST v_s]))"
 ));
 store_met
 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID
 	  (["EqSystem","top_down_substitution","4x4"],
-	   [("#Given" ,["equalities es_", "solveForVars v_s"]),
+	   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	    ("#Where" , (*accepts missing variables up to diagonal form*)
-	     ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
+	     ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
-	      "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
+	      "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
-	      "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
+	      "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
-	      "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
+	      "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
 	      ]),
-	    ("#Find"  ,["solution ss___"])
+	    ("#Find"  ,["solution ss'''"])
 	    ],
 	   {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
 	    srls = append_rls "srls_top_down_4x4" srls [],
 	    prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
 			      [Calc ("Atools.occurs'_in",eval_occurs_in "")],
 	    crls = Erls, nrls = Erls},
 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
-"Script SolveSystemScript (es_::bool list) (v_s::real list) =                " ^
+"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
-"  (let e1_ = nth_ 1 es_;                                                    " ^
+"  (let e_1 = NTH 1 e_s;                                                    " ^
-"       e2_ = Take (nth_ 2 es_);                                             " ^
+"       e_2 = Take (NTH 2 e_s);                                             " ^
-"       e2_ = ((Substitute [e1_]) @@                                         " ^
+"       e_2 = ((Substitute [e_1]) @@                                         " ^
-"              (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
+"              (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
-"                                      (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
+"                                      (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
 "                                 simplify_System_parenthesized False)) @@   " ^
-"              (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
+"              (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
-"                                      (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
+"                                      (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
 "                                 isolate_bdvs False))                  @@   " ^
-"              (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
+"              (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
-"                                      (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
+"                                      (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
-"                                 norm_Rational False)))             e2_     " ^
+"                                 norm_Rational False)))             e_2     " ^
-"    in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
+"    in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
 ));
 *}
 end

branch	isac-update-Isa09-2
changeset 37997	8721c71fe3a3
parent 37995	fac82f29f143
child 37998	6d9fb5475156