48 text {* |
48 text {* |
49 Alternative definitions. |
49 Alternative definitions. |
50 *} |
50 *} |
51 |
51 |
52 lemma Ex1_unfold [nitpick_unfold, no_atp]: |
52 lemma Ex1_unfold [nitpick_unfold, no_atp]: |
53 "Ex1 P \<equiv> \<exists>x. P = {x}" |
53 "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}" |
54 apply (rule eq_reflection) |
54 apply (rule eq_reflection) |
55 apply (simp add: Ex1_def set_eq_iff) |
55 apply (simp add: Ex1_def set_eq_iff) |
56 apply (rule iffI) |
56 apply (rule iffI) |
57 apply (erule exE) |
57 apply (erule exE) |
58 apply (erule conjE) |
58 apply (erule conjE) |
59 apply (rule_tac x = x in exI) |
59 apply (rule_tac x = x in exI) |
60 apply (rule allI) |
60 apply (rule allI) |
61 apply (rename_tac y) |
61 apply (rename_tac y) |
62 apply (erule_tac x = y in allE) |
62 apply (erule_tac x = y in allE) |
63 by (auto simp: mem_def) |
63 by auto |
64 |
64 |
65 lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>=" |
65 lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>=" |
66 by (simp only: rtrancl_trancl_reflcl) |
66 by (simp only: rtrancl_trancl_reflcl) |
67 |
67 |
68 lemma rtranclp_unfold [nitpick_unfold, no_atp]: |
68 lemma rtranclp_unfold [nitpick_unfold, no_atp]: |
69 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)" |
69 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)" |
70 by (rule eq_reflection) (auto dest: rtranclpD) |
70 by (rule eq_reflection) (auto dest: rtranclpD) |
71 |
71 |
72 lemma tranclp_unfold [nitpick_unfold, no_atp]: |
72 lemma tranclp_unfold [nitpick_unfold, no_atp]: |
73 "tranclp r a b \<equiv> trancl (split r) (a, b)" |
73 "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" |
74 by (simp add: trancl_def Collect_def mem_def) |
74 by (simp add: trancl_def) |
75 |
75 |
76 definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where |
76 definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where |
77 "prod A B = {(a, b). a \<in> A \<and> b \<in> B}" |
77 "prod A B = {(a, b). a \<in> A \<and> b \<in> B}" |
78 |
78 |
79 definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where |
79 definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where |
96 The following lemmas are not strictly necessary but they help the |
96 The following lemmas are not strictly necessary but they help the |
97 \textit{special\_level} optimization. |
97 \textit{special\_level} optimization. |
98 *} |
98 *} |
99 |
99 |
100 lemma The_psimp [nitpick_psimp, no_atp]: |
100 lemma The_psimp [nitpick_psimp, no_atp]: |
101 "P = {x} \<Longrightarrow> The P = x" |
101 "P = (op =) x \<Longrightarrow> The P = x" |
102 by (subgoal_tac "{x} = (\<lambda>y. y = x)") (auto simp: mem_def) |
102 by auto |
103 |
103 |
104 lemma Eps_psimp [nitpick_psimp, no_atp]: |
104 lemma Eps_psimp [nitpick_psimp, no_atp]: |
105 "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x" |
105 "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x" |
106 apply (case_tac "P (Eps P)") |
106 apply (case_tac "P (Eps P)") |
107 apply auto |
107 apply auto |