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