# HG changeset patch
# User nipkow
# Date 1251358132 -7200
# Node ID e87d9c78910c10a4bc3b63fa53e2aa047c2aca8e
# Parent  4ea7648b6ae2ca677d859842313c83372cf8530d
tuned code generation for lists

diff -r 4ea7648b6ae2 -r e87d9c78910c src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 26 19:54:19 2009 +0200
+++ b/src/HOL/List.thy	Thu Aug 27 09:28:52 2009 +0200
@@ -881,10 +881,8 @@
 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] = {k. i \<le> k \<and> k < j}"
-apply (induct j, simp_all)
-apply (erule ssubst, auto)
-done
+lemma set_upt [simp]: "set[i..<j] = {i..<j}"
+by (induct j) (simp_all add: atLeastLessThanSuc)
 
 
 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
@@ -3782,9 +3780,7 @@
   "{n<..<m} = set [Suc n..<m]"
 by auto
 
-lemma atLeastLessThan_upt [code_unfold]:
-  "{n..<m} = set [n..<m]"
-by auto
+lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
 
 lemma greaterThanAtMost_upt [code_unfold]:
   "{n<..m} = set [Suc n..<Suc m]"
diff -r 4ea7648b6ae2 -r e87d9c78910c src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Aug 26 19:54:19 2009 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Thu Aug 27 09:28:52 2009 +0200
@@ -62,15 +62,9 @@
 lemma bounded_err_stepI:
   "\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
   \<Longrightarrow> bounded (err_step n ap step) n"
-apply (unfold bounded_def)
-apply clarify
-apply (simp add: err_step_def split: err.splits)
-apply (simp add: error_def)
- apply blast
-apply (simp split: split_if_asm) 
- apply (blast dest: in_map_sndD)
-apply (simp add: error_def)
-apply blast
+apply (clarsimp simp: bounded_def err_step_def split: err.splits)
+apply (simp add: error_def image_def)
+apply (blast dest: in_map_sndD)
 done