234 | is_rewtac input = is_rewset input; |
234 | is_rewtac input = is_rewset input; |
235 |
235 |
236 |
236 |
237 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
237 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
238 | rls_of (Rewrite_Set rls) = rls |
238 | rls_of (Rewrite_Set rls) = rls |
239 | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\""); |
239 | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\""); |
240 |
240 |
241 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID) |
241 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID) |
242 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm'' |
242 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm'' |
243 | rule2tac _ subst (Rule.Thm thm'') = |
243 | rule2tac _ subst (Rule.Thm thm'') = |
244 Rewrite_Inst (Subst.T_to_input subst, thm'') |
244 Rewrite_Inst (Subst.T_to_input subst, thm'') |
245 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) |
245 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) |
246 | rule2tac _ subst (Rule.Rls_ rls) = |
246 | rule2tac _ subst (Rule.Rls_ rls) = |
247 Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls)) |
247 Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls)) |
248 | rule2tac _ _ rule = |
248 | rule2tac _ _ rule = |
249 error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\""); |
249 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\""); |
250 |
250 |
251 (* try if a rewrite-rule is applicable to a given formula; |
251 (* try if a rewrite-rule is applicable to a given formula; |
252 in case of rule-sets (recursivley) collect all _atomic_ rewrites *) |
252 in case of rule-sets (recursivley) collect all _atomic_ rewrites *) |
253 fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) = |
253 fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) = |
254 if Auto_Prog.contains_bdv thm |
254 if Auto_Prog.contains_bdv thm |
265 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) = |
265 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) = |
266 (case Eval.adhoc_thm thy c f of |
266 (case Eval.adhoc_thm thy c f of |
267 SOME _ => [rule2tac thy [] cal] |
267 SOME _ => [rule2tac thy [] cal] |
268 | NONE => []) |
268 | NONE => []) |
269 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls |
269 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls |
270 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case" |
270 | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case" |
271 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = |
271 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = |
272 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) |
272 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) |
273 | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = |
273 | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = |
274 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) |
274 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) |
275 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = [] |
275 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = [] |
276 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case" |
276 | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case" |
277 |
277 |
278 (* decide if a tactic is applicable to a given formula; |
278 (* decide if a tactic is applicable to a given formula; |
279 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *) |
279 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *) |
280 fun applicable thy _ _ f (Calculate scrID) = |
280 fun applicable thy _ _ f (Calculate scrID) = |
281 try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd)) |
281 try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd)) |