src/Pure/pure_thy.ML
changeset 15964 f2074e12d1d4
parent 15884 89124b6752e5
child 15975 cc4821a9f1b1
equal deleted inserted replaced
15963:5b70f789e079 15964:f2074e12d1d4
    31   val get_thms_closure: theory -> thmref -> thm list
    31   val get_thms_closure: theory -> thmref -> thm list
    32   val single_thm: string -> thm list -> thm
    32   val single_thm: string -> thm list -> thm
    33   val select_thm: thmref -> thm list -> thm list
    33   val select_thm: thmref -> thm list -> thm list
    34   val cond_extern_thm_sg: Sign.sg -> string -> xstring
    34   val cond_extern_thm_sg: Sign.sg -> string -> xstring
    35   val thms_containing: theory -> string list * string list -> (string * thm list) list
    35   val thms_containing: theory -> string list * string list -> (string * thm list) list
    36   val find_theorems: Sign.sg -> (string * thm list) list -> string list -> (string * thm list) list 
    36   val find_theorems: ('a * 'b list) list -> ('a * 'b -> bool) list -> ('a * 'b list) list
    37   val thms_containing_consts: theory -> string list -> (string * thm) list
    37   val thms_containing_consts: theory -> string list -> (string * thm) list
    38   val find_matching_thms: (thm -> thm list) * (term -> term)
    38   val find_matching_thms: (thm -> thm list) * (term -> term)
    39         -> theory -> term -> (string * thm) list
    39         -> theory -> term -> (string * thm) list
       
    40   val is_matching_thm: (thm -> thm list) * (term -> term)
       
    41         -> Sign.sg -> term -> (string * thm) -> bool
    40   val find_intros: theory -> term -> (string * thm) list
    42   val find_intros: theory -> term -> (string * thm) list
    41   val find_intros_goal : theory -> thm -> int -> (string * thm) list
    43   val find_intros_goal : theory -> thm -> int -> (string * thm) list
    42   val find_elims : theory -> term -> (string * thm) list
    44   val find_elims : theory -> term -> (string * thm) list
    43   val hide_thms: bool -> string list -> theory -> theory
    45   val hide_thms: bool -> string list -> theory -> theory
    44   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
    46   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
   250 
   252 
   251 fun thms_containing_consts thy consts =
   253 fun thms_containing_consts thy consts =
   252   thms_containing thy (consts, []) |> map #2 |> List.concat
   254   thms_containing thy (consts, []) |> map #2 |> List.concat
   253   |> map (fn th => (Thm.name_of_thm th, th))
   255   |> map (fn th => (Thm.name_of_thm th, th))
   254 
   256 
   255 (* find_theorems - finding theorems by matching on a series of subterms  *)
   257 (* Searching based on filters *)
   256 
   258 (* a filter must only take a (name:string, theorem:Thm.thm) and return true
   257 (* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into
   259    if it finds a match, false if it doesn't *)
   258     a term with all free variables made schematic *)
   260 
   259 fun str_pattern_to_term sg str_pattern =
   261 (* given facts and filters, find all facts in which at least one theorem 
       
   262    matches on ALL filters *)
       
   263 fun find_theorems facts filters =
   260   let
   264   let
   261     (* pattern as term with dummies as Consts *)
   265     (* break fact up into theorems, but associate them with the name of this 
   262     val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) 
   266        fact, so that filters looking by name will only consider the fact's
   263                        |> Thm.term_of; 
   267        name *)
   264     (* with dummies as Vars *)
   268     fun fact_to_names_thms (name, thms) =
   265     val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern));
   269       map (fn thm => (name, thm)) thms;
   266   in
   270 
   267     (* with schematic vars *)
   271     (* all filters return true when applied to a named theorem *)
   268     #1 (Type.varify (v_pattern, []))
   272     fun match_all_filters filters name_thm =
   269   end;
   273       List.all (fn filter => filter name_thm) filters;
   270 
   274 
   271 (* find all thms such that for each returned thm, all given 
   275     (* at least one theorem in this fact which matches all filters *)
   272     propositions are subterms of it *)
   276     fun fact_matches_filters filters fact =
   273 fun thms_matching_patterns tsign (pat::pats) thms = 
   277       List.exists (match_all_filters filters) (fact_to_names_thms fact);
   274     let 
   278 
   275         fun match_single pattern thm = 
   279     fun matches x = (fact_matches_filters filters x)
   276             Pattern.matches_subterm tsign (pat, Thm.prop_of thm);
       
   277     in
       
   278         thms_matching_patterns tsign pats
       
   279             (List.filter (match_single pat) thms)
       
   280     end
       
   281   | thms_matching_patterns _ _ thms = thms; 
       
   282 
       
   283 (* facts are pairs of theorem name and a list of its thms *)
       
   284 fun find_theorems sg facts str_patterns =
       
   285   let
       
   286     val typesg = Sign.tsig_of sg;
       
   287     
       
   288     (* the patterns we will be looking for *)
       
   289     val patterns = map (str_pattern_to_term sg) str_patterns;
       
   290 
       
   291     (* we are interested in theorems which have one or more thms for which
       
   292        all patterns are subterms *)
       
   293     fun matches (_, thms) = 
       
   294         (not o null o (thms_matching_patterns typesg patterns)) thms
       
   295   in
   280   in
   296     List.filter matches facts
   281     List.filter matches facts
   297   end;
   282   end;
   298 
   283 
   299 (* intro/elim theorems *)
   284 (* intro/elim theorems *)
   344                                 else sels)
   329                                 else sels)
   345            end
   330            end
   346         | select([],sels) = sels
   331         | select([],sels) = sels
   347 
   332 
   348   in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
   333   in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
       
   334 
       
   335 (* like find_matching_thms, but for one named theorem only *)
       
   336 fun is_matching_thm extract sg prop name_thm =
       
   337   (case top_const prop of NONE => false
       
   338    | SOME c => 
       
   339       not ([] = select_match(c,prop, sg,[name_thm],extract)));
       
   340 
   349 
   341 
   350 fun find_matching_thms extract thy prop =
   342 fun find_matching_thms extract thy prop =
   351   (case top_const prop of NONE => []
   343   (case top_const prop of NONE => []
   352    | SOME c => let val thms = thms_containing_consts thy [c]
   344    | SOME c => let val thms = thms_containing_consts thy [c]
   353                in select_match(c,prop,Theory.sign_of thy,thms,extract) end)
   345                in select_match(c,prop,Theory.sign_of thy,thms,extract) end)