Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/Bit_Int.thy
changeset 54489 03ff4d1e6784
parent 54427 783861a66a60
child 54847 d6cf9a5b9be9
equal deleted inserted replaced
54488:b60f1fab408c 54489:03ff4d1e6784 
    50   unfolding int_not_def Bit_def by (cases b, simp_all)
 
    50   unfolding int_not_def Bit_def by (cases b, simp_all)
 
    51 
    51 
    52 lemma int_not_simps [simp]:
 
    52 lemma int_not_simps [simp]:
 
    53   "NOT (0::int) = -1"
 
    53   "NOT (0::int) = -1"
 
    54   "NOT (1::int) = -2"
 
    54   "NOT (1::int) = -2"
 
    55   "NOT (-1::int) = 0"
 
    55   "NOT (- 1::int) = 0"
 
    56   "NOT (numeral w::int) = neg_numeral (w + Num.One)"
 
    56   "NOT (numeral w::int) = - numeral (w + Num.One)"
 
    57   "NOT (neg_numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
 
    57   "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
 
    58   "NOT (neg_numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
 
    58   "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
 
    59   unfolding int_not_def by simp_all
 
    59   unfolding int_not_def by simp_all
 
    60 
    60 
    61 lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
 
    61 lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
 
    62   unfolding int_not_def by simp
 
    62   unfolding int_not_def by simp
 
    63 
    63 
   226 
   226 
   227 lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
 
   227 lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
 
   228   by (metis bin_rl_simp)
 
   228   by (metis bin_rl_simp)
 
   229 
   229 
   230 lemma bin_rest_neg_numeral_BitM [simp]:
 
   230 lemma bin_rest_neg_numeral_BitM [simp]:
 
   231   "bin_rest (neg_numeral (Num.BitM w)) = neg_numeral w"
 
   231   "bin_rest (- numeral (Num.BitM w)) = - numeral w"
 
   232   by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
 
   232   by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
 
   233 
   233 
   234 lemma bin_last_neg_numeral_BitM [simp]:
 
   234 lemma bin_last_neg_numeral_BitM [simp]:
 
   235   "bin_last (neg_numeral (Num.BitM w)) = 1"
 
   235   "bin_last (-  numeral (Num.BitM w)) = 1"
 
   236   by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
 
   236   by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
 
   237 
   237 
   238 text {* FIXME: The rule sets below are very large (24 rules for each
 
   238 text {* FIXME: The rule sets below are very large (24 rules for each
 
   239   operator). Is there a simpler way to do this? *}
 
   239   operator). Is there a simpler way to do this? *}
 
   240 
   240 
   241 lemma int_and_numerals [simp]:
 
   241 lemma int_and_numerals [simp]:
 
   242   "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
 
   242   "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
 
   243   "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 0"
 
   243   "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 0"
 
   244   "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
 
   244   "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
 
   245   "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 1"
 
   245   "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 1"
 
   246   "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
 
   246   "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
 
   247   "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 0"
 
   247   "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 0"
 
   248   "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
 
   248   "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
 
   249   "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 1"
 
   249   "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 1"
 
   250   "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (neg_numeral x AND numeral y) BIT 0"
 
   250   "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT 0"
 
   251   "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (neg_numeral x AND numeral y) BIT 0"
 
   251   "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT 0"
 
   252   "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 0"
 
   252   "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT 0"
 
   253   "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 1"
 
   253   "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT 1"
 
   254   "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral x AND neg_numeral y) BIT 0"
 
   254   "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT 0"
 
   255   "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral x AND neg_numeral (y + Num.One)) BIT 0"
 
   255   "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT 0"
 
   256   "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND neg_numeral y) BIT 0"
 
   256   "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT 0"
 
   257   "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND neg_numeral (y + Num.One)) BIT 1"
 
   257   "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT 1"
 
   258   "(1::int) AND numeral (Num.Bit0 y) = 0"
 
   258   "(1::int) AND numeral (Num.Bit0 y) = 0"
 
   259   "(1::int) AND numeral (Num.Bit1 y) = 1"
 
   259   "(1::int) AND numeral (Num.Bit1 y) = 1"
 
   260   "(1::int) AND neg_numeral (Num.Bit0 y) = 0"
 
   260   "(1::int) AND - numeral (Num.Bit0 y) = 0"
 
   261   "(1::int) AND neg_numeral (Num.Bit1 y) = 1"
 
   261   "(1::int) AND - numeral (Num.Bit1 y) = 1"
 
   262   "numeral (Num.Bit0 x) AND (1::int) = 0"
 
   262   "numeral (Num.Bit0 x) AND (1::int) = 0"
 
   263   "numeral (Num.Bit1 x) AND (1::int) = 1"
 
   263   "numeral (Num.Bit1 x) AND (1::int) = 1"
 
   264   "neg_numeral (Num.Bit0 x) AND (1::int) = 0"
 
   264   "- numeral (Num.Bit0 x) AND (1::int) = 0"
 
   265   "neg_numeral (Num.Bit1 x) AND (1::int) = 1"
 
   265   "- numeral (Num.Bit1 x) AND (1::int) = 1"
 
   266   by (rule bin_rl_eqI, simp, simp)+
 
   266   by (rule bin_rl_eqI, simp, simp)+
 
   267 
   267 
   268 lemma int_or_numerals [simp]:
 
   268 lemma int_or_numerals [simp]:
 
   269   "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 0"
 
   269   "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 0"
 
   270   "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
 
   270   "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
 
   271   "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 1"
 
   271   "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 1"
 
   272   "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
 
   272   "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
 
   273   "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 0"
 
   273   "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 0"
 
   274   "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
 
   274   "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
 
   275   "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 1"
 
   275   "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 1"
 
   276   "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
 
   276   "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
 
   277   "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (neg_numeral x OR numeral y) BIT 0"
 
   277   "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT 0"
 
   278   "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (neg_numeral x OR numeral y) BIT 1"
 
   278   "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT 1"
 
   279   "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
 
   279   "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
 
   280   "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
 
   280   "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
 
   281   "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral x OR neg_numeral y) BIT 0"
 
   281   "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT 0"
 
   282   "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral x OR neg_numeral (y + Num.One)) BIT 1"
 
   282   "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT 1"
 
   283   "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR neg_numeral y) BIT 1"
 
   283   "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT 1"
 
   284   "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR neg_numeral (y + Num.One)) BIT 1"
 
   284   "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT 1"
 
   285   "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
 
   285   "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
 
   286   "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
 
   286   "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
 
   287   "(1::int) OR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
 
   287   "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
 
   288   "(1::int) OR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit1 y)"
 
   288   "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
 
   289   "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
 
   289   "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
 
   290   "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
 
   290   "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
 
   291   "neg_numeral (Num.Bit0 x) OR (1::int) = neg_numeral (Num.BitM x)"
 
   291   "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
 
   292   "neg_numeral (Num.Bit1 x) OR (1::int) = neg_numeral (Num.Bit1 x)"
 
   292   "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
 
   293   by (rule bin_rl_eqI, simp, simp)+
 
   293   by (rule bin_rl_eqI, simp, simp)+
 
   294 
   294 
   295 lemma int_xor_numerals [simp]:
 
   295 lemma int_xor_numerals [simp]:
 
   296   "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 0"
 
   296   "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 0"
 
   297   "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 1"
 
   297   "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 1"
 
   298   "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 1"
 
   298   "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 1"
 
   299   "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 0"
 
   299   "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 0"
 
   300   "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 0"
 
   300   "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 0"
 
   301   "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 1"
 
   301   "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 1"
 
   302   "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 1"
 
   302   "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 1"
 
   303   "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 0"
 
   303   "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 0"
 
   304   "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (neg_numeral x XOR numeral y) BIT 0"
 
   304   "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT 0"
 
   305   "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (neg_numeral x XOR numeral y) BIT 1"
 
   305   "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT 1"
 
   306   "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 1"
 
   306   "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT 1"
 
   307   "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 0"
 
   307   "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT 0"
 
   308   "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral x XOR neg_numeral y) BIT 0"
 
   308   "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT 0"
 
   309   "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral x XOR neg_numeral (y + Num.One)) BIT 1"
 
   309   "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT 1"
 
   310   "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR neg_numeral y) BIT 1"
 
   310   "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT 1"
 
   311   "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR neg_numeral (y + Num.One)) BIT 0"
 
   311   "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT 0"
 
   312   "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
 
   312   "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
 
   313   "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
 
   313   "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
 
   314   "(1::int) XOR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
 
   314   "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
 
   315   "(1::int) XOR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit0 (y + Num.One))"
 
   315   "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
 
   316   "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
 
   316   "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
 
   317   "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
 
   317   "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
 
   318   "neg_numeral (Num.Bit0 x) XOR (1::int) = neg_numeral (Num.BitM x)"
 
   318   "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
 
   319   "neg_numeral (Num.Bit1 x) XOR (1::int) = neg_numeral (Num.Bit0 (x + Num.One))"
 
   319   "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
 
   320   by (rule bin_rl_eqI, simp, simp)+
 
   320   by (rule bin_rl_eqI, simp, simp)+
 
   321 
   321 
   322 subsubsection {* Interactions with arithmetic *}
 
   322 subsubsection {* Interactions with arithmetic *}
 
   323 
   323 
   324 lemma plus_and_or [rule_format]:
 
   324 lemma plus_and_or [rule_format]:
isabelle