# HG changeset patch
# User berghofe
# Date 1170866647 -3600
# Node ID 51a80e238b297337d50691b81af4ef9447ab49fd
# Parent  4ccb7e6be929b4c9d1396ef45245d7a941995612
Adapted to new inductive definition package.

diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/InductTermi.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -14,21 +14,18 @@
 
 subsection {* Terminating lambda terms *}
 
-consts
-  IT :: "dB set"
-
-inductive IT
-  intros
-    Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT"
-    Lambda [intro]: "r : IT ==> Abs r : IT"
-    Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT"
+inductive2 IT :: "dB => bool"
+  where
+    Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
+  | Lambda [intro]: "IT r ==> IT (Abs r)"
+  | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
 
 
 subsection {* Every term in IT terminates *}
 
 lemma double_induction_lemma [rule_format]:
-  "s : termi beta ==> \<forall>t. t : termi beta -->
-    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
+  "termi beta s ==> \<forall>t. termi beta t -->
+    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termi beta (Abs r \<degree> s \<degree>\<degree> ss))"
   apply (erule acc_induct)
   apply (rule allI)
   apply (rule impI)
@@ -39,17 +36,15 @@
   apply (safe elim!: apps_betasE)
      apply assumption
     apply (blast intro: subst_preserves_beta apps_preserves_beta)
-   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
+   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI'
      dest: acc_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
   apply (blast dest: apps_preserves_betas)
   done
 
-lemma IT_implies_termi: "t : IT ==> t : termi beta"
+lemma IT_implies_termi: "IT t ==> termi beta t"
   apply (induct set: IT)
-    apply (drule rev_subsetD)
-     apply (rule lists_mono)
-     apply (rule Int_lower2)
-    apply simp
+    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termi beta"]])
+    apply fast
     apply (drule lists_accD)
     apply (erule acc_induct)
     apply (rule accI)
@@ -72,12 +67,12 @@
   "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
   by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
 
-inductive_cases [elim!]:
-  "Var n \<degree>\<degree> ss : IT"
-  "Abs t : IT"
-  "Abs r \<degree> s \<degree>\<degree> ts : IT"
+inductive_cases2 [elim!]:
+  "IT (Var n \<degree>\<degree> ss)"
+  "IT (Abs t)"
+  "IT (Abs r \<degree> s \<degree>\<degree> ts)"
 
-theorem termi_implies_IT: "r : termi beta ==> r : IT"
+theorem termi_implies_IT: "termi beta r ==> IT r"
   apply (erule acc_induct)
   apply (rename_tac r)
   apply (erule thin_rl)
@@ -90,8 +85,8 @@
    apply (drule bspec, assumption)
    apply (erule mp)
    apply clarify
-   apply (drule converseI)
-   apply (drule ex_step1I, assumption)
+   apply (drule_tac r=beta in conversepI)
+   apply (drule_tac r="beta^--1" in ex_step1I, assumption)
    apply clarify
    apply (rename_tac us)
    apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -53,29 +53,21 @@
 
 subsection {* Beta-reduction *}
 
-consts
-  beta :: "(dB \<times> dB) set"
-
-abbreviation
-  beta_red :: "[dB, dB] => bool"  (infixl "->" 50) where
-  "s -> t == (s, t) \<in> beta"
+inductive2 beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  where
+    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
+  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
 
 abbreviation
   beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
-  "s ->> t == (s, t) \<in> beta^*"
+  "s ->> t == beta^** s t"
 
 notation (latex)
-  beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50) and
   beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
 
-inductive beta
-  intros
-    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
-    appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
-    appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
-    abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
-
-inductive_cases beta_cases [elim!]:
+inductive_cases2 beta_cases [elim!]:
   "Var i \<rightarrow>\<^sub>\<beta> t"
   "Abs r \<rightarrow>\<^sub>\<beta> s"
   "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
@@ -88,19 +80,19 @@
 
 lemma rtrancl_beta_Abs [intro!]:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
-  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppL:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
-  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppR:
     "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
-  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_App [intro]:
     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
-  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans)
+  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans')
 
 
 subsection {* Substitution-lemmas *}
@@ -164,8 +156,8 @@
 
 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
   apply (induct set: rtrancl)
-   apply (rule rtrancl_refl)
-  apply (erule rtrancl_into_rtrancl)
+   apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl.rtrancl_into_rtrancl)
   apply (erule subst_preserves_beta)
   done
 
@@ -175,22 +167,22 @@
 
 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
   apply (induct set: rtrancl)
-   apply (rule rtrancl_refl)
-  apply (erule rtrancl_into_rtrancl)
+   apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl.rtrancl_into_rtrancl)
   apply (erule lift_preserves_beta)
   done
 
 theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   apply (induct t arbitrary: r s i)
-    apply (simp add: subst_Var r_into_rtrancl)
+    apply (simp add: subst_Var r_into_rtrancl')
    apply (simp add: rtrancl_beta_App)
   apply (simp add: rtrancl_beta_Abs)
   done
 
 theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   apply (induct set: rtrancl)
-   apply (rule rtrancl_refl)
-  apply (erule rtrancl_trans)
+   apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl_trans')
   apply (erule subst_preserves_beta2)
   done
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -14,10 +14,10 @@
 
 abbreviation
   list_beta :: "dB list => dB list => bool"  (infixl "=>" 50) where
-  "rs => ss == (rs, ss) : step1 beta"
+  "rs => ss == step1 beta rs ss"
 
 lemma head_Var_reduction:
-  "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
+  "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
   apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
      apply simp
     apply (rule_tac xs = rs in rev_exhaust)
@@ -29,14 +29,14 @@
   done
 
 lemma apps_betasE [elim!]:
-  assumes major: "r \<degree>\<degree> rs -> s"
-    and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
+  assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s"
+    and cases: "!!r'. [| r \<rightarrow>\<^sub>\<beta> r'; s = r' \<degree>\<degree> rs |] ==> R"
       "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
       "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
   shows R
 proof -
   from major have
-   "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
+   "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
     (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
     (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
     apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
@@ -66,18 +66,18 @@
 qed
 
 lemma apps_preserves_beta [simp]:
-    "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
+    "r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss"
   by (induct ss rule: rev_induct) auto
 
 lemma apps_preserves_beta2 [simp]:
     "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
   apply (induct set: rtrancl)
    apply blast
-  apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
+  apply (blast intro: apps_preserves_beta rtrancl.rtrancl_into_rtrancl)
   done
 
 lemma apps_preserves_betas [simp]:
-    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
+    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss"
   apply (induct rs arbitrary: ss rule: rev_induct)
    apply simp
   apply simp
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -14,21 +14,14 @@
 
 subsection {* Parallel reduction *}
 
-consts
-  par_beta :: "(dB \<times> dB) set"
-
-abbreviation
-  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50) where
-  "s => t == (s, t) \<in> par_beta"
+inductive2 par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
+  where
+    var [simp, intro!]: "Var n => Var n"
+  | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
+  | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
+  | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
 
-inductive par_beta
-  intros
-    var [simp, intro!]: "Var n => Var n"
-    abs [simp, intro!]: "s => t ==> Abs s => Abs t"
-    app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
-    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
-
-inductive_cases par_beta_cases [elim!]:
+inductive_cases2 par_beta_cases [elim!]:
   "Var n => t"
   "Abs s => Abs t"
   "(Abs s) \<degree> t => u"
@@ -48,18 +41,16 @@
   by (induct t) simp_all
 
 lemma beta_subset_par_beta: "beta <= par_beta"
-  apply (rule subsetI)
-  apply clarify
+  apply (rule predicate2I)
   apply (erule beta.induct)
      apply (blast intro!: par_beta_refl)+
   done
 
-lemma par_beta_subset_beta: "par_beta <= beta^*"
-  apply (rule subsetI)
-  apply clarify
+lemma par_beta_subset_beta: "par_beta <= beta^**"
+  apply (rule predicate2I)
   apply (erule par_beta.induct)
      apply blast
-    apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
+    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
       -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
   done
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/StrongNorm.thy
--- a/src/HOL/Lambda/StrongNorm.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/StrongNorm.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -16,41 +16,38 @@
 
 subsection {* Properties of @{text IT} *}
 
-lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
+lemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)"
   apply (induct arbitrary: i set: IT)
     apply (simp (no_asm))
     apply (rule conjI)
      apply
       (rule impI,
        rule IT.Var,
-       erule lists.induct,
+       erule listsp.induct,
        simp (no_asm),
-       rule lists.Nil,
+       rule listsp.Nil,
        simp (no_asm),
-       erule IntE,
-       rule lists.Cons,
+       rule listsp.Cons,
        blast,
        assumption)+
      apply auto
    done
 
-lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
+lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)"
   by (induct ts) auto
 
-lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
+lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])"
   apply (induct arbitrary: i j set: IT)
     txt {* Case @{term Var}: *}
     apply (simp (no_asm) add: subst_Var)
     apply
     ((rule conjI impI)+,
       rule IT.Var,
-      erule lists.induct,
-      simp (no_asm),
-      rule lists.Nil,
+      erule listsp.induct,
       simp (no_asm),
-      erule IntE,
-      erule CollectE,
-      rule lists.Cons,
+      rule listsp.Nil,
+      simp (no_asm),
+      rule listsp.Cons,
       fast,
       assumption)+
    txt {* Case @{term Lambda}: *}
@@ -65,21 +62,21 @@
    apply auto
   done
 
-lemma Var_IT: "Var n \<in> IT"
-  apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
+lemma Var_IT: "IT (Var n)"
+  apply (subgoal_tac "IT (Var n \<degree>\<degree> [])")
    apply simp
   apply (rule IT.Var)
-  apply (rule lists.Nil)
+  apply (rule listsp.Nil)
   done
 
-lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
+lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)"
   apply (induct set: IT)
     apply (subst app_last)
     apply (rule IT.Var)
     apply simp
-    apply (rule lists.Cons)
+    apply (rule listsp.Cons)
      apply (rule Var_IT)
-    apply (rule lists.Nil)
+    apply (rule listsp.Nil)
    apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
     apply (erule subst_Var_IT)
    apply (rule Var_IT)
@@ -94,26 +91,26 @@
 subsection {* Well-typed substitution preserves termination *}
 
 lemma subst_type_IT:
-  "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
-    u \<in> IT \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> t[u/i] \<in> IT"
+  "\<And>t e T u i. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
+    IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])"
   (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
 proof (induct U)
   fix T t
   assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
   assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
-  assume "t \<in> IT"
+  assume "IT t"
   thus "\<And>e T' u i. PROP ?Q t e T' u i T"
   proof induct
     fix e T' u i
-    assume uIT: "u \<in> IT"
+    assume uIT: "IT u"
     assume uT: "e \<turnstile> u : T"
     {
-      case (Var n rs e_ T'_ u_ i_)
+      case (Var rs n e_ T'_ u_ i_)
       assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
-      let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
+      let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'"
       let ?R = "\<lambda>t. \<forall>e T' u i.
-        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
-      show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
+        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])"
+      show "IT ((Var n \<degree>\<degree> rs)[u/i])"
       proof (cases "n = i")
         case True
         show ?thesis
@@ -134,13 +131,13 @@
           from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
             by cases auto
           with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
-          from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
-            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
+          from T have "IT ((Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
+            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])"
           proof (rule MI2)
-            from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
+            from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])"
             proof (rule MI1)
-              have "lift u 0 \<in> IT" by (rule lift_IT)
-              thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
+              have "IT (lift u 0)" by (rule lift_IT)
+              thus "IT (lift u 0 \<degree> Var 0)" by (rule app_Var_IT)
               show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
               proof (rule typing.App)
                 show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
@@ -149,19 +146,19 @@
                   by (rule typing.Var) simp
               qed
               from Var have "?R a" by cases (simp_all add: Cons)
-              with argT uIT uT show "a[u/i] \<in> IT" by simp
+              with argT uIT uT show "IT (a[u/i])" by simp
               from argT uT show "e \<turnstile> a[u/i] : T''"
                 by (rule subst_lemma) simp
             qed
-            thus "u \<degree> a[u/i] \<in> IT" by simp
-            from Var have "as \<in> lists {t. ?R t}"
+            thus "IT (u \<degree> a[u/i])" by simp
+            from Var have "listsp ?R as"
               by cases (simp_all add: Cons)
-            moreover from argsT have "as \<in> lists ?ty"
+            moreover from argsT have "listsp ?ty as"
               by (rule lists_typings)
-            ultimately have "as \<in> lists ({t. ?R t} \<inter> ?ty)"
-              by (rule lists_IntI)
-            hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
-              (is "(?ls as) \<in> _")
+            ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) as"
+              by simp
+            hence "listsp IT (map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as))"
+              (is "listsp IT (?ls as)")
             proof induct
               case Nil
               show ?case by fastsimp
@@ -169,13 +166,13 @@
               case (Cons b bs)
               hence I: "?R b" by simp
               from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
-              with uT uIT I have "b[u/i] \<in> IT" by simp
-              hence "lift (b[u/i]) 0 \<in> IT" by (rule lift_IT)
-              hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
-                by (rule lists.Cons) (rule Cons)
+              with uT uIT I have "IT (b[u/i])" by simp
+              hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
+              hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
+                by (rule listsp.Cons) (rule Cons)
               thus ?case by simp
             qed
-            thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
+            thus "IT (Var 0 \<degree>\<degree> ?ls as)" by (rule IT.Var)
             have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
               by (rule typing.Var) simp
             moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
@@ -194,13 +191,13 @@
         qed
       next
         case False
-        from Var have "rs \<in> lists {t. ?R t}" by simp
+        from Var have "listsp ?R rs" by simp
         moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
           by (rule list_app_typeE)
-        hence "rs \<in> lists ?ty" by (rule lists_typings)
-        ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"
-          by (rule lists_IntI)
-        hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
+        hence "listsp ?ty rs" by (rule lists_typings)
+        ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) rs"
+          by simp
+        hence "listsp IT (map (\<lambda>x. x[u/i]) rs)"
         proof induct
           case Nil
           show ?case by fastsimp
@@ -208,9 +205,9 @@
           case (Cons a as)
           hence I: "?R a" by simp
           from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
-          with uT uIT I have "a[u/i] \<in> IT" by simp
-          hence "(a[u/i] # map (\<lambda>t. t[u/i]) as) \<in> lists IT"
-            by (rule lists.Cons) (rule Cons)
+          with uT uIT I have "IT (a[u/i])" by simp
+          hence "listsp IT (a[u/i] # map (\<lambda>t. t[u/i]) as)"
+            by (rule listsp.Cons) (rule Cons)
           thus ?case by simp
         qed
         with False show ?thesis by (auto simp add: subst_Var)
@@ -219,29 +216,29 @@
       case (Lambda r e_ T'_ u_ i_)
       assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
         and "\<And>e T' u i. PROP ?Q r e T' u i T"
-      with uIT uT show "Abs r[u/i] \<in> IT"
+      with uIT uT show "IT (Abs r[u/i])"
         by fastsimp
     next
       case (Beta r a as e_ T'_ u_ i_)
       assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
       assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
       assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
-      have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+      have "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
       proof (rule IT.Beta)
         have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> r[a/0] \<degree>\<degree> as"
           by (rule apps_preserves_beta) (rule beta.beta)
         with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
           by (rule subject_reduction)
-        hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
+        hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])"
           by (rule SI1)
-        thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+        thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
           by (simp del: subst_map add: subst_subst subst_map [symmetric])
         from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
           by (rule list_app_typeE) fast
         then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
-        thus "a[u/i] \<in> IT" by (rule SI2)
+        thus "IT (a[u/i])" by (rule SI2)
       qed
-      thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
+      thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp
     }
   qed
 qed
@@ -251,7 +248,7 @@
 
 lemma type_implies_IT:
   assumes "e \<turnstile> t : T"
-  shows "t \<in> IT"
+  shows "IT t"
   using prems
 proof induct
   case Var
@@ -260,14 +257,14 @@
   case Abs
   show ?case by (rule IT.Lambda)
 next
-  case (App T U e s t)
-  have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
+  case (App e s T U t)
+  have "IT ((Var 0 \<degree> lift t 0)[s/0])"
   proof (rule subst_type_IT)
-    have "lift t 0 \<in> IT" by (rule lift_IT)
-    hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
-    hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+    have "IT (lift t 0)" by (rule lift_IT)
+    hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
+    hence "IT (Var 0 \<degree>\<degree> [lift t 0])" by (rule IT.Var)
     also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
-    finally show "\<dots> \<in> IT" .
+    finally show "IT \<dots>" .
     have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
       by (rule typing.Var) simp
     moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
@@ -278,10 +275,10 @@
   thus ?case by simp
 qed
 
-theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
+theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termi beta t"
 proof -
   assume "e \<turnstile> t : T"
-  hence "t \<in> IT" by (rule type_implies_IT)
+  hence "IT t" by (rule type_implies_IT)
   thus ?thesis by (rule IT_implies_termi)
 qed
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/Type.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -45,8 +45,18 @@
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
+inductive2 typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+  where
+    Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
+  | Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
+  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
+
+inductive_cases2 typing_elims [elim!]:
+  "e \<turnstile> Var i : T"
+  "e \<turnstile> t \<degree> u : T"
+  "e \<turnstile> Abs t : T"
+
 consts
-  typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
   typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
 
 abbreviation
@@ -54,32 +64,14 @@
   "Ts =>> T == foldr Fun Ts T"
 
 abbreviation
-  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ |- _ : _" [50, 50, 50] 50) where
-  "env |- t : T == (env, t, T) \<in> typing"
-
-abbreviation
   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ ||- _ : _" [50, 50, 50] 50) where
   "env ||- ts : Ts == typings env ts Ts"
 
-notation (xsymbols)
-  typing_rel  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-
 notation (latex)
   funs  (infixr "\<Rrightarrow>" 200) and
   typings_rel  ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
 
-inductive typing
-  intros
-    Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
-    Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
-    App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
-
-inductive_cases typing_elims [elim!]:
-  "e \<turnstile> Var i : T"
-  "e \<turnstile> t \<degree> u : T"
-  "e \<turnstile> Abs t : T"
-
 primrec
   "(e \<tturnstile> [] : Ts) = (Ts = [])"
   "(e \<tturnstile> (t # ts) : Ts) =
@@ -100,16 +92,16 @@
 subsection {* Lists of types *}
 
 lemma lists_typings:
-    "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+    "e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts"
   apply (induct ts arbitrary: Ts)
    apply (case_tac Ts)
      apply simp
-     apply (rule lists.Nil)
+     apply (rule listsp.Nil)
     apply simp
   apply (case_tac Ts)
    apply simp
   apply simp
-  apply (rule lists.Cons)
+  apply (rule listsp.Cons)
    apply blast
   apply blast
   done
@@ -172,7 +164,7 @@
   apply (erule impE)
    apply assumption
   apply (elim exE conjE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
   apply (rule_tac x = "Ta # Ts" in exI)
   apply simp
   done
@@ -210,12 +202,12 @@
   "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
   apply (induct ts arbitrary: T U rule: rev_induct)
   apply simp
-  apply (ind_cases "e \<turnstile> Var i : T")
-  apply (ind_cases "e \<turnstile> Var i : T")
+  apply (ind_cases2 "e \<turnstile> Var i : T" for T)
+  apply (ind_cases2 "e \<turnstile> Var i : T" for T)
   apply simp
   apply simp
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
   apply atomize
   apply (erule_tac x="Ta \<Rightarrow> T" in allE)
   apply (erule_tac x="Tb \<Rightarrow> U" in allE)
@@ -238,7 +230,7 @@
   apply (rule FalseE)
   apply simp
   apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
   apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -250,7 +242,7 @@
   apply (rule types_snoc)
   apply assumption
   apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
   apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -258,7 +250,7 @@
   apply (rule typing.App)
   apply assumption
   apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
   apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -266,7 +258,7 @@
   apply (rule_tac x="type1 # Us" in exI)
   apply simp
   apply (erule list_app_typeE)
-  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
   apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -281,13 +273,13 @@
 lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
   apply (cases T)
   apply (rule FalseE)
-  apply (erule typing.elims)
+  apply (erule typing.cases)
   apply simp_all
   apply atomize
   apply (erule_tac x="type1" in allE)
   apply (erule_tac x="type2" in allE)
   apply (erule mp)
-  apply (erule typing.elims)
+  apply (erule typing.cases)
   apply simp_all
   done
 
@@ -335,14 +327,14 @@
 
 subsection {* Subject reduction *}
 
-lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
+lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T"
   apply (induct arbitrary: t' set: typing)
     apply blast
    apply blast
   apply atomize
-  apply (ind_cases "s \<degree> t -> t'")
+  apply (ind_cases2 "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
     apply hypsubst
-    apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
+    apply (ind_cases2 "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
     apply (rule subst_lemma)
       apply assumption
      apply assumption
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -73,11 +73,10 @@
   -- {* Currently needed for strange technical reasons *}
   by (unfold listall_def) simp
 
-consts NF :: "dB set"
-inductive NF
-intros
-  App: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow> Var x \<degree>\<degree> ts \<in> NF"
-  Abs: "t \<in> NF \<Longrightarrow> Abs t \<in> NF"
+inductive2 NF :: "dB \<Rightarrow> bool"
+where
+  App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)"
+| Abs: "NF t \<Longrightarrow> NF (Abs t)"
 monos listall_def
 
 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
@@ -94,26 +93,26 @@
   apply (simp del: simp_thms, iprover?)+
   done
 
-lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF"
-  shows "listall (\<lambda>t. t \<in> NF) ts" using NF
+lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"
+  shows "listall NF ts" using NF
   by cases simp_all
 
 
 subsection {* Properties of @{text NF} *}
 
-lemma Var_NF: "Var n \<in> NF"
-  apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> NF")
+lemma Var_NF: "NF (Var n)"
+  apply (subgoal_tac "NF (Var n \<degree>\<degree> [])")
    apply simp
   apply (rule NF.App)
   apply simp
   done
 
-lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
-    listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
-    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
+lemma subst_terms_NF: "listall NF ts \<Longrightarrow>
+    listall (\<lambda>t. \<forall>i j. NF (t[Var i/j])) ts \<Longrightarrow>
+    listall NF (map (\<lambda>t. t[Var i/j]) ts)"
   by (induct ts) simp_all
 
-lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
+lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])"
   apply (induct arbitrary: i j set: NF)
   apply simp
   apply (frule listall_conj1)
@@ -132,30 +131,30 @@
   apply (iprover intro: NF.Abs)
   done
 
-lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
   apply (induct set: NF)
   apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}
   apply (rule exI)
   apply (rule conjI)
-  apply (rule rtrancl_refl)
+  apply (rule rtrancl.rtrancl_refl)
   apply (rule NF.App)
   apply (drule listall_conj1)
   apply (simp add: listall_app)
   apply (rule Var_NF)
   apply (rule exI)
   apply (rule conjI)
-  apply (rule rtrancl_into_rtrancl)
-  apply (rule rtrancl_refl)
+  apply (rule rtrancl.rtrancl_into_rtrancl)
+  apply (rule rtrancl.rtrancl_refl)
   apply (rule beta)
   apply (erule subst_Var_NF)
   done
 
-lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
-    listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
-    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
+lemma lift_terms_NF: "listall NF ts \<Longrightarrow>
+    listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow>
+    listall NF (map (\<lambda>t. lift t i) ts)"
   by (induct ts) simp_all
 
-lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
+lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)"
   apply (induct arbitrary: i set: NF)
   apply (frule listall_conj1)
   apply (drule listall_conj2)
@@ -178,13 +177,13 @@
 
 lemma norm_list:
   assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
-  and f_NF: "\<And>t. t \<in> NF \<Longrightarrow> f t \<in> NF"
-  and uNF: "u \<in> NF" and uT: "e \<turnstile> u : T"
+  and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
+  and uNF: "NF u" and uT: "e \<turnstile> u : T"
   shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>
     listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
-      u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)) as \<Longrightarrow>
+      NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
     \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
-      Var j \<degree>\<degree> map f as' \<and> Var j \<degree>\<degree> map f as' \<in> NF"
+      Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')"
   (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")
 proof (induct as rule: rev_induct)
   case (Nil Us)
@@ -200,18 +199,18 @@
   with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
   then obtain bs' where
     bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
-    and bsNF: "\<And>j. Var j \<degree>\<degree> map f bs' \<in> NF" by iprover
+    and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
   from snoc have "?R b" by simp
-  with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF"
+  with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
     by iprover
-  then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF"
+  then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'"
     by iprover
-  from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) (map f bs')"
+  from bsNF [of 0] have "listall NF (map f bs')"
     by (rule App_NF_D)
-  moreover have "f b' \<in> NF" by (rule f_NF)
-  ultimately have "listall (\<lambda>t. t \<in> NF) (map f (bs' @ [b']))"
+  moreover have "NF (f b')" by (rule f_NF)
+  ultimately have "listall NF (map f (bs' @ [b']))"
     by simp
-  hence "\<And>j. Var j \<degree>\<degree> map f (bs' @ [b']) \<in> NF" by (rule NF.App)
+  hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App)
   moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"
     by (rule f_compat)
   with bsred have
@@ -222,18 +221,18 @@
 qed
 
 lemma subst_type_NF:
-  "\<And>t e T u i. t \<in> NF \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> u \<in> NF \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+  "\<And>t e T u i. NF t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> NF u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
   (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
 proof (induct U)
   fix T t
   let ?R = "\<lambda>t. \<forall>e T' u i.
-    e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)"
+    e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')"
   assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
   assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
-  assume "t \<in> NF"
+  assume "NF t"
   thus "\<And>e T' u i. PROP ?Q t e T' u i T"
   proof induct
-    fix e T' u i assume uNF: "u \<in> NF" and uT: "e \<turnstile> u : T"
+    fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
     {
       case (App ts x e_ T'_ u_ i_)
       assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
@@ -241,7 +240,7 @@
 	where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
 	and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
 	by (rule var_app_typesE)
-      from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+      from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
       proof
 	assume eq: "x = i"
 	show ?thesis
@@ -264,20 +263,20 @@
 	  with lift_preserves_beta' lift_NF uNF uT argsT'
 	  have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
             Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
-	    Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by (rule norm_list)
+	    NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
 	  then obtain as' where
 	    asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
 	      Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
-	    and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by iprover
+	    and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover
 	  from App and Cons have "?R a" by simp
-	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF"
+	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'"
 	    by iprover
-	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by iprover
-	  from uNF have "lift u 0 \<in> NF" by (rule lift_NF)
-	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF)
-	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF"
+	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover
+	  from uNF have "NF (lift u 0)" by (rule lift_NF)
+	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF)
+	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'"
 	    by iprover
-	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF"
+	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua"
 	  proof (rule MI1)
 	    have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
 	    proof (rule typing.App)
@@ -287,7 +286,7 @@
 	    with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
 	    from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
 	  qed
-	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF"
+	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
 	    by iprover
 	  from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"
 	    by (rule subst_preserves_beta2')
@@ -296,7 +295,7 @@
 	  also note uared
 	  finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
 	  hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
-	  from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> r \<in> NF"
+	  from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r"
 	  proof (rule MI2)
 	    have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"
 	    proof (rule list_app_typeI)
@@ -315,7 +314,7 @@
 	    with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
 	  qed
 	  then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
-	    and rnf: "r \<in> NF" by iprover
+	    and rnf: "NF r" by iprover
 	  from asred have
 	    "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
 	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
@@ -332,7 +331,7 @@
 	from App have "listall ?R ts" by (iprover dest: listall_conj2)
 	with TrueI TrueI uNF uT argsT
 	have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and>
-	  Var j \<degree>\<degree> ts' \<in> NF" (is "\<exists>ts'. ?ex ts'")
+	  NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
 	  by (rule norm_list [of "\<lambda>t. t", simplified])
 	then obtain ts' where NF: "?ex ts'" ..
 	from nat_le_dec show ?thesis
@@ -348,31 +347,22 @@
       case (Abs r e_ T'_ u_ i_)
       assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
       then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
-      moreover have "lift u 0 \<in> NF" by (rule lift_NF)
+      moreover have "NF (lift u 0)" by (rule lift_NF)
       moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)
-      ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs)
-      thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+      ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
+      thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
 	by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
     }
   qed
 qed
 
 
-consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
-  rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
-
-abbreviation
-  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) where
-  "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
-
-notation (xsymbols)
-  rtyping_rel  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
-
-inductive rtyping
-  intros
+-- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
+inductive2 rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+  where
     Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
-    Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
-    App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"
+  | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
+  | App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"
 
 lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
   apply (induct set: rtyping)
@@ -385,7 +375,7 @@
 
 theorem type_NF:
   assumes "e \<turnstile>\<^sub>R t : T"
-  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
+  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using prems
 proof induct
   case Var
   show ?case by (iprover intro: Var_NF)
@@ -393,16 +383,16 @@
   case Abs
   thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
 next
-  case (App T U e s t)
+  case (App e s T U t)
   from App obtain s' t' where
-    sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"
-    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover
-  have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"
+    sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "NF s'"
+    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
+  have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
   proof (rule subst_type_NF)
-    have "lift t' 0 \<in> NF" by (rule lift_NF)
-    hence "listall (\<lambda>t. t \<in> NF) [lift t' 0]" by (rule listall_cons) (rule listall_nil)
-    hence "Var 0 \<degree>\<degree> [lift t' 0] \<in> NF" by (rule NF.App)
-    thus "Var 0 \<degree> lift t' 0 \<in> NF" by simp
+    have "NF (lift t' 0)" by (rule lift_NF)
+    hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
+    hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
+    thus "NF (Var 0 \<degree> lift t' 0)" by simp
     show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
     proof (rule typing.App)
       show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
@@ -415,9 +405,9 @@
     from sred show "e \<turnstile> s' : T \<Rightarrow> U"
       by (rule subject_reduction') (rule rtyping_imp_typing)
   qed
-  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover
+  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
   from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
-  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)
+  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans')
   with unf show ?case by iprover
 qed
 
@@ -427,23 +417,23 @@
 declare NF.induct [ind_realizer]
 declare rtrancl.induct [ind_realizer irrelevant]
 declare rtyping.induct [ind_realizer]
-lemmas [extraction_expand] = trans_def conj_assoc listall_cons_eq
+lemmas [extraction_expand] = conj_assoc listall_cons_eq
 
 extract type_NF
 
-lemma rtranclR_rtrancl_eq: "((a, b) \<in> rtranclR r) = ((a, b) \<in> rtrancl (Collect r))"
+lemma rtranclR_rtrancl_eq: "rtranclR r a b = rtrancl r a b"
   apply (rule iffI)
   apply (erule rtranclR.induct)
-  apply (rule rtrancl_refl)
-  apply (erule rtrancl_into_rtrancl)
-  apply (erule CollectI)
+  apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl.rtrancl_into_rtrancl)
+  apply assumption
   apply (erule rtrancl.induct)
   apply (rule rtranclR.rtrancl_refl)
   apply (erule rtranclR.rtrancl_into_rtrancl)
-  apply (erule CollectD)
+  apply assumption
   done
 
-lemma NFR_imp_NF: "(nf, t) \<in> NFR \<Longrightarrow> t \<in> NF"
+lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
   apply (erule NFR.induct)
   apply (rule NF.intros)
   apply (simp add: listall_def)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -65,27 +65,27 @@
 
 text {* The subclass releation spelled out: *}
 lemma subcls1:
-  "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
+  "subcls1 E = member2 {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
   apply (simp add: subcls1_def2)
   apply (simp add: name_defs class_defs system_defs E_def class_def)
-  apply (auto split: split_if_asm)
+  apply (auto simp: member2_inject split: split_if_asm)
   done
 
 text {* The subclass relation is acyclic; hence its converse is well founded: *}
 lemma notin_rtrancl:
-  "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
-  by (auto elim: converse_rtranclE)  
+  "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False"
+  by (auto elim: converse_rtranclE')
 
-lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
-  apply (rule acyclicI)
+lemma acyclic_subcls1_E: "acyclicP (subcls1 E)"
+  apply (rule acyclicI [to_pred])
   apply (simp add: subcls1)
-  apply (auto dest!: tranclD)
+  apply (auto dest!: tranclD')
   apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
   done
 
-lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
-  apply (rule finite_acyclic_wf_converse)
+lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)"
+  apply (rule finite_acyclic_wf_converse [to_pred])
   apply (simp add: subcls1)
   apply (rule acyclic_subcls1_E)
   done  
@@ -431,8 +431,6 @@
   apply simp+
   done
 
-lemmas [code] = lessThan_0 lessThan_Suc
-
 constdefs
   some_elem :: "'a set \<Rightarrow> 'a"
   "some_elem == (%S. SOME x. x : S)"
@@ -464,7 +462,7 @@
   meta_eq_to_obj_eq [OF JType.sup_def [unfolded exec_lub_def]]
   meta_eq_to_obj_eq [OF JVM_le_unfold]
 
-lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
+lemmas [code ind] = rtrancl.rtrancl_refl converse_rtrancl_into_rtrancl'
 
 code_module BV
 contains
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -190,7 +190,7 @@
 lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer \<Longrightarrow> isIntg v"
   apply (unfold conf_def)
   apply auto
-  apply (erule widen.elims)
+  apply (erule widen.cases)
   apply auto
   apply (cases v)
   apply auto
@@ -322,7 +322,7 @@
       obtain apTs X ST' where
         ST: "ST = rev apTs @ X # ST'" and
         ps: "length apTs = length ps" and
-        w:   "\<forall>x\<in>set (zip apTs ps). x \<in> widen G" and
+        w:   "\<forall>(x, y)\<in>set (zip apTs ps). G \<turnstile> x \<preceq> y" and
         C:   "G \<turnstile> X \<preceq> Class C" and
         mth: "method (G, C) (mn, ps) \<noteq> None"
         by (simp del: app'.simps) blast
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -91,7 +91,7 @@
     from False C
     have "\<not> match_exception_entry G C pc e"
       by - (erule contrapos_nn, 
-            auto simp add: match_exception_entry_def elim: rtrancl_trans)
+            auto simp add: match_exception_entry_def)
     with m
     have "match_exception_table G C pc (e#es) = Some pc'" by simp
     moreover note C
@@ -640,7 +640,7 @@
  apply (simp add: null)
 apply (clarsimp simp add: conf_def obj_ty_def)
 apply (cases v)
-apply (auto intro: rtrancl_trans)
+apply auto
 done
 
 lemmas defs2 = defs1 raise_system_xcpt_def
@@ -838,7 +838,7 @@
     s:  "s = (rev apTs @ X # ST, LT)" and
     l:  "length apTs = length pTs" and
     X:  "G\<turnstile> X \<preceq> Class C'" and
-    w:  "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
+    w:  "\<forall>(x, y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq> y" and
     mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and
     pc: "Suc pc < length ins" and
     eff: "G \<turnstile> norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -224,7 +224,7 @@
   by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
 
 lemma approx_stk_all_widen:
-  "\<lbrakk> approx_stk G hp stk ST; \<forall>x \<in> set (zip ST ST'). x \<in> widen G; length ST = length ST'; wf_prog wt G \<rbrakk> 
+  "\<lbrakk> approx_stk G hp stk ST; \<forall>(x, y) \<in> set (zip ST ST'). G \<turnstile> x \<preceq> y; length ST = length ST'; wf_prog wt G \<rbrakk> 
   \<Longrightarrow> approx_stk G hp stk ST'"
 apply (unfold approx_stk_def)
 apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -10,7 +10,7 @@
 
 
 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
-  by (auto elim: widen.elims)
+  by (auto elim: widen.cases)
 
 
 lemma sup_loc_some [rule_format]:
@@ -42,7 +42,7 @@
 
 lemma all_widen_is_sup_loc:
 "\<forall>b. length a = length b \<longrightarrow> 
-     (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))" 
+     (\<forall>(x, y)\<in>set (zip a b). G \<turnstile> x \<preceq> y) = (G \<turnstile> (map OK a) <=l (map OK b))" 
  (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
 proof (induct "a")
   show "?P []" by simp
@@ -219,7 +219,7 @@
         l:  "length apTs = length list" and
         c:  "is_class G cname" and
         C:  "G \<turnstile> X \<preceq> Class cname" and
-        w:  "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
+        w:  "\<forall>(x, y) \<in> set (zip apTs list). G \<turnstile> x \<preceq> y" and
         m:  "method (G, cname) (mname, list) = Some (mD', rT', b')" and
         x:  "\<forall>C \<in> set (match_any G pc et). is_class G C"
         by (simp del: not_None_eq, elim exE conjE) (rule that)
@@ -261,7 +261,7 @@
       have "G \<turnstile> map OK apTs' <=l map OK list" .
 
       with l'
-      have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
+      have w': "\<forall>(x, y) \<in> set (zip apTs' list). G \<turnstile> x \<preceq> y"
         by (simp add: all_widen_is_sup_loc)
 
       from Invoke s2 l' w' C' m c x
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -155,7 +155,7 @@
 
 lemma acc_err [simp, intro!]:  "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
-apply (simp add: wf_eq_minimal split: err.split)
+apply (simp add: wfP_eq_minimal split: err.split)
 apply clarify
 apply (case_tac "Err : Q")
  apply blast
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -13,7 +13,7 @@
   "super G C == fst (the (class G C))"
 
 lemma superI:
-  "(C,D) \<in> subcls1 G \<Longrightarrow> super G C = D"
+  "G \<turnstile> C \<prec>C1 D \<Longrightarrow> super G C = D"
   by (unfold super_def) (auto dest: subcls1D)
 
 constdefs
@@ -34,7 +34,7 @@
 
   is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool"
   "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
-               (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C,Object):(subcls1 G)^*)"
+               (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (subcls1 G)^** C Object)"
 
 
 translations
@@ -45,10 +45,10 @@
   "esl G == (types G, subtype G, sup G)"
 
 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
-  by (auto elim: widen.elims)
+  by (auto elim: widen.cases)
 
 lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
-  by (auto elim: widen.elims)
+  by (auto elim: widen.cases)
 
 lemma is_tyI:
   "\<lbrakk> is_type G T; ws_prog G \<rbrakk> \<Longrightarrow> is_ty G T"
@@ -77,8 +77,8 @@
     from R wf ty
     have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
      by (auto simp add: is_ty_def is_class_def split_tupled_all
-               elim!: subcls1.elims
-               elim: converse_rtranclE
+               elim!: subcls1.cases
+               elim: converse_rtranclE'
                split: ref_ty.splits)
     ultimately    
     show ?thesis by blast
@@ -86,7 +86,7 @@
 qed
 
 lemma order_widen:
-  "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
+  "acyclicP (subcls1 G) \<Longrightarrow> order (subtype G)"
   apply (unfold Semilat.order_def lesub_def subtype_def)
   apply (auto intro: widen_trans)
   apply (case_tac x)
@@ -102,16 +102,16 @@
   apply (case_tac ref_tya)
    apply simp
   apply simp
-  apply (auto dest: acyclic_impl_antisym_rtrancl antisymD)  
+  apply (auto dest: acyclic_impl_antisym_rtrancl [to_pred] antisymD)
   done
 
 lemma wf_converse_subcls1_impl_acc_subtype:
-  "wf ((subcls1 G)^-1) \<Longrightarrow> acc (subtype G)"
-apply (unfold acc_def lesssub_def)
-apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
- apply blast
-apply (drule wf_trancl)
-apply (simp add: wf_eq_minimal)
+  "wfP ((subcls1 G)^--1) \<Longrightarrow> acc (subtype G)"
+apply (unfold Semilat.acc_def lesssub_def)
+apply (drule_tac p = "meet ((subcls1 G)^--1) op \<noteq>" in wfP_subset)
+ apply auto
+apply (drule wfP_trancl)
+apply (simp add: wfP_eq_minimal)
 apply clarify
 apply (unfold lesub_def subtype_def)
 apply (rename_tac M T) 
@@ -146,20 +146,20 @@
 apply (case_tac t)
  apply simp
 apply simp
-apply (insert rtrancl_r_diff_Id [symmetric, standard, of "(subcls1 G)"])
+apply (insert rtrancl_r_diff_Id' [symmetric, standard, of "subcls1 G"])
 apply simp
-apply (erule rtranclE)
+apply (erule rtrancl.cases)
  apply blast
-apply (drule rtrancl_converseI)
-apply (subgoal_tac "((subcls1 G)-Id)^-1 = ((subcls1 G)^-1 - Id)")
+apply (drule rtrancl_converseI')
+apply (subgoal_tac "(meet (subcls1 G) op \<noteq>)^--1 = (meet ((subcls1 G)^--1) op \<noteq>)")
  prefer 2
- apply blast
-apply simp 
-apply (blast intro: rtrancl_into_trancl2)
+ apply (simp add: converse_meet)
+apply simp
+apply (blast intro: rtrancl_into_trancl2')
 done 
 
 lemma closed_err_types:
-  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
+  "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G) \<rbrakk> 
   \<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
   apply (unfold closed_def plussub_def lift2_def sup_def)
   apply (auto split: err.split)
@@ -171,13 +171,13 @@
 
 
 lemma sup_subtype_greater:
-  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
+  "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G);
       is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk> 
   \<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
 proof -
   assume ws_prog:       "ws_prog G"
-  assume single_valued: "single_valued (subcls1 G)" 
-  assume acyclic:       "acyclic (subcls1 G)"
+  assume single_valued: "single_valuedP (subcls1 G)"
+  assume acyclic:       "acyclicP (subcls1 G)"
  
   { fix c1 c2
     assume is_class: "is_class G c1" "is_class G c2"
@@ -188,12 +188,12 @@
       by (blast intro: subcls_C_Object)
     with ws_prog single_valued
     obtain u where
-      "is_lub ((subcls1 G)^* ) c1 c2 u"      
+      "is_lub ((subcls1 G)^** ) c1 c2 u"
       by (blast dest: single_valued_has_lubs)
     moreover
     note acyclic
     moreover
-    have "\<forall>x y. (x, y) \<in> subcls1 G \<longrightarrow> super G x = y"
+    have "\<forall>x y. G \<turnstile> x \<prec>C1 y \<longrightarrow> super G x = y"
       by (blast intro: superI)
     ultimately
     have "G \<turnstile> c1 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2 \<and>
@@ -210,14 +210,14 @@
 qed
 
 lemma sup_subtype_smallest:
-  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
+  "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G);
       is_type G a; is_type G b; is_type G c; 
       subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
   \<Longrightarrow> subtype G d c"
 proof -
   assume ws_prog:       "ws_prog G"
-  assume single_valued: "single_valued (subcls1 G)" 
-  assume acyclic:       "acyclic (subcls1 G)"
+  assume single_valued: "single_valuedP (subcls1 G)"
+  assume acyclic:       "acyclicP (subcls1 G)"
 
   { fix c1 c2 D
     assume is_class: "is_class G c1" "is_class G c2"
@@ -229,7 +229,7 @@
       by (blast intro: subcls_C_Object)
     with ws_prog single_valued
     obtain u where
-      lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
+      lub: "is_lub ((subcls1 G)^** ) c1 c2 u"
       by (blast dest: single_valued_has_lubs)   
     with acyclic
     have "exec_lub (subcls1 G) (super G) c1 c2 = u"
@@ -260,12 +260,12 @@
            split: ty.splits ref_ty.splits)
 
 lemma err_semilat_JType_esl_lemma:
-  "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
+  "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G) \<rbrakk> 
   \<Longrightarrow> err_semilat (esl G)"
 proof -
   assume ws_prog:   "ws_prog G"
-  assume single_valued: "single_valued (subcls1 G)" 
-  assume acyclic:   "acyclic (subcls1 G)"
+  assume single_valued: "single_valuedP (subcls1 G)"
+  assume acyclic:   "acyclicP (subcls1 G)"
   
   hence "order (subtype G)"
     by (rule order_widen)
@@ -297,9 +297,9 @@
 qed
 
 lemma single_valued_subcls1:
-  "ws_prog G \<Longrightarrow> single_valued (subcls1 G)"
+  "ws_prog G \<Longrightarrow> single_valuedP (subcls1 G)"
   by (auto simp add: ws_prog_def unique_def single_valued_def
-    intro: subcls1I elim!: subcls1.elims)
+    intro: subcls1I elim!: subcls1.cases)
 
 theorem err_semilat_JType_esl:
   "ws_prog G \<Longrightarrow> err_semilat (esl G)"
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -40,7 +40,7 @@
 	 simp add: symmetric sl_triple_conv)
       apply (simp (no_asm) add: JVM_le_unfold)
       apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
-                   dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
+                   dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog)
      apply (simp add: JVM_le_unfold)
     apply (erule exec_pres_type)
    apply assumption
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -193,7 +193,7 @@
 
 lemma widen_PrimT_conv1 [simp]:
   "\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
-  by (auto elim: widen.elims)
+  by (auto elim: widen.cases)
 
 theorem sup_PTS_eq:
   "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -402,7 +402,7 @@
 -- "Well-foundedness of the termination relation:"
 apply (rule wf_lex_prod)
  apply (insert orderI [THEN acc_le_listI])
- apply (simp only: acc_def lesssub_def)
+ apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
 apply (rule wf_finite_psubset) 
 
 -- "Loop decreases along termination relation:"
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -321,22 +321,22 @@
   "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
 apply (unfold acc_def)
 apply (subgoal_tac
- "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
- apply (erule wf_subset)
+ "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))")
+ apply (erule wfP_subset)
  apply (blast intro: lesssub_list_impl_same_size)
-apply (rule wf_UN)
+apply (rule wfP_SUP)
  prefer 2
  apply clarify
  apply (rename_tac m n)
  apply (case_tac "m=n")
   apply simp
- apply (fast intro!: equals0I dest: not_sym)
+ apply (fast intro!: equals0I [to_pred] dest: not_sym)
 apply clarify
 apply (rename_tac n)
 apply (induct_tac n)
  apply (simp add: lesssub_def cong: conj_cong)
 apply (rename_tac k)
-apply (simp add: wf_eq_minimal)
+apply (simp add: wfP_eq_minimal)
 apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
 apply clarify
 apply (rename_tac M m)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -272,7 +272,7 @@
 lemma acc_le_optI [intro!]:
   "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
-apply (simp add: wf_eq_minimal split: option.split)
+apply (simp add: wfP_eq_minimal split: option.split)
 apply clarify
 apply (case_tac "? a. Some a : Q")
  apply (erule_tac x = "{a . Some a : Q}" in allE)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -51,8 +51,8 @@
 lemma acc_le_prodI [intro!]:
   "\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
 apply (unfold acc_def)
-apply (rule wf_subset)
- apply (erule wf_lex_prod)
+apply (rule wfP_subset)
+ apply (erule wf_lex_prod [to_pred, THEN wfP_wf_eq [THEN iffD2]])
  apply assumption
 apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
 done
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -40,16 +40,13 @@
 
 
 constdefs
- ord :: "('a*'a)set \<Rightarrow> 'a ord"
-"ord r == %x y. (x,y):r"
-
  order :: "'a ord \<Rightarrow> bool"
 "order r == (!x. x <=_r x) &
             (!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) &
             (!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)"
 
  acc :: "'a ord \<Rightarrow> bool"
-"acc r == wf{(y,x) . x <_r y}"
+"acc r == wfP (\<lambda>y x. x <_r y)"
 
  top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
 "top r T == !x. x <=_r T"
@@ -63,13 +60,13 @@
                 (!x:A. !y:A. y <=_r x +_f y)  &
                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
 
- is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-"is_ub r x y u == (x,u):r & (y,u):r"
+ is_ub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_ub r x y u == r x u & r y u"
 
- is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
+ is_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> r u z)"
 
- some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ some_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z";
 
 locale (open) semilat =
@@ -244,113 +241,113 @@
 by(blast intro: order_antisym plus_com_lemma)
 
 lemma is_lubD:
-  "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
+  "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> r u z)"
   by (simp add: is_lub_def)
 
 lemma is_ubI:
-  "\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u"
+  "\<lbrakk> r x u; r y u \<rbrakk> \<Longrightarrow> is_ub r x y u"
   by (simp add: is_ub_def)
 
 lemma is_ubD:
-  "is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r"
+  "is_ub r x y u \<Longrightarrow> r x u & r y u"
   by (simp add: is_ub_def)
 
 
 lemma is_lub_bigger1 [iff]:  
-  "is_lub (r^* ) x y y = ((x,y):r^* )"
+  "is_lub (r^** ) x y y = r^** x y"
 apply (unfold is_lub_def is_ub_def)
 apply blast
 done
 
 lemma is_lub_bigger2 [iff]:
-  "is_lub (r^* ) x y x = ((y,x):r^* )"
+  "is_lub (r^** ) x y x = r^** y x"
 apply (unfold is_lub_def is_ub_def)
 apply blast 
 done
 
 lemma extend_lub:
-  "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk> 
-  \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
+  "\<lbrakk> single_valuedP r; is_lub (r^** ) x y u; r x' x \<rbrakk> 
+  \<Longrightarrow> EX v. is_lub (r^** ) x' y v"
 apply (unfold is_lub_def is_ub_def)
-apply (case_tac "(y,x) : r^*")
- apply (case_tac "(y,x') : r^*")
+apply (case_tac "r^** y x")
+ apply (case_tac "r^** y x'")
   apply blast
- apply (blast elim: converse_rtranclE dest: single_valuedD)
+ apply (blast elim: converse_rtranclE' dest: single_valuedD)
 apply (rule exI)
 apply (rule conjI)
- apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD)
-apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 
-             elim: converse_rtranclE dest: single_valuedD)
+ apply (blast intro: converse_rtrancl_into_rtrancl' dest: single_valuedD)
+apply (blast intro: rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl'
+             elim: converse_rtranclE' dest: single_valuedD)
 done
 
 lemma single_valued_has_lubs [rule_format]:
-  "\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow> 
-  (EX z. is_lub (r^* ) x y z))"
-apply (erule converse_rtrancl_induct)
+  "\<lbrakk> single_valuedP r; r^** x u \<rbrakk> \<Longrightarrow> (!y. r^** y u \<longrightarrow> 
+  (EX z. is_lub (r^** ) x y z))"
+apply (erule converse_rtrancl_induct')
  apply clarify
- apply (erule converse_rtrancl_induct)
+ apply (erule converse_rtrancl_induct')
   apply blast
- apply (blast intro: converse_rtrancl_into_rtrancl)
+ apply (blast intro: converse_rtrancl_into_rtrancl')
 apply (blast intro: extend_lub)
 done
 
 lemma some_lub_conv:
-  "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
+  "\<lbrakk> acyclicP r; is_lub (r^** ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^** ) x y = u"
 apply (unfold some_lub_def is_lub_def)
 apply (rule someI2)
  apply assumption
-apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl)
+apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl [to_pred])
 done
 
 lemma is_lub_some_lub:
-  "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk> 
-  \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+  "\<lbrakk> single_valuedP r; acyclicP r; r^** x u; r^** y u \<rbrakk> 
+  \<Longrightarrow> is_lub (r^** ) x y (some_lub (r^** ) x y)";
   by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
 
 subsection{*An executable lub-finder*}
 
 constdefs
- exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop"
-"exec_lub r f x y == while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y"
+ exec_lub :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop"
+"exec_lub r f x y == while (\<lambda>z. \<not> r\<^sup>*\<^sup>* x z) f y"
 
 
 lemma acyclic_single_valued_finite:
- "\<lbrakk>acyclic r; single_valued r; (x,y) \<in> r\<^sup>*\<rbrakk>
-  \<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})"
-apply(erule converse_rtrancl_induct)
+ "\<lbrakk>acyclicP r; single_valuedP r; r\<^sup>*\<^sup>* x y \<rbrakk>
+  \<Longrightarrow> finite (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y})"
+apply(erule converse_rtrancl_induct')
  apply(rule_tac B = "{}" in finite_subset)
-  apply(simp only:acyclic_def)
-  apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl)
+  apply(simp only:acyclic_def [to_pred])
+  apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
  apply simp
 apply(rename_tac x x')
-apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} =
-                   insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})")
+apply(subgoal_tac "Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y} =
+                   insert (x,x') (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x' a} \<times> {b. r\<^sup>*\<^sup>* b y})")
  apply simp
-apply(blast intro:converse_rtrancl_into_rtrancl
-            elim:converse_rtranclE dest:single_valuedD)
+apply(blast intro:converse_rtrancl_into_rtrancl'
+            elim:converse_rtranclE' dest:single_valuedD)
 done
 
 
 lemma exec_lub_conv:
-  "\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
+  "\<lbrakk> acyclicP r; !x y. r x y \<longrightarrow> f x = y; is_lub (r\<^sup>*\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
   exec_lub r f x y = u";
 apply(unfold exec_lub_def)
-apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and
-               r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule)
+apply(rule_tac P = "\<lambda>z. r\<^sup>*\<^sup>* y z \<and> r\<^sup>*\<^sup>* z u" and
+               r = "(Collect2 r \<inter> {(a,b). r\<^sup>*\<^sup>* y a \<and> r\<^sup>*\<^sup>* b u})^-1" in while_rule)
     apply(blast dest: is_lubD is_ubD)
    apply(erule conjE)
-   apply(erule_tac z = u in converse_rtranclE)
+   apply(erule_tac z = u in converse_rtranclE')
     apply(blast dest: is_lubD is_ubD)
-   apply(blast dest:rtrancl_into_rtrancl)
+   apply(blast dest: rtrancl.rtrancl_into_rtrancl)
   apply(rename_tac s)
-  apply(subgoal_tac "is_ub (r\<^sup>*) x y s")
+  apply(subgoal_tac "is_ub (r\<^sup>*\<^sup>*) x y s")
    prefer 2; apply(simp add:is_ub_def)
-  apply(subgoal_tac "(u, s) \<in> r\<^sup>*")
+  apply(subgoal_tac "r\<^sup>*\<^sup>* u s")
    prefer 2; apply(blast dest:is_lubD)
-  apply(erule converse_rtranclE)
+  apply(erule converse_rtranclE')
    apply blast
-  apply(simp only:acyclic_def)
-  apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl)
+  apply(simp only:acyclic_def [to_pred])
+  apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
  apply(rule finite_acyclic_wf)
   apply simp
   apply(erule acyclic_single_valued_finite)
@@ -361,14 +358,14 @@
  apply blast
 apply simp
 apply(erule conjE)
-apply(erule_tac z = u in converse_rtranclE)
+apply(erule_tac z = u in converse_rtranclE')
  apply(blast dest: is_lubD is_ubD)
-apply(blast dest:rtrancl_into_rtrancl)
+apply blast
 done
 
 lemma is_lub_exec_lub:
-  "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; !x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk>
-  \<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)"
+  "\<lbrakk> single_valuedP r; acyclicP r; r^** x u; r^** y u; !x y. r x y \<longrightarrow> f x = y \<rbrakk>
+  \<Longrightarrow> is_lub (r^** ) x y (exec_lub r f x y)"
   by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv)
 
 end
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -14,14 +14,14 @@
 (* If no exception is present after evaluation/execution, 
   none can have been present before *)
 lemma eval_evals_exec_xcpt:
- "((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
-  ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
-  ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
+ "(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
+  (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
+  (G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
 by (induct rule: eval_evals_exec.induct, auto)
 
 
 (* instance of eval_evals_exec_xcpt for eval *)
-lemma eval_xcpt: "(xs,ex,val,xs') \<in> Eval.eval G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+lemma eval_xcpt: "G \<turnstile> xs -ex\<succ>val-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
  (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
 proof-
   assume h1: ?H1
@@ -30,7 +30,7 @@
 qed
 
 (* instance of eval_evals_exec_xcpt for evals *)
-lemma evals_xcpt: "(xs,exs,vals,xs') \<in> Eval.evals G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+lemma evals_xcpt: "G \<turnstile> xs -exs[\<succ>]vals-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
  (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
 proof-
   assume h1: ?H1
@@ -39,7 +39,7 @@
 qed
 
 (* instance of eval_evals_exec_xcpt for exec *)
-lemma exec_xcpt: "(xs,st,xs') \<in> Eval.exec G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+lemma exec_xcpt: "G \<turnstile> xs -st-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
  (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
 proof-
   assume h1: ?H1
@@ -404,7 +404,7 @@
        E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
 apply (simp only: wtpd_expr_def wtpd_exprs_def)
 apply (erule exE)
-apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T")
+apply (ind_cases2 "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
 apply (auto simp: max_spec_preserves_length)
 done
 
@@ -437,7 +437,7 @@
   "\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) & 
   (G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow>  (\<exists> s. (xs' = (None, s))) \<longrightarrow> 
   length es = length vs) &
-  ((xc, xb, xa) \<in> Eval.exec G \<longrightarrow> True)")
+  (G \<turnstile> xc -xb-> xa \<longrightarrow> True)")
 apply blast
 apply (rule allI)
 apply (rule Eval.eval_evals_exec.induct)
@@ -576,7 +576,7 @@
 done
 
 lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es;
-  (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
+  prg E \<turnstile> xs -es[\<succ>]vs-> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
 apply (simp only: wtpd_exprs_def)
 apply (erule exE)
 apply (case_tac xs) apply (case_tac xs')
@@ -584,7 +584,7 @@
 done
 
 lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st;
-  (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
+  prg E \<turnstile> xs -st-> xs'\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
 apply (simp only: wtpd_stmt_def)
 apply (case_tac xs', case_tac xs)
 apply (auto dest: exec_type_sound)
@@ -618,13 +618,13 @@
 apply simp
 apply (rule allI)
 apply (rule iffI)
-  apply (ind_cases "E \<turnstile> [] [::] Ts", assumption)
+  apply (ind_cases2 "E \<turnstile> [] [::] Ts" for Ts, assumption)
   apply simp apply (rule WellType.Nil)
 apply (simp add: list_all2_Cons1)
 apply (rule allI)
 apply (rule iffI)
   apply (rename_tac a exs Ts)
-  apply (ind_cases "E \<turnstile> a # exs  [::] Ts") apply blast
+  apply (ind_cases2 "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
   apply (auto intro: WellType.Cons)
 done
 
@@ -718,7 +718,7 @@
 (* 2. possibly skip env_of_jmb ??? *)
 theorem compiler_correctness: 
   "wf_java_prog G \<Longrightarrow>
-  ((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow>
+  (G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow>
   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
   (\<forall> os CL S.
   (class_sig_defined G CL S) \<longrightarrow> 
@@ -729,7 +729,7 @@
     >- (compExpr (gmb G CL S) ex) \<rightarrow>
     {gh xs', val#os, locvars_xstate G CL S xs'}))) \<and> 
 
- ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow>
+ (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow>
   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
   (\<forall> os CL S.
   (class_sig_defined G CL S) \<longrightarrow> 
@@ -740,7 +740,7 @@
     >- (compExprs (gmb G CL S) exs) \<rightarrow>
     {gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and> 
 
-  ((xs,st,xs') \<in> Eval.exec G \<longrightarrow>
+  (G \<turnstile> xs -st-> xs' \<longrightarrow>
    gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
   (\<forall> os CL S.
   (class_sig_defined G CL S) \<longrightarrow> 
@@ -1189,7 +1189,7 @@
   (* show list_all2 (conf G h) pvs pTs *)
 apply (erule exE)+ apply (erule conjE)+
 apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption
-apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
+apply (subgoal_tac "G \<turnstile> (gx s1, gs s1) -ps[\<succ>]pvs-> (x, h, l)")
 apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
 apply assumption+
 apply (simp only: env_of_jmb_fst) 
@@ -1247,7 +1247,7 @@
 done
 
 theorem compiler_correctness_exec: "
-  \<lbrakk> ((None,hp,loc), st, (None,hp',loc')) \<in> Eval.exec G;
+  \<lbrakk> G \<turnstile> Norm (hp, loc) -st-> Norm (hp', loc');
   wf_java_prog G;
   class_sig_defined G C S;
   wtpd_stmt (env_of_jmb G C S) st;
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -109,22 +109,24 @@
 by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
 
 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
-by (auto simp add: subcls1_def2 comp_classname comp_is_class)
+by (auto simp add: subcls1_def2 comp_classname comp_is_class member2_inject)
 
-lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
-  apply rule
-  apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) 
+lemma comp_widen: "widen (comp G) = widen G"
+  apply (simp add: expand_fun_eq)
+  apply (intro allI iffI)
+  apply (erule widen.cases) 
   apply (simp_all add: comp_subcls1 widen.null)
-  apply (cases "(ty1,ty2)" G rule: widen.cases) 
+  apply (erule widen.cases) 
   apply (simp_all add: comp_subcls1 widen.null)
   done
 
-lemma comp_cast: "((ty1,ty2) \<in> cast (comp G)) = ((ty1,ty2) \<in> cast G)"
-  apply rule
-  apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) 
+lemma comp_cast: "cast (comp G) = cast G"
+  apply (simp add: expand_fun_eq)
+  apply (intro allI iffI)
+  apply (erule cast.cases) 
   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   apply (rule cast.widen) apply (simp add: comp_widen)
-  apply (cases "(ty1,ty2)" G rule: cast.cases)
+  apply (erule cast.cases)
   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   apply (rule cast.widen) apply (simp add: comp_widen)
   done
@@ -180,16 +182,16 @@
 done
 
 
-lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> 
+lemma comp_class_rec: " wfP ((subcls1 G)^--1) \<Longrightarrow> 
 class_rec (comp G) C t f = 
   class_rec G C t (\<lambda> C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')"
-apply (rule_tac a = C in  wf_induct) apply assumption
-apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
+apply (rule_tac a = C in  wfP_induct) apply assumption
+apply (subgoal_tac "wfP ((subcls1 (comp G))\<inverse>\<inverse>)")
 apply (subgoal_tac "(class G x = None) \<or> (\<exists> D fs ms. (class G x = Some (D, fs, ms)))")
 apply (erule disjE)
 
   (* case class G x = None *)
-apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec cut_apply)
+apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec [to_pred] cut_apply)
 apply (simp add: comp_class_None)
 
   (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
@@ -214,11 +216,11 @@
 apply (simp add: comp_subcls1)
 done
 
-lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> 
+lemma comp_fields: "wfP ((subcls1 G)^--1) \<Longrightarrow> 
   fields (comp G,C) = fields (G,C)" 
 by (simp add: fields_def comp_class_rec)
 
-lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> 
+lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow> 
   field (comp G,C) = field (G,C)" 
 by (simp add: field_def comp_fields)
 
@@ -230,7 +232,7 @@
   \<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow> 
   R (class_rec G C t1 f1) (class_rec G C t2 f2)"
 apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *)
-apply (rule_tac a = C in  wf_induct) apply assumption
+apply (rule_tac a = C in  wfP_induct) apply assumption
 apply (intro strip)
 apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
   apply (erule exE)+
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -32,86 +32,62 @@
 
   -- "Evaluation relations"
 
-consts
-  eval  :: "java_mb prog => (xstate \<times> expr      \<times> val      \<times> xstate) set"
-  evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
-  exec  :: "java_mb prog => (xstate \<times> stmt                 \<times> xstate) set"
-
-syntax (xsymbols)
+inductive2
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
           ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
-  evals:: "[java_mb prog,xstate,expr list,
+  and evals :: "[java_mb prog,xstate,expr list,
                         val list,xstate] => bool "
           ("_ \<turnstile> _ -_[\<succ>]_-> _" [51,82,60,51,82] 81)
-  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
+  and exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
           ("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
-
-syntax
-  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
-          ("_ |- _ -_>_-> _" [51,82,60,82,82] 81)
-  evals:: "[java_mb prog,xstate,expr list,
-                        val list,xstate] => bool "
-          ("_ |- _ -_[>]_-> _" [51,82,60,51,82] 81)
-  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
-          ("_ |- _ -_-> _" [51,82,60,82] 81)
-
+  for G :: "java_mb prog"
+where
 
-translations
-  "G\<turnstile>s -e \<succ> v-> (x,s')" <= "(s, e, v, x, s') \<in> eval  G"
-  "G\<turnstile>s -e \<succ> v->    s' " == "(s, e, v,    s') \<in> eval  G"
-  "G\<turnstile>s -e[\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \<in> evals G"
-  "G\<turnstile>s -e[\<succ>]v->    s' " == "(s, e, v,    s') \<in> evals G"
-  "G\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \<in> exec G"
-  "G\<turnstile>s -c    ->    s' " == "(s, c,    s') \<in> exec G"
-
-
-inductive "eval G" "evals G" "exec G" intros
-
-  (* evaluation of expressions *)
+  -- "evaluation of expressions"
 
   XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"  -- "cf. 15.5"
 
   -- "cf. 15.8.1"
-  NewC: "[| h = heap s; (a,x) = new_Addr h;
+| NewC: "[| h = heap s; (a,x) = new_Addr h;
             h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
          G\<turnstile>Norm s -NewC C\<succ>Addr a-> c_hupd h' (x,s)"
 
   -- "cf. 15.15"
-  Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
+| Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
             x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
          G\<turnstile>Norm s0 -Cast C e\<succ>v-> (x2,s1)"
 
   -- "cf. 15.7.1"
-  Lit:  "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
+| Lit:  "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
 
-  BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
+| BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
             G\<turnstile>s1     -e2\<succ>v2-> s2;
             v = (case bop of Eq  => Bool (v1 = v2)
                            | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
          G\<turnstile>Norm s -BinOp bop e1 e2\<succ>v-> s2"
 
   -- "cf. 15.13.1, 15.2"
-  LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
+| LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
 
   -- "cf. 15.25.1"
-  LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
+| LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
             l' = (if x = None then l(va\<mapsto>v) else l) |] ==>
          G\<turnstile>Norm s -va::=e\<succ>v-> (x,(h,l'))"
 
   -- "cf. 15.10.1, 15.2"
-  FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1); 
+| FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1); 
             v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
          G\<turnstile>Norm s0 -{T}e..fn\<succ>v-> (np a' x1,s1)"
 
   -- "cf. 15.25.1"
-  FAss: "[| G\<turnstile>     Norm s0  -e1\<succ>a'-> (x1,s1); a = the_Addr a';
+| FAss: "[| G\<turnstile>     Norm s0  -e1\<succ>a'-> (x1,s1); a = the_Addr a';
             G\<turnstile>(np a' x1,s1) -e2\<succ>v -> (x2,s2);
             h  = heap s2; (c,fs) = the (h a);
             h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
          G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
 
   -- "cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15"
-  Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
+| Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
             G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
             (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
             G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
@@ -122,13 +98,13 @@
   -- "evaluation of expression lists"
 
   -- "cf. 15.5"
-  XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
+| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
 
   -- "cf. 15.11.???"
-  Nil:  "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
+| Nil:  "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
 
   -- "cf. 15.6.4"
-  Cons: "[| G\<turnstile>Norm s0 -e  \<succ> v -> s1;
+| Cons: "[| G\<turnstile>Norm s0 -e  \<succ> v -> s1;
             G\<turnstile>     s1 -es[\<succ>]vs-> s2 |] ==>
          G\<turnstile>Norm s0 -e#es[\<succ>]v#vs-> s2"
 
@@ -136,29 +112,29 @@
   -- "execution of statements"
 
   -- "cf. 14.1"
-  XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
+| XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
 
   -- "cf. 14.5"
-  Skip: "G\<turnstile>Norm s -Skip-> Norm s"
+| Skip: "G\<turnstile>Norm s -Skip-> Norm s"
 
   -- "cf. 14.7"
-  Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
+| Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
          G\<turnstile>Norm s0 -Expr e-> s1"
 
   -- "cf. 14.2"
-  Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
+| Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
             G\<turnstile>     s1 -c2-> s2|] ==>
          G\<turnstile>Norm s0 -c1;; c2-> s2"
 
   -- "cf. 14.8.2"
-  Cond: "[| G\<turnstile>Norm s0  -e\<succ>v-> s1;
+| Cond: "[| G\<turnstile>Norm s0  -e\<succ>v-> s1;
             G\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
          G\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
 
   -- "cf. 14.10, 14.10.1"
-  LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
+| LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
          G\<turnstile>Norm s0 -While(e) c-> s1"
-  LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1;  the_Bool v;
+| LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1;  the_Bool v;
       G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
          G\<turnstile>Norm s0 -While(e) c-> s3"
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -172,19 +172,19 @@
 apply (simp (no_asm))
 done
 
-lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R"
-apply (auto dest!: tranclD subcls1D)
+lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R"
+apply (auto dest!: tranclD' subcls1D)
 done
 
 lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
-apply (erule rtrancl_induct)
+apply (erule rtrancl_induct')
 apply  auto
 apply (drule subcls1D)
 apply auto
 done
 
-lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R"
-apply (auto dest!: tranclD subcls1D)
+lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R"
+apply (auto dest!: tranclD' subcls1D)
 done
 
 lemma class_tprgD: 
@@ -193,11 +193,11 @@
 apply (auto split add: split_if_asm simp add: map_of_Cons)
 done
 
-lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R"
-apply (auto dest!: tranclD subcls1D)
+lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R"
+apply (auto dest!: tranclD' subcls1D)
 apply (frule class_tprgD)
 apply (auto dest!:)
-apply (drule rtranclD)
+apply (drule rtranclD')
 apply auto
 done
 
@@ -205,7 +205,7 @@
 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
 done
 
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl' [where r="subcls1 G"], standard]
 
 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
 apply (rule subcls_direct)
@@ -219,12 +219,12 @@
 
 declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
 
-lemma acyclic_subcls1_: "acyclic (subcls1 tprg)"
-apply (rule acyclicI)
+lemma acyclic_subcls1_: "acyclicP (subcls1 tprg)"
+apply (rule acyclicI [to_pred])
 apply safe
 done
 
-lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
+lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
 
 lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
 
@@ -345,7 +345,7 @@
 apply (fold ExtC_def)
 apply (rule mp) defer apply (rule wf_foo_Ext)
 apply (auto simp add: wf_mdecl_def)
-apply (drule rtranclD)
+apply (drule rtranclD')
 apply auto
 done
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -27,7 +27,7 @@
 apply (case_tac "ref_ty")
 apply (clarsimp simp add: conf_def)
 apply simp
-apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp) 
+apply (ind_cases2 "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
 apply (rule conf_widen, assumption+) apply (erule widen.subcls)
 
 apply (unfold cast_ok_def)
@@ -205,7 +205,7 @@
 -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
 apply( simp_all)
 apply( tactic "ALLGOALS strip_tac")
-apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
+apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
                  THEN_ALL_NEW Full_simp_tac) *})
 apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
 
@@ -222,7 +222,7 @@
 apply( rule conjI)
 apply(  force elim!: NewC_conforms)
 apply( rule conf_obj_AddrI)
-apply(  rule_tac [2] rtrancl_refl)
+apply(  rule_tac [2] rtrancl.rtrancl_refl)
 apply( simp (no_asm))
 
 -- "for Cast"
@@ -245,22 +245,22 @@
 apply( fast elim: conforms_localD [THEN lconfD])
 
 -- "for FAss"
-apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
+apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
        THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
 
 -- "for if"
-apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
+apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 7*})
 
 apply (tactic "forward_hyp_tac")
 
 -- "11+1 if"
-prefer 8
+prefer 7
 apply(  fast intro: hext_trans)
-prefer 8
+prefer 7
 apply(  fast intro: hext_trans)
 
 -- "10 Expr"
-prefer 7
+prefer 6
 apply( fast)
 
 -- "9 ???"
@@ -280,7 +280,7 @@
 
 -- "7 LAss"
 apply (fold fun_upd_def)
-apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
+apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
                  THEN_ALL_NEW Full_simp_tac) 1 *})
 apply (intro strip)
 apply (case_tac E)
@@ -315,7 +315,7 @@
 
 
 -- "2 FAss"
-apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
+apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)")
   prefer 2
   apply (simp add: np_def)
   apply (fast intro: conforms_xcpt_change xconf_raise_if)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -8,61 +8,45 @@
 
 theory TypeRel imports Decl begin
 
-consts
-  subcls1 :: "'c prog => (cname \<times> cname) set"  -- "subclass"
-  widen   :: "'c prog => (ty    \<times> ty   ) set"  -- "widening"
-  cast    :: "'c prog => (ty    \<times> ty   ) set"  -- "casting"
-
-syntax (xsymbols)
+-- "direct subclass, cf. 8.1.3"
+inductive2
   subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
-  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
-  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
-  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
+  for G :: "'c prog"
+where
+  subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
 
-syntax
-  subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
-  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
-  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
-  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
-
-translations
-  "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
-  "G\<turnstile>C \<preceq>C  D" == "(C,D) \<in> (subcls1 G)^*"
-  "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
-  "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
-
--- "direct subclass, cf. 8.1.3"
-inductive "subcls1 G" intros
-  subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
+abbreviation
+  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
+  where "G\<turnstile>C \<preceq>C  D \<equiv> (subcls1 G)^** C D"
   
 lemma subcls1D: 
   "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
-apply (erule subcls1.elims)
+apply (erule subcls1.cases)
 apply auto
 done
 
 lemma subcls1_def2: 
-  "subcls1 G = 
+  "subcls1 G = member2
      (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
-  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
+  by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I)
 
-lemma finite_subcls1: "finite (subcls1 G)"
-apply(subst subcls1_def2)
+lemma finite_subcls1: "finite (Collect2 (subcls1 G))"
+apply(simp add: subcls1_def2)
 apply(rule finite_SigmaI [OF finite_is_class])
 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
 apply  auto
 done
 
-lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C"
+lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C"
 apply (unfold is_class_def)
-apply(erule trancl_trans_induct)
+apply(erule trancl_trans_induct')
 apply (auto dest!: subcls1D)
 done
 
 lemma subcls_is_class2 [rule_format (no_asm)]: 
   "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
 apply (unfold is_class_def)
-apply (erule rtrancl_induct)
+apply (erule rtrancl_induct')
 apply  (drule_tac [2] subcls1D)
 apply  auto
 done
@@ -70,18 +54,19 @@
 constdefs
   class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
     (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
-  "class_rec G == wfrec ((subcls1 G)^-1)
+  "class_rec G == wfrec (Collect2 ((subcls1 G)^--1))
     (\<lambda>r C t f. case class G C of
          None \<Rightarrow> arbitrary
        | Some (D,fs,ms) \<Rightarrow> 
            f C fs ms (if C = Object then t else r D t f))"
 
-lemma class_rec_lemma: "wf ((subcls1 G)^-1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
+lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
  class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
-  by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
+  by (simp add: class_rec_def wfrec [to_pred]
+    cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
 
 definition
-  "wf_class G = wf ((subcls1 G)^-1)"
+  "wf_class G = wfP ((subcls1 G)^--1)"
 
 lemma class_rec_func [code func]:
   "class_rec G C t f = (if wf_class G then
@@ -93,13 +78,14 @@
   case False then show ?thesis by auto
 next
   case True
-  from `wf_class G` have wf: "wf ((subcls1 G)^-1)"
+  from `wf_class G` have wf: "wfP ((subcls1 G)^--1)"
     unfolding wf_class_def .
   show ?thesis
   proof (cases "class G C")
     case None
     with wf show ?thesis
-      by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
+      by (simp add: class_rec_def wfrec [to_pred]
+        cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
   next
     case (Some x) show ?thesis
     proof (cases x)
@@ -121,7 +107,7 @@
 defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
                            ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
 
-lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==>
   method (G,C) = (if C = Object then empty else method (G,D)) ++  
   map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
 apply (unfold method_def)
@@ -135,7 +121,7 @@
 defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
                            map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
 
-lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==>
  fields (G,C) = 
   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
 apply (unfold fields_def)
@@ -156,56 +142,62 @@
 
 
 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
-inductive "widen G" intros 
+inductive2
+  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
+  for G :: "'c prog"
+where
   refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
-  subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
-  null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
+| subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
+| null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
 
 -- "casting conversion, cf. 5.5 / 5.1.5"
 -- "left out casts on primitve types"
-inductive "cast G" intros
+inductive2
+  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
+  for G :: "'c prog"
+where
   widen:  "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
-  subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
+| subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
 
 lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
 apply (rule iffI)
-apply (erule widen.elims)
+apply (erule widen.cases)
 apply auto
 done
 
 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
 apply auto
 done
 
 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
 apply auto
 done
 
 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
 apply auto
 done
 
 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
 apply (rule iffI)
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT")
 apply auto
 done
 
 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
 apply (rule iffI)
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D")
 apply (auto elim: widen.subcls)
 done
 
 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
-by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
+by (ind_cases2 "G \<turnstile> T \<preceq> NT",  auto)
 
 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
 apply (rule iffI)
-apply (erule cast.elims)
+apply (erule cast.cases)
 apply auto
 done
 
@@ -223,7 +215,7 @@
   next
     case (subcls C D T)
     then obtain E where "T = Class E" by (blast dest: widen_Class)
-    with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
+    with subcls show "G\<turnstile>Class C\<preceq>T" by auto
   next
     case (null R RT)
     then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -134,13 +134,13 @@
   apply (auto intro!: map_of_SomeI)
   done
 
-lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
-apply( frule r_into_trancl)
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not> (subcls1 G)^++ D C"
+apply( frule trancl.r_into_trancl [where r="subcls1 G"])
 apply( drule subcls1D)
 apply(clarify)
 apply( drule (1) class_wf_struct)
 apply( unfold ws_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+apply(force simp add: reflcl_trancl' [THEN sym] simp del: reflcl_trancl')
 done
 
 lemma wf_cdecl_supD: 
@@ -149,42 +149,42 @@
 apply (auto split add: option.split_asm)
 done
 
-lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
-apply(erule tranclE)
+lemma subcls_asym: "[|ws_prog G; (subcls1 G)^++ C D|] ==> \<not> (subcls1 G)^++ D C"
+apply(erule trancl.cases)
 apply(fast dest!: subcls1_wfD )
-apply(fast dest!: subcls1_wfD intro: trancl_trans)
+apply(fast dest!: subcls1_wfD intro: trancl_trans')
 done
 
-lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
-apply (erule trancl_trans_induct)
+lemma subcls_irrefl: "[|ws_prog G; (subcls1 G)^++ C D|] ==> C \<noteq> D"
+apply (erule trancl_trans_induct')
 apply  (auto dest: subcls1_wfD subcls_asym)
 done
 
-lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
-apply (unfold acyclic_def)
+lemma acyclic_subcls1: "ws_prog G ==> acyclicP (subcls1 G)"
+apply (simp add: acyclic_def [to_pred])
 apply (fast dest: subcls_irrefl)
 done
 
-lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
-apply (rule finite_acyclic_wf)
-apply ( subst finite_converse)
+lemma wf_subcls1: "ws_prog G ==> wfP ((subcls1 G)^--1)"
+apply (rule finite_acyclic_wf [to_pred])
+apply ( subst finite_converse [to_pred])
 apply ( rule finite_subcls1)
-apply (subst acyclic_converse)
+apply (subst acyclic_converse [to_pred])
 apply (erule acyclic_subcls1)
 done
 
 
 lemma subcls_induct: 
-"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|wf_prog wf_mb G; !!C. \<forall>D. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
   assume ?A thus ?thesis apply -
 apply (drule wf_prog_ws_prog)
 apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
 done
@@ -225,15 +225,15 @@
 qed
 
 lemma subcls_induct_struct: 
-"[|ws_prog G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|ws_prog G; !!C. \<forall>D. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
   assume ?A thus ?thesis apply -
 apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
 done
@@ -339,7 +339,7 @@
 apply( simp (no_asm))
 apply( erule UnE)
 apply(  force)
-apply( erule r_into_rtrancl [THEN rtrancl_trans])
+apply( erule r_into_rtrancl' [THEN rtrancl_trans'])
 apply auto
 done
 
@@ -381,9 +381,9 @@
 done
 
 lemma fields_mono_lemma [rule_format (no_asm)]: 
-  "[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==>  
+  "[|ws_prog G; (subcls1 G)^** C' C|] ==>  
   x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
-apply(erule converse_rtrancl_induct)
+apply(erule converse_rtrancl_induct')
 apply( safe dest!: subcls1D)
 apply(subst fields_rec)
 apply(  auto)
@@ -402,10 +402,10 @@
 "[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>  
   map_of (fields (G,D)) (fn, fd) = Some fT"
 apply (drule field_fields)
-apply (drule rtranclD)
+apply (drule rtranclD')
 apply safe
 apply (frule subcls_is_class)
-apply (drule trancl_into_rtrancl)
+apply (drule trancl_into_rtrancl')
 apply (fast dest: fields_mono)
 done
 
@@ -437,10 +437,10 @@
 apply (frule map_of_SomeD)
 apply (clarsimp simp add: wf_cdecl_def)
 apply( clarify)
-apply( rule rtrancl_trans)
+apply( rule rtrancl_trans')
 prefer 2
 apply(  assumption)
-apply( rule r_into_rtrancl)
+apply( rule r_into_rtrancl')
 apply( fast intro: subcls1I)
 done
 
@@ -473,10 +473,10 @@
 apply (clarsimp simp add: ws_cdecl_def)
 apply blast
 apply clarify
-apply( rule rtrancl_trans)
+apply( rule rtrancl_trans')
 prefer 2
 apply(  assumption)
-apply( rule r_into_rtrancl)
+apply( rule r_into_rtrancl')
 apply( fast intro: subcls1I)
 done
 
@@ -484,15 +484,15 @@
   "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>  
    \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> 
   (\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
-apply( drule rtranclD)
+apply( drule rtranclD')
 apply( erule disjE)
 apply(  fast)
 apply( erule conjE)
-apply( erule trancl_trans_induct)
+apply( erule trancl_trans_induct')
 prefer 2
 apply(  clarify)
 apply(  drule spec, drule spec, drule spec, erule (1) impE)
-apply(  fast elim: widen_trans rtrancl_trans)
+apply(  fast elim: widen_trans rtrancl_trans')
 apply( clarify)
 apply( drule subcls1D)
 apply( clarify)
@@ -512,7 +512,7 @@
 apply( unfold wf_cdecl_def)
 apply( drule map_of_SomeD)
 apply (auto simp add: wf_mrT_def)
-apply (rule rtrancl_trans)
+apply (rule rtrancl_trans')
 defer
 apply (rule method_wf_mhead [THEN conjunct1])
 apply (simp only: wf_prog_def)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -106,74 +106,57 @@
   java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
 -- "method body with parameter names, local variables, block, result expression."
 -- "local variables might include This, which is hidden anyway"
-
-consts
-  ty_expr :: "('c env \<times> expr      \<times> ty     ) set"
-  ty_exprs:: "('c env \<times> expr list \<times> ty list) set"
-  wt_stmt :: "('c env \<times> stmt               ) set"
-
-syntax (xsymbols)
-  ty_expr :: "'c env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
-  ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
-  wt_stmt :: "'c env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
-
-syntax
-  ty_expr :: "'c env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
-  ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
-  wt_stmt :: "'c env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
-
-
-translations
-  "E\<turnstile>e :: T" == "(E,e,T) \<in> ty_expr"
-  "E\<turnstile>e[::]T" == "(E,e,T) \<in> ty_exprs"
-  "E\<turnstile>c \<surd>"    == "(E,c)   \<in> wt_stmt"
   
-inductive "ty_expr" "ty_exprs" "wt_stmt" intros
+inductive2
+  ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50)
+  and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50)
+  and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50)
+where
   
   NewC: "[| is_class (prg E) C |] ==>
          E\<turnstile>NewC C::Class C"  -- "cf. 15.8"
 
   -- "cf. 15.15"
-  Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
+| Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
             prg E\<turnstile>C\<preceq>? Class D |] ==>
          E\<turnstile>Cast D e:: Class D"
 
   -- "cf. 15.7.1"
-  Lit:    "[| typeof (\<lambda>v. None) x = Some T |] ==>
+| Lit:    "[| typeof (\<lambda>v. None) x = Some T |] ==>
          E\<turnstile>Lit x::T"
 
   
   -- "cf. 15.13.1"
-  LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
+| LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
          E\<turnstile>LAcc v::T"
 
-  BinOp:"[| E\<turnstile>e1::T;
+| BinOp:"[| E\<turnstile>e1::T;
             E\<turnstile>e2::T;
             if bop = Eq then T' = PrimT Boolean
                         else T' = T \<and> T = PrimT Integer|] ==>
             E\<turnstile>BinOp bop e1 e2::T'"
 
   -- "cf. 15.25, 15.25.1"
-  LAss: "[| v ~= This;
+| LAss: "[| v ~= This;
             E\<turnstile>LAcc v::T;
             E\<turnstile>e::T';
             prg E\<turnstile>T'\<preceq>T |] ==>
          E\<turnstile>v::=e::T'"
 
   -- "cf. 15.10.1"
-  FAcc: "[| E\<turnstile>a::Class C; 
+| FAcc: "[| E\<turnstile>a::Class C; 
             field (prg E,C) fn = Some (fd,fT) |] ==>
             E\<turnstile>{fd}a..fn::fT"
 
   -- "cf. 15.25, 15.25.1"
-  FAss: "[| E\<turnstile>{fd}a..fn::T;
+| FAss: "[| E\<turnstile>{fd}a..fn::T;
             E\<turnstile>v        ::T';
             prg E\<turnstile>T'\<preceq>T |] ==>
          E\<turnstile>{fd}a..fn:=v::T'"
 
 
   -- "cf. 15.11.1, 15.11.2, 15.11.3"
-  Call: "[| E\<turnstile>a::Class C;
+| Call: "[| E\<turnstile>a::Class C;
             E\<turnstile>ps[::]pTs;
             max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
          E\<turnstile>{C}a..mn({pTs'}ps)::rT"
@@ -181,32 +164,32 @@
 -- "well-typed expression lists"
 
   -- "cf. 15.11.???"
-  Nil: "E\<turnstile>[][::][]"
+| Nil: "E\<turnstile>[][::][]"
 
   -- "cf. 15.11.???"
-  Cons:"[| E\<turnstile>e::T;
+| Cons:"[| E\<turnstile>e::T;
            E\<turnstile>es[::]Ts |] ==>
         E\<turnstile>e#es[::]T#Ts"
 
 -- "well-typed statements"
 
-  Skip:"E\<turnstile>Skip\<surd>"
+| Skip:"E\<turnstile>Skip\<surd>"
 
-  Expr:"[| E\<turnstile>e::T |] ==>
+| Expr:"[| E\<turnstile>e::T |] ==>
         E\<turnstile>Expr e\<surd>"
 
-  Comp:"[| E\<turnstile>s1\<surd>; 
+| Comp:"[| E\<turnstile>s1\<surd>; 
            E\<turnstile>s2\<surd> |] ==>
         E\<turnstile>s1;; s2\<surd>"
 
   -- "cf. 14.8"
-  Cond:"[| E\<turnstile>e::PrimT Boolean;
+| Cond:"[| E\<turnstile>e::PrimT Boolean;
            E\<turnstile>s1\<surd>;
            E\<turnstile>s2\<surd> |] ==>
          E\<turnstile>If(e) s1 Else s2\<surd>"
 
   -- "cf. 14.10"
-  Loop:"[| E\<turnstile>e::PrimT Boolean;
+| Loop:"[| E\<turnstile>e::PrimT Boolean;
            E\<turnstile>s\<surd> |] ==>
         E\<turnstile>While(e) s\<surd>"
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Nominal/Examples/Compile.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -45,62 +45,42 @@
 
 text {* valid contexts *}
 
-consts
-  ctxts :: "((name\<times>'a::pt_name) list) set" 
-  valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
-translations
-  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
-
-inductive ctxts
-intros
-v1[intro]: "valid []"
-v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
+inductive2 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
+where
+  v1[intro]: "valid []"
+| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
 
 text {* typing judgements for trms *}
 
-consts
-  typing :: "(((name\<times>ty) list)\<times>trm\<times>ty) set" 
-syntax
-  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
-translations
-  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
-
-inductive typing
-intros
-t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
-t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
-t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) \<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : \<tau>1\<rightarrow>\<tau>2"
-t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)"
-t4[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : Data(\<sigma>1); \<Gamma> \<turnstile> e2 : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e1 e2 : Data (DProd \<sigma>1 \<sigma>2)"
-t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)"
-t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)"
-t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)"
-t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)"
-t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2); 
+inductive2 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+where
+  t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
+| t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
+| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) \<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : \<tau>1\<rightarrow>\<tau>2"
+| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)"
+| t4[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : Data(\<sigma>1); \<Gamma> \<turnstile> e2 : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e1 e2 : Data (DProd \<sigma>1 \<sigma>2)"
+| t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)"
+| t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)"
+| t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)"
+| t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)"
+| t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2); 
              ((x1,Data(\<sigma>1))#\<Gamma>) \<turnstile> e1 : \<tau>; ((x2,Data(\<sigma>2))#\<Gamma>) \<turnstile> e2 : \<tau>\<rbrakk> 
              \<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) : \<tau>"
 
 text {* typing judgements for Itrms *}
 
-consts
-  Ityping :: "(((name\<times>tyI) list)\<times>trmI\<times>tyI) set" 
-syntax
-  "_typing_judge" :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80) 
-translations
-  "\<Gamma> I\<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> Ityping"  
-
-inductive Ityping
-intros
-t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
-t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
-t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) I\<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> ILam [x].t : \<tau>1\<rightarrow>\<tau>2"
-t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)"
-t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)"
-t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)"
-t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)"
-t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)"
-t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>"
-t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>"
+inductive2 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
+where
+  t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
+| t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
+| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) I\<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> ILam [x].t : \<tau>1\<rightarrow>\<tau>2"
+| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)"
+| t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)"
+| t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)"
+| t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)"
+| t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)"
+| t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>"
+| t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>"
 
 text {* capture-avoiding substitution *}
 
@@ -257,46 +237,32 @@
 
 text {* big-step evaluation for trms *}
 
-consts
-  big :: "(trm\<times>trm) set" 
-syntax
-  "_big_judge" :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
-translations
-  "e1 \<Down> e2" \<rightleftharpoons> "(e1,e2) \<in> big"
-
-inductive big
-intros
-b0[intro]: "Lam [x].e \<Down> Lam [x].e"
-b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
-b2[intro]: "Const n \<Down> Const n"
-b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'"
-b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1"
-b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2"
-b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'"
-b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'"
-b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
-b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
+inductive2 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
+where
+  b0[intro]: "Lam [x].e \<Down> Lam [x].e"
+| b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
+| b2[intro]: "Const n \<Down> Const n"
+| b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'"
+| b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1"
+| b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2"
+| b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'"
+| b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'"
+| b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
+| b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 
-consts
-  Ibig :: "(((nat\<Rightarrow>nat)\<times>trmI)\<times>((nat\<Rightarrow>nat)\<times>trmI)) set" 
-syntax
-  "_Ibig_judge" :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80) 
-translations
-  "(m,e1) I\<Down> (m',e2)" \<rightleftharpoons> "((m,e1),(m',e2)) \<in> Ibig"
-
-inductive Ibig
-intros
-m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
-m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk> 
+inductive2 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
+where
+  m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
+| m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk> 
             \<Longrightarrow> (m,IApp e1 e2) I\<Down> (m''',e4)"
-m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)"
-m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))"
-m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))"
-m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))"
-m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)"
-m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)"
-m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
-m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
+| m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)"
+| m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))"
+| m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))"
+| m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))"
+| m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)"
+| m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)"
+| m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
+| m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
 
 text {* Translation functions *}
 
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -45,21 +45,16 @@
 apply(simp_all add: fresh_atm)
 done
 
-consts
-  Beta :: "(lam\<times>lam) set"
-syntax 
-  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
-  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
-translations 
-  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
-  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
-inductive Beta
-  intros
+inductive2 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+where
   b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
-  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
-  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
-  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
+| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
+| b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
 
+abbreviation "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) where
+  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2 \<equiv> Beta\<^sup>*\<^sup>* t1 t2"
+ 
 lemma eqvt_beta: 
   fixes pi :: "name prm"
   and   t  :: "lam"
@@ -86,7 +81,7 @@
   next
     case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
   next
-    case (b3 a s1 s2)
+    case (b3 s1 s2 a)
     have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
     have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
     show ?case 
@@ -137,7 +132,7 @@
 
 
 lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
 apply(auto simp add: lam.distinct lam.inject)
 apply(auto simp add: alpha)
 apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
@@ -201,15 +196,10 @@
   "dom_ty []    = []"
   "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
 
-consts
-  ctxts :: "((name\<times>ty) list) set" 
-  valid :: "(name\<times>ty) list \<Rightarrow> bool"
-translations
-  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
-inductive ctxts
-intros
-v1[intro]: "valid []"
-v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
+inductive2 valid :: "(name\<times>ty) list \<Rightarrow> bool"
+where
+  v1[intro]: "valid []"
+| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
 lemma valid_eqvt:
   fixes   pi:: "name prm"
@@ -238,7 +228,7 @@
   and    a :: "name"
   and    \<tau> :: "ty"
   shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
-apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
+apply(ind_cases2 "valid ((a,\<tau>)#\<Gamma>)", simp)
 done
 
 lemma valid_unicity[rule_format]: 
@@ -251,18 +241,11 @@
 apply(auto dest!: valid_elim fresh_context)
 done
 
-consts
-  typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
-syntax
-  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
-translations
-  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
-
-inductive typing
-intros
-t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
-t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
-t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
+inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+where
+  t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
+| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
+| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
 lemma eqvt_typing: 
   fixes  \<Gamma> :: "(name\<times>ty) list"
@@ -273,14 +256,14 @@
   shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
 using a
 proof (induct)
-  case (t1 \<Gamma> \<tau> a)
+  case (t1 \<Gamma> a \<tau>)
   have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
   moreover
   have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
     using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
 next 
-  case (t3 \<Gamma> \<sigma> \<tau> a t)
+  case (t3 a \<Gamma> \<tau> t \<sigma>)
   moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
 qed (auto)
@@ -302,7 +285,7 @@
 proof -
   from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
   proof (induct)
-    case (t1 \<Gamma> \<tau> a)
+    case (t1 \<Gamma> a \<tau>)
     have j1: "valid \<Gamma>" by fact
     have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
     from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
@@ -310,10 +293,10 @@
     hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
     show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
   next
-    case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
+    case (t2 \<Gamma> t1 \<tau> \<sigma> t2)
     thus ?case using a2 by (simp, blast intro: eqvt_typing)
   next
-    case (t3 \<Gamma> \<sigma> \<tau> a t)
+    case (t3 a \<Gamma> \<tau> t \<sigma>)
     have k1: "a\<sharp>\<Gamma>" by fact
     have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
     have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
@@ -375,17 +358,17 @@
 done
 
 lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
-apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
+apply(ind_cases2 "\<Gamma> \<turnstile> Var a : \<tau>")
 apply(auto simp add: lam.inject lam.distinct)
 done
 
 lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
-apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
+apply(ind_cases2 "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
 apply(auto simp add: lam.inject lam.distinct)
 done
 
 lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
-apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
+apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
 apply(auto simp add: lam.distinct lam.inject alpha) 
 apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
 apply(simp)
@@ -534,7 +517,7 @@
 
 constdefs
   "SN" :: "lam \<Rightarrow> bool"
-  "SN t \<equiv> t\<in>termi Beta"
+  "SN t \<equiv> termi Beta t"
 
 lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
 apply(simp add: SN_def)
@@ -561,30 +544,24 @@
   "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
 
 (* a slight hack to get the first element of applications *)
-consts
-  FST :: "(lam\<times>lam) set"
-syntax 
-  "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
-translations 
-  "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
-inductive FST
-  intros
+inductive2 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
+where
 fst[intro!]:  "(App t s) \<guillemotright> t"
 
 lemma fst_elim[elim!]: 
   shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
-apply(ind_cases "App t s \<guillemotright> t'")
+apply(ind_cases2 "App t s \<guillemotright> t'")
 apply(simp add: lam.inject)
 done
 
 lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
 apply(simp add: SN_def)
-apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
+apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> termi Beta z")(*A*)
 apply(force)
 (*A*)
 apply(erule acc_induct)
 apply(clarify)
-apply(ind_cases "x \<guillemotright> z")
+apply(ind_cases2 "x \<guillemotright> z" for x z)
 apply(clarify)
 apply(rule accI)
 apply(auto intro: b1)
@@ -626,7 +603,7 @@
 apply(force simp only: NEUT_def)
 apply(simp (no_asm) add: CR3_RED_def)
 apply(clarify)
-apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "App t x \<longrightarrow>\<^isub>\<beta> t'" for x t t')
 apply(simp_all add: lam.inject)
 apply(simp only:  CR3_RED_def)
 apply(drule_tac x="s2" in spec)
@@ -701,21 +678,21 @@
 qed
     
 lemma double_acc_aux:
-  assumes a_acc: "a \<in> acc r"
-  and b_acc: "b \<in> acc r"
+  assumes a_acc: "acc r a"
+  and b_acc: "acc r b"
   and hyp: "\<And>x z.
-    (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
-    (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
-    (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
-    (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
+    (\<And>y. r y x \<Longrightarrow> acc r y) \<Longrightarrow>
+    (\<And>y. r y x \<Longrightarrow> P y z) \<Longrightarrow>
+    (\<And>u. r u z \<Longrightarrow> acc r u) \<Longrightarrow>
+    (\<And>u. r u z \<Longrightarrow> P x u) \<Longrightarrow> P x z"
   shows "P a b"
 proof -
   from a_acc
-  have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
+  have r: "\<And>b. acc r b \<Longrightarrow> P a b"
   proof (induct a rule: acc.induct)
     case (accI x)
     note accI' = accI
-    have "b \<in> acc r" .
+    have "acc r b" .
     thus ?case
     proof (induct b rule: acc.induct)
       case (accI y)
@@ -734,7 +711,7 @@
 qed
 
 lemma double_acc:
-  "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
+  "\<lbrakk>acc r a; acc r b; \<forall>x z. ((\<forall>y. r y x \<longrightarrow> P y z) \<and> (\<forall>u. r u z \<longrightarrow> P x u)) \<longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
 apply(rule_tac r="r" in double_acc_aux)
 apply(assumption)+
 apply(blast)
@@ -743,7 +720,7 @@
 lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
 apply(simp)
 apply(clarify)
-apply(subgoal_tac "t\<in>termi Beta")(*1*)
+apply(subgoal_tac "termi Beta t")(*1*)
 apply(erule rev_mp)
 apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
 apply(erule rev_mp)
@@ -764,7 +741,7 @@
 apply(force simp add: NEUT_def)
 apply(simp add: CR3_RED_def)
 apply(clarify)
-apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'" for xa z t')
 apply(auto simp add: lam.inject lam.distinct)
 apply(drule beta_abs)
 apply(auto)
@@ -813,7 +790,7 @@
 apply(force simp add: NEUT_def)
 apply(simp add: NORMAL_def)
 apply(clarify)
-apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "Var x \<longrightarrow>\<^isub>\<beta> t'" for t')
 apply(auto simp add: lam.inject lam.distinct)
 apply(force simp add: RED_props)
 apply(simp add: id_subs)
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Feb 07 17:44:07 2007 +0100
@@ -7,7 +7,7 @@
 
 signature INDUCTIVE_CODEGEN =
 sig
-  val add : string option -> attribute
+  val add : string option -> int option -> attribute
   val setup : theory -> theory
 end;
 
@@ -16,6 +16,17 @@
 
 open Codegen;
 
+(* read off parameters of inductive predicate from raw induction rule *)
+fun params_of induct =
+  let
+    val (_ $ t $ u :: _) =
+      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
+    val (_, ts) = strip_comb t;
+    val (_, us) = strip_comb u
+  in
+    List.take (ts, length ts - length us)
+  end;
+
 (**** theory data ****)
 
 fun merge_rules tabs =
@@ -26,7 +37,7 @@
 (struct
   val name = "HOL/inductive_codegen";
   type T =
-    {intros : (thm * string) list Symtab.table,
+    {intros : (thm * (string * int)) list Symtab.table,
      graph : unit Graph.T,
      eqns : (thm * string) list Symtab.table};
   val empty =
@@ -47,39 +58,46 @@
 
 fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
 
-fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
+fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
   let
     val {intros, graph, eqns} = CodegenData.get thy;
     fun thyname_of s = (case optmod of
       NONE => thyname_of_const s thy | SOME s => s);
-  in (case concl_of thm of
-      _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
-        Const (s, _) =>
-          let val cs = foldr add_term_consts [] (prems_of thm)
-          in CodegenData.put
-            {intros = intros |>
-             Symtab.update (s, Symtab.lookup_list intros s @ [(thm, thyname_of s)]),
-             graph = foldr (uncurry (Graph.add_edge o pair s))
-               (Library.foldl add_node (graph, s :: cs)) cs,
-             eqns = eqns} thy
-          end
-      | _ => (warn thm; thy))
-    | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
+  in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
+      SOME (Const ("op =", _), [t, _]) => (case head_of t of
         Const (s, _) =>
           CodegenData.put {intros = intros, graph = graph,
              eqns = eqns |> Symtab.update
                (s, Symtab.lookup_list eqns s @ [(thm, thyname_of s)])} thy
       | _ => (warn thm; thy))
+    | SOME (Const (s, _), _) =>
+        let
+          val cs = foldr add_term_consts [] (prems_of thm);
+          val rules = Symtab.lookup_list intros s;
+          val nparms = (case optnparms of
+            SOME k => k
+          | NONE => (case rules of
+             [] => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
+                 SOME (_, {raw_induct, ...}) => length (params_of raw_induct)
+               | NONE => 0)
+            | xs => snd (snd (snd (split_last xs)))))
+        in CodegenData.put
+          {intros = intros |>
+           Symtab.update (s, rules @ [(thm, (thyname_of s, nparms))]),
+           graph = foldr (uncurry (Graph.add_edge o pair s))
+             (Library.foldl add_node (graph, s :: cs)) cs,
+           eqns = eqns} thy
+        end
     | _ => (warn thm; thy))
   end) I);
 
 fun get_clauses thy s =
   let val {intros, graph, ...} = CodegenData.get thy
   in case Symtab.lookup intros s of
-      NONE => (case OldInductivePackage.get_inductive thy s of
+      NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
         NONE => NONE
-      | SOME ({names, ...}, {intrs, ...}) =>
-          SOME (names, thyname_of_const s thy,
+      | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
+          SOME (names, thyname_of_const s thy, length (params_of raw_induct),
             preprocess thy intrs))
     | SOME _ =>
         let
@@ -87,64 +105,11 @@
             (fn xs => s mem xs) (Graph.strong_conn graph);
           val intrs = List.concat (map
             (fn s => the (Symtab.lookup intros s)) names);
-          val (_, (_, thyname)) = split_last intrs
-        in SOME (names, thyname, preprocess thy (map fst intrs)) end
+          val (_, (_, (thyname, nparms))) = split_last intrs
+        in SOME (names, thyname, nparms, preprocess thy (map fst intrs)) end
   end;
 
 
-(**** improper tuples ****)
-
-fun prod_factors p (Const ("Pair", _) $ t $ u) =
-      p :: prod_factors (1::p) t @ prod_factors (2::p) u
-  | prod_factors p _ = [];
-
-fun split_prod p ps t = if p mem ps then (case t of
-       Const ("Pair", _) $ t $ u =>
-         split_prod (1::p) ps t @ split_prod (2::p) ps u
-     | _ => error "Inconsistent use of products") else [t];
-
-fun full_split_prod (Const ("Pair", _) $ t $ u) =
-      full_split_prod t @ full_split_prod u
-  | full_split_prod t = [t];
-
-datatype factors = FVar of int list list | FFix of int list list;
-
-exception Factors;
-
-fun mg_factor (FVar f) (FVar f') = FVar (f inter f')
-  | mg_factor (FVar f) (FFix f') =
-      if f' subset f then FFix f' else raise Factors
-  | mg_factor (FFix f) (FVar f') =
-      if f subset f' then FFix f else raise Factors
-  | mg_factor (FFix f) (FFix f') =
-      if f subset f' andalso f' subset f then FFix f else raise Factors;
-
-fun dest_factors (FVar f) = f
-  | dest_factors (FFix f) = f;
-
-fun infer_factors sg extra_fs (fs, (optf, t)) =
-  let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
-  in (case (optf, strip_comb t) of
-      (SOME f, (Const (name, _), args)) =>
-        (case AList.lookup (op =) extra_fs name of
-           NONE => AList.update (op =) (name, getOpt
-             (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
-         | SOME (fs', f') => (mg_factor f (FFix f');
-             Library.foldl (infer_factors sg extra_fs)
-               (fs, map (Option.map FFix) fs' ~~ args)))
-    | (SOME f, (Var ((name, _), _), [])) =>
-        AList.update (op =) (name, getOpt
-          (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
-    | (NONE, _) => fs
-    | _ => err "Illegal term")
-      handle Factors => err "Product factor mismatch in"
-  end;
-
-fun string_of_factors p ps = if p mem ps then
-    "(" ^ string_of_factors (1::p) ps ^ ", " ^ string_of_factors (2::p) ps ^ ")"
-  else "_";
-
-
 (**** check if a term contains only constructor functions ****)
 
 fun is_constrt thy =
@@ -202,31 +167,47 @@
 
 fun cprods xss = foldr (map op :: o cprod) [[]] xss;
 
-datatype mode = Mode of (int list option list * int list) * mode option list;
+datatype mode = Mode of (int list option list * int list) * int list * mode option list;
 
 fun modes_of modes t =
   let
-    fun mk_modes name args = List.concat
-      (map (fn (m as (iss, is)) => map (Mode o pair m) (cprods (map
-        (fn (NONE, _) => [NONE]
-          | (SOME js, arg) => map SOME
-              (List.filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
-                (iss ~~ args)))) ((the o AList.lookup (op =) modes) name))
+    val ks = 1 upto length (binder_types (fastype_of t));
+    val default = [Mode (([], ks), ks, [])];
+    fun mk_modes name args = Option.map (List.concat o
+      map (fn (m as (iss, is)) =>
+        let
+          val (args1, args2) =
+            if length args < length iss then
+              error ("Too few arguments for inductive predicate " ^ name)
+            else chop (length iss) args;
+          val k = length args2;
+          val prfx = 1 upto k
+        in
+          if not (is_prefix op = prfx is) then [] else
+          let val is' = map (fn i => i - k) (List.drop (is, k))
+          in map (fn x => Mode (m, is', x)) (cprods (map
+            (fn (NONE, _) => [NONE]
+              | (SOME js, arg) => map SOME (List.filter
+                  (fn Mode (_, js', _) => js=js') (modes_of modes arg)))
+                    (iss ~~ args1)))
+          end
+        end)) (AList.lookup op = modes name)
 
   in (case strip_comb t of
       (Const ("op =", Type (_, [T, _])), _) =>
-        [Mode (([], [1]), []), Mode (([], [2]), [])] @
-        (if is_eqT T then [Mode (([], [1, 2]), [])] else [])
-    | (Const (name, _), args) => mk_modes name args
-    | (Var ((name, _), _), args) => mk_modes name args
-    | (Free (name, _), args) => mk_modes name args)
+        [Mode (([], [1]), [1], []), Mode (([], [2]), [2], [])] @
+        (if is_eqT T then [Mode (([], [1, 2]), [1, 2], [])] else [])
+    | (Const (name, _), args) => the_default default (mk_modes name args)
+    | (Var ((name, _), _), args) => the (mk_modes name args)
+    | (Free (name, _), args) => the (mk_modes name args)
+    | _ => default)
   end;
 
 datatype indprem = Prem of term list * term | Sidecond of term;
 
 fun select_mode_prem thy modes vs ps =
   find_first (is_some o snd) (ps ~~ map
-    (fn Prem (us, t) => find_first (fn Mode ((_, is), _) =>
+    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
           let
             val (in_ts, out_ts) = get_args is 1 us;
             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
@@ -239,8 +220,8 @@
             term_vs t subset vs andalso
             forall is_eqT dupTs
           end)
-            (modes_of modes t handle Option => [Mode (([], []), [])])
-      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), []))
+            (modes_of modes t handle Option => [Mode (([], []), [], [])])
+      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
           else NONE) ps);
 
 fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
@@ -278,12 +259,12 @@
   let val y = f x
   in if x = y then x else fixp f y end;
 
-fun infer_modes thy extra_modes factors arg_vs preds = fixp (fn modes =>
+fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
   map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
-    (map (fn (s, (fs, f)) => (s, cprod (cprods (map
+    (map (fn (s, (ks, k)) => (s, cprod (cprods (map
       (fn NONE => [NONE]
-        | SOME f' => map SOME (subsets 1 (length f' + 1))) fs),
-      subsets 1 (length f + 1)))) factors);
+        | SOME k' => map SOME (subsets 1 k')) ks),
+      subsets 1 k))) arities);
 
 (**** code generation ****)
 
@@ -296,51 +277,6 @@
   List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
   [Pretty.str ")"]);
 
-(* convert nested pairs to n-tuple *)
-
-fun conv_ntuple [_] t ps = ps
-  | conv_ntuple [_, _] t ps = ps
-  | conv_ntuple us t ps =
-      let
-        val xs = map (fn i => Pretty.str ("x" ^ string_of_int i))
-          (1 upto length us);
-        fun ntuple (ys as (x, T) :: xs) U =
-          if T = U then (x, xs)
-          else
-            let
-              val Type ("*", [U1, U2]) = U;
-              val (p1, ys1) = ntuple ys U1;
-              val (p2, ys2) = ntuple ys1 U2
-            in (mk_tuple [p1, p2], ys2) end
-      in
-        [Pretty.str "Seq.map (fn", Pretty.brk 1,
-         fst (ntuple (xs ~~ map fastype_of us) (HOLogic.dest_setT (fastype_of t))),
-         Pretty.str " =>", Pretty.brk 1, mk_tuple xs, Pretty.str ")",
-         Pretty.brk 1, parens (Pretty.block ps)]
-      end;
-
-(* convert n-tuple to nested pairs *)
-
-fun conv_ntuple' fs T ps =
-  let
-    fun mk_x i = Pretty.str ("x" ^ string_of_int i);
-    fun conv i js (Type ("*", [T, U])) =
-          if js mem fs then
-            let
-              val (p, i') = conv i (1::js) T;
-              val (q, i'') = conv i' (2::js) U
-            in (mk_tuple [p, q], i'') end
-          else (mk_x i, i+1)
-      | conv i js _ = (mk_x i, i+1)
-    val (p, i) = conv 1 [] T
-  in
-    if i > 3 then
-      [Pretty.str "Seq.map (fn", Pretty.brk 1,
-       mk_tuple (map mk_x (1 upto i-1)), Pretty.str " =>", Pretty.brk 1,
-       p, Pretty.str ")", Pretty.brk 1, parens (Pretty.block ps)]
-    else ps
-  end;
-
 fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
       NONE => ((names, (s, [s])::vs), s)
     | SOME xs => let val s' = Name.variant names s in
@@ -383,23 +319,37 @@
       map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])))
   end;
 
-fun compile_expr thy defs dep module brack (gr, (NONE, t)) =
+fun mk_funcomp brack s k p = (if brack then parens else I)
+  (Pretty.block [Pretty.block ((if k = 0 then [] else [Pretty.str "("]) @
+    separate (Pretty.brk 1) (Pretty.str s :: replicate k (Pretty.str "|> ???")) @
+    (if k = 0 then [] else [Pretty.str ")"])), Pretty.brk 1, p]);
+
+fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) =
       apsnd single (invoke_codegen thy defs dep module brack (gr, t))
-  | compile_expr _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
+  | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
       (gr, [Pretty.str name])
-  | compile_expr thy defs dep module brack (gr, (SOME (Mode (mode, ms)), t)) =
-      let
-        val (Const (name, _), args) = strip_comb t;
-        val (gr', (ps, mode_id)) = foldl_map
-            (compile_expr thy defs dep module true) (gr, ms ~~ args) |>>>
-          modename module name mode;
-      in (gr', (if brack andalso not (null ps) then
-        single o parens o Pretty.block else I)
-          (List.concat (separate [Pretty.brk 1]
-            ([Pretty.str mode_id] :: ps))))
-      end;
+  | compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) =
+      (case strip_comb t of
+         (Const (name, _), args) =>
+           if name = "op =" orelse AList.defined op = modes name then
+             let
+               val (args1, args2) = chop (length ms) args;
+               val (gr', (ps, mode_id)) = foldl_map
+                   (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
+                 modename module name mode;
+               val (gr'', ps') = foldl_map
+                 (invoke_codegen thy defs dep module true) (gr', args2)
+             in (gr', (if brack andalso not (null ps andalso null ps') then
+               single o parens o Pretty.block else I)
+                 (List.concat (separate [Pretty.brk 1]
+                   ([Pretty.str mode_id] :: ps @ map single ps'))))
+             end
+           else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
+             (invoke_codegen thy defs dep module true (gr, t))
+       | _ => apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
+           (invoke_codegen thy defs dep module true (gr, t)));
 
-fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) =
+fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) inp =
   let
     val modes' = modes @ List.mapPartial
       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
@@ -442,7 +392,7 @@
       | compile_prems out_ts vs names gr ps =
           let
             val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
-            val SOME (p, mode as SOME (Mode ((_, js), _))) =
+            val SOME (p, mode as SOME (Mode (_, js, _))) =
               select_mode_prem thy modes' vs' ps;
             val ps' = filter_out (equal p) ps;
             val ((names', eqs), out_ts') =
@@ -458,14 +408,14 @@
                  let
                    val (in_ts, out_ts''') = get_args js 1 us;
                    val (gr2, in_ps) = foldl_map
-                     (invoke_codegen thy defs dep module false) (gr1, in_ts);
+                     (invoke_codegen thy defs dep module true) (gr1, in_ts);
                    val (gr3, ps) = if is_ind t then
-                       apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
-                         (compile_expr thy defs dep module false
+                       apsnd (fn ps => ps @ Pretty.brk 1 ::
+                           separate (Pretty.brk 1) in_ps)
+                         (compile_expr thy defs dep module false modes
                            (gr2, (mode, t)))
                      else
-                       apsnd (fn p => conv_ntuple us t
-                         [Pretty.str "Seq.of_list", Pretty.brk 1, p])
+                       apsnd (fn p => [Pretty.str "Seq.of_list", Pretty.brk 1, p])
                            (invoke_codegen thy defs dep module true (gr2, t));
                    val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
                  in
@@ -488,20 +438,24 @@
 
     val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
   in
-    (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
+    (gr', Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, inp,
+       Pretty.str " :->", Pretty.brk 1, prem_p])
   end;
 
 fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
-  let val (gr', (cl_ps, mode_id)) =
-    foldl_map (fn (gr, cl) => compile_clause thy defs
-      gr dep module all_vs arg_vs modes mode cl) (gr, cls) |>>>
-    modename module s mode
+  let
+    val xs = map Pretty.str (Name.variant_list arg_vs
+      (map (fn i => "x" ^ string_of_int i) (snd mode)));
+    val (gr', (cl_ps, mode_id)) =
+      foldl_map (fn (gr, cl) => compile_clause thy defs
+        gr dep module all_vs arg_vs modes mode cl (mk_tuple xs)) (gr, cls) |>>>
+      modename module s mode
   in
     ((gr', "and "), Pretty.block
       ([Pretty.block (separate (Pretty.brk 1)
          (Pretty.str (prfx ^ mode_id) ::
-           map Pretty.str arg_vs) @
-         [Pretty.str " inp ="]),
+           map Pretty.str arg_vs @ xs) @
+         [Pretty.str " ="]),
         Pretty.brk 1] @
        List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
   end;
@@ -519,17 +473,17 @@
 
 exception Modes of
   (string * (int list option list * int list) list) list *
-  (string * (int list list option list * int list list)) list;
+  (string * (int option list * int)) list;
 
 fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
   (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
     (Graph.all_preds (fst gr) [dep]))));
 
-fun print_factors factors = message ("Factors:\n" ^
-  space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
+fun print_arities arities = message ("Arities:\n" ^
+  space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
     space_implode " -> " (map
-      (fn NONE => "X" | SOME f' => string_of_factors [] f')
-        (fs @ [SOME f]))) factors));
+      (fn NONE => "X" | SOME k' => string_of_int k')
+        (ks @ [SOME k]))) arities));
 
 fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
 
@@ -543,133 +497,97 @@
     if name mem names then gr
     else (case get_clauses thy name of
         NONE => gr
-      | SOME (names, thyname, intrs) =>
+      | SOME (names, thyname, nparms, intrs) =>
           mk_ind_def thy defs gr dep names (if_library thyname module)
-            [] [] (prep_intrs intrs)))
+            [] (prep_intrs intrs) nparms))
             (gr, foldr add_term_consts [] ts)
 
-and mk_ind_def thy defs gr dep names module modecs factorcs intrs =
+and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
     let
-      val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
-      val (_, args) = strip_comb u;
+      val _ $ u = Logic.strip_imp_concl (hd intrs);
+      val args = List.take (snd (strip_comb u), nparms);
       val arg_vs = List.concat (map term_vs args);
 
-      fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
-            (case AList.lookup (op =) factors (case head_of u of
-                 Const (name, _) => name | Var ((name, _), _) => name) of
-               NONE => Prem (full_split_prod t, u)
-             | SOME f => Prem (split_prod [] f t, u))
-        | dest_prem factors (_ $ ((eq as Const ("op =", _)) $ t $ u)) =
-            Prem ([t, u], eq)
-        | dest_prem factors (_ $ t) = Sidecond t;
+      fun get_nparms s = if s mem names then SOME nparms else
+        Option.map #3 (get_clauses thy s);
 
-      fun add_clause factors (clauses, intr) =
+      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], u)
+        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq)
+        | dest_prem (_ $ t) =
+            (case strip_comb t of
+               (v as Var _, ts) => Prem (ts, v)
+             | (c as Const (s, _), ts) => (case get_nparms s of
+                 NONE => Sidecond t
+               | SOME k =>
+                   let val (ts1, ts2) = chop k ts
+                   in Prem (ts2, list_comb (c, ts1)) end)
+             | _ => Sidecond t);
+
+      fun add_clause intr (clauses, arities) =
         let
-          val _ $ (_ $ t $ u) = Logic.strip_imp_concl intr;
-          val Const (name, _) = head_of u;
-          val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
+          val _ $ t = Logic.strip_imp_concl intr;
+          val (Const (name, T), ts) = strip_comb t;
+          val (ts1, ts2) = chop nparms ts;
+          val prems = map dest_prem (Logic.strip_imp_prems intr);
+          val (Ts, Us) = chop nparms (binder_types T)
         in
-          AList.update (op =) (name, ((these o AList.lookup (op =) clauses) name) @
-             [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
+          (AList.update op = (name, these (AList.lookup op = clauses name) @
+             [(ts2, prems)]) clauses,
+           AList.update op = (name, (map (fn U => (case strip_type U of
+                 (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
+               | _ => NONE)) Ts,
+             length Us)) arities)
         end;
 
-      fun check_set (Const (s, _)) = s mem names orelse is_some (get_clauses thy s)
-        | check_set (Var ((s, _), _)) = s mem arg_vs
-        | check_set _ = false;
-
-      fun add_prod_factors extra_fs (fs, _ $ (Const ("op :", _) $ t $ u)) =
-            if check_set (head_of u)
-            then infer_factors (sign_of thy) extra_fs
-              (fs, (SOME (FVar (prod_factors [] t)), u))
-            else fs
-        | add_prod_factors _ (fs, _) = fs;
-
       val gr' = mk_extra_defs thy defs
         (add_edge (hd names, dep)
           (new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
-      val (extra_modes, extra_factors) = lookup_modes gr' (hd names);
-      val fs = constrain factorcs (map (apsnd dest_factors)
-        (Library.foldl (add_prod_factors extra_factors) ([], List.concat (map (fn t =>
-          Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
-      val factors = List.mapPartial (fn (name, f) =>
-        if name mem arg_vs then NONE
-        else SOME (name, (map (AList.lookup (op =) fs) arg_vs, f))) fs;
-      val clauses =
-        Library.foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
+      val (extra_modes, extra_arities) = lookup_modes gr' (hd names);
+      val (clauses, arities) = fold add_clause intrs ([], []);
       val modes = constrain modecs
-        (infer_modes thy extra_modes factors arg_vs clauses);
-      val _ = print_factors factors;
+        (infer_modes thy extra_modes arities arg_vs clauses);
+      val _ = print_arities arities;
       val _ = print_modes modes;
       val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs)
         arg_vs (modes @ extra_modes) clauses;
     in
       (map_node (hd names)
-        (K (SOME (Modes (modes, factors)), module, s)) gr'')
+        (K (SOME (Modes (modes, arities)), module, s)) gr'')
     end;
 
-fun find_mode gr dep s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
+fun find_mode gr dep s u modes is = (case find_first (fn Mode (_, js, _) => is=js)
   (modes_of modes u handle Option => []) of
      NONE => codegen_error gr dep
        ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
    | mode => mode);
 
-fun mk_ind_call thy defs gr dep module t u is_query = (case head_of u of
-  Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
-       (NONE, _) => NONE
-     | (SOME (names, thyname, intrs), NONE) =>
-         let
-          fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
-                ((ts, mode), i+1)
-            | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
+fun mk_ind_call thy defs gr dep module is_query s T ts names thyname k intrs =
+  let
+    val (ts1, ts2) = chop k ts;
+    val u = list_comb (Const (s, T), ts1);
+
+    fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
+          ((ts, mode), i+1)
+      | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
 
-           val module' = if_library thyname module;
-           val gr1 = mk_extra_defs thy defs
-             (mk_ind_def thy defs gr dep names module'
-             [] [] (prep_intrs intrs)) dep names module' [u];
-           val (modes, factors) = lookup_modes gr1 dep;
-           val ts = split_prod [] ((snd o the o AList.lookup (op =) factors) s) t;
-           val (ts', is) = if is_query then
-               fst (Library.foldl mk_mode ((([], []), 1), ts))
-             else (ts, 1 upto length ts);
-           val mode = find_mode gr1 dep s u modes is;
-           val (gr2, in_ps) = foldl_map
-             (invoke_codegen thy defs dep module false) (gr1, ts');
-           val (gr3, ps) =
-             compile_expr thy defs dep module false (gr2, (mode, u))
-         in
-           SOME (gr3, Pretty.block
-             (ps @ [Pretty.brk 1, mk_tuple in_ps]))
-         end
-     | _ => NONE)
-  | _ => NONE);
-
-fun list_of_indset thy defs gr dep module brack u = (case head_of u of
-  Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
-       (NONE, _) => NONE
-     | (SOME (names, thyname, intrs), NONE) =>
-         let
-           val module' = if_library thyname module;
-           val gr1 = mk_extra_defs thy defs
-             (mk_ind_def thy defs gr dep names module'
-             [] [] (prep_intrs intrs)) dep names module' [u];
-           val (modes, factors) = lookup_modes gr1 dep;
-           val mode = find_mode gr1 dep s u modes [];
-           val (gr2, ps) =
-             compile_expr thy defs dep module false (gr1, (mode, u));
-           val (gr3, _) =
-             invoke_tycodegen thy defs dep module false (gr2, body_type T)
-         in
-           SOME (gr3, (if brack then parens else I)
-             (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
-               Pretty.str "("] @
-                conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))
-                 (HOLogic.dest_setT (fastype_of u))
-                 (ps @ [Pretty.brk 1, Pretty.str "()"]) @
-               [Pretty.str ")"])))
-         end
-     | _ => NONE)
-  | _ => NONE);
+    val module' = if_library thyname module;
+    val gr1 = mk_extra_defs thy defs
+      (mk_ind_def thy defs gr dep names module'
+      [] (prep_intrs intrs) k) dep names module' [u];
+    val (modes, _) = lookup_modes gr1 dep;
+    val (ts', is) = if is_query then
+        fst (Library.foldl mk_mode ((([], []), 1), ts2))
+      else (ts2, 1 upto length (binder_types T) - k);
+    val mode = find_mode gr1 dep s u modes is;
+    val (gr2, in_ps) = foldl_map
+      (invoke_codegen thy defs dep module true) (gr1, ts');
+    val (gr3, ps) =
+      compile_expr thy defs dep module false modes (gr2, (mode, u))
+  in
+    (gr3, Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
+       separate (Pretty.brk 1) in_ps))
+  end;
 
 fun clause_of_eqn eqn =
   let
@@ -677,10 +595,8 @@
     val (Const (s, T), ts) = strip_comb t;
     val (Ts, U) = strip_type T
   in
-    rename_term
-      (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
-        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ "_aux",
-          HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
+    rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop
+      (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u]))))
   end;
 
 fun mk_fun thy defs name eqns dep module module' gr =
@@ -699,44 +615,57 @@
       val s = Pretty.string_of (Pretty.block
         [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =",
          Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
-         parens (Pretty.block [Pretty.str mode_id,
-           Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
+         parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id ::
+           vars)))]) ^ ";\n\n";
       val gr'' = mk_ind_def thy defs (add_edge (name, dep)
         (new_node (name, (NONE, module', s)) gr')) name [pname] module'
-        [(pname, [([], mode)])]
-        [(pname, map (fn i => replicate i 2) (0 upto arity-1))]
-        clauses;
+        [(pname, [([], mode)])] clauses 0;
       val (modes, _) = lookup_modes gr'' dep;
-      val _ = find_mode gr'' dep pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
-        (Logic.strip_imp_concl (hd clauses))))) modes mode
+      val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop
+        (Logic.strip_imp_concl (hd clauses)))) modes mode
     in (gr'', mk_qual_id module fun_id) end
   | SOME _ =>
       (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
 
-fun inductive_codegen thy defs gr dep module brack (Const ("op :", _) $ t $ u) =
-      ((case mk_ind_call thy defs gr dep module (Term.no_dummy_patterns t) u false of
-         NONE => NONE
-       | SOME (gr', call_p) => SOME (gr', (if brack then parens else I)
-           (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
-        handle TERM _ => mk_ind_call thy defs gr dep module t u true)
-  | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
-      (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
-        NONE => list_of_indset thy defs gr dep module brack t
-      | SOME eqns =>
-          let
-            val (_, (_, thyname)) = split_last eqns;
-            val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
-              dep module (if_library thyname module) gr;
-            val (gr'', ps) = foldl_map
-              (invoke_codegen thy defs dep module true) (gr', ts);
-          in SOME (gr'', mk_app brack (Pretty.str id) ps)
-          end)
-    | _ => NONE);
+fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
+    (Const ("Collect", Type (_, [_, Type (_, [U])])), [u]) => (case strip_comb u of
+        (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy s T) of
+          (SOME (names, thyname, k, intrs), NONE) =>
+            let val (gr', call_p) = mk_ind_call thy defs gr dep module true
+              s T (ts @ [Term.dummy_pattern U]) names thyname k intrs
+            in SOME (gr', (if brack then parens else I) (Pretty.block
+              [Pretty.str "Seq.list_of", Pretty.brk 1, Pretty.str "(",
+               call_p, Pretty.str ")"]))
+            end
+        | _ => NONE)
+      | _ => NONE)
+  | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
+      NONE => (case (get_clauses thy s, get_assoc_code thy s T) of
+        (SOME (names, thyname, k, intrs), NONE) =>
+          if length ts < k then NONE else SOME
+            (let val (gr', call_p) = mk_ind_call thy defs gr dep module false
+               s T (map Term.no_dummy_patterns ts) names thyname k intrs
+             in (gr', mk_funcomp brack "?!"
+               (length (binder_types T) - length ts) (parens call_p))
+             end handle TERM _ => mk_ind_call thy defs gr dep module true
+               s T ts names thyname k intrs)
+      | _ => NONE)
+    | SOME eqns =>
+        let
+          val (_, (_, thyname)) = split_last eqns;
+          val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
+            dep module (if_library thyname module) gr;
+          val (gr'', ps) = foldl_map
+            (invoke_codegen thy defs dep module true) (gr', ts);
+        in SOME (gr'', mk_app brack (Pretty.str id) ps)
+        end)
+  | _ => NONE);
 
 val setup =
   add_codegen "inductive" inductive_codegen #>
   CodegenData.init #>
-  add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
+  add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+    Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
 
 end;
 
@@ -752,6 +681,8 @@
 
 fun ?? b = if b then Seq.single () else Seq.empty;
 
+fun ??? f g = f o g;
+
 fun ?! s = is_some (Seq.pull s);
 
 fun equal__1 x = Seq.single x;
diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Feb 07 17:44:07 2007 +0100
@@ -15,51 +15,103 @@
 structure InductiveRealizer : INDUCTIVE_REALIZER =
 struct
 
+(* FIXME: LocalTheory.note should return theorems with proper names! *)
+fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP
+    (Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of
+    (PThm (name, _, _, _), _) => name
+  | _ => error "name_of_thm: bad proof");
+
+(* infer order of variables in intro rules from order of quantifiers in elim rule *)
+fun infer_intro_vars elim arity intros =
+  let
+    val thy = theory_of_thm elim;
+    val _ :: cases = prems_of elim;
+    val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
+    fun mtch (t, u) =
+      let
+        val params = Logic.strip_params t;
+        val vars = map (Var o apfst (rpair 0))
+          (Name.variant_list used (map fst params) ~~ map snd params);
+        val ts = map (curry subst_bounds (rev vars))
+          (List.drop (Logic.strip_assums_hyp t, arity));
+        val us = Logic.strip_imp_prems u;
+        val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
+          (Vartab.empty, Vartab.empty);
+      in
+        map (Envir.subst_vars tab) vars
+      end
+  in
+    map (mtch o apsnd prop_of) (cases ~~ intros)
+  end;
+
+(* read off arities of inductive predicates from raw induction rule *)
+fun arities_of induct =
+  map (fn (_ $ t $ u) =>
+      (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
+    (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+
+(* read off parameters of inductive predicate from raw induction rule *)
+fun params_of induct =
+  let
+    val (_ $ t $ u :: _) =
+      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
+    val (_, ts) = strip_comb t;
+    val (_, us) = strip_comb u
+  in
+    List.take (ts, length ts - length us)
+  end;
+
 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
 
 fun prf_of thm =
   let val {sign, prop, der = (_, prf), ...} = rep_thm thm
-  in Reconstruct.reconstruct_proof sign prop prf end;
+  in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *)
 
 fun forall_intr_prf (t, prf) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
 
+fun forall_intr_term (t, u) =
+  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
+  in all T $ Abs (a, T, abstract_over (t, u)) end;
+
 fun subsets [] = [[]]
   | subsets (x::xs) =
       let val ys = subsets xs
       in ys @ map (cons x) ys end;
 
-val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
+val pred_of = fst o dest_Const o head_of;
 
-fun strip_all t =
-  let
-    fun strip used (Const ("all", _) $ Abs (s, T, t)) =
-          let val s' = Name.variant used s
-          in strip (s'::used) (subst_bound (Free (s', T), t)) end
-      | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
-      | strip _ t = t;
-  in strip (add_term_free_names (t, [])) t end;
+fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
+      let val (s', names') = (case names of
+          [] => (Name.variant used s, [])
+        | name :: names' => (name, names'))
+      in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
+  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
+      t $ strip_all' used names Q
+  | strip_all' _ _ t = t;
+
+fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t;
+
+fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
+      (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
+  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
 
 fun relevant_vars prop = foldr (fn
       (Var ((a, i), T), vs) => (case strip_type T of
-        (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
+        (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
       | _ => vs)
     | (_, vs) => vs) [] (term_vars prop);
 
-fun params_of intr = map (fst o fst o dest_Var) (term_vars
-  (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
-    (Logic.strip_imp_concl intr)))));
-
-fun dt_of_intrs thy vs intrs =
+fun dt_of_intrs thy vs nparms intrs =
   let
     val iTs = term_tvars (prop_of (hd intrs));
     val Tvs = map TVar iTs;
-    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
-    val (Const (s, _), ts) = strip_comb S;
-    val params = map dest_Var ts;
+    val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
+      (Logic.strip_imp_concl (prop_of (hd intrs))));
+    val params = map dest_Var (Library.take (nparms, ts));
     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
-    fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
+    fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
       map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
           (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -70,43 +122,40 @@
 
 fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
 
-(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
+(** turn "P" into "%r x. realizes r (P x)" **)
 
 fun gen_rvar vs (t as Var ((a, 0), T)) =
-      let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
-      in case try HOLogic.dest_setT T of
-          NONE => if body_type T <> HOLogic.boolT then t else
-            let
-              val Ts = binder_types T;
-              val i = length Ts;
-              val xs = map (pair "x") Ts;
-              val u = list_comb (t, map Bound (i - 1 downto 0))
-            in 
-              if a mem vs then
-                list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
-              else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
-            end
-        | SOME T' => if a mem vs then
-              Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
-                (HOLogic.mk_mem (Bound 0, t))))
-            else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
-              (HOLogic.mk_mem (Bound 0, t)))
-      end
+      if body_type T <> HOLogic.boolT then t else
+        let
+          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
+          val Ts = binder_types T;
+          val i = length Ts;
+          val xs = map (pair "x") Ts;
+          val u = list_comb (t, map Bound (i - 1 downto 0))
+        in 
+          if a mem vs then
+            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
+          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
+        end
   | gen_rvar _ t = t;
 
-fun mk_realizes_eqn n vs intrs =
+fun mk_realizes_eqn n vs nparms intrs =
   let
-    val iTs = term_tvars (prop_of (hd intrs));
+    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
+    val iTs = term_tvars concl;
     val Tvs = map TVar iTs;
-    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
-    val (Const (s, T), ts') = strip_comb S;
-    val setT = body_type T;
-    val elT = HOLogic.dest_setT setT;
-    val x = Var (("x", 0), elT);
+    val (h as Const (s, T), us) = strip_comb concl;
+    val params = List.take (us, nparms);
+    val elTs = List.drop (binder_types T, nparms);
+    val predT = elTs ---> HOLogic.boolT;
+    val used = map (fst o fst o dest_Var) params;
+    val xs = map (Var o apfst (rpair 0))
+      (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
     val rT = if n then Extraction.nullT
       else Type (space_implode "_" (s ^ "T" :: vs),
         map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
     val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
+    val S = list_comb (h, params @ xs);
     val rvs = relevant_vars S;
     val vs' = map fst rvs \\ vs;
     val rname = space_implode "_" (s ^ "R" :: vs);
@@ -119,23 +168,20 @@
       end;
 
     val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
-    val ts = map (gen_rvar vs) ts';
+    val ts = map (gen_rvar vs) params;
     val argTs = map fastype_of ts;
 
-  in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
+  in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
        Extraction.mk_typ rT)),
-    (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
-       if n then
-         HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
-       else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
-         argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
+    (prems, (mk_rlz rT $ r $ S,
+       if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
+       else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
   end;
 
-fun fun_of_prem thy rsets vs params rule intr =
+fun fun_of_prem thy rsets vs params rule ivs intr =
   let
-    (* add_term_vars and Term.add_vars may return variables in different order *)
-    val args = map (Free o apfst fst o dest_Var)
-      (add_term_vars (prop_of intr, []) \\ map Var params);
+    val ctxt = ProofContext.init thy
+    val args = map (Free o apfst fst o dest_Var) ivs;
     val args' = map (Free o apfst fst)
       (Term.add_vars (prop_of intr) [] \\ params);
     val rule' = strip_all rule;
@@ -146,7 +192,9 @@
 
     fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
       | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
-      | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
+      | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
+          Const (s, _) => can (InductivePackage.the_inductive ctxt) s
+        | _ => true)
       | is_meta _ = false;
 
     fun fun_of ts rts args used (prem :: prems) =
@@ -189,50 +237,42 @@
           in if conclT = Extraction.nullT
             then list_abs_free (map dest_Free xs, HOLogic.unit)
             else list_abs_free (map dest_Free xs, list_comb
-              (Free ("r" ^ Sign.base_name (Thm.get_name intr),
+              (Free ("r" ^ Sign.base_name (name_of_thm intr),
                 map fastype_of (rev args) ---> conclT), rev args))
           end
 
   in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
 
-fun find_first f = Library.find_first f;
-
 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
   let
     val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
     val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
-      SOME (map (fn r => List.nth (prems_of raw_induct,
+      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
         find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
-    val concls' = List.mapPartial (fn (s, _) => if s mem rsets then
-        find_first (fn concl => s mem term_consts concl) concls
-      else NONE) rss;
-    val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
+    val fs = maps (fn ((intrs, prems), dummy) =>
       let
-        val (intrs1, intrs2) = chop (length prems) intrs;
-        val fs = map (fn (rule, intr) =>
-          fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
-      in (intrs2, if dummy then Const ("arbitrary",
+        val fs = map (fn (rule, (ivs, intr)) =>
+          fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
+      in if dummy then Const ("arbitrary",
           HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
-        else fs)
-      end) (intrs, (premss ~~ dummies))));
+        else fs
+      end) (premss ~~ dummies);
     val frees = fold Term.add_frees fs [];
     val Ts = map fastype_of fs;
-    val rlzs = List.mapPartial (fn (a, concl) =>
+    fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
+  in
+    fst (fold_map (fn concl => fn names =>
       let val T = Extraction.etype_of thy vs [] concl
-      in if T = Extraction.nullT then NONE
-        else SOME (list_comb (Const (a, Ts ---> T), fs))
-      end) (rec_names ~~ concls')
-  in if null rlzs then Extraction.nullt else
-    let
-      val r = foldr1 HOLogic.mk_prod rlzs;
-      val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
-      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
-      val r' = list_abs_free (List.mapPartial (fn intr =>
-        Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
-          if length concls = 1 then r $ x else r)
-    in
-      if length concls = 1 then lambda x r' else r'
-    end
+      in if T = Extraction.nullT then (Extraction.nullt, names) else
+        let
+          val Type ("fun", [U, _]) = T;
+          val a :: names' = names
+        in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
+          Option.map (pair (name_of_fn intr))
+            (AList.lookup (op =) frees (name_of_fn intr))) intrs,
+          list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
+        end
+      end) concls rec_names)
   end;
 
 fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
@@ -254,48 +294,47 @@
         |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
       end;
 
-fun mk_realizer thy vs params ((rule, rrule), rt) =
+fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
   let
-    val prems = prems_of rule ~~ prems_of rrule;
     val rvs = map fst (relevant_vars (prop_of rule));
     val xs = rev (Term.add_vars (prop_of rule) []);
     val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
     val rlzvs = rev (Term.add_vars (prop_of rrule) []);
     val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
-    val rs = subtract (op = o pairself fst) xs rlzvs;
-
-    fun mk_prf _ [] prf = prf
-      | mk_prf rs ((prem, rprem) :: prems) prf =
-          if Extraction.etype_of thy vs [] prem = Extraction.nullT
-          then AbsP ("H", SOME rprem, mk_prf rs prems prf)
-          else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
-            mk_prf (tl rs) prems prf));
-
-  in (Thm.get_name rule, (vs,
+    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
+    val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
+    val rlz'' = foldr forall_intr_term rlz vs2
+  in (name, (vs,
     if rt = Extraction.nullt then rt else
       foldr (uncurry lambda) rt vs1,
-    foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
-      (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
+    ProofRewriteRules.un_hhf_proof rlz' rlz''
+      (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
   end;
 
-fun add_rule r rss =
+fun partition_rules induct intrs =
   let
-    val _ $ (_ $ _ $ S) = concl_of r;
-    val (Const (s, _), _) = strip_comb S;
+    fun name_of t = fst (dest_Const (head_of t));
+    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
+    val sets = map (name_of o fst o HOLogic.dest_imp) ts;
   in
-    rss
-    |> AList.default (op =) (s, [])
-    |> AList.map_entry (op =) s (fn rs => rs @ [r])
+    map (fn s => (s, filter
+      (equal s o name_of o HOLogic.dest_Trueprop o concl_of) intrs)) sets
   end;
 
 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   let
+    val qualifier = NameSpace.qualifier (name_of_thm induct);
+    val inducts = PureThy.get_thms thy (Name
+      (NameSpace.qualified qualifier "inducts"));
     val iTs = term_tvars (prop_of (hd intrs));
     val ar = length vs + length iTs;
-    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
-    val (_, params) = strip_comb S;
+    val params = params_of raw_induct;
+    val arities = arities_of raw_induct;
+    val nparms = length params;
     val params' = map dest_Var params;
-    val rss = [] |> fold add_rule intrs;
+    val rss = partition_rules raw_induct intrs;
+    val rss' = map (fn (((s, rs), (_, arity)), elim) =>
+      (s, (infer_intro_vars elim arity rs ~~ rs))) (rss ~~ arities ~~ elims);
     val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
 
@@ -303,7 +342,7 @@
       Theory.root_path |>
       Theory.add_path (NameSpace.implode prfx);
     val (ty_eqs, rlz_eqs) = split_list
-      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
+      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
 
     val thy1' = thy1 |>
       Theory.copy |>
@@ -312,7 +351,7 @@
         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
         Extraction.add_typeof_eqns_i ty_eqs;
     val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
-      SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
+      SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
 
     (** datatype representing computational content of inductive set **)
 
@@ -338,51 +377,89 @@
         ((get #rec_thms dt_info, dummies), rss);
     val rintrs = map (fn (intr, c) => Envir.eta_contract
       (Extraction.realizes_of thy2 vs
-        c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
-          (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
-            (intrs ~~ List.concat constrss);
-    val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem
-      (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
+        (if c = Extraction.nullt then c else list_comb (c, map Var (rev
+          (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
+            (maps snd rss ~~ List.concat constrss);
+    val (rlzpreds, rlzpreds') = split_list
+      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
+        let
+          val Const (s, T) = head_of (HOLogic.dest_Trueprop
+            (Logic.strip_assums_concl rintr));
+          val s' = Sign.base_name s;
+          val T' = Logic.unvarifyT T
+        in ((s', SOME T', NoSyn),
+          (Const (s, T'), Free (s', T')))
+        end) rintrs));
+    val rlzparams = map (fn Var ((s, _), T) => (s, SOME (Logic.unvarifyT T)))
+      (List.take (snd (strip_comb
+        (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
 
     (** realizability predicate **)
 
-    val (thy3', ind_info) = thy2 |>
-      OldInductivePackage.add_inductive_i false true "" false false false
-        (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
-          ((Sign.base_name (Thm.get_name intr), strip_all
-            (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
+    val (ind_info, thy3') = thy2 |>
+      TheoryTarget.init NONE |>
+      InductivePackage.add_inductive_i false "" false false false
+        rlzpreds rlzparams (map (fn (rintr, intr) =>
+          ((Sign.base_name (name_of_thm intr), []),
+           subst_atomic rlzpreds' (Logic.unvarify rintr)))
+             (rintrs ~~ maps snd rss)) [] ||>
+      ProofContext.theory_of o LocalTheory.exit ||>
       Theory.absolute_path;
     val thy3 = PureThy.hide_thms false
-      (map Thm.get_name (#intrs ind_info)) thy3';
+      (map name_of_thm (#intrs ind_info)) thy3';
 
     (** realizer for induction rule **)
 
-    val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then
+    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
       SOME (fst (fst (dest_Var (head_of P)))) else NONE)
         (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
 
     fun add_ind_realizer (thy, Ps) =
       let
-        val r = indrule_realizer thy induct raw_induct rsets params'
-          (vs @ Ps) rec_names rss intrs dummies;
-        val rlz = strip_all (Logic.unvarify
-          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
+        val rs = indrule_realizer thy induct raw_induct rsets params'
+          (vs @ Ps) rec_names rss' intrs dummies;
+        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r
+          (prop_of ind)) (rs ~~ inducts);
+        val used = foldr add_term_free_names [] rlzs;
+        val rnames = Name.variant_list used (replicate (length inducts) "r");
+        val rnames' = Name.variant_list
+          (used @ rnames) (replicate (length intrs) "s");
+        val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
+          let
+            val (P, Q) = strip_one name (Logic.unvarify rlz);
+            val Q' = strip_all' [] rnames' Q
+          in
+            (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
+          end) (rlzs ~~ rnames);
+        val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
+          (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
         val rews = map mk_meta_eq
           (fst_conv :: snd_conv :: get #rec_thms dt_info);
-        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
-          [if length rss = 1 then
-             cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
-           else EVERY [rewrite_goals_tac (rews @ all_simps),
-             REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
+        val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
+          [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
+          (NameSpace.qualified qualifier "induct" :: vs @ Ps @
+             ["correctness"]), thm), []) thy;
+        val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
+          (DatatypeAux.split_conj_thm thm');
+        val ([thms'], thy'') = PureThy.add_thmss
+          [((space_implode "_"
+             (NameSpace.qualified qualifier "inducts" :: vs @ Ps @
+               ["correctness"]), thms), [])] thy';
+        val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
       in
         Extraction.add_realizers_i
-          [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
+          (map (fn (((ind, corr), rlz), r) =>
+              mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
+            realizers @ (case realizers of
+             [(((ind, corr), rlz), r)] =>
+               [mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct",
+                  ind, corr, rlz, r)]
+           | _ => [])) thy''
       end;
 
     (** realizer for elimination rules **)
@@ -394,15 +471,13 @@
       (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
       let
         val (prem :: prems) = prems_of elim;
-        fun reorder1 (p, intr) =
+        fun reorder1 (p, (_, intr)) =
           Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
             (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
-        fun reorder2 (intr, i) =
-          let
-            val fs1 = term_vars (prop_of intr) \\ params;
-            val fs2 = Term.add_vars (prop_of intr) [] \\ params'
+        fun reorder2 ((ivs, intr), i) =
+          let val fs = Term.add_vars (prop_of intr) [] \\ params'
           in Library.foldl (fn (t, x) => lambda (Var x) t)
-            (list_comb (Bound (i + length fs1), fs1), fs2)
+            (list_comb (Bound (i + length ivs), ivs), fs)
           end;
         val p = Logic.list_implies
           (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
@@ -416,37 +491,36 @@
              else []) @
             map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
             [Bound (length prems)]));
-        val rlz = strip_all (Logic.unvarify
-          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
+        val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
+        val rlz' = strip_all (Logic.unvarify rlz);
         val rews = map mk_meta_eq case_thms;
-        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
+        val thm = Goal.prove_global thy []
+          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
           [cut_facts_tac [hd prems] 1,
            etac elimR 1,
-           ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
+           ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
+          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i
-          [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
+          [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
       end;
 
     (** add realizers to theory **)
 
-    val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
-      (#intrs ind_info, find_index (fn th => eq_thm (th, r)) intrs)) rs) rss);
     val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
     val thy5 = Extraction.add_realizers_i
-      (map (mk_realizer thy4 vs params')
-         (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
-            map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 
-              (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
-    val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
-        Option.map (rpair intrs) (find_first (fn (thm, _) =>
-          s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info))
-      else NONE) rss;
+      (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
+         (name_of_thm rule, rule, rrule, rlz,
+            list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
+              (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
+                 List.concat constrss))) thy4;
+    val elimps = List.mapPartial (fn ((s, intrs), p) =>
+      if s mem rsets then SOME (p, intrs) else NONE)
+        (rss' ~~ (elims ~~ #elims ind_info));
     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
@@ -457,12 +531,9 @@
 fun add_ind_realizers name rsets thy =
   let
     val (_, {intrs, induct, raw_induct, elims, ...}) =
-      (case OldInductivePackage.get_inductive thy name of
-         NONE => error ("Unknown inductive set " ^ quote name)
-       | SOME info => info);
-    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
+      InductivePackage.the_inductive (ProofContext.init thy) name;
     val vss = sort (int_ord o pairself length)
-      (subsets (map fst (relevant_vars S)))
+      (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   in
     Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
   end
@@ -472,8 +543,8 @@
     fun err () = error "ind_realizer: bad rule";
     val sets =
       (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
-           [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
-         | xs => map (set_of o fst o HOLogic.dest_imp) xs)
+           [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
+         | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
          handle TERM _ => err () | Empty => err ();
   in 
     add_ind_realizers (hd sets)