From c0c6f5750e1c06cdf0f7ba5136e062341a39ab23 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 3 Aug 2010 12:47:35 +0000 Subject: Deleted file --- isar/KnasterTarski.thy | 113 ------- isar/Root2_Isar.thy | 153 --------- isar/Root2_Tactic.thy | 83 ----- isar/Tarski.thy | 904 ------------------------------------------------- 4 files changed, 1253 deletions(-) delete mode 100644 isar/KnasterTarski.thy delete mode 100644 isar/Root2_Isar.thy delete mode 100644 isar/Root2_Tactic.thy delete mode 100644 isar/Tarski.thy (limited to 'isar') diff --git a/isar/KnasterTarski.thy b/isar/KnasterTarski.thy deleted file mode 100644 index 5d0bbce0..00000000 --- a/isar/KnasterTarski.thy +++ /dev/null @@ -1,113 +0,0 @@ -(********** This file is from the Isabelle distribution **********) - -(* Title: HOL/Isar_examples/KnasterTarski.thy - Author: Markus Wenzel, TU Muenchen - -Typical textbook proof example. -*) - -header {* Textbook-style reasoning: the Knaster-Tarski Theorem *} - -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.} - - \textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a - complete lattice and @{text "f: L \ L"} an order-preserving map. - Then @{text "\{x \ L | f(x) \ x}"} is a fixpoint of @{text f}. - - \textbf{Proof.} Let @{text "H = {x \ L | f(x) \ x}"} and @{text "a = - \H"}. For all @{text "x \ H"} we have @{text "a \ x"}, so @{text - "f(a) \ f(x) \ x"}. Thus @{text "f(a)"} is a lower bound of @{text - H}, whence @{text "f(a) \ 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)) \ - f(a)"}. This says @{text "f(a) \ H"}, so @{text "a \ 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. -*} - -theorem Knaster_Tarski: - fixes f :: "'a::complete_lattice \ 'a" - assumes "mono f" - shows "\a. f a = a" -proof - let ?H = "{u. f u \ u}" - let ?a = "\?H" - show "f ?a = ?a" - proof - - { - fix x - assume "x \ ?H" - then have "?a \ x" by (rule Inf_lower) - with `mono f` have "f ?a \ f x" .. - also from `x \ ?H` have "\ \ x" .. - finally have "f ?a \ x" . - } - then have "f ?a \ ?a" by (rule Inf_greatest) - { - also presume "\ \ f ?a" - finally (order_antisym) show ?thesis . - } - from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. - then have "f ?a \ ?H" .. - then show "?a \ 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. - - 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 Knaster_Tarski': - fixes f :: "'a::complete_lattice \ 'a" - assumes "mono f" - shows "\a. f a = a" -proof - let ?H = "{u. f u \ u}" - let ?a = "\?H" - show "f ?a = ?a" - proof (rule order_antisym) - show "f ?a \ ?a" - proof (rule Inf_greatest) - fix x - assume "x \ ?H" - then have "?a \ x" by (rule Inf_lower) - with `mono f` have "f ?a \ f x" .. - also from `x \ ?H` have "\ \ x" .. - finally show "f ?a \ x" . - qed - show "?a \ f ?a" - proof (rule Inf_lower) - from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. - then show "f ?a \ ?H" .. - qed - qed -qed - -end diff --git a/isar/Root2_Isar.thy b/isar/Root2_Isar.thy deleted file mode 100644 index 7a0123dd..00000000 --- a/isar/Root2_Isar.thy +++ /dev/null @@ -1,153 +0,0 @@ -(* Example proof by Markus Wenzel; see http://www.cs.kun.nl/~freek/comparison/ - Taken from Isabelle2005 distribution. *) - - -(* Title: HOL/Hyperreal/ex/Sqrt.thy - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -*) - -header {* Square roots of primes are irrational *} - -theory Root2_Isar -imports Primes Complex_Main -begin - -subsection {* Preliminaries *} - -text {* - The set of rational numbers, including the key representation - theorem. -*} - -constdefs - rationals :: "real set" ("\") - "\ \ {x. \m n. n \ 0 \ \x\ = real (m::nat) / real (n::nat)}" - -theorem rationals_rep: "x \ \ \ - \m n. n \ 0 \ \x\ = real m / real n \ gcd (m, n) = 1" -proof - - assume "x \ \" - then obtain m n :: nat where - n: "n \ 0" and x_rat: "\x\ = real m / real n" - by (unfold rationals_def) blast - let ?gcd = "gcd (m, n)" - from n have gcd: "?gcd \ 0" by (simp add: gcd_zero) - let ?k = "m div ?gcd" - let ?l = "n div ?gcd" - let ?gcd' = "gcd (?k, ?l)" - have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m" - by (rule dvd_mult_div_cancel) - have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n" - by (rule dvd_mult_div_cancel) - - from n and gcd_l have "?l \ 0" - by (auto iff del: neq0_conv) - moreover - have "\x\ = real ?k / real ?l" - proof - - from gcd have "real ?k / real ?l = - real (?gcd * ?k) / real (?gcd * ?l)" - by (simp add: mult_divide_cancel_left) - also from gcd_k and gcd_l have "\ = real m / real n" by simp - also from x_rat have "\ = \x\" .. - finally show ?thesis .. - qed - moreover - have "?gcd' = 1" - proof - - have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)" - by (rule gcd_mult_distrib2) - with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp - with gcd show ?thesis by simp - qed - ultimately show ?thesis by blast -qed - -lemma [elim?]: "r \ \ \ - (\m n. n \ 0 \ \r\ = real m / real n \ gcd (m, n) = 1 \ C) - \ C" - using rationals_rep by blast - - -subsection {* Main theorem *} - -text {* - The square root of any prime number (including @{text 2}) is - irrational. -*} - -theorem sqrt_prime_irrational: "prime p \ sqrt (real p) \ \" -proof - assume p_prime: "prime p" - then have p: "1 < p" by (simp add: prime_def) - assume "sqrt (real p) \ \" - then obtain m n where - n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" - and gcd: "gcd (m, n) = 1" .. - have eq: "m\ = p * n\" - proof - - from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp - then have "real (m\) = (sqrt (real p))\ * real (n\)" - by (auto simp add: power2_eq_square) - also have "(sqrt (real p))\ = real p" by simp - also have "\ * real (n\) = real (p * n\)" by simp - finally show ?thesis .. - qed - have "p dvd m \ p dvd n" - proof - from eq have "p dvd m\" .. - with p_prime show "p dvd m" by (rule prime_dvd_power_two) - then obtain k where "m = p * k" .. - with eq have "p * n\ = p\ * k\" by (auto simp add: power2_eq_square mult_ac) - with p have "n\ = p * k\" by (simp add: power2_eq_square) - then have "p dvd n\" .. - with p_prime show "p dvd n" by (rule prime_dvd_power_two) - qed - then have "p dvd gcd (m, n)" .. - with gcd have "p dvd 1" by simp - then have "p \ 1" by (simp add: dvd_imp_le) - with p show False by simp -qed - -corollary "sqrt (real (2::nat)) \ \" - by (rule sqrt_prime_irrational) (rule two_is_prime) - - -subsection {* Variations *} - -text {* - Here is an alternative version of the main proof, using mostly - linear forward-reasoning. While this results in less top-down - structure, it is probably closer to proofs seen in mathematics. -*} - -theorem "prime p \ sqrt (real p) \ \" -proof - assume p_prime: "prime p" - then have p: "1 < p" by (simp add: prime_def) - assume "sqrt (real p) \ \" - then obtain m n where - n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" - and gcd: "gcd (m, n) = 1" .. - from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp - then have "real (m\) = (sqrt (real p))\ * real (n\)" - by (auto simp add: power2_eq_square) - also have "(sqrt (real p))\ = real p" by simp - also have "\ * real (n\) = real (p * n\)" by simp - finally have eq: "m\ = p * n\" .. - then have "p dvd m\" .. - with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two) - then obtain k where "m = p * k" .. - with eq have "p * n\ = p\ * k\" by (auto simp add: power2_eq_square mult_ac) - with p have "n\ = p * k\" by (simp add: power2_eq_square) - then have "p dvd n\" .. - with p_prime have "p dvd n" by (rule prime_dvd_power_two) - with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest) - with gcd have "p dvd 1" by simp - then have "p \ 1" by (simp add: dvd_imp_le) - with p show False by simp -qed - -end diff --git a/isar/Root2_Tactic.thy b/isar/Root2_Tactic.thy deleted file mode 100644 index 7c0620c5..00000000 --- a/isar/Root2_Tactic.thy +++ /dev/null @@ -1,83 +0,0 @@ -(* Example proof by Larry Paulson; see http://www.cs.kun.nl/~freek/comparison/ - Taken from Isabelle2005 distribution. *) - - -(* Title: HOL/Hyperreal/ex/Sqrt_Script.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge -*) - -header {* Square roots of primes are irrational (script version) *} - -theory Root2_Tactic -imports Primes Complex_Main -begin - -text {* - \medskip Contrast this linear Isabelle/Isar script with Markus - Wenzel's more mathematical version. -*} - -subsection {* Preliminaries *} - -lemma prime_nonzero: "prime p \ p \ 0" - by (force simp add: prime_def) - -lemma prime_dvd_other_side: - "n * n = p * (k * k) \ prime p \ p dvd n" - apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult) - apply (rule_tac j = "k * k" in dvd_mult_left, simp) - done - -lemma reduction: "prime p \ - 0 < k \ k * k = p * (j * j) \ k < p * j \ 0 < j" - apply (rule ccontr) - apply (simp add: linorder_not_less) - apply (erule disjE) - apply (frule mult_le_mono, assumption) - apply auto - apply (force simp add: prime_def) - done - -lemma rearrange: "(j::nat) * (p * j) = k * k \ k * k = p * (j * j)" - by (simp add: mult_ac) - -lemma prime_not_square: - "prime p \ (\k. 0 < k \ m * m \ p * (k * k))" - apply (induct m rule: nat_less_induct) - apply clarify - apply (frule prime_dvd_other_side, assumption) - apply (erule dvdE) - apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) - apply (blast dest: rearrange reduction) - done - - -subsection {* The set of rational numbers *} - -constdefs - rationals :: "real set" ("\") - "\ \ {x. \m n. n \ 0 \ \x\ = real (m::nat) / real (n::nat)}" - - -subsection {* Main theorem *} - -text {* - The square root of any prime number (including @{text 2}) is - irrational. -*} - -theorem prime_sqrt_irrational: - "prime p \ x * x = real p \ 0 \ x \ x \ \" - apply (simp add: rationals_def real_abs_def) - apply clarify - apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) - apply (simp del: real_of_nat_mult - add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) - done - -lemmas two_sqrt_irrational = - prime_sqrt_irrational [OF two_is_prime] - -end diff --git a/isar/Tarski.thy b/isar/Tarski.thy deleted file mode 100644 index e68006e5..00000000 --- a/isar/Tarski.thy +++ /dev/null @@ -1,904 +0,0 @@ -(********** This file is from the Isabelle distribution **********) - -(* Title: HOL/ex/Tarski.thy - ID: Id: Tarski.thy,v 1.10 2002/09/26 08:51:32 paulson Exp - Author: Florian Kammüller, Cambridge University Computer Laboratory -*) - -header {* The Full Theorem of Tarski *} - -theory Tarski imports Main FuncSet begin - -text {* - Minimal version of lattice theory plus the full theorem of Tarski: - The fixedpoints of a complete lattice themselves form a complete - lattice. - - Illustrates first-class theories, using the Sigma representation of - structures. Tidied and converted to Isar by lcp. -*} - -record 'a potype = - pset :: "'a set" - order :: "('a * 'a) set" - -constdefs - monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" - "monotone f A r == \x\A. \y\A. (x, y): r --> ((f x), (f y)) : r" - - least :: "['a => bool, 'a potype] => 'a" - "least P po == @ x. x: pset po & P x & - (\y \ pset po. P y --> (x,y): order po)" - - greatest :: "['a => bool, 'a potype] => 'a" - "greatest P po == @ x. x: pset po & P x & - (\y \ pset po. P y --> (y,x): order po)" - - lub :: "['a set, 'a potype] => 'a" - "lub S po == least (%x. \y\S. (y,x): order po) po" - - glb :: "['a set, 'a potype] => 'a" - "glb S po == greatest (%x. \y\S. (x,y): order po) po" - - isLub :: "['a set, 'a potype, 'a] => bool" - "isLub S po == %L. (L: pset po & (\y\S. (y,L): order po) & - (\z\pset po. (\y\S. (y,z): order po) --> (L,z): order po))" - - isGlb :: "['a set, 'a potype, 'a] => bool" - "isGlb S po == %G. (G: pset po & (\y\S. (G,y): order po) & - (\z \ pset po. (\y\S. (z,y): order po) --> (z,G): order po))" - - "fix" :: "[('a => 'a), 'a set] => 'a set" - "fix f A == {x. x: A & f x = x}" - - interval :: "[('a*'a) set,'a, 'a ] => 'a set" - "interval r a b == {x. (a,x): r & (x,b): r}" - - -constdefs - Bot :: "'a potype => 'a" - "Bot po == least (%x. True) po" - - Top :: "'a potype => 'a" - "Top po == greatest (%x. True) po" - - PartialOrder :: "('a potype) set" - "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) & - trans (order P)}" - - CompleteLattice :: "('a potype) set" - "CompleteLattice == {cl. cl: PartialOrder & - (\S. S <= pset cl --> (\L. isLub S cl L)) & - (\S. S <= pset cl --> (\G. isGlb S cl G))}" - - CLF :: "('a potype * ('a => 'a)) set" - "CLF == SIGMA cl: CompleteLattice. - {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}" - - induced :: "['a set, ('a * 'a) set] => ('a *'a)set" - "induced A r == {(a,b). a : A & b: A & (a,b): r}" - - -constdefs - sublattice :: "('a potype * 'a set)set" - "sublattice == - SIGMA cl: CompleteLattice. - {S. S <= pset cl & - (| pset = S, order = induced S (order cl) |): CompleteLattice }" - -syntax - "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) - -translations - "S <<= cl" == "S : sublattice `` {cl}" - -constdefs - dual :: "'a potype => 'a potype" - "dual po == (| pset = pset po, order = converse (order po) |)" - -locale (open) PO = - fixes cl :: "'a potype" - and A :: "'a set" - and r :: "('a * 'a) set" - assumes cl_po: "cl : PartialOrder" - defines A_def: "A == pset cl" - and r_def: "r == order cl" - -locale (open) CL = PO + - assumes cl_co: "cl : CompleteLattice" - -locale (open) CLF = CL + - fixes f :: "'a => 'a" - and P :: "'a set" - assumes f_cl: "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*) - defines P_def: "P == fix f A" - - -locale (open) Tarski = CLF + - fixes Y :: "'a set" - and intY1 :: "'a set" - and v :: "'a" - assumes - Y_ss: "Y <= P" - defines - intY1_def: "intY1 == interval r (lub Y cl) (Top cl)" - 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 *} - -lemma (in PO) PO_imp_refl: "refl A r" -apply (insert cl_po) -apply (simp add: PartialOrder_def A_def r_def) -done - -lemma (in PO) PO_imp_sym: "antisym r" -apply (insert cl_po) -apply (simp add: PartialOrder_def A_def r_def) -done - -lemma (in PO) PO_imp_trans: "trans r" -apply (insert cl_po) -apply (simp add: PartialOrder_def A_def r_def) -done - -lemma (in PO) reflE: "[| refl A r; x \ A|] ==> (x, x) \ r" -apply (insert cl_po) -apply (simp add: PartialOrder_def refl_def) -done - -lemma (in PO) antisymE: "[| antisym r; (a, b) \ r; (b, a) \ r |] ==> a = b" -apply (insert cl_po) -apply (simp add: PartialOrder_def antisym_def) -done - -lemma (in PO) transE: "[| trans r; (a, b) \ r; (b, c) \ r|] ==> (a,c) \ r" -apply (insert cl_po) -apply (simp add: PartialOrder_def) -apply (unfold trans_def, fast) -done - -lemma (in PO) monotoneE: - "[| monotone f A r; x \ A; y \ A; (x, y) \ r |] ==> (f x, f y) \ r" -by (simp add: monotone_def) - -lemma (in PO) po_subset_po: - "S <= A ==> (| pset = S, order = induced S r |) \ PartialOrder" -apply (simp (no_asm) add: PartialOrder_def) -apply auto --- {* refl *} -apply (simp add: refl_def induced_def) -apply (blast intro: PO_imp_refl [THEN reflE]) --- {* antisym *} -apply (simp add: antisym_def induced_def) -apply (blast intro: PO_imp_sym [THEN antisymE]) --- {* trans *} -apply (simp add: trans_def induced_def) -apply (blast intro: PO_imp_trans [THEN transE]) -done - -lemma (in PO) indE: "[| (x, y) \ induced S r; S <= A |] ==> (x, y) \ r" -by (simp add: add: induced_def) - -lemma (in PO) indI: "[| (x, y) \ r; x \ S; y \ S |] ==> (x, y) \ induced S r" -by (simp add: add: induced_def) - -lemma (in CL) CL_imp_ex_isLub: "S <= A ==> \L. isLub S cl L" -apply (insert cl_co) -apply (simp add: CompleteLattice_def A_def) -done - -declare (in CL) cl_co [simp] - -lemma isLub_lub: "(\L. isLub S cl L) = isLub S cl (lub S cl)" -by (simp add: lub_def least_def isLub_def some_eq_ex [symmetric]) - -lemma isGlb_glb: "(\G. isGlb S cl G) = isGlb S cl (glb S cl)" -by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric]) - -lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)" -by (simp add: isLub_def isGlb_def dual_def converse_def) - -lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)" -by (simp add: isLub_def isGlb_def dual_def converse_def) - -lemma (in PO) dualPO: "dual cl \ PartialOrder" -apply (insert cl_po) -apply (simp add: PartialOrder_def dual_def refl_converse - trans_converse antisym_converse) -done - -lemma Rdual: - "\S. (S <= A -->( \L. isLub S (| pset = A, order = r|) L)) - ==> \S. (S <= A --> (\G. isGlb S (| pset = A, order = r|) G))" -apply safe -apply (rule_tac x = "lub {y. y \ A & (\k \ S. (y, k) \ r)} - (|pset = A, order = r|) " in exI) -apply (drule_tac x = "{y. y \ A & (\k \ S. (y,k) \ r) }" in spec) -apply (drule mp, fast) -apply (simp add: isLub_lub isGlb_def) -apply (simp add: isLub_def, blast) -done - -lemma lub_dual_glb: "lub S cl = glb S (dual cl)" -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def) - -lemma glb_dual_lub: "glb S cl = lub S (dual cl)" -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def) - -lemma CL_subset_PO: "CompleteLattice <= PartialOrder" -by (simp add: PartialOrder_def CompleteLattice_def, fast) - -lemmas CL_imp_PO = CL_subset_PO [THEN subsetD] - -declare CL_imp_PO [THEN Tarski.PO_imp_refl, simp] -declare CL_imp_PO [THEN Tarski.PO_imp_sym, simp] -declare CL_imp_PO [THEN Tarski.PO_imp_trans, simp] - -lemma (in CL) CO_refl: "refl A r" -by (rule PO_imp_refl) - -lemma (in CL) CO_antisym: "antisym r" -by (rule PO_imp_sym) - -lemma (in CL) CO_trans: "trans r" -by (rule PO_imp_trans) - -lemma CompleteLatticeI: - "[| po \ PartialOrder; (\S. S <= pset po --> (\L. isLub S po L)); - (\S. S <= pset po --> (\G. isGlb S po G))|] - ==> po \ CompleteLattice" -apply (unfold CompleteLattice_def, blast) -done - -lemma (in CL) CL_dualCL: "dual cl \ CompleteLattice" -apply (insert cl_co) -apply (simp add: CompleteLattice_def dual_def) -apply (fold dual_def) -apply (simp add: isLub_dual_isGlb [symmetric] isGlb_dual_isLub [symmetric] - dualPO) -done - -lemma (in PO) dualA_iff: "pset (dual cl) = pset cl" -by (simp add: dual_def) - -lemma (in PO) dualr_iff: "((x, y) \ (order(dual cl))) = ((y, x) \ order cl)" -by (simp add: dual_def) - -lemma (in PO) monotone_dual: - "monotone f (pset cl) (order cl) - ==> monotone f (pset (dual cl)) (order(dual cl))" -by (simp add: monotone_def dualA_iff dualr_iff) - -lemma (in PO) interval_dual: - "[| x \ A; y \ A|] ==> interval r x y = interval (order(dual cl)) y x" -apply (simp add: interval_def dualr_iff) -apply (fold r_def, fast) -done - -lemma (in PO) interval_not_empty: - "[| trans r; interval r a b \ {} |] ==> (a, b) \ r" -apply (simp add: interval_def) -apply (unfold trans_def, blast) -done - -lemma (in PO) interval_imp_mem: "x \ interval r a b ==> (a, x) \ r" -by (simp add: interval_def) - -lemma (in PO) left_in_interval: - "[| a \ A; b \ A; interval r a b \ {} |] ==> a \ interval r a b" -apply (simp (no_asm_simp) add: interval_def) -apply (simp add: PO_imp_trans interval_not_empty) -apply (simp add: PO_imp_refl [THEN reflE]) -done - -lemma (in PO) right_in_interval: - "[| a \ A; b \ A; interval r a b \ {} |] ==> b \ interval r a b" -apply (simp (no_asm_simp) add: interval_def) -apply (simp add: PO_imp_trans interval_not_empty) -apply (simp add: PO_imp_refl [THEN reflE]) -done - - -subsubsection {* sublattice *} - -lemma (in PO) sublattice_imp_CL: - "S <<= cl ==> (| pset = S, order = induced S r |) \ CompleteLattice" -by (simp add: sublattice_def CompleteLattice_def A_def r_def) - -lemma (in CL) sublatticeI: - "[| S <= A; (| pset = S, order = induced S r |) \ CompleteLattice |] - ==> S <<= cl" -by (simp add: sublattice_def A_def r_def) - - -subsubsection {* 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) -done - -lemma (in CL) lub_upper: "[|S <= A; x \ S|] ==> (x, lub S cl) \ r" -apply (rule CL_imp_ex_isLub [THEN exE], assumption) -apply (unfold lub_def least_def) -apply (rule some_equality [THEN ssubst]) - apply (simp add: isLub_def) - apply (simp add: lub_unique A_def isLub_def) -apply (simp add: isLub_def r_def) -done - -lemma (in CL) lub_least: - "[| S <= A; L \ A; \x \ S. (x,L) \ r |] ==> (lub S cl, L) \ r" -apply (rule CL_imp_ex_isLub [THEN exE], assumption) -apply (unfold lub_def least_def) -apply (rule_tac s=x in some_equality [THEN ssubst]) - apply (simp add: isLub_def) - apply (simp add: lub_unique A_def isLub_def) -apply (simp add: isLub_def r_def A_def) -done - -lemma (in CL) lub_in_lattice: "S <= A ==> lub S cl \ A" -apply (rule CL_imp_ex_isLub [THEN exE], assumption) -apply (unfold lub_def least_def) -apply (subst some_equality) -apply (simp add: isLub_def) -prefer 2 apply (simp add: isLub_def A_def) -apply (simp add: lub_unique A_def isLub_def) -done - -lemma (in CL) lubI: - "[| S <= A; L \ A; \x \ S. (x,L) \ r; - \z \ A. (\y \ S. (y,z) \ r) --> (L,z) \ r |] ==> L = lub S cl" -apply (rule lub_unique, assumption) -apply (simp add: isLub_def A_def r_def) -apply (unfold isLub_def) -apply (rule conjI) -apply (fold A_def r_def) -apply (rule lub_in_lattice, assumption) -apply (simp add: lub_upper lub_least) -done - -lemma (in CL) lubIa: "[| S <= A; isLub S cl L |] ==> L = lub S cl" -by (simp add: lubI isLub_def A_def r_def) - -lemma (in CL) isLub_in_lattice: "isLub S cl L ==> L \ A" -by (simp add: isLub_def A_def) - -lemma (in CL) isLub_upper: "[|isLub S cl L; y \ S|] ==> (y, L) \ r" -by (simp add: isLub_def r_def) - -lemma (in CL) isLub_least: - "[| isLub S cl L; z \ A; \y \ S. (y, z) \ r|] ==> (L, z) \ r" -by (simp add: isLub_def A_def r_def) - -lemma (in CL) isLubI: - "[| L \ A; \y \ S. (y, L) \ r; - (\z \ A. (\y \ S. (y, z):r) --> (L, z) \ r)|] ==> isLub S cl L" -by (simp add: isLub_def A_def r_def) - - -subsubsection {* glb *} - -lemma (in CL) glb_in_lattice: "S <= A ==> glb S cl \ A" -apply (subst glb_dual_lub) -apply (simp add: A_def) -apply (rule dualA_iff [THEN subst]) -apply (rule Tarski.lub_in_lattice) -apply (rule dualPO) -apply (rule CL_dualCL) -apply (simp add: dualA_iff) -done - -lemma (in CL) glb_lower: "[|S <= A; x \ S|] ==> (glb S cl, x) \ r" -apply (subst glb_dual_lub) -apply (simp add: r_def) -apply (rule dualr_iff [THEN subst]) -apply (rule Tarski.lub_upper [rule_format]) -apply (rule dualPO) -apply (rule CL_dualCL) -apply (simp add: dualA_iff A_def, assumption) -done - -text {* - Reduce the sublattice property by using substructural properties; - abandoned see @{text "Tarski_4.ML"}. -*} - -lemma (in CLF) [simp]: - "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" -apply (insert f_cl) -apply (simp add: CLF_def) -done - -declare (in CLF) f_cl [simp] - - -lemma (in CLF) f_in_funcset: "f \ A -> A" -by (simp add: A_def) - -lemma (in CLF) monotone_f: "monotone f A r" -by (simp add: A_def r_def) - -lemma (in CLF) CLF_dual: "(cl,f) \ CLF ==> (dual cl, f) \ CLF" -apply (simp add: CLF_def CL_dualCL monotone_dual) -apply (simp add: dualA_iff) -done - - -subsubsection {* fixed points *} - -lemma fix_subset: "fix f A <= A" -by (simp add: fix_def, fast) - -lemma fix_imp_eq: "x \ fix f A ==> f x = x" -by (simp add: fix_def) - -lemma fixf_subset: - "[| A <= B; x \ fix (%y: A. f y) A |] ==> x \ fix f B" -apply (simp add: fix_def, auto) -done - - -subsubsection {* lemmas for Tarski, lub *} -lemma (in CLF) lubH_le_flubH: - "H = {x. (x, f x) \ r & x \ A} ==> (lub H cl, f (lub H cl)) \ r" -apply (rule lub_least, fast) -apply (rule f_in_funcset [THEN funcset_mem]) -apply (rule lub_in_lattice, fast) --- {* @{text "\x:H. (x, f (lub H r)) \ r"} *} -apply (rule ballI) -apply (rule transE) -apply (rule CO_trans) --- {* instantiates @{text "(x, ???z) \ order cl to (x, f x)"}, *} --- {* because of the def of @{text H} *} -apply fast --- {* so it remains to show @{text "(f x, f (lub H cl)) \ r"} *} -apply (rule_tac f = "f" in monotoneE) -apply (rule monotone_f, fast) -apply (rule lub_in_lattice, fast) -apply (rule lub_upper, fast) -apply assumption -done - -lemma (in CLF) flubH_le_lubH: - "[| H = {x. (x, f x) \ r & x \ A} |] ==> (f (lub H cl), lub H cl) \ r" -apply (rule lub_upper, fast) -apply (rule_tac t = "H" in ssubst, assumption) -apply (rule CollectI) -apply (rule conjI) -apply (rule_tac [2] f_in_funcset [THEN funcset_mem]) -apply (rule_tac [2] lub_in_lattice) -prefer 2 apply fast -apply (rule_tac f = "f" in monotoneE) -apply (rule monotone_f) - apply (blast intro: lub_in_lattice) - apply (blast intro: lub_in_lattice f_in_funcset [THEN funcset_mem]) -apply (simp add: lubH_le_flubH) -done - -lemma (in CLF) lubH_is_fixp: - "H = {x. (x, f x) \ r & x \ A} ==> lub H cl \ fix f A" -apply (simp add: fix_def) -apply (rule conjI) -apply (rule lub_in_lattice, fast) -apply (rule antisymE) -apply (rule CO_antisym) -apply (simp add: flubH_le_lubH) -apply (simp add: lubH_le_flubH) -done - -lemma (in CLF) fix_in_H: - "[| H = {x. (x, f x) \ r & x \ A}; x \ P |] ==> x \ H" -by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl - fix_subset [of f A, THEN subsetD]) - -lemma (in CLF) fixf_le_lubH: - "H = {x. (x, f x) \ r & x \ A} ==> \x \ fix f A. (x, lub H cl) \ r" -apply (rule ballI) -apply (rule lub_upper, fast) -apply (rule fix_in_H) -apply (simp_all add: P_def) -done - -lemma (in CLF) lubH_least_fixf: - "H = {x. (x, f x) \ r & x \ A} - ==> \L. (\y \ fix f A. (y,L) \ r) --> (lub H cl, L) \ r" -apply (rule allI) -apply (rule impI) -apply (erule bspec) -apply (rule lubH_is_fixp, assumption) -done - -subsubsection {* Tarski fixpoint theorem 1, first part *} -lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \ r & x \ A} cl" -apply (rule sym) -apply (simp add: P_def) -apply (rule lubI) -apply (rule fix_subset) -apply (rule lub_in_lattice, fast) -apply (simp add: fixf_le_lubH) -apply (simp add: lubH_least_fixf) -done - -lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \ r & x \ A} ==> glb H cl \ P" - -- {* Tarski for glb *} -apply (simp add: glb_dual_lub P_def A_def r_def) -apply (rule dualA_iff [THEN subst]) -apply (rule Tarski.lubH_is_fixp) -apply (rule dualPO) -apply (rule CL_dualCL) -apply (rule f_cl [THEN CLF_dual]) -apply (simp add: dualr_iff dualA_iff) -done - -lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \ r & x \ A} cl" -apply (simp add: glb_dual_lub P_def A_def r_def) -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 *} - -lemma (in CLF) rel_imp_elem: "(x, y) \ r ==> x \ A" -apply (insert CO_refl) -apply (simp add: refl_def, blast) -done - -lemma (in CLF) interval_subset: "[| a \ A; b \ A |] ==> interval r a b <= A" -apply (simp add: interval_def) -apply (blast intro: rel_imp_elem) -done - -lemma (in CLF) intervalI: - "[| (a, x) \ r; (x, b) \ r |] ==> x \ interval r a b" -apply (simp add: interval_def) -done - -lemma (in CLF) interval_lemma1: - "[| S <= interval r a b; x \ S |] ==> (a, x) \ r" -apply (unfold interval_def, fast) -done - -lemma (in CLF) interval_lemma2: - "[| S <= interval r a b; x \ S |] ==> (x, b) \ r" -apply (unfold interval_def, fast) -done - -lemma (in CLF) a_less_lub: - "[| S <= A; S \ {}; - \x \ S. (a,x) \ r; \y \ S. (y, L) \ r |] ==> (a,L) \ r" -by (blast intro: transE PO_imp_trans) - -lemma (in CLF) glb_less_b: - "[| S <= A; S \ {}; - \x \ S. (x,b) \ r; \y \ S. (G, y) \ r |] ==> (G,b) \ r" -by (blast intro: transE PO_imp_trans) - -lemma (in CLF) S_intv_cl: - "[| a \ A; b \ A; S <= interval r a b |]==> S <= A" -by (simp add: subset_trans [OF _ interval_subset]) - -lemma (in CLF) L_in_interval: - "[| a \ A; b \ A; S <= interval r a b; - S \ {}; isLub S cl L; interval r a b \ {} |] ==> L \ interval r a b" -apply (rule intervalI) -apply (rule a_less_lub) -prefer 2 apply assumption -apply (simp add: S_intv_cl) -apply (rule ballI) -apply (simp add: interval_lemma1) -apply (simp add: isLub_upper) --- {* @{text "(L, b) \ r"} *} -apply (simp add: isLub_least interval_lemma2) -done - -lemma (in CLF) G_in_interval: - "[| a \ A; b \ A; interval r a b \ {}; S <= interval r a b; isGlb S cl G; - S \ {} |] ==> G \ interval r a b" -apply (simp add: interval_dual) -apply (simp add: Tarski.L_in_interval [of _ f] - dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) -done - -lemma (in CLF) intervalPO: - "[| a \ A; b \ A; interval r a b \ {} |] - ==> (| pset = interval r a b, order = induced (interval r a b) r |) - \ PartialOrder" -apply (rule po_subset_po) -apply (simp add: interval_subset) -done - -lemma (in CLF) intv_CL_lub: - "[| a \ A; b \ A; interval r a b \ {} |] - ==> \S. S <= interval r a b --> - (\L. isLub S (| pset = interval r a b, - order = induced (interval r a b) r |) L)" -apply (intro strip) -apply (frule S_intv_cl [THEN CL_imp_ex_isLub]) -prefer 2 apply assumption -apply assumption -apply (erule exE) --- {* define the lub for the interval as *} -apply (rule_tac x = "if S = {} then a else L" in exI) -apply (simp (no_asm_simp) add: isLub_def split del: split_if) -apply (intro impI conjI) --- {* @{text "(if S = {} then a else L) \ interval r a b"} *} -apply (simp add: CL_imp_PO L_in_interval) -apply (simp add: left_in_interval) --- {* lub prop 1 *} -apply (case_tac "S = {}") --- {* @{text "S = {}, y \ S = False => everything"} *} -apply fast --- {* @{text "S \ {}"} *} -apply simp --- {* @{text "\y:S. (y, L) \ induced (interval r a b) r"} *} -apply (rule ballI) -apply (simp add: induced_def L_in_interval) -apply (rule conjI) -apply (rule subsetD) -apply (simp add: S_intv_cl, assumption) -apply (simp add: isLub_upper) --- {* @{text "\z:interval r a b. (\y:S. (y, z) \ induced (interval r a b) r \ (if S = {} then a else L, z) \ induced (interval r a b) r"} *} -apply (rule ballI) -apply (rule impI) -apply (case_tac "S = {}") --- {* @{text "S = {}"} *} -apply simp -apply (simp add: induced_def interval_def) -apply (rule conjI) -apply (rule reflE) -apply (rule CO_refl, assumption) -apply (rule interval_not_empty) -apply (rule CO_trans) -apply (simp add: interval_def) --- {* @{text "S \ {}"} *} -apply simp -apply (simp add: induced_def L_in_interval) -apply (rule isLub_least, assumption) -apply (rule subsetD) -prefer 2 apply assumption -apply (simp add: S_intv_cl, fast) -done - -lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] - -lemma (in CLF) interval_is_sublattice: - "[| a \ A; b \ A; interval r a b \ {} |] - ==> interval r a b <<= cl" -apply (rule sublatticeI) -apply (simp add: interval_subset) -apply (rule CompleteLatticeI) -apply (simp add: intervalPO) - apply (simp add: intv_CL_lub) -apply (simp add: intv_CL_glb) -done - -lemmas (in CLF) interv_is_compl_latt = - interval_is_sublattice [THEN sublattice_imp_CL] - - -subsubsection {* 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) - -lemma (in CLF) Bot_in_lattice: "Bot cl \ A" -apply (simp add: Bot_def least_def) -apply (rule someI2) -apply (fold A_def) -apply (erule_tac [2] conjunct1) -apply (rule conjI) -apply (rule glb_in_lattice) -apply (rule subset_refl) -apply (fold r_def) -apply (simp add: glb_lower) -done - -lemma (in CLF) Top_in_lattice: "Top cl \ A" -apply (simp add: Top_dual_Bot A_def) -apply (rule dualA_iff [THEN subst]) -apply (blast intro!: Tarski.Bot_in_lattice dualPO CL_dualCL CLF_dual f_cl) -done - -lemma (in CLF) Top_prop: "x \ A ==> (x, Top cl) \ r" -apply (simp add: Top_def greatest_def) -apply (rule someI2) -apply (fold r_def A_def) -prefer 2 apply fast -apply (intro conjI ballI) -apply (rule_tac [2] lub_upper) -apply (auto simp add: lub_in_lattice) -done - -lemma (in CLF) Bot_prop: "x \ A ==> (Bot cl, x) \ r" -apply (simp add: Bot_dual_Top r_def) -apply (rule dualr_iff [THEN subst]) -apply (simp add: Tarski.Top_prop [of _ f] - dualA_iff A_def dualPO CL_dualCL CLF_dual) -done - -lemma (in CLF) Top_intv_not_empty: "x \ A ==> interval r x (Top cl) \ {}" -apply (rule notI) -apply (drule_tac a = "Top cl" in equals0D) -apply (simp add: interval_def) -apply (simp add: refl_def Top_in_lattice Top_prop) -done - -lemma (in CLF) Bot_intv_not_empty: "x \ A ==> interval r (Bot cl) x \ {}" -apply (simp add: Bot_dual_Top) -apply (subst interval_dual) -prefer 2 apply assumption -apply (simp add: A_def) -apply (rule dualA_iff [THEN subst]) -apply (blast intro!: Tarski.Top_in_lattice - 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 *} - -lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \ PartialOrder" -by (simp add: P_def fix_subset po_subset_po) - -lemma (in Tarski) Y_subset_A: "Y <= A" -apply (rule subset_trans [OF _ fix_subset]) -apply (rule Y_ss [simplified P_def]) -done - -lemma (in Tarski) lubY_in_A: "lub Y cl \ A" -by (simp add: Y_subset_A [THEN lub_in_lattice]) - -lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \ r" -apply (rule lub_least) -apply (rule Y_subset_A) -apply (rule f_in_funcset [THEN funcset_mem]) -apply (rule lubY_in_A) --- {* @{text "Y <= P ==> f x = x"} *} -apply (rule ballI) -apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) -apply (erule Y_ss [simplified P_def, THEN subsetD]) --- {* @{text "reduce (f x, f (lub Y cl)) \ r to (x, lub Y cl) \ r"} by monotonicity *} -apply (rule_tac f = "f" in monotoneE) -apply (rule monotone_f) -apply (simp add: Y_subset_A [THEN subsetD]) -apply (rule lubY_in_A) -apply (simp add: lub_upper Y_subset_A) -done - -lemma (in Tarski) intY1_subset: "intY1 <= A" -apply (unfold intY1_def) -apply (rule interval_subset) -apply (rule lubY_in_A) -apply (rule Top_in_lattice) -done - -lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] - -lemma (in Tarski) intY1_f_closed: "x \ intY1 \ f x \ intY1" -apply (simp add: intY1_def interval_def) -apply (rule conjI) -apply (rule transE) -apply (rule CO_trans) -apply (rule lubY_le_flubY) --- {* @{text "(f (lub Y cl), f x) \ r"} *} -apply (rule_tac f=f in monotoneE) -apply (rule monotone_f) -apply (rule lubY_in_A) -apply (simp add: intY1_def interval_def intY1_elem) -apply (simp add: intY1_def interval_def) --- {* @{text "(f x, Top cl) \ r"} *} -apply (rule Top_prop) -apply (rule f_in_funcset [THEN funcset_mem]) -apply (simp add: intY1_def interval_def intY1_elem) -done - -lemma (in Tarski) intY1_func: "(%x: intY1. f x) \ intY1 -> intY1" -apply (rule restrictI) -apply (erule intY1_f_closed) -done - -lemma (in Tarski) intY1_mono: - "monotone (%x: intY1. f x) intY1 (induced intY1 r)" -apply (auto simp add: monotone_def induced_def intY1_f_closed) -apply (blast intro: intY1_elem monotone_f [THEN monotoneE]) -done - -lemma (in Tarski) intY1_is_cl: - "(| pset = intY1, order = induced intY1 r |) \ CompleteLattice" -apply (unfold intY1_def) -apply (rule interv_is_compl_latt) -apply (rule lubY_in_A) -apply (rule Top_in_lattice) -apply (rule Top_intv_not_empty) -apply (rule lubY_in_A) -done - -lemma (in Tarski) v_in_P: "v \ P" -apply (unfold P_def) -apply (rule_tac A = "intY1" in fixf_subset) -apply (rule intY1_subset) -apply (simp add: Tarski.glbH_is_fixp [OF _ intY1_is_cl, simplified] - v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono) -done - -lemma (in Tarski) z_in_interval: - "[| z \ P; \y\Y. (y, z) \ induced P r |] ==> z \ intY1" -apply (unfold intY1_def P_def) -apply (rule intervalI) -prefer 2 - apply (erule fix_subset [THEN subsetD, THEN Top_prop]) -apply (rule lub_least) -apply (rule Y_subset_A) -apply (fast elim!: fix_subset [THEN subsetD]) -apply (simp add: induced_def) -done - -lemma (in Tarski) f'z_in_int_rel: "[| z \ P; \y\Y. (y, z) \ induced P r |] - ==> ((%x: intY1. f x) z, z) \ induced intY1 r" -apply (simp add: induced_def intY1_f_closed z_in_interval P_def) -apply (simp add: fix_imp_eq [of _ f A] fix_subset [of f A, THEN subsetD] - CO_refl [THEN reflE]) -done - -lemma (in Tarski) tarski_full_lemma: - "\L. isLub Y (| pset = P, order = induced P r |) L" -apply (rule_tac x = "v" in exI) -apply (simp add: isLub_def) --- {* @{text "v \ P"} *} -apply (simp add: v_in_P) -apply (rule conjI) --- {* @{text v} is lub *} --- {* @{text "1. \y:Y. (y, v) \ induced P r"} *} -apply (rule ballI) -apply (simp add: induced_def subsetD v_in_P) -apply (rule conjI) -apply (erule Y_ss [THEN subsetD]) -apply (rule_tac b = "lub Y cl" in transE) -apply (rule CO_trans) -apply (rule lub_upper) -apply (rule Y_subset_A, assumption) -apply (rule_tac b = "Top cl" in interval_imp_mem) -apply (simp add: v_def) -apply (fold intY1_def) -apply (rule Tarski.glb_in_lattice [OF _ intY1_is_cl, simplified]) - apply (simp add: CL_imp_PO intY1_is_cl, force) --- {* @{text v} is LEAST ub *} -apply clarify -apply (rule indI) - prefer 3 apply assumption - prefer 2 apply (simp add: v_in_P) -apply (unfold v_def) -apply (rule indE) -apply (rule_tac [2] intY1_subset) -apply (rule Tarski.glb_lower [OF _ intY1_is_cl, simplified]) - apply (simp add: CL_imp_PO intY1_is_cl) - apply force -apply (simp add: induced_def intY1_f_closed z_in_interval) -apply (simp add: P_def fix_imp_eq [of _ f A] - fix_subset [of f A, THEN subsetD] - CO_refl [THEN reflE]) -done - -lemma CompleteLatticeI_simp: - "[| (| pset = A, order = r |) \ PartialOrder; - \S. S <= A --> (\L. isLub S (| pset = A, order = r |) L) |] - ==> (| pset = A, order = r |) \ CompleteLattice" -by (simp add: CompleteLatticeI Rdual) - -theorem (in CLF) Tarski_full: - "(| pset = P, order = induced P r|) \ CompleteLattice" -apply (rule CompleteLatticeI_simp) -apply (rule fixf_po, clarify) -apply (simp add: P_def A_def r_def) -apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl) -done - -end -- cgit v1.2.3