|
1 (* Title: HOLCF/Tools/Domain/domain_axioms.ML |
|
2 Author: David von Oheimb |
|
3 Author: Brian Huffman |
|
4 |
|
5 Syntax generator for domain command. |
|
6 *) |
|
7 |
|
8 signature DOMAIN_AXIOMS = |
|
9 sig |
|
10 val axiomatize_isomorphism : |
|
11 binding * (typ * typ) -> |
|
12 theory -> Domain_Take_Proofs.iso_info * theory |
|
13 |
|
14 val axiomatize_lub_take : |
|
15 binding * term -> theory -> thm * theory |
|
16 |
|
17 val add_axioms : |
|
18 (binding * mixfix * (typ * typ)) list -> theory -> |
|
19 (Domain_Take_Proofs.iso_info list |
|
20 * Domain_Take_Proofs.take_induct_info) * theory |
|
21 end; |
|
22 |
|
23 |
|
24 structure Domain_Axioms : DOMAIN_AXIOMS = |
|
25 struct |
|
26 |
|
27 open HOLCF_Library; |
|
28 |
|
29 infixr 6 ->>; |
|
30 infix -->>; |
|
31 infix 9 `; |
|
32 |
|
33 fun axiomatize_isomorphism |
|
34 (dbind : binding, (lhsT, rhsT)) |
|
35 (thy : theory) |
|
36 : Domain_Take_Proofs.iso_info * theory = |
|
37 let |
|
38 val abs_bind = Binding.suffix_name "_abs" dbind; |
|
39 val rep_bind = Binding.suffix_name "_rep" dbind; |
|
40 |
|
41 val (abs_const, thy) = |
|
42 Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; |
|
43 val (rep_const, thy) = |
|
44 Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; |
|
45 |
|
46 val x = Free ("x", lhsT); |
|
47 val y = Free ("y", rhsT); |
|
48 |
|
49 val abs_iso_eqn = |
|
50 Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y))); |
|
51 val rep_iso_eqn = |
|
52 Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))); |
|
53 |
|
54 val abs_iso_bind = Binding.qualified true "abs_iso" dbind; |
|
55 val rep_iso_bind = Binding.qualified true "rep_iso" dbind; |
|
56 |
|
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; |
|
59 |
|
60 val result = |
|
61 { |
|
62 absT = lhsT, |
|
63 repT = rhsT, |
|
64 abs_const = abs_const, |
|
65 rep_const = rep_const, |
|
66 abs_inverse = Drule.export_without_context abs_iso_thm, |
|
67 rep_inverse = Drule.export_without_context rep_iso_thm |
|
68 }; |
|
69 in |
|
70 (result, thy) |
|
71 end; |
|
72 |
|
73 fun axiomatize_lub_take |
|
74 (dbind : binding, take_const : term) |
|
75 (thy : theory) |
|
76 : thm * theory = |
|
77 let |
|
78 val i = Free ("i", natT); |
|
79 val T = (fst o dest_cfunT o range_type o fastype_of) take_const; |
|
80 |
|
81 val lub_take_eqn = |
|
82 mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)); |
|
83 |
|
84 val lub_take_bind = Binding.qualified true "lub_take" dbind; |
|
85 |
|
86 val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy; |
|
87 in |
|
88 (lub_take_thm, thy) |
|
89 end; |
|
90 |
|
91 fun add_axioms |
|
92 (dom_eqns : (binding * mixfix * (typ * typ)) list) |
|
93 (thy : theory) = |
|
94 let |
|
95 |
|
96 val dbinds = map #1 dom_eqns; |
|
97 |
|
98 (* declare new types *) |
|
99 fun thy_type (dbind, mx, (lhsT, _)) = |
|
100 (dbind, (length o snd o dest_Type) lhsT, mx); |
|
101 val thy = Sign.add_types (map thy_type dom_eqns) thy; |
|
102 |
|
103 (* axiomatize type constructor arities *) |
|
104 fun thy_arity (_, _, (lhsT, _)) = |
|
105 let val (dname, tvars) = dest_Type lhsT; |
|
106 in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end; |
|
107 val thy = fold (AxClass.axiomatize_arity o thy_arity) dom_eqns thy; |
|
108 |
|
109 (* declare and axiomatize abs/rep *) |
|
110 val (iso_infos, thy) = |
|
111 fold_map axiomatize_isomorphism |
|
112 (map (fn (dbind, _, eqn) => (dbind, eqn)) dom_eqns) thy; |
|
113 |
|
114 (* define take functions *) |
|
115 val (take_info, thy) = |
|
116 Domain_Take_Proofs.define_take_functions |
|
117 (dbinds ~~ iso_infos) thy; |
|
118 |
|
119 (* declare lub_take axioms *) |
|
120 val (lub_take_thms, thy) = |
|
121 fold_map axiomatize_lub_take |
|
122 (dbinds ~~ #take_consts take_info) thy; |
|
123 |
|
124 (* prove additional take theorems *) |
|
125 val (take_info2, thy) = |
|
126 Domain_Take_Proofs.add_lub_take_theorems |
|
127 (dbinds ~~ iso_infos) take_info lub_take_thms thy; |
|
128 |
|
129 (* define map functions *) |
|
130 val (map_info, thy) = |
|
131 Domain_Isomorphism.define_map_functions |
|
132 (dbinds ~~ iso_infos) thy; |
|
133 |
|
134 in |
|
135 ((iso_infos, take_info2), thy) |
|
136 end; |
|
137 |
|
138 end; (* struct *) |