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.
|
wenzelm@60217
|
6 |
So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minimsubpbl/* *)
|
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>
|
wneuper@59472
|
26 |
text \<open>variables known from formalisation provide type-inference
|
wneuper@59472
|
27 |
for further input\<close>
|
neuper@42023
|
28 |
|
wneuper@59472
|
29 |
ML \<open>
|
wneuper@59276
|
30 |
val ctxt = Ctree.get_ctxt pt p;
|
wneuper@59395
|
31 |
val SOME known_x = TermC.parseNEW ctxt "x + y + z";
|
wneuper@59395
|
32 |
val SOME unknown = TermC.parseNEW ctxt "a + b + c";
|
neuper@42103
|
33 |
if type_of known_x = HOLogic.realT andalso
|
neuper@42103
|
34 |
type_of unknown = TFree ("'a",["Groups.plus"])
|
neuper@42103
|
35 |
then () else error "All_Ctx: type constraints beginning specification of root-problem ";
|
wneuper@59472
|
36 |
\<close>
|
neuper@42023
|
37 |
|
wneuper@59472
|
38 |
ML \<open>
|
walther@59814
|
39 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
40 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
41 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
42 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
43 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
44 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
45 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
46 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
47 |
\<close>
|
neuper@42023
|
48 |
|
wneuper@59472
|
49 |
section \<open>start interpretation of method\<close>
|
wneuper@59472
|
50 |
text \<open>preconditions are known at start of interpretation of (root-)method\<close>
|
neuper@42023
|
51 |
|
wneuper@59472
|
52 |
ML \<open>
|
walther@59868
|
53 |
if UnparseC.terms_to_strings (Ctree.get_assumptions pt p) = ["precond_rootmet x"]
|
neuper@42103
|
54 |
then () else error "All_Ctx: asms after start interpretation of root-method";
|
wneuper@59472
|
55 |
\<close>
|
neuper@42023
|
56 |
|
wneuper@59472
|
57 |
ML \<open>
|
walther@59814
|
58 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
59 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
60 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
61 |
\<close>
|
neuper@42023
|
62 |
|
wneuper@59472
|
63 |
section \<open>start a subproblem: specification\<close>
|
wneuper@59472
|
64 |
text \<open>
|
neuper@42092
|
65 |
ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args"
|
wneuper@59472
|
66 |
and extended with the types of the variables in args.\<close>
|
neuper@42023
|
67 |
|
wneuper@59472
|
68 |
ML \<open>(*not significant in this example*)
|
wneuper@59276
|
69 |
val ctxt = Ctree.get_ctxt pt p;
|
wneuper@59395
|
70 |
val SOME known_x = TermC.parseNEW ctxt "x+y+z";
|
wneuper@59395
|
71 |
val SOME unknown = TermC.parseNEW ctxt "a+b+c";
|
neuper@42103
|
72 |
if type_of known_x = HOLogic.realT andalso
|
neuper@42103
|
73 |
type_of unknown = TFree ("'a",["Groups.plus"])
|
neuper@42103
|
74 |
then () else error "All_Ctx: type constraints beginning specification of SubProblem ";
|
wneuper@59472
|
75 |
\<close>
|
neuper@42023
|
76 |
|
wneuper@59472
|
77 |
ML \<open>
|
walther@59814
|
78 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
79 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
80 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
81 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
82 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
83 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
84 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
85 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
86 |
\<close>
|
neuper@42023
|
87 |
|
wneuper@59472
|
88 |
section \<open>interpretation of subproblem's method\<close>
|
neuper@42023
|
89 |
|
wneuper@59472
|
90 |
text \<open>preconds are known at start of interpretation of (sub-)method\<close>
|
neuper@42023
|
91 |
|
wneuper@59472
|
92 |
ML \<open>
|
wneuper@59472
|
93 |
\<close> ML \<open>
|
wneuper@59472
|
94 |
\<close>
|
wneuper@59410
|
95 |
|
wneuper@59472
|
96 |
ML \<open>
|
walther@59868
|
97 |
if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),
|
walther@60329
|
98 |
["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"])
|
neuper@42103
|
99 |
then () else error "All_Ctx: asms after start interpretation of SubProblem";
|
wneuper@59472
|
100 |
\<close>
|
neuper@42023
|
101 |
|
wneuper@59472
|
102 |
ML \<open>
|
walther@59814
|
103 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
104 |
\<close>
|
neuper@42023
|
105 |
|
wneuper@59472
|
106 |
ML \<open>
|
neuper@42023
|
107 |
"artifically inject assumptions";
|
wneuper@59276
|
108 |
val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);
|
wneuper@59577
|
109 |
val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out",
|
wneuper@59395
|
110 |
TermC.str2term "a < sub_asm_local"] cres;
|
wneuper@59275
|
111 |
val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
|
wneuper@59472
|
112 |
\<close>
|
neuper@42023
|
113 |
|
wneuper@59472
|
114 |
ML \<open>
|
walther@59814
|
115 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
116 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
117 |
\<close>
|
neuper@42023
|
118 |
|
wneuper@59472
|
119 |
section \<open>finish subproblem, return to calling method\<close>
|
neuper@42023
|
120 |
|
wneuper@59472
|
121 |
text \<open>transfer non-local assumptions and result from sub-method to root-method.
|
neuper@42023
|
122 |
non-local assumptions are those contaning a variable known in root-method.
|
wneuper@59472
|
123 |
\<close>
|
neuper@42023
|
124 |
|
wneuper@59472
|
125 |
ML \<open>
|
walther@59832
|
126 |
eq_set
|
wneuper@59472
|
127 |
\<close>
|
wneuper@59411
|
128 |
|
wneuper@59472
|
129 |
ML \<open>
|
walther@59868
|
130 |
if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),
|
walther@60329
|
131 |
["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])
|
neuper@42103
|
132 |
then () else error "All_Ctx: asms after finishing SubProblem";
|
wneuper@59472
|
133 |
\<close>
|
neuper@42023
|
134 |
|
wneuper@59472
|
135 |
ML \<open>
|
walther@59814
|
136 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
walther@59814
|
137 |
val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;
|
wneuper@59472
|
138 |
\<close>
|
neuper@42023
|
139 |
|
wneuper@59472
|
140 |
section \<open>finish Lucas interpretation\<close>
|
neuper@42023
|
141 |
|
wneuper@59472
|
142 |
text \<open>assumptions collected during lucas-interpretation for proof of postcondition\<close>
|
neuper@42023
|
143 |
|
wneuper@59472
|
144 |
ML \<open>
|
wneuper@59472
|
145 |
\<close> ML \<open>
|
wneuper@59472
|
146 |
\<close>
|
wneuper@59411
|
147 |
|
wneuper@59472
|
148 |
ML \<open>
|
walther@59868
|
149 |
if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),
|
walther@60329
|
150 |
["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])
|
neuper@42103
|
151 |
then () else error "All_Ctx at final result";
|
wneuper@59472
|
152 |
\<close>
|
neuper@42023
|
153 |
|
wneuper@59472
|
154 |
ML \<open>
|
walther@59983
|
155 |
Test_Tool.show_pt pt;
|
wneuper@59472
|
156 |
\<close>
|
e0726734@42032
|
157 |
|
wneuper@59472
|
158 |
ML \<open>
|
wneuper@59472
|
159 |
\<close> ML \<open>
|
wneuper@59472
|
160 |
\<close>
|
wneuper@59410
|
161 |
|
neuper@42023
|
162 |
end |