src/HOL/Nitpick.thy
changeset 45970 b6d0cff57d96
parent 45140 339a8b3c4791
child 46319 c248e4f1be74
     1.1 --- a/src/HOL/Nitpick.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  *}
     1.5  
     1.6  lemma Ex1_unfold [nitpick_unfold, no_atp]:
     1.7 -"Ex1 P \<equiv> \<exists>x. P = {x}"
     1.8 +"Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
     1.9  apply (rule eq_reflection)
    1.10  apply (simp add: Ex1_def set_eq_iff)
    1.11  apply (rule iffI)
    1.12 @@ -60,7 +60,7 @@
    1.13   apply (rule allI)
    1.14   apply (rename_tac y)
    1.15   apply (erule_tac x = y in allE)
    1.16 -by (auto simp: mem_def)
    1.17 +by auto
    1.18  
    1.19  lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.20    by (simp only: rtrancl_trancl_reflcl)
    1.21 @@ -70,8 +70,8 @@
    1.22  by (rule eq_reflection) (auto dest: rtranclpD)
    1.23  
    1.24  lemma tranclp_unfold [nitpick_unfold, no_atp]:
    1.25 -"tranclp r a b \<equiv> trancl (split r) (a, b)"
    1.26 -by (simp add: trancl_def Collect_def mem_def)
    1.27 +"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
    1.28 +by (simp add: trancl_def)
    1.29  
    1.30  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.31  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    1.32 @@ -98,8 +98,8 @@
    1.33  *}
    1.34  
    1.35  lemma The_psimp [nitpick_psimp, no_atp]:
    1.36 -"P = {x} \<Longrightarrow> The P = x"
    1.37 -by (subgoal_tac "{x} = (\<lambda>y. y = x)") (auto simp: mem_def)
    1.38 +  "P = (op =) x \<Longrightarrow> The P = x"
    1.39 +  by auto
    1.40  
    1.41  lemma Eps_psimp [nitpick_psimp, no_atp]:
    1.42  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"