# HG changeset patch # User haftmann # Date 1286187778 -7200 # Node ID ecf97cf3d248be0cd5bac50f378fd38b938e75b7 # Parent 2f7b060d0c8db6343ce8597f52671e9ffa4d90b0 turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs diff -r 2f7b060d0c8d -r ecf97cf3d248 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Sat Oct 02 12:32:31 2010 +0200 +++ b/src/HOL/Library/Dlist.thy Mon Oct 04 12:22:58 2010 +0200 @@ -140,7 +140,7 @@ case (Abs_dlist xs) then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) from `distinct xs` have "P (Dlist xs)" - proof (induct xs rule: distinct_induct) + proof (induct xs) case Nil from empty show ?case by (simp add: empty_def) next case (insert x xs) diff -r 2f7b060d0c8d -r ecf97cf3d248 src/HOL/List.thy --- a/src/HOL/List.thy Sat Oct 02 12:32:31 2010 +0200 +++ b/src/HOL/List.thy Mon Oct 04 12:22:58 2010 +0200 @@ -157,16 +157,6 @@ upt_0: "[i..<0] = []" | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i.. bool" where - "distinct [] \ True" - | "distinct (x # xs) \ x \ set xs \ distinct xs" - -primrec - remdups :: "'a list \ 'a list" where - "remdups [] = []" - | "remdups (x # xs) = (if x \ set xs then remdups xs else x # remdups xs)" - definition insert :: "'a \ 'a list \ 'a list" where "insert x xs = (if x \ set xs then xs else x # xs)" @@ -184,6 +174,21 @@ "removeAll x [] = []" | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)" +inductive + distinct :: "'a list \ bool" where + Nil: "distinct []" + | insert: "x \ set xs \ distinct xs \ distinct (x # xs)" + +lemma distinct_simps [simp, code]: + "distinct [] \ True" + "distinct (x # xs) \ x \ set xs \ distinct xs" + by (auto intro: distinct.intros elim: distinct.cases) + +primrec + remdups :: "'a list \ 'a list" where + "remdups [] = []" + | "remdups (x # xs) = (if x \ set xs then remdups xs else x # remdups xs)" + primrec replicate :: "nat \ 'a \ 'a list" where replicate_0: "replicate 0 x = []" @@ -275,10 +280,26 @@ context linorder begin -fun sorted :: "'a list \ bool" where -"sorted [] \ True" | -"sorted [x] \ True" | -"sorted (x#y#zs) \ x <= y \ sorted (y#zs)" +inductive sorted :: "'a list \ bool" where + Nil [iff]: "sorted []" +| Cons: "\y\set xs. x \ y \ sorted xs \ sorted (x # xs)" + +lemma sorted_single [iff]: + "sorted [x]" + by (rule sorted.Cons) auto + +lemma sorted_many: + "x \ y \ sorted (y # zs) \ sorted (x # y # zs)" + by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto) + +lemma sorted_many_eq [simp, code]: + "sorted (x # y # zs) \ x \ y \ sorted (y # zs)" + by (auto intro: sorted_many elim: sorted.cases) + +lemma [code]: + "sorted [] \ True" + "sorted [x] \ True" + by simp_all primrec insort_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where "insort_key f x [] = [x]" | @@ -2118,36 +2139,6 @@ "length xs = length ys \ zip xs ys = zs \ map fst zs = xs \ map snd zs = ys" by (auto simp add: zip_map_fst_snd) -lemma distinct_zipI1: - "distinct xs \ distinct (zip xs ys)" -proof (induct xs arbitrary: ys) - case (Cons x xs) - show ?case - proof (cases ys) - case (Cons y ys') - have "(x, y) \ set (zip xs ys')" - using Cons.prems by (auto simp: set_zip) - thus ?thesis - unfolding Cons zip_Cons_Cons distinct.simps - using Cons.hyps Cons.prems by simp - qed simp -qed simp - -lemma distinct_zipI2: - "distinct xs \ distinct (zip xs ys)" -proof (induct xs arbitrary: ys) - case (Cons x xs) - show ?case - proof (cases ys) - case (Cons y ys') - have "(x, y) \ set (zip xs ys')" - using Cons.prems by (auto simp: set_zip) - thus ?thesis - unfolding Cons zip_Cons_Cons distinct.simps - using Cons.hyps Cons.prems by simp - qed simp -qed simp - subsubsection {* @{text list_all2} *} @@ -2868,6 +2859,30 @@ "remdups (map f (remdups xs)) = remdups (map f xs)" by (induct xs) simp_all +lemma distinct_zipI1: + assumes "distinct xs" + shows "distinct (zip xs ys)" +proof (rule zip_obtain_same_length) + fix xs' :: "'a list" and ys' :: "'b list" and n + assume "length xs' = length ys'" + assume "xs' = take n xs" + with assms have "distinct xs'" by simp + with `length xs' = length ys'` show "distinct (zip xs' ys')" + by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE) +qed + +lemma distinct_zipI2: + assumes "distinct ys" + shows "distinct (zip xs ys)" +proof (rule zip_obtain_same_length) + fix xs' :: "'b list" and ys' :: "'a list" and n + assume "length xs' = length ys'" + assume "ys' = take n ys" + with assms have "distinct ys'" by simp + with `length xs' = length ys'` show "distinct (zip xs' ys')" + by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE) +qed + subsubsection {* List summation: @{const listsum} and @{text"\"}*} @@ -3023,21 +3038,6 @@ "List.insert x (remdups xs) = remdups (List.insert x xs)" by (simp add: List.insert_def) -lemma distinct_induct [consumes 1, case_names Nil insert]: - assumes "distinct xs" - assumes "P []" - assumes insert: "\x xs. distinct xs \ x \ set xs - \ P xs \ P (List.insert x xs)" - shows "P xs" -using `distinct xs` proof (induct xs) - case Nil from `P []` show ?case . -next - case (Cons x xs) - then have "distinct xs" and "x \ set xs" and "P xs" by simp_all - with insert have "P (List.insert x xs)" . - with `x \ set xs` show ?case by simp -qed - subsubsection {* @{text remove1} *} @@ -3822,39 +3822,21 @@ apply (auto simp: sorted_distinct_set_unique) done -lemma sorted_take: - "sorted xs \ sorted (take n xs)" -proof (induct xs arbitrary: n rule: sorted.induct) - case 1 show ?case by simp -next - case 2 show ?case by (cases n) simp_all -next - case (3 x y xs) - then have "x \ y" by simp - show ?case proof (cases n) - case 0 then show ?thesis by simp - next - case (Suc m) - with 3 have "sorted (take m (y # xs))" by simp - with Suc `x \ y` show ?thesis by (cases m) simp_all - qed -qed - -lemma sorted_drop: - "sorted xs \ sorted (drop n xs)" -proof (induct xs arbitrary: n rule: sorted.induct) - case 1 show ?case by simp -next - case 2 show ?case by (cases n) simp_all -next - case 3 then show ?case by (cases n) simp_all +lemma + assumes "sorted xs" + shows sorted_take: "sorted (take n xs)" + and sorted_drop: "sorted (drop n xs)" +proof - + from assms have "sorted (take n xs @ drop n xs)" by simp + then show "sorted (take n xs)" and "sorted (drop n xs)" + unfolding sorted_append by simp_all qed lemma sorted_dropWhile: "sorted xs \ sorted (dropWhile P xs)" - unfolding dropWhile_eq_drop by (rule sorted_drop) + by (auto dest: sorted_drop simp add: dropWhile_eq_drop) lemma sorted_takeWhile: "sorted xs \ sorted (takeWhile P xs)" - apply (subst takeWhile_eq_take) by (rule sorted_take) + by (subst takeWhile_eq_take) (auto dest: sorted_take) lemma sorted_filter: "sorted (map f xs) \ sorted (map f (filter P xs))" @@ -4153,7 +4135,6 @@ by (rule sorted_distinct_set_unique) simp_all - subsubsection {* @{text lists}: the list-forming operator over sets *} inductive_set