1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/IsacKnowledge/EqSystem.ML Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,673 @@
1.4 +(* tools for systems of equations over the reals
1.5 + author: Walther Neuper 050905, 08:51
1.6 + (c) due to copyright terms
1.7 +
1.8 +use"IsacKnowledge/EqSystem.ML";
1.9 +use"EqSystem.ML";
1.10 +
1.11 +remove_thy"EqSystem";
1.12 +use_thy"IsacKnowledge/Isac";
1.13 +*)
1.14 +
1.15 +(** interface isabelle -- isac **)
1.16 +
1.17 +theory' := overwritel (!theory', [("EqSystem.thy",EqSystem.thy)]);
1.18 +
1.19 +(** eval functions **)
1.20 +
1.21 +(*certain variables of a given list occur _all_ in a term
1.22 + args: all: ..variables, which are under consideration (eg. the bound vars)
1.23 + vs: variables which must be in t,
1.24 + and none of the others in all must be in t
1.25 + t: the term under consideration
1.26 + *)
1.27 +fun occur_exactly_in vs all t =
1.28 + let fun occurs_in' a b = occurs_in b a
1.29 + in foldl and_ (true, map (occurs_in' t) vs)
1.30 + andalso not (foldl or_ (false, map (occurs_in' t) (all \\ vs)))
1.31 + end;
1.32 +
1.33 +(*("occur_exactly_in", ("EqSystem.occur'_exactly'_in",
1.34 + eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
1.35 +fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in"
1.36 + (p as (Const ("EqSystem.occur'_exactly'_in",_)
1.37 + $ vs $ all $ t)) _ =
1.38 + if occur_exactly_in (isalist2list vs) (isalist2list all) t
1.39 + then Some ((term2str p) ^ " = True",
1.40 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.41 + else Some ((term2str p) ^ " = False",
1.42 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.43 + | eval_occur_exactly_in _ _ _ _ = None;
1.44 +
1.45 +calclist':=
1.46 +overwritel (!calclist',
1.47 + [("occur_exactly_in",
1.48 + ("EqSystem.occur'_exactly'_in",
1.49 + eval_occur_exactly_in "#eval_occur_exactly_in_"))
1.50 + ]);
1.51 +
1.52 +
1.53 +(** rewrite order 'ord_simplify_System' **)
1.54 +
1.55 +(* order wrt. several linear (i.e. without exponents) variables "c","c_2",..
1.56 + which leaves the monomials containing c, c_2,... at the end of an Integral
1.57 + and puts the c, c_2,... rightmost within a monomial.
1.58 +
1.59 + WN050906 this is a quick and dirty adaption of ord_make_polynomial_in,
1.60 + which was most adequate, because it uses size_of_term*)
1.61 +(**)
1.62 +local (*. for simplify_System .*)
1.63 +(**)
1.64 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.65 +
1.66 +fun pr_ord EQUAL = "EQUAL"
1.67 + | pr_ord LESS = "LESS"
1.68 + | pr_ord GREATER = "GREATER";
1.69 +
1.70 +fun dest_hd' (Const (a, T)) = (((a, 0), T), 0)
1.71 + | dest_hd' (Free (ccc, T)) =
1.72 + (case explode ccc of
1.73 + "c"::[] => ((("|||||||||||||||||||||", 0), T), 1)(*greatest string WN*)
1.74 + | "c"::"_"::_ => ((("|||||||||||||||||||||", 0), T), 1)
1.75 + | _ => (((ccc, 0), T), 1))
1.76 + | dest_hd' (Var v) = (v, 2)
1.77 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1.78 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1.79 +
1.80 +fun size_of_term' (Free (ccc, _)) =
1.81 + (case explode ccc of (*WN0510 hack for the bound variables*)
1.82 + "c"::[] => 1000
1.83 + | "c"::"_"::is => 1000 * ((str2int o implode) is)
1.84 + | _ => 1)
1.85 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.86 + | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.87 + | size_of_term' _ = 1;
1.88 +
1.89 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.90 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.91 + | term_ord' pr thy (t, u) =
1.92 + (if pr then
1.93 + let
1.94 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.95 + val _=writeln("t= f@ts= \""^
1.96 + ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
1.97 + (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
1.98 + val _=writeln("u= g@us= \""^
1.99 + ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
1.100 + (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
1.101 + val _=writeln("size_of_term(t,u)= ("^
1.102 + (string_of_int(size_of_term' t))^", "^
1.103 + (string_of_int(size_of_term' u))^")");
1.104 + val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
1.105 + val _=writeln("terms_ord(ts,us) = "^
1.106 + ((pr_ord o terms_ord str false)(ts,us)));
1.107 + val _=writeln("-------");
1.108 + in () end
1.109 + else ();
1.110 + case int_ord (size_of_term' t, size_of_term' u) of
1.111 + EQUAL =>
1.112 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.113 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.114 + | ord => ord)
1.115 + end
1.116 + | ord => ord)
1.117 +and hd_ord (f, g) = (* ~ term.ML *)
1.118 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f,
1.119 + dest_hd' g)
1.120 +and terms_ord str pr (ts, us) =
1.121 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.122 +(**)
1.123 +in
1.124 +(**)
1.125 +(*WN0510 for preliminary use in eval_order_system, see case-study mat-eng.tex
1.126 +fun ord_simplify_System_rev (pr:bool) thy subst tu =
1.127 + (term_ord' pr thy (Library.swap tu) = LESS);*)
1.128 +
1.129 +(*for the rls's*)
1.130 +fun ord_simplify_System (pr:bool) thy subst tu =
1.131 + (term_ord' pr thy tu = LESS);
1.132 +(**)
1.133 +end;
1.134 +(**)
1.135 +rew_ord' := overwritel (!rew_ord',
1.136 +[("ord_simplify_System", ord_simplify_System false thy)
1.137 + ]);
1.138 +
1.139 +
1.140 +(** rulesets **)
1.141 +
1.142 +(*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
1.143 +val order_add_mult_System =
1.144 + Rls{id = "order_add_mult_System", preconds = [],
1.145 + rew_ord = ("ord_simplify_System",
1.146 + ord_simplify_System false Integrate.thy),
1.147 + erls = e_rls,srls = Erls, calc = [],
1.148 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.149 + (* z * w = w * z *)
1.150 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.151 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.152 + Thm ("real_mult_assoc",num_str real_mult_assoc),
1.153 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.154 + Thm ("real_add_commute",num_str real_add_commute),
1.155 + (*z + w = w + z*)
1.156 + Thm ("real_add_left_commute",num_str real_add_left_commute),
1.157 + (*x + (y + z) = y + (x + z)*)
1.158 + Thm ("real_add_assoc",num_str real_add_assoc)
1.159 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.160 + ],
1.161 + scr = EmptyScr}:rls;
1.162 +
1.163 +(*.adapted from 'norm_Rational' by
1.164 + #1 using 'ord_simplify_System' in 'order_add_mult_System'
1.165 + #2 NOT using common_nominator_p .*)
1.166 +val norm_System_noadd_fractions =
1.167 + Rls {id = "norm_System_noadd_fractions", preconds = [],
1.168 + rew_ord = ("dummy_ord",dummy_ord),
1.169 + erls = norm_rat_erls, srls = Erls, calc = [],
1.170 + rules = [(*sequence given by operator precedence*)
1.171 + Rls_ discard_minus,
1.172 + Rls_ powers,
1.173 + Rls_ rat_mult_divide,
1.174 + Rls_ expand,
1.175 + Rls_ reduce_0_1_2,
1.176 + Rls_ (*order_add_mult #1*) order_add_mult_System,
1.177 + Rls_ collect_numerals,
1.178 + (*Rls_ add_fractions_p, #2*)
1.179 + Rls_ cancel_p
1.180 + ],
1.181 + scr = Script ((term_of o the o (parse thy))
1.182 + "empty_script")
1.183 + }:rls;
1.184 +(*.adapted from 'norm_Rational' by
1.185 + *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
1.186 +val norm_System =
1.187 + Rls {id = "norm_System", preconds = [],
1.188 + rew_ord = ("dummy_ord",dummy_ord),
1.189 + erls = norm_rat_erls, srls = Erls, calc = [],
1.190 + rules = [(*sequence given by operator precedence*)
1.191 + Rls_ discard_minus,
1.192 + Rls_ powers,
1.193 + Rls_ rat_mult_divide,
1.194 + Rls_ expand,
1.195 + Rls_ reduce_0_1_2,
1.196 + Rls_ (*order_add_mult *1*) order_add_mult_System,
1.197 + Rls_ collect_numerals,
1.198 + Rls_ add_fractions_p,
1.199 + Rls_ cancel_p
1.200 + ],
1.201 + scr = Script ((term_of o the o (parse thy))
1.202 + "empty_script")
1.203 + }:rls;
1.204 +
1.205 +(*.simplify an equational system BEFORE solving it such that parentheses are
1.206 + ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) )
1.207 +ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION
1.208 + This is a copy from 'make_ratpoly_in' with respective reductions:
1.209 + *0* expand the term, ie. distribute * and / over +
1.210 + *1* ord_simplify_System instead of termlessI
1.211 + *2* no add_fractions_p (= common_nominator_p_rls !)
1.212 + *3* discard_parentheses only for (.*(.*.))
1.213 + analoguous to simplify_Integral .*)
1.214 +val simplify_System_parenthesized =
1.215 + Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.216 + rew_ord = ("dummy_ord", dummy_ord),
1.217 + erls = Atools_erls, srls = Erls, calc = [],
1.218 + rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib),
1.219 + (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.220 + Thm ("real_add_divide_distrib",num_str real_add_divide_distrib),
1.221 + (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.222 + (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.223 + Rls_ norm_Rational_noadd_fractions(**2**),
1.224 + Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.225 + Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym))
1.226 + (*Rls_ discard_parentheses *3**),
1.227 + Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.228 + Rls_ separate_bdv2,
1.229 + Calc ("HOL.divide" ,eval_cancel "#divide_")
1.230 + ],
1.231 + scr = EmptyScr}:rls;
1.232 +
1.233 +(*.simplify an equational system AFTER solving it;
1.234 + This is a copy of 'make_ratpoly_in' with the differences
1.235 + *1* ord_simplify_System instead of termlessI .*)
1.236 +(*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
1.237 +val simplify_System =
1.238 + Seq {id = "simplify_System", preconds = []:term list,
1.239 + rew_ord = ("dummy_ord", dummy_ord),
1.240 + erls = Atools_erls, srls = Erls, calc = [],
1.241 + rules = [Rls_ norm_Rational,
1.242 + Rls_ (*order_add_mult_in*) norm_System (**1**),
1.243 + Rls_ discard_parentheses,
1.244 + Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.245 + Rls_ separate_bdv2,
1.246 + Calc ("HOL.divide" ,eval_cancel "#divide_")
1.247 + ],
1.248 + scr = EmptyScr}:rls;
1.249 +(*
1.250 +val simplify_System =
1.251 + append_rls "simplify_System" simplify_System_parenthesized
1.252 + [Thm ("sym_real_add_assoc", num_str (real_add_assoc RS sym))];
1.253 +*)
1.254 +
1.255 +val isolate_bdvs =
1.256 + Rls {id="isolate_bdvs", preconds = [],
1.257 + rew_ord = ("e_rew_ord", e_rew_ord),
1.258 + erls = append_rls "erls_isolate_bdvs" e_rls
1.259 + [(Calc ("EqSystem.occur'_exactly'_in",
1.260 + eval_occur_exactly_in
1.261 + "#eval_occur_exactly_in_"))
1.262 + ],
1.263 + srls = Erls, calc = [],
1.264 + rules = [Thm ("commute_0_equality",
1.265 + num_str commute_0_equality),
1.266 + Thm ("separate_bdvs_add", num_str separate_bdvs_add),
1.267 + Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)],
1.268 + scr = EmptyScr};
1.269 +val isolate_bdvs_4x4 =
1.270 + Rls {id="isolate_bdvs_4x4", preconds = [],
1.271 + rew_ord = ("e_rew_ord", e_rew_ord),
1.272 + erls = append_rls
1.273 + "erls_isolate_bdvs_4x4" e_rls
1.274 + [Calc ("EqSystem.occur'_exactly'_in",
1.275 + eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.276 + Calc ("Atools.ident",eval_ident "#ident_"),
1.277 + Calc ("Atools.some'_occur'_in",
1.278 + eval_some_occur_in "#some_occur_in_"),
1.279 + Thm ("not_true",num_str not_true),
1.280 + Thm ("not_false",num_str not_false)
1.281 + ],
1.282 + srls = Erls, calc = [],
1.283 + rules = [Thm ("commute_0_equality",
1.284 + num_str commute_0_equality),
1.285 + Thm ("separate_bdvs0", num_str separate_bdvs0),
1.286 + Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
1.287 + Thm ("separate_bdvs_add1", num_str separate_bdvs_add2),
1.288 + Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)],
1.289 + scr = EmptyScr};
1.290 +
1.291 +(*.order the equations in a system such, that a triangular system (if any)
1.292 + appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.293 +val order_system =
1.294 + Rls {id="order_system", preconds = [],
1.295 + rew_ord = ("ord_simplify_System",
1.296 + ord_simplify_System false thy),
1.297 + erls = Erls, srls = Erls, calc = [],
1.298 + rules = [Thm ("order_system_NxN", num_str order_system_NxN)
1.299 + ],
1.300 + scr = EmptyScr};
1.301 +
1.302 +val prls_triangular =
1.303 + Rls {id="prls_triangular", preconds = [],
1.304 + rew_ord = ("e_rew_ord", e_rew_ord),
1.305 + erls = Rls {id="erls_prls_triangular", preconds = [],
1.306 + rew_ord = ("e_rew_ord", e_rew_ord),
1.307 + erls = Erls, srls = Erls, calc = [],
1.308 + rules = [(*for precond nth_Cons_ ...*)
1.309 + Calc ("op <",eval_equ "#less_"),
1.310 + Calc ("op +", eval_binop "#add_")
1.311 + (*immediately repeated rewrite pushes
1.312 + '+' into precondition !*)
1.313 + ],
1.314 + scr = EmptyScr},
1.315 + srls = Erls, calc = [],
1.316 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.317 + Calc ("op +", eval_binop "#add_"),
1.318 + Thm ("nth_Nil_",num_str nth_Nil_),
1.319 + Thm ("tl_Cons",num_str tl_Cons),
1.320 + Thm ("tl_Nil",num_str tl_Nil),
1.321 + Calc ("EqSystem.occur'_exactly'_in",
1.322 + eval_occur_exactly_in
1.323 + "#eval_occur_exactly_in_")
1.324 + ],
1.325 + scr = EmptyScr};
1.326 +
1.327 +(*WN060914 quickly created for 4x4;
1.328 + more similarity to prls_triangular desirable*)
1.329 +val prls_triangular4 =
1.330 + Rls {id="prls_triangular4", preconds = [],
1.331 + rew_ord = ("e_rew_ord", e_rew_ord),
1.332 + erls = Rls {id="erls_prls_triangular4", preconds = [],
1.333 + rew_ord = ("e_rew_ord", e_rew_ord),
1.334 + erls = Erls, srls = Erls, calc = [],
1.335 + rules = [(*for precond nth_Cons_ ...*)
1.336 + Calc ("op <",eval_equ "#less_"),
1.337 + Calc ("op +", eval_binop "#add_")
1.338 + (*immediately repeated rewrite pushes
1.339 + '+' into precondition !*)
1.340 + ],
1.341 + scr = EmptyScr},
1.342 + srls = Erls, calc = [],
1.343 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.344 + Calc ("op +", eval_binop "#add_"),
1.345 + Thm ("nth_Nil_",num_str nth_Nil_),
1.346 + Thm ("tl_Cons",num_str tl_Cons),
1.347 + Thm ("tl_Nil",num_str tl_Nil),
1.348 + Calc ("EqSystem.occur'_exactly'_in",
1.349 + eval_occur_exactly_in
1.350 + "#eval_occur_exactly_in_")
1.351 + ],
1.352 + scr = EmptyScr};
1.353 +
1.354 +ruleset' :=
1.355 +overwritelthy thy
1.356 + (!ruleset',
1.357 +[("simplify_System_parenthesized", prep_rls simplify_System_parenthesized),
1.358 + ("simplify_System", prep_rls simplify_System),
1.359 + ("isolate_bdvs", prep_rls isolate_bdvs),
1.360 + ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4),
1.361 + ("order_system", prep_rls order_system),
1.362 + ("order_add_mult_System", prep_rls order_add_mult_System),
1.363 + ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions),
1.364 + ("norm_System", prep_rls norm_System)
1.365 + ]);
1.366 +
1.367 +
1.368 +(** problems **)
1.369 +
1.370 +store_pbt
1.371 + (prep_pbt EqSystem.thy "pbl_equsys" [] e_pblID
1.372 + (["system"],
1.373 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.374 + ("#Find" ,["solution ss___"](*___ is copy-named*))
1.375 + ],
1.376 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.377 + Some "solveSystem es_ vs_",
1.378 + []));
1.379 +store_pbt
1.380 + (prep_pbt EqSystem.thy "pbl_equsys_lin" [] e_pblID
1.381 + (["linear", "system"],
1.382 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.383 + (*TODO.WN050929 check linearity*)
1.384 + ("#Find" ,["solution ss___"])
1.385 + ],
1.386 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.387 + Some "solveSystem es_ vs_",
1.388 + []));
1.389 +store_pbt
1.390 + (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2" [] e_pblID
1.391 + (["2x2", "linear", "system"],
1.392 + (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.393 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.394 + ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]),
1.395 + ("#Find" ,["solution ss___"])
1.396 + ],
1.397 + append_rls "prls_2x2_linear_system" e_rls
1.398 + [Thm ("length_Cons_",num_str length_Cons_),
1.399 + Thm ("length_Nil_",num_str length_Nil_),
1.400 + Calc ("op +", eval_binop "#add_"),
1.401 + Calc ("op =",eval_equal "#equal_")
1.402 + ],
1.403 + Some "solveSystem es_ vs_",
1.404 + []));
1.405 +store_pbt
1.406 + (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2_tri" [] e_pblID
1.407 + (["triangular", "2x2", "linear", "system"],
1.408 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.409 + ("#Where" ,
1.410 + ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
1.411 + " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.412 + ("#Find" ,["solution ss___"])
1.413 + ],
1.414 + prls_triangular,
1.415 + Some "solveSystem es_ vs_",
1.416 + [["EqSystem","top_down_substitution","2x2"]]));
1.417 +store_pbt
1.418 + (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2_norm" [] e_pblID
1.419 + (["normalize", "2x2", "linear", "system"],
1.420 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.421 + ("#Find" ,["solution ss___"])
1.422 + ],
1.423 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.424 + Some "solveSystem es_ vs_",
1.425 + [["EqSystem","normalize","2x2"]]));
1.426 +store_pbt
1.427 + (prep_pbt EqSystem.thy "pbl_equsys_lin_3x3" [] e_pblID
1.428 + (["3x3", "linear", "system"],
1.429 + (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.430 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.431 + ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]),
1.432 + ("#Find" ,["solution ss___"])
1.433 + ],
1.434 + append_rls "prls_3x3_linear_system" e_rls
1.435 + [Thm ("length_Cons_",num_str length_Cons_),
1.436 + Thm ("length_Nil_",num_str length_Nil_),
1.437 + Calc ("op +", eval_binop "#add_"),
1.438 + Calc ("op =",eval_equal "#equal_")
1.439 + ],
1.440 + Some "solveSystem es_ vs_",
1.441 + []));
1.442 +store_pbt
1.443 + (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4" [] e_pblID
1.444 + (["4x4", "linear", "system"],
1.445 + (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.446 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.447 + ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]),
1.448 + ("#Find" ,["solution ss___"])
1.449 + ],
1.450 + append_rls "prls_4x4_linear_system" e_rls
1.451 + [Thm ("length_Cons_",num_str length_Cons_),
1.452 + Thm ("length_Nil_",num_str length_Nil_),
1.453 + Calc ("op +", eval_binop "#add_"),
1.454 + Calc ("op =",eval_equal "#equal_")
1.455 + ],
1.456 + Some "solveSystem es_ vs_",
1.457 + []));
1.458 +store_pbt
1.459 + (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID
1.460 + (["triangular", "4x4", "linear", "system"],
1.461 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.462 + ("#Where" , (*accepts missing variables up to diagional form*)
1.463 + ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.464 + "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.465 + "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.466 + "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.467 + ]),
1.468 + ("#Find" ,["solution ss___"])
1.469 + ],
1.470 + append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.471 + [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.472 + Some "solveSystem es_ vs_",
1.473 + [["EqSystem","top_down_substitution","4x4"]]));
1.474 +
1.475 +store_pbt
1.476 + (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_norm" [] e_pblID
1.477 + (["normalize", "4x4", "linear", "system"],
1.478 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.479 + (*length_ is checked 1 level above*)
1.480 + ("#Find" ,["solution ss___"])
1.481 + ],
1.482 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.483 + Some "solveSystem es_ vs_",
1.484 + [["EqSystem","normalize","4x4"]]));
1.485 +
1.486 +
1.487 +(* show_ptyps();
1.488 + *)
1.489 +
1.490 +(** methods **)
1.491 +
1.492 +store_met
1.493 + (prep_met EqSystem.thy "met_eqsys" [] e_metID
1.494 + (["EqSystem"],
1.495 + [],
1.496 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.497 + srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
1.498 + "empty_script"
1.499 + ));
1.500 +store_met
1.501 + (prep_met EqSystem.thy "met_eqsys_topdown" [] e_metID
1.502 + (["EqSystem","top_down_substitution"],
1.503 + [],
1.504 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.505 + srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
1.506 + "empty_script"
1.507 + ));
1.508 +store_met
1.509 + (prep_met EqSystem.thy "met_eqsys_topdown_2x2" [] e_metID
1.510 + (["EqSystem","top_down_substitution","2x2"],
1.511 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.512 + ("#Where" ,
1.513 + ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
1.514 + " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.515 + ("#Find" ,["solution ss___"])
1.516 + ],
1.517 + {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.518 + srls = append_rls "srls_top_down_2x2" e_rls
1.519 + [Thm ("hd_thm",num_str hd_thm),
1.520 + Thm ("tl_Cons",num_str tl_Cons),
1.521 + Thm ("tl_Nil",num_str tl_Nil)
1.522 + ],
1.523 + prls = prls_triangular, crls = Erls, nrls = Erls},
1.524 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.525 +\ (let e1__ = Take (hd es_); \
1.526 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.527 +\ isolate_bdvs False)) @@ \
1.528 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.529 +\ simplify_System False))) e1__; \
1.530 +\ e2__ = Take (hd (tl es_)); \
1.531 +\ e2__ = ((Substitute [e1__]) @@ \
1.532 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.533 +\ simplify_System_parenthesized False)) @@ \
1.534 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.535 +\ isolate_bdvs False)) @@ \
1.536 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.537 +\ simplify_System False))) e2__; \
1.538 +\ es__ = Take [e1__, e2__] \
1.539 +\ in (Try (Rewrite_Set order_system False)) es__)"
1.540 +(*---------------------------------------------------------------------------
1.541 + this script does NOT separate the equations as abolve,
1.542 + but it does not yet work due to preliminary script-interpreter,
1.543 + see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
1.544 +
1.545 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.546 +\ (let es__ = Take es_; \
1.547 +\ e1__ = hd es__; \
1.548 +\ e2__ = hd (tl es__); \
1.549 +\ es__ = [e1__, Substitute [e1__] e2__] \
1.550 +\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.551 +\ simplify_System_parenthesized False)) @@ \
1.552 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
1.553 +\ isolate_bdvs False)) @@ \
1.554 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.555 +\ simplify_System False))) es__)"
1.556 +---------------------------------------------------------------------------*)
1.557 + ));
1.558 +store_met
1.559 + (prep_met EqSystem.thy "met_eqsys_norm" [] e_metID
1.560 + (["EqSystem","normalize"],
1.561 + [],
1.562 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.563 + srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
1.564 + "empty_script"
1.565 + ));
1.566 +store_met
1.567 + (prep_met EqSystem.thy "met_eqsys_norm_2x2" [] e_metID
1.568 + (["EqSystem","normalize","2x2"],
1.569 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.570 + ("#Find" ,["solution ss___"])],
1.571 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.572 + srls = append_rls "srls_normalize_2x2" e_rls
1.573 + [Thm ("hd_thm",num_str hd_thm),
1.574 + Thm ("tl_Cons",num_str tl_Cons),
1.575 + Thm ("tl_Nil",num_str tl_Nil)
1.576 + ],
1.577 + prls = Erls, crls = Erls, nrls = Erls},
1.578 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.579 +\ (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ \
1.580 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.581 +\ simplify_System_parenthesized False)) @@ \
1.582 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.583 +\ isolate_bdvs False)) @@ \
1.584 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.585 +\ simplify_System_parenthesized False)) @@ \
1.586 +\ (Try (Rewrite_Set order_system False))) es_ \
1.587 +\ in (SubProblem (EqSystem_,[linear,system],[no_met]) \
1.588 +\ [bool_list_ es__, real_list_ vs_]))"
1.589 + ));
1.590 +
1.591 +(*this is for nth_ only*)
1.592 +val srls = Rls {id="srls_normalize_4x4",
1.593 + preconds = [],
1.594 + rew_ord = ("termlessI",termlessI),
1.595 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.596 + [(*for asm in nth_Cons_ ...*)
1.597 + Calc ("op <",eval_equ "#less_"),
1.598 + (*2nd nth_Cons_ pushes n+-1 into asms*)
1.599 + Calc("op +", eval_binop "#add_")
1.600 + ],
1.601 + srls = Erls, calc = [],
1.602 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.603 + Calc("op +", eval_binop "#add_"),
1.604 + Thm ("nth_Nil_",num_str nth_Nil_)],
1.605 + scr = EmptyScr};
1.606 +store_met
1.607 + (prep_met EqSystem.thy "met_eqsys_norm_4x4" [] e_metID
1.608 + (["EqSystem","normalize","4x4"],
1.609 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.610 + ("#Find" ,["solution ss___"])],
1.611 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.612 + srls = append_rls "srls_normalize_4x4" srls
1.613 + [Thm ("hd_thm",num_str hd_thm),
1.614 + Thm ("tl_Cons",num_str tl_Cons),
1.615 + Thm ("tl_Nil",num_str tl_Nil)
1.616 + ],
1.617 + prls = Erls, crls = Erls, nrls = Erls},
1.618 +(*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.619 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.620 +\ (let es__ = \
1.621 +\ ((Try (Rewrite_Set norm_Rational False)) @@ \
1.622 +\ (Repeat (Rewrite commute_0_equality False)) @@ \
1.623 +\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.624 +\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.625 +\ simplify_System_parenthesized False)) @@ \
1.626 +\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.627 +\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.628 +\ isolate_bdvs_4x4 False)) @@ \
1.629 +\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.630 +\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.631 +\ simplify_System_parenthesized False)) @@ \
1.632 +\ (Try (Rewrite_Set order_system False))) es_ \
1.633 +\ in (SubProblem (EqSystem_,[linear,system],[no_met]) \
1.634 +\ [bool_list_ es__, real_list_ vs_]))"
1.635 +));
1.636 +store_met
1.637 +(prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID
1.638 + (["EqSystem","top_down_substitution","4x4"],
1.639 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.640 + ("#Where" , (*accepts missing variables up to diagonal form*)
1.641 + ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.642 + "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.643 + "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.644 + "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.645 + ]),
1.646 + ("#Find" ,["solution ss___"])
1.647 + ],
1.648 + {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.649 + srls = append_rls "srls_top_down_4x4" srls [],
1.650 + prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.651 + [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.652 + crls = Erls, nrls = Erls},
1.653 +(*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.654 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.655 +\ (let e1_ = nth_ 1 es_; \
1.656 +\ e2_ = Take (nth_ 2 es_); \
1.657 +\ e2_ = ((Substitute [e1_]) @@ \
1.658 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.659 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.660 +\ simplify_System_parenthesized False)) @@ \
1.661 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.662 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.663 +\ isolate_bdvs False)) @@ \
1.664 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.665 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.666 +\ norm_Rational False))) e2_ \
1.667 +\ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
1.668 +));
1.669 +
1.670 +(* show_mets();
1.671 + *)
1.672 +
1.673 +(*
1.674 +use"IsacKnowledge/EqSystem.ML";
1.675 +use"EqSystem.ML";
1.676 +*)