author | wenzelm |
Sun, 07 Feb 2010 19:33:34 +0100 | |
changeset 35021 | c839a4c670c6 |
parent 33680 | a47277e09012 |
child 35129 | ed24ba6f69aa |
permissions | -rw-r--r-- |
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31725
diff
changeset
|
1 |
(* Title: HOLCF/Tools/pcpodef.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 |
||
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31725
diff
changeset
|
8 |
signature PCPODEF = |
23152 | 9 |
sig |
33646 | 10 |
type cpo_info = |
11 |
{ below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
|
12 |
lub: thm, thelub: thm, compact: thm } |
|
13 |
type pcpo_info = |
|
14 |
{ Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm, |
|
15 |
Rep_defined: thm, Abs_defined: thm } |
|
16 |
||
17 |
val add_podef: bool -> binding option -> binding * string list * mixfix -> |
|
18 |
term -> (binding * binding) option -> tactic -> theory -> |
|
19 |
(Typedef.info * thm) * theory |
|
20 |
val add_cpodef: bool -> binding option -> binding * string list * mixfix -> |
|
21 |
term -> (binding * binding) option -> tactic * tactic -> theory -> |
|
22 |
(Typedef.info * cpo_info) * theory |
|
33645
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
23 |
val add_pcpodef: bool -> binding option -> binding * string list * mixfix -> |
33646 | 24 |
term -> (binding * binding) option -> tactic * tactic -> theory -> |
25 |
(Typedef.info * cpo_info * pcpo_info) * theory |
|
26 |
||
27 |
val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term |
|
28 |
* (binding * binding) option -> theory -> Proof.state |
|
29 |
val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string |
|
30 |
* (binding * binding) option -> theory -> Proof.state |
|
30345 | 31 |
val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term |
32 |
* (binding * binding) option -> theory -> Proof.state |
|
33 |
val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string |
|
34 |
* (binding * binding) option -> theory -> Proof.state |
|
23152 | 35 |
end; |
36 |
||
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31725
diff
changeset
|
37 |
structure Pcpodef :> PCPODEF = |
23152 | 38 |
struct |
39 |
||
40 |
(** type definitions **) |
|
41 |
||
33646 | 42 |
type cpo_info = |
43 |
{ below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
|
44 |
lub: thm, thelub: thm, compact: thm } |
|
23152 | 45 |
|
33646 | 46 |
type pcpo_info = |
47 |
{ Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm, |
|
48 |
Rep_defined: thm, Abs_defined: thm } |
|
49 |
||
50 |
(* building terms *) |
|
23152 | 51 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
52 |
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); |
23152 | 53 |
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); |
54 |
||
33646 | 55 |
fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT); |
56 |
||
57 |
(* manipulating theorems *) |
|
58 |
||
59 |
fun fold_adm_mem thm NONE = thm |
|
60 |
| fold_adm_mem thm (SOME set_def) = |
|
61 |
let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} |
|
62 |
in rule OF [set_def, thm] end; |
|
63 |
||
64 |
fun fold_UU_mem thm NONE = thm |
|
65 |
| fold_UU_mem thm (SOME set_def) = |
|
66 |
let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp} |
|
67 |
in rule OF [set_def, thm] end; |
|
68 |
||
69 |
(* proving class instances *) |
|
70 |
||
71 |
fun prove_cpo |
|
72 |
(name: binding) |
|
73 |
(newT: typ) |
|
74 |
(Rep_name: binding, Abs_name: binding) |
|
75 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
76 |
(set_def: thm option) (* A == set *) |
|
77 |
(below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
78 |
(admissible: thm) (* adm (%x. x : set) *) |
|
79 |
(thy: theory) |
|
80 |
= |
|
81 |
let |
|
82 |
val admissible' = fold_adm_mem admissible set_def; |
|
83 |
val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible']; |
|
84 |
val (full_tname, Ts) = dest_Type newT; |
|
85 |
val lhs_sorts = map (snd o dest_TFree) Ts; |
|
86 |
val thy2 = |
|
87 |
thy |
|
88 |
|> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) |
|
89 |
(Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1); |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
90 |
(* transfer thms so that they will know about the new cpo instance *) |
33646 | 91 |
val cpo_thms' = map (Thm.transfer thy2) cpo_thms; |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33680
diff
changeset
|
92 |
fun make thm = Drule.export_without_context (thm OF cpo_thms'); |
33646 | 93 |
val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) = |
94 |
thy2 |
|
95 |
|> Sign.add_path (Binding.name_of name) |
|
96 |
|> PureThy.add_thms |
|
97 |
([((Binding.prefix_name "adm_" name, admissible'), []), |
|
98 |
((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []), |
|
99 |
((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []), |
|
100 |
((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []), |
|
101 |
((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []), |
|
102 |
((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])]) |
|
103 |
||> Sign.parent_path; |
|
104 |
val cpo_info : cpo_info = |
|
105 |
{ below_def = below_def, adm = admissible', cont_Rep = cont_Rep, |
|
106 |
cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact }; |
|
107 |
in |
|
108 |
(cpo_info, thy3) |
|
109 |
end; |
|
110 |
||
111 |
fun prove_pcpo |
|
112 |
(name: binding) |
|
113 |
(newT: typ) |
|
114 |
(Rep_name: binding, Abs_name: binding) |
|
115 |
(type_definition: thm) (* type_definition Rep Abs A *) |
|
116 |
(set_def: thm option) (* A == set *) |
|
117 |
(below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
118 |
(UU_mem: thm) (* UU : set *) |
|
119 |
(thy: theory) |
|
120 |
= |
|
121 |
let |
|
122 |
val UU_mem' = fold_UU_mem UU_mem set_def; |
|
123 |
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem']; |
|
124 |
val (full_tname, Ts) = dest_Type newT; |
|
125 |
val lhs_sorts = map (snd o dest_TFree) Ts; |
|
126 |
val thy2 = thy |
|
127 |
|> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) |
|
128 |
(Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1); |
|
129 |
val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms; |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33680
diff
changeset
|
130 |
fun make thm = Drule.export_without_context (thm OF pcpo_thms'); |
33646 | 131 |
val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff, |
132 |
Rep_defined, Abs_defined], thy3) = |
|
133 |
thy2 |
|
134 |
|> Sign.add_path (Binding.name_of name) |
|
135 |
|> PureThy.add_thms |
|
136 |
([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []), |
|
137 |
((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []), |
|
138 |
((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []), |
|
139 |
((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []), |
|
140 |
((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []), |
|
141 |
((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])]) |
|
142 |
||> Sign.parent_path; |
|
143 |
val pcpo_info = |
|
144 |
{ Rep_strict = Rep_strict, Abs_strict = Abs_strict, |
|
145 |
Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff, |
|
146 |
Rep_defined = Rep_defined, Abs_defined = Abs_defined }; |
|
147 |
in |
|
148 |
(pcpo_info, thy3) |
|
149 |
end; |
|
150 |
||
151 |
(* prepare_cpodef *) |
|
152 |
||
153 |
fun declare_type_name a = |
|
154 |
Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
|
155 |
||
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
156 |
fun prepare prep_term name (t, vs, mx) raw_set opt_morphs thy = |
23152 | 157 |
let |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
158 |
val _ = Theory.requires thy "Pcpodef" "pcpodefs"; |
23152 | 159 |
val ctxt = ProofContext.init thy; |
30345 | 160 |
|
23152 | 161 |
(*rhs*) |
162 |
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
|
163 |
val setT = Term.fastype_of set; |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
164 |
val rhs_tfrees = Term.add_tfrees set []; |
23152 | 165 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
24920 | 166 |
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); |
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
167 |
|
33646 | 168 |
(*lhs*) |
169 |
val defS = Sign.defaultS thy; |
|
170 |
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
|
171 |
val tname = Binding.map_name (Syntax.type_name mx) t; |
|
172 |
val full_tname = Sign.full_name thy tname; |
|
173 |
val newT = Type (full_tname, map TFree lhs_tfrees); |
|
174 |
||
175 |
val morphs = opt_morphs |
|
176 |
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); |
|
177 |
in |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
178 |
(newT, oldT, set, morphs) |
33646 | 179 |
end |
180 |
||
181 |
fun add_podef def opt_name typ set opt_morphs tac thy = |
|
182 |
let |
|
183 |
val name = the_default (#1 typ) opt_name; |
|
184 |
val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy |
|
185 |
|> Typedef.add_typedef def opt_name typ set opt_morphs tac; |
|
186 |
val oldT = #rep_type info; |
|
187 |
val newT = #abs_type info; |
|
188 |
val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); |
|
189 |
||
190 |
val RepC = Const (Rep_name, newT --> oldT); |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
191 |
val below_eqn = Logic.mk_equals (below_const newT, |
33646 | 192 |
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); |
193 |
val lthy3 = thy2 |
|
194 |
|> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po}); |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
195 |
val ((_, (_, below_ldef)), lthy4) = lthy3 |
33646 | 196 |
|> Specification.definition (NONE, |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
197 |
((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)); |
33646 | 198 |
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
199 |
val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef; |
33646 | 200 |
val thy5 = lthy4 |
201 |
|> Class.prove_instantiation_instance |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
202 |
(K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) |
33671 | 203 |
|> Local_Theory.exit_global; |
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
204 |
in ((info, below_def), thy5) end; |
33646 | 205 |
|
206 |
fun prepare_cpodef |
|
207 |
(prep_term: Proof.context -> 'a -> term) |
|
208 |
(def: bool) |
|
209 |
(name: binding) |
|
210 |
(typ: binding * string list * mixfix) |
|
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 |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
216 |
val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
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 = |
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
220 |
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
221 |
val goal_admissible = |
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
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 |
33646 | 226 |
val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy |
227 |
|> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1); |
|
228 |
val (cpo_info, thy3) = thy2 |
|
229 |
|> prove_cpo name newT morphs type_definition set_def below_def admissible; |
|
23152 | 230 |
in |
33646 | 231 |
((info, cpo_info), thy3) |
23152 | 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 => |
237 |
cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)); |
|
23152 | 238 |
|
33646 | 239 |
fun prepare_pcpodef |
240 |
(prep_term: Proof.context -> 'a -> term) |
|
241 |
(def: bool) |
|
242 |
(name: binding) |
|
243 |
(typ: binding * string list * mixfix) |
|
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 |
|
33678
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
249 |
val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
2a2014cbb2a6
cleaned up, removed unneeded call to Syntax.check_term
huffman
parents:
33646
diff
changeset
|
250 |
prepare prep_term name typ raw_set opt_morphs thy; |
33646 | 251 |
|
252 |
val goal_UU_mem = |
|
253 |
HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); |
|
254 |
||
255 |
val goal_admissible = |
|
256 |
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
|
257 |
||
258 |
fun pcpodef_result UU_mem admissible thy = |
|
259 |
let |
|
260 |
val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1; |
|
261 |
val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy |
|
262 |
|> add_podef def (SOME name) typ set opt_morphs tac; |
|
263 |
val (cpo_info, thy3) = thy2 |
|
264 |
|> prove_cpo name newT morphs type_definition set_def below_def admissible; |
|
265 |
val (pcpo_info, thy4) = thy3 |
|
266 |
|> prove_pcpo name newT morphs type_definition set_def below_def UU_mem; |
|
267 |
in |
|
268 |
((info, cpo_info, pcpo_info), thy4) |
|
269 |
end; |
|
270 |
in |
|
271 |
(goal_UU_mem, goal_admissible, pcpodef_result) |
|
272 |
end |
|
273 |
handle ERROR msg => |
|
274 |
cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)); |
|
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 |
|
281 |
val name = the_default (#1 typ) opt_name; |
|
282 |
val (goal1, goal2, cpodef_result) = |
|
283 |
prepare_cpodef Syntax.check_term def name typ set opt_morphs thy; |
|
284 |
val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
|
285 |
handle ERROR msg => cat_error msg |
|
286 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
|
287 |
val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
|
288 |
handle ERROR msg => cat_error msg |
|
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 |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
294 |
val name = the_default (#1 typ) opt_name; |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
295 |
val (goal1, goal2, pcpodef_result) = |
33646 | 296 |
prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy; |
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 |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
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 |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
302 |
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)); |
562635ab559b
use Drule.standard (following typedef package), add pcpodef tactic interface
huffman
parents:
33553
diff
changeset
|
303 |
in pcpodef_result thm1 thm2 thy end; |
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 |
|
33646 | 310 |
fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy = |
23152 | 311 |
let |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
312 |
val (goal1, goal2, make_result) = |
33646 | 313 |
prepare_cpodef prep_term def name typ set opt_morphs thy; |
314 |
fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2); |
|
315 |
in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; |
|
316 |
||
317 |
fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy = |
|
318 |
let |
|
319 |
val (goal1, goal2, make_result) = |
|
320 |
prepare_pcpodef prep_term def name typ set opt_morphs thy; |
|
321 |
fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2); |
|
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
29060
diff
changeset
|
322 |
in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; |
23152 | 323 |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
324 |
in |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
325 |
|
33646 | 326 |
fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x; |
327 |
fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x; |
|
23152 | 328 |
|
33646 | 329 |
fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x; |
330 |
fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x; |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
331 |
|
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
332 |
end; |
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
333 |
|
23152 | 334 |
|
335 |
||
336 |
(** outer syntax **) |
|
337 |
||
338 |
local structure P = OuterParse and K = OuterKeyword in |
|
339 |
||
340 |
val typedef_proof_decl = |
|
341 |
Scan.optional (P.$$$ "(" |-- |
|
30345 | 342 |
((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) |
23152 | 343 |
--| P.$$$ ")") (true, NONE) -- |
30345 | 344 |
(P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- |
345 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); |
|
23152 | 346 |
|
347 |
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = |
|
29060
d7bde0b4bf72
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
wenzelm
parents:
28965
diff
changeset
|
348 |
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
30345 | 349 |
((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs); |
23152 | 350 |
|
24867 | 351 |
val _ = |
23152 | 352 |
OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal |
353 |
(typedef_proof_decl >> |
|
354 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); |
|
355 |
||
24867 | 356 |
val _ = |
23152 | 357 |
OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal |
358 |
(typedef_proof_decl >> |
|
359 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); |
|
360 |
||
361 |
end; |
|
362 |
||
363 |
end; |