# HG changeset patch # User berghofe # Date 1210150618 -7200 # Node ID 27941d7d9a11eaeddc5188661485682a903cbfc5 # Parent e2b1e6868c2f2a5054462a1cb6d72cb304c1273a Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification diff -r e2b1e6868c2f -r 27941d7d9a11 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Wed May 07 10:56:55 2008 +0200 +++ b/src/HOL/Algebra/Group.thy Wed May 07 10:56:58 2008 +0200 @@ -735,38 +735,42 @@ proof (rule partial_order.complete_lattice_criterion1) show "partial_order ?L" by (rule subgroups_partial_order) next - have "greatest ?L (carrier G) (carrier ?L)" - by (unfold greatest_def) - (simp add: subgroup.subset subgroup_self) - then show "\G. greatest ?L G (carrier ?L)" .. + show "\G. greatest ?L G (carrier ?L)" + proof + show "greatest ?L (carrier G) (carrier ?L)" + by (unfold greatest_def) + (simp add: subgroup.subset subgroup_self) + qed next fix A assume L: "A \ carrier ?L" and non_empty: "A ~= {}" then have Int_subgroup: "subgroup (\A) G" by (fastsimp intro: subgroups_Inter) - have "greatest ?L (\A) (Lower ?L A)" - (is "greatest _ ?Int _") - proof (rule greatest_LowerI) - fix H - assume H: "H \ A" - with L have subgroupH: "subgroup H G" by auto - from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") - by (rule subgroup_imp_group) - from groupH have monoidH: "monoid ?H" - by (rule group.is_monoid) - from H have Int_subset: "?Int \ H" by fastsimp - then show "le ?L ?Int H" by simp - next - fix H - assume H: "H \ Lower ?L A" - with L Int_subgroup show "le ?L H ?Int" - by (fastsimp simp: Lower_def intro: Inter_greatest) - next - show "A \ carrier ?L" by (rule L) - next - show "?Int \ carrier ?L" by simp (rule Int_subgroup) + show "\I. greatest ?L I (Lower ?L A)" + proof + show "greatest ?L (\A) (Lower ?L A)" + (is "greatest _ ?Int _") + proof (rule greatest_LowerI) + fix H + assume H: "H \ A" + with L have subgroupH: "subgroup H G" by auto + from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") + by (rule subgroup_imp_group) + from groupH have monoidH: "monoid ?H" + by (rule group.is_monoid) + from H have Int_subset: "?Int \ H" by fastsimp + then show "le ?L ?Int H" by simp + next + fix H + assume H: "H \ Lower ?L A" + with L Int_subgroup show "le ?L H ?Int" + by (fastsimp simp: Lower_def intro: Inter_greatest) + next + show "A \ carrier ?L" by (rule L) + next + show "?Int \ carrier ?L" by simp (rule Int_subgroup) + qed qed - then show "\I. greatest ?L I (Lower ?L A)" .. qed end diff -r e2b1e6868c2f -r 27941d7d9a11 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Wed May 07 10:56:55 2008 +0200 +++ b/src/HOL/Algebra/Lattice.thy Wed May 07 10:56:58 2008 +0200 @@ -847,18 +847,22 @@ by (rule partial_order.intro) auto next fix B - assume "B \ carrier ?L" - then have "least ?L (\ B) (Upper ?L B)" - by (fastsimp intro!: least_UpperI simp: Upper_def) - then show "EX s. least ?L s (Upper ?L B)" .. + assume B: "B \ carrier ?L" + show "EX s. least ?L s (Upper ?L B)" + proof + from B show "least ?L (\ B) (Upper ?L B)" + by (fastsimp intro!: least_UpperI simp: Upper_def) + qed next fix B - assume "B \ carrier ?L" - then have "greatest ?L (\ B \ A) (Lower ?L B)" - txt {* @{term "\ B"} is not the infimum of @{term B}: - @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *} - by (fastsimp intro!: greatest_LowerI simp: Lower_def) - then show "EX i. greatest ?L i (Lower ?L B)" .. + assume B: "B \ carrier ?L" + show "EX i. greatest ?L i (Lower ?L B)" + proof + from B show "greatest ?L (\ B \ A) (Lower ?L B)" + txt {* @{term "\ B"} is not the infimum of @{term B}: + @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *} + by (fastsimp intro!: greatest_LowerI simp: Lower_def) + qed qed text {* An other example, that of the lattice of subgroups of a group, diff -r e2b1e6868c2f -r 27941d7d9a11 src/HOL/Hyperreal/Filter.thy --- a/src/HOL/Hyperreal/Filter.thy Wed May 07 10:56:55 2008 +0200 +++ b/src/HOL/Hyperreal/Filter.thy Wed May 07 10:56:58 2008 +0200 @@ -394,10 +394,12 @@ fix A assume "A \ U" with U show "infinite A" by (rule mem_superfrechet_all_infinite) qed - from fil ultra free have "freeultrafilter U" - by (rule freeultrafilter.intro [OF ultrafilter.intro]) - (* FIXME: unfold_locales should use chained facts *) - thus ?thesis .. + show ?thesis + proof + from fil ultra free show "freeultrafilter U" + by (rule freeultrafilter.intro [OF ultrafilter.intro]) + (* FIXME: unfold_locales should use chained facts *) + qed qed lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex