1.1 --- a/src/sml/IsacKnowledge/EqSystem.ML Sat Sep 16 12:57:11 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML Sat Sep 16 21:29:08 2006 +0200
1.3 @@ -261,30 +261,28 @@
1.4 rules = [Thm ("commute_0_equality",
1.5 num_str commute_0_equality),
1.6 Thm ("separate_bdvs_add", num_str separate_bdvs_add),
1.7 - Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)(*,
1.8 - Thm ("", num_str ),
1.9 - Thm ("", num_str ),
1.10 - Thm ("", num_str )*)
1.11 - ],
1.12 + Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)],
1.13 scr = EmptyScr};
1.14 val isolate_bdvs_4x4 =
1.15 Rls {id="isolate_bdvs_4x4", preconds = [],
1.16 rew_ord = ("e_rew_ord", e_rew_ord),
1.17 - erls = append_rls "erls_isolate_bdvs_4x4" e_rls
1.18 - [(Calc ("EqSystem.occur'_exactly'_in",
1.19 - eval_occur_exactly_in
1.20 - "#eval_occur_exactly_in_"))
1.21 + erls = append_rls
1.22 + "erls_isolate_bdvs_4x4" e_rls
1.23 + [Calc ("EqSystem.occur'_exactly'_in",
1.24 + eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.25 + Calc ("Atools.ident",eval_ident "#ident_"),
1.26 + Calc ("Atools.some'_occur'_in",
1.27 + eval_some_occur_in "#some_occur_in_"),
1.28 + Thm ("not_true",num_str not_true),
1.29 + Thm ("not_false",num_str not_false)
1.30 ],
1.31 - srls = Erls, calc = [],
1.32 - rules = [Thm ("commute_0_equality",
1.33 - num_str commute_0_equality),
1.34 - Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
1.35 - (*GOON rls isolate_bdvs_4x4 @@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.36 - Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)(*,
1.37 - Thm ("", num_str ),
1.38 - Thm ("", num_str ),
1.39 - Thm ("", num_str )*)
1.40 - ],
1.41 + srls = Erls, calc = [],
1.42 + rules = [Thm ("commute_0_equality",
1.43 + num_str commute_0_equality),
1.44 + Thm ("separate_bdvs0", num_str separate_bdvs0),
1.45 + Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
1.46 + Thm ("separate_bdvs_add1", num_str separate_bdvs_add2),
1.47 + Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)],
1.48 scr = EmptyScr};
1.49
1.50 (*.order the equations in a system such, that a triangular system (if any)
1.51 @@ -483,8 +481,8 @@
1.52 [["EqSystem","normalize","4x4"]]));
1.53
1.54
1.55 -show_ptyps();
1.56 -
1.57 +(* show_ptyps();
1.58 + *)
1.59
1.60 (** methods **)
1.61
1.62 @@ -608,7 +606,7 @@
1.63 [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.64 ("#Find" ,["solution ss___"])],
1.65 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.66 - srls = append_rls "srls_normalize_4x4" e_rls
1.67 + srls = append_rls "srls_normalize_4x4" srls
1.68 [Thm ("hd_thm",num_str hd_thm),
1.69 Thm ("tl_Cons",num_str tl_Cons),
1.70 Thm ("tl_Nil",num_str tl_Nil)
1.71 @@ -618,6 +616,7 @@
1.72 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.73 \ (let es__ = \
1.74 \ ((Try (Rewrite_Set norm_Rational False)) @@ \
1.75 +\ (Repeat (Rewrite commute_0_equality False)) @@ \
1.76 \ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.77 \ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.78 \ simplify_System_parenthesized False)) @@ \
1.79 @@ -626,7 +625,7 @@
1.80 \ isolate_bdvs_4x4 False)) @@ \
1.81 \ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.82 \ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.83 -\ simplify_System False)) @@ \
1.84 +\ simplify_System_parenthesized False)) @@ \
1.85 \ (Try (Rewrite_Set order_system False))) es_ \
1.86 \ in (SubProblem (EqSystem_,[linear,system],[no_met]) \
1.87 \ [bool_list_ es__, real_list_ vs_]))"
1.88 @@ -635,7 +634,7 @@
1.89 (prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID
1.90 (["EqSystem","top_down_substitution","4x4"],
1.91 [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.92 - ("#Where" , (*accepts missing variables up to diagional form*)
1.93 + ("#Where" , (*accepts missing variables up to diagonal form*)
1.94 ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.95 "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.96 "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.97 @@ -671,7 +670,8 @@
1.98 \ in (Try (Rewrite_Set order_system False)) es__)"
1.99 ));
1.100
1.101 -show_mets();
1.102 +(* show_mets();
1.103 + *)
1.104
1.105 (*
1.106 use"IsacKnowledge/EqSystem.ML";
2.1 --- a/src/sml/IsacKnowledge/EqSystem.thy Sat Sep 16 12:57:11 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/EqSystem.thy Sat Sep 16 21:29:08 2006 +0200
2.3 @@ -5,6 +5,7 @@
2.4
2.5 remove_thy"EqSystem";
2.6 use_thy"IsacKnowledge/EqSystem";
2.7 +
2.8 use_thy_only"IsacKnowledge/EqSystem";
2.9
2.10 remove_thy"Typefix";
2.11 @@ -42,17 +43,17 @@
2.12 separate_bdvs_add
2.13 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.14 \ ==> (a + b = c) = (b = c + -1*a)"
2.15 + separate_bdvs0
2.16 + "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |]\
2.17 + \ ==> (a = b) = (a + -1*b = 0)"
2.18 separate_bdvs_add1
2.19 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\
2.20 \ ==> (a = b + c) = (a + -1*c = b)"
2.21 -(*
2.22 - separate_bdvs_add3
2.23 - "[| [bdv_3] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.24 - \ ==> (a + b = c) = (b = c + -1*a)"
2.25 - separate_bdvs_add4
2.26 - "[| [bdv_4] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.27 - \ ==> (a + b = c) = (b = c + -1*a)"
2.28 -*)
2.29 + separate_bdvs_add2
2.30 + "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]\
2.31 + \ ==> (a + b = c) = (b = -1*a + c)"
2.32 +
2.33 +
2.34
2.35 separate_bdvs_mult
2.36 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\
3.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml Sat Sep 16 12:57:11 2006 +0200
3.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Sat Sep 16 21:29:08 2006 +0200
3.3 @@ -1021,7 +1021,7 @@
3.4 "[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n 0 + -1 * (c_4 + L * c_3),\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]";
3.5
3.6
3.7 -"----- go through the rewrites in met_eqsys_norm_4x4";
3.8 +"----- 7.27 go through the rewrites in met_eqsys_norm_4x4";
3.9 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
3.10 val None = rewrite_set_ thy false norm_Rational t;
3.11 val Some (t,_) =
3.12 @@ -1086,67 +1086,87 @@
3.13 c_3 |
3.14 c_4 | GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.15
3.16 -"----- go through the rewrites in met_eqsys_norm_4x4";
3.17 +"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
3.18 val t = str2term"[L * q_0 = c, \
3.19 -\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
3.20 -\ 0 = c_4 + 0 / (-1 * EI), \
3.21 -\ 0 = c_3 + 0 / (-1 * EI)]";
3.22 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
3.23 + \ 0 = c_4, \
3.24 + \ 0 = c_3]";
3.25 val Some (t,_) =
3.26 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
3.27 val Some (t,_) =
3.28 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
3.29 val Some (t,_) =
3.30 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
3.31 -term2str t;
3.32 -
3.33 -
3.34 +term2str t =
3.35 + "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";
3.36 val Some (t,_) =
3.37 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
3.38 -term2str t;
3.39 +term2str t =
3.40 +"[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";
3.41 val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
3.42 -term2str t;
3.43 +term2str t =
3.44 + "[c = (-1 * (L * q_0) + 0) / -1,\n L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]";
3.45 +val Some (t,_) =
3.46 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
3.47 +term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
3.48 +val Some (t,_) = rewrite_set_ thy false order_system t;
3.49 +if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
3.50 +else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
3.51
3.52 -val Some (t',_) = rewrite_set_ thy false order_system t;
3.53 -term2str t';
3.54
3.55 -val t = str2term"c_3 + 0 / (-1 * EI)";
3.56 -val Some (t',_) = rewrite_set_ Isac.thy false reduce_0_1_2 t;
3.57 -term2str t';
3.58 -rewrite_set_ Isac.thy false norm_Rational t;
3.59 -term2str t';
3.60 -trace_rewrite := true;
3.61 -trace_rewrite := false;
3.62 -
3.63 -"----- 7.70 solving pbl with met";
3.64 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.65 +"----- 7.70 with met normalize: ";
3.66 val fmz = ["equalities \
3.67 - \[L * q_0 = c, \
3.68 - \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
3.69 - \ 0 = c_4, \
3.70 - \ 0 = c_3]",
3.71 + \[L * q_0 = c, \
3.72 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
3.73 + \ 0 = c_4, \
3.74 + \ 0 = c_3]",
3.75 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
3.76 val (dI',pI',mI') =
3.77 ("Biegelinie.thy",["linear", "system"],["no_met"]);
3.78 val p = e_pos'; val c = [];
3.79 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.83 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.84 +case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
3.85 + | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
3.86 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.88 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.90 +
3.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.92 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.95 +if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
3.96 +then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
3.97 +
3.98 +"----- 7.70 with met top_down_: ";
3.99 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.100 +val fmz = ["equalities \
3.101 + \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
3.102 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
3.103 +val (dI',pI',mI') =
3.104 + ("Biegelinie.thy",["linear", "system"],["no_met"]);
3.105 +val p = e_pos'; val c = [];
3.106 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.107 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.109 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.111 +case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
3.112 + | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
3.113 +
3.114 +
3.115 +print_depth 7; nxt; print_depth 3;
3.116 +
3.117 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.118
3.119
3.120 (*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.121 -map ((split_dts thy) o term_of o the o (parse thy)) fmz;
3.122 -map ((parse thy)) fmz;
3.123 -
3.124 -parse thy "[L * q_0 = c, \
3.125 - \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
3.126 - \ 0 = c_4, \
3.127 - \ 0 = c_3]";
3.128 -
3.129 (*
3.130 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.131 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.132 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.133 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.134 -case nxt of ("Specify_Method",_) => ()
3.135 - | _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
3.136
3.137
3.138