author | paulson |
Fri, 03 Jan 1997 15:01:55 +0100 | |
changeset 2469 | b50b8c0eec01 |
parent 1461 | 6bcb44e4d6e5 |
child 2493 | bdeb5024353a |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/Data.ML |
56 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
56 | 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))"; |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
13 |
let open data; val rew = rewrite_rule con_defs in |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
14 |
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs) |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
15 |
addEs [rew elim]) 1) |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
16 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
529
diff
changeset
|
17 |
qed "data_unfold"; |
56 | 18 |
|
19 |
(** Lemmas to justify using "data" in other recursive type definitions **) |
|
20 |
||
515 | 21 |
goalw Data.thy data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)"; |
56 | 22 |
by (rtac lfp_mono 1); |
515 | 23 |
by (REPEAT (rtac data.bnd_mono 1)); |
56 | 24 |
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
529
diff
changeset
|
25 |
qed "data_mono"; |
56 | 26 |
|
515 | 27 |
goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)"; |
56 | 28 |
by (rtac lfp_lowerbound 1); |
29 |
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2); |
|
2469 | 30 |
by (fast_tac (!claset addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
1461 | 31 |
Pair_in_univ]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
529
diff
changeset
|
32 |
qed "data_univ"; |
56 | 33 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
529
diff
changeset
|
34 |
bind_thm ("data_subset_univ", ([data_mono, data_univ] MRS subset_trans)); |
56 | 35 |
|
36 |