set attributes on 'set_cases' theorem
authorblanchet
Mon Aug 18 19:16:30 2014 +0200 (2014-08-18)
changeset 57987ecb227b40907
parent 57986 0d60b9e58487
child 57988 030ff4ceb6c3
set attributes on 'set_cases' theorem
src/HOL/BNF_LFP.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Aug 18 18:48:39 2014 +0200
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Aug 18 19:16:30 2014 +0200
     1.3 @@ -17,37 +17,37 @@
     1.4  begin
     1.5  
     1.6  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
     1.7 -by blast
     1.8 +  by blast
     1.9  
    1.10  lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
    1.11 -by blast
    1.12 +  by blast
    1.13  
    1.14  lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
    1.15 -by auto
    1.16 +  by auto
    1.17  
    1.18  lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
    1.19 -by auto
    1.20 +  by auto
    1.21  
    1.22  lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
    1.23 -unfolding underS_def by simp
    1.24 +  unfolding underS_def by simp
    1.25  
    1.26  lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
    1.27 -unfolding underS_def by simp
    1.28 +  unfolding underS_def by simp
    1.29  
    1.30  lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
    1.31 -unfolding underS_def Field_def by auto
    1.32 +  unfolding underS_def Field_def by auto
    1.33  
    1.34  lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
    1.35 -unfolding Field_def by auto
    1.36 +  unfolding Field_def by auto
    1.37  
    1.38  lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
    1.39 -using fst_convol unfolding convol_def by simp
    1.40 +  using fst_convol unfolding convol_def by simp
    1.41  
    1.42  lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    1.43 -using snd_convol unfolding convol_def by simp
    1.44 +  using snd_convol unfolding convol_def by simp
    1.45  
    1.46  lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    1.47 -unfolding convol_def by auto
    1.48 +  unfolding convol_def by auto
    1.49  
    1.50  lemma convol_expand_snd':
    1.51    assumes "(fst o f = g)"
    1.52 @@ -59,11 +59,12 @@
    1.53    moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    1.54    ultimately show ?thesis by simp
    1.55  qed
    1.56 +
    1.57  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    1.58 -unfolding bij_betw_def by auto
    1.59 +  unfolding bij_betw_def by auto
    1.60  
    1.61  lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
    1.62 -unfolding bij_betw_def by auto
    1.63 +  unfolding bij_betw_def by auto
    1.64  
    1.65  lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
    1.66    (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    1.67 @@ -77,7 +78,7 @@
    1.68    "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
    1.69      \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
    1.70      \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
    1.71 -unfolding bij_betw_def inj_on_def by blast
    1.72 +  unfolding bij_betw_def inj_on_def by blast
    1.73  
    1.74  lemma surj_fun_eq:
    1.75    assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
    1.76 @@ -192,6 +193,8 @@
    1.77  ML_file "Tools/BNF/bnf_lfp_compat.ML"
    1.78  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
    1.79  
    1.80 +datatype_new 'a l = N | C 'a "'a l"
    1.81 +
    1.82  hide_fact (open) id_transfer
    1.83  
    1.84  end
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 18:48:39 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 19:16:30 2014 +0200
     2.3 @@ -1574,9 +1574,13 @@
     2.4                              |> singleton (Proof_Context.export names_lthy lthy)
     2.5                              |> Thm.close_derivation
     2.6                              |> rotate_prems ~1;
     2.7 +
     2.8 +                          val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
     2.9 +                          val cases_set_attr =
    2.10 +                            Attrib.internal (K (Induct.cases_pred (name_of_set set)));
    2.11                          in
    2.12 -                          (thm, [](* TODO: [@{attributes [elim?]},
    2.13 -                            Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *))
    2.14 +                          (* TODO: @{attributes [elim?]} *)
    2.15 +                          (thm, [consumes_attr, cases_set_attr])
    2.16                          end) setAs)
    2.17                      end;
    2.18