src/HOL/List.thy
changeset 45607 16b4f5774621
parent 45181 c8eb935e2e87
child 45714 ad4242285560
equal deleted inserted replaced
45606:b1e1508643b1 45607:16b4f5774621
  2562 
  2562 
  2563 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  2563 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  2564 -- {* simp does not terminate! *}
  2564 -- {* simp does not terminate! *}
  2565 by (induct j) auto
  2565 by (induct j) auto
  2566 
  2566 
  2567 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
  2567 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n"] for m n
  2568 
  2568 
  2569 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
  2569 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
  2570 by (subst upt_rec) simp
  2570 by (subst upt_rec) simp
  2571 
  2571 
  2572 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
  2572 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
  2677 by (cases n) simp_all
  2677 by (cases n) simp_all
  2678 
  2678 
  2679 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2679 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2680 by (cases n) simp_all
  2680 by (cases n) simp_all
  2681 
  2681 
  2682 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
  2682 lemmas take_Cons_number_of = take_Cons'[of "number_of v"] for v
  2683 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
  2683 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v"] for v
  2684 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
  2684 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v"] for v
  2685 
  2685 
  2686 declare take_Cons_number_of [simp] 
  2686 declare take_Cons_number_of [simp] 
  2687         drop_Cons_number_of [simp] 
  2687         drop_Cons_number_of [simp] 
  2688         nth_Cons_number_of [simp] 
  2688         nth_Cons_number_of [simp] 
  2689 
  2689 
  2698 termination
  2698 termination
  2699 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
  2699 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
  2700 
  2700 
  2701 declare upto.simps[code, simp del]
  2701 declare upto.simps[code, simp del]
  2702 
  2702 
  2703 lemmas upto_rec_number_of[simp] =
  2703 lemmas upto_rec_number_of[simp] = upto.simps[of "number_of m" "number_of n"] for m n
  2704   upto.simps[of "number_of m" "number_of n", standard]
       
  2705 
  2704 
  2706 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  2705 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  2707 by(simp add: upto.simps)
  2706 by(simp add: upto.simps)
  2708 
  2707 
  2709 lemma set_upto[simp]: "set[i..j] = {i..j}"
  2708 lemma set_upto[simp]: "set[i..j] = {i..j}"