author | wenzelm |
Tue, 13 Mar 2012 20:04:24 +0100 | |
changeset 46909 | 3c73a121a387 |
parent 44241 | 7943b69f0188 |
child 46949 | 94aa7b81bcf6 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/cpodef.ML |
23152 | 2 |
Author: Brian Huffman |
3 |
||
4 |
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style |
|
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31725
diff
changeset
|
5 |
typedef (see also ~~/src/HOL/Tools/typedef.ML). |
23152 | 6 |
*) |
7 |
||
40772 | 8 |
signature CPODEF = |
23152 | 9 |
sig |
33646 | 10 |
type cpo_info = |
11 |
{ below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
|
41028
0acff85f95c7
cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
huffman
parents:
40889
diff
changeset
|
12 |
lub: thm, compact: thm } |
33646 | 13 |
type pcpo_info = |
41029
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
41028
diff
changeset
|
14 |
{ Rep_strict: thm, Abs_strict: thm, |
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
41028
diff
changeset
|
15 |
Rep_bottom_iff: thm, Abs_bottom_iff: thm } |
33646 | 16 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
17 |
val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
33646 | 18 |
term -> (binding * binding) option -> tactic -> theory -> |
19 |
(Typedef.info * thm) * theory |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
20 |
val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
33646 | 21 |
term -> (binding * binding) option -> tactic * tactic -> theory -> |
22 |
(Typedef.info * cpo_info) * theory |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
23 |
val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
33646 | 24 |
term -> (binding * binding) option -> tactic * tactic -> theory -> |
25 |
(Typedef.info * cpo_info * pcpo_info) * theory |
|
26 |
||
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
27 |
val cpodef_proof: (bool * binding) |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
28 |
* (binding * (string * sort) list * mixfix) * term |
33646 | 29 |
* (binding * binding) option -> theory -> Proof.state |
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
30 |
val cpodef_proof_cmd: (bool * binding) |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
31 |
* (binding * (string * string option) list * mixfix) * string |
33646 | 32 |
* (binding * binding) option -> theory -> Proof.state |
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
33 |
val pcpodef_proof: (bool * binding) |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
34 |
* (binding * (string * sort) list * mixfix) * term |
30345 | 35 |
* (binding * binding) option -> theory -> Proof.state |
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
36 |
val pcpodef_proof_cmd: (bool * binding) |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
37 |
* (binding * (string * string option) list * mixfix) * string |
30345 | 38 |
* (binding * binding) option -> theory -> Proof.state |
40832 | 39 |
end |
23152 | 40 |
|
41296
6aaf80ea9715
switch to transparent ascription, to avoid warning messages
huffman
parents:
41029
diff
changeset
|
41 |
structure Cpodef : CPODEF = |
23152 | 42 |
struct |
43 |
||
44 |
(** type definitions **) |
|
45 |
||
33646 | 46 |
type cpo_info = |
47 |
{ below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
|
41028
0acff85f95c7
cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
huffman
parents:
40889
diff
changeset
|
48 |
lub: thm, compact: thm } |
23152 | 49 |
|
33646 | 50 |
type pcpo_info = |
41029
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
41028
diff
changeset
|
51 |
{ Rep_strict: thm, Abs_strict: thm, |
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
41028
diff
changeset
|
52 |
Rep_bottom_iff: thm, Abs_bottom_iff: thm } |
33646 | 53 |
|
54 |
(* building terms *) |
|
23152 | 55 |
|
40832 | 56 |
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT) |
44241 | 57 |
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P |
23152 | 58 |
|
40832 | 59 |
fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT) |
33646 | 60 |
|
61 |
(* manipulating theorems *) |
|
62 |
||
63 |
fun fold_adm_mem thm NONE = thm |
|
64 |
| fold_adm_mem thm (SOME set_def) = |
|
65 |
let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} |
|
40832 | 66 |
in rule OF [set_def, thm] end |
33646 | 67 |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
68 |
fun fold_bottom_mem thm NONE = thm |
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
69 |
| fold_bottom_mem thm (SOME set_def) = |
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
70 |
let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp} |
40832 | 71 |
in rule OF [set_def, thm] end |
33646 | 72 |
|
73 |
(* proving class instances *) |
|
74 |
||
75 |
fun prove_cpo |
|
76 |
(name: binding) |
|
77 |
(newT: typ) |
|
78 |
(Rep_name: binding, Abs_name: binding) |
|
79 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
80 |
(set_def: thm option) (* A == set *) |
|
81 |
(below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
82 |
(admissible: thm) (* adm (%x. x : set) *) |
|
83 |
(thy: theory) |
|
84 |
= |
|
85 |
let |
|
40832 | 86 |
val admissible' = fold_adm_mem admissible set_def |
87 |
val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'] |
|
88 |
val (full_tname, Ts) = dest_Type newT |
|
89 |
val lhs_sorts = map (snd o dest_TFree) Ts |
|
90 |
val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1 |
|
91 |
val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
92 |
(* transfer thms so that they will know about the new cpo instance *) |
40832 | 93 |
val cpo_thms' = map (Thm.transfer thy) cpo_thms |
94 |
fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') |
|
95 |
val cont_Rep = make @{thm typedef_cont_Rep} |
|
96 |
val cont_Abs = make @{thm typedef_cont_Abs} |
|
97 |
val lub = make @{thm typedef_lub} |
|
98 |
val compact = make @{thm typedef_compact} |
|
35902 | 99 |
val (_, thy) = |
100 |
thy |
|
33646 | 101 |
|> Sign.add_path (Binding.name_of name) |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38756
diff
changeset
|
102 |
|> Global_Theory.add_thms |
35902 | 103 |
([((Binding.prefix_name "adm_" name, admissible'), []), |
104 |
((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), |
|
105 |
((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), |
|
106 |
((Binding.prefix_name "lub_" name, lub ), []), |
|
107 |
((Binding.prefix_name "compact_" name, compact ), [])]) |
|
40832 | 108 |
||> Sign.parent_path |
33646 | 109 |
val cpo_info : cpo_info = |
110 |
{ below_def = below_def, adm = admissible', cont_Rep = cont_Rep, |
|
41028
0acff85f95c7
cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
huffman
parents:
40889
diff
changeset
|
111 |
cont_Abs = cont_Abs, lub = lub, compact = compact } |
33646 | 112 |
in |
35902 | 113 |
(cpo_info, thy) |
40832 | 114 |
end |
33646 | 115 |
|
116 |
fun prove_pcpo |
|
117 |
(name: binding) |
|
118 |
(newT: typ) |
|
119 |
(Rep_name: binding, Abs_name: binding) |
|
120 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
121 |
(set_def: thm option) (* A == set *) |
|
122 |
(below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
123 |
(bottom_mem: thm) (* bottom : set *) |
33646 | 124 |
(thy: theory) |
125 |
= |
|
126 |
let |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
127 |
val bottom_mem' = fold_bottom_mem bottom_mem set_def |
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
128 |
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem'] |
40832 | 129 |
val (full_tname, Ts) = dest_Type newT |
130 |
val lhs_sorts = map (snd o dest_TFree) Ts |
|
131 |
val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 |
|
132 |
val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
|
133 |
val pcpo_thms' = map (Thm.transfer thy) pcpo_thms |
|
134 |
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') |
|
135 |
val Rep_strict = make @{thm typedef_Rep_strict} |
|
136 |
val Abs_strict = make @{thm typedef_Abs_strict} |
|
137 |
val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff} |
|
138 |
val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff} |
|
35902 | 139 |
val (_, thy) = |
140 |
thy |
|
33646 | 141 |
|> Sign.add_path (Binding.name_of name) |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38756
diff
changeset
|
142 |
|> Global_Theory.add_thms |
35902 | 143 |
([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []), |
144 |
((Binding.suffix_name "_strict" Abs_name, Abs_strict), []), |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
39557
diff
changeset
|
145 |
((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []), |
41029
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
41028
diff
changeset
|
146 |
((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), [])]) |
40832 | 147 |
||> Sign.parent_path |
33646 | 148 |
val pcpo_info = |
149 |
{ Rep_strict = Rep_strict, Abs_strict = Abs_strict, |
|
41029
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
41028
diff
changeset
|
150 |
Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff } |
33646 | 151 |
in |
35902 | 152 |
(pcpo_info, thy) |
40832 | 153 |
end |
33646 | 154 |
|
155 |
(* prepare_cpodef *) |
|
156 |
||
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
157 |
fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy = |
23152 | 158 |
let |
40832 | 159 |
val _ = Theory.requires thy "Cpodef" "cpodefs" |
30345 | 160 |
|
23152 | 161 |
(*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
|
162 |
val tmp_ctxt = |
42361 | 163 |
Proof_Context.init_global thy |
40832 | 164 |
|> fold (Variable.declare_typ o TFree) raw_args |
165 |
val set = prep_term tmp_ctxt raw_set |
|
166 |
val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
167 |
|
40832 | 168 |
val setT = Term.fastype_of set |
23152 | 169 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
40832 | 170 |
error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT)) |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
171 |
|
33646 | 172 |
(*lhs*) |
42361 | 173 |
val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args |
40832 | 174 |
val full_tname = Sign.full_name thy tname |
175 |
val newT = Type (full_tname, map TFree lhs_tfrees) |
|
33646 | 176 |
|
177 |
val morphs = opt_morphs |
|
40832 | 178 |
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) |
33646 | 179 |
in |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
180 |
(newT, oldT, set, morphs) |
33646 | 181 |
end |
182 |
||
183 |
fun add_podef def opt_name typ set opt_morphs tac thy = |
|
184 |
let |
|
40832 | 185 |
val name = the_default (#1 typ) opt_name |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
186 |
val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy |
40832 | 187 |
|> Typedef.add_typedef_global def opt_name typ set opt_morphs tac |
188 |
val oldT = #rep_type (#1 info) |
|
189 |
val newT = #abs_type (#1 info) |
|
190 |
val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) |
|
33646 | 191 |
|
40832 | 192 |
val RepC = Const (Rep_name, newT --> oldT) |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
193 |
val below_eqn = Logic.mk_equals (below_const newT, |
40832 | 194 |
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))) |
40889 | 195 |
val ((_, (_, below_ldef)), lthy) = thy |
40832 | 196 |
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}) |
33646 | 197 |
|> Specification.definition (NONE, |
46909 | 198 |
((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)) |
42361 | 199 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) |
200 |
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef |
|
40889 | 201 |
val thy = lthy |
202 |
|> Class.prove_instantiation_exit |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
203 |
(K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) |
40889 | 204 |
in ((info, below_def), thy) end |
33646 | 205 |
|
206 |
fun prepare_cpodef |
|
207 |
(prep_term: Proof.context -> 'a -> term) |
|
208 |
(def: bool) |
|
209 |
(name: binding) |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
210 |
(typ: binding * (string * sort) list * mixfix) |
33646 | 211 |
(raw_set: 'a) |
212 |
(opt_morphs: (binding * binding) option) |
|
213 |
(thy: theory) |
|
214 |
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = |
|
215 |
let |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
216 |
val (newT, oldT, set, morphs) = |
40832 | 217 |
prepare prep_term name typ raw_set opt_morphs thy |
33646 | 218 |
|
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
219 |
val goal_nonempty = |
40832 | 220 |
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
221 |
val goal_admissible = |
40832 | 222 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
23152 | 223 |
|
33646 | 224 |
fun cpodef_result nonempty admissible thy = |
28073 | 225 |
let |
40889 | 226 |
val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |
40832 | 227 |
|> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1) |
40889 | 228 |
val (cpo_info, thy) = thy |
40832 | 229 |
|> prove_cpo name newT morphs type_definition set_def below_def admissible |
23152 | 230 |
in |
40889 | 231 |
((info, cpo_info), thy) |
40832 | 232 |
end |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
233 |
in |
33646 | 234 |
(goal_nonempty, goal_admissible, cpodef_result) |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
235 |
end |
30345 | 236 |
handle ERROR msg => |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42361
diff
changeset
|
237 |
cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print name) |
23152 | 238 |
|
33646 | 239 |
fun prepare_pcpodef |
240 |
(prep_term: Proof.context -> 'a -> term) |
|
241 |
(def: bool) |
|
242 |
(name: binding) |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
243 |
(typ: binding * (string * sort) list * mixfix) |
33646 | 244 |
(raw_set: 'a) |
245 |
(opt_morphs: (binding * binding) option) |
|
246 |
(thy: theory) |
|
247 |
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
|
248 |
let |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
249 |
val (newT, oldT, set, morphs) = |
40832 | 250 |
prepare prep_term name typ raw_set opt_morphs thy |
33646 | 251 |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
252 |
val goal_bottom_mem = |
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
253 |
HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set)) |
33646 | 254 |
|
255 |
val goal_admissible = |
|
40832 | 256 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
33646 | 257 |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
258 |
fun pcpodef_result bottom_mem admissible thy = |
33646 | 259 |
let |
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
260 |
val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1 |
40889 | 261 |
val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |
40832 | 262 |
|> add_podef def (SOME name) typ set opt_morphs tac |
40889 | 263 |
val (cpo_info, thy) = thy |
40832 | 264 |
|> prove_cpo name newT morphs type_definition set_def below_def admissible |
40889 | 265 |
val (pcpo_info, thy) = thy |
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
266 |
|> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem |
33646 | 267 |
in |
40889 | 268 |
((info, cpo_info, pcpo_info), thy) |
40832 | 269 |
end |
33646 | 270 |
in |
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
271 |
(goal_bottom_mem, goal_admissible, pcpodef_result) |
33646 | 272 |
end |
273 |
handle ERROR msg => |
|
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42361
diff
changeset
|
274 |
cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print name) |
33646 | 275 |
|
23152 | 276 |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
277 |
(* tactic interface *) |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
278 |
|
33646 | 279 |
fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy = |
280 |
let |
|
40832 | 281 |
val name = the_default (#1 typ) opt_name |
33646 | 282 |
val (goal1, goal2, cpodef_result) = |
40832 | 283 |
prepare_cpodef Syntax.check_term def name typ set opt_morphs thy |
33646 | 284 |
val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
285 |
handle ERROR msg => cat_error msg |
|
40832 | 286 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
33646 | 287 |
val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
288 |
handle ERROR msg => cat_error msg |
|
40832 | 289 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
290 |
in cpodef_result thm1 thm2 thy end |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
291 |
|
33646 | 292 |
fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy = |
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
293 |
let |
40832 | 294 |
val name = the_default (#1 typ) opt_name |
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
295 |
val (goal1, goal2, pcpodef_result) = |
40832 | 296 |
prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy |
33646 | 297 |
val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
298 |
handle ERROR msg => cat_error msg |
40832 | 299 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
33646 | 300 |
val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
301 |
handle ERROR msg => cat_error msg |
40832 | 302 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
303 |
in pcpodef_result thm1 thm2 thy end |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
304 |
|
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
305 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
306 |
(* proof interface *) |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
307 |
|
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
308 |
local |
23152 | 309 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
310 |
fun gen_cpodef_proof prep_term prep_constraint |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
311 |
((def, name), (b, raw_args, mx), set, opt_morphs) thy = |
23152 | 312 |
let |
42361 | 313 |
val ctxt = Proof_Context.init_global thy |
40832 | 314 |
val args = map (apsnd (prep_constraint ctxt)) raw_args |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
315 |
val (goal1, goal2, make_result) = |
40832 | 316 |
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy |
42361 | 317 |
fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
40832 | 318 |
| after_qed _ = raise Fail "cpodef_proof" |
319 |
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
|
33646 | 320 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
321 |
fun gen_pcpodef_proof prep_term prep_constraint |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
322 |
((def, name), (b, raw_args, mx), set, opt_morphs) thy = |
33646 | 323 |
let |
42361 | 324 |
val ctxt = Proof_Context.init_global thy |
40832 | 325 |
val args = map (apsnd (prep_constraint ctxt)) raw_args |
33646 | 326 |
val (goal1, goal2, make_result) = |
40832 | 327 |
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy |
42361 | 328 |
fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
40832 | 329 |
| after_qed _ = raise Fail "pcpodef_proof" |
330 |
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
|
23152 | 331 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
332 |
in |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
333 |
|
40832 | 334 |
fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x |
335 |
fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x |
|
23152 | 336 |
|
40832 | 337 |
fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x |
338 |
fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
339 |
|
40832 | 340 |
end |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
341 |
|
23152 | 342 |
|
343 |
||
344 |
(** outer syntax **) |
|
345 |
||
346 |
val typedef_proof_decl = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
347 |
Scan.optional (Parse.$$$ "(" |-- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
348 |
((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding || |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
349 |
Parse.binding >> (fn s => (true, SOME s))) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
350 |
--| Parse.$$$ ")") (true, NONE) -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
351 |
(Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
352 |
(Parse.$$$ "=" |-- Parse.term) -- |
40832 | 353 |
Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)) |
23152 | 354 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
355 |
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) = |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
356 |
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
40832 | 357 |
((def, the_default t opt_name), (t, args, mx), A, morphs) |
23152 | 358 |
|
24867 | 359 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
360 |
Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
361 |
Keyword.thy_goal |
23152 | 362 |
(typedef_proof_decl >> |
40832 | 363 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))) |
23152 | 364 |
|
24867 | 365 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
366 |
Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
367 |
Keyword.thy_goal |
23152 | 368 |
(typedef_proof_decl >> |
40832 | 369 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))) |
23152 | 370 |
|
40832 | 371 |
end |