# HG changeset patch
# User urbanc
# Date 1136630218 -3600
# Node ID e01112713fdc538a0ffea33156df74974cf17318
# Parent  94d658871c98fd5e08f06703d93c0eaa198574f0
changed PRO_RED proof to conform with the new induction rules

diff -r 94d658871c98 -r e01112713fdc src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Fri Jan 06 18:18:16 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Sat Jan 07 11:36:58 2006 +0100
@@ -646,56 +646,56 @@
 lemma RED_props: 
   shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
 proof (induct \<tau>)
-  case (TVar a)
-  have "CR1 (TVar a)" by (simp add: CR1_def)
-  moreover
-  have "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
-  moreover
-  have "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
-  ultimately show "CR1 (TVar a) \<and> CR2 (TVar a) \<and> CR3 (TVar a)" by simp
+  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 (TArr \<tau>1 \<tau>2)
-  have ih_\<tau>1: "CR1 \<tau>1 \<and> CR2 \<tau>1 \<and> CR3 \<tau>1" by fact
-  have ih_\<tau>2: "CR1 \<tau>2 \<and> CR2 \<tau>2 \<and> CR3 \<tau>2" by fact
-  have "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
+  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_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4) 
+    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
-    moreover 
-    from ih_\<tau>2 have "CR1 \<tau>2" by simp
-    ultimately have "SN (App t (Var a))" by (simp add: CR1_def)
+    hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
     thus "SN(t)" by (rule qq3)
   qed
-  moreover
-  have "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
+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"
+      and  "u \<in> RED \<tau>1"
     hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
-    moreover
-    from ih_\<tau>2 have "CR2 \<tau>2" by simp
-    ultimately show "App t2 u \<in> RED \<tau>2" by (force simp add: CR2_def)
+    thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
   qed
-  moreover
-  have "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
+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_\<tau>1 by (simp add: CR1_def)
+    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_\<tau>1 ih_\<tau>2 by simp
+    with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
   qed
-  ultimately show "CR1 (\<tau>1 \<rightarrow> \<tau>2) \<and> CR2 (\<tau>1 \<rightarrow> \<tau>2) \<and> CR3 (\<tau>1 \<rightarrow> \<tau>2)" by blast
 qed
     
 lemma double_acc_aux: