wneuper@59353
|
1 |
(* this is evaluated BEFORE Test_Isac.thy opens structures*)
|
e0726734@42026
|
2 |
|
neuper@48884
|
3 |
theory All_Ctxt imports
|
neuper@48884
|
4 |
"~~/src/Tools/isac/Knowledge/Isac"
|
neuper@48884
|
5 |
(*Isac ...ERROR Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/Isac.thy")
|
neuper@48884
|
6 |
from Isac.thy ...*)
|
neuper@48884
|
7 |
begin
|
neuper@42023
|
8 |
|
neuper@42023
|
9 |
text {* all changes of context are demonstrated in a mini example.
|
neuper@42023
|
10 |
see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 --- *}
|
neuper@42023
|
11 |
|
neuper@42023
|
12 |
section {* start of the mini example *}
|
neuper@42023
|
13 |
|
neuper@42023
|
14 |
ML {*
|
neuper@42033
|
15 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
neuper@42023
|
16 |
val (dI',pI',mI') =
|
neuper@42023
|
17 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@42023
|
18 |
["Test","squ-equ-test-subpbl1"]);
|
wneuper@59261
|
19 |
val (p,_,f,nxt,_,pt) = Math_Engine.CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@42023
|
20 |
*}
|
neuper@42023
|
21 |
|
neuper@42023
|
22 |
section {* start of specify phase *}
|
neuper@42023
|
23 |
text {* variables known from formalisation provide type-inference
|
neuper@42023
|
24 |
for further input *}
|
neuper@42023
|
25 |
|
neuper@42023
|
26 |
ML {*
|
wneuper@59276
|
27 |
val ctxt = Ctree.get_ctxt pt p;
|
neuper@42023
|
28 |
val SOME known_x = parseNEW ctxt "x + y + z";
|
neuper@42023
|
29 |
val SOME unknown = parseNEW ctxt "a + b + c";
|
neuper@42103
|
30 |
if type_of known_x = HOLogic.realT andalso
|
neuper@42103
|
31 |
type_of unknown = TFree ("'a",["Groups.plus"])
|
neuper@42103
|
32 |
then () else error "All_Ctx: type constraints beginning specification of root-problem ";
|
neuper@42023
|
33 |
*}
|
neuper@42023
|
34 |
|
neuper@42023
|
35 |
ML {*
|
wneuper@59261
|
36 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
37 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
38 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
39 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
40 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
41 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
42 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
43 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
neuper@42023
|
44 |
*}
|
neuper@42023
|
45 |
|
neuper@42023
|
46 |
section {* start interpretation of method *}
|
neuper@42023
|
47 |
text {* preconditions are known at start of interpretation of (root-)method *}
|
neuper@42023
|
48 |
|
neuper@42023
|
49 |
ML {*
|
wneuper@59276
|
50 |
if terms2strs (Ctree.get_assumptions_ pt p) = ["precond_rootmet x"]
|
neuper@42103
|
51 |
then () else error "All_Ctx: asms after start interpretation of root-method";
|
neuper@42023
|
52 |
*}
|
neuper@42023
|
53 |
|
neuper@42023
|
54 |
ML {*
|
wneuper@59261
|
55 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
56 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
57 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
neuper@42023
|
58 |
*}
|
neuper@42023
|
59 |
|
neuper@42023
|
60 |
section {* start a subproblem: specification *}
|
neuper@42092
|
61 |
text {*
|
neuper@42092
|
62 |
ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args"
|
neuper@42092
|
63 |
and extended with the types of the variables in args. *}
|
neuper@42023
|
64 |
|
neuper@42092
|
65 |
ML {* (*not significant in this example*)
|
wneuper@59276
|
66 |
val ctxt = Ctree.get_ctxt pt p;
|
neuper@42023
|
67 |
val SOME known_x = parseNEW ctxt "x+y+z";
|
neuper@42023
|
68 |
val SOME unknown = parseNEW ctxt "a+b+c";
|
neuper@42103
|
69 |
if type_of known_x = HOLogic.realT andalso
|
neuper@42103
|
70 |
type_of unknown = TFree ("'a",["Groups.plus"])
|
neuper@42103
|
71 |
then () else error "All_Ctx: type constraints beginning specification of SubProblem ";
|
neuper@42023
|
72 |
*}
|
neuper@42023
|
73 |
|
neuper@42023
|
74 |
ML {*
|
wneuper@59261
|
75 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
76 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
77 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
78 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
79 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
80 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
81 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
82 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
neuper@42023
|
83 |
*}
|
neuper@42023
|
84 |
|
neuper@42023
|
85 |
section {* interpretation of subproblem's method *}
|
neuper@42023
|
86 |
|
neuper@42023
|
87 |
text {* preconds are known at start of interpretation of (sub-)method *}
|
neuper@42023
|
88 |
|
neuper@42023
|
89 |
ML {*
|
wneuper@59276
|
90 |
if terms2strs (Ctree.get_assumptions_ pt p) = ["matches (?a = ?b) (-1 + x = 0)"]
|
neuper@42103
|
91 |
then () else error "All_Ctx: asms after start interpretation of SubProblem";
|
neuper@42023
|
92 |
*}
|
neuper@42023
|
93 |
|
neuper@42023
|
94 |
ML {*
|
wneuper@59261
|
95 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
neuper@42023
|
96 |
*}
|
neuper@42023
|
97 |
|
neuper@42023
|
98 |
ML {*
|
neuper@42023
|
99 |
"artifically inject assumptions";
|
wneuper@59276
|
100 |
val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);
|
wneuper@59308
|
101 |
val ctxt = Stool.insert_assumptions [str2term "x < sub_asm_out",
|
neuper@42023
|
102 |
str2term "a < sub_asm_local"] cres;
|
wneuper@59275
|
103 |
val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
|
neuper@42023
|
104 |
*}
|
neuper@42023
|
105 |
|
neuper@42033
|
106 |
ML {*
|
wneuper@59261
|
107 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
108 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
neuper@42023
|
109 |
*}
|
neuper@42023
|
110 |
|
neuper@42023
|
111 |
section {* finish subproblem, return to calling method*}
|
neuper@42023
|
112 |
|
neuper@42023
|
113 |
text {* transfer non-local assumptions and result from sub-method to root-method.
|
neuper@42023
|
114 |
non-local assumptions are those contaning a variable known in root-method.
|
neuper@42023
|
115 |
*}
|
neuper@42023
|
116 |
|
neuper@42023
|
117 |
ML {*
|
wneuper@59275
|
118 |
if terms2strs (Ctree.get_assumptions_ pt p) =
|
neuper@42103
|
119 |
["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
|
neuper@42103
|
120 |
then () else error "All_Ctx: asms after finishing SubProblem";
|
neuper@42023
|
121 |
*}
|
neuper@42023
|
122 |
|
neuper@42023
|
123 |
ML {*
|
wneuper@59261
|
124 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
wneuper@59261
|
125 |
val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
|
neuper@42023
|
126 |
*}
|
neuper@42023
|
127 |
|
neuper@42023
|
128 |
section {* finish Lucas interpretation *}
|
neuper@42023
|
129 |
|
neuper@42023
|
130 |
text {* assumptions collected during lucas-interpretation for proof of postcondition *}
|
neuper@42023
|
131 |
|
neuper@42023
|
132 |
ML {*
|
wneuper@59276
|
133 |
if terms2strs (Ctree.get_assumptions_ pt p) =
|
neuper@42103
|
134 |
["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
|
neuper@42103
|
135 |
then () else error "All_Ctx at final result";
|
neuper@42023
|
136 |
*}
|
neuper@42023
|
137 |
|
e0726734@42032
|
138 |
ML {*
|
wneuper@59265
|
139 |
Chead.show_pt pt;
|
e0726734@42032
|
140 |
*}
|
e0726734@42032
|
141 |
|
neuper@42023
|
142 |
end |