src/HOL/BNF_LFP.thy
changeset 57987 ecb227b40907
parent 57698 afef6616cbae
child 57989 45873fcbbf2e
     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