6 imports Main |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 subsection \<open>Logic\<close> |
9 subsection \<open>Logic\<close> |
10 |
10 |
11 lemma and_de_morgan_and_absorbe: "(~(A&B)) = ((~A)&B| ~B)" |
11 lemma and_de_morgan_and_absorbe: "(\<not>(A\<and>B)) = ((\<not>A)\<and>B\<or> \<not>B)" |
12 by blast |
12 by blast |
13 |
13 |
14 lemma bool_if_impl_or: "(if C then A else B) --> (A|B)" |
14 lemma bool_if_impl_or: "(if C then A else B) \<longrightarrow> (A\<or>B)" |
15 by auto |
15 by auto |
16 |
16 |
17 lemma exis_elim: "(? x. x=P & Q(x)) = Q(P)" |
17 lemma exis_elim: "(\<exists>x. x=P \<and> Q(x)) = Q(P)" |
18 by blast |
18 by blast |
19 |
19 |
20 |
20 |
21 subsection \<open>Sets\<close> |
21 subsection \<open>Sets\<close> |
22 |
22 |
23 lemma set_lemmas: |
23 lemma set_lemmas: |
24 "f(x) : (UN x. {f(x)})" |
24 "f(x) \<in> (\<Union>x. {f(x)})" |
25 "f x y : (UN x y. {f x y})" |
25 "f x y \<in> (\<Union>x y. {f x y})" |
26 "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})" |
26 "\<And>a. (\<forall>x. a \<noteq> f(x)) \<Longrightarrow> a \<notin> (\<Union>x. {f(x)})" |
27 "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})" |
27 "\<And>a. (\<forall>x y. a \<noteq> f x y) ==> a \<notin> (\<Union>x y. {f x y})" |
28 by auto |
28 by auto |
29 |
29 |
30 text \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling, |
30 text \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling, |
31 namely for Intersections and the empty list (compatibility of IOA!).\<close> |
31 namely for Intersections and the empty list (compatibility of IOA!).\<close> |
32 lemma singleton_set: "(UN b.{x. x=f(b)})= (UN b.{f(b)})" |
32 lemma singleton_set: "(\<Union>b.{x. x=f(b)}) = (\<Union>b.{f(b)})" |
33 by blast |
33 by blast |
34 |
34 |
35 lemma de_morgan: "((A|B)=False) = ((~A)&(~B))" |
35 lemma de_morgan: "((A\<or>B)=False) = ((\<not>A)\<and>(\<not>B))" |
36 by blast |
36 by blast |
37 |
37 |
38 |
38 |
39 subsection \<open>Lists\<close> |
39 subsection \<open>Lists\<close> |
40 |
40 |
41 lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))" |
41 lemma cons_not_nil: "l \<noteq> [] \<longrightarrow> (\<exists>x xs. l = (x#xs))" |
42 by (induct l) simp_all |
42 by (induct l) simp_all |
43 |
43 |
44 end |
44 end |