src/HOL/BNF_Least_Fixpoint.thy
changeset 58147 967444d352b8
parent 58136 10f92532f128
child 58159 e3d1912a0c8f
equal deleted inserted replaced
58146:d91c1e50b36e 58147:967444d352b8
    88   from surj_on obtain x where "x \<in> X" and "y = f x" by blast
    88   from surj_on obtain x where "x \<in> X" and "y = f x" by blast
    89   thus "g1 y = g2 y" using eq_on by simp
    89   thus "g1 y = g2 y" using eq_on by simp
    90 qed
    90 qed
    91 
    91 
    92 lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
    92 lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
    93 unfolding wo_rel_def card_order_on_def by blast
    93   unfolding wo_rel_def card_order_on_def by blast
    94 
    94 
    95 lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
    95 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"
    96   \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
    96   unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
    97 unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
       
    98 
    97 
    99 lemma Card_order_trans:
    98 lemma Card_order_trans:
   100   "\<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"
    99   "\<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"
   101 unfolding card_order_on_def well_order_on_def linear_order_on_def
   100   unfolding card_order_on_def well_order_on_def linear_order_on_def
   102   partial_order_on_def preorder_on_def trans_def antisym_def by blast
   101     partial_order_on_def preorder_on_def trans_def antisym_def by blast
   103 
   102 
   104 lemma Cinfinite_limit2:
   103 lemma Cinfinite_limit2:
   105  assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
   104   assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
   106  shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
   105   shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
   107 proof -
   106 proof -
   108   from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
   107   from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
   109     unfolding card_order_on_def well_order_on_def linear_order_on_def
   108     unfolding card_order_on_def well_order_on_def linear_order_on_def
   110       partial_order_on_def preorder_on_def by auto
   109       partial_order_on_def preorder_on_def by auto
   111   obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
   110   obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
   130       with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
   129       with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
   131     qed
   130     qed
   132   qed
   131   qed
   133 qed
   132 qed
   134 
   133 
   135 lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
   134 lemma Cinfinite_limit_finite:
   136  \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
   135   "\<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)"
   137 proof (induct X rule: finite_induct)
   136 proof (induct X rule: finite_induct)
   138   case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
   137   case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
   139 next
   138 next
   140   case (insert x X)
   139   case (insert x X)
   141   then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
   140   then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
   151     apply (rule z(1))
   150     apply (rule z(1))
   152     done
   151     done
   153 qed
   152 qed
   154 
   153 
   155 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   154 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   156 by auto
   155   by auto
   157 
   156 
   158 lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
   157 lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
   159 
   158 
   160 lemma meta_spec2:
   159 lemma meta_spec2:
   161   assumes "(\<And>x y. PROP P x y)"
   160   assumes "(\<And>x y. PROP P x y)"