diff -r 9e185f78e7d4 -r 96ba62dff413 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 07 17:26:49 2007 +0100
+++ b/src/HOL/List.thy	Wed Feb 07 17:28:09 2007 +0100
@@ -2200,40 +2200,71 @@
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
-consts lists :: "'a set => 'a list set"
-inductive "lists A"
- intros
-  Nil [intro!]: "[]: lists A"
-  Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
-
-inductive_cases listsE [elim!]: "x#l : lists A"
-
-lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B"
-by (unfold lists.defs) (blast intro!: lfp_mono)
-
-lemma lists_IntI:
-  assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l
+inductive2
+  listsp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+  for A :: "'a \<Rightarrow> bool"
+where
+    Nil [intro!]: "listsp A []"
+  | Cons [intro!]: "[| A a; listsp A l |] ==> listsp A (a # l)"
+
+constdefs
+  lists :: "'a set => 'a list set"
+  "lists A == Collect (listsp (member A))"
+
+lemma listsp_lists_eq [pred_set_conv]: "listsp (member A) = member (lists A)"
+  by (simp add: lists_def)
+
+lemmas lists_intros [intro!] = listsp.intros [to_set]
+
+lemmas lists_induct [consumes 1, case_names Nil Cons, induct set: lists] =
+  listsp.induct [to_set]
+
+inductive_cases2 listspE [elim!]: "listsp A (x # l)"
+
+lemmas listsE [elim!] = listspE [to_set]
+
+lemma listsp_mono [mono2]: "A \<le> B ==> listsp A \<le> listsp B"
+  by (clarify, erule listsp.induct, blast+)
+
+lemmas lists_mono [mono] = listsp_mono [to_set]
+
+lemma listsp_meetI:
+  assumes l: "listsp A l" shows "listsp B l ==> listsp (meet A B) l" using l
   by induct blast+
 
-lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
-proof (rule mono_Int [THEN equalityI])
-  show "mono lists" by (simp add: mono_def lists_mono)
-  show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI)
+lemmas lists_IntI = listsp_meetI [to_set]
+
+lemma listsp_meet_eq [simp]: "listsp (meet A B) = meet (listsp A) (listsp B)"
+proof (rule mono_meet [where f=listsp, THEN order_antisym])
+  show "mono listsp" by (simp add: mono_def listsp_mono)
+  show "meet (listsp A) (listsp B) \<le> listsp (meet A B)" by (blast intro: listsp_meetI)
 qed
 
-lemma append_in_lists_conv [iff]:
-     "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
+lemmas listsp_conj_eq [simp] = listsp_meet_eq [simplified meet_fun_eq meet_bool_eq]
+
+lemmas lists_Int_eq [simp] = listsp_meet_eq [to_set]
+
+lemma append_in_listsp_conv [iff]:
+     "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
 by (induct xs) auto
 
-lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
--- {* eliminate @{text lists} in favour of @{text set} *}
+lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
+
+lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
+-- {* eliminate @{text listsp} in favour of @{text set} *}
 by (induct xs) auto
 
-lemma in_listsD [dest!]: "xs \<in> lists A ==> \<forall>x\<in>set xs. x \<in> A"
-by (rule in_lists_conv_set [THEN iffD1])
-
-lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
-by (rule in_lists_conv_set [THEN iffD2])
+lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
+
+lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+by (rule in_listsp_conv_set [THEN iffD1])
+
+lemmas in_listsD [dest!] = in_listspD [to_set]
+
+lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+by (rule in_listsp_conv_set [THEN iffD2])
+
+lemmas in_listsI [intro!] = in_listspI [to_set]
 
 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
 by auto
@@ -2242,13 +2273,12 @@
 
 subsubsection{* Inductive definition for membership *}
 
-consts ListMem :: "('a \<times> 'a list)set"
-inductive ListMem
-intros
- elem:  "(x,x#xs) \<in> ListMem"
- insert:  "(x,xs) \<in> ListMem \<Longrightarrow> (x,y#xs) \<in> ListMem"
-
-lemma ListMem_iff: "((x,xs) \<in> ListMem) = (x \<in> set xs)"
+inductive2 ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+    elem:  "ListMem x (x # xs)"
+  | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
+
+lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
 apply (rule iffI)
  apply (induct set: ListMem)
   apply auto
@@ -2495,60 +2525,73 @@
 
 subsubsection{*Lifting a Relation on List Elements to the Lists*}
 
-consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"
-
-inductive "listrel(r)"
- intros
-   Nil:  "([],[]) \<in> listrel r"
-   Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
-
-inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
-inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
-inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
-inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
+inductive2
+  list_all2' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+where
+    Nil:  "list_all2' r [] []"
+  | Cons: "[| r x y; list_all2' r xs ys |] ==> list_all2' r (x#xs) (y#ys)"
+
+constdefs
+  listrel :: "('a * 'b) set => ('a list * 'b list) set"
+  "listrel r == Collect2 (list_all2' (member2 r))"
+
+lemma list_all2_listrel_eq [pred_set_conv]:
+  "list_all2' (member2 r) = member2 (listrel r)"
+  by (simp add: listrel_def)
+
+lemmas listrel_induct [consumes 1, case_names Nil Cons, induct set: listrel] =
+  list_all2'.induct [to_set]
+
+lemmas listrel_intros = list_all2'.intros [to_set]
+
+inductive_cases2 listrel_Nil1 [to_set, elim!]: "list_all2' r [] xs"
+inductive_cases2 listrel_Nil2 [to_set, elim!]: "list_all2' r xs []"
+inductive_cases2 listrel_Cons1 [to_set, elim!]: "list_all2' r  (y#ys) xs"
+inductive_cases2 listrel_Cons2 [to_set, elim!]: "list_all2' r xs (y#ys)"
 
 
 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
 apply clarify  
-apply (erule listrel.induct)
-apply (blast intro: listrel.intros)+
+apply (erule listrel_induct)
+apply (blast intro: listrel_intros)+
 done
 
 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
 apply clarify 
-apply (erule listrel.induct, auto) 
+apply (erule listrel_induct, auto) 
 done
 
 lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)" 
 apply (simp add: refl_def listrel_subset Ball_def)
 apply (rule allI) 
 apply (induct_tac x) 
-apply (auto intro: listrel.intros)
+apply (auto intro: listrel_intros)
 done
 
 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
 apply (auto simp add: sym_def)
-apply (erule listrel.induct) 
-apply (blast intro: listrel.intros)+
+apply (erule listrel_induct) 
+apply (blast intro: listrel_intros)+
 done
 
 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
 apply (simp add: trans_def)
 apply (intro allI) 
 apply (rule impI) 
-apply (erule listrel.induct) 
-apply (blast intro: listrel.intros)+
+apply (erule listrel_induct) 
+apply (blast intro: listrel_intros)+
 done
 
 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
 by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) 
 
 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
-by (blast intro: listrel.intros)
+by (blast intro: listrel_intros)
 
 lemma listrel_Cons:
      "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
-by (auto simp add: set_Cons_def intro: listrel.intros) 
+by (auto simp add: set_Cons_def intro: listrel_intros) 
 
 
 subsection{*Miscellany*}