src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Tue Sep 25 10:27:43 2007 +0200
+++ b/src/HOL/Product_Type.thy	Tue Sep 25 12:16:08 2007 +0200
@@ -7,10 +7,24 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Typedef Fun
-uses ("Tools/split_rule.ML")
+imports Inductive
+uses
+  ("Tools/split_rule.ML")
+  ("Tools/inductive_set_package.ML")
+  ("Tools/inductive_realizer.ML")
+  ("Tools/datatype_realizer.ML")
 begin
 
+subsection {* @{typ bool} is a datatype *}
+
+rep_datatype bool
+  distinct True_not_False False_not_True
+  induction bool_induct
+
+declare case_split [cases type: bool]
+  -- "prefer plain propositional version"
+
+
 subsection {* Unit *}
 
 typedef unit = "{True}"
@@ -18,9 +32,10 @@
   show "True : ?unit" ..
 qed
 
-constdefs
+definition
   Unity :: unit    ("'(')")
-  "() == Abs_unit True"
+where
+  "() = Abs_unit True"
 
 lemma unit_eq [noatp]: "u = ()"
   by (induct u) (simp add: unit_def Unity_def)
@@ -32,23 +47,26 @@
 
 ML_setup {*
   val unit_eq_proc =
-    let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
-      Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"]
+    let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
+      Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
       (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
     end;
 
   Addsimprocs [unit_eq_proc];
 *}
 
+lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
+  by simp
+
+rep_datatype unit
+  induction unit_induct
+
 lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
   by simp
 
 lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
   by (rule triv_forall_equality)
 
-lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
-  by simp
-
 text {*
   This rewrite counters the effect of @{text unit_eq_proc} on @{term
   [source] "%u::unit. f u"}, replacing it by @{term [source]
@@ -84,7 +102,6 @@
 
 local
 
-
 subsubsection {* Definitions *}
 
 global
@@ -343,6 +360,10 @@
 lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
   by fast
 
+rep_datatype prod
+  inject Pair_eq
+  induction prod_induct
+
 lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
   by fast
 
@@ -765,6 +786,77 @@
 setup SplitRule.setup
 
 
+
+lemmas prod_caseI = prod.cases [THEN iffD2, standard]
+
+lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
+  by auto
+
+lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
+  by (auto simp: split_tupled_all)
+
+lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+  by (induct p) auto
+
+lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+  by (induct p) auto
+
+lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
+  by (simp add: expand_fun_eq)
+
+declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
+declare prod_caseE' [elim!] prod_caseE [elim!]
+
+lemma prod_case_split [code post]:
+  "prod_case = split"
+  by (auto simp add: expand_fun_eq)
+
+lemmas [code inline] = prod_case_split [symmetric]
+
+
+subsection {* Further cases/induct rules for tuples *}
+
+lemma prod_cases3 [cases type]:
+  obtains (fields) a b c where "y = (a, b, c)"
+  by (cases y, case_tac b) blast
+
+lemma prod_induct3 [case_names fields, induct type]:
+    "(!!a b c. P (a, b, c)) ==> P x"
+  by (cases x) blast
+
+lemma prod_cases4 [cases type]:
+  obtains (fields) a b c d where "y = (a, b, c, d)"
+  by (cases y, case_tac c) blast
+
+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 [cases type]:
+  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
+  by (cases y, case_tac d) blast
+
+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 [cases type]:
+  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
+  by (cases y, case_tac e) blast
+
+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 [cases type]:
+  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
+  by (cases y, case_tac f) blast
+
+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 {* Further lemmas *}
 
 lemma
@@ -914,6 +1006,9 @@
 end
 *}
 
+
+subsection {* Legacy bindings *}
+
 ML {*
 val Collect_split = thm "Collect_split";
 val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
@@ -1011,4 +1106,16 @@
 val unit_induct = thm "unit_induct";
 *}
 
+
+subsection {* Further inductive packages *}
+
+use "Tools/inductive_realizer.ML"
+setup InductiveRealizer.setup
+
+use "Tools/inductive_set_package.ML"
+setup InductiveSetPackage.setup
+
+use "Tools/datatype_realizer.ML"
+setup DatatypeRealizer.setup
+
 end