--- a/src/HOL/Product_Type.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Product_Type.thy Wed Feb 12 08:35:56 2014 +0100
@@ -25,8 +25,6 @@
-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
setup {* Sign.mandatory_path "bool" *}
-declare old.bool.cases[simp del]
-
lemmas induct = old.bool.induct
lemmas inducts = old.bool.inducts
lemmas recs = old.bool.recs
@@ -95,8 +93,6 @@
-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
setup {* Sign.mandatory_path "unit" *}
-declare old.unit.cases[simp del]
-
lemmas induct = old.unit.induct
lemmas inducts = old.unit.inducts
lemmas recs = old.unit.recs
@@ -203,15 +199,7 @@
setup {* Sign.mandatory_path "old" *}
rep_datatype Pair
-proof -
- fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
- assume "\<And>a b. P (Pair a b)"
- then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
-next
- fix a c :: 'a and b d :: 'b
- show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
- by (rule prod.inject)
-qed
+by (erule prod_cases) (rule prod.inject)
setup {* Sign.parent_path *}
@@ -220,7 +208,6 @@
declare
old.prod.inject[iff del]
- old.prod.cases[simp del]
lemmas induct = old.prod.induct
lemmas inducts = old.prod.inducts
--- a/src/HOL/Sum_Type.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Sum_Type.thy Wed Feb 12 08:35:56 2014 +0100
@@ -107,7 +107,6 @@
declare
old.sum.inject[iff del]
old.sum.distinct(1)[simp del, induct_simp del]
- old.sum.cases[simp del]
lemmas induct = old.sum.induct
lemmas inducts = old.sum.inducts
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Feb 12 08:35:56 2014 +0100
@@ -271,6 +271,7 @@
let
val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
+ val ctxt = Proof_Context.init_global thy;
val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
val descr' = flat descr;
@@ -288,49 +289,62 @@
val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
- val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
+ val case_names0 = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
(* define case combinators via primrec combinators *)
- fun def_case ((((i, (_, _, constrs)), T), name), recname) (defs, thy) =
- let
- val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
- let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
- val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
- val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
- val frees = take (length cargs) frees';
- val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j;
- in
- (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
- end) (constrs ~~ (1 upto length constrs)));
+ fun def_case ((((i, (_, _, constrs)), T as Type (Tcon, _)), name), recname) (defs, thy) =
+ if is_some (Ctr_Sugar.ctr_sugar_of ctxt Tcon) then
+ (defs, thy)
+ else
+ let
+ val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
+ let
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
+ val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
+ val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
+ val frees = take (length cargs) frees';
+ val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j;
+ in
+ (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
+ end) (constrs ~~ (1 upto length constrs)));
- val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
- val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
- val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
- val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
- val def =
- (Binding.name (Thm.def_name (Long_Name.base_name name)),
- Logic.mk_equals (Const (name, caseT),
- fold_rev lambda fns1
- (list_comb (reccomb,
- flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
- val ([def_thm], thy') =
- thy
- |> Sign.declare_const_global decl |> snd
- |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
- in (defs @ [def_thm], thy') end;
+ val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
+ val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
+ val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
+ val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
+ val def =
+ (Binding.name (Thm.def_name (Long_Name.base_name name)),
+ Logic.mk_equals (Const (name, caseT),
+ fold_rev lambda fns1
+ (list_comb (reccomb,
+ flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
+ val ([def_thm], thy') =
+ thy
+ |> Sign.declare_const_global decl |> snd
+ |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
+ in (defs @ [def_thm], thy') end;
val (case_defs, thy2) =
- fold def_case (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names)
+ fold def_case (hd descr ~~ newTs ~~ case_names0 ~~ take (length newTs) reccomb_names)
([], thy1);
- fun prove_case _ t =
+ fun prove_case t =
Goal.prove_sorry_global thy2 [] [] t (fn {context = ctxt, ...} =>
EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]);
+ fun prove_cases (Type (Tcon, _)) ts =
+ (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
+ SOME {case_thms, ...} => case_thms
+ | NONE => map prove_case ts);
+
val case_thms =
- map2 (map o prove_case) new_type_names (Datatype_Prop.make_cases case_names descr thy2);
+ map2 prove_cases newTs (Datatype_Prop.make_cases case_names0 descr thy2);
+
+ fun case_name_of (th :: _) =
+ fst (dest_Const (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))));
+
+ val case_names = map case_name_of case_thms;
in
thy2
|> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)