author | huffman |
Wed, 01 Dec 2010 20:52:16 -0800 | |
changeset 40889 | 0317c902dbfa |
parent 40832 | 4352ca878c41 |
child 41028 | 0acff85f95c7 |
permissions | -rw-r--r-- |
40772 | 1 |
(* Title: 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, |
|
40770
6023808b38d4
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
huffman
parents:
40321
diff
changeset
|
12 |
is_lub: thm, lub: thm, compact: thm } |
33646 | 13 |
type pcpo_info = |
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
39557
diff
changeset
|
14 |
{ Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
33646 | 15 |
Rep_defined: thm, Abs_defined: thm } |
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 |
|
40772 | 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, |
|
40770
6023808b38d4
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
huffman
parents:
40321
diff
changeset
|
48 |
is_lub: thm, lub: thm, compact: thm } |
23152 | 49 |
|
33646 | 50 |
type pcpo_info = |
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
39557
diff
changeset
|
51 |
{ Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
33646 | 52 |
Rep_defined: thm, Abs_defined: thm } |
53 |
||
54 |
(* building terms *) |
|
23152 | 55 |
|
40832 | 56 |
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT) |
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 |
|
68 |
fun fold_UU_mem thm NONE = thm |
|
69 |
| fold_UU_mem thm (SOME set_def) = |
|
70 |
let val rule = @{lemma "A == B ==> UU : B ==> UU : 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 is_lub = make @{thm typedef_is_lub} |
|
98 |
val lub = make @{thm typedef_lub} |
|
99 |
val compact = make @{thm typedef_compact} |
|
35902 | 100 |
val (_, thy) = |
101 |
thy |
|
33646 | 102 |
|> 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
|
103 |
|> Global_Theory.add_thms |
35902 | 104 |
([((Binding.prefix_name "adm_" name, admissible'), []), |
105 |
((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), |
|
106 |
((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), |
|
40770
6023808b38d4
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
huffman
parents:
40321
diff
changeset
|
107 |
((Binding.prefix_name "is_lub_" name, is_lub ), []), |
35902 | 108 |
((Binding.prefix_name "lub_" name, lub ), []), |
109 |
((Binding.prefix_name "compact_" name, compact ), [])]) |
|
40832 | 110 |
||> Sign.parent_path |
33646 | 111 |
val cpo_info : cpo_info = |
112 |
{ below_def = below_def, adm = admissible', cont_Rep = cont_Rep, |
|
40832 | 113 |
cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact } |
33646 | 114 |
in |
35902 | 115 |
(cpo_info, thy) |
40832 | 116 |
end |
33646 | 117 |
|
118 |
fun prove_pcpo |
|
119 |
(name: binding) |
|
120 |
(newT: typ) |
|
121 |
(Rep_name: binding, Abs_name: binding) |
|
122 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
123 |
(set_def: thm option) (* A == set *) |
|
124 |
(below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
125 |
(UU_mem: thm) (* UU : set *) |
|
126 |
(thy: theory) |
|
127 |
= |
|
128 |
let |
|
40832 | 129 |
val UU_mem' = fold_UU_mem UU_mem set_def |
130 |
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'] |
|
131 |
val (full_tname, Ts) = dest_Type newT |
|
132 |
val lhs_sorts = map (snd o dest_TFree) Ts |
|
133 |
val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 |
|
134 |
val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
|
135 |
val pcpo_thms' = map (Thm.transfer thy) pcpo_thms |
|
136 |
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') |
|
137 |
val Rep_strict = make @{thm typedef_Rep_strict} |
|
138 |
val Abs_strict = make @{thm typedef_Abs_strict} |
|
139 |
val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff} |
|
140 |
val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff} |
|
141 |
val Rep_defined = make @{thm typedef_Rep_defined} |
|
142 |
val Abs_defined = make @{thm typedef_Abs_defined} |
|
35902 | 143 |
val (_, thy) = |
144 |
thy |
|
33646 | 145 |
|> 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
|
146 |
|> Global_Theory.add_thms |
35902 | 147 |
([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []), |
148 |
((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
|
149 |
((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []), |
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
39557
diff
changeset
|
150 |
((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []), |
35902 | 151 |
((Binding.suffix_name "_defined" Rep_name, Rep_defined), []), |
152 |
((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])]) |
|
40832 | 153 |
||> Sign.parent_path |
33646 | 154 |
val pcpo_info = |
155 |
{ Rep_strict = Rep_strict, Abs_strict = Abs_strict, |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
39557
diff
changeset
|
156 |
Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff, |
40832 | 157 |
Rep_defined = Rep_defined, Abs_defined = Abs_defined } |
33646 | 158 |
in |
35902 | 159 |
(pcpo_info, thy) |
40832 | 160 |
end |
33646 | 161 |
|
162 |
(* prepare_cpodef *) |
|
163 |
||
164 |
fun declare_type_name a = |
|
40832 | 165 |
Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))) |
33646 | 166 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
167 |
fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy = |
23152 | 168 |
let |
40832 | 169 |
val _ = Theory.requires thy "Cpodef" "cpodefs" |
30345 | 170 |
|
23152 | 171 |
(*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
|
172 |
val tmp_ctxt = |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36323
diff
changeset
|
173 |
ProofContext.init_global thy |
40832 | 174 |
|> fold (Variable.declare_typ o TFree) raw_args |
175 |
val set = prep_term tmp_ctxt raw_set |
|
176 |
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
|
177 |
|
40832 | 178 |
val setT = Term.fastype_of set |
23152 | 179 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
40832 | 180 |
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
|
181 |
|
33646 | 182 |
(*lhs*) |
40832 | 183 |
val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args |
184 |
val full_tname = Sign.full_name thy tname |
|
185 |
val newT = Type (full_tname, map TFree lhs_tfrees) |
|
33646 | 186 |
|
187 |
val morphs = opt_morphs |
|
40832 | 188 |
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) |
33646 | 189 |
in |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
190 |
(newT, oldT, set, morphs) |
33646 | 191 |
end |
192 |
||
193 |
fun add_podef def opt_name typ set opt_morphs tac thy = |
|
194 |
let |
|
40832 | 195 |
val name = the_default (#1 typ) opt_name |
40889 | 196 |
val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy) = thy |
40832 | 197 |
|> Typedef.add_typedef_global def opt_name typ set opt_morphs tac |
198 |
val oldT = #rep_type (#1 info) |
|
199 |
val newT = #abs_type (#1 info) |
|
200 |
val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) |
|
33646 | 201 |
|
40832 | 202 |
val RepC = Const (Rep_name, newT --> oldT) |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
203 |
val below_eqn = Logic.mk_equals (below_const newT, |
40832 | 204 |
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))) |
40889 | 205 |
val ((_, (_, below_ldef)), lthy) = thy |
40832 | 206 |
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}) |
33646 | 207 |
|> Specification.definition (NONE, |
40832 | 208 |
((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)) |
40889 | 209 |
val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy) |
210 |
val below_def = singleton (ProofContext.export lthy ctxt_thy) below_ldef |
|
211 |
val thy = lthy |
|
212 |
|> Class.prove_instantiation_exit |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
213 |
(K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) |
40889 | 214 |
in ((info, below_def), thy) end |
33646 | 215 |
|
216 |
fun prepare_cpodef |
|
217 |
(prep_term: Proof.context -> 'a -> term) |
|
218 |
(def: bool) |
|
219 |
(name: binding) |
|
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) |
222 |
(opt_morphs: (binding * binding) option) |
|
223 |
(thy: theory) |
|
224 |
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = |
|
225 |
let |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
226 |
val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
40832 | 227 |
prepare prep_term name typ raw_set opt_morphs thy |
33646 | 228 |
|
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
229 |
val goal_nonempty = |
40832 | 230 |
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
|
231 |
val goal_admissible = |
40832 | 232 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
23152 | 233 |
|
33646 | 234 |
fun cpodef_result nonempty admissible thy = |
28073 | 235 |
let |
40889 | 236 |
val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |
40832 | 237 |
|> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1) |
40889 | 238 |
val (cpo_info, thy) = thy |
40832 | 239 |
|> prove_cpo name newT morphs type_definition set_def below_def admissible |
23152 | 240 |
in |
40889 | 241 |
((info, cpo_info), thy) |
40832 | 242 |
end |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
243 |
in |
33646 | 244 |
(goal_nonempty, goal_admissible, cpodef_result) |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
245 |
end |
30345 | 246 |
handle ERROR msg => |
40832 | 247 |
cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)) |
23152 | 248 |
|
33646 | 249 |
fun prepare_pcpodef |
250 |
(prep_term: Proof.context -> 'a -> term) |
|
251 |
(def: bool) |
|
252 |
(name: binding) |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
253 |
(typ: binding * (string * sort) list * mixfix) |
33646 | 254 |
(raw_set: 'a) |
255 |
(opt_morphs: (binding * binding) option) |
|
256 |
(thy: theory) |
|
257 |
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
|
258 |
let |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
259 |
val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
40832 | 260 |
prepare prep_term name typ raw_set opt_morphs thy |
33646 | 261 |
|
262 |
val goal_UU_mem = |
|
40832 | 263 |
HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)) |
33646 | 264 |
|
265 |
val goal_admissible = |
|
40832 | 266 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
33646 | 267 |
|
268 |
fun pcpodef_result UU_mem admissible thy = |
|
269 |
let |
|
40832 | 270 |
val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1 |
40889 | 271 |
val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |
40832 | 272 |
|> add_podef def (SOME name) typ set opt_morphs tac |
40889 | 273 |
val (cpo_info, thy) = thy |
40832 | 274 |
|> prove_cpo name newT morphs type_definition set_def below_def admissible |
40889 | 275 |
val (pcpo_info, thy) = thy |
40832 | 276 |
|> prove_pcpo name newT morphs type_definition set_def below_def UU_mem |
33646 | 277 |
in |
40889 | 278 |
((info, cpo_info, pcpo_info), thy) |
40832 | 279 |
end |
33646 | 280 |
in |
281 |
(goal_UU_mem, goal_admissible, pcpodef_result) |
|
282 |
end |
|
283 |
handle ERROR msg => |
|
40832 | 284 |
cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)) |
33646 | 285 |
|
23152 | 286 |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
287 |
(* tactic interface *) |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
288 |
|
33646 | 289 |
fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy = |
290 |
let |
|
40832 | 291 |
val name = the_default (#1 typ) opt_name |
33646 | 292 |
val (goal1, goal2, cpodef_result) = |
40832 | 293 |
prepare_cpodef Syntax.check_term def name typ set opt_morphs thy |
33646 | 294 |
val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
295 |
handle ERROR msg => cat_error msg |
|
40832 | 296 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
33646 | 297 |
val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
298 |
handle ERROR msg => cat_error msg |
|
40832 | 299 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
300 |
in cpodef_result thm1 thm2 thy end |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
301 |
|
33646 | 302 |
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
|
303 |
let |
40832 | 304 |
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
|
305 |
val (goal1, goal2, pcpodef_result) = |
40832 | 306 |
prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy |
33646 | 307 |
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
|
308 |
handle ERROR msg => cat_error msg |
40832 | 309 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
33646 | 310 |
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
|
311 |
handle ERROR msg => cat_error msg |
40832 | 312 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
313 |
in pcpodef_result thm1 thm2 thy end |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
314 |
|
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
315 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
316 |
(* proof interface *) |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
317 |
|
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
318 |
local |
23152 | 319 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
320 |
fun gen_cpodef_proof prep_term prep_constraint |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
321 |
((def, name), (b, raw_args, mx), set, opt_morphs) thy = |
23152 | 322 |
let |
40832 | 323 |
val ctxt = ProofContext.init_global thy |
324 |
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
|
325 |
val (goal1, goal2, make_result) = |
40832 | 326 |
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy |
38756
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38348
diff
changeset
|
327 |
fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) |
40832 | 328 |
| after_qed _ = raise Fail "cpodef_proof" |
329 |
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
|
33646 | 330 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
331 |
fun gen_pcpodef_proof prep_term prep_constraint |
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
332 |
((def, name), (b, raw_args, mx), set, opt_morphs) thy = |
33646 | 333 |
let |
40832 | 334 |
val ctxt = ProofContext.init_global thy |
335 |
val args = map (apsnd (prep_constraint ctxt)) raw_args |
|
33646 | 336 |
val (goal1, goal2, make_result) = |
40832 | 337 |
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy |
38756
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38348
diff
changeset
|
338 |
fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) |
40832 | 339 |
| after_qed _ = raise Fail "pcpodef_proof" |
340 |
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
|
23152 | 341 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
342 |
in |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
343 |
|
40832 | 344 |
fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x |
345 |
fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x |
|
23152 | 346 |
|
40832 | 347 |
fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x |
348 |
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
|
349 |
|
40832 | 350 |
end |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
351 |
|
23152 | 352 |
|
353 |
||
354 |
(** outer syntax **) |
|
355 |
||
356 |
val typedef_proof_decl = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
357 |
Scan.optional (Parse.$$$ "(" |-- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
358 |
((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding || |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
359 |
Parse.binding >> (fn s => (true, SOME s))) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
360 |
--| Parse.$$$ ")") (true, NONE) -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
361 |
(Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
362 |
(Parse.$$$ "=" |-- Parse.term) -- |
40832 | 363 |
Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)) |
23152 | 364 |
|
35840
01d7c4ba9050
allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents:
35742
diff
changeset
|
365 |
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
|
366 |
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
40832 | 367 |
((def, the_default t opt_name), (t, args, mx), A, morphs) |
23152 | 368 |
|
24867 | 369 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
370 |
Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
371 |
Keyword.thy_goal |
23152 | 372 |
(typedef_proof_decl >> |
40832 | 373 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))) |
23152 | 374 |
|
24867 | 375 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
376 |
Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
377 |
Keyword.thy_goal |
23152 | 378 |
(typedef_proof_decl >> |
40832 | 379 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))) |
23152 | 380 |
|
40832 | 381 |
end |