[isabelle-dev] Sketch for generic interval notation [_..<_] / [_.._]
Florian Haftmann
florian at haftmann-online.de
Sun Mar 13 11:30:37 CET 2016
Hi all,
the attached patches (based on f26dc26f2161) sketch how a generic
interval [_..<_] / [_.._] could look like in List.thy.
Key points:
* The required logical properties are obtained by a specialization of
linordered_semidom with
a <= b <--> (EX n. b = a + of_nat n)"
This avoids introducing yet another auxiliary operation like succ etc.
I am still in search for a better name than pointed_linordered_semidom,
though.
* nat and int are instances of pointed_linordered_semidom.
* "finite {a..<b}" is easily proven then.
* The interval operation itself is bootstrapped using
"sorted_list_of_set {a..<b}"
* Fundamental properties are easily proven then.
This is not supposed to be pushed at the moment, but I want to encourage
feedback.
An aside: in List.thy, in the beginning there is a traditional table
depicting examples for the list operations. However only operations
specified *before* that table can be listed there; in large parts
List.thy follows the archaic tradition to specify everything in the
beginning and derive properties afterwards, but for a couple of
operations (including sorted_list_of_set) this is not done. To avoid a
massive restructuring (as had to be done for this experimental patch)
IMHO it would be better to move those examples to the »What's in Main«
document, where they would also gain more attention.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp
-------------- next part --------------
# HG changeset patch
# Parent 2743f729d4e2b2805876fc18b358e23a1db4a96e
put interval material after sorted_list_of_set
diff -r 2743f729d4e2 src/HOL/List.thy
--- a/src/HOL/List.thy Sat Mar 12 08:48:57 2016 +0100
+++ b/src/HOL/List.thy Sat Mar 12 09:10:13 2016 +0100
@@ -161,10 +161,6 @@
"product_lists [] = [[]]" |
"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)"
-primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
-upt_0: "[i..<0] = []" |
-upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
-
definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insert x xs = (if x \<in> set xs then xs else x # xs)"
@@ -232,9 +228,6 @@
abbreviation length :: "'a list \<Rightarrow> nat" where
"length \<equiv> size"
-definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where
-enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs"
-
primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
"rotate1 [] = []" |
"rotate1 (x # xs) = xs @ [x]"
@@ -242,13 +235,6 @@
definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"rotate n = rotate1 ^^ n"
-definition sublist :: "'a list => nat set => 'a list" where
-"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
-
-primrec sublists :: "'a list \<Rightarrow> 'a list list" where
-"sublists [] = [[]]" |
-"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
-
primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
"n_lists 0 xs = [[]]" |
"n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
@@ -280,7 +266,6 @@
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
-@{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\
@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
@@ -306,13 +291,10 @@
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
-@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
-@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
@{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\
@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
-@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}
\end{tabular}}
\caption{Characteristic examples}
\label{fig:Characteristic}
@@ -1290,9 +1272,6 @@
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
by (induct xs) auto
-lemma set_upt [simp]: "set[i..<j] = {i..<j}"
-by (induct j) auto
-
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
proof (induct xs)
@@ -2977,86 +2956,6 @@
by (simp add: fold_append_concat_rev foldr_conv_fold)
-subsubsection \<open>@{const upt}\<close>
-
-lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
-\<comment> \<open>simp does not terminate!\<close>
-by (induct j) auto
-
-lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
-
-lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
-by (subst upt_rec) simp
-
-lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
-by(induct j)simp_all
-
-lemma upt_eq_Cons_conv:
- "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
-apply(induct j arbitrary: x xs)
- apply simp
-apply(clarsimp simp add: append_eq_Cons_conv)
-apply arith
-done
-
-lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
-\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
-by simp
-
-lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
-by (simp add: upt_rec)
-
-lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close>
- "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
-proof (cases "m < q")
- case False then show ?thesis by simp
-next
- case True then show ?thesis by (simp add: upt_conv_Cons)
-qed
-
-lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
-\<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
-by (induct k) auto
-
-lemma length_upt [simp]: "length [i..<j] = j - i"
-by (induct j) (auto simp add: Suc_diff_le)
-
-lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
-by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
-
-lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
-by(simp add:upt_conv_Cons)
-
-lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
-by(cases j)(auto simp: upt_Suc_append)
-
-lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
-apply (induct m arbitrary: i, simp)
-apply (subst upt_rec)
-apply (rule sym)
-apply (subst upt_rec)
-apply (simp del: upt.simps)
-done
-
-lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
-by(induct j) auto
-
-lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
-by (induct n) auto
-
-lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
-by (induct m) simp_all
-
-lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
-apply (induct n m arbitrary: i rule: diff_induct)
- prefer 3 apply (subst map_Suc_upt[symmetric])
- apply (auto simp add: less_diff_conv)
-done
-
-lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
-
-
lemma nth_take_lemma:
"k <= length xs ==> k <= length ys ==>
(!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
@@ -3076,9 +2975,6 @@
"[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
-lemma map_nth:
- "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
-by (rule nth_equalityI, auto)
lemma list_all2_antisym:
"\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk>
@@ -3118,57 +3014,6 @@
by (simp add: nth_Cons')
-subsubsection \<open>\<open>upto\<close>: interval-list on @{typ int}\<close>
-
-function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
- "upto i j = (if i \<le> j then i # [i+1..j] else [])"
-by auto
-termination
-by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
-
-declare upto.simps[simp del]
-
-lemmas upto_rec_numeral [simp] =
- upto.simps[of "numeral m" "numeral n"]
- upto.simps[of "numeral m" "- numeral n"]
- upto.simps[of "- numeral m" "numeral n"]
- upto.simps[of "- numeral m" "- numeral n"] for m n
-
-lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
-by(simp add: upto.simps)
-
-lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
-by(simp add: upto.simps)
-
-lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..j] = [i..j - 1]@[j]"
-proof(induct "nat(j-i)" arbitrary: i j)
- case 0 thus ?case by(simp add: upto.simps)
-next
- case (Suc n)
- hence "n = nat (j - (i + 1))" "i < j" by linarith+
- from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp
-qed
-
-lemma set_upto[simp]: "set[i..j] = {i..j}"
-proof(induct i j rule:upto.induct)
- case (1 i j)
- from this show ?case
- unfolding upto.simps[of i j] by auto
-qed
-
-text\<open>Tail recursive version for code generation:\<close>
-
-definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
- "upto_aux i j js = [i..j] @ js"
-
-lemma upto_aux_rec [code]:
- "upto_aux i j js = (if j<i then js else upto_aux i (j - 1) (j#js))"
-by (simp add: upto_aux_def upto_rec2)
-
-lemma upto_code[code]: "[i..j] = upto_aux i j []"
-by(simp add: upto_aux_def)
-
-
subsubsection \<open>@{const distinct} and @{const remdups} and @{const remdups_adj}\<close>
lemma distinct_tl: "distinct xs \<Longrightarrow> distinct (tl xs)"
@@ -3228,15 +3073,6 @@
lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
by (induct xs) auto
-lemma distinct_upt[simp]: "distinct[i..<j]"
-by (induct j) auto
-
-lemma distinct_upto[simp]: "distinct[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
-
lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
apply(induct xs arbitrary: i)
apply simp
@@ -3676,17 +3512,6 @@
"remdups_adj (replicate n x) = (if n = 0 then [] else [x])"
by (induction n) (auto simp: remdups_adj_Cons)
-lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]"
-proof (cases "m \<le> n")
- case False then show ?thesis by simp
-next
- case True then obtain q where "n = m + q"
- by (auto simp add: le_iff_add)
- moreover have "remdups [m..<m + q] = [m..<m + q]"
- by (induct q) simp_all
- ultimately show ?thesis by simp
-qed
-
subsubsection \<open>@{const insert}\<close>
@@ -4011,10 +3836,6 @@
"replicate i x @ [x] = x # replicate i x"
by (induct i) simp_all
-lemma map_replicate_trivial:
- "map (\<lambda>i. x) [0..<i] = replicate i x"
- by (induct i) (simp_all add: replicate_append_same)
-
lemma concat_replicate_trivial[simp]:
"concat (replicate i []) = []"
by (induct i) (auto simp add: map_replicate_const)
@@ -4117,73 +3938,6 @@
by (subst foldr_fold [symmetric]) simp_all
-subsubsection \<open>@{const enumerate}\<close>
-
-lemma enumerate_simps [simp, code]:
- "enumerate n [] = []"
- "enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
- apply (auto simp add: enumerate_eq_zip not_le)
- apply (cases "n < n + length xs")
- apply (auto simp add: upt_conv_Cons)
- done
-
-lemma length_enumerate [simp]:
- "length (enumerate n xs) = length xs"
- by (simp add: enumerate_eq_zip)
-
-lemma map_fst_enumerate [simp]:
- "map fst (enumerate n xs) = [n..<n + length xs]"
- by (simp add: enumerate_eq_zip)
-
-lemma map_snd_enumerate [simp]:
- "map snd (enumerate n xs) = xs"
- by (simp add: enumerate_eq_zip)
-
-lemma in_set_enumerate_eq:
- "p \<in> set (enumerate n xs) \<longleftrightarrow> n \<le> fst p \<and> fst p < length xs + n \<and> nth xs (fst p - n) = snd p"
-proof -
- { fix m
- assume "n \<le> m"
- moreover assume "m < length xs + n"
- ultimately have "[n..<n + length xs] ! (m - n) = m \<and>
- xs ! (m - n) = xs ! (m - n) \<and> m - n < length xs" by auto
- then have "\<exists>q. [n..<n + length xs] ! q = m \<and>
- xs ! q = xs ! (m - n) \<and> q < length xs" ..
- } then show ?thesis by (cases p) (auto simp add: enumerate_eq_zip in_set_zip)
-qed
-
-lemma nth_enumerate_eq:
- assumes "m < length xs"
- shows "enumerate n xs ! m = (n + m, xs ! m)"
- using assms by (simp add: enumerate_eq_zip)
-
-lemma enumerate_replicate_eq:
- "enumerate n (replicate m a) = map (\<lambda>q. (q, a)) [n..<n + m]"
- by (rule pair_list_eqI)
- (simp_all add: enumerate_eq_zip comp_def map_replicate_const)
-
-lemma enumerate_Suc_eq:
- "enumerate (Suc n) xs = map (apfst Suc) (enumerate n xs)"
- by (rule pair_list_eqI)
- (simp_all add: not_le, simp del: map_map [simp del] add: map_Suc_upt map_map [symmetric])
-
-lemma distinct_enumerate [simp]:
- "distinct (enumerate n xs)"
- by (simp add: enumerate_eq_zip distinct_zipI1)
-
-lemma enumerate_append_eq:
- "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
- unfolding enumerate_eq_zip apply auto
- apply (subst zip_append [symmetric]) apply simp
- apply (subst upt_add_eq_append [symmetric])
- apply (simp_all add: ac_simps)
- done
-
-lemma enumerate_map_upt:
- "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
- by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
-
-
subsubsection \<open>@{const rotate1} and @{const rotate}\<close>
lemma rotate0[simp]: "rotate 0 = id"
@@ -4278,140 +4032,6 @@
using mod_less_divisor[of "length xs" n] by arith
-subsubsection \<open>@{const sublist} --- a generalization of @{const nth} to sets\<close>
-
-lemma sublist_empty [simp]: "sublist xs {} = []"
-by (auto simp add: sublist_def)
-
-lemma sublist_nil [simp]: "sublist [] A = []"
-by (auto simp add: sublist_def)
-
-lemma length_sublist:
- "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
-by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
-
-lemma sublist_shift_lemma_Suc:
- "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
- map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
-apply(induct xs arbitrary: "is")
- apply simp
-apply (case_tac "is")
- apply simp
-apply simp
-done
-
-lemma sublist_shift_lemma:
- "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
- map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
-by (induct xs rule: rev_induct) (simp_all add: add.commute)
-
-lemma sublist_append:
- "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
-apply (unfold sublist_def)
-apply (induct l' rule: rev_induct, simp)
-apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
-apply (simp add: add.commute)
-done
-
-lemma sublist_Cons:
-"sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
-apply (induct l rule: rev_induct)
- apply (simp add: sublist_def)
-apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
-done
-
-lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
-apply(induct xs arbitrary: I)
-apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
-done
-
-lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
-by(auto simp add:set_sublist)
-
-lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
-by(auto simp add:set_sublist)
-
-lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
-by(auto simp add:set_sublist)
-
-lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
-by (simp add: sublist_Cons)
-
-
-lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
-apply(induct xs arbitrary: I)
- apply simp
-apply(auto simp add:sublist_Cons)
-done
-
-
-lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
-apply (induct l rule: rev_induct, simp)
-apply (simp split: nat_diff_split add: sublist_append)
-done
-
-lemma filter_in_sublist:
- "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
-proof (induct xs arbitrary: s)
- case Nil thus ?case by simp
-next
- case (Cons a xs)
- then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
- with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
-qed
-
-
-subsubsection \<open>@{const sublists} and @{const List.n_lists}\<close>
-
-lemma length_sublists:
- "length (sublists xs) = 2 ^ length xs"
- by (induct xs) (simp_all add: Let_def)
-
-lemma sublists_powset:
- "set ` set (sublists xs) = Pow (set xs)"
-proof -
- have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
- by (auto simp add: image_def)
- have "set (map set (sublists xs)) = Pow (set xs)"
- by (induct xs)
- (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
- then show ?thesis by simp
-qed
-
-lemma distinct_set_sublists:
- assumes "distinct xs"
- shows "distinct (map set (sublists xs))"
-proof (rule card_distinct)
- have "finite (set xs)" by rule
- then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
- with assms distinct_card [of xs]
- have "card (Pow (set xs)) = 2 ^ length xs" by simp
- then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
- by (simp add: sublists_powset length_sublists)
-qed
-
-lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
- by (induct n) simp_all
-
-lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
- by (induct n arbitrary: ys) auto
-
-lemma set_n_lists: "set (List.n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
-proof (rule set_eqI)
- fix ys :: "'a list"
- show "ys \<in> set (List.n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
- proof -
- have "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
- by (induct n arbitrary: ys) auto
- moreover have "\<And>x. ys \<in> set (List.n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
- by (induct n arbitrary: ys) auto
- moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (List.n_lists (length ys) xs)"
- by (induct ys) auto
- ultimately show ?thesis by auto
- qed
-qed
-
-
subsubsection \<open>@{const splice}\<close>
lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
@@ -4984,19 +4604,6 @@
end
-lemma sorted_upt[simp]: "sorted[i..<j]"
-by (induct j) (simp_all add:sorted_append)
-
-lemma sort_upt [simp]:
- "sort [m..<n] = [m..<n]"
- by (rule sorted_sort_id) simp
-
-lemma sorted_upto[simp]: "sorted[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp add:sorted_Cons)
-done
-
lemma sorted_find_Min:
assumes "sorted xs"
assumes "\<exists>x \<in> set xs. P x"
@@ -5013,10 +4620,6 @@
qed
qed
-lemma sorted_enumerate [simp]:
- "sorted (map fst (enumerate n xs))"
- by (simp add: enumerate_eq_zip)
-
subsubsection \<open>@{const transpose} on sorted lists\<close>
@@ -5148,6 +4751,190 @@
(simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
qed
+
+subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
+
+text\<open>This function maps (finite) linearly ordered sets to sorted
+lists. Warning: in most cases it is not a good idea to convert from
+sets to lists but one should convert in the other direction (via
+@{const set}).\<close>
+
+context linorder
+begin
+
+definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
+ "sorted_list_of_set = folding.F insort []"
+
+sublocale sorted_list_of_set: folding insort Nil
+rewrites
+ "folding.F insort [] = sorted_list_of_set"
+proof -
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
+ show "folding insort" by standard (fact comp_fun_commute)
+ show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
+qed
+
+lemma sorted_list_of_set_empty:
+ "sorted_list_of_set {} = []"
+ by (fact sorted_list_of_set.empty)
+
+lemma sorted_list_of_set_insert [simp]:
+ "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
+ by (fact sorted_list_of_set.insert_remove)
+
+lemma sorted_list_of_set_eq_Nil_iff [simp]:
+ "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
+ by (auto simp: sorted_list_of_set.remove)
+
+lemma sorted_list_of_set [simp]:
+ "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
+ \<and> distinct (sorted_list_of_set A)"
+ by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
+
+lemma distinct_sorted_list_of_set:
+ "distinct (sorted_list_of_set A)"
+ using sorted_list_of_set by (cases "finite A") auto
+
+lemma sorted_list_of_set_sort_remdups [code]:
+ "sorted_list_of_set (set xs) = sort (remdups xs)"
+proof -
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
+ show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)
+qed
+
+lemma sorted_list_of_set_remove:
+ assumes "finite A"
+ shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
+proof (cases "x \<in> A")
+ case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
+ with False show ?thesis by (simp add: remove1_idem)
+next
+ case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
+ with assms show ?thesis by simp
+qed
+
+end
+
+
+subsubsection \<open>@{text upt}\<close>
+
+primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
+upt_0: "[i..<0] = []" |
+upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
+
+lemma set_upt [simp]: "set[i..<j] = {i..<j}"
+by (induct j) auto
+
+lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
+\<comment> \<open>simp does not terminate!\<close>
+by (induct j) auto
+
+lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
+
+lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
+by (subst upt_rec) simp
+
+lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
+by(induct j)simp_all
+
+lemma upt_eq_Cons_conv:
+ "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
+apply(induct j arbitrary: x xs)
+ apply simp
+apply(clarsimp simp add: append_eq_Cons_conv)
+apply arith
+done
+
+lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
+\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
+by simp
+
+lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
+by (simp add: upt_rec)
+
+lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close>
+ "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
+proof (cases "m < q")
+ case False then show ?thesis by simp
+next
+ case True then show ?thesis by (simp add: upt_conv_Cons)
+qed
+
+lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
+\<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
+by (induct k) auto
+
+lemma length_upt [simp]: "length [i..<j] = j - i"
+by (induct j) (auto simp add: Suc_diff_le)
+
+lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
+by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
+
+lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
+by(simp add:upt_conv_Cons)
+
+lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
+by(cases j)(auto simp: upt_Suc_append)
+
+lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
+apply (induct m arbitrary: i, simp)
+apply (subst upt_rec)
+apply (rule sym)
+apply (subst upt_rec)
+apply (simp del: upt.simps)
+done
+
+lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
+by(induct j) auto
+
+lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
+by (induct n) auto
+
+lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
+by (induct m) simp_all
+
+lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
+apply (induct n m arbitrary: i rule: diff_induct)
+ prefer 3 apply (subst map_Suc_upt[symmetric])
+ apply (auto simp add: less_diff_conv)
+done
+
+lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
+by (induct n) simp_all
+
+lemma map_nth:
+ "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
+by (rule nth_equalityI, auto)
+
+lemma distinct_upt[simp]: "distinct[i..<j]"
+by (induct j) auto
+
+lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]"
+proof (cases "m \<le> n")
+ case False then show ?thesis by simp
+next
+ case True then obtain q where "n = m + q"
+ by (auto simp add: le_iff_add)
+ moreover have "remdups [m..<m + q] = [m..<m + q]"
+ by (induct q) simp_all
+ ultimately show ?thesis by simp
+qed
+
+lemma sorted_upt[simp]: "sorted[i..<j]"
+by (induct j) (simp_all add:sorted_append)
+
+lemma sort_upt [simp]:
+ "sort [m..<n] = [m..<n]"
+ by (rule sorted_sort_id) simp
+
+lemma sorted_list_of_set_range [simp]:
+ "sorted_list_of_set {m..<n} = [m..<n]"
+ by (rule sorted_distinct_set_unique) simp_all
+
+lemma map_replicate_trivial:
+ "map (\<lambda>i. x) [0..<i] = replicate i x"
+ by (induct i) (simp_all add: replicate_append_same)
+
theorem transpose_rectangle:
assumes "xs = [] \<Longrightarrow> n = 0"
assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"
@@ -5167,79 +4954,282 @@
qed
-subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
-
-text\<open>This function maps (finite) linearly ordered sets to sorted
-lists. Warning: in most cases it is not a good idea to convert from
-sets to lists but one should convert in the other direction (via
-@{const set}).\<close>
-
-subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
-
-text\<open>This function maps (finite) linearly ordered sets to sorted
-lists. Warning: in most cases it is not a good idea to convert from
-sets to lists but one should convert in the other direction (via
-@{const set}).\<close>
-
-context linorder
-begin
-
-definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- "sorted_list_of_set = folding.F insort []"
-
-sublocale sorted_list_of_set: folding insort Nil
-rewrites
- "folding.F insort [] = sorted_list_of_set"
+subsubsection \<open>\<open>upto\<close>: interval-list on @{typ int}\<close>
+
+function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
+ "upto i j = (if i \<le> j then i # [i+1..j] else [])"
+by auto
+termination
+by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
+
+declare upto.simps[simp del]
+
+lemmas upto_rec_numeral [simp] =
+ upto.simps[of "numeral m" "numeral n"]
+ upto.simps[of "numeral m" "- numeral n"]
+ upto.simps[of "- numeral m" "numeral n"]
+ upto.simps[of "- numeral m" "- numeral n"] for m n
+
+lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
+by(simp add: upto.simps)
+
+lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
+by(simp add: upto.simps)
+
+lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..j] = [i..j - 1]@[j]"
+proof(induct "nat(j-i)" arbitrary: i j)
+ case 0 thus ?case by(simp add: upto.simps)
+next
+ case (Suc n)
+ hence "n = nat (j - (i + 1))" "i < j" by linarith+
+ from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp
+qed
+
+lemma set_upto[simp]: "set[i..j] = {i..j}"
+proof(induct i j rule:upto.induct)
+ case (1 i j)
+ from this show ?case
+ unfolding upto.simps[of i j] by auto
+qed
+
+lemma distinct_upto[simp]: "distinct[i..j]"
+apply(induct i j rule:upto.induct)
+apply(subst upto.simps)
+apply(simp)
+done
+
+text\<open>Tail recursive version for code generation:\<close>
+
+definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+ "upto_aux i j js = [i..j] @ js"
+
+lemma upto_aux_rec [code]:
+ "upto_aux i j js = (if j<i then js else upto_aux i (j - 1) (j#js))"
+by (simp add: upto_aux_def upto_rec2)
+
+lemma upto_code[code]: "[i..j] = upto_aux i j []"
+by(simp add: upto_aux_def)
+
+lemma sorted_upto[simp]: "sorted[i..j]"
+apply(induct i j rule:upto.induct)
+apply(subst upto.simps)
+apply(simp add:sorted_Cons)
+done
+
+
+subsubsection \<open>@{text enumerate}\<close>
+
+definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where
+enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs"
+
+lemma enumerate_simps [simp, code]:
+ "enumerate n [] = []"
+ "enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
+ apply (auto simp add: enumerate_eq_zip not_le)
+ apply (cases "n < n + length xs")
+ apply (auto simp add: upt_conv_Cons)
+ done
+
+lemma length_enumerate [simp]:
+ "length (enumerate n xs) = length xs"
+ by (simp add: enumerate_eq_zip)
+
+lemma map_fst_enumerate [simp]:
+ "map fst (enumerate n xs) = [n..<n + length xs]"
+ by (simp add: enumerate_eq_zip)
+
+lemma map_snd_enumerate [simp]:
+ "map snd (enumerate n xs) = xs"
+ by (simp add: enumerate_eq_zip)
+
+lemma in_set_enumerate_eq:
+ "p \<in> set (enumerate n xs) \<longleftrightarrow> n \<le> fst p \<and> fst p < length xs + n \<and> nth xs (fst p - n) = snd p"
proof -
- interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show "folding insort" by standard (fact comp_fun_commute)
- show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
+ { fix m
+ assume "n \<le> m"
+ moreover assume "m < length xs + n"
+ ultimately have "[n..<n + length xs] ! (m - n) = m \<and>
+ xs ! (m - n) = xs ! (m - n) \<and> m - n < length xs" by auto
+ then have "\<exists>q. [n..<n + length xs] ! q = m \<and>
+ xs ! q = xs ! (m - n) \<and> q < length xs" ..
+ } then show ?thesis by (cases p) (auto simp add: enumerate_eq_zip in_set_zip)
qed
-lemma sorted_list_of_set_empty:
- "sorted_list_of_set {} = []"
- by (fact sorted_list_of_set.empty)
-
-lemma sorted_list_of_set_insert [simp]:
- "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
- by (fact sorted_list_of_set.insert_remove)
-
-lemma sorted_list_of_set_eq_Nil_iff [simp]:
- "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
- by (auto simp: sorted_list_of_set.remove)
-
-lemma sorted_list_of_set [simp]:
- "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
- \<and> distinct (sorted_list_of_set A)"
- by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
-
-lemma distinct_sorted_list_of_set:
- "distinct (sorted_list_of_set A)"
- using sorted_list_of_set by (cases "finite A") auto
-
-lemma sorted_list_of_set_sort_remdups [code]:
- "sorted_list_of_set (set xs) = sort (remdups xs)"
+lemma nth_enumerate_eq:
+ assumes "m < length xs"
+ shows "enumerate n xs ! m = (n + m, xs ! m)"
+ using assms by (simp add: enumerate_eq_zip)
+
+lemma enumerate_replicate_eq:
+ "enumerate n (replicate m a) = map (\<lambda>q. (q, a)) [n..<n + m]"
+ by (rule pair_list_eqI)
+ (simp_all add: enumerate_eq_zip comp_def map_replicate_const)
+
+lemma enumerate_Suc_eq:
+ "enumerate (Suc n) xs = map (apfst Suc) (enumerate n xs)"
+ by (rule pair_list_eqI)
+ (simp_all add: not_le, simp del: map_map [simp del] add: map_Suc_upt map_map [symmetric])
+
+lemma distinct_enumerate [simp]:
+ "distinct (enumerate n xs)"
+ by (simp add: enumerate_eq_zip distinct_zipI1)
+
+lemma enumerate_append_eq:
+ "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
+ unfolding enumerate_eq_zip apply auto
+ apply (subst zip_append [symmetric]) apply simp
+ apply (subst upt_add_eq_append [symmetric])
+ apply (simp_all add: ac_simps)
+ done
+
+lemma enumerate_map_upt:
+ "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
+ by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
+
+lemma sorted_enumerate [simp]:
+ "sorted (map fst (enumerate n xs))"
+ by (simp add: enumerate_eq_zip)
+
+
+subsubsection \<open>@{text sublist} --- a generalization of @{const nth} to sets\<close>
+
+definition sublist :: "'a list => nat set => 'a list" where
+"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
+
+primrec sublists :: "'a list \<Rightarrow> 'a list list" where
+"sublists [] = [[]]" |
+"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
+
+lemma sublist_empty [simp]: "sublist xs {} = []"
+by (auto simp add: sublist_def)
+
+lemma sublist_nil [simp]: "sublist [] A = []"
+by (auto simp add: sublist_def)
+
+lemma length_sublist:
+ "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
+by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
+
+lemma sublist_shift_lemma_Suc:
+ "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
+ map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
+apply(induct xs arbitrary: "is")
+ apply simp
+apply (case_tac "is")
+ apply simp
+apply simp
+done
+
+lemma sublist_shift_lemma:
+ "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
+ map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
+by (induct xs rule: rev_induct) (simp_all add: add.commute)
+
+lemma sublist_append:
+ "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
+apply (unfold sublist_def)
+apply (induct l' rule: rev_induct, simp)
+apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
+apply (simp add: add.commute)
+done
+
+lemma sublist_Cons:
+"sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
+apply (induct l rule: rev_induct)
+ apply (simp add: sublist_def)
+apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
+done
+
+lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
+apply(induct xs arbitrary: I)
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
+done
+
+lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
+by(auto simp add:set_sublist)
+
+lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
+by(auto simp add:set_sublist)
+
+lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
+by(auto simp add:set_sublist)
+
+lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
+by (simp add: sublist_Cons)
+
+
+lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
+apply(induct xs arbitrary: I)
+ apply simp
+apply(auto simp add:sublist_Cons)
+done
+
+
+lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
+apply (induct l rule: rev_induct, simp)
+apply (simp split: nat_diff_split add: sublist_append)
+done
+
+lemma filter_in_sublist:
+ "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
+proof (induct xs arbitrary: s)
+ case Nil thus ?case by simp
+next
+ case (Cons a xs)
+ then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
+ with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
+qed
+
+
+subsubsection \<open>@{const sublists} and @{const List.n_lists}\<close>
+
+lemma length_sublists:
+ "length (sublists xs) = 2 ^ length xs"
+ by (induct xs) (simp_all add: Let_def)
+
+lemma sublists_powset:
+ "set ` set (sublists xs) = Pow (set xs)"
proof -
- interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)
+ have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
+ by (auto simp add: image_def)
+ have "set (map set (sublists xs)) = Pow (set xs)"
+ by (induct xs)
+ (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
+ then show ?thesis by simp
qed
-lemma sorted_list_of_set_remove:
- assumes "finite A"
- shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
-proof (cases "x \<in> A")
- case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
- with False show ?thesis by (simp add: remove1_idem)
-next
- case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
- with assms show ?thesis by simp
+lemma distinct_set_sublists:
+ assumes "distinct xs"
+ shows "distinct (map set (sublists xs))"
+proof (rule card_distinct)
+ have "finite (set xs)" by rule
+ then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
+ with assms distinct_card [of xs]
+ have "card (Pow (set xs)) = 2 ^ length xs" by simp
+ then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
+ by (simp add: sublists_powset length_sublists)
qed
-end
-
-lemma sorted_list_of_set_range [simp]:
- "sorted_list_of_set {m..<n} = [m..<n]"
- by (rule sorted_distinct_set_unique) simp_all
+lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
+ by (induct n) simp_all
+
+lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
+ by (induct n arbitrary: ys) auto
+
+lemma set_n_lists: "set (List.n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+proof (rule set_eqI)
+ fix ys :: "'a list"
+ show "ys \<in> set (List.n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+ proof -
+ have "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
+ by (induct n arbitrary: ys) auto
+ moreover have "\<And>x. ys \<in> set (List.n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
+ by (induct n arbitrary: ys) auto
+ moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (List.n_lists (length ys) xs)"
+ by (induct ys) auto
+ ultimately show ?thesis by auto
+ qed
+qed
subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>
-------------- next part --------------
# HG changeset patch
# Parent f3ef1ecc3fbc275c5ce86ab695c4db9cbe414be1
type class for generic list intervals
diff -r f3ef1ecc3fbc src/HOL/List.thy
--- a/src/HOL/List.thy Sat Mar 12 16:26:37 2016 +0100
+++ b/src/HOL/List.thy Sat Mar 12 19:56:50 2016 +0100
@@ -4816,34 +4816,294 @@
end
-subsubsection \<open>@{text upt}\<close>
-
-primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
-upt_0: "[i..<0] = []" |
-upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
-
-lemma set_upt [simp]: "set[i..<j] = {i..<j}"
-by (induct j) auto
-
-lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
+subsubsection \<open>Intervals: @{text upt} and @{text upto}\<close>
+
+class pointed_linordered_semidom = linordered_semidom +
+ assumes less_eq_imp_ex_add: "a \<le> b \<Longrightarrow> (\<exists>n. b = a + of_nat n)"
+begin
+
+lemma less_eq_iff_add:
+ "a \<le> b \<longleftrightarrow> (\<exists>n. b = a + of_nat n)" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P with less_eq_imp_ex_add show ?Q .
+next
+ assume ?Q then obtain n
+ where "b = a + of_nat n" ..
+ then show ?P by simp
+qed
+
+lemma less_iff_add:
+ "a < b \<longleftrightarrow> (\<exists>n>0. b = a + of_nat n)" (is "?P \<longleftrightarrow> ?Q")
+ unfolding less_le less_eq_iff_add by auto
+
+lemma less_eqI:
+ assumes "b = a + of_nat n"
+ shows "a \<le> b"
+ using assms by (auto simp add: less_eq_iff_add)
+
+lemma less_eqE:
+ assumes "a \<le> b"
+ obtains n where "b = a + of_nat n"
+ using assms by (auto simp add: less_eq_iff_add)
+
+lemma lessI:
+ assumes "b = a + of_nat n" and "n > 0"
+ shows "a < b"
+ using assms by (auto simp add: less_iff_add)
+
+lemma lessE:
+ assumes "a < b"
+ obtains n where "b = a + of_nat n" and "n > 0"
+ using assms by (auto simp add: less_iff_add)
+
+lemma less_eq_succ_iff:
+ "a + 1 \<le> b \<longleftrightarrow> a < b" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q
+ then obtain n where "b = a + of_nat n" and "n > 0"
+ by (auto elim!: lessE)
+ moreover have "1 \<le> of_nat n \<longleftrightarrow> 1 \<le> n"
+ by (cases n) simp_all
+ ultimately show ?P by (simp add: ac_simps)
+next
+ assume ?P
+ then obtain n where "b = a + 1 + of_nat n"
+ by (auto elim!: less_eqE)
+ then show ?Q by (simp add: ac_simps add_pos_nonneg)
+qed
+
+lemma less_succ_iff:
+ "a < b + 1 \<longleftrightarrow> a \<le> b" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q
+ then obtain n where "b = a + of_nat n"
+ by (auto elim!: less_eqE)
+ then show ?P by (simp add: ac_simps add_pos_nonneg)
+next
+ assume ?P
+ then obtain n where "b + 1 = a + of_nat n" and "n > 0"
+ by (auto elim!: lessE)
+ then have "b + 1 - 1 = a + of_nat n - 1"
+ by simp
+ then have "b = a + of_nat n - 1"
+ by simp
+ with \<open>n > 0\<close> have "b = a + (of_nat n - 1)"
+ by (cases n) (simp_all add: add.left_commute [of _ 1])
+ with \<open>n > 0\<close> show ?Q by (cases n) simp_all
+qed
+
+lemma interval_inc_interval_inc:
+ "{a..<b + 1} = {a..b}"
+ by (auto simp add: less_succ_iff)
+
+lemma finite_interval:
+ "finite {a..<b}"
+proof (cases "b \<ge> a")
+ case False then have "b < a" by (simp add: not_le)
+ then show ?thesis by simp
+next
+ case True with less_eq_iff_add
+ obtain n where "b = a + of_nat n" by auto
+ moreover have "finite {a..<a + of_nat n}"
+ proof (induct n)
+ case 0 then show ?case by simp
+ next
+ case (Suc n)
+ then have "finite (insert (a + of_nat n) {a..<a + of_nat n})"
+ by simp
+ also have "insert (a + of_nat n) {a..<a + of_nat n} = {a..<a + of_nat (Suc n)}"
+ (is "?A = ?B")
+ proof (rule set_eqI)
+ fix b
+ have "b < a + of_nat n \<Longrightarrow> b < (a + of_nat n) + 1"
+ by (drule add_strict_mono [of _ _ 0 1]) simp_all
+ then show "b \<in> ?A \<longleftrightarrow> b \<in> ?B"
+ using less_succ_iff [of b "a + of_nat n"]
+ by (auto simp add: ac_simps)
+ qed
+ finally show ?case by simp
+ qed
+ ultimately show ?thesis by simp
+qed
+
+lemma finite_interval_inc:
+ "finite {a..b}"
+ by (simp add: finite_interval interval_inc_interval_inc [symmetric])
+
+definition upt :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_..</_])")
+where
+ "[a..<b] = sorted_list_of_set {a..<b}"
+
+abbreviation upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])")
+where
+ "[a..b] \<equiv> [a..<b + 1]"
+
+lemma upt_induct [case_names less init step]:
+ assumes less: "b < a \<Longrightarrow> P a b"
+ assumes init: "P a a"
+ assumes step: "\<And>b. a \<le> b \<Longrightarrow> P a b \<Longrightarrow> P a (b + 1)"
+ shows "P a b"
+proof (cases "a \<le> b")
+ case False with less show ?thesis by (simp add: not_le)
+next
+ case True then obtain n where b: "b = a + of_nat n"
+ by (blast elim: less_eqE)
+ then have "P a (a + of_nat n)"
+ proof (induct n arbitrary: b)
+ case 0 with init show ?case by simp
+ next
+ case (Suc n)
+ from Suc.prems have "b - 1 = a + of_nat (Suc n) - 1"
+ by simp
+ then have *: "b - 1 = a + of_nat n"
+ by (simp add: add.left_commute [of _ 1])
+ with Suc.hyps have "P a (a + of_nat n)" .
+ with step [of "a + of_nat n"] show ?case
+ by (simp add: ac_simps)
+ qed
+ with b show ?thesis by simp
+qed
+
+lemma sorted_upt [simp]:
+ "sorted [a..<b]"
+ by (simp add: upt_def finite_interval)
+
+lemma sort_upt [simp]:
+ "sort [a..<b] = [a..<b]"
+ by (rule sorted_sort_id) simp
+
+lemma distinct_upt [simp]:
+ "distinct [a..<b]"
+ by (simp add: upt_def finite_interval)
+
+lemma set_upt [simp]:
+ "set [a..<b] = {a..<b}"
+ by (simp add: upt_def finite_interval)
+
+lemma sorted_list_of_set_interval [simp]:
+ "sorted_list_of_set {a..<b} = [a..<b]"
+ by (simp add: upt_def)
+
+lemma set_upto [simp]:
+ "set [a..b] = {a..b}"
+ by (simp only: set_upt interval_inc_interval_inc)
+
+lemma sorted_list_of_set_interval_inc [simp]:
+ "sorted_list_of_set {a..b} = [a..b]"
+ by (simp only: upt_def interval_inc_interval_inc)
+
+lemma remdups_upt [simp]:
+ "remdups [a..<b] = [a..<b]"
+ by simp
+
+lemma upt_triv [simp]:
+ "[a..<a] = []"
+ by (rule sorted_distinct_set_unique) simp_all
+
+lemma upto_triv [simp]:
+ "[a..a] = [a]"
+ by (rule sorted_distinct_set_unique)
+ (simp_all add: interval_inc_interval_inc)
+
+lemma upt_conv_Nil [simp]:
+ "b \<le> a \<Longrightarrow> [a..<b] = []"
+ by (rule sorted_distinct_set_unique) simp_all
+
+lemma upto_conv_Nil [simp]:
+ "b < a \<Longrightarrow> [a..b] = []"
+ by (rule sorted_distinct_set_unique)
+ (simp_all add: interval_inc_interval_inc)
+
+lemma upto_conv_snoc_0:
+ "a \<le> b \<Longrightarrow> [a..b] = [a..<b] @ [b]"
+ by (rule sorted_distinct_set_unique)
+ (auto simp add: sorted_append less_succ_iff)
+
+lemma upt_conv_snoc_0:
+ assumes "a < b"
+ shows "[a..<b] = [a..<b - 1] @ [b - 1]"
+proof -
+ from assms obtain m where b: "b = a + of_nat m" and "m > 0"
+ by (blast elim: lessE)
+ then obtain n where "m = Suc n" by (cases m) simp_all
+ moreover have "[a..a + of_nat n] = [a..<a + of_nat n] @ [a + of_nat n]"
+ by (rule upto_conv_snoc_0) simp
+ moreover have "a + (1 + of_nat n) - 1 = a + of_nat n"
+ by (simp add: add.left_commute [of _ 1])
+ ultimately show ?thesis using b
+ by (simp add: ac_simps)
+qed
+
+lemma upto_conv_snoc_1:
+ "a \<le> b \<Longrightarrow> [a..b + 1] = [a..b] @ [b + 1]"
+ by (rule upto_conv_snoc_0) (insert add_mono [of a b 0 1], simp)
+
+lemma upt_conv_snoc_2:
+ "a \<le> b \<Longrightarrow> [a..<b + 2] = [a..b] @ [b + 1]"
+ by (drule upto_conv_snoc_1) (simp add: ac_simps)
+
+lemmas upt_conv_snoc_simps = upto_conv_snoc_0 upt_conv_snoc_0 upto_conv_snoc_1 upt_conv_snoc_2
+
+lemma upt_conv_Cons:
+ "a < b \<Longrightarrow> [a..<b] = a # [a + 1..<b]"
+ by (rule sorted_distinct_set_unique)
+ (auto simp add: sorted_Cons less_eq_succ_iff)
+
+lemma upto_conv_Cons:
+ "a \<le> b \<Longrightarrow> [a..b] = a # [a + 1..b]"
+ by (simp add: upt_conv_Cons less_succ_iff )
+
+lemmas upt_conv_Cons_simps = upt_conv_Cons upto_conv_Cons
+
+lemma upt_eq_Nil_conv [simp]:
+ "[a..<b] = [] \<longleftrightarrow> b \<le> a"
+ by (simp only: upt_def sorted_list_of_set_eq_Nil_iff finite_interval) auto
+
+lemma upto_eq_Nil_conv [simp]:
+ "[a..b] = [] \<longleftrightarrow> b < a"
+ by (simp add: less_eq_succ_iff)
+
+lemma upt_eq_Cons_conv:
+ "[a..<b] = x # xs \<longleftrightarrow> a < b \<and> a = x \<and> [a + 1..<b] = xs"
+ by (cases "a < b") (auto simp add: not_less upt_conv_Cons_simps)
+
+text \<open>Tail recursive version for code generation\<close>
+
+definition upt_aux :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+ "upt_aux i j js = [i..<j] @ js"
+
+lemma upt_code [code]:
+ "[i..<j] = upt_aux i j []"
+ by (simp add: upt_aux_def)
+
+lemma upt_aux_rec [code]:
+ "upt_aux i j js =
+ (if j \<le> i then js else let k = j - 1 in upt_aux i k (k # js))"
+ by (auto simp add: upt_aux_def upt_conv_snoc_simps Let_def)
+
+end
+
+instance nat :: pointed_linordered_semidom
+ by standard (simp add: nat_le_iff_add)
+
+instance int :: pointed_linordered_semidom
+ by standard (simp add: zle_iff_zadd)
+
+lemma upt_simps [simp]:
+ "[i..<0] = []"
+ "[i..<Suc j] = (if i <= j then [i..<j] @ [j] else [])"
+ by (auto intro!: sorted_distinct_set_unique simp add: sorted_append)
+
+lemma upt_rec: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
\<comment> \<open>simp does not terminate!\<close>
-by (induct j) auto
+ by (induct j) simp_all
lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
-lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
-by (subst upt_rec) simp
-
-lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
-by(induct j)simp_all
-
-lemma upt_eq_Cons_conv:
- "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
-apply(induct j arbitrary: x xs)
- apply simp
-apply(clarsimp simp add: append_eq_Cons_conv)
-apply arith
-done
+lemma upt_eq_Nil_conv [simp]:
+ "[i::nat..<j] = [] \<longleftrightarrow> j = 0 \<or> j \<le> i"
+ by auto
lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
@@ -4860,7 +5120,7 @@
case True then show ?thesis by (simp add: upt_conv_Cons)
qed
-lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
+lemma upt_add_eq_append: "(i::nat)<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
\<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
by (induct k) auto
@@ -4870,18 +5130,18 @@
lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
-lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
+lemma hd_upt[simp]: "(i::nat) < j \<Longrightarrow> hd[i..<j] = i"
by(simp add:upt_conv_Cons)
-lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
+lemma last_upt[simp]: "(i::nat) < j \<Longrightarrow> last[i..<j] = j - 1"
by(cases j)(auto simp: upt_Suc_append)
-lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
+lemma take_upt [simp]: "(i::nat)+m <= n ==> take m [i..<n] = [i..<i+m]"
apply (induct m arbitrary: i, simp)
apply (subst upt_rec)
apply (rule sym)
apply (subst upt_rec)
-apply (simp del: upt.simps)
+apply (simp del: upt_simps)
done
lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
@@ -4890,7 +5150,7 @@
lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
by (induct n) auto
-lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
+lemma map_add_upt: "map (\<lambda>i::nat. i + n) [0..<m] = [n..<m + n]"
by (induct m) simp_all
lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
@@ -4906,31 +5166,6 @@
"map (\<lambda>i. xs ! i) [0..<length xs] = xs"
by (rule nth_equalityI, auto)
-lemma distinct_upt[simp]: "distinct[i..<j]"
-by (induct j) auto
-
-lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]"
-proof (cases "m \<le> n")
- case False then show ?thesis by simp
-next
- case True then obtain q where "n = m + q"
- by (auto simp add: le_iff_add)
- moreover have "remdups [m..<m + q] = [m..<m + q]"
- by (induct q) simp_all
- ultimately show ?thesis by simp
-qed
-
-lemma sorted_upt[simp]: "sorted[i..<j]"
-by (induct j) (simp_all add:sorted_append)
-
-lemma sort_upt [simp]:
- "sort [m..<n] = [m..<n]"
- by (rule sorted_sort_id) simp
-
-lemma sorted_list_of_set_range [simp]:
- "sorted_list_of_set {m..<n} = [m..<n]"
- by (rule sorted_distinct_set_unique) simp_all
-
lemma map_replicate_trivial:
"map (\<lambda>i. x) [0..<i] = replicate i x"
by (induct i) (simp_all add: replicate_append_same)
@@ -4953,68 +5188,25 @@
by (auto simp: nth_transpose intro: nth_equalityI)
qed
-
-subsubsection \<open>\<open>upto\<close>: interval-list on @{typ int}\<close>
-
-function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
- "upto i j = (if i \<le> j then i # [i+1..j] else [])"
-by auto
-termination
-by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
-
-declare upto.simps[simp del]
+lemma upto_simps:
+ fixes i j :: int
+ shows "upto i j = (if i \<le> j then i # [i+1..j] else [])"
+ by (rule sorted_distinct_set_unique) (auto simp add: sorted_Cons)
lemmas upto_rec_numeral [simp] =
- upto.simps[of "numeral m" "numeral n"]
- upto.simps[of "numeral m" "- numeral n"]
- upto.simps[of "- numeral m" "numeral n"]
- upto.simps[of "- numeral m" "- numeral n"] for m n
-
-lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
-by(simp add: upto.simps)
-
-lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
-by(simp add: upto.simps)
-
-lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..j] = [i..j - 1]@[j]"
-proof(induct "nat(j-i)" arbitrary: i j)
- case 0 thus ?case by(simp add: upto.simps)
-next
- case (Suc n)
- hence "n = nat (j - (i + 1))" "i < j" by linarith+
- from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp
-qed
-
-lemma set_upto[simp]: "set[i..j] = {i..j}"
-proof(induct i j rule:upto.induct)
- case (1 i j)
- from this show ?case
- unfolding upto.simps[of i j] by auto
-qed
-
-lemma distinct_upto[simp]: "distinct[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
-
-text\<open>Tail recursive version for code generation:\<close>
-
-definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
- "upto_aux i j js = [i..j] @ js"
-
-lemma upto_aux_rec [code]:
- "upto_aux i j js = (if j<i then js else upto_aux i (j - 1) (j#js))"
-by (simp add: upto_aux_def upto_rec2)
-
-lemma upto_code[code]: "[i..j] = upto_aux i j []"
-by(simp add: upto_aux_def)
-
-lemma sorted_upto[simp]: "sorted[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp add:sorted_Cons)
-done
+ upto_simps[of "numeral m" "numeral n"]
+ upto_simps[of "numeral m" "- numeral n"]
+ upto_simps[of "- numeral m" "numeral n"]
+ upto_simps[of "- numeral m" "- numeral n"] for m n
+
+lemma upto_empty[simp]: "(j::int) < i \<Longrightarrow> [i..j] = []"
+ by (fact upto_conv_Nil)
+
+lemma upto_rec1: "(i::int) \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
+ by (fact upto_conv_Cons)
+
+lemma upto_rec2: "(i::int) \<le> j \<Longrightarrow> [i..j] = [i..j - 1] @ [j]"
+ by (rule sorted_distinct_set_unique) (auto simp add: sorted_append)
subsubsection \<open>@{text enumerate}\<close>
@@ -6352,7 +6544,7 @@
by auto
lemma atLeast_upt [code_unfold]:
- "{..<n} = set [0..<n]"
+ "{..<n} = set [0..<(n::nat)]"
by auto
lemma greaterThanLessThan_upt [code_unfold]:
@@ -6528,11 +6720,11 @@
lemma list_all_iff_all_interval_int [code_unfold]:
"list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"
- by (simp add: list_all_iff all_interval_int_def)
+ by (simp add: list_all_iff all_interval_int_def interval_inc_interval_inc)
lemma list_ex_iff_not_all_inverval_int [code_unfold]:
"list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
- by (simp add: list_ex_iff all_interval_int_def)
+ by (simp add: list_ex_iff all_interval_int_def interval_inc_interval_inc)
text \<open>optimized code (tail-recursive) for @{term length}\<close>
diff -r f3ef1ecc3fbc src/HOL/Random.thy
--- a/src/HOL/Random.thy Sat Mar 12 16:26:37 2016 +0100
+++ b/src/HOL/Random.thy Sat Mar 12 19:56:50 2016 +0100
@@ -118,7 +118,7 @@
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
- by (induct xs) (auto simp add: less_natural_def, simp add: plus_natural_def)
+ by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160313/fcb36270/attachment-0001.asc>
More information about the isabelle-dev
mailing list