--- 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: