diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1170 +1,1170 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples in Isabelle/HOL. " sessions "HOL-Library" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Seq 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 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-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-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 Leftist_Heap Binomial_Heap 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 Hoare 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-Number_Theory" + sessions "HOL-Data_Structures" "HOL-Examples" "HOL-Word" 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 " 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" 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 for Higher-Order Logic. " sessions "HOL-Word" theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists 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 Functions Function_Growth Gauge_Integration Guess 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 Primrec Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Sqrt 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 - Word_Conversions 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] 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" + 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 LDL TLList 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-Word" (main timing) in Word = HOL + sessions "HOL-Library" theories Word More_Word Word_Examples + Conversions document_files "root.bib" "root.tex" 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" in Mirabelle = HOL + theories Mirabelle_Test session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + options [timeout = 60] theories Ex session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" + options [quick_and_dirty] theories Boogie SMT_Examples SMT_Word_Examples SMT_Tests session "HOL-SPARK" in "SPARK" = "HOL-Word" + 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-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types 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 Mueller 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 Mueller The Alternating Bit Protocol performed in I/O-Automata. " 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 Mueller. " theories Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Mueller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Mueller " theories TrivEx TrivEx2 diff --git a/src/HOL/ex/Word_Conversions.thy b/src/HOL/Word/Conversions.thy rename from src/HOL/ex/Word_Conversions.thy rename to src/HOL/Word/Conversions.thy --- a/src/HOL/ex/Word_Conversions.thy +++ b/src/HOL/Word/Conversions.thy @@ -1,202 +1,325 @@ (* Author: Florian Haftmann, TUM *) section \Proof of concept for conversions for algebraically founded bit word types\ -theory Word_Conversions +theory Conversions imports Main "HOL-Library.Type_Length" "HOL-Library.Bit_Operations" "HOL-Word.Word" begin +hide_const (open) unat uint sint word_of_int ucast scast + +subsection \Conversions to words\ + +abbreviation word_of_nat :: \nat \ 'a::len word\ + where \word_of_nat \ of_nat\ + +abbreviation word_of_int :: \int \ 'a::len word\ + where \word_of_int \ of_int\ + +lemma Word_eq_word_of_int [simp]: + \Word.Word = word_of_int\ + by (rule ext; transfer) simp + +lemma word_of_nat_eq_iff: + \word_of_nat m = (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ + by transfer (simp add: take_bit_of_nat) + +lemma word_of_int_eq_iff: + \word_of_int k = (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ + by transfer rule + +lemma word_of_nat_less_eq_iff: + \word_of_nat m \ (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ + by transfer (simp add: take_bit_of_nat) + +lemma word_of_int_less_eq_iff: + \word_of_int k \ (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ + by transfer rule + +lemma word_of_nat_less_iff: + \word_of_nat m < (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ + by transfer (simp add: take_bit_of_nat) + +lemma word_of_int_less_iff: + \word_of_int k < (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ + by transfer rule + +lemma word_of_nat_eq_0_iff [simp]: + \word_of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ + using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) + +lemma word_of_int_eq_0_iff [simp]: + \word_of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ + using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) + +lemma int_AND_eq: + \int (m AND n) = int m AND int n\ + by (rule bit_eqI) (simp add: bit_and_iff) + +lemma int_OR_eq: + \int (m OR n) = int m OR int n\ + by (rule bit_eqI) (simp add: bit_or_iff) + +lemma int_XOR_eq: + \int (m XOR n) = int m XOR int n\ + by (rule bit_eqI) (simp add: bit_xor_iff) + +context semiring_bit_operations +begin + +lemma push_bit_and [simp]: + \push_bit n (a AND b) = push_bit n a AND push_bit n b\ + by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff) + +lemma push_bit_or [simp]: + \push_bit n (a OR b) = push_bit n a OR push_bit n b\ + by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff) + +lemma push_bit_xor [simp]: + \push_bit n (a XOR b) = push_bit n a XOR push_bit n b\ + by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff) + +lemma drop_bit_and [simp]: + \drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\ + by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff) + +lemma drop_bit_or [simp]: + \drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\ + by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff) + +lemma drop_bit_xor [simp]: + \drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\ + by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff) + +end + +lemma bit_word_of_nat_iff: + \bit (word_of_nat m :: 'a::len word) n \ n < LENGTH('a) \ bit m n\ + by transfer simp + +lemma bit_word_of_int_iff: + \bit (word_of_int k :: 'a::len word) n \ n < LENGTH('a) \ bit k n\ + by transfer simp + +lemma word_of_nat_AND_eq: + \word_of_nat (m AND n) = word_of_nat m AND word_of_nat n\ + by (rule bit_eqI) (auto simp add: bit_word_of_nat_iff bit_and_iff) + +lemma word_of_int_AND_eq: + \word_of_int (k AND l) = word_of_int k AND word_of_int l\ + by (rule bit_eqI) (auto simp add: bit_word_of_int_iff bit_and_iff) + +lemma word_of_nat_OR_eq: + \word_of_nat (m OR n) = word_of_nat m OR word_of_nat n\ + by (rule bit_eqI) (auto simp add: bit_word_of_nat_iff bit_or_iff) + +lemma word_of_int_OR_eq: + \word_of_int (k OR l) = word_of_int k OR word_of_int l\ + by (rule bit_eqI) (auto simp add: bit_word_of_int_iff bit_or_iff) + +lemma word_of_nat_XOR_eq: + \word_of_nat (m XOR n) = word_of_nat m XOR word_of_nat n\ + by (rule bit_eqI) (auto simp add: bit_word_of_nat_iff bit_xor_iff) + +lemma word_of_int_XOR_eq: + \word_of_int (k XOR l) = word_of_int k XOR word_of_int l\ + by (rule bit_eqI) (auto simp add: bit_word_of_int_iff bit_xor_iff) + + +subsection \Conversion from words\ + context semiring_1 begin lift_definition unsigned :: \'b::len word \ 'a\ is \of_nat \ nat \ take_bit LENGTH('b)\ by simp lemma unsigned_0 [simp]: \unsigned 0 = 0\ by transfer simp lemma unsigned_1 [simp]: \unsigned 1 = 1\ by transfer simp end -lemma unat_unsigned: - \unat = unsigned\ - by transfer simp - -lemma uint_unsigned: - \uint = unsigned\ - by transfer (simp add: fun_eq_iff) - context semiring_char_0 begin lemma unsigned_word_eqI: \v = w\ if \unsigned v = unsigned w\ using that by transfer (simp add: eq_nat_nat_iff) lemma word_eq_iff_unsigned: \v = w \ unsigned v = unsigned w\ by (auto intro: unsigned_word_eqI) end context ring_1 begin lift_definition signed :: \'b::len word \ 'a\ is \of_int \ signed_take_bit (LENGTH('b) - 1)\ by (simp flip: signed_take_bit_decr_length_iff) lemma signed_0 [simp]: \signed 0 = 0\ by transfer simp lemma signed_1 [simp]: \signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\ by (transfer fixing: uminus) (simp_all add: signed_take_bit_eq not_le Suc_lessI) lemma signed_minus_1 [simp]: \signed (- 1 :: 'b::len word) = - 1\ by (transfer fixing: uminus) simp end -lemma sint_signed: - \sint = signed\ - by transfer simp - context ring_char_0 begin lemma signed_word_eqI: \v = w\ if \signed v = signed w\ using that by transfer (simp flip: signed_take_bit_decr_length_iff) lemma word_eq_iff_signed: \v = w \ signed v = signed w\ by (auto intro: signed_word_eqI) end -abbreviation nat_of_word :: \'a::len word \ nat\ - where \nat_of_word \ unsigned\ - -abbreviation unsigned_int :: \'a::len word \ int\ - where \unsigned_int \ unsigned\ +abbreviation unat :: \'a::len word \ nat\ + where \unat \ unsigned\ -abbreviation signed_int :: \'a::len word \ int\ - where \signed_int \ signed\ +abbreviation uint :: \'a::len word \ int\ + where \uint \ unsigned\ -abbreviation word_of_nat :: \nat \ 'a::len word\ - where \word_of_nat \ of_nat\ +abbreviation sint :: \'a::len word \ int\ + where \sint \ signed\ -abbreviation word_of_int :: \int \ 'a::len word\ - where \word_of_int \ of_int\ +abbreviation ucast :: \'a::len word \ 'b::len word\ + where \ucast \ unsigned\ + +abbreviation scast :: \'a::len word \ 'b::len word\ + where \scast \ signed\ + +context + includes lifting_syntax +begin + +lemma [transfer_rule]: + \(pcr_word ===> (=)) (nat \ take_bit LENGTH('a)) (unat :: 'a::len word \ nat)\ + using unsigned.transfer [where ?'a = nat] by simp + +lemma [transfer_rule]: + \(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \ int)\ + using unsigned.transfer [where ?'a = int] by (simp add: comp_def) + +lemma [transfer_rule]: + \(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \ int)\ + using signed.transfer [where ?'a = int] by simp + +lemma [transfer_rule]: + \(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \ 'b::len word)\ +proof (rule rel_funI) + fix k :: int and w :: \'a word\ + assume \pcr_word k w\ + then have \w = word_of_int k\ + by (simp add: pcr_word_def cr_word_def relcompp_apply) + moreover have \pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\ + by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) + ultimately show \pcr_word (take_bit LENGTH('a) k) (ucast w)\ + by simp +qed + +lemma [transfer_rule]: + \(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - 1)) (scast :: 'a::len word \ 'b::len word)\ +proof (rule rel_funI) + fix k :: int and w :: \'a word\ + assume \pcr_word k w\ + then have \w = word_of_int k\ + by (simp add: pcr_word_def cr_word_def relcompp_apply) + moreover have \pcr_word (signed_take_bit (LENGTH('a) - 1) k) (scast (word_of_int k :: 'a word))\ + by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) + ultimately show \pcr_word (signed_take_bit (LENGTH('a) - 1) k) (scast w)\ + by simp +qed + +end lemma unsigned_of_nat [simp]: \unsigned (of_nat n :: 'a::len word) = of_nat (take_bit LENGTH('a) n)\ by transfer (simp add: nat_eq_iff take_bit_of_nat) -lemma of_nat_of_word [simp]: - \of_nat (nat_of_word w) = unsigned w\ - by transfer simp - -lemma of_int_unsigned [simp]: - \of_int (unsigned_int w) = unsigned w\ - by transfer simp - -lemma unsigned_int_greater_eq: - \0 \ unsigned_int w\ for w :: \'a::len word\ +lemma of_nat_unat [simp]: + \of_nat (unat w) = unsigned w\ by transfer simp -lemma nat_of_word_less: - \nat_of_word w < 2 ^ LENGTH('a)\ for w :: \'a::len word\ - by transfer (simp add: take_bit_eq_mod) - -lemma unsigned_int_less: - \unsigned_int w < 2 ^ LENGTH('a)\ for w :: \'a::len word\ - by transfer (simp add: take_bit_eq_mod) - -lemma signed_of_int [simp]: - \signed (word_of_int k :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - 1) k)\ +lemma of_int_uint [simp]: + \of_int (uint w) = unsigned w\ by transfer simp -lemma of_int_signed [simp]: - \of_int (signed_int a) = signed a\ - by transfer (simp_all add: take_bit_signed_take_bit) +context unique_euclidean_semiring_numeral +begin -lemma signed_int_greater_eq: - \- (2 ^ (LENGTH('a) - 1)) \ signed_int w\ for w :: \'a::len word\ -proof (cases \bit w (LENGTH('a) - 1)\) - case True - then show ?thesis - by transfer (simp add: signed_take_bit_eq_or minus_exp_eq_not_mask or_greater_eq ac_simps) -next - have *: \- (2 ^ (LENGTH('a) - Suc 0)) \ (0::int)\ - by simp - case False - then show ?thesis - by transfer (auto simp add: signed_take_bit_eq intro: order_trans *) -qed +lemma unsigned_greater_eq: + \0 \ unsigned w\ for w :: \'b::len word\ + by (transfer fixing: less_eq) simp -lemma signed_int_less: - \signed_int w < 2 ^ (LENGTH('a) - 1)\ for w :: \'a::len word\ - by (cases \bit w (LENGTH('a) - 1)\; transfer) - (simp_all add: signed_take_bit_eq signed_take_bit_eq_or take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper) +lemma unsigned_less: + \unsigned w < 2 ^ LENGTH('b)\ for w :: \'b::len word\ + by (transfer fixing: less) (simp add: take_bit_int_less_exp) + +end context linordered_semidom begin lemma word_less_eq_iff_unsigned: "a \ b \ unsigned a \ unsigned b" by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) lemma word_less_iff_unsigned: "a < b \ unsigned a < unsigned b" by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) end -lemma word_of_nat_eq_iff: - \word_of_nat m = (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ - by transfer (simp add: take_bit_of_nat) - -lemma word_of_nat_less_eq_iff: - \word_of_nat m \ (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ - by transfer (simp add: take_bit_of_nat) - -lemma word_of_nat_less_iff: - \word_of_nat m < (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ - by transfer (simp add: take_bit_of_nat) +lemma signed_of_int [simp]: + \signed (word_of_int k :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - 1) k)\ + by transfer simp -lemma word_of_nat_eq_0_iff: - \word_of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ - using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) - -lemma word_of_int_eq_iff: - \word_of_int k = (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ - by transfer rule +lemma of_int_sint [simp]: + \of_int (sint a) = signed a\ + by transfer (simp_all add: take_bit_signed_take_bit) -lemma word_of_int_less_eq_iff: - \word_of_int k \ (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ - by transfer rule +lemma sint_greater_eq: + \- (2 ^ (LENGTH('a) - 1)) \ sint w\ for w :: \'a::len word\ +proof (cases \bit w (LENGTH('a) - 1)\) + case True + then show ?thesis + by transfer (simp add: signed_take_bit_eq_or minus_exp_eq_not_mask or_greater_eq ac_simps) +next + have *: \- (2 ^ (LENGTH('a) - Suc 0)) \ (0::int)\ + by simp + case False + then show ?thesis + by transfer (auto simp add: signed_take_bit_eq intro: order_trans *) +qed -lemma word_of_int_less_iff: - \word_of_int k < (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ - by transfer rule - -lemma word_of_int_eq_0_iff: - \word_of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ - using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) +lemma sint_less: + \sint w < 2 ^ (LENGTH('a) - 1)\ for w :: \'a::len word\ + by (cases \bit w (LENGTH('a) - 1)\; transfer) + (simp_all add: signed_take_bit_eq signed_take_bit_eq_or take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper) end diff --git a/src/HOL/ex/Bit_Lists.thy b/src/HOL/ex/Bit_Lists.thy --- a/src/HOL/ex/Bit_Lists.thy +++ b/src/HOL/ex/Bit_Lists.thy @@ -1,357 +1,357 @@ (* Author: Florian Haftmann, TUM *) section \Proof(s) of concept for algebraically founded lists of bits\ theory Bit_Lists imports - Word_Conversions "HOL-Library.More_List" + "HOL-Word.Conversions" "HOL-Library.More_List" begin subsection \Fragments of algebraic bit representations\ context comm_semiring_1 begin abbreviation (input) unsigned_of_bits :: "bool list \ 'a" where "unsigned_of_bits \ horner_sum of_bool 2" lemma unsigned_of_bits_replicate_False [simp]: "unsigned_of_bits (replicate n False) = 0" by (induction n) simp_all end context unique_euclidean_semiring_with_bit_shifts begin lemma unsigned_of_bits_append [simp]: "unsigned_of_bits (bs @ cs) = unsigned_of_bits bs + push_bit (length bs) (unsigned_of_bits cs)" by (induction bs) (simp_all add: push_bit_double, simp_all add: algebra_simps) lemma unsigned_of_bits_take [simp]: "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)" proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) then show ?case by (cases n) (simp_all add: ac_simps take_bit_Suc) qed lemma unsigned_of_bits_drop [simp]: "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)" proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) then show ?case by (cases n) (simp_all add: drop_bit_Suc) qed lemma bit_unsigned_of_bits_iff: \bit (unsigned_of_bits bs) n \ nth_default False bs n\ proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) then show ?case by (cases n) (simp_all add: bit_Suc) qed primrec n_bits_of :: "nat \ 'a \ bool list" where "n_bits_of 0 a = []" | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)" lemma n_bits_of_eq_iff: "n_bits_of n a = n_bits_of n b \ take_bit n a = take_bit n b" apply (induction n arbitrary: a b) apply (auto elim!: evenE oddE simp add: take_bit_Suc mod_2_eq_odd) apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one) apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one) done lemma take_n_bits_of [simp]: "take m (n_bits_of n a) = n_bits_of (min m n) a" proof - define q and v and w where "q = min m n" and "v = m - q" and "w = n - q" then have "v = 0 \ w = 0" by auto then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a" by (induction q arbitrary: a) auto with q_def v_def w_def show ?thesis by simp qed lemma unsigned_of_bits_n_bits_of [simp]: "unsigned_of_bits (n_bits_of n a) = take_bit n a" by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc mod_2_eq_odd) end subsection \Syntactic bit representation\ class bit_representation = fixes bits_of :: "'a \ bool list" and of_bits :: "bool list \ 'a" assumes of_bits_of [simp]: "of_bits (bits_of a) = a" text \Unclear whether a \<^typ>\bool\ instantiation is needed or not\ instantiation nat :: bit_representation begin fun bits_of_nat :: "nat \ bool list" where "bits_of (n::nat) = (if n = 0 then [] else odd n # bits_of (n div 2))" lemma bits_of_nat_simps [simp]: "bits_of (0::nat) = []" "n > 0 \ bits_of n = odd n # bits_of (n div 2)" for n :: nat by simp_all declare bits_of_nat.simps [simp del] definition of_bits_nat :: "bool list \ nat" where [simp]: "of_bits_nat = unsigned_of_bits" \ \remove simp\ instance proof show "of_bits (bits_of n) = n" for n :: nat by (induction n rule: nat_bit_induct) simp_all qed end lemma bit_of_bits_nat_iff: \bit (of_bits bs :: nat) n \ nth_default False bs n\ by (simp add: bit_unsigned_of_bits_iff) lemma bits_of_Suc_0 [simp]: "bits_of (Suc 0) = [True]" by simp lemma bits_of_1_nat [simp]: "bits_of (1 :: nat) = [True]" by simp lemma bits_of_nat_numeral_simps [simp]: "bits_of (numeral Num.One :: nat) = [True]" (is ?One) "bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0) "bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1) proof - show ?One by simp define m :: nat where "m = numeral n" then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)" by simp_all from \m > 0\ show ?Bit0 ?Bit1 by (simp_all add: *) qed lemma unsigned_of_bits_of_nat [simp]: "unsigned_of_bits (bits_of n) = n" for n :: nat using of_bits_of [of n] by simp instantiation int :: bit_representation begin fun bits_of_int :: "int \ bool list" where "bits_of_int k = odd k # (if k = 0 \ k = - 1 then [] else bits_of_int (k div 2))" lemma bits_of_int_simps [simp]: "bits_of (0 :: int) = [False]" "bits_of (- 1 :: int) = [True]" "k \ 0 \ k \ - 1 \ bits_of k = odd k # bits_of (k div 2)" for k :: int by simp_all lemma bits_of_not_Nil [simp]: "bits_of k \ []" for k :: int by simp declare bits_of_int.simps [simp del] definition of_bits_int :: "bool list \ int" where "of_bits_int bs = (if bs = [] \ \ last bs then unsigned_of_bits bs else unsigned_of_bits bs - 2 ^ length bs)" lemma of_bits_int_simps [simp]: "of_bits [] = (0 :: int)" "of_bits [False] = (0 :: int)" "of_bits [True] = (- 1 :: int)" "of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b" "of_bits (False # bs) = 2 * (of_bits bs :: int)" "bs \ [] \ of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)" by (simp_all add: of_bits_int_def push_bit_of_1) instance proof show "of_bits (bits_of k) = k" for k :: int by (induction k rule: int_bit_induct) simp_all qed lemma bits_of_1_int [simp]: "bits_of (1 :: int) = [True, False]" by simp lemma bits_of_int_numeral_simps [simp]: "bits_of (numeral Num.One :: int) = [True, False]" (is ?One) "bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0) "bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1) "bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0) "bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1) proof - show ?One by simp define k :: int where "k = numeral n" then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1" "numeral (Num.inc n) = k + 1" by (simp_all add: add_One) have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1" by simp_all with \k > 0\ show ?Bit0 ?Bit1 ?nBit0 ?nBit1 by (simp_all add: *) qed lemma bit_of_bits_int_iff: \bit (of_bits bs :: int) n \ nth_default (bs \ [] \ last bs) bs n\ proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) then show ?case by (cases n; cases b; cases bs) (simp_all add: bit_Suc) qed lemma of_bits_append [simp]: "of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)" if "bs \ []" "\ last bs" using that proof (induction bs rule: list_nonempty_induct) case (single b) then show ?case by simp next case (cons b bs) then show ?case by (cases b) (simp_all add: push_bit_double) qed lemma of_bits_replicate_False [simp]: "of_bits (replicate n False) = (0 :: int)" by (auto simp add: of_bits_int_def) lemma of_bits_drop [simp]: "of_bits (drop n bs) = drop_bit n (of_bits bs :: int)" if "n < length bs" using that proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) show ?case proof (cases n) case 0 then show ?thesis by simp next case (Suc n) with Cons.prems have "bs \ []" by auto with Suc Cons.IH [of n] Cons.prems show ?thesis by (cases b) (simp_all add: drop_bit_Suc) qed qed end lemma unsigned_of_bits_eq_of_bits: "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)" by (simp add: of_bits_int_def) unbundle word.lifting instantiation word :: (len) bit_representation begin lift_definition bits_of_word :: "'a word \ bool list" is "n_bits_of LENGTH('a)" by (simp add: n_bits_of_eq_iff) lift_definition of_bits_word :: "bool list \ 'a word" is unsigned_of_bits . instance proof fix a :: "'a word" show "of_bits (bits_of a) = a" by transfer simp qed end lifting_update word.lifting lifting_forget word.lifting subsection \Bit representations with bit operations\ class semiring_bit_representation = semiring_bit_operations + bit_representation + assumes and_eq: "length bs = length cs \ of_bits bs AND of_bits cs = of_bits (map2 (\) bs cs)" and or_eq: "length bs = length cs \ of_bits bs OR of_bits cs = of_bits (map2 (\) bs cs)" and xor_eq: "length bs = length cs \ of_bits bs XOR of_bits cs = of_bits (map2 (\) bs cs)" and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)" and drop_bit_eq: "n < length (bits_of a) \ drop_bit n a = of_bits (drop n (bits_of a))" class ring_bit_representation = ring_bit_operations + semiring_bit_representation + assumes not_eq: "not = of_bits \ map Not \ bits_of" instance nat :: semiring_bit_representation by standard (simp_all add: bit_eq_iff bit_unsigned_of_bits_iff nth_default_map2 [of _ _ _ False False] bit_and_iff bit_or_iff bit_xor_iff) instance int :: ring_bit_representation proof { fix bs cs :: \bool list\ assume \length bs = length cs\ then have \cs = [] \ bs = []\ by auto with \length bs = length cs\ have \zip bs cs \ [] \ last (map2 (\) bs cs) \ (bs \ [] \ last bs) \ (cs \ [] \ last cs)\ and \zip bs cs \ [] \ last (map2 (\) bs cs) \ (bs \ [] \ last bs) \ (cs \ [] \ last cs)\ and \zip bs cs \ [] \ last (map2 (\) bs cs) \ ((bs \ [] \ last bs) \ (cs \ [] \ last cs))\ by (auto simp add: last_map last_zip zip_eq_Nil_iff prod_eq_iff) then show \of_bits bs AND of_bits cs = (of_bits (map2 (\) bs cs) :: int)\ and \of_bits bs OR of_bits cs = (of_bits (map2 (\) bs cs) :: int)\ and \of_bits bs XOR of_bits cs = (of_bits (map2 (\) bs cs) :: int)\ by (simp_all add: fun_eq_iff bit_eq_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff bit_of_bits_int_iff \length bs = length cs\ nth_default_map2 [of bs cs _ \bs \ [] \ last bs\ \cs \ [] \ last cs\]) } show \push_bit n k = of_bits (replicate n False @ bits_of k)\ for k :: int and n :: nat by (cases "n = 0") simp_all show \drop_bit n k = of_bits (drop n (bits_of k))\ if \n < length (bits_of k)\ for k :: int and n :: nat using that by simp show \(not :: int \ _) = of_bits \ map Not \ bits_of\ proof (rule sym, rule ext) fix k :: int show \(of_bits \ map Not \ bits_of) k = NOT k\ by (induction k rule: int_bit_induct) (simp_all add: not_int_def) qed qed end