Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Presburger.thy
changeset 25919 8b1c0d434824
parent 25230 022029099a83
child 26075 815f3ccc0b45
equal deleted inserted replaced
25918:82dd239e0f65 25919:8b1c0d434824 
   494   Presburger arithmetic is convenient to prove some
 
   494   Presburger arithmetic is convenient to prove some
 
   495   of the following code lemmas on integer numerals:
 
   495   of the following code lemmas on integer numerals:
 
   496 *}
 
   496 *}
 
   497 
   497 
   498 lemma eq_Pls_Pls:
 
   498 lemma eq_Pls_Pls:
 
   499   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
 
   499   "Int.Pls = Int.Pls \<longleftrightarrow> True" by presburger
 
   500 
   500 
   501 lemma eq_Pls_Min:
 
   501 lemma eq_Pls_Min:
 
   502   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
 
   502   "Int.Pls = Int.Min \<longleftrightarrow> False"
 
   503   unfolding Pls_def Numeral.Min_def by presburger
 
   503   unfolding Pls_def Int.Min_def by presburger
 
   504 
   504 
   505 lemma eq_Pls_Bit0:
 
   505 lemma eq_Pls_Bit0:
 
   506   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
 
   506   "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
 
   507   unfolding Pls_def Bit_def bit.cases by presburger
 
   507   unfolding Pls_def Bit_def bit.cases by presburger
 
   508 
   508 
   509 lemma eq_Pls_Bit1:
 
   509 lemma eq_Pls_Bit1:
 
   510   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
 
   510   "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
 
   511   unfolding Pls_def Bit_def bit.cases by presburger
 
   511   unfolding Pls_def Bit_def bit.cases by presburger
 
   512 
   512 
   513 lemma eq_Min_Pls:
 
   513 lemma eq_Min_Pls:
 
   514   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
 
   514   "Int.Min = Int.Pls \<longleftrightarrow> False"
 
   515   unfolding Pls_def Numeral.Min_def by presburger
 
   515   unfolding Pls_def Int.Min_def by presburger
 
   516 
   516 
   517 lemma eq_Min_Min:
 
   517 lemma eq_Min_Min:
 
   518   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
 
   518   "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
 
   519 
   519 
   520 lemma eq_Min_Bit0:
 
   520 lemma eq_Min_Bit0:
 
   521   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
 
   521   "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
 
   522   unfolding Numeral.Min_def Bit_def bit.cases by presburger
 
   522   unfolding Int.Min_def Bit_def bit.cases by presburger
 
   523 
   523 
   524 lemma eq_Min_Bit1:
 
   524 lemma eq_Min_Bit1:
 
   525   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
 
   525   "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
 
   526   unfolding Numeral.Min_def Bit_def bit.cases by presburger
 
   526   unfolding Int.Min_def Bit_def bit.cases by presburger
 
   527 
   527 
   528 lemma eq_Bit0_Pls:
 
   528 lemma eq_Bit0_Pls:
 
   529   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
 
   529   "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
 
   530   unfolding Pls_def Bit_def bit.cases by presburger
 
   530   unfolding Pls_def Bit_def bit.cases by presburger
 
   531 
   531 
   532 lemma eq_Bit1_Pls:
 
   532 lemma eq_Bit1_Pls:
 
   533   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
 
   533   "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
 
   534   unfolding Pls_def Bit_def bit.cases  by presburger
 
   534   unfolding Pls_def Bit_def bit.cases  by presburger
 
   535 
   535 
   536 lemma eq_Bit0_Min:
 
   536 lemma eq_Bit0_Min:
 
   537   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
 
   537   "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
 
   538   unfolding Numeral.Min_def Bit_def bit.cases  by presburger
 
   538   unfolding Int.Min_def Bit_def bit.cases  by presburger
 
   539 
   539 
   540 lemma eq_Bit1_Min:
 
   540 lemma eq_Bit1_Min:
 
   541   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
 
   541   "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
 
   542   unfolding Numeral.Min_def Bit_def bit.cases  by presburger
 
   542   unfolding Int.Min_def Bit_def bit.cases  by presburger
 
   543 
   543 
   544 lemma eq_Bit_Bit:
 
   544 lemma eq_Bit_Bit:
 
   545   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
 
   545   "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
 
   546     v1 = v2 \<and> k1 = k2" 
   546     v1 = v2 \<and> k1 = k2" 
   547   unfolding Bit_def
 
   547   unfolding Bit_def
 
   548   apply (cases v1)
 
   548   apply (cases v1)
 
   549   apply (cases v2)
 
   549   apply (cases v2)
 
   550   apply auto
 
   550   apply auto
 
   560   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   560   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   561   unfolding number_of_is_id ..
 
   561   unfolding number_of_is_id ..
 
   562 
   562 
   563 
   563 
   564 lemma less_eq_Pls_Pls:
 
   564 lemma less_eq_Pls_Pls:
 
   565   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
 
   565   "Int.Pls \<le> Int.Pls \<longleftrightarrow> True" by rule+
 
   566 
   566 
   567 lemma less_eq_Pls_Min:
 
   567 lemma less_eq_Pls_Min:
 
   568   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
 
   568   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
 
   569   unfolding Pls_def Numeral.Min_def by presburger
 
   569   unfolding Pls_def Int.Min_def by presburger
 
   570 
   570 
   571 lemma less_eq_Pls_Bit:
 
   571 lemma less_eq_Pls_Bit:
 
   572   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
 
   572   "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
 
   573   unfolding Pls_def Bit_def by (cases v) auto
 
   573   unfolding Pls_def Bit_def by (cases v) auto
 
   574 
   574 
   575 lemma less_eq_Min_Pls:
 
   575 lemma less_eq_Min_Pls:
 
   576   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
 
   576   "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
 
   577   unfolding Pls_def Numeral.Min_def by presburger
 
   577   unfolding Pls_def Int.Min_def by presburger
 
   578 
   578 
   579 lemma less_eq_Min_Min:
 
   579 lemma less_eq_Min_Min:
 
   580   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
 
   580   "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
 
   581 
   581 
   582 lemma less_eq_Min_Bit0:
 
   582 lemma less_eq_Min_Bit0:
 
   583   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
 
   583   "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
 
   584   unfolding Numeral.Min_def Bit_def by auto
 
   584   unfolding Int.Min_def Bit_def by auto
 
   585 
   585 
   586 lemma less_eq_Min_Bit1:
 
   586 lemma less_eq_Min_Bit1:
 
   587   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
 
   587   "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
 
   588   unfolding Numeral.Min_def Bit_def by auto
 
   588   unfolding Int.Min_def Bit_def by auto
 
   589 
   589 
   590 lemma less_eq_Bit0_Pls:
 
   590 lemma less_eq_Bit0_Pls:
 
   591   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
 
   591   "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
 
   592   unfolding Pls_def Bit_def by simp
 
   592   unfolding Pls_def Bit_def by simp
 
   593 
   593 
   594 lemma less_eq_Bit1_Pls:
 
   594 lemma less_eq_Bit1_Pls:
 
   595   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
 
   595   "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
 
   596   unfolding Pls_def Bit_def by auto
 
   596   unfolding Pls_def Bit_def by auto
 
   597 
   597 
   598 lemma less_eq_Bit_Min:
 
   598 lemma less_eq_Bit_Min:
 
   599   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
 
   599   "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
 
   600   unfolding Numeral.Min_def Bit_def by (cases v) auto
 
   600   unfolding Int.Min_def Bit_def by (cases v) auto
 
   601 
   601 
   602 lemma less_eq_Bit0_Bit:
 
   602 lemma less_eq_Bit0_Bit:
 
   603   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
 
   603   "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
 
   604   unfolding Bit_def bit.cases by (cases v) auto
 
   604   unfolding Bit_def bit.cases by (cases v) auto
 
   605 
   605 
   606 lemma less_eq_Bit_Bit1:
 
   606 lemma less_eq_Bit_Bit1:
 
   607   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
 
   607   "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
 
   608   unfolding Bit_def bit.cases by (cases v) auto
 
   608   unfolding Bit_def bit.cases by (cases v) auto
 
   609 
   609 
   610 lemma less_eq_Bit1_Bit0:
 
   610 lemma less_eq_Bit1_Bit0:
 
   611   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
 
   611   "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
 
   612   unfolding Bit_def by (auto split: bit.split)
 
   612   unfolding Bit_def by (auto split: bit.split)
 
   613 
   613 
   614 lemma less_eq_number_of:
 
   614 lemma less_eq_number_of:
 
   615   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
 
   615   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
 
   616   unfolding number_of_is_id ..
 
   616   unfolding number_of_is_id ..
 
   617 
   617 
   618 
   618 
   619 lemma less_Pls_Pls:
 
   619 lemma less_Pls_Pls:
 
   620   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 
   620   "Int.Pls < Int.Pls \<longleftrightarrow> False" by simp 
   621 
   621 
   622 lemma less_Pls_Min:
 
   622 lemma less_Pls_Min:
 
   623   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
 
   623   "Int.Pls < Int.Min \<longleftrightarrow> False"
 
   624   unfolding Pls_def Numeral.Min_def  by presburger 
   624   unfolding Pls_def Int.Min_def  by presburger 
   625 
   625 
   626 lemma less_Pls_Bit0:
 
   626 lemma less_Pls_Bit0:
 
   627   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
 
   627   "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
 
   628   unfolding Pls_def Bit_def by auto
 
   628   unfolding Pls_def Bit_def by auto
 
   629 
   629 
   630 lemma less_Pls_Bit1:
 
   630 lemma less_Pls_Bit1:
 
   631   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
 
   631   "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
 
   632   unfolding Pls_def Bit_def by auto
 
   632   unfolding Pls_def Bit_def by auto
 
   633 
   633 
   634 lemma less_Min_Pls:
 
   634 lemma less_Min_Pls:
 
   635   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
 
   635   "Int.Min < Int.Pls \<longleftrightarrow> True"
 
   636   unfolding Pls_def Numeral.Min_def by presburger 
   636   unfolding Pls_def Int.Min_def by presburger 
   637 
   637 
   638 lemma less_Min_Min:
 
   638 lemma less_Min_Min:
 
   639   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
 
   639   "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
 
   640 
   640 
   641 lemma less_Min_Bit:
 
   641 lemma less_Min_Bit:
 
   642   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
 
   642   "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
 
   643   unfolding Numeral.Min_def Bit_def by (auto split: bit.split)
 
   643   unfolding Int.Min_def Bit_def by (auto split: bit.split)
 
   644 
   644 
   645 lemma less_Bit_Pls:
 
   645 lemma less_Bit_Pls:
 
   646   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
 
   646   "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
 
   647   unfolding Pls_def Bit_def by (auto split: bit.split)
 
   647   unfolding Pls_def Bit_def by (auto split: bit.split)
 
   648 
   648 
   649 lemma less_Bit0_Min:
 
   649 lemma less_Bit0_Min:
 
   650   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
 
   650   "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
 
   651   unfolding Numeral.Min_def Bit_def by auto
 
   651   unfolding Int.Min_def Bit_def by auto
 
   652 
   652 
   653 lemma less_Bit1_Min:
 
   653 lemma less_Bit1_Min:
 
   654   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
 
   654   "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
 
   655   unfolding Numeral.Min_def Bit_def by auto
 
   655   unfolding Int.Min_def Bit_def by auto
 
   656 
   656 
   657 lemma less_Bit_Bit0:
 
   657 lemma less_Bit_Bit0:
 
   658   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
 
   658   "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
 
   659   unfolding Bit_def by (auto split: bit.split)
 
   659   unfolding Bit_def by (auto split: bit.split)
 
   660 
   660 
   661 lemma less_Bit1_Bit:
 
   661 lemma less_Bit1_Bit:
 
   662   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
 
   662   "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
 
   663   unfolding Bit_def by (auto split: bit.split)
 
   663   unfolding Bit_def by (auto split: bit.split)
 
   664 
   664 
   665 lemma less_Bit0_Bit1:
 
   665 lemma less_Bit0_Bit1:
 
   666   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
 
   666   "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
 
   667   unfolding Bit_def bit.cases  by arith
 
   667   unfolding Bit_def bit.cases  by arith
 
   668 
   668 
   669 lemma less_number_of:
 
   669 lemma less_number_of:
 
   670   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
 
   670   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
 
   671   unfolding number_of_is_id ..
 
   671   unfolding number_of_is_id ..
wneuper/isa