tiny bit of extra restructuring
authorpaulson <lp15@cam.ac.uk>
Sat Apr 27 21:56:59 2019 +0100 (7 months ago)
changeset 70202373eb0aa97e3
parent 70201 2e496190039d
child 70203 cd2af90360ee
child 70208 65b3bfc565b5
tiny bit of extra restructuring
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/ex/Tarski.thy	Sat Apr 27 20:00:38 2019 +0100
     1.2 +++ b/src/HOL/ex/Tarski.thy	Sat Apr 27 21:56:59 2019 +0100
     1.3 @@ -444,34 +444,34 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma flubH_le_lubH: 
     1.8 +lemma lubH_is_fixp: 
     1.9    assumes "H = {x \<in> A. (x, f x) \<in> r}"
    1.10 -  shows "(f (lub H cl), lub H cl) \<in> r"
    1.11 +  shows "lub H cl \<in> fix f A"
    1.12  proof -
    1.13 -  have "(lub H cl, f (lub H cl)) \<in> r"
    1.14 -    using assms lubH_le_flubH by blast
    1.15 -  then have "(f (lub H cl), f (f (lub H cl))) \<in> r"
    1.16 -    by (meson PO_imp_refl_on monotoneE monotone_f refl_on_domain)
    1.17 -  then have "f (lub H cl) \<in> H"
    1.18 -    by (metis (no_types, lifting) PO_imp_refl_on assms mem_Collect_eq refl_on_domain)
    1.19 -  then show ?thesis
    1.20 -    by (simp add: assms lub_upper)
    1.21 +  have "(f (lub H cl), lub H cl) \<in> r"
    1.22 +  proof -
    1.23 +    have "(lub H cl, f (lub H cl)) \<in> r"
    1.24 +      using assms lubH_le_flubH by blast
    1.25 +    then have "(f (lub H cl), f (f (lub H cl))) \<in> r"
    1.26 +      by (meson PO_imp_refl_on monotoneE monotone_f refl_on_domain)
    1.27 +    then have "f (lub H cl) \<in> H"
    1.28 +      by (metis (no_types, lifting) PO_imp_refl_on assms mem_Collect_eq refl_on_domain)
    1.29 +    then show ?thesis
    1.30 +      by (simp add: assms lub_upper)
    1.31 +  qed
    1.32 +  with assms show ?thesis
    1.33 +    by (simp add: fix_def antisymE lubH_le_flubH lub_in_lattice)
    1.34  qed
    1.35  
    1.36 -
    1.37 -
    1.38 -lemma lubH_is_fixp: "H = {x \<in> A. (x, f x) \<in> r} \<Longrightarrow> lub H cl \<in> fix f A"
    1.39 -  by (simp add: fix_def antisymE flubH_le_lubH lubH_le_flubH lub_in_lattice)
    1.40 -
    1.41 -lemma fix_in_H: "\<lbrakk>H = {x \<in> A. (x, f x) \<in> r}; x \<in> P\<rbrakk> \<Longrightarrow> x \<in> H"
    1.42 -  by (simp add: P_def fix_imp_eq [of _ f A] reflE fix_subset [of f A, THEN subsetD])
    1.43 -
    1.44 -lemma fixf_le_lubH: "H = {x \<in> A. (x, f x) \<in> r} \<Longrightarrow> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r"
    1.45 -  by (metis (no_types, lifting) P_def fix_in_H lub_upper mem_Collect_eq subset_eq)
    1.46 -
    1.47 -lemma lubH_least_fixf:
    1.48 -  "H = {x \<in> A. (x, f x) \<in> r} \<Longrightarrow> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) \<longrightarrow> (lub H cl, L) \<in> r"
    1.49 -  using lubH_is_fixp by blast
    1.50 +lemma fixf_le_lubH: 
    1.51 +  assumes "H = {x \<in> A. (x, f x) \<in> r}" "x \<in> fix f A"
    1.52 +  shows "(x, lub H cl) \<in> r"
    1.53 +proof -
    1.54 +  have "x \<in> P \<Longrightarrow> x \<in> H"
    1.55 +    by (simp add: assms P_def fix_imp_eq [of _ f A] reflE fix_subset [of f A, THEN subsetD])
    1.56 +  with assms show ?thesis
    1.57 +    by (metis (no_types, lifting) P_def lub_upper mem_Collect_eq subset_eq)
    1.58 +qed
    1.59  
    1.60  
    1.61  subsection \<open>Tarski fixpoint theorem 1, first part\<close>
    1.62 @@ -623,9 +623,8 @@
    1.63    using Bot_dual_Top Bot_prop intervalI reflE by fastforce
    1.64  
    1.65  
    1.66 -subsection \<open>fixed points form a partial order\<close>
    1.67 -
    1.68 -lemma fixf_po: "\<lparr>pset = P, order = induced P r\<rparr> \<in> PartialOrder"
    1.69 +text \<open>the set of fixed points form a partial order\<close>
    1.70 +proposition fixf_po: "\<lparr>pset = P, order = induced P r\<rparr> \<in> PartialOrder"
    1.71    by (simp add: P_def fix_subset po_subset_po)
    1.72  
    1.73  end
    1.74 @@ -723,11 +722,9 @@
    1.75  end
    1.76  
    1.77  lemma CompleteLatticeI_simp:
    1.78 -  "\<lbrakk>po \<in> PartialOrder; \<And>S. S \<subseteq> A \<Longrightarrow> \<exists>L. isLub S po  L; A = pset po\<rbrakk>
    1.79 -    \<Longrightarrow> po \<in> CompleteLattice"
    1.80 +  "\<lbrakk>po \<in> PartialOrder; \<And>S. S \<subseteq> A \<Longrightarrow> \<exists>L. isLub S po  L; A = pset po\<rbrakk> \<Longrightarrow> po \<in> CompleteLattice"
    1.81    by (metis CompleteLatticeI Rdual)
    1.82  
    1.83 -
    1.84  theorem (in CLF) Tarski_full: "\<lparr>pset = P, order = induced P r\<rparr> \<in> CompleteLattice"
    1.85  proof (intro CompleteLatticeI_simp allI impI)
    1.86    show "\<lparr>pset = P, order = induced P r\<rparr> \<in> PartialOrder"