# HG changeset patch
# User wenzelm
# Date 1004133605 -7200
# Node ID 3d1780208bf3c91aa98fff0bff70145627eefa33
# Parent  f98623fdf6ef406f6625eb3fa4d05bbf9cd3feb3
made new-style theory;
tuned;

diff -r f98623fdf6ef -r 3d1780208bf3 src/HOL/Datatype.ML
--- a/src/HOL/Datatype.ML	Fri Oct 26 23:59:13 2001 +0200
+++ b/src/HOL/Datatype.ML	Sat Oct 27 00:00:05 2001 +0200
@@ -1,9 +1,68 @@
 (*  Title:      HOL/Datatype.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1999  TU Muenchen
+    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
+(** legacy ML bindings **)
+
+structure bool =
+struct
+  val distinct = thms "bool.distinct";
+  val inject = thms "bool.inject";
+  val exhaust = thm "bool.exhaust";
+  val cases = thms "bool.cases";
+  val split = thm "bool.split";
+  val split_asm = thm "bool.split_asm";
+  val induct = thm "bool.induct";
+  val recs = thms "bool.recs";
+  val simps = thms "bool.simps";
+  val size = thms "bool.size";
+end;
+
+structure sum =
+struct
+  val distinct = thms "sum.distinct";
+  val inject = thms "sum.inject";
+  val exhaust = thm "sum.exhaust";
+  val cases = thms "sum.cases";
+  val split = thm "sum.split";
+  val split_asm = thm "sum.split_asm";
+  val induct = thm "sum.induct";
+  val recs = thms "sum.recs";
+  val simps = thms "sum.simps";
+  val size = thms "sum.size";
+end;
+
+structure unit =
+struct
+  val distinct = thms "unit.distinct";
+  val inject = thms "unit.inject";
+  val exhaust = thm "unit.exhaust";
+  val cases = thms "unit.cases";
+  val split = thm "unit.split";
+  val split_asm = thm "unit.split_asm";
+  val induct = thm "unit.induct";
+  val recs = thms "unit.recs";
+  val simps = thms "unit.simps";
+  val size = thms "unit.size";
+end;
+
+structure prod =
+struct
+  val distinct = thms "prod.distinct";
+  val inject = thms "prod.inject";
+  val exhaust = thm "prod.exhaust";
+  val cases = thms "prod.cases";
+  val split = thm "prod.split";
+  val split_asm = thm "prod.split_asm";
+  val induct = thm "prod.induct";
+  val recs = thms "prod.recs";
+  val simps = thms "prod.simps";
+  val size = thms "prod.size";
+end;
+
+
 (** sum_case -- the selection operator for sums **)
 
 (*compatibility*)
@@ -12,7 +71,7 @@
 bind_thm ("sum_case_Inr", sum_case_Inr);
 
 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
-by (EVERY1 [res_inst_tac [("s","s")] sumE, 
+by (EVERY1 [res_inst_tac [("s","s")] sumE,
             etac ssubst, rtac sum_case_Inl,
             etac ssubst, rtac sum_case_Inr]);
 qed "surjective_sum";
diff -r f98623fdf6ef -r 3d1780208bf3 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Oct 26 23:59:13 2001 +0200
+++ b/src/HOL/Datatype.thy	Sat Oct 27 00:00:05 2001 +0200
@@ -1,25 +1,95 @@
 (*  Title:      HOL/Datatype.thy
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-Datatype = Datatype_Universe +
+header {* Datatype package setup -- final stage *}
+
+theory Datatype = Datatype_Universe:
+
+(*belongs to theory Datatype_Universe; hides popular names *)
+hide const Node Atom Leaf Numb Lim Funs Split Case
+hide type node item
+
+
+subsection {* Representing primitive types *}
 
 rep_datatype bool
-  distinct True_not_False, False_not_True
-  induct   bool_induct
+  distinct True_not_False False_not_True
+  induction bool_induct
+
+declare case_split [cases type: bool]
+  -- "prefer plain propositional version"
+
 
 rep_datatype sum
-  distinct Inl_not_Inr, Inr_not_Inl
-  inject   Inl_eq, Inr_eq
-  induct   sum_induct
+  distinct Inl_not_Inr Inr_not_Inl
+  inject Inl_eq Inr_eq
+  induction sum_induct
+
+rep_datatype unit
+  induction unit_induct
 
 rep_datatype prod
-  inject   Pair_eq
-  induct   prod_induct
+  inject Pair_eq
+  induction prod_induct
+
+text {* Further cases/induct rules for 3--7 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)
+  apply 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)
+  apply 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
 
-rep_datatype unit
-  induct   unit_induct
+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)
+  apply 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)
+  apply 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)
+  apply 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
 
 end