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