src/HOL/Datatype.thy
changeset 24699 c6674504103f
parent 24286 7619080e49f0
child 24728 e2b3a1065676
     1.1 --- a/src/HOL/Datatype.thy	Tue Sep 25 10:27:43 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Sep 25 12:16:08 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Nat Sum_Type
     1.8 +imports Nat
     1.9  begin
    1.10  
    1.11  typedef (Node)
    1.12 @@ -537,52 +537,7 @@
    1.13  
    1.14  section {* Datatypes *}
    1.15  
    1.16 -subsection {* Representing primitive types *}
    1.17 -
    1.18 -rep_datatype bool
    1.19 -  distinct True_not_False False_not_True
    1.20 -  induction bool_induct
    1.21 -
    1.22 -declare case_split [cases type: bool]
    1.23 -  -- "prefer plain propositional version"
    1.24 -
    1.25 -lemma size_bool [code func]:
    1.26 -  "size (b\<Colon>bool) = 0" by (cases b) auto
    1.27 -
    1.28 -rep_datatype unit
    1.29 -  induction unit_induct
    1.30 -
    1.31 -rep_datatype prod
    1.32 -  inject Pair_eq
    1.33 -  induction prod_induct
    1.34 -
    1.35 -declare prod.size [noatp]
    1.36 -
    1.37 -lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    1.38 -
    1.39 -lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
    1.40 -  by auto
    1.41 -
    1.42 -lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
    1.43 -  by (auto simp: split_tupled_all)
    1.44 -
    1.45 -lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
    1.46 -  by (induct p) auto
    1.47 -
    1.48 -lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
    1.49 -  by (induct p) auto
    1.50 -
    1.51 -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
    1.52 -  by (simp add: expand_fun_eq)
    1.53 -
    1.54 -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
    1.55 -declare prod_caseE' [elim!] prod_caseE [elim!]
    1.56 -
    1.57 -lemma prod_case_split [code post]:
    1.58 -  "prod_case = split"
    1.59 -  by (auto simp add: expand_fun_eq)
    1.60 -
    1.61 -lemmas [code inline] = prod_case_split [symmetric]
    1.62 +subsection {* Representing sums *}
    1.63  
    1.64  rep_datatype sum
    1.65    distinct Inl_not_Inr Inr_not_Inl
    1.66 @@ -637,49 +592,6 @@
    1.67  hide (open) const Suml Sumr
    1.68  
    1.69  
    1.70 -subsection {* Further cases/induct rules for tuples *}
    1.71 -
    1.72 -lemma prod_cases3 [cases type]:
    1.73 -  obtains (fields) a b c where "y = (a, b, c)"
    1.74 -  by (cases y, case_tac b) blast
    1.75 -
    1.76 -lemma prod_induct3 [case_names fields, induct type]:
    1.77 -    "(!!a b c. P (a, b, c)) ==> P x"
    1.78 -  by (cases x) blast
    1.79 -
    1.80 -lemma prod_cases4 [cases type]:
    1.81 -  obtains (fields) a b c d where "y = (a, b, c, d)"
    1.82 -  by (cases y, case_tac c) blast
    1.83 -
    1.84 -lemma prod_induct4 [case_names fields, induct type]:
    1.85 -    "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.86 -  by (cases x) blast
    1.87 -
    1.88 -lemma prod_cases5 [cases type]:
    1.89 -  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
    1.90 -  by (cases y, case_tac d) blast
    1.91 -
    1.92 -lemma prod_induct5 [case_names fields, induct type]:
    1.93 -    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.94 -  by (cases x) blast
    1.95 -
    1.96 -lemma prod_cases6 [cases type]:
    1.97 -  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
    1.98 -  by (cases y, case_tac e) blast
    1.99 -
   1.100 -lemma prod_induct6 [case_names fields, induct type]:
   1.101 -    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   1.102 -  by (cases x) blast
   1.103 -
   1.104 -lemma prod_cases7 [cases type]:
   1.105 -  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
   1.106 -  by (cases y, case_tac f) blast
   1.107 -
   1.108 -lemma prod_induct7 [case_names fields, induct type]:
   1.109 -    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.110 -  by (cases x) blast
   1.111 -
   1.112 -
   1.113  subsection {* The option datatype *}
   1.114  
   1.115  datatype 'a option = None | Some 'a