Skip to content
Failed

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. build bit operations on word on library theory on bit operations
  2. more instances for uint types
  3. canonical bit shifts for word type, leaving duplicates as they are at the moment
  4. dropped yet another duplicate
  5. replaced mere alias by input abbreviation
  6. replaced mere alias by abbreviation
  7. replaced operation with weak abstraction by input abbreviation
  8. avoid compound operation
  9. replaced mere alias by input abbreviation
Changeset 11135:d5522275e109 by haftmann:
build bit operations on word on library theory on bit operations
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy
The file was modified thys/Collections/Lib/HashCode.thy
The file was modified thys/IP_Addresses/IPv6.thy
The file was modified thys/IP_Addresses/NumberWang_IPv6.thy
The file was modified thys/IP_Addresses/Prefix_Match.thy
The file was modified thys/Interval_Arithmetic_Word32/Interval_Word32.thy
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Native_Word/More_Bits_Int.thy
The file was modified thys/Native_Word/Uint.thy
The file was modified thys/Native_Word/Uint16.thy
The file was modified thys/Native_Word/Uint32.thy
The file was modified thys/Native_Word/Uint64.thy
The file was modified thys/Native_Word/Uint8.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lemmas_32.thy
The file was modified thys/Word_Lib/Word_Lemmas_64.thy
The file was modified thys/Word_Lib/Word_Lib.thy
The file was modified thys/Word_Lib/Word_Next.thy
Changeset 11134:c47d97b64977 by haftmann:
more instances for uint types
The file was modified thys/Native_Word/Uint.thy
The file was modified thys/Native_Word/Uint16.thy
The file was modified thys/Native_Word/Uint32.thy
The file was modified thys/Native_Word/Uint64.thy
The file was modified thys/Native_Word/Uint8.thy
Changeset 11133:25bc16f7e44a by haftmann:
canonical bit shifts for word type, leaving duplicates as they are at the moment
The file was modified thys/Complx/ex/SumArr.thy
The file was modified thys/Containers/ITP-2013/Benchmark_Set.thy
The file was modified thys/Containers/ITP-2013/Benchmark_Set_LC.thy
The file was modified thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy
The file was modified thys/IP_Addresses/WordInterval.thy
The file was modified thys/Interval_Arithmetic_Word32/Interval_Word32.thy
The file was modified thys/Iptables_Semantics/Common/Word_Upto.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Refine_Monadic/examples/WordRefine.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_State.thy
The file was modified thys/Word_Lib/Word_EqI.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lib.thy
The file was modified thys/Word_Lib/Word_Next.thy
The file was modified thys/Word_Lib/Word_Syntax.thy
Changeset 11132:ae31a7712d9c by haftmann:
dropped yet another duplicate
The file was modified thys/Collections/GenCF/Impl/Impl_Bit_Set.thy
The file was modified thys/Interval_Arithmetic_Word32/Interval_Word32.thy
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Bits_Int.thy
The file was modified thys/Native_Word/More_Bits_Int.thy
Changeset 11131:20b49280a650 by haftmann:
replaced mere alias by input abbreviation
The file was modified thys/IEEE_Floating_Point/IEEE_Properties.thy
The file was modified thys/IP_Addresses/Lib_Word_toString.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
Changeset 11130:cf6da1bed594 by haftmann:
replaced mere alias by abbreviation
The file was modified thys/IEEE_Floating_Point/IEEE_Properties.thy
The file was modified thys/IP_Addresses/IP_Address.thy
The file was modified thys/IP_Addresses/IPv4.thy
The file was modified thys/IP_Addresses/IPv6.thy
The file was modified thys/Interval_Arithmetic_Word32/Interval_Word32.thy
The file was modified thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher.thy
The file was modified thys/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy
The file was modified thys/Iptables_Semantics/Semantics_Embeddings.thy
The file was modified thys/Iptables_Semantics/Simple_Firewall/SimpleFw_Compliance.thy
The file was modified thys/LOFT/LinuxRouter_OpenFlow_Translation.thy
The file was modified thys/Simple_Firewall/Service_Matrix.thy
The file was modified thys/Simple_Firewall/SimpleFw_Semantics.thy
The file was modified thys/Word_Lib/Word_Enum.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lib.thy
The file was modified thys/Word_Lib/Word_Next.thy
Changeset 11129:23e6a075730d by haftmann:
replaced operation with weak abstraction by input abbreviation
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lemmas_32.thy
The file was modified thys/Word_Lib/Word_Lemmas_64.thy
Changeset 11128:320af0a4f22c by haftmann:
avoid compound operation
The file was modified thys/Word_Lib/Word_Lemmas.thy
Changeset 11127:bd201908b618 by haftmann:
replaced mere alias by input abbreviation
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Bits_Int.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. more lemmas
  2. build bit operations on word on library theory on bit operations
  3. bit operations as distinctive library theory
  4. tweak for code generation
  5. pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
  6. more lemmas and less name space pollution
  7. canonical bit shifts for word type, leaving duplicates as they are at the moment
  8. essential instance about bit structure
  9. more transfer rules
  10. dropped yet another duplicate
  11. fundamental construction of word type following existing transfer rules
  12. replaced mere alias by input abbreviation
  13. replaced mere alias by abbreviation
  14. replaced operation with weak abstraction by input abbreviation
  15. avoid compound operation
  16. formal relationships between operations
  17. eliminated warnings
  18. replaced mere alias by input abbreviation
Changeset 71958:4320875eb8a1 by haftmann:
more lemmas
The file was modified src/HOL/Parity.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71957:3e162c63371a by haftmann:
build bit operations on word on library theory on bit operations
The file was modified CONTRIBUTORS
The file was modified NEWS
The file was modified src/HOL/Library/Z2.thy
The file was modified src/HOL/Word/Bits.thy
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
The file was modified src/HOL/Word/Word_Bitwise.thy
The file was removedsrc/HOL/Word/Bits_Z2.thy
Changeset 71956:a4bffc0de967 by haftmann:
bit operations as distinctive library theory
The file was addedsrc/HOL/Library/Bit_Operations.thy
The file was modified CONTRIBUTORS
The file was modified NEWS
The file was modified src/HOL/Library/Library.thy
The file was modified src/HOL/ex/Word.thy
The file was removedsrc/HOL/ex/Bit_Operations.thy
Changeset 71955:a9f913d17d00 by haftmann:
tweak for code generation
The file was modified src/HOL/Word/Word.thy
Changeset 71954:13bb3f5cdc5b by haftmann:
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
The file was modified src/HOL/SPARK/SPARK.thy
The file was modified src/HOL/Word/Word.thy
The file was modified src/HOL/Word/Word_Bitwise.thy
The file was modified src/HOL/Word/Word_Examples.thy
The file was modified src/HOL/ex/Word.thy
Changeset 71953:428609096812 by haftmann:
more lemmas and less name space pollution
The file was modified src/HOL/Library/Z2.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71952:2efc5b8c7456 by haftmann:
canonical bit shifts for word type, leaving duplicates as they are at the moment
The file was modified src/HOL/Word/Word.thy
Changeset 71951:ac6f9738c200 by haftmann:
essential instance about bit structure
The file was modified src/HOL/Word/Word.thy
Changeset 71950:c9251bc7da4e by haftmann:
more transfer rules
The file was modified src/HOL/Word/Word.thy
Changeset 71949:5b8b1183c641 by haftmann:
dropped yet another duplicate
The file was modified NEWS
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71948:6ede899d26d3 by haftmann:
fundamental construction of word type following existing transfer rules
The file was modified src/HOL/Word/Word.thy
Changeset 71947:476b9e6904d9 by haftmann:
replaced mere alias by input abbreviation
The file was modified NEWS
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71946:4d4079159be7 by haftmann:
replaced mere alias by abbreviation
The file was modified NEWS
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
The file was modified src/HOL/Word/Word_Examples.thy
Changeset 71945:4b1264316270 by haftmann:
replaced operation with weak abstraction by input abbreviation
The file was modified NEWS
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71944:18357df1cd20 by haftmann:
avoid compound operation
The file was modified NEWS
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71943:d3fb19847662 by haftmann:
formal relationships between operations
The file was modified src/HOL/Word/Bits_Int.thy
Changeset 71942:d2654b30f7bd by haftmann:
eliminated warnings
The file was modified src/HOL/Library/Cardinality.thy
The file was modified src/HOL/Library/Z2.thy
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Misc_Typedef.thy
The file was modified src/HOL/Word/Word.thy
Changeset 71941:49af3d9a818c by haftmann:
replaced mere alias by input abbreviation
The file was modified NEWS
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word_Bitwise.thy