79 |
79 |
80 val eq_tac : input * input -> bool |
80 val eq_tac : input * input -> bool |
81 val is_rewtac : input -> bool |
81 val is_rewtac : input -> bool |
82 val is_rewset : input -> bool |
82 val is_rewset : input -> bool |
83 val rls_of : input -> Rule_Set.id |
83 val rls_of : input -> Rule_Set.id |
84 val rule2tac : theory -> Env.T -> Rule.rule -> input |
84 val rule2tac : Proof.context -> Env.T -> Rule.rule -> input |
85 val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list |
85 val applicable : Proof.context -> string -> Rule_Set.T -> term -> input ->input list |
86 val for_specify: input -> bool |
86 val for_specify: input -> bool |
87 |
87 |
88 val input_from_T : T -> input |
88 val input_from_T : T -> input |
89 val result : T -> term |
89 val result : T -> term |
90 val creates_assms: T -> term list |
90 val creates_assms: T -> term list |
226 |
226 |
227 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
227 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
228 | rls_of (Rewrite_Set rls) = rls |
228 | rls_of (Rewrite_Set rls) = rls |
229 | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\""); |
229 | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\""); |
230 |
230 |
231 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID) |
231 fun rule2tac ctxt _ (Rule.Eval (opID, _)) = Calculate (assoc_calc (Proof_Context.theory_of ctxt) opID) |
232 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm'' |
232 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm'' |
233 | rule2tac _ subst (Rule.Thm thm'') = |
233 | rule2tac _ subst (Rule.Thm thm'') = |
234 Rewrite_Inst (Subst.T_to_input subst, thm'') |
234 Rewrite_Inst (Subst.T_to_input subst, thm'') |
235 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) |
235 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) |
236 | rule2tac _ subst (Rule.Rls_ rls) = |
236 | rule2tac _ subst (Rule.Rls_ rls) = |
238 | rule2tac _ _ rule = |
238 | rule2tac _ _ rule = |
239 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\""); |
239 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\""); |
240 |
240 |
241 (* try if a rewrite-rule is applicable to a given formula; |
241 (* try if a rewrite-rule is applicable to a given formula; |
242 in case of rule-sets (recursivley) collect all _atomic_ rewrites *) |
242 in case of rule-sets (recursivley) collect all _atomic_ rewrites *) |
243 fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) = |
243 fun try_rew ctxt ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) = |
244 if Auto_Prog.contains_bdv thm |
244 if Auto_Prog.contains_bdv thm |
245 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of |
245 then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of |
246 SOME _ => [rule2tac thy subst thm'] |
246 SOME _ => [rule2tac ctxt subst thm'] |
247 | NONE => [] |
247 | NONE => [] |
248 else (case Rewrite.rewrite_ thy ro erls false thm f of |
248 else (case Rewrite.rewrite_ ctxt ro erls false thm f of |
249 SOME _ => [rule2tac thy [] thm'] |
249 SOME _ => [rule2tac ctxt [] thm'] |
250 | NONE => []) |
250 | NONE => []) |
251 | try_rew thy _ _ _ f (cal as Rule.Eval c) = |
251 | try_rew ctxt _ _ _ f (cal as Rule.Eval c) = |
252 (case Eval.adhoc_thm thy c f of |
252 (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of |
253 SOME _ => [rule2tac thy [] cal] |
253 SOME _ => [rule2tac ctxt [] cal] |
254 | NONE => []) |
254 | NONE => []) |
255 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) = |
255 | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) = |
256 (case Eval.adhoc_thm thy c f of |
256 (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of |
257 SOME _ => [rule2tac thy [] cal] |
257 SOME _ => [rule2tac ctxt [] cal] |
258 | NONE => []) |
258 | NONE => []) |
259 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls |
259 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls |
260 | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case" |
260 | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case" |
261 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = |
261 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = |
262 distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) |
262 distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) |
265 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = [] |
265 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = [] |
266 | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case" |
266 | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case" |
267 |
267 |
268 (* decide if a tactic is applicable to a given formula; |
268 (* decide if a tactic is applicable to a given formula; |
269 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *) |
269 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *) |
270 fun applicable thy _ _ f (Calculate scrID) = |
270 fun applicable ctxt _ _ f (Calculate scrID) = |
271 try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd)) |
271 try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f |
272 | applicable thy ro erls f (Rewrite thm'') = |
272 (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd)) |
273 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'') |
273 | applicable ctxt ro erls f (Rewrite thm'') = |
274 | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) = |
274 try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'') |
275 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'') |
275 | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) = |
|
276 try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input ctxt subs) f (Rule.Thm thm'') |
276 |
277 |
277 | applicable thy _ _ f (Rewrite_Set rls') = |
278 | applicable thy _ _ f (Rewrite_Set rls') = |
278 filter_appl_rews thy [] f (assoc_rls rls') |
279 filter_appl_rews thy [] f (assoc_rls rls') |
279 | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) = |
280 | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) = |
280 filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls') |
281 filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls') |