1 (* Title: Tactics; tac_ for interaction with frontend, input for internal use.
2 Author: Walther Neuper 170121
3 (c) due to copyright terms
5 regular expression for search:
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_Asm|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
12 datatype T = datatype Tactic_Def.T
13 val string_of : T -> string
15 datatype input = datatype Tactic_Def.input
16 val tac2str : input -> string
18 val eq_tac : input * input -> bool
19 val is_empty_tac : input -> bool
20 val is_rewtac : input -> bool
21 val is_rewset : input -> bool
22 val rls_of : input -> Rule.rls'
23 val tac2IDstr : input -> string
24 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
25 val input_from_T : T -> input
26 val result : T -> term
27 val creates_assms: T -> term list
28 val insert_assumptions: T -> Proof.context -> Proof.context
30 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
32 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
34 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
36 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
41 structure Tactic(**): TACTIC(**) =
45 (* tactics for user at front-end.
46 input propagates the construction of the calc-tree;
48 (a) 'specsteps' for the specify-phase, and others for the solve-phase
49 (b) those of the solve-phase are 'initac's and others;
50 initacs start with a formula different from the preceding formula.
51 see 'type tac_' for the internal representation of tactics
53 datatype input = datatype Tactic_Def.input
55 val tac2str = Tactic_Def.tac2str
57 val is_empty_tac = Tactic_Def.is_empty_tac
59 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
60 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
61 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
62 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
63 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
66 fun is_rewset (Rewrite_Set_Inst _) = true
67 | is_rewset (Rewrite_Set _) = true
68 | is_rewset _ = false;
69 fun is_rewtac (Rewrite _) = true
70 | is_rewtac (Rewrite_Inst _) = true
71 | is_rewtac (Rewrite_Asm _) = true
72 | is_rewtac input = is_rewset input;
74 fun tac2IDstr ma = case ma of
75 Model_Problem => "Model_Problem"
76 | Refine_Tacitly _ => "Refine_Tacitly"
77 | Refine_Problem _ => "Refine_Problem"
78 | Add_Given _ => "Add_Given"
79 | Del_Given _ => "Del_Given"
80 | Add_Find _ => "Add_Find"
81 | Del_Find _ => "Del_Find"
82 | Add_Relation _ => "Add_Relation"
83 | Del_Relation _ => "Del_Relation"
85 | Specify_Theory _ => "Specify_Theory"
86 | Specify_Problem _ => "Specify_Problem"
87 | Specify_Method _ => "Specify_Method"
88 | Apply_Method _ => "Apply_Method"
89 | Check_Postcond _ => "Check_Postcond"
90 | Free_Solve => "Free_Solve"
92 | Rewrite_Inst _ => "Rewrite_Inst"
93 | Rewrite _ => "Rewrite"
94 | Rewrite_Asm _ => "Rewrite_Asm"
95 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
96 | Rewrite_Set _ => "Rewrite_Set"
97 | Detail_Set _ => "Detail_Set"
98 | Detail_Set_Inst _ => "Detail_Set_Inst"
99 | Derive _ => "Derive "
100 | Calculate _ => "Calculate "
101 | Substitute _ => "Substitute"
102 | Apply_Assumption _ => "Apply_Assumption"
105 | Take_Inst _ => "Take_Inst"
106 | Subproblem _ => "Subproblem"
107 | End_Subproblem => "End_Subproblem"
108 | CAScmd _ => "CAScmd"
110 | Check_elementwise _ => "Check_elementwise"
111 | Or_to_List => "Or_to_List "
112 | Collect_Trues => "Collect_Trues"
114 | Empty_Tac => "Empty_Tac"
116 | End_Proof' => "End_Proof'"
117 | _ => "tac2str not impl. for ?!";
119 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
120 | rls_of (Rewrite_Set rls) = rls
121 | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
123 fun rule2tac thy _ (Rule.Calc (opID, _)) = Calculate (assoc_calc thy opID)
124 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
125 | rule2tac _ subst (Rule.Thm thm'') =
126 Rewrite_Inst (Selem.subst2subs subst, thm'')
127 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule.id_rls rls)
128 | rule2tac _ subst (Rule.Rls_ rls) =
129 Rewrite_Set_Inst (Selem.subst2subs subst, (Rule.id_rls rls))
130 | rule2tac _ _ rule =
131 error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
133 (* tactics for for internal use, compare "input" for user at the front-end.
134 tac_ contains results from check in 'fun applicable_in'.
135 This is useful for costly results, e.g. from rewriting;
136 however, these results might be changed by Scripts like
137 " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
138 " eq = (Rewrite_Set equival_trans False) eq;" ^
139 TODO.WN120106 ANALOGOUSLY TO Substitute':
140 So tac_ contains the term t the result was calculated from
141 in order to compare t with t' possibly changed by "Expr "
142 and re-calculate result if t<>t'
143 TODO.WN161219: replace *every* cterm' by term
145 datatype T = datatype Tactic_Def.T
147 val string_of = Tactic_Def.string_of
149 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
150 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
151 | input_from_T (Add_Given' (t, _)) = Add_Given t
152 | input_from_T (Add_Find' (t, _)) = Add_Find t
153 | input_from_T (Add_Relation' (t, _)) = Add_Relation t
155 | input_from_T (Specify_Theory' dI) = Specify_Theory dI
156 | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
157 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
159 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
160 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
162 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule.id_rls rls)
163 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule.id_rls rls)
165 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
166 Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
167 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
168 Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
170 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
171 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
173 | input_from_T (Or_to_List' _) = Or_to_List
174 | input_from_T (Take' term) = Take (Rule.term2str term)
175 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
176 | input_from_T (Tac_ (_, _, id, _)) = Tac id
178 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
179 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
180 | input_from_T Empty_Tac_ = Empty_Tac
181 | input_from_T m = error (": not impl. for "^(string_of m));
183 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
184 | res (Rewrite' (_, _, _, _, _, _, res)) = res
185 | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
186 | res (Rewrite_Set' (_, _, _, _, res)) = res
187 | res (Calculate' (_, _, _, (t, _))) = (t, [])
188 | res (Check_elementwise' (_, _, res)) = res
189 | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
190 | res (Take' t) = (t, [])
191 | res (Substitute' (_, _, _, _, t)) = (t, [])
192 | res (Or_to_List' (_, t)) = (t, [])
193 | res m = raise ERROR ("result: not impl.for " ^ string_of m)
195 (*fun result m = (fst o res) m; TODO*)
196 fun result tac = (fst o res) tac;
197 fun creates_assms tac = (snd o res) tac;
199 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt