author | huffman |
Mon, 08 Mar 2010 12:21:07 -0800 | |
changeset 35658 | 3d8da9fac424 |
parent 35657 | 0537c34c6067 |
child 35659 | a78bc1930a7a |
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 -> |
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
19 |
(Domain_Take_Proofs.iso_info list |
35658 | 20 |
* Domain_Take_Proofs.take_info |
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
21 |
* Domain_Take_Proofs.take_induct_info) * theory |
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
22 |
end; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
23 |
|
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset
|
24 |
|
33245 | 25 |
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
|
26 |
struct |
23152 | 27 |
|
35556 | 28 |
open HOLCF_Library; |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
29 |
|
35561 | 30 |
infixr 6 ->>; |
31 |
infix -->>; |
|
32 |
infix 9 `; |
|
33 |
||
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
34 |
fun axiomatize_isomorphism |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
35 |
(dbind : binding, (lhsT, rhsT)) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
36 |
(thy : theory) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
37 |
: Domain_Take_Proofs.iso_info * theory = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
38 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
39 |
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
|
40 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
41 |
val abs_bind = Binding.suffix_name "_abs" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
42 |
val rep_bind = Binding.suffix_name "_rep" dbind; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
43 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
44 |
val (abs_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
45 |
Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
46 |
val (rep_const, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
47 |
Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; |
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 x = Free ("x", lhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
50 |
val y = Free ("y", rhsT); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
51 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
52 |
val abs_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
53 |
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
|
54 |
val rep_iso_eqn = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
55 |
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
|
56 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
57 |
val thy = Sign.add_path dname thy; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
58 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
59 |
val (abs_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
60 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
61 |
((Binding.name "abs_iso", abs_iso_eqn), []) thy; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
62 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
63 |
val (rep_iso_thm, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
64 |
yield_singleton PureThy.add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
65 |
((Binding.name "rep_iso", rep_iso_eqn), []) 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 thy = Sign.parent_path thy; |
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 result = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
70 |
{ |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
71 |
absT = lhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
72 |
repT = rhsT, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
73 |
abs_const = abs_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
74 |
rep_const = rep_const, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
75 |
abs_inverse = abs_iso_thm, |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
76 |
rep_inverse = rep_iso_thm |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
77 |
}; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
78 |
in |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
79 |
(result, thy) |
35517 | 80 |
end; |
23152 | 81 |
|
35556 | 82 |
fun axiomatize_lub_take |
83 |
(dbind : binding, take_const : term) |
|
84 |
(thy : theory) |
|
85 |
: thm * theory = |
|
86 |
let |
|
87 |
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
|
88 |
|
35556 | 89 |
val i = Free ("i", natT); |
90 |
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
|
91 |
|
35556 | 92 |
val lub_take_eqn = |
93 |
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
|
94 |
|
35556 | 95 |
val thy = Sign.add_path dname thy; |
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset
|
96 |
|
35556 | 97 |
val (lub_take_thm, thy) = |
98 |
yield_singleton PureThy.add_axioms |
|
99 |
((Binding.name "lub_take", lub_take_eqn), []) thy; |
|
23152 | 100 |
|
35556 | 101 |
val thy = Sign.parent_path thy; |
102 |
in |
|
103 |
(lub_take_thm, thy) |
|
104 |
end; |
|
23152 | 105 |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
106 |
fun add_axioms |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
107 |
(dom_eqns : (binding * (typ * typ)) list) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
108 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
109 |
let |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
110 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
111 |
(* declare and axiomatize abs/rep *) |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
112 |
val (iso_infos, thy) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
113 |
fold_map axiomatize_isomorphism dom_eqns thy; |
23152 | 114 |
|
35556 | 115 |
(* define take functions *) |
35517 | 116 |
val (take_info, thy) = |
117 |
Domain_Take_Proofs.define_take_functions |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
118 |
(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
|
119 |
|
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset
|
120 |
(* declare lub_take axioms *) |
35556 | 121 |
val (lub_take_thms, thy) = |
122 |
fold_map axiomatize_lub_take |
|
123 |
(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
|
124 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
125 |
(* prove additional take theorems *) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
126 |
val (take_info2, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
127 |
Domain_Take_Proofs.add_lub_take_theorems |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
128 |
(map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy; |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35561
diff
changeset
|
129 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33504
diff
changeset
|
130 |
in |
35658 | 131 |
((iso_infos, take_info, take_info2), thy) |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
132 |
end; |
31227 | 133 |
|
23152 | 134 |
end; (* struct *) |