author | wenzelm |
Mon, 06 Apr 2015 17:06:48 +0200 | |
changeset 59936 | b8ffc3dc9e24 |
parent 58959 | 1f195ed99941 |
child 60754 | 02924903a6fd |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/domaindef.ML |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
3 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
4 |
Defining representable domains using algebraic deflations. |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
5 |
*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
6 |
|
40575 | 7 |
signature DOMAINDEF = |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
8 |
sig |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
9 |
type rep_info = |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
10 |
{ |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
11 |
emb_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
12 |
prj_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
13 |
defl_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
14 |
liftemb_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
15 |
liftprj_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
16 |
liftdefl_def : thm, |
40494
db8a09daba7b
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
huffman
parents:
40491
diff
changeset
|
17 |
DEFL : thm |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
18 |
} |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
19 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
20 |
val add_domaindef: binding * (string * sort) list * mixfix -> |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
21 |
term -> (binding * binding) option -> theory -> |
40772 | 22 |
(Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
23 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
24 |
val domaindef_cmd: (binding * (string * string option) list * mixfix) * string |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
25 |
* (binding * binding) option -> theory -> theory |
40832 | 26 |
end |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
27 |
|
41296
6aaf80ea9715
switch to transparent ascription, to avoid warning messages
huffman
parents:
41292
diff
changeset
|
28 |
structure Domaindef : DOMAINDEF = |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
29 |
struct |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
30 |
|
40832 | 31 |
open HOLCF_Library |
35527 | 32 |
|
40832 | 33 |
infixr 6 ->> |
34 |
infix -->> |
|
35527 | 35 |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
36 |
(** type definitions **) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
37 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
38 |
type rep_info = |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
39 |
{ |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
40 |
emb_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
41 |
prj_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
42 |
defl_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
43 |
liftemb_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
44 |
liftprj_def : thm, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
45 |
liftdefl_def : thm, |
40494
db8a09daba7b
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
huffman
parents:
40491
diff
changeset
|
46 |
DEFL : thm |
40832 | 47 |
} |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
48 |
|
35527 | 49 |
(* building types and terms *) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
50 |
|
40832 | 51 |
val udomT = @{typ udom} |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41228
diff
changeset
|
52 |
val deflT = @{typ "udom defl"} |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
53 |
val udeflT = @{typ "udom u defl"} |
40832 | 54 |
fun emb_const T = Const (@{const_name emb}, T ->> udomT) |
55 |
fun prj_const T = Const (@{const_name prj}, udomT ->> T) |
|
56 |
fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT) |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
57 |
fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> mk_upT udomT) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
58 |
fun liftprj_const T = Const (@{const_name liftprj}, mk_upT udomT ->> mk_upT T) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
59 |
fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
60 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
61 |
fun mk_u_map t = |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
62 |
let |
40832 | 63 |
val (T, U) = dest_cfunT (fastype_of t) |
64 |
val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U) |
|
65 |
val u_map_const = Const (@{const_name u_map}, u_map_type) |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
66 |
in |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
67 |
mk_capply (u_map_const, t) |
40832 | 68 |
end |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
69 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
70 |
fun mk_cast (t, x) = |
35527 | 71 |
capply_const (udomT, udomT) |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41228
diff
changeset
|
72 |
$ (capply_const (deflT, udomT ->> udomT) $ @{term "cast :: udom defl -> udom -> udom"} $ t) |
40832 | 73 |
$ x |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
74 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
75 |
(* manipulating theorems *) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
76 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
77 |
(* proving class instances *) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
78 |
|
40575 | 79 |
fun gen_add_domaindef |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
80 |
(prep_term: Proof.context -> 'a -> term) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
81 |
(typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
82 |
(raw_defl: 'a) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
83 |
(opt_morphs: (binding * binding) option) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
84 |
(thy: theory) |
40772 | 85 |
: (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory = |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
86 |
let |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
87 |
(*rhs*) |
36153
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35994
diff
changeset
|
88 |
val tmp_ctxt = |
42361 | 89 |
Proof_Context.init_global thy |
40832 | 90 |
|> fold (Variable.declare_typ o TFree) raw_args |
91 |
val defl = prep_term tmp_ctxt raw_defl |
|
92 |
val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35527
diff
changeset
|
93 |
|
40832 | 94 |
val deflT = Term.fastype_of defl |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41228
diff
changeset
|
95 |
val _ = if deflT = @{typ "udom defl"} then () |
40832 | 96 |
else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
97 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
98 |
(*lhs*) |
42361 | 99 |
val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args |
40832 | 100 |
val full_tname = Sign.full_name thy tname |
101 |
val newT = Type (full_tname, map TFree lhs_tfrees) |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
102 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
103 |
(*morphisms*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
104 |
val morphs = opt_morphs |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
105 |
|> the_default (Binding.prefix_name "Rep_" tname, Binding.prefix_name "Abs_" tname) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
106 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
107 |
(*set*) |
44169 | 108 |
val set = @{term "defl_set :: udom defl => udom set"} $ defl |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
109 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
110 |
(*pcpodef*) |
58959 | 111 |
fun tac1 _ = rtac @{thm defl_set_bottom} 1 |
112 |
fun tac2 _ = rtac @{thm adm_defl_set} 1 |
|
35904 | 113 |
val ((info, cpo_info, pcpo_info), thy) = thy |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
114 |
|> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
115 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
116 |
(*definitions*) |
40832 | 117 |
val Rep_const = Const (#Rep_name (#1 info), newT --> udomT) |
118 |
val Abs_const = Const (#Abs_name (#1 info), udomT --> newT) |
|
119 |
val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const) |
|
35527 | 120 |
val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $ |
40832 | 121 |
Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
122 |
val defl_eqn = Logic.mk_equals (defl_const newT, |
40832 | 123 |
Abs ("x", Term.itselfT newT, defl)) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
124 |
val liftemb_eqn = |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
125 |
Logic.mk_equals (liftemb_const newT, mk_u_map (emb_const newT)) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
126 |
val liftprj_eqn = |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
127 |
Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT)) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
128 |
val liftdefl_eqn = |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
129 |
Logic.mk_equals (liftdefl_const newT, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
130 |
Abs ("t", Term.itselfT newT, |
41436 | 131 |
mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT))) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
132 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
133 |
val name_def = Thm.def_binding tname |
40832 | 134 |
val emb_bind = (Binding.prefix_name "emb_" name_def, []) |
135 |
val prj_bind = (Binding.prefix_name "prj_" name_def, []) |
|
136 |
val defl_bind = (Binding.prefix_name "defl_" name_def, []) |
|
137 |
val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, []) |
|
138 |
val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []) |
|
139 |
val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []) |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
140 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
141 |
(*instantiate class rep*) |
35904 | 142 |
val lthy = thy |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
143 |
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain}) |
35904 | 144 |
val ((_, (_, emb_ldef)), lthy) = |
40832 | 145 |
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy |
35904 | 146 |
val ((_, (_, prj_ldef)), lthy) = |
40832 | 147 |
Specification.definition (NONE, (prj_bind, prj_eqn)) lthy |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
148 |
val ((_, (_, defl_ldef)), lthy) = |
40832 | 149 |
Specification.definition (NONE, (defl_bind, defl_eqn)) lthy |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
150 |
val ((_, (_, liftemb_ldef)), lthy) = |
40832 | 151 |
Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
152 |
val ((_, (_, liftprj_ldef)), lthy) = |
40832 | 153 |
Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
154 |
val ((_, (_, liftdefl_ldef)), lthy) = |
40832 | 155 |
Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy |
42361 | 156 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) |
157 |
val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef |
|
158 |
val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef |
|
159 |
val defl_def = singleton (Proof_Context.export lthy ctxt_thy) defl_ldef |
|
160 |
val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef |
|
161 |
val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef |
|
162 |
val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
163 |
val typedef_thms = |
49833 | 164 |
[#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def, |
40832 | 165 |
liftemb_def, liftprj_def, liftdefl_def] |
35904 | 166 |
val thy = lthy |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
167 |
|> Class.prove_instantiation_instance |
52732 | 168 |
(K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1)) |
40832 | 169 |
|> Local_Theory.exit_global |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
170 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
171 |
(*other theorems*) |
40832 | 172 |
val defl_thm' = Thm.transfer thy defl_def |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
173 |
val (DEFL_thm, thy) = thy |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
174 |
|> Sign.add_path (Binding.name_of tname) |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38348
diff
changeset
|
175 |
|> Global_Theory.add_thm |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
176 |
((Binding.prefix_name "DEFL_" tname, |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
177 |
Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), []) |
40832 | 178 |
||> Sign.restore_naming thy |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
179 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
180 |
val rep_info = |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
181 |
{ emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40038
diff
changeset
|
182 |
liftemb_def = liftemb_def, liftprj_def = liftprj_def, |
40832 | 183 |
liftdefl_def = liftdefl_def, DEFL = DEFL_thm } |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
184 |
in |
35904 | 185 |
((info, cpo_info, pcpo_info, rep_info), thy) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
186 |
end |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
187 |
handle ERROR msg => |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
188 |
cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
189 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
190 |
fun add_domaindef typ defl opt_morphs thy = |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
191 |
gen_add_domaindef Syntax.check_term typ defl opt_morphs thy |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
192 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
193 |
fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy = |
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35527
diff
changeset
|
194 |
let |
42361 | 195 |
val ctxt = Proof_Context.init_global thy |
40832 | 196 |
val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
197 |
in snd (gen_add_domaindef Syntax.read_term (b, args, mx) A morphs thy) end |
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35527
diff
changeset
|
198 |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
199 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
200 |
(** outer syntax **) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
201 |
|
40575 | 202 |
val domaindef_decl = |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
203 |
(Parse.type_args_constrained -- Parse.binding) -- |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
204 |
Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) -- |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
205 |
Scan.option |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
206 |
(@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
207 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
208 |
fun mk_domaindef (((((args, t)), mx), A), morphs) = |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
209 |
domaindef_cmd ((t, args, mx), A, morphs) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
210 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
211 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
58959
diff
changeset
|
212 |
Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations" |
56895
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56249
diff
changeset
|
213 |
(domaindef_decl >> (Toplevel.theory o mk_domaindef)) |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
214 |
|
40832 | 215 |
end |