1 (* Title: "Specify/specify.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
11 "----------- maximum-example: complete_metitms -------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
16 "----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
17 "----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
18 "----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
19 (*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
20 val (p,_,f,nxt,_,pt) =
22 [(["fixedValues [r=Arbfix]","maximum A",
24 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
25 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
26 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
28 "boundVariable a","boundVariable b","boundVariable alpha",
29 "interval {x::real. 0 <= x & x <= 2*r}",
30 "interval {x::real. 0 <= x & x <= 2*r}",
31 "interval {x::real. 0 <= x & x <= pi}",
32 "errorBound (eps=(0::real))"],
33 ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
35 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
38 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
39 val pits = get_obj g_pbl pt (fst p);
40 writeln (I_Model.to_string ctxt pits);
42 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
43 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
44 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
45 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
46 val (pt,p) = complete_mod (pt,p);
47 val pits = get_obj g_pbl pt (fst p);
48 if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
49 then () else error "completetest.sml: new behav. in complete_mod 3";
50 writeln (I_Model.to_string ctxt pits);
52 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
53 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
54 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
55 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
56 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
57 val mits = get_obj g_met pt (fst p);
58 if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
59 then () else error "completetest.sml: new behav. in complete_mod 3";
60 writeln (I_Model.to_string ctxt mits);
62 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
63 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
64 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
65 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
66 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
67 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
68 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
69 0 <= x & x <= 2 * r}])),
70 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
71 ( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
73 "----------- maximum-example: complete_metitms -------------------------------------------------";
74 "----------- maximum-example: complete_metitms -------------------------------------------------";
75 "----------- maximum-example: complete_metitms -------------------------------------------------";
77 val (p,_,f,nxt,_,pt) =
79 [(["fixedValues [r=Arbfix]","maximum A",
81 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
82 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
83 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
85 "boundVariable a","boundVariable b","boundVariable alpha",
86 "interval {x::real. 0 <= x & x <= 2*r}",
87 "interval {x::real. 0 <= x & x <= 2*r}",
88 "interval {x::real. 0 <= x & x <= pi}",
89 "errorBound (eps=(0::real))"],
90 ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
92 val (p,_,f,nxt,_,pt) = me nxt p c pt;
93 val (p,_,f,nxt,_,pt) = me nxt p c pt;
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;
96 val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e;*)
97 val (p,_,f,nxt,_,pt) = me nxt p c pt;
98 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 (*nxt = Specify_Theory "DiffApp"*)
100 val (oris, _, _) = get_obj g_origin pt (fst p);
101 writeln (O_Model.to_string oris);
103 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
104 (2, ["1","2","3"], #Find,maximum, ["A"]),
105 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
106 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
107 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
108 (6, ["1"], #undef,boundVariable, ["a"]),
109 (7, ["2"], #undef,boundVariable, ["b"]),
110 (8, ["3"], #undef,boundVariable, ["alpha"]),
111 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
112 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
113 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
114 val pits = get_obj g_pbl pt (fst p);
115 writeln (I_Model.to_string ctxt pits);
117 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
118 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
119 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
120 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
121 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
122 val mits = get_obj g_met pt (fst p);
123 val mits = complete_metitms oris pits []
124 ((#ppc o Method.from_store) ["DiffApp","max_by_calculus"]);
125 writeln (I_Model.to_string ctxt mits);
127 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
128 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
129 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
130 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
131 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
132 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
133 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
134 0 <= x & x <= 2 * r}])),
135 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
136 if I_Model.to_string ctxt mits
137 = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_m, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
138 then () else error "completetest.sml: new behav. in complete_metitms 1";