author | huffman |
Fri, 20 Nov 2009 15:29:56 -0800 | |
changeset 33826 | 7f12ab745298 |
parent 33812 | 10c335383c8b |
child 35021 | c839a4c670c6 |
permissions | -rw-r--r-- |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
1 |
(* Title: HOLCF/Tools/repdef.ML |
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 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
7 |
signature REPDEF = |
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 = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
10 |
{ emb_def: thm, prj_def: thm, approx_def: thm, REP: thm } |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
11 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
12 |
val add_repdef: bool -> binding option -> binding * string list * mixfix -> |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
13 |
term -> (binding * binding) option -> theory -> |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
14 |
(Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
15 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
16 |
val repdef_cmd: (bool * binding) * (binding * string list * mixfix) * string |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
17 |
* (binding * binding) option -> theory -> theory |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
18 |
end; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
19 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
20 |
structure Repdef :> REPDEF = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
21 |
struct |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
22 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
23 |
(** type definitions **) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
24 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
25 |
type rep_info = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
26 |
{ emb_def: thm, prj_def: thm, approx_def: thm, REP: thm }; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
27 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
28 |
(* building terms *) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
29 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
30 |
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
31 |
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
32 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
33 |
fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
34 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
35 |
val natT = @{typ nat}; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
36 |
val udomT = @{typ udom}; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
37 |
fun alg_deflT T = Type (@{type_name alg_defl}, [T]); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
38 |
fun cfunT (T, U) = Type (@{type_name "->"}, [T, U]); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
39 |
fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
40 |
fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
41 |
fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
42 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
43 |
fun LAM_const (T, U) = Const (@{const_name Abs_CFun}, (T --> U) --> cfunT (T, U)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
44 |
fun APP_const (T, U) = Const (@{const_name Rep_CFun}, cfunT (T, U) --> (T --> U)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
45 |
fun cast_const T = Const (@{const_name cast}, cfunT (alg_deflT T, cfunT (T, T))); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
46 |
fun mk_cast (t, x) = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
47 |
APP_const (udomT, udomT) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
48 |
$ (APP_const (alg_deflT udomT, cfunT (udomT, udomT)) $ cast_const udomT $ t) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
49 |
$ x; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
50 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
51 |
(* manipulating theorems *) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
52 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
53 |
(* proving class instances *) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
54 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
55 |
fun declare_type_name a = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
56 |
Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
57 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
58 |
fun gen_add_repdef |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
59 |
(prep_term: Proof.context -> 'a -> term) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
60 |
(def: bool) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
61 |
(name: binding) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
62 |
(typ as (t, vs, mx) : binding * string list * mixfix) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
63 |
(raw_defl: 'a) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
64 |
(opt_morphs: (binding * binding) option) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
65 |
(thy: theory) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
66 |
: (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
67 |
let |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
68 |
val _ = Theory.requires thy "Representable" "repdefs"; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
69 |
val ctxt = ProofContext.init thy; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
70 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
71 |
(*rhs*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
72 |
val defl = prep_term (ctxt |> fold declare_type_name vs) raw_defl; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
73 |
val deflT = Term.fastype_of defl; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
74 |
val _ = if deflT = @{typ "udom alg_defl"} then () |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
75 |
else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ ctxt deflT)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
76 |
val rhs_tfrees = Term.add_tfrees defl []; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
77 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
78 |
(*lhs*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
79 |
val defS = Sign.defaultS thy; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
80 |
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
81 |
val lhs_sorts = map snd lhs_tfrees; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
82 |
val tname = Binding.map_name (Syntax.type_name mx) t; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
83 |
val full_tname = Sign.full_name thy tname; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
84 |
val newT = Type (full_tname, map TFree lhs_tfrees); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
85 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
86 |
(*morphisms*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
87 |
val morphs = opt_morphs |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
88 |
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
89 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
90 |
(*set*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
91 |
val in_defl = @{term "in_deflation :: udom => udom alg_defl => bool"}; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
92 |
val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
93 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
94 |
(*pcpodef*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
95 |
val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
96 |
val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
97 |
val ((info, cpo_info, pcpo_info), thy2) = thy |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
98 |
|> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
99 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
100 |
(*definitions*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
101 |
val Rep_const = Const (#Rep_name info, newT --> udomT); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
102 |
val Abs_const = Const (#Abs_name info, udomT --> newT); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
103 |
val emb_eqn = Logic.mk_equals (emb_const newT, LAM_const (newT, udomT) $ Rep_const); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
104 |
val prj_eqn = Logic.mk_equals (prj_const newT, LAM_const (udomT, newT) $ |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
105 |
Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
106 |
val repdef_approx_const = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
107 |
Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
108 |
--> alg_deflT udomT --> natT --> cfunT (newT, newT)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
109 |
val approx_eqn = Logic.mk_equals (approx_const newT, |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
110 |
repdef_approx_const $ Rep_const $ Abs_const $ defl); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
111 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
112 |
(*instantiate class rep*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
113 |
val name_def = Binding.suffix_name "_def" name; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
114 |
val ([emb_ldef, prj_ldef, approx_ldef], lthy3) = thy2 |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
115 |
|> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep}) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
116 |
|> fold_map Specification.definition |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
117 |
[ (NONE, ((Binding.prefix_name "emb_" name_def, []), emb_eqn)) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
118 |
, (NONE, ((Binding.prefix_name "prj_" name_def, []), prj_eqn)) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
119 |
, (NONE, ((Binding.prefix_name "approx_" name_def, []), approx_eqn)) ] |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
120 |
|>> map (snd o snd); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
121 |
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy3); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
122 |
val [emb_def, prj_def, approx_def] = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
123 |
ProofContext.export lthy3 ctxt_thy [emb_ldef, prj_ldef, approx_ldef]; |
33826 | 124 |
val type_definition_thm = |
125 |
MetaSimplifier.rewrite_rule |
|
126 |
(the_list (#set_def info)) |
|
127 |
(#type_definition info); |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
128 |
val typedef_thms = |
33826 | 129 |
[type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
130 |
val thy4 = lthy3 |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
131 |
|> Class.prove_instantiation_instance |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
132 |
(K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) |
33681 | 133 |
|> Local_Theory.exit_global; |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
134 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
135 |
(*other theorems*) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
136 |
val typedef_thms' = map (Thm.transfer thy4) |
33826 | 137 |
[type_definition_thm, #below_def cpo_info, emb_def, prj_def]; |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
138 |
val ([REP_thm], thy5) = thy4 |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
139 |
|> Sign.add_path (Binding.name_of name) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
140 |
|> PureThy.add_thms |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
141 |
[((Binding.prefix_name "REP_" name, |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
142 |
Drule.standard (@{thm typedef_REP} OF typedef_thms')), [])] |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
143 |
||> Sign.parent_path; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
144 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
145 |
val rep_info = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
146 |
{ emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
147 |
in |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
148 |
((info, cpo_info, pcpo_info, rep_info), thy5) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
149 |
end |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
150 |
handle ERROR msg => |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
151 |
cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
152 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
153 |
fun add_repdef def opt_name typ defl opt_morphs thy = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
154 |
let |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
155 |
val name = the_default (#1 typ) opt_name; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
156 |
in |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
157 |
gen_add_repdef Syntax.check_term def name typ defl opt_morphs thy |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
158 |
end; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
159 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
160 |
fun repdef_cmd ((def, name), typ, A, morphs) = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
161 |
snd o gen_add_repdef Syntax.read_term def name typ A morphs; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
162 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
163 |
(** outer syntax **) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
164 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
165 |
local structure P = OuterParse and K = OuterKeyword in |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
166 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
167 |
val repdef_decl = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
168 |
Scan.optional (P.$$$ "(" |-- |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
169 |
((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
170 |
--| P.$$$ ")") (true, NONE) -- |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
171 |
(P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
172 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
173 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
174 |
fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
175 |
repdef_cmd |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
176 |
((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
177 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
178 |
val _ = |
33812 | 179 |
OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
180 |
(repdef_decl >> |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
181 |
(Toplevel.print oo (Toplevel.theory o mk_repdef))); |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
182 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
183 |
end; |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
184 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
diff
changeset
|
185 |
end; |