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: walther@60278: 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: walther@60377: lemma commute_0_equality : \(0 = a) = (a = 0)\ walther@60377: by auto walther@60377: neuper@52148: axiomatization where 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 !*) walther@60377: (* these require lemmas about occur_exactly_in* ) walther@60377: lemma xxx : walther@60377: \[| [] from [bdv_1, bdv_2, bdv_3, bdv_4] occur_exactly_in a |] ==> (a + b = c) = (b = c + -1 * a)\ walther@60377: by auto walther@60377: ( **) 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; walther@60377: works for lists of any length, interestingly !?! walther@60377: CONTRADICTS PROPERTIES OF LIST: take set instead*) neuper@37906: wneuper@59472: ML \ 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 = walther@59603: let fun occurs_in' a b = Prog_Expr.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: walther@60278: (*("occur_exactly_in", ("EqSystem.occur_exactly_in", walther@60330: eval_occur_exactly_in "#eval_occur_exactly_in_") )*) walther@60278: fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in" walther@60335: (p as (Const (\<^const_name>\EqSystem.occur_exactly_in\,_) neuper@37954: $ vs $ all $ t)) _ = wneuper@59389: if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t walther@59868: then SOME ((UnparseC.term p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) walther@59868: else SOME ((UnparseC.term p) ^ " = False", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) neuper@37954: | eval_occur_exactly_in _ _ _ _ = NONE; wneuper@59472: \ wenzelm@60313: calculation occur_exactly_in = \eval_occur_exactly_in "#eval_occur_exactly_in_"\ wenzelm@60313: wneuper@59472: ML \ neuper@37954: (** rewrite order 'ord_simplify_System' **) neuper@37954: walther@59997: (* 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) walther@60269: | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4) walther@60269: | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def."; 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; walther@60375: val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^ walther@59870: commas (map (UnparseC.term_in_thy thy) ts) ^ "]\""); walther@60375: val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^ walther@59870: commas (map (UnparseC.term_in_thy thy) us) ^ "]\""); walther@60375: val _ = tracing ("size_of_term (t, u) = (" ^ string_of_int (size_of_term' t) ^ ", " ^ neuper@52070: string_of_int (size_of_term' u) ^ ")"); walther@60375: val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) ); walther@60375: (** )val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}( **) walther@60375: val _ = tracing ("terms_ord (ts, us) = " ^(pr_ord o terms_ord str false) (ts,us)); walther@60375: 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) walther@60269: and terms_ord _ pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "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*) walther@60324: fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = walther@60324: (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS); Walther@60506: Walther@60506: (**)end;(**) Walther@60506: \ ML \ wneuper@59472: \ Walther@60506: setup \KEStore_Elems.add_rew_ord [ Walther@60506: ("ord_simplify_System", ord_simplify_System false \<^theory>)]\ Walther@60506: 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 = walther@60358: Rule_Def.Repeat{ walther@60358: id = "order_add_mult_System", preconds = [], walther@60358: rew_ord = ("ord_simplify_System", ord_simplify_System false @{theory "Integrate"}), walther@60358: erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\mult.commute\, (* z * w = w * z *) walther@60358: \<^rule_thm>\real_mult_left_commute\, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) walther@60358: \<^rule_thm>\mult.assoc\, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) walther@60358: \<^rule_thm>\add.commute\, (*z + w = w + z*) walther@60358: \<^rule_thm>\add.left_commute\, (*x + (y + z) = y + (x + z)*) walther@60358: \<^rule_thm>\add.assoc\ ], (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) walther@60358: scr = Rule.Empty_Prog}; 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 = walther@59851: Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [], Walther@60509: rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), walther@60358: erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [(*sequence given by operator precedence*) walther@60358: Rule.Rls_ discard_minus, walther@60358: Rule.Rls_ powers, walther@60358: Rule.Rls_ rat_mult_divide, walther@60358: Rule.Rls_ expand, walther@60358: Rule.Rls_ reduce_0_1_2, walther@60358: Rule.Rls_ (*order_add_mult #1*) order_add_mult_System, walther@60358: Rule.Rls_ collect_numerals, walther@60358: (*Rule.Rls_ add_fractions_p, #2*) walther@60358: Rule.Rls_ cancel_p], walther@60358: scr = Rule.Empty_Prog}; 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 = walther@59851: Rule_Def.Repeat {id = "norm_System", preconds = [], Walther@60509: rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), walther@60358: erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [(*sequence given by operator precedence*) walther@60358: Rule.Rls_ discard_minus, walther@60358: Rule.Rls_ powers, walther@60358: Rule.Rls_ rat_mult_divide, walther@60358: Rule.Rls_ expand, walther@60358: Rule.Rls_ reduce_0_1_2, walther@60358: Rule.Rls_ (*order_add_mult *1*) order_add_mult_System, walther@60358: Rule.Rls_ collect_numerals, walther@60358: Rule.Rls_ add_fractions_p, walther@60358: Rule.Rls_ cancel_p], walther@60358: scr = Rule.Empty_Prog}; 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 = walther@59878: Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list, Walther@60509: rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), walther@60358: erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\distrib_right\, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) walther@60358: \<^rule_thm>\add_divide_distrib\, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) walther@60358: Rule.Rls_ norm_Rational_noadd_fractions, walther@60358: Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions, walther@60358: \<^rule_thm_sym>\mult.assoc\, walther@60358: Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) walther@60358: Rule.Rls_ separate_bdv2, walther@60358: \<^rule_eval>\divide\ (Prog_Expr.eval_cancel "#divide_e")], walther@60358: scr = Rule.Empty_Prog}; 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 = walther@59878: Rule_Set.Sequence {id = "simplify_System", preconds = []:term list, Walther@60509: rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), walther@60358: erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: Rule.Rls_ norm_Rational, walther@60358: Rule.Rls_ (*order_add_mult_in*) norm_System (**1**), walther@60358: Rule.Rls_ discard_parentheses, walther@60358: Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) walther@60358: Rule.Rls_ separate_bdv2, walther@60358: \<^rule_eval>\divide\ (Prog_Expr.eval_cancel "#divide_e")], walther@60358: scr = Rule.Empty_Prog}; neuper@37906: (* neuper@37954: val simplify_System = walther@59852: Rule_Set.append_rules "simplify_System" simplify_System_parenthesized wenzelm@60296: [\<^rule_thm_sym>\add.assoc\]; neuper@37954: *) wneuper@59472: \ wneuper@59472: ML \ neuper@37954: val isolate_bdvs = walther@60358: Rule_Def.Repeat { Walther@60509: id="isolate_bdvs", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), walther@60358: erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [ walther@60358: (\<^rule_eval>\occur_exactly_in\ (eval_occur_exactly_in "#eval_occur_exactly_in_"))], walther@60358: srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\commute_0_equality\, walther@60358: \<^rule_thm>\separate_bdvs_add\, walther@60358: \<^rule_thm>\separate_bdvs_mult\], walther@60358: scr = Rule.Empty_Prog}; wneuper@59472: \ wneuper@59472: ML \ neuper@37954: val isolate_bdvs_4x4 = walther@60358: Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [], Walther@60509: rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), walther@60358: erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [ walther@60358: \<^rule_eval>\occur_exactly_in\ (eval_occur_exactly_in "#eval_occur_exactly_in_"), walther@60358: \<^rule_eval>\Prog_Expr.ident\ (Prog_Expr.eval_ident "#ident_"), walther@60358: \<^rule_eval>\Prog_Expr.some_occur_in\ (Prog_Expr.eval_some_occur_in "#some_occur_in_"), walther@60358: \<^rule_thm>\not_true\, walther@60358: \<^rule_thm>\not_false\], walther@60358: srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\commute_0_equality\, walther@60358: \<^rule_thm>\separate_bdvs0\, walther@60358: \<^rule_thm>\separate_bdvs_add1\, walther@60358: \<^rule_thm>\separate_bdvs_add2\, walther@60358: \<^rule_thm>\separate_bdvs_mult\], walther@60358: scr = Rule.Empty_Prog}; 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 = walther@60358: Rule_Def.Repeat {id="order_system", preconds = [], walther@60358: rew_ord = ("ord_simplify_System", ord_simplify_System false \<^theory>), walther@60358: erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\order_system_NxN\], walther@60358: scr = Rule.Empty_Prog}; neuper@37954: neuper@37954: val prls_triangular = walther@60358: Rule_Def.Repeat { Walther@60509: id="prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), walther@60358: erls = Rule_Def.Repeat { Walther@60509: id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), walther@60358: erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [(*for precond NTH_CONS ...*) walther@60358: \<^rule_eval>\less\ (Prog_Expr.eval_equ "#less_"), walther@60358: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), walther@60358: \<^rule_eval>\occur_exactly_in\ (eval_occur_exactly_in "#eval_occur_exactly_in_")], walther@60358: (*immediately repeated rewrite pushes '+' into precondition !*) walther@60358: scr = Rule.Empty_Prog}, walther@60358: srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\NTH_CONS\, walther@60358: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), walther@60358: \<^rule_thm>\NTH_NIL\, walther@60358: \<^rule_thm>\tl_Cons\, walther@60358: \<^rule_thm>\tl_Nil\, walther@60358: \<^rule_eval>\occur_exactly_in\ (eval_occur_exactly_in "#eval_occur_exactly_in_")], walther@60358: scr = Rule.Empty_Prog}; 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 = walther@60358: Rule_Def.Repeat { Walther@60509: id="prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), walther@60358: erls = Rule_Def.Repeat { Walther@60509: id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), walther@60358: erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [(*for precond NTH_CONS ...*) walther@60358: \<^rule_eval>\less\ (Prog_Expr.eval_equ "#less_"), walther@60358: \<^rule_eval>\plus\ (**)(eval_binop "#add_")], walther@60358: (*immediately repeated rewrite pushes '+' into precondition !*) walther@60358: scr = Rule.Empty_Prog}, walther@60358: srls = Rule_Set.Empty, calc = [], errpatts = [], walther@60358: rules = [ walther@60358: \<^rule_thm>\NTH_CONS\, walther@60358: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), walther@60358: \<^rule_thm>\NTH_NIL\, walther@60358: \<^rule_thm>\tl_Cons\, walther@60358: \<^rule_thm>\tl_Nil\, walther@60358: \<^rule_eval>\occur_exactly_in\ (eval_occur_exactly_in "#eval_occur_exactly_in_")], walther@60358: scr = Rule.Empty_Prog}; wneuper@59472: \ t@42197: wenzelm@60289: rule_set_knowledge wenzelm@60286: simplify_System_parenthesized = \prep_rls' simplify_System_parenthesized\ and wenzelm@60286: simplify_System = \prep_rls' simplify_System\ and wenzelm@60286: isolate_bdvs = \prep_rls' isolate_bdvs\ and wenzelm@60286: isolate_bdvs_4x4 = \prep_rls' isolate_bdvs_4x4\ and wenzelm@60286: order_system = \prep_rls' order_system\ and wenzelm@60286: order_add_mult_System = \prep_rls' order_add_mult_System\ and wenzelm@60286: norm_System_noadd_fractions = \prep_rls' norm_System_noadd_fractions\ and wenzelm@60286: norm_System = \prep_rls' norm_System\ t@42197: walther@60023: walther@60023: section \Problems\ walther@60023: wenzelm@60306: problem pbl_equsys : "system" = wenzelm@60306: \Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\ wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Find: "solution ss'''" (*''' is copy-named*) wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin : "LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\ wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: (*TODO.WN050929 check linearity*) wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_2x2: "2x2/LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty wenzelm@60306: [\<^rule_thm>\LENGTH_CONS\, wenzelm@60306: \<^rule_thm>\LENGTH_NIL\, wenzelm@60306: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), wenzelm@60306: \<^rule_eval>\HOL.eq\ (Prog_Expr.eval_equal "#equal_")]\ wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Where: "Length (e_s:: bool list) = 2" "Length v_s = 2" wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_2x2_tri : "triangular/2x2/LINEAR/system" = wenzelm@60306: \prls_triangular\ Walther@60449: Method_Ref: "EqSystem/top_down_substitution/2x2" wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Where: wenzelm@60306: "(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))" wenzelm@60306: " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))" wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_2x2_norm : "normalise/2x2/LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\ Walther@60449: Method_Ref: "EqSystem/normalise/2x2" wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_3x3 : "3x3/LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty wenzelm@60306: [\<^rule_thm>\LENGTH_CONS\, wenzelm@60306: \<^rule_thm>\LENGTH_NIL\, wenzelm@60306: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), wenzelm@60306: \<^rule_eval>\HOL.eq\ (Prog_Expr.eval_equal "#equal_")]\ wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Where: "Length (e_s:: bool list) = 3" "Length v_s = 3" wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_4x4 : "4x4/LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty wenzelm@60306: [\<^rule_thm>\LENGTH_CONS\, wenzelm@60306: \<^rule_thm>\LENGTH_NIL\, wenzelm@60306: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), wenzelm@60306: \<^rule_eval>\HOL.eq\ (Prog_Expr.eval_equal "#equal_")]\ wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Where: "Length (e_s:: bool list) = 4" "Length v_s = 4" wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_4x4_tri : "triangular/4x4/LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular wenzelm@60306: [\<^rule_eval>\Prog_Expr.occurs_in\ (Prog_Expr.eval_occurs_in "")]\ Walther@60449: Method_Ref: "EqSystem/top_down_substitution/4x4" wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: Where: (*accepts missing variables up to diagional form*) wenzelm@60306: "(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))" wenzelm@60306: "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))" wenzelm@60306: "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))" wenzelm@60306: "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))" wenzelm@60306: Find: "solution ss'''" wenzelm@60306: wenzelm@60306: problem pbl_equsys_lin_4x4_norm : "normalise/4x4/LINEAR/system" = wenzelm@60306: \Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\ Walther@60449: Method_Ref: "EqSystem/normalise/4x4" wenzelm@60306: CAS: "solveSystem e_s v_s" wenzelm@60306: Given: "equalities e_s" "solveForVars v_s" wenzelm@60306: (*Length is checked 1 level above*) wenzelm@60306: Find: "solution ss'''" neuper@37954: wneuper@59472: ML \ neuper@37997: (*this is for NTH only*) walther@59851: val srls = Rule_Def.Repeat {id="srls_normalise_4x4", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), walther@59852: erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty neuper@37997: [(*for asm in NTH_CONS ...*) wenzelm@60294: \<^rule_eval>\less\ (Prog_Expr.eval_equ "#less_"), neuper@37997: (*2nd NTH_CONS pushes n+-1 into asms*) wenzelm@60294: \<^rule_eval>\plus\ (**)(eval_binop "#add_") neuper@37954: ], walther@59851: srls = Rule_Set.Empty, calc = [], errpatts = [], wenzelm@60297: rules = [\<^rule_thm>\NTH_CONS\, wenzelm@60294: \<^rule_eval>\plus\ (**)(eval_binop "#add_"), wenzelm@60297: \<^rule_thm>\NTH_NIL\], walther@59878: scr = Rule.Empty_Prog}; wneuper@59472: \ neuper@37954: walther@60023: section \Methods\ walther@60023: wenzelm@60303: method met_eqsys : "EqSystem" = wenzelm@60303: \{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty, wenzelm@60303: errpats = [], nrls = Rule_Set.Empty}\ wenzelm@60303: wenzelm@60303: method met_eqsys_topdown : "EqSystem/top_down_substitution" = wenzelm@60303: \{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty, wenzelm@60303: errpats = [], nrls = Rule_Set.Empty}\ wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system :: "bool list => real list => bool list" wneuper@59504: where walther@59635: "solve_system e_s v_s = ( walther@59635: let walther@59635: e_1 = Take (hd e_s); walther@59635: e_1 = ( walther@59637: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System'')) walther@59635: ) e_1; walther@59635: e_2 = Take (hd (tl e_s)); walther@59635: e_2 = ( walther@59637: (Substitute [e_1]) #> walther@59637: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #> walther@59637: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System'' )) walther@59635: ) e_2; walther@59635: e__s = Take [e_1, e_2] walther@59635: in walther@59635: Try (Rewrite_Set ''order_system'' ) e__s) " wenzelm@60303: wenzelm@60303: method met_eqsys_topdown_2x2 : "EqSystem/top_down_substitution/2x2" = wenzelm@60303: \{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], wenzelm@60303: srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty wenzelm@60303: [\<^rule_thm>\hd_thm\, wenzelm@60303: \<^rule_thm>\tl_Cons\, wenzelm@60303: \<^rule_thm>\tl_Nil\], wenzelm@60303: prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\ wenzelm@60303: Program: solve_system.simps wenzelm@60303: Given: "equalities e_s" "solveForVars v_s" wenzelm@60303: Where: wenzelm@60303: "(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))" wenzelm@60303: " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))" wenzelm@60303: Find: "solution ss'''" wenzelm@60303: wenzelm@60303: method met_eqsys_norm : "EqSystem/normalise" = wenzelm@60303: \{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty, wenzelm@60303: errpats = [], nrls = Rule_Set.Empty}\ wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system2 :: "bool list => real list => bool list" wneuper@59504: where walther@59635: "solve_system2 e_s v_s = ( walther@59635: let walther@59635: e__s = ( walther@59637: (Try (Rewrite_Set ''norm_Rational'' )) #> walther@59637: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #> walther@59637: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) #> walther@59637: (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #> walther@59635: (Try (Rewrite_Set ''order_system'' )) walther@59635: ) e_s walther@59635: in walther@59635: SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met'']) walther@59635: [BOOL_LIST e__s, REAL_LIST v_s])" wenzelm@60303: wenzelm@60303: method met_eqsys_norm_2x2 : "EqSystem/normalise/2x2" = wenzelm@60303: \{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], wenzelm@60303: srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty wenzelm@60303: [\<^rule_thm>\hd_thm\, wenzelm@60303: \<^rule_thm>\tl_Cons\, wenzelm@60303: \<^rule_thm>\tl_Nil\], wenzelm@60303: prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\ wenzelm@60303: Program: solve_system2.simps wenzelm@60303: Given: "equalities e_s" "solveForVars v_s" wenzelm@60303: Find: "solution ss'''" wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system3 :: "bool list => real list => bool list" wneuper@59504: where walther@59635: "solve_system3 e_s v_s = ( walther@59635: let walther@59635: e__s = ( walther@59637: (Try (Rewrite_Set ''norm_Rational'' )) #> walther@59637: (Repeat (Rewrite ''commute_0_equality'' )) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ), walther@59637: (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ), walther@59637: (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ), walther@59637: (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) #> walther@59635: (Try (Rewrite_Set ''order_system'')) walther@59635: ) e_s walther@59635: in walther@59635: SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met'']) walther@59635: [BOOL_LIST e__s, REAL_LIST v_s])" wenzelm@60303: wenzelm@60303: method met_eqsys_norm_4x4 : "EqSystem/normalise/4x4" = wenzelm@60303: \{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], wenzelm@60303: srls = wenzelm@60303: Rule_Set.append_rules "srls_normalise_4x4" srls wenzelm@60303: [\<^rule_thm>\hd_thm\, \<^rule_thm>\tl_Cons\, \<^rule_thm>\tl_Nil\], wenzelm@60303: prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\ wenzelm@60303: Program: solve_system3.simps wenzelm@60303: Given: "equalities e_s" "solveForVars v_s" wenzelm@60303: Find: "solution ss'''" wenzelm@60303: (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*) wneuper@59545: wneuper@59504: partial_function (tailrec) solve_system4 :: "bool list => real list => bool list" wneuper@59504: where walther@59635: "solve_system4 e_s v_s = ( walther@59635: let walther@59635: e_1 = NTH 1 e_s; walther@59635: e_2 = Take (NTH 2 e_s); walther@59635: e_2 = ( walther@59637: (Substitute [e_1]) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s), walther@59637: (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s), walther@59637: (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) #> walther@59635: (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s), walther@59635: (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''norm_Rational'' )) walther@59635: ) e_2 walther@59635: in walther@59635: [e_1, e_2, NTH 3 e_s, NTH 4 e_s])" wenzelm@60303: wenzelm@60303: method met_eqsys_topdown_4x4 : "EqSystem/top_down_substitution/4x4" = wenzelm@60303: \{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], wenzelm@60303: srls = Rule_Set.append_rules "srls_top_down_4x4" srls [], wenzelm@60303: prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular walther@60358: [\<^rule_eval>\Prog_Expr.occurs_in\ (Prog_Expr.eval_occurs_in "")], wenzelm@60303: crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\ wenzelm@60303: (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*) wenzelm@60303: Program: solve_system4.simps wenzelm@60303: Given: "equalities e_s" "solveForVars v_s" wenzelm@60303: Where: (*accepts missing variables up to diagonal form*) wenzelm@60303: "(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))" wenzelm@60303: "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))" wenzelm@60303: "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))" wenzelm@60303: "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))" wenzelm@60303: Find: "solution ss'''" wenzelm@60303: wenzelm@60303: ML \ walther@60278: \ ML \ walther@60278: \ ML \ wneuper@59472: \ walther@60278: end