5 'cterm 's' im Isabelle-Format (pretty-printing !)*) |
5 'cterm 's' im Isabelle-Format (pretty-printing !)*) |
6 |
6 |
7 ML> ... |
7 ML> ... |
8 ML> val c = (the o (parse thy)) s; |
8 ML> val c = (the o (parse thy)) s; |
9 val c = |
9 val c = |
10 "Script1 Maximum_value fix_ m_ rs_ v_v itv_ err_ = |
10 "Script1 Maximum_value f_ix m_ r_s v_v itv_ err_ = |
11 let e_e = (hd o filter (Testvar m_)) rs_; |
11 let e_e = (hd o filter (Testvar m_)) r_s; |
12 t_ = |
12 t_ = |
13 if #1 < Length rs_ |
13 if #1 < Length r_s |
14 then make_fun (R, [make, function], no_met) m_ v_v rs_ |
14 then make_fun (R, [make, function], no_met) m_ v_v r_s |
15 else (Lhs o hd) rs_; |
15 else (Lhs o hd) r_s; |
16 mx_ = |
16 mx_ = |
17 max_on_interval (R, [on_interval, max_of, function], |
17 max_on_interval (R, [on_interval, max_of, function], |
18 maximum_on_interval) t_ v_v itv_ |
18 maximum_on_interval) t_ v_v itv_ |
19 in find_vals (R, [find_values, tool], find_values) |
19 in find_vals (R, [find_values, tool], find_values) |
20 mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm |
20 mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm |
21 |
21 |
22 ML> set show_types; |
22 ML> set show_types; |
23 ML> c; |
23 ML> c; |
24 val c = |
24 val c = |
25 "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool = |
25 "Script1 Maximum_value f_ix::bool list m_::real r_s::bool list v_v::real itv_v::real set err_::bool = |
26 let e_e::bool = (hd o filter (Testvar m_)) rs_; |
26 let e_e::bool = (hd o filter (Testvar m_)) r_s; |
27 t_::real = |
27 t_::real = |
28 if (#1::real) < Length rs_ |
28 if (#1::real) < Length r_s |
29 then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v rs_ |
29 then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v r_s |
30 else (Lhs o hd) rs_; |
30 else (Lhs o hd) r_s; |
31 mx_::real = |
31 mx_::real = |
32 max_on_interval (R, [on_interval::ID, max_of::ID, function], |
32 max_on_interval (R, [on_interval::ID, max_of::ID, function], |
33 maximum_on_interval::ID) t_ v_v itv_ |
33 maximum_on_interval::ID) t_ v_v itv_ |
34 in find_vals (R, [find_values::ID, tool::ID], find_values) |
34 in find_vals (R, [find_values::ID, tool::ID], find_values) |
35 mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm |
35 mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm |
36 |
36 |
37 |
37 |
38 |
38 |
39 (* Die ersten 3 Scripts aus dem Maximum-Beispiel. |
39 (* Die ersten 3 Scripts aus dem Maximum-Beispiel. |
40 parse erzeugt aus dem string 's' den |
40 parse erzeugt aus dem string 's' den |
42 |
42 |
43 ML> ... |
43 ML> ... |
44 ML> val c = (the o (parse thy)) s; |
44 ML> val c = (the o (parse thy)) s; |
45 val c = |
45 val c = |
46 "Script maximum = |
46 "Script maximum = |
47 Input [Bool fix_, Real m_, BoolList rs_, Real v_v, RealSet itv_, Bool err_] |
47 Input [Bool f_ix, Real m_, BoolList r_s, Real v_v, RealSet itv_, Bool err_] |
48 Local [Bool e_e, Real t_, Real mx_, RealList vs_] |
48 Local [Bool e_e, Real t_, Real mx_, RealList v_s] |
49 Tacs [SEQU |
49 Tacs [SEQU |
50 [let e_e = (hd o filter (Testvar m_)) rs_ |
50 [let e_e = (hd o filter (Testvar m_)) r_s |
51 in if #1 < Length rs_ |
51 in if #1 < Length r_s |
52 then Subproblem Spec (R, [make, function], no_met) |
52 then Subproblem Spec (R, [make, function], no_met) |
53 InOut [In m_, In v_v, In rs_, Out t_] |
53 InOut [In m_, In v_v, In r_s, Out t_] |
54 else t_ := (Lhs o hd) rs_ ; |
54 else t_ := (Lhs o hd) r_s ; |
55 Subproblem Spec (R, [on_interval, max_of, function], |
55 Subproblem Spec (R, [on_interval, max_of, function], |
56 maximum_on_interval) |
56 maximum_on_interval) |
57 InOut [In t_, In v_v, In itv_, In err_, Out mx_] ; |
57 InOut [In t_, In v_v, In itv_, In err_, Out mx_] ; |
58 Subproblem Spec (R, [find_values, tool], find_values) |
58 Subproblem Spec (R, [find_values, tool], find_values) |
59 InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) rs_), |
59 InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) r_s), |
60 Out vs_]]] |
60 Out v_s]]] |
61 Return []" : cterm |
61 Return []" : cterm |
62 |
62 |
63 ML> ... |
63 ML> ... |
64 ML> val c = (the o (parse thy)) s; |
64 ML> val c = (the o (parse thy)) s; |
65 val c = |
65 val c = |
66 "Script make_fun_by_new_variable = |
66 "Script make_fun_by_new_variable = |
67 Input [Real f_f, Real v_v, BoolList eqs] |
67 Input [Real f_f, Real v_v, BoolList eqs] |
68 Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1, |
68 Local [Bool h_, BoolList es_, RealList v_s, Real v1_, Real v2_, Bool e1, |
69 Bool e2_, BoolList s_1, BoolList s_2] |
69 Bool e2_, BoolList s_1, BoolList s_2] |
70 Tacs [SEQU |
70 Tacs [SEQU |
71 [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_]; |
71 [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_]; |
72 vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_; |
72 v_s = Var h_ -- [f_]; v1_ = Nth #1 v_s; v2_ = Nth #2 v_s; |
73 e1_ = (hd o filter (Testvar v1_)) es_; |
73 e1_ = (hd o filter (Testvar v1_)) es_; |
74 e2_ = (hd o filter (Testvar v2_)) es_ |
74 e2_ = (hd o filter (Testvar v2_)) es_ |
75 in Subproblem Spec (R, [univar, equation], no_met) |
75 in Subproblem Spec (R, [univar, equation], no_met) |
76 InOut [In e1_, In v1_, Out s_1] ; |
76 InOut [In e1_, In v1_, Out s_1] ; |
77 Subproblem Spec (R, [univar, equation], no_met) |
77 Subproblem Spec (R, [univar, equation], no_met) |
83 ML> ... |
83 ML> ... |
84 ML> val c = (the o (parse thy)) s; |
84 ML> val c = (the o (parse thy)) s; |
85 val c = |
85 val c = |
86 "Script make_fun_explicit = |
86 "Script make_fun_explicit = |
87 Input [Real f_f, Real v_v, BoolList eqs] |
87 Input [Real f_f, Real v_v, BoolList eqs] |
88 Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_] |
88 Local [Bool h_, Bool eq_, RealList v_s, Real v1_, BoolList ss_] |
89 Tacs [SEQU |
89 Tacs [SEQU |
90 [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]); |
90 [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]); |
91 vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_]) |
91 v_s = Var h_ -- [f_]; v1_ = hd (v_s -- [v_]) |
92 in Subproblem Spec (R, [univar, equation], no_met) |
92 in Subproblem Spec (R, [univar, equation], no_met) |
93 InOut [In eq_, In v1_, Out ss_]], |
93 InOut [In eq_, In v1_, Out ss_]], |
94 Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]] |
94 Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]] |
95 Return [Currform]" : cterm |
95 Return [Currform]" : cterm |
96 ML> |
96 ML> |