|
neuper@37906
|
1 |
(* RL 09.02
|
|
neuper@37906
|
2 |
testexamples for RatEq, equations with fractions
|
|
neuper@37906
|
3 |
|
|
neuper@37906
|
4 |
Compiler.Control.Print.printDepth:=10; (*4 default*)
|
|
neuper@37906
|
5 |
Compiler.Control.Print.printDepth:=5; (*4 default*)
|
|
neuper@37906
|
6 |
trace_rewrite:=true;
|
|
neuper@37906
|
7 |
|
|
neuper@37906
|
8 |
use"kbtest/rateq.sml";
|
|
neuper@37906
|
9 |
*)
|
|
neuper@37906
|
10 |
"----------- rateq.sml begin--------";
|
|
neuper@37906
|
11 |
"---------(1/x=5) ---------------------";
|
|
neuper@37906
|
12 |
"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
|
|
neuper@37906
|
13 |
|
|
neuper@41943
|
14 |
(*=== inhibit exn ?=============================================================
|
|
neuper@41943
|
15 |
|
|
neuper@37906
|
16 |
val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
|
|
neuper@37926
|
17 |
val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
|
|
neuper@37906
|
18 |
val result = term2str t_;
|
|
neuper@41928
|
19 |
if result <> "HOL.True" then error "rateq.sml: new behaviour 1:" else ();
|
|
neuper@37906
|
20 |
|
|
neuper@37906
|
21 |
val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
|
|
neuper@37926
|
22 |
val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
|
|
neuper@37906
|
23 |
val result = term2str t_;
|
|
neuper@41928
|
24 |
if result <> "HOL.False" then error "rateq.sml: new behaviour 2:" else ();
|
|
neuper@37906
|
25 |
|
|
neuper@37906
|
26 |
val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
|
|
neuper@37926
|
27 |
val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
|
|
neuper@37906
|
28 |
val result = term2str t_;
|
|
neuper@41928
|
29 |
if result <> "HOL.False" then error "rateq.sml: new behaviour 3:" else ();
|
|
neuper@37906
|
30 |
|
|
neuper@37906
|
31 |
val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
|
|
neuper@37926
|
32 |
val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
|
|
neuper@37906
|
33 |
val result = term2str t_;
|
|
neuper@41928
|
34 |
if result <> "HOL.True" then error "rateq.sml: new behaviour 4:" else ();
|
|
neuper@37906
|
35 |
|
|
neuper@37906
|
36 |
val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
|
|
neuper@37906
|
37 |
(get_pbt ["rational","univariate","equation"]);
|
|
neuper@38031
|
38 |
case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
|
|
neuper@37906
|
39 |
|
|
neuper@37906
|
40 |
val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
|
|
neuper@37906
|
41 |
(get_pbt ["rational","univariate","equation"]);
|
|
neuper@38031
|
42 |
case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
|
|
neuper@37906
|
43 |
|
|
neuper@37906
|
44 |
|
|
neuper@37906
|
45 |
(*---------rateq---- 23.8.02 ---------------------*)
|
|
neuper@37906
|
46 |
"---------(1/x=5) ---------------------";
|
|
neuper@37906
|
47 |
val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
|
|
neuper@37906
|
48 |
(* refine fmz ["univariate","equation"];
|
|
neuper@37906
|
49 |
*)
|
|
neuper@37906
|
50 |
|
|
neuper@37991
|
51 |
val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
52 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
53 |
(* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
54 |
--------------------------------------- Refine_Tacitly*)
|
|
neuper@37906
|
55 |
(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
|
|
neuper@37906
|
56 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
57 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
58 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
59 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
60 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37991
|
61 |
(* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*)
|
|
neuper@37906
|
62 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
63 |
(* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
64 |
--------------------------------------- Refine_Tacitly*)
|
|
neuper@37906
|
65 |
(*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
|
|
neuper@37906
|
66 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
68 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
69 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
70 |
(*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)
|
|
neuper@37906
|
71 |
|
|
neuper@37906
|
72 |
(* get_obj g_fmz pt [2];
|
|
neuper@37906
|
73 |
*)
|
|
neuper@37906
|
74 |
|
|
neuper@37906
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
76 |
(**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
|
|
neuper@37906
|
77 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37991
|
78 |
(* val nxt = ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
|
|
neuper@37906
|
79 |
|
|
neuper@37906
|
80 |
|
|
neuper@37906
|
81 |
|
|
neuper@37906
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
84 |
(* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
|
|
neuper@37906
|
85 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
86 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
87 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
89 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
90 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
91 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
92 |
(* "x = 1 / 5" *)
|
|
neuper@37906
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
94 |
if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then ()
|
|
neuper@38031
|
95 |
else error "rateq.sml: new behaviour: [x = 1 / 5]";
|
|
neuper@37906
|
96 |
|
|
neuper@37906
|
97 |
|
|
neuper@37906
|
98 |
|
|
neuper@37906
|
99 |
(*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
|
|
neuper@37906
|
100 |
"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
|
|
neuper@37906
|
101 |
(*EP Schalk_II_p68_n40*)
|
|
neuper@37906
|
102 |
val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];
|
|
neuper@37906
|
103 |
(* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",
|
|
neuper@37906
|
104 |
"solveFor x","solutions L"];*)
|
|
neuper@37906
|
105 |
|
|
neuper@37906
|
106 |
(* refine fmz ["univariate","equation"];
|
|
neuper@37906
|
107 |
*)
|
|
neuper@37906
|
108 |
|
|
neuper@37991
|
109 |
val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
110 |
(*val p = e_pos';
|
|
neuper@37906
|
111 |
val c = [];
|
|
neuper@37906
|
112 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
|
neuper@37906
|
113 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
|
neuper@37906
|
114 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
115 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
116 |
(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
|
|
neuper@37906
|
117 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
118 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
119 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
120 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
121 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
122 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37991
|
123 |
(* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
|
|
neuper@37906
|
124 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
125 |
(* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
|
|
neuper@37906
|
126 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
127 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37991
|
132 |
(* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
|
|
neuper@37906
|
133 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
134 |
(* nxt = ("Model_Problem", Model_Problem
|
|
neuper@37906
|
135 |
["abcFormula","degree_2","polynomial","univariate","equation"])*)
|
|
neuper@37906
|
136 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
138 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
141 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
143 |
(* "x = -2, x = 10" *)
|
|
neuper@37906
|
144 |
if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then()
|
|
neuper@38031
|
145 |
else error "rateq.sml: new behaviour: [x = -2, x = 10]";
|
|
neuper@37906
|
146 |
|
|
neuper@37906
|
147 |
"----------- rateq.sml end--------";
|
|
neuper@41943
|
148 |
|
|
neuper@41943
|
149 |
===== inhibit exn ?===========================================================*)
|