14115
|
1 |
(* Title: HOL/Tools/specification_package.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sebastian Skalberg, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
|
|
6 |
Package for defining constants by specification.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature SPECIFICATION_PACKAGE =
|
|
10 |
sig
|
|
11 |
val quiet_mode: bool ref
|
|
12 |
val add_specification: (bstring * bool) list -> bstring * Args.src list
|
|
13 |
-> theory * thm -> theory * thm
|
|
14 |
val add_specification_i: (bstring * bool) list -> bstring * theory attribute list
|
|
15 |
-> theory * thm -> theory * thm
|
|
16 |
end
|
|
17 |
|
|
18 |
structure SpecificationPackage : SPECIFICATION_PACKAGE =
|
|
19 |
struct
|
|
20 |
|
|
21 |
(* messages *)
|
|
22 |
|
|
23 |
val quiet_mode = ref false
|
|
24 |
fun message s = if ! quiet_mode then () else writeln s
|
|
25 |
|
|
26 |
local
|
|
27 |
val _ = Goal "[| Ex P ; c == Eps P |] ==> P c"
|
|
28 |
val _ = by (Asm_simp_tac 1)
|
|
29 |
val _ = by (rtac (thm "someI_ex") 1)
|
|
30 |
val _ = ba 1
|
|
31 |
in
|
|
32 |
val helper = Goals.result()
|
|
33 |
end
|
|
34 |
|
|
35 |
(* Akin to HOLogic.exists_const *)
|
|
36 |
fun choice_const T = Const("Hilbert_Choice.Eps",(T-->HOLogic.boolT)-->T)
|
|
37 |
|
|
38 |
(* Actual code *)
|
|
39 |
|
|
40 |
fun proc_exprop [] arg = arg
|
|
41 |
| proc_exprop ((cname,covld)::cos) (thy,thm) =
|
|
42 |
case concl_of thm of
|
|
43 |
Const("Trueprop",_) $ (Const("Ex",_) $ P) =>
|
|
44 |
let
|
|
45 |
val ctype = domain_type (type_of P)
|
|
46 |
val cdefname = Thm.def_name (Sign.base_name cname)
|
|
47 |
val def_eq = Logic.mk_equals (Const(cname,ctype),choice_const ctype $ P)
|
|
48 |
val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
|
|
49 |
val thm' = [thm,hd thms] MRS helper
|
|
50 |
in
|
|
51 |
proc_exprop cos (thy',thm')
|
|
52 |
end
|
|
53 |
| _ => raise THM ("Internal error: Bad specification theorem",0,[thm])
|
|
54 |
|
|
55 |
fun add_specification_i cos (name,atts) arg =
|
|
56 |
let
|
|
57 |
fun apply_attributes arg = Thm.apply_attributes(arg,atts)
|
|
58 |
fun add_final (arg as (thy,thm)) =
|
|
59 |
if name = ""
|
|
60 |
then arg
|
|
61 |
else (writeln ("specification " ^ name ^ ": " ^ (string_of_thm thm));
|
|
62 |
PureThy.store_thm((name,thm),[]) thy)
|
|
63 |
in
|
|
64 |
arg |> apsnd freezeT
|
|
65 |
|> proc_exprop cos
|
|
66 |
|> apsnd standard
|
|
67 |
|> apply_attributes
|
|
68 |
|> add_final
|
|
69 |
end
|
|
70 |
|
|
71 |
fun add_specification cos (name,atts) arg =
|
|
72 |
add_specification_i cos (name,map (Attrib.global_attribute thy) atts) arg
|
|
73 |
|
|
74 |
(* Collect all intances of constants in term *)
|
|
75 |
|
|
76 |
fun collect_consts ( t $ u,tms) = collect_consts (u,collect_consts (t,tms))
|
|
77 |
| collect_consts ( Abs(_,_,t),tms) = collect_consts (t,tms)
|
|
78 |
| collect_consts (tm as Const _,tms) = gen_ins (op aconv) (tm,tms)
|
|
79 |
| collect_consts ( _,tms) = tms
|
|
80 |
|
|
81 |
(* Complementing Type.varify... *)
|
|
82 |
|
|
83 |
fun unvarify t fmap =
|
|
84 |
let
|
|
85 |
val fmap' = map Library.swap fmap
|
|
86 |
fun unthaw (f as (a,S)) =
|
|
87 |
(case assoc (fmap',a) of
|
|
88 |
None => TVar f
|
|
89 |
| Some b => TFree (b,S))
|
|
90 |
in
|
|
91 |
map_term_types (map_type_tvar unthaw) t
|
|
92 |
end
|
|
93 |
|
|
94 |
(* The syntactic meddling needed to setup add_specification for work *)
|
|
95 |
|
|
96 |
fun process_spec cos alt_name sprop int thy =
|
|
97 |
let
|
|
98 |
val sg = sign_of thy
|
|
99 |
fun typ_equiv t u =
|
|
100 |
let
|
|
101 |
val tsig = Sign.tsig_of sg
|
|
102 |
in
|
|
103 |
Type.typ_instance(tsig,t,u) andalso
|
|
104 |
Type.typ_instance(tsig,u,t)
|
|
105 |
end
|
|
106 |
val prop = term_of (Thm.read_cterm sg (sprop,HOLogic.boolT))
|
|
107 |
val (prop_thawed,vmap) = Type.varify (prop,[])
|
|
108 |
val thawed_prop_consts = collect_consts (prop_thawed,[])
|
|
109 |
val (sconsts,overloaded) = Library.split_list cos
|
|
110 |
val consts = map (term_of o Thm.read_cterm sg o rpair TypeInfer.logicT) sconsts
|
|
111 |
val _ = assert (not (Library.exists (not o Term.is_Const) consts))
|
|
112 |
"Non-constant found as parameter"
|
|
113 |
fun proc_const c =
|
|
114 |
let
|
|
115 |
val c' = fst (Type.varify (c,[]))
|
|
116 |
val (cname,ctyp) = dest_Const c'
|
|
117 |
in
|
|
118 |
case filter (fn t => let val (name,typ) = dest_Const t
|
|
119 |
in name = cname andalso typ_equiv typ ctyp
|
|
120 |
end) thawed_prop_consts of
|
|
121 |
[] => error ("Constant \"" ^ (Sign.string_of_term sg c) ^ "\" not found in specification")
|
|
122 |
| [cf] => unvarify cf vmap
|
|
123 |
| _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification")
|
|
124 |
end
|
|
125 |
val proc_consts = map proc_const consts
|
|
126 |
fun mk_exist (c,prop) =
|
|
127 |
let
|
|
128 |
val T = type_of c
|
|
129 |
in
|
|
130 |
HOLogic.exists_const T $ Abs("x",T,Term.abstract_over (c,prop))
|
|
131 |
end
|
|
132 |
val ex_prop = foldr mk_exist (proc_consts,prop)
|
|
133 |
val cnames = map (fst o dest_Const) proc_consts
|
|
134 |
in
|
|
135 |
IsarThy.theorem_i Drule.internalK
|
|
136 |
(("",[add_specification (cnames ~~ overloaded) alt_name]),
|
|
137 |
(HOLogic.mk_Trueprop ex_prop,([],[]))) int thy
|
|
138 |
end
|
|
139 |
|
|
140 |
(* outer syntax *)
|
|
141 |
|
|
142 |
local structure P = OuterParse and K = OuterSyntax.Keyword in
|
|
143 |
|
|
144 |
(* taken from ~~/Pure/Isar/isar_syn.ML *)
|
|
145 |
val opt_overloaded =
|
|
146 |
Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false
|
|
147 |
|
|
148 |
val specification_decl =
|
|
149 |
P.$$$ "(" |-- Scan.repeat1 (P.term -- opt_overloaded) --| P.$$$ ")" --
|
|
150 |
P.opt_thm_name ":" -- P.prop
|
|
151 |
|
|
152 |
val specificationP =
|
|
153 |
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
|
|
154 |
(specification_decl >> (fn ((cos,alt_name), prop) =>
|
|
155 |
Toplevel.print o (Toplevel.theory_to_proof (process_spec cos alt_name prop))))
|
|
156 |
|
|
157 |
val _ = OuterSyntax.add_parsers [specificationP]
|
|
158 |
|
|
159 |
end
|
|
160 |
|
|
161 |
|
|
162 |
end
|