1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 27 16:40:11 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue Apr 28 15:31:49 2020 +0200
     1.3 @@ -113,11 +113,13 @@
     1.4    val is_rewset : input -> bool
     1.5    val rls_of : input -> Rule_Set.id
     1.6    val rule2tac : theory -> (term * term) list ->  Rule.rule -> input
     1.7 +  val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
     1.8 +  val for_specify: input -> bool
     1.9 +
    1.10    val input_from_T : T -> input
    1.11    val result : T -> term
    1.12    val creates_assms: T -> term list
    1.13    val insert_assumptions: T -> Proof.context -> Proof.context
    1.14 -  val for_specify: input -> bool
    1.15    val for_specify': T -> bool
    1.16  
    1.17  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.18 @@ -135,6 +137,8 @@
    1.19  struct
    1.20  (**)
    1.21  
    1.22 +(** tactics for user at front-end **)
    1.23 +
    1.24  (* tactics for user at front-end.
    1.25     input propagates the construction of the calc-tree;
    1.26     there are
    1.27 @@ -321,6 +325,52 @@
    1.28    | rule2tac _ _ rule = 
    1.29      error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
    1.30  
    1.31 +(* try if a rewrite-rule is applicable to a given formula; 
    1.32 +   in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 
    1.33 +fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
    1.34 +    if Auto_Prog.contains_bdv thm
    1.35 +    then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
    1.36 +	    SOME _ => [rule2tac thy subst thm']
    1.37 +	  | NONE => []
    1.38 +    else (case Rewrite.rewrite_ thy ro erls false thm f of
    1.39 +	    SOME _ => [rule2tac thy [] thm']
    1.40 +	  | NONE => [])
    1.41 +  | try_rew thy _ _ _ f (cal as Rule.Eval c) = 
    1.42 +    (case Eval.adhoc_thm thy c f of
    1.43 +	    SOME _ => [rule2tac thy [] cal]
    1.44 +    | NONE => [])
    1.45 +  | try_rew thy _ _ _ f (cal as Rule.Cal1 c) = 
    1.46 +    (case Eval.adhoc_thm thy c f of
    1.47 +	      SOME _ => [rule2tac thy [] cal]
    1.48 +      | NONE => [])
    1.49 +  | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
    1.50 +  | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
    1.51 +and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = 
    1.52 +    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.53 +  | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = 
    1.54 +    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.55 +  | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
    1.56 +  | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
    1.57 +
    1.58 +(* decide if a tactic is applicable to a given formula; 
    1.59 +   in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
    1.60 +fun applicable thy _ _ f (Calculate scrID) =
    1.61 +    try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
    1.62 +  | applicable thy ro erls f (Rewrite thm'') =
    1.63 +    try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
    1.64 +  | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
    1.65 +    try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
    1.66 +
    1.67 +  | applicable thy _ _ f (Rewrite_Set rls') =
    1.68 +    filter_appl_rews thy [] f (assoc_rls rls')
    1.69 +  | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
    1.70 +    filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
    1.71 +  | applicable _ _ _ _ tac = 
    1.72 +    (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
    1.73 +
    1.74 +
    1.75 +(** tactics for internal use **)
    1.76 +
    1.77  (* tactics for for internal use, compare "input" for user at the front-end.
    1.78    tac_ contains results from check in 'fun applicable_in'.
    1.79    This is useful for costly results, e.g. from rewriting;