author | wenzelm |
Mon, 12 May 2014 17:17:32 +0200 | |
changeset 56941 | 952833323c99 |
parent 51685 | 385ef6706252 |
child 63003 | bf5fcc65586b |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/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 |
||
31288 | 17 |
val add_axioms : |
36117
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
18 |
(binding * mixfix * (typ * typ)) list -> theory -> |
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
19 |
(Domain_Take_Proofs.iso_info list |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
20 |
* Domain_Take_Proofs.take_induct_info) * theory |
40832 | 21 |
end |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
22 |
|
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
23 |
|
33245 | 24 |
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
|
25 |
struct |
23152 | 26 |
|
40832 | 27 |
open HOLCF_Library |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
28 |
|
40832 | 29 |
infixr 6 ->> |
30 |
infix -->> |
|
31 |
infix 9 ` |
|
35561 | 32 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
33 |
fun axiomatize_isomorphism |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
34 |
(dbind : binding, (lhsT, rhsT)) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
35 |
(thy : theory) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
36 |
: Domain_Take_Proofs.iso_info * theory = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
37 |
let |
40832 | 38 |
val abs_bind = Binding.suffix_name "_abs" dbind |
39 |
val rep_bind = Binding.suffix_name "_rep" dbind |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
40 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
41 |
val (abs_const, thy) = |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42151
diff
changeset
|
42 |
Sign.declare_const_global ((abs_bind, rhsT ->> lhsT), NoSyn) thy |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
43 |
val (rep_const, thy) = |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42151
diff
changeset
|
44 |
Sign.declare_const_global ((rep_bind, lhsT ->> rhsT), NoSyn) thy |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
45 |
|
40832 | 46 |
val x = Free ("x", lhsT) |
47 |
val y = Free ("y", rhsT) |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
48 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
49 |
val abs_iso_eqn = |
40832 | 50 |
Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y))) |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
51 |
val rep_iso_eqn = |
40832 | 52 |
Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))) |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
53 |
|
40832 | 54 |
val abs_iso_bind = Binding.qualified true "abs_iso" dbind |
55 |
val rep_iso_bind = Binding.qualified true "rep_iso" dbind |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
56 |
|
40832 | 57 |
val (abs_iso_thm, thy) = Specification.axiom ((abs_iso_bind, []), abs_iso_eqn) thy |
58 |
val (rep_iso_thm, thy) = Specification.axiom ((rep_iso_bind, []), rep_iso_eqn) thy |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
59 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
60 |
val result = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
61 |
{ |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
62 |
absT = lhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
63 |
repT = rhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
64 |
abs_const = abs_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
65 |
rep_const = rep_const, |
35897
8758895ea413
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
wenzelm
parents:
35856
diff
changeset
|
66 |
abs_inverse = Drule.export_without_context abs_iso_thm, |
8758895ea413
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
wenzelm
parents:
35856
diff
changeset
|
67 |
rep_inverse = Drule.export_without_context rep_iso_thm |
40832 | 68 |
} |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
69 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
70 |
(result, thy) |
40832 | 71 |
end |
23152 | 72 |
|
35556 | 73 |
fun axiomatize_lub_take |
74 |
(dbind : binding, take_const : term) |
|
75 |
(thy : theory) |
|
76 |
: thm * theory = |
|
77 |
let |
|
40832 | 78 |
val i = Free ("i", natT) |
79 |
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
|
80 |
|
35556 | 81 |
val lub_take_eqn = |
40832 | 82 |
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
|
83 |
|
40832 | 84 |
val lub_take_bind = Binding.qualified true "lub_take" dbind |
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
85 |
|
40832 | 86 |
val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy |
35556 | 87 |
in |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
36117
diff
changeset
|
88 |
(lub_take_thm, thy) |
40832 | 89 |
end |
23152 | 90 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
91 |
fun add_axioms |
36117
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
92 |
(dom_eqns : (binding * mixfix * (typ * typ)) list) |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
93 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
94 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
95 |
|
40832 | 96 |
val dbinds = map #1 dom_eqns |
36117
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
97 |
|
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
98 |
(* declare new types *) |
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
99 |
fun thy_type (dbind, mx, (lhsT, _)) = |
40832 | 100 |
(dbind, (length o snd o dest_Type) lhsT, mx) |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42151
diff
changeset
|
101 |
val thy = Sign.add_types_global (map thy_type dom_eqns) thy |
36117
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
102 |
|
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
103 |
(* axiomatize type constructor arities *) |
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
104 |
fun thy_arity (_, _, (lhsT, _)) = |
40832 | 105 |
let val (dname, tvars) = dest_Type lhsT |
106 |
in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end |
|
56941
952833323c99
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
wenzelm
parents:
51685
diff
changeset
|
107 |
val thy = fold (Axclass.arity_axiomatization o thy_arity) dom_eqns thy |
36117
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
108 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
109 |
(* declare and axiomatize abs/rep *) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
110 |
val (iso_infos, thy) = |
36117
01a9db7382f5
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
huffman
parents:
35897
diff
changeset
|
111 |
fold_map axiomatize_isomorphism |
40832 | 112 |
(map (fn (dbind, _, eqn) => (dbind, eqn)) dom_eqns) thy |
23152 | 113 |
|
35556 | 114 |
(* define take functions *) |
35517 | 115 |
val (take_info, thy) = |
116 |
Domain_Take_Proofs.define_take_functions |
|
40832 | 117 |
(dbinds ~~ iso_infos) thy |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
118 |
|
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
119 |
(* declare lub_take axioms *) |
35556 | 120 |
val (lub_take_thms, thy) = |
121 |
fold_map axiomatize_lub_take |
|
40832 | 122 |
(dbinds ~~ #take_consts take_info) thy |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
123 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
124 |
(* prove additional take theorems *) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
125 |
val (take_info2, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
126 |
Domain_Take_Proofs.add_lub_take_theorems |
40832 | 127 |
(dbinds ~~ iso_infos) take_info lub_take_thms thy |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
128 |
|
35792 | 129 |
(* define map functions *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
130 |
val (_, thy) = |
35792 | 131 |
Domain_Isomorphism.define_map_functions |
40832 | 132 |
(dbinds ~~ iso_infos) thy |
35792 | 133 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
134 |
in |
35659 | 135 |
((iso_infos, take_info2), thy) |
40832 | 136 |
end |
31227 | 137 |
|
40832 | 138 |
end (* struct *) |