proper setup of "parallel";
authorwenzelm
Fri Nov 03 21:35:36 2000 +0100 (2000-11-03)
changeset 10389c7d8901ab269
parent 10388 ac1ae85a5605
child 10390 1d54567bed24
proper setup of "parallel";
removed unused rules;
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Nov 03 21:34:22 2000 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Nov 03 21:35:36 2000 +0100
     1.3 @@ -15,86 +15,85 @@
     1.4  instance list :: ("term") ord ..
     1.5  
     1.6  defs (overloaded)
     1.7 -  prefix_def: "xs \<le> zs == \<exists>ys. zs = xs @ ys"
     1.8 -  strict_prefix_def: "xs < zs == xs \<le> zs \<and> xs \<noteq> (zs::'a list)"
     1.9 +  prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
    1.10 +  strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.11  
    1.12  instance list :: ("term") order
    1.13 -proof
    1.14 -  fix xs ys zs :: "'a list"
    1.15 -  show "xs \<le> xs" by (simp add: prefix_def)
    1.16 -  { assume "xs \<le> ys" and "ys \<le> zs" thus "xs \<le> zs" by (auto simp add: prefix_def) }
    1.17 -  { assume "xs \<le> ys" and "ys \<le> xs" thus "xs = ys" by (auto simp add: prefix_def) }
    1.18 -  show "(xs < zs) = (xs \<le> zs \<and> xs \<noteq> zs)" by (simp only: strict_prefix_def)
    1.19 -qed
    1.20 +  by intro_classes (auto simp add: prefix_def strict_prefix_def)
    1.21  
    1.22 -constdefs
    1.23 -  parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
    1.24 -  "xs \<parallel> ys == \<not> (xs \<le> ys) \<and> \<not> (ys \<le> xs)"
    1.25 +lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    1.26 +  by (unfold prefix_def) blast
    1.27  
    1.28 -lemma parallelI [intro]: "\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> xs \<parallel> ys"
    1.29 -  by (unfold parallel_def) blast
    1.30 +lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
    1.31 +  by (unfold prefix_def) blast
    1.32  
    1.33 -lemma parellelE [elim]:
    1.34 -    "xs \<parallel> ys ==> (\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> C) ==> C"
    1.35 -  by (unfold parallel_def) blast
    1.36 +lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    1.37 +  by (unfold strict_prefix_def) blast
    1.38  
    1.39 -theorem prefix_cases:
    1.40 -  "(xs \<le> ys ==> C) ==>
    1.41 -    (ys \<le> xs ==> C) ==>
    1.42 -    (xs \<parallel> ys ==> C) ==> C"
    1.43 -  by (unfold parallel_def) blast
    1.44 +lemma strict_prefixE [elim?]:
    1.45 +    "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
    1.46 +  by (unfold strict_prefix_def) blast
    1.47  
    1.48  
    1.49 -subsection {* Recursion equations *}
    1.50 +subsection {* Basic properties of prefixes *}
    1.51  
    1.52  theorem Nil_prefix [iff]: "[] \<le> xs"
    1.53 -  apply (simp add: prefix_def)
    1.54 -  done
    1.55 +  by (simp add: prefix_def)
    1.56  
    1.57  theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
    1.58 -  apply (induct_tac xs)
    1.59 -   apply simp
    1.60 -  apply (simp add: prefix_def)
    1.61 -  done
    1.62 +  by (induct xs) (simp_all add: prefix_def)
    1.63  
    1.64  lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    1.65 -  apply (unfold prefix_def)
    1.66 -  apply (rule iffI)
    1.67 -   apply (erule exE)
    1.68 -   apply (rename_tac zs)
    1.69 -   apply (rule_tac xs = zs in rev_exhaust)
    1.70 -    apply simp
    1.71 -   apply hypsubst
    1.72 -   apply (simp del: append_assoc add: append_assoc [symmetric])
    1.73 -  apply force
    1.74 -  done
    1.75 +proof
    1.76 +  assume "xs \<le> ys @ [y]"
    1.77 +  then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    1.78 +  show "xs = ys @ [y] \<or> xs \<le> ys"
    1.79 +  proof (cases zs rule: rev_cases)
    1.80 +    assume "zs = []"
    1.81 +    with zs have "xs = ys @ [y]" by simp
    1.82 +    thus ?thesis ..
    1.83 +  next
    1.84 +    fix z zs' assume "zs = zs' @ [z]"
    1.85 +    with zs have "ys = xs @ zs'" by simp
    1.86 +    hence "xs \<le> ys" ..
    1.87 +    thus ?thesis ..
    1.88 +  qed
    1.89 +next
    1.90 +  assume "xs = ys @ [y] \<or> xs \<le> ys"
    1.91 +  thus "xs \<le> ys @ [y]"
    1.92 +  proof
    1.93 +    assume "xs = ys @ [y]"
    1.94 +    thus ?thesis by simp
    1.95 +  next
    1.96 +    assume "xs \<le> ys"
    1.97 +    then obtain zs where "ys = xs @ zs" ..
    1.98 +    hence "ys @ [y] = xs @ (zs @ [y])" by simp
    1.99 +    thus ?thesis ..
   1.100 +  qed
   1.101 +qed
   1.102  
   1.103  lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
   1.104 -  apply (auto simp add: prefix_def)
   1.105 -  done
   1.106 +  by (auto simp add: prefix_def)
   1.107  
   1.108  lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
   1.109 -  apply (induct_tac xs)
   1.110 -   apply simp_all
   1.111 -  done
   1.112 +  by (induct xs) simp_all
   1.113  
   1.114 -lemma [iff]: "(xs @ ys \<le> xs) = (ys = [])"
   1.115 -  apply (insert same_prefix_prefix [where ?zs = "[]"])
   1.116 -  apply simp
   1.117 -  apply blast
   1.118 -  done
   1.119 +lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
   1.120 +proof -
   1.121 +  have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)
   1.122 +  thus ?thesis by simp
   1.123 +qed
   1.124  
   1.125  lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
   1.126 -  apply (unfold prefix_def)
   1.127 -  apply clarify
   1.128 -  apply simp
   1.129 -  done
   1.130 +proof -
   1.131 +  assume "xs \<le> ys"
   1.132 +  then obtain us where "ys = xs @ us" ..
   1.133 +  hence "ys @ zs = xs @ (us @ zs)" by simp
   1.134 +  thus ?thesis ..
   1.135 +qed
   1.136  
   1.137  theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   1.138 -  apply (unfold prefix_def)
   1.139 -  apply (case_tac xs)
   1.140 -   apply auto
   1.141 -  done
   1.142 +  by (cases xs) (auto simp add: prefix_def)
   1.143  
   1.144  theorem prefix_append:
   1.145      "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
   1.146 @@ -109,42 +108,78 @@
   1.147      "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
   1.148    apply (unfold prefix_def)
   1.149    apply (auto simp add: nth_append)
   1.150 -  apply (case_tac ys)
   1.151 +  apply (case_tac zs)
   1.152     apply auto
   1.153    done
   1.154  
   1.155  theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   1.156 -  apply (auto simp add: prefix_def)
   1.157 -  done
   1.158 +  by (auto simp add: prefix_def)
   1.159  
   1.160  
   1.161 -subsection {* Prefix cases *}
   1.162 +subsection {* Parallel lists *}
   1.163 +
   1.164 +constdefs
   1.165 +  parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
   1.166 +  "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   1.167 +
   1.168 +lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
   1.169 +  by (unfold parallel_def) blast
   1.170  
   1.171 -lemma prefix_Nil_cases [case_names Nil]:
   1.172 -  "xs \<le> [] ==>
   1.173 -    (xs = [] ==> C) ==> C"
   1.174 -  by simp
   1.175 +lemma parallelE [elim]:
   1.176 +    "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
   1.177 +  by (unfold parallel_def) blast
   1.178  
   1.179 -lemma prefix_Cons_cases [case_names Nil Cons]:
   1.180 -  "xs \<le> y # ys ==>
   1.181 -    (xs = [] ==> C) ==>
   1.182 -    (!!zs. xs = y # zs ==> zs \<le> ys ==> C) ==> C"
   1.183 -  by (simp only: prefix_Cons) blast
   1.184 +theorem prefix_cases:
   1.185 +  "(xs \<le> ys ==> C) ==>
   1.186 +    (ys \<le> xs ==> C) ==>
   1.187 +    (xs \<parallel> ys ==> C) ==> C"
   1.188 +  by (unfold parallel_def) blast
   1.189  
   1.190 -lemma prefix_snoc_cases [case_names prefix snoc]:
   1.191 -  "xs \<le> ys @ [y] ==>
   1.192 -    (xs \<le> ys ==> C) ==>
   1.193 -    (xs = ys @ [y] ==> C) ==> C"
   1.194 -  by (simp only: prefix_snoc) blast
   1.195 -
   1.196 -lemma prefix_append_cases [case_names prefix append]:
   1.197 -  "xs \<le> ys @ zs ==>
   1.198 -    (xs \<le> ys ==> C) ==>
   1.199 -    (!!us. xs = ys @ us ==> us \<le> zs ==> C) ==> C"
   1.200 -  by (simp only: prefix_append) blast
   1.201 -
   1.202 -lemmas prefix_any_cases [cases set: prefix] =    (*dummy set name*)
   1.203 -  prefix_Nil_cases prefix_Cons_cases
   1.204 -  prefix_snoc_cases prefix_append_cases
   1.205 +theorem parallel_decomp:
   1.206 +  "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
   1.207 +  (concl is "?E xs")
   1.208 +proof -
   1.209 +  assume "xs \<parallel> ys"
   1.210 +  have "?this --> ?E xs" (is "?P xs")
   1.211 +  proof (induct (stripped) xs rule: rev_induct)
   1.212 +    assume "[] \<parallel> ys" hence False by auto
   1.213 +    thus "?E []" ..
   1.214 +  next
   1.215 +    fix x xs
   1.216 +    assume hyp: "?P xs"
   1.217 +    assume asm: "xs @ [x] \<parallel> ys"
   1.218 +    show "?E (xs @ [x])"
   1.219 +    proof (rule prefix_cases)
   1.220 +      assume le: "xs \<le> ys"
   1.221 +      then obtain ys' where ys: "ys = xs @ ys'" ..
   1.222 +      show ?thesis
   1.223 +      proof (cases ys')
   1.224 +        assume "ys' = []" with ys have "xs = ys" by simp
   1.225 +        with asm have "[x] \<parallel> []" by auto
   1.226 +        hence False by blast
   1.227 +        thus ?thesis ..
   1.228 +      next
   1.229 +        fix c cs assume ys': "ys' = c # cs"
   1.230 +        with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
   1.231 +        hence "x \<noteq> c" by auto
   1.232 +        moreover have "xs @ [x] = xs @ x # []" by simp
   1.233 +        moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
   1.234 +        ultimately show ?thesis by blast
   1.235 +      qed
   1.236 +    next
   1.237 +      assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
   1.238 +      with asm have False by blast
   1.239 +      thus ?thesis ..
   1.240 +    next
   1.241 +      assume "xs \<parallel> ys"
   1.242 +      with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
   1.243 +          and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
   1.244 +	by blast
   1.245 +      from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
   1.246 +      with neq ys show ?thesis by blast
   1.247 +    qed
   1.248 +  qed
   1.249 +  thus ?thesis ..
   1.250 +qed
   1.251  
   1.252  end