1 (* 1.if-te-else- 8.02 f"ur Richard
4 use"tests/rationals2.sml";
9 (*---------------- 25.7.02 ---------------------*)
12 val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
13 val Some(ss,tt) = eval_contains_root "xxx" 1 t thy;
15 val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";
16 val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
19 val v = (term_of o the o (parse thy)) "x";
20 val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)";
22 val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)";
24 val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
26 val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
29 val t = (term_of o the o (parse thy))
30 "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";
31 val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
33 val t = (term_of o the o (parse thy))
34 "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";
35 val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
37 val t = (term_of o the o (parse Test.thy))
38 "is_rootequation_in (sqrt(x)=1) x";
40 val t = (term_of o the o (parse Isac.thy))
41 "is_rootequation_in (sqrt(x)=1) x";
45 val Some(tt,_) = rewrite_set_ Test.thytrue tval_rls t;
47 val Some(tt,_) = rewrite_set_ Isac.thy true tval_rls t;
49 rewrite_set "Isac.thy" true
50 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
51 rewrite_set "Test.thy" true
52 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
55 (*WN: ^^^--- bitte nimm vorerst immer Isac.thy, damit wird richtig gematcht,
56 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
58 (prep_pbt (*Test.thy*) Isac.thy
59 (["root","univariate","equation","test"],
60 [("#Given" ,["equality e_","solveFor v_"]),
61 ("#Where" ,["is_rootequation_in (e_::bool) (v_::real)"]),
62 ("#Find" ,["solutions v_i_"])
64 append_rls e_rls [Calc ("Test.is'_rootequation'_in",
65 eval_is_rootequation_in "")],
66 [("Test.thy","methode")]));
68 match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root","univariate","equation","test"]);
71 (*---------------- 29.7.02 ---------------------*)
75 (["approximate","univariate","equation","test"],
76 [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
77 ("#Where" ,["matches (?a = ?b) e_"]),
78 ("#Find" ,["solutions v_i_"])
80 append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],
83 methods:= overwritel (!methods,
86 (("Isac.thy","solve_univar_err"):metID,
87 [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
88 ("#Find" ,["solutions v_i_"])
90 {rew_ord'="tless_true",rls'="tval_rls",erls=e_rls,prls=e_rls,calc=[],
91 asm_rls=[],asm_thm=[]},
92 "Script Solve_univar_err (e_::bool) (v_::real) (err_::bool) = \
93 \ (if (is_rootequation_in e_ v_)\
94 \ then ((SubProblem (Isac_,[squareroot,univariate,equation],\
95 \ (SqRoot_,square_equation)) [bool_ e_, real_ v_, bool_ err_]))\
96 \ else ((SubProblem (Isac_,[linear,univariate,equation],\
97 \ (RatArith_,solve_linear)) [bool_ e_, real_ v_])))"
100 val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",
103 ("Isac.thy",["approximate","univariate","equation","test"],
104 ("Isac.thy","solve_univar_err"));
105 val p = e_pos'; val c = [];
106 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
107 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
115 (*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
117 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 (*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)
126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]"))
132 andalso nxt = ("End_Proof'",End_Proof') then ()
133 else raise error "new behaviour in testexample rationals2.sml 1+2*x=0";
135 (*---------------------------------*)
136 "-------------- is_rootequ_in - SubProblem -------------------------";
137 "-------------- is_rootequ_in - SubProblem -------------------------";
138 "-------------- is_rootequ_in - SubProblem -------------------------";
139 val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",
142 ("Isac.thy",["approximate","univariate","equation","test"],
143 ("Isac.thy","solve_univar_err"));
144 val p = e_pos'; val c = [];
145 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
146 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 (*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
166 if p = ([1,1],Frm) andalso
167 f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso
168 nxt = ("Empty_Mstep",Empty_Mstep) (*script ist noch 'helpless'*) then ()
169 else raise error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0";