author | huffman |
Wed, 03 Mar 2010 08:26:01 -0800 | |
changeset 35561 | b56d5b1b1a55 |
parent 35559 | 119653afcd6e |
child 35654 | 7a15e181bf3b |
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 |
||
31288 | 17 |
val add_axioms : |
35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35556
diff
changeset
|
18 |
(binding * (typ * typ)) list -> theory -> |
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35556
diff
changeset
|
19 |
Domain_Take_Proofs.iso_info list * 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 |
|
35556 | 26 |
open HOLCF_Library; |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
27 |
|
35561 | 28 |
infixr 6 ->>; |
29 |
infix -->>; |
|
30 |
infix 9 `; |
|
31 |
||
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
32 |
fun axiomatize_isomorphism |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
33 |
(dbind : binding, (lhsT, rhsT)) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
34 |
(thy : theory) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
35 |
: Domain_Take_Proofs.iso_info * theory = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
36 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
37 |
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
|
38 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
39 |
val abs_bind = Binding.suffix_name "_abs" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
40 |
val rep_bind = Binding.suffix_name "_rep" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
41 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
42 |
val (abs_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
43 |
Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
44 |
val (rep_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
45 |
Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
46 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
47 |
val x = Free ("x", lhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
48 |
val y = Free ("y", rhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
49 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
50 |
val abs_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
51 |
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
|
52 |
val rep_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
53 |
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
|
54 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
55 |
val thy = Sign.add_path dname thy; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
56 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
57 |
val (abs_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
58 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
59 |
((Binding.name "abs_iso", abs_iso_eqn), []) thy; |
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 (rep_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
62 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
63 |
((Binding.name "rep_iso", rep_iso_eqn), []) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
64 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
65 |
val thy = Sign.parent_path thy; |
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 result = |
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 |
absT = lhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
70 |
repT = rhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
71 |
abs_const = abs_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
72 |
rep_const = rep_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
73 |
abs_inverse = abs_iso_thm, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
74 |
rep_inverse = rep_iso_thm |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
75 |
}; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
76 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
77 |
(result, thy) |
35517 | 78 |
end; |
23152 | 79 |
|
35556 | 80 |
fun axiomatize_lub_take |
81 |
(dbind : binding, take_const : term) |
|
82 |
(thy : theory) |
|
83 |
: thm * theory = |
|
84 |
let |
|
85 |
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
|
86 |
|
35556 | 87 |
val i = Free ("i", natT); |
88 |
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
|
89 |
|
35556 | 90 |
val lub_take_eqn = |
91 |
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
|
92 |
|
35556 | 93 |
val thy = Sign.add_path dname thy; |
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
94 |
|
35556 | 95 |
val (lub_take_thm, thy) = |
96 |
yield_singleton PureThy.add_axioms |
|
97 |
((Binding.name "lub_take", lub_take_eqn), []) thy; |
|
23152 | 98 |
|
35556 | 99 |
val thy = Sign.parent_path thy; |
100 |
in |
|
101 |
(lub_take_thm, thy) |
|
102 |
end; |
|
23152 | 103 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
104 |
fun add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
105 |
(dom_eqns : (binding * (typ * typ)) list) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
106 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
107 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
108 |
|
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) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
111 |
fold_map axiomatize_isomorphism dom_eqns thy; |
23152 | 112 |
|
35556 | 113 |
(* define take functions *) |
35517 | 114 |
val (take_info, thy) = |
115 |
Domain_Take_Proofs.define_take_functions |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
116 |
(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
|
117 |
|
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
118 |
(* declare lub_take axioms *) |
35556 | 119 |
val (lub_take_thms, thy) = |
120 |
fold_map axiomatize_lub_take |
|
121 |
(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
|
122 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
123 |
in |
35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35556
diff
changeset
|
124 |
(iso_infos, thy) (* TODO: also return take_info, lub_take_thms *) |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
125 |
end; |
31227 | 126 |
|
23152 | 127 |
end; (* struct *) |