author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
parent 9000 | c20d58286a51 |
child 12134 | 7049eead7a50 |
permissions | -rw-r--r-- |
516 | 1 |
(* Title: ZF/Datatype.ML |
0 | 2 |
ID: $Id$ |
516 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
120 | 6 |
(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory |
0 | 7 |
*) |
8 |
||
9 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
10 |
(*Typechecking rules for most datatypes involving univ*) |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
11 |
structure Data_Arg = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
12 |
struct |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
13 |
val intrs = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
14 |
[SigmaI, InlI, InrI, |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
15 |
Pair_in_univ, Inl_in_univ, Inr_in_univ, |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
16 |
zero_in_univ, A_into_univ, nat_into_univ, UnCI]; |
0 | 17 |
|
6112 | 18 |
|
19 |
val elims = [make_elim InlD, make_elim InrD, (*for mutual recursion*) |
|
20 |
SigmaE, sumE]; (*allows * and + in spec*) |
|
516 | 21 |
end; |
22 |
||
23 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
24 |
structure Data_Package = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
25 |
Add_datatype_def_Fun |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
26 |
(structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
27 |
and Su=Standard_Sum |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
28 |
and Ind_Package = Ind_Package |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
29 |
and Datatype_Arg = Data_Arg); |
516 | 30 |
|
31 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
32 |
(*Typechecking rules for most codatatypes involving quniv*) |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
33 |
structure CoData_Arg = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
34 |
struct |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
35 |
val intrs = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
36 |
[QSigmaI, QInlI, QInrI, |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
37 |
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
38 |
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI]; |
516 | 39 |
|
6112 | 40 |
val elims = [make_elim QInlD, make_elim QInrD, (*for mutual recursion*) |
41 |
QSigmaE, qsumE]; (*allows * and + in spec*) |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
42 |
end; |
516 | 43 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
44 |
structure CoData_Package = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
45 |
Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
46 |
and Su=Quine_Sum |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
47 |
and Ind_Package = CoInd_Package |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1461
diff
changeset
|
48 |
and Datatype_Arg = CoData_Arg); |
516 | 49 |
|
6141 | 50 |
|
51 |
||
52 |
(*Simproc for freeness reasoning: compare datatype constructors for equality*) |
|
53 |
structure DataFree = |
|
54 |
struct |
|
55 |
(*prove while suppressing timing information*) |
|
9000 | 56 |
fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct); |
6141 | 57 |
|
58 |
val trace = ref false; |
|
59 |
||
60 |
fun mk_new ([],[]) = Const("True",FOLogic.oT) |
|
61 |
| mk_new (largs,rargs) = |
|
7693 | 62 |
fold_bal FOLogic.mk_conj |
6141 | 63 |
(map FOLogic.mk_eq (ListPair.zip (largs,rargs))); |
64 |
||
65 |
||
66 |
fun proc sg _ old = |
|
67 |
let val _ = if !trace then writeln ("data_free: OLD = " ^ |
|
68 |
string_of_cterm (cterm_of sg old)) |
|
69 |
else () |
|
70 |
val (lhs,rhs) = FOLogic.dest_eq old |
|
71 |
val (lhead, largs) = strip_comb lhs |
|
72 |
and (rhead, rargs) = strip_comb rhs |
|
73 |
val lname = #1 (dest_Const lhead) |
|
74 |
and rname = #1 (dest_Const rhead) |
|
75 |
val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname)) |
|
76 |
and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname)) |
|
77 |
val new = |
|
78 |
if #big_rec_name lcon_info = #big_rec_name rcon_info |
|
79 |
andalso not (null (#free_iffs lcon_info)) then |
|
80 |
if lname = rname then mk_new (largs, rargs) |
|
81 |
else Const("False",FOLogic.oT) |
|
82 |
else raise Match |
|
83 |
val _ = if !trace then |
|
84 |
writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) |
|
85 |
else () |
|
86 |
val ct = Thm.cterm_of sg (Logic.mk_equals (old, new)) |
|
87 |
val thm = prove ct |
|
88 |
(fn _ => [rtac iff_reflection 1, |
|
89 |
simp_tac (simpset_of Datatype.thy |
|
90 |
addsimps #free_iffs lcon_info) 1]) |
|
91 |
handle ERROR => |
|
92 |
error("data_free simproc:\nfailed to prove " ^ |
|
93 |
string_of_cterm ct) |
|
94 |
in Some thm end |
|
95 |
handle _ => None; |
|
96 |
||
97 |
||
98 |
val conv = |
|
99 |
Simplifier.mk_simproc "data_free" |
|
100 |
[Thm.read_cterm (sign_of ZF.thy) ("(x::i) = y", FOLogic.oT)] |
|
101 |
proc; |
|
102 |
end; |
|
103 |
||
104 |
||
105 |
Addsimprocs [DataFree.conv]; |