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@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: wneuper@59472: 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 wneuper@59416: then SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) wneuper@59416: else SOME ((Rule.term2str p) ^ " = False", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) neuper@37954: | eval_occur_exactly_in _ _ _ _ = NONE; wneuper@59472: \ wneuper@59472: setup \KEStore_Elems.add_calcs s1210629013@52145: [("occur_exactly_in", s1210629013@52145: ("EqSystem.occur'_exactly'_in", wneuper@59472: eval_occur_exactly_in "#eval_occur_exactly_in_"))]\ wneuper@59472: 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@59390: | "c"::"_"::is => 1000 * ((TermC.int_of_str 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; wneuper@59416: val _ = tracing ("t= f@ts= \"" ^ Rule.term_to_string''' thy f ^ "\" @ \"[" ^ wneuper@59416: commas (map (Rule.term_to_string''' thy) ts) ^ "]\""); wneuper@59416: val _ = tracing ("u= g@us= \"" ^ Rule.term_to_string''' thy g ^ "\" @ \"[" ^ wneuper@59416: commas (map (Rule.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) wneuper@59592: and terms_ord str pr (ts, us) = list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(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: (**) wneuper@59416: Rule.rew_ord' := overwritel (! Rule.rew_ord', neuper@37954: [("ord_simplify_System", ord_simplify_System false thy) neuper@37954: ]); wneuper@59472: \ wneuper@59472: 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 = wneuper@59416: Rule.Rls{id = "order_add_mult_System", preconds = [], neuper@37954: rew_ord = ("ord_simplify_System", bonzai@41919: ord_simplify_System false @{theory "Integrate"}), wneuper@59416: erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}), neuper@37954: (* z * w = w * z *) wneuper@59416: Rule.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@59416: Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}), neuper@37954: (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) wneuper@59416: Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}), neuper@37954: (*z + w = w + z*) wneuper@59416: Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}), neuper@37954: (*x + (y + z) = y + (x + z)*) wneuper@59416: Rule.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: ], wneuper@59416: scr = Rule.EmptyScr}; wneuper@59472: \ wneuper@59472: 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 = wneuper@59416: Rule.Rls {id = "norm_System_noadd_fractions", preconds = [], wneuper@59416: rew_ord = ("dummy_ord",Rule.dummy_ord), wneuper@59416: erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [], neuper@37954: rules = [(*sequence given by operator precedence*) wneuper@59416: Rule.Rls_ discard_minus, wneuper@59416: Rule.Rls_ powers, wneuper@59416: Rule.Rls_ rat_mult_divide, wneuper@59416: Rule.Rls_ expand, wneuper@59416: Rule.Rls_ reduce_0_1_2, wneuper@59416: Rule.Rls_ (*order_add_mult #1*) order_add_mult_System, wneuper@59416: Rule.Rls_ collect_numerals, wneuper@59416: (*Rule.Rls_ add_fractions_p, #2*) wneuper@59416: Rule.Rls_ cancel_p neuper@37954: ], wneuper@59552: scr = Rule.EmptyScr wneuper@59406: }; wneuper@59472: \ wneuper@59472: 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 = wneuper@59416: Rule.Rls {id = "norm_System", preconds = [], wneuper@59416: rew_ord = ("dummy_ord",Rule.dummy_ord), wneuper@59416: erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [], neuper@37954: rules = [(*sequence given by operator precedence*) wneuper@59416: Rule.Rls_ discard_minus, wneuper@59416: Rule.Rls_ powers, wneuper@59416: Rule.Rls_ rat_mult_divide, wneuper@59416: Rule.Rls_ expand, wneuper@59416: Rule.Rls_ reduce_0_1_2, wneuper@59416: Rule.Rls_ (*order_add_mult *1*) order_add_mult_System, wneuper@59416: Rule.Rls_ collect_numerals, wneuper@59416: Rule.Rls_ add_fractions_p, wneuper@59416: Rule.Rls_ cancel_p neuper@37954: ], wneuper@59552: scr = Rule.EmptyScr wneuper@59406: }; wneuper@59472: \ wneuper@59472: 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 = wneuper@59416: Rule.Seq {id = "simplify_System_parenthesized", preconds = []:term list, wneuper@59416: rew_ord = ("dummy_ord", Rule.dummy_ord), wneuper@59416: erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}), neuper@37954: (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) wneuper@59416: Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}), neuper@37954: (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) neuper@37954: (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) wneuper@59416: Rule.Rls_ norm_Rational_noadd_fractions(**2**), wneuper@59416: Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**), wneuper@59416: Rule.Thm ("sym_mult_assoc", wneuper@59389: TermC.num_str (@{thm mult.assoc} RS @{thm sym})) wneuper@59416: (*Rule.Rls_ discard_parentheses *3**), wneuper@59416: Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) wneuper@59416: Rule.Rls_ separate_bdv2, wneuper@59416: Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}; wneuper@59472: \ wneuper@59472: 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 = wneuper@59416: Rule.Seq {id = "simplify_System", preconds = []:term list, wneuper@59416: rew_ord = ("dummy_ord", Rule.dummy_ord), wneuper@59416: erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Rls_ norm_Rational, wneuper@59416: Rule.Rls_ (*order_add_mult_in*) norm_System (**1**), wneuper@59416: Rule.Rls_ discard_parentheses, wneuper@59416: Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) wneuper@59416: Rule.Rls_ separate_bdv2, wneuper@59416: Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}; neuper@37906: (* neuper@37954: val simplify_System = wneuper@59416: Rule.append_rls "simplify_System" simplify_System_parenthesized wneuper@59416: [Rule.Thm ("sym_add_assoc", wneuper@59389: TermC.num_str (@{thm add.assoc} RS @{thm sym}))]; neuper@37954: *) wneuper@59472: \ wneuper@59472: ML \ neuper@37954: val isolate_bdvs = wneuper@59416: Rule.Rls {id="isolate_bdvs", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord", Rule.e_rew_ord), wneuper@59416: erls = Rule.append_rls "erls_isolate_bdvs" Rule.e_rls wneuper@59416: [(Rule.Calc ("EqSystem.occur'_exactly'_in", neuper@37954: eval_occur_exactly_in neuper@37954: "#eval_occur_exactly_in_")) neuper@37954: ], wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], neuper@37997: rules = wneuper@59416: [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}), wneuper@59416: Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}), wneuper@59416: Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})], wneuper@59416: scr = Rule.EmptyScr}; wneuper@59472: \ wneuper@59472: ML \ neuper@37954: val isolate_bdvs_4x4 = wneuper@59416: Rule.Rls {id="isolate_bdvs_4x4", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord", Rule.e_rew_ord), wneuper@59416: erls = Rule.append_rls wneuper@59416: "erls_isolate_bdvs_4x4" Rule.e_rls wneuper@59416: [Rule.Calc ("EqSystem.occur'_exactly'_in", neuper@37954: eval_occur_exactly_in "#eval_occur_exactly_in_"), wneuper@59416: Rule.Calc ("Atools.ident",eval_ident "#ident_"), wneuper@59416: Rule.Calc ("Atools.some'_occur'_in", neuper@37954: eval_some_occur_in "#some_occur_in_"), wneuper@59416: Rule.Thm ("not_true",TermC.num_str @{thm not_true}), wneuper@59416: Rule.Thm ("not_false",TermC.num_str @{thm not_false}) neuper@37954: ], wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}), wneuper@59416: Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}), wneuper@59416: Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}), wneuper@59416: Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add2}), wneuper@59416: Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult}) wneuper@59416: ], scr = Rule.EmptyScr}; neuper@37954: wneuper@59472: \ wneuper@59472: 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 = wneuper@59416: Rule.Rls {id="order_system", preconds = [], neuper@37954: rew_ord = ("ord_simplify_System", neuper@37954: ord_simplify_System false thy), wneuper@59416: erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN}) neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}; neuper@37954: neuper@37954: val prls_triangular = wneuper@59416: Rule.Rls {id="prls_triangular", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord", Rule.e_rew_ord), wneuper@59416: erls = Rule.Rls {id="erls_prls_triangular", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord", Rule.e_rew_ord), wneuper@59416: erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], neuper@37997: rules = [(*for precond NTH_CONS ...*) wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_") neuper@37954: (*immediately repeated rewrite pushes neuper@37954: '+' into precondition !*) neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}, wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), wneuper@59416: Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59416: Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}), wneuper@59416: Rule.Calc ("EqSystem.occur'_exactly'_in", neuper@37954: eval_occur_exactly_in neuper@37954: "#eval_occur_exactly_in_") neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}; wneuper@59472: \ wneuper@59472: ML \ neuper@37954: neuper@37954: (*WN060914 quickly created for 4x4; neuper@37954: more similarity to prls_triangular desirable*) neuper@37954: val prls_triangular4 = wneuper@59416: Rule.Rls {id="prls_triangular4", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord", Rule.e_rew_ord), wneuper@59416: erls = Rule.Rls {id="erls_prls_triangular4", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord", Rule.e_rew_ord), wneuper@59416: erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], neuper@37997: rules = [(*for precond NTH_CONS ...*) wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_") neuper@37954: (*immediately repeated rewrite pushes neuper@37954: '+' into precondition !*) neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}, wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), wneuper@59416: Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59416: Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}), wneuper@59416: Rule.Calc ("EqSystem.occur'_exactly'_in", neuper@37954: eval_occur_exactly_in neuper@37954: "#eval_occur_exactly_in_") neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr}; wneuper@59472: \ t@42197: wneuper@59472: 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)), wneuper@59472: ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))]\ t@42197: neuper@37954: (** problems **) wneuper@59472: setup \KEStore_Elems.add_pbts wneuper@59406: [(Specify.prep_pbt thy "pbl_equsys" [] Celem.e_pblID s1210629013@55339: (["system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Find" ,["solution ss'''"](*''' is copy-named*))], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.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'''"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.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'''"])], wneuper@59416: Rule.append_rls "prls_2x2_linear_system" Rule.e_rls wneuper@59416: [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), wneuper@59416: Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("HOL.eq",eval_equal "#equal_")], s1210629013@55339: SOME "solveSystem e_s v_s", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.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@59406: (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Celem.e_pblID wneuper@59367: (["normalise", "2x2", "LINEAR", "system"], s1210629013@55339: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55339: ("#Find" ,["solution ss'''"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], s1210629013@55339: SOME "solveSystem e_s v_s", wneuper@59367: [["EqSystem","normalise","2x2"]])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.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'''"])], wneuper@59416: Rule.append_rls "prls_3x3_linear_system" Rule.e_rls wneuper@59416: [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), wneuper@59416: Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("HOL.eq",eval_equal "#equal_")], s1210629013@55339: SOME "solveSystem e_s v_s", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.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'''"])], wneuper@59416: Rule.append_rls "prls_4x4_linear_system" Rule.e_rls wneuper@59416: [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), wneuper@59416: Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("HOL.eq",eval_equal "#equal_")], s1210629013@55339: SOME "solveSystem e_s v_s", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.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'''"])], wneuper@59416: Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular wneuper@59416: [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")], s1210629013@55339: SOME "solveSystem e_s v_s", s1210629013@55339: [["EqSystem","top_down_substitution","4x4"]])), wneuper@59406: (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.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'''"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], s1210629013@55339: SOME "solveSystem e_s v_s", wneuper@59472: [["EqSystem","normalise","4x4"]]))]\ neuper@37954: wneuper@59472: ML \ neuper@37997: (*this is for NTH only*) wneuper@59416: val srls = Rule.Rls {id="srls_normalise_4x4", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), wneuper@59416: erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls neuper@37997: [(*for asm in NTH_CONS ...*) wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), neuper@37997: (*2nd NTH_CONS pushes n+-1 into asms*) wneuper@59416: Rule.Calc("Groups.plus_class.plus", eval_binop "#add_") neuper@37954: ], wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), wneuper@59416: Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})], wneuper@59416: scr = Rule.EmptyScr}; wneuper@59472: \ neuper@37954: s1210629013@55380: (**methods**) wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_eqsys" [] Celem.e_metID s1210629013@55373: (["EqSystem"], [], wneuper@59416: {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, wneuper@59416: errpats = [], nrls = Rule.Erls}, wneuper@59545: @{thm refl}), wneuper@59406: Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID s1210629013@55373: (["EqSystem","top_down_substitution"], [], wneuper@59416: {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, wneuper@59416: errpats = [], nrls = Rule.Erls}, wneuper@59545: @{thm refl})] wneuper@59473: \ wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system :: "bool list => real list => bool list" wneuper@59504: where wneuper@59504: "solve_system e_s v_s = wneuper@59504: (let e_1 = Take (hd e_s); wneuper@59504: e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] wneuper@59504: ''isolate_bdvs'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] wneuper@59504: ''simplify_System'' False))) e_1; wneuper@59504: e_2 = Take (hd (tl e_s)); wneuper@59504: e_2 = ((Substitute [e_1]) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] wneuper@59504: ''simplify_System_parenthesized'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] wneuper@59504: ''isolate_bdvs'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] wneuper@59504: ''simplify_System'' False))) e_2; wneuper@59504: e__s = Take [e_1, e_2] wneuper@59504: in Try (Rewrite_Set ''order_system'' False) e__s) " wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.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'''"])], wneuper@59416: {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [], wneuper@59416: srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls wneuper@59416: [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), wneuper@59416: Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59416: Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], wneuper@59416: prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, wneuper@59551: @{thm solve_system.simps})] wneuper@59473: \ wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID wneuper@59367: (["EqSystem", "normalise"], [], wneuper@59416: {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, wneuper@59416: errpats = [], nrls = Rule.Erls}, wneuper@59545: @{thm refl})] wneuper@59473: \ wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system2 :: "bool list => real list => bool list" wneuper@59504: where wneuper@59545: "solve_system2 e_s v_s = wneuper@59504: (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] wneuper@59504: ''simplify_System_parenthesized'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] wneuper@59504: ''isolate_bdvs'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] wneuper@59504: ''simplify_System_parenthesized'' False)) @@ wneuper@59504: (Try (Rewrite_Set ''order_system'' False))) e_s wneuper@59504: in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met'']) wneuper@59504: [BOOL_LIST e__s, REAL_LIST v_s]))" wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID wneuper@59367: (["EqSystem","normalise","2x2"], s1210629013@55373: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55373: ("#Find" ,["solution ss'''"])], wneuper@59416: {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], wneuper@59416: srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls wneuper@59416: [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), wneuper@59416: Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59416: Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], wneuper@59416: prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, wneuper@59551: @{thm solve_system2.simps})] wneuper@59473: \ wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system3 :: "bool list => real list => bool list" wneuper@59504: where wneuper@59545: "solve_system3 e_s v_s = wneuper@59504: (let e__s = wneuper@59504: ((Try (Rewrite_Set ''norm_Rational'' False)) @@ wneuper@59504: (Repeat (Rewrite ''commute_0_equality'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), wneuper@59504: (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] wneuper@59504: ''simplify_System_parenthesized'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), wneuper@59504: (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] wneuper@59504: ''isolate_bdvs_4x4'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), wneuper@59504: (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] wneuper@59504: ''simplify_System_parenthesized'' False)) @@ wneuper@59504: (Try (Rewrite_Set ''order_system'' False))) e_s wneuper@59504: in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met'']) wneuper@59504: [BOOL_LIST e__s, REAL_LIST v_s]))" wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID wneuper@59367: (["EqSystem","normalise","4x4"], s1210629013@55373: [("#Given" ,["equalities e_s", "solveForVars v_s"]), s1210629013@55373: ("#Find" ,["solution ss'''"])], wneuper@59416: {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], wneuper@59416: srls = Rule.append_rls "srls_normalise_4x4" srls wneuper@59416: [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), wneuper@59416: Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), wneuper@59416: Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], wneuper@59416: prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, wneuper@59367: (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) wneuper@59551: @{thm solve_system3.simps})] wneuper@59473: \ wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system4 :: "bool list => real list => bool list" wneuper@59504: where wneuper@59545: "solve_system4 e_s v_s = wneuper@59504: (let e_1 = NTH 1 e_s; wneuper@59504: e_2 = Take (NTH 2 e_s); wneuper@59504: e_2 = ((Substitute [e_1]) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s), wneuper@59504: (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)] wneuper@59504: ''simplify_System_parenthesized'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s), wneuper@59504: (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)] wneuper@59504: ''isolate_bdvs'' False)) @@ wneuper@59504: (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s), wneuper@59504: (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)] wneuper@59504: ''norm_Rational'' False))) e_2 wneuper@59504: in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])" wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.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'''"])], wneuper@59416: {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [], wneuper@59416: srls = Rule.append_rls "srls_top_down_4x4" srls [], wneuper@59416: prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular wneuper@59416: [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")], wneuper@59416: crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, s1210629013@55373: (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) wneuper@59551: @{thm solve_system4.simps})] wneuper@59472: \ s1210629013@55373: neuper@37906: end