rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
1.1 --- a/NEWS Wed Apr 11 20:42:28 2012 +0200
1.2 +++ b/NEWS Wed Apr 11 21:40:46 2012 +0200
1.3 @@ -53,6 +53,11 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
1.8 +tolerant against multiple unifiers, as long as the final result is
1.9 +unique. (As before, rules are composed in canonical right-to-left
1.10 +order to accommodate newly introduced premises.)
1.11 +
1.12 * Command 'definition' no longer exports the foundational "raw_def"
1.13 into the user context. Minor INCOMPATIBILITY, may use the regular
1.14 "def" result with attribute "abs_def" to imitate the old version.
2.1 --- a/src/Pure/drule.ML Wed Apr 11 20:42:28 2012 +0200
2.2 +++ b/src/Pure/drule.ML Wed Apr 11 21:40:46 2012 +0200
2.3 @@ -67,6 +67,8 @@
2.4 val store_standard_thm: binding -> thm -> thm
2.5 val store_thm_open: binding -> thm -> thm
2.6 val store_standard_thm_open: binding -> thm -> thm
2.7 + val multi_resolve: thm list -> thm -> thm Seq.seq
2.8 + val multi_resolves: thm list -> thm list -> thm Seq.seq
2.9 val compose_single: thm * int * thm -> thm
2.10 val equals_cong: thm
2.11 val imp_cong: thm
2.12 @@ -108,8 +110,6 @@
2.13 val equal_elim_rule1: thm
2.14 val equal_elim_rule2: thm
2.15 val remdups_rl: thm
2.16 - val multi_resolve: thm list -> thm -> thm Seq.seq
2.17 - val multi_resolves: thm list -> thm list -> thm Seq.seq
2.18 val abs_def: thm -> thm
2.19 end;
2.20
2.21 @@ -314,50 +314,64 @@
2.22 (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm))
2.23 in rearr 0 end;
2.24
2.25 -(*Resolution: exactly one resolvent must be produced.*)
2.26 -fun tha RSN (i,thb) =
2.27 - case Seq.chop 2 (Thm.biresolution false [(false,tha)] i thb) of
2.28 - ([th],_) => th
2.29 - | ([],_) => raise THM("RSN: no unifiers", i, [tha,thb])
2.30 - | _ => raise THM("RSN: multiple unifiers", i, [tha,thb]);
2.31
2.32 -(*resolution: P==>Q, Q==>R gives P==>R. *)
2.33 +(*Resolution: multiple arguments, multiple results*)
2.34 +local
2.35 + fun res th i rule =
2.36 + Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
2.37 +
2.38 + fun multi_res _ [] rule = Seq.single rule
2.39 + | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
2.40 +in
2.41 + val multi_resolve = multi_res 1;
2.42 + fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
2.43 +end;
2.44 +
2.45 +(*Resolution: exactly one resolvent must be produced*)
2.46 +fun tha RSN (i, thb) =
2.47 + (case Seq.chop 2 (Thm.biresolution false [(false, tha)] i thb) of
2.48 + ([th], _) => th
2.49 + | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
2.50 + | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
2.51 +
2.52 +(*Resolution: P==>Q, Q==>R gives P==>R*)
2.53 fun tha RS thb = tha RSN (1,thb);
2.54
2.55 (*For joining lists of rules*)
2.56 -fun thas RLN (i,thbs) =
2.57 +fun thas RLN (i, thbs) =
2.58 let val resolve = Thm.biresolution false (map (pair false) thas) i
2.59 fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
2.60 in maps resb thbs end;
2.61
2.62 -fun thas RL thbs = thas RLN (1,thbs);
2.63 +fun thas RL thbs = thas RLN (1, thbs);
2.64 +
2.65 +(*Isar-style multi-resolution*)
2.66 +fun bottom_rl OF rls =
2.67 + (case Seq.chop 2 (multi_resolve rls bottom_rl) of
2.68 + ([th], _) => th
2.69 + | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls)
2.70 + | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls));
2.71
2.72 (*Resolve a list of rules against bottom_rl from right to left;
2.73 makes proof trees*)
2.74 -fun rls MRS bottom_rl =
2.75 - let fun rs_aux i [] = bottom_rl
2.76 - | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
2.77 - in rs_aux 1 rls end;
2.78 -
2.79 -(*A version of MRS with more appropriate argument order*)
2.80 -fun bottom_rl OF rls = rls MRS bottom_rl;
2.81 +fun rls MRS bottom_rl = bottom_rl OF rls;
2.82
2.83 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
2.84 with no lifting or renaming! Q may contain ==> or meta-quants
2.85 ALWAYS deletes premise i *)
2.86 fun compose(tha,i,thb) =
2.87 - distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
2.88 + distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
2.89
2.90 fun compose_single (tha,i,thb) =
2.91 - case compose (tha,i,thb) of
2.92 + (case compose (tha,i,thb) of
2.93 [th] => th
2.94 - | _ => raise THM ("compose: unique result expected", i, [tha,thb]);
2.95 + | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
2.96
2.97 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
2.98 fun tha COMP thb =
2.99 - case compose(tha,1,thb) of
2.100 - [th] => th
2.101 - | _ => raise THM("COMP", 1, [tha,thb]);
2.102 + (case compose(tha, 1, thb) of
2.103 + [th] => th
2.104 + | _ => raise THM ("COMP", 1, [tha, thb]));
2.105
2.106
2.107 (** theorem equality **)
2.108 @@ -866,25 +880,6 @@
2.109 | _ => error "More names than abstractions in theorem"
2.110 end;
2.111
2.112 -
2.113 -
2.114 -(** multi_resolve **)
2.115 -
2.116 -local
2.117 -
2.118 -fun res th i rule =
2.119 - Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
2.120 -
2.121 -fun multi_res _ [] rule = Seq.single rule
2.122 - | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
2.123 -
2.124 -in
2.125 -
2.126 -val multi_resolve = multi_res 1;
2.127 -fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
2.128 -
2.129 -end;
2.130 -
2.131 end;
2.132
2.133 structure Basic_Drule: BASIC_DRULE = Drule;