# 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 =>