src/Pure/Isar/find_theorems.ML
changeset 16486 1a12cdb6ee6b
parent 16088 f084ba24de29
child 16895 df67fc190e06
equal deleted inserted replaced
16485:77ae3bfa8b76 16486:1a12cdb6ee6b
    36 
    36 
    37 fun read_criterion _ (Name name) = Name name
    37 fun read_criterion _ (Name name) = Name name
    38   | read_criterion _ Intro = Intro
    38   | read_criterion _ Intro = Intro
    39   | read_criterion _ Elim = Elim
    39   | read_criterion _ Elim = Elim
    40   | read_criterion _ Dest = Dest
    40   | read_criterion _ Dest = Dest
    41   | read_criterion ctxt (Simp str) = 
    41   | read_criterion ctxt (Simp str) =
    42       Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
    42       Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
    43   | read_criterion ctxt (Pattern str) =
    43   | read_criterion ctxt (Pattern str) =
    44       Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
    44       Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
    45 
    45 
    46 fun pretty_criterion ctxt (b, c) =
    46 fun pretty_criterion ctxt (b, c) =
    68 fun is_matching_thm (extract_thms, extract_term) ctxt po obj thm =
    68 fun is_matching_thm (extract_thms, extract_term) ctxt po obj thm =
    69   let
    69   let
    70     val sg = ProofContext.sign_of ctxt;
    70     val sg = ProofContext.sign_of ctxt;
    71     val tsig = Sign.tsig_of sg;
    71     val tsig = Sign.tsig_of sg;
    72 
    72 
    73     val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;    
    73     val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;
    74 
    74 
    75     fun matches pat = 
    75     fun matches pat =
    76       is_nontrivial pat andalso 
    76       is_nontrivial pat andalso
    77       Pattern.matches tsig (if po then (pat,obj) else (obj,pat))
    77       Pattern.matches tsig (if po then (pat,obj) else (obj,pat))
    78       handle Pattern.MATCH => false;
    78       handle Pattern.MATCH => false;
    79 
    79 
    80     val match_thm = matches o extract_term o Thm.prop_of
    80     val match_thm = matches o extract_term o Thm.prop_of
    81   in       
    81   in
    82     List.exists match_thm (extract_thms thm)
    82     List.exists match_thm (extract_thms thm)
    83   end;
    83   end;
    84 
    84 
    85 
    85 
    86 (* filter_name *)
    86 (* filter_name *)
    91   else if String.substring (str, 0, String.size pat) = pat then true
    91   else if String.substring (str, 0, String.size pat) = pat then true
    92   else is_substring pat (String.extract (str, 1, NONE));
    92   else is_substring pat (String.extract (str, 1, NONE));
    93 
    93 
    94 (*filter that just looks for a string in the name,
    94 (*filter that just looks for a string in the name,
    95   substring match only (no regexps are performed)*)
    95   substring match only (no regexps are performed)*)
    96 fun filter_name str_pat ((name, _), _) = is_substring str_pat name;
    96 fun filter_name str_pat (thmref, _) = is_substring str_pat (PureThy.name_of_thmref thmref);
    97 
    97 
    98 
    98 
    99 (* filter intro/elim/dest rules *)
    99 (* filter intro/elim/dest rules *)
   100 
   100 
   101 local
   101 local
   119     val extract_elim =
   119     val extract_elim =
   120      (fn thm => if Thm.no_prems thm then [] else [thm],
   120      (fn thm => if Thm.no_prems thm then [] else [thm],
   121       hd o Logic.strip_imp_prems);
   121       hd o Logic.strip_imp_prems);
   122     val prems = Logic.prems_of_goal goal 1;
   122     val prems = Logic.prems_of_goal goal 1;
   123   in
   123   in
   124     prems |> 
   124     prems |>
   125     List.exists (fn prem => 
   125     List.exists (fn prem =>
   126       is_matching_thm extract_elim ctxt true prem thm
   126       is_matching_thm extract_elim ctxt true prem thm
   127       andalso (check_thm ctxt) thm)
   127       andalso (check_thm ctxt) thm)
   128   end;
   128   end;
   129 
   129 
   130 in
   130 in