# HG changeset patch
# User urbanc
# Date 1136638238 -3600
# Node ID 687c9bffbca1af159fffb42c4fd6ca258103400a
# Parent  05a5e950d5f1cb942d4ab21d3cc87f041060abc4
another change for the new induct-method

diff -r 05a5e950d5f1 -r 687c9bffbca1 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Sat Jan 07 12:28:25 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Sat Jan 07 13:50:38 2006 +0100
@@ -646,56 +646,60 @@
 lemma RED_props: 
   shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
 proof (induct \<tau>)
-  case (TVar1 a) show "CR1 (TVar a)" by (simp add: CR1_def)
-next
-  case (TVar2 a) show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
-next
-  case (TVar3 a) show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
-next
-  case (TArr1 \<tau>1 \<tau>2)
-  have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
-  have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
-  show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
-  proof (simp add: CR1_def, intro strip)
-    fix t
-    assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
-    from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4) 
-    moreover
-    have "NEUT (Var a)" by (force simp add: NEUT_def)
-    moreover
-    have "NORMAL (Var a)" by (rule NORMAL_Var)
-    ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
-    with a have "App t (Var a) \<in> RED \<tau>2" by simp
-    hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
-    thus "SN(t)" by (rule qq3)
-  qed
+  case (TVar a)
+  { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
+  next
+    case 2 show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
+  next
+    case 3 show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
+  }
 next
-  case (TArr2 \<tau>1 \<tau>2)
-  have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
-  have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
-  show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
-  proof (simp add: CR2_def, intro strip)
-    fix t1 t2 u
-    assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and>  t1 \<longrightarrow>\<^isub>\<beta> t2" 
-      and  "u \<in> RED \<tau>1"
-    hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
-    thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
-  qed
-next
-  case (TArr3 \<tau>1 \<tau>2)
-  have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
-  have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
-  have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
-  show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
-  proof (simp add: CR3_def, intro strip)
-    fix t u
-    assume a1: "u \<in> RED \<tau>1"
-    assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
-    from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
-    hence "u\<in>RED \<tau>1\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>1\<and>CR3 \<tau>2\<and>CR3_RED t (\<tau>1\<rightarrow>\<tau>2))\<longrightarrow>(App t u)\<in>RED \<tau>2)" 
-      by (rule sub_ind)
-    with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
-  qed
+  case (TArr \<tau>1 \<tau>2)
+  { case 1
+    have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
+    have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
+    show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
+    proof (simp add: CR1_def, intro strip)
+      fix t
+      assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
+      from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4) 
+      moreover
+      have "NEUT (Var a)" by (force simp add: NEUT_def)
+      moreover
+      have "NORMAL (Var a)" by (rule NORMAL_Var)
+      ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
+      with a have "App t (Var a) \<in> RED \<tau>2" by simp
+      hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
+      thus "SN(t)" by (rule qq3)
+    qed
+  next
+    case 2
+    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
+    have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
+    show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
+    proof (simp add: CR2_def, intro strip)
+      fix t1 t2 u
+      assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and>  t1 \<longrightarrow>\<^isub>\<beta> t2" 
+	and  "u \<in> RED \<tau>1"
+      hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
+      thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
+    qed
+  next
+    case 3
+    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
+    have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
+    have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
+    show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
+    proof (simp add: CR3_def, intro strip)
+      fix t u
+      assume a1: "u \<in> RED \<tau>1"
+      assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
+      from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
+      hence "u\<in>RED \<tau>1\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>1\<and>CR3 \<tau>2\<and>CR3_RED t (\<tau>1\<rightarrow>\<tau>2))\<longrightarrow>(App t u)\<in>RED \<tau>2)" 
+	by (rule sub_ind)
+      with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
+    qed
+  }
 qed
     
 lemma double_acc_aux: