1.1 --- a/src/sml/IsacKnowledge/PolyEq.ML Thu May 29 21:17:25 2003 +0200
1.2 +++ b/src/sml/IsacKnowledge/PolyEq.ML Fri May 30 19:13:25 2003 +0200
1.3 @@ -1,5 +1,5 @@
1.4 (* (c) by Richard Lang
1.5 - collecting all knowledge for PolynomialEquations
1.6 + collecting all knowledge for PolynomialEquations
1.7 created by: rlang
1.8 date: 02.07
1.9 changed by: rlang
1.10 @@ -22,12 +22,14 @@
1.11 theory' := overwritel (!theory', [("PolyEq.thy",PolyEq.thy)]);
1.12 (*-------------------------functions---------------------*)
1.13 local
1.14 + (* just for try*)
1.15 fun add0 l d d_ = if (d_+1) < d then add0 (str2term"0"::l) d (d_+1) else l;
1.16 fun poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("Atools.pow",_) $ v_ $ Free (d_,_)))) v l d =
1.17 if (v=v_)
1.18 then poly2list_ t1 v (((str2term("1")))::(add0 l d (int_of_str' d_))) (int_of_str' d_)
1.19 else t::(add0 l d 0)
1.20 - | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ (Const ("Atools.pow",_) $ v_ $ Free (d_,_))))) v l d =
1.21 + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $
1.22 + (Const ("Atools.pow",_) $ v_ $ Free (d_,_))))) v l d =
1.23 if (v=v_)
1.24 then poly2list_ t1 v (((t11))::(add0 l d (int_of_str' d_))) (int_of_str' d_)
1.25 else t::(add0 l d 0)
1.26 @@ -179,36 +181,14 @@
1.27 Calc ("op *",eval_binop "#mult_"),
1.28 Calc ("HOL.divide", eval_cancel "#divide_"),
1.29 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.30 - Calc ("Atools.pow" ,eval_binop "#power_")
1.31 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.32 + Rls_ reduce_012
1.33 ],
1.34 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.35 }:rls;
1.36 ruleset' := overwritel (!ruleset',
1.37 [("polyeq_simplify",polyeq_simplify)]);
1.38
1.39 -val normalize_poly =
1.40 - Rls{id = "normalize_poly", preconds = [],
1.41 - rew_ord = ("termlessI",termlessI),
1.42 - erls = polyeq_erls,
1.43 - srls = Erls,
1.44 - calc = [],
1.45 - asm_thm = [],
1.46 - rules = [Thm ("all_left",num_str all_left), (* (a=b) = (a+(-1)*b=0) *)
1.47 - Thm ("makex1_x",num_str makex1_x), (* a^^^1 = a *)
1.48 - Thm ("real_assoc_1",num_str real_assoc_1), (* a+(b+c) = a+b+c *)
1.49 - Calc ("op +",eval_binop "#add_"),
1.50 - Calc ("op -",eval_binop "#sub_"),
1.51 - Calc ("op *",eval_binop "#mult_"),
1.52 - Calc ("HOL.divide", eval_cancel "#divide_"),
1.53 - Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.54 - Calc ("Atools.pow" ,eval_binop "#power_")
1.55 - ],
1.56 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.57 - }:rls;
1.58 -
1.59 -ruleset' := overwritel (!ruleset',
1.60 - [("normalize_poly", normalize_poly)
1.61 - ]);
1.62
1.63 (* ------------- polySolve ------------------ *)
1.64 (* -- d0 -- *)
1.65 @@ -650,14 +630,14 @@
1.66 asm_rls=[],
1.67 asm_thm=[]},
1.68 (*RL: Ratpoly loest Brueche ohne bdv*)
1.69 - "Script Normalize_poly (e_::bool) (v_::real) = \
1.70 - \(let e_ =((Try (Rewrite all_left False)) @@ \
1.71 - \ (Try (Repeat (Rewrite makex1_x False))) @@ \
1.72 - \ (Try (Repeat (Rewrite_Set expand_binoms False))) @@ \
1.73 - \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \
1.74 - \ make_ratpoly_in False))) @@ \
1.75 - \ (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_ \
1.76 - \ in (SubProblem (PolyEq_,[polynomial,univariate,equation], \
1.77 + "Script Normalize_poly (e_::bool) (v_::real) = \
1.78 + \(let e_ =((Try (Rewrite all_left False)) @@ \
1.79 + \ (Try (Repeat (Rewrite makex1_x False))) @@ \
1.80 + \ (Try (Repeat (Rewrite_Set expand_binoms False))) @@ \
1.81 + \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \
1.82 + \ make_ratpoly_in False))) @@ \
1.83 + \ (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_ \
1.84 + \ in (SubProblem (PolyEq_,[polynomial,univariate,equation], \
1.85 \ [no_met]) [bool_ e_, real_ v_]))"
1.86 ));
1.87
1.88 @@ -676,8 +656,9 @@
1.89 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
1.90 asm_rls=[],
1.91 asm_thm=[]},
1.92 - "Script Solve_d0_polyeq_equation (e_::bool) (v_::real) = \
1.93 - \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d0_polyeq_simplify False))) e_ \
1.94 + "Script Solve_d0_polyeq_equation (e_::bool) (v_::real) = \
1.95 + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.96 + \ d0_polyeq_simplify False))) e_ \
1.97 \ in ((Or_to_List e_)::bool list))"
1.98 ));
1.99
1.100 @@ -697,11 +678,12 @@
1.101 (* asm_rls=["d1_polyeq_simplify"],*)
1.102 asm_rls=[],
1.103 asm_thm=[("d1_isolate_div","")]},
1.104 - "Script Solve_d1_polyeq_equation (e_::bool) (v_::real) = \
1.105 - \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d1_polyeq_simplify True)) @@ \
1.106 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.107 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.108 - \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.109 + "Script Solve_d1_polyeq_equation (e_::bool) (v_::real) = \
1.110 + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.111 + \ d1_polyeq_simplify True)) @@ \
1.112 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.113 + \ (Try (Rewrite_Set make_ratpoly False))) e_;\
1.114 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.115 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.116 ));
1.117
1.118 @@ -723,13 +705,15 @@
1.119 asm_thm = [("d1_isolate_div",""),("d2_pqformula1",""),("d2_pqformula2",""),
1.120 ("d2_pqformula3",""),("d2_pqformula4",""),("d2_abcformula1",""),
1.121 ("d2_abcformula2",""),("d2_sqrt_equation1",""),("d2_isolate_div","")]},
1.122 - "Script Solve_d2_polyeq_equation (e_::bool) (v_::real) = \
1.123 - \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d2_polyeq_simplify True)) @@ \
1.124 - \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.125 - \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] d1_polyeq_simplify True)) @@ \
1.126 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.127 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.128 - \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.129 + "Script Solve_d2_polyeq_equation (e_::bool) (v_::real) = \
1.130 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.131 + \ d2_polyeq_simplify True)) @@ \
1.132 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.133 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.134 + \ d1_polyeq_simplify True)) @@ \
1.135 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.136 + \ (Try (Rewrite_Set make_ratpoly False))) e_;\
1.137 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.138 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.139 ));
1.140
1.141 @@ -756,8 +740,8 @@
1.142 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.143 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.144 \ d1_polyeq_simplify True)) @@ \
1.145 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.146 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.147 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.148 + \ (Try (Rewrite_Set make_ratpoly False))) e_;\
1.149 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.150 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.151 ));
1.152 @@ -780,9 +764,9 @@
1.153 asm_thm=[("d2_sqrt_equation1",""),("d2_isolate_div","")]},
1.154 "Script Solve_d2_polyeq_sqonly_equation (e_::bool) (v_::real) =\
1.155 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.156 - \ d2_polyeq_sq_only_simplify True)) @@ \
1.157 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.158 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.159 + \ d2_polyeq_sq_only_simplify True)) @@ \
1.160 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.161 + \ (Try (Rewrite_Set make_ratpoly False))) e_; \
1.162 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.163 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.164 ));
1.165 @@ -806,12 +790,12 @@
1.166 ("d2_pqformula4",""),("d2_pqformula5",""),("d2_pqformula6",""),
1.167 ("d2_pqformula7",""),("d2_pqformula8",""),("d2_pqformula9",""),
1.168 ("d2_pqformula10","")]},
1.169 - "Script Solve_d2_polyeq_pq_equation (e_::bool) (v_::real) = \
1.170 - \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.171 - \ d2_polyeq_pqFormula_simplify True)) @@ \
1.172 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.173 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.174 - \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.175 + "Script Solve_d2_polyeq_pq_equation (e_::bool) (v_::real) = \
1.176 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.177 + \ d2_polyeq_pqFormula_simplify True)) @@ \
1.178 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.179 + \ (Try (Rewrite_Set make_ratpoly False))) e_;\
1.180 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.181 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.182 ));
1.183
1.184 @@ -835,11 +819,11 @@
1.185 ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""),
1.186 ("d2_abcformula10","")]},
1.187 "Script Solve_d2_polyeq_abc_equation (e_::bool) (v_::real) = \
1.188 - \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.189 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.190 \ d2_polyeq_abcFormula_simplify True)) @@ \
1.191 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.192 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.193 - \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.194 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.195 + \ (Try (Rewrite_Set make_ratpoly False))) e_;\
1.196 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.197 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.198 ));
1.199
1.200 @@ -862,15 +846,18 @@
1.201 ("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
1.202 ("d2_abcformula1",""),("d2_abcformula2",""),("d2_sqrt_equation1",""),
1.203 ("d2_isolate_div","")]},
1.204 - "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = \
1.205 - \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d3_polyeq_simplify True)) @@ \
1.206 - \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.207 - \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] d2_polyeq_simplify True)) @@ \
1.208 - \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.209 - \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] d1_polyeq_simplify True)) @@ \
1.210 - \ (Try (Rewrite_Set make_ratpoly False)) @@ \
1.211 - \ (Try (Rewrite_Set polyeq_simplify False))) e_;\
1.212 - \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.213 + "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = \
1.214 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.215 + \ d3_polyeq_simplify True)) @@ \
1.216 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.217 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.218 + \ d2_polyeq_simplify True)) @@ \
1.219 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.220 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.221 + \ d1_polyeq_simplify True)) @@ \
1.222 + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
1.223 + \ (Try (Rewrite_Set make_ratpoly False))) e_;\
1.224 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
1.225 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
1.226 ));
1.227
2.1 --- a/src/sml/IsacKnowledge/RatEq.ML Thu May 29 21:17:25 2003 +0200
2.2 +++ b/src/sml/IsacKnowledge/RatEq.ML Fri May 30 19:13:25 2003 +0200
2.3 @@ -167,12 +167,12 @@
2.4 ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),
2.5 ("rat_mult_denominator_right","")]},
2.6 "Script Solve_rat_equation (e_::bool) (v_::real) = \
2.7 - \(let e_ = ((Repeat(Try (Rewrite_Set rat_simplify True))) @@ \
2.8 - \ (Repeat(Try (Rewrite_Set make_ratpoly False))) @@ \
2.9 + \(let e_ = ((Repeat(Try (Rewrite_Set rat_simplify True))) @@ \
2.10 + \ (Repeat(Try (Rewrite_Set make_ratpoly False))) @@ \
2.11 \ (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ \
2.12 \ (Repeat(Try (Rewrite_Set rat_eliminate True)))) e_;\
2.13 \ (L_::bool list) = (SubProblem (RatEq_,[univariate,equation], \
2.14 - \ [no_met]) [bool_ e_, real_ v_]) \
2.15 + \ [no_met]) [bool_ e_, real_ v_]) \
2.16 \ in Check_elementwise L_ {(v_::real). Assumptions})"
2.17 ));
2.18 "******* RatEq.ML end *******";
3.1 --- a/src/sml/ROOT.ML Thu May 29 21:17:25 2003 +0200
3.2 +++ b/src/sml/ROOT.ML Fri May 30 19:13:25 2003 +0200
3.3 @@ -102,31 +102,29 @@
3.4 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
3.5 use"logexp.sml";
3.6 use"poly.sml"; (*TODO //*)
3.7 - use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all expanded)*)
3.8 + use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all expanded) WN*)
3.9 use"rateq.sml"; (*TODO //*)
3.10 use"ratrooteq.sml";(*TODO //*)
3.11 use"rational.sml"; (*TODO //*)
3.12 - use"root.sml"; (*TODO 1 Example: no set UniversalList*)
3.13 + use"root.sml"; (*TODO 1 Example: no set UniversalList WN*)
3.14 use"rooteq.sml"; (*TODO //*)
3.15 use"rlang.sml";
3.16 (*TODO Schalk I
3.17 - 104a, 104a(2), 118a, almost! rls? RL1
3.18 + 104a, almost! rls? RL2
3.19
3.20 Schalk II
3.21 68a, one solution too much =False!? WN
3.22 73b, no UniversalList WN
3.23 10b, 6 +...+x^3 not solvable WN
3.24 23b, [-1064944 + 32 * x + -48 * x ^^^ 2 = 0] e C WN
3.25 - 28a, seltsam grosses Ergebnis RL1
3.26 52b, check_postcond *** No such constant: "Root.sqrt" WN1
3.27 - 56a, common_nominator_p wird nicht angewendet RL1
3.28 - 61b, simplify result RL1
3.29 + 56a, common_nominator_p wird nicht angewendet RL2
3.30 + 61b, simplify result RL2
3.31 62b simplify asms
3.32
3.33 Pythagoras, extrem (WN) Problem with common_nominator_p =56a ?
3.34
3.35 -RL1: make_ratpoly
3.36 -RL2:
3.37 +RL2: geht auch mit make_ratpoly nicht
3.38 WN1: thy aus spec ueberschreibt thy aus pbl, met !!!
3.39 *)
3.40 use"termorder.sml";
4.1 --- a/src/sml/kbtest/polyeq.sml Thu May 29 21:17:25 2003 +0200
4.2 +++ b/src/sml/kbtest/polyeq.sml Fri May 30 19:13:25 2003 +0200
4.3 @@ -383,7 +383,6 @@
4.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.7 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.8 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
4.9 | _ => raise error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
4.10 (* [x = 2 / 15 , x = 1]*)
4.11 @@ -408,7 +407,6 @@
4.12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.15 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.16 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
4.17 | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
4.18
5.1 --- a/src/sml/kbtest/rateq.sml Thu May 29 21:17:25 2003 +0200
5.2 +++ b/src/sml/kbtest/rateq.sml Fri May 30 19:13:25 2003 +0200
5.3 @@ -12,30 +12,30 @@
5.4 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
5.5 val Some(t_, _) = rewrite_set_ RatEq.thy false rateq_prls t;
5.6 val result = term2str t_;
5.7 -if result <> "True" then raise error "rateq.sml: new behaviour:" else ();
5.8 +if result <> "True" then raise error "rateq.sml: new behaviour 1:" else ();
5.9
5.10 val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
5.11 val Some(t_, _) = rewrite_set_ RatEq.thy false rateq_prls t;
5.12 val result = term2str t_;
5.13 -if result <> "False" then raise error "rateq.sml: new behaviour:" else ();
5.14 +if result <> "False" then raise error "rateq.sml: new behaviour 2:" else ();
5.15
5.16 val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
5.17 val Some(t_,_) = rewrite_set_ RatEq.thy false rateq_prls t;
5.18 val result = term2str t_;
5.19 -if result <> "False" then raise error "rateq.sml: new behaviour:" else ();
5.20 +if result <> "False" then raise error "rateq.sml: new behaviour 3:" else ();
5.21
5.22 val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
5.23 val Some(t_,_) = rewrite_set_ RatEq.thy false rateq_prls t;
5.24 val result = term2str t_;
5.25 -if result <> "True" then raise error "rateq.sml: new behaviour:" else ();
5.26 +if result <> "True" then raise error "rateq.sml: new behaviour 4:" else ();
5.27
5.28 val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
5.29 (get_pbt ["rational","univariate","equation"]);
5.30 -case result of NoMatch' _ => () | _ => raise error "rateq.sml: new behaviour:";
5.31 +case result of NoMatch' _ => () | _ => raise error "rateq.sml: new behaviour: 5";
5.32
5.33 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
5.34 (get_pbt ["rational","univariate","equation"]);
5.35 -case result of Matches' _ => () | _ => raise error "rateq.sml: new behaviour:";
5.36 +case result of Matches' _ => () | _ => raise error "rateq.sml: new behaviour: 6";
5.37
5.38
5.39 (*---------rateq---- 23.8.02 ---------------------*)
5.40 @@ -77,7 +77,7 @@
5.41 (* "x = 1 / 5" *)
5.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.43 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then ()
5.44 -else raise error "rateq.sml: new behaviour:";
5.45 +else raise error "rateq.sml: new behaviour: [x = 1 / 5]";
5.46
5.47 (*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
5.48 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
5.49 @@ -121,9 +121,8 @@
5.50 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.53 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.54 (* "x = -2, x = 10" *)
5.55 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then ()
5.56 -else raise error "rateq.sml: new behaviour:";
5.57 +else raise error "rateq.sml: new behaviour: [x = -2, x = 10]";
5.58
5.59 "----------- rateq.sml end--------";
6.1 --- a/src/sml/kbtest/rlang.sml Thu May 29 21:17:25 2003 +0200
6.2 +++ b/src/sml/kbtest/rlang.sml Fri May 30 19:13:25 2003 +0200
6.3 @@ -579,9 +579,7 @@
6.4 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[]")) : mout
6.5 val nxt = Check_Postcond ["rational","univariate","equation"]) *)
6.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.7 -case f of Form'
6.8 - (FormKF
6.9 - (~1,EdUndef,0,Nundef,
6.10 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,
6.11 "[v = (u * v0 + v0 * w + -1 * f * w) / f]")) => ()
6.12 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
6.13 if get_assumptions_ pt p = [("(u * v0 + v0 * w + -1 * f * w) / f + w ~= 0",[])] then ()
6.14 @@ -657,8 +655,8 @@
6.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.16 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.17 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.18 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]"))
6.19 -then () else raise error "rlang.sml: diff.behav. in 98a(1)";
6.20 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]")) => ()
6.21 + | _ => raise error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
6.22 if get_assumptions_ pt p = [("R * R2 * R2 ~= (R2 + -1 * R) * 0 & R2 + -1 * R ~= 0",[])]
6.23 then writeln "should be simplified"
6.24 else raise error "rlang.sml: diff.behav. in 98a(1) asm";
6.25 @@ -683,8 +681,7 @@
6.26 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.29 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.30 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*d1_poly_simplify -> asms*)
6.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.32 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.33 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.34 case f of Form' (FormKF (_,_,_,_,"[p = -1 * y ^^^ 2 / (-2 * x)]")) => ()
6.35 @@ -721,7 +718,8 @@
6.36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.37 case f of Form' (FormKF (_,_,_,_,"[y = sqrt (2 * p * x), y = -1 * sqrt (2 * p * x)]")) => ()
6.38 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a(2) [x = ]";
6.39 -if get_assumptions_ pt p = [("0 <= -1 * (-2 * p * x)",[]),("0 <= -1 * (-2 * p * x)",[])] then ()
6.40 +if get_assumptions_ pt p = [("0 <= -1 * (-2 * p * x)",[]),("0 <= -1 * (-2 * p * x)",[])]
6.41 + then writeln "should be simplified"
6.42 else raise error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
6.43
6.44
6.45 @@ -889,7 +887,6 @@
6.46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.47 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.48 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.49 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.50 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4, x = 1 / 9]"))
6.51 then writeln "only [x = 4] ?\nonly [x = 4] ?\nonly [x = 4] ?\n"
6.52 else raise error "rlang.sml: diff.behav. in II 68a";
6.53 @@ -1088,7 +1085,6 @@
6.54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.57 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.58 case f of Form' (FormKF (_,_,_,_,"[x = 5, x = -5]")) => ()
6.59 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 4 []";
6.60
6.61 @@ -1123,7 +1119,6 @@
6.62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.65 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.66 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
6.67 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a [x = 2, x = -2]";
6.68
6.69 @@ -1199,7 +1194,7 @@
6.70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.73 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.74 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.75 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 5, x = -5]")) => ()
6.76 | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a [x = 5, x = -5]";
6.77
6.78 @@ -1280,7 +1275,7 @@
6.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.81 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[a = sqrt ((-1 * c ^^^ 4 + -1 * A ^^^ 2 * d ^^^ 2) / (-4 * c ^^^ 2)),\n a = -1 * sqrt ((-1 * c ^^^ 4 + -1 * A ^^^ 2 * d ^^^ 2) / (-4 * c ^^^ 2))]")) => ()
6.82 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a [...]";
6.83 + | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a [a=...]";
6.84
6.85 (*----------------- Schalk II s.68 Bsp 52b ------------------------*)
6.86 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";
6.87 @@ -1325,7 +1320,7 @@
6.88 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";
6.89 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))",
6.90 "solveFor x","solutions L"];
6.91 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
6.92 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
6.93 val p = e_pos';
6.94 val c = [];
6.95 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.96 @@ -1337,8 +1332,8 @@
6.97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.100 -(* "(a + b * x) / (a + -1 * b * x) + (-1 * a + b * x) / (a + b * x) = /
6.101 - / 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)"
6.102 +(* (a + b * x) / (a + -1 * b * x) + (-1 * a + b * x) / (a + b * x) =
6.103 + 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)"
6.104 common_nominator_p wird nicht angewendet
6.105 *)
6.106