author urbanc Sat Jan 07 13:50:38 2006 +0100 (2006-01-07) changeset 18611 687c9bffbca1 parent 18610 05a5e950d5f1 child 18612 7300f75028dc
another change for the new induct-method
1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Sat Jan 07 12:28:25 2006 +0100
1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sat Jan 07 13:50:38 2006 +0100
1.3 @@ -646,56 +646,60 @@
1.4  lemma RED_props:
1.5    shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
1.6  proof (induct \<tau>)
1.7 -  case (TVar1 a) show "CR1 (TVar a)" by (simp add: CR1_def)
1.8 -next
1.9 -  case (TVar2 a) show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
1.10 -next
1.11 -  case (TVar3 a) show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
1.12 -next
1.13 -  case (TArr1 \<tau>1 \<tau>2)
1.14 -  have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
1.15 -  have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
1.16 -  show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
1.17 -  proof (simp add: CR1_def, intro strip)
1.18 -    fix t
1.19 -    assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
1.20 -    from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4)
1.21 -    moreover
1.22 -    have "NEUT (Var a)" by (force simp add: NEUT_def)
1.23 -    moreover
1.24 -    have "NORMAL (Var a)" by (rule NORMAL_Var)
1.25 -    ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
1.26 -    with a have "App t (Var a) \<in> RED \<tau>2" by simp
1.27 -    hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
1.28 -    thus "SN(t)" by (rule qq3)
1.29 -  qed
1.30 +  case (TVar a)
1.31 +  { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
1.32 +  next
1.33 +    case 2 show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
1.34 +  next
1.35 +    case 3 show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
1.36 +  }
1.37  next
1.38 -  case (TArr2 \<tau>1 \<tau>2)
1.39 -  have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
1.40 -  have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
1.41 -  show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
1.42 -  proof (simp add: CR2_def, intro strip)
1.43 -    fix t1 t2 u
1.44 -    assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and>  t1 \<longrightarrow>\<^isub>\<beta> t2"
1.45 -      and  "u \<in> RED \<tau>1"
1.46 -    hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
1.47 -    thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
1.48 -  qed
1.49 -next
1.50 -  case (TArr3 \<tau>1 \<tau>2)
1.51 -  have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
1.52 -  have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
1.53 -  have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
1.54 -  show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
1.55 -  proof (simp add: CR3_def, intro strip)
1.56 -    fix t u
1.57 -    assume a1: "u \<in> RED \<tau>1"
1.58 -    assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
1.59 -    from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
1.60 -    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)"
1.61 -      by (rule sub_ind)
1.62 -    with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
1.63 -  qed
1.64 +  case (TArr \<tau>1 \<tau>2)
1.65 +  { case 1
1.66 +    have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
1.67 +    have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
1.68 +    show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
1.69 +    proof (simp add: CR1_def, intro strip)
1.70 +      fix t
1.71 +      assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
1.72 +      from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4)
1.73 +      moreover
1.74 +      have "NEUT (Var a)" by (force simp add: NEUT_def)
1.75 +      moreover
1.76 +      have "NORMAL (Var a)" by (rule NORMAL_Var)
1.77 +      ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
1.78 +      with a have "App t (Var a) \<in> RED \<tau>2" by simp
1.79 +      hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
1.80 +      thus "SN(t)" by (rule qq3)
1.81 +    qed
1.82 +  next
1.83 +    case 2
1.84 +    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
1.85 +    have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
1.86 +    show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
1.87 +    proof (simp add: CR2_def, intro strip)
1.88 +      fix t1 t2 u
1.89 +      assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and>  t1 \<longrightarrow>\<^isub>\<beta> t2"
1.90 +	and  "u \<in> RED \<tau>1"
1.91 +      hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
1.92 +      thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
1.93 +    qed
1.94 +  next
1.95 +    case 3
1.96 +    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
1.97 +    have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
1.98 +    have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
1.99 +    show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
1.100 +    proof (simp add: CR3_def, intro strip)
1.101 +      fix t u
1.102 +      assume a1: "u \<in> RED \<tau>1"
1.103 +      assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
1.104 +      from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
1.105 +      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)"
1.106 +	by (rule sub_ind)
1.107 +      with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
1.108 +    qed
1.109 +  }
1.110  qed
1.112  lemma double_acc_aux: