diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/IsacKnowledge/EqSystem.ML --- a/src/Tools/isac/IsacKnowledge/EqSystem.ML Wed Aug 25 15:15:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,673 +0,0 @@ -(* tools for systems of equations over the reals - author: Walther Neuper 050905, 08:51 - (c) due to copyright terms - -use"IsacKnowledge/EqSystem.ML"; -use"EqSystem.ML"; - -remove_thy"EqSystem"; -use_thy"IsacKnowledge/Isac"; -*) - -(** interface isabelle -- isac **) - -theory' := overwritel (!theory', [("EqSystem.thy",EqSystem.thy)]); - -(** eval functions **) - -(*certain variables of a given list occur _all_ in a term - args: all: ..variables, which are under consideration (eg. the bound vars) - vs: variables which must be in t, - and none of the others in all must be in t - t: the term under consideration - *) -fun occur_exactly_in vs all t = - let fun occurs_in' a b = occurs_in b a - in foldl and_ (true, map (occurs_in' t) vs) - andalso not (foldl or_ (false, map (occurs_in' t) (all \\ vs))) - end; - -(*("occur_exactly_in", ("EqSystem.occur'_exactly'_in", - eval_occur_exactly_in "#eval_occur_exactly_in_"))*) -fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in" - (p as (Const ("EqSystem.occur'_exactly'_in",_) - $ vs $ all $ t)) _ = - if occur_exactly_in (isalist2list vs) (isalist2list all) t - then SOME ((term2str p) ^ " = True", - Trueprop $ (mk_equality (p, HOLogic.true_const))) - else SOME ((term2str p) ^ " = False", - Trueprop $ (mk_equality (p, HOLogic.false_const))) - | eval_occur_exactly_in _ _ _ _ = NONE; - -calclist':= -overwritel (!calclist', - [("occur_exactly_in", - ("EqSystem.occur'_exactly'_in", - eval_occur_exactly_in "#eval_occur_exactly_in_")) - ]); - - -(** rewrite order 'ord_simplify_System' **) - -(* order wrt. several linear (i.e. without exponents) variables "c","c_2",.. - which leaves the monomials containing c, c_2,... at the end of an Integral - and puts the c, c_2,... rightmost within a monomial. - - WN050906 this is a quick and dirty adaption of ord_make_polynomial_in, - which was most adequate, because it uses size_of_term*) -(**) -local (*. for simplify_System .*) -(**) -open Term; (* for type order = EQUAL | LESS | GREATER *) - -fun pr_ord EQUAL = "EQUAL" - | pr_ord LESS = "LESS" - | pr_ord GREATER = "GREATER"; - -fun dest_hd' (Const (a, T)) = (((a, 0), T), 0) - | dest_hd' (Free (ccc, T)) = - (case explode ccc of - "c"::[] => ((("|||||||||||||||||||||", 0), T), 1)(*greatest string WN*) - | "c"::"_"::_ => ((("|||||||||||||||||||||", 0), T), 1) - | _ => (((ccc, 0), T), 1)) - | dest_hd' (Var v) = (v, 2) - | dest_hd' (Bound i) = ((("", i), dummyT), 3) - | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); - -fun size_of_term' (Free (ccc, _)) = - (case explode ccc of (*WN0510 hack for the bound variables*) - "c"::[] => 1000 - | "c"::"_"::is => 1000 * ((str2int o implode) is) - | _ => 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' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord) - | 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)^"\" @ \"["^ - (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\""); - val _=writeln("u= g@us= \""^ - ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ - (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\""); - val _=writeln("size_of_term(t,u)= ("^ - (string_of_int(size_of_term' t))^", "^ - (string_of_int(size_of_term' u))^")"); - val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); - val _=writeln("terms_ord(ts,us) = "^ - ((pr_ord o terms_ord str false)(ts,us))); - val _=writeln("-------"); - in () end - else (); - case int_ord (size_of_term' t, size_of_term' u) of - EQUAL => - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) - | ord => ord) - end - | ord => ord) -and hd_ord (f, g) = (* ~ term.ML *) - prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, - dest_hd' g) -and terms_ord str pr (ts, us) = - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); -(**) -in -(**) -(*WN0510 for preliminary use in eval_order_system, see case-study mat-eng.tex -fun ord_simplify_System_rev (pr:bool) thy subst tu = - (term_ord' pr thy (Library.swap tu) = LESS);*) - -(*for the rls's*) -fun ord_simplify_System (pr:bool) thy subst tu = - (term_ord' pr thy tu = LESS); -(**) -end; -(**) -rew_ord' := overwritel (!rew_ord', -[("ord_simplify_System", ord_simplify_System false thy) - ]); - - -(** 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 = [], - rew_ord = ("ord_simplify_System", - ord_simplify_System false Integrate.thy), - erls = e_rls,srls = Erls, calc = [], - rules = [Thm ("real_mult_commute",num_str real_mult_commute), - (* z * w = w * z *) - Thm ("real_mult_left_commute",num_str real_mult_left_commute), - (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) - Thm ("real_mult_assoc",num_str real_mult_assoc), - (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) - Thm ("real_add_commute",num_str real_add_commute), - (*z + w = w + z*) - Thm ("real_add_left_commute",num_str real_add_left_commute), - (*x + (y + z) = y + (x + z)*) - Thm ("real_add_assoc",num_str real_add_assoc) - (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) - ], - scr = EmptyScr}:rls; - -(*.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 = [], - rew_ord = ("dummy_ord",dummy_ord), - erls = norm_rat_erls, srls = Erls, calc = [], - rules = [(*sequence given by operator precedence*) - Rls_ discard_minus, - Rls_ powers, - Rls_ rat_mult_divide, - Rls_ expand, - Rls_ reduce_0_1_2, - Rls_ (*order_add_mult #1*) order_add_mult_System, - Rls_ collect_numerals, - (*Rls_ add_fractions_p, #2*) - Rls_ cancel_p - ], - scr = Script ((term_of o the o (parse thy)) - "empty_script") - }:rls; -(*.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), - erls = norm_rat_erls, srls = Erls, calc = [], - rules = [(*sequence given by operator precedence*) - Rls_ discard_minus, - Rls_ powers, - Rls_ rat_mult_divide, - Rls_ expand, - Rls_ reduce_0_1_2, - Rls_ (*order_add_mult *1*) order_add_mult_System, - Rls_ collect_numerals, - Rls_ add_fractions_p, - Rls_ cancel_p - ], - scr = Script ((term_of o the o (parse thy)) - "empty_script") - }:rls; - -(*.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 + - *1* ord_simplify_System instead of termlessI - *2* no add_fractions_p (= common_nominator_p_rls !) - *3* discard_parentheses only for (.*(.*.)) - analoguous to simplify_Integral .*) -val simplify_System_parenthesized = - Seq {id = "simplify_System_parenthesized", preconds = []:term list, - rew_ord = ("dummy_ord", dummy_ord), - erls = Atools_erls, srls = Erls, calc = [], - rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib), - (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) - Thm ("real_add_divide_distrib",num_str real_add_divide_distrib), - (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) - (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) - Rls_ norm_Rational_noadd_fractions(**2**), - Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**), - Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)) - (*Rls_ discard_parentheses *3**), - Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) - Rls_ separate_bdv2, - Calc ("HOL.divide" ,eval_cancel "#divide_") - ], - scr = EmptyScr}:rls; - -(*.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 = - Seq {id = "simplify_System", preconds = []:term list, - rew_ord = ("dummy_ord", dummy_ord), - erls = Atools_erls, srls = Erls, calc = [], - rules = [Rls_ norm_Rational, - Rls_ (*order_add_mult_in*) norm_System (**1**), - Rls_ discard_parentheses, - Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) - Rls_ separate_bdv2, - Calc ("HOL.divide" ,eval_cancel "#divide_") - ], - scr = EmptyScr}:rls; -(* -val simplify_System = - append_rls "simplify_System" simplify_System_parenthesized - [Thm ("sym_real_add_assoc", num_str (real_add_assoc RS sym))]; -*) - -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", - num_str commute_0_equality), - Thm ("separate_bdvs_add", num_str separate_bdvs_add), - Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)], - scr = EmptyScr}; -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 - [Calc ("EqSystem.occur'_exactly'_in", - eval_occur_exactly_in "#eval_occur_exactly_in_"), - Calc ("Atools.ident",eval_ident "#ident_"), - Calc ("Atools.some'_occur'_in", - eval_some_occur_in "#some_occur_in_"), - Thm ("not_true",num_str not_true), - Thm ("not_false",num_str not_false) - ], - srls = Erls, calc = [], - rules = [Thm ("commute_0_equality", - num_str commute_0_equality), - Thm ("separate_bdvs0", num_str separate_bdvs0), - Thm ("separate_bdvs_add1", num_str separate_bdvs_add1), - Thm ("separate_bdvs_add1", num_str separate_bdvs_add2), - Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)], - scr = EmptyScr}; - -(*.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 = [], - rew_ord = ("ord_simplify_System", - ord_simplify_System false thy), - erls = Erls, srls = Erls, calc = [], - rules = [Thm ("order_system_NxN", num_str order_system_NxN) - ], - scr = EmptyScr}; - -val prls_triangular = - 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_ ...*) - 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 nth_Cons_), - Calc ("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str nth_Nil_), - Thm ("tl_Cons",num_str tl_Cons), - Thm ("tl_Nil",num_str tl_Nil), - Calc ("EqSystem.occur'_exactly'_in", - eval_occur_exactly_in - "#eval_occur_exactly_in_") - ], - scr = EmptyScr}; - -(*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_ ...*) - 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 nth_Cons_), - Calc ("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str nth_Nil_), - Thm ("tl_Cons",num_str tl_Cons), - Thm ("tl_Nil",num_str tl_Nil), - Calc ("EqSystem.occur'_exactly'_in", - eval_occur_exactly_in - "#eval_occur_exactly_in_") - ], - scr = EmptyScr}; - -ruleset' := -overwritelthy thy - (!ruleset', -[("simplify_System_parenthesized", prep_rls simplify_System_parenthesized), - ("simplify_System", prep_rls simplify_System), - ("isolate_bdvs", prep_rls isolate_bdvs), - ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4), - ("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) - ]); - - -(** problems **) - -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys" [] e_pblID - (["system"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Find" ,["solution ss___"](*___ is copy-named*)) - ], - append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ vs_", - [])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin" [] e_pblID - (["linear", "system"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - (*TODO.WN050929 check linearity*) - ("#Find" ,["solution ss___"]) - ], - append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ vs_", - [])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2" [] e_pblID - (["2x2", "linear", "system"], - (*~~~~~~~~~~~~~~~~~~~~~~~~~*) - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]), - ("#Find" ,["solution ss___"]) - ], - append_rls "prls_2x2_linear_system" e_rls - [Thm ("length_Cons_",num_str length_Cons_), - Thm ("length_Nil_",num_str length_Nil_), - Calc ("op +", eval_binop "#add_"), - Calc ("op =",eval_equal "#equal_") - ], - SOME "solveSystem es_ vs_", - [])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2_tri" [] e_pblID - (["triangular", "2x2", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" , - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), - ("#Find" ,["solution ss___"]) - ], - prls_triangular, - SOME "solveSystem es_ vs_", - [["EqSystem","top_down_substitution","2x2"]])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2_norm" [] e_pblID - (["normalize", "2x2", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Find" ,["solution ss___"]) - ], - append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ vs_", - [["EqSystem","normalize","2x2"]])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_3x3" [] e_pblID - (["3x3", "linear", "system"], - (*~~~~~~~~~~~~~~~~~~~~~~~~~*) - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]), - ("#Find" ,["solution ss___"]) - ], - append_rls "prls_3x3_linear_system" e_rls - [Thm ("length_Cons_",num_str length_Cons_), - Thm ("length_Nil_",num_str length_Nil_), - Calc ("op +", eval_binop "#add_"), - Calc ("op =",eval_equal "#equal_") - ], - SOME "solveSystem es_ vs_", - [])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4" [] e_pblID - (["4x4", "linear", "system"], - (*~~~~~~~~~~~~~~~~~~~~~~~~~*) - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]), - ("#Find" ,["solution ss___"]) - ], - append_rls "prls_4x4_linear_system" e_rls - [Thm ("length_Cons_",num_str length_Cons_), - Thm ("length_Nil_",num_str length_Nil_), - Calc ("op +", eval_binop "#add_"), - Calc ("op =",eval_equal "#equal_") - ], - SOME "solveSystem es_ vs_", - [])); -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID - (["triangular", "4x4", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" , (*accepts missing variables up to diagional form*) - ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", - "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", - "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", - "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" - ]), - ("#Find" ,["solution ss___"]) - ], - append_rls "prls_tri_4x4_lin_sys" prls_triangular - [Calc ("Atools.occurs'_in",eval_occurs_in "")], - SOME "solveSystem es_ vs_", - [["EqSystem","top_down_substitution","4x4"]])); - -store_pbt - (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_norm" [] e_pblID - (["normalize", "4x4", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - (*length_ is checked 1 level above*) - ("#Find" ,["solution ss___"]) - ], - append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ vs_", - [["EqSystem","normalize","4x4"]])); - - -(* show_ptyps(); - *) - -(** methods **) - -store_met - (prep_met EqSystem.thy "met_eqsys" [] e_metID - (["EqSystem"], - [], - {rew_ord'="tless_true", rls' = Erls, calc = [], - srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, - "empty_script" - )); -store_met - (prep_met EqSystem.thy "met_eqsys_topdown" [] e_metID - (["EqSystem","top_down_substitution"], - [], - {rew_ord'="tless_true", rls' = Erls, calc = [], - srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, - "empty_script" - )); -store_met - (prep_met EqSystem.thy "met_eqsys_topdown_2x2" [] e_metID - (["EqSystem","top_down_substitution","2x2"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" , - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), - ("#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 hd_thm), - Thm ("tl_Cons",num_str tl_Cons), - Thm ("tl_Nil",num_str tl_Nil) - ], - prls = prls_triangular, crls = Erls, nrls = Erls}, -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \ -\ (let e1__ = Take (hd es_); \ -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ isolate_bdvs False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System False))) e1__; \ -\ e2__ = Take (hd (tl es_)); \ -\ e2__ = ((Substitute [e1__]) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ isolate_bdvs False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System False))) e2__; \ -\ es__ = Take [e1__, e2__] \ -\ in (Try (Rewrite_Set order_system False)) es__)" -(*--------------------------------------------------------------------------- - this script does NOT separate the equations as abolve, - 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) (vs_::real list) = \ -\ (let es__ = Take es_; \ -\ e1__ = hd es__; \ -\ e2__ = hd (tl es__); \ -\ es__ = [e1__, Substitute [e1__] e2__] \ -\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \ -\ isolate_bdvs False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System False))) es__)" ----------------------------------------------------------------------------*) - )); -store_met - (prep_met EqSystem.thy "met_eqsys_norm" [] e_metID - (["EqSystem","normalize"], - [], - {rew_ord'="tless_true", rls' = Erls, calc = [], - srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, - "empty_script" - )); -store_met - (prep_met EqSystem.thy "met_eqsys_norm_2x2" [] e_metID - (["EqSystem","normalize","2x2"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Find" ,["solution ss___"])], - {rew_ord'="tless_true", rls' = Erls, calc = [], - srls = append_rls "srls_normalize_2x2" e_rls - [Thm ("hd_thm",num_str hd_thm), - Thm ("tl_Cons",num_str tl_Cons), - Thm ("tl_Nil",num_str tl_Nil) - ], - prls = Erls, crls = Erls, nrls = Erls}, -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \ -\ (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ isolate_bdvs False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set order_system False))) es_ \ -\ in (SubProblem (EqSystem_,[linear,system],[no_met]) \ -\ [bool_list_ es__, real_list_ vs_]))" - )); - -(*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_ ...*) - Calc ("op <",eval_equ "#less_"), - (*2nd nth_Cons_ pushes n+-1 into asms*) - Calc("op +", eval_binop "#add_") - ], - srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str nth_Cons_), - Calc("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str nth_Nil_)], - scr = EmptyScr}; -store_met - (prep_met EqSystem.thy "met_eqsys_norm_4x4" [] e_metID - (["EqSystem","normalize","4x4"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Find" ,["solution ss___"])], - {rew_ord'="tless_true", rls' = Erls, calc = [], - srls = append_rls "srls_normalize_4x4" srls - [Thm ("hd_thm",num_str hd_thm), - Thm ("tl_Cons",num_str tl_Cons), - Thm ("tl_Nil",num_str tl_Nil) - ], - prls = Erls, crls = Erls, nrls = Erls}, -(*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \ -\ (let es__ = \ -\ ((Try (Rewrite_Set norm_Rational False)) @@ \ -\ (Repeat (Rewrite commute_0_equality False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \ -\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \ -\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \ -\ isolate_bdvs_4x4 False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \ -\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set order_system False))) es_ \ -\ in (SubProblem (EqSystem_,[linear,system],[no_met]) \ -\ [bool_list_ es__, real_list_ vs_]))" -)); -store_met -(prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID - (["EqSystem","top_down_substitution","4x4"], - [("#Given" ,["equalities es_", "solveForVars vs_"]), - ("#Where" , (*accepts missing variables up to diagonal form*) - ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", - "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", - "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", - "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" - ]), - ("#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) (vs_::real list) = \ -\ (let e1_ = nth_ 1 es_; \ -\ e2_ = Take (nth_ 2 es_); \ -\ e2_ = ((Substitute [e1_]) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\ -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\ -\ simplify_System_parenthesized False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\ -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\ -\ isolate_bdvs False)) @@ \ -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\ -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\ -\ norm_Rational False))) e2_ \ -\ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])" -)); - -(* show_mets(); - *) - -(* -use"IsacKnowledge/EqSystem.ML"; -use"EqSystem.ML"; -*)