1.1 --- a/src/Tools/isac/IsacKnowledge/EqSystem.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,673 +0,0 @@
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 - ((Syntax.string_of_term (thy2ctxt 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 - ((Syntax.string_of_term (thy2ctxt 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 -*)