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

author | wenzelm |

Tue, 31 Mar 2009 14:10:46 +0200 | |

changeset 30821 | 7d6d1f9a0b41 |

parent 30820 | a489921b77f4 (current diff) |

parent 30818 | 17059c24014d (diff) |

child 30822 | 8aac4b974280 |

child 30827 | fe4331fb3806 |

merged

--- a/lib/texinputs/isabellesym.sty Tue Mar 31 12:59:31 2009 +0200 +++ b/lib/texinputs/isabellesym.sty Tue Mar 31 14:10:46 2009 +0200 @@ -249,7 +249,7 @@ \newcommand{\isasymsqunion}{\isamath{\sqcup}} \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd \newcommand{\isasymsetminus}{\isamath{\setminus}} \newcommand{\isasympropto}{\isamath{\propto}} \newcommand{\isasymuplus}{\isamath{\uplus}}

--- a/src/HOL/Isar_examples/KnasterTarski.thy Tue Mar 31 12:59:31 2009 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Tue Mar 31 14:10:46 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Isar_examples/KnasterTarski.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen Typical textbook proof example. @@ -7,100 +6,104 @@ header {* Textbook-style reasoning: the Knaster-Tarski Theorem *} -theory KnasterTarski imports Main begin +theory KnasterTarski +imports Main Lattice_Syntax +begin subsection {* Prose version *} text {* - According to the textbook \cite[pages 93--94]{davey-priestley}, the - Knaster-Tarski fixpoint theorem is as follows.\footnote{We have - dualized the argument, and tuned the notation a little bit.} + According to the textbook \cite[pages 93--94]{davey-priestley}, the + Knaster-Tarski fixpoint theorem is as follows.\footnote{We have + dualized the argument, and tuned the notation a little bit.} - \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a - complete lattice and $f \colon L \to L$ an order-preserving map. - Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$. + \textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a + complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map. + Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}. - \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a = - \bigwedge H$. For all $x \in H$ we have $a \le x$, so $f(a) \le f(x) - \le x$. Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$. - We now use this inequality to prove the reverse one (!) and thereby - complete the proof that $a$ is a fixpoint. Since $f$ is - order-preserving, $f(f(a)) \le f(a)$. This says $f(a) \in H$, so $a - \le f(a)$. + \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a = + \<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text + "f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text + H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove + the reverse one (!) and thereby complete the proof that @{text a} is + a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le> + f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}. *} subsection {* Formal versions *} text {* - The Isar proof below closely follows the original presentation. - Virtually all of the prose narration has been rephrased in terms of - formal Isar language elements. Just as many textbook-style proofs, - there is a strong bias towards forward proof, and several bends - in the course of reasoning. + The Isar proof below closely follows the original presentation. + Virtually all of the prose narration has been rephrased in terms of + formal Isar language elements. Just as many textbook-style proofs, + there is a strong bias towards forward proof, and several bends in + the course of reasoning. *} -theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a" +theorem Knaster_Tarski: + fixes f :: "'a::complete_lattice \<Rightarrow> 'a" + assumes "mono f" + shows "\<exists>a. f a = a" proof - let ?H = "{u. f u <= u}" - let ?a = "Inter ?H" - - assume mono: "mono f" + let ?H = "{u. f u \<le> u}" + let ?a = "\<Sqinter>?H" show "f ?a = ?a" proof - { fix x - assume H: "x : ?H" - hence "?a <= x" by (rule Inter_lower) - with mono have "f ?a <= f x" .. - also from H have "... <= x" .. - finally have "f ?a <= x" . + assume "x \<in> ?H" + then have "?a \<le> x" by (rule Inf_lower) + with `mono f` have "f ?a \<le> f x" .. + also from `x \<in> ?H` have "\<dots> \<le> x" .. + finally have "f ?a \<le> x" . } - hence ge: "f ?a <= ?a" by (rule Inter_greatest) + then have "f ?a \<le> ?a" by (rule Inf_greatest) { - also presume "... <= f ?a" + also presume "\<dots> \<le> f ?a" finally (order_antisym) show ?thesis . } - from mono ge have "f (f ?a) <= f ?a" .. - hence "f ?a : ?H" by simp - thus "?a <= f ?a" by (rule Inter_lower) + from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" .. + then have "f ?a \<in> ?H" .. + then show "?a \<le> f ?a" by (rule Inf_lower) qed qed text {* - Above we have used several advanced Isar language elements, such as - explicit block structure and weak assumptions. Thus we have mimicked - the particular way of reasoning of the original text. + Above we have used several advanced Isar language elements, such as + explicit block structure and weak assumptions. Thus we have + mimicked the particular way of reasoning of the original text. - In the subsequent version the order of reasoning is changed to - achieve structured top-down decomposition of the problem at the outer - level, while only the inner steps of reasoning are done in a forward - manner. We are certainly more at ease here, requiring only the most - basic features of the Isar language. + In the subsequent version the order of reasoning is changed to + achieve structured top-down decomposition of the problem at the + outer level, while only the inner steps of reasoning are done in a + forward manner. We are certainly more at ease here, requiring only + the most basic features of the Isar language. *} -theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a" +theorem Knaster_Tarski': + fixes f :: "'a::complete_lattice \<Rightarrow> 'a" + assumes "mono f" + shows "\<exists>a. f a = a" proof - let ?H = "{u. f u <= u}" - let ?a = "Inter ?H" - - assume mono: "mono f" + let ?H = "{u. f u \<le> u}" + let ?a = "\<Sqinter>?H" show "f ?a = ?a" proof (rule order_antisym) - show ge: "f ?a <= ?a" - proof (rule Inter_greatest) + show "f ?a \<le> ?a" + proof (rule Inf_greatest) fix x - assume H: "x : ?H" - hence "?a <= x" by (rule Inter_lower) - with mono have "f ?a <= f x" .. - also from H have "... <= x" .. - finally show "f ?a <= x" . + assume "x \<in> ?H" + then have "?a \<le> x" by (rule Inf_lower) + with `mono f` have "f ?a \<le> f x" .. + also from `x \<in> ?H` have "\<dots> \<le> x" .. + finally show "f ?a \<le> x" . qed - show "?a <= f ?a" - proof (rule Inter_lower) - from mono ge have "f (f ?a) <= f ?a" .. - thus "f ?a : ?H" by simp + show "?a \<le> f ?a" + proof (rule Inf_lower) + from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" .. + then show "f ?a \<in> ?H" .. qed qed qed

--- a/src/HOL/Isar_examples/document/style.tex Tue Mar 31 12:59:31 2009 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Tue Mar 31 14:10:46 2009 +0200 @@ -1,8 +1,6 @@ - -%% $Id$ - \documentclass[11pt,a4paper]{article} -\usepackage{ifthen,proof,isabelle,isabellesym} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} \isabellestyle{it} \usepackage{pdfsetup}\urlstyle{rm}

--- a/src/HOL/Set.thy Tue Mar 31 12:59:31 2009 +0200 +++ b/src/HOL/Set.thy Tue Mar 31 14:10:46 2009 +0200 @@ -2384,7 +2384,7 @@ unfolding Inf_bool_def by auto lemma not_Sup_empty_bool [simp]: - "\<not> Sup {}" + "\<not> \<Squnion>{}" unfolding Sup_bool_def by auto

--- a/src/Pure/Isar/proof_context.ML Tue Mar 31 12:59:31 2009 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Mar 31 14:10:46 2009 +0200 @@ -582,8 +582,9 @@ | (SOME S, NONE) => S | (SOME S, SOME S') => if Type.eq_sort tsig (S, S') then S' - else error ("Sort constraint inconsistent with default for type variable " ^ - quote (Term.string_of_vname' xi))); + else error ("Sort constraint " ^ Syntax.string_of_sort_global thy S ^ + " inconsistent with default " ^ Syntax.string_of_sort_global thy S' ^ + " for type variable " ^ quote (Term.string_of_vname' xi))); in get end; local