src/HOL/Presburger.thy
changeset 23405 8993b3144358
parent 23390 01ef1135de73
child 23430 771117253634
equal deleted 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 
   376 lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))"
       
   377 by blast
       
   378 
       
   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