# HG changeset patch # User wenzelm # Date 1135347406 -3600 # Node ID 466351242c6fba90efb7dd59b78c5a56e14012d4 # Parent 7569674d7bb1914be44d5b2a68e305eb8c290c11 conj_elim_precise: proper treatment of nested conjunctions; diff -r 7569674d7bb1 -r 466351242c6f src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Dec 23 15:16:46 2005 +0100 +++ b/src/Pure/drule.ML Fri Dec 23 15:16:46 2005 +0100 @@ -153,7 +153,7 @@ val conj_intr_list: thm list -> thm val conj_elim: thm -> thm * thm val conj_elim_list: thm -> thm list - val conj_elim_precise: int -> thm -> thm list + val conj_elim_precise: int list -> thm -> thm list list val conj_intr_thm: thm val conj_curry: thm -> thm val abs_def: thm -> thm @@ -1203,15 +1203,23 @@ let val th' = forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th in (incr_indexes th' proj1 COMP th', incr_indexes th' proj2 COMP th') end; +(*((A && B) && C) && D && E -- flat*) fun conj_elim_list th = let val (th1, th2) = conj_elim th in conj_elim_list th1 @ conj_elim_list th2 end handle THM _ => [th]; -fun conj_elim_precise 0 _ = [] - | conj_elim_precise 1 th = [th] - | conj_elim_precise n th = - let val (th1, th2) = conj_elim th - in th1 :: conj_elim_precise (n - 1) th2 end; +(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*) +fun conj_elim_precise spans = + let + fun elim 0 _ = [] + | elim 1 th = [th] + | elim n th = + let val (th1, th2) = conj_elim th + in th1 :: elim (n - 1) th2 end; + fun elims (0 :: ns) ths = [] :: elims ns ths + | elims (n :: ns) (th :: ths) = elim n th :: elims ns ths + | elims _ _ = []; + in elims spans o elim (length (filter_out (equal 0) spans)) end; val conj_intr_thm = store_standard_thm_open "conjunctionI" (implies_intr_list [A, B] (conj_intr (Thm.assume A) (Thm.assume B)));