Adapted to new package for inductive sets.

--- a/src/HOL/List.thy	Wed Jul 11 11:03:11 2007 +0200
+++ b/src/HOL/List.thy	Wed Jul 11 11:04:39 2007 +0200
@@ -2386,33 +2386,20 @@
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
-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
+inductive_set
   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"
+  for A :: "'a set"
+where
+    Nil [intro!]: "[]: lists A"
+  | Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
+
+inductive_cases listsE [elim!]: "x#l : lists A"
+inductive_cases listspE [elim!]: "listsp A (x # l)"
+
+lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
   by (clarify, erule listsp.induct, blast+)
 
-lemmas lists_mono [mono] = listsp_mono [to_set]
+lemmas lists_mono = listsp_mono [to_set]
 
 lemma listsp_infI:
   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
@@ -2459,7 +2446,7 @@
 
 subsubsection{* Inductive definition for membership *}
 
-inductive2 ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 where
     elem:  "ListMem x (x # xs)"
   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
@@ -2711,73 +2698,60 @@
 
 subsubsection{*Lifting a Relation on List Elements to the Lists*}
 
-inductive2
-  list_all2' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"
-  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+inductive_set
+  listrel :: "('a * 'a)set => ('a list * 'a list)set"
+  for r :: "('a * 'a)set"
 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)"
+    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"
 
 
 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*}
@@ -2875,7 +2849,7 @@
 subsubsection {* Generation of efficient code *}
 
 consts
-  memberl :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
+  member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
   null:: "'a list \<Rightarrow> bool"
   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"

--- a/src/HOL/Nat.thy	Wed Jul 11 11:03:11 2007 +0200
+++ b/src/HOL/Nat.thy	Wed Jul 11 11:04:39 2007 +0200
@@ -34,18 +34,17 @@
 
 text {* Type definition *}
 
-inductive2 Nat :: "ind \<Rightarrow> bool"
+inductive_set Nat :: "ind set"
 where
-    Zero_RepI: "Nat Zero_Rep"
-  | Suc_RepI: "Nat i ==> Nat (Suc_Rep i)"
+    Zero_RepI: "Zero_Rep : Nat"
+  | Suc_RepI: "i : Nat ==> Suc_Rep i : Nat"
 
 global
 
 typedef (open Nat)
-  nat = "Collect Nat"
+  nat = Nat
 proof
-  from Nat.Zero_RepI
-  show "Zero_Rep : Collect Nat" ..
+  show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
 qed
 
 text {* Abstract constants and syntax *}
@@ -72,23 +71,17 @@
 
 text {* Induction *}
 
-lemma Rep_Nat': "Nat (Rep_Nat x)"
-  by (rule Rep_Nat [simplified mem_Collect_eq])
-
-lemma Abs_Nat_inverse': "Nat y \<Longrightarrow> Rep_Nat (Abs_Nat y) = y"
-  by (rule Abs_Nat_inverse [simplified mem_Collect_eq])
-
 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
   apply (unfold Zero_nat_def Suc_def)
   apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
-  apply (erule Rep_Nat' [THEN Nat.induct])
-  apply (iprover elim: Abs_Nat_inverse' [THEN subst])
+  apply (erule Rep_Nat [THEN Nat.induct])
+  apply (iprover elim: Abs_Nat_inverse [THEN subst])
   done
 
 text {* Distinctness of constructors *}
 
 lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
-  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat' Suc_RepI Zero_RepI
+  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI
                 Suc_Rep_not_Zero_Rep)
 
 lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
@@ -103,7 +96,7 @@
 text {* Injectiveness of @{term Suc} *}
 
 lemma inj_Suc[simp]: "inj_on Suc N"
-  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat' Suc_RepI
+  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI
                 inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
 
 lemma Suc_inject: "Suc x = Suc y ==> x = y"