# HG changeset patch # User wenzelm # Date 1116782776 -7200 # Node ID 1da07ac337114f0222bb6ed183cd2db982b36d5a # Parent 31bd65f7b22ac287293c6fd29ecdcafa0d1abad8 added read_criterion/pretty_criterion; improved rule filters -- intro excludes elim rules; tuned output; tuned; diff -r 31bd65f7b22a -r 1da07ac33711 src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Sun May 22 19:26:15 2005 +0200 +++ b/src/Pure/Isar/find_theorems.ML Sun May 22 19:26:16 2005 +0200 @@ -13,10 +13,10 @@ val find_intros: Proof.context -> term -> (thmref * thm) list val find_intros_goal: Proof.context -> thm -> int -> (thmref * thm) list val find_elims: Proof.context -> term -> (thmref * thm) list - datatype search_criterion = - Name of string | Intro | Elim | Dest | Rewrite of string | Pattern of string + datatype 'term criterion = + Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term val print_theorems: Proof.context -> term option -> int option -> - (bool * search_criterion) list -> unit + (bool * string criterion) list -> unit end; structure FindTheorems: FIND_THEOREMS = @@ -101,17 +101,31 @@ (** search criteria **) -datatype search_criterion = - Name of string | Intro | Elim | Dest | Rewrite of string | Pattern of string; +datatype 'term criterion = + Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term; + +fun read_criterion _ (Name name) = Name name + | read_criterion _ Intro = Intro + | read_criterion _ Elim = Elim + | read_criterion _ Dest = Dest + | read_criterion ctxt (Rewrite str) = Rewrite (ProofContext.read_term ctxt str) + | read_criterion ctxt (Pattern str) = + Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str])); -fun string_of_crit (Name name) = "name: " ^ quote name - | string_of_crit Intro = "intro" - | string_of_crit Elim = "elim" - | string_of_crit Dest = "dest" - | string_of_crit (Rewrite s) = "rewrite: " ^ quote s - | string_of_crit (Pattern s) = quote s; - -fun string_of_criterion (b, c) = (if b then "" else "-") ^ string_of_crit c; +fun pretty_criterion ctxt (b, c) = + let + fun prfx s = if b then s else "-" ^ s; + in + (case c of + Name name => Pretty.str (prfx "name: " ^ quote name) + | Intro => Pretty.str (prfx "intro") + | Elim => Pretty.str (prfx "elim") + | Dest => Pretty.str (prfx "dest") + | Rewrite t => Pretty.block [Pretty.str (prfx "rewrite:"), Pretty.brk 1, + Pretty.quote (ProofContext.pretty_term ctxt t)] + | Pattern pat => Pretty.enclose (prfx " \"") "\"" + [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)]) + end; @@ -130,113 +144,118 @@ fun filter_name str_pat ((name, _), _) = is_substring str_pat name; -(* filter_intro *) +(* filter intro/elim/dest rules *) -(*checking conclusion of theorem against conclusion of goal*) -fun filter_intro ctxt goal = +local + +(*elimination rule: conclusion is a Var which does not appear in the major premise*) +fun is_elim ctxt thm = let - val extract_intro = (single, Logic.strip_imp_concl); - val concl = Logic.concl_of_goal goal 1; - in is_matching_thm extract_intro ctxt concl end; - + val sg = ProofContext.sign_of ctxt; + val prop = Thm.prop_of thm; + val concl = ObjectLogic.drop_judgment sg (Logic.strip_imp_concl prop); + val major_prem = Library.take (1, Logic.strip_imp_prems prop); + val prem_vars = Drule.vars_of_terms major_prem; + in + not (null major_prem) andalso + Term.is_Var concl andalso + not (Term.dest_Var concl mem prem_vars) + end; -(* filter_elim_dest *) - -(*for elimination and destruction rules, we must check if the major - premise matches with one of the assumptions in the top subgoal, but - we must additionally make sure that we tell elim/dest apart, using - check_thm (cf. is_elim_rule below)*) fun filter_elim_dest check_thm ctxt goal = let val extract_elim = (fn thm => if Thm.no_prems thm then [] else [thm], hd o Logic.strip_imp_prems); - val prems = Logic.prems_of_goal goal 1; in - fn fact => List.exists (fn prem => - is_matching_thm extract_elim ctxt prem fact andalso check_thm (#2 fact)) prems + fn fact => prems |> List.exists (fn prem => + is_matching_thm extract_elim ctxt prem fact + andalso (check_thm ctxt) (#2 fact)) end; -(*elimination rule: conclusion is a Var which does not appears in the - major premise*) -fun is_elim_rule thm = +in + +fun filter_intro ctxt goal = let - val prop = Thm.prop_of thm; - val concl = ObjectLogic.drop_judgment (Thm.sign_of_thm thm) (Logic.strip_imp_concl prop); - val major_prem = hd (Logic.strip_imp_prems prop); - val prem_vars = Drule.vars_of_terms [major_prem]; + val extract_intro = (single, Logic.strip_imp_concl); + val concl = Logic.concl_of_goal goal 1; in - Term.is_Var concl andalso not (Term.dest_Var concl mem prem_vars) + fn fact => is_matching_thm extract_intro ctxt concl fact + andalso not (is_elim ctxt (#2 fact)) end; +fun filter_elim ctxt = filter_elim_dest is_elim ctxt; +fun filter_dest ctxt = filter_elim_dest (not oo is_elim) ctxt; + +end; + (* filter_rewrite *) -fun filter_rewrite ctxt str = +fun filter_rewrite ctxt t = let val (_, {mk_rews = {mk, ...}, ...}) = MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt); val extract_rewrite = (mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); - in is_matching_thm extract_rewrite ctxt (ProofContext.read_term ctxt str) end; + in is_matching_thm extract_rewrite ctxt t end; (* filter_pattern *) -(*subterm pattern supplied as raw string*) -fun filter_pattern ctxt str = - let - val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); - val [pat] = ProofContext.read_term_pats TypeInfer.logicT ctxt [str]; +fun filter_pattern ctxt pat = + let val tsig = Sign.tsig_of (ProofContext.sign_of ctxt) in fn (_, thm) => Pattern.matches_subterm tsig (pat, Thm.prop_of thm) end; (* interpret criteria as filters *) +local + +fun err_no_goal c = + error ("Current goal required for " ^ c ^ " search criterion"); + fun filter_crit _ _ (Name name) = filter_name name + | filter_crit _ NONE Intro = err_no_goal "intro" + | filter_crit _ NONE Elim = err_no_goal "elim" + | filter_crit _ NONE Dest = err_no_goal "dest" + | filter_crit ctxt (SOME goal) Intro = filter_intro ctxt goal + | filter_crit ctxt (SOME goal) Elim = filter_elim ctxt goal + | filter_crit ctxt (SOME goal) Dest = filter_dest ctxt goal | filter_crit ctxt _ (Rewrite str) = filter_rewrite ctxt str - | filter_crit ctxt _ (Pattern str) = filter_pattern ctxt str - (*beyond this point, only criteria requiring a goal!*) - | filter_crit _ NONE c = - error ("Need to have a current goal to use " ^ string_of_crit c) - | filter_crit ctxt (SOME goal) Intro = filter_intro ctxt goal - | filter_crit ctxt (SOME goal) Elim = filter_elim_dest is_elim_rule ctxt goal - | filter_crit ctxt (SOME goal) Dest = - filter_elim_dest (not o is_elim_rule) ctxt goal; - (*in this case all that is not elim is dest*) + | filter_crit ctxt _ (Pattern str) = filter_pattern ctxt str; + +in fun filter_criterion ctxt opt_goal (b, c) = (if b then I else not) o filter_crit ctxt opt_goal c; fun all_filters filters = List.filter (fn x => List.all (fn f => f x) filters); +end; + (* print_theorems *) -fun print_theorems ctxt opt_goal opt_limit criteria = +fun print_theorems ctxt opt_goal opt_limit raw_criteria = let - fun prt_fact (thmref, thm) = - ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]); - val prt_crit = Pretty.str o string_of_criterion; + val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; + val filters = map (filter_criterion ctxt opt_goal) criteria; - val all_facts = find_thms ctxt ([], []); - val filters = map (filter_criterion ctxt opt_goal) criteria; - val matches = all_filters filters all_facts; - + val matches = all_filters filters (find_thms ctxt ([], [])); val len = length matches; val limit = if_none opt_limit (! thms_containing_limit); - val count = Int.min (limit, len); - val pruned = len <= limit; - val found = "found " ^ string_of_int len ^ " theorems" ^ - (if pruned then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":"; + fun prt_fact (thmref, thm) = + ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]); in - Pretty.big_list "searched for:" (map prt_crit criteria) :: + Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" :: (if null matches then [Pretty.str "nothing found"] else - [Pretty.str "", Pretty.str found] @ - (if pruned then [] else [Pretty.str "..."]) @ - map prt_fact (Library.drop (len - limit, matches))) + [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^ + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":"), + Pretty.str ""] @ + map prt_fact (Library.drop (len - limit, matches))) |> Pretty.chunks |> Pretty.writeln end;