another change for the new induct-method
authorurbanc
Sat Jan 07 13:50:38 2006 +0100 (2006-01-07)
changeset 18611687c9bffbca1
parent 18610 05a5e950d5f1
child 18612 7300f75028dc
another change for the new induct-method
src/HOL/Nominal/Examples/SN.thy
     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.111      
   1.112  lemma double_acc_aux: