# HG changeset patch # User wenzelm # Date 1135207738 -3600 # Node ID 324245a561b530888dab98f1df27a9306efc30f1 # Parent 43951ffb6304b03c9aaa622ae99b2d887a34e490 mk_conjunction: proper treatment of bounds; added dest_conjunction(s); diff -r 43951ffb6304 -r 324245a561b5 src/Pure/logic.ML --- a/src/Pure/logic.ML Thu Dec 22 00:28:54 2005 +0100 +++ b/src/Pure/logic.ML Thu Dec 22 00:28:58 2005 +0100 @@ -23,6 +23,8 @@ val nth_prem: int * term -> term val mk_conjunction: term * term -> term val mk_conjunction_list: term list -> term + val dest_conjunction: term -> term * term + val dest_conjunctions: term -> term list val strip_horn: term -> term list * term val mk_cond_defpair: term list -> term * term -> string * term val mk_defpair: term * term -> string * term @@ -130,11 +132,26 @@ (** conjunction **) fun mk_conjunction (t, u) = - Term.list_all ([("X", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0)); + Term.list_all ([("X", propT)], + mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0)); fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) | mk_conjunction_list ts = foldr1 mk_conjunction ts; +fun dest_conjunction + (t as Const ("all", _) $ Abs (_, _, + Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) = + if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0) + then raise TERM ("dest_conjunction", [t]) + else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B) + | dest_conjunction t = raise TERM ("dest_conjunction", [t]); + +fun dest_conjunctions t = + (case try dest_conjunction t of + NONE => [t] + | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); + + (** definitions **)