equal
deleted
inserted
replaced
1 (* Title: HOLCF/IOA/ABP/Lemmas.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 *) |
|
5 |
|
6 (* Logic *) |
|
7 |
|
8 Goal "(~(A&B)) = ((~A)&B| ~B)"; |
|
9 by (Fast_tac 1); |
|
10 qed "and_de_morgan_and_absorbe"; |
|
11 |
|
12 Goal "(if C then A else B) --> (A|B)"; |
|
13 by (stac split_if 1); |
|
14 by (Fast_tac 1); |
|
15 qed "bool_if_impl_or"; |
|
16 |
|
17 Goal "(? x. x=P & Q(x)) = Q(P)"; |
|
18 by (Fast_tac 1); |
|
19 qed"exis_elim"; |
|
20 |
|
21 |
|
22 (* Sets *) |
|
23 |
|
24 val set_lemmas = |
|
25 map (fn s => prove_goal Main.thy s (fn _ => [Fast_tac 1])) |
|
26 ["f(x) : (UN x. {f(x)})", |
|
27 "f x y : (UN x y. {f x y})", |
|
28 "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", |
|
29 "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; |
|
30 |
|
31 (* 2 Lemmas to add to set_lemmas ... , used also for action handling, |
|
32 namely for Intersections and the empty list (compatibility of IOA!) *) |
|
33 Goal "(UN b.{x. x=f(b)})= (UN b.{f(b)})"; |
|
34 by (rtac set_ext 1); |
|
35 by (Fast_tac 1); |
|
36 qed "singleton_set"; |
|
37 |
|
38 Goal "((A|B)=False) = ((~A)&(~B))"; |
|
39 by (Fast_tac 1); |
|
40 qed "de_morgan"; |
|
41 |
|
42 (* Lists *) |
|
43 |
|
44 Goal "hd(l@m) = (if l~=[] then hd(l) else hd(m))"; |
|
45 by (induct_tac "l" 1); |
|
46 by (Simp_tac 1); |
|
47 by (Simp_tac 1); |
|
48 qed "hd_append"; |
|
49 |
|
50 Goal "l ~= [] --> (? x xs. l = (x#xs))"; |
|
51 by (induct_tac "l" 1); |
|
52 by (Simp_tac 1); |
|
53 by (Fast_tac 1); |
|
54 qed"cons_not_nil"; |
|