# HG changeset patch
# User paulson
# Date 867746070 -7200
# Node ID 1f972dc8eafb277175161d06a82bbe6d6cf9ff24
# Parent  a0797ba03dfe7f662db3514881558afaf9bf6e07
New laws for the "lists" operator

diff -r a0797ba03dfe -r 1f972dc8eafb src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Jun 30 12:08:19 1997 +0200
+++ b/src/HOL/List.ML	Tue Jul 01 10:34:30 1997 +0200
@@ -19,13 +19,29 @@
 qed "neq_Nil_conv";
 
 
-(** List operator over sets **)
+(** "lists": the list-forming operator over sets **)
 
 goalw thy lists.defs "!!A B. A<=B ==> lists A <= lists B";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "lists_mono";
 
+val listsE = lists.mk_cases list.simps  "x#l : lists A";
+AddSEs [listsE];
+AddSIs lists.intrs;
+
+goal thy "!!l. l: lists A ==> l: lists B --> l: lists (A Int B)";
+by (etac lists.induct 1);
+by (ALLGOALS Blast_tac);
+qed_spec_mp "lists_IntI";
+
+goal thy "lists (A Int B) = lists A Int lists B";
+br (mono_Int RS equalityI) 1;
+by (simp_tac (!simpset addsimps [mono_def, lists_mono]) 1);
+by (blast_tac (!claset addSIs [lists_IntI]) 1);
+qed "lists_Int_eq";
+Addsimps [lists_Int_eq];
+
 
 (** list_case **)