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