author | huffman |
Tue, 02 Mar 2010 20:04:17 -0800 | |
changeset 35529 | 089e438b925b |
parent 35525 | fa231b86cb1e |
child 35556 | 730fdfbbd5f8 |
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 |
|
33801 | 14 |
val copy_of_dtyp : |
15 |
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
|
16 |
|
31288 | 17 |
val add_axioms : |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
18 |
(binding * (typ * typ)) list -> |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
19 |
theory -> theory |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
20 |
end; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
21 |
|
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
22 |
|
33245 | 23 |
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
|
24 |
struct |
23152 | 25 |
|
31227 | 26 |
open Domain_Library; |
23152 | 27 |
|
28 |
infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
|
29 |
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
|
30 |
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
|
31 |
||
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset
|
32 |
(* 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
|
33 |
val copy_tab : string Symtab.table = |
35525 | 34 |
Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}), |
35 |
(@{type_name ssum}, @{const_name "ssum_map"}), |
|
36 |
(@{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
|
37 |
(@{type_name "*"}, @{const_name "cprod_map"}), |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
33396
diff
changeset
|
38 |
(@{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
|
39 |
|
33801 | 40 |
fun copy_of_dtyp tab r dt = |
33971 | 41 |
if Datatype_Aux.is_rec_type dt then copy tab r dt else ID |
42 |
and copy tab r (Datatype_Aux.DtRec i) = r i |
|
43 |
| copy tab r (Datatype_Aux.DtTFree a) = ID |
|
44 |
| copy tab r (Datatype_Aux.DtType (c, ds)) = |
|
33801 | 45 |
case Symtab.lookup tab c of |
46 |
SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds) |
|
31288 | 47 |
| 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
|
48 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
49 |
local open HOLCF_Library in |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
50 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
51 |
fun axiomatize_isomorphism |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
52 |
(dbind : binding, (lhsT, rhsT)) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
53 |
(thy : theory) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
54 |
: Domain_Take_Proofs.iso_info * theory = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
55 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
56 |
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
|
57 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
58 |
val abs_bind = Binding.suffix_name "_abs" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
59 |
val rep_bind = Binding.suffix_name "_rep" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
60 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
61 |
val (abs_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
62 |
Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
63 |
val (rep_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
64 |
Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
65 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
66 |
val x = Free ("x", lhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
67 |
val y = Free ("y", rhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
68 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
69 |
val abs_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
70 |
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
|
71 |
val rep_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
72 |
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
|
73 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
74 |
val thy = Sign.add_path dname thy; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
75 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
76 |
val (abs_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
77 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
78 |
((Binding.name "abs_iso", abs_iso_eqn), []) thy; |
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 (rep_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
81 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
82 |
((Binding.name "rep_iso", rep_iso_eqn), []) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
83 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
84 |
val thy = Sign.parent_path 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 result = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
87 |
{ |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
88 |
absT = lhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
89 |
repT = rhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
90 |
abs_const = abs_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
91 |
rep_const = rep_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
92 |
abs_inverse = abs_iso_thm, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
93 |
rep_inverse = rep_iso_thm |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
94 |
}; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
95 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
96 |
(result, thy) |
35517 | 97 |
end; |
23152 | 98 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
99 |
end; |
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
100 |
|
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
101 |
(* legacy type inference *) |
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
102 |
|
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
103 |
fun legacy_infer_term thy t = |
31227 | 104 |
singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); |
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
105 |
|
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
106 |
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); |
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
107 |
|
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
108 |
fun infer_props thy = map (apsnd (legacy_infer_prop thy)); |
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
109 |
|
23152 | 110 |
|
29585 | 111 |
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); |
23152 | 112 |
fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; |
113 |
||
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
114 |
fun add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
115 |
(dom_eqns : (binding * (typ * typ)) list) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
116 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
117 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
118 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
119 |
(* declare and axiomatize abs/rep *) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
120 |
val (iso_infos, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
121 |
fold_map axiomatize_isomorphism dom_eqns thy; |
23152 | 122 |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
123 |
fun add_one (dnam, axs) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
124 |
Sign.add_path dnam |
33245 | 125 |
#> add_axioms_infer axs |
126 |
#> Sign.parent_path; |
|
31227 | 127 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
128 |
(* define take function *) |
35517 | 129 |
val (take_info, thy) = |
130 |
Domain_Take_Proofs.define_take_functions |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
131 |
(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
|
132 |
|
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
133 |
(* declare lub_take axioms *) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
134 |
local |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
135 |
fun ax_lub_take (dbind, take_const) = |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
136 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
137 |
val dnam = Long_Name.base_name (Binding.name_of dbind); |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
138 |
val lub = %%: @{const_name lub}; |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
139 |
val image = %%: @{const_name image}; |
35499 | 140 |
val UNIV = @{term "UNIV :: nat set"}; |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
141 |
val lhs = lub $ (image $ take_const $ UNIV); |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
142 |
val ax = mk_trp (lhs === ID); |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
143 |
in |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
144 |
add_one (dnam, [("lub_take", ax)]) |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
145 |
end |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
146 |
val dbinds = map fst dom_eqns; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
147 |
val take_consts = #take_consts take_info; |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
148 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
149 |
val thy = fold ax_lub_take (dbinds ~~ take_consts) thy |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
150 |
end; |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
151 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
152 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
153 |
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
|
154 |
end; |
31227 | 155 |
|
23152 | 156 |
end; (* struct *) |