wneuper@59571
|
1 |
(* Title: Tactics; tac_ for interaction with frontend, input for internal use.
|
wneuper@59304
|
2 |
Author: Walther Neuper 170121
|
wneuper@59304
|
3 |
(c) due to copyright terms
|
wneuper@59304
|
4 |
|
wneuper@59304
|
5 |
regular expression for search:
|
wneuper@59304
|
6 |
|
walther@59812
|
7 |
Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
|
wneuper@59304
|
8 |
|
wneuper@59304
|
9 |
*)
|
wneuper@59298
|
10 |
signature TACTIC =
|
wneuper@59298
|
11 |
sig
|
walther@59846
|
12 |
datatype T =
|
walther@59865
|
13 |
Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
|
walther@59865
|
14 |
| Add_Relation' of TermC.as_string * Model.itm list
|
walther@59903
|
15 |
| Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
|
walther@59846
|
16 |
|
walther@59846
|
17 |
| Begin_Sequ' | Begin_Trans' of term
|
walther@59846
|
18 |
| Split_And' of term | Split_Or' of term | Split_Intersect' of term
|
walther@59846
|
19 |
| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
|
walther@59846
|
20 |
| End_Sequ' | End_Trans' of Selem.result
|
walther@59846
|
21 |
| End_Ruleset' of term | End_Intersect' of term | End_Proof''
|
walther@59846
|
22 |
|
walther@59846
|
23 |
| CAScmd' of term
|
walther@59879
|
24 |
| Calculate' of ThyC.id * string * term * (term * ThmC.T)
|
walther@59903
|
25 |
| Check_Postcond' of Problem.id * term
|
walther@59865
|
26 |
| Check_elementwise' of term * TermC.as_string * Selem.result
|
walther@59865
|
27 |
| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
|
walther@59846
|
28 |
|
walther@59851
|
29 |
| Derive' of Rule_Set.T
|
walther@59879
|
30 |
| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
|
walther@59910
|
31 |
| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
|
walther@59846
|
32 |
| End_Detail' of Selem.result
|
walther@59846
|
33 |
|
walther@59846
|
34 |
| Empty_Tac_
|
walther@59846
|
35 |
| Free_Solve'
|
walther@59846
|
36 |
|
walther@59903
|
37 |
| Init_Proof' of TermC.as_string list * Spec.T
|
walther@59903
|
38 |
| Model_Problem' of Problem.id * Model.itm list * Model.itm list
|
walther@59846
|
39 |
| Or_to_List' of term * term
|
walther@59903
|
40 |
| Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
|
walther@59903
|
41 |
| Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
|
walther@59846
|
42 |
|
walther@59879
|
43 |
| Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
|
walther@59910
|
44 |
| Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
|
walther@59879
|
45 |
| Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
|
walther@59910
|
46 |
| Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
|
walther@59846
|
47 |
|
walther@59903
|
48 |
| Specify_Method' of Method.id * Model.ori list * Model.itm list
|
walther@59903
|
49 |
| Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
|
walther@59879
|
50 |
| Specify_Theory' of ThyC.id
|
walther@59846
|
51 |
| Subproblem' of
|
walther@59903
|
52 |
Spec.T * Model.ori list *
|
walther@59846
|
53 |
term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
|
walther@59846
|
54 |
Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
|
walther@59846
|
55 |
(*Istate.T * ? *)
|
walther@59846
|
56 |
Proof.context * (* derived from prog. in ??? *)
|
walther@59846
|
57 |
term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
|
walther@59912
|
58 |
| Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
|
walther@59846
|
59 |
| Tac_ of theory * string * string * string
|
walther@59846
|
60 |
| Take' of term
|
walther@59812
|
61 |
val string_of: T -> string
|
walther@59741
|
62 |
|
walther@59846
|
63 |
datatype input =
|
walther@59865
|
64 |
Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
|
walther@59865
|
65 |
| Apply_Assumption of TermC.as_string list
|
walther@59903
|
66 |
| Apply_Method of Method.id
|
walther@59846
|
67 |
(*/--- TODO: re-design ? -----------------------------------------------------------------\*)
|
walther@59846
|
68 |
| Begin_Sequ | Begin_Trans
|
walther@59846
|
69 |
| Split_And | Split_Or | Split_Intersect
|
walther@59846
|
70 |
| Conclude_And | Conclude_Or | Collect_Trues
|
walther@59846
|
71 |
| End_Sequ | End_Trans
|
walther@59846
|
72 |
| End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
|
walther@59846
|
73 |
(*\--- TODO: re-design ? -----------------------------------------------------------------/*)
|
walther@59865
|
74 |
| CAScmd of TermC.as_string
|
walther@59846
|
75 |
| Calculate of string
|
walther@59903
|
76 |
| Check_Postcond of Problem.id
|
walther@59865
|
77 |
| Check_elementwise of TermC.as_string
|
walther@59865
|
78 |
| Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
|
walther@59846
|
79 |
|
walther@59867
|
80 |
| Derive of Rule_Set.id
|
walther@59867
|
81 |
| Detail_Set of Rule_Set.id
|
walther@59911
|
82 |
| Detail_Set_Inst of Subst.input * Rule_Set.id
|
walther@59846
|
83 |
| End_Detail
|
walther@59846
|
84 |
|
walther@59846
|
85 |
| Empty_Tac
|
walther@59846
|
86 |
| Free_Solve
|
walther@59846
|
87 |
|
walther@59903
|
88 |
| Init_Proof of TermC.as_string list * Spec.T
|
walther@59846
|
89 |
| Model_Problem
|
walther@59846
|
90 |
| Or_to_List
|
walther@59903
|
91 |
| Refine_Problem of Problem.id
|
walther@59903
|
92 |
| Refine_Tacitly of Problem.id
|
walther@59846
|
93 |
|
walther@59874
|
94 |
| Rewrite of ThmC.T
|
walther@59911
|
95 |
| Rewrite_Inst of Subst.input * ThmC.T
|
walther@59867
|
96 |
| Rewrite_Set of Rule_Set.id
|
walther@59911
|
97 |
| Rewrite_Set_Inst of Subst.input * Rule_Set.id
|
walther@59846
|
98 |
|
walther@59903
|
99 |
| Specify_Method of Method.id
|
walther@59903
|
100 |
| Specify_Problem of Problem.id
|
walther@59879
|
101 |
| Specify_Theory of ThyC.id
|
walther@59903
|
102 |
| Subproblem of ThyC.id * Problem.id
|
walther@59846
|
103 |
|
walther@59912
|
104 |
| Substitute of Subst.input
|
walther@59846
|
105 |
| Tac of string
|
walther@59865
|
106 |
| Take of TermC.as_string | Take_Inst of TermC.as_string
|
walther@59846
|
107 |
val input_to_string : input -> string
|
walther@59812
|
108 |
val tac2IDstr : input -> string
|
walther@59844
|
109 |
val is_empty : input -> bool
|
wneuper@59302
|
110 |
|
walther@59728
|
111 |
val eq_tac : input * input -> bool
|
walther@59728
|
112 |
val is_rewtac : input -> bool
|
walther@59728
|
113 |
val is_rewset : input -> bool
|
walther@59867
|
114 |
val rls_of : input -> Rule_Set.id
|
walther@59728
|
115 |
val rule2tac : theory -> (term * term) list -> Rule.rule -> input
|
walther@59914
|
116 |
val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
|
walther@59914
|
117 |
val for_specify: input -> bool
|
walther@59914
|
118 |
|
walther@59704
|
119 |
val input_from_T : T -> input
|
walther@59728
|
120 |
val result : T -> term
|
walther@59728
|
121 |
val creates_assms: T -> term list
|
walther@59728
|
122 |
val insert_assumptions: T -> Proof.context -> Proof.context
|
walther@59749
|
123 |
val for_specify': T -> bool
|
walther@59735
|
124 |
|
wneuper@59310
|
125 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59310
|
126 |
(* NONE *)
|
walther@59886
|
127 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59310
|
128 |
(* NONE *)
|
walther@59886
|
129 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59298
|
130 |
|
wneuper@59310
|
131 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59310
|
132 |
(* NONE *)
|
wneuper@59298
|
133 |
end
|
wneuper@59298
|
134 |
|
walther@59728
|
135 |
(**)
|
wneuper@59571
|
136 |
structure Tactic(**): TACTIC(**) =
|
wneuper@59298
|
137 |
struct
|
walther@59728
|
138 |
(**)
|
wneuper@59298
|
139 |
|
walther@59914
|
140 |
(** tactics for user at front-end **)
|
walther@59914
|
141 |
|
walther@59846
|
142 |
(* tactics for user at front-end.
|
walther@59846
|
143 |
input propagates the construction of the calc-tree;
|
walther@59846
|
144 |
there are
|
walther@59846
|
145 |
(a) 'specsteps' for the specify-phase, and others for the solve-phase
|
walther@59846
|
146 |
(b) those of the solve-phase are 'initac's and others;
|
walther@59846
|
147 |
initacs start with a formula different from the preceding formula.
|
walther@59846
|
148 |
see 'type tac_' for the internal representation of tactics
|
walther@59846
|
149 |
*)
|
walther@59846
|
150 |
datatype input =
|
walther@59865
|
151 |
Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
|
walther@59865
|
152 |
| Apply_Assumption of TermC.as_string list
|
walther@59903
|
153 |
| Apply_Method of Method.id
|
walther@59846
|
154 |
(* creates an "istate" in PblObj.env; in case of "implicit_take"
|
walther@59846
|
155 |
creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
|
walther@59846
|
156 |
a "SOME istate" at fst of "loc".
|
walther@59846
|
157 |
As each step (in the solve-phase) has a resulting formula (at the front-end)
|
walther@59846
|
158 |
Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
|
walther@59846
|
159 |
(*/--- TODO: re-design ? -----------------------------------------------------------------\*)
|
walther@59846
|
160 |
| Begin_Sequ | Begin_Trans
|
walther@59846
|
161 |
| Split_And | Split_Or | Split_Intersect
|
walther@59846
|
162 |
| Conclude_And | Conclude_Or | Collect_Trues
|
walther@59846
|
163 |
| End_Sequ | End_Trans
|
walther@59846
|
164 |
| End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
|
walther@59846
|
165 |
(*\--- TODO: re-design ? -----------------------------------------------------------------/*)
|
walther@59865
|
166 |
| CAScmd of TermC.as_string
|
walther@59846
|
167 |
| Calculate of string
|
walther@59903
|
168 |
| Check_Postcond of Problem.id
|
walther@59865
|
169 |
| Check_elementwise of TermC.as_string
|
walther@59865
|
170 |
| Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
|
wneuper@59302
|
171 |
|
walther@59867
|
172 |
| Derive of Rule_Set.id (* WN0509 drop *)
|
walther@59867
|
173 |
| Detail_Set of Rule_Set.id (* WN0509 drop *)
|
walther@59911
|
174 |
| Detail_Set_Inst of Subst.input * Rule_Set.id (* WN0509 drop *)
|
walther@59846
|
175 |
| End_Detail (* WN0509 drop *)
|
walther@59846
|
176 |
|
walther@59846
|
177 |
| Empty_Tac
|
walther@59846
|
178 |
| Free_Solve
|
walther@59846
|
179 |
|
walther@59903
|
180 |
| Init_Proof of TermC.as_string list * Spec.T
|
walther@59846
|
181 |
| Model_Problem
|
walther@59846
|
182 |
| Or_to_List
|
walther@59903
|
183 |
| Refine_Problem of Problem.id
|
walther@59903
|
184 |
| Refine_Tacitly of Problem.id
|
walther@59846
|
185 |
|
walther@59846
|
186 |
(* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
|
walther@59846
|
187 |
because there all the thms are present with both (thmID, thm)
|
walther@59846
|
188 |
(where user-views can show both or only one of (thmID, thm)),
|
walther@59846
|
189 |
and thm is created from ThmID by assoc_thm'' when entering isabisac *)
|
walther@59874
|
190 |
| Rewrite of ThmC.T
|
walther@59911
|
191 |
| Rewrite_Inst of Subst.input * ThmC.T
|
walther@59867
|
192 |
| Rewrite_Set of Rule_Set.id
|
walther@59911
|
193 |
| Rewrite_Set_Inst of Subst.input * Rule_Set.id
|
walther@59846
|
194 |
|
walther@59903
|
195 |
| Specify_Method of Method.id
|
walther@59903
|
196 |
| Specify_Problem of Problem.id
|
walther@59879
|
197 |
| Specify_Theory of ThyC.id
|
walther@59903
|
198 |
| Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
|
walther@59846
|
199 |
|
walther@59912
|
200 |
| Substitute of Subst.input
|
walther@59846
|
201 |
| Tac of string (* WN0509 drop *)
|
walther@59865
|
202 |
| Take of TermC.as_string | Take_Inst of TermC.as_string
|
walther@59846
|
203 |
|
walther@59846
|
204 |
fun input_to_string ma = case ma of
|
walther@59846
|
205 |
Init_Proof (ppc, spec) =>
|
walther@59902
|
206 |
"Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
|
walther@59846
|
207 |
| Model_Problem => "Model_Problem "
|
walther@59846
|
208 |
| Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
|
walther@59846
|
209 |
| Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
|
walther@59846
|
210 |
| Add_Given cterm' => "Add_Given " ^ cterm'
|
walther@59846
|
211 |
| Del_Given cterm' => "Del_Given " ^ cterm'
|
walther@59846
|
212 |
| Add_Find cterm' => "Add_Find " ^ cterm'
|
walther@59846
|
213 |
| Del_Find cterm' => "Del_Find " ^ cterm'
|
walther@59846
|
214 |
| Add_Relation cterm' => "Add_Relation " ^ cterm'
|
walther@59846
|
215 |
| Del_Relation cterm' => "Del_Relation " ^ cterm'
|
walther@59846
|
216 |
|
walther@59846
|
217 |
| Specify_Theory domID => "Specify_Theory " ^ quote domID
|
walther@59846
|
218 |
| Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
|
walther@59846
|
219 |
| Specify_Method metID => "Specify_Method " ^ strs2str metID
|
walther@59846
|
220 |
| Apply_Method metID => "Apply_Method " ^ strs2str metID
|
walther@59846
|
221 |
| Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
|
walther@59846
|
222 |
| Free_Solve => "Free_Solve"
|
walther@59846
|
223 |
|
walther@59846
|
224 |
| Rewrite_Inst (subs, (id, thm)) =>
|
walther@59868
|
225 |
"Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term)))
|
walther@59868
|
226 |
| Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term)
|
walther@59846
|
227 |
| Rewrite_Set_Inst (subs, rls) =>
|
walther@59846
|
228 |
"Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
|
walther@59846
|
229 |
| Rewrite_Set rls => "Rewrite_Set " ^ quote rls
|
walther@59846
|
230 |
| Detail_Set rls => "Detail_Set " ^ quote rls
|
walther@59846
|
231 |
| Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
|
walther@59846
|
232 |
| End_Detail => "End_Detail"
|
walther@59846
|
233 |
| Derive rls' => "Derive " ^ rls'
|
walther@59911
|
234 |
| Calculate op_ => "Calculate " ^ op_
|
walther@59912
|
235 |
| Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
|
walther@59846
|
236 |
| Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
|
walther@59846
|
237 |
|
walther@59846
|
238 |
| Take cterm' => "Take " ^ quote cterm'
|
walther@59846
|
239 |
| Take_Inst cterm' => "Take_Inst " ^ quote cterm'
|
walther@59846
|
240 |
| Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
|
walther@59846
|
241 |
| End_Subproblem => "End_Subproblem"
|
walther@59846
|
242 |
| CAScmd cterm' => "CAScmd " ^ quote cterm'
|
walther@59846
|
243 |
|
walther@59846
|
244 |
| Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
|
walther@59846
|
245 |
| Or_to_List => "Or_to_List "
|
walther@59846
|
246 |
| Collect_Trues => "Collect_Trues"
|
walther@59846
|
247 |
|
walther@59846
|
248 |
| Empty_Tac => "Empty_Tac"
|
walther@59846
|
249 |
| Tac string => "Tac " ^ string
|
walther@59846
|
250 |
| End_Proof' => "input End_Proof'"
|
walther@59846
|
251 |
| _ => "input_to_string not impl. for ?!";
|
walther@59846
|
252 |
|
walther@59846
|
253 |
fun tac2IDstr ma = case ma of
|
walther@59846
|
254 |
Model_Problem => "Model_Problem"
|
walther@59846
|
255 |
| Refine_Tacitly _ => "Refine_Tacitly"
|
walther@59846
|
256 |
| Refine_Problem _ => "Refine_Problem"
|
walther@59846
|
257 |
| Add_Given _ => "Add_Given"
|
walther@59846
|
258 |
| Del_Given _ => "Del_Given"
|
walther@59846
|
259 |
| Add_Find _ => "Add_Find"
|
walther@59846
|
260 |
| Del_Find _ => "Del_Find"
|
walther@59846
|
261 |
| Add_Relation _ => "Add_Relation"
|
walther@59846
|
262 |
| Del_Relation _ => "Del_Relation"
|
walther@59846
|
263 |
|
walther@59846
|
264 |
| Specify_Theory _ => "Specify_Theory"
|
walther@59846
|
265 |
| Specify_Problem _ => "Specify_Problem"
|
walther@59846
|
266 |
| Specify_Method _ => "Specify_Method"
|
walther@59846
|
267 |
| Apply_Method _ => "Apply_Method"
|
walther@59846
|
268 |
| Check_Postcond _ => "Check_Postcond"
|
walther@59846
|
269 |
| Free_Solve => "Free_Solve"
|
walther@59846
|
270 |
|
walther@59846
|
271 |
| Rewrite_Inst _ => "Rewrite_Inst"
|
walther@59846
|
272 |
| Rewrite _ => "Rewrite"
|
walther@59846
|
273 |
| Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
|
walther@59846
|
274 |
| Rewrite_Set _ => "Rewrite_Set"
|
walther@59846
|
275 |
| Detail_Set _ => "Detail_Set"
|
walther@59846
|
276 |
| Detail_Set_Inst _ => "Detail_Set_Inst"
|
walther@59846
|
277 |
| Derive _ => "Derive "
|
walther@59846
|
278 |
| Calculate _ => "Calculate "
|
walther@59846
|
279 |
| Substitute _ => "Substitute"
|
walther@59846
|
280 |
| Apply_Assumption _ => "Apply_Assumption"
|
walther@59846
|
281 |
|
walther@59846
|
282 |
| Take _ => "Take"
|
walther@59846
|
283 |
| Take_Inst _ => "Take_Inst"
|
walther@59846
|
284 |
| Subproblem _ => "Subproblem"
|
walther@59846
|
285 |
| End_Subproblem => "End_Subproblem"
|
walther@59846
|
286 |
| CAScmd _ => "CAScmd"
|
walther@59846
|
287 |
|
walther@59846
|
288 |
| Check_elementwise _ => "Check_elementwise"
|
walther@59846
|
289 |
| Or_to_List => "Or_to_List "
|
walther@59846
|
290 |
| Collect_Trues => "Collect_Trues"
|
walther@59846
|
291 |
|
walther@59846
|
292 |
| Empty_Tac => "Empty_Tac"
|
walther@59846
|
293 |
| Tac _ => "Tac "
|
walther@59846
|
294 |
| End_Proof' => "End_Proof'"
|
walther@59846
|
295 |
| _ => "input_to_string not impl. for ?!";
|
walther@59846
|
296 |
|
walther@59846
|
297 |
fun is_empty input = case input of Empty_Tac => true | _ => false
|
wneuper@59302
|
298 |
|
wneuper@59302
|
299 |
fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
|
wneuper@59302
|
300 |
| eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
|
wneuper@59302
|
301 |
| eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
|
wneuper@59302
|
302 |
| eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
|
wneuper@59302
|
303 |
| eq_tac (Calculate id1, Calculate id2) = id1 = id2
|
wneuper@59302
|
304 |
| eq_tac _ = false
|
wneuper@59302
|
305 |
|
wneuper@59302
|
306 |
fun is_rewset (Rewrite_Set_Inst _) = true
|
wneuper@59302
|
307 |
| is_rewset (Rewrite_Set _) = true
|
wneuper@59302
|
308 |
| is_rewset _ = false;
|
wneuper@59302
|
309 |
fun is_rewtac (Rewrite _) = true
|
wneuper@59302
|
310 |
| is_rewtac (Rewrite_Inst _) = true
|
wneuper@59571
|
311 |
| is_rewtac input = is_rewset input;
|
wneuper@59302
|
312 |
|
wneuper@59302
|
313 |
|
wneuper@59302
|
314 |
fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
|
wneuper@59302
|
315 |
| rls_of (Rewrite_Set rls) = rls
|
walther@59846
|
316 |
| rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
|
wneuper@59302
|
317 |
|
walther@59878
|
318 |
fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
|
wneuper@59416
|
319 |
| rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
|
wneuper@59416
|
320 |
| rule2tac _ subst (Rule.Thm thm'') =
|
walther@59911
|
321 |
Rewrite_Inst (Subst.T_to_input subst, thm'')
|
walther@59867
|
322 |
| rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
|
wneuper@59416
|
323 |
| rule2tac _ subst (Rule.Rls_ rls) =
|
walther@59911
|
324 |
Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
|
wneuper@59302
|
325 |
| rule2tac _ _ rule =
|
walther@59867
|
326 |
error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
|
wneuper@59302
|
327 |
|
walther@59914
|
328 |
(* try if a rewrite-rule is applicable to a given formula;
|
walther@59914
|
329 |
in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
|
walther@59914
|
330 |
fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
|
walther@59914
|
331 |
if Auto_Prog.contains_bdv thm
|
walther@59914
|
332 |
then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
|
walther@59914
|
333 |
SOME _ => [rule2tac thy subst thm']
|
walther@59914
|
334 |
| NONE => []
|
walther@59914
|
335 |
else (case Rewrite.rewrite_ thy ro erls false thm f of
|
walther@59914
|
336 |
SOME _ => [rule2tac thy [] thm']
|
walther@59914
|
337 |
| NONE => [])
|
walther@59914
|
338 |
| try_rew thy _ _ _ f (cal as Rule.Eval c) =
|
walther@59914
|
339 |
(case Eval.adhoc_thm thy c f of
|
walther@59914
|
340 |
SOME _ => [rule2tac thy [] cal]
|
walther@59914
|
341 |
| NONE => [])
|
walther@59914
|
342 |
| try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
|
walther@59914
|
343 |
(case Eval.adhoc_thm thy c f of
|
walther@59914
|
344 |
SOME _ => [rule2tac thy [] cal]
|
walther@59914
|
345 |
| NONE => [])
|
walther@59914
|
346 |
| try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
|
walther@59914
|
347 |
| try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
|
walther@59914
|
348 |
and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
|
walther@59914
|
349 |
gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
|
walther@59914
|
350 |
| filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
|
walther@59914
|
351 |
gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
|
walther@59914
|
352 |
| filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
|
walther@59914
|
353 |
| filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
|
walther@59914
|
354 |
|
walther@59914
|
355 |
(* decide if a tactic is applicable to a given formula;
|
walther@59914
|
356 |
in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
|
walther@59914
|
357 |
fun applicable thy _ _ f (Calculate scrID) =
|
walther@59914
|
358 |
try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
|
walther@59914
|
359 |
| applicable thy ro erls f (Rewrite thm'') =
|
walther@59914
|
360 |
try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
|
walther@59914
|
361 |
| applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
|
walther@59914
|
362 |
try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
|
walther@59914
|
363 |
|
walther@59914
|
364 |
| applicable thy _ _ f (Rewrite_Set rls') =
|
walther@59914
|
365 |
filter_appl_rews thy [] f (assoc_rls rls')
|
walther@59914
|
366 |
| applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
|
walther@59914
|
367 |
filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
|
walther@59914
|
368 |
| applicable _ _ _ _ tac =
|
walther@59914
|
369 |
(tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
|
walther@59914
|
370 |
|
walther@59914
|
371 |
|
walther@59914
|
372 |
(** tactics for internal use **)
|
walther@59914
|
373 |
|
walther@59846
|
374 |
(* tactics for for internal use, compare "input" for user at the front-end.
|
walther@59846
|
375 |
tac_ contains results from check in 'fun applicable_in'.
|
walther@59846
|
376 |
This is useful for costly results, e.g. from rewriting;
|
walther@59846
|
377 |
however, these results might be changed by Scripts like
|
walther@59846
|
378 |
" eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
|
walther@59846
|
379 |
" eq = (Rewrite_Set equival_trans False) eq;" ^
|
walther@59846
|
380 |
TODO.WN120106 ANALOGOUSLY TO Substitute':
|
walther@59846
|
381 |
So tac_ contains the term t the result was calculated from
|
walther@59846
|
382 |
in order to compare t with t' possibly changed by "Expr "
|
walther@59846
|
383 |
and re-calculate result if t<>t'
|
walther@59846
|
384 |
TODO.WN161219: replace *every* cterm' by term
|
walther@59846
|
385 |
*)
|
walther@59846
|
386 |
datatype T =
|
walther@59865
|
387 |
Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
|
walther@59865
|
388 |
| Add_Relation' of TermC.as_string * Model.itm list
|
walther@59846
|
389 |
| Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
|
walther@59846
|
390 |
* tactic Apply_Method metID
|
walther@59846
|
391 |
* formula term *)
|
walther@59903
|
392 |
Method.id * (* key for Know_Store *)
|
walther@59846
|
393 |
term option * (* the first formula of Calc.T. TODO: rm option *)
|
walther@59846
|
394 |
Istate_Def.T * (* for the newly started program *)
|
walther@59846
|
395 |
Proof.context (* for the newly started program *)
|
walther@59846
|
396 |
(*/--- TODO: re-design ? -----------------------------------------------------------------\*)
|
walther@59846
|
397 |
| Begin_Sequ' | Begin_Trans' of term
|
walther@59846
|
398 |
| Split_And' of term | Split_Or' of term | Split_Intersect' of term
|
walther@59846
|
399 |
| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
|
walther@59846
|
400 |
| End_Sequ' | End_Trans' of Selem.result
|
walther@59846
|
401 |
| End_Ruleset' of term | End_Intersect' of term | End_Proof''
|
walther@59846
|
402 |
(*\--- TODO: re-design ? -----------------------------------------------------------------/*)
|
walther@59846
|
403 |
| CAScmd' of term
|
walther@59879
|
404 |
| Calculate' of ThyC.id * string * term * (term * ThmC.T)
|
walther@59903
|
405 |
| Check_Postcond' of Problem.id *
|
walther@59846
|
406 |
term (* returnvalue of program in solve *)
|
walther@59846
|
407 |
| Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
|
walther@59846
|
408 |
term * (* (1) the current formula: [x=1,x=...] *)
|
walther@59846
|
409 |
string * (* (2) the pred from Check_elementwise *)
|
walther@59846
|
410 |
Selem.result (* (3) composed from (1) and (2): {x. pred} *)
|
walther@59865
|
411 |
| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
|
wneuper@59302
|
412 |
|
walther@59851
|
413 |
| Derive' of Rule_Set.T
|
walther@59879
|
414 |
| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
|
walther@59910
|
415 |
| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
|
walther@59846
|
416 |
| End_Detail' of Selem.result
|
walther@59846
|
417 |
|
walther@59846
|
418 |
| Empty_Tac_
|
walther@59846
|
419 |
| Free_Solve'
|
walther@59846
|
420 |
|
walther@59903
|
421 |
| Init_Proof' of TermC.as_string list * Spec.T
|
walther@59846
|
422 |
| Model_Problem' of (* first step in specifying *)
|
walther@59903
|
423 |
Problem.id * (* key into Know_Store *)
|
walther@59846
|
424 |
Model.itm list * (* the 'untouched' pbl *)
|
walther@59846
|
425 |
Model.itm list (* the casually completed met *)
|
walther@59846
|
426 |
| Or_to_List' of term * term
|
walther@59903
|
427 |
| Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
|
walther@59846
|
428 |
| Refine_Tacitly' of
|
walther@59903
|
429 |
Problem.id * (* input *)
|
walther@59903
|
430 |
Problem.id * (* the refined from applicable_in *)
|
walther@59879
|
431 |
ThyC.id * (* from new pbt?! filled in specify *)
|
walther@59903
|
432 |
Method.id * (* from new pbt?! filled in specify *)
|
walther@59846
|
433 |
Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
|
walther@59879
|
434 |
| Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
|
walther@59910
|
435 |
| Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
|
walther@59879
|
436 |
| Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
|
walther@59910
|
437 |
| Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
|
walther@59846
|
438 |
|
walther@59903
|
439 |
| Specify_Method' of Method.id * Model.ori list * Model.itm list
|
walther@59903
|
440 |
| Specify_Problem' of Problem.id *
|
walther@59846
|
441 |
(bool * (* matches *)
|
walther@59846
|
442 |
(Model.itm list * (* ppc *)
|
walther@59846
|
443 |
(bool * term) list)) (* preconditions marked true/false *)
|
walther@59879
|
444 |
| Specify_Theory' of ThyC.id
|
walther@59846
|
445 |
| Subproblem' of
|
walther@59903
|
446 |
Spec.T *
|
walther@59846
|
447 |
(Model.ori list) * (* filled in associate Subproblem' *)
|
walther@59846
|
448 |
term * (* filled -"-, headline of calc-head *)
|
walther@59846
|
449 |
Selem.fmz_ * (* string list from arguments *)
|
walther@59846
|
450 |
Proof.context * (* for specify-phase *)
|
walther@59846
|
451 |
term (* Subproblem (thyID, pbl) OR cascmd *)
|
walther@59846
|
452 |
| Substitute' of
|
walther@59850
|
453 |
Rule_Def.rew_ord_ * (* for re-calculation *)
|
walther@59851
|
454 |
Rule_Set.T * (* for re-calculation *)
|
walther@59912
|
455 |
Subst.as_eqs * (* the 'substitution': terms of type bool *)
|
walther@59846
|
456 |
term * (* to be substituted into *)
|
walther@59846
|
457 |
term (* resulting from the substitution *)
|
walther@59846
|
458 |
| Tac_ of theory * string * string * string
|
walther@59846
|
459 |
| Take' of term
|
walther@59846
|
460 |
|
walther@59846
|
461 |
fun string_of ma = case ma of
|
walther@59902
|
462 |
Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
|
walther@59846
|
463 |
| Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
|
walther@59846
|
464 |
| Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
|
walther@59846
|
465 |
strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
|
walther@59846
|
466 |
| Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
|
walther@59846
|
467 |
| Add_Given' _ => "Add_Given' "(*^cterm'*)
|
walther@59846
|
468 |
| Del_Given' _ => "Del_Given' "(*^cterm'*)
|
walther@59846
|
469 |
| Add_Find' _ => "Add_Find' "(*^cterm'*)
|
walther@59846
|
470 |
| Del_Find' _ => "Del_Find' "(*^cterm'*)
|
walther@59846
|
471 |
| Add_Relation' _ => "Add_Relation' "(*^cterm'*)
|
walther@59846
|
472 |
| Del_Relation' _ => "Del_Relation' "(*^cterm'*)
|
walther@59846
|
473 |
|
walther@59846
|
474 |
| Specify_Theory' domID => "Specify_Theory' " ^ quote domID
|
walther@59846
|
475 |
| Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
|
walther@59846
|
476 |
spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
|
walther@59846
|
477 |
| Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
|
walther@59903
|
478 |
Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
|
walther@59846
|
479 |
|
walther@59846
|
480 |
| Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
|
walther@59846
|
481 |
| Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
|
walther@59868
|
482 |
(spair2str (strs2str pblID, UnparseC.term scval))
|
walther@59846
|
483 |
|
walther@59846
|
484 |
| Free_Solve' => "Free_Solve'"
|
walther@59846
|
485 |
|
walther@59846
|
486 |
| Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
|
walther@59846
|
487 |
| Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
|
walther@59846
|
488 |
| Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
|
walther@59846
|
489 |
| Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
|
walther@59868
|
490 |
"," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
|
walther@59846
|
491 |
| End_Detail' _ => "End_Detail' xxx"
|
walther@59846
|
492 |
| Detail_Set' _ => "Detail_Set' xxx"
|
walther@59846
|
493 |
| Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
|
walther@59846
|
494 |
|
walther@59867
|
495 |
| Derive' rls => "Derive' " ^ Rule_Set.id rls
|
walther@59846
|
496 |
| Calculate' _ => "Calculate' "
|
walther@59846
|
497 |
| Substitute' _ => "Substitute' "(*^(subs2str subs)*)
|
walther@59846
|
498 |
|
walther@59846
|
499 |
| Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
|
walther@59846
|
500 |
| Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
|
walther@59846
|
501 |
"Subproblem' "(*^(pair2str (domID, strs2str ,))*)
|
walther@59846
|
502 |
| CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
|
walther@59846
|
503 |
|
walther@59846
|
504 |
| Empty_Tac_ => "Empty_Tac_"
|
walther@59846
|
505 |
| Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
|
walther@59846
|
506 |
| _ => "string_of not impl. for arg";
|
wneuper@59302
|
507 |
|
walther@59704
|
508 |
fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
|
walther@59704
|
509 |
| input_from_T (Model_Problem' (_, _, _)) = Model_Problem
|
walther@59704
|
510 |
| input_from_T (Add_Given' (t, _)) = Add_Given t
|
walther@59704
|
511 |
| input_from_T (Add_Find' (t, _)) = Add_Find t
|
walther@59704
|
512 |
| input_from_T (Add_Relation' (t, _)) = Add_Relation t
|
walther@59704
|
513 |
|
walther@59704
|
514 |
| input_from_T (Specify_Theory' dI) = Specify_Theory dI
|
walther@59704
|
515 |
| input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
|
walther@59704
|
516 |
| input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
|
walther@59704
|
517 |
|
walther@59704
|
518 |
| input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
|
walther@59911
|
519 |
| input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
|
walther@59704
|
520 |
|
walther@59867
|
521 |
| input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
|
walther@59867
|
522 |
| input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
|
walther@59704
|
523 |
|
walther@59704
|
524 |
| input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
|
walther@59911
|
525 |
Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
|
walther@59704
|
526 |
| input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
|
walther@59911
|
527 |
Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
|
walther@59704
|
528 |
|
walther@59704
|
529 |
| input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
|
walther@59704
|
530 |
| input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
|
walther@59704
|
531 |
|
walther@59704
|
532 |
| input_from_T (Or_to_List' _) = Or_to_List
|
walther@59868
|
533 |
| input_from_T (Take' term) = Take (UnparseC.term term)
|
walther@59912
|
534 |
| input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte)
|
walther@59704
|
535 |
| input_from_T (Tac_ (_, _, id, _)) = Tac id
|
walther@59704
|
536 |
|
walther@59704
|
537 |
| input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
|
walther@59704
|
538 |
| input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
|
walther@59704
|
539 |
| input_from_T Empty_Tac_ = Empty_Tac
|
walther@59846
|
540 |
| input_from_T m = raise ERROR (": not impl. for "^(string_of m));
|
walther@59704
|
541 |
|
walther@59728
|
542 |
fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
|
walther@59728
|
543 |
| res (Rewrite' (_, _, _, _, _, _, res)) = res
|
walther@59728
|
544 |
| res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
|
walther@59728
|
545 |
| res (Rewrite_Set' (_, _, _, _, res)) = res
|
walther@59728
|
546 |
| res (Calculate' (_, _, _, (t, _))) = (t, [])
|
walther@59728
|
547 |
| res (Check_elementwise' (_, _, res)) = res
|
walther@59728
|
548 |
| res (Subproblem' (_, _, _, _, _, t)) = (t, [])
|
walther@59728
|
549 |
| res (Take' t) = (t, [])
|
walther@59728
|
550 |
| res (Substitute' (_, _, _, _, t)) = (t, [])
|
walther@59728
|
551 |
| res (Or_to_List' (_, t)) = (t, [])
|
walther@59846
|
552 |
| res m = raise ERROR ("result: not impl.for " ^ string_of m)
|
walther@59728
|
553 |
|
walther@59728
|
554 |
(*fun result m = (fst o res) m; TODO*)
|
walther@59728
|
555 |
fun result tac = (fst o res) tac;
|
walther@59728
|
556 |
fun creates_assms tac = (snd o res) tac;
|
walther@59728
|
557 |
|
walther@59728
|
558 |
fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
|
walther@59728
|
559 |
|
walther@59749
|
560 |
fun for_specify (Init_Proof _) = true
|
walther@59749
|
561 |
| for_specify Model_Problem = true
|
walther@59749
|
562 |
| for_specify (Refine_Tacitly _) = true
|
walther@59749
|
563 |
| for_specify (Refine_Problem _) = true
|
walther@59749
|
564 |
| for_specify (Add_Given _) = true
|
walther@59749
|
565 |
| for_specify (Del_Given _) = true
|
walther@59749
|
566 |
| for_specify (Add_Find _) = true
|
walther@59749
|
567 |
| for_specify (Del_Find _) = true
|
walther@59749
|
568 |
| for_specify (Add_Relation _) = true
|
walther@59749
|
569 |
| for_specify (Del_Relation _) = true
|
walther@59749
|
570 |
| for_specify (Specify_Theory _) = true
|
walther@59749
|
571 |
| for_specify (Specify_Problem _) = true
|
walther@59749
|
572 |
| for_specify (Specify_Method _) = true
|
walther@59749
|
573 |
| for_specify _ = false
|
walther@59749
|
574 |
fun for_specify' (Init_Proof' _) = true
|
walther@59749
|
575 |
| for_specify' (Model_Problem' _) = true
|
walther@59749
|
576 |
| for_specify' (Refine_Tacitly' _) = true
|
walther@59749
|
577 |
| for_specify' (Refine_Problem' _) = true
|
walther@59749
|
578 |
| for_specify' (Add_Given' _) = true
|
walther@59749
|
579 |
| for_specify' (Del_Given' _) = true
|
walther@59749
|
580 |
| for_specify' (Add_Find' _) = true
|
walther@59749
|
581 |
| for_specify' (Del_Find' _) = true
|
walther@59749
|
582 |
| for_specify' (Add_Relation' _) = true
|
walther@59749
|
583 |
| for_specify' (Del_Relation' _) = true
|
walther@59749
|
584 |
| for_specify' (Specify_Theory' _) = true
|
walther@59749
|
585 |
| for_specify' (Specify_Problem' _) = true
|
walther@59749
|
586 |
| for_specify' (Specify_Method' _) = true
|
walther@59749
|
587 |
| for_specify' _ = false
|
walther@59749
|
588 |
|
walther@59728
|
589 |
(**)end(**)
|