diff --git a/src/HOL/Library/Boolean_Algebra.thy b/src/HOL/Library/Boolean_Algebra.thy --- a/src/HOL/Library/Boolean_Algebra.thy +++ b/src/HOL/Library/Boolean_Algebra.thy @@ -1,284 +1,286 @@ (* Title: HOL/Library/Boolean_Algebra.thy Author: Brian Huffman *) section \Boolean Algebras\ theory Boolean_Algebra imports Main begin locale boolean_algebra = conj: abel_semigroup "(\<^bold>\)" + disj: abel_semigroup "(\<^bold>\)" for conj :: "'a \ 'a \ 'a" (infixr "\<^bold>\" 70) and disj :: "'a \ 'a \ 'a" (infixr "\<^bold>\" 65) + fixes compl :: "'a \ 'a" ("\ _" [81] 80) and zero :: "'a" ("\") and one :: "'a" ("\") assumes conj_disj_distrib: "x \<^bold>\ (y \<^bold>\ z) = (x \<^bold>\ y) \<^bold>\ (x \<^bold>\ z)" and disj_conj_distrib: "x \<^bold>\ (y \<^bold>\ z) = (x \<^bold>\ y) \<^bold>\ (x \<^bold>\ z)" and conj_one_right: "x \<^bold>\ \ = x" and disj_zero_right: "x \<^bold>\ \ = x" and conj_cancel_right [simp]: "x \<^bold>\ \ x = \" and disj_cancel_right [simp]: "x \<^bold>\ \ x = \" begin sublocale conj: semilattice_neutr "(\<^bold>\)" "\" proof show "x \<^bold>\ \ = x" for x by (fact conj_one_right) show "x \<^bold>\ x = x" for x proof - have "x \<^bold>\ x = (x \<^bold>\ x) \<^bold>\ \" by (simp add: disj_zero_right) also have "\ = (x \<^bold>\ x) \<^bold>\ (x \<^bold>\ \ x)" by simp also have "\ = x \<^bold>\ (x \<^bold>\ \ x)" by (simp only: conj_disj_distrib) also have "\ = x \<^bold>\ \" by simp also have "\ = x" by (simp add: conj_one_right) finally show ?thesis . qed qed sublocale disj: semilattice_neutr "(\<^bold>\)" "\" proof show "x \<^bold>\ \ = x" for x by (fact disj_zero_right) show "x \<^bold>\ x = x" for x proof - have "x \<^bold>\ x = (x \<^bold>\ x) \<^bold>\ \" by simp also have "\ = (x \<^bold>\ x) \<^bold>\ (x \<^bold>\ \ x)" by simp also have "\ = x \<^bold>\ (x \<^bold>\ \ x)" by (simp only: disj_conj_distrib) also have "\ = x \<^bold>\ \" by simp also have "\ = x" by (simp add: disj_zero_right) finally show ?thesis . qed qed subsection \Complement\ lemma complement_unique: assumes 1: "a \<^bold>\ x = \" assumes 2: "a \<^bold>\ x = \" assumes 3: "a \<^bold>\ y = \" assumes 4: "a \<^bold>\ y = \" shows "x = y" proof - from 1 3 have "(a \<^bold>\ x) \<^bold>\ (x \<^bold>\ y) = (a \<^bold>\ y) \<^bold>\ (x \<^bold>\ y)" by simp then have "(x \<^bold>\ a) \<^bold>\ (x \<^bold>\ y) = (y \<^bold>\ a) \<^bold>\ (y \<^bold>\ x)" by (simp add: ac_simps) then have "x \<^bold>\ (a \<^bold>\ y) = y \<^bold>\ (a \<^bold>\ x)" by (simp add: conj_disj_distrib) with 2 4 have "x \<^bold>\ \ = y \<^bold>\ \" by simp then show "x = y" by simp qed lemma compl_unique: "x \<^bold>\ y = \ \ x \<^bold>\ y = \ \ \ x = y" by (rule complement_unique [OF conj_cancel_right disj_cancel_right]) lemma double_compl [simp]: "\ (\ x) = x" proof (rule compl_unique) show "\ x \<^bold>\ x = \" by (simp only: conj_cancel_right conj.commute) show "\ x \<^bold>\ x = \" by (simp only: disj_cancel_right disj.commute) qed lemma compl_eq_compl_iff [simp]: "\ x = \ y \ x = y" by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl) subsection \Conjunction\ lemma conj_zero_right [simp]: "x \<^bold>\ \ = \" using conj.left_idem conj_cancel_right by fastforce lemma compl_one [simp]: "\ \ = \" by (rule compl_unique [OF conj_zero_right disj_zero_right]) lemma conj_zero_left [simp]: "\ \<^bold>\ x = \" by (subst conj.commute) (rule conj_zero_right) lemma conj_cancel_left [simp]: "\ x \<^bold>\ x = \" by (subst conj.commute) (rule conj_cancel_right) lemma conj_disj_distrib2: "(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)" by (simp only: conj.commute conj_disj_distrib) lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2 lemma conj_assoc: "(x \<^bold>\ y) \<^bold>\ z = x \<^bold>\ (y \<^bold>\ z)" by (fact ac_simps) lemma conj_commute: "x \<^bold>\ y = y \<^bold>\ x" by (fact ac_simps) lemmas conj_left_commute = conj.left_commute lemmas conj_ac = conj.assoc conj.commute conj.left_commute lemma conj_one_left: "\ \<^bold>\ x = x" by (fact conj.left_neutral) lemma conj_left_absorb: "x \<^bold>\ (x \<^bold>\ y) = x \<^bold>\ y" by (fact conj.left_idem) lemma conj_absorb: "x \<^bold>\ x = x" by (fact conj.idem) subsection \Disjunction\ interpretation dual: boolean_algebra "(\<^bold>\)" "(\<^bold>\)" compl \ \ apply standard apply (rule disj_conj_distrib) apply (rule conj_disj_distrib) apply simp_all done lemma compl_zero [simp]: "\ \ = \" by (fact dual.compl_one) lemma disj_one_right [simp]: "x \<^bold>\ \ = \" by (fact dual.conj_zero_right) lemma disj_one_left [simp]: "\ \<^bold>\ x = \" by (fact dual.conj_zero_left) lemma disj_cancel_left [simp]: "\ x \<^bold>\ x = \" by (rule dual.conj_cancel_left) lemma disj_conj_distrib2: "(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)" by (rule dual.conj_disj_distrib2) lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2 lemma disj_assoc: "(x \<^bold>\ y) \<^bold>\ z = x \<^bold>\ (y \<^bold>\ z)" by (fact ac_simps) lemma disj_commute: "x \<^bold>\ y = y \<^bold>\ x" by (fact ac_simps) lemmas disj_left_commute = disj.left_commute lemmas disj_ac = disj.assoc disj.commute disj.left_commute lemma disj_zero_left: "\ \<^bold>\ x = x" by (fact disj.left_neutral) lemma disj_left_absorb: "x \<^bold>\ (x \<^bold>\ y) = x \<^bold>\ y" by (fact disj.left_idem) lemma disj_absorb: "x \<^bold>\ x = x" by (fact disj.idem) subsection \De Morgan's Laws\ lemma de_Morgan_conj [simp]: "\ (x \<^bold>\ y) = \ x \<^bold>\ \ y" proof (rule compl_unique) have "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = ((x \<^bold>\ y) \<^bold>\ \ x) \<^bold>\ ((x \<^bold>\ y) \<^bold>\ \ y)" by (rule conj_disj_distrib) also have "\ = (y \<^bold>\ (x \<^bold>\ \ x)) \<^bold>\ (x \<^bold>\ (y \<^bold>\ \ y))" by (simp only: conj_ac) finally show "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = \" by (simp only: conj_cancel_right conj_zero_right disj_zero_right) next have "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = (x \<^bold>\ (\ x \<^bold>\ \ y)) \<^bold>\ (y \<^bold>\ (\ x \<^bold>\ \ y))" by (rule disj_conj_distrib2) also have "\ = (\ y \<^bold>\ (x \<^bold>\ \ x)) \<^bold>\ (\ x \<^bold>\ (y \<^bold>\ \ y))" by (simp only: disj_ac) finally show "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = \" by (simp only: disj_cancel_right disj_one_right conj_one_right) qed lemma de_Morgan_disj [simp]: "\ (x \<^bold>\ y) = \ x \<^bold>\ \ y" using dual.boolean_algebra_axioms by (rule boolean_algebra.de_Morgan_conj) subsection \Symmetric Difference\ definition xor :: "'a \ 'a \ 'a" (infixr "\" 65) where "x \ y = (x \<^bold>\ \ y) \<^bold>\ (\ x \<^bold>\ y)" -sublocale xor: abel_semigroup xor +sublocale xor: comm_monoid xor \ proof fix x y z :: 'a let ?t = "(x \<^bold>\ y \<^bold>\ z) \<^bold>\ (x \<^bold>\ \ y \<^bold>\ \ z) \<^bold>\ (\ x \<^bold>\ y \<^bold>\ \ z) \<^bold>\ (\ x \<^bold>\ \ y \<^bold>\ z)" have "?t \<^bold>\ (z \<^bold>\ x \<^bold>\ \ x) \<^bold>\ (z \<^bold>\ y \<^bold>\ \ y) = ?t \<^bold>\ (x \<^bold>\ y \<^bold>\ \ y) \<^bold>\ (x \<^bold>\ z \<^bold>\ \ z)" by (simp only: conj_cancel_right conj_zero_right) then show "(x \ y) \ z = x \ (y \ z)" by (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) (simp only: conj_disj_distribs conj_ac disj_ac) show "x \ y = y \ x" by (simp only: xor_def conj_commute disj_commute) + show "x \ \ = x" + by (simp add: xor_def) qed lemmas xor_assoc = xor.assoc lemmas xor_commute = xor.commute lemmas xor_left_commute = xor.left_commute lemmas xor_ac = xor.assoc xor.commute xor.left_commute lemma xor_def2: "x \ y = (x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y)" using conj.commute conj_disj_distrib2 disj.commute xor_def by auto lemma xor_zero_right [simp]: "x \ \ = x" by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right) lemma xor_zero_left [simp]: "\ \ x = x" by (subst xor_commute) (rule xor_zero_right) lemma xor_one_right [simp]: "x \ \ = \ x" by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left) lemma xor_one_left [simp]: "\ \ x = \ x" by (subst xor_commute) (rule xor_one_right) lemma xor_self [simp]: "x \ x = \" by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right) lemma xor_left_self [simp]: "x \ (x \ y) = y" by (simp only: xor_assoc [symmetric] xor_self xor_zero_left) lemma xor_compl_left [simp]: "\ x \ y = \ (x \ y)" by (metis xor_assoc xor_one_left) lemma xor_compl_right [simp]: "x \ \ y = \ (x \ y)" using xor_commute xor_compl_left by auto lemma xor_cancel_right: "x \ \ x = \" by (simp only: xor_compl_right xor_self compl_zero) lemma xor_cancel_left: "\ x \ x = \" by (simp only: xor_compl_left xor_self compl_zero) lemma conj_xor_distrib: "x \<^bold>\ (y \ z) = (x \<^bold>\ y) \ (x \<^bold>\ z)" proof - have *: "(x \<^bold>\ y \<^bold>\ \ z) \<^bold>\ (x \<^bold>\ \ y \<^bold>\ z) = (y \<^bold>\ x \<^bold>\ \ x) \<^bold>\ (z \<^bold>\ x \<^bold>\ \ x) \<^bold>\ (x \<^bold>\ y \<^bold>\ \ z) \<^bold>\ (x \<^bold>\ \ y \<^bold>\ z)" by (simp only: conj_cancel_right conj_zero_right disj_zero_left) then show "x \<^bold>\ (y \ z) = (x \<^bold>\ y) \ (x \<^bold>\ z)" by (simp (no_asm_use) only: xor_def de_Morgan_disj de_Morgan_conj double_compl conj_disj_distribs conj_ac disj_ac) qed lemma conj_xor_distrib2: "(y \ z) \<^bold>\ x = (y \<^bold>\ x) \ (z \<^bold>\ x)" by (simp add: conj.commute conj_xor_distrib) lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2 end end diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1116 +1,1116 @@ 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-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 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-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-Library" + 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-Library" + 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. " 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 AVL_Map RBT_Map Tree23_Map 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-ex" 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-Library" + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " 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-Library" + description " A new approach to verifying authentication protocols. " 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-Library" + options [print_mode = "no_brackets,no_type_brackets"] theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = "HOL-Library" + theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" + options [print_mode = "iff,no_brackets"] 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-Isar_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-Library" + 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-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-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. " theories Adhoc_Overloading_Examples 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 Coherent Commands Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Groebner_Examples Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Iff_Oracle Induction_Schema Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 "ML" MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Records Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Seq 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_Type + Word 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 Knaster_Tarski Peirce Drinker Cantor Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation First_Order_Logic Higher_Order_Logic 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-Library" + description " Verification of the SET Protocol. " theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" + description " Two-dimensional matrices and linear programming. " 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-Library" + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " 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-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 Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec 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 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-Library" + theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "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-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/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,1046 +1,368 @@ (* Author: Florian Haftmann, TUM *) section \Proof(s) of concept for algebraically founded lists of bits\ theory Bit_Lists imports - Main - "HOL-Library.Boolean_Algebra" -begin - -context ab_group_add + Bit_Operations begin -lemma minus_diff_commute: - "- b - a = - a - b" - by (simp only: diff_conv_add_uminus add.commute) - -end - - -subsection \Bit representations\ - -subsubsection \Mere 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" - - -subsubsection \Algebraic bit representation\ +subsection \Fragments of algebraic bit representations\ context comm_semiring_1 begin primrec radix_value :: "('b \ 'a) \ 'a \ 'b list \ 'a" where "radix_value f b [] = 0" | "radix_value f b (a # as) = f a + radix_value f b as * b" abbreviation (input) unsigned_of_bits :: "bool list \ 'a" where "unsigned_of_bits \ radix_value 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_nat 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)" + "unsigned_of_bits (take n bs) = Parity.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) qed lemma unsigned_of_bits_drop [simp]: - "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)" + "unsigned_of_bits (drop n bs) = Parity.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 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 \ Parity.take_bit n a = Parity.take_bit n b" + apply (induction n arbitrary: a b) + apply (auto elim!: evenE oddE) + apply (metis dvd_triv_right even_plus_one_iff) + apply (metis dvd_triv_right even_plus_one_iff) + 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) = Parity.take_bit n a" + by (induction n arbitrary: a) (simp_all add: ac_simps) + end -subsubsection \Instances\ +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 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 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)" + "of_bits (drop n bs) = Parity.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 qed qed end - -subsection \Syntactic bit operations\ +lemma unsigned_of_bits_eq_of_bits: + "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)" + by (simp add: of_bits_int_def) -class bit_operations = bit_representation + - fixes not :: "'a \ 'a" ("NOT") - and "and" :: "'a \ 'a \ 'a" (infixr "AND" 64) - and or :: "'a \ 'a \ 'a" (infixr "OR" 59) - and xor :: "'a \ 'a \ 'a" (infixr "XOR" 59) - and shift_left :: "'a \ nat \ 'a" (infixl "<<" 55) - and shift_right :: "'a \ nat \ 'a" (infixl ">>" 55) - assumes not_eq: "not = of_bits \ map Not \ bits_of" - and and_eq: "length bs = length cs \ - of_bits bs AND of_bits cs = of_bits (map2 (\) bs cs)" - and semilattice_and: "semilattice (AND)" - and or_eq: "length bs = length cs \ - of_bits bs OR of_bits cs = of_bits (map2 (\) bs cs)" - and semilattice_or: "semilattice (OR)" - and xor_eq: "length bs = length cs \ - of_bits bs XOR of_bits cs = of_bits (map2 (\) bs cs)" - and abel_semigroup_xor: "abel_semigroup (XOR)" - and shift_right_eq: "a << n = of_bits (replicate n False @ bits_of a)" - and shift_left_eq: "n < length (bits_of a) \ a >> n = of_bits (drop n (bits_of a))" +instantiation word :: (len) bit_representation begin -text \ - We want the bitwise operations to bind slightly weaker - than \+\ and \-\, but \~~\ to - bind slightly stronger than \*\. -\ +lift_definition bits_of_word :: "'a word \ bool list" + is "n_bits_of LENGTH('a)" + by (simp add: n_bits_of_eq_iff) -sublocale "and": semilattice "(AND)" - by (fact semilattice_and) +lift_definition of_bits_word :: "bool list \ 'a word" + is unsigned_of_bits . -sublocale or: semilattice "(OR)" - by (fact semilattice_or) - -sublocale xor: abel_semigroup "(XOR)" - by (fact abel_semigroup_xor) +instance proof + fix a :: "'a word" + show "of_bits (bits_of a) = a" + by transfer simp +qed end -subsubsection \Instance \<^typ>\nat\\ - -locale zip_nat = single: abel_semigroup f - for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) + - assumes end_of_bits: "\ False \<^bold>* False" -begin - -lemma False_P_imp: - "False \<^bold>* True \ P" if "False \<^bold>* P" - using that end_of_bits by (cases P) simp_all - -function F :: "nat \ nat \ nat" (infixl "\<^bold>\" 70) - where "m \<^bold>\ n = (if m = 0 \ n = 0 then 0 - else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2)" - by auto - -termination - by (relation "measure (case_prod (+))") auto - -lemma zero_left_eq: - "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" - by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) - -lemma zero_right_eq: - "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" - by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits) - -lemma simps [simp]: - "0 \<^bold>\ 0 = 0" - "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" - "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" - "m > 0 \ n > 0 \ m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" - by (simp_all only: zero_left_eq zero_right_eq) simp - -lemma rec: - "m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" - by (cases "m = 0 \ n = 0") (auto simp add: end_of_bits) - -declare F.simps [simp del] +subsection \Bit representations with bit operations\ -sublocale abel_semigroup F -proof - show "m \<^bold>\ n \<^bold>\ q = m \<^bold>\ (n \<^bold>\ q)" for m n q :: nat - proof (induction m arbitrary: n q rule: nat_bit_induct) - case zero - show ?case - by simp - next - case (even m) - with rec [of "2 * m"] rec [of _ q] show ?case - by (cases "even n") (auto dest: False_P_imp) - next - case (odd m) - with rec [of "Suc (2 * m)"] rec [of _ q] show ?case - by (cases "even n"; cases "even q") - (auto dest: False_P_imp simp add: ac_simps) - qed - show "m \<^bold>\ n = n \<^bold>\ m" for m n :: nat - proof (induction m arbitrary: n rule: nat_bit_induct) - case zero - show ?case - by (simp add: ac_simps) - next - case (even m) - with rec [of "2 * m" n] rec [of n "2 * m"] show ?case - by (simp add: ac_simps) - next - case (odd m) - with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case - by (simp add: ac_simps) - qed -qed +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 shift_bit_eq: "shift_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))" -lemma self [simp]: - "n \<^bold>\ n = of_bool (True \<^bold>* True) * n" - by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) +class ring_bit_representation = ring_bit_operations + semiring_bit_representation + + assumes not_eq: "not = of_bits \ map Not \ bits_of" -lemma even_iff [simp]: - "even (m \<^bold>\ n) \ \ (odd m \<^bold>* odd n)" -proof (induction m arbitrary: n rule: nat_bit_induct) - case zero - show ?case - by (cases "even n") (simp_all add: end_of_bits) -next - case (even m) - then show ?case - by (simp add: rec [of "2 * m"]) -next - case (odd m) - then show ?case - by (simp add: rec [of "Suc (2 * m)"]) -qed + +context zip_nat +begin lemma of_bits: "of_bits bs \<^bold>\ of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: nat)" if "length bs = length cs" for bs cs using that proof (induction bs cs rule: list_induct2) case Nil then show ?case by simp next case (Cons b bs c cs) then show ?case by (cases "of_bits bs = (0::nat) \ of_bits cs = (0::nat)") (auto simp add: ac_simps end_of_bits rec [of "Suc 0"]) qed end -instantiation nat :: bit_operations -begin - -definition not_nat :: "nat \ nat" - where "not_nat = of_bits \ map Not \ bits_of" - -global_interpretation and_nat: zip_nat "(\)" - defines and_nat = and_nat.F - by standard auto - -global_interpretation and_nat: semilattice "(AND) :: nat \ nat \ nat" -proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard) - show "n AND n = n" for n :: nat - by (simp add: and_nat.self) -qed - -declare and_nat.simps [simp] \ \inconsistent declaration handling by - \global_interpretation\ in \instantiation\\ - -lemma zero_nat_and_eq [simp]: - "0 AND n = 0" for n :: nat - by simp - -lemma and_zero_nat_eq [simp]: - "n AND 0 = 0" for n :: nat - by simp - -global_interpretation or_nat: zip_nat "(\)" - defines or_nat = or_nat.F - by standard auto - -global_interpretation or_nat: semilattice "(OR) :: nat \ nat \ nat" -proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard) - show "n OR n = n" for n :: nat - by (simp add: or_nat.self) -qed - -declare or_nat.simps [simp] \ \inconsistent declaration handling by - \global_interpretation\ in \instantiation\\ - -lemma zero_nat_or_eq [simp]: - "0 OR n = n" for n :: nat - by simp - -lemma or_zero_nat_eq [simp]: - "n OR 0 = n" for n :: nat - by simp - -global_interpretation xor_nat: zip_nat "(\)" - defines xor_nat = xor_nat.F - by standard auto - -declare xor_nat.simps [simp] \ \inconsistent declaration handling by - \global_interpretation\ in \instantiation\\ - -lemma zero_nat_xor_eq [simp]: - "0 XOR n = n" for n :: nat - by simp - -lemma xor_zero_nat_eq [simp]: - "n XOR 0 = n" for n :: nat - by simp - -definition shift_left_nat :: "nat \ nat \ nat" - where [simp]: "m << n = push_bit n m" for m :: nat - -definition shift_right_nat :: "nat \ nat \ nat" - where [simp]: "m >> n = drop_bit n m" for m :: nat +instance nat :: semiring_bit_representation + apply standard + apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits) + apply (simp_all add: drop_bit_eq_div Parity.drop_bit_eq_div shift_bit_eq_mult push_bit_eq_mult) + done -instance proof - show "semilattice ((AND) :: nat \ _)" - by (fact and_nat.semilattice_axioms) - show "semilattice ((OR):: nat \ _)" - by (fact or_nat.semilattice_axioms) - show "abel_semigroup ((XOR):: nat \ _)" - by (fact xor_nat.abel_semigroup_axioms) - show "(not :: nat \ _) = of_bits \ map Not \ bits_of" - by (fact not_nat_def) - show "of_bits bs AND of_bits cs = (of_bits (map2 (\) bs cs) :: nat)" - if "length bs = length cs" for bs cs - using that by (fact and_nat.of_bits) - show "of_bits bs OR of_bits cs = (of_bits (map2 (\) bs cs) :: nat)" - if "length bs = length cs" for bs cs - using that by (fact or_nat.of_bits) - show "of_bits bs XOR of_bits cs = (of_bits (map2 (\) bs cs) :: nat)" - if "length bs = length cs" for bs cs - using that by (fact xor_nat.of_bits) - show "m << n = of_bits (replicate n False @ bits_of m)" - for m n :: nat - by simp - show "m >> n = of_bits (drop n (bits_of m))" - for m n :: nat - by simp -qed - -end - -global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat" - by standard simp - -global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat" - by standard simp - -lemma not_nat_simps [simp]: - "NOT 0 = (0::nat)" - "n > 0 \ NOT n = of_bool (even n) + 2 * NOT (n div 2)" for n :: nat - by (simp_all add: not_eq) - -lemma not_1_nat [simp]: - "NOT 1 = (0::nat)" - by simp - -lemma not_Suc_0 [simp]: - "NOT (Suc 0) = (0::nat)" - by simp - -lemma Suc_0_and_eq [simp]: - "Suc 0 AND n = n mod 2" - by (cases n) auto - -lemma and_Suc_0_eq [simp]: - "n AND Suc 0 = n mod 2" - using Suc_0_and_eq [of n] by (simp add: ac_simps) - -lemma Suc_0_or_eq [simp]: - "Suc 0 OR n = n + of_bool (even n)" - by (cases n) (simp_all add: ac_simps) - -lemma or_Suc_0_eq [simp]: - "n OR Suc 0 = n + of_bool (even n)" - using Suc_0_or_eq [of n] by (simp add: ac_simps) - -lemma Suc_0_xor_eq [simp]: - "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)" - by (cases n) (simp_all add: ac_simps) - -lemma xor_Suc_0_eq [simp]: - "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)" - using Suc_0_xor_eq [of n] by (simp add: ac_simps) - - -subsubsection \Instance \<^typ>\int\\ - -abbreviation (input) complement :: "int \ int" - where "complement k \ - k - 1" - -lemma complement_half: - "complement (k * 2) div 2 = complement k" - by simp - -lemma complement_div_2: - "complement (k div 2) = complement k div 2" - by linarith - -locale zip_int = single: abel_semigroup f - for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) +context zip_int begin -lemma False_False_imp_True_True: - "True \<^bold>* True" if "False \<^bold>* False" -proof (rule ccontr) - assume "\ True \<^bold>* True" - with that show False - using single.assoc [of False True True] - by (cases "False \<^bold>* True") simp_all -qed - -function F :: "int \ int \ int" (infixl "\<^bold>\" 70) - where "k \<^bold>\ l = (if k \ {0, - 1} \ l \ {0, - 1} - then - of_bool (odd k \<^bold>* odd l) - else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2)" - by auto - -termination - by (relation "measure (\(k, l). nat (\k\ + \l\))") auto - -lemma zero_left_eq: - "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ l - | (True, False) \ complement l - | (True, True) \ - 1)" - by (induction l rule: int_bit_induct) - (simp_all split: bool.split) - -lemma minus_left_eq: - "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ l - | (True, False) \ complement l - | (True, True) \ - 1)" - by (induction l rule: int_bit_induct) - (simp_all split: bool.split) - -lemma zero_right_eq: - "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ k - | (True, False) \ complement k - | (True, True) \ - 1)" - by (induction k rule: int_bit_induct) - (simp_all add: ac_simps split: bool.split) - -lemma minus_right_eq: - "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ k - | (True, False) \ complement k - | (True, True) \ - 1)" - by (induction k rule: int_bit_induct) - (simp_all add: ac_simps split: bool.split) - -lemma simps [simp]: - "0 \<^bold>\ 0 = - of_bool (False \<^bold>* False)" - "- 1 \<^bold>\ 0 = - of_bool (True \<^bold>* False)" - "0 \<^bold>\ - 1 = - of_bool (False \<^bold>* True)" - "- 1 \<^bold>\ - 1 = - of_bool (True \<^bold>* True)" - "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ l - | (True, False) \ complement l - | (True, True) \ - 1)" - "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ l - | (True, False) \ complement l - | (True, True) \ - 1)" - "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ k - | (True, False) \ complement k - | (True, True) \ - 1)" - "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ k - | (True, False) \ complement k - | (True, True) \ - 1)" - "k \ 0 \ k \ - 1 \ l \ 0 \ l \ - 1 - \ k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" - by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp) - -declare F.simps [simp del] - -lemma rec: - "k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" - by (cases "k \ {0, - 1} \ l \ {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split) - -sublocale abel_semigroup F -proof - show "k \<^bold>\ l \<^bold>\ r = k \<^bold>\ (l \<^bold>\ r)" for k l r :: int - proof (induction k arbitrary: l r rule: int_bit_induct) - case zero - have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "False \<^bold>* False" "\ False \<^bold>* True" - proof (induction l arbitrary: r rule: int_bit_induct) - case zero - from that show ?case - by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - next - case minus - from that show ?case - by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - next - case (even l) - with that rec [of _ r] show ?case - by (cases "even r") - (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) - next - case (odd l) - moreover have "- l - 1 = - 1 - l" - by simp - ultimately show ?case - using that rec [of _ r] - by (cases "even r") - (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - qed - then show ?case - by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - next - case minus - have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "\ True \<^bold>* True" "False \<^bold>* True" - proof (induction l arbitrary: r rule: int_bit_induct) - case zero - from that show ?case - by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - next - case minus - from that show ?case - by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - next - case (even l) - with that rec [of _ r] show ?case - by (cases "even r") - (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) - next - case (odd l) - moreover have "- l - 1 = - 1 - l" - by simp - ultimately show ?case - using that rec [of _ r] - by (cases "even r") - (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - qed - then show ?case - by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) - next - case (even k) - with rec [of "k * 2"] rec [of _ r] show ?case - by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) - next - case (odd k) - with rec [of "1 + k * 2"] rec [of _ r] show ?case - by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) - qed - show "k \<^bold>\ l = l \<^bold>\ k" for k l :: int - proof (induction k arbitrary: l rule: int_bit_induct) - case zero - show ?case - by simp - next - case minus - show ?case - by simp - next - case (even k) - with rec [of "k * 2" l] rec [of l "k * 2"] show ?case - by (simp add: ac_simps) - next - case (odd k) - with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case - by (simp add: ac_simps) - qed -qed - -lemma self [simp]: - "k \<^bold>\ k = (case (False \<^bold>* False, True \<^bold>* True) - of (False, False) \ 0 - | (False, True) \ k - | (True, True) \ - 1)" - by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split) - -lemma even_iff [simp]: - "even (k \<^bold>\ l) \ \ (odd k \<^bold>* odd l)" -proof (induction k arbitrary: l rule: int_bit_induct) - case zero - show ?case - by (cases "even l") (simp_all split: bool.splits) -next - case minus - show ?case - by (cases "even l") (simp_all split: bool.splits) -next - case (even k) - then show ?case - by (simp add: rec [of "k * 2"]) -next - case (odd k) - then show ?case - by (simp add: rec [of "1 + k * 2"]) -qed - lemma of_bits: "of_bits bs \<^bold>\ of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)" if "length bs = length cs" and "\ False \<^bold>* False" for bs cs using \length bs = length cs\ proof (induction bs cs rule: list_induct2) case Nil then show ?case using \\ False \<^bold>* False\ by (auto simp add: False_False_imp_True_True split: bool.splits) next case (Cons b bs c cs) show ?case proof (cases "bs = []") case True with Cons show ?thesis using \\ False \<^bold>* False\ by (cases b; cases c) (auto simp add: ac_simps split: bool.splits) next case False with Cons.hyps have "cs \ []" by auto with \bs \ []\ have "map2 (\<^bold>*) bs cs \ []" by (simp add: zip_eq_Nil_iff) from \bs \ []\ \cs \ []\ \map2 (\<^bold>*) bs cs \ []\ Cons show ?thesis by (cases b; cases c) (auto simp add: \\ False \<^bold>* False\ ac_simps rec [of "of_bits bs * 2"] rec [of "of_bits cs * 2"] rec [of "1 + of_bits bs * 2"]) qed qed end -instantiation int :: bit_operations -begin - -definition not_int :: "int \ int" - where "not_int = complement" - -global_interpretation and_int: zip_int "(\)" - defines and_int = and_int.F - by standard - -declare and_int.simps [simp] \ \inconsistent declaration handling by - \global_interpretation\ in \instantiation\\ - -global_interpretation and_int: semilattice "(AND) :: int \ int \ int" -proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard) - show "k AND k = k" for k :: int - by (simp add: and_int.self) -qed - -lemma zero_int_and_eq [simp]: - "0 AND k = 0" for k :: int - by simp - -lemma and_zero_int_eq [simp]: - "k AND 0 = 0" for k :: int - by simp - -lemma minus_int_and_eq [simp]: - "- 1 AND k = k" for k :: int - by simp - -lemma and_minus_int_eq [simp]: - "k AND - 1 = k" for k :: int - by simp - -global_interpretation or_int: zip_int "(\)" - defines or_int = or_int.F - by standard - -declare or_int.simps [simp] \ \inconsistent declaration handling by - \global_interpretation\ in \instantiation\\ - -global_interpretation or_int: semilattice "(OR) :: int \ int \ int" -proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard) - show "k OR k = k" for k :: int - by (simp add: or_int.self) -qed - -lemma zero_int_or_eq [simp]: - "0 OR k = k" for k :: int - by simp - -lemma and_zero_or_eq [simp]: - "k OR 0 = k" for k :: int - by simp - -lemma minus_int_or_eq [simp]: - "- 1 OR k = - 1" for k :: int - by simp - -lemma or_minus_int_eq [simp]: - "k OR - 1 = - 1" for k :: int - by simp - -global_interpretation xor_int: zip_int "(\)" - defines xor_int = xor_int.F - by standard - -declare xor_int.simps [simp] \ \inconsistent declaration handling by - \global_interpretation\ in \instantiation\\ - -lemma zero_int_xor_eq [simp]: - "0 XOR k = k" for k :: int - by simp - -lemma and_zero_xor_eq [simp]: - "k XOR 0 = k" for k :: int - by simp - -lemma minus_int_xor_eq [simp]: - "- 1 XOR k = complement k" for k :: int - by simp - -lemma xor_minus_int_eq [simp]: - "k XOR - 1 = complement k" for k :: int - by simp - -definition shift_left_int :: "int \ nat \ int" - where [simp]: "k << n = push_bit n k" for k :: int - -definition shift_right_int :: "int \ nat \ int" - where [simp]: "k >> n = drop_bit n k" for k :: int - -instance proof - show "semilattice ((AND) :: int \ _)" - by (fact and_int.semilattice_axioms) - show "semilattice ((OR) :: int \ _)" - by (fact or_int.semilattice_axioms) - show "abel_semigroup ((XOR) :: int \ _)" - by (fact xor_int.abel_semigroup_axioms) +instance int :: ring_bit_representation +proof 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 - show "of_bits bs AND of_bits cs = (of_bits (map2 (\) bs cs) :: int)" - if "length bs = length cs" for bs cs - using that by (rule and_int.of_bits) simp - show "of_bits bs OR of_bits cs = (of_bits (map2 (\) bs cs) :: int)" - if "length bs = length cs" for bs cs - using that by (rule or_int.of_bits) simp - show "of_bits bs XOR of_bits cs = (of_bits (map2 (\) bs cs) :: int)" - if "length bs = length cs" for bs cs - using that by (rule xor_int.of_bits) simp - show "k << n = of_bits (replicate n False @ bits_of k)" + show "shift_bit n k = of_bits (replicate n False @ bits_of k)" for k :: int and n :: nat - by (cases "n = 0") simp_all - show "k >> n = of_bits (drop n (bits_of k))" - if "n < length (bits_of k)" - for k :: int and n :: nat - using that by simp -qed + by (cases "n = 0") (simp_all add: shift_bit_eq_push_bit) +qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits + drop_bit_eq_drop_bit) end - -global_interpretation and_int: semilattice_neutr "(AND)" "- 1 :: int" - by standard simp - -global_interpretation or_int: semilattice_neutr "(OR)" "0 :: int" - by standard simp - -global_interpretation xor_int: comm_monoid "(XOR)" "0 :: int" - by standard simp - -lemma not_int_simps [simp]: - "NOT 0 = (- 1 :: int)" - "NOT (- 1) = (0 :: int)" - "k \ 0 \ k \ - 1 \ NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int - by (auto simp add: not_int_def elim: oddE) - -lemma not_one_int [simp]: - "NOT 1 = (- 2 :: int)" - by simp - -lemma even_not_iff [simp]: - "even (NOT k) \ odd k" - for k :: int - by (simp add: not_int_def) - -lemma not_div_2: - "NOT k div 2 = NOT (k div 2)" - for k :: int - by (simp add: complement_div_2 not_int_def) - -lemma one_and_int_eq [simp]: - "1 AND k = k mod 2" for k :: int - using and_int.rec [of 1] by (simp add: mod2_eq_if) - -lemma and_one_int_eq [simp]: - "k AND 1 = k mod 2" for k :: int - using one_and_int_eq [of 1] by (simp add: ac_simps) - -lemma one_or_int_eq [simp]: - "1 OR k = k + of_bool (even k)" for k :: int - using or_int.rec [of 1] by (auto elim: oddE) - -lemma or_one_int_eq [simp]: - "k OR 1 = k + of_bool (even k)" for k :: int - using one_or_int_eq [of k] by (simp add: ac_simps) - -lemma one_xor_int_eq [simp]: - "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int - using xor_int.rec [of 1] by (auto elim: oddE) - -lemma xor_one_int_eq [simp]: - "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int - using one_xor_int_eq [of k] by (simp add: ac_simps) - -global_interpretation bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int" - rewrites "bit_int.xor = ((XOR) :: int \ _)" -proof - - interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int" - proof - show "k AND (l OR r) = k AND l OR k AND r" - for k l r :: int - proof (induction k arbitrary: l r rule: int_bit_induct) - case zero - show ?case - by simp - next - case minus - show ?case - by simp - next - case (even k) - then show ?case by (simp add: and_int.rec [of "k * 2"] - or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l]) - next - case (odd k) - then show ?case by (simp add: and_int.rec [of "1 + k * 2"] - or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l]) - qed - show "k OR l AND r = (k OR l) AND (k OR r)" - for k l r :: int - proof (induction k arbitrary: l r rule: int_bit_induct) - case zero - then show ?case - by simp - next - case minus - then show ?case - by simp - next - case (even k) - then show ?case by (simp add: or_int.rec [of "k * 2"] - and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l]) - next - case (odd k) - then show ?case by (simp add: or_int.rec [of "1 + k * 2"] - and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l]) - qed - show "k AND NOT k = 0" for k :: int - by (induction k rule: int_bit_induct) - (simp_all add: not_int_def complement_half minus_diff_commute [of 1]) - show "k OR NOT k = - 1" for k :: int - by (induction k rule: int_bit_induct) - (simp_all add: not_int_def complement_half minus_diff_commute [of 1]) - qed simp_all - show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)" - by (fact bit_int.boolean_algebra_axioms) - show "bit_int.xor = ((XOR) :: int \ _)" - proof (rule ext)+ - fix k l :: int - have "k XOR l = k AND NOT l OR NOT k AND l" - proof (induction k arbitrary: l rule: int_bit_induct) - case zero - show ?case - by simp - next - case minus - show ?case - by (simp add: not_int_def) - next - case (even k) - then show ?case - by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"] - or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2) - (simp add: and_int.rec [of _ l]) - next - case (odd k) - then show ?case - by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"] - or_int.rec [of _ "2 * NOT k AND l"] not_div_2) - (simp add: and_int.rec [of _ l]) - qed - then show "bit_int.xor k l = k XOR l" - by (simp add: bit_int.xor_def) - qed -qed - -end diff --git a/src/HOL/ex/Bit_Operations.thy b/src/HOL/ex/Bit_Operations.thy new file mode 100644 --- /dev/null +++ b/src/HOL/ex/Bit_Operations.thy @@ -0,0 +1,1033 @@ +(* Author: Florian Haftmann, TUM +*) + +section \Proof of concept for purely algebraically founded lists of bits\ + +theory Bit_Operations + imports + "HOL-Library.Boolean_Algebra" + Word +begin + +hide_const (open) drop_bit take_bit + +subsection \Algebraic structures with bits\ + +class semiring_bits = semiring_parity + + assumes bit_split_eq: \\a. of_bool (odd a) + 2 * (a div 2) = a\ + and bit_eq_rec: \\a b. a = b \ (even a = even b) \ a div 2 = b div 2\ + and bit_induct [case_names stable rec]: + \(\a. a div 2 = a \ P a) + \ (\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)) + \ P a\ + + +subsubsection \Instance \<^typ>\nat\\ + +instance nat :: semiring_bits +proof + show \of_bool (odd n) + 2 * (n div 2) = n\ + for n :: nat + by simp + show \m = n \ (even m \ even n) \ m div 2 = n div 2\ + for m n :: nat + by (auto dest: odd_two_times_div_two_succ) + show \P n\ if stable: \\n. n div 2 = n \ P n\ + and rec: \\n b. P n \ (of_bool b + 2 * n) div 2 = n \ P (of_bool b + 2 * n)\ + for P and n :: nat + proof (induction n rule: nat_bit_induct) + case zero + from stable [of 0] show ?case + by simp + next + case (even n) + with rec [of n False] show ?case + by simp + next + case (odd n) + with rec [of n True] show ?case + by simp + qed +qed + + +subsubsection \Instance \<^typ>\int\\ + +instance int :: semiring_bits +proof + show \of_bool (odd k) + 2 * (k div 2) = k\ + for k :: int + by (auto elim: oddE) + show \k = l \ (even k \ even l) \ k div 2 = l div 2\ + for k l :: int + by (auto dest: odd_two_times_div_two_succ) + show \P k\ if stable: \\k. k div 2 = k \ P k\ + and rec: \\k b. P k \ (of_bool b + 2 * k) div 2 = k \ P (of_bool b + 2 * k)\ + for P and k :: int + proof (induction k rule: int_bit_induct) + case zero + from stable [of 0] show ?case + by simp + next + case minus + from stable [of \- 1\] show ?case + by simp + next + case (even k) + with rec [of k False] show ?case + by (simp add: ac_simps) + next + case (odd k) + with rec [of k True] show ?case + by (simp add: ac_simps) + qed +qed + + +subsubsection \Instance \<^typ>\'a word\\ + +instance word :: (len) semiring_bits +proof + show \of_bool (odd a) + 2 * (a div 2) = a\ + for a :: \'a word\ + apply (cases \even a\; simp, transfer; cases rule: length_cases [where ?'a = 'a]) + apply auto + apply (auto simp add: take_bit_eq_mod) + apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod) + done + show \a = b \ (even a \ even b) \ a div 2 = b div 2\ + for a b :: \'a word\ + apply transfer + apply (cases rule: length_cases [where ?'a = 'a]) + apply auto + apply (metis even_take_bit_eq len_not_eq_0) + apply (metis even_take_bit_eq len_not_eq_0) + apply (metis (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus) + apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod) + done + show \P a\ if stable: \\a. a div 2 = a \ P a\ + and rec: \\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)\ + for P and a :: \'a word\ + proof (induction a rule: word_bit_induct) + case zero + from stable [of 0] show ?case + by simp + next + case (even a) + with rec [of a False] show ?case + using bit_word_half_eq [of a False] by (simp add: ac_simps) + next + case (odd a) + with rec [of a True] show ?case + using bit_word_half_eq [of a True] by (simp add: ac_simps) + qed +qed + + +subsection \Bit shifts in suitable algebraic structures\ + +class semiring_bit_shifts = semiring_bits + + fixes shift_bit :: \nat \ 'a \ 'a\ + assumes shift_bit_eq_mult: \shift_bit n a = a * 2 ^ n\ + fixes drop_bit :: \nat \ 'a \ 'a\ + assumes drop_bit_eq_div: \drop_bit n a = a div 2 ^ n\ +begin + +definition take_bit :: \nat \ 'a \ 'a\ + where take_bit_eq_mod: \take_bit n a = a mod 2 ^ n\ + +text \ + Logically, \<^const>\shift_bit\, + \<^const>\drop_bit\ and \<^const>\take_bit\ are just aliases; having them + as separate operations makes proofs easier, otherwise proof automation + would fiddle with concrete expressions \<^term>\2 ^ n\ in a way obfuscating the basic + algebraic relationships between those operations; having + \<^const>\push_bit\ and \<^const>\drop_bit\ as definitional class operations + takes into account that specific instances of these can be implemented + differently wrt. code generation. +\ + +end + +subsubsection \Instance \<^typ>\nat\\ + +instantiation nat :: semiring_bit_shifts +begin + +definition shift_bit_nat :: \nat \ nat \ nat\ + where \shift_bit_nat n m = m * 2 ^ n\ + +definition drop_bit_nat :: \nat \ nat \ nat\ + where \drop_bit_nat n m = m div 2 ^ n\ + +instance proof + show \shift_bit n m = m * 2 ^ n\ for n m :: nat + by (simp add: shift_bit_nat_def) + show \drop_bit n m = m div 2 ^ n\ for n m :: nat + by (simp add: drop_bit_nat_def) +qed + +end + + +subsubsection \Instance \<^typ>\int\\ + +instantiation int :: semiring_bit_shifts +begin + +definition shift_bit_int :: \nat \ int \ int\ + where \shift_bit_int n k = k * 2 ^ n\ + +definition drop_bit_int :: \nat \ int \ int\ + where \drop_bit_int n k = k div 2 ^ n\ + +instance proof + show \shift_bit n k = k * 2 ^ n\ for n :: nat and k :: int + by (simp add: shift_bit_int_def) + show \drop_bit n k = k div 2 ^ n\ for n :: nat and k :: int + by (simp add: drop_bit_int_def) +qed + +end + +lemma shift_bit_eq_push_bit: + \shift_bit = (push_bit :: nat \ int \ int)\ + by (simp add: fun_eq_iff push_bit_eq_mult shift_bit_eq_mult) + +lemma drop_bit_eq_drop_bit: + \drop_bit = (Parity.drop_bit :: nat \ int \ int)\ + by (simp add: fun_eq_iff drop_bit_eq_div Parity.drop_bit_eq_div) + +lemma take_bit_eq_take_bit: + \take_bit = (Parity.take_bit :: nat \ int \ int)\ + by (simp add: fun_eq_iff take_bit_eq_mod Parity.take_bit_eq_mod) + + +subsubsection \Instance \<^typ>\'a word\\ + +instantiation word :: (len) semiring_bit_shifts +begin + +lift_definition shift_bit_word :: \nat \ 'a word \ 'a word\ + is shift_bit +proof - + show \Parity.take_bit LENGTH('a) (shift_bit n k) = Parity.take_bit LENGTH('a) (shift_bit n l)\ + if \Parity.take_bit LENGTH('a) k = Parity.take_bit LENGTH('a) l\ for k l :: int and n :: nat + proof - + from that + have \Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) k) + = Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) l)\ + by simp + moreover have \min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\ + by simp + ultimately show ?thesis + by (simp add: shift_bit_eq_push_bit take_bit_push_bit) + qed +qed + +lift_definition drop_bit_word :: \nat \ 'a word \ 'a word\ + is \\n. drop_bit n \ take_bit LENGTH('a)\ + by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod) + +instance proof + show \shift_bit n a = a * 2 ^ n\ for n :: nat and a :: "'a word" + by transfer (simp add: shift_bit_eq_mult) + show \drop_bit n a = a div 2 ^ n\ for n :: nat and a :: "'a word" + proof (cases \n < LENGTH('a)\) + case True + then show ?thesis + by transfer + (simp add: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div) + next + case False + then obtain m where n: \n = LENGTH('a) + m\ + by (auto simp add: not_less dest: le_Suc_ex) + then show ?thesis + by transfer + (simp add: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq) + qed +qed + +end + + +subsection \Bit operations in suitable algebraic structures\ + +class semiring_bit_operations = semiring_bit_shifts + + fixes "and" :: "'a \ 'a \ 'a" (infixr "AND" 64) + and or :: "'a \ 'a \ 'a" (infixr "OR" 59) + and xor :: "'a \ 'a \ 'a" (infixr "XOR" 59) +begin + +text \ + We want the bitwise operations to bind slightly weaker + than \+\ and \-\, but \~~\ to + bind slightly stronger than \*\. + For the sake of code generation + the operations \<^const>\and\, \<^const>\or\ and \<^const>\xor\ + are specified as definitional class operations. + +\ + +definition bit :: \'a \ nat \ bool\ + where \bit a n \ odd (drop_bit n a)\ + +definition map_bit :: \nat \ (bool \ bool) \ 'a \ 'a\ + where \map_bit n f a = take_bit n a + shift_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\ + +definition set_bit :: \nat \ 'a \ 'a\ + where \set_bit n = map_bit n top\ + +definition unset_bit :: \nat \ 'a \ 'a\ + where \unset_bit n = map_bit n bot\ + +definition flip_bit :: \nat \ 'a \ 'a\ + where \flip_bit n = map_bit n Not\ + +text \ + The logical core are \<^const>\bit\ and \<^const>\map_bit\; having + <^const>\set_bit\, \<^const>\unset_bit\ and \<^const>\flip_bit\ as separate + operations allows to implement them using bit masks later. +\ + +end + +class ring_bit_operations = semiring_bit_operations + ring_parity + + fixes not :: \'a \ 'a\ (\NOT\) + assumes boolean_algebra: \boolean_algebra (AND) (OR) NOT 0 (- 1)\ + and boolean_algebra_xor_eq: \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ +begin + +sublocale bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ + rewrites \bit.xor = (XOR)\ +proof - + interpret bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ + by (fact boolean_algebra) + show \boolean_algebra (AND) (OR) NOT 0 (- 1)\ + by standard + show \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ + by (fact boolean_algebra_xor_eq) +qed + +text \ + For the sake of code generation \<^const>\not\ is specified as + definitional class operation. Note that \<^const>\not\ has no + sensible definition for unlimited but only positive bit strings + (type \<^typ>\nat\). +\ + +end + + +subsubsection \Instance \<^typ>\nat\\ + +locale zip_nat = single: abel_semigroup f + for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) + + assumes end_of_bits: "\ False \<^bold>* False" +begin + +lemma False_P_imp: + "False \<^bold>* True \ P" if "False \<^bold>* P" + using that end_of_bits by (cases P) simp_all + +function F :: "nat \ nat \ nat" (infixl "\<^bold>\" 70) + where "m \<^bold>\ n = (if m = 0 \ n = 0 then 0 + else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2)" + by auto + +termination + by (relation "measure (case_prod (+))") auto + +lemma zero_left_eq: + "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" + by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) + +lemma zero_right_eq: + "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" + by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits) + +lemma simps [simp]: + "0 \<^bold>\ 0 = 0" + "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" + "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" + "m > 0 \ n > 0 \ m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" + by (simp_all only: zero_left_eq zero_right_eq) simp + +lemma rec: + "m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" + by (cases "m = 0 \ n = 0") (auto simp add: end_of_bits) + +declare F.simps [simp del] + +sublocale abel_semigroup F +proof + show "m \<^bold>\ n \<^bold>\ q = m \<^bold>\ (n \<^bold>\ q)" for m n q :: nat + proof (induction m arbitrary: n q rule: nat_bit_induct) + case zero + show ?case + by simp + next + case (even m) + with rec [of "2 * m"] rec [of _ q] show ?case + by (cases "even n") (auto dest: False_P_imp) + next + case (odd m) + with rec [of "Suc (2 * m)"] rec [of _ q] show ?case + by (cases "even n"; cases "even q") + (auto dest: False_P_imp simp add: ac_simps) + qed + show "m \<^bold>\ n = n \<^bold>\ m" for m n :: nat + proof (induction m arbitrary: n rule: nat_bit_induct) + case zero + show ?case + by (simp add: ac_simps) + next + case (even m) + with rec [of "2 * m" n] rec [of n "2 * m"] show ?case + by (simp add: ac_simps) + next + case (odd m) + with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case + by (simp add: ac_simps) + qed +qed + +lemma self [simp]: + "n \<^bold>\ n = of_bool (True \<^bold>* True) * n" + by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) + +lemma even_iff [simp]: + "even (m \<^bold>\ n) \ \ (odd m \<^bold>* odd n)" +proof (induction m arbitrary: n rule: nat_bit_induct) + case zero + show ?case + by (cases "even n") (simp_all add: end_of_bits) +next + case (even m) + then show ?case + by (simp add: rec [of "2 * m"]) +next + case (odd m) + then show ?case + by (simp add: rec [of "Suc (2 * m)"]) +qed + +end + +instantiation nat :: semiring_bit_operations +begin + +global_interpretation and_nat: zip_nat "(\)" + defines and_nat = and_nat.F + by standard auto + +global_interpretation and_nat: semilattice "(AND) :: nat \ nat \ nat" +proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard) + show "n AND n = n" for n :: nat + by (simp add: and_nat.self) +qed + +declare and_nat.simps [simp] \ \inconsistent declaration handling by + \global_interpretation\ in \instantiation\\ + +lemma zero_nat_and_eq [simp]: + "0 AND n = 0" for n :: nat + by simp + +lemma and_zero_nat_eq [simp]: + "n AND 0 = 0" for n :: nat + by simp + +global_interpretation or_nat: zip_nat "(\)" + defines or_nat = or_nat.F + by standard auto + +global_interpretation or_nat: semilattice "(OR) :: nat \ nat \ nat" +proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard) + show "n OR n = n" for n :: nat + by (simp add: or_nat.self) +qed + +declare or_nat.simps [simp] \ \inconsistent declaration handling by + \global_interpretation\ in \instantiation\\ + +lemma zero_nat_or_eq [simp]: + "0 OR n = n" for n :: nat + by simp + +lemma or_zero_nat_eq [simp]: + "n OR 0 = n" for n :: nat + by simp + +global_interpretation xor_nat: zip_nat "(\)" + defines xor_nat = xor_nat.F + by standard auto + +declare xor_nat.simps [simp] \ \inconsistent declaration handling by + \global_interpretation\ in \instantiation\\ + +lemma zero_nat_xor_eq [simp]: + "0 XOR n = n" for n :: nat + by simp + +lemma xor_zero_nat_eq [simp]: + "n XOR 0 = n" for n :: nat + by simp + +instance .. + +end + +global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat" + by standard simp + +global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat" + by standard simp + +lemma Suc_0_and_eq [simp]: + "Suc 0 AND n = n mod 2" + by (cases n) auto + +lemma and_Suc_0_eq [simp]: + "n AND Suc 0 = n mod 2" + using Suc_0_and_eq [of n] by (simp add: ac_simps) + +lemma Suc_0_or_eq [simp]: + "Suc 0 OR n = n + of_bool (even n)" + by (cases n) (simp_all add: ac_simps) + +lemma or_Suc_0_eq [simp]: + "n OR Suc 0 = n + of_bool (even n)" + using Suc_0_or_eq [of n] by (simp add: ac_simps) + +lemma Suc_0_xor_eq [simp]: + "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)" + by (cases n) (simp_all add: ac_simps) + +lemma xor_Suc_0_eq [simp]: + "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)" + using Suc_0_xor_eq [of n] by (simp add: ac_simps) + + +subsubsection \Instance \<^typ>\int\\ + +abbreviation (input) complement :: "int \ int" + where "complement k \ - k - 1" + +lemma complement_half: + "complement (k * 2) div 2 = complement k" + by simp + +lemma complement_div_2: + "complement (k div 2) = complement k div 2" + by linarith + +locale zip_int = single: abel_semigroup f + for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) +begin + +lemma False_False_imp_True_True: + "True \<^bold>* True" if "False \<^bold>* False" +proof (rule ccontr) + assume "\ True \<^bold>* True" + with that show False + using single.assoc [of False True True] + by (cases "False \<^bold>* True") simp_all +qed + +function F :: "int \ int \ int" (infixl "\<^bold>\" 70) + where "k \<^bold>\ l = (if k \ {0, - 1} \ l \ {0, - 1} + then - of_bool (odd k \<^bold>* odd l) + else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2)" + by auto + +termination + by (relation "measure (\(k, l). nat (\k\ + \l\))") auto + +lemma zero_left_eq: + "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ l + | (True, False) \ complement l + | (True, True) \ - 1)" + by (induction l rule: int_bit_induct) + (simp_all split: bool.split) + +lemma minus_left_eq: + "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ l + | (True, False) \ complement l + | (True, True) \ - 1)" + by (induction l rule: int_bit_induct) + (simp_all split: bool.split) + +lemma zero_right_eq: + "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ k + | (True, False) \ complement k + | (True, True) \ - 1)" + by (induction k rule: int_bit_induct) + (simp_all add: ac_simps split: bool.split) + +lemma minus_right_eq: + "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ k + | (True, False) \ complement k + | (True, True) \ - 1)" + by (induction k rule: int_bit_induct) + (simp_all add: ac_simps split: bool.split) + +lemma simps [simp]: + "0 \<^bold>\ 0 = - of_bool (False \<^bold>* False)" + "- 1 \<^bold>\ 0 = - of_bool (True \<^bold>* False)" + "0 \<^bold>\ - 1 = - of_bool (False \<^bold>* True)" + "- 1 \<^bold>\ - 1 = - of_bool (True \<^bold>* True)" + "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ l + | (True, False) \ complement l + | (True, True) \ - 1)" + "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ l + | (True, False) \ complement l + | (True, True) \ - 1)" + "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ k + | (True, False) \ complement k + | (True, True) \ - 1)" + "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ k + | (True, False) \ complement k + | (True, True) \ - 1)" + "k \ 0 \ k \ - 1 \ l \ 0 \ l \ - 1 + \ k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" + by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp) + +declare F.simps [simp del] + +lemma rec: + "k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" + by (cases "k \ {0, - 1} \ l \ {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split) + +sublocale abel_semigroup F +proof + show "k \<^bold>\ l \<^bold>\ r = k \<^bold>\ (l \<^bold>\ r)" for k l r :: int + proof (induction k arbitrary: l r rule: int_bit_induct) + case zero + have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "False \<^bold>* False" "\ False \<^bold>* True" + proof (induction l arbitrary: r rule: int_bit_induct) + case zero + from that show ?case + by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + next + case minus + from that show ?case + by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + next + case (even l) + with that rec [of _ r] show ?case + by (cases "even r") + (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) + next + case (odd l) + moreover have "- l - 1 = - 1 - l" + by simp + ultimately show ?case + using that rec [of _ r] + by (cases "even r") + (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + qed + then show ?case + by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + next + case minus + have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "\ True \<^bold>* True" "False \<^bold>* True" + proof (induction l arbitrary: r rule: int_bit_induct) + case zero + from that show ?case + by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + next + case minus + from that show ?case + by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + next + case (even l) + with that rec [of _ r] show ?case + by (cases "even r") + (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) + next + case (odd l) + moreover have "- l - 1 = - 1 - l" + by simp + ultimately show ?case + using that rec [of _ r] + by (cases "even r") + (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + qed + then show ?case + by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) + next + case (even k) + with rec [of "k * 2"] rec [of _ r] show ?case + by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) + next + case (odd k) + with rec [of "1 + k * 2"] rec [of _ r] show ?case + by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) + qed + show "k \<^bold>\ l = l \<^bold>\ k" for k l :: int + proof (induction k arbitrary: l rule: int_bit_induct) + case zero + show ?case + by simp + next + case minus + show ?case + by simp + next + case (even k) + with rec [of "k * 2" l] rec [of l "k * 2"] show ?case + by (simp add: ac_simps) + next + case (odd k) + with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case + by (simp add: ac_simps) + qed +qed + +lemma self [simp]: + "k \<^bold>\ k = (case (False \<^bold>* False, True \<^bold>* True) + of (False, False) \ 0 + | (False, True) \ k + | (True, True) \ - 1)" + by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split) + +lemma even_iff [simp]: + "even (k \<^bold>\ l) \ \ (odd k \<^bold>* odd l)" +proof (induction k arbitrary: l rule: int_bit_induct) + case zero + show ?case + by (cases "even l") (simp_all split: bool.splits) +next + case minus + show ?case + by (cases "even l") (simp_all split: bool.splits) +next + case (even k) + then show ?case + by (simp add: rec [of "k * 2"]) +next + case (odd k) + then show ?case + by (simp add: rec [of "1 + k * 2"]) +qed + +end + +instantiation int :: ring_bit_operations +begin + +definition not_int :: "int \ int" + where "not_int = complement" + +global_interpretation and_int: zip_int "(\)" + defines and_int = and_int.F + by standard + +declare and_int.simps [simp] \ \inconsistent declaration handling by + \global_interpretation\ in \instantiation\\ + +global_interpretation and_int: semilattice "(AND) :: int \ int \ int" +proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard) + show "k AND k = k" for k :: int + by (simp add: and_int.self) +qed + +lemma zero_int_and_eq [simp]: + "0 AND k = 0" for k :: int + by simp + +lemma and_zero_int_eq [simp]: + "k AND 0 = 0" for k :: int + by simp + +lemma minus_int_and_eq [simp]: + "- 1 AND k = k" for k :: int + by simp + +lemma and_minus_int_eq [simp]: + "k AND - 1 = k" for k :: int + by simp + +global_interpretation or_int: zip_int "(\)" + defines or_int = or_int.F + by standard + +declare or_int.simps [simp] \ \inconsistent declaration handling by + \global_interpretation\ in \instantiation\\ + +global_interpretation or_int: semilattice "(OR) :: int \ int \ int" +proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard) + show "k OR k = k" for k :: int + by (simp add: or_int.self) +qed + +lemma zero_int_or_eq [simp]: + "0 OR k = k" for k :: int + by simp + +lemma and_zero_or_eq [simp]: + "k OR 0 = k" for k :: int + by simp + +lemma minus_int_or_eq [simp]: + "- 1 OR k = - 1" for k :: int + by simp + +lemma or_minus_int_eq [simp]: + "k OR - 1 = - 1" for k :: int + by simp + +global_interpretation xor_int: zip_int "(\)" + defines xor_int = xor_int.F + by standard + +declare xor_int.simps [simp] \ \inconsistent declaration handling by + \global_interpretation\ in \instantiation\\ + +lemma zero_int_xor_eq [simp]: + "0 XOR k = k" for k :: int + by simp + +lemma and_zero_xor_eq [simp]: + "k XOR 0 = k" for k :: int + by simp + +lemma minus_int_xor_eq [simp]: + "- 1 XOR k = complement k" for k :: int + by simp + +lemma xor_minus_int_eq [simp]: + "k XOR - 1 = complement k" for k :: int + by simp + +lemma not_div_2: + "NOT k div 2 = NOT (k div 2)" + for k :: int + by (simp add: complement_div_2 not_int_def) + +lemma not_int_simps [simp]: + "NOT 0 = (- 1 :: int)" + "NOT (- 1) = (0 :: int)" + "k \ 0 \ k \ - 1 \ NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int + by (auto simp add: not_int_def elim: oddE) + +lemma not_one_int [simp]: + "NOT 1 = (- 2 :: int)" + by simp + +lemma even_not_iff [simp]: + "even (NOT k) \ odd k" + for k :: int + by (simp add: not_int_def) + +instance proof + interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int" + proof + show "k AND (l OR r) = k AND l OR k AND r" + for k l r :: int + proof (induction k arbitrary: l r rule: int_bit_induct) + case zero + show ?case + by simp + next + case minus + show ?case + by simp + next + case (even k) + then show ?case by (simp add: and_int.rec [of "k * 2"] + or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l]) + next + case (odd k) + then show ?case by (simp add: and_int.rec [of "1 + k * 2"] + or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l]) + qed + show "k OR l AND r = (k OR l) AND (k OR r)" + for k l r :: int + proof (induction k arbitrary: l r rule: int_bit_induct) + case zero + then show ?case + by simp + next + case minus + then show ?case + by simp + next + case (even k) + then show ?case by (simp add: or_int.rec [of "k * 2"] + and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l]) + next + case (odd k) + then show ?case by (simp add: or_int.rec [of "1 + k * 2"] + and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l]) + qed + show "k AND NOT k = 0" for k :: int + by (induction k rule: int_bit_induct) + (simp_all add: not_int_def complement_half minus_diff_commute [of 1]) + show "k OR NOT k = - 1" for k :: int + by (induction k rule: int_bit_induct) + (simp_all add: not_int_def complement_half minus_diff_commute [of 1]) + qed (simp_all add: and_int.assoc or_int.assoc, + simp_all add: and_int.commute or_int.commute) + show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)" + by (fact bit_int.boolean_algebra_axioms) + show "bit_int.xor = ((XOR) :: int \ _)" + proof (rule ext)+ + fix k l :: int + have "k XOR l = k AND NOT l OR NOT k AND l" + proof (induction k arbitrary: l rule: int_bit_induct) + case zero + show ?case + by simp + next + case minus + show ?case + by (simp add: not_int_def) + next + case (even k) + then show ?case + by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"] + or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2) + (simp add: and_int.rec [of _ l]) + next + case (odd k) + then show ?case + by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"] + or_int.rec [of _ "2 * NOT k AND l"] not_div_2) + (simp add: and_int.rec [of _ l]) + qed + then show "bit_int.xor k l = k XOR l" + by (simp add: bit_int.xor_def) + qed +qed + +end + +lemma one_and_int_eq [simp]: + "1 AND k = k mod 2" for k :: int + using and_int.rec [of 1] by (simp add: mod2_eq_if) + +lemma and_one_int_eq [simp]: + "k AND 1 = k mod 2" for k :: int + using one_and_int_eq [of 1] by (simp add: ac_simps) + +lemma one_or_int_eq [simp]: + "1 OR k = k + of_bool (even k)" for k :: int + using or_int.rec [of 1] by (auto elim: oddE) + +lemma or_one_int_eq [simp]: + "k OR 1 = k + of_bool (even k)" for k :: int + using one_or_int_eq [of k] by (simp add: ac_simps) + +lemma one_xor_int_eq [simp]: + "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int + using xor_int.rec [of 1] by (auto elim: oddE) + +lemma xor_one_int_eq [simp]: + "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int + using one_xor_int_eq [of k] by (simp add: ac_simps) + +lemma take_bit_complement_iff: + "Parity.take_bit n (complement k) = Parity.take_bit n (complement l) \ Parity.take_bit n k = Parity.take_bit n l" + for k l :: int + by (simp add: Parity.take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute) + +lemma take_bit_not_iff: + "Parity.take_bit n (NOT k) = Parity.take_bit n (NOT l) \ Parity.take_bit n k = Parity.take_bit n l" + for k l :: int + by (simp add: not_int_def take_bit_complement_iff) + +lemma take_bit_and [simp]: + "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l" + for k l :: int + apply (induction n arbitrary: k l) + apply simp + apply (subst and_int.rec) + apply (subst (2) and_int.rec) + apply simp + done + +lemma take_bit_or [simp]: + "Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l" + for k l :: int + apply (induction n arbitrary: k l) + apply simp + apply (subst or_int.rec) + apply (subst (2) or_int.rec) + apply simp + done + +lemma take_bit_xor [simp]: + "Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l" + for k l :: int + apply (induction n arbitrary: k l) + apply simp + apply (subst xor_int.rec) + apply (subst (2) xor_int.rec) + apply simp + done + + +subsubsection \Instance \<^typ>\'a word\\ + +instantiation word :: (len) ring_bit_operations +begin + +lift_definition not_word :: "'a word \ 'a word" + is not + by (simp add: take_bit_not_iff) + +lift_definition and_word :: "'a word \ 'a word \ 'a word" + is "and" + by simp + +lift_definition or_word :: "'a word \ 'a word \ 'a word" + is or + by simp + +lift_definition xor_word :: "'a word \ 'a word \ 'a word" + is xor + by simp + +instance proof + interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word" + proof + show "a AND (b OR c) = a AND b OR a AND c" + for a b c :: "'a word" + by transfer (simp add: bit.conj_disj_distrib) + show "a OR b AND c = (a OR b) AND (a OR c)" + for a b c :: "'a word" + by transfer (simp add: bit.disj_conj_distrib) + qed (transfer; simp add: ac_simps)+ + show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)" + by (fact bit_word.boolean_algebra_axioms) + show "bit_word.xor = ((XOR) :: 'a word \ _)" + proof (rule ext)+ + fix a b :: "'a word" + have "a XOR b = a AND NOT b OR NOT a AND b" + by transfer (simp add: bit.xor_def) + then show "bit_word.xor a b = a XOR b" + by (simp add: bit_word.xor_def) + qed +qed + +end + +end diff --git a/src/HOL/ex/Word_Type.thy b/src/HOL/ex/Word.thy rename from src/HOL/ex/Word_Type.thy rename to src/HOL/ex/Word.thy --- a/src/HOL/ex/Word_Type.thy +++ b/src/HOL/ex/Word.thy @@ -1,730 +1,574 @@ (* Author: Florian Haftmann, TUM *) section \Proof of concept for algebraically founded bit word types\ -theory Word_Type +theory Word imports Main - "HOL-ex.Bit_Lists" "HOL-Library.Type_Length" begin subsection \Preliminaries\ +context ab_group_add +begin + +lemma minus_diff_commute: + "- b - a = - a - b" + by (simp only: diff_conv_add_uminus add.commute) + +end + lemma take_bit_uminus: "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int by (simp add: take_bit_eq_mod mod_minus_eq) lemma take_bit_minus: "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" for k l :: int by (simp add: take_bit_eq_mod mod_diff_eq) lemma take_bit_nonnegative [simp]: "take_bit n k \ 0" for k :: int by (simp add: take_bit_eq_mod) definition signed_take_bit :: "nat \ int \ int" where signed_take_bit_eq_take_bit: "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n" lemma signed_take_bit_eq_take_bit': "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" if "n > 0" using that by (simp add: signed_take_bit_eq_take_bit) - + lemma signed_take_bit_0 [simp]: "signed_take_bit 0 k = - (k mod 2)" proof (cases "even k") case True then have "odd (k + 1)" by simp then have "(k + 1) mod 2 = 1" by (simp add: even_iff_mod_2_eq_zero) with True show ?thesis by (simp add: signed_take_bit_eq_take_bit) next case False then show ?thesis by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one) qed lemma signed_take_bit_Suc [simp]: "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2" by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps) lemma signed_take_bit_of_0 [simp]: "signed_take_bit n 0 = 0" by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod) lemma signed_take_bit_of_minus_1 [simp]: "signed_take_bit n (- 1) = - 1" by (induct n) simp_all lemma signed_take_bit_eq_iff_take_bit_eq: "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \ take_bit n k = take_bit n l" (is "?P \ ?Q") if "n > 0" proof - from that obtain m where m: "n = Suc m" by (cases n) auto show ?thesis - proof + proof assume ?Q have "take_bit (Suc m) (k + 2 ^ m) = take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))" by (simp only: take_bit_add) also have "\ = take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))" by (simp only: \?Q\ m [symmetric]) also have "\ = take_bit (Suc m) (l + 2 ^ m)" by (simp only: take_bit_add) finally show ?P by (simp only: signed_take_bit_eq_take_bit m) simp next assume ?P with that have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n" by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod) then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i by (metis mod_add_eq) then have "k mod 2 ^ n = l mod 2 ^ n" by (metis add_diff_cancel_right' uminus_add_conv_diff) then show ?Q by (simp add: take_bit_eq_mod) qed -qed +qed subsection \Bit strings as quotient type\ subsubsection \Basic properties\ quotient_type (overloaded) 'a word = int / "\k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l" by (auto intro!: equivpI reflpI sympI transpI) instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}" begin lift_definition zero_word :: "'a word" is 0 . lift_definition one_word :: "'a word" is 1 . lift_definition plus_word :: "'a word \ 'a word \ 'a word" is plus by (subst take_bit_add [symmetric]) (simp add: take_bit_add) lift_definition uminus_word :: "'a word \ 'a word" is uminus by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus) lift_definition minus_word :: "'a word \ 'a word \ 'a word" is minus by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus) lift_definition times_word :: "'a word \ 'a word \ 'a word" is times by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) instance by standard (transfer; simp add: algebra_simps)+ end instance word :: (len) comm_ring_1 by standard (transfer; simp)+ quickcheck_generator word constructors: "zero_class.zero :: ('a::len0) word", "numeral :: num \ ('a::len0) word", "uminus :: ('a::len0) word \ ('a::len0) word" context includes lifting_syntax notes power_transfer [transfer_rule] begin lemma power_transfer_word [transfer_rule]: \(pcr_word ===> (=) ===> pcr_word) (^) (^)\ by transfer_prover end subsubsection \Conversions\ context includes lifting_syntax notes transfer_rule_numeral [transfer_rule] transfer_rule_of_nat [transfer_rule] transfer_rule_of_int [transfer_rule] begin lemma [transfer_rule]: "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) numeral numeral" by transfer_prover lemma [transfer_rule]: "((=) ===> pcr_word) int of_nat" by transfer_prover - + lemma [transfer_rule]: "((=) ===> pcr_word) (\k. k) of_int" proof - have "((=) ===> pcr_word) of_int of_int" by transfer_prover then show ?thesis by (simp add: id_def) qed end lemma abs_word_eq: "abs_word = of_int" by (rule ext) (transfer, rule) context semiring_1 begin lift_definition unsigned :: "'b::len0 word \ 'a" is "of_nat \ nat \ take_bit LENGTH('b)" by simp lemma unsigned_0 [simp]: "unsigned 0 = 0" by transfer simp end context semiring_char_0 begin lemma word_eq_iff_unsigned: "a = b \ unsigned a = unsigned b" by safe (transfer; simp add: eq_nat_nat_iff) end instantiation word :: (len0) equal begin definition equal_word :: "'a word \ 'a word \ bool" where "equal_word a b \ (unsigned a :: int) = unsigned b" instance proof fix a b :: "'a word" show "HOL.equal a b \ a = b" using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def) qed end context ring_1 begin lift_definition signed :: "'b::len word \ 'a" is "of_int \ signed_take_bit (LENGTH('b) - 1)" by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric]) lemma signed_0 [simp]: "signed 0 = 0" by transfer simp end lemma unsigned_of_nat [simp]: "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n" by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int) lemma of_nat_unsigned [simp]: "of_nat (unsigned a) = a" by transfer simp lemma of_int_unsigned [simp]: "of_int (unsigned a) = a" by transfer simp lemma unsigned_nat_less: \unsigned a < (2 ^ LENGTH('a) :: nat)\ for a :: \'a::len0 word\ by transfer (simp add: take_bit_eq_mod) lemma unsigned_int_less: \unsigned a < (2 ^ LENGTH('a) :: int)\ for a :: \'a::len0 word\ by transfer (simp add: take_bit_eq_mod) context ring_char_0 begin lemma word_eq_iff_signed: "a = b \ signed a = signed b" by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq) end lemma signed_of_int [simp]: "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k" by transfer simp lemma of_int_signed [simp]: "of_int (signed a) = a" by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps) subsubsection \Properties\ lemma length_cases: obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)" | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)" proof (cases "LENGTH('a) \ 2") case False then have "LENGTH('a) = 1" by (auto simp add: not_le dest: less_2_cases) then have "take_bit LENGTH('a) 2 = (0 :: int)" by simp with \LENGTH('a) = 1\ triv show ?thesis by simp next case True then obtain n where "LENGTH('a) = Suc (Suc n)" by (auto dest: le_Suc_ex) then have "take_bit LENGTH('a) 2 = (2 :: int)" by simp with take_bit_2 show ?thesis by simp qed subsubsection \Division\ instantiation word :: (len0) modulo begin lift_definition divide_word :: "'a word \ 'a word \ 'a word" is "\a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b" by simp lift_definition modulo_word :: "'a word \ 'a word \ 'a word" is "\a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b" by simp instance .. end lemma zero_word_div_eq [simp]: \0 div a = 0\ for a :: \'a::len0 word\ by transfer simp lemma div_zero_word_eq [simp]: \a div 0 = 0\ for a :: \'a::len0 word\ by transfer simp context includes lifting_syntax begin lemma [transfer_rule]: "(pcr_word ===> (\)) even ((dvd) 2 :: 'a::len word \ bool)" proof - have even_word_unfold: "even k \ (\l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \ ?Q") for k :: int proof assume ?P then show ?Q by auto next assume ?Q then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" .. then have "even (take_bit LENGTH('a) k)" by simp then show ?P by simp qed show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def]) transfer_prover qed end instance word :: (len) semiring_modulo proof show "a div b * b + a mod b = a" for a b :: "'a word" proof transfer fix k l :: int define r :: int where "r = 2 ^ LENGTH('a)" then have r: "take_bit LENGTH('a) k = k mod r" for k by (simp add: take_bit_eq_mod) have "k mod r = ((k mod r) div (l mod r) * (l mod r) + (k mod r) mod (l mod r)) mod r" by (simp add: div_mult_mod_eq) also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_add_left_eq) also have "... = (((k mod r) div (l mod r) * l) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_mult_right_eq) finally have "k mod r = ((k mod r) div (l mod r) * l + (k mod r) mod (l mod r)) mod r" by (simp add: mod_simps) with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k" by simp qed qed instance word :: (len) semiring_parity proof show "\ 2 dvd (1::'a word)" by transfer simp show even_iff_mod_2_eq_0: "2 dvd a \ a mod 2 = 0" for a :: "'a word" by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd) show "\ 2 dvd a \ a mod 2 = 1" for a :: "'a word" by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd) qed subsubsection \Orderings\ instantiation word :: (len0) linorder begin lift_definition less_eq_word :: "'a word \ 'a word \ bool" is "\a b. take_bit LENGTH('a) a \ take_bit LENGTH('a) b" by simp lift_definition less_word :: "'a word \ 'a word \ bool" is "\a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" by simp instance by standard (transfer; auto)+ 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_greater_zero_iff: \a > 0 \ a \ 0\ for a :: \'a::len0 word\ by transfer (simp add: less_le) lemma of_nat_word_eq_iff: \of_nat m = (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 of_nat_word_less_eq_iff: \of_nat m \ (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 of_nat_word_less_iff: \of_nat m < (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 of_nat_word_eq_0_iff: \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 of_int_word_eq_iff: \of_int k = (of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_less_eq_iff: \of_int k \ (of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_less_iff: \of_int k < (of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_eq_0_iff: \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) -subsection \Bit operation on \<^typ>\'a word\\ - -context unique_euclidean_semiring_with_nat -begin - -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) - apply (metis dvd_triv_right even_plus_one_iff) - apply (metis dvd_triv_right even_plus_one_iff) - 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) - -end - -lemma unsigned_of_bits_eq_of_bits: - "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)" - by (simp add: of_bits_int_def) - - -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 - -lemma take_bit_complement_iff: - "take_bit n (complement k) = take_bit n (complement l) \ take_bit n k = take_bit n l" - for k l :: int - by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute) - -lemma take_bit_not_iff: - "take_bit n (NOT k) = take_bit n (NOT l) \ take_bit n k = take_bit n l" - for k l :: int - by (simp add: not_int_def take_bit_complement_iff) - -lemma n_bits_of_not: - "n_bits_of n (NOT k) = map Not (n_bits_of n k)" - for k :: int - by (induction n arbitrary: k) (simp_all add: not_div_2) - -lemma take_bit_and [simp]: - "take_bit n (k AND l) = take_bit n k AND take_bit n l" - for k l :: int - apply (induction n arbitrary: k l) - apply simp - apply (subst and_int.rec) - apply (subst (2) and_int.rec) - apply simp - done - -lemma take_bit_or [simp]: - "take_bit n (k OR l) = take_bit n k OR take_bit n l" - for k l :: int - apply (induction n arbitrary: k l) - apply simp - apply (subst or_int.rec) - apply (subst (2) or_int.rec) - apply simp - done - -lemma take_bit_xor [simp]: - "take_bit n (k XOR l) = take_bit n k XOR take_bit n l" - for k l :: int - apply (induction n arbitrary: k l) - apply simp - apply (subst xor_int.rec) - apply (subst (2) xor_int.rec) - apply simp - done - -instantiation word :: (len) bit_operations -begin - -lift_definition not_word :: "'a word \ 'a word" - is not - by (simp add: take_bit_not_iff) - -lift_definition and_word :: "'a word \ 'a word \ 'a word" - is "and" - by simp - -lift_definition or_word :: "'a word \ 'a word \ 'a word" - is or - by simp - -lift_definition xor_word :: "'a word \ 'a word \ 'a word" - is xor - by simp - -lift_definition shift_left_word :: "'a word \ nat \ 'a word" - is shift_left -proof - - show "take_bit LENGTH('a) (k << n) = take_bit LENGTH('a) (l << n)" - if "take_bit LENGTH('a) k = take_bit LENGTH('a) l" for k l :: int and n :: nat - proof - - from that - have "take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k) - = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)" - by simp - moreover have "min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n" - by simp - ultimately show ?thesis by (simp add: take_bit_push_bit) - qed -qed - -lift_definition shift_right_word :: "'a word \ nat \ 'a word" - is "\k n. drop_bit n (take_bit LENGTH('a) k)" - by simp - -instance proof - show "semilattice ((AND) :: 'a word \ _)" - by standard (transfer; simp add: ac_simps)+ - show "semilattice ((OR) :: 'a word \ _)" - by standard (transfer; simp add: ac_simps)+ - show "abel_semigroup ((XOR) :: 'a word \ _)" - by standard (transfer; simp add: ac_simps)+ - show "not = (of_bits \ map Not \ bits_of :: 'a word \ 'a word)" - proof - fix a :: "'a word" - have "NOT a = of_bits (map Not (bits_of a))" - by transfer (simp flip: unsigned_of_bits_take n_bits_of_not add: take_map) - then show "NOT a = (of_bits \ map Not \ bits_of) a" - by simp - qed - show "of_bits bs AND of_bits cs = (of_bits (map2 (\) bs cs) :: 'a word)" - if "length bs = length cs" for bs cs - using that apply transfer - apply (simp only: unsigned_of_bits_eq_of_bits) - apply (subst and_eq) - apply simp_all - done - show "of_bits bs OR of_bits cs = (of_bits (map2 (\) bs cs) :: 'a word)" - if "length bs = length cs" for bs cs - using that apply transfer - apply (simp only: unsigned_of_bits_eq_of_bits) - apply (subst or_eq) - apply simp_all - done - show "of_bits bs XOR of_bits cs = (of_bits (map2 (\) bs cs) :: 'a word)" - if "length bs = length cs" for bs cs - using that apply transfer - apply (simp only: unsigned_of_bits_eq_of_bits) - apply (subst xor_eq) - apply simp_all - done - show "a << n = of_bits (replicate n False @ bits_of a)" - for a :: "'a word" and n :: nat - by transfer (simp add: push_bit_take_bit) - show "a >> n = of_bits (drop n (bits_of a))" - if "n < length (bits_of a)" - for a :: "'a word" and n :: nat - using that by transfer simp -qed - - subsection \Bit structure on \<^typ>\'a word\\ lemma word_bit_induct [case_names zero even odd]: \P a\ if word_zero: \P 0\ and word_even: \\a. P a \ 0 < a \ a < 2 ^ (LENGTH('a) - 1) \ P (2 * a)\ and word_odd: \\a. P a \ a < 2 ^ (LENGTH('a) - 1) \ P (1 + 2 * a)\ for P and a :: \'a::len word\ proof - define m :: nat where \m = LENGTH('a) - 1\ then have l: \LENGTH('a) = Suc m\ by simp define n :: nat where \n = unsigned a\ then have \n < 2 ^ LENGTH('a)\ by (simp add: unsigned_nat_less) then have \n < 2 * 2 ^ m\ by (simp add: l) then have \P (of_nat n)\ proof (induction n rule: nat_bit_induct) case zero show ?case by simp (rule word_zero) next case (even n) then have \n < 2 ^ m\ by simp with even.IH have \P (of_nat n)\ by simp moreover from \n < 2 ^ m\ even.hyps have \0 < (of_nat n :: 'a word)\ by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) moreover from \n < 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (cases \m = 0\) (simp_all add: not_less take_bit_eq_self ac_simps l) ultimately have \P (2 * of_nat n)\ by (rule word_even) then show ?case by simp next case (odd n) then have \Suc n \ 2 ^ m\ by simp with odd.IH have \P (of_nat n)\ by simp moreover from \Suc n \ 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (cases \m = 0\) (simp_all add: not_less take_bit_eq_self ac_simps l) ultimately have \P (1 + 2 * of_nat n)\ by (rule word_odd) then show ?case by simp qed then show ?thesis by (simp add: n_def) qed -end - -global_interpretation bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a::len word" - rewrites "bit_word.xor = ((XOR) :: 'a word \ _)" -proof - - interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word" - proof - show "a AND (b OR c) = a AND b OR a AND c" - for a b c :: "'a word" - by transfer (simp add: bit_int.conj_disj_distrib) - show "a OR b AND c = (a OR b) AND (a OR c)" - for a b c :: "'a word" - by transfer (simp add: bit_int.disj_conj_distrib) - show "a AND NOT a = 0" for a :: "'a word" - by transfer simp - show "a OR NOT a = - 1" for a :: "'a word" - by transfer simp - qed (transfer; simp)+ - show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)" - by (fact bit_word.boolean_algebra_axioms) - show "bit_word.xor = ((XOR) :: 'a word \ _)" - proof (rule ext)+ - fix a b :: "'a word" - have "a XOR b = a AND NOT b OR NOT a AND b" - by transfer (simp add: bit_int.xor_def) - then show "bit_word.xor a b = a XOR b" - by (simp add: bit_word.xor_def) +lemma bit_word_half_eq: + \(of_bool b + a * 2) div 2 = a\ + if \a < 2 ^ (LENGTH('a) - Suc 0)\ + for a :: \'a::len word\ +proof (cases rule: length_cases [where ?'a = 'a]) + case triv + have \of_bool (odd k) < (1 :: int) \ even k\ for k :: int + by auto + with triv that show ?thesis + by (auto; transfer) simp_all +next + case take_bit_2 + obtain n where length: \LENGTH('a) = Suc n\ + by (cases \LENGTH('a)\) simp_all + show ?thesis proof (cases b) + case False + moreover have \a * 2 div 2 = a\ + using that proof transfer + fix k :: int + from length have \k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\ + by simp + moreover assume \take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\ + with \LENGTH('a) = Suc n\ + have \k mod 2 ^ LENGTH('a) = k mod 2 ^ n\ + by (simp add: take_bit_eq_mod divmod_digit_0) + ultimately have \take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\ + by (simp add: take_bit_eq_mod) + with take_bit_2 show \take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) + = take_bit LENGTH('a) k\ + by simp + qed + ultimately show ?thesis + by simp + next + case True + moreover have \(1 + a * 2) div 2 = a\ + using that proof transfer + fix k :: int + from length have \(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\ + using pos_zmod_mult_2 [of \2 ^ n\ k] by (simp add: ac_simps) + moreover assume \take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\ + with \LENGTH('a) = Suc n\ + have \k mod 2 ^ LENGTH('a) = k mod 2 ^ n\ + by (simp add: take_bit_eq_mod divmod_digit_0) + ultimately have \take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\ + by (simp add: take_bit_eq_mod) + with take_bit_2 show \take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) + = take_bit LENGTH('a) k\ + by simp + qed + ultimately show ?thesis + by simp qed qed end