tuned code generation for lists
authornipkow
Thu Aug 27 09:28:52 2009 +0200 (2009-08-27)
changeset 32417e87d9c78910c
parent 32416 4ea7648b6ae2
child 32419 016134424f71
child 32422 46fc4d4ff4c0
child 32527 569e8d6729a1
tuned code generation for lists
src/HOL/List.thy
src/HOL/MicroJava/BV/Typing_Framework_err.thy
     1.1 --- a/src/HOL/List.thy	Wed Aug 26 19:54:19 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Aug 27 09:28:52 2009 +0200
     1.3 @@ -881,10 +881,8 @@
     1.4  lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
     1.5  by (induct xs) auto
     1.6  
     1.7 -lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
     1.8 -apply (induct j, simp_all)
     1.9 -apply (erule ssubst, auto)
    1.10 -done
    1.11 +lemma set_upt [simp]: "set[i..<j] = {i..<j}"
    1.12 +by (induct j) (simp_all add: atLeastLessThanSuc)
    1.13  
    1.14  
    1.15  lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
    1.16 @@ -3782,9 +3780,7 @@
    1.17    "{n<..<m} = set [Suc n..<m]"
    1.18  by auto
    1.19  
    1.20 -lemma atLeastLessThan_upt [code_unfold]:
    1.21 -  "{n..<m} = set [n..<m]"
    1.22 -by auto
    1.23 +lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
    1.24  
    1.25  lemma greaterThanAtMost_upt [code_unfold]:
    1.26    "{n<..m} = set [Suc n..<Suc m]"
     2.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Aug 26 19:54:19 2009 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Thu Aug 27 09:28:52 2009 +0200
     2.3 @@ -62,15 +62,9 @@
     2.4  lemma bounded_err_stepI:
     2.5    "\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
     2.6    \<Longrightarrow> bounded (err_step n ap step) n"
     2.7 -apply (unfold bounded_def)
     2.8 -apply clarify
     2.9 -apply (simp add: err_step_def split: err.splits)
    2.10 -apply (simp add: error_def)
    2.11 - apply blast
    2.12 -apply (simp split: split_if_asm) 
    2.13 - apply (blast dest: in_map_sndD)
    2.14 -apply (simp add: error_def)
    2.15 -apply blast
    2.16 +apply (clarsimp simp: bounded_def err_step_def split: err.splits)
    2.17 +apply (simp add: error_def image_def)
    2.18 +apply (blast dest: in_map_sndD)
    2.19  done
    2.20  
    2.21