# Theory Datatype

Up to index of Isabelle/HOL

theory Datatype
imports Datatype_Universe
uses [Datatype.ML]
begin

    (*  Title:      HOL/Datatype.thy
        ID:         $Id: Datatype.thy,v 1.15 2005/09/17 16:11:18 wenzelm Exp $
        Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    *)

    header {* Datatypes *}

    theory Datatype
    imports Datatype_Universe
    begin

    subsection {* Representing primitive types *}

    rep_datatype bool
      distinct True_not_False False_not_True
      induction bool_induct

    declare case_split [cases type: bool]
      -- "prefer plain propositional version"

    rep_datatype unit
      induction unit_induct

    rep_datatype prod
      inject Pair_eq
      induction prod_induct

    rep_datatype sum
      distinct Inl_not_Inr Inr_not_Inl
      inject Inl_eq Inr_eq
      induction sum_induct

    ML {*
      val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
      bind_thm ("sum_case_Inl", sum_case_Inl);
      bind_thm ("sum_case_Inr", sum_case_Inr);
    *} -- {* compatibility *}

    lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
      apply (rule_tac s = s in sumE)
       apply (erule ssubst)
       apply (rule sum_case_Inl)
      apply (erule ssubst)
      apply (rule sum_case_Inr)
      done

    lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
      -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
      by (erule arg_cong)

    lemma sum_case_inject:
      "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    proof -
      assume a: "sum_case f1 f2 = sum_case g1 g2"
      assume r: "f1 = g1 ==> f2 = g2 ==> P"
      show P
        apply (rule r)
         apply (rule ext)
         apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
        apply (rule ext)
        apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
        done
    qed

    constdefs
      Suml :: "('a => 'c) => 'a + 'b => 'c"
      "Suml == (%f. sum_case f arbitrary)"

      Sumr :: "('b => 'c) => 'a + 'b => 'c"
      "Sumr == sum_case arbitrary"

    lemma Suml_inject: "Suml f = Suml g ==> f = g"
      by (unfold Suml_def) (erule sum_case_inject)

    lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
      by (unfold Sumr_def) (erule sum_case_inject)

    subsection {* Finishing the datatype package setup *}

    text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    hide type node item

    subsection {* Further cases/induct rules for tuples *}

    lemma prod_cases3 [case_names fields, cases type]:
        "(!!a b c. y = (a, b, c) ==> P) ==> P"
      apply (cases y)
      apply (case_tac b, blast)
      done

    lemma prod_induct3 [case_names fields, induct type]:
        "(!!a b c. P (a, b, c)) ==> P x"
      by (cases x) blast

    lemma prod_cases4 [case_names fields, cases type]:
        "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
      apply (cases y)
      apply (case_tac c, blast)
      done

    lemma prod_induct4 [case_names fields, induct type]:
        "(!!a b c d. P (a, b, c, d)) ==> P x"
      by (cases x) blast

    lemma prod_cases5 [case_names fields, cases type]:
        "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
      apply (cases y)
      apply (case_tac d, blast)
      done

    lemma prod_induct5 [case_names fields, induct type]:
        "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
      by (cases x) blast

    lemma prod_cases6 [case_names fields, cases type]:
        "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
      apply (cases y)
      apply (case_tac e, blast)
      done

    lemma prod_induct6 [case_names fields, induct type]:
        "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
      by (cases x) blast

    lemma prod_cases7 [case_names fields, cases type]:
        "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
      apply (cases y)
      apply (case_tac f, blast)
      done

    lemma prod_induct7 [case_names fields, induct type]:
        "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
      by (cases x) blast

    subsection {* The option type *}

    datatype 'a option = None | Some 'a

    lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
      by (induct x) auto

    lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
      by (induct x) auto

    lemma option_caseE:
      "(case x of None => P | Some y => Q y) ==>
        (x = None ==> P ==> R) ==>
        (!!y. x = Some y ==> Q y ==> R) ==> R"
      by (cases x) simp_all

    subsubsection {* Operations *}

    consts
      the :: "'a option => 'a"
    primrec
      "the (Some x) = x"

    consts
      o2s :: "'a option => 'a set"
    primrec
      "o2s None = {}"
      "o2s (Some x) = {x}"

    lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
      by simp

    ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}

    lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
      by (cases xo) auto

    lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
      by (cases xo) auto

    constdefs
      option_map :: "('a => 'b) => ('a option => 'b option)"
      "option_map == %f y. case y of None => None | Some x => Some (f x)"

    lemma option_map_None [simp]: "option_map f None = None"
      by (simp add: option_map_def)

    lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
      by (simp add: option_map_def)

    lemma option_map_is_None[iff]:
     "(option_map f opt = None) = (opt = None)"
    by (simp add: option_map_def split add: option.split)

    lemma option_map_eq_Some [iff]:
        "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
    by (simp add: option_map_def split add: option.split)

    lemma option_map_comp:
     "option_map f (option_map g opt) = option_map (f o g) opt"
    by (simp add: option_map_def split add: option.split)

    lemma option_map_o_sum_case [simp]:
        "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
      apply (rule ext)
      apply (simp split add: sum.split)
      done

    lemmas [code] = imp_conv_disj

    end

### Representing primitive types

theorem sum_case_Inl:

      sum_case f1.0 f2.0 (Inl a) = f1.0 a

theorem sum_case_Inr:

      sum_case f1.0 f2.0 (Inr b) = f2.0 b

lemma surjective_sum:

      (case s of Inl x => f (Inl x) | Inr y => f (Inr y)) = f s

lemma sum_case_weak_cong:

      s = t ==> sum_case f g s = sum_case f g t

lemma sum_case_inject:

      [| sum_case f1.0 f2.0 = sum_case g1.0 g2.0;
         [| f1.0 = g1.0; f2.0 = g2.0 |] ==> P |]
      ==> P

lemma Suml_inject:

      Suml f = Suml g ==> f = g

lemma Sumr_inject:

      Sumr f = Sumr g ==> f = g

### Finishing the datatype package setup

### Further cases/induct rules for tuples

lemma prod_cases3:

      (!!a b c. y = (a, b, c) ==> P) ==> P

lemma prod_induct3:

      (!!a b c. P (a, b, c)) ==> P x

lemma prod_cases4:

      (!!a b c d. y = (a, b, c, d) ==> P) ==> P

lemma prod_induct4:

      (!!a b c d. P (a, b, c, d)) ==> P x

lemma prod_cases5:

      (!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P

lemma prod_induct5:

      (!!a b c d e. P (a, b, c, d, e)) ==> P x

lemma prod_cases6:

      (!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P

lemma prod_induct6:

      (!!a b c d e f. P (a, b, c, d, e, f)) ==> P x

lemma prod_cases7:

      (!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P

lemma prod_induct7:

      (!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x

### The option type

lemma not_None_eq:

      (x ≠ None) = (∃y. x = Some y)

lemma not_Some_eq:

      (∀y. x ≠ Some y) = (x = None)

lemma option_caseE:

      [| case x of None => P | Some y => Q y; [| x = None; P |] ==> R;
         !!y. [| x = Some y; Q y |] ==> R |]
      ==> R

#### Operations

lemma ospec:

      [| ∀x∈o2s A. P x; A = Some x |] ==> P x

lemma elem_o2s:

      (x ∈ o2s xo) = (xo = Some x)

lemma o2s_empty_eq:

      (o2s xo = {}) = (xo = None)

lemma option_map_None:

      option_map f None = None

lemma option_map_Some:

      option_map f (Some x) = Some (f x)

lemma option_map_is_None:

      (option_map f opt = None) = (opt = None)

lemma option_map_eq_Some:

      (option_map f xo = Some y) = (∃z. xo = Some z ∧ f z = y)

lemma option_map_comp:

      option_map f (option_map g opt) = option_map (f o g) opt

lemma option_map_o_sum_case:

      option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)

lemmas

      (P --> Q) = (¬ P ∨ Q)

lemmas

      (P --> Q) = (¬ P ∨ Q)