diff -r d91c1e50b36e -r 967444d352b8 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Wed Sep 03 00:06:18 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Wed Sep 03 00:06:19 2014 +0200 @@ -90,20 +90,19 @@ qed lemma Card_order_wo_rel: "Card_order r \ wo_rel r" -unfolding wo_rel_def card_order_on_def by blast + unfolding wo_rel_def card_order_on_def by blast -lemma Cinfinite_limit: "\x \ Field r; Cinfinite r\ \ - \y \ Field r. x \ y \ (x, y) \ r" -unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) +lemma Cinfinite_limit: "\x \ Field r; Cinfinite r\ \ \y \ Field r. x \ y \ (x, y) \ r" + unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) lemma Card_order_trans: "\Card_order r; x \ y; (x, y) \ r; y \ z; (y, z) \ r\ \ x \ z \ (x, z) \ r" -unfolding card_order_on_def well_order_on_def linear_order_on_def - partial_order_on_def preorder_on_def trans_def antisym_def by blast + unfolding card_order_on_def well_order_on_def linear_order_on_def + partial_order_on_def preorder_on_def trans_def antisym_def by blast lemma Cinfinite_limit2: - assumes x1: "x1 \ Field r" and x2: "x2 \ Field r" and r: "Cinfinite r" - shows "\y \ Field r. (x1 \ y \ (x1, y) \ r) \ (x2 \ y \ (x2, y) \ r)" + assumes x1: "x1 \ Field r" and x2: "x2 \ Field r" and r: "Cinfinite r" + shows "\y \ Field r. (x1 \ y \ (x1, y) \ r) \ (x2 \ y \ (x2, y) \ r)" proof - from r have trans: "trans r" and total: "Total r" and antisym: "antisym r" unfolding card_order_on_def well_order_on_def linear_order_on_def @@ -132,8 +131,8 @@ qed qed -lemma Cinfinite_limit_finite: "\finite X; X \ Field r; Cinfinite r\ - \ \y \ Field r. \x \ X. (x \ y \ (x, y) \ r)" +lemma Cinfinite_limit_finite: + "\finite X; X \ Field r; Cinfinite r\ \ \y \ Field r. \x \ X. (x \ y \ (x, y) \ r)" proof (induct X rule: finite_induct) case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto next @@ -153,7 +152,7 @@ qed lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A" -by auto + by auto lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\x. x \ Field r \ P x" for r P]