src/HOL/Datatype.thy
changeset 24194 96013f81faef
parent 24162 8dfd5dd65d82
child 24286 7619080e49f0
     1.1 --- a/src/HOL/Datatype.thy	Thu Aug 09 15:52:38 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Thu Aug 09 15:52:42 2007 +0200
     1.3 @@ -539,9 +539,23 @@
     1.4  
     1.5  subsection {* Representing primitive types *}
     1.6  
     1.7 +rep_datatype bool
     1.8 +  distinct True_not_False False_not_True
     1.9 +  induction bool_induct
    1.10 +
    1.11  declare case_split [cases type: bool]
    1.12    -- "prefer plain propositional version"
    1.13  
    1.14 +lemma size_bool [code func]:
    1.15 +  "size (b\<Colon>bool) = 0" by (cases b) auto
    1.16 +
    1.17 +rep_datatype unit
    1.18 +  induction unit_induct
    1.19 +
    1.20 +rep_datatype prod
    1.21 +  inject Pair_eq
    1.22 +  induction prod_induct
    1.23 +
    1.24  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    1.25  
    1.26  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
    1.27 @@ -568,6 +582,14 @@
    1.28  
    1.29  lemmas [code inline] = prod_case_split [symmetric]
    1.30  
    1.31 +rep_datatype sum
    1.32 +  distinct Inl_not_Inr Inr_not_Inl
    1.33 +  inject Inl_eq Inr_eq
    1.34 +  induction sum_induct
    1.35 +
    1.36 +lemma size_sum [code func]:
    1.37 +  "size (x \<Colon> 'a + 'b) = 0" by (cases x) auto
    1.38 +
    1.39  lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    1.40    by (rule ext) (simp split: sum.split)
    1.41  
    1.42 @@ -655,4 +677,125 @@
    1.43      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    1.44    by (cases x) blast
    1.45  
    1.46 +
    1.47 +subsection {* The option datatype *}
    1.48 +
    1.49 +datatype 'a option = None | Some 'a
    1.50 +
    1.51 +lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
    1.52 +  by (induct x) auto
    1.53 +
    1.54 +lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
    1.55 +  by (induct x) auto
    1.56 +
    1.57 +text{*Although it may appear that both of these equalities are helpful
    1.58 +only when applied to assumptions, in practice it seems better to give
    1.59 +them the uniform iff attribute. *}
    1.60 +
    1.61 +lemma option_caseE:
    1.62 +  assumes c: "(case x of None => P | Some y => Q y)"
    1.63 +  obtains
    1.64 +    (None) "x = None" and P
    1.65 +  | (Some) y where "x = Some y" and "Q y"
    1.66 +  using c by (cases x) simp_all
    1.67 +
    1.68 +
    1.69 +subsubsection {* Operations *}
    1.70 +
    1.71 +consts
    1.72 +  the :: "'a option => 'a"
    1.73 +primrec
    1.74 +  "the (Some x) = x"
    1.75 +
    1.76 +consts
    1.77 +  o2s :: "'a option => 'a set"
    1.78 +primrec
    1.79 +  "o2s None = {}"
    1.80 +  "o2s (Some x) = {x}"
    1.81 +
    1.82 +lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
    1.83 +  by simp
    1.84 +
    1.85 +ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
    1.86 +
    1.87 +lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
    1.88 +  by (cases xo) auto
    1.89 +
    1.90 +lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
    1.91 +  by (cases xo) auto
    1.92 +
    1.93 +
    1.94 +constdefs
    1.95 +  option_map :: "('a => 'b) => ('a option => 'b option)"
    1.96 +  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.97 +
    1.98 +lemmas [code func del] = option_map_def
    1.99 +
   1.100 +lemma option_map_None [simp, code]: "option_map f None = None"
   1.101 +  by (simp add: option_map_def)
   1.102 +
   1.103 +lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
   1.104 +  by (simp add: option_map_def)
   1.105 +
   1.106 +lemma option_map_is_None [iff]:
   1.107 +    "(option_map f opt = None) = (opt = None)"
   1.108 +  by (simp add: option_map_def split add: option.split)
   1.109 +
   1.110 +lemma option_map_eq_Some [iff]:
   1.111 +    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   1.112 +  by (simp add: option_map_def split add: option.split)
   1.113 +
   1.114 +lemma option_map_comp:
   1.115 +    "option_map f (option_map g opt) = option_map (f o g) opt"
   1.116 +  by (simp add: option_map_def split add: option.split)
   1.117 +
   1.118 +lemma option_map_o_sum_case [simp]:
   1.119 +    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   1.120 +  by (rule ext) (simp split: sum.split)
   1.121 +
   1.122 +
   1.123 +subsubsection {* Code generator setup *}
   1.124 +
   1.125 +definition
   1.126 +  is_none :: "'a option \<Rightarrow> bool" where
   1.127 +  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
   1.128 +
   1.129 +lemma is_none_code [code]:
   1.130 +  shows "is_none None \<longleftrightarrow> True"
   1.131 +    and "is_none (Some x) \<longleftrightarrow> False"
   1.132 +  unfolding is_none_none [symmetric] by simp_all
   1.133 +
   1.134 +hide (open) const is_none
   1.135 +
   1.136 +code_type option
   1.137 +  (SML "_ option")
   1.138 +  (OCaml "_ option")
   1.139 +  (Haskell "Maybe _")
   1.140 +
   1.141 +code_const None and Some
   1.142 +  (SML "NONE" and "SOME")
   1.143 +  (OCaml "None" and "Some _")
   1.144 +  (Haskell "Nothing" and "Just")
   1.145 +
   1.146 +code_instance option :: eq
   1.147 +  (Haskell -)
   1.148 +
   1.149 +code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   1.150 +  (Haskell infixl 4 "==")
   1.151 +
   1.152 +code_reserved SML
   1.153 +  option NONE SOME
   1.154 +
   1.155 +code_reserved OCaml
   1.156 +  option None Some
   1.157 +
   1.158 +code_modulename SML
   1.159 +  Datatype Nat
   1.160 +
   1.161 +code_modulename OCaml
   1.162 +  Datatype Nat
   1.163 +
   1.164 +code_modulename Haskell
   1.165 +  Datatype Nat
   1.166 +
   1.167  end