src/Pure/Isar/proof_context.ML
changeset 15964 f2074e12d1d4
parent 15884 89124b6752e5
child 15966 73cf5ef8ed20
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 16 09:34:20 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 16 09:35:05 2005 +0200
     1.3 @@ -155,7 +155,9 @@
     1.4    val prems_limit: int ref
     1.5    val pretty_asms: context -> Pretty.T list
     1.6    val pretty_context: context -> Pretty.T list
     1.7 -  val print_thms_containing: context -> int option -> string list -> unit
     1.8 +  datatype search_criterion = Intro | Elim  | Dest | Rewrite |
     1.9 +                              Pattern of string | Name of string;
    1.10 +  val print_thms_containing: context -> term option -> int option -> (bool * search_criterion) list -> unit
    1.11  end;
    1.12  
    1.13  signature PRIVATE_PROOF_CONTEXT =
    1.14 @@ -171,6 +173,8 @@
    1.15  structure ProofContext: PRIVATE_PROOF_CONTEXT =
    1.16  struct
    1.17  
    1.18 +datatype search_criterion = Intro | Elim | Dest | Rewrite |
    1.19 +                          Pattern of string | Name of string;
    1.20  
    1.21  (** datatype context **)
    1.22  
    1.23 @@ -1470,28 +1474,159 @@
    1.24      (* things like "prems" can occur twice under some circumstances *)
    1.25      gen_distinct eq_fst (FactIndex.find ([],[]) index);
    1.26  
    1.27 -fun print_thms_containing ctxt opt_limit ss =
    1.28 +fun isSubstring pat str = 
    1.29 +  if String.size pat = 0 then true
    1.30 +  else if String.size pat > String.size str then false
    1.31 +  else if String.substring (str, 0, String.size pat) = pat then true
    1.32 +  else isSubstring pat (String.extract (str, 1, NONE));
    1.33 +
    1.34 +(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into
    1.35 +    a term with all free variables made schematic *)
    1.36 +fun str_pattern_to_term sg str_pattern =
    1.37 +  let
    1.38 +    (* pattern as term with dummies as Consts *)
    1.39 +    val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) 
    1.40 +                       |> Thm.term_of; 
    1.41 +    (* with dummies as Vars *)
    1.42 +    val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern));
    1.43 +  in
    1.44 +    (* with schematic vars *)
    1.45 +    #1 (Type.varify (v_pattern, []))
    1.46 +  end;
    1.47 +
    1.48 +(* alternate rem_top which checks for a Trueprop, unlike that in PureThy *)
    1.49 +fun rem_top_c (Term.Const ("Trueprop", _)  $ t) = t
    1.50 +  | rem_top_c _ = Bound 0;
    1.51 +
    1.52 +(* ---------- search filter contructions go here *)
    1.53 +
    1.54 +(* terms supplied in string form as patterns *)
    1.55 +fun str_term_pat_to_filter sg str_pat = 
    1.56 +  let
    1.57 +    val tsig = Sign.tsig_of sg;
    1.58 +    val pat = str_pattern_to_term sg str_pat;
    1.59 +    
    1.60 +    (* must qualify type so ML doesn't go and replace it with a concrete one *)
    1.61 +    fun name_thm_matches_pattern tsig pat (_:string, thm) =
    1.62 +      Pattern.matches_subterm tsig (pat, Thm.prop_of thm);
    1.63 +  in
    1.64 +    name_thm_matches_pattern (Sign.tsig_of sg) pat
    1.65 +  end;
    1.66 + 
    1.67 +(* create filter that just looks for a string in the name,
    1.68 +   substring match only (no regexps are performed) *)
    1.69 +fun str_name_pat_to_filter str_pat (name, _:Thm.thm) = isSubstring str_pat name;
    1.70 +
    1.71 +(* for elimination and destruction rules, we must check if the major premise
    1.72 +   matches with one of the assumptions in the top subgoal, but we must 
    1.73 +   additionally make sure that we tell elim/dest apart, using thm_check_fun *)
    1.74 +fun elim_dest_filter thm_check_fun sg goal =
    1.75 +  let
    1.76 +    val elims_extract = (fn thm => if Thm.no_prems thm then [] else [thm],
    1.77 +                       rem_top_c o hd o Logic.strip_imp_prems);
    1.78 +
    1.79 +    (* assumptions of the top subgoal *)
    1.80 +    val prems = map rem_top_c (Logic.prems_of_goal goal 1);  
    1.81 +    
    1.82 +    fun prem_matches_name_thm prems (name_thm as (name,thm)) =
    1.83 +        List.exists
    1.84 +        (fn p => PureThy.is_matching_thm elims_extract sg p name_thm
    1.85 +                andalso (thm_check_fun thm)) prems;
    1.86 +  in
    1.87 +    prem_matches_name_thm prems      
    1.88 +  end;
    1.89 +
    1.90 +(* ------------</filter constructions> *)
    1.91 +
    1.92 +(* collect all the Var statements in a term *)
    1.93 +fun vars_of_term (Const _) = []
    1.94 +  | vars_of_term (Free _) = []
    1.95 +  | vars_of_term (Bound _) = []
    1.96 +  | vars_of_term (Abs (_,_,t)) = vars_of_term t
    1.97 +  | vars_of_term (v as (Var _)) = [v]
    1.98 +  | vars_of_term (x $ y) = vars_of_term x @ (vars_of_term y);
    1.99 +
   1.100 +(* elimination rule: conclusion is a Var and 
   1.101 +   no Var in the conclusion appears in the major premise
   1.102 +   Note: only makes sense if the major premise already matched the assumption 
   1.103 +         of some goal! *)
   1.104 +fun is_elim_rule thm =
   1.105 +  let
   1.106 +    val {prop, ...} = rep_thm thm;
   1.107 +    val concl = rem_top_c (Logic.strip_imp_concl prop);
   1.108 +    val major_prem = hd (Logic.strip_imp_prems prop);
   1.109 +    val prem_vars = distinct (vars_of_term major_prem);
   1.110 +    val concl_vars = distinct (vars_of_term concl);
   1.111 +  in
   1.112 +    Term.is_Var concl andalso ((prem_vars inter concl_vars) = [])
   1.113 +  end;
   1.114 +
   1.115 +fun crit2str (Name name) = "name:" ^ name
   1.116 +  | crit2str Elim = "elim"
   1.117 +  | crit2str Intro = "intro"
   1.118 +  | crit2str Rewrite = "rewrite"
   1.119 +  | crit2str Dest = "dest"
   1.120 +  | crit2str (Pattern x) = x;
   1.121 +
   1.122 +val criteria_to_str =
   1.123 +  let
   1.124 +    fun criterion_to_str ( true, ct) = "+ :   " ^ crit2str ct
   1.125 +      | criterion_to_str (false, ct) = "- :   " ^ crit2str ct
   1.126 +  in 
   1.127 +    map criterion_to_str 
   1.128 +  end;
   1.129 +
   1.130 +fun make_filter _ _ (Name name) = str_name_pat_to_filter name
   1.131 +  | make_filter sg _ (Pattern p) = str_term_pat_to_filter sg p
   1.132 +  (* beyond this point, only criteria requiring a goal! *)
   1.133 +  | make_filter _ NONE c =
   1.134 +      error ("Need to have a current goal to use " ^ (crit2str c))
   1.135 +  | make_filter sg (SOME goal) Elim =
   1.136 +      elim_dest_filter is_elim_rule sg goal
   1.137 +  | make_filter sg (SOME goal) Dest =
   1.138 +      (* in this case all that is not elim rule is dest *)
   1.139 +      elim_dest_filter (not o is_elim_rule) sg goal
   1.140 +  | make_filter sg (SOME goal) Intro =
   1.141 +    let
   1.142 +      (* filter by checking conclusion of theorem against conclusion of goal *)
   1.143 +      fun intros_extract () = (single, rem_top_c o Logic.strip_imp_concl);
   1.144 +      val concl = rem_top_c (Logic.concl_of_goal goal 1);
   1.145 +    in
   1.146 +      (fn name_thm => 
   1.147 +            PureThy.is_matching_thm (intros_extract ()) sg concl name_thm)
   1.148 +    end
   1.149 +  | make_filter _ _ c =
   1.150 +      error (crit2str c ^ " unimplemented");
   1.151 +  (* XXX: searching for rewrites currently impossible since we'd need
   1.152 +          a simplifier, which is included *after* Pure *)
   1.153 +
   1.154 +(* create filters ... convert negative ones to positive ones *)
   1.155 +fun make_filters sg opt_goal =
   1.156 +    map (fn (b,sc) => (if b then I else not) o (make_filter sg opt_goal sc));
   1.157 +
   1.158 +fun print_thms_containing ctxt opt_goal opt_limit criteria =
   1.159    let
   1.160      val prt_term = pretty_term ctxt;
   1.161      val prt_fact = pretty_fact ctxt;
   1.162 +    val ss = criteria_to_str criteria;
   1.163  
   1.164 -    (* theorems from the theory and its ancestors *)
   1.165 +    (* facts from the theory and its ancestors *)
   1.166      val thy = theory_of ctxt;
   1.167      val sg1 = Theory.sign_of thy;
   1.168      val all_thys = thy :: (Theory.ancestors_of thy)
   1.169 -    val thms1 = List.concat (map PureThy.thms_with_names_of all_thys);
   1.170 -    val facts1 =
   1.171 -      PureThy.find_theorems sg1 thms1 ss;
   1.172 +    val facts1 = List.concat (map PureThy.thms_with_names_of all_thys);
   1.173 +    val filters1 = make_filters sg1 opt_goal criteria;
   1.174 +    val matches1 = PureThy.find_theorems facts1 filters1;
   1.175  
   1.176 -    (* theorems from the local context *)
   1.177 +    (* facts from the local context *)
   1.178      val sg2 = sign_of ctxt;
   1.179 -    val thms2 = local_facts ctxt;
   1.180 -    val facts2 = 
   1.181 -      PureThy.find_theorems sg2 thms2 ss;
   1.182 +    val facts2 = local_facts ctxt;
   1.183 +    val filters2 = make_filters sg2 opt_goal criteria;
   1.184 +    val matches2 = PureThy.find_theorems facts2 filters2;
   1.185      
   1.186      (* combine them, use a limit, then print *)
   1.187 -    val facts = facts1 @ facts2; 
   1.188 -    val len = length facts;
   1.189 +    val matches = matches1 @ matches2;
   1.190 +    val len = length matches;
   1.191      val limit = getOpt (opt_limit, ! thms_containing_limit);
   1.192      val count = Int.min (limit, len);
   1.193      
   1.194 @@ -1503,13 +1638,14 @@
   1.195                  " theorems (" ^ (Int.toString count) ^ " displayed):"), 
   1.196              Pretty.fbrk]);
   1.197    in
   1.198 -    if null facts then
   1.199 +    if null matches then
   1.200        warning "find_theorems: nothing found"
   1.201      else 
   1.202 -        Pretty.writeln header;
   1.203 -        ((if len <= limit then [] else [Pretty.str "..."]) @
   1.204 -        map (prt_fact) (Library.drop (len - limit, facts))) |> 
   1.205 -            Pretty.chunks |> Pretty.writeln
   1.206 +      Pretty.writeln header;
   1.207 +      ((if len <= limit then [] else [Pretty.str "..."]) @
   1.208 +      map (prt_fact) (Library.drop (len - limit, matches))) |> 
   1.209 +        Pretty.chunks |> Pretty.writeln
   1.210    end;
   1.211  
   1.212  end;
   1.213 +