got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
authornipkow
Wed Aug 26 19:54:01 2009 +0200 (2009-08-26)
changeset 324151dddf2f64266
parent 32409 7e38dedf3f7d
child 32416 4ea7648b6ae2
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
src/HOL/GCD.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Aug 26 16:41:37 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Aug 26 19:54:01 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 16:41:37 2009 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Aug 26 19:54:01 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.23 +by(simp add: upto.simps)
    2.24 +
    2.25 +lemma set_upto[simp]: "set[i..j] = {i..j}"
    2.26 +apply(induct i j rule:upto.induct)
    2.27 +apply(simp add: upto.simps simp_from_to)
    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.54 +apply(simp add:sorted_Cons)
    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.80 -by(simp add:upto_def finite_intvl)
    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.90 -apply(simp add:sorted_list_of_set_def upto_def)
    2.91 -apply (rule the1_equality[OF finite_sorted_distinct_unique])
    2.92 - apply (simp add:finite_intvl)
    2.93 -apply(rule the1I2[OF finite_sorted_distinct_unique])
    2.94 - apply (simp add:finite_intvl)
    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.102 -apply(simp add:sorted_list_of_set_def upto_def)
   2.103 -apply (rule the1_equality[OF finite_sorted_distinct_unique])
   2.104 - apply (simp add:finite_intvl)
   2.105 -apply(rule the1I2[OF finite_sorted_distinct_unique])
   2.106 - apply (simp add:finite_intvl)
   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.114 -by(simp add: upto_def sorted_list_of_set_rec)
   2.115 -
   2.116 -lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
   2.117 -by(simp add: upto_rec)
   2.118 -
   2.119 -lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
   2.120 -by(simp add: upto_def sorted_list_of_set_rec2)
   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])"