src/HOL/Datatype.thy
changeset 12918 bca45be2d25b
parent 12029 7df1d840d01d
child 13635 c41e88151b54
     1.1 --- a/src/HOL/Datatype.thy	Thu Feb 21 20:06:39 2002 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Thu Feb 21 20:08:09 2002 +0100
     1.3 @@ -4,10 +4,12 @@
     1.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.5  *)
     1.6  
     1.7 -header {* Final stage of datatype setup *}
     1.8 +header {* Datatypes *}
     1.9  
    1.10  theory Datatype = Datatype_Universe:
    1.11  
    1.12 +subsection {* Finishing the datatype package setup *}
    1.13 +
    1.14  text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    1.15  hide const Node Atom Leaf Numb Lim Funs Split Case
    1.16  hide type node item
    1.17 @@ -22,11 +24,6 @@
    1.18  declare case_split [cases type: bool]
    1.19    -- "prefer plain propositional version"
    1.20  
    1.21 -rep_datatype sum
    1.22 -  distinct Inl_not_Inr Inr_not_Inl
    1.23 -  inject Inl_eq Inr_eq
    1.24 -  induction sum_induct
    1.25 -
    1.26  rep_datatype unit
    1.27    induction unit_induct
    1.28  
    1.29 @@ -34,7 +31,47 @@
    1.30    inject Pair_eq
    1.31    induction prod_induct
    1.32  
    1.33 -text {* Further cases/induct rules for 3--7 tuples. *}
    1.34 +rep_datatype sum
    1.35 +  distinct Inl_not_Inr Inr_not_Inl
    1.36 +  inject Inl_eq Inr_eq
    1.37 +  induction sum_induct
    1.38 +
    1.39 +ML {*
    1.40 +  val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
    1.41 +  bind_thm ("sum_case_Inl", sum_case_Inl);
    1.42 +  bind_thm ("sum_case_Inr", sum_case_Inr);
    1.43 +*} -- {* compatibility *}
    1.44 +
    1.45 +lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.46 +  apply (rule_tac s = s in sumE)
    1.47 +   apply (erule ssubst)
    1.48 +   apply (rule sum_case_Inl)
    1.49 +  apply (erule ssubst)
    1.50 +  apply (rule sum_case_Inr)
    1.51 +  done
    1.52 +
    1.53 +lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    1.54 +  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    1.55 +  by (erule arg_cong)
    1.56 +
    1.57 +lemma sum_case_inject:
    1.58 +  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    1.59 +proof -
    1.60 +  assume a: "sum_case f1 f2 = sum_case g1 g2"
    1.61 +  assume r: "f1 = g1 ==> f2 = g2 ==> P"
    1.62 +  show P
    1.63 +    apply (rule r)
    1.64 +     apply (rule ext)
    1.65 +     apply (cut_tac x = "Inl x" in a [THEN fun_cong])
    1.66 +     apply simp
    1.67 +    apply (rule ext)
    1.68 +    apply (cut_tac x = "Inr x" in a [THEN fun_cong])
    1.69 +    apply simp
    1.70 +    done
    1.71 +qed
    1.72 +
    1.73 +
    1.74 +subsection {* Further cases/induct rules for tuples *}
    1.75  
    1.76  lemma prod_cases3 [case_names fields, cases type]:
    1.77      "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.78 @@ -91,4 +128,67 @@
    1.79      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    1.80    by (cases x) blast
    1.81  
    1.82 +
    1.83 +subsection {* The option type *}
    1.84 +
    1.85 +datatype 'a option = None | Some 'a
    1.86 +
    1.87 +lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
    1.88 +  by (induct x) auto
    1.89 +
    1.90 +lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
    1.91 +  by (induct x) auto
    1.92 +
    1.93 +lemma option_caseE:
    1.94 +  "(case x of None => P | Some y => Q y) ==>
    1.95 +    (x = None ==> P ==> R) ==>
    1.96 +    (!!y. x = Some y ==> Q y ==> R) ==> R"
    1.97 +  by (cases x) simp_all
    1.98 +
    1.99 +
   1.100 +subsubsection {* Operations *}
   1.101 +
   1.102 +consts
   1.103 +  the :: "'a option => 'a"
   1.104 +primrec
   1.105 +  "the (Some x) = x"
   1.106 +
   1.107 +consts
   1.108 +  o2s :: "'a option => 'a set"
   1.109 +primrec
   1.110 +  "o2s None = {}"
   1.111 +  "o2s (Some x) = {x}"
   1.112 +
   1.113 +lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   1.114 +  by simp
   1.115 +
   1.116 +ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
   1.117 +
   1.118 +lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   1.119 +  by (cases xo) auto
   1.120 +
   1.121 +lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   1.122 +  by (cases xo) auto
   1.123 +
   1.124 +
   1.125 +constdefs
   1.126 +  option_map :: "('a => 'b) => ('a option => 'b option)"
   1.127 +  "option_map == %f y. case y of None => None | Some x => Some (f x)"
   1.128 +
   1.129 +lemma option_map_None [simp]: "option_map f None = None"
   1.130 +  by (simp add: option_map_def)
   1.131 +
   1.132 +lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
   1.133 +  by (simp add: option_map_def)
   1.134 +
   1.135 +lemma option_map_eq_Some [iff]:
   1.136 +    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   1.137 +  by (simp add: option_map_def split add: option.split)
   1.138 +
   1.139 +lemma option_map_o_sum_case [simp]:
   1.140 +    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   1.141 +  apply (rule ext)
   1.142 +  apply (simp split add: sum.split)
   1.143 +  done
   1.144 +
   1.145  end