# HG changeset patch
# User blanchet
# Date 1407851339 -7200
# Node ID 2d037f8dc4d590df2bc8eec3b9d00aed1560b959
# Parent  a85e0ab840c1922193ca0a3a427e42d62b97264b
tuned whitespace

diff -r a85e0ab840c1 -r 2d037f8dc4d5 src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Tue Aug 12 15:48:59 2014 +0200
+++ b/src/HOL/BNF_GFP.thy	Tue Aug 12 15:48:59 2014 +0200
@@ -22,33 +22,33 @@
 *}
 
 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
+  by simp
 
 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (cases s) auto
+  by (cases s) auto
 
 lemma not_TrueE: "\<not> True \<Longrightarrow> P"
-by (erule notE, rule TrueI)
+  by (erule notE, rule TrueI)
 
 lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
-by fast
+  by fast
 
 lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
-by (auto split: sum.splits)
+  by (auto split: sum.splits)
 
 lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
-apply rule
- apply (rule ext, force split: sum.split)
-by (rule ext, metis case_sum_o_inj(2))
+  apply rule
+   apply (rule ext, force split: sum.split)
+  by (rule ext, metis case_sum_o_inj(2))
 
 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
-by fast
+  by fast
 
 lemma equiv_proj:
-  assumes e: "equiv A R" and "z \<in> R"
+  assumes e: "equiv A R" and m: "z \<in> R"
   shows "(proj R o fst) z = (proj R o snd) z"
 proof -
-  from assms(2) have z: "(fst z, snd z) \<in> R" by auto
+  from m have z: "(fst z, snd z) \<in> R" by auto
   with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
     unfolding equiv_def sym_def trans_def by blast+
   then show ?thesis unfolding proj_def[abs_def] by auto
@@ -58,93 +58,93 @@
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
 lemma Id_on_Gr: "Id_on A = Gr A id"
-unfolding Id_on_def Gr_def by auto
+  unfolding Id_on_def Gr_def by auto
 
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
-unfolding image2_def by auto
+  unfolding image2_def by auto
 
 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
-by auto
+  by auto
 
 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
-unfolding image2_def Gr_def by auto
+  unfolding image2_def Gr_def by auto
 
 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
-unfolding Gr_def by simp
+  unfolding Gr_def by simp
 
 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
-unfolding Gr_def by simp
+  unfolding Gr_def by simp
 
 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
-unfolding Gr_def by auto
+  unfolding Gr_def by auto
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
-by blast
+  by blast
 
 lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
-by blast
+  by blast
 
 lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
-unfolding fun_eq_iff by auto
+  unfolding fun_eq_iff by auto
 
 lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
-by auto
+  by auto
 
 lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
-by force
+  by force
 
 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
-unfolding fun_eq_iff by auto
+  unfolding fun_eq_iff by auto
 
 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
-unfolding fun_eq_iff by auto
+  unfolding fun_eq_iff by auto
 
 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
-unfolding Gr_def Grp_def fun_eq_iff by auto
+  unfolding Gr_def Grp_def fun_eq_iff by auto
 
 definition relImage where
-"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
+  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
 
 definition relInvImage where
-"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
+  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
 
 lemma relImage_Gr:
-"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
-unfolding relImage_def Gr_def relcomp_def by auto
+  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
+  unfolding relImage_def Gr_def relcomp_def by auto
 
 lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
-unfolding Gr_def relcomp_def image_def relInvImage_def by auto
+  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
 
 lemma relImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
-unfolding relImage_def by auto
+  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
+  unfolding relImage_def by auto
 
 lemma relInvImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
-unfolding relInvImage_def by auto
+  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
+  unfolding relInvImage_def by auto
 
 lemma relInvImage_Id_on:
-"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
-unfolding relInvImage_def Id_on_def by auto
+  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
+  unfolding relInvImage_def Id_on_def by auto
 
 lemma relInvImage_UNIV_relImage:
-"R \<subseteq> relInvImage UNIV (relImage R f) f"
-unfolding relInvImage_def relImage_def by auto
+  "R \<subseteq> relInvImage UNIV (relImage R f) f"
+  unfolding relInvImage_def relImage_def by auto
 
 lemma relImage_proj:
-assumes "equiv A R"
-shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
-unfolding relImage_def Id_on_def
-using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
-by (auto simp: proj_preserves)
+  assumes "equiv A R"
+  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
+  unfolding relImage_def Id_on_def
+  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
+  by (auto simp: proj_preserves)
 
 lemma relImage_relInvImage:
-assumes "R \<subseteq> f ` A <*> f ` A"
-shows "relImage (relInvImage A R f) f = R"
-using assms unfolding relImage_def relInvImage_def by fast
+  assumes "R \<subseteq> f ` A <*> f ` A"
+  shows "relImage (relInvImage A R f) f = R"
+  using assms unfolding relImage_def relInvImage_def by fast
 
 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
-by simp
+  by simp
 
 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
@@ -159,76 +159,75 @@
 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
 
 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
-unfolding Shift_def Succ_def by simp
+  unfolding Shift_def Succ_def by simp
 
 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
-unfolding Succ_def by simp
+  unfolding Succ_def by simp
 
 lemmas SuccE = SuccD[elim_format]
 
 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
-unfolding Succ_def by simp
+  unfolding Succ_def by simp
 
 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
-unfolding Shift_def by simp
+  unfolding Shift_def by simp
 
 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
-unfolding Succ_def Shift_def by auto
+  unfolding Succ_def Shift_def by auto
 
 lemma length_Cons: "length (x # xs) = Suc (length xs)"
-by simp
+  by simp
 
 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
-by simp
+  by simp
 
 (*injection into the field of a cardinal*)
 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
 
 lemma ex_toCard_pred:
-"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
-unfolding toCard_pred_def
-using card_of_ordLeq[of A "Field r"]
-      ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
-by blast
+  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
+  unfolding toCard_pred_def
+  using card_of_ordLeq[of A "Field r"]
+    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
+  by blast
 
 lemma toCard_pred_toCard:
   "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
-unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
+  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
 
-lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
-  toCard A r x = toCard A r y \<longleftrightarrow> x = y"
-using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
+lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
+  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
 
 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
 
 lemma fromCard_toCard:
-"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
-unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
+  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
+  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
 
 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
+  unfolding Field_card_of csum_def by auto
 
 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
+  unfolding Field_card_of csum_def by auto
 
 lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
-by auto
+  by auto
 
 lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
-by auto
+  by auto
 
 lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
-by auto
+  by auto
 
 lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
-by auto
+  by auto
 
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
-by simp
+  by simp
 
 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
-by auto
+  by auto
 
 definition image2p where
   "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
@@ -250,20 +249,21 @@
 
 lemma equiv_Eps_in:
 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
-apply (rule someI2_ex)
-using in_quotient_imp_non_empty by blast
+  apply (rule someI2_ex)
+  using in_quotient_imp_non_empty by blast
 
 lemma equiv_Eps_preserves:
-assumes ECH: "equiv A r" and X: "X \<in> A//r"
-shows "Eps (%x. x \<in> X) \<in> A"
-apply (rule in_mono[rule_format])
- using assms apply (rule in_quotient_imp_subset)
-by (rule equiv_Eps_in) (rule assms)+
+  assumes ECH: "equiv A r" and X: "X \<in> A//r"
+  shows "Eps (%x. x \<in> X) \<in> A"
+  apply (rule in_mono[rule_format])
+   using assms apply (rule in_quotient_imp_subset)
+  by (rule equiv_Eps_in) (rule assms)+
 
 lemma proj_Eps:
-assumes "equiv A r" and "X \<in> A//r"
-shows "proj r (Eps (%x. x \<in> X)) = X"
-unfolding proj_def proof auto
+  assumes "equiv A r" and "X \<in> A//r"
+  shows "proj r (Eps (%x. x \<in> X)) = X"
+unfolding proj_def
+proof auto
   fix x assume x: "x \<in> X"
   thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
 next
@@ -276,7 +276,7 @@
 lemma univ_commute:
 assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
 shows "(univ f) (proj r x) = f x"
-unfolding univ_def proof -
+proof (unfold univ_def)
   have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
@@ -285,9 +285,8 @@
 qed
 
 lemma univ_preserves:
-assumes ECH: "equiv A r" and RES: "f respects r" and
-        PRES: "\<forall> x \<in> A. f x \<in> B"
-shows "\<forall>X \<in> A//r. univ f X \<in> B"
+  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall> x \<in> A. f x \<in> B"
+  shows "\<forall>X \<in> A//r. univ f X \<in> B"
 proof
   fix X assume "X \<in> A//r"
   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast