author | wenzelm |
Sat, 06 Oct 2007 16:50:04 +0200 | |
changeset 24867 | e5b55d7be9bb |
parent 24712 | 64ed05609568 |
child 24920 | 2a45e400fdad |
permissions | -rw-r--r-- |
23152 | 1 |
(* Title: HOLCF/Tools/pcpodef_package.ML |
2 |
ID: $Id$ |
|
3 |
Author: Brian Huffman |
|
4 |
||
5 |
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style |
|
6 |
typedef. |
|
7 |
*) |
|
8 |
||
9 |
signature PCPODEF_PACKAGE = |
|
10 |
sig |
|
11 |
val quiet_mode: bool ref |
|
12 |
val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string |
|
13 |
* (string * string) option -> theory -> Proof.state |
|
14 |
val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term |
|
15 |
* (string * string) option -> theory -> Proof.state |
|
16 |
val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string |
|
17 |
* (string * string) option -> theory -> Proof.state |
|
18 |
val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term |
|
19 |
* (string * string) option -> theory -> Proof.state |
|
20 |
end; |
|
21 |
||
22 |
structure PcpodefPackage: PCPODEF_PACKAGE = |
|
23 |
struct |
|
24 |
||
25 |
(** theory context references **) |
|
26 |
||
27 |
val typedef_po = thm "typedef_po"; |
|
28 |
val typedef_cpo = thm "typedef_cpo"; |
|
29 |
val typedef_pcpo = thm "typedef_pcpo"; |
|
30 |
val typedef_lub = thm "typedef_lub"; |
|
31 |
val typedef_thelub = thm "typedef_thelub"; |
|
32 |
val typedef_compact = thm "typedef_compact"; |
|
33 |
val cont_Rep = thm "typedef_cont_Rep"; |
|
34 |
val cont_Abs = thm "typedef_cont_Abs"; |
|
35 |
val Rep_strict = thm "typedef_Rep_strict"; |
|
36 |
val Abs_strict = thm "typedef_Abs_strict"; |
|
37 |
val Rep_defined = thm "typedef_Rep_defined"; |
|
38 |
val Abs_defined = thm "typedef_Abs_defined"; |
|
39 |
||
40 |
||
41 |
(** type definitions **) |
|
42 |
||
43 |
(* messages *) |
|
44 |
||
45 |
val quiet_mode = ref false; |
|
46 |
fun message s = if ! quiet_mode then () else writeln s; |
|
47 |
||
48 |
||
49 |
(* prepare_cpodef *) |
|
50 |
||
51 |
fun err_in_cpodef msg name = |
|
52 |
cat_error msg ("The error(s) above occurred in cpodef " ^ quote name); |
|
53 |
||
54 |
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
|
55 |
||
56 |
fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT); |
|
57 |
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); |
|
58 |
||
59 |
fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = |
|
60 |
let |
|
61 |
val ctxt = ProofContext.init thy; |
|
62 |
val full = Sign.full_name thy; |
|
63 |
||
64 |
(*rhs*) |
|
65 |
val full_name = full name; |
|
66 |
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
|
67 |
val setT = Term.fastype_of set; |
|
68 |
val rhs_tfrees = term_tfrees set; |
|
69 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
|
70 |
error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT)); |
|
71 |
fun mk_nonempty A = |
|
72 |
HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)); |
|
73 |
fun mk_admissible A = |
|
74 |
mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)); |
|
75 |
fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A); |
|
76 |
val goal = if pcpo |
|
77 |
then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set)) |
|
78 |
else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set)); |
|
79 |
||
80 |
(*lhs*) |
|
81 |
val defS = Sign.defaultS thy; |
|
82 |
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
|
83 |
val lhs_sorts = map snd lhs_tfrees; |
|
84 |
val tname = Syntax.type_name t mx; |
|
85 |
val full_tname = full tname; |
|
86 |
val newT = Type (full_tname, map TFree lhs_tfrees); |
|
87 |
||
88 |
val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; |
|
89 |
val RepC = Const (full Rep_name, newT --> oldT); |
|
23284
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
23152
diff
changeset
|
90 |
fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT); |
23152 | 91 |
val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT, |
92 |
Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))); |
|
93 |
||
94 |
fun make_po tac theory = theory |
|
95 |
|> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac |
|
96 |
||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"]) |
|
24218 | 97 |
(Class.intro_classes_tac []) |
23152 | 98 |
||>> PureThy.add_defs_i true [Thm.no_attributes less_def] |
99 |
|-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) => |
|
100 |
AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"]) |
|
101 |
(Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) |
|
102 |
#> pair (type_definition, less_definition, set_def)); |
|
103 |
||
104 |
fun make_cpo admissible (type_def, less_def, set_def) theory = |
|
105 |
let |
|
106 |
val admissible' = fold_rule (the_list set_def) admissible; |
|
107 |
val cpo_thms = [type_def, less_def, admissible']; |
|
108 |
in |
|
109 |
theory |
|
110 |
|> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"]) |
|
111 |
(Tactic.rtac (typedef_cpo OF cpo_thms) 1) |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
112 |
|> Sign.add_path name |
23152 | 113 |
|> PureThy.add_thms |
114 |
([(("adm_" ^ name, admissible'), []), |
|
115 |
(("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []), |
|
116 |
(("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []), |
|
117 |
(("lub_" ^ name, typedef_lub OF cpo_thms), []), |
|
118 |
(("thelub_" ^ name, typedef_thelub OF cpo_thms), []), |
|
119 |
(("compact_" ^ name, typedef_compact OF cpo_thms), [])]) |
|
120 |
|> snd |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
121 |
|> Sign.parent_path |
23152 | 122 |
end; |
123 |
||
124 |
fun make_pcpo UUmem (type_def, less_def, set_def) theory = |
|
125 |
let |
|
126 |
val UUmem' = fold_rule (the_list set_def) UUmem; |
|
127 |
val pcpo_thms = [type_def, less_def, UUmem']; |
|
128 |
in |
|
129 |
theory |
|
130 |
|> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"]) |
|
131 |
(Tactic.rtac (typedef_pcpo OF pcpo_thms) 1) |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
132 |
|> Sign.add_path name |
23152 | 133 |
|> PureThy.add_thms |
134 |
([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []), |
|
135 |
((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []), |
|
136 |
((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []), |
|
137 |
((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), []) |
|
138 |
]) |
|
139 |
|> snd |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
140 |
|> Sign.parent_path |
23152 | 141 |
end; |
142 |
||
143 |
fun pcpodef_result UUmem_admissible theory = |
|
144 |
let |
|
145 |
val UUmem = UUmem_admissible RS conjunct1; |
|
146 |
val admissible = UUmem_admissible RS conjunct2; |
|
147 |
in |
|
148 |
theory |
|
149 |
|> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1) |
|
150 |
|-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs) |
|
151 |
end; |
|
152 |
||
153 |
fun cpodef_result nonempty_admissible theory = |
|
154 |
let |
|
155 |
val nonempty = nonempty_admissible RS conjunct1; |
|
156 |
val admissible = nonempty_admissible RS conjunct2; |
|
157 |
in |
|
158 |
theory |
|
159 |
|> make_po (Tactic.rtac nonempty 1) |
|
160 |
|-> make_cpo admissible |
|
161 |
end; |
|
162 |
||
163 |
in (goal, if pcpo then pcpodef_result else cpodef_result) end |
|
164 |
handle ERROR msg => err_in_cpodef msg name; |
|
165 |
||
166 |
||
167 |
(* cpodef_proof interface *) |
|
168 |
||
169 |
fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = |
|
170 |
let |
|
171 |
val (goal, pcpodef_result) = |
|
172 |
prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; |
|
173 |
fun after_qed [[th]] = ProofContext.theory (pcpodef_result th); |
|
174 |
in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end; |
|
175 |
||
24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24218
diff
changeset
|
176 |
fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x; |
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24218
diff
changeset
|
177 |
fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x; |
23152 | 178 |
|
24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24218
diff
changeset
|
179 |
fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x; |
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24218
diff
changeset
|
180 |
fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x; |
23152 | 181 |
|
182 |
||
183 |
(** outer syntax **) |
|
184 |
||
185 |
local structure P = OuterParse and K = OuterKeyword in |
|
186 |
||
24867 | 187 |
(* cf. HOL/Tools/typedef_package.ML *) |
23152 | 188 |
val typedef_proof_decl = |
189 |
Scan.optional (P.$$$ "(" |-- |
|
190 |
((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) |
|
191 |
--| P.$$$ ")") (true, NONE) -- |
|
192 |
(P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- |
|
193 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); |
|
194 |
||
195 |
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = |
|
196 |
(if pcpo then pcpodef_proof else cpodef_proof) |
|
197 |
((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); |
|
198 |
||
24867 | 199 |
val _ = |
23152 | 200 |
OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal |
201 |
(typedef_proof_decl >> |
|
202 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); |
|
203 |
||
24867 | 204 |
val _ = |
23152 | 205 |
OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal |
206 |
(typedef_proof_decl >> |
|
207 |
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); |
|
208 |
||
209 |
end; |
|
210 |
||
211 |
end; |