src/HOL/Presburger.thy
 changeset 23405 8993b3144358 parent 23390 01ef1135de73 child 23430 771117253634
equal inserted replaced
23404:8659acd81f9d 23405:8993b3144358
`   371 `
`   371 `
`   372 lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"`
`   372 lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"`
`   373 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" `
`   373 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" `
`   374   using not0 by (simp add: dvd_def)`
`   374   using not0 by (simp add: dvd_def)`
`   375 `
`   375 `
`   379 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"`
`   376 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"`
`   380   by simp_all`
`   377   by simp_all`
`   381 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}`
`   378 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}`
`   382 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"`
`   379 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"`
`   383   by (simp split add: split_nat)`
`   380   by (simp split add: split_nat)`
`   597   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"`
`   594   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"`
`   598   unfolding number_of_is_id ..`
`   595   unfolding number_of_is_id ..`
`   599 `
`   596 `
`   600 `
`   597 `
`   601 lemma less_Pls_Pls:`
`   598 lemma less_Pls_Pls:`
`   602   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger `
`   599   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp `
`   603 `
`   600 `
`   604 lemma less_Pls_Min:`
`   601 lemma less_Pls_Min:`
`   605   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"`
`   602   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"`
`   606   unfolding Pls_def Min_def  by presburger `
`   603   unfolding Pls_def Min_def  by presburger `
`   607 `
`   604 `
`   616 lemma less_Min_Pls:`
`   613 lemma less_Min_Pls:`
`   617   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"`
`   614   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"`
`   618   unfolding Pls_def Min_def by presburger `
`   615   unfolding Pls_def Min_def by presburger `
`   619 `
`   616 `
`   620 lemma less_Min_Min:`
`   617 lemma less_Min_Min:`
`   621   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger `
`   618   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp`
`   622 `
`   619 `
`   623 lemma less_Min_Bit:`
`   620 lemma less_Min_Bit:`
`   624   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"`
`   621   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"`
`   625   unfolding Min_def Bit_def by (auto split: bit.split)`
`   622   unfolding Min_def Bit_def by (auto split: bit.split)`
`   626 `
`   623 `