# HG changeset patch
# User blanchet
# Date 1408382190 -7200
# Node ID ecb227b40907190561616ca24f1f1d8aa185545b
# Parent  0d60b9e5848763619198ba68346f14be4284724e
set attributes on 'set_cases' theorem

diff -r 0d60b9e58487 -r ecb227b40907 src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Aug 18 18:48:39 2014 +0200
+++ b/src/HOL/BNF_LFP.thy	Mon Aug 18 19:16:30 2014 +0200
@@ -17,37 +17,37 @@
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
-by blast
+  by blast
 
 lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
-by blast
+  by blast
 
 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
-by auto
+  by auto
 
 lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
-by auto
+  by auto
 
 lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
-unfolding underS_def by simp
+  unfolding underS_def by simp
 
 lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
-unfolding underS_def by simp
+  unfolding underS_def by simp
 
 lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
-unfolding underS_def Field_def by auto
+  unfolding underS_def Field_def by auto
 
 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
-unfolding Field_def by auto
+  unfolding Field_def by auto
 
 lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
-using fst_convol unfolding convol_def by simp
+  using fst_convol unfolding convol_def by simp
 
 lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
-using snd_convol unfolding convol_def by simp
+  using snd_convol unfolding convol_def by simp
 
 lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
-unfolding convol_def by auto
+  unfolding convol_def by auto
 
 lemma convol_expand_snd':
   assumes "(fst o f = g)"
@@ -59,11 +59,12 @@
   moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
   ultimately show ?thesis by simp
 qed
+
 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
-unfolding bij_betw_def by auto
+  unfolding bij_betw_def by auto
 
 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
-unfolding bij_betw_def by auto
+  unfolding bij_betw_def by auto
 
 lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
   (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
@@ -77,7 +78,7 @@
   "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
     \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
     \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
-unfolding bij_betw_def inj_on_def by blast
+  unfolding bij_betw_def inj_on_def by blast
 
 lemma surj_fun_eq:
   assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
@@ -192,6 +193,8 @@
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
 
+datatype_new 'a l = N | C 'a "'a l"
+
 hide_fact (open) id_transfer
 
 end
diff -r 0d60b9e58487 -r ecb227b40907 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 18:48:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 19:16:30 2014 +0200
@@ -1574,9 +1574,13 @@
                             |> singleton (Proof_Context.export names_lthy lthy)
                             |> Thm.close_derivation
                             |> rotate_prems ~1;
+
+                          val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
+                          val cases_set_attr =
+                            Attrib.internal (K (Induct.cases_pred (name_of_set set)));
                         in
-                          (thm, [](* TODO: [@{attributes [elim?]},
-                            Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *))
+                          (* TODO: @{attributes [elim?]} *)
+                          (thm, [consumes_attr, cases_set_attr])
                         end) setAs)
                     end;