
neuper@37906: (* equational systems, minimal -- for use in Biegelinie
neuper@37906:    author: Walther Neuper
neuper@37906:    050826,
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37997: theory EqSystem imports Integrate Rational Root begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   occur'_exactly'_in :: 
neuper@37998:    "[real list, real list, 'a] => bool" ("_ from _ occur'_exactly'_in _")
neuper@37906: 
neuper@37906:   (*descriptions in the related problems*)
neuper@37997:   solveForVars       :: "real list => toreall"
neuper@37997:   solution           :: "bool list => toreall"
neuper@37906: 
neuper@37906:   (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
neuper@37906:   solveSystem        :: "[bool list, real list] => bool list"
neuper@37906: 
neuper@37906:   (*Script-names*)
neuper@37954:   SolveSystemScript  :: "[bool list, real list,     bool list]  
neuper@37954: 						 => bool list"
neuper@37906:                   ("((Script SolveSystemScript (_ _ =))// (_))" 9)
neuper@37906: 
neuper@37954: axioms 
neuper@37906: (*stated as axioms, todo: prove as theorems
neuper@37906:   'bdv' is a constant handled on the meta-level 
neuper@37906:    specifically as a 'bound variable'            *)
neuper@37906: 
neuper@37983:   commute_0_equality:  "(0 = a) = (a = 0)"
neuper@37906: 
neuper@37906:   (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
neuper@37906:     [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
neuper@37983:   separate_bdvs_add:   
neuper@37998:     "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] 
neuper@37954: 		      			     ==> (a + b = c) = (b = c + -1*a)"
neuper@37983:   separate_bdvs0:
neuper@37954:     "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0)  |] 
neuper@37954: 		      			     ==> (a = b) = (a + -1*b = 0)"
neuper@37983:   separate_bdvs_add1:  
neuper@37954:     "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] 
neuper@37954: 		      			     ==> (a = b + c) = (a + -1*c = b)"
neuper@37983:   separate_bdvs_add2:
neuper@37954:     "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] 
neuper@37954: 		      			     ==> (a + b = c) = (b = -1*a + c)"
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37983:   separate_bdvs_mult:  
neuper@37998:     "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] 
neuper@37954: 		      			     ==>(a * b = c) = (b = c / a)"
neuper@37906: 
neuper@37906:   (*requires rew_ord for termination, eg. ord_simplify_Integral;
neuper@37906:     works for lists of any length, interestingly !?!*)
neuper@37983:   order_system_NxN:     "[a,b] = [b,a]"
neuper@37906: 
neuper@37954: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37954: (** eval functions **)
neuper@37954: 
neuper@37954: (*certain variables of a given list occur _all_ in a term
neuper@37954:   args: all: ..variables, which are under consideration (eg. the bound vars)
neuper@37954:         vs:  variables which must be in t, 
neuper@37954:              and none of the others in all must be in t
neuper@37954:         t: the term under consideration
neuper@37954:  *)
neuper@37954: fun occur_exactly_in vs all t =
neuper@37954:     let fun occurs_in' a b = occurs_in b a
neuper@37954:     in foldl and_ (true, map (occurs_in' t) vs)
neuper@37954:        andalso not (foldl or_ (false, map (occurs_in' t) 
neuper@37954:                                           (subtract op = vs all)))
neuper@37954:     end;
neuper@37954: 
neuper@37954: (*("occur_exactly_in", ("EqSystem.occur'_exactly'_in", 
neuper@37954: 			eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
neuper@37954: fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in"
neuper@37954: 			  (p as (Const ("EqSystem.occur'_exactly'_in",_) 
neuper@37954: 				       $ vs $ all $ t)) _ =
neuper@37954:     if occur_exactly_in (isalist2list vs) (isalist2list all) t
neuper@37954:     then SOME ((term2str p) ^ " = True",
neuper@37954: 	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37954:     else SOME ((term2str p) ^ " = False",
neuper@37954: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37954:   | eval_occur_exactly_in _ _ _ _ = NONE;
neuper@37954: 
neuper@37954: calclist':= 
neuper@37954: overwritel (!calclist', 
neuper@37954: 	    [("occur_exactly_in", 
neuper@37954: 	      ("EqSystem.occur'_exactly'_in", 
neuper@37954: 	       eval_occur_exactly_in "#eval_occur_exactly_in_"))
neuper@37954:     ]);
neuper@37954: 
neuper@37954: 
neuper@37954: (** rewrite order 'ord_simplify_System' **)
neuper@37954: 
neuper@37954: (* order wrt. several linear (i.e. without exponents) variables "c","c_2",..
neuper@37954:    which leaves the monomials containing c, c_2,... at the end of an Integral
neuper@37954:    and puts the c, c_2,... rightmost within a monomial.
neuper@37954: 
neuper@37954:    WN050906 this is a quick and dirty adaption of ord_make_polynomial_in,
neuper@37954:    which was most adequate, because it uses size_of_term*)
neuper@37954: (**)
neuper@37954: local (*. for simplify_System .*)
neuper@37954: (**)
neuper@37954: open Term;  (* for type order = EQUAL | LESS | GREATER *)
neuper@37954: 
neuper@37954: fun pr_ord EQUAL = "EQUAL"
neuper@37954:   | pr_ord LESS  = "LESS"
neuper@37954:   | pr_ord GREATER = "GREATER";
neuper@37954: 
neuper@37954: fun dest_hd' (Const (a, T)) = (((a, 0), T), 0)
neuper@37954:   | dest_hd' (Free (ccc, T)) =
neuper@37954:     (case explode ccc of
neuper@37954: 	"c"::[] => ((("|||||||||||||||||||||", 0), T), 1)(*greatest string WN*)
neuper@37954:       | "c"::"_"::_ => ((("|||||||||||||||||||||", 0), T), 1)
neuper@37954:       | _ => (((ccc, 0), T), 1))
neuper@37954:   | dest_hd' (Var v) = (v, 2)
neuper@37954:   | dest_hd' (Bound i) = ((("", i), dummyT), 3)
neuper@37954:   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
neuper@37954: 
neuper@37954: fun size_of_term' (Free (ccc, _)) =
neuper@37954:     (case explode ccc of (*WN0510 hack for the bound variables*)
neuper@37954: 	"c"::[] => 1000
neuper@37954:       | "c"::"_"::is => 1000 * ((str2int o implode) is)
neuper@37954:       | _ => 1)
neuper@37954:   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
neuper@37954:   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
neuper@37954:   | size_of_term' _ = 1;
neuper@37954: 
neuper@37997: fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
neuper@37997:       (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
neuper@37997:   | term_ord' pr thy (t, u) =
neuper@37954:       (if pr then 
neuper@37954: 	 let
neuper@37954: 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;
neuper@37954: 	   val _=writeln("t= f@ts= \""^
neuper@37954: 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
neuper@37991: 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
neuper@37954: 	   val _=writeln("u= g@us= \""^
neuper@37954: 	      ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
neuper@37991: 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
neuper@37954: 	   val _=writeln("size_of_term(t,u)= ("^
neuper@37954: 	      (string_of_int(size_of_term' t))^", "^
neuper@37954: 	      (string_of_int(size_of_term' u))^")");
neuper@37954: 	   val _=writeln("hd_ord(f,g)      = "^((pr_ord o hd_ord)(f,g)));
neuper@37954: 	   val _=writeln("terms_ord(ts,us) = "^
neuper@37954: 			   ((pr_ord o terms_ord str false)(ts,us)));
neuper@37954: 	   val _=writeln("-------");
neuper@37954: 	 in () end
neuper@37954:        else ();
neuper@37954: 	 case int_ord (size_of_term' t, size_of_term' u) of
neuper@37954: 	   EQUAL =>
neuper@37954: 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
neuper@37954: 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 
neuper@37954: 	     | ord => ord)
neuper@37954: 	     end
neuper@37954: 	 | ord => ord)
neuper@37954: and hd_ord (f, g) =                                        (* ~ term.ML *)
neuper@37991:   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, 
neuper@37954: 						     dest_hd' g)
neuper@37954: and terms_ord str pr (ts, us) = 
neuper@37991:     list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
neuper@37954: (**)
neuper@37954: in
neuper@37954: (**)
neuper@37954: (*WN0510 for preliminary use in eval_order_system, see case-study mat-eng.tex
neuper@37954: fun ord_simplify_System_rev (pr:bool) thy subst tu = 
neuper@37954:     (term_ord' pr thy (Library.swap tu) = LESS);*)
neuper@37954: 
neuper@37954: (*for the rls's*)
neuper@37954: fun ord_simplify_System (pr:bool) thy subst tu = 
neuper@37954:     (term_ord' pr thy tu = LESS);
neuper@37954: (**)
neuper@37954: end;
neuper@37954: (**)
neuper@37954: rew_ord' := overwritel (!rew_ord',
neuper@37954: [("ord_simplify_System", ord_simplify_System false thy)
neuper@37954:  ]);
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: (** rulesets **)
neuper@37954: 
neuper@37954: (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
neuper@37954: val order_add_mult_System = 
neuper@37954:   Rls{id = "order_add_mult_System", preconds = [], 
neuper@37954:       rew_ord = ("ord_simplify_System",
neuper@37954: 		 ord_simplify_System false (theory "Integrate")),
neuper@37954:       erls = e_rls,srls = Erls, calc = [],
neuper@37969:       rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37954: 	       (* z * w = w * z *)
neuper@37969: 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
neuper@37954: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37969: 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),		
neuper@37954: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37965: 	       Thm ("add_commute",num_str @{thm add_commute}),	
neuper@37954: 	       (*z + w = w + z*)
neuper@37965: 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37954: 	       (*x + (y + z) = y + (x + z)*)
neuper@37965: 	       Thm ("add_assoc",num_str @{thm add_assoc})	               
neuper@37954: 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
neuper@37954: 	       ], 
neuper@37954:       scr = EmptyScr}:rls;
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: (*.adapted from 'norm_Rational' by
neuper@37954:   #1 using 'ord_simplify_System' in 'order_add_mult_System'
neuper@37954:   #2 NOT using common_nominator_p                          .*)
neuper@37954: val norm_System_noadd_fractions = 
neuper@37954:   Rls {id = "norm_System_noadd_fractions", preconds = [], 
neuper@37954:        rew_ord = ("dummy_ord",dummy_ord), 
neuper@37954:        erls = norm_rat_erls, srls = Erls, calc = [],
neuper@37954:        rules = [(*sequence given by operator precedence*)
neuper@37954: 		Rls_ discard_minus,
neuper@37954: 		Rls_ powers,
neuper@37954: 		Rls_ rat_mult_divide,
neuper@37954: 		Rls_ expand,
neuper@37954: 		Rls_ reduce_0_1_2,
neuper@37954: 		Rls_ (*order_add_mult #1*) order_add_mult_System,
neuper@37954: 		Rls_ collect_numerals,
neuper@37954: 		(*Rls_ add_fractions_p, #2*)
neuper@37954: 		Rls_ cancel_p
neuper@37954: 		],
neuper@37954:        scr = Script ((term_of o the o (parse thy)) 
neuper@37954: 			 "empty_script")
neuper@37954:        }:rls;
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: (*.adapted from 'norm_Rational' by
neuper@37954:   *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
neuper@37954: val norm_System = 
neuper@37954:   Rls {id = "norm_System", preconds = [], 
neuper@37954:        rew_ord = ("dummy_ord",dummy_ord), 
neuper@37954:        erls = norm_rat_erls, srls = Erls, calc = [],
neuper@37954:        rules = [(*sequence given by operator precedence*)
neuper@37954: 		Rls_ discard_minus,
neuper@37954: 		Rls_ powers,
neuper@37954: 		Rls_ rat_mult_divide,
neuper@37954: 		Rls_ expand,
neuper@37954: 		Rls_ reduce_0_1_2,
neuper@37954: 		Rls_ (*order_add_mult *1*) order_add_mult_System,
neuper@37954: 		Rls_ collect_numerals,
neuper@37954: 		Rls_ add_fractions_p,
neuper@37954: 		Rls_ cancel_p
neuper@37954: 		],
neuper@37954:        scr = Script ((term_of o the o (parse thy)) 
neuper@37954: 			 "empty_script")
neuper@37954:        }:rls;
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: (*.simplify an equational system BEFORE solving it such that parentheses are
neuper@37954:    ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) )
neuper@37954: ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION
neuper@37954:    This is a copy from 'make_ratpoly_in' with respective reductions:
neuper@37954:    *0* expand the term, ie. distribute * and / over +
neuper@37954:    *1* ord_simplify_System instead of termlessI
neuper@37954:    *2* no add_fractions_p (= common_nominator_p_rls !)
neuper@37954:    *3* discard_parentheses only for (.*(.*.))
neuper@37954:    analoguous to simplify_Integral                                       .*)
neuper@37954: val simplify_System_parenthesized = 
neuper@37954:   Seq {id = "simplify_System_parenthesized", preconds = []:term list, 
neuper@37954:        rew_ord = ("dummy_ord", dummy_ord),
neuper@37954:       erls = Atools_erls, srls = Erls, calc = [],
neuper@37965:       rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
neuper@37954:  	       (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
neuper@37991: 	       Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
neuper@37954:  	       (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
neuper@37954: 	       (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
neuper@37954: 	       Rls_ norm_Rational_noadd_fractions(**2**),
neuper@37954: 	       Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
neuper@37969: 	       Thm ("sym_real_mult_assoc",
neuper@37969:                      num_str (@{thm real_mult_assoc} RS @{thm sym}))
neuper@37954: 	       (*Rls_ discard_parentheses *3**),
neuper@37954: 	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
neuper@37954: 	       Rls_ separate_bdv2,
neuper@37981: 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
neuper@37954: 	       ],
neuper@37954:       scr = EmptyScr}:rls;      
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: (*.simplify an equational system AFTER solving it;
neuper@37954:    This is a copy of 'make_ratpoly_in' with the differences
neuper@37954:    *1* ord_simplify_System instead of termlessI           .*)
neuper@37954: (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
neuper@37954: val simplify_System = 
neuper@37954:   Seq {id = "simplify_System", preconds = []:term list, 
neuper@37954:        rew_ord = ("dummy_ord", dummy_ord),
neuper@37954:       erls = Atools_erls, srls = Erls, calc = [],
neuper@37954:       rules = [Rls_ norm_Rational,
neuper@37954: 	       Rls_ (*order_add_mult_in*) norm_System (**1**),
neuper@37954: 	       Rls_ discard_parentheses,
neuper@37954: 	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
neuper@37954: 	       Rls_ separate_bdv2,
neuper@37981: 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
neuper@37954: 	       ],
neuper@37954:       scr = EmptyScr}:rls;      
neuper@37906: (*
neuper@37954: val simplify_System = 
neuper@37954:     append_rls "simplify_System" simplify_System_parenthesized
neuper@37974: 	       [Thm ("sym_add_assoc",
neuper@37974:                       num_str (@{thm add_assoc} RS @{thm sym}))];
neuper@37954: *)
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: val isolate_bdvs = 
neuper@37954:     Rls {id="isolate_bdvs", preconds = [], 
neuper@37954: 	 rew_ord = ("e_rew_ord", e_rew_ord), 
neuper@37954: 	 erls = append_rls "erls_isolate_bdvs" e_rls 
neuper@37954: 			   [(Calc ("EqSystem.occur'_exactly'_in", 
neuper@37954: 				   eval_occur_exactly_in 
neuper@37954: 				       "#eval_occur_exactly_in_"))
neuper@37954: 			    ], 
neuper@37954: 			   srls = Erls, calc = [],
neuper@37997: 	      rules = 
neuper@37997:              [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
neuper@37997: 	      Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}),
neuper@37997: 	      Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})],
neuper@37954: 	      scr = EmptyScr};
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: val isolate_bdvs_4x4 = 
neuper@37954:     Rls {id="isolate_bdvs_4x4", preconds = [], 
neuper@37954: 	 rew_ord = ("e_rew_ord", e_rew_ord), 
neuper@37954: 	 erls = append_rls 
neuper@37954: 		    "erls_isolate_bdvs_4x4" e_rls 
neuper@37954: 		    [Calc ("EqSystem.occur'_exactly'_in", 
neuper@37954: 			   eval_occur_exactly_in "#eval_occur_exactly_in_"),
neuper@37954: 		     Calc ("Atools.ident",eval_ident "#ident_"),
neuper@37954: 		     Calc ("Atools.some'_occur'_in", 
neuper@37954: 			   eval_some_occur_in "#some_occur_in_"),
neuper@37969:                      Thm ("not_true",num_str @{thm not_true}),
neuper@37969: 		     Thm ("not_false",num_str @{thm not_false})
neuper@37954: 			    ], 
neuper@37954: 	 srls = Erls, calc = [],
neuper@37997: 	 rules = [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
neuper@37969: 		  Thm ("separate_bdvs0", num_str @{thm separate_bdvs0}),
neuper@37969: 		  Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add1}),
neuper@37969: 		  Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add2}),
neuper@37969: 		  Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})
neuper@37969:                  ], scr = EmptyScr};
neuper@37954: 
neuper@37997: *}
neuper@37997: ML {*
neuper@37997: 
neuper@37954: (*.order the equations in a system such, that a triangular system (if any)
neuper@37954:    appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
neuper@37954: val order_system = 
neuper@37954:     Rls {id="order_system", preconds = [], 
neuper@37954: 	 rew_ord = ("ord_simplify_System", 
neuper@37954: 		    ord_simplify_System false thy), 
neuper@37954: 	 erls = Erls, srls = Erls, calc = [],
neuper@37969: 	 rules = [Thm ("order_system_NxN", num_str @{thm order_system_NxN})
neuper@37954: 		  ],
neuper@37954: 	 scr = EmptyScr};
neuper@37954: 
neuper@37954: val prls_triangular = 
neuper@37954:     Rls {id="prls_triangular", preconds = [], 
neuper@37954: 	 rew_ord = ("e_rew_ord", e_rew_ord), 
neuper@37954: 	 erls = Rls {id="erls_prls_triangular", preconds = [], 
neuper@37954: 		     rew_ord = ("e_rew_ord", e_rew_ord), 
neuper@37954: 		     erls = Erls, srls = Erls, calc = [],
neuper@37997: 		     rules = [(*for precond NTH_CONS ...*)
neuper@37954: 			      Calc ("op <",eval_equ "#less_"),
neuper@37954: 			      Calc ("op +", eval_binop "#add_")
neuper@37954: 			      (*immediately repeated rewrite pushes
neuper@37954: 					    '+' into precondition !*)
neuper@37954: 			      ],
neuper@37954: 		     scr = EmptyScr}, 
neuper@37954: 	 srls = Erls, calc = [],
neuper@37997: 	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
neuper@37954: 		  Calc ("op +", eval_binop "#add_"),
neuper@37997: 		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
neuper@37969: 		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
neuper@37969: 		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
neuper@37954: 		  Calc ("EqSystem.occur'_exactly'_in", 
neuper@37954: 			eval_occur_exactly_in 
neuper@37954: 			    "#eval_occur_exactly_in_")
neuper@37954: 		  ],
neuper@37954: 	 scr = EmptyScr};
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: 
neuper@37954: (*WN060914 quickly created for 4x4; 
neuper@37954:  more similarity to prls_triangular desirable*)
neuper@37954: val prls_triangular4 = 
neuper@37954:     Rls {id="prls_triangular4", preconds = [], 
neuper@37954: 	 rew_ord = ("e_rew_ord", e_rew_ord), 
neuper@37954: 	 erls = Rls {id="erls_prls_triangular4", preconds = [], 
neuper@37954: 		     rew_ord = ("e_rew_ord", e_rew_ord), 
neuper@37954: 		     erls = Erls, srls = Erls, calc = [],
neuper@37997: 		     rules = [(*for precond NTH_CONS ...*)
neuper@37954: 			      Calc ("op <",eval_equ "#less_"),
neuper@37954: 			      Calc ("op +", eval_binop "#add_")
neuper@37954: 			      (*immediately repeated rewrite pushes
neuper@37954: 					    '+' into precondition !*)
neuper@37954: 			      ],
neuper@37954: 		     scr = EmptyScr}, 
neuper@37954: 	 srls = Erls, calc = [],
neuper@37997: 	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
neuper@37954: 		  Calc ("op +", eval_binop "#add_"),
neuper@37997: 		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
neuper@37969: 		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
neuper@37969: 		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
neuper@37954: 		  Calc ("EqSystem.occur'_exactly'_in", 
neuper@37954: 			eval_occur_exactly_in 
neuper@37954: 			    "#eval_occur_exactly_in_")
neuper@37954: 		  ],
neuper@37954: 	 scr = EmptyScr};
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: 
neuper@37954: ruleset' := 
neuper@37967: overwritelthy @{theory} 
neuper@37954: 	      (!ruleset', 
neuper@37954: [("simplify_System_parenthesized", prep_rls simplify_System_parenthesized),
neuper@37954:  ("simplify_System", prep_rls simplify_System),
neuper@37954:  ("isolate_bdvs", prep_rls isolate_bdvs),
neuper@37954:  ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4),
neuper@37954:  ("order_system", prep_rls order_system),
neuper@37954:  ("order_add_mult_System", prep_rls order_add_mult_System),
neuper@37954:  ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions),
neuper@37954:  ("norm_System", prep_rls norm_System)
neuper@37954:  ]);
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: 
neuper@37954: 
neuper@37954: (** problems **)
neuper@37954: 
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys" [] e_pblID
neuper@37954:  (["system"],
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997:    ("#Find"  ,["solution ss'''"](*''' is copy-named*))
neuper@37954:   ],
neuper@37954:   append_rls "e_rls" e_rls [(*for preds in where_*)], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   []));
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin" [] e_pblID
neuper@37954:  (["linear", "system"],
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37954:    (*TODO.WN050929 check linearity*)
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "e_rls" e_rls [(*for preds in where_*)], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   []));
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
neuper@37954:  (["2x2", "linear", "system"],
neuper@37954:   (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997:    ("#Where"  ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "prls_2x2_linear_system" e_rls 
neuper@37997: 			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
neuper@37997: 			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
neuper@37954: 			      Calc ("op +", eval_binop "#add_"),
neuper@37954: 			      Calc ("op =",eval_equal "#equal_")
neuper@37954: 			      ], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   []));
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
neuper@37954:  (["triangular", "2x2", "linear", "system"],
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37954:    ("#Where"  ,
neuper@37998:     ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
neuper@37998:      "    v_s  from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   prls_triangular, 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   [["EqSystem","top_down_substitution","2x2"]]));
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
neuper@37954:  (["normalize", "2x2", "linear", "system"],
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "e_rls" e_rls [(*for preds in where_*)], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   [["EqSystem","normalize","2x2"]]));
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
neuper@37954:  (["3x3", "linear", "system"],
neuper@37954:   (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997:    ("#Where"  ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "prls_3x3_linear_system" e_rls 
neuper@37997: 			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
neuper@37997: 			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
neuper@37954: 			      Calc ("op +", eval_binop "#add_"),
neuper@37954: 			      Calc ("op =",eval_equal "#equal_")
neuper@37954: 			      ], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   []));
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
neuper@37954:  (["4x4", "linear", "system"],
neuper@37954:   (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997:    ("#Where"  ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "prls_4x4_linear_system" e_rls 
neuper@37997: 			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
neuper@37997: 			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
neuper@37954: 			      Calc ("op +", eval_binop "#add_"),
neuper@37954: 			      Calc ("op =",eval_equal "#equal_")
neuper@37954: 			      ], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   []));
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
neuper@37954:  (["triangular", "4x4", "linear", "system"],
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37954:    ("#Where" , (*accepts missing variables up to diagional form*)
neuper@37997:     ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
neuper@37997:      "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
neuper@37997:      "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
neuper@37997:      "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
neuper@37954:      ]),
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "prls_tri_4x4_lin_sys" prls_triangular
neuper@37954: 	     [Calc ("Atools.occurs'_in",eval_occurs_in "")], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   [["EqSystem","top_down_substitution","4x4"]]));
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
neuper@37954:  (["normalize", "4x4", "linear", "system"],
neuper@37997:   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997:    (*LENGTH is checked 1 level above*)
neuper@37997:    ("#Find"  ,["solution ss'''"])
neuper@37954:   ],
neuper@37954:   append_rls "e_rls" e_rls [(*for preds in where_*)], 
neuper@37997:   SOME "solveSystem e_s v_s", 
neuper@37954:   [["EqSystem","normalize","4x4"]]));
neuper@37954: 
neuper@37954: 
neuper@37954: (* show_ptyps();
neuper@37954:    *)
neuper@37954: 
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: (** methods **)
neuper@37954: 
neuper@37954: store_met
neuper@37972:     (prep_met thy "met_eqsys" [] e_metID
neuper@37954: 	      (["EqSystem"],
neuper@37954: 	       [],
neuper@37954: 	       {rew_ord'="tless_true", rls' = Erls, calc = [], 
neuper@37954: 		srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
neuper@37954: 	       "empty_script"
neuper@37954: 	       ));
neuper@37954: store_met
neuper@37972:     (prep_met thy "met_eqsys_topdown" [] e_metID
neuper@37954: 	      (["EqSystem","top_down_substitution"],
neuper@37954: 	       [],
neuper@37954: 	       {rew_ord'="tless_true", rls' = Erls, calc = [], 
neuper@37954: 		srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
neuper@37954: 	       "empty_script"
neuper@37954: 	       ));
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: store_met
neuper@37972:     (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
neuper@37954: 	 (["EqSystem","top_down_substitution","2x2"],
neuper@37997: 	  [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37954: 	   ("#Where"  ,
neuper@37998: 	    ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
neuper@37998: 	     "    v_s  from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
neuper@37997: 	   ("#Find"  ,["solution ss'''"])
neuper@37954: 	   ],
neuper@37954: 	  {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], 
neuper@37954: 	   srls = append_rls "srls_top_down_2x2" e_rls
neuper@37969: 				  [Thm ("hd_thm",num_str @{thm hd_thm}),
neuper@37969: 				   Thm ("tl_Cons",num_str @{thm tl_Cons}),
neuper@37969: 				   Thm ("tl_Nil",num_str @{thm tl_Nil})
neuper@37954: 				   ], 
neuper@37954: 	   prls = prls_triangular, crls = Erls, nrls = Erls},
neuper@37997: "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
neuper@37997: "  (let e_1 = Take (hd e_s);                                                " ^
neuper@37997: "       e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                  isolate_bdvs False))     @@               " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37997: "                                  simplify_System False))) e_1;            " ^
neuper@37997: "       e_2 = Take (hd (tl e_s));                                           " ^
neuper@37997: "       e_2 = ((Substitute [e_1]) @@                                       " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                  simplify_System_parenthesized False)) @@  " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                  isolate_bdvs False))     @@               " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37997: "                                  simplify_System False))) e_2;            " ^
neuper@37997: "       e__s = Take [e_1, e_2]                                             " ^
neuper@37997: "   in (Try (Rewrite_Set order_system False)) e__s)"
neuper@37954: (*---------------------------------------------------------------------------
neuper@37997:   this script does NOT separate the equations as above, 
neuper@37954:   but it does not yet work due to preliminary script-interpreter,
neuper@37954:   see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
neuper@37954: 
neuper@37997: "Script SolveSystemScript (e_s::bool list) (v_s::real list) =         " ^
neuper@37997: "  (let e__s = Take e_s;                                              " ^
neuper@37997: "       e_1 = hd e__s;                                               " ^
neuper@37997: "       e_2 = hd (tl e__s);                                          " ^
neuper@37997: "       e__s = [e_1, Substitute [e_1] e_2]                         " ^
neuper@37995: "   in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                  simplify_System_parenthesized False)) @@ " ^
neuper@37995: "       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
neuper@37954: "                              isolate_bdvs False))              @@   " ^
neuper@37995: "       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37997: "                                  simplify_System False))) e__s)"
neuper@37954: ---------------------------------------------------------------------------*)
neuper@37954: 	  ));
neuper@37997: *}
neuper@37997: ML {*
neuper@37954: store_met
neuper@37972:     (prep_met thy "met_eqsys_norm" [] e_metID
neuper@37954: 	      (["EqSystem","normalize"],
neuper@37954: 	       [],
neuper@37954: 	       {rew_ord'="tless_true", rls' = Erls, calc = [], 
neuper@37954: 		srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
neuper@37954: 	       "empty_script"
neuper@37954: 	       ));
neuper@37998: *}
neuper@37998: ML {*
neuper@37954: store_met
neuper@37972:     (prep_met thy "met_eqsys_norm_2x2" [] e_metID
neuper@37954: 	      (["EqSystem","normalize","2x2"],
neuper@37997: 	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997: 		("#Find"  ,["solution ss'''"])],
neuper@37954: 	       {rew_ord'="tless_true", rls' = Erls, calc = [], 
neuper@37954: 		srls = append_rls "srls_normalize_2x2" e_rls
neuper@37969: 				  [Thm ("hd_thm",num_str @{thm hd_thm}),
neuper@37969: 				   Thm ("tl_Cons",num_str @{thm tl_Cons}),
neuper@37969: 				   Thm ("tl_Nil",num_str @{thm tl_Nil})
neuper@37954: 				   ], 
neuper@37954: 		prls = Erls, crls = Erls, nrls = Erls},
neuper@37997: "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
neuper@37997: "  (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@                   " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                  simplify_System_parenthesized False)) @@  " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                                    isolate_bdvs False)) @@ " ^
neuper@37995: "               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
neuper@37954: "                                  simplify_System_parenthesized False)) @@  " ^
neuper@37997: "               (Try (Rewrite_Set order_system False))) e_s                  " ^
neuper@37998: "   in (SubProblem (EqSystem',[linear,system],[no_met])                      " ^
neuper@37997: "                  [BOOL_LIST e__s, REAL_LIST v_s]))"
neuper@37954: 	       ));
neuper@37954: 
neuper@37998: *}
neuper@37998: ML {*
neuper@37997: (*this is for NTH only*)
neuper@37954: val srls = Rls {id="srls_normalize_4x4", 
neuper@37954: 		preconds = [], 
neuper@37954: 		rew_ord = ("termlessI",termlessI), 
neuper@37954: 		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
neuper@37997: 				  [(*for asm in NTH_CONS ...*)
neuper@37954: 				   Calc ("op <",eval_equ "#less_"),
neuper@37997: 				   (*2nd NTH_CONS pushes n+-1 into asms*)
neuper@37954: 				   Calc("op +", eval_binop "#add_")
neuper@37954: 				   ], 
neuper@37954: 		srls = Erls, calc = [],
neuper@37997: 		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
neuper@37954: 			 Calc("op +", eval_binop "#add_"),
neuper@37997: 			 Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
neuper@37954: 		scr = EmptyScr};
neuper@37954: store_met
neuper@37972:     (prep_met thy "met_eqsys_norm_4x4" [] e_metID
neuper@37954: 	      (["EqSystem","normalize","4x4"],
neuper@37997: 	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37997: 		("#Find"  ,["solution ss'''"])],
neuper@37954: 	       {rew_ord'="tless_true", rls' = Erls, calc = [], 
neuper@37954: 		srls = append_rls "srls_normalize_4x4" srls
neuper@37969: 				  [Thm ("hd_thm",num_str @{thm hd_thm}),
neuper@37969: 				   Thm ("tl_Cons",num_str @{thm tl_Cons}),
neuper@37969: 				   Thm ("tl_Nil",num_str @{thm tl_Nil})
neuper@37954: 				   ], 
neuper@37954: 		prls = Erls, crls = Erls, nrls = Erls},
neuper@37954: (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
neuper@37997: "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
neuper@37997: "  (let e__s =                                                               " ^
neuper@37954: "     ((Try (Rewrite_Set norm_Rational False)) @@                            " ^
neuper@37954: "      (Repeat (Rewrite commute_0_equality False)) @@                        " ^
neuper@37997: "      (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ),     " ^
neuper@37997: "                              (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )]     " ^
neuper@37954: "                             simplify_System_parenthesized False))    @@    " ^
neuper@37997: "      (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ),     " ^
neuper@37997: "                              (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )]     " ^
neuper@37954: "                             isolate_bdvs_4x4 False))                 @@    " ^
neuper@37997: "      (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ),     " ^
neuper@37997: "                              (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )]     " ^
neuper@37954: "                             simplify_System_parenthesized False))    @@    " ^
neuper@37997: "      (Try (Rewrite_Set order_system False)))                           e_s " ^
neuper@37998: "   in (SubProblem (EqSystem',[linear,system],[no_met])                      " ^
neuper@37997: "                  [BOOL_LIST e__s, REAL_LIST v_s]))"
neuper@37954: ));
neuper@37954: store_met
neuper@37972: (prep_met thy "met_eqsys_topdown_4x4" [] e_metID
neuper@37954: 	  (["EqSystem","top_down_substitution","4x4"],
neuper@37997: 	   [("#Given" ,["equalities e_s", "solveForVars v_s"]),
neuper@37954: 	    ("#Where" , (*accepts missing variables up to diagonal form*)
neuper@37997: 	     ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
neuper@37997: 	      "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
neuper@37997: 	      "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
neuper@37997: 	      "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
neuper@37954: 	      ]),
neuper@37997: 	    ("#Find"  ,["solution ss'''"])
neuper@37954: 	    ],
neuper@37954: 	   {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], 
neuper@37954: 	    srls = append_rls "srls_top_down_4x4" srls [], 
neuper@37954: 	    prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
neuper@37954: 			      [Calc ("Atools.occurs'_in",eval_occurs_in "")], 
neuper@37954: 	    crls = Erls, nrls = Erls},
neuper@37954: (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
neuper@37997: "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
neuper@37997: "  (let e_1 = NTH 1 e_s;                                                    " ^
neuper@37997: "       e_2 = Take (NTH 2 e_s);                                             " ^
neuper@37997: "       e_2 = ((Substitute [e_1]) @@                                         " ^
neuper@37997: "              (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
neuper@37997: "                                      (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
neuper@37954: "                                 simplify_System_parenthesized False)) @@   " ^
neuper@37997: "              (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
neuper@37997: "                                      (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
neuper@37954: "                                 isolate_bdvs False))                  @@   " ^
neuper@37997: "              (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
neuper@37997: "                                      (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
neuper@37997: "                                 norm_Rational False)))             e_2     " ^
neuper@37997: "    in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
neuper@37954: ));
neuper@37954: *}
neuper@37954: 
neuper@37906: end



