author | wenzelm |
Fri, 12 Oct 2012 15:08:29 +0200 | |
changeset 49833 | 1d80798e8d8a |
parent 49759 | ecf1d5d87e5e |
child 49835 | 31f32ec4d766 |
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 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
17 |
val add_podef: binding * (string * sort) list * mixfix -> |
33646 | 18 |
term -> (binding * binding) option -> tactic -> theory -> |
19 |
(Typedef.info * thm) * theory |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
20 |
val add_cpodef: binding * (string * sort) list * mixfix -> |
33646 | 21 |
term -> (binding * binding) option -> tactic * tactic -> theory -> |
22 |
(Typedef.info * cpo_info) * theory |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
23 |
val add_pcpodef: binding * (string * sort) list * mixfix -> |
33646 | 24 |
term -> (binding * binding) option -> tactic * tactic -> theory -> |
25 |
(Typedef.info * cpo_info * pcpo_info) * theory |
|
26 |
||
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
27 |
val cpodef_proof: |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
28 |
(binding * (string * sort) list * mixfix) * term |
33646 | 29 |
* (binding * binding) option -> theory -> Proof.state |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
30 |
val cpodef_proof_cmd: |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
31 |
(binding * (string * string option) list * mixfix) * string |
33646 | 32 |
* (binding * binding) option -> theory -> Proof.state |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
33 |
val pcpodef_proof: |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
34 |
(binding * (string * sort) list * mixfix) * term |
30345 | 35 |
* (binding * binding) option -> theory -> Proof.state |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
36 |
val pcpodef_proof_cmd: |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
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 |
(* proving class instances *) |
|
62 |
||
63 |
fun prove_cpo |
|
64 |
(name: binding) |
|
65 |
(newT: typ) |
|
66 |
(Rep_name: binding, Abs_name: binding) |
|
67 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
68 |
(below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
69 |
(admissible: thm) (* adm (%x. x : set) *) |
|
70 |
(thy: theory) |
|
71 |
= |
|
72 |
let |
|
49833 | 73 |
val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] |
40832 | 74 |
val (full_tname, Ts) = dest_Type newT |
75 |
val lhs_sorts = map (snd o dest_TFree) Ts |
|
76 |
val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1 |
|
77 |
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
|
78 |
(* transfer thms so that they will know about the new cpo instance *) |
40832 | 79 |
val cpo_thms' = map (Thm.transfer thy) cpo_thms |
80 |
fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') |
|
81 |
val cont_Rep = make @{thm typedef_cont_Rep} |
|
82 |
val cont_Abs = make @{thm typedef_cont_Abs} |
|
83 |
val lub = make @{thm typedef_lub} |
|
84 |
val compact = make @{thm typedef_compact} |
|
35902 | 85 |
val (_, thy) = |
86 |
thy |
|
33646 | 87 |
|> 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
|
88 |
|> Global_Theory.add_thms |
49833 | 89 |
([((Binding.prefix_name "adm_" name, admissible), []), |
90 |
((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), |
|
91 |
((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), |
|
92 |
((Binding.prefix_name "lub_" name, lub ), []), |
|
93 |
((Binding.prefix_name "compact_" name, compact ), [])]) |
|
40832 | 94 |
||> Sign.parent_path |
33646 | 95 |
val cpo_info : cpo_info = |
49833 | 96 |
{ 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
|
97 |
cont_Abs = cont_Abs, lub = lub, compact = compact } |
33646 | 98 |
in |
35902 | 99 |
(cpo_info, thy) |
40832 | 100 |
end |
33646 | 101 |
|
102 |
fun prove_pcpo |
|
103 |
(name: binding) |
|
104 |
(newT: typ) |
|
105 |
(Rep_name: binding, Abs_name: binding) |
|
106 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
107 |
(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
|
108 |
(bottom_mem: thm) (* bottom : set *) |
33646 | 109 |
(thy: theory) |
110 |
= |
|
111 |
let |
|
49833 | 112 |
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] |
40832 | 113 |
val (full_tname, Ts) = dest_Type newT |
114 |
val lhs_sorts = map (snd o dest_TFree) Ts |
|
115 |
val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 |
|
116 |
val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
|
117 |
val pcpo_thms' = map (Thm.transfer thy) pcpo_thms |
|
118 |
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') |
|
119 |
val Rep_strict = make @{thm typedef_Rep_strict} |
|
120 |
val Abs_strict = make @{thm typedef_Abs_strict} |
|
121 |
val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff} |
|
122 |
val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff} |
|
35902 | 123 |
val (_, thy) = |
124 |
thy |
|
33646 | 125 |
|> 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
|
126 |
|> Global_Theory.add_thms |
35902 | 127 |
([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []), |
128 |
((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
|
129 |
((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
|
130 |
((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), [])]) |
40832 | 131 |
||> Sign.parent_path |
33646 | 132 |
val pcpo_info = |
133 |
{ 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
|
134 |
Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff } |
33646 | 135 |
in |
35902 | 136 |
(pcpo_info, thy) |
40832 | 137 |
end |
33646 | 138 |
|
139 |
(* prepare_cpodef *) |
|
140 |
||
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
141 |
fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy = |
23152 | 142 |
let |
40832 | 143 |
val _ = Theory.requires thy "Cpodef" "cpodefs" |
30345 | 144 |
|
23152 | 145 |
(*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
|
146 |
val tmp_ctxt = |
42361 | 147 |
Proof_Context.init_global thy |
40832 | 148 |
|> fold (Variable.declare_typ o TFree) raw_args |
149 |
val set = prep_term tmp_ctxt raw_set |
|
150 |
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
|
151 |
|
40832 | 152 |
val setT = Term.fastype_of set |
23152 | 153 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
40832 | 154 |
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
|
155 |
|
33646 | 156 |
(*lhs*) |
42361 | 157 |
val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args |
40832 | 158 |
val full_tname = Sign.full_name thy tname |
159 |
val newT = Type (full_tname, map TFree lhs_tfrees) |
|
33646 | 160 |
|
161 |
val morphs = opt_morphs |
|
40832 | 162 |
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) |
33646 | 163 |
in |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
164 |
(newT, oldT, set, morphs) |
33646 | 165 |
end |
166 |
||
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
167 |
fun add_podef typ set opt_morphs tac thy = |
33646 | 168 |
let |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
169 |
val name = #1 typ |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
170 |
val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy |
49833 | 171 |
|> Typedef.add_typedef_global NONE typ set opt_morphs tac |
40832 | 172 |
val oldT = #rep_type (#1 info) |
173 |
val newT = #abs_type (#1 info) |
|
174 |
val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) |
|
33646 | 175 |
|
40832 | 176 |
val RepC = Const (Rep_name, newT --> oldT) |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
177 |
val below_eqn = Logic.mk_equals (below_const newT, |
40832 | 178 |
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))) |
40889 | 179 |
val ((_, (_, below_ldef)), lthy) = thy |
40832 | 180 |
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}) |
33646 | 181 |
|> Specification.definition (NONE, |
46909 | 182 |
((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)) |
42361 | 183 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) |
184 |
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef |
|
40889 | 185 |
val thy = lthy |
186 |
|> Class.prove_instantiation_exit |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
187 |
(K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) |
40889 | 188 |
in ((info, below_def), thy) end |
33646 | 189 |
|
190 |
fun prepare_cpodef |
|
191 |
(prep_term: Proof.context -> 'a -> term) |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
192 |
(typ: binding * (string * sort) list * mixfix) |
33646 | 193 |
(raw_set: 'a) |
194 |
(opt_morphs: (binding * binding) option) |
|
195 |
(thy: theory) |
|
196 |
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = |
|
197 |
let |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
198 |
val name = #1 typ |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
199 |
val (newT, oldT, set, morphs) = |
40832 | 200 |
prepare prep_term name typ raw_set opt_morphs thy |
33646 | 201 |
|
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
202 |
val goal_nonempty = |
40832 | 203 |
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
|
204 |
val goal_admissible = |
40832 | 205 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
23152 | 206 |
|
33646 | 207 |
fun cpodef_result nonempty admissible thy = |
28073 | 208 |
let |
49833 | 209 |
val ((info as (_, {type_definition, ...}), below_def), thy) = thy |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
210 |
|> add_podef typ set opt_morphs (Tactic.rtac nonempty 1) |
40889 | 211 |
val (cpo_info, thy) = thy |
49833 | 212 |
|> prove_cpo name newT morphs type_definition below_def admissible |
23152 | 213 |
in |
40889 | 214 |
((info, cpo_info), thy) |
40832 | 215 |
end |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
216 |
in |
33646 | 217 |
(goal_nonempty, goal_admissible, cpodef_result) |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
218 |
end |
30345 | 219 |
handle ERROR msg => |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
220 |
cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print (#1 typ)) |
23152 | 221 |
|
33646 | 222 |
fun prepare_pcpodef |
223 |
(prep_term: Proof.context -> 'a -> term) |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
224 |
(typ: binding * (string * sort) list * mixfix) |
33646 | 225 |
(raw_set: 'a) |
226 |
(opt_morphs: (binding * binding) option) |
|
227 |
(thy: theory) |
|
228 |
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
|
229 |
let |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
230 |
val name = #1 typ |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42381
diff
changeset
|
231 |
val (newT, oldT, set, morphs) = |
40832 | 232 |
prepare prep_term name typ raw_set opt_morphs thy |
33646 | 233 |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
234 |
val goal_bottom_mem = |
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
235 |
HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set)) |
33646 | 236 |
|
237 |
val goal_admissible = |
|
40832 | 238 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
33646 | 239 |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
240 |
fun pcpodef_result bottom_mem admissible thy = |
33646 | 241 |
let |
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
242 |
val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1 |
49833 | 243 |
val ((info as (_, {type_definition, ...}), below_def), thy) = thy |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
244 |
|> add_podef typ set opt_morphs tac |
40889 | 245 |
val (cpo_info, thy) = thy |
49833 | 246 |
|> prove_cpo name newT morphs type_definition below_def admissible |
40889 | 247 |
val (pcpo_info, thy) = thy |
49833 | 248 |
|> prove_pcpo name newT morphs type_definition below_def bottom_mem |
33646 | 249 |
in |
40889 | 250 |
((info, cpo_info, pcpo_info), thy) |
40832 | 251 |
end |
33646 | 252 |
in |
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41296
diff
changeset
|
253 |
(goal_bottom_mem, goal_admissible, pcpodef_result) |
33646 | 254 |
end |
255 |
handle ERROR msg => |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
256 |
cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ)) |
33646 | 257 |
|
23152 | 258 |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
259 |
(* tactic interface *) |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
260 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
261 |
fun add_cpodef typ set opt_morphs (tac1, tac2) thy = |
33646 | 262 |
let |
263 |
val (goal1, goal2, cpodef_result) = |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
264 |
prepare_cpodef Syntax.check_term typ set opt_morphs thy |
33646 | 265 |
val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
266 |
handle ERROR msg => cat_error msg |
|
40832 | 267 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
33646 | 268 |
val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
269 |
handle ERROR msg => cat_error msg |
|
40832 | 270 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
271 |
in cpodef_result thm1 thm2 thy end |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
272 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
273 |
fun add_pcpodef typ set opt_morphs (tac1, tac2) thy = |
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
274 |
let |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
275 |
val (goal1, goal2, pcpodef_result) = |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
276 |
prepare_pcpodef Syntax.check_term typ set opt_morphs thy |
33646 | 277 |
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
|
278 |
handle ERROR msg => cat_error msg |
40832 | 279 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
33646 | 280 |
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
|
281 |
handle ERROR msg => cat_error msg |
40832 | 282 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
283 |
in pcpodef_result thm1 thm2 thy end |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
284 |
|
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
285 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
286 |
(* proof interface *) |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
287 |
|
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
288 |
local |
23152 | 289 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
290 |
fun gen_cpodef_proof prep_term prep_constraint |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
291 |
((b, raw_args, mx), set, opt_morphs) thy = |
23152 | 292 |
let |
42361 | 293 |
val ctxt = Proof_Context.init_global thy |
40832 | 294 |
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
|
295 |
val (goal1, goal2, make_result) = |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
296 |
prepare_cpodef prep_term (b, args, mx) set opt_morphs thy |
42361 | 297 |
fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
40832 | 298 |
| after_qed _ = raise Fail "cpodef_proof" |
299 |
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
|
33646 | 300 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
301 |
fun gen_pcpodef_proof prep_term prep_constraint |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
302 |
((b, raw_args, mx), set, opt_morphs) thy = |
33646 | 303 |
let |
42361 | 304 |
val ctxt = Proof_Context.init_global thy |
40832 | 305 |
val args = map (apsnd (prep_constraint ctxt)) raw_args |
33646 | 306 |
val (goal1, goal2, make_result) = |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
307 |
prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy |
42361 | 308 |
fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
40832 | 309 |
| after_qed _ = raise Fail "pcpodef_proof" |
310 |
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
|
23152 | 311 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
312 |
in |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
313 |
|
40832 | 314 |
fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x |
315 |
fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x |
|
23152 | 316 |
|
40832 | 317 |
fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x |
318 |
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
|
319 |
|
40832 | 320 |
end |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
321 |
|
23152 | 322 |
|
323 |
||
324 |
(** outer syntax **) |
|
325 |
||
326 |
val typedef_proof_decl = |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
327 |
(Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
328 |
(@{keyword "="} |-- Parse.term) -- |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
329 |
Scan.option |
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
330 |
(@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) |
23152 | 331 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
332 |
fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) = |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
333 |
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
334 |
((t, args, mx), A, morphs) |
23152 | 335 |
|
24867 | 336 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
337 |
Outer_Syntax.command @{command_spec "pcpodef"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
338 |
"HOLCF type definition (requires admissibility proof)" |
23152 | 339 |
(typedef_proof_decl >> |
40832 | 340 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))) |
23152 | 341 |
|
24867 | 342 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
343 |
Outer_Syntax.command @{command_spec "cpodef"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
344 |
"HOLCF type definition (requires admissibility proof)" |
23152 | 345 |
(typedef_proof_decl >> |
40832 | 346 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))) |
23152 | 347 |
|
40832 | 348 |
end |