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@52148: axiomatization where 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@52148: commute_0_equality: "(0 = a) = (a = 0)" and 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@52148: ==> (a + b = c) = (b = c + -1*a)" and neuper@37983: separate_bdvs0: neuper@37954: "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |] neuper@52148: ==> (a = b) = (a + -1*b = 0)" and neuper@37983: separate_bdvs_add1: neuper@37954: "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] neuper@52148: ==> (a = b + c) = (a + -1*c = b)" and neuper@37983: separate_bdvs_add2: neuper@37954: "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] neuper@52148: ==> (a + b = c) = (b = -1*a + c)" and neuper@37983: separate_bdvs_mult: neuper@37998: "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] t@42197: ==>(a * b = c) = (b = c / a)" neuper@55276: axiomatization where (*..if replaced by "and" we get an error in wneuper@59370: --- rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*) t@42197: order_system_NxN: "[a,b] = [b,a]" neuper@37906: (*requires rew_ord for termination, eg. ord_simplify_Integral; neuper@37906: works for lists of any length, interestingly !?!*) 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)) _ = wneuper@59389: if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t neuper@37954: then SOME ((term2str p) ^ " = True", wneuper@59389: TermC.Trueprop $ (TermC.mk_equality (p, @{term True}))) neuper@37954: else SOME ((term2str p) ^ " = False", wneuper@59389: TermC.Trueprop $ (TermC.mk_equality (p, @{term False}))) neuper@37954: | eval_occur_exactly_in _ _ _ _ = NONE; s1210629013@52145: *} s1210629013@52145: setup {* KEStore_Elems.add_calcs s1210629013@52145: [("occur_exactly_in", s1210629013@52145: ("EqSystem.occur'_exactly'_in", s1210629013@52145: eval_occur_exactly_in "#eval_occur_exactly_in_"))] *} s1210629013@52145: ML {* 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@40836: (case Symbol.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@40836: (case Symbol.explode ccc of (*WN0510 hack for the bound variables*) neuper@37954: "c"::[] => 1000 wneuper@59389: | "c"::"_"::is => 1000 * ((TermC.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@52070: (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@52070: (if pr neuper@52070: then neuper@52070: let neuper@52070: val (f, ts) = strip_comb t and (g, us) = strip_comb u; neuper@52070: val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^ neuper@52070: commas (map (term_to_string''' thy) ts) ^ "]\""); neuper@52070: val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^ neuper@52070: commas (map (term_to_string''' thy) us) ^ "]\""); neuper@52070: val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^ neuper@52070: string_of_int (size_of_term' u) ^ ")"); neuper@52070: val _ = tracing ("hd_ord(f,g) = " ^ ((pr_ord o hd_ord) (f,g))); neuper@52070: val _ = tracing ("terms_ord (ts,us) = " ^(pr_ord o terms_ord str false) (ts,us)); neuper@52070: val _=tracing("-------"); neuper@52070: in () end neuper@52070: else (); neuper@52070: case int_ord (size_of_term' t, size_of_term' u) of neuper@52070: EQUAL => neuper@52070: let val (f, ts) = strip_comb t and (g, us) = strip_comb u neuper@52070: in (case hd_ord (f, g) of neuper@52070: EQUAL => (terms_ord str pr) (ts, us) neuper@52070: | ord => ord) neuper@52070: end neuper@37954: | ord => ord) neuper@37954: and hd_ord (f, g) = (* ~ term.ML *) neuper@52070: prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) neuper@52070: and terms_ord str pr (ts, us) = 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", bonzai@41919: ord_simplify_System false @{theory "Integrate"}), neuper@42451: erls = e_rls,srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("mult_commute",TermC.num_str @{thm mult.commute}), neuper@37954: (* z * w = w * z *) wneuper@59389: Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}), neuper@37954: (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) wneuper@59389: Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}), neuper@37954: (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) wneuper@59389: Thm ("add_commute",TermC.num_str @{thm add.commute}), neuper@37954: (*z + w = w + z*) wneuper@59389: Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}), neuper@37954: (*x + (y + z) = y + (x + z)*) wneuper@59389: Thm ("add_assoc",TermC.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@42451: erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], 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: ], wneuper@59389: scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "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@42451: erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], 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: ], wneuper@59389: scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "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@42451: erls = Atools_erls, srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("distrib_right",TermC.num_str @{thm distrib_right}), neuper@37954: (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) wneuper@59389: Thm ("add_divide_distrib",TermC.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@48763: Thm ("sym_mult_assoc", wneuper@59389: TermC.num_str (@{thm 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, wneuper@59360: Calc ("Rings.divide_class.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@42451: erls = Atools_erls, srls = Erls, calc = [], errpatts = [], 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, wneuper@59360: Calc ("Rings.divide_class.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", wneuper@59389: TermC.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@42451: srls = Erls, calc = [], errpatts = [], neuper@37997: rules = wneuper@59389: [Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}), wneuper@59389: Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}), wneuper@59389: Thm ("separate_bdvs_mult", TermC.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_"), wneuper@59389: Thm ("not_true",TermC.num_str @{thm not_true}), wneuper@59389: Thm ("not_false",TermC.num_str @{thm not_false}) neuper@37954: ], neuper@42451: srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}), wneuper@59389: Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}), wneuper@59389: Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}), wneuper@59389: Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add2}), wneuper@59389: Thm ("separate_bdvs_mult", TermC.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@42451: erls = Erls, srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("order_system_NxN", TermC.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@42451: erls = Erls, srls = Erls, calc = [], errpatts = [], neuper@37997: rules = [(*for precond NTH_CONS ...*) neuper@38045: Calc ("Orderings.ord_class.less",eval_equ "#less_"), neuper@38014: Calc ("Groups.plus_class.plus", eval_binop "#add_") neuper@37954: (*immediately repeated rewrite pushes neuper@37954: '+' into precondition !*) neuper@37954: ], neuper@37954: scr = EmptyScr}, neuper@42451: srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), neuper@38014: Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59389: Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), wneuper@59389: Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59389: Thm ("tl_Nil",TermC.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@42451: erls = Erls, srls = Erls, calc = [], errpatts = [], neuper@37997: rules = [(*for precond NTH_CONS ...*) neuper@38045: Calc ("Orderings.ord_class.less",eval_equ "#less_"), neuper@38014: Calc ("Groups.plus_class.plus", eval_binop "#add_") neuper@37954: (*immediately repeated rewrite pushes neuper@37954: '+' into precondition !*) neuper@37954: ], neuper@37954: scr = EmptyScr}, neuper@42451: srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), neuper@38014: Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59389: Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), wneuper@59389: Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59389: Thm ("tl_Nil",TermC.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: *} t@42197: neuper@52125: setup {* KEStore_Elems.add_rlss neuper@52125: [("simplify_System_parenthesized", s1210629013@55444: (Context.theory_name @{theory}, prep_rls' simplify_System_parenthesized)), s1210629013@55444: ("simplify_System", (Context.theory_name @{theory}, prep_rls' simplify_System)), s1210629013@55444: ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls' isolate_bdvs)), s1210629013@55444: ("isolate_bdvs_4x4", (Context.theory_name @{theory}, prep_rls' isolate_bdvs_4x4)), s1210629013@55444: ("order_system", (Context.theory_name @{theory}, prep_rls' order_system)), s1210629013@55444: ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls' order_add_mult_System)), neuper@52125: ("norm_System_noadd_fractions", s1210629013@55444: (Context.theory_name @{theory}, prep_rls' norm_System_noadd_fractions)), s1210629013@55444: ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))] *} t@42197: neuper@37954: (** problems **) s1210629013@55359: setup {* KEStore_Elems.add_pbts wneuper@59269: [(Specify.prep_pbt thy "pbl_equsys" [] e_pblID s1210629013@55339: (["system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Find" ,["solution ss'''"](*''' is copy-named*))], s1210629013@55339: append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin" [] e_pblID s1210629013@55339: (["LINEAR", "system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: (*TODO.WN050929 check linearity*) s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID s1210629013@55339: (["2x2", "LINEAR", "system"], s1210629013@55339: (*~~~~~~~~~~~~~~~~~~~~~~~~~*) s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "prls_2x2_linear_system" e_rls wneuper@59389: [Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), wneuper@59389: Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), s1210629013@55339: Calc ("Groups.plus_class.plus", eval_binop "#add_"), s1210629013@55339: Calc ("HOL.eq",eval_equal "#equal_")], s1210629013@55339: SOME "solveSystem e_s v_s", [])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID s1210629013@55339: (["triangular", "2x2", "LINEAR", "system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Where", s1210629013@55339: ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))", s1210629013@55339: " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID wneuper@59367: (["normalise", "2x2", "LINEAR", "system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "e_rls" e_rls [(*for preds in where_*)], s1210629013@55339: SOME "solveSystem e_s v_s", wneuper@59367: [["EqSystem","normalise","2x2"]])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID s1210629013@55339: (["3x3", "LINEAR", "system"], s1210629013@55339: (*~~~~~~~~~~~~~~~~~~~~~~~~~*) s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "prls_3x3_linear_system" e_rls wneuper@59389: [Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), wneuper@59389: Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), s1210629013@55339: Calc ("Groups.plus_class.plus", eval_binop "#add_"), s1210629013@55339: Calc ("HOL.eq",eval_equal "#equal_")], s1210629013@55339: SOME "solveSystem e_s v_s", [])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID s1210629013@55339: (["4x4", "LINEAR", "system"], s1210629013@55339: (*~~~~~~~~~~~~~~~~~~~~~~~~~*) s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "prls_4x4_linear_system" e_rls wneuper@59389: [Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), wneuper@59389: Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), s1210629013@55339: Calc ("Groups.plus_class.plus", eval_binop "#add_"), s1210629013@55339: Calc ("HOL.eq",eval_equal "#equal_")], s1210629013@55339: SOME "solveSystem e_s v_s", [])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID s1210629013@55339: (["triangular", "4x4", "LINEAR", "system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Where" , (*accepts missing variables up to diagional form*) s1210629013@55339: ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))", s1210629013@55339: "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))", s1210629013@55339: "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))", s1210629013@55339: "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "prls_tri_4x4_lin_sys" prls_triangular s1210629013@55339: [Calc ("Atools.occurs'_in",eval_occurs_in "")], s1210629013@55339: SOME "solveSystem e_s v_s", s1210629013@55339: [["EqSystem","top_down_substitution","4x4"]])), wneuper@59269: (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID wneuper@59367: (["normalise", "4x4", "LINEAR", "system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: (*LENGTH is checked 1 level above*) s1210629013@55339: ("#Find" ,["solution ss'''"])], s1210629013@55339: append_rls "e_rls" e_rls [(*for preds in where_*)], s1210629013@55339: SOME "solveSystem e_s v_s", wneuper@59367: [["EqSystem","normalise","4x4"]]))] *} neuper@37954: neuper@37998: ML {* neuper@37997: (*this is for NTH only*) wneuper@59370: val srls = Rls {id="srls_normalise_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@38045: Calc ("Orderings.ord_class.less",eval_equ "#less_"), neuper@37997: (*2nd NTH_CONS pushes n+-1 into asms*) neuper@38014: Calc("Groups.plus_class.plus", eval_binop "#add_") neuper@37954: ], neuper@42451: srls = Erls, calc = [], errpatts = [], wneuper@59389: rules = [Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), neuper@38014: Calc("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59389: Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})], neuper@37954: scr = EmptyScr}; neuper@37954: *} neuper@37954: s1210629013@55380: (**methods**) s1210629013@55373: setup {* KEStore_Elems.add_mets wneuper@59269: [Specify.prep_met thy "met_eqsys" [] e_metID s1210629013@55373: (["EqSystem"], [], s1210629013@55373: {rew_ord'="tless_true", rls' = Erls, calc = [], srls = Erls, prls = Erls, crls = Erls, s1210629013@55373: errpats = [], nrls = Erls}, s1210629013@55373: "empty_script"), wneuper@59269: Specify.prep_met thy "met_eqsys_topdown" [] e_metID s1210629013@55373: (["EqSystem","top_down_substitution"], [], s1210629013@55373: {rew_ord'="tless_true", rls' = Erls, calc = [], srls = Erls, prls = Erls, crls = Erls, s1210629013@55373: errpats = [], nrls = Erls}, s1210629013@55373: "empty_script"), wneuper@59269: Specify.prep_met thy "met_eqsys_topdown_2x2" [] e_metID s1210629013@55373: (["EqSystem", "top_down_substitution", "2x2"], s1210629013@55373: [("#Given", ["equalities e_s", "solveForVars v_s"]), s1210629013@55373: ("#Where", s1210629013@55373: ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))", s1210629013@55373: " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]), s1210629013@55373: ("#Find" ,["solution ss'''"])], s1210629013@55373: {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], s1210629013@55373: srls = append_rls "srls_top_down_2x2" e_rls wneuper@59389: [Thm ("hd_thm",TermC.num_str @{thm hd_thm}), wneuper@59389: Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59389: Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], s1210629013@55373: prls = prls_triangular, crls = Erls, errpats = [], nrls = Erls}, s1210629013@55373: "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ s1210629013@55373: " (let e_1 = Take (hd e_s); " ^ s1210629013@55373: " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " isolate_bdvs False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System False))) e_1; " ^ s1210629013@55373: " e_2 = Take (hd (tl e_s)); " ^ s1210629013@55373: " e_2 = ((Substitute [e_1]) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " isolate_bdvs False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System False))) e_2; " ^ s1210629013@55373: " e__s = Take [e_1, e_2] " ^ s1210629013@55373: " in (Try (Rewrite_Set order_system False)) e__s)" s1210629013@55373: (*--------------------------------------------------------------------------- s1210629013@55373: this script does NOT separate the equations as above, s1210629013@55373: but it does not yet work due to preliminary script-interpreter, s1210629013@55373: see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' s1210629013@55373: s1210629013@55373: "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ s1210629013@55373: " (let e__s = Take e_s; " ^ s1210629013@55373: " e_1 = hd e__s; " ^ s1210629013@55373: " e_2 = hd (tl e__s); " ^ s1210629013@55373: " e__s = [e_1, Substitute [e_1] e_2] " ^ s1210629013@55373: " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^ s1210629013@55373: " isolate_bdvs False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System False))) e__s)" s1210629013@55373: ---------------------------------------------------------------------------*)), wneuper@59269: Specify.prep_met thy "met_eqsys_norm" [] e_metID wneuper@59367: (["EqSystem", "normalise"], [], s1210629013@55373: {rew_ord'="tless_true", rls' = Erls, calc = [], srls = Erls, prls = Erls, crls = Erls, s1210629013@55373: errpats = [], nrls = Erls}, s1210629013@55373: "empty_script"), wneuper@59269: Specify.prep_met thy "met_eqsys_norm_2x2" [] e_metID wneuper@59367: (["EqSystem","normalise","2x2"], s1210629013@55373: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55373: ("#Find" ,["solution ss'''"])], s1210629013@55373: {rew_ord'="tless_true", rls' = Erls, calc = [], wneuper@59370: srls = append_rls "srls_normalise_2x2" e_rls wneuper@59389: [Thm ("hd_thm",TermC.num_str @{thm hd_thm}), wneuper@59389: Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59389: Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], s1210629013@55373: prls = Erls, crls = Erls, errpats = [], nrls = Erls}, s1210629013@55373: "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ s1210629013@55373: " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " isolate_bdvs False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set order_system False))) e_s " ^ s1210629013@55373: " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^ s1210629013@55373: " [BOOL_LIST e__s, REAL_LIST v_s]))"), wneuper@59269: Specify.prep_met thy "met_eqsys_norm_4x4" [] e_metID wneuper@59367: (["EqSystem","normalise","4x4"], s1210629013@55373: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55373: ("#Find" ,["solution ss'''"])], s1210629013@55373: {rew_ord'="tless_true", rls' = Erls, calc = [], wneuper@59370: srls = append_rls "srls_normalise_4x4" srls wneuper@59389: [Thm ("hd_thm",TermC.num_str @{thm hd_thm}), wneuper@59389: Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59389: Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], s1210629013@55373: prls = Erls, crls = Erls, errpats = [], nrls = Erls}, wneuper@59367: (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) s1210629013@55373: "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ s1210629013@55373: " (let e__s = " ^ s1210629013@55373: " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ s1210629013@55373: " (Repeat (Rewrite commute_0_equality False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ s1210629013@55373: " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ s1210629013@55373: " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ s1210629013@55373: " isolate_bdvs_4x4 False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ s1210629013@55373: " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set order_system False))) e_s " ^ s1210629013@55373: " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^ s1210629013@55373: " [BOOL_LIST e__s, REAL_LIST v_s]))"), wneuper@59269: Specify.prep_met thy "met_eqsys_topdown_4x4" [] e_metID s1210629013@55373: (["EqSystem","top_down_substitution","4x4"], s1210629013@55373: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55373: ("#Where" , (*accepts missing variables up to diagonal form*) s1210629013@55373: ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))", s1210629013@55373: "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))", s1210629013@55373: "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))", s1210629013@55373: "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]), s1210629013@55373: ("#Find", ["solution ss'''"])], s1210629013@55373: {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], s1210629013@55373: srls = append_rls "srls_top_down_4x4" srls [], s1210629013@55373: prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular s1210629013@55373: [Calc ("Atools.occurs'_in",eval_occurs_in "")], s1210629013@55373: crls = Erls, errpats = [], nrls = Erls}, s1210629013@55373: (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) s1210629013@55373: "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ s1210629013@55373: " (let e_1 = NTH 1 e_s; " ^ s1210629013@55373: " e_2 = Take (NTH 2 e_s); " ^ s1210629013@55373: " e_2 = ((Substitute [e_1]) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ s1210629013@55373: " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ s1210629013@55373: " simplify_System_parenthesized False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ s1210629013@55373: " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ s1210629013@55373: " isolate_bdvs False)) @@ " ^ s1210629013@55373: " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ s1210629013@55373: " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ s1210629013@55373: " norm_Rational False))) e_2 " ^ s1210629013@55373: " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")] s1210629013@55373: *} s1210629013@55373: neuper@37906: end