src/HOL/ex/Tarski.thy

     and v_def: "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r &
                              x: intY1}
                       (| pset=intY1, order=induced intY1 r|)"
 
 
-subsubsection {* Partial Order *}
+subsection {* Partial Order *}
 
 lemma (in PO) PO_imp_refl: "refl A r"
 apply (insert cl_po)
 apply (simp add: PartialOrder_def A_def r_def)
 done

 apply (simp add: PO_imp_trans interval_not_empty)
 apply (simp add: PO_imp_refl [THEN reflE])
 done
 
 
-subsubsection {* sublattice *}
+subsection {* sublattice *}
 
 lemma (in PO) sublattice_imp_CL:
      "S <<= cl  ==> (| pset = S, order = induced S r |) \<in> CompleteLattice"
 by (simp add: sublattice_def CompleteLattice_def A_def r_def)
 

      "[| S <= A; (| pset = S, order = induced S r |) \<in> CompleteLattice |]
       ==> S <<= cl"
 by (simp add: sublattice_def A_def r_def)
 
 
-subsubsection {* lub *}
+subsection {* lub *}
 
 lemma (in CL) lub_unique: "[| S <= A; isLub S cl x; isLub S cl L|] ==> x = L"
 apply (rule antisymE)
 apply (rule CO_antisym)
 apply (auto simp add: isLub_def r_def)

      "[| L \<in> A; \<forall>y \<in> S. (y, L) \<in> r;
          (\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) --> (L, z) \<in> r)|] ==> isLub S cl L"
 by (simp add: isLub_def A_def r_def)
 
 
-subsubsection {* glb *}
+subsection {* glb *}
 
 lemma (in CL) glb_in_lattice: "S <= A ==> glb S cl \<in> A"
 apply (subst glb_dual_lub)
 apply (simp add: A_def)
 apply (rule dualA_iff [THEN subst])

 apply (simp add: CLF_def  CL_dualCL monotone_dual)
 apply (simp add: dualA_iff)
 done
 
 
-subsubsection {* fixed points *}
+subsection {* fixed points *}
 
 lemma fix_subset: "fix f A <= A"
 by (simp add: fix_def, fast)
 
 lemma fix_imp_eq: "x \<in> fix f A ==> f x = x"

      "[| A <= B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B"
 apply (simp add: fix_def, auto)
 done
 
 
-subsubsection {* lemmas for Tarski, lub *}
+subsection {* lemmas for Tarski, lub *}
 lemma (in CLF) lubH_le_flubH:
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r"
 apply (rule lub_least, fast)
 apply (rule f_in_funcset [THEN funcset_mem])
 apply (rule lub_in_lattice, fast)

 apply (rule impI)
 apply (erule bspec)
 apply (rule lubH_is_fixp, assumption)
 done
 
-subsubsection {* Tarski fixpoint theorem 1, first part *}
+subsection {* Tarski fixpoint theorem 1, first part *}
 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl"
 apply (rule sym)
 apply (simp add: P_def)
 apply (rule lubI)
 apply (rule fix_subset)

 apply (rule dualA_iff [THEN subst])
 apply (simp add: Tarski.T_thm_1_lub [of _ f, OF dualPO CL_dualCL]
                  dualPO CL_dualCL CLF_dual dualr_iff)
 done
 
-subsubsection {* interval *}
+subsection {* interval *}
 
 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
 apply (insert CO_refl)
 apply (simp add: refl_def, blast)
 done

 
 lemmas (in CLF) interv_is_compl_latt =
     interval_is_sublattice [THEN sublattice_imp_CL]
 
 
-subsubsection {* Top and Bottom *}
+subsection {* Top and Bottom *}
 lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)"
 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
 
 lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)"
 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)

                  f_cl dualPO CL_dualCL CLF_dual)
 apply (simp add: Tarski.Top_intv_not_empty [of _ f]
                  dualA_iff A_def dualPO CL_dualCL CLF_dual)
 done
 
-subsubsection {* fixed points form a partial order *}
+subsection {* fixed points form a partial order *}
 
 lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder"
 by (simp add: P_def fix_subset po_subset_po)
 
 lemma (in Tarski) Y_subset_A: "Y <= A"