author | huffman |
Wed, 03 Mar 2010 06:48:00 -0800 | |
changeset 35556 | 730fdfbbd5f8 |
parent 35529 | 089e438b925b |
child 35558 | bb088a6fafbc |
permissions | -rw-r--r-- |
32126 | 1 |
(* Title: HOLCF/Tools/Domain/domain_axioms.ML |
23152 | 2 |
Author: David von Oheimb |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
3 |
Author: Brian Huffman |
23152 | 4 |
|
5 |
Syntax generator for domain command. |
|
6 |
*) |
|
7 |
||
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
8 |
signature DOMAIN_AXIOMS = |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
9 |
sig |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
10 |
val axiomatize_isomorphism : |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
11 |
binding * (typ * typ) -> |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
12 |
theory -> Domain_Take_Proofs.iso_info * theory |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
13 |
|
35556 | 14 |
val axiomatize_lub_take : |
15 |
binding * term -> theory -> thm * theory |
|
16 |
||
33801 | 17 |
val copy_of_dtyp : |
18 |
string Symtab.table -> (int -> term) -> Datatype.dtyp -> term |
|
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset
|
19 |
|
31288 | 20 |
val add_axioms : |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
21 |
(binding * (typ * typ)) list -> |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
22 |
theory -> theory |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
23 |
end; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
24 |
|
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
25 |
|
33245 | 26 |
structure Domain_Axioms : DOMAIN_AXIOMS = |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
27 |
struct |
23152 | 28 |
|
35556 | 29 |
(* TODO: move copy_of_dtyp somewhere else! *) |
30 |
local open Domain_Library in |
|
23152 | 31 |
|
32 |
infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
|
33 |
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
|
34 |
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
|
35 |
||
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset
|
36 |
(* FIXME: use theory data for this *) |
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset
|
37 |
val copy_tab : string Symtab.table = |
35525 | 38 |
Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}), |
39 |
(@{type_name ssum}, @{const_name "ssum_map"}), |
|
40 |
(@{type_name sprod}, @{const_name "sprod_map"}), |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset
|
41 |
(@{type_name "*"}, @{const_name "cprod_map"}), |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset
|
42 |
(@{type_name "u"}, @{const_name "u_map"})]; |
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset
|
43 |
|
33801 | 44 |
fun copy_of_dtyp tab r dt = |
33971 | 45 |
if Datatype_Aux.is_rec_type dt then copy tab r dt else ID |
46 |
and copy tab r (Datatype_Aux.DtRec i) = r i |
|
47 |
| copy tab r (Datatype_Aux.DtTFree a) = ID |
|
48 |
| copy tab r (Datatype_Aux.DtType (c, ds)) = |
|
33801 | 49 |
case Symtab.lookup tab c of |
50 |
SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds) |
|
31288 | 51 |
| NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); |
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset
|
52 |
|
35556 | 53 |
end; (* local open *) |
54 |
||
55 |
open HOLCF_Library; |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
56 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
57 |
fun axiomatize_isomorphism |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
58 |
(dbind : binding, (lhsT, rhsT)) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
59 |
(thy : theory) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
60 |
: Domain_Take_Proofs.iso_info * theory = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
61 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
62 |
val dname = Long_Name.base_name (Binding.name_of dbind); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
63 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
64 |
val abs_bind = Binding.suffix_name "_abs" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
65 |
val rep_bind = Binding.suffix_name "_rep" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
66 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
67 |
val (abs_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
68 |
Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
69 |
val (rep_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
70 |
Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
71 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
72 |
val x = Free ("x", lhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
73 |
val y = Free ("y", rhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
74 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
75 |
val abs_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
76 |
Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y))); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
77 |
val rep_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
78 |
Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
79 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
80 |
val thy = Sign.add_path dname thy; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
81 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
82 |
val (abs_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
83 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
84 |
((Binding.name "abs_iso", abs_iso_eqn), []) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
85 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
86 |
val (rep_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
87 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
88 |
((Binding.name "rep_iso", rep_iso_eqn), []) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
89 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
90 |
val thy = Sign.parent_path thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
91 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
92 |
val result = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
93 |
{ |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
94 |
absT = lhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
95 |
repT = rhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
96 |
abs_const = abs_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
97 |
rep_const = rep_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
98 |
abs_inverse = abs_iso_thm, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
99 |
rep_inverse = rep_iso_thm |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
100 |
}; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
101 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
102 |
(result, thy) |
35517 | 103 |
end; |
23152 | 104 |
|
35556 | 105 |
fun axiomatize_lub_take |
106 |
(dbind : binding, take_const : term) |
|
107 |
(thy : theory) |
|
108 |
: thm * theory = |
|
109 |
let |
|
110 |
val dname = Long_Name.base_name (Binding.name_of dbind); |
|
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
111 |
|
35556 | 112 |
val i = Free ("i", natT); |
113 |
val T = (fst o dest_cfunT o range_type o fastype_of) take_const; |
|
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
114 |
|
35556 | 115 |
val lub_take_eqn = |
116 |
mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)); |
|
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
117 |
|
35556 | 118 |
val thy = Sign.add_path dname thy; |
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
119 |
|
35556 | 120 |
val (lub_take_thm, thy) = |
121 |
yield_singleton PureThy.add_axioms |
|
122 |
((Binding.name "lub_take", lub_take_eqn), []) thy; |
|
23152 | 123 |
|
35556 | 124 |
val thy = Sign.parent_path thy; |
125 |
in |
|
126 |
(lub_take_thm, thy) |
|
127 |
end; |
|
23152 | 128 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
129 |
fun add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
130 |
(dom_eqns : (binding * (typ * typ)) list) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
131 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
132 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
133 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
134 |
(* declare and axiomatize abs/rep *) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
135 |
val (iso_infos, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
136 |
fold_map axiomatize_isomorphism dom_eqns thy; |
23152 | 137 |
|
35556 | 138 |
(* define take functions *) |
35517 | 139 |
val (take_info, thy) = |
140 |
Domain_Take_Proofs.define_take_functions |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
141 |
(map fst dom_eqns ~~ iso_infos) thy; |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
142 |
|
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
143 |
(* declare lub_take axioms *) |
35556 | 144 |
val (lub_take_thms, thy) = |
145 |
fold_map axiomatize_lub_take |
|
146 |
(map fst dom_eqns ~~ #take_consts take_info) thy; |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
147 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
148 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
149 |
thy (* TODO: also return iso_infos, take_info, lub_take_thms *) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
150 |
end; |
31227 | 151 |
|
23152 | 152 |
end; (* struct *) |