src/HOL/BNF_Least_Fixpoint.thy
changeset 58147 967444d352b8
parent 58136 10f92532f128
child 58159 e3d1912a0c8f
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Wed Sep 03 00:06:18 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Wed Sep 03 00:06:19 2014 +0200
     1.3 @@ -90,20 +90,19 @@
     1.4  qed
     1.5  
     1.6  lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
     1.7 -unfolding wo_rel_def card_order_on_def by blast
     1.8 +  unfolding wo_rel_def card_order_on_def by blast
     1.9  
    1.10 -lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
    1.11 -  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
    1.12 -unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
    1.13 +lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow> \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
    1.14 +  unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
    1.15  
    1.16  lemma Card_order_trans:
    1.17    "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
    1.18 -unfolding card_order_on_def well_order_on_def linear_order_on_def
    1.19 -  partial_order_on_def preorder_on_def trans_def antisym_def by blast
    1.20 +  unfolding card_order_on_def well_order_on_def linear_order_on_def
    1.21 +    partial_order_on_def preorder_on_def trans_def antisym_def by blast
    1.22  
    1.23  lemma Cinfinite_limit2:
    1.24 - assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
    1.25 - shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
    1.26 +  assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
    1.27 +  shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
    1.28  proof -
    1.29    from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
    1.30      unfolding card_order_on_def well_order_on_def linear_order_on_def
    1.31 @@ -132,8 +131,8 @@
    1.32    qed
    1.33  qed
    1.34  
    1.35 -lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
    1.36 - \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
    1.37 +lemma Cinfinite_limit_finite:
    1.38 +  "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk> \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
    1.39  proof (induct X rule: finite_induct)
    1.40    case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
    1.41  next
    1.42 @@ -153,7 +152,7 @@
    1.43  qed
    1.44  
    1.45  lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
    1.46 -by auto
    1.47 +  by auto
    1.48  
    1.49  lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
    1.50