5846
|
1 |
(* Title: HOL/ex/Points.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
|
5741
|
4 |
|
5846
|
5 |
Basic use of extensible records in HOL, including the famous points
|
|
6 |
and coloured points.
|
|
7 |
|
|
8 |
Note: any of these goals may be solved at a stroke by Auto_tac or Force_tac
|
|
9 |
*)
|
5753
|
10 |
|
|
11 |
|
|
12 |
(* some basic simplifications *)
|
5741
|
13 |
|
5846
|
14 |
Goal "x (| x = m, y = n, ... = p |) = m";
|
5741
|
15 |
by (Simp_tac 1);
|
5753
|
16 |
result();
|
5741
|
17 |
|
5846
|
18 |
Goal "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
|
5741
|
19 |
by (Simp_tac 1);
|
5753
|
20 |
result();
|
5741
|
21 |
|
|
22 |
|
5846
|
23 |
(* splitting quantifiers: the !!r is NECESSARY *)
|
5741
|
24 |
|
5846
|
25 |
Goal "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
|
5741
|
26 |
by (record_split_tac 1);
|
|
27 |
by (Simp_tac 1);
|
5753
|
28 |
result();
|
5741
|
29 |
|
5846
|
30 |
Goal "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
|
5741
|
31 |
by (record_split_tac 1);
|
|
32 |
by (Simp_tac 1);
|
5753
|
33 |
result();
|
5741
|
34 |
|
|
35 |
|
5753
|
36 |
(* record equality *)
|
5741
|
37 |
|
5846
|
38 |
Goal "(| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0";
|
5741
|
39 |
by (Asm_full_simp_tac 1);
|
5753
|
40 |
by (Blast_tac 1);
|
|
41 |
result();
|
5741
|
42 |
|
|
43 |
Goalw [getX_def, setX_def, incX_def] "!!r n. incX r = setX r (Suc (getX r))";
|
|
44 |
by (record_split_tac 1);
|
5753
|
45 |
by (Simp_tac 1);
|
|
46 |
result();
|