src/HOL/MicroJava/BV/Listn.thy
changeset 13066 b57d926d1de2
parent 13006 51c5f3f11d16
child 13074 96bf406fd3e5
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 24 14:05:53 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 24 14:06:21 2002 +0100
     1.3 @@ -142,6 +142,20 @@
     1.4  apply auto
     1.5  done  
     1.6  
     1.7 +lemma le_list_appendI:
     1.8 +  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
     1.9 +apply (induct a)
    1.10 + apply simp
    1.11 +apply (case_tac b)
    1.12 +apply auto
    1.13 +done
    1.14 +
    1.15 +lemma le_listI:
    1.16 +  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
    1.17 +  apply (unfold lesub_def Listn.le_def)
    1.18 +  apply (simp add: list_all2_conv_all_nth)
    1.19 +  done
    1.20 +
    1.21  lemma listI:
    1.22    "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
    1.23  apply (unfold list_def)
    1.24 @@ -202,6 +216,37 @@
    1.25    "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
    1.26    by auto
    1.27  
    1.28 +
    1.29 +lemma listn_Cons_Suc [elim!]:
    1.30 +  "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
    1.31 +  by (cases n) auto
    1.32 +
    1.33 +lemma listn_appendE [elim!]:
    1.34 +  "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P" 
    1.35 +proof -
    1.36 +  have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
    1.37 +    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
    1.38 +  proof (induct a)
    1.39 +    fix n assume "?list [] n"
    1.40 +    hence "?P [] n 0 n" by simp
    1.41 +    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
    1.42 +  next
    1.43 +    fix n l ls
    1.44 +    assume "?list (l#ls) n"
    1.45 +    then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
    1.46 +    assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
    1.47 +    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
    1.48 +    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
    1.49 +    with n have "?P (l#ls) n (n1+1) n2" by simp
    1.50 +    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
    1.51 +  qed
    1.52 +  moreover
    1.53 +  assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
    1.54 +  ultimately
    1.55 +  show ?thesis by blast
    1.56 +qed
    1.57 +
    1.58 +
    1.59  lemma listt_update_in_list [simp, intro!]:
    1.60    "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
    1.61  apply (unfold list_def)