src/HOL/Presburger.thy
changeset 23390 01ef1135de73
parent 23389 aaca6a8e5414
child 23405 8993b3144358
equal deleted inserted replaced
23389:aaca6a8e5414 23390:01ef1135de73
   406   by (simp cong: conj_cong)
   406   by (simp cong: conj_cong)
   407 lemma int_eq_number_of_eq:
   407 lemma int_eq_number_of_eq:
   408   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   408   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   409   by simp
   409   by simp
   410 
   410 
       
   411 lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
       
   412 unfolding dvd_eq_mod_eq_0[symmetric] ..
       
   413 
       
   414 lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
       
   415 unfolding zdvd_iff_zmod_eq_0[symmetric] ..
       
   416 declare mod_1[presburger]
       
   417 declare mod_0[presburger]
       
   418 declare zmod_1[presburger]
       
   419 declare zmod_zero[presburger]
       
   420 declare zmod_self[presburger]
       
   421 declare mod_self[presburger]
       
   422 declare DIVISION_BY_ZERO_MOD[presburger]
       
   423 declare nat_mod_div_trivial[presburger]
       
   424 declare div_mod_equality2[presburger]
       
   425 declare div_mod_equality[presburger]
       
   426 declare mod_div_equality2[presburger]
       
   427 declare mod_div_equality[presburger]
       
   428 declare mod_mult_self1[presburger]
       
   429 declare mod_mult_self2[presburger]
       
   430 declare zdiv_zmod_equality2[presburger]
       
   431 declare zdiv_zmod_equality[presburger]
       
   432 declare mod2_Suc_Suc[presburger]
       
   433 lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
       
   434 using IntDiv.DIVISION_BY_ZERO by blast+
   411 
   435 
   412 use "Tools/Presburger/cooper.ML"
   436 use "Tools/Presburger/cooper.ML"
   413 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
   437 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
   414 
   438 
   415 use "Tools/Presburger/presburger.ML"
   439 use "Tools/Presburger/presburger.ML"
   439   #> (fn (((elim, add_ths), del_ths),ctxt) => 
   463   #> (fn (((elim, add_ths), del_ths),ctxt) => 
   440          Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
   464          Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
   441 end
   465 end
   442 *} ""
   466 *} ""
   443 
   467 
       
   468 lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
       
   469 lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
       
   470 lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
       
   471 lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
       
   472 lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
       
   473 
   444 subsection {* Code generator setup *}
   474 subsection {* Code generator setup *}
   445 text {*
   475 text {*
   446   Presburger arithmetic is convenient to prove some
   476   Presburger arithmetic is convenient to prove some
   447   of the following code lemmas on integer numerals:
   477   of the following code lemmas on integer numerals:
   448 *}
   478 *}
   449 
   479 
   450 lemma eq_Pls_Pls:
   480 lemma eq_Pls_Pls:
   451   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
   481   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
   452 
   482 
   453 lemma eq_Pls_Min:
   483 lemma eq_Pls_Min:
   454   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   484   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   455   unfolding Pls_def Min_def by auto
   485   unfolding Pls_def Min_def by presburger
   456 
   486 
   457 lemma eq_Pls_Bit0:
   487 lemma eq_Pls_Bit0:
   458   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   488   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   459   unfolding Pls_def Bit_def bit.cases by auto
   489   unfolding Pls_def Bit_def bit.cases by presburger
   460 
   490 
   461 lemma eq_Pls_Bit1:
   491 lemma eq_Pls_Bit1:
   462   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   492   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   463   unfolding Pls_def Bit_def bit.cases by arith
   493   unfolding Pls_def Bit_def bit.cases by presburger
   464 
   494 
   465 lemma eq_Min_Pls:
   495 lemma eq_Min_Pls:
   466   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   496   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   467   unfolding Pls_def Min_def by auto
   497   unfolding Pls_def Min_def by presburger
   468 
   498 
   469 lemma eq_Min_Min:
   499 lemma eq_Min_Min:
   470   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
   500   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
   471 
   501 
   472 lemma eq_Min_Bit0:
   502 lemma eq_Min_Bit0:
   473   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   503   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   474   unfolding Min_def Bit_def bit.cases by arith
   504   unfolding Min_def Bit_def bit.cases by presburger
   475 
   505 
   476 lemma eq_Min_Bit1:
   506 lemma eq_Min_Bit1:
   477   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   507   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   478   unfolding Min_def Bit_def bit.cases by auto
   508   unfolding Min_def Bit_def bit.cases by presburger
   479 
   509 
   480 lemma eq_Bit0_Pls:
   510 lemma eq_Bit0_Pls:
   481   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   511   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   482   unfolding Pls_def Bit_def bit.cases by auto
   512   unfolding Pls_def Bit_def bit.cases by presburger
   483 
   513 
   484 lemma eq_Bit1_Pls:
   514 lemma eq_Bit1_Pls:
   485   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   515   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   486   unfolding Pls_def Bit_def bit.cases by arith
   516   unfolding Pls_def Bit_def bit.cases  by presburger
   487 
   517 
   488 lemma eq_Bit0_Min:
   518 lemma eq_Bit0_Min:
   489   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   519   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   490   unfolding Min_def Bit_def bit.cases by arith
   520   unfolding Min_def Bit_def bit.cases  by presburger
   491 
   521 
   492 lemma eq_Bit1_Min:
   522 lemma eq_Bit1_Min:
   493   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   523   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   494   unfolding Min_def Bit_def bit.cases by auto
   524   unfolding Min_def Bit_def bit.cases  by presburger
   495 
   525 
   496 lemma eq_Bit_Bit:
   526 lemma eq_Bit_Bit:
   497   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   527   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   498     v1 = v2 \<and> k1 = k2"
   528     v1 = v2 \<and> k1 = k2" 
   499   unfolding Bit_def
   529   unfolding Bit_def
   500   apply (cases v1)
   530   apply (cases v1)
   501   apply (cases v2)
   531   apply (cases v2)
   502   apply auto
   532   apply auto
   503   apply arith
   533   apply presburger
   504   apply (cases v2)
   534   apply (cases v2)
   505   apply auto
   535   apply auto
   506   apply arith
   536   apply presburger
   507   apply (cases v2)
   537   apply (cases v2)
   508   apply auto
   538   apply auto
   509 done
   539 done
   510 
   540 
   511 lemma eq_number_of:
   541 lemma eq_number_of:
   512   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
   542   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   513   unfolding number_of_is_id ..
   543   unfolding number_of_is_id ..
   514 
   544 
   515 
   545 
   516 lemma less_eq_Pls_Pls:
   546 lemma less_eq_Pls_Pls:
   517   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   547   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   518 
   548 
   519 lemma less_eq_Pls_Min:
   549 lemma less_eq_Pls_Min:
   520   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   550   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   521   unfolding Pls_def Min_def by auto
   551   unfolding Pls_def Min_def by presburger
   522 
   552 
   523 lemma less_eq_Pls_Bit:
   553 lemma less_eq_Pls_Bit:
   524   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   554   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   525   unfolding Pls_def Bit_def by (cases v) auto
   555   unfolding Pls_def Bit_def by (cases v) auto
   526 
   556 
   527 lemma less_eq_Min_Pls:
   557 lemma less_eq_Min_Pls:
   528   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   558   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   529   unfolding Pls_def Min_def by auto
   559   unfolding Pls_def Min_def by presburger
   530 
   560 
   531 lemma less_eq_Min_Min:
   561 lemma less_eq_Min_Min:
   532   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   562   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   533 
   563 
   534 lemma less_eq_Min_Bit0:
   564 lemma less_eq_Min_Bit0:
   567   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   597   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   568   unfolding number_of_is_id ..
   598   unfolding number_of_is_id ..
   569 
   599 
   570 
   600 
   571 lemma less_Pls_Pls:
   601 lemma less_Pls_Pls:
   572   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
   602   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger 
   573 
   603 
   574 lemma less_Pls_Min:
   604 lemma less_Pls_Min:
   575   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   605   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   576   unfolding Pls_def Min_def by auto
   606   unfolding Pls_def Min_def  by presburger 
   577 
   607 
   578 lemma less_Pls_Bit0:
   608 lemma less_Pls_Bit0:
   579   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   609   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   580   unfolding Pls_def Bit_def by auto
   610   unfolding Pls_def Bit_def by auto
   581 
   611 
   583   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   613   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   584   unfolding Pls_def Bit_def by auto
   614   unfolding Pls_def Bit_def by auto
   585 
   615 
   586 lemma less_Min_Pls:
   616 lemma less_Min_Pls:
   587   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   617   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   588   unfolding Pls_def Min_def by auto
   618   unfolding Pls_def Min_def by presburger 
   589 
   619 
   590 lemma less_Min_Min:
   620 lemma less_Min_Min:
   591   "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
   621   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger 
   592 
   622 
   593 lemma less_Min_Bit:
   623 lemma less_Min_Bit:
   594   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   624   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   595   unfolding Min_def Bit_def by (auto split: bit.split)
   625   unfolding Min_def Bit_def by (auto split: bit.split)
   596 
   626 
   614   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   644   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   615   unfolding Bit_def by (auto split: bit.split)
   645   unfolding Bit_def by (auto split: bit.split)
   616 
   646 
   617 lemma less_Bit0_Bit1:
   647 lemma less_Bit0_Bit1:
   618   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   648   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   619   unfolding Bit_def bit.cases by auto
   649   unfolding Bit_def bit.cases  by arith
   620 
   650 
   621 lemma less_number_of:
   651 lemma less_number_of:
   622   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   652   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   623   unfolding number_of_is_id ..
   653   unfolding number_of_is_id ..
   624 
   654