515
|
1 |
(* Title: ZF/ex/Data.ML
|
56
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Sample datatype definition.
|
|
7 |
It has four contructors, of arities 0-3, and two parameters A and B.
|
|
8 |
*)
|
|
9 |
|
515
|
10 |
open Data;
|
56
|
11 |
|
515
|
12 |
goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
|
|
13 |
by (rtac (data.unfold RS trans) 1);
|
|
14 |
bws data.con_defs;
|
|
15 |
br equalityI 1;
|
|
16 |
by (fast_tac sum_cs 1);
|
|
17 |
(*for this direction, fast_tac is just too slow!*)
|
|
18 |
by (safe_tac sum_cs);
|
|
19 |
by (REPEAT_FIRST (swap_res_tac [refl, conjI, disjCI, exI]));
|
|
20 |
by (REPEAT (fast_tac (sum_cs addIs datatype_intrs
|
|
21 |
addDs [data.dom_subset RS subsetD]) 1));
|
|
22 |
val data_unfold = result();
|
56
|
23 |
|
|
24 |
(** Lemmas to justify using "data" in other recursive type definitions **)
|
|
25 |
|
515
|
26 |
goalw Data.thy data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
|
56
|
27 |
by (rtac lfp_mono 1);
|
515
|
28 |
by (REPEAT (rtac data.bnd_mono 1));
|
56
|
29 |
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
|
|
30 |
val data_mono = result();
|
|
31 |
|
515
|
32 |
goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
|
56
|
33 |
by (rtac lfp_lowerbound 1);
|
|
34 |
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
|
|
35 |
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
|
|
36 |
Pair_in_univ]) 1);
|
|
37 |
val data_univ = result();
|
|
38 |
|
|
39 |
val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
|
|
40 |
|
|
41 |
|