summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Wed, 07 May 2008 10:56:58 +0200 | |

changeset 26805 | 27941d7d9a11 |

parent 26804 | e2b1e6868c2f |

child 26806 | 40b411ec05aa |

Replaced forward proofs of existential statements by backward proofs
to avoid problems with HO unification

--- 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 "\<exists>G. greatest ?L G (carrier ?L)" .. + show "\<exists>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 \<subseteq> carrier ?L" and non_empty: "A ~= {}" then have Int_subgroup: "subgroup (\<Inter>A) G" by (fastsimp intro: subgroups_Inter) - have "greatest ?L (\<Inter>A) (Lower ?L A)" - (is "greatest _ ?Int _") - proof (rule greatest_LowerI) - fix H - assume H: "H \<in> 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 \<subseteq> H" by fastsimp - then show "le ?L ?Int H" by simp - next - fix H - assume H: "H \<in> Lower ?L A" - with L Int_subgroup show "le ?L H ?Int" - by (fastsimp simp: Lower_def intro: Inter_greatest) - next - show "A \<subseteq> carrier ?L" by (rule L) - next - show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) + show "\<exists>I. greatest ?L I (Lower ?L A)" + proof + show "greatest ?L (\<Inter>A) (Lower ?L A)" + (is "greatest _ ?Int _") + proof (rule greatest_LowerI) + fix H + assume H: "H \<in> 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 \<subseteq> H" by fastsimp + then show "le ?L ?Int H" by simp + next + fix H + assume H: "H \<in> Lower ?L A" + with L Int_subgroup show "le ?L H ?Int" + by (fastsimp simp: Lower_def intro: Inter_greatest) + next + show "A \<subseteq> carrier ?L" by (rule L) + next + show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) + qed qed - then show "\<exists>I. greatest ?L I (Lower ?L A)" .. qed end

--- 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 \<subseteq> carrier ?L" - then have "least ?L (\<Union> 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 \<subseteq> carrier ?L" + show "EX s. least ?L s (Upper ?L B)" + proof + from B show "least ?L (\<Union> B) (Upper ?L B)" + by (fastsimp intro!: least_UpperI simp: Upper_def) + qed next fix B - assume "B \<subseteq> carrier ?L" - then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" - txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: - @{term "\<Inter> {} = 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 \<subseteq> carrier ?L" + show "EX i. greatest ?L i (Lower ?L B)" + proof + from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" + txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: + @{term "\<Inter> {} = 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,

--- 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 \<in> 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