searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
authorkleing
Mon May 16 09:35:05 2005 +0200 (2005-05-16)
changeset 15964f2074e12d1d4
parent 15963 5b70f789e079
child 15965 f422f8283491
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/proof_general.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon May 16 09:34:20 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 16 09:35:05 2005 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     1.5    val print_methods: Toplevel.transition -> Toplevel.transition
     1.6    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     1.7 -  val print_thms_containing: int option * string list
     1.8 +  val print_thms_containing: int option * (bool * ProofContext.search_criterion) list
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    1.11    val print_binds: Toplevel.transition -> Toplevel.transition
    1.12 @@ -244,9 +244,22 @@
    1.13  
    1.14  val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
    1.15  
    1.16 -fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.17 -  ProofContext.print_thms_containing
    1.18 -    (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec);
    1.19 +fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o 
    1.20 +Toplevel.keep (fn state =>
    1.21 +  let
    1.22 +    fun get_goal () = 
    1.23 +      let val (_, (_, st)) = Proof.get_goal (Toplevel.proof_of state);
    1.24 +      in prop_of st end;
    1.25 +    
    1.26 +    (* searching is permitted without a goal.
    1.27 +       I am not sure whether the only exception that I should catch is UNDEF *)
    1.28 +    val goal = SOME (get_goal ()) handle Toplevel.UNDEF => NONE;
    1.29 +    
    1.30 +    val ctxt = (Toplevel.node_case ProofContext.init Proof.context_of state);
    1.31 +  in
    1.32 +    ProofContext.print_thms_containing ctxt goal lim spec
    1.33 +  end);
    1.34 +
    1.35  
    1.36  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.37    ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 16 09:34:20 2005 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 16 09:35:05 2005 +0200
     2.3 @@ -631,10 +631,30 @@
     2.4      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
     2.5  
     2.6  val thms_containingP =
     2.7 -  OuterSyntax.improper_command "thms_containing"
     2.8 -    "print facts containing certain constants or variables"
     2.9 -    K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
    2.10 -      Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
    2.11 +  let
    2.12 +    (* intro, elim, dest and rewrite are reserved, otherwise it's a pattern *)
    2.13 +    fun decode "intro" = ProofContext.Intro
    2.14 +      | decode "elim" = ProofContext.Elim
    2.15 +      | decode "dest" = ProofContext.Dest
    2.16 +      | decode "rewrite" = ProofContext.Rewrite
    2.17 +      | decode x = ProofContext.Pattern x;
    2.18 +  
    2.19 +    (* either name:term or term *)
    2.20 +    val criterion = ((P.term :-- (fn "name" => P.$$$ ":" |-- P.term | 
    2.21 +                                     _ => Scan.fail)
    2.22 +                                 ) >> (ProofContext.Name o #2)) ||
    2.23 +                    (P.term >> decode);
    2.24 +  in
    2.25 +    OuterSyntax.improper_command "thms_containing"
    2.26 +      "print facts meeting specified criteria"
    2.27 +      K.diag 
    2.28 +      (* obtain (int option * (bool * string) list) representing
    2.29 +         a limit and a set of constraints (the bool indicates whether
    2.30 +         the constraint is inclusive or exclusive) *)
    2.31 +      (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
    2.32 +       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    2.33 +        >> (Toplevel.no_timing oo IsarCmd.print_thms_containing))
    2.34 +  end;
    2.35  
    2.36  val thm_depsP =
    2.37    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
     3.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 16 09:34:20 2005 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 16 09:35:05 2005 +0200
     3.3 @@ -155,7 +155,9 @@
     3.4    val prems_limit: int ref
     3.5    val pretty_asms: context -> Pretty.T list
     3.6    val pretty_context: context -> Pretty.T list
     3.7 -  val print_thms_containing: context -> int option -> string list -> unit
     3.8 +  datatype search_criterion = Intro | Elim  | Dest | Rewrite |
     3.9 +                              Pattern of string | Name of string;
    3.10 +  val print_thms_containing: context -> term option -> int option -> (bool * search_criterion) list -> unit
    3.11  end;
    3.12  
    3.13  signature PRIVATE_PROOF_CONTEXT =
    3.14 @@ -171,6 +173,8 @@
    3.15  structure ProofContext: PRIVATE_PROOF_CONTEXT =
    3.16  struct
    3.17  
    3.18 +datatype search_criterion = Intro | Elim | Dest | Rewrite |
    3.19 +                          Pattern of string | Name of string;
    3.20  
    3.21  (** datatype context **)
    3.22  
    3.23 @@ -1470,28 +1474,159 @@
    3.24      (* things like "prems" can occur twice under some circumstances *)
    3.25      gen_distinct eq_fst (FactIndex.find ([],[]) index);
    3.26  
    3.27 -fun print_thms_containing ctxt opt_limit ss =
    3.28 +fun isSubstring pat str = 
    3.29 +  if String.size pat = 0 then true
    3.30 +  else if String.size pat > String.size str then false
    3.31 +  else if String.substring (str, 0, String.size pat) = pat then true
    3.32 +  else isSubstring pat (String.extract (str, 1, NONE));
    3.33 +
    3.34 +(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into
    3.35 +    a term with all free variables made schematic *)
    3.36 +fun str_pattern_to_term sg str_pattern =
    3.37 +  let
    3.38 +    (* pattern as term with dummies as Consts *)
    3.39 +    val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) 
    3.40 +                       |> Thm.term_of; 
    3.41 +    (* with dummies as Vars *)
    3.42 +    val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern));
    3.43 +  in
    3.44 +    (* with schematic vars *)
    3.45 +    #1 (Type.varify (v_pattern, []))
    3.46 +  end;
    3.47 +
    3.48 +(* alternate rem_top which checks for a Trueprop, unlike that in PureThy *)
    3.49 +fun rem_top_c (Term.Const ("Trueprop", _)  $ t) = t
    3.50 +  | rem_top_c _ = Bound 0;
    3.51 +
    3.52 +(* ---------- search filter contructions go here *)
    3.53 +
    3.54 +(* terms supplied in string form as patterns *)
    3.55 +fun str_term_pat_to_filter sg str_pat = 
    3.56 +  let
    3.57 +    val tsig = Sign.tsig_of sg;
    3.58 +    val pat = str_pattern_to_term sg str_pat;
    3.59 +    
    3.60 +    (* must qualify type so ML doesn't go and replace it with a concrete one *)
    3.61 +    fun name_thm_matches_pattern tsig pat (_:string, thm) =
    3.62 +      Pattern.matches_subterm tsig (pat, Thm.prop_of thm);
    3.63 +  in
    3.64 +    name_thm_matches_pattern (Sign.tsig_of sg) pat
    3.65 +  end;
    3.66 + 
    3.67 +(* create filter that just looks for a string in the name,
    3.68 +   substring match only (no regexps are performed) *)
    3.69 +fun str_name_pat_to_filter str_pat (name, _:Thm.thm) = isSubstring str_pat name;
    3.70 +
    3.71 +(* for elimination and destruction rules, we must check if the major premise
    3.72 +   matches with one of the assumptions in the top subgoal, but we must 
    3.73 +   additionally make sure that we tell elim/dest apart, using thm_check_fun *)
    3.74 +fun elim_dest_filter thm_check_fun sg goal =
    3.75 +  let
    3.76 +    val elims_extract = (fn thm => if Thm.no_prems thm then [] else [thm],
    3.77 +                       rem_top_c o hd o Logic.strip_imp_prems);
    3.78 +
    3.79 +    (* assumptions of the top subgoal *)
    3.80 +    val prems = map rem_top_c (Logic.prems_of_goal goal 1);  
    3.81 +    
    3.82 +    fun prem_matches_name_thm prems (name_thm as (name,thm)) =
    3.83 +        List.exists
    3.84 +        (fn p => PureThy.is_matching_thm elims_extract sg p name_thm
    3.85 +                andalso (thm_check_fun thm)) prems;
    3.86 +  in
    3.87 +    prem_matches_name_thm prems      
    3.88 +  end;
    3.89 +
    3.90 +(* ------------</filter constructions> *)
    3.91 +
    3.92 +(* collect all the Var statements in a term *)
    3.93 +fun vars_of_term (Const _) = []
    3.94 +  | vars_of_term (Free _) = []
    3.95 +  | vars_of_term (Bound _) = []
    3.96 +  | vars_of_term (Abs (_,_,t)) = vars_of_term t
    3.97 +  | vars_of_term (v as (Var _)) = [v]
    3.98 +  | vars_of_term (x $ y) = vars_of_term x @ (vars_of_term y);
    3.99 +
   3.100 +(* elimination rule: conclusion is a Var and 
   3.101 +   no Var in the conclusion appears in the major premise
   3.102 +   Note: only makes sense if the major premise already matched the assumption 
   3.103 +         of some goal! *)
   3.104 +fun is_elim_rule thm =
   3.105 +  let
   3.106 +    val {prop, ...} = rep_thm thm;
   3.107 +    val concl = rem_top_c (Logic.strip_imp_concl prop);
   3.108 +    val major_prem = hd (Logic.strip_imp_prems prop);
   3.109 +    val prem_vars = distinct (vars_of_term major_prem);
   3.110 +    val concl_vars = distinct (vars_of_term concl);
   3.111 +  in
   3.112 +    Term.is_Var concl andalso ((prem_vars inter concl_vars) = [])
   3.113 +  end;
   3.114 +
   3.115 +fun crit2str (Name name) = "name:" ^ name
   3.116 +  | crit2str Elim = "elim"
   3.117 +  | crit2str Intro = "intro"
   3.118 +  | crit2str Rewrite = "rewrite"
   3.119 +  | crit2str Dest = "dest"
   3.120 +  | crit2str (Pattern x) = x;
   3.121 +
   3.122 +val criteria_to_str =
   3.123 +  let
   3.124 +    fun criterion_to_str ( true, ct) = "+ :   " ^ crit2str ct
   3.125 +      | criterion_to_str (false, ct) = "- :   " ^ crit2str ct
   3.126 +  in 
   3.127 +    map criterion_to_str 
   3.128 +  end;
   3.129 +
   3.130 +fun make_filter _ _ (Name name) = str_name_pat_to_filter name
   3.131 +  | make_filter sg _ (Pattern p) = str_term_pat_to_filter sg p
   3.132 +  (* beyond this point, only criteria requiring a goal! *)
   3.133 +  | make_filter _ NONE c =
   3.134 +      error ("Need to have a current goal to use " ^ (crit2str c))
   3.135 +  | make_filter sg (SOME goal) Elim =
   3.136 +      elim_dest_filter is_elim_rule sg goal
   3.137 +  | make_filter sg (SOME goal) Dest =
   3.138 +      (* in this case all that is not elim rule is dest *)
   3.139 +      elim_dest_filter (not o is_elim_rule) sg goal
   3.140 +  | make_filter sg (SOME goal) Intro =
   3.141 +    let
   3.142 +      (* filter by checking conclusion of theorem against conclusion of goal *)
   3.143 +      fun intros_extract () = (single, rem_top_c o Logic.strip_imp_concl);
   3.144 +      val concl = rem_top_c (Logic.concl_of_goal goal 1);
   3.145 +    in
   3.146 +      (fn name_thm => 
   3.147 +            PureThy.is_matching_thm (intros_extract ()) sg concl name_thm)
   3.148 +    end
   3.149 +  | make_filter _ _ c =
   3.150 +      error (crit2str c ^ " unimplemented");
   3.151 +  (* XXX: searching for rewrites currently impossible since we'd need
   3.152 +          a simplifier, which is included *after* Pure *)
   3.153 +
   3.154 +(* create filters ... convert negative ones to positive ones *)
   3.155 +fun make_filters sg opt_goal =
   3.156 +    map (fn (b,sc) => (if b then I else not) o (make_filter sg opt_goal sc));
   3.157 +
   3.158 +fun print_thms_containing ctxt opt_goal opt_limit criteria =
   3.159    let
   3.160      val prt_term = pretty_term ctxt;
   3.161      val prt_fact = pretty_fact ctxt;
   3.162 +    val ss = criteria_to_str criteria;
   3.163  
   3.164 -    (* theorems from the theory and its ancestors *)
   3.165 +    (* facts from the theory and its ancestors *)
   3.166      val thy = theory_of ctxt;
   3.167      val sg1 = Theory.sign_of thy;
   3.168      val all_thys = thy :: (Theory.ancestors_of thy)
   3.169 -    val thms1 = List.concat (map PureThy.thms_with_names_of all_thys);
   3.170 -    val facts1 =
   3.171 -      PureThy.find_theorems sg1 thms1 ss;
   3.172 +    val facts1 = List.concat (map PureThy.thms_with_names_of all_thys);
   3.173 +    val filters1 = make_filters sg1 opt_goal criteria;
   3.174 +    val matches1 = PureThy.find_theorems facts1 filters1;
   3.175  
   3.176 -    (* theorems from the local context *)
   3.177 +    (* facts from the local context *)
   3.178      val sg2 = sign_of ctxt;
   3.179 -    val thms2 = local_facts ctxt;
   3.180 -    val facts2 = 
   3.181 -      PureThy.find_theorems sg2 thms2 ss;
   3.182 +    val facts2 = local_facts ctxt;
   3.183 +    val filters2 = make_filters sg2 opt_goal criteria;
   3.184 +    val matches2 = PureThy.find_theorems facts2 filters2;
   3.185      
   3.186      (* combine them, use a limit, then print *)
   3.187 -    val facts = facts1 @ facts2; 
   3.188 -    val len = length facts;
   3.189 +    val matches = matches1 @ matches2;
   3.190 +    val len = length matches;
   3.191      val limit = getOpt (opt_limit, ! thms_containing_limit);
   3.192      val count = Int.min (limit, len);
   3.193      
   3.194 @@ -1503,13 +1638,14 @@
   3.195                  " theorems (" ^ (Int.toString count) ^ " displayed):"), 
   3.196              Pretty.fbrk]);
   3.197    in
   3.198 -    if null facts then
   3.199 +    if null matches then
   3.200        warning "find_theorems: nothing found"
   3.201      else 
   3.202 -        Pretty.writeln header;
   3.203 -        ((if len <= limit then [] else [Pretty.str "..."]) @
   3.204 -        map (prt_fact) (Library.drop (len - limit, facts))) |> 
   3.205 -            Pretty.chunks |> Pretty.writeln
   3.206 +      Pretty.writeln header;
   3.207 +      ((if len <= limit then [] else [Pretty.str "..."]) @
   3.208 +      map (prt_fact) (Library.drop (len - limit, matches))) |> 
   3.209 +        Pretty.chunks |> Pretty.writeln
   3.210    end;
   3.211  
   3.212  end;
   3.213 +
     4.1 --- a/src/Pure/proof_general.ML	Mon May 16 09:34:20 2005 +0200
     4.2 +++ b/src/Pure/proof_general.ML	Mon May 16 09:35:05 2005 +0200
     4.3 @@ -372,8 +372,11 @@
     4.4  
     4.5  (* misc commands for ProofGeneral/isa *)
     4.6  
     4.7 +(* PG/isa mode does not go through the Isar parser, hence we 
     4.8 +   interpret everything as term pattern only *)
     4.9  fun thms_containing ss =
    4.10 -  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE ss;
    4.11 +  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE NONE 
    4.12 +    (map (fn s => (true, ProofContext.Pattern s)) ss);
    4.13  
    4.14  val welcome = priority o Session.welcome;
    4.15  val help = welcome;
     5.1 --- a/src/Pure/pure_thy.ML	Mon May 16 09:34:20 2005 +0200
     5.2 +++ b/src/Pure/pure_thy.ML	Mon May 16 09:35:05 2005 +0200
     5.3 @@ -33,10 +33,12 @@
     5.4    val select_thm: thmref -> thm list -> thm list
     5.5    val cond_extern_thm_sg: Sign.sg -> string -> xstring
     5.6    val thms_containing: theory -> string list * string list -> (string * thm list) list
     5.7 -  val find_theorems: Sign.sg -> (string * thm list) list -> string list -> (string * thm list) list 
     5.8 +  val find_theorems: ('a * 'b list) list -> ('a * 'b -> bool) list -> ('a * 'b list) list
     5.9    val thms_containing_consts: theory -> string list -> (string * thm) list
    5.10    val find_matching_thms: (thm -> thm list) * (term -> term)
    5.11          -> theory -> term -> (string * thm) list
    5.12 +  val is_matching_thm: (thm -> thm list) * (term -> term)
    5.13 +        -> Sign.sg -> term -> (string * thm) -> bool
    5.14    val find_intros: theory -> term -> (string * thm) list
    5.15    val find_intros_goal : theory -> thm -> int -> (string * thm) list
    5.16    val find_elims : theory -> term -> (string * thm) list
    5.17 @@ -252,46 +254,29 @@
    5.18    thms_containing thy (consts, []) |> map #2 |> List.concat
    5.19    |> map (fn th => (Thm.name_of_thm th, th))
    5.20  
    5.21 -(* find_theorems - finding theorems by matching on a series of subterms  *)
    5.22 -
    5.23 -(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into
    5.24 -    a term with all free variables made schematic *)
    5.25 -fun str_pattern_to_term sg str_pattern =
    5.26 -  let
    5.27 -    (* pattern as term with dummies as Consts *)
    5.28 -    val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) 
    5.29 -                       |> Thm.term_of; 
    5.30 -    (* with dummies as Vars *)
    5.31 -    val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern));
    5.32 -  in
    5.33 -    (* with schematic vars *)
    5.34 -    #1 (Type.varify (v_pattern, []))
    5.35 -  end;
    5.36 +(* Searching based on filters *)
    5.37 +(* a filter must only take a (name:string, theorem:Thm.thm) and return true
    5.38 +   if it finds a match, false if it doesn't *)
    5.39  
    5.40 -(* find all thms such that for each returned thm, all given 
    5.41 -    propositions are subterms of it *)
    5.42 -fun thms_matching_patterns tsign (pat::pats) thms = 
    5.43 -    let 
    5.44 -        fun match_single pattern thm = 
    5.45 -            Pattern.matches_subterm tsign (pat, Thm.prop_of thm);
    5.46 -    in
    5.47 -        thms_matching_patterns tsign pats
    5.48 -            (List.filter (match_single pat) thms)
    5.49 -    end
    5.50 -  | thms_matching_patterns _ _ thms = thms; 
    5.51 +(* given facts and filters, find all facts in which at least one theorem 
    5.52 +   matches on ALL filters *)
    5.53 +fun find_theorems facts filters =
    5.54 +  let
    5.55 +    (* break fact up into theorems, but associate them with the name of this 
    5.56 +       fact, so that filters looking by name will only consider the fact's
    5.57 +       name *)
    5.58 +    fun fact_to_names_thms (name, thms) =
    5.59 +      map (fn thm => (name, thm)) thms;
    5.60  
    5.61 -(* facts are pairs of theorem name and a list of its thms *)
    5.62 -fun find_theorems sg facts str_patterns =
    5.63 -  let
    5.64 -    val typesg = Sign.tsig_of sg;
    5.65 -    
    5.66 -    (* the patterns we will be looking for *)
    5.67 -    val patterns = map (str_pattern_to_term sg) str_patterns;
    5.68 +    (* all filters return true when applied to a named theorem *)
    5.69 +    fun match_all_filters filters name_thm =
    5.70 +      List.all (fn filter => filter name_thm) filters;
    5.71  
    5.72 -    (* we are interested in theorems which have one or more thms for which
    5.73 -       all patterns are subterms *)
    5.74 -    fun matches (_, thms) = 
    5.75 -        (not o null o (thms_matching_patterns typesg patterns)) thms
    5.76 +    (* at least one theorem in this fact which matches all filters *)
    5.77 +    fun fact_matches_filters filters fact =
    5.78 +      List.exists (match_all_filters filters) (fact_to_names_thms fact);
    5.79 +
    5.80 +    fun matches x = (fact_matches_filters filters x)
    5.81    in
    5.82      List.filter matches facts
    5.83    end;
    5.84 @@ -347,6 +332,13 @@
    5.85  
    5.86    in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
    5.87  
    5.88 +(* like find_matching_thms, but for one named theorem only *)
    5.89 +fun is_matching_thm extract sg prop name_thm =
    5.90 +  (case top_const prop of NONE => false
    5.91 +   | SOME c => 
    5.92 +      not ([] = select_match(c,prop, sg,[name_thm],extract)));
    5.93 +
    5.94 +
    5.95  fun find_matching_thms extract thy prop =
    5.96    (case top_const prop of NONE => []
    5.97     | SOME c => let val thms = thms_containing_consts thy [c]