src/HOL/Library/Nonpos_Ints.thy
changeset 63092 a949b2a5f51d
parent 62390 842917225d56
child 67135 1a94352812f4
equal deleted inserted replaced
63091:54f16a0a3069 63092:a949b2a5f51d
    52 lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0"
    52 lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0"
    53   unfolding nonpos_Ints_def by blast
    53   unfolding nonpos_Ints_def by blast
    54 
    54 
    55 lemma nonpos_IntsI: 
    55 lemma nonpos_IntsI: 
    56   "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0"
    56   "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0"
    57   using assms unfolding nonpos_Ints_def Ints_def by auto
    57   unfolding nonpos_Ints_def Ints_def by auto
    58 
    58 
    59 lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>"
    59 lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>"
    60   unfolding nonpos_Ints_def Ints_def by blast
    60   unfolding nonpos_Ints_def Ints_def by blast
    61 
    61 
    62 lemma nonpos_Ints_nonpos [dest]: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<le> (0 :: 'a :: linordered_idom)"
    62 lemma nonpos_Ints_nonpos [dest]: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<le> (0 :: 'a :: linordered_idom)"