tuned;
authorwenzelm
Thu Dec 06 00:40:19 2001 +0100 (2001-12-06)
changeset 123992ba27248af7f
parent 12398 9c27f28c8f5a
child 12400 f12f95e216e0
tuned;
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Library/Multiset.thy
src/Pure/Isar/context_rules.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/HOL/Lattice/CompleteLattice.thy	Thu Dec 06 00:40:04 2001 +0100
     1.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Thu Dec 06 00:40:19 2001 +0100
     1.3 @@ -129,7 +129,7 @@
     1.4    also have "?a \<sqsubseteq> f ?a"
     1.5    proof
     1.6      from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
     1.7 -    thus "f ?a : ?H" ..
     1.8 +    thus "f ?a \<in> ?H" ..
     1.9    qed
    1.10    finally show "f ?a = ?a" .
    1.11  qed
     2.1 --- a/src/HOL/Library/Multiset.thy	Thu Dec 06 00:40:04 2001 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Thu Dec 06 00:40:19 2001 +0100
     2.3 @@ -1,8 +1,7 @@
     2.4  (*  Title:      HOL/Library/Multiset.thy
     2.5      ID:         $Id$
     2.6 -    Author:     Tobias Nipkow, TU Muenchen
     2.7 -    Author:     Markus Wenzel, TU Muenchen
     2.8 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.9 +    Author:     Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson
    2.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    2.11  *)
    2.12  
    2.13  header {*
    2.14 @@ -482,7 +481,7 @@
    2.15    {
    2.16      fix M M0 a
    2.17      assume M0: "M0 \<in> ?W"
    2.18 -      and wf_hyp: "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
    2.19 +      and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
    2.20        and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
    2.21      have "M0 + {#a#} \<in> ?W"
    2.22      proof (rule accI [of "M0 + {#a#}"])
    2.23 @@ -538,7 +537,7 @@
    2.24      from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
    2.25      proof induct
    2.26        fix a
    2.27 -      assume "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
    2.28 +      assume "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
    2.29        show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
    2.30        proof
    2.31          fix M assume "M \<in> ?W"
     3.1 --- a/src/Pure/Isar/context_rules.ML	Thu Dec 06 00:40:04 2001 +0100
     3.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Dec 06 00:40:19 2001 +0100
     3.3 @@ -14,7 +14,8 @@
     3.4    val netpair_bang: Proof.context -> netpair
     3.5    val netpair: Proof.context -> netpair
     3.6    val orderlist: ((int * int) * 'a) list -> 'a list
     3.7 -  val find_rules: Proof.context -> thm list -> term -> thm list list
     3.8 +  val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
     3.9 +  val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
    3.10    val print_global_rules: theory -> unit
    3.11    val print_local_rules: Proof.context -> unit
    3.12    val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    3.13 @@ -166,6 +167,8 @@
    3.14  val netpair = hd o tl o netpairs;
    3.15  
    3.16  
    3.17 +(* retrieving rules *)
    3.18 +
    3.19  fun untaglist [] = []
    3.20    | untaglist [(k : int * int, x)] = [x]
    3.21    | untaglist ((k, x) :: (rest as (k', x') :: _)) =
    3.22 @@ -174,16 +177,22 @@
    3.23  
    3.24  fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    3.25  fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
    3.26 -fun may_unify t net = map snd (orderlist_no_weight (Net.unify_term net t));
    3.27 +
    3.28 +fun may_unify weighted t net =
    3.29 +  map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
    3.30 +
    3.31 +fun find_erules _ [] = K []
    3.32 +  | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
    3.33 +fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
    3.34  
    3.35 -fun find_erules [] = K []
    3.36 -  | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
    3.37 -fun find_irules goal = may_unify (Logic.strip_assums_concl goal);
    3.38 +fun find_rules_netpair weighted facts goal (inet, enet) =
    3.39 +  find_erules weighted facts enet @ find_irules weighted goal inet;
    3.40  
    3.41 -fun find_rules ctxt facts goal =
    3.42 -  map (fn (inet, enet) => find_erules facts enet @ find_irules goal inet) (netpairs ctxt);
    3.43 +fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
    3.44  
    3.45  
    3.46 +(* wrappers *)
    3.47 +
    3.48  fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    3.49    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
    3.50  
     4.1 --- a/src/Pure/Isar/method.ML	Thu Dec 06 00:40:04 2001 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Thu Dec 06 00:40:19 2001 +0100
     4.3 @@ -272,7 +272,7 @@
     4.4    let
     4.5      val rules =
     4.6        if not (null arg_rules) then arg_rules
     4.7 -      else flat (ContextRules.find_rules ctxt facts goal)
     4.8 +      else flat (ContextRules.find_rules false facts goal ctxt)
     4.9    in trace ctxt rules; tac rules facts i end);
    4.10  
    4.11  fun meth tac x = METHOD (HEADGOAL o tac x);