1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:55:08 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Sep 09 09:49:14 2010 +0200
1.3 @@ -80,8 +80,9 @@
1.4 use_thy "Knowledge/LogExp"
1.5 use_thy "Knowledge/Diff"
1.6 use_thy "Knowledge/DiffApp"
1.7 +use_thy "Knowledge/Integrate"
1.8
1.9 -use_thy "Knowledge/Integrate"
1.10 +use_thy "Knowledge/EqSystem"
1.11
1.12 ML {* 111;
1.13 *}
1.14 @@ -89,7 +90,6 @@
1.15
1.16 text {*------------------------------------------*}
1.17 (*
1.18 -use_thy "Knowledge/EqSystem"
1.19 use_thy "Knowledge/Biegelinie"
1.20 use_thy "Knowledge/AlgEin"
1.21 use_thy "Knowledge/Test"
2.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 17:55:08 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 09 09:49:14 2010 +0200
2.3 @@ -4,7 +4,7 @@
2.4 (c) due to copyright terms
2.5 *)
2.6
2.7 -theory EqSystem imports Rational Root begin
2.8 +theory EqSystem imports Integrate Rational Root begin
2.9
2.10 consts
2.11
2.12 @@ -12,8 +12,8 @@
2.13 "[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _")
2.14
2.15 (*descriptions in the related problems*)
2.16 - solveForVars :: real list => toreall
2.17 - solution :: bool list => toreall
2.18 + solveForVars :: "real list => toreall"
2.19 + solution :: "bool list => toreall"
2.20
2.21 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
2.22 solveSystem :: "[bool list, real list] => bool list"
2.23 @@ -129,9 +129,9 @@
2.24 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
2.25 | size_of_term' _ = 1;
2.26
2.27 -fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.28 - (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
2.29 - | Term_Ord.term_ord' pr thy (t, u) =
2.30 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.31 + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
2.32 + | term_ord' pr thy (t, u) =
2.33 (if pr then
2.34 let
2.35 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
2.36 @@ -178,8 +178,8 @@
2.37 rew_ord' := overwritel (!rew_ord',
2.38 [("ord_simplify_System", ord_simplify_System false thy)
2.39 ]);
2.40 -
2.41 -
2.42 +*}
2.43 +ML {*
2.44 (** rulesets **)
2.45
2.46 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
2.47 @@ -202,7 +202,8 @@
2.48 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
2.49 ],
2.50 scr = EmptyScr}:rls;
2.51 -
2.52 +*}
2.53 +ML {*
2.54 (*.adapted from 'norm_Rational' by
2.55 #1 using 'ord_simplify_System' in 'order_add_mult_System'
2.56 #2 NOT using common_nominator_p .*)
2.57 @@ -224,6 +225,8 @@
2.58 scr = Script ((term_of o the o (parse thy))
2.59 "empty_script")
2.60 }:rls;
2.61 +*}
2.62 +ML {*
2.63 (*.adapted from 'norm_Rational' by
2.64 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
2.65 val norm_System =
2.66 @@ -244,7 +247,8 @@
2.67 scr = Script ((term_of o the o (parse thy))
2.68 "empty_script")
2.69 }:rls;
2.70 -
2.71 +*}
2.72 +ML {*
2.73 (*.simplify an equational system BEFORE solving it such that parentheses are
2.74 ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) )
2.75 ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION
2.76 @@ -273,7 +277,8 @@
2.77 Calc ("HOL.divide" ,eval_cancel "#divide_e")
2.78 ],
2.79 scr = EmptyScr}:rls;
2.80 -
2.81 +*}
2.82 +ML {*
2.83 (*.simplify an equational system AFTER solving it;
2.84 This is a copy of 'make_ratpoly_in' with the differences
2.85 *1* ord_simplify_System instead of termlessI .*)
2.86 @@ -296,7 +301,8 @@
2.87 [Thm ("sym_add_assoc",
2.88 num_str (@{thm add_assoc} RS @{thm sym}))];
2.89 *)
2.90 -
2.91 +*}
2.92 +ML {*
2.93 val isolate_bdvs =
2.94 Rls {id="isolate_bdvs", preconds = [],
2.95 rew_ord = ("e_rew_ord", e_rew_ord),
2.96 @@ -306,11 +312,13 @@
2.97 "#eval_occur_exactly_in_"))
2.98 ],
2.99 srls = Erls, calc = [],
2.100 - rules = [Thm ("commute_0_equality",
2.101 - num_str @{commute_0_equality),
2.102 - Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}),
2.103 - Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})],
2.104 + rules =
2.105 + [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
2.106 + Thm ("separate_bdvs_add", num_str @{thm separate_bdvs_add}),
2.107 + Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})],
2.108 scr = EmptyScr};
2.109 +*}
2.110 +ML {*
2.111 val isolate_bdvs_4x4 =
2.112 Rls {id="isolate_bdvs_4x4", preconds = [],
2.113 rew_ord = ("e_rew_ord", e_rew_ord),
2.114 @@ -325,14 +333,16 @@
2.115 Thm ("not_false",num_str @{thm not_false})
2.116 ],
2.117 srls = Erls, calc = [],
2.118 - rules = [Thm ("commute_0_equality",
2.119 - num_str @{commute_0_equality),
2.120 + rules = [Thm ("commute_0_equality", num_str @{thm commute_0_equality}),
2.121 Thm ("separate_bdvs0", num_str @{thm separate_bdvs0}),
2.122 Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add1}),
2.123 Thm ("separate_bdvs_add1", num_str @{thm separate_bdvs_add2}),
2.124 Thm ("separate_bdvs_mult", num_str @{thm separate_bdvs_mult})
2.125 ], scr = EmptyScr};
2.126
2.127 +*}
2.128 +ML {*
2.129 +
2.130 (*.order the equations in a system such, that a triangular system (if any)
2.131 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
2.132 val order_system =
2.133 @@ -350,7 +360,7 @@
2.134 erls = Rls {id="erls_prls_triangular", preconds = [],
2.135 rew_ord = ("e_rew_ord", e_rew_ord),
2.136 erls = Erls, srls = Erls, calc = [],
2.137 - rules = [(*for precond nth_Cons_ ...*)
2.138 + rules = [(*for precond NTH_CONS ...*)
2.139 Calc ("op <",eval_equ "#less_"),
2.140 Calc ("op +", eval_binop "#add_")
2.141 (*immediately repeated rewrite pushes
2.142 @@ -358,9 +368,9 @@
2.143 ],
2.144 scr = EmptyScr},
2.145 srls = Erls, calc = [],
2.146 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
2.147 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
2.148 Calc ("op +", eval_binop "#add_"),
2.149 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
2.150 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
2.151 Thm ("tl_Cons",num_str @{thm tl_Cons}),
2.152 Thm ("tl_Nil",num_str @{thm tl_Nil}),
2.153 Calc ("EqSystem.occur'_exactly'_in",
2.154 @@ -368,6 +378,8 @@
2.155 "#eval_occur_exactly_in_")
2.156 ],
2.157 scr = EmptyScr};
2.158 +*}
2.159 +ML {*
2.160
2.161 (*WN060914 quickly created for 4x4;
2.162 more similarity to prls_triangular desirable*)
2.163 @@ -377,7 +389,7 @@
2.164 erls = Rls {id="erls_prls_triangular4", preconds = [],
2.165 rew_ord = ("e_rew_ord", e_rew_ord),
2.166 erls = Erls, srls = Erls, calc = [],
2.167 - rules = [(*for precond nth_Cons_ ...*)
2.168 + rules = [(*for precond NTH_CONS ...*)
2.169 Calc ("op <",eval_equ "#less_"),
2.170 Calc ("op +", eval_binop "#add_")
2.171 (*immediately repeated rewrite pushes
2.172 @@ -385,9 +397,9 @@
2.173 ],
2.174 scr = EmptyScr},
2.175 srls = Erls, calc = [],
2.176 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
2.177 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
2.178 Calc ("op +", eval_binop "#add_"),
2.179 - Thm ("nth_Nil_",num_str @{thm thm nth_Nil_}),
2.180 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
2.181 Thm ("tl_Cons",num_str @{thm tl_Cons}),
2.182 Thm ("tl_Nil",num_str @{thm tl_Nil}),
2.183 Calc ("EqSystem.occur'_exactly'_in",
2.184 @@ -395,6 +407,8 @@
2.185 "#eval_occur_exactly_in_")
2.186 ],
2.187 scr = EmptyScr};
2.188 +*}
2.189 +ML {*
2.190
2.191 ruleset' :=
2.192 overwritelthy @{theory}
2.193 @@ -408,6 +422,8 @@
2.194 ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions),
2.195 ("norm_System", prep_rls norm_System)
2.196 ]);
2.197 +*}
2.198 +ML {*
2.199
2.200
2.201 (** problems **)
2.202 @@ -415,123 +431,130 @@
2.203 store_pbt
2.204 (prep_pbt thy "pbl_equsys" [] e_pblID
2.205 (["system"],
2.206 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.207 - ("#Find" ,["solution ss___"](*___ is copy-named*))
2.208 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.209 + ("#Find" ,["solution ss'''"](*''' is copy-named*))
2.210 ],
2.211 append_rls "e_rls" e_rls [(*for preds in where_*)],
2.212 - SOME "solveSystem es_ v_s",
2.213 + SOME "solveSystem e_s v_s",
2.214 []));
2.215 store_pbt
2.216 (prep_pbt thy "pbl_equsys_lin" [] e_pblID
2.217 (["linear", "system"],
2.218 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.219 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.220 (*TODO.WN050929 check linearity*)
2.221 - ("#Find" ,["solution ss___"])
2.222 + ("#Find" ,["solution ss'''"])
2.223 ],
2.224 append_rls "e_rls" e_rls [(*for preds in where_*)],
2.225 - SOME "solveSystem es_ v_s",
2.226 + SOME "solveSystem e_s v_s",
2.227 []));
2.228 store_pbt
2.229 (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
2.230 (["2x2", "linear", "system"],
2.231 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.232 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.233 - ("#Where" ,["length_ (es_:: bool list) = 2", "length_ v_s = 2"]),
2.234 - ("#Find" ,["solution ss___"])
2.235 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.236 + ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
2.237 + ("#Find" ,["solution ss'''"])
2.238 ],
2.239 append_rls "prls_2x2_linear_system" e_rls
2.240 - [Thm ("length_Cons_",num_str @{thm length_Cons_}),
2.241 - Thm ("length_Nil_",num_str @{thm length_Nil_}),
2.242 + [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
2.243 + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
2.244 Calc ("op +", eval_binop "#add_"),
2.245 Calc ("op =",eval_equal "#equal_")
2.246 ],
2.247 - SOME "solveSystem es_ v_s",
2.248 + SOME "solveSystem e_s v_s",
2.249 []));
2.250 +*}
2.251 +ML {*
2.252 store_pbt
2.253 (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
2.254 (["triangular", "2x2", "linear", "system"],
2.255 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.256 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.257 ("#Where" ,
2.258 - ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
2.259 - " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
2.260 - ("#Find" ,["solution ss___"])
2.261 + ["(tl v_s) from_ v_s occur_exactly_in (NTH 1 (e_s::bool list))",
2.262 + " v_s from_ v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
2.263 + ("#Find" ,["solution ss'''"])
2.264 ],
2.265 prls_triangular,
2.266 - SOME "solveSystem es_ v_s",
2.267 + SOME "solveSystem e_s v_s",
2.268 [["EqSystem","top_down_substitution","2x2"]]));
2.269 store_pbt
2.270 (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
2.271 (["normalize", "2x2", "linear", "system"],
2.272 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.273 - ("#Find" ,["solution ss___"])
2.274 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.275 + ("#Find" ,["solution ss'''"])
2.276 ],
2.277 append_rls "e_rls" e_rls [(*for preds in where_*)],
2.278 - SOME "solveSystem es_ v_s",
2.279 + SOME "solveSystem e_s v_s",
2.280 [["EqSystem","normalize","2x2"]]));
2.281 store_pbt
2.282 (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
2.283 (["3x3", "linear", "system"],
2.284 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.285 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.286 - ("#Where" ,["length_ (es_:: bool list) = 3", "length_ v_s = 3"]),
2.287 - ("#Find" ,["solution ss___"])
2.288 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.289 + ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
2.290 + ("#Find" ,["solution ss'''"])
2.291 ],
2.292 append_rls "prls_3x3_linear_system" e_rls
2.293 - [Thm ("length_Cons_",num_str @{thm length_Cons_}),
2.294 - Thm ("length_Nil_",num_str @{thm length_Nil_}),
2.295 + [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
2.296 + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
2.297 Calc ("op +", eval_binop "#add_"),
2.298 Calc ("op =",eval_equal "#equal_")
2.299 ],
2.300 - SOME "solveSystem es_ v_s",
2.301 + SOME "solveSystem e_s v_s",
2.302 []));
2.303 store_pbt
2.304 (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
2.305 (["4x4", "linear", "system"],
2.306 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.307 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.308 - ("#Where" ,["length_ (es_:: bool list) = 4", "length_ v_s = 4"]),
2.309 - ("#Find" ,["solution ss___"])
2.310 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.311 + ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
2.312 + ("#Find" ,["solution ss'''"])
2.313 ],
2.314 append_rls "prls_4x4_linear_system" e_rls
2.315 - [Thm ("length_Cons_",num_str @{thm length_Cons_}),
2.316 - Thm ("length_Nil_",num_str @{thm length_Nil_}),
2.317 + [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
2.318 + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
2.319 Calc ("op +", eval_binop "#add_"),
2.320 Calc ("op =",eval_equal "#equal_")
2.321 ],
2.322 - SOME "solveSystem es_ v_s",
2.323 + SOME "solveSystem e_s v_s",
2.324 []));
2.325 +*}
2.326 +ML {*
2.327 store_pbt
2.328 (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
2.329 (["triangular", "4x4", "linear", "system"],
2.330 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.331 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.332 ("#Where" , (*accepts missing variables up to diagional form*)
2.333 - ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
2.334 - "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
2.335 - "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
2.336 - "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
2.337 + ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
2.338 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
2.339 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
2.340 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
2.341 ]),
2.342 - ("#Find" ,["solution ss___"])
2.343 + ("#Find" ,["solution ss'''"])
2.344 ],
2.345 append_rls "prls_tri_4x4_lin_sys" prls_triangular
2.346 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
2.347 - SOME "solveSystem es_ v_s",
2.348 + SOME "solveSystem e_s v_s",
2.349 [["EqSystem","top_down_substitution","4x4"]]));
2.350 -
2.351 +*}
2.352 +ML {*
2.353 store_pbt
2.354 (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
2.355 (["normalize", "4x4", "linear", "system"],
2.356 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.357 - (*length_ is checked 1 level above*)
2.358 - ("#Find" ,["solution ss___"])
2.359 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.360 + (*LENGTH is checked 1 level above*)
2.361 + ("#Find" ,["solution ss'''"])
2.362 ],
2.363 append_rls "e_rls" e_rls [(*for preds in where_*)],
2.364 - SOME "solveSystem es_ v_s",
2.365 + SOME "solveSystem e_s v_s",
2.366 [["EqSystem","normalize","4x4"]]));
2.367
2.368
2.369 (* show_ptyps();
2.370 *)
2.371
2.372 +*}
2.373 +ML {*
2.374 (** methods **)
2.375
2.376 store_met
2.377 @@ -550,14 +573,16 @@
2.378 srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
2.379 "empty_script"
2.380 ));
2.381 +*}
2.382 +ML {*
2.383 store_met
2.384 (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
2.385 (["EqSystem","top_down_substitution","2x2"],
2.386 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.387 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.388 ("#Where" ,
2.389 - ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
2.390 - " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
2.391 - ("#Find" ,["solution ss___"])
2.392 + ["(tl v_s) from_ v_s occur_exactly_in (NTH 1 (e_s::bool list))",
2.393 + " v_s from_ v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
2.394 + ("#Find" ,["solution ss'''"])
2.395 ],
2.396 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
2.397 srls = append_rls "srls_top_down_2x2" e_rls
2.398 @@ -566,40 +591,42 @@
2.399 Thm ("tl_Nil",num_str @{thm tl_Nil})
2.400 ],
2.401 prls = prls_triangular, crls = Erls, nrls = Erls},
2.402 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
2.403 -" (let e1__ = Take (hd es_); " ^
2.404 -" e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.405 +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
2.406 +" (let e_1 = Take (hd e_s); " ^
2.407 +" e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.408 " isolate_bdvs False)) @@ " ^
2.409 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.410 -" simplify_System False))) e1__; " ^
2.411 -" e2__ = Take (hd (tl es_)); " ^
2.412 -" e2__ = ((Substitute [e1__]) @@ " ^
2.413 +" simplify_System False))) e_1; " ^
2.414 +" e_2 = Take (hd (tl e_s)); " ^
2.415 +" e_2 = ((Substitute [e_1]) @@ " ^
2.416 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.417 " simplify_System_parenthesized False)) @@ " ^
2.418 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.419 " isolate_bdvs False)) @@ " ^
2.420 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.421 -" simplify_System False))) e2__; " ^
2.422 -" es__ = Take [e1__, e2__] " ^
2.423 -" in (Try (Rewrite_Set order_system False)) es__)"
2.424 +" simplify_System False))) e_2; " ^
2.425 +" e__s = Take [e_1, e_2] " ^
2.426 +" in (Try (Rewrite_Set order_system False)) e__s)"
2.427 (*---------------------------------------------------------------------------
2.428 - this script does NOT separate the equations as abolve,
2.429 + this script does NOT separate the equations as above,
2.430 but it does not yet work due to preliminary script-interpreter,
2.431 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
2.432
2.433 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
2.434 -" (let es__ = Take es_; " ^
2.435 -" e1__ = hd es__; " ^
2.436 -" e2__ = hd (tl es__); " ^
2.437 -" es__ = [e1__, Substitute [e1__] e2__] " ^
2.438 +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
2.439 +" (let e__s = Take e_s; " ^
2.440 +" e_1 = hd e__s; " ^
2.441 +" e_2 = hd (tl e__s); " ^
2.442 +" e__s = [e_1, Substitute [e_1] e_2] " ^
2.443 " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.444 " simplify_System_parenthesized False)) @@ " ^
2.445 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
2.446 " isolate_bdvs False)) @@ " ^
2.447 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.448 -" simplify_System False))) es__)"
2.449 +" simplify_System False))) e__s)"
2.450 ---------------------------------------------------------------------------*)
2.451 ));
2.452 +*}
2.453 +ML {*
2.454 store_met
2.455 (prep_met thy "met_eqsys_norm" [] e_metID
2.456 (["EqSystem","normalize"],
2.457 @@ -611,8 +638,8 @@
2.458 store_met
2.459 (prep_met thy "met_eqsys_norm_2x2" [] e_metID
2.460 (["EqSystem","normalize","2x2"],
2.461 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.462 - ("#Find" ,["solution ss___"])],
2.463 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.464 + ("#Find" ,["solution ss'''"])],
2.465 {rew_ord'="tless_true", rls' = Erls, calc = [],
2.466 srls = append_rls "srls_normalize_2x2" e_rls
2.467 [Thm ("hd_thm",num_str @{thm hd_thm}),
2.468 @@ -620,39 +647,39 @@
2.469 Thm ("tl_Nil",num_str @{thm tl_Nil})
2.470 ],
2.471 prls = Erls, crls = Erls, nrls = Erls},
2.472 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
2.473 -" (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
2.474 +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
2.475 +" (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
2.476 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.477 " simplify_System_parenthesized False)) @@ " ^
2.478 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.479 " isolate_bdvs False)) @@ " ^
2.480 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
2.481 " simplify_System_parenthesized False)) @@ " ^
2.482 -" (Try (Rewrite_Set order_system False))) es_ " ^
2.483 +" (Try (Rewrite_Set order_system False))) e_s " ^
2.484 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^
2.485 -" [BOOL_LIST es__, REAL_LIST v_s]))"
2.486 +" [BOOL_LIST e__s, REAL_LIST v_s]))"
2.487 ));
2.488
2.489 -(*this is for nth_ only*)
2.490 +(*this is for NTH only*)
2.491 val srls = Rls {id="srls_normalize_4x4",
2.492 preconds = [],
2.493 rew_ord = ("termlessI",termlessI),
2.494 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
2.495 - [(*for asm in nth_Cons_ ...*)
2.496 + [(*for asm in NTH_CONS ...*)
2.497 Calc ("op <",eval_equ "#less_"),
2.498 - (*2nd nth_Cons_ pushes n+-1 into asms*)
2.499 + (*2nd NTH_CONS pushes n+-1 into asms*)
2.500 Calc("op +", eval_binop "#add_")
2.501 ],
2.502 srls = Erls, calc = [],
2.503 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
2.504 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
2.505 Calc("op +", eval_binop "#add_"),
2.506 - Thm ("nth_Nil_",num_str @{thm nth_Nil_})],
2.507 + Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
2.508 scr = EmptyScr};
2.509 store_met
2.510 (prep_met thy "met_eqsys_norm_4x4" [] e_metID
2.511 (["EqSystem","normalize","4x4"],
2.512 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.513 - ("#Find" ,["solution ss___"])],
2.514 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.515 + ("#Find" ,["solution ss'''"])],
2.516 {rew_ord'="tless_true", rls' = Erls, calc = [],
2.517 srls = append_rls "srls_normalize_4x4" srls
2.518 [Thm ("hd_thm",num_str @{thm hd_thm}),
2.519 @@ -661,34 +688,34 @@
2.520 ],
2.521 prls = Erls, crls = Erls, nrls = Erls},
2.522 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
2.523 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
2.524 -" (let es__ = " ^
2.525 +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
2.526 +" (let e__s = " ^
2.527 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
2.528 " (Repeat (Rewrite commute_0_equality False)) @@ " ^
2.529 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
2.530 -" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
2.531 +" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
2.532 +" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
2.533 " simplify_System_parenthesized False)) @@ " ^
2.534 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
2.535 -" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
2.536 +" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
2.537 +" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
2.538 " isolate_bdvs_4x4 False)) @@ " ^
2.539 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
2.540 -" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
2.541 +" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
2.542 +" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
2.543 " simplify_System_parenthesized False)) @@ " ^
2.544 -" (Try (Rewrite_Set order_system False))) es_ " ^
2.545 +" (Try (Rewrite_Set order_system False))) e_s " ^
2.546 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^
2.547 -" [BOOL_LIST es__, REAL_LIST v_s]))"
2.548 +" [BOOL_LIST e__s, REAL_LIST v_s]))"
2.549 ));
2.550 store_met
2.551 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID
2.552 (["EqSystem","top_down_substitution","4x4"],
2.553 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
2.554 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
2.555 ("#Where" , (*accepts missing variables up to diagonal form*)
2.556 - ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
2.557 - "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
2.558 - "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
2.559 - "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
2.560 + ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
2.561 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
2.562 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
2.563 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
2.564 ]),
2.565 - ("#Find" ,["solution ss___"])
2.566 + ("#Find" ,["solution ss'''"])
2.567 ],
2.568 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
2.569 srls = append_rls "srls_top_down_4x4" srls [],
2.570 @@ -696,20 +723,20 @@
2.571 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
2.572 crls = Erls, nrls = Erls},
2.573 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
2.574 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
2.575 -" (let e1_ = nth_ 1 es_; " ^
2.576 -" e2_ = Take (nth_ 2 es_); " ^
2.577 -" e2_ = ((Substitute [e1_]) @@ " ^
2.578 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
2.579 -" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
2.580 +"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
2.581 +" (let e_1 = NTH 1 e_s; " ^
2.582 +" e_2 = Take (NTH 2 e_s); " ^
2.583 +" e_2 = ((Substitute [e_1]) @@ " ^
2.584 +" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
2.585 +" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
2.586 " simplify_System_parenthesized False)) @@ " ^
2.587 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
2.588 -" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
2.589 +" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
2.590 +" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
2.591 " isolate_bdvs False)) @@ " ^
2.592 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
2.593 -" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
2.594 -" norm_Rational False))) e2_ " ^
2.595 -" in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
2.596 +" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
2.597 +" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
2.598 +" norm_Rational False))) e_2 " ^
2.599 +" in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
2.600 ));
2.601 *}
2.602
3.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Sep 08 17:55:08 2010 +0200
3.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Thu Sep 09 09:49:14 2010 +0200
3.3 @@ -16,10 +16,10 @@
3.4
3.5 text {* 'nat' in List.thy replaced by 'real' *}
3.6
3.7 -primrec length_' :: "'a list => real"
3.8 +primrec LENGTH :: "'a list => real"
3.9 where
3.10 - LENGTH_NIL: "length_' [] = 0" (*length: 'a list => nat*)
3.11 -| LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs"
3.12 + LENGTH_NIL: "LENGTH [] = 0" (*length: 'a list => nat*)
3.13 +| LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
3.14
3.15 primrec del :: "['a list, 'a] => 'a list"
3.16 where
3.17 @@ -31,15 +31,15 @@
3.18 ("(_ --/ _)" [66, 66] 65)
3.19 where "a -- b == foldl del a b"
3.20
3.21 -consts nth_' :: "[real, 'a list] => 'a"
3.22 +consts NTH :: "[real, 'a list] => 'a"
3.23 axioms
3.24 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
3.25 - NTH_NIL: "nth_' 1 (x#xs) = x"
3.26 -(* NTH_CONS: "nth_' n (x#xs) = nth_' (n+ -1) xs" *)
3.27 + NTH_NIL: "NTH 1 (x#xs) = x"
3.28 +(* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *)
3.29
3.30 (*rewriter does not reach base case ...... ;
3.31 the condition involves another rule set (erls, eval_binop in Atools):*)
3.32 - NTH_CONS: "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs"
3.33 + NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs"
3.34
3.35 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
3.36 (*primrec*)