src/HOL/BNF_Least_Fixpoint.thy
 changeset 58147 967444d352b8 parent 58136 10f92532f128 child 58159 e3d1912a0c8f
equal 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)"`