Code

Add more theorems and constants#1375

Code

Merged

xrchz merged 19 commits intodevelopHOL-Theorem-Prover/HOL:developfrom upstreamingHOL-Theorem-Prover/HOL:upstreamingCopy head branch name to clipboardDec 18, 2024

+701-115

Commits

Commits on Dec 15, 2024

• Add bool_to_bit

  xrchz

  committed
  cbc649c

• Prove more theorems about chunks

  xrchz

  committed
  0484556

• Fix some Unicode violations

  xrchz

  committed
  9c5d06b

• Add some theorems about dropWhile

  xrchz

  committed
  aa170a5

• Add LENGTH_word_to_bin_list_bound

  xrchz

  committed
  c46c51b

• Prove word_from_bin_list rol and ror

  xrchz

  committed
  eebff12

• Prove word_from_bin_list_and

  xrchz

  committed
  ae219da

• Prove word_from_bin_list_not

  xrchz

  committed
  afdcb4a

• Add some theorems about l2w and w2l

  xrchz

  committed
  5ae53ad

• Prove BITWISE_COMM and BITWISE_AND_0

  xrchz

  committed
  5fb53e4

• Prove word_and_lsl_eq_0

  xrchz

  committed
  db90904

• Attempt to fix OpenTheory base vs HOL4

  xrchz

  committed
  4e16bd3

Commits on Dec 16, 2024

• Remove unneeded inline proof about BITWISE /\ 0

  xrchz

  committed
  4640431

• Revert "Attempt to fix OpenTheory base vs HOL4"

  Show description for 6081abe
  xrchz

  committed
  6081abe

Commits on Dec 17, 2024

• Prove a new opentheory bridge assumption

  xrchz

  committed
  f7257e6

Commits on Dec 18, 2024

• Remove redundant proof of BOOL_EQ_DISTINCT

  xrchz

  committed
  b9dead1

• Make chunks_length a simp

  xrchz

  committed
  00b7c1d

• Reorient l2n_2_neg

  xrchz

  committed
  4d1168d

• Fix proof after reorienting statement

  xrchz

  committed
  8274f79