# HG changeset patch
# User nipkow
# Date 1034585072 -7200
# Node ID 46ed3d042ba5444ae4439c2c90c7413c60636564
# Parent  430310b12c5b14fa27f9fc5a5d1bfbcd7359721a
Ported find_intro/elim to Isar.

diff -r 430310b12c5b -r 46ed3d042ba5 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -249,7 +249,7 @@
         val thms = flat (map (fn (s, ps) =>
             if s mem defnames then []
             else map (pair s o Some o fst) (filter_out (fn (p, _) =>
-              null (add_term_consts (p, []) inter cnames)) ps))
+              null (term_consts p inter cnames)) ps))
           (Symtab.dest (thms_of_proof Symtab.empty prf)))
       in Reconstruct.expand_proof sign thms end
   in
diff -r 430310b12c5b -r 46ed3d042ba5 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/goals.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -107,6 +107,7 @@
   val print_locales: theory -> unit
   val get_thm: theory -> xstring -> thm
   val get_thms: theory -> xstring -> thm list
+  val find_intros_goal : theory -> thm -> int -> (string * thm) list
   val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
     (string * string) list -> (string * string) list -> theory -> theory
   val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
@@ -899,9 +900,11 @@
 fun uresult () = !curr_mkresult (false, topthm());
 
 (*Get subgoal i from goal stack*)
-fun getgoal i = List.nth (prems_of (topthm()), i-1)
+fun get_goal st i = List.nth (prems_of st, i-1)
                 handle Subscript => error"getgoal: Goal number out of range";
 
+fun getgoal i = get_goal (topthm()) i;
+
 (*Return subgoal i's hypotheses as meta-level assumptions.
   For debugging uses of METAHYPS*)
 local exception GETHYPS of thm list
@@ -1134,93 +1137,40 @@
     (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
       [] => ()
     | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
-    PureThy.thms_containing thy (consts, [])
-    |> map #2 |> flat
-    |> map (fn th => (Thm.name_of_thm th, th))
+    PureThy.thms_containing_consts thy consts
   end;
 
-(*top_const: main constant, ignoring Trueprop*)
-fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
-  | top_const _ = None;
-
-val intro_const = top_const o concl_of;
-fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
-
-fun index_intros c = thms_containing [c] |> filter (fn (_, thm) => intro_const thm = Some c);
-fun index_elims c = thms_containing [c] |> filter (fn (_, thm) => elim_const thm = Some c);
-
 (*assume that parameters have unique names; reverse them for substitution*)
-fun goal_params i =
-  let val gi = getgoal i
+fun goal_params st i =
+  let val gi = get_goal st i
       val rfrees = rev(map Free (Logic.strip_params gi))
   in (gi,rfrees) end;
 
-fun concl_of_goal i =
-  let val (gi,rfrees) = goal_params i
+fun concl_of_goal st i =
+  let val (gi,rfrees) = goal_params st i
       val B = Logic.strip_assums_concl gi
   in subst_bounds(rfrees,B) end;
 
-fun prems_of_goal i =
-  let val (gi,rfrees) = goal_params i
+fun prems_of_goal st i =
+  let val (gi,rfrees) = goal_params st i
       val As = Logic.strip_assums_hyp gi
   in map (fn A => subst_bounds(rfrees,A)) As end;
 
-(*returns all those named_thms whose subterm extracted by extract can be
-  instantiated to obj; the list is sorted according to the number of premises
-  and the size of the required substitution.*)
-fun select_match(obj, signobj, named_thms, extract) =
-  let fun matches(prop, tsig) =
-            case extract prop of
-              None => false
-            | Some pat => Pattern.matches tsig (pat, obj);
-
-      fun substsize(prop, tsig) =
-            let val Some pat = extract prop
-                val (_,subst) = Pattern.match tsig (pat,obj)
-            in foldl op+
-                (0, map (fn (_,t) => size_of_term t) subst)
-            end
-
-      fun thm_ord ((p0,s0,_),(p1,s1,_)) =
-            prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
+fun find_intros_goal thy st i = PureThy.find_intros thy (concl_of_goal st i);
 
-      fun select((p as (_,thm))::named_thms, sels) =
-            let val {prop, sign, ...} = rep_thm thm
-            in select(named_thms,
-                      if Sign.subsig(sign, signobj) andalso
-                         matches(prop,#tsig(Sign.rep_sg signobj))
-                      then
-                        (nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
-                      else sels)
-            end
-        | select([],sels) = sels
-
-  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
-
-fun find_matching(prop,sign,index,extract) =
-  (case top_const prop of
-     Some c => select_match(prop,sign,index c,extract)
-   | _      => []);
-
-fun find_intros(prop,sign) =
-  find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
-
-fun find_elims sign prop =
-  let fun major prop = case Logic.strip_imp_prems prop of
-                         [] => None | p::_ => Some p
-  in find_matching(prop,sign,index_elims,major) end;
-
-fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
+fun findI i = find_intros_goal (theory_of_goal()) (topthm()) i;
 
 fun findEs i =
   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
-      val sign = #sign(rep_thm(topthm()))
-      val thmss = map (find_elims sign) (prems_of_goal i)
+      val prems = prems_of_goal (topthm()) i
+      val thy = theory_of_goal();
+      val thmss = map (PureThy.find_elims thy) prems
   in foldl (gen_union eq_nth) ([],thmss) end;
 
 fun findE i j =
-  let val sign = #sign(rep_thm(topthm()))
-  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
+  let val prems = prems_of_goal (topthm()) i
+      val thy = theory_of_goal();
+  in PureThy.find_elims thy (nth_elem(j-1, prems)) end;
 
 end;
 
diff -r 430310b12c5b -r 46ed3d042ba5 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/proof_general.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -14,6 +14,7 @@
   val inform_file_retracted: string -> unit
   val inform_file_processed: string -> unit
   val thms_containing: string list -> unit
+  val print_intros: unit -> unit
   val help: unit -> unit
   val show_context: unit -> theory
   val kill_goal: unit -> unit
@@ -247,6 +248,14 @@
 fun thms_containing ss =
   ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
 
+fun print_intros() =
+  let val proof_state = Toplevel.proof_of (Toplevel.get_state ())
+      val (ctxt,(_,st)) = Proof.get_goal proof_state
+      val prt_fact = ProofContext.pretty_fact ctxt
+      val thy = ProofContext.theory_of ctxt
+      val facts = map (apsnd single) (Goals.find_intros_goal thy st 1)
+  in map prt_fact (rev facts) |> Pretty.chunks |> Pretty.writeln end
+
 val welcome = priority o Session.welcome;
 val help = welcome;
 val show_context = Context.the_context;
diff -r 430310b12c5b -r 46ed3d042ba5 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/pure_thy.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -30,6 +30,9 @@
   val single_thm: string -> thm list -> thm
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
   val thms_containing: theory -> string list * string list -> (string * thm list) list
+  val thms_containing_consts: theory -> string list -> (string * thm) list
+  val find_intros: theory -> term -> (string * thm) list
+  val find_elims : theory -> term -> (string * thm) list
   val hide_thms: bool -> string list -> theory -> theory
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
   val smart_store_thms: (bstring * thm list) -> thm list
@@ -189,6 +192,65 @@
     |> flat
   end;
 
+fun thms_containing_consts thy consts =
+  thms_containing thy (consts, []) |> map #2 |> flat
+  |> map (fn th => (Thm.name_of_thm th, th))
+
+(* intro/elim theorems *)
+
+(* intro: given a goal state, find a suitable intro rule for some subgoal *)
+(* elim: given a theorem thm,
+         find a theorem whose major premise eliminates the conclusion of thm *)
+
+(*top_const: main constant, ignoring Trueprop *)
+fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
+  | top_const _ = None;
+
+val intro_const = top_const o concl_of;
+fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
+
+fun index_intros thy c = thms_containing_consts thy [c]
+  |> filter (fn (_, thm) => intro_const thm = Some c);
+fun index_elims thy c = thms_containing_consts thy [c]
+  |> filter (fn (_, thm) => elim_const thm = Some c);
+
+(*returns all those named_thms whose subterm extracted by extract can be
+  instantiated to obj; the list is sorted according to the number of premises
+  and the size of the required substitution.*)
+fun select_match(obj, signobj, named_thms, extract) =
+  let val tsig = Sign.tsig_of signobj
+      fun matches prop =
+            case extract prop of
+              None => false
+            | Some pat => Pattern.matches tsig (pat, obj);
+
+      fun substsize prop =
+            let val Some pat = extract prop
+                val (_,subst) = Pattern.match tsig (pat,obj)
+            in foldl op+ (0, map (size_of_term o snd) subst) end
+
+      fun thm_ord ((p0,s0,_),(p1,s1,_)) =
+            prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
+
+      fun select((p as (_,thm))::named_thms, sels) =
+            let val {prop, sign, ...} = rep_thm thm
+            in select(named_thms,
+                      if Sign.subsig(sign, signobj) andalso matches prop
+                      then (nprems_of thm,substsize prop,p)::sels
+                      else sels)
+            end
+        | select([],sels) = sels
+
+  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
+
+fun find_matching index extract thy prop =
+  (case top_const prop of None => []
+   | Some c => select_match(prop,Theory.sign_of thy,index thy c,extract))
+
+val find_intros = find_matching index_intros (Some o Logic.strip_imp_concl)
+
+val find_elims = find_matching index_elims
+  (fn prop => case Logic.strip_imp_prems prop of [] => None | p::_ => Some p)
 
 
 (** store theorems **)                    (*DESTRUCTIVE*)
diff -r 430310b12c5b -r 46ed3d042ba5 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/term.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -154,6 +154,7 @@
   val add_typ_varnames: typ * string list -> string list
   val add_term_classes: term * class list -> class list
   val add_term_consts: term * string list -> string list
+  val term_consts: term -> string list
   val add_term_frees: term * term list -> term list
   val term_frees: term -> term list
   val add_term_free_names: term * string list -> string list
@@ -793,6 +794,8 @@
   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   | add_term_consts (_, cs) = cs;
 
+fun term_consts t = add_term_consts(t,[]);
+
 fun exists_Const P t = let
         fun ex (Const c      ) = P c
         |   ex (t $ u        ) = ex t orelse ex u
diff -r 430310b12c5b -r 46ed3d042ba5 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/theory.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -410,7 +410,7 @@
     else
       (case overloading sg c_decl ty of
         NoOverloading =>
-          (add_deps (c, Term.add_term_consts (rhs, [])) deps
+          (add_deps (c, Term.term_consts rhs) deps
               handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess),
             def :: axms)
       | Useless =>