1 (* Title: ZF/Datatype_ZF.thy |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1997 University of Cambridge |
|
4 *) |
|
5 |
|
6 section\<open>Datatype and CoDatatype Definitions\<close> |
|
7 |
|
8 theory Datatype_ZF |
|
9 imports Inductive_ZF Univ QUniv |
|
10 keywords "datatype" "codatatype" :: thy_decl |
|
11 begin |
|
12 |
|
13 ML_file "Tools/datatype_package.ML" |
|
14 |
|
15 ML \<open> |
|
16 (*Typechecking rules for most datatypes involving univ*) |
|
17 structure Data_Arg = |
|
18 struct |
|
19 val intrs = |
|
20 [@{thm SigmaI}, @{thm InlI}, @{thm InrI}, |
|
21 @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ}, |
|
22 @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}]; |
|
23 |
|
24 |
|
25 val elims = [make_elim @{thm InlD}, make_elim @{thm InrD}, (*for mutual recursion*) |
|
26 @{thm SigmaE}, @{thm sumE}]; (*allows * and + in spec*) |
|
27 end; |
|
28 |
|
29 |
|
30 structure Data_Package = |
|
31 Add_datatype_def_Fun |
|
32 (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP |
|
33 and Su=Standard_Sum |
|
34 and Ind_Package = Ind_Package |
|
35 and Datatype_Arg = Data_Arg |
|
36 val coind = false); |
|
37 |
|
38 |
|
39 (*Typechecking rules for most codatatypes involving quniv*) |
|
40 structure CoData_Arg = |
|
41 struct |
|
42 val intrs = |
|
43 [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI}, |
|
44 @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv}, |
|
45 @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}]; |
|
46 |
|
47 val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD}, (*for mutual recursion*) |
|
48 @{thm QSigmaE}, @{thm qsumE}]; (*allows * and + in spec*) |
|
49 end; |
|
50 |
|
51 structure CoData_Package = |
|
52 Add_datatype_def_Fun |
|
53 (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP |
|
54 and Su=Quine_Sum |
|
55 and Ind_Package = CoInd_Package |
|
56 and Datatype_Arg = CoData_Arg |
|
57 val coind = true); |
|
58 |
|
59 |
|
60 |
|
61 (*Simproc for freeness reasoning: compare datatype constructors for equality*) |
|
62 structure DataFree = |
|
63 struct |
|
64 val trace = Unsynchronized.ref false; |
|
65 |
|
66 fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT) |
|
67 | mk_new (largs,rargs) = |
|
68 Balanced_Tree.make FOLogic.mk_conj |
|
69 (map FOLogic.mk_eq (ListPair.zip (largs,rargs))); |
|
70 |
|
71 val datatype_ss = simpset_of @{context}; |
|
72 |
|
73 fun proc ctxt ct = |
|
74 let val old = Thm.term_of ct |
|
75 val thy = Proof_Context.theory_of ctxt |
|
76 val _ = |
|
77 if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old) |
|
78 else () |
|
79 val (lhs,rhs) = FOLogic.dest_eq old |
|
80 val (lhead, largs) = strip_comb lhs |
|
81 and (rhead, rargs) = strip_comb rhs |
|
82 val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; |
|
83 val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; |
|
84 val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname) |
|
85 handle Option.Option => raise Match; |
|
86 val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname) |
|
87 handle Option.Option => raise Match; |
|
88 val new = |
|
89 if #big_rec_name lcon_info = #big_rec_name rcon_info |
|
90 andalso not (null (#free_iffs lcon_info)) then |
|
91 if lname = rname then mk_new (largs, rargs) |
|
92 else Const(@{const_name False},FOLogic.oT) |
|
93 else raise Match |
|
94 val _ = |
|
95 if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new) |
|
96 else (); |
|
97 val goal = Logic.mk_equals (old, new) |
|
98 val thm = Goal.prove ctxt [] [] goal |
|
99 (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN |
|
100 simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1) |
|
101 handle ERROR msg => |
|
102 (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); |
|
103 raise Match) |
|
104 in SOME thm end |
|
105 handle Match => NONE; |
|
106 |
|
107 |
|
108 val conv = |
|
109 Simplifier.make_simproc @{context} "data_free" |
|
110 {lhss = [@{term "(x::i) = y"}], proc = K proc}; |
|
111 |
|
112 end; |
|
113 \<close> |
|
114 |
|
115 setup \<open> |
|
116 Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv]) |
|
117 \<close> |
|
118 |
|
119 end |
|