turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
authorhaftmann
Mon Oct 04 12:22:58 2010 +0200 (2010-10-04)
changeset 39915ecf97cf3d248
parent 39914 2f7b060d0c8d
child 39916 8c83139a1433
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
src/HOL/Library/Dlist.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Dlist.thy	Sat Oct 02 12:32:31 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Oct 04 12:22:58 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4    case (Abs_dlist xs)
     1.5    then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
     1.6    from `distinct xs` have "P (Dlist xs)"
     1.7 -  proof (induct xs rule: distinct_induct)
     1.8 +  proof (induct xs)
     1.9      case Nil from empty show ?case by (simp add: empty_def)
    1.10    next
    1.11      case (insert x xs)
     2.1 --- a/src/HOL/List.thy	Sat Oct 02 12:32:31 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Oct 04 12:22:58 2010 +0200
     2.3 @@ -157,16 +157,6 @@
     2.4      upt_0: "[i..<0] = []"
     2.5    | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
     2.6  
     2.7 -primrec
     2.8 -  distinct :: "'a list \<Rightarrow> bool" where
     2.9 -    "distinct [] \<longleftrightarrow> True"
    2.10 -  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
    2.11 -
    2.12 -primrec
    2.13 -  remdups :: "'a list \<Rightarrow> 'a list" where
    2.14 -    "remdups [] = []"
    2.15 -  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
    2.16 -
    2.17  definition
    2.18    insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.19    "insert x xs = (if x \<in> set xs then xs else x # xs)"
    2.20 @@ -184,6 +174,21 @@
    2.21      "removeAll x [] = []"
    2.22    | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
    2.23  
    2.24 +inductive
    2.25 +  distinct :: "'a list \<Rightarrow> bool" where
    2.26 +    Nil: "distinct []"
    2.27 +  | insert: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (x # xs)"
    2.28 +
    2.29 +lemma distinct_simps [simp, code]:
    2.30 +  "distinct [] \<longleftrightarrow> True"
    2.31 +  "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
    2.32 +  by (auto intro: distinct.intros elim: distinct.cases)
    2.33 +
    2.34 +primrec
    2.35 +  remdups :: "'a list \<Rightarrow> 'a list" where
    2.36 +    "remdups [] = []"
    2.37 +  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
    2.38 +
    2.39  primrec
    2.40    replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
    2.41      replicate_0: "replicate 0 x = []"
    2.42 @@ -275,10 +280,26 @@
    2.43  context linorder
    2.44  begin
    2.45  
    2.46 -fun sorted :: "'a list \<Rightarrow> bool" where
    2.47 -"sorted [] \<longleftrightarrow> True" |
    2.48 -"sorted [x] \<longleftrightarrow> True" |
    2.49 -"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
    2.50 +inductive sorted :: "'a list \<Rightarrow> bool" where
    2.51 +  Nil [iff]: "sorted []"
    2.52 +| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
    2.53 +
    2.54 +lemma sorted_single [iff]:
    2.55 +  "sorted [x]"
    2.56 +  by (rule sorted.Cons) auto
    2.57 +
    2.58 +lemma sorted_many:
    2.59 +  "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
    2.60 +  by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
    2.61 +
    2.62 +lemma sorted_many_eq [simp, code]:
    2.63 +  "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
    2.64 +  by (auto intro: sorted_many elim: sorted.cases)
    2.65 +
    2.66 +lemma [code]:
    2.67 +  "sorted [] \<longleftrightarrow> True"
    2.68 +  "sorted [x] \<longleftrightarrow> True"
    2.69 +  by simp_all
    2.70  
    2.71  primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    2.72  "insort_key f x [] = [x]" |
    2.73 @@ -2118,36 +2139,6 @@
    2.74    "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
    2.75    by (auto simp add: zip_map_fst_snd)
    2.76  
    2.77 -lemma distinct_zipI1:
    2.78 -  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
    2.79 -proof (induct xs arbitrary: ys)
    2.80 -  case (Cons x xs)
    2.81 -  show ?case
    2.82 -  proof (cases ys)
    2.83 -    case (Cons y ys')
    2.84 -    have "(x, y) \<notin> set (zip xs ys')"
    2.85 -      using Cons.prems by (auto simp: set_zip)
    2.86 -    thus ?thesis
    2.87 -      unfolding Cons zip_Cons_Cons distinct.simps
    2.88 -      using Cons.hyps Cons.prems by simp
    2.89 -  qed simp
    2.90 -qed simp
    2.91 -
    2.92 -lemma distinct_zipI2:
    2.93 -  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
    2.94 -proof (induct xs arbitrary: ys)
    2.95 -  case (Cons x xs)
    2.96 -  show ?case
    2.97 -  proof (cases ys)
    2.98 -    case (Cons y ys')
    2.99 -     have "(x, y) \<notin> set (zip xs ys')"
   2.100 -      using Cons.prems by (auto simp: set_zip)
   2.101 -    thus ?thesis
   2.102 -      unfolding Cons zip_Cons_Cons distinct.simps
   2.103 -      using Cons.hyps Cons.prems by simp
   2.104 -  qed simp
   2.105 -qed simp
   2.106 -
   2.107  
   2.108  subsubsection {* @{text list_all2} *}
   2.109  
   2.110 @@ -2868,6 +2859,30 @@
   2.111    "remdups (map f (remdups xs)) = remdups (map f xs)"
   2.112    by (induct xs) simp_all
   2.113  
   2.114 +lemma distinct_zipI1:
   2.115 +  assumes "distinct xs"
   2.116 +  shows "distinct (zip xs ys)"
   2.117 +proof (rule zip_obtain_same_length)
   2.118 +  fix xs' :: "'a list" and ys' :: "'b list" and n
   2.119 +  assume "length xs' = length ys'"
   2.120 +  assume "xs' = take n xs"
   2.121 +  with assms have "distinct xs'" by simp
   2.122 +  with `length xs' = length ys'` show "distinct (zip xs' ys')"
   2.123 +    by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
   2.124 +qed
   2.125 +
   2.126 +lemma distinct_zipI2:
   2.127 +  assumes "distinct ys"
   2.128 +  shows "distinct (zip xs ys)"
   2.129 +proof (rule zip_obtain_same_length)
   2.130 +  fix xs' :: "'b list" and ys' :: "'a list" and n
   2.131 +  assume "length xs' = length ys'"
   2.132 +  assume "ys' = take n ys"
   2.133 +  with assms have "distinct ys'" by simp
   2.134 +  with `length xs' = length ys'` show "distinct (zip xs' ys')"
   2.135 +    by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
   2.136 +qed
   2.137 +
   2.138  
   2.139  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
   2.140  
   2.141 @@ -3023,21 +3038,6 @@
   2.142    "List.insert x (remdups xs) = remdups (List.insert x xs)"
   2.143    by (simp add: List.insert_def)
   2.144  
   2.145 -lemma distinct_induct [consumes 1, case_names Nil insert]:
   2.146 -  assumes "distinct xs"
   2.147 -  assumes "P []"
   2.148 -  assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
   2.149 -    \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
   2.150 -  shows "P xs"
   2.151 -using `distinct xs` proof (induct xs)
   2.152 -  case Nil from `P []` show ?case .
   2.153 -next
   2.154 -  case (Cons x xs)
   2.155 -  then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
   2.156 -  with insert have "P (List.insert x xs)" .
   2.157 -  with `x \<notin> set xs` show ?case by simp
   2.158 -qed
   2.159 -
   2.160  
   2.161  subsubsection {* @{text remove1} *}
   2.162  
   2.163 @@ -3822,39 +3822,21 @@
   2.164  apply (auto simp: sorted_distinct_set_unique)
   2.165  done
   2.166  
   2.167 -lemma sorted_take:
   2.168 -  "sorted xs \<Longrightarrow> sorted (take n xs)"
   2.169 -proof (induct xs arbitrary: n rule: sorted.induct)
   2.170 -  case 1 show ?case by simp
   2.171 -next
   2.172 -  case 2 show ?case by (cases n) simp_all
   2.173 -next
   2.174 -  case (3 x y xs)
   2.175 -  then have "x \<le> y" by simp
   2.176 -  show ?case proof (cases n)
   2.177 -    case 0 then show ?thesis by simp
   2.178 -  next
   2.179 -    case (Suc m) 
   2.180 -    with 3 have "sorted (take m (y # xs))" by simp
   2.181 -    with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
   2.182 -  qed
   2.183 -qed
   2.184 -
   2.185 -lemma sorted_drop:
   2.186 -  "sorted xs \<Longrightarrow> sorted (drop n xs)"
   2.187 -proof (induct xs arbitrary: n rule: sorted.induct)
   2.188 -  case 1 show ?case by simp
   2.189 -next
   2.190 -  case 2 show ?case by (cases n) simp_all
   2.191 -next
   2.192 -  case 3 then show ?case by (cases n) simp_all
   2.193 +lemma
   2.194 +  assumes "sorted xs"
   2.195 +  shows sorted_take: "sorted (take n xs)"
   2.196 +  and sorted_drop: "sorted (drop n xs)"
   2.197 +proof -
   2.198 +  from assms have "sorted (take n xs @ drop n xs)" by simp
   2.199 +  then show "sorted (take n xs)" and "sorted (drop n xs)"
   2.200 +    unfolding sorted_append by simp_all
   2.201  qed
   2.202  
   2.203  lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
   2.204 -  unfolding dropWhile_eq_drop by (rule sorted_drop)
   2.205 +  by (auto dest: sorted_drop simp add: dropWhile_eq_drop)
   2.206  
   2.207  lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
   2.208 -  apply (subst takeWhile_eq_take) by (rule sorted_take)
   2.209 +  by (subst takeWhile_eq_take) (auto dest: sorted_take)
   2.210  
   2.211  lemma sorted_filter:
   2.212    "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
   2.213 @@ -4153,7 +4135,6 @@
   2.214    by (rule sorted_distinct_set_unique) simp_all
   2.215  
   2.216  
   2.217 -
   2.218  subsubsection {* @{text lists}: the list-forming operator over sets *}
   2.219  
   2.220  inductive_set