equal
deleted
inserted
replaced
5 |
5 |
6 theory Lemmas |
6 theory Lemmas |
7 imports Main |
7 imports Main |
8 begin |
8 begin |
9 |
9 |
|
10 subsubsection {* Logic *} |
|
11 |
|
12 lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)" |
|
13 by blast |
|
14 |
|
15 |
|
16 subsection {* Sets *} |
|
17 |
|
18 lemma set_lemmas: |
|
19 "f(x) : (UN x. {f(x)})" |
|
20 "f x y : (UN x y. {f x y})" |
|
21 "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})" |
|
22 "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})" |
|
23 by auto |
|
24 |
|
25 |
|
26 subsection {* Arithmetic *} |
|
27 |
|
28 lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))" |
|
29 by (simp add: diff_Suc split add: nat.split) |
|
30 |
|
31 lemmas [simp] = hd_append set_lemmas |
|
32 |
10 end |
33 end |
11 |
|