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