added mk_conjunction_list2;
authorwenzelm
Fri Dec 23 15:16:48 2005 +0100 (2005-12-23)
changeset 18499567370efb6d7
parent 18498 466351242c6f
child 18500 8b1a4e8ed199
added mk_conjunction_list2;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Fri Dec 23 15:16:46 2005 +0100
     1.2 +++ b/src/Pure/logic.ML	Fri Dec 23 15:16:48 2005 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    val nth_prem: int * term -> term
     1.5    val mk_conjunction: term * term -> term
     1.6    val mk_conjunction_list: term list -> term
     1.7 +  val mk_conjunction_list2: term list list -> term
     1.8    val dest_conjunction: term -> term * term
     1.9    val dest_conjunctions: term -> term list
    1.10    val strip_horn: term -> term list * term
    1.11 @@ -131,13 +132,20 @@
    1.12  
    1.13  (** conjunction **)
    1.14  
    1.15 +(*A && B*)
    1.16  fun mk_conjunction (t, u) =
    1.17    Term.list_all ([("X", propT)],
    1.18      mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0));
    1.19  
    1.20 +(*A && B && C -- improper*)
    1.21  fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
    1.22    | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    1.23  
    1.24 +(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
    1.25 +fun mk_conjunction_list2 tss =
    1.26 +  mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
    1.27 +
    1.28 +(*A && B*)
    1.29  fun dest_conjunction
    1.30        (t as Const ("all", _) $ Abs (_, _,
    1.31          Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) =
    1.32 @@ -146,6 +154,7 @@
    1.33        else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B)
    1.34    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
    1.35  
    1.36 +(*((A && B) && C) && D && E -- flat*)
    1.37  fun dest_conjunctions t =
    1.38    (case try dest_conjunction t of
    1.39      NONE => [t]