--- a/src/HOL/Lattice/CompleteLattice.thy Thu Dec 06 00:40:04 2001 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Thu Dec 06 00:40:19 2001 +0100
@@ -129,7 +129,7 @@
also have "?a \<sqsubseteq> f ?a"
proof
from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
- thus "f ?a : ?H" ..
+ thus "f ?a \<in> ?H" ..
qed
finally show "f ?a = ?a" .
qed
--- a/src/HOL/Library/Multiset.thy Thu Dec 06 00:40:04 2001 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Dec 06 00:40:19 2001 +0100
@@ -1,8 +1,7 @@
(* Title: HOL/Library/Multiset.thy
ID: $Id$
- Author: Tobias Nipkow, TU Muenchen
- Author: Markus Wenzel, TU Muenchen
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {*
@@ -482,7 +481,7 @@
{
fix M M0 a
assume M0: "M0 \<in> ?W"
- and wf_hyp: "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+ and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
have "M0 + {#a#} \<in> ?W"
proof (rule accI [of "M0 + {#a#}"])
@@ -538,7 +537,7 @@
from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
proof induct
fix a
- assume "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
+ assume "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
proof
fix M assume "M \<in> ?W"
--- a/src/Pure/Isar/context_rules.ML Thu Dec 06 00:40:04 2001 +0100
+++ b/src/Pure/Isar/context_rules.ML Thu Dec 06 00:40:19 2001 +0100
@@ -14,7 +14,8 @@
val netpair_bang: Proof.context -> netpair
val netpair: Proof.context -> netpair
val orderlist: ((int * int) * 'a) list -> 'a list
- val find_rules: Proof.context -> thm list -> term -> thm list list
+ val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
+ val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
val print_global_rules: theory -> unit
val print_local_rules: Proof.context -> unit
val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
@@ -166,6 +167,8 @@
val netpair = hd o tl o netpairs;
+(* retrieving rules *)
+
fun untaglist [] = []
| untaglist [(k : int * int, x)] = [x]
| untaglist ((k, x) :: (rest as (k', x') :: _)) =
@@ -174,16 +177,22 @@
fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
-fun may_unify t net = map snd (orderlist_no_weight (Net.unify_term net t));
+
+fun may_unify weighted t net =
+ map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
+
+fun find_erules _ [] = K []
+ | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
+fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
-fun find_erules [] = K []
- | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
-fun find_irules goal = may_unify (Logic.strip_assums_concl goal);
+fun find_rules_netpair weighted facts goal (inet, enet) =
+ find_erules weighted facts enet @ find_irules weighted goal inet;
-fun find_rules ctxt facts goal =
- map (fn (inet, enet) => find_erules facts enet @ find_irules goal inet) (netpairs ctxt);
+fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
+(* wrappers *)
+
fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
--- a/src/Pure/Isar/method.ML Thu Dec 06 00:40:04 2001 +0100
+++ b/src/Pure/Isar/method.ML Thu Dec 06 00:40:19 2001 +0100
@@ -272,7 +272,7 @@
let
val rules =
if not (null arg_rules) then arg_rules
- else flat (ContextRules.find_rules ctxt facts goal)
+ else flat (ContextRules.find_rules false facts goal ctxt)
in trace ctxt rules; tac rules facts i end);
fun meth tac x = METHOD (HEADGOAL o tac x);