1.1 --- a/src/HOL/MicroJava/BV/Step.thy Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/MicroJava/BV/Step.thy Fri Oct 05 21:52:39 2001 +0200
1.3 @@ -114,26 +114,26 @@
1.4 "succs (Invoke C mn fpTs) pc = [pc+1]"
1.5
1.6
1.7 -lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
1.8 +lemma 1: "Suc (Suc 0) < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
1.9 proof (cases a)
1.10 - fix x xs assume "a = x#xs" "2 < length a"
1.11 + fix x xs assume "a = x#xs" "Suc (Suc 0) < length a"
1.12 thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
1.13 qed auto
1.14
1.15 -lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
1.16 +lemma 2: "\<not>(Suc (Suc 0) < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
1.17 proof -;
1.18 - assume "\<not>(2 < length a)"
1.19 - hence "length a < (Suc 2)" by simp
1.20 - hence * : "length a = 0 \<or> length a = 1' \<or> length a = 2"
1.21 + assume "\<not>(Suc (Suc 0) < length a)"
1.22 + hence "length a < Suc (Suc (Suc 0))" by simp
1.23 + hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)"
1.24 by (auto simp add: less_Suc_eq)
1.25
1.26 {
1.27 fix x
1.28 - assume "length x = 1'"
1.29 + assume "length x = Suc 0"
1.30 hence "\<exists> l. x = [l]" by - (cases x, auto)
1.31 } note 0 = this
1.32
1.33 - have "length a = 2 ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
1.34 + have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
1.35 with * show ?thesis by (auto dest: 0)
1.36 qed
1.37
1.38 @@ -152,7 +152,7 @@
1.39
1.40 lemma appStore[simp]:
1.41 "(app (Store idx) G maxs rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
1.42 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.43 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.44
1.45 lemma appLitPush[simp]:
1.46 "(app (LitPush v) G maxs rT (Some s)) = (maxs < length (fst s) \<and> typeof (\<lambda>v. None) v \<noteq> None)"
1.47 @@ -162,13 +162,13 @@
1.48 "(app (Getfield F C) G maxs rT (Some s)) =
1.49 (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>
1.50 field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C))"
1.51 - by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def)
1.52 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest!: 1 2 simp add: app_def)
1.53
1.54 lemma appPutField[simp]:
1.55 "(app (Putfield F C) G maxs rT (Some s)) =
1.56 (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>
1.57 field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT')"
1.58 - by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def)
1.59 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest!: 1 2 simp add: app_def)
1.60
1.61 lemma appNew[simp]:
1.62 "(app (New C) G maxs rT (Some s)) = (is_class G C \<and> maxs < length (fst s))"
1.63 @@ -181,27 +181,27 @@
1.64
1.65 lemma appPop[simp]:
1.66 "(app Pop G maxs rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
1.67 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.68 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.69
1.70
1.71 lemma appDup[simp]:
1.72 "(app Dup G maxs rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> maxs < Suc (length ST))"
1.73 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.74 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.75
1.76
1.77 lemma appDup_x1[simp]:
1.78 "(app Dup_x1 G maxs rT (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> maxs < Suc (Suc (length ST)))"
1.79 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.80 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.81
1.82
1.83 lemma appDup_x2[simp]:
1.84 "(app Dup_x2 G maxs rT (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \<and> maxs < Suc (Suc (Suc (length ST))))"
1.85 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.86 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.87
1.88
1.89 lemma appSwap[simp]:
1.90 "app Swap G maxs rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
1.91 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.92 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.93
1.94
1.95 lemma appIAdd[simp]:
1.96 @@ -238,12 +238,12 @@
1.97 lemma appIfcmpeq[simp]:
1.98 "app (Ifcmpeq b) G maxs rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and>
1.99 ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))"
1.100 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.101 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.102
1.103
1.104 lemma appReturn[simp]:
1.105 "app Return G maxs rT (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))"
1.106 - by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
1.107 + by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
1.108
1.109 lemma appGoto[simp]:
1.110 "app (Goto branch) G maxs rT (Some s) = True"