diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1209 +1,1208 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_theories Tools.Code_Generator document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples for Isabelle/HOL. " sessions "HOL-Computational_Algebra" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Functions Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Rewrite_Examples Seq Sqrt document_files "root.bib" "root.tex" session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral Code_Target_Numeral_Float Complex_Order DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Combinatorics" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Combinatorics" (main timing) in "Combinatorics" = "HOL" + sessions "HOL-Library" theories Combinatorics document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree23_of_List Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Queue_2Lists Heaps Leftist_Heap Binomial_Heap Selection document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + sessions "HOL-Number_Theory" "HOL-Data_Structures" "HOL-Examples" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " options [kodkod_scala] sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" "HOL-Combinatorics" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). \ options [print_mode = "no_brackets", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples and experiments for Isabelle/HOL. " theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples - Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Function_Growth Gauge_Integration HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Specifications_with_bundle_mixins Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] sessions "HOL-Hoare" theories Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + sessions "HOL-Combinatorics" theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid Regex_ACI Regex_ACIDZ TLList FAE_Sequence Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + description "Some arbitrary small test case for Mirabelle." options [timeout = 60, mirabelle_theories = "HOL-Analysis.Inner_Product", mirabelle_actions = "arith"] sessions "HOL-Analysis" theories "HOL-Analysis.Inner_Product" session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] sessions "HOL-Library" theories Boogie SMT_Examples SMT_Word_Examples SMT_Examples_Verit SMT_Tests_Verit theories [condition = Z3_INSTALLED] SMT_Tests session "HOL-SPARK" in "SPARK" = HOL + sessions "HOL-Library" theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-Library" "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_theories "HOL-SPARK-Examples.Greatest_Common_Divisor" document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 theories [condition = ISABELLE_SWIPL] Code_Prolog_Examples Context_Free_Grammar_Example Hotel_Example_Prolog Lambda_Example List_Examples theories [condition = ISABELLE_SWIPL, quick_and_dirty] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Müller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Müller The Alternating Bit Protocol performed in I/O-Automata: combining IOA with Model Checking. Theory Correctness contains the proof of the abstraction from unbounded channels to finite ones. File Check.ML contains a simple ModelChecker prototype checking Spec against the finite version of the ABP-protocol. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Müller. " theories Overview Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Müller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Müller " theories TrivEx TrivEx2 diff --git a/src/HOL/Real.thy b/src/HOL/Real.thy --- a/src/HOL/Real.thy +++ b/src/HOL/Real.thy @@ -1,1772 +1,1772 @@ (* Title: HOL/Real.thy Author: Jacques D. Fleuriot, University of Edinburgh, 1998 Author: Larry Paulson, University of Cambridge Author: Jeremy Avigad, Carnegie Mellon University Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 Construction of Cauchy Reals by Brian Huffman, 2010 *) section \Development of the Reals using Cauchy Sequences\ theory Real imports Rat begin text \ This theory contains a formalization of the real numbers as equivalence - classes of Cauchy sequences of rationals. See - \<^file>\~~/src/HOL/ex/Dedekind_Real.thy\ for an alternative construction using + classes of Cauchy sequences of rationals. See the AFP entry + @{text Dedekind_Real} for an alternative construction using Dedekind cuts. \ subsection \Preliminary lemmas\ text\Useful in convergence arguments\ lemma inverse_of_nat_le: fixes n::nat shows "\n \ m; n\0\ \ 1 / of_nat m \ (1::'a::linordered_field) / of_nat n" by (simp add: frac_le) lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)" for a b c d :: "'a::ab_group_add" by simp lemma minus_diff_minus: "- a - - b = - (a - b)" for a b :: "'a::ab_group_add" by simp lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b" for x y a b :: "'a::ring" by (simp add: algebra_simps) lemma inverse_diff_inverse: fixes a b :: "'a::division_ring" assumes "a \ 0" and "b \ 0" shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)" using assms by (simp add: algebra_simps) lemma obtain_pos_sum: fixes r :: rat assumes r: "0 < r" obtains s t where "0 < s" and "0 < t" and "r = s + t" proof from r show "0 < r/2" by simp from r show "0 < r/2" by simp show "r = r/2 + r/2" by simp qed subsection \Sequences that converge to zero\ definition vanishes :: "(nat \ rat) \ bool" where "vanishes X \ (\r>0. \k. \n\k. \X n\ < r)" lemma vanishesI: "(\r. 0 < r \ \k. \n\k. \X n\ < r) \ vanishes X" unfolding vanishes_def by simp lemma vanishesD: "vanishes X \ 0 < r \ \k. \n\k. \X n\ < r" unfolding vanishes_def by simp lemma vanishes_const [simp]: "vanishes (\n. c) \ c = 0" proof (cases "c = 0") case True then show ?thesis by (simp add: vanishesI) next case False then show ?thesis unfolding vanishes_def using zero_less_abs_iff by blast qed lemma vanishes_minus: "vanishes X \ vanishes (\n. - X n)" unfolding vanishes_def by simp lemma vanishes_add: assumes X: "vanishes X" and Y: "vanishes Y" shows "vanishes (\n. X n + Y n)" proof (rule vanishesI) fix r :: rat assume "0 < r" then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\n\i. \X n\ < s" using vanishesD [OF X s] .. obtain j where j: "\n\j. \Y n\ < t" using vanishesD [OF Y t] .. have "\n\max i j. \X n + Y n\ < r" proof clarsimp fix n assume n: "i \ n" "j \ n" have "\X n + Y n\ \ \X n\ + \Y n\" by (rule abs_triangle_ineq) also have "\ < s + t" by (simp add: add_strict_mono i j n) finally show "\X n + Y n\ < r" by (simp only: r) qed then show "\k. \n\k. \X n + Y n\ < r" .. qed lemma vanishes_diff: assumes "vanishes X" "vanishes Y" shows "vanishes (\n. X n - Y n)" unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus assms) lemma vanishes_mult_bounded: assumes X: "\a>0. \n. \X n\ < a" assumes Y: "vanishes (\n. Y n)" shows "vanishes (\n. X n * Y n)" proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a where a: "0 < a" "\n. \X n\ < a" using X by blast obtain b where b: "0 < b" "r = a * b" proof show "0 < r / a" using r a by simp show "r = a * (r / a)" using a by simp qed obtain k where k: "\n\k. \Y n\ < b" using vanishesD [OF Y b(1)] .. have "\n\k. \X n * Y n\ < r" by (simp add: b(2) abs_mult mult_strict_mono' a k) then show "\k. \n\k. \X n * Y n\ < r" .. qed subsection \Cauchy sequences\ definition cauchy :: "(nat \ rat) \ bool" where "cauchy X \ (\r>0. \k. \m\k. \n\k. \X m - X n\ < r)" lemma cauchyI: "(\r. 0 < r \ \k. \m\k. \n\k. \X m - X n\ < r) \ cauchy X" unfolding cauchy_def by simp lemma cauchyD: "cauchy X \ 0 < r \ \k. \m\k. \n\k. \X m - X n\ < r" unfolding cauchy_def by simp lemma cauchy_const [simp]: "cauchy (\n. x)" unfolding cauchy_def by simp lemma cauchy_add [simp]: assumes X: "cauchy X" and Y: "cauchy Y" shows "cauchy (\n. X n + Y n)" proof (rule cauchyI) fix r :: rat assume "0 < r" then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t" using cauchyD [OF Y t] .. have "\m\max i j. \n\max i j. \(X m + Y m) - (X n + Y n)\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\(X m + Y m) - (X n + Y n)\ \ \X m - X n\ + \Y m - Y n\" unfolding add_diff_add by (rule abs_triangle_ineq) also have "\ < s + t" by (rule add_strict_mono) (simp_all add: i j *) finally show "\(X m + Y m) - (X n + Y n)\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \(X m + Y m) - (X n + Y n)\ < r" .. qed lemma cauchy_minus [simp]: assumes X: "cauchy X" shows "cauchy (\n. - X n)" using assms unfolding cauchy_def unfolding minus_diff_minus abs_minus_cancel . lemma cauchy_diff [simp]: assumes "cauchy X" "cauchy Y" shows "cauchy (\n. X n - Y n)" using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff) lemma cauchy_imp_bounded: assumes "cauchy X" shows "\b>0. \n. \X n\ < b" proof - obtain k where k: "\m\k. \n\k. \X m - X n\ < 1" using cauchyD [OF assms zero_less_one] .. show "\b>0. \n. \X n\ < b" proof (intro exI conjI allI) have "0 \ \X 0\" by simp also have "\X 0\ \ Max (abs ` X ` {..k})" by simp finally have "0 \ Max (abs ` X ` {..k})" . then show "0 < Max (abs ` X ` {..k}) + 1" by simp next fix n :: nat show "\X n\ < Max (abs ` X ` {..k}) + 1" proof (rule linorder_le_cases) assume "n \ k" then have "\X n\ \ Max (abs ` X ` {..k})" by simp then show "\X n\ < Max (abs ` X ` {..k}) + 1" by simp next assume "k \ n" have "\X n\ = \X k + (X n - X k)\" by simp also have "\X k + (X n - X k)\ \ \X k\ + \X n - X k\" by (rule abs_triangle_ineq) also have "\ < Max (abs ` X ` {..k}) + 1" by (rule add_le_less_mono) (simp_all add: k \k \ n\) finally show "\X n\ < Max (abs ` X ` {..k}) + 1" . qed qed qed lemma cauchy_mult [simp]: assumes X: "cauchy X" and Y: "cauchy Y" shows "cauchy (\n. X n * Y n)" proof (rule cauchyI) fix r :: rat assume "0 < r" then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v" by (rule obtain_pos_sum) obtain a where a: "0 < a" "\n. \X n\ < a" using cauchy_imp_bounded [OF X] by blast obtain b where b: "0 < b" "\n. \Y n\ < b" using cauchy_imp_bounded [OF Y] by blast obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b" proof show "0 < v/b" using v b(1) by simp show "0 < u/a" using u a(1) by simp show "r = a * (u/a) + (v/b) * b" using a(1) b(1) \r = u + v\ by simp qed obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t" using cauchyD [OF Y t] .. have "\m\max i j. \n\max i j. \X m * Y m - X n * Y n\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\X m * Y m - X n * Y n\ = \X m * (Y m - Y n) + (X m - X n) * Y n\" unfolding mult_diff_mult .. also have "\ \ \X m * (Y m - Y n)\ + \(X m - X n) * Y n\" by (rule abs_triangle_ineq) also have "\ = \X m\ * \Y m - Y n\ + \X m - X n\ * \Y n\" unfolding abs_mult .. also have "\ < a * t + s * b" by (simp_all add: add_strict_mono mult_strict_mono' a b i j *) finally show "\X m * Y m - X n * Y n\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \X m * Y m - X n * Y n\ < r" .. qed lemma cauchy_not_vanishes_cases: assumes X: "cauchy X" assumes nz: "\ vanishes X" shows "\b>0. \k. (\n\k. b < - X n) \ (\n\k. b < X n)" proof - obtain r where "0 < r" and r: "\k. \n\k. r \ \X n\" using nz unfolding vanishes_def by (auto simp add: not_less) obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t" using \0 < r\ by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain k where "i \ k" and "r \ \X k\" using r by blast have k: "\n\k. \X n - X k\ < s" using i \i \ k\ by auto have "X k \ - r \ r \ X k" using \r \ \X k\\ by auto then have "(\n\k. t < - X n) \ (\n\k. t < X n)" unfolding \r = s + t\ using k by auto then have "\k. (\n\k. t < - X n) \ (\n\k. t < X n)" .. then show "\t>0. \k. (\n\k. t < - X n) \ (\n\k. t < X n)" using t by auto qed lemma cauchy_not_vanishes: assumes X: "cauchy X" and nz: "\ vanishes X" shows "\b>0. \k. \n\k. b < \X n\" using cauchy_not_vanishes_cases [OF assms] by (elim ex_forward conj_forward asm_rl) auto lemma cauchy_inverse [simp]: assumes X: "cauchy X" and nz: "\ vanishes X" shows "cauchy (\n. inverse (X n))" proof (rule cauchyI) fix r :: rat assume "0 < r" obtain b i where b: "0 < b" and i: "\n\i. b < \X n\" using cauchy_not_vanishes [OF X nz] by blast from b i have nz: "\n\i. X n \ 0" by auto obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b" proof show "0 < b * r * b" by (simp add: \0 < r\ b) show "r = inverse b * (b * r * b) * inverse b" using b by simp qed obtain j where j: "\m\j. \n\j. \X m - X n\ < s" using cauchyD [OF X s] .. have "\m\max i j. \n\max i j. \inverse (X m) - inverse (X n)\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\inverse (X m) - inverse (X n)\ = inverse \X m\ * \X m - X n\ * inverse \X n\" by (simp add: inverse_diff_inverse nz * abs_mult) also have "\ < inverse b * s * inverse b" by (simp add: mult_strict_mono less_imp_inverse_less i j b * s) finally show "\inverse (X m) - inverse (X n)\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \inverse (X m) - inverse (X n)\ < r" .. qed lemma vanishes_diff_inverse: assumes X: "cauchy X" "\ vanishes X" and Y: "cauchy Y" "\ vanishes Y" and XY: "vanishes (\n. X n - Y n)" shows "vanishes (\n. inverse (X n) - inverse (Y n))" proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a i where a: "0 < a" and i: "\n\i. a < \X n\" using cauchy_not_vanishes [OF X] by blast obtain b j where b: "0 < b" and j: "\n\j. b < \Y n\" using cauchy_not_vanishes [OF Y] by blast obtain s where s: "0 < s" and "inverse a * s * inverse b = r" proof show "0 < a * r * b" using a r b by simp show "inverse a * (a * r * b) * inverse b = r" using a r b by simp qed obtain k where k: "\n\k. \X n - Y n\ < s" using vanishesD [OF XY s] .. have "\n\max (max i j) k. \inverse (X n) - inverse (Y n)\ < r" proof clarsimp fix n assume n: "i \ n" "j \ n" "k \ n" with i j a b have "X n \ 0" and "Y n \ 0" by auto then have "\inverse (X n) - inverse (Y n)\ = inverse \X n\ * \X n - Y n\ * inverse \Y n\" by (simp add: inverse_diff_inverse abs_mult) also have "\ < inverse a * s * inverse b" by (intro mult_strict_mono' less_imp_inverse_less) (simp_all add: a b i j k n) also note \inverse a * s * inverse b = r\ finally show "\inverse (X n) - inverse (Y n)\ < r" . qed then show "\k. \n\k. \inverse (X n) - inverse (Y n)\ < r" .. qed subsection \Equivalence relation on Cauchy sequences\ definition realrel :: "(nat \ rat) \ (nat \ rat) \ bool" where "realrel = (\X Y. cauchy X \ cauchy Y \ vanishes (\n. X n - Y n))" lemma realrelI [intro?]: "cauchy X \ cauchy Y \ vanishes (\n. X n - Y n) \ realrel X Y" by (simp add: realrel_def) lemma realrel_refl: "cauchy X \ realrel X X" by (simp add: realrel_def) lemma symp_realrel: "symp realrel" by (simp add: abs_minus_commute realrel_def symp_def vanishes_def) lemma transp_realrel: "transp realrel" unfolding realrel_def by (rule transpI) (force simp add: dest: vanishes_add) lemma part_equivp_realrel: "part_equivp realrel" by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const) subsection \The field of real numbers\ quotient_type real = "nat \ rat" / partial: realrel morphisms rep_real Real by (rule part_equivp_realrel) lemma cr_real_eq: "pcr_real = (\x y. cauchy x \ Real x = y)" unfolding real.pcr_cr_eq cr_real_def realrel_def by auto lemma Real_induct [induct type: real]: (* TODO: generate automatically *) assumes "\X. cauchy X \ P (Real X)" shows "P x" proof (induct x) case (1 X) then have "cauchy X" by (simp add: realrel_def) then show "P (Real X)" by (rule assms) qed lemma eq_Real: "cauchy X \ cauchy Y \ Real X = Real Y \ vanishes (\n. X n - Y n)" using real.rel_eq_transfer unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy" by (simp add: real.domain_eq realrel_def) instantiation real :: field begin lift_definition zero_real :: "real" is "\n. 0" by (simp add: realrel_refl) lift_definition one_real :: "real" is "\n. 1" by (simp add: realrel_refl) lift_definition plus_real :: "real \ real \ real" is "\X Y n. X n + Y n" unfolding realrel_def add_diff_add by (simp only: cauchy_add vanishes_add simp_thms) lift_definition uminus_real :: "real \ real" is "\X n. - X n" unfolding realrel_def minus_diff_minus by (simp only: cauchy_minus vanishes_minus simp_thms) lift_definition times_real :: "real \ real \ real" is "\X Y n. X n * Y n" proof - fix f1 f2 f3 f4 have "\cauchy f1; cauchy f4; vanishes (\n. f1 n - f2 n); vanishes (\n. f3 n - f4 n)\ \ vanishes (\n. f1 n * (f3 n - f4 n) + f4 n * (f1 n - f2 n))" by (simp add: vanishes_add vanishes_mult_bounded cauchy_imp_bounded) then show "\realrel f1 f2; realrel f3 f4\ \ realrel (\n. f1 n * f3 n) (\n. f2 n * f4 n)" by (simp add: mult.commute realrel_def mult_diff_mult) qed lift_definition inverse_real :: "real \ real" is "\X. if vanishes X then (\n. 0) else (\n. inverse (X n))" proof - fix X Y assume "realrel X Y" then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\n. X n - Y n)" by (simp_all add: realrel_def) have "vanishes X \ vanishes Y" proof assume "vanishes X" from vanishes_diff [OF this XY] show "vanishes Y" by simp next assume "vanishes Y" from vanishes_add [OF this XY] show "vanishes X" by simp qed then show "?thesis X Y" by (simp add: vanishes_diff_inverse X Y XY realrel_def) qed definition "x - y = x + - y" for x y :: real definition "x div y = x * inverse y" for x y :: real lemma add_Real: "cauchy X \ cauchy Y \ Real X + Real Y = Real (\n. X n + Y n)" using plus_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma minus_Real: "cauchy X \ - Real X = Real (\n. - X n)" using uminus_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma diff_Real: "cauchy X \ cauchy Y \ Real X - Real Y = Real (\n. X n - Y n)" by (simp add: minus_Real add_Real minus_real_def) lemma mult_Real: "cauchy X \ cauchy Y \ Real X * Real Y = Real (\n. X n * Y n)" using times_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma inverse_Real: "cauchy X \ inverse (Real X) = (if vanishes X then 0 else Real (\n. inverse (X n)))" using inverse_real.transfer zero_real.transfer unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis) instance proof fix a b c :: real show "a + b = b + a" by transfer (simp add: ac_simps realrel_def) show "(a + b) + c = a + (b + c)" by transfer (simp add: ac_simps realrel_def) show "0 + a = a" by transfer (simp add: realrel_def) show "- a + a = 0" by transfer (simp add: realrel_def) show "a - b = a + - b" by (rule minus_real_def) show "(a * b) * c = a * (b * c)" by transfer (simp add: ac_simps realrel_def) show "a * b = b * a" by transfer (simp add: ac_simps realrel_def) show "1 * a = a" by transfer (simp add: ac_simps realrel_def) show "(a + b) * c = a * c + b * c" by transfer (simp add: distrib_right realrel_def) show "(0::real) \ (1::real)" by transfer (simp add: realrel_def) have "vanishes (\n. inverse (X n) * X n - 1)" if X: "cauchy X" "\ vanishes X" for X proof (rule vanishesI) fix r::rat assume "0 < r" obtain b k where "b>0" "\n\k. b < \X n\" using X cauchy_not_vanishes by blast then show "\k. \n\k. \inverse (X n) * X n - 1\ < r" using \0 < r\ by force qed then show "a \ 0 \ inverse a * a = 1" by transfer (simp add: realrel_def) show "a div b = a * inverse b" by (rule divide_real_def) show "inverse (0::real) = 0" by transfer (simp add: realrel_def) qed end subsection \Positive reals\ lift_definition positive :: "real \ bool" is "\X. \r>0. \k. \n\k. r < X n" proof - have 1: "\r>0. \k. \n\k. r < Y n" if *: "realrel X Y" and **: "\r>0. \k. \n\k. r < X n" for X Y proof - from * have XY: "vanishes (\n. X n - Y n)" by (simp_all add: realrel_def) from ** obtain r i where "0 < r" and i: "\n\i. r < X n" by blast obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" using \0 < r\ by (rule obtain_pos_sum) obtain j where j: "\n\j. \X n - Y n\ < s" using vanishesD [OF XY s] .. have "\n\max i j. t < Y n" proof clarsimp fix n assume n: "i \ n" "j \ n" have "\X n - Y n\ < s" and "r < X n" using i j n by simp_all then show "t < Y n" by (simp add: r) qed then show ?thesis using t by blast qed fix X Y assume "realrel X Y" then have "realrel X Y" and "realrel Y X" using symp_realrel by (auto simp: symp_def) then show "?thesis X Y" by (safe elim!: 1) qed lemma positive_Real: "cauchy X \ positive (Real X) \ (\r>0. \k. \n\k. r < X n)" using positive.transfer by (simp add: cr_real_eq rel_fun_def) lemma positive_zero: "\ positive 0" by transfer auto lemma positive_add: assumes "positive x" "positive y" shows "positive (x + y)" proof - have *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\ \ a+b < x n + y n" for x y and a b::rat and i j n::nat by (simp add: add_strict_mono) show ?thesis using assms by transfer (blast intro: * pos_add_strict) qed lemma positive_mult: assumes "positive x" "positive y" shows "positive (x * y)" proof - have *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\ \ a*b < x n * y n" for x y and a b::rat and i j n::nat by (simp add: mult_strict_mono') show ?thesis using assms by transfer (blast intro: * mult_pos_pos) qed lemma positive_minus: "\ positive x \ x \ 0 \ positive (- x)" apply transfer apply (simp add: realrel_def) apply (blast dest: cauchy_not_vanishes_cases) done instantiation real :: linordered_field begin definition "x < y \ positive (y - x)" definition "x \ y \ x < y \ x = y" for x y :: real definition "\a\ = (if a < 0 then - a else a)" for a :: real definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: real instance proof fix a b c :: real show "\a\ = (if a < 0 then - a else a)" by (rule abs_real_def) show "a < b \ a \ b \ \ b \ a" "a \ b \ b \ c \ a \ c" "a \ a" "a \ b \ b \ a \ a = b" "a \ b \ c + a \ c + b" unfolding less_eq_real_def less_real_def by (force simp add: positive_zero dest: positive_add)+ show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" by (rule sgn_real_def) show "a \ b \ b \ a" by (auto dest!: positive_minus simp: less_eq_real_def less_real_def) show "a < b \ 0 < c \ c * a < c * b" unfolding less_real_def by (force simp add: algebra_simps dest: positive_mult) qed end instantiation real :: distrib_lattice begin definition "(inf :: real \ real \ real) = min" definition "(sup :: real \ real \ real) = max" instance by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2) end lemma of_nat_Real: "of_nat x = Real (\n. of_nat x)" by (induct x) (simp_all add: zero_real_def one_real_def add_Real) lemma of_int_Real: "of_int x = Real (\n. of_int x)" by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real) lemma of_rat_Real: "of_rat x = Real (\n. x)" proof (induct x) case (Fract a b) then show ?case apply (simp add: Fract_of_int_quotient of_rat_divide) apply (simp add: of_int_Real divide_inverse inverse_Real mult_Real) done qed instance real :: archimedean_field proof show "\z. x \ of_int z" for x :: real proof (induct x) case (1 X) then obtain b where "0 < b" and b: "\n. \X n\ < b" by (blast dest: cauchy_imp_bounded) then have "Real X < of_int (\b\ + 1)" using 1 apply (simp add: of_int_Real less_real_def diff_Real positive_Real) apply (rule_tac x=1 in exI) apply (simp add: algebra_simps) by (metis abs_ge_self le_less_trans le_of_int_ceiling less_le) then show ?case using less_eq_real_def by blast qed qed instantiation real :: floor_ceiling begin definition [code del]: "\x::real\ = (THE z. of_int z \ x \ x < of_int (z + 1))" instance proof show "of_int \x\ \ x \ x < of_int (\x\ + 1)" for x :: real unfolding floor_real_def using floor_exists1 by (rule theI') qed end subsection \Completeness\ lemma not_positive_Real: assumes "cauchy X" shows "\ positive (Real X) \ (\r>0. \k. \n\k. X n \ r)" (is "?lhs = ?rhs") unfolding positive_Real [OF assms] proof (intro iffI allI notI impI) show "\k. \n\k. X n \ r" if r: "\ (\r>0. \k. \n\k. r < X n)" and "0 < r" for r proof - obtain s t where "s > 0" "t > 0" "r = s+t" using \r > 0\ obtain_pos_sum by blast obtain k where k: "\m n. \m\k; n\k\ \ \X m - X n\ < t" using cauchyD [OF assms \t > 0\] by blast obtain n where "n \ k" "X n \ s" by (meson r \0 < s\ not_less) then have "X l \ r" if "l \ n" for l using k [OF \n \ k\, of l] that \r = s+t\ by linarith then show ?thesis by blast qed qed (meson le_cases not_le) lemma le_Real: assumes "cauchy X" "cauchy Y" shows "Real X \ Real Y = (\r>0. \k. \n\k. X n \ Y n + r)" unfolding not_less [symmetric, where 'a=real] less_real_def apply (simp add: diff_Real not_positive_Real assms) apply (simp add: diff_le_eq ac_simps) done lemma le_RealI: assumes Y: "cauchy Y" shows "\n. x \ of_rat (Y n) \ x \ Real Y" proof (induct x) fix X assume X: "cauchy X" and "\n. Real X \ of_rat (Y n)" then have le: "\m r. 0 < r \ \k. \n\k. X n \ Y m + r" by (simp add: of_rat_Real le_Real) then have "\k. \n\k. X n \ Y n + r" if "0 < r" for r :: rat proof - from that obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \Y m - Y n\ < s" using cauchyD [OF Y s] .. obtain j where j: "\n\j. X n \ Y i + t" using le [OF t] .. have "\n\max i j. X n \ Y n + r" proof clarsimp fix n assume n: "i \ n" "j \ n" have "X n \ Y i + t" using n j by simp moreover have "\Y i - Y n\ < s" using n i by simp ultimately show "X n \ Y n + r" unfolding r by simp qed then show ?thesis .. qed then show "Real X \ Real Y" by (simp add: of_rat_Real le_Real X Y) qed lemma Real_leI: assumes X: "cauchy X" assumes le: "\n. of_rat (X n) \ y" shows "Real X \ y" proof - have "- y \ - Real X" by (simp add: minus_Real X le_RealI of_rat_minus le) then show ?thesis by simp qed lemma less_RealD: assumes "cauchy Y" shows "x < Real Y \ \n. x < of_rat (Y n)" apply (erule contrapos_pp) apply (simp add: not_less) apply (erule Real_leI [OF assms]) done lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n" apply (induct n) apply simp apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc) done lemma complete_real: fixes S :: "real set" assumes "\x. x \ S" and "\z. \x\S. x \ z" shows "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)" proof - obtain x where x: "x \ S" using assms(1) .. obtain z where z: "\x\S. x \ z" using assms(2) .. define P where "P x \ (\y\S. y \ of_rat x)" for x obtain a where a: "\ P a" proof have "of_int \x - 1\ \ x - 1" by (rule of_int_floor_le) also have "x - 1 < x" by simp finally have "of_int \x - 1\ < x" . then have "\ x \ of_int \x - 1\" by (simp only: not_le) then show "\ P (of_int \x - 1\)" unfolding P_def of_rat_of_int_eq using x by blast qed obtain b where b: "P b" proof show "P (of_int \z\)" unfolding P_def of_rat_of_int_eq proof fix y assume "y \ S" then have "y \ z" using z by simp also have "z \ of_int \z\" by (rule le_of_int_ceiling) finally show "y \ of_int \z\" . qed qed define avg where "avg x y = x/2 + y/2" for x y :: rat define bisect where "bisect = (\(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y))" define A where "A n = fst ((bisect ^^ n) (a, b))" for n define B where "B n = snd ((bisect ^^ n) (a, b))" for n define C where "C n = avg (A n) (B n)" for n have A_0 [simp]: "A 0 = a" unfolding A_def by simp have B_0 [simp]: "B 0 = b" unfolding B_def by simp have A_Suc [simp]: "\n. A (Suc n) = (if P (C n) then A n else C n)" unfolding A_def B_def C_def bisect_def split_def by simp have B_Suc [simp]: "\n. B (Suc n) = (if P (C n) then C n else B n)" unfolding A_def B_def C_def bisect_def split_def by simp have width: "B n - A n = (b - a) / 2^n" for n proof (induct n) case (Suc n) then show ?case by (simp add: C_def eq_divide_eq avg_def algebra_simps) qed simp have twos: "\n. y / 2 ^ n < r" if "0 < r" for y r :: rat proof - obtain n where "y / r < rat_of_nat n" using \0 < r\ reals_Archimedean2 by blast then have "\n. y < r * 2 ^ n" by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that) then show ?thesis by (simp add: field_split_simps) qed have PA: "\ P (A n)" for n by (induct n) (simp_all add: a) have PB: "P (B n)" for n by (induct n) (simp_all add: b) have ab: "a < b" using a b unfolding P_def by (meson leI less_le_trans of_rat_less) have AB: "A n < B n" for n by (induct n) (simp_all add: ab C_def avg_def) have "A i \ A j \ B j \ B i" if "i < j" for i j using that proof (induction rule: less_Suc_induct) case (1 i) then show ?case apply (clarsimp simp add: C_def avg_def add_divide_distrib [symmetric]) apply (rule AB [THEN less_imp_le]) done qed simp then have A_mono: "A i \ A j" and B_mono: "B j \ B i" if "i \ j" for i j by (metis eq_refl le_neq_implies_less that)+ have cauchy_lemma: "cauchy X" if *: "\n i. i\n \ A n \ X i \ X i \ B n" for X proof (rule cauchyI) fix r::rat assume "0 < r" then obtain k where k: "(b - a) / 2 ^ k < r" using twos by blast have "\X m - X n\ < r" if "m\k" "n\k" for m n proof - have "\X m - X n\ \ B k - A k" by (simp add: * abs_rat_def diff_mono that) also have "... < r" by (simp add: k width) finally show ?thesis . qed then show "\k. \m\k. \n\k. \X m - X n\ < r" by blast qed have "cauchy A" by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order less_le_trans) have "cauchy B" by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order le_less_trans) have "\x\S. x \ Real B" proof fix x assume "x \ S" then show "x \ Real B" using PB [unfolded P_def] \cauchy B\ by (simp add: le_RealI) qed moreover have "\z. (\x\S. x \ z) \ Real A \ z" by (meson PA Real_leI P_def \cauchy A\ le_cases order.trans) moreover have "vanishes (\n. (b - a) / 2 ^ n)" proof (rule vanishesI) fix r :: rat assume "0 < r" then obtain k where k: "\b - a\ / 2 ^ k < r" using twos by blast have "\n\k. \(b - a) / 2 ^ n\ < r" proof clarify fix n assume n: "k \ n" have "\(b - a) / 2 ^ n\ = \b - a\ / 2 ^ n" by simp also have "\ \ \b - a\ / 2 ^ k" using n by (simp add: divide_left_mono) also note k finally show "\(b - a) / 2 ^ n\ < r" . qed then show "\k. \n\k. \(b - a) / 2 ^ n\ < r" .. qed then have "Real B = Real A" by (simp add: eq_Real \cauchy A\ \cauchy B\ width) ultimately show "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)" by force qed instantiation real :: linear_continuum begin subsection \Supremum of a set of reals\ definition "Sup X = (LEAST z::real. \x\X. x \ z)" definition "Inf X = - Sup (uminus ` X)" for X :: "real set" instance proof show Sup_upper: "x \ Sup X" if "x \ X" "bdd_above X" for x :: real and X :: "real set" proof - from that obtain s where s: "\y\X. y \ s" "\z. \y\X. y \ z \ s \ z" using complete_real[of X] unfolding bdd_above_def by blast then show ?thesis unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that) qed show Sup_least: "Sup X \ z" if "X \ {}" and z: "\x. x \ X \ x \ z" for z :: real and X :: "real set" proof - from that obtain s where s: "\y\X. y \ s" "\z. \y\X. y \ z \ s \ z" using complete_real [of X] by blast then have "Sup X = s" unfolding Sup_real_def by (best intro: Least_equality) also from s z have "\ \ z" by blast finally show ?thesis . qed show "Inf X \ x" if "x \ X" "bdd_below X" for x :: real and X :: "real set" using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that) show "z \ Inf X" if "X \ {}" "\x. x \ X \ z \ x" for z :: real and X :: "real set" using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that) show "\a b::real. a \ b" using zero_neq_one by blast qed end subsection \Hiding implementation details\ hide_const (open) vanishes cauchy positive Real declare Real_induct [induct del] declare Abs_real_induct [induct del] declare Abs_real_cases [cases del] lifting_update real.lifting lifting_forget real.lifting subsection \Embedding numbers into the Reals\ abbreviation real_of_nat :: "nat \ real" where "real_of_nat \ of_nat" abbreviation real :: "nat \ real" where "real \ of_nat" abbreviation real_of_int :: "int \ real" where "real_of_int \ of_int" abbreviation real_of_rat :: "rat \ real" where "real_of_rat \ of_rat" declare [[coercion_enabled]] declare [[coercion "of_nat :: nat \ int"]] declare [[coercion "of_nat :: nat \ real"]] declare [[coercion "of_int :: int \ real"]] (* We do not add rat to the coerced types, this has often unpleasant side effects when writing inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *) declare [[coercion_map map]] declare [[coercion_map "\f g h x. g (h (f x))"]] declare [[coercion_map "\f g (x,y). (f x, g y)"]] declare of_int_eq_0_iff [algebra, presburger] declare of_int_eq_1_iff [algebra, presburger] declare of_int_eq_iff [algebra, presburger] declare of_int_less_0_iff [algebra, presburger] declare of_int_less_1_iff [algebra, presburger] declare of_int_less_iff [algebra, presburger] declare of_int_le_0_iff [algebra, presburger] declare of_int_le_1_iff [algebra, presburger] declare of_int_le_iff [algebra, presburger] declare of_int_0_less_iff [algebra, presburger] declare of_int_0_le_iff [algebra, presburger] declare of_int_1_less_iff [algebra, presburger] declare of_int_1_le_iff [algebra, presburger] lemma int_less_real_le: "n < m \ real_of_int n + 1 \ real_of_int m" proof - have "(0::real) \ 1" by (metis less_eq_real_def zero_less_one) then show ?thesis by (metis floor_of_int less_floor_iff) qed lemma int_le_real_less: "n \ m \ real_of_int n < real_of_int m + 1" by (meson int_less_real_le not_le) lemma real_of_int_div_aux: "(real_of_int x) / (real_of_int d) = real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)" proof - have "x = (x div d) * d + x mod d" by auto then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)" by (metis of_int_add of_int_mult) then have "real_of_int x / real_of_int d = \ / real_of_int d" by simp then show ?thesis by (auto simp add: add_divide_distrib algebra_simps) qed lemma real_of_int_div: "d dvd n \ real_of_int (n div d) = real_of_int n / real_of_int d" for d n :: int by (simp add: real_of_int_div_aux) lemma real_of_int_div2: "0 \ real_of_int n / real_of_int x - real_of_int (n div x)" proof (cases "x = 0") case False then show ?thesis by (metis diff_ge_0_iff_ge floor_divide_of_int_eq of_int_floor_le) qed simp lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x) \ 1" apply (simp add: algebra_simps) by (metis add.commute floor_correct floor_divide_of_int_eq less_eq_real_def of_int_1 of_int_add) lemma real_of_int_div4: "real_of_int (n div x) \ real_of_int n / real_of_int x" using real_of_int_div2 [of n x] by simp subsection \Embedding the Naturals into the Reals\ lemma real_of_card: "real (card A) = sum (\x. 1) A" by simp lemma nat_less_real_le: "n < m \ real n + 1 \ real m" by (metis discrete of_nat_1 of_nat_add of_nat_le_iff) lemma nat_le_real_less: "n \ m \ real n < real m + 1" for m n :: nat by (meson nat_less_real_le not_le) lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d" proof - have "x = (x div d) * d + x mod d" by auto then have "real x = real (x div d) * real d + real(x mod d)" by (metis of_nat_add of_nat_mult) then have "real x / real d = \ / real d" by simp then show ?thesis by (auto simp add: add_divide_distrib algebra_simps) qed lemma real_of_nat_div: "d dvd n \ real(n div d) = real n / real d" by (subst real_of_nat_div_aux) (auto simp add: dvd_eq_mod_eq_0 [symmetric]) lemma real_of_nat_div2: "0 \ real n / real x - real (n div x)" for n x :: nat apply (simp add: algebra_simps) by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq) lemma real_of_nat_div3: "real n / real x - real (n div x) \ 1" for n x :: nat proof (cases "x = 0") case False then show ?thesis by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int) qed auto lemma real_of_nat_div4: "real (n div x) \ real n / real x" for n x :: nat using real_of_nat_div2 [of n x] by simp subsection \The Archimedean Property of the Reals\ lemma real_arch_inverse: "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat] by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc) lemma reals_Archimedean3: "0 < x \ \y. \n. y < real n * x" by (auto intro: ex_less_of_nat_mult) lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\m::nat. m > 0 \ real m * x \ c" shows "x = 0" by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) subsection \Rationals\ lemma Rats_abs_iff[simp]: "\(x::real)\ \ \ \ x \ \" by(simp add: abs_real_def split: if_splits) lemma Rats_eq_int_div_int: "\ = {real_of_int i / real_of_int j | i j. j \ 0}" (is "_ = ?S") proof show "\ \ ?S" proof fix x :: real assume "x \ \" then obtain r where "x = of_rat r" unfolding Rats_def .. have "of_rat r \ ?S" by (cases r) (auto simp add: of_rat_rat) then show "x \ ?S" using \x = of_rat r\ by simp qed next show "?S \ \" proof (auto simp: Rats_def) fix i j :: int assume "j \ 0" then have "real_of_int i / real_of_int j = of_rat (Fract i j)" by (simp add: of_rat_rat) then show "real_of_int i / real_of_int j \ range of_rat" by blast qed qed lemma Rats_eq_int_div_nat: "\ = { real_of_int i / real n | i n. n \ 0}" proof (auto simp: Rats_eq_int_div_int) fix i j :: int assume "j \ 0" show "\(i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i' / real n \ 0 < n" proof (cases "j > 0") case True then have "real_of_int i / real_of_int j = real_of_int i / real (nat j) \ 0 < nat j" by simp then show ?thesis by blast next case False with \j \ 0\ have "real_of_int i / real_of_int j = real_of_int (- i) / real (nat (- j)) \ 0 < nat (- j)" by simp then show ?thesis by blast qed next fix i :: int and n :: nat assume "0 < n" then have "real_of_int i / real n = real_of_int i / real_of_int(int n) \ int n \ 0" by simp then show "\i' j. real_of_int i / real n = real_of_int i' / real_of_int j \ j \ 0" by blast qed lemma Rats_abs_nat_div_natE: assumes "x \ \" obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "coprime m n" proof - from \x \ \\ obtain i :: int and n :: nat where "n \ 0" and "x = real_of_int i / real n" by (auto simp add: Rats_eq_int_div_nat) then have "\x\ = real (nat \i\) / real n" by simp then obtain m :: nat where x_rat: "\x\ = real m / real n" by blast let ?gcd = "gcd m n" from \n \ 0\ have gcd: "?gcd \ 0" by simp 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 \ 0\ and gcd_l have "?gcd * ?l \ 0" by simp then have "?l \ 0" by (blast dest!: mult_not_zero) moreover have "\x\ = real ?k / real ?l" proof - from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" by (simp add: real_of_nat_div) 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_distrib_nat) with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp with gcd show ?thesis by auto qed then have "coprime ?k ?l" by (simp only: coprime_iff_gcd_eq_1) ultimately show ?thesis .. qed subsection \Density of the Rational Reals in the Reals\ text \ This density proof is due to Stefan Richter and was ported by TN. The original source is \<^emph>\Real Analysis\ by H.L. Royden. It employs the Archimedean property of the reals.\ lemma Rats_dense_in_real: fixes x :: real assumes "x < y" shows "\r\\. x < r \ r < y" proof - from \x < y\ have "0 < y - x" by simp with reals_Archimedean obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q" by blast define p where "p = \y * real q\ - 1" define r where "r = of_int p / real q" from q have "x < y - inverse (real q)" by simp also from \0 < q\ have "y - inverse (real q) \ r" by (simp add: r_def p_def le_divide_eq left_diff_distrib) finally have "x < r" . moreover from \0 < q\ have "r < y" by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric]) moreover have "r \ \" by (simp add: r_def) ultimately show ?thesis by blast qed lemma of_rat_dense: fixes x y :: real assumes "x < y" shows "\q :: rat. x < of_rat q \ of_rat q < y" using Rats_dense_in_real [OF \x < y\] by (auto elim: Rats_cases) subsection \Numerals and Arithmetic\ declaration \ K (Lin_Arith.add_inj_const (\<^const_name>\of_nat\, \<^typ>\nat \ real\) #> Lin_Arith.add_inj_const (\<^const_name>\of_int\, \<^typ>\int \ real\)) \ subsection \Simprules combining \x + y\ and \0\\ (* FIXME ARE THEY NEEDED? *) lemma real_add_minus_iff [simp]: "x + - a = 0 \ x = a" for x a :: real by arith lemma real_add_less_0_iff: "x + y < 0 \ y < - x" for x y :: real by auto lemma real_0_less_add_iff: "0 < x + y \ - x < y" for x y :: real by auto lemma real_add_le_0_iff: "x + y \ 0 \ y \ - x" for x y :: real by auto lemma real_0_le_add_iff: "0 \ x + y \ - x \ y" for x y :: real by auto subsection \Lemmas about powers\ lemma two_realpow_ge_one: "(1::real) \ 2 ^ n" by simp (* FIXME: declare this [simp] for all types, or not at all *) declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp] lemma real_minus_mult_self_le [simp]: "- (u * u) \ x * x" for u x :: real by (rule order_trans [where y = 0]) auto lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \ x\<^sup>2" for u x :: real by (auto simp add: power2_eq_square) subsection \Density of the Reals\ lemma field_lbound_gt_zero: "0 < d1 \ 0 < d2 \ \e. 0 < e \ e < d1 \ e < d2" for d1 d2 :: "'a::linordered_field" by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def) lemma field_less_half_sum: "x < y \ x < (x + y) / 2" for x y :: "'a::linordered_field" by auto lemma field_sum_of_halves: "x / 2 + x / 2 = x" for x :: "'a::linordered_field" by simp subsection \Archimedean properties and useful consequences\ text\Bernoulli's inequality\ proposition Bernoulli_inequality: fixes x :: real assumes "-1 \ x" shows "1 + n * x \ (1 + x) ^ n" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" by (simp add: algebra_simps) also have "... = (1 + x) * (1 + n*x)" by (auto simp: power2_eq_square algebra_simps) also have "... \ (1 + x) ^ Suc n" using Suc.hyps assms mult_left_mono by fastforce finally show ?case . qed corollary Bernoulli_inequality_even: fixes x :: real assumes "even n" shows "1 + n * x \ (1 + x) ^ n" proof (cases "-1 \ x \ n=0") case True then show ?thesis by (auto simp: Bernoulli_inequality) next case False then have "real n \ 1" by simp with False have "n * x \ -1" by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) then have "1 + n * x \ 0" by auto also have "... \ (1 + x) ^ n" using assms using zero_le_even_power by blast finally show ?thesis . qed corollary real_arch_pow: fixes x :: real assumes x: "1 < x" shows "\n. y < x^n" proof - from x have x0: "x - 1 > 0" by arith from reals_Archimedean3[OF x0, rule_format, of y] obtain n :: nat where n: "y < real n * (x - 1)" by metis from x0 have x00: "x- 1 \ -1" by arith from Bernoulli_inequality[OF x00, of n] n have "y < x^n" by auto then show ?thesis by metis qed corollary real_arch_pow_inv: fixes x y :: real assumes y: "y > 0" and x1: "x < 1" shows "\n. x^n < y" proof (cases "x > 0") case True with x1 have ix: "1 < 1/x" by (simp add: field_simps) from real_arch_pow[OF ix, of "1/y"] obtain n where n: "1/y < (1/x)^n" by blast then show ?thesis using y \x > 0\ by (auto simp add: field_simps) next case False with y x1 show ?thesis by (metis less_le_trans not_less power_one_right) qed lemma forall_pos_mono: "(\d e::real. d < e \ P d \ P e) \ (\n::nat. n \ 0 \ P (inverse (real n))) \ (\e. 0 < e \ P e)" by (metis real_arch_inverse) lemma forall_pos_mono_1: "(\d e::real. d < e \ P d \ P e) \ (\n. P (inverse (real (Suc n)))) \ 0 < e \ P e" apply (rule forall_pos_mono) apply auto apply (metis Suc_pred of_nat_Suc) done subsection \Floor and Ceiling Functions from the Reals to the Integers\ (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *) lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \ n < numeral w" for n :: nat by (metis of_nat_less_iff of_nat_numeral) lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \ numeral w < n" for n :: nat by (metis of_nat_less_iff of_nat_numeral) lemma numeral_le_real_of_nat_iff [simp]: "numeral n \ real m \ numeral n \ m" for m :: nat by (metis not_le real_of_nat_less_numeral_iff) lemma of_int_floor_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" by (metis floor_of_int) lemma floor_eq: "real_of_int n < x \ x < real_of_int n + 1 \ \x\ = n" by linarith lemma floor_eq2: "real_of_int n \ x \ x < real_of_int n + 1 \ \x\ = n" by (fact floor_unique) lemma floor_eq3: "real n < x \ x < real (Suc n) \ nat \x\ = n" by linarith lemma floor_eq4: "real n \ x \ x < real (Suc n) \ nat \x\ = n" by linarith lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \ real_of_int \r\" by linarith lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int \r\" by linarith lemma real_of_int_floor_add_one_ge [simp]: "r \ real_of_int \r\ + 1" by linarith lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \r\ + 1" by linarith lemma floor_divide_real_eq_div: assumes "0 \ b" shows "\a / real_of_int b\ = \a\ div b" proof (cases "b = 0") case True then show ?thesis by simp next case False with assms have b: "b > 0" by simp have "j = i div b" if "real_of_int i \ a" "a < 1 + real_of_int i" "real_of_int j * real_of_int b \ a" "a < real_of_int b + real_of_int j * real_of_int b" for i j :: int proof - from that have "i < b + j * b" by (metis le_less_trans of_int_add of_int_less_iff of_int_mult) moreover have "j * b < 1 + i" proof - have "real_of_int (j * b) < real_of_int i + 1" using \a < 1 + real_of_int i\ \real_of_int j * real_of_int b \ a\ by force then show "j * b < 1 + i" by linarith qed ultimately have "(j - i div b) * b \ i mod b" "i mod b < ((j - i div b) + 1) * b" by (auto simp: field_simps) then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b" using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i] by linarith+ then show ?thesis using b unfolding mult_less_cancel_right by auto qed with b show ?thesis by (auto split: floor_split simp: field_simps) qed lemma floor_one_divide_eq_div_numeral [simp]: "\1 / numeral b::real\ = 1 div numeral b" by (metis floor_divide_of_int_eq of_int_1 of_int_numeral) lemma floor_minus_one_divide_eq_div_numeral [simp]: "\- (1 / numeral b)::real\ = - 1 div numeral b" by (metis (mono_tags, opaque_lifting) div_minus_right minus_divide_right floor_divide_of_int_eq of_int_neg_numeral of_int_1) lemma floor_divide_eq_div_numeral [simp]: "\numeral a / numeral b::real\ = numeral a div numeral b" by (metis floor_divide_of_int_eq of_int_numeral) lemma floor_minus_divide_eq_div_numeral [simp]: "\- (numeral a / numeral b)::real\ = - numeral a div numeral b" by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral) lemma of_int_ceiling_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" using ceiling_of_int by metis lemma ceiling_eq: "of_int n < x \ x \ of_int n + 1 \ \x\ = n + 1" by (simp add: ceiling_unique) lemma of_int_ceiling_diff_one_le [simp]: "of_int \r\ - 1 \ r" by linarith lemma of_int_ceiling_le_add_one [simp]: "of_int \r\ \ r + 1" by linarith lemma ceiling_le: "x \ of_int a \ \x\ \ a" by (simp add: ceiling_le_iff) lemma ceiling_divide_eq_div: "\of_int a / of_int b\ = - (- a div b)" by (metis ceiling_def floor_divide_of_int_eq minus_divide_left of_int_minus) lemma ceiling_divide_eq_div_numeral [simp]: "\numeral a / numeral b :: real\ = - (- numeral a div numeral b)" using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp lemma ceiling_minus_divide_eq_div_numeral [simp]: "\- (numeral a / numeral b :: real)\ = - (numeral a div numeral b)" using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp text \ The following lemmas are remnants of the erstwhile functions natfloor and natceiling. \ lemma nat_floor_neg: "x \ 0 \ nat \x\ = 0" for x :: real by linarith lemma le_nat_floor: "real x \ a \ x \ nat \a\" by linarith lemma le_mult_nat_floor: "nat \a\ * nat \b\ \ nat \a * b\" by (cases "0 \ a \ 0 \ b") (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor) lemma nat_ceiling_le_eq [simp]: "nat \x\ \ a \ x \ real a" by linarith lemma real_nat_ceiling_ge: "x \ real (nat \x\)" by linarith lemma Rats_no_top_le: "\q \ \. x \ q" for x :: real by (auto intro!: bexI[of _ "of_nat (nat \x\)"]) linarith lemma Rats_no_bot_less: "\q \ \. q < x" for x :: real by (auto intro!: bexI[of _ "of_int (\x\ - 1)"]) linarith subsection \Exponentiation with floor\ lemma floor_power: assumes "x = of_int \x\" shows "\x ^ n\ = \x\ ^ n" proof - have "x ^ n = of_int (\x\ ^ n)" using assms by (induct n arbitrary: x) simp_all then show ?thesis by (metis floor_of_int) qed lemma floor_numeral_power [simp]: "\numeral x ^ n\ = numeral x ^ n" by (metis floor_of_int of_int_numeral of_int_power) lemma ceiling_numeral_power [simp]: "\numeral x ^ n\ = numeral x ^ n" by (metis ceiling_of_int of_int_numeral of_int_power) subsection \Implementation of rational real numbers\ text \Formal constructor\ definition Ratreal :: "rat \ real" where [code_abbrev, simp]: "Ratreal = real_of_rat" code_datatype Ratreal text \Quasi-Numerals\ lemma [code_abbrev]: "real_of_rat (numeral k) = numeral k" "real_of_rat (- numeral k) = - numeral k" "real_of_rat (rat_of_int a) = real_of_int a" by simp_all lemma [code_post]: "real_of_rat 0 = 0" "real_of_rat 1 = 1" "real_of_rat (- 1) = - 1" "real_of_rat (1 / numeral k) = 1 / numeral k" "real_of_rat (numeral k / numeral l) = numeral k / numeral l" "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)" "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)" by (simp_all add: of_rat_divide of_rat_minus) text \Operations\ lemma zero_real_code [code]: "0 = Ratreal 0" by simp lemma one_real_code [code]: "1 = Ratreal 1" by simp instantiation real :: equal begin definition "HOL.equal x y \ x - y = 0" for x :: real instance by standard (simp add: equal_real_def) lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \ HOL.equal x y" by (simp add: equal_real_def equal) lemma [code nbe]: "HOL.equal x x \ True" for x :: real by (rule equal_refl) end lemma real_less_eq_code [code]: "Ratreal x \ Ratreal y \ x \ y" by (simp add: of_rat_less_eq) lemma real_less_code [code]: "Ratreal x < Ratreal y \ x < y" by (simp add: of_rat_less) lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)" by (simp add: of_rat_add) lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)" by (simp add: of_rat_mult) lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)" by (simp add: of_rat_minus) lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)" by (simp add: of_rat_diff) lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)" by (simp add: of_rat_inverse) lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)" by (simp add: of_rat_divide) lemma real_floor_code [code]: "\Ratreal x\ = \x\" by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code) text \Quickcheck\ context includes term_syntax begin definition valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)" where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k" end instantiation real :: random begin context includes state_combinator_syntax begin definition "Quickcheck_Random.random i = Quickcheck_Random.random i \\ (\r. Pair (valterm_ratreal r))" instance .. end end instantiation real :: exhaustive begin definition "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (\r. f (Ratreal r)) d" instance .. end instantiation real :: full_exhaustive begin definition "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (\r. f (valterm_ratreal r)) d" instance .. end instantiation real :: narrowing begin definition "narrowing_real = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing" instance .. end subsection \Setup for Nitpick\ declaration \ Nitpick_HOL.register_frac_type \<^type_name>\real\ [(\<^const_name>\zero_real_inst.zero_real\, \<^const_name>\Nitpick.zero_frac\), (\<^const_name>\one_real_inst.one_real\, \<^const_name>\Nitpick.one_frac\), (\<^const_name>\plus_real_inst.plus_real\, \<^const_name>\Nitpick.plus_frac\), (\<^const_name>\times_real_inst.times_real\, \<^const_name>\Nitpick.times_frac\), (\<^const_name>\uminus_real_inst.uminus_real\, \<^const_name>\Nitpick.uminus_frac\), (\<^const_name>\inverse_real_inst.inverse_real\, \<^const_name>\Nitpick.inverse_frac\), (\<^const_name>\ord_real_inst.less_real\, \<^const_name>\Nitpick.less_frac\), (\<^const_name>\ord_real_inst.less_eq_real\, \<^const_name>\Nitpick.less_eq_frac\)] \ lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real times_real_inst.times_real uminus_real_inst.uminus_real zero_real_inst.zero_real subsection \Setup for SMT\ ML_file \Tools/SMT/smt_real.ML\ ML_file \Tools/SMT/z3_real.ML\ lemma [z3_rule]: "0 + x = x" "x + 0 = x" "0 * x = 0" "1 * x = x" "-x = -1 * x" "x + y = y + x" for x y :: real by auto lemma [smt_arith_multiplication]: fixes A B :: real and p n :: real assumes "A \ B" "0 < n" "p > 0" shows "(A / n) * p \ (B / n) * p" using assms by (auto simp: field_simps) lemma [smt_arith_multiplication]: fixes A B :: real and p n :: real assumes "A < B" "0 < n" "p > 0" shows "(A / n) * p < (B / n) * p" using assms by (auto simp: field_simps) lemma [smt_arith_multiplication]: fixes A B :: real and p n :: int assumes "A \ B" "0 < n" "p > 0" shows "(A / n) * p \ (B / n) * p" using assms by (auto simp: field_simps) lemma [smt_arith_multiplication]: fixes A B :: real and p n :: int assumes "A < B" "0 < n" "p > 0" shows "(A / n) * p < (B / n) * p" using assms by (auto simp: field_simps) lemmas [smt_arith_multiplication] = verit_le_mono_div[THEN mult_left_mono, unfolded int_distrib, of _ _ \nat (floor (_ :: real))\ \nat (floor (_ :: real))\] div_le_mono[THEN mult_left_mono, unfolded int_distrib, of _ _ \nat (floor (_ :: real))\ \nat (floor (_ :: real))\] verit_le_mono_div_int[THEN mult_left_mono, unfolded int_distrib, of _ _ \floor (_ :: real)\ \floor (_ :: real)\] zdiv_mono1[THEN mult_left_mono, unfolded int_distrib, of _ _ \floor (_ :: real)\ \floor (_ :: real)\] arg_cong[of _ _ \\a :: real. a / real (n::nat) * real (p::nat)\ for n p :: nat, THEN sym] arg_cong[of _ _ \\a :: real. a / real_of_int n * real_of_int p\ for n p :: int, THEN sym] arg_cong[of _ _ \\a :: real. a / n * p\ for n p :: real, THEN sym] lemmas [smt_arith_simplify] = floor_one floor_numeral div_by_1 times_divide_eq_right nonzero_mult_div_cancel_left division_ring_divide_zero div_0 divide_minus_left zero_less_divide_iff subsection \Setup for Argo\ ML_file \Tools/Argo/argo_real.ML\ end diff --git a/src/HOL/ex/Dedekind_Real.thy b/src/HOL/ex/Dedekind_Real.thy deleted file mode 100644 --- a/src/HOL/ex/Dedekind_Real.thy +++ /dev/null @@ -1,1663 +0,0 @@ -section \The Reals as Dedekind Sections of Positive Rationals\ - -text \Fundamentals of Abstract Analysis [Gleason- p. 121] provides some of the definitions.\ - -(* Title: HOL/ex/Dedekind_Real.thy - Author: Jacques D. Fleuriot, University of Cambridge - Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4; 2019 -*) - -theory Dedekind_Real -imports Complex_Main -begin - -text\Could be moved to \Groups\\ -lemma add_eq_exists: "\x. a+x = (b::'a::ab_group_add)" - by (rule_tac x="b-a" in exI, simp) - -subsection \Dedekind cuts or sections\ - -definition - cut :: "rat set \ bool" where - "cut A \ {} \ A \ A \ {0<..} \ - (\y \ A. ((\z. 0 z < y \ z \ A) \ (\u \ A. y < u)))" - -lemma cut_of_rat: - assumes q: "0 < q" shows "cut {r::rat. 0 < r \ r < q}" (is "cut ?A") -proof - - from q have pos: "?A \ {0<..}" by force - have nonempty: "{} \ ?A" - proof - show "{} \ ?A" by simp - show "{} \ ?A" - using field_lbound_gt_zero q by auto - qed - show ?thesis - by (simp add: cut_def pos nonempty, - blast dest: dense intro: order_less_trans) -qed - - -typedef preal = "Collect cut" - by (blast intro: cut_of_rat [OF zero_less_one]) - -lemma Abs_preal_induct [induct type: preal]: - "(\x. cut x \ P (Abs_preal x)) \ P x" - using Abs_preal_induct [of P x] by simp - -lemma cut_Rep_preal [simp]: "cut (Rep_preal x)" - using Rep_preal [of x] by simp - -definition - psup :: "preal set \ preal" where - "psup P = Abs_preal (\X \ P. Rep_preal X)" - -definition - add_set :: "[rat set,rat set] \ rat set" where - "add_set A B = {w. \x \ A. \y \ B. w = x + y}" - -definition - diff_set :: "[rat set,rat set] \ rat set" where - "diff_set A B = {w. \x. 0 < w \ 0 < x \ x \ B \ x + w \ A}" - -definition - mult_set :: "[rat set,rat set] \ rat set" where - "mult_set A B = {w. \x \ A. \y \ B. w = x * y}" - -definition - inverse_set :: "rat set \ rat set" where - "inverse_set A \ {x. \y. 0 < x \ x < y \ inverse y \ A}" - -instantiation preal :: "{ord, plus, minus, times, inverse, one}" -begin - -definition - preal_less_def: - "r < s \ Rep_preal r < Rep_preal s" - -definition - preal_le_def: - "r \ s \ Rep_preal r \ Rep_preal s" - -definition - preal_add_def: - "r + s \ Abs_preal (add_set (Rep_preal r) (Rep_preal s))" - -definition - preal_diff_def: - "r - s \ Abs_preal (diff_set (Rep_preal r) (Rep_preal s))" - -definition - preal_mult_def: - "r * s \ Abs_preal (mult_set (Rep_preal r) (Rep_preal s))" - -definition - preal_inverse_def: - "inverse r \ Abs_preal (inverse_set (Rep_preal r))" - -definition "r div s = r * inverse (s::preal)" - -definition - preal_one_def: - "1 \ Abs_preal {x. 0 < x \ x < 1}" - -instance .. - -end - - -text\Reduces equality on abstractions to equality on representatives\ -declare Abs_preal_inject [simp] -declare Abs_preal_inverse [simp] - -lemma rat_mem_preal: "0 < q \ cut {r::rat. 0 < r \ r < q}" -by (simp add: cut_of_rat) - -lemma preal_nonempty: "cut A \ \x\A. 0 < x" - unfolding cut_def [abs_def] by blast - -lemma preal_Ex_mem: "cut A \ \x. x \ A" - using preal_nonempty by blast - -lemma preal_exists_bound: "cut A \ \x. 0 < x \ x \ A" - using Dedekind_Real.cut_def by fastforce - -lemma preal_exists_greater: "\cut A; y \ A\ \ \u \ A. y < u" - unfolding cut_def [abs_def] by blast - -lemma preal_downwards_closed: "\cut A; y \ A; 0 < z; z < y\ \ z \ A" - unfolding cut_def [abs_def] by blast - -text\Relaxing the final premise\ -lemma preal_downwards_closed': "\cut A; y \ A; 0 < z; z \ y\ \ z \ A" - using less_eq_rat_def preal_downwards_closed by blast - -text\A positive fraction not in a positive real is an upper bound. - Gleason p. 122 - Remark (1)\ - -lemma not_in_preal_ub: - assumes A: "cut A" - and notx: "x \ A" - and y: "y \ A" - and pos: "0 < x" - shows "y < x" -proof (cases rule: linorder_cases) - assume "xpreal lemmas instantiated to \<^term>\Rep_preal X\\ - -lemma mem_Rep_preal_Ex: "\x. x \ Rep_preal X" -thm preal_Ex_mem -by (rule preal_Ex_mem [OF cut_Rep_preal]) - -lemma Rep_preal_exists_bound: "\x>0. x \ Rep_preal X" -by (rule preal_exists_bound [OF cut_Rep_preal]) - -lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF cut_Rep_preal] - - -subsection\Properties of Ordering\ - -instance preal :: order -proof - fix w :: preal - show "w \ w" by (simp add: preal_le_def) -next - fix i j k :: preal - assume "i \ j" and "j \ k" - then show "i \ k" by (simp add: preal_le_def) -next - fix z w :: preal - assume "z \ w" and "w \ z" - then show "z = w" by (simp add: preal_le_def Rep_preal_inject) -next - fix z w :: preal - show "z < w \ z \ w \ \ w \ z" - by (auto simp: preal_le_def preal_less_def Rep_preal_inject) -qed - -lemma preal_imp_pos: "\cut A; r \ A\ \ 0 < r" - by (auto simp: cut_def) - -instance preal :: linorder -proof - fix x y :: preal - show "x \ y \ y \ x" - unfolding preal_le_def - by (meson cut_Rep_preal not_in_preal_ub preal_downwards_closed preal_imp_pos subsetI) -qed - -instantiation preal :: distrib_lattice -begin - -definition - "(inf :: preal \ preal \ preal) = min" - -definition - "(sup :: preal \ preal \ preal) = max" - -instance - by intro_classes - (auto simp: inf_preal_def sup_preal_def max_min_distrib2) - -end - -subsection\Properties of Addition\ - -lemma preal_add_commute: "(x::preal) + y = y + x" - unfolding preal_add_def add_set_def - by (metis (no_types, opaque_lifting) add.commute) - -text\Lemmas for proving that addition of two positive reals gives - a positive real\ - -lemma mem_add_set: - assumes "cut A" "cut B" - shows "cut (add_set A B)" -proof - - have "{} \ add_set A B" - using assms by (force simp: add_set_def dest: preal_nonempty) - moreover - obtain q where "q > 0" "q \ add_set A B" - proof - - obtain a b where "a > 0" "a \ A" "b > 0" "b \ B" "\x. x \ A \ x < a" "\y. y \ B \ y < b" - by (meson assms preal_exists_bound not_in_preal_ub) - with assms have "a+b \ add_set A B" - by (fastforce simp add: add_set_def) - then show thesis - using \0 < a\ \0 < b\ add_pos_pos that by blast - qed - then have "add_set A B \ {0<..}" - unfolding add_set_def - using preal_imp_pos [OF \cut A\] preal_imp_pos [OF \cut B\] by fastforce - moreover have "z \ add_set A B" - if u: "u \ add_set A B" and "0 < z" "z < u" for u z - using u unfolding add_set_def - proof (clarify) - fix x::rat and y::rat - assume ueq: "u = x + y" and x: "x \ A" and y:"y \ B" - have xpos [simp]: "x > 0" and ypos [simp]: "y > 0" - using assms preal_imp_pos x y by blast+ - have xypos [simp]: "x+y > 0" by (simp add: pos_add_strict) - let ?f = "z/(x+y)" - have fless: "?f < 1" - using divide_less_eq_1_pos \z < u\ ueq xypos by blast - show "\x' \ A. \y'\B. z = x' + y'" - proof (intro bexI) - show "z = x*?f + y*?f" - by (simp add: distrib_right [symmetric] divide_inverse ac_simps order_less_imp_not_eq2) - next - show "y * ?f \ B" - proof (rule preal_downwards_closed [OF \cut B\ y]) - show "0 < y * ?f" - by (simp add: \0 < z\) - next - show "y * ?f < y" - by (insert mult_strict_left_mono [OF fless ypos], simp) - qed - next - show "x * ?f \ A" - proof (rule preal_downwards_closed [OF \cut A\ x]) - show "0 < x * ?f" - by (simp add: \0 < z\) - next - show "x * ?f < x" - by (insert mult_strict_left_mono [OF fless xpos], simp) - qed - qed - qed - moreover - have "\y. y \ add_set A B \ \u \ add_set A B. y < u" - unfolding add_set_def using preal_exists_greater assms by fastforce - ultimately show ?thesis - by (simp add: Dedekind_Real.cut_def) -qed - -lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)" - apply (simp add: preal_add_def mem_add_set) - apply (force simp: add_set_def ac_simps) - done - -instance preal :: ab_semigroup_add -proof - fix a b c :: preal - show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc) - show "a + b = b + a" by (rule preal_add_commute) -qed - - -subsection\Properties of Multiplication\ - -text\Proofs essentially same as for addition\ - -lemma preal_mult_commute: "(x::preal) * y = y * x" - unfolding preal_mult_def mult_set_def - by (metis (no_types, opaque_lifting) mult.commute) - -text\Multiplication of two positive reals gives a positive real.\ - -lemma mem_mult_set: - assumes "cut A" "cut B" - shows "cut (mult_set A B)" -proof - - have "{} \ mult_set A B" - using assms - by (force simp: mult_set_def dest: preal_nonempty) - moreover - obtain q where "q > 0" "q \ mult_set A B" - proof - - obtain x y where x [simp]: "0 < x" "x \ A" and y [simp]: "0 < y" "y \ B" - using preal_exists_bound assms by blast - show thesis - proof - show "0 < x*y" by simp - show "x * y \ mult_set A B" - proof - - { - fix u::rat and v::rat - assume u: "u \ A" and v: "v \ B" and xy: "x*y = u*v" - moreover have "uv" - using less_imp_le preal_imp_pos assms x y u v by blast - moreover have "u*v < x*y" - using assms x \u < x\ \v < y\ \0 \ v\ by (blast intro: mult_strict_mono) - ultimately have False by force - } - thus ?thesis by (auto simp: mult_set_def) - qed - qed - qed - then have "mult_set A B \ {0<..}" - unfolding mult_set_def - using preal_imp_pos [OF \cut A\] preal_imp_pos [OF \cut B\] by fastforce - moreover have "z \ mult_set A B" - if u: "u \ mult_set A B" and "0 < z" "z < u" for u z - using u unfolding mult_set_def - proof (clarify) - fix x::rat and y::rat - assume ueq: "u = x * y" and x: "x \ A" and y: "y \ B" - have [simp]: "y > 0" - using \cut B\ preal_imp_pos y by blast - show "\x' \ A. \y' \ B. z = x' * y'" - proof - have "z = (z/y)*y" - by (simp add: divide_inverse mult.commute [of y] mult.assoc order_less_imp_not_eq2) - then show "\y'\B. z = (z/y) * y'" - using y by blast - next - show "z/y \ A" - proof (rule preal_downwards_closed [OF \cut A\ x]) - show "0 < z/y" - by (simp add: \0 < z\) - show "z/y < x" - using \0 < y\ pos_divide_less_eq \z < u\ ueq by blast - qed - qed - qed - moreover have "\y. y \ mult_set A B \ \u \ mult_set A B. y < u" - apply (simp add: mult_set_def) - by (metis preal_exists_greater mult_strict_right_mono preal_imp_pos assms) - ultimately show ?thesis - by (simp add: Dedekind_Real.cut_def) -qed - -lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)" - apply (simp add: preal_mult_def mem_mult_set Rep_preal) - apply (simp add: mult_set_def) - apply (metis (no_types, opaque_lifting) ab_semigroup_mult_class.mult_ac(1)) - done - -instance preal :: ab_semigroup_mult -proof - fix a b c :: preal - show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc) - show "a * b = b * a" by (rule preal_mult_commute) -qed - - -text\Positive real 1 is the multiplicative identity element\ - -lemma preal_mult_1: "(1::preal) * z = z" -proof (induct z) - fix A :: "rat set" - assume A: "cut A" - have "{w. \u. 0 < u \ u < 1 \ (\v \ A. w = u * v)} = A" (is "?lhs = A") - proof - show "?lhs \ A" - proof clarify - fix x::rat and u::rat and v::rat - assume upos: "0 A" - have vpos: "0u < 1\ v) - thus "u * v \ A" - by (force intro: preal_downwards_closed [OF A v] mult_pos_pos upos vpos) - qed - next - show "A \ ?lhs" - proof clarify - fix x::rat - assume x: "x \ A" - have xpos: "0 A" and xlessv: "x < v" .. - have vpos: "0u. 0 < u \ u < 1 \ (\v\A. x = u * v)" - proof (intro exI conjI) - show "0 < x/v" - by (simp add: zero_less_divide_iff xpos vpos) - show "x / v < 1" - by (simp add: pos_divide_less_eq vpos xlessv) - have "x = (x/v)*v" - by (simp add: divide_inverse mult.assoc vpos order_less_imp_not_eq2) - then show "\v'\A. x = (x / v) * v'" - using v by blast - qed - qed - qed - thus "1 * Abs_preal A = Abs_preal A" - by (simp add: preal_one_def preal_mult_def mult_set_def rat_mem_preal A) -qed - -instance preal :: comm_monoid_mult - by intro_classes (rule preal_mult_1) - - -subsection\Distribution of Multiplication across Addition\ - -lemma mem_Rep_preal_add_iff: - "(z \ Rep_preal(r+s)) = (\x \ Rep_preal r. \y \ Rep_preal s. z = x + y)" - apply (simp add: preal_add_def mem_add_set Rep_preal) - apply (simp add: add_set_def) - done - -lemma mem_Rep_preal_mult_iff: - "(z \ Rep_preal(r*s)) = (\x \ Rep_preal r. \y \ Rep_preal s. z = x * y)" - apply (simp add: preal_mult_def mem_mult_set Rep_preal) - apply (simp add: mult_set_def) - done - -lemma distrib_subset1: - "Rep_preal (w * (x + y)) \ Rep_preal (w * x + w * y)" - by (force simp: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff distrib_left) - -lemma preal_add_mult_distrib_mean: - assumes a: "a \ Rep_preal w" - and b: "b \ Rep_preal w" - and d: "d \ Rep_preal x" - and e: "e \ Rep_preal y" - shows "\c \ Rep_preal w. a * d + b * e = c * (d + e)" -proof - let ?c = "(a*d + b*e)/(d+e)" - have [simp]: "0 Rep_preal w" - proof (cases rule: linorder_le_cases) - assume "a \ b" - hence "?c \ b" - by (simp add: pos_divide_le_eq distrib_left mult_right_mono - order_less_imp_le) - thus ?thesis by (rule preal_downwards_closed' [OF cut_Rep_preal b cpos]) - next - assume "b \ a" - hence "?c \ a" - by (simp add: pos_divide_le_eq distrib_left mult_right_mono - order_less_imp_le) - thus ?thesis by (rule preal_downwards_closed' [OF cut_Rep_preal a cpos]) - qed -qed - -lemma distrib_subset2: - "Rep_preal (w * x + w * y) \ Rep_preal (w * (x + y))" - apply (clarsimp simp: mem_Rep_preal_add_iff mem_Rep_preal_mult_iff) - using mem_Rep_preal_add_iff preal_add_mult_distrib_mean by blast - -lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)" - by (metis Rep_preal_inverse distrib_subset1 distrib_subset2 subset_antisym) - -lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)" - by (simp add: preal_mult_commute preal_add_mult_distrib2) - -instance preal :: comm_semiring - by intro_classes (rule preal_add_mult_distrib) - - -subsection\Existence of Inverse, a Positive Real\ - -lemma mem_inverse_set: - assumes "cut A" shows "cut (inverse_set A)" -proof - - have "\x y. 0 < x \ x < y \ inverse y \ A" - proof - - from preal_exists_bound [OF \cut A\] - obtain x where [simp]: "0 A" by blast - show ?thesis - proof (intro exI conjI) - show "0 < inverse (x+1)" - by (simp add: order_less_trans [OF _ less_add_one]) - show "inverse(x+1) < inverse x" - by (simp add: less_imp_inverse_less less_add_one) - show "inverse (inverse x) \ A" - by (simp add: order_less_imp_not_eq2) - qed - qed - then have "{} \ inverse_set A" - using inverse_set_def by fastforce - moreover obtain q where "q > 0" "q \ inverse_set A" - proof - - from preal_nonempty [OF \cut A\] - obtain x where x: "x \ A" and xpos [simp]: "0 inverse_set A" - proof - - { fix y::rat - assume ygt: "inverse x < y" - have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt]) - have iyless: "inverse y < x" - by (simp add: inverse_less_imp_less [of x] ygt) - have "inverse y \ A" - by (simp add: preal_downwards_closed [OF \cut A\ x] iyless)} - thus ?thesis by (auto simp: inverse_set_def) - qed - qed - qed - moreover have "inverse_set A \ {0<..}" - using calculation inverse_set_def by blast - moreover have "z \ inverse_set A" - if u: "u \ inverse_set A" and "0 < z" "z < u" for u z - using u that less_trans unfolding inverse_set_def by auto - moreover have "\y. y \ inverse_set A \ \u \ inverse_set A. y < u" - by (simp add: inverse_set_def) (meson dense less_trans) - ultimately show ?thesis - by (simp add: Dedekind_Real.cut_def) -qed - - -subsection\Gleason's Lemma 9-3.4, page 122\ - -lemma Gleason9_34_exists: - assumes A: "cut A" - and "\x\A. x + u \ A" - and "0 \ z" - shows "\b\A. b + (of_int z) * u \ A" -proof (cases z rule: int_cases) - case (nonneg n) - show ?thesis - proof (simp add: nonneg, induct n) - case 0 - from preal_nonempty [OF A] - show ?case by force - next - case (Suc k) - then obtain b where b: "b \ A" "b + of_nat k * u \ A" .. - hence "b + of_int (int k)*u + u \ A" by (simp add: assms) - thus ?case by (force simp: algebra_simps b) - qed -next - case (neg n) - with assms show ?thesis by simp -qed - -lemma Gleason9_34_contra: - assumes A: "cut A" - shows "\\x\A. x + u \ A; 0 < u; 0 < y; y \ A\ \ False" -proof (induct u, induct y) - fix a::int and b::int - fix c::int and d::int - assume bpos [simp]: "0 < b" - and dpos [simp]: "0 < d" - and closed: "\x\A. x + (Fract c d) \ A" - and upos: "0 < Fract c d" - and ypos: "0 < Fract a b" - and notin: "Fract a b \ A" - have cpos [simp]: "0 < c" - by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) - have apos [simp]: "0 < a" - by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) - let ?k = "a*d" - have frle: "Fract a b \ Fract ?k 1 * (Fract c d)" - proof - - have "?thesis = ((a * d * b * d) \ c * b * (a * d * b * d))" - by (simp add: order_less_imp_not_eq2 ac_simps) - moreover - have "(1 * (a * d * b * d)) \ c * b * (a * d * b * d)" - by (rule mult_mono, - simp_all add: int_one_le_iff_zero_less zero_less_mult_iff - order_less_imp_le) - ultimately - show ?thesis by simp - qed - have k: "0 \ ?k" by (simp add: order_less_imp_le zero_less_mult_iff) - from Gleason9_34_exists [OF A closed k] - obtain z where z: "z \ A" - and mem: "z + of_int ?k * Fract c d \ A" .. - have less: "z + of_int ?k * Fract c d < Fract a b" - by (rule not_in_preal_ub [OF A notin mem ypos]) - have "0r \ A. r + u \ A" - using assms Gleason9_34_contra preal_exists_bound by blast - - - -subsection\Gleason's Lemma 9-3.6\ - -lemma lemma_gleason9_36: - assumes A: "cut A" - and x: "1 < x" - shows "\r \ A. r*x \ A" -proof - - from preal_nonempty [OF A] - obtain y where y: "y \ A" and ypos: "0r\A. r * x \ A)" - with y have ymem: "y * x \ A" by blast - from ypos mult_strict_left_mono [OF x] - have yless: "y < y*x" by simp - let ?d = "y*x - y" - from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto - from Gleason9_34 [OF A dpos] - obtain r where r: "r\A" and notin: "r + ?d \ A" .. - have rpos: "0 y + ?d)" - proof - assume le: "r + ?d \ y + ?d" - from ymem have yd: "y + ?d \ A" by (simp add: eq) - have "r + ?d \ A" by (rule preal_downwards_closed' [OF A yd rdpos le]) - with notin show False by simp - qed - hence "y < r" by simp - with ypos have dless: "?d < (r * ?d)/y" - using dpos less_divide_eq_1 by fastforce - have "r + ?d < r*x" - proof - - have "r + ?d < r + (r * ?d)/y" by (simp add: dless) - also from ypos have "\ = (r/y) * (y + ?d)" - by (simp only: algebra_simps divide_inverse, simp) - also have "\ = r*x" using ypos - by simp - finally show "r + ?d < r*x" . - qed - with r notin rdpos - show "\r\A. r * x \ A" by (blast dest: preal_downwards_closed [OF A]) - qed -qed - -subsection\Existence of Inverse: Part 2\ - -lemma mem_Rep_preal_inverse_iff: - "(z \ Rep_preal(inverse r)) \ (0 < z \ (\y. z < y \ inverse y \ Rep_preal r))" - apply (simp add: preal_inverse_def mem_inverse_set Rep_preal) - apply (simp add: inverse_set_def) - done - -lemma Rep_preal_one: - "Rep_preal 1 = {x. 0 < x \ x < 1}" -by (simp add: preal_one_def rat_mem_preal) - -lemma subset_inverse_mult_lemma: - assumes xpos: "0 < x" and xless: "x < 1" - shows "\v u y. 0 < v \ v < y \ inverse y \ Rep_preal R \ - u \ Rep_preal R \ x = v * u" -proof - - from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff) - from lemma_gleason9_36 [OF cut_Rep_preal this] - obtain t where t: "t \ Rep_preal R" - and notin: "t * (inverse x) \ Rep_preal R" .. - have rpos: "0 Rep_preal R" and rless: "t < u" .. - have upos: "0 Rep_preal R" using notin - by (simp add: divide_inverse mult.commute) - show "u \ Rep_preal R" by (rule u) - show "x = x / u * u" using upos - by (simp add: divide_inverse mult.commute) - qed -qed - -lemma subset_inverse_mult: - "Rep_preal 1 \ Rep_preal(inverse r * r)" - by (force simp: Rep_preal_one mem_Rep_preal_inverse_iff mem_Rep_preal_mult_iff dest: subset_inverse_mult_lemma) - -lemma inverse_mult_subset: "Rep_preal(inverse r * r) \ Rep_preal 1" - proof - - have "0 < u * v" if "v \ Rep_preal r" "0 < u" "u < t" for u v t :: rat - using that by (simp add: zero_less_mult_iff preal_imp_pos [OF cut_Rep_preal]) - moreover have "t * q < 1" - if "q \ Rep_preal r" "0 < t" "t < y" "inverse y \ Rep_preal r" - for t q y :: rat - proof - - have "q < inverse y" - using not_in_Rep_preal_ub that by auto - hence "t * q < t/y" - using that by (simp add: divide_inverse mult_less_cancel_left) - also have "\ \ 1" - using that by (simp add: pos_divide_le_eq) - finally show ?thesis . - qed - ultimately show ?thesis - by (auto simp: Rep_preal_one mem_Rep_preal_inverse_iff mem_Rep_preal_mult_iff) -qed - -lemma preal_mult_inverse: "inverse r * r = (1::preal)" - by (meson Rep_preal_inject inverse_mult_subset subset_antisym subset_inverse_mult) - -lemma preal_mult_inverse_right: "r * inverse r = (1::preal)" - using preal_mult_commute preal_mult_inverse by auto - - -text\Theorems needing \Gleason9_34\\ - -lemma Rep_preal_self_subset: "Rep_preal (r) \ Rep_preal(r + s)" -proof - fix x - assume x: "x \ Rep_preal r" - obtain y where y: "y \ Rep_preal s" and "y > 0" - using Rep_preal preal_nonempty by blast - have ry: "x+y \ Rep_preal(r + s)" using x y - by (auto simp: mem_Rep_preal_add_iff) - then show "x \ Rep_preal(r + s)" - by (meson \0 < y\ add_less_same_cancel1 not_in_Rep_preal_ub order.asym preal_imp_pos [OF cut_Rep_preal x]) -qed - -lemma Rep_preal_sum_not_subset: "~ Rep_preal (r + s) \ Rep_preal(r)" -proof - - obtain y where y: "y \ Rep_preal s" and "y > 0" - using Rep_preal preal_nonempty by blast - obtain x where "x \ Rep_preal r" and notin: "x + y \ Rep_preal r" - using Dedekind_Real.Rep_preal Gleason9_34 \0 < y\ by blast - then have "x + y \ Rep_preal (r + s)" using y - by (auto simp: mem_Rep_preal_add_iff) - thus ?thesis using notin by blast -qed - -text\at last, Gleason prop. 9-3.5(iii) page 123\ -proposition preal_self_less_add_left: "(r::preal) < r + s" - by (meson Rep_preal_sum_not_subset not_less preal_le_def) - - -subsection\Subtraction for Positive Reals\ - -text\gleason prop. 9-3.5(iv), page 123: proving \<^prop>\a < b \ \d. a + d = b\. -We define the claimed \<^term>\D\ and show that it is a positive real\ - -lemma mem_diff_set: - assumes "r < s" - shows "cut (diff_set (Rep_preal s) (Rep_preal r))" -proof - - obtain p where "Rep_preal r \ Rep_preal s" "p \ Rep_preal s" "p \ Rep_preal r" - using assms unfolding preal_less_def by auto - then have "{} \ diff_set (Rep_preal s) (Rep_preal r)" - apply (simp add: diff_set_def psubset_eq) - by (metis cut_Rep_preal add_eq_exists less_add_same_cancel1 preal_exists_greater preal_imp_pos) - moreover - obtain q where "q > 0" "q \ Rep_preal s" - using Rep_preal_exists_bound by blast - then have qnot: "q \ diff_set (Rep_preal s) (Rep_preal r)" - by (auto simp: diff_set_def dest: cut_Rep_preal [THEN preal_downwards_closed]) - moreover have "diff_set (Rep_preal s) (Rep_preal r) \ {0<..}" (is "?lhs < ?rhs") - using \0 < q\ diff_set_def qnot by blast - moreover have "z \ diff_set (Rep_preal s) (Rep_preal r)" - if u: "u \ diff_set (Rep_preal s) (Rep_preal r)" and "0 < z" "z < u" for u z - using u that less_trans Rep_preal unfolding diff_set_def Dedekind_Real.cut_def by auto - moreover have "\u \ diff_set (Rep_preal s) (Rep_preal r). y < u" - if y: "y \ diff_set (Rep_preal s) (Rep_preal r)" for y - proof - - obtain a b where "0 < a" "0 < b" "a \ Rep_preal r" "a + y + b \ Rep_preal s" - using y - by (simp add: diff_set_def) (metis cut_Rep_preal add_eq_exists less_add_same_cancel1 preal_exists_greater) - then have "a + (y + b) \ Rep_preal s" - by (simp add: add.assoc) - then have "y + b \ diff_set (Rep_preal s) (Rep_preal r)" - using \0 < a\ \0 < b\ \a \ Rep_preal r\ y - by (auto simp: diff_set_def) - then show ?thesis - using \0 < b\ less_add_same_cancel1 by blast - qed - ultimately show ?thesis - by (simp add: Dedekind_Real.cut_def) -qed - -lemma mem_Rep_preal_diff_iff: - "r < s \ - (z \ Rep_preal (s - r)) \ - (\x. 0 < x \ 0 < z \ x \ Rep_preal r \ x + z \ Rep_preal s)" - apply (simp add: preal_diff_def mem_diff_set Rep_preal) - apply (force simp: diff_set_def) - done - -proposition less_add_left: - fixes r::preal - assumes "r < s" - shows "r + (s-r) = s" -proof - - have "a + b \ Rep_preal s" - if "a \ Rep_preal r" "c + b \ Rep_preal s" "c \ Rep_preal r" - and "0 < b" "0 < c" for a b c - by (meson cut_Rep_preal add_less_imp_less_right add_pos_pos not_in_Rep_preal_ub preal_downwards_closed preal_imp_pos that) - then have "r + (s-r) \ s" - using assms mem_Rep_preal_add_iff mem_Rep_preal_diff_iff preal_le_def by auto - have "x \ Rep_preal (r + (s - r))" if "x \ Rep_preal s" for x - proof (cases "x \ Rep_preal r") - case True - then show ?thesis - using Rep_preal_self_subset by blast - next - case False - have "\u v z. 0 < v \ 0 < z \ u \ Rep_preal r \ z \ Rep_preal r \ z + v \ Rep_preal s \ x = u + v" - if x: "x \ Rep_preal s" - proof - - have xpos: "x > 0" - using Rep_preal preal_imp_pos that by blast - obtain e where epos: "0 < e" and xe: "x + e \ Rep_preal s" - by (metis cut_Rep_preal x add_eq_exists less_add_same_cancel1 preal_exists_greater) - from Gleason9_34 [OF cut_Rep_preal epos] - obtain u where r: "u \ Rep_preal r" and notin: "u + e \ Rep_preal r" .. - with x False xpos have rless: "u < x" by (blast intro: not_in_Rep_preal_ub) - from add_eq_exists [of u x] - obtain y where eq: "x = u+y" by auto - show ?thesis - proof (intro exI conjI) - show "u + e \ Rep_preal r" by (rule notin) - show "u + e + y \ Rep_preal s" using xe eq by (simp add: ac_simps) - show "0 < u + e" - using epos preal_imp_pos [OF cut_Rep_preal r] by simp - qed (use r rless eq in auto) - qed - then show ?thesis - using assms mem_Rep_preal_add_iff mem_Rep_preal_diff_iff that by blast - qed - then have "s \ r + (s-r)" - by (auto simp: preal_le_def) - then show ?thesis - by (simp add: \r + (s - r) \ s\ antisym) -qed - -lemma preal_add_less2_mono1: "r < (s::preal) \ r + t < s + t" - by (metis add.assoc add.commute less_add_left preal_self_less_add_left) - -lemma preal_add_less2_mono2: "r < (s::preal) \ t + r < t + s" - by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of t]) - -lemma preal_add_right_less_cancel: "r + t < s + t \ r < (s::preal)" - by (metis linorder_cases order.asym preal_add_less2_mono1) - -lemma preal_add_left_less_cancel: "t + r < t + s \ r < (s::preal)" - by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of t]) - -lemma preal_add_less_cancel_left [simp]: "(t + (r::preal) < t + s) \ (r < s)" - by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel) - -lemma preal_add_less_cancel_right [simp]: "((r::preal) + t < s + t) = (r < s)" - using preal_add_less_cancel_left [symmetric, of r s t] by (simp add: ac_simps) - -lemma preal_add_le_cancel_left [simp]: "(t + (r::preal) \ t + s) = (r \ s)" - by (simp add: linorder_not_less [symmetric]) - -lemma preal_add_le_cancel_right [simp]: "((r::preal) + t \ s + t) = (r \ s)" - using preal_add_le_cancel_left [symmetric, of r s t] by (simp add: ac_simps) - -lemma preal_add_right_cancel: "(r::preal) + t = s + t \ r = s" - by (metis less_irrefl linorder_cases preal_add_less_cancel_right) - -lemma preal_add_left_cancel: "c + a = c + b \ a = (b::preal)" - by (auto intro: preal_add_right_cancel simp add: preal_add_commute) - -instance preal :: linordered_ab_semigroup_add -proof - fix a b c :: preal - show "a \ b \ c + a \ c + b" by (simp only: preal_add_le_cancel_left) -qed - - -subsection\Completeness of type \<^typ>\preal\\ - -text\Prove that supremum is a cut\ - -text\Part 1 of Dedekind sections definition\ - -lemma preal_sup: - assumes le: "\X. X \ P \ X \ Y" and "P \ {}" - shows "cut (\X \ P. Rep_preal(X))" -proof - - have "{} \ (\X \ P. Rep_preal(X))" - using \P \ {}\ mem_Rep_preal_Ex by fastforce - moreover - obtain q where "q > 0" and "q \ (\X \ P. Rep_preal(X))" - using Rep_preal_exists_bound [of Y] le by (auto simp: preal_le_def) - then have "(\X \ P. Rep_preal(X)) \ {0<..}" - using cut_Rep_preal preal_imp_pos by force - moreover - have "\u z. \u \ (\X \ P. Rep_preal(X)); 0 < z; z < u\ \ z \ (\X \ P. Rep_preal(X))" - by (auto elim: cut_Rep_preal [THEN preal_downwards_closed]) - moreover - have "\y. y \ (\X \ P. Rep_preal(X)) \ \u \ (\X \ P. Rep_preal(X)). y < u" - by (blast dest: cut_Rep_preal [THEN preal_exists_greater]) - ultimately show ?thesis - by (simp add: Dedekind_Real.cut_def) -qed - -lemma preal_psup_le: - "\\X. X \ P \ X \ Y; x \ P\ \ x \ psup P" - using preal_sup [of P Y] unfolding preal_le_def psup_def by fastforce - -lemma psup_le_ub: "\\X. X \ P \ X \ Y; P \ {}\ \ psup P \ Y" - using preal_sup [of P Y] by (simp add: SUP_least preal_le_def psup_def) - -text\Supremum property\ -proposition preal_complete: - assumes le: "\X. X \ P \ X \ Y" and "P \ {}" - shows "(\X \ P. Z < X) \ (Z < psup P)" (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - using preal_sup [OF assms] preal_less_def psup_def by auto -next - assume ?rhs - then show ?lhs - by (meson \P \ {}\ not_less psup_le_ub) -qed - -subsection \Defining the Reals from the Positive Reals\ - -text \Here we do quotients the old-fashioned way\ - -definition - realrel :: "((preal * preal) * (preal * preal)) set" where - "realrel = {p. \x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) \ x1+y2 = x2+y1}" - -definition "Real = UNIV//realrel" - -typedef real = Real - morphisms Rep_Real Abs_Real - unfolding Real_def by (auto simp: quotient_def) - -text \This doesn't involve the overloaded "real" function: users don't see it\ -definition - real_of_preal :: "preal \ real" where - "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})" - -instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}" -begin - -definition - real_zero_def: "0 = Abs_Real(realrel``{(1, 1)})" - -definition - real_one_def: "1 = Abs_Real(realrel``{(1 + 1, 1)})" - -definition - real_add_def: "z + w = - the_elem (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). - { Abs_Real(realrel``{(x+u, y+v)}) })" - -definition - real_minus_def: "- r = the_elem (\(x,y) \ Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })" - -definition - real_diff_def: "r - (s::real) = r + - s" - -definition - real_mult_def: - "z * w = - the_elem (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). - { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" - -definition - real_inverse_def: "inverse (r::real) = (THE s. (r = 0 \ s = 0) \ s * r = 1)" - -definition - real_divide_def: "r div (s::real) = r * inverse s" - -definition - real_le_def: "z \ (w::real) \ - (\x y u v. x+v \ u+y \ (x,y) \ Rep_Real z \ (u,v) \ Rep_Real w)" - -definition - real_less_def: "x < (y::real) \ x \ y \ x \ y" - -definition - real_abs_def: "\r::real\ = (if r < 0 then - r else r)" - -definition - real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0Equivalence relation over positive reals\ - -lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)) \ realrel) = (x1 + y2 = x2 + y1)" - by (simp add: realrel_def) - -lemma preal_trans_lemma: - assumes "x + y1 = x1 + y" and "x + y2 = x2 + y" - shows "x1 + y2 = x2 + (y1::preal)" - by (metis add.left_commute assms preal_add_left_cancel) - -lemma equiv_realrel: "equiv UNIV realrel" - by (auto simp: equiv_def refl_on_def sym_def trans_def realrel_def intro: dest: preal_trans_lemma) - -text\Reduces equality of equivalence classes to the \<^term>\realrel\ relation: - \<^term>\(realrel `` {x} = realrel `` {y}) = ((x,y) \ realrel)\\ -lemmas equiv_realrel_iff [simp] = - eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I] - -lemma realrel_in_real [simp]: "realrel``{(x,y)} \ Real" - by (simp add: Real_def realrel_def quotient_def, blast) - -declare Abs_Real_inject [simp] Abs_Real_inverse [simp] - - -text\Case analysis on the representation of a real number as an equivalence - class of pairs of positive reals.\ -lemma eq_Abs_Real [case_names Abs_Real, cases type: real]: - "(\x y. z = Abs_Real(realrel``{(x,y)}) \ P) \ P" - by (metis Rep_Real_inverse prod.exhaust Rep_Real [of z, unfolded Real_def, THEN quotientE]) - -subsection \Addition and Subtraction\ - -lemma real_add: - "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) = - Abs_Real (realrel``{(x+u, y+v)})" -proof - - have "(\z w. (\(x,y). (\(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z) - respects2 realrel" - by (clarsimp simp: congruent2_def) (metis add.left_commute preal_add_assoc) - thus ?thesis - by (simp add: real_add_def UN_UN_split_split_eq UN_equiv_class2 [OF equiv_realrel equiv_realrel]) -qed - -lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})" -proof - - have "(\(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel" - by (auto simp: congruent_def add.commute) - thus ?thesis - by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel]) -qed - -instance real :: ab_group_add -proof - fix x y z :: real - show "(x + y) + z = x + (y + z)" - by (cases x, cases y, cases z, simp add: real_add add.assoc) - show "x + y = y + x" - by (cases x, cases y, simp add: real_add add.commute) - show "0 + x = x" - by (cases x, simp add: real_add real_zero_def ac_simps) - show "- x + x = 0" - by (cases x, simp add: real_minus real_add real_zero_def add.commute) - show "x - y = x + - y" - by (simp add: real_diff_def) -qed - - -subsection \Multiplication\ - -lemma real_mult_congruent2_lemma: - "!!(x1::preal). \x1 + y2 = x2 + y1\ \ - x * x1 + y * y1 + (x * y2 + y * x2) = - x * x2 + y * y2 + (x * y1 + y * x1)" - by (metis (no_types, opaque_lifting) add.left_commute preal_add_commute preal_add_mult_distrib2) - -lemma real_mult_congruent2: - "(\p1 p2. - (\(x1,y1). (\(x2,y2). - { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1) - respects2 realrel" - apply (rule congruent2_commuteI [OF equiv_realrel]) - by (auto simp: mult.commute add.commute combine_common_factor preal_add_assoc preal_add_commute) - -lemma real_mult: - "Abs_Real((realrel``{(x1,y1)})) * Abs_Real((realrel``{(x2,y2)})) = - Abs_Real(realrel `` {(x1*x2+y1*y2,x1*y2+y1*x2)})" - by (simp add: real_mult_def UN_UN_split_split_eq - UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2]) - -lemma real_mult_commute: "(z::real) * w = w * z" -by (cases z, cases w, simp add: real_mult ac_simps) - -lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)" - by (cases z1, cases z2, cases z3) (simp add: real_mult algebra_simps) - -lemma real_mult_1: "(1::real) * z = z" - by (cases z) (simp add: real_mult real_one_def algebra_simps) - -lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" - by (cases z1, cases z2, cases w) (simp add: real_add real_mult algebra_simps) - -text\one and zero are distinct\ -lemma real_zero_not_eq_one: "0 \ (1::real)" -proof - - have "(1::preal) < 1 + 1" - by (simp add: preal_self_less_add_left) - then show ?thesis - by (simp add: real_zero_def real_one_def neq_iff) -qed - -instance real :: comm_ring_1 -proof - fix x y z :: real - show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) - show "x * y = y * x" by (rule real_mult_commute) - show "1 * x = x" by (rule real_mult_1) - show "(x + y) * z = x * z + y * z" by (rule real_add_mult_distrib) - show "0 \ (1::real)" by (rule real_zero_not_eq_one) -qed - -subsection \Inverse and Division\ - -lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0" - by (simp add: real_zero_def add.commute) - -lemma real_mult_inverse_left_ex: - assumes "x \ 0" obtains y::real where "y*x = 1" -proof (cases x) - case (Abs_Real u v) - show ?thesis - proof (cases u v rule: linorder_cases) - case less - then have "v * inverse (v - u) = 1 + u * inverse (v - u)" - using less_add_left [of u v] - by (metis preal_add_commute preal_add_mult_distrib preal_mult_inverse_right) - then have "Abs_Real (realrel``{(1, inverse (v-u) + 1)}) * x - 1 = 0" - by (simp add: Abs_Real real_mult preal_mult_inverse_right real_one_def) (simp add: algebra_simps) - with that show thesis by auto - next - case equal - then show ?thesis - using Abs_Real assms real_zero_iff by blast - next - case greater - then have "u * inverse (u - v) = 1 + v * inverse (u - v)" - using less_add_left [of v u] by (metis add.commute distrib_right preal_mult_inverse_right) - then have "Abs_Real (realrel``{(inverse (u-v) + 1, 1)}) * x - 1 = 0" - by (simp add: Abs_Real real_mult preal_mult_inverse_right real_one_def) (simp add: algebra_simps) - with that show thesis by auto - qed -qed - - -lemma real_mult_inverse_left: - fixes x :: real - assumes "x \ 0" shows "inverse x * x = 1" -proof - - obtain y where "y*x = 1" - using assms real_mult_inverse_left_ex by blast - then have "(THE s. s * x = 1) * x = 1" - proof (rule theI) - show "y' = y" if "y' * x = 1" for y' - by (metis \y * x = 1\ mult.left_commute mult.right_neutral that) - qed - then show ?thesis - using assms real_inverse_def by auto -qed - - -subsection\The Real Numbers form a Field\ - -instance real :: field -proof - fix x y z :: real - show "x \ 0 \ inverse x * x = 1" by (rule real_mult_inverse_left) - show "x / y = x * inverse y" by (simp add: real_divide_def) - show "inverse 0 = (0::real)" by (simp add: real_inverse_def) -qed - - -subsection\The \\\ Ordering\ - -lemma real_le_refl: "w \ (w::real)" - by (cases w, force simp: real_le_def) - -text\The arithmetic decision procedure is not set up for type preal. - This lemma is currently unused, but it could simplify the proofs of the - following two lemmas.\ -lemma preal_eq_le_imp_le: - assumes eq: "a+b = c+d" and le: "c \ a" - shows "b \ (d::preal)" -proof - - from le have "c+d \ a+d" by simp - hence "a+b \ a+d" by (simp add: eq) - thus "b \ d" by simp -qed - -lemma real_le_lemma: - assumes l: "u1 + v2 \ u2 + v1" - and "x1 + v1 = u1 + y1" - and "x2 + v2 = u2 + y2" - shows "x1 + y2 \ x2 + (y1::preal)" -proof - - have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms) - hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: ac_simps) - also have "\ \ (x2+y1) + (u2+v1)" by (simp add: assms) - finally show ?thesis by simp -qed - -lemma real_le: - "Abs_Real(realrel``{(x1,y1)}) \ Abs_Real(realrel``{(x2,y2)}) \ x1 + y2 \ x2 + y1" - unfolding real_le_def by (auto intro: real_le_lemma) - -lemma real_le_antisym: "\z \ w; w \ z\ \ z = (w::real)" - by (cases z, cases w, simp add: real_le) - -lemma real_trans_lemma: - assumes "x + v \ u + y" - and "u + v' \ u' + v" - and "x2 + v2 = u2 + y2" - shows "x + v' \ u' + (y::preal)" -proof - - have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: ac_simps) - also have "\ \ (u+y) + (u+v')" by (simp add: assms) - also have "\ \ (u+y) + (u'+v)" by (simp add: assms) - also have "\ = (u'+y) + (u+v)" by (simp add: ac_simps) - finally show ?thesis by simp -qed - -lemma real_le_trans: "\i \ j; j \ k\ \ i \ (k::real)" - by (cases i, cases j, cases k) (auto simp: real_le intro: real_trans_lemma) - -instance real :: order -proof - show "u < v \ u \ v \ \ v \ u" for u v::real - by (auto simp: real_less_def intro: real_le_antisym) -qed (auto intro: real_le_refl real_le_trans real_le_antisym) - -instance real :: linorder -proof - show "x \ y \ y \ x" for x y :: real - by (meson eq_refl le_cases real_le_def) -qed - -instantiation real :: distrib_lattice -begin - -definition - "(inf :: real \ real \ real) = min" - -definition - "(sup :: real \ real \ real) = max" - -instance - by standard (auto simp: inf_real_def sup_real_def max_min_distrib2) - -end - -subsection\The Reals Form an Ordered Field\ - -lemma real_le_eq_diff: "(x \ y) \ (x-y \ (0::real))" - by (cases x, cases y) (simp add: real_le real_zero_def real_diff_def real_add real_minus preal_add_commute) - -lemma real_add_left_mono: - assumes le: "x \ y" shows "z + x \ z + (y::real)" -proof - - have "z + x - (z + y) = (z + -z) + (x - y)" - by (simp add: algebra_simps) - with le show ?thesis - by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"]) -qed - -lemma real_sum_gt_zero_less: "(0 < s + (-w::real)) \ (w < s)" - by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of s]) - -lemma real_less_sum_gt_zero: "(w < s) \ (0 < s + (-w::real))" - by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of s]) - -lemma real_mult_order: - fixes x y::real - assumes "0 < x" "0 < y" - shows "0 < x * y" - proof (cases x, cases y) - show "0 < x * y" - if x: "x = Abs_Real (Dedekind_Real.realrel `` {(x1, x2)})" - and y: "y = Abs_Real (Dedekind_Real.realrel `` {(y1, y2)})" - for x1 x2 y1 y2 - proof - - have "x2 < x1" "y2 < y1" - using assms not_le real_zero_def real_le x y - by (metis preal_add_le_cancel_left real_zero_iff)+ - then obtain xd yd where "x1 = x2 + xd" "y1 = y2 + yd" - using less_add_left by metis - then have "\ (x * y \ 0)" - apply (simp add: x y real_mult real_zero_def real_le) - apply (simp add: not_le algebra_simps preal_self_less_add_left) - done - then show ?thesis - by auto - qed -qed - -lemma real_mult_less_mono2: "\(0::real) < z; x < y\ \ z * x < z * y" - by (metis add_uminus_conv_diff real_less_sum_gt_zero real_mult_order real_sum_gt_zero_less right_diff_distrib') - - -instance real :: linordered_field -proof - fix x y z :: real - show "x \ y \ z + x \ z + y" by (rule real_add_left_mono) - show "\x\ = (if x < 0 then -x else x)" by (simp only: real_abs_def) - show "sgn x = (if x=0 then 0 else if 0Completeness of the reals\ - -text\The function \<^term>\real_of_preal\ requires many proofs, but it seems -to be essential for proving completeness of the reals from that of the -positive reals.\ - -lemma real_of_preal_add: - "real_of_preal ((x::preal) + y) = real_of_preal x + real_of_preal y" - by (simp add: real_of_preal_def real_add algebra_simps) - -lemma real_of_preal_mult: - "real_of_preal ((x::preal) * y) = real_of_preal x * real_of_preal y" - by (simp add: real_of_preal_def real_mult algebra_simps) - -text\Gleason prop 9-4.4 p 127\ -lemma real_of_preal_trichotomy: - "\m. (x::real) = real_of_preal m \ x = 0 \ x = -(real_of_preal m)" -proof (cases x) - case (Abs_Real u v) - show ?thesis - proof (cases u v rule: linorder_cases) - case less - then show ?thesis - using less_add_left - apply (simp add: Abs_Real real_of_preal_def real_minus real_zero_def) - by (metis preal_add_assoc preal_add_commute) - next - case equal - then show ?thesis - using Abs_Real real_zero_iff by blast - next - case greater - then show ?thesis - using less_add_left - apply (simp add: Abs_Real real_of_preal_def real_minus real_zero_def) - by (metis preal_add_assoc preal_add_commute) - qed -qed - -lemma real_of_preal_less_iff [simp]: - "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" - by (metis not_less preal_add_less_cancel_right real_le real_of_preal_def) - -lemma real_of_preal_le_iff [simp]: - "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" - by (simp add: linorder_not_less [symmetric]) - -lemma real_of_preal_zero_less [simp]: "0 < real_of_preal m" - by (metis less_add_same_cancel2 preal_self_less_add_left real_of_preal_add real_of_preal_less_iff) - - -subsection\Theorems About the Ordering\ - -lemma real_gt_zero_preal_Ex: "(0 < x) \ (\y. x = real_of_preal y)" - using order.asym real_of_preal_trichotomy by fastforce - -subsection \Completeness of Positive Reals\ - -text \ - Supremum property for the set of positive reals - - Let \P\ be a non-empty set of positive reals, with an upper - bound \y\. Then \P\ has a least upper bound - (written \S\). - - FIXME: Can the premise be weakened to \\x \ P. x\ y\? -\ - -lemma posreal_complete: - assumes positive_P: "\x \ P. (0::real) < x" - and not_empty_P: "\x. x \ P" - and upper_bound_Ex: "\y. \x \ P. xs. \y. (\x \ P. y < x) = (y < s)" -proof (rule exI, rule allI) - fix y - let ?pP = "{w. real_of_preal w \ P}" - - show "(\x\P. y < x) = (y < real_of_preal (psup ?pP))" - proof (cases "0 < y") - assume neg_y: "\ 0 < y" - show ?thesis - proof - assume "\x\P. y < x" - thus "y < real_of_preal (psup ?pP)" - by (metis dual_order.strict_trans neg_y not_less_iff_gr_or_eq real_of_preal_zero_less) - next - assume "y < real_of_preal (psup ?pP)" - obtain "x" where x_in_P: "x \ P" using not_empty_P .. - thus "\x \ P. y < x" using x_in_P - using neg_y not_less_iff_gr_or_eq positive_P by fastforce - qed - next - assume pos_y: "0 < y" - then obtain py where y_is_py: "y = real_of_preal py" - by (auto simp: real_gt_zero_preal_Ex) - - obtain a where "a \ P" using not_empty_P .. - with positive_P have a_pos: "0 < a" .. - then obtain pa where "a = real_of_preal pa" - by (auto simp: real_gt_zero_preal_Ex) - hence "pa \ ?pP" using \a \ P\ by auto - hence pP_not_empty: "?pP \ {}" by auto - - obtain sup where sup: "\x \ P. x < sup" - using upper_bound_Ex .. - from this and \a \ P\ have "a < sup" .. - hence "0 < sup" using a_pos by arith - then obtain possup where "sup = real_of_preal possup" - by (auto simp: real_gt_zero_preal_Ex) - hence "\X \ ?pP. X \ possup" - using sup by auto - with pP_not_empty have psup: "\Z. (\X \ ?pP. Z < X) = (Z < psup ?pP)" - by (meson preal_complete) - show ?thesis - proof - assume "\x \ P. y < x" - then obtain x where x_in_P: "x \ P" and y_less_x: "y < x" .. - hence "0 < x" using pos_y by arith - then obtain px where x_is_px: "x = real_of_preal px" - by (auto simp: real_gt_zero_preal_Ex) - - have py_less_X: "\X \ ?pP. py < X" - proof - show "py < px" using y_is_py and x_is_px and y_less_x - by simp - show "px \ ?pP" using x_in_P and x_is_px by simp - qed - - have "(\X \ ?pP. py < X) \ (py < psup ?pP)" - using psup by simp - hence "py < psup ?pP" using py_less_X by simp - thus "y < real_of_preal (psup {w. real_of_preal w \ P})" - using y_is_py and pos_y by simp - next - assume y_less_psup: "y < real_of_preal (psup ?pP)" - - hence "py < psup ?pP" using y_is_py - by simp - then obtain "X" where py_less_X: "py < X" and X_in_pP: "X \ ?pP" - using psup by auto - then obtain x where x_is_X: "x = real_of_preal X" - by (simp add: real_gt_zero_preal_Ex) - hence "y < x" using py_less_X and y_is_py - by simp - moreover have "x \ P" - using x_is_X and X_in_pP by simp - ultimately show "\ x \ P. y < x" .. - qed - qed -qed - - -subsection \Completeness\ - -lemma reals_complete: - fixes S :: "real set" - assumes notempty_S: "\X. X \ S" - and exists_Ub: "bdd_above S" - shows "\x. (\s\S. s \ x) \ (\y. (\s\S. s \ y) \ x \ y)" -proof - - obtain X where X_in_S: "X \ S" using notempty_S .. - obtain Y where Y_isUb: "\s\S. s \ Y" - using exists_Ub by (auto simp: bdd_above_def) - let ?SHIFT = "{z. \x \S. z = x + (-X) + 1} \ {x. 0 < x}" - - { - fix x - assume S_le_x: "\s\S. s \ x" - { - fix s - assume "s \ {z. \x\S. z = x + - X + 1}" - hence "\ x \ S. s = x + -X + 1" .. - then obtain x1 where x1: "x1 \ S" "s = x1 + (-X) + 1" .. - then have "x1 \ x" using S_le_x by simp - with x1 have "s \ x + - X + 1" by arith - } - then have "\s\?SHIFT. s \ x + (-X) + 1" - by auto - } note S_Ub_is_SHIFT_Ub = this - - have *: "\s\?SHIFT. s \ Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub) - have "\s\?SHIFT. s < Y + (-X) + 2" - proof - fix s assume "s\?SHIFT" - with * have "s \ Y + (-X) + 1" by simp - also have "\ < Y + (-X) + 2" by simp - finally show "s < Y + (-X) + 2" . - qed - moreover have "\y \ ?SHIFT. 0 < y" by auto - moreover have shifted_not_empty: "\u. u \ ?SHIFT" - using X_in_S and Y_isUb by auto - ultimately obtain t where t_is_Lub: "\y. (\x\?SHIFT. y < x) = (y < t)" - using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast - - show ?thesis - proof - show "(\s\S. s \ (t + X + (-1))) \ (\y. (\s\S. s \ y) \ (t + X + (-1)) \ y)" - proof safe - fix x - assume "\s\S. s \ x" - hence "\s\?SHIFT. s \ x + (-X) + 1" - using S_Ub_is_SHIFT_Ub by simp - then have "\ x + (-X) + 1 < t" - by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less) - thus "t + X + -1 \ x" by arith - next - fix y - assume y_in_S: "y \ S" - obtain "u" where u_in_shift: "u \ ?SHIFT" using shifted_not_empty .. - hence "\ x \ S. u = x + - X + 1" by simp - then obtain "x" where x_and_u: "u = x + - X + 1" .. - have u_le_t: "u \ t" - proof (rule dense_le) - fix x assume "x < u" then have "x < t" - using u_in_shift t_is_Lub by auto - then show "x \ t" by simp - qed - - show "y \ t + X + -1" - proof cases - assume "y \ x" - moreover have "x = u + X + - 1" using x_and_u by arith - moreover have "u + X + - 1 \ t + X + -1" using u_le_t by arith - ultimately show "y \ t + X + -1" by arith - next - assume "~(y \ x)" - hence x_less_y: "x < y" by arith - - have "x + (-X) + 1 \ ?SHIFT" using x_and_u and u_in_shift by simp - hence "0 < x + (-X) + 1" by simp - hence "0 < y + (-X) + 1" using x_less_y by arith - hence *: "y + (-X) + 1 \ ?SHIFT" using y_in_S by simp - have "y + (-X) + 1 \ t" - proof (rule dense_le) - fix x assume "x < y + (-X) + 1" then have "x < t" - using * t_is_Lub by auto - then show "x \ t" by simp - qed - thus ?thesis by simp - qed - qed - qed -qed - -subsection \The Archimedean Property of the Reals\ - -theorem reals_Archimedean: - fixes x :: real - assumes x_pos: "0 < x" - shows "\n. inverse (of_nat (Suc n)) < x" -proof (rule ccontr) - assume contr: "\ ?thesis" - have "\n. x * of_nat (Suc n) \ 1" - proof - fix n - from contr have "x \ inverse (of_nat (Suc n))" - by (simp add: linorder_not_less) - hence "x \ (1 / (of_nat (Suc n)))" - by (simp add: inverse_eq_divide) - moreover have "(0::real) \ of_nat (Suc n)" - by (rule of_nat_0_le_iff) - ultimately have "x * of_nat (Suc n) \ (1 / of_nat (Suc n)) * of_nat (Suc n)" - by (rule mult_right_mono) - thus "x * of_nat (Suc n) \ 1" by (simp del: of_nat_Suc) - qed - hence 2: "bdd_above {z. \n. z = x * (of_nat (Suc n))}" - by (auto intro!: bdd_aboveI[of _ 1]) - have 1: "\X. X \ {z. \n. z = x* (of_nat (Suc n))}" by auto - obtain t where - upper: "\z. z \ {z. \n. z = x * of_nat (Suc n)} \ z \ t" and - least: "\y. (\a. a \ {z. \n. z = x * of_nat (Suc n)} \ a \ y) \ t \ y" - using reals_complete[OF 1 2] by auto - - have "t \ t + - x" - proof (rule least) - fix a assume a: "a \ {z. \n. z = x * (of_nat (Suc n))}" - have "\n::nat. x * of_nat n \ t + - x" - proof - fix n - have "x * of_nat (Suc n) \ t" - by (simp add: upper) - hence "x * (of_nat n) + x \ t" - by (simp add: distrib_left) - thus "x * (of_nat n) \ t + - x" by arith - qed hence "\m. x * of_nat (Suc m) \ t + - x" by (simp del: of_nat_Suc) - with a show "a \ t + - x" - by auto - qed - thus False using x_pos by arith -qed - -text \ - There must be other proofs, e.g. \Suc\ of the largest - integer in the cut representing \x\. -\ - -lemma reals_Archimedean2: "\n. (x::real) < of_nat (n::nat)" -proof cases - assume "x \ 0" - hence "x < of_nat (1::nat)" by simp - thus ?thesis .. -next - assume "\ x \ 0" - hence x_greater_zero: "0 < x" by simp - hence "0 < inverse x" by simp - then obtain n where "inverse (of_nat (Suc n)) < inverse x" - using reals_Archimedean by blast - hence "inverse (of_nat (Suc n)) * x < inverse x * x" - using x_greater_zero by (rule mult_strict_right_mono) - hence "inverse (of_nat (Suc n)) * x < 1" - using x_greater_zero by simp - hence "of_nat (Suc n) * (inverse (of_nat (Suc n)) * x) < of_nat (Suc n) * 1" - by (rule mult_strict_left_mono) (simp del: of_nat_Suc) - hence "x < of_nat (Suc n)" - by (simp add: algebra_simps del: of_nat_Suc) - thus "\(n::nat). x < of_nat n" .. -qed - -instance real :: archimedean_field -proof - fix r :: real - obtain n :: nat where "r < of_nat n" - using reals_Archimedean2 .. - then have "r \ of_int (int n)" - by simp - then show "\z. r \ of_int z" .. -qed - -end