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@37954: theory EqSystem imports Rational Root begin neuper@37906: neuper@37906: consts neuper@37906: neuper@37906: occur'_exactly'_in :: neuper@37906: "[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _") neuper@37906: neuper@37906: (*descriptions in the related problems*) neuper@37906: solveForVars :: real list => toreall neuper@37906: 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@37954: "[| [] 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@37954: "[| [] 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@37982: fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) neuper@37982: (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) neuper@37982: | Term_Ord.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@37954: (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\""); neuper@37954: val _=writeln("u= g@us= \""^ neuper@37954: ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ neuper@37954: (commas(map(string_of_cterm o cterm_of(sign_of 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@37982: prod_ord (prod_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@37954: list_ord (term_ord' pr (assoc_thy "Isac.thy"))(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@37954: neuper@37954: 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@37954: 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@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@37954: 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@37965: Thm ("nadd_divide_distrib",num_str @{thm nadd_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@37954: 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@37954: 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@37954: rules = [Thm ("commute_0_equality", neuper@37966: num_str @{commute_0_equality), neuper@37969: Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}), neuper@37969: Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})], neuper@37954: scr = EmptyScr}; 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@37954: rules = [Thm ("commute_0_equality", neuper@37966: num_str @{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@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@37954: 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@37969: rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), neuper@37954: Calc ("op +", eval_binop "#add_"), neuper@37969: 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@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@37954: 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@37969: rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), neuper@37954: Calc ("op +", eval_binop "#add_"), neuper@37969: Thm ("nth_Nil_",num_str @{thm 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@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@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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Find" ,["solution ss___"](*___ is copy-named*)) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [(*for preds in where_*)], neuper@37954: SOME "solveSystem es_ vs_", neuper@37954: [])); neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_equsys_lin" [] e_pblID neuper@37954: (["linear", "system"], neuper@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: (*TODO.WN050929 check linearity*) neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [(*for preds in where_*)], neuper@37954: SOME "solveSystem es_ vs_", 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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]), neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: append_rls "prls_2x2_linear_system" e_rls neuper@37969: [Thm ("length_Cons_",num_str @{thm length_Cons_}), neuper@37969: 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@37954: SOME "solveSystem es_ vs_", neuper@37954: [])); neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID neuper@37954: (["triangular", "2x2", "linear", "system"], neuper@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" , neuper@37954: ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", neuper@37954: " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: prls_triangular, neuper@37954: SOME "solveSystem es_ vs_", 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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [(*for preds in where_*)], neuper@37954: SOME "solveSystem es_ vs_", 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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]), neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: append_rls "prls_3x3_linear_system" e_rls neuper@37969: [Thm ("length_Cons_",num_str @{thm length_Cons_}), neuper@37969: 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@37954: SOME "solveSystem es_ vs_", 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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]), neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: append_rls "prls_4x4_linear_system" e_rls neuper@37969: [Thm ("length_Cons_",num_str @{thm length_Cons_}), neuper@37969: 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@37954: SOME "solveSystem es_ vs_", neuper@37954: [])); neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID neuper@37954: (["triangular", "4x4", "linear", "system"], neuper@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" , (*accepts missing variables up to diagional form*) neuper@37954: ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", neuper@37954: "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", neuper@37954: "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", neuper@37954: "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" neuper@37954: ]), neuper@37954: ("#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@37954: SOME "solveSystem es_ vs_", neuper@37954: [["EqSystem","top_down_substitution","4x4"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID neuper@37954: (["normalize", "4x4", "linear", "system"], neuper@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: (*length_ is checked 1 level above*) neuper@37954: ("#Find" ,["solution ss___"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [(*for preds in where_*)], neuper@37954: SOME "solveSystem es_ vs_", neuper@37954: [["EqSystem","normalize","4x4"]])); neuper@37954: neuper@37954: neuper@37954: (* show_ptyps(); neuper@37954: *) neuper@37954: 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@37954: store_met neuper@37972: (prep_met thy "met_eqsys_topdown_2x2" [] e_metID neuper@37954: (["EqSystem","top_down_substitution","2x2"], neuper@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" , neuper@37954: ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", neuper@37954: " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), neuper@37954: ("#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@37954: "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ neuper@37954: " (let e1__ = Take (hd es_); " ^ neuper@37954: " e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " isolate_bdvs False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System False))) e1__; " ^ neuper@37954: " e2__ = Take (hd (tl es_)); " ^ neuper@37954: " e2__ = ((Substitute [e1__]) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " isolate_bdvs False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System False))) e2__; " ^ neuper@37954: " es__ = Take [e1__, e2__] " ^ neuper@37954: " in (Try (Rewrite_Set order_system False)) es__)" neuper@37954: (*--------------------------------------------------------------------------- neuper@37954: this script does NOT separate the equations as abolve, 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@37954: "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ neuper@37954: " (let es__ = Take es_; " ^ neuper@37954: " e1__ = hd es__; " ^ neuper@37954: " e2__ = hd (tl es__); " ^ neuper@37954: " es__ = [e1__, Substitute [e1__] e2__] " ^ neuper@37954: " in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] " ^ neuper@37954: " isolate_bdvs False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System False))) es__)" neuper@37954: ---------------------------------------------------------------------------*) neuper@37954: )); 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@37954: store_met neuper@37972: (prep_met thy "met_eqsys_norm_2x2" [] e_metID neuper@37954: (["EqSystem","normalize","2x2"], neuper@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#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@37954: "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ neuper@37954: " (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " isolate_bdvs False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set order_system False))) es_ " ^ neuper@37954: " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ neuper@37954: " [bool_list_ es__, real_list_ vs_]))" neuper@37954: )); neuper@37954: neuper@37954: (*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@37954: [(*for asm in nth_Cons_ ...*) neuper@37954: Calc ("op <",eval_equ "#less_"), neuper@37954: (*2nd nth_Cons_ pushes n+-1 into asms*) neuper@37954: Calc("op +", eval_binop "#add_") neuper@37954: ], neuper@37954: srls = Erls, calc = [], neuper@37969: rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), neuper@37954: Calc("op +", eval_binop "#add_"), neuper@37969: 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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#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@37954: "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ neuper@37954: " (let es__ = " ^ neuper@37954: " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ neuper@37954: " (Repeat (Rewrite commute_0_equality False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ neuper@37954: " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ neuper@37954: " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ neuper@37954: " isolate_bdvs_4x4 False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ neuper@37954: " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set order_system False))) es_ " ^ neuper@37954: " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ neuper@37954: " [bool_list_ es__, real_list_ vs_]))" 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@37954: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37954: ("#Where" , (*accepts missing variables up to diagonal form*) neuper@37954: ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", neuper@37954: "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", neuper@37954: "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", neuper@37954: "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" neuper@37954: ]), neuper@37954: ("#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@37954: "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ neuper@37954: " (let e1_ = nth_ 1 es_; " ^ neuper@37954: " e2_ = Take (nth_ 2 es_); " ^ neuper@37954: " e2_ = ((Substitute [e1_]) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ neuper@37954: " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ neuper@37954: " simplify_System_parenthesized False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ neuper@37954: " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ neuper@37954: " isolate_bdvs False)) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ neuper@37954: " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ neuper@37954: " norm_Rational False))) e2_ " ^ neuper@37954: " in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])" neuper@37954: )); neuper@37954: *} neuper@37954: neuper@37906: end