# HG changeset patch # User Walther Neuper # Date 1284018554 -7200 # Node ID 8721c71fe3a3382008b0d685456d768f3ae8e867 # Parent eb7d9cbaa3ef7d41a4a84d22134c381377b31410 intermediate state in Knowledge/EqSystem.thy diff -r eb7d9cbaa3ef -r 8721c71fe3a3 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:55:08 2010 +0200 +++ b/src/Tools/isac/Build_Isac.thy Thu Sep 09 09:49:14 2010 +0200 @@ -80,8 +80,9 @@ use_thy "Knowledge/LogExp" use_thy "Knowledge/Diff" use_thy "Knowledge/DiffApp" +use_thy "Knowledge/Integrate" -use_thy "Knowledge/Integrate" +use_thy "Knowledge/EqSystem" ML {* 111; *} @@ -89,7 +90,6 @@ text {*------------------------------------------*} (* -use_thy "Knowledge/EqSystem" use_thy "Knowledge/Biegelinie" use_thy "Knowledge/AlgEin" use_thy "Knowledge/Test" diff -r eb7d9cbaa3ef -r 8721c71fe3a3 src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 17:55:08 2010 +0200 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 09 09:49:14 2010 +0200 @@ -4,7 +4,7 @@ (c) due to copyright terms *) -theory EqSystem imports Rational Root begin +theory EqSystem imports Integrate Rational Root begin consts @@ -12,8 +12,8 @@ "[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _") (*descriptions in the related problems*) - solveForVars :: real list => toreall - solution :: bool list => toreall + solveForVars :: "real list => toreall" + solution :: "bool list => toreall" (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*) solveSystem :: "[bool list, real list] => bool list" @@ -129,9 +129,9 @@ | size_of_term' (f$t) = size_of_term' f + size_of_term' t | size_of_term' _ = 1; -fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | Term_Ord.term_ord' pr thy (t, u) = +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) + | term_ord' pr thy (t, u) = (if pr then let val (f, ts) = strip_comb t and (g, us) = strip_comb u; @@ -178,8 +178,8 @@ rew_ord' := overwritel (!rew_ord', [("ord_simplify_System", ord_simplify_System false thy) ]); - - +*} +ML {* (** rulesets **) (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*) @@ -202,7 +202,8 @@ (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) ], scr = EmptyScr}:rls; - +*} +ML {* (*.adapted from 'norm_Rational' by #1 using 'ord_simplify_System' in 'order_add_mult_System' #2 NOT using common_nominator_p .*) @@ -224,6 +225,8 @@ scr = Script ((term_of o the o (parse thy)) "empty_script") }:rls; +*} +ML {* (*.adapted from 'norm_Rational' by *1* using 'ord_simplify_System' in 'order_add_mult_System'.*) val norm_System = @@ -244,7 +247,8 @@ scr = Script ((term_of o the o (parse thy)) "empty_script") }:rls; - +*} +ML {* (*.simplify an equational system BEFORE solving it such that parentheses are ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) ) ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION @@ -273,7 +277,8 @@ Calc ("HOL.divide" ,eval_cancel "#divide_e") ], scr = EmptyScr}:rls; - +*} +ML {* (*.simplify an equational system AFTER solving it; This is a copy of 'make_ratpoly_in' with the differences *1* ord_simplify_System instead of termlessI .*) @@ -296,7 +301,8 @@ [Thm ("sym_add_assoc", num_str (@{thm add_assoc} RS @{thm sym}))]; *) - +*} +ML {* val isolate_bdvs = Rls {id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", e_rew_ord), @@ -306,11 +312,13 @@ "#eval_occur_exactly_in_")) ], srls = Erls, calc = [], - rules = [Thm ("commute_0_equality", - num_str @{commute_0_equality), - Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}), - Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})], + rules = + [Thm ("commute_0_equality", num_str @{thm commute_0_equality}), + Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}), + Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})], scr = EmptyScr}; +*} +ML {* val isolate_bdvs_4x4 = Rls {id="isolate_bdvs_4x4", preconds = [], rew_ord = ("e_rew_ord", e_rew_ord), @@ -325,14 +333,16 @@ Thm ("not_false",num_str @{thm not_false}) ], srls = Erls, calc = [], - rules = [Thm ("commute_0_equality", - num_str @{commute_0_equality), + rules = [Thm ("commute_0_equality", num_str @{thm commute_0_equality}), Thm ("separate_bdvs0", num_str @{thm separate_bdvs0}), Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add1}), Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add2}), Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult}) ], scr = EmptyScr}; +*} +ML {* + (*.order the equations in a system such, that a triangular system (if any) appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*) val order_system = @@ -350,7 +360,7 @@ erls = Rls {id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", e_rew_ord), erls = Erls, srls = Erls, calc = [], - rules = [(*for precond nth_Cons_ ...*) + rules = [(*for precond NTH_CONS ...*) Calc ("op <",eval_equ "#less_"), Calc ("op +", eval_binop "#add_") (*immediately repeated rewrite pushes @@ -358,9 +368,9 @@ ], scr = EmptyScr}, srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), Calc ("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str @{thm nth_Nil_}), + Thm ("NTH_NIL",num_str @{thm NTH_NIL}), Thm ("tl_Cons",num_str @{thm tl_Cons}), Thm ("tl_Nil",num_str @{thm tl_Nil}), Calc ("EqSystem.occur'_exactly'_in", @@ -368,6 +378,8 @@ "#eval_occur_exactly_in_") ], scr = EmptyScr}; +*} +ML {* (*WN060914 quickly created for 4x4; more similarity to prls_triangular desirable*) @@ -377,7 +389,7 @@ erls = Rls {id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", e_rew_ord), erls = Erls, srls = Erls, calc = [], - rules = [(*for precond nth_Cons_ ...*) + rules = [(*for precond NTH_CONS ...*) Calc ("op <",eval_equ "#less_"), Calc ("op +", eval_binop "#add_") (*immediately repeated rewrite pushes @@ -385,9 +397,9 @@ ], scr = EmptyScr}, srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), Calc ("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str @{thm thm nth_Nil_}), + Thm ("NTH_NIL",num_str @{thm NTH_NIL}), Thm ("tl_Cons",num_str @{thm tl_Cons}), Thm ("tl_Nil",num_str @{thm tl_Nil}), Calc ("EqSystem.occur'_exactly'_in", @@ -395,6 +407,8 @@ "#eval_occur_exactly_in_") ], scr = EmptyScr}; +*} +ML {* ruleset' := overwritelthy @{theory} @@ -408,6 +422,8 @@ ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions), ("norm_System", prep_rls norm_System) ]); +*} +ML {* (** problems **) @@ -415,123 +431,130 @@ store_pbt (prep_pbt thy "pbl_equsys" [] e_pblID (["system"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Find" ,["solution ss___"](*___ is copy-named*)) + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Find" ,["solution ss'''"](*''' is copy-named*)) ], append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [])); store_pbt (prep_pbt thy "pbl_equsys_lin" [] e_pblID (["linear", "system"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), + [("#Given" ,["equalities e_s", "solveForVars v_s"]), (*TODO.WN050929 check linearity*) - ("#Find" ,["solution ss___"]) + ("#Find" ,["solution ss'''"]) ], append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [])); store_pbt (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID (["2x2", "linear", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Where" ,["length_ (es_:: bool list) = 2", "length_ v_s = 2"]), - ("#Find" ,["solution ss___"]) + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]), + ("#Find" ,["solution ss'''"]) ], append_rls "prls_2x2_linear_system" e_rls - [Thm ("length_Cons_",num_str @{thm length_Cons_}), - Thm ("length_Nil_",num_str @{thm length_Nil_}), + [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), Calc ("op +", eval_binop "#add_"), Calc ("op =",eval_equal "#equal_") ], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [])); +*} +ML {* store_pbt (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID (["triangular", "2x2", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), + [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" , - ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))", - " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]), - ("#Find" ,["solution ss___"]) + ["(tl v_s) from_ v_s occur_exactly_in (NTH 1 (e_s::bool list))", + " v_s from_ v_s occur_exactly_in (NTH 2 (e_s::bool list))"]), + ("#Find" ,["solution ss'''"]) ], prls_triangular, - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])); store_pbt (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID (["normalize", "2x2", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Find" ,["solution ss___"]) + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Find" ,["solution ss'''"]) ], append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [["EqSystem","normalize","2x2"]])); store_pbt (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID (["3x3", "linear", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Where" ,["length_ (es_:: bool list) = 3", "length_ v_s = 3"]), - ("#Find" ,["solution ss___"]) + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]), + ("#Find" ,["solution ss'''"]) ], append_rls "prls_3x3_linear_system" e_rls - [Thm ("length_Cons_",num_str @{thm length_Cons_}), - Thm ("length_Nil_",num_str @{thm length_Nil_}), + [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), Calc ("op +", eval_binop "#add_"), Calc ("op =",eval_equal "#equal_") ], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [])); store_pbt (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID (["4x4", "linear", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Where" ,["length_ (es_:: bool list) = 4", "length_ v_s = 4"]), - ("#Find" ,["solution ss___"]) + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]), + ("#Find" ,["solution ss'''"]) ], append_rls "prls_4x4_linear_system" e_rls - [Thm ("length_Cons_",num_str @{thm length_Cons_}), - Thm ("length_Nil_",num_str @{thm length_Nil_}), + [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), Calc ("op +", eval_binop "#add_"), Calc ("op =",eval_equal "#equal_") ], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [])); +*} +ML {* store_pbt (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID (["triangular", "4x4", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), + [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" , (*accepts missing variables up to diagional form*) - ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))", - "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))", - "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))", - "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))" + ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))", + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))", + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))", + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))" ]), - ("#Find" ,["solution ss___"]) + ("#Find" ,["solution ss'''"]) ], append_rls "prls_tri_4x4_lin_sys" prls_triangular [Calc ("Atools.occurs'_in",eval_occurs_in "")], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","4x4"]])); - +*} +ML {* store_pbt (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID (["normalize", "4x4", "linear", "system"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), - (*length_ is checked 1 level above*) - ("#Find" ,["solution ss___"]) + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + (*LENGTH is checked 1 level above*) + ("#Find" ,["solution ss'''"]) ], append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "solveSystem es_ v_s", + SOME "solveSystem e_s v_s", [["EqSystem","normalize","4x4"]])); (* show_ptyps(); *) +*} +ML {* (** methods **) store_met @@ -550,14 +573,16 @@ srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, "empty_script" )); +*} +ML {* store_met (prep_met thy "met_eqsys_topdown_2x2" [] e_metID (["EqSystem","top_down_substitution","2x2"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), + [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" , - ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))", - " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]), - ("#Find" ,["solution ss___"]) + ["(tl v_s) from_ v_s occur_exactly_in (NTH 1 (e_s::bool list))", + " v_s from_ v_s occur_exactly_in (NTH 2 (e_s::bool list))"]), + ("#Find" ,["solution ss'''"]) ], {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], srls = append_rls "srls_top_down_2x2" e_rls @@ -566,40 +591,42 @@ Thm ("tl_Nil",num_str @{thm tl_Nil}) ], prls = prls_triangular, crls = Erls, nrls = Erls}, -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ -" (let e1__ = Take (hd es_); " ^ -" e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ +" (let e_1 = Take (hd e_s); " ^ +" e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " isolate_bdvs False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ -" simplify_System False))) e1__; " ^ -" e2__ = Take (hd (tl es_)); " ^ -" e2__ = ((Substitute [e1__]) @@ " ^ +" simplify_System False))) e_1; " ^ +" e_2 = Take (hd (tl e_s)); " ^ +" e_2 = ((Substitute [e_1]) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " simplify_System_parenthesized False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " isolate_bdvs False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ -" simplify_System False))) e2__; " ^ -" es__ = Take [e1__, e2__] " ^ -" in (Try (Rewrite_Set order_system False)) es__)" +" simplify_System False))) e_2; " ^ +" e__s = Take [e_1, e_2] " ^ +" in (Try (Rewrite_Set order_system False)) e__s)" (*--------------------------------------------------------------------------- - this script does NOT separate the equations as abolve, + this script does NOT separate the equations as above, but it does not yet work due to preliminary script-interpreter, see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ -" (let es__ = Take es_; " ^ -" e1__ = hd es__; " ^ -" e2__ = hd (tl es__); " ^ -" es__ = [e1__, Substitute [e1__] e2__] " ^ +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ +" (let e__s = Take e_s; " ^ +" e_1 = hd e__s; " ^ +" e_2 = hd (tl e__s); " ^ +" e__s = [e_1, Substitute [e_1] e_2] " ^ " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " simplify_System_parenthesized False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^ " isolate_bdvs False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ -" simplify_System False))) es__)" +" simplify_System False))) e__s)" ---------------------------------------------------------------------------*) )); +*} +ML {* store_met (prep_met thy "met_eqsys_norm" [] e_metID (["EqSystem","normalize"], @@ -611,8 +638,8 @@ store_met (prep_met thy "met_eqsys_norm_2x2" [] e_metID (["EqSystem","normalize","2x2"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Find" ,["solution ss___"])], + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Find" ,["solution ss'''"])], {rew_ord'="tless_true", rls' = Erls, calc = [], srls = append_rls "srls_normalize_2x2" e_rls [Thm ("hd_thm",num_str @{thm hd_thm}), @@ -620,39 +647,39 @@ Thm ("tl_Nil",num_str @{thm tl_Nil}) ], prls = Erls, crls = Erls, nrls = Erls}, -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ -" (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ +" (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " simplify_System_parenthesized False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " isolate_bdvs False)) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ " simplify_System_parenthesized False)) @@ " ^ -" (Try (Rewrite_Set order_system False))) es_ " ^ +" (Try (Rewrite_Set order_system False))) e_s " ^ " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ -" [BOOL_LIST es__, REAL_LIST v_s]))" +" [BOOL_LIST e__s, REAL_LIST v_s]))" )); -(*this is for nth_ only*) +(*this is for NTH only*) val srls = Rls {id="srls_normalize_4x4", preconds = [], rew_ord = ("termlessI",termlessI), erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls - [(*for asm in nth_Cons_ ...*) + [(*for asm in NTH_CONS ...*) Calc ("op <",eval_equ "#less_"), - (*2nd nth_Cons_ pushes n+-1 into asms*) + (*2nd NTH_CONS pushes n+-1 into asms*) Calc("op +", eval_binop "#add_") ], srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), Calc("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str @{thm nth_Nil_})], + Thm ("NTH_NIL",num_str @{thm NTH_NIL})], scr = EmptyScr}; store_met (prep_met thy "met_eqsys_norm_4x4" [] e_metID (["EqSystem","normalize","4x4"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), - ("#Find" ,["solution ss___"])], + [("#Given" ,["equalities e_s", "solveForVars v_s"]), + ("#Find" ,["solution ss'''"])], {rew_ord'="tless_true", rls' = Erls, calc = [], srls = append_rls "srls_normalize_4x4" srls [Thm ("hd_thm",num_str @{thm hd_thm}), @@ -661,34 +688,34 @@ ], prls = Erls, crls = Erls, nrls = Erls}, (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ -" (let es__ = " ^ +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ +" (let e__s = " ^ " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ " (Repeat (Rewrite commute_0_equality False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^ -" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^ +" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ +" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ " simplify_System_parenthesized False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^ -" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^ +" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ +" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ " isolate_bdvs_4x4 False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^ -" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^ +" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ +" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ " simplify_System_parenthesized False)) @@ " ^ -" (Try (Rewrite_Set order_system False))) es_ " ^ +" (Try (Rewrite_Set order_system False))) e_s " ^ " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ -" [BOOL_LIST es__, REAL_LIST v_s]))" +" [BOOL_LIST e__s, REAL_LIST v_s]))" )); store_met (prep_met thy "met_eqsys_topdown_4x4" [] e_metID (["EqSystem","top_down_substitution","4x4"], - [("#Given" ,["equalities es_", "solveForVars v_s"]), + [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" , (*accepts missing variables up to diagonal form*) - ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))", - "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))", - "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))", - "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))" + ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))", + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))", + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))", + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))" ]), - ("#Find" ,["solution ss___"]) + ("#Find" ,["solution ss'''"]) ], {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], srls = append_rls "srls_top_down_4x4" srls [], @@ -696,20 +723,20 @@ [Calc ("Atools.occurs'_in",eval_occurs_in "")], crls = Erls, nrls = Erls}, (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ -" (let e1_ = nth_ 1 es_; " ^ -" e2_ = Take (nth_ 2 es_); " ^ -" e2_ = ((Substitute [e1_]) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^ -" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^ +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ +" (let e_1 = NTH 1 e_s; " ^ +" e_2 = Take (NTH 2 e_s); " ^ +" e_2 = ((Substitute [e_1]) @@ " ^ +" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ +" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ " simplify_System_parenthesized False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^ -" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^ +" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ +" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ " isolate_bdvs False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^ -" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^ -" norm_Rational False))) e2_ " ^ -" in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])" +" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ +" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ +" norm_Rational False))) e_2 " ^ +" in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])" )); *} diff -r eb7d9cbaa3ef -r 8721c71fe3a3 src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Wed Sep 08 17:55:08 2010 +0200 +++ b/src/Tools/isac/ProgLang/ListC.thy Thu Sep 09 09:49:14 2010 +0200 @@ -16,10 +16,10 @@ text {* 'nat' in List.thy replaced by 'real' *} -primrec length_' :: "'a list => real" +primrec LENGTH :: "'a list => real" where - LENGTH_NIL: "length_' [] = 0" (*length: 'a list => nat*) -| LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs" + LENGTH_NIL: "LENGTH [] = 0" (*length: 'a list => nat*) +| LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs" primrec del :: "['a list, 'a] => 'a list" where @@ -31,15 +31,15 @@ ("(_ --/ _)" [66, 66] 65) where "a -- b == foldl del a b" -consts nth_' :: "[real, 'a list] => 'a" +consts NTH :: "[real, 'a list] => 'a" axioms (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*) - NTH_NIL: "nth_' 1 (x#xs) = x" -(* NTH_CONS: "nth_' n (x#xs) = nth_' (n+ -1) xs" *) + NTH_NIL: "NTH 1 (x#xs) = x" +(* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *) (*rewriter does not reach base case ...... ; the condition involves another rule set (erls, eval_binop in Atools):*) - NTH_CONS: "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs" + NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*) (*primrec*)