src/HOL/Algebra/Group.thy
changeset 26805 27941d7d9a11
parent 26199 04817a8802f2
child 27611 2c01c0bdb385
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed May 07 10:56:55 2008 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 07 10:56:58 2008 +0200
     1.3 @@ -735,38 +735,42 @@
     1.4  proof (rule partial_order.complete_lattice_criterion1)
     1.5    show "partial_order ?L" by (rule subgroups_partial_order)
     1.6  next
     1.7 -  have "greatest ?L (carrier G) (carrier ?L)"
     1.8 -    by (unfold greatest_def)
     1.9 -      (simp add: subgroup.subset subgroup_self)
    1.10 -  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
    1.11 +  show "\<exists>G. greatest ?L G (carrier ?L)"
    1.12 +  proof
    1.13 +    show "greatest ?L (carrier G) (carrier ?L)"
    1.14 +      by (unfold greatest_def)
    1.15 +        (simp add: subgroup.subset subgroup_self)
    1.16 +  qed
    1.17  next
    1.18    fix A
    1.19    assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
    1.20    then have Int_subgroup: "subgroup (\<Inter>A) G"
    1.21      by (fastsimp intro: subgroups_Inter)
    1.22 -  have "greatest ?L (\<Inter>A) (Lower ?L A)"
    1.23 -    (is "greatest _ ?Int _")
    1.24 -  proof (rule greatest_LowerI)
    1.25 -    fix H
    1.26 -    assume H: "H \<in> A"
    1.27 -    with L have subgroupH: "subgroup H G" by auto
    1.28 -    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
    1.29 -      by (rule subgroup_imp_group)
    1.30 -    from groupH have monoidH: "monoid ?H"
    1.31 -      by (rule group.is_monoid)
    1.32 -    from H have Int_subset: "?Int \<subseteq> H" by fastsimp
    1.33 -    then show "le ?L ?Int H" by simp
    1.34 -  next
    1.35 -    fix H
    1.36 -    assume H: "H \<in> Lower ?L A"
    1.37 -    with L Int_subgroup show "le ?L H ?Int"
    1.38 -      by (fastsimp simp: Lower_def intro: Inter_greatest)
    1.39 -  next
    1.40 -    show "A \<subseteq> carrier ?L" by (rule L)
    1.41 -  next
    1.42 -    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    1.43 +  show "\<exists>I. greatest ?L I (Lower ?L A)"
    1.44 +  proof
    1.45 +    show "greatest ?L (\<Inter>A) (Lower ?L A)"
    1.46 +      (is "greatest _ ?Int _")
    1.47 +    proof (rule greatest_LowerI)
    1.48 +      fix H
    1.49 +      assume H: "H \<in> A"
    1.50 +      with L have subgroupH: "subgroup H G" by auto
    1.51 +      from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
    1.52 +	by (rule subgroup_imp_group)
    1.53 +      from groupH have monoidH: "monoid ?H"
    1.54 +	by (rule group.is_monoid)
    1.55 +      from H have Int_subset: "?Int \<subseteq> H" by fastsimp
    1.56 +      then show "le ?L ?Int H" by simp
    1.57 +    next
    1.58 +      fix H
    1.59 +      assume H: "H \<in> Lower ?L A"
    1.60 +      with L Int_subgroup show "le ?L H ?Int"
    1.61 +	by (fastsimp simp: Lower_def intro: Inter_greatest)
    1.62 +    next
    1.63 +      show "A \<subseteq> carrier ?L" by (rule L)
    1.64 +    next
    1.65 +      show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    1.66 +    qed
    1.67    qed
    1.68 -  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
    1.69  qed
    1.70  
    1.71  end