# 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 \" and "CR2 \" and "CR3 \" proof (induct \) - 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 \1 \2) - have ih_CR3_\1: "CR3 \1" by fact - have ih_CR1_\2: "CR1 \2" by fact - show "CR1 (\1 \ \2)" - proof (simp add: CR1_def, intro strip) - fix t - assume a: "\u. u \ RED \1 \ App t u \ RED \2" - from ih_CR3_\1 have "CR4 \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)\ RED \1" by (simp add: CR4_def) - with a have "App t (Var a) \ RED \2" by simp - hence "SN (App t (Var a))" using ih_CR1_\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 \1 \2) - have ih_CR1_\1: "CR1 \1" by fact - have ih_CR2_\2: "CR2 \2" by fact - show "CR2 (\1 \ \2)" - proof (simp add: CR2_def, intro strip) - fix t1 t2 u - assume "(\u. u \ RED \1 \ App t1 u \ RED \2) \ t1 \\<^isub>\ t2" - and "u \ RED \1" - hence "t1 \\<^isub>\ t2" and "App t1 u \ RED \2" by simp_all - thus "App t2 u \ RED \2" using ih_CR2_\2 by (force simp add: CR2_def) - qed -next - case (TArr3 \1 \2) - have ih_CR1_\1: "CR1 \1" by fact - have ih_CR2_\1: "CR2 \1" by fact - have ih_CR3_\2: "CR3 \2" by fact - show "CR3 (\1 \ \2)" - proof (simp add: CR3_def, intro strip) - fix t u - assume a1: "u \ RED \1" - assume a2: "NEUT t \ CR3_RED t (\1 \ \2)" - from a1 have "SN(u)" using ih_CR1_\1 by (simp add: CR1_def) - hence "u\RED \1\(\t. (NEUT t\CR2 \1\CR3 \2\CR3_RED t (\1\\2))\(App t u)\RED \2)" - by (rule sub_ind) - with a1 a2 show "(App t u)\RED \2" using ih_CR2_\1 ih_CR3_\2 by simp - qed + case (TArr \1 \2) + { case 1 + have ih_CR3_\1: "CR3 \1" by fact + have ih_CR1_\2: "CR1 \2" by fact + show "CR1 (\1 \ \2)" + proof (simp add: CR1_def, intro strip) + fix t + assume a: "\u. u \ RED \1 \ App t u \ RED \2" + from ih_CR3_\1 have "CR4 \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)\ RED \1" by (simp add: CR4_def) + with a have "App t (Var a) \ RED \2" by simp + hence "SN (App t (Var a))" using ih_CR1_\2 by (simp add: CR1_def) + thus "SN(t)" by (rule qq3) + qed + next + case 2 + have ih_CR1_\1: "CR1 \1" by fact + have ih_CR2_\2: "CR2 \2" by fact + show "CR2 (\1 \ \2)" + proof (simp add: CR2_def, intro strip) + fix t1 t2 u + assume "(\u. u \ RED \1 \ App t1 u \ RED \2) \ t1 \\<^isub>\ t2" + and "u \ RED \1" + hence "t1 \\<^isub>\ t2" and "App t1 u \ RED \2" by simp_all + thus "App t2 u \ RED \2" using ih_CR2_\2 by (force simp add: CR2_def) + qed + next + case 3 + have ih_CR1_\1: "CR1 \1" by fact + have ih_CR2_\1: "CR2 \1" by fact + have ih_CR3_\2: "CR3 \2" by fact + show "CR3 (\1 \ \2)" + proof (simp add: CR3_def, intro strip) + fix t u + assume a1: "u \ RED \1" + assume a2: "NEUT t \ CR3_RED t (\1 \ \2)" + from a1 have "SN(u)" using ih_CR1_\1 by (simp add: CR1_def) + hence "u\RED \1\(\t. (NEUT t\CR2 \1\CR3 \2\CR3_RED t (\1\\2))\(App t u)\RED \2)" + by (rule sub_ind) + with a1 a2 show "(App t u)\RED \2" using ih_CR2_\1 ih_CR3_\2 by simp + qed + } qed lemma double_acc_aux: