improved code lemmas
authorhaftmann
Tue Jun 06 14:56:42 2006 +0200 (2006-06-06)
changeset 19787b949911ecff5
parent 19786 eeefc22d08d8
child 19788 be3a84d22a58
improved code lemmas
src/HOL/Datatype.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Datatype.thy	Tue Jun 06 14:55:56 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Jun 06 14:56:42 2006 +0200
     1.3 @@ -218,6 +218,17 @@
     1.4    apply (simp split add: sum.split)
     1.5    done
     1.6  
     1.7 +
     1.8 +consts
     1.9 +  is_none :: "'a option \<Rightarrow> bool"
    1.10 +primrec
    1.11 +  "is_none None = True"
    1.12 +  "is_none (Some x) = False"
    1.13 +
    1.14 +(* lemma is_none_none [code unfolt]:
    1.15 +  "(x = None) = (is_none x)" 
    1.16 +by (cases "x") simp_all *)
    1.17 +
    1.18  lemmas [code] = imp_conv_disj
    1.19  
    1.20  subsubsection {* Codegenerator setup *}
     2.1 --- a/src/HOL/List.thy	Tue Jun 06 14:55:56 2006 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Jun 06 14:56:42 2006 +0200
     2.3 @@ -270,6 +270,9 @@
     2.4  lemma null_empty: "null xs = (xs = [])"
     2.5    by (cases xs) simp_all
     2.6  
     2.7 +(*lemma empty_null [code unfolt]:
     2.8 +  "(xs = []) = null xs"
     2.9 +using null_empty [symmetric] .*)
    2.10  
    2.11  subsubsection {* @{text length} *}
    2.12  
    2.13 @@ -1086,19 +1089,6 @@
    2.14  lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
    2.15  by(induct xs)(auto simp:neq_Nil_conv)
    2.16  
    2.17 -lemma last_code [code]:
    2.18 -  "last (x # xs) = (if null xs then x else last xs)"
    2.19 -by (cases xs) simp_all
    2.20 -
    2.21 -declare last.simps [code del]
    2.22 -
    2.23 -lemma butlast_code [code]:
    2.24 -  "butlast [] = []"
    2.25 -  "butlast (x # xs) = (if null xs then [] else x # butlast xs)"
    2.26 -by (simp, cases xs) simp_all
    2.27 -
    2.28 -declare butlast.simps [code del]
    2.29 -
    2.30  subsubsection {* @{text take} and @{text drop} *}
    2.31  
    2.32  lemma take_0 [simp]: "take 0 xs = []"
    2.33 @@ -1461,17 +1451,11 @@
    2.34    "list_all2 P xs ys ==> length xs = length ys"
    2.35    by (simp add: list_all2_def)
    2.36  
    2.37 -lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
    2.38 -  by (simp add: list_all2_def)
    2.39 -
    2.40 -lemma list_all2_Nil2 [iff]: "list_all2 P xs [] = (xs = [])"
    2.41 +lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
    2.42    by (simp add: list_all2_def)
    2.43  
    2.44 -lemma list_all2_Nil_code [code]: "list_all2 P [] ys = null ys"
    2.45 -  unfolding null_empty by simp
    2.46 -
    2.47 -lemma list_all2_Nil2_code [code]: "list_all2 P xs [] = null xs"
    2.48 -  unfolding null_empty by simp
    2.49 +lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
    2.50 +  by (simp add: list_all2_def)
    2.51  
    2.52  lemma list_all2_Cons [iff, code]:
    2.53    "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
    2.54 @@ -2750,7 +2734,7 @@
    2.55  
    2.56  code_alias
    2.57    "List.op @" "List.append"
    2.58 -  "List.op mem" "List.member"
    2.59 +  "List.op mem" "List.mem"
    2.60  
    2.61  code_generate Nil Cons
    2.62