author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 62002 | f1599e98c4d0 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/ABP/Lemmas.thy |
40945 | 2 |
Author: Olaf Müller |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
*) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
17244 | 5 |
theory Lemmas |
6 |
imports Main |
|
7 |
begin |
|
8 |
||
62002 | 9 |
subsection \<open>Logic\<close> |
19738 | 10 |
|
67613 | 11 |
lemma and_de_morgan_and_absorbe: "(\<not>(A\<and>B)) = ((\<not>A)\<and>B\<or> \<not>B)" |
19738 | 12 |
by blast |
13 |
||
67613 | 14 |
lemma bool_if_impl_or: "(if C then A else B) \<longrightarrow> (A\<or>B)" |
19738 | 15 |
by auto |
16 |
||
67613 | 17 |
lemma exis_elim: "(\<exists>x. x=P \<and> Q(x)) = Q(P)" |
19738 | 18 |
by blast |
19 |
||
20 |
||
62002 | 21 |
subsection \<open>Sets\<close> |
19738 | 22 |
|
23 |
lemma set_lemmas: |
|
67613 | 24 |
"f(x) \<in> (\<Union>x. {f(x)})" |
25 |
"f x y \<in> (\<Union>x y. {f x y})" |
|
26 |
"\<And>a. (\<forall>x. a \<noteq> f(x)) \<Longrightarrow> a \<notin> (\<Union>x. {f(x)})" |
|
27 |
"\<And>a. (\<forall>x y. a \<noteq> f x y) ==> a \<notin> (\<Union>x y. {f x y})" |
|
19738 | 28 |
by auto |
29 |
||
62002 | 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> |
|
67613 | 32 |
lemma singleton_set: "(\<Union>b.{x. x=f(b)}) = (\<Union>b.{f(b)})" |
19738 | 33 |
by blast |
34 |
||
67613 | 35 |
lemma de_morgan: "((A\<or>B)=False) = ((\<not>A)\<and>(\<not>B))" |
19738 | 36 |
by blast |
37 |
||
38 |
||
62002 | 39 |
subsection \<open>Lists\<close> |
19738 | 40 |
|
67613 | 41 |
lemma cons_not_nil: "l \<noteq> [] \<longrightarrow> (\<exists>x xs. l = (x#xs))" |
19738 | 42 |
by (induct l) simp_all |
43 |
||
17244 | 44 |
end |