author nipkow Wed Aug 26 19:54:19 2009 +0200 (2009-08-26) changeset 32416 4ea7648b6ae2 parent 32414 62a7aea5f50c parent 32415 1dddf2f64266 child 32417 e87d9c78910c
merged
```     1.1 --- a/src/HOL/GCD.thy	Wed Aug 26 17:38:18 2009 +0100
1.2 +++ b/src/HOL/GCD.thy	Wed Aug 26 19:54:19 2009 +0200
1.3 @@ -1895,8 +1895,6 @@
1.4
1.5  lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
1.6
1.7 -declare successor_int_def[simp]
1.8 -
1.9  lemma two_is_prime_nat [simp]: "prime (2::nat)"
1.10  by simp
1.11
```
```     2.1 --- a/src/HOL/List.thy	Wed Aug 26 17:38:18 2009 +0100
2.2 +++ b/src/HOL/List.thy	Wed Aug 26 19:54:19 2009 +0200
2.3 @@ -2394,6 +2394,30 @@
2.4          nth_Cons_number_of [simp]
2.5
2.6
2.7 +subsubsection {* @{text upto}: interval-list on @{typ int} *}
2.8 +
2.9 +(* FIXME make upto tail recursive? *)
2.10 +
2.11 +function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
2.12 +"upto i j = (if i \<le> j then i # [i+1..j] else [])"
2.13 +by auto
2.14 +termination
2.15 +by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
2.16 +
2.17 +declare upto.simps[code, simp del]
2.18 +
2.19 +lemmas upto_rec_number_of[simp] =
2.20 +  upto.simps[of "number_of m" "number_of n", standard]
2.21 +
2.22 +lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
2.24 +
2.25 +lemma set_upto[simp]: "set[i..j] = {i..j}"
2.26 +apply(induct i j rule:upto.induct)
2.28 +done
2.29 +
2.30 +
2.31  subsubsection {* @{text "distinct"} and @{text remdups} *}
2.32
2.33  lemma distinct_append [simp]:
2.34 @@ -2448,6 +2472,12 @@
2.35  lemma distinct_upt[simp]: "distinct[i..<j]"
2.36  by (induct j) auto
2.37
2.38 +lemma distinct_upto[simp]: "distinct[i..j]"
2.39 +apply(induct i j rule:upto.induct)
2.40 +apply(subst upto.simps)
2.41 +apply(simp)
2.42 +done
2.43 +
2.44  lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
2.45  apply(induct xs arbitrary: i)
2.46   apply simp
2.47 @@ -3091,6 +3121,12 @@
2.48  lemma sorted_upt[simp]: "sorted[i..<j]"
2.49  by (induct j) (simp_all add:sorted_append)
2.50
2.51 +lemma sorted_upto[simp]: "sorted[i..j]"
2.52 +apply(induct i j rule:upto.induct)
2.53 +apply(subst upto.simps)
2.55 +done
2.56 +
2.57
2.58  subsubsection {* @{text sorted_list_of_set} *}
2.59
2.60 @@ -3124,89 +3160,6 @@
2.61  end
2.62
2.63
2.64 -subsubsection {* @{text upto}: the generic interval-list *}
2.65 -
2.66 -class finite_intvl_succ = linorder +
2.67 -fixes successor :: "'a \<Rightarrow> 'a"
2.68 -assumes finite_intvl: "finite{a..b}"
2.69 -and successor_incr: "a < successor a"
2.70 -and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
2.71 -
2.72 -context finite_intvl_succ
2.73 -begin
2.74 -
2.75 -definition
2.76 - upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
2.77 -"upto i j == sorted_list_of_set {i..j}"
2.78 -
2.79 -lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
2.81 -
2.82 -lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
2.83 -apply(insert successor_incr[of i])
2.84 -apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
2.85 -apply(metis ord_discrete less_le not_le)
2.86 -done
2.87 -
2.88 -lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
2.89 -  sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
2.91 -apply (rule the1_equality[OF finite_sorted_distinct_unique])
2.93 -apply(rule the1I2[OF finite_sorted_distinct_unique])
2.95 -apply (simp add: sorted_Cons insert_intvl Ball_def)
2.96 -apply (metis successor_incr leD less_imp_le order_trans)
2.97 -done
2.98 -
2.99 -lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
2.100 -  sorted_list_of_set {i..successor j} =
2.101 -  sorted_list_of_set {i..j} @ [successor j]"
2.103 -apply (rule the1_equality[OF finite_sorted_distinct_unique])
2.105 -apply(rule the1I2[OF finite_sorted_distinct_unique])
2.107 -apply (simp add: sorted_append Ball_def expand_set_eq)
2.108 -apply(rule conjI)
2.109 -apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
2.110 -apply (metis leD linear order_trans successor_incr)
2.111 -done
2.112 -
2.113 -lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
2.115 -
2.116 -lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
2.118 -
2.119 -lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
2.121 -
2.122 -end
2.123 -
2.124 -text{* The integers are an instance of the above class: *}
2.125 -
2.126 -instantiation int:: finite_intvl_succ
2.127 -begin
2.128 -
2.129 -definition
2.130 -successor_int_def[simp]: "successor = (%i\<Colon>int. i+1)"
2.131 -
2.132 -instance
2.133 -by intro_classes (simp_all add: successor_int_def)
2.134 -
2.135 -end
2.136 -
2.137 -text{* Now @{term"[i..j::int]"} is defined for integers. *}
2.138 -
2.139 -hide (open) const successor
2.140 -
2.141 -lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
2.142 -by(rule upto_rec2[where 'a = int, simplified successor_int_def])
2.143 -
2.144 -lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard]
2.145 -
2.146 -
2.147  subsubsection {* @{text lists}: the list-forming operator over sets *}
2.148
2.149  inductive_set
2.150 @@ -3880,9 +3833,7 @@
2.151    "{i<..j::int} = set [i+1..j]"
2.152  by auto
2.153
2.154 -lemma atLeastAtMost_upto [code_unfold]:
2.155 -  "{i..j::int} = set [i..j]"
2.156 -by auto
2.157 +lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
2.158
2.159  lemma setsum_set_upto_conv_listsum [code_unfold]:
2.160    "setsum f (set [i..j::int]) = listsum (map f [i..j])"
```