28 |
28 |
29 |
29 |
30 |
30 |
31 |
31 |
32 (* |
32 (* |
33 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
33 > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3"; |
34 > val eval_fn = the (assoc (!eval_list, "pow")); |
34 > val eval_fn = the (assoc (!eval_list, "pow")); |
35 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
35 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
36 > Syntax.string_of_term (thy2ctxt thy) t'; |
36 > Syntax.string_of_term (thy2ctxt thy) t'; |
37 *) |
37 *) |
38 (******************************************************************) |
38 (******************************************************************) |
118 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
118 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
119 val givens = map (the o (parse thy)) given; |
119 val givens = map (the o (parse thy)) given; |
120 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}"; |
120 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}"; |
121 (* 31.1.00 |
121 (* 31.1.00 |
122 val tag__forms = chktyps thy (formals, givens); |
122 val tag__forms = chktyps thy (formals, givens); |
123 map ((atomty) o term_of) tag__forms; *) |
123 map ((atomty) o Thm.term_of) tag__forms; *) |
124 |
124 |
125 " --- subproblem 2: linear-equation --- "; |
125 " --- subproblem 2: linear-equation --- "; |
126 val origin = ["x + 4 = (0::real)","x::real"]; |
126 val origin = ["x + 4 = (0::real)","x::real"]; |
127 val formals = map (the o (parse thy)) origin; |
127 val formals = map (the o (parse thy)) origin; |
128 |
128 |
133 val with_ = ["l = (%x. l) bdv"]; |
133 val with_ = ["l = (%x. l) bdv"]; |
134 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_); |
134 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_); |
135 val givens = map (the o (parse thy)) given; |
135 val givens = map (the o (parse thy)) given; |
136 |
136 |
137 val tag__forms = chktyps thy (formals, givens); |
137 val tag__forms = chktyps thy (formals, givens); |
138 map ((atomty) o term_of) tag__forms; |
138 map ((atomty) o Thm.term_of) tag__forms; |
139 |
139 |
140 |
140 |
141 |
141 |
142 " _________________ rewrite_ x+4_________________ "; |
142 " _________________ rewrite_ x+4_________________ "; |
143 " _________________ rewrite_ x+4_________________ "; |
143 " _________________ rewrite_ x+4_________________ "; |
144 " _________________ rewrite_ x+4_________________ "; |
144 " _________________ rewrite_ x+4_________________ "; |
145 val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
145 val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
146 val thm = num_str @{thm square_equation_left}; |
146 val thm = num_str @{thm square_equation_left}; |
147 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t); |
147 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t); |
148 val rls = Test_simplify; |
148 val rls = Test_simplify; |
149 val (t,_) = the (rewrite_set_ thy false rls t); |
149 val (t,_) = the (rewrite_set_ thy false rls t); |
150 val rls = rearrange_assoc; |
150 val rls = rearrange_assoc; |
208 " _________________ rewrite x=4_________________ "; |
208 " _________________ rewrite x=4_________________ "; |
209 " _________________ rewrite x=4_________________ "; |
209 " _________________ rewrite x=4_________________ "; |
210 " _________________ rewrite x=4_________________ "; |
210 " _________________ rewrite x=4_________________ "; |
211 (* |
211 (* |
212 rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct; |
212 rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct; |
213 atomty ((#prop o rep_thm) (!tthm)); |
213 atomty ((#prop o Thm.rep_thm) (!tthm)); |
214 atomty (term_of (!tct)); |
214 atomty (Thm.term_of (!tct)); |
215 *) |
215 *) |
216 val thy' = "Test"; |
216 val thy' = "Test"; |
217 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
217 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
218 (*1*)val thm = ("square_equation_left",""); |
218 (*1*)val thm = ("square_equation_left",""); |
219 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
219 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
571 next_tac thy' (pt'(*'*),p') sc is'; |
571 next_tac thy' (pt'(*'*),p') sc is'; |
572 |
572 |
573 |
573 |
574 |
574 |
575 |
575 |
576 val ttt = (term_of o the o (parse Test.thy)) |
576 val ttt = (Thm.term_of o the o (parse Test.thy)) |
577 "Let (((While contains_root e_e Do\ |
577 "Let (((While contains_root e_e Do\ |
578 \Rewrite square_equation_left True @@\ |
578 \Rewrite square_equation_left True @@\ |
579 \Try (Rewrite_Set Test_simplify False) @@\ |
579 \Try (Rewrite_Set Test_simplify False) @@\ |
580 \Try (Rewrite_Set rearrange_assoc False) @@\ |
580 \Try (Rewrite_Set rearrange_assoc False) @@\ |
581 \Try (Rewrite_Set Test_simplify False)) @@\ |
581 \Try (Rewrite_Set Test_simplify False)) @@\ |