avoid implicit use of prems;
authorwenzelm
Thu Nov 08 20:09:17 2007 +0100 (2007-11-08)
changeset 2535569c0a39ba028
parent 25354 69560579abf1
child 25356 059c03630d6e
avoid implicit use of prems;
tuned proofs;
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Nov 08 20:08:11 2007 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Nov 08 20:09:17 2007 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -lemma map_prefixI: 
     1.8 +lemma map_prefixI:
     1.9    "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
    1.10    by (clarsimp simp: prefix_def)
    1.11  
    1.12 @@ -188,36 +188,33 @@
    1.13    apply (case_tac ys, simp_all)
    1.14    done
    1.15  
    1.16 -lemma not_prefix_cases: 
    1.17 +lemma not_prefix_cases:
    1.18    assumes pfx: "\<not> ps \<le> ls"
    1.19    and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R"
    1.20    and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R"
    1.21    and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R"
    1.22 -  shows "R"  
    1.23 +  shows "R"
    1.24  proof (cases ps)
    1.25 -  case Nil thus ?thesis using pfx by simp
    1.26 +  case Nil then show ?thesis using pfx by simp
    1.27  next
    1.28    case (Cons a as)
    1.29 -  
    1.30 -  hence c: "ps = a#as" .
    1.31 -  
    1.32 +  then have c: "ps = a#as" .
    1.33 +
    1.34    show ?thesis
    1.35    proof (cases ls)
    1.36 -    case Nil thus ?thesis 
    1.37 -      by (intro c1, simp add: Cons)
    1.38 +    case Nil
    1.39 +    have "ps \<noteq> []" by (simp add: Nil Cons)
    1.40 +    from this and Nil show ?thesis by (rule c1)
    1.41    next
    1.42      case (Cons x xs)
    1.43      show ?thesis
    1.44      proof (cases "x = a")
    1.45 -      case True 
    1.46 -      show ?thesis 
    1.47 -      proof (intro c2) 
    1.48 -     	  show "\<not> as \<le> xs" using pfx c Cons True
    1.49 -	        by simp
    1.50 -      qed
    1.51 -    next 
    1.52 -      case False 
    1.53 -      show ?thesis by (rule c3)
    1.54 +      case True
    1.55 +      have "\<not> as \<le> xs" using pfx c Cons True by simp
    1.56 +      with c Cons True show ?thesis by (rule c2)
    1.57 +    next
    1.58 +      case False
    1.59 +      with c Cons show ?thesis by (rule c3)
    1.60      qed
    1.61    qed
    1.62  qed
    1.63 @@ -230,17 +227,17 @@
    1.64    shows "P ps ls"
    1.65    using np
    1.66  proof (induct ls arbitrary: ps)
    1.67 -  case Nil thus ?case  
    1.68 +  case Nil then show ?case
    1.69      by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
    1.70  next
    1.71 -  case (Cons y ys)  
    1.72 -  hence npfx: "\<not> ps \<le> (y # ys)" by simp
    1.73 -  then obtain x xs where pv: "ps = x # xs" 
    1.74 +  case (Cons y ys)
    1.75 +  then have npfx: "\<not> ps \<le> (y # ys)" by simp
    1.76 +  then obtain x xs where pv: "ps = x # xs"
    1.77      by (rule not_prefix_cases) auto
    1.78  
    1.79    from Cons
    1.80    have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp
    1.81 -  
    1.82 +
    1.83    show ?case using npfx
    1.84      by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
    1.85  qed
    1.86 @@ -305,16 +302,16 @@
    1.87  
    1.88  lemma parallel_append:
    1.89    "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
    1.90 -  by (rule parallelI) 
    1.91 -     (erule parallelE, erule conjE, 
    1.92 +  by (rule parallelI)
    1.93 +     (erule parallelE, erule conjE,
    1.94              induct rule: not_prefix_induct, simp+)+
    1.95  
    1.96 -lemma parallel_appendI: 
    1.97 +lemma parallel_appendI:
    1.98    "\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y"
    1.99    by simp (rule parallel_append)
   1.100  
   1.101  lemma parallel_commute:
   1.102 -  "(a \<parallel> b) = (b \<parallel> a)" 
   1.103 +  "(a \<parallel> b) = (b \<parallel> a)"
   1.104    unfolding parallel_def by auto
   1.105  
   1.106  subsection {* Postfix order on lists *}
   1.107 @@ -389,7 +386,7 @@
   1.108    using dx pf by (clarsimp elim!: postfixE)
   1.109  
   1.110  lemma postfix_map:
   1.111 -  assumes pf: "xs >>= ys" 
   1.112 +  assumes pf: "xs >>= ys"
   1.113    shows   "map f xs >>= map f ys"
   1.114    using pf by (auto elim!: postfixE intro: postfixI)
   1.115  
   1.116 @@ -402,15 +399,15 @@
   1.117    "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
   1.118    by (clarsimp elim!: postfixE)
   1.119  
   1.120 -lemma parallelD1: 
   1.121 +lemma parallelD1:
   1.122    "x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast
   1.123  
   1.124 -lemma parallelD2: 
   1.125 +lemma parallelD2:
   1.126    "x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast
   1.127 -  
   1.128 -lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []" 
   1.129 +
   1.130 +lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
   1.131    unfolding parallel_def by simp
   1.132 -  
   1.133 +
   1.134  lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
   1.135    unfolding parallel_def by simp
   1.136  
   1.137 @@ -418,7 +415,7 @@
   1.138    "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" by auto
   1.139  
   1.140  lemma Cons_parallelI2:
   1.141 -  "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" 
   1.142 +  "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
   1.143    apply simp
   1.144    apply (rule parallelI)
   1.145     apply simp
   1.146 @@ -432,25 +429,24 @@
   1.147    and     len: "length xs = length ys"
   1.148    shows   "xs \<parallel> ys"
   1.149    using len neq
   1.150 -proof (induct rule: list_induct2) 
   1.151 -  case 1 thus ?case by simp
   1.152 +proof (induct rule: list_induct2)
   1.153 +  case 1 then show ?case by simp
   1.154  next
   1.155    case (2 a as b bs)
   1.156 +  have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
   1.157  
   1.158 -  have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" .
   1.159 -  
   1.160    show ?case
   1.161    proof (cases "a = b")
   1.162 -    case True 
   1.163 -    hence "as \<noteq> bs" using 2 by simp
   1.164 -   
   1.165 -    thus ?thesis by (rule Cons_parallelI2 [OF True ih])
   1.166 +    case True
   1.167 +    then have "as \<noteq> bs" using 2 by simp
   1.168 +    then show ?thesis by (rule Cons_parallelI2 [OF True ih])
   1.169    next
   1.170      case False
   1.171 -    thus ?thesis by (rule Cons_parallelI1)
   1.172 +    then show ?thesis by (rule Cons_parallelI1)
   1.173    qed
   1.174  qed
   1.175  
   1.176 +
   1.177  subsection {* Exeuctable code *}
   1.178  
   1.179  lemma less_eq_code [code func]: