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