author | wenzelm |
Fri, 29 Sep 2006 22:47:01 +0200 | |
changeset 20784 | eece9aaaf352 |
parent 19664 | e1dc01a48a52 |
child 20890 | 052bde912a51 |
permissions | -rw-r--r-- |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/specification.ML |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
4 |
|
19664 | 5 |
Common local_theory specifications --- with type-inference and |
18810 | 6 |
toplevel polymorphism. |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
7 |
*) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
8 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
9 |
signature SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
10 |
sig |
18771 | 11 |
val read_specification: (string * string option * mixfix) list -> |
18954 | 12 |
((string * Attrib.src list) * string list) list -> local_theory -> |
18771 | 13 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
18954 | 14 |
local_theory |
18771 | 15 |
val cert_specification: (string * typ option * mixfix) list -> |
18954 | 16 |
((string * Attrib.src list) * term list) list -> local_theory -> |
18771 | 17 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
18954 | 18 |
local_theory |
19 |
val axiomatization: (string * string option * mixfix) list -> |
|
20 |
((bstring * Attrib.src list) * string list) list -> local_theory -> |
|
21 |
(term list * (bstring * thm list) list) * local_theory |
|
22 |
val axiomatization_i: (string * typ option * mixfix) list -> |
|
23 |
((bstring * Attrib.src list) * term list) list -> local_theory -> |
|
24 |
(term list * (bstring * thm list) list) * local_theory |
|
25 |
val definition: |
|
18786 | 26 |
((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list -> |
18954 | 27 |
local_theory -> (term * (bstring * thm)) list * local_theory |
28 |
val definition_i: |
|
18786 | 29 |
((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list -> |
18954 | 30 |
local_theory -> (term * (bstring * thm)) list * local_theory |
20784 | 31 |
val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list -> |
19080 | 32 |
local_theory -> local_theory |
20784 | 33 |
val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list -> |
19080 | 34 |
local_theory -> local_theory |
20784 | 35 |
val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory |
36 |
val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
37 |
end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
38 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
39 |
structure Specification: SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
40 |
struct |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
41 |
|
19664 | 42 |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
43 |
(* prepare specification *) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
44 |
|
18828 | 45 |
fun prep_specification prep_vars prep_propp prep_att raw_vars raw_specs ctxt = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
46 |
let |
18670 | 47 |
val thy = ProofContext.theory_of ctxt; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
48 |
|
18670 | 49 |
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; |
50 |
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
|
51 |
val ((specs, vs), specs_ctxt) = |
|
19585 | 52 |
prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
53 |
|> swap |>> map (map fst) |
18771 | 54 |
||>> fold_map ProofContext.inferred_param xs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
55 |
|
18771 | 56 |
val params = vs ~~ map #3 vars; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
57 |
val names = map (fst o fst) raw_specs; |
18670 | 58 |
val atts = map (map (prep_att thy) o snd o fst) raw_specs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
59 |
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
60 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
61 |
fun read_specification x = |
18771 | 62 |
prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
63 |
fun cert_specification x = |
18670 | 64 |
prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
65 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
66 |
|
18771 | 67 |
(* axiomatization *) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
68 |
|
18954 | 69 |
fun gen_axioms prep raw_vars raw_specs ctxt = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
70 |
let |
18786 | 71 |
val (vars, specs) = fst (prep raw_vars raw_specs ctxt); |
18828 | 72 |
val cs = map fst vars; |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
73 |
val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []); |
18786 | 74 |
|
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
75 |
val (consts, consts_ctxt) = ctxt |> LocalTheory.consts_restricted spec_frees vars; |
18828 | 76 |
val subst = Term.subst_atomic (map Free cs ~~ consts); |
18786 | 77 |
|
18771 | 78 |
val (axioms, axioms_ctxt) = |
79 |
consts_ctxt |
|
80 |
|> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props))) |
|
18786 | 81 |
||> LocalTheory.theory (Theory.add_finals_i false (map Term.head_of consts)); |
18954 | 82 |
val _ = LocalTheory.print_consts ctxt spec_frees cs; |
83 |
in ((consts, axioms), axioms_ctxt) end; |
|
18786 | 84 |
|
18954 | 85 |
val axiomatization = gen_axioms read_specification; |
86 |
val axiomatization_i = gen_axioms cert_specification; |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
87 |
|
18786 | 88 |
|
89 |
(* definition *) |
|
90 |
||
18954 | 91 |
fun gen_defs prep args ctxt = |
18786 | 92 |
let |
18954 | 93 |
fun define (raw_var, (raw_a, raw_prop)) ctxt' = |
18786 | 94 |
let |
18954 | 95 |
val (vars, [(a, [prop])]) = fst (prep (the_list raw_var) [(raw_a, [raw_prop])] ctxt'); |
96 |
val (((x, T), rhs), prove) = LocalDefs.derived_def ctxt' true prop; |
|
18786 | 97 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
98 |
if x = x' then mx |
|
99 |
else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
18810 | 100 |
in |
18954 | 101 |
ctxt' |
18810 | 102 |
|> LocalTheory.def_finish prove ((x, mx), (a, rhs)) |
103 |
|>> pair (x, T) |
|
104 |
end; |
|
18786 | 105 |
|
18828 | 106 |
val ((cs, defs), defs_ctxt) = ctxt |> fold_map define args |>> split_list; |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
107 |
val def_frees = member (op =) (fold (Term.add_frees o fst) defs []); |
18954 | 108 |
val _ = LocalTheory.print_consts ctxt def_frees cs; |
109 |
in (defs, defs_ctxt) end; |
|
18786 | 110 |
|
18954 | 111 |
val definition = gen_defs read_specification; |
112 |
val definition_i = gen_defs cert_specification; |
|
18786 | 113 |
|
19080 | 114 |
|
115 |
(* abbreviation *) |
|
116 |
||
19544 | 117 |
fun gen_abbrevs prep mode args ctxt = |
19080 | 118 |
let |
119 |
fun abbrev (raw_var, raw_prop) ctxt' = |
|
120 |
let |
|
19372
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
121 |
val ((vars, [(_, [prop])]), _) = |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
122 |
prep (the_list raw_var) [(("", []), [raw_prop])] |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
123 |
(ctxt' |> ProofContext.expand_abbrevs false); |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
124 |
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def ctxt' prop)); |
19080 | 125 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
126 |
if x = x' then mx |
|
127 |
else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
128 |
in |
|
129 |
ctxt' |
|
19664 | 130 |
|> LocalTheory.abbrevs mode [((x, mx), rhs)] |
19080 | 131 |
|> pair (x, T) |
132 |
end; |
|
133 |
||
19664 | 134 |
val (cs, result_ctxt) = ctxt |
19544 | 135 |
|> ProofContext.set_syntax_mode mode |
136 |
|> fold_map abbrev args |
|
137 |
||> ProofContext.restore_syntax_mode ctxt; |
|
19080 | 138 |
val _ = LocalTheory.print_consts ctxt (K false) cs; |
19664 | 139 |
in result_ctxt end; |
19080 | 140 |
|
141 |
val abbreviation = gen_abbrevs read_specification; |
|
142 |
val abbreviation_i = gen_abbrevs cert_specification; |
|
143 |
||
19664 | 144 |
|
145 |
(* const syntax *) |
|
146 |
||
147 |
fun gen_syntax intern_const mode raw_args ctxt = |
|
148 |
let val args = raw_args |> map (apfst (intern_const (ProofContext.consts_of ctxt))) |
|
149 |
in ctxt |> LocalTheory.syntax mode args end; |
|
150 |
||
151 |
val const_syntax = gen_syntax Consts.intern; |
|
152 |
val const_syntax_i = gen_syntax (K I); |
|
153 |
||
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
154 |
end; |