# HG changeset patch # User wenzelm # Date 1135347408 -3600 # Node ID 567370efb6d7f623e8af0456dbca1a7df7fc0cda # Parent 466351242c6fba90efb7dd59b78c5a56e14012d4 added mk_conjunction_list2; diff -r 466351242c6f -r 567370efb6d7 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Dec 23 15:16:46 2005 +0100 +++ b/src/Pure/logic.ML Fri Dec 23 15:16:48 2005 +0100 @@ -23,6 +23,7 @@ val nth_prem: int * term -> term val mk_conjunction: term * term -> term val mk_conjunction_list: term list -> term + val mk_conjunction_list2: term list list -> term val dest_conjunction: term -> term * term val dest_conjunctions: term -> term list val strip_horn: term -> term list * term @@ -131,13 +132,20 @@ (** conjunction **) +(*A && B*) fun mk_conjunction (t, u) = Term.list_all ([("X", propT)], mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0)); +(*A && B && C -- improper*) fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) | mk_conjunction_list ts = foldr1 mk_conjunction ts; +(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*) +fun mk_conjunction_list2 tss = + mk_conjunction_list (map mk_conjunction_list (filter_out null tss)); + +(*A && B*) fun dest_conjunction (t as Const ("all", _) $ Abs (_, _, Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) = @@ -146,6 +154,7 @@ else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B) | dest_conjunction t = raise TERM ("dest_conjunction", [t]); +(*((A && B) && C) && D && E -- flat*) fun dest_conjunctions t = (case try dest_conjunction t of NONE => [t]