1.1 --- a/src/Pure/drule.ML	Wed Apr 11 20:42:28 2012 +0200
     1.2 +++ b/src/Pure/drule.ML	Wed Apr 11 21:40:46 2012 +0200
     1.3 @@ -67,6 +67,8 @@
     1.4    val store_standard_thm: binding -> thm -> thm
     1.5    val store_thm_open: binding -> thm -> thm
     1.6    val store_standard_thm_open: binding -> thm -> thm
     1.7 +  val multi_resolve: thm list -> thm -> thm Seq.seq
     1.8 +  val multi_resolves: thm list -> thm list -> thm Seq.seq
     1.9    val compose_single: thm * int * thm -> thm
    1.10    val equals_cong: thm
    1.11    val imp_cong: thm
    1.12 @@ -108,8 +110,6 @@
    1.13    val equal_elim_rule1: thm
    1.14    val equal_elim_rule2: thm
    1.15    val remdups_rl: thm
    1.16 -  val multi_resolve: thm list -> thm -> thm Seq.seq
    1.17 -  val multi_resolves: thm list -> thm list -> thm Seq.seq
    1.18    val abs_def: thm -> thm
    1.19  end;
    1.20  
    1.21 @@ -314,50 +314,64 @@
    1.22              (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm))
    1.23    in rearr 0 end;
    1.24  
    1.25 -(*Resolution: exactly one resolvent must be produced.*)
    1.26 -fun tha RSN (i,thb) =
    1.27 -  case Seq.chop 2 (Thm.biresolution false [(false,tha)] i thb) of
    1.28 -      ([th],_) => th
    1.29 -    | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
    1.30 -    |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
    1.31  
    1.32 -(*resolution: P==>Q, Q==>R gives P==>R. *)
    1.33 +(*Resolution: multiple arguments, multiple results*)
    1.34 +local
    1.35 +  fun res th i rule =
    1.36 +    Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
    1.37 +
    1.38 +  fun multi_res _ [] rule = Seq.single rule
    1.39 +    | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
    1.40 +in
    1.41 +  val multi_resolve = multi_res 1;
    1.42 +  fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
    1.43 +end;
    1.44 +
    1.45 +(*Resolution: exactly one resolvent must be produced*)
    1.46 +fun tha RSN (i, thb) =
    1.47 +  (case Seq.chop 2 (Thm.biresolution false [(false, tha)] i thb) of
    1.48 +    ([th], _) => th
    1.49 +  | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
    1.50 +  | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
    1.51 +
    1.52 +(*Resolution: P==>Q, Q==>R gives P==>R*)
    1.53  fun tha RS thb = tha RSN (1,thb);
    1.54  
    1.55  (*For joining lists of rules*)
    1.56 -fun thas RLN (i,thbs) =
    1.57 +fun thas RLN (i, thbs) =
    1.58    let val resolve = Thm.biresolution false (map (pair false) thas) i
    1.59        fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
    1.60    in maps resb thbs end;
    1.61  
    1.62 -fun thas RL thbs = thas RLN (1,thbs);
    1.63 +fun thas RL thbs = thas RLN (1, thbs);
    1.64 +
    1.65 +(*Isar-style multi-resolution*)
    1.66 +fun bottom_rl OF rls =
    1.67 +  (case Seq.chop 2 (multi_resolve rls bottom_rl) of
    1.68 +    ([th], _) => th
    1.69 +  | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls)
    1.70 +  | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls));
    1.71  
    1.72  (*Resolve a list of rules against bottom_rl from right to left;
    1.73    makes proof trees*)
    1.74 -fun rls MRS bottom_rl =
    1.75 -  let fun rs_aux i [] = bottom_rl
    1.76 -        | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
    1.77 -  in  rs_aux 1 rls  end;
    1.78 -
    1.79 -(*A version of MRS with more appropriate argument order*)
    1.80 -fun bottom_rl OF rls = rls MRS bottom_rl;
    1.81 +fun rls MRS bottom_rl = bottom_rl OF rls;
    1.82  
    1.83  (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
    1.84    with no lifting or renaming!  Q may contain ==> or meta-quants
    1.85    ALWAYS deletes premise i *)
    1.86  fun compose(tha,i,thb) =
    1.87 -    distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
    1.88 +  distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
    1.89  
    1.90  fun compose_single (tha,i,thb) =
    1.91 -  case compose (tha,i,thb) of
    1.92 +  (case compose (tha,i,thb) of
    1.93      [th] => th
    1.94 -  | _ => raise THM ("compose: unique result expected", i, [tha,thb]);
    1.95 +  | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
    1.96  
    1.97  (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
    1.98  fun tha COMP thb =
    1.99 -    case compose(tha,1,thb) of
   1.100 -        [th] => th
   1.101 -      | _ =>   raise THM("COMP", 1, [tha,thb]);
   1.102 +  (case compose(tha, 1, thb) of
   1.103 +    [th] => th
   1.104 +  | _ => raise THM ("COMP", 1, [tha, thb]));
   1.105  
   1.106  
   1.107  (** theorem equality **)
   1.108 @@ -866,25 +880,6 @@
   1.109      | _ => error "More names than abstractions in theorem"
   1.110    end;
   1.111  
   1.112 -
   1.113 -
   1.114 -(** multi_resolve **)
   1.115 -
   1.116 -local
   1.117 -
   1.118 -fun res th i rule =
   1.119 -  Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
   1.120 -
   1.121 -fun multi_res _ [] rule = Seq.single rule
   1.122 -  | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
   1.123 -
   1.124 -in
   1.125 -
   1.126 -val multi_resolve = multi_res 1;
   1.127 -fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
   1.128 -
   1.129 -end;
   1.130 -
   1.131  end;
   1.132  
   1.133  structure Basic_Drule: BASIC_DRULE = Drule;