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_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
17 val tac2IDstr : input -> string
18 val is_empty : input -> bool
20 (*//-------------------------------------------------------------- only AFTER ctree.sml required *)
21 val eq_tac : input * input -> bool
22 val is_rewtac : input -> bool
23 val is_rewset : input -> bool
24 val rls_of : input -> Rule.rls'
25 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
26 val input_from_T : T -> input
27 val result : T -> term
28 val creates_assms: T -> term list
29 val insert_assumptions: T -> Proof.context -> Proof.context
30 val for_specify: input -> bool
31 val for_specify': T -> bool
33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
35 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
37 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
39 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
44 structure Tactic(**): TACTIC(**) =
48 datatype input = datatype Tactic_Def.input
50 val tac2str = Tactic_Def.tac2str
51 val tac2IDstr = Tactic_Def.tac2IDstr
52 val is_empty = Tactic_Def.is_empty
54 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
55 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
56 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
57 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
58 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
61 fun is_rewset (Rewrite_Set_Inst _) = true
62 | is_rewset (Rewrite_Set _) = true
63 | is_rewset _ = false;
64 fun is_rewtac (Rewrite _) = true
65 | is_rewtac (Rewrite_Inst _) = true
66 | is_rewtac input = is_rewset input;
69 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
70 | rls_of (Rewrite_Set rls) = rls
71 | rls_of input = error ("rls_of: called with input \"" ^ Tactic_Def.tac2IDstr input ^ "\"");
73 fun rule2tac thy _ (Rule.Num_Calc (opID, _)) = Calculate (assoc_calc thy opID)
74 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
75 | rule2tac _ subst (Rule.Thm thm'') =
76 Rewrite_Inst (Selem.subst2subs subst, thm'')
77 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule.id_rls rls)
78 | rule2tac _ subst (Rule.Rls_ rls) =
79 Rewrite_Set_Inst (Selem.subst2subs subst, (Rule.id_rls rls))
81 error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
83 datatype T = datatype Tactic_Def.T
85 val string_of = Tactic_Def.string_of
87 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
88 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
89 | input_from_T (Add_Given' (t, _)) = Add_Given t
90 | input_from_T (Add_Find' (t, _)) = Add_Find t
91 | input_from_T (Add_Relation' (t, _)) = Add_Relation t
93 | input_from_T (Specify_Theory' dI) = Specify_Theory dI
94 | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
95 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
97 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
98 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
100 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule.id_rls rls)
101 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule.id_rls rls)
103 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
104 Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
105 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
106 Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
108 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
109 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
111 | input_from_T (Or_to_List' _) = Or_to_List
112 | input_from_T (Take' term) = Take (Rule.term2str term)
113 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
114 | input_from_T (Tac_ (_, _, id, _)) = Tac id
116 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
117 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
118 | input_from_T Empty_Tac_ = Empty_Tac
119 | input_from_T m = raise ERROR (": not impl. for "^(Tactic_Def.string_of m));
121 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
122 | res (Rewrite' (_, _, _, _, _, _, res)) = res
123 | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
124 | res (Rewrite_Set' (_, _, _, _, res)) = res
125 | res (Calculate' (_, _, _, (t, _))) = (t, [])
126 | res (Check_elementwise' (_, _, res)) = res
127 | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
128 | res (Take' t) = (t, [])
129 | res (Substitute' (_, _, _, _, t)) = (t, [])
130 | res (Or_to_List' (_, t)) = (t, [])
131 | res m = raise ERROR ("result: not impl.for " ^ Tactic_Def.string_of m)
133 (*fun result m = (fst o res) m; TODO*)
134 fun result tac = (fst o res) tac;
135 fun creates_assms tac = (snd o res) tac;
137 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
139 fun for_specify (Init_Proof _) = true
140 | for_specify Model_Problem = true
141 | for_specify (Refine_Tacitly _) = true
142 | for_specify (Refine_Problem _) = true
143 | for_specify (Add_Given _) = true
144 | for_specify (Del_Given _) = true
145 | for_specify (Add_Find _) = true
146 | for_specify (Del_Find _) = true
147 | for_specify (Add_Relation _) = true
148 | for_specify (Del_Relation _) = true
149 | for_specify (Specify_Theory _) = true
150 | for_specify (Specify_Problem _) = true
151 | for_specify (Specify_Method _) = true
152 | for_specify _ = false
153 fun for_specify' (Init_Proof' _) = true
154 | for_specify' (Model_Problem' _) = true
155 | for_specify' (Refine_Tacitly' _) = true
156 | for_specify' (Refine_Problem' _) = true
157 | for_specify' (Add_Given' _) = true
158 | for_specify' (Del_Given' _) = true
159 | for_specify' (Add_Find' _) = true
160 | for_specify' (Del_Find' _) = true
161 | for_specify' (Add_Relation' _) = true
162 | for_specify' (Del_Relation' _) = true
163 | for_specify' (Specify_Theory' _) = true
164 | for_specify' (Specify_Problem' _) = true
165 | for_specify' (Specify_Method' _) = true
166 | for_specify' _ = false