# HG changeset patch # User paulson # Date 1636473851 0 # Node ID 329cb9e6b184337d723bfec8a6f86f2156c774a3 # Parent cba1da393958ac15a155abaadf5d3472705d83ff A tiny bit of tidying connected with Zorn's Lemma diff -r cba1da393958 -r 329cb9e6b184 src/HOL/Wfrec.thy --- a/src/HOL/Wfrec.thy Tue Nov 09 11:23:27 2021 +0100 +++ b/src/HOL/Wfrec.thy Tue Nov 09 16:04:11 2021 +0000 @@ -84,6 +84,9 @@ finally show "wfrec R F x = F (wfrec R F) x" . qed +lemma wfrec_def_adm: "f \ wfrec R F \ wf R \ adm_wf R F \ f = F f" + using wfrec_fixpoint by simp + subsection \Wellfoundedness of \same_fst\\ diff -r cba1da393958 -r 329cb9e6b184 src/HOL/Zorn.thy --- a/src/HOL/Zorn.thy Tue Nov 09 11:23:27 2021 +0100 +++ b/src/HOL/Zorn.thy Tue Nov 09 16:04:11 2021 +0000 @@ -4,10 +4,9 @@ Author: Christian Sternagel, JAIST Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF). -The well-ordering theorem. *) -section \Zorn's Lemma\ +section \Zorn's Lemma and the Well-ordering Theorem\ theory Zorn imports Order_Relation Hilbert_Choice @@ -155,16 +154,8 @@ then show ?case proof assume "Y \ X" - with * and \Y \ \\ have "X = Y \ suc Y \ X" by blast - then show ?thesis - proof - assume "X = Y" - then show ?thesis by simp - next - assume "suc Y \ X" - then have "suc Y \ suc X" by (rule subset_suc) - then show ?thesis by simp - qed + with * and \Y \ \\ subset_suc show ?thesis + by fastforce next assume "suc X \ Y" with \Y \ suc X\ show ?thesis by blast @@ -186,20 +177,11 @@ then show False proof assume "Y \ x" - with * [OF \Y \ \\] have "x = Y \ suc Y \ x" by blast - then show False - proof - assume "x = Y" - with \y \ x\ and \y \ Y\ show False by blast - next - assume "suc Y \ x" - with \x \ X\ have "suc Y \ \X" by blast - with \\ suc Y \ \X\ show False by contradiction - qed + with * [OF \Y \ \\] \y \ x\ \y \ Y\ \x \ X\ \\ suc Y \ \X\ show False + by blast next assume "suc x \ Y" - moreover from suc_subset and \y \ x\ have "y \ suc x" by blast - ultimately show False using \y \ Y\ by blast + with \y \ Y\ suc_subset \y \ x\ show False by blast qed qed qed @@ -874,11 +856,6 @@ with 1 show ?thesis by auto qed -(* Move this to Hilbert Choice and wfrec to Wellfounded*) - -lemma wfrec_def_adm: "f \ wfrec R F \ wf R \ adm_wf R F \ f = F f" - using wfrec_fixpoint by simp - lemma dependent_wf_choice: fixes P :: "('a \ 'b) \ 'a \ 'b \ bool" assumes "wf R" @@ -894,7 +871,7 @@ show "P f x (f x)" proof (subst (2) wfrec_def_adm[OF f_def \wf R\]) show "adm_wf R (\f x. SOME r. P f x r)" - by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm) + by (auto simp: adm_wf_def intro!: arg_cong[where f=Eps] adm) show "P f x (Eps (P f x))" using P by (rule someI_ex) fact qed