wneuper@59582
|
1 |
(* Title: "ADDTESTS/All_Ctxt.thy"
|
wneuper@59582
|
2 |
Author: Walther Neuper
|
wneuper@59582
|
3 |
(c) due to copyright terms
|
wneuper@59582
|
4 |
|
wneuper@59582
|
5 |
this theory is evaluated BEFORE Test_Isac.thy opens structures.
|
Walther@60558
|
6 |
So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/* *)
|
e0726734@42026
|
7 |
|
walther@59814
|
8 |
theory All_Ctxt imports Isac.Build_Isac
|
neuper@48884
|
9 |
begin
|
neuper@42023
|
10 |
|
wneuper@59472
|
11 |
text \<open>all changes of context are demonstrated in a mini example.
|
wneuper@59472
|
12 |
see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 ---\<close>
|
neuper@42023
|
13 |
|
wneuper@59472
|
14 |
section \<open>start of the mini example\<close>
|
neuper@42023
|
15 |
|
wneuper@59472
|
16 |
ML \<open>
|
neuper@42033
|
17 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
neuper@42023
|
18 |
val (dI',pI',mI') =
|
walther@59997
|
19 |
("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
20 |
["Test", "squ-equ-test-subpbl1"]);
|
wneuper@59592
|
21 |
\<close> ML \<open>
|
walther@59814
|
22 |
val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
wneuper@59472
|
23 |
\<close>
|
neuper@42023
|
24 |
|
wneuper@59472
|
25 |
section \<open>start of specify phase\<close>
|
Walther@60422
|
26 |
text \<open>
|
Walther@60422
|
27 |
variables known from formalisation provide type-inference for further input
|
Walther@60422
|
28 |
\<close>
|
neuper@42023
|
29 |
|
wneuper@59472
|
30 |
ML \<open>
|
Walther@60422
|
31 |
(*+*)if ((fst p) |> get_obj g_origin pt |> LibraryC.fst3) <> []
|
Walther@60422
|
32 |
(*+*)then () else error "check correct of get_ctxt at start of (sub-)problem";
|
Walther@60422
|
33 |
|
Walther@60422
|
34 |
val ctxt = Ctree.get_ctxt pt p;
|
Walther@60422
|
35 |
(*must NOT check ThyC.id_empty in specify_data.spec, .. is still empty in this case
|
Walther@60422
|
36 |
but for References_Def.T in specify_data.origin. .. is already assigned in this case
|
Walther@60422
|
37 |
and in case of CAS-cmd *)
|
wneuper@59395
|
38 |
val SOME known_x = TermC.parseNEW ctxt "x + y + z";
|
wneuper@59395
|
39 |
val SOME unknown = TermC.parseNEW ctxt "a + b + c";
|
neuper@42103
|
40 |
if type_of known_x = HOLogic.realT andalso
|
neuper@42103
|
41 |
type_of unknown = TFree ("'a",["Groups.plus"])
|
neuper@42103
|
42 |
then () else error "All_Ctx: type constraints beginning specification of root-problem ";
|
wneuper@59472
|
43 |
\<close>
|
neuper@42023
|
44 |
|
wneuper@59472
|
45 |
ML \<open>
|
walther@59814
|
46 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
47 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
48 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
49 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
50 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
51 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
52 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
53 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
54 |
\<close>
|
neuper@42023
|
55 |
|
wneuper@59472
|
56 |
section \<open>start interpretation of method\<close>
|
wneuper@59472
|
57 |
text \<open>preconditions are known at start of interpretation of (root-)method\<close>
|
neuper@42023
|
58 |
|
wneuper@59472
|
59 |
ML \<open>
|
walther@59868
|
60 |
if UnparseC.terms_to_strings (Ctree.get_assumptions pt p) = ["precond_rootmet x"]
|
neuper@42103
|
61 |
then () else error "All_Ctx: asms after start interpretation of root-method";
|
wneuper@59472
|
62 |
\<close>
|
neuper@42023
|
63 |
|
wneuper@59472
|
64 |
ML \<open>
|
walther@59814
|
65 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
66 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
67 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
68 |
\<close>
|
neuper@42023
|
69 |
|
wneuper@59472
|
70 |
section \<open>start a subproblem: specification\<close>
|
wneuper@59472
|
71 |
text \<open>
|
neuper@42092
|
72 |
ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args"
|
wneuper@59472
|
73 |
and extended with the types of the variables in args.\<close>
|
neuper@42023
|
74 |
|
wneuper@59472
|
75 |
ML \<open>(*not significant in this example*)
|
wneuper@59276
|
76 |
val ctxt = Ctree.get_ctxt pt p;
|
wneuper@59395
|
77 |
val SOME known_x = TermC.parseNEW ctxt "x+y+z";
|
wneuper@59395
|
78 |
val SOME unknown = TermC.parseNEW ctxt "a+b+c";
|
neuper@42103
|
79 |
if type_of known_x = HOLogic.realT andalso
|
neuper@42103
|
80 |
type_of unknown = TFree ("'a",["Groups.plus"])
|
neuper@42103
|
81 |
then () else error "All_Ctx: type constraints beginning specification of SubProblem ";
|
wneuper@59472
|
82 |
\<close>
|
neuper@42023
|
83 |
|
wneuper@59472
|
84 |
ML \<open>
|
walther@59814
|
85 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
86 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
87 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
88 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
89 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
90 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
91 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
92 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
93 |
\<close>
|
neuper@42023
|
94 |
|
wneuper@59472
|
95 |
section \<open>interpretation of subproblem's method\<close>
|
neuper@42023
|
96 |
|
wneuper@59472
|
97 |
text \<open>preconds are known at start of interpretation of (sub-)method\<close>
|
neuper@42023
|
98 |
|
wneuper@59472
|
99 |
ML \<open>
|
wneuper@59472
|
100 |
\<close> ML \<open>
|
Walther@60558
|
101 |
UnparseC.terms_to_strings (Ctree.get_assumptions pt p);
|
Walther@60558
|
102 |
(*"precond_rootmet (x::real)" -- fix in Model_Pattern? *)
|
Walther@60558
|
103 |
\<close> ML \<open>
|
wneuper@59472
|
104 |
\<close>
|
wneuper@59410
|
105 |
|
wneuper@59472
|
106 |
ML \<open>
|
walther@59868
|
107 |
if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),
|
walther@60329
|
108 |
["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"])
|
neuper@42103
|
109 |
then () else error "All_Ctx: asms after start interpretation of SubProblem";
|
wneuper@59472
|
110 |
\<close>
|
neuper@42023
|
111 |
|
wneuper@59472
|
112 |
ML \<open>
|
walther@59814
|
113 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
114 |
\<close>
|
neuper@42023
|
115 |
|
wneuper@59472
|
116 |
ML \<open>
|
neuper@42023
|
117 |
"artifically inject assumptions";
|
wneuper@59276
|
118 |
val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);
|
Walther@60565
|
119 |
val ctxt = ContextC.insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out",
|
Walther@60565
|
120 |
TermC.parse_test @{context} "a < sub_asm_local"] cres;
|
wneuper@59275
|
121 |
val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
|
wneuper@59472
|
122 |
\<close>
|
neuper@42023
|
123 |
|
wneuper@59472
|
124 |
ML \<open>
|
walther@59814
|
125 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
126 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
127 |
\<close>
|
neuper@42023
|
128 |
|
wneuper@59472
|
129 |
section \<open>finish subproblem, return to calling method\<close>
|
neuper@42023
|
130 |
|
wneuper@59472
|
131 |
text \<open>transfer non-local assumptions and result from sub-method to root-method.
|
neuper@42023
|
132 |
non-local assumptions are those contaning a variable known in root-method.
|
wneuper@59472
|
133 |
\<close>
|
neuper@42023
|
134 |
|
wneuper@59472
|
135 |
ML \<open>
|
walther@59832
|
136 |
eq_set
|
wneuper@59472
|
137 |
\<close>
|
wneuper@59411
|
138 |
|
wneuper@59472
|
139 |
ML \<open>
|
walther@59868
|
140 |
if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),
|
walther@60329
|
141 |
["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])
|
neuper@42103
|
142 |
then () else error "All_Ctx: asms after finishing SubProblem";
|
wneuper@59472
|
143 |
\<close>
|
neuper@42023
|
144 |
|
wneuper@59472
|
145 |
ML \<open>
|
walther@59814
|
146 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
147 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
148 |
\<close>
|
neuper@42023
|
149 |
|
wneuper@59472
|
150 |
section \<open>finish Lucas interpretation\<close>
|
neuper@42023
|
151 |
|
wneuper@59472
|
152 |
text \<open>assumptions collected during lucas-interpretation for proof of postcondition\<close>
|
neuper@42023
|
153 |
|
wneuper@59472
|
154 |
ML \<open>
|
wneuper@59472
|
155 |
\<close> ML \<open>
|
wneuper@59472
|
156 |
\<close>
|
wneuper@59411
|
157 |
|
wneuper@59472
|
158 |
ML \<open>
|
walther@59868
|
159 |
if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),
|
walther@60329
|
160 |
["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])
|
neuper@42103
|
161 |
then () else error "All_Ctx at final result";
|
wneuper@59472
|
162 |
\<close>
|
neuper@42023
|
163 |
|
wneuper@59472
|
164 |
ML \<open>
|
walther@59983
|
165 |
Test_Tool.show_pt pt;
|
wneuper@59472
|
166 |
\<close>
|
e0726734@42032
|
167 |
|
wneuper@59472
|
168 |
ML \<open>
|
wneuper@59472
|
169 |
\<close> ML \<open>
|
wneuper@59472
|
170 |
\<close>
|
wneuper@59410
|
171 |
|
Walther@60422
|
172 |
end
|