author | wenzelm |
Sun, 07 May 2006 00:22:05 +0200 | |
changeset 19585 | 70a1ce3b23ae |
parent 19544 | e3a39dae2004 |
child 19664 | e1dc01a48a52 |
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 |
|
18810 | 5 |
Common theory/locale specifications --- with type-inference and |
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 |
19372
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
31 |
val abbreviation: string * bool -> ((string * string option * mixfix) option * string) list -> |
19080 | 32 |
local_theory -> local_theory |
19372
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
33 |
val abbreviation_i: string * bool -> ((string * typ option * mixfix) option * term) list -> |
19080 | 34 |
local_theory -> local_theory |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
35 |
end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
36 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
37 |
structure Specification: SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
38 |
struct |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
39 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
40 |
(* prepare specification *) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
41 |
|
18828 | 42 |
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
|
43 |
let |
18670 | 44 |
val thy = ProofContext.theory_of ctxt; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
45 |
|
18670 | 46 |
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; |
47 |
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
|
48 |
val ((specs, vs), specs_ctxt) = |
|
19585 | 49 |
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
|
50 |
|> swap |>> map (map fst) |
18771 | 51 |
||>> fold_map ProofContext.inferred_param xs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
52 |
|
18771 | 53 |
val params = vs ~~ map #3 vars; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
54 |
val names = map (fst o fst) raw_specs; |
18670 | 55 |
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
|
56 |
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
57 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
58 |
fun read_specification x = |
18771 | 59 |
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
|
60 |
fun cert_specification x = |
18670 | 61 |
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
|
62 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
63 |
|
18771 | 64 |
(* axiomatization *) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
65 |
|
18954 | 66 |
fun gen_axioms prep raw_vars raw_specs ctxt = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
67 |
let |
18786 | 68 |
val (vars, specs) = fst (prep raw_vars raw_specs ctxt); |
18828 | 69 |
val cs = map fst vars; |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
70 |
val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []); |
18786 | 71 |
|
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
72 |
val (consts, consts_ctxt) = ctxt |> LocalTheory.consts_restricted spec_frees vars; |
18828 | 73 |
val subst = Term.subst_atomic (map Free cs ~~ consts); |
18786 | 74 |
|
18771 | 75 |
val (axioms, axioms_ctxt) = |
76 |
consts_ctxt |
|
77 |
|> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props))) |
|
18786 | 78 |
||> LocalTheory.theory (Theory.add_finals_i false (map Term.head_of consts)); |
18954 | 79 |
val _ = LocalTheory.print_consts ctxt spec_frees cs; |
80 |
in ((consts, axioms), axioms_ctxt) end; |
|
18786 | 81 |
|
18954 | 82 |
val axiomatization = gen_axioms read_specification; |
83 |
val axiomatization_i = gen_axioms cert_specification; |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
84 |
|
18786 | 85 |
|
86 |
(* definition *) |
|
87 |
||
18954 | 88 |
fun gen_defs prep args ctxt = |
18786 | 89 |
let |
18954 | 90 |
fun define (raw_var, (raw_a, raw_prop)) ctxt' = |
18786 | 91 |
let |
18954 | 92 |
val (vars, [(a, [prop])]) = fst (prep (the_list raw_var) [(raw_a, [raw_prop])] ctxt'); |
93 |
val (((x, T), rhs), prove) = LocalDefs.derived_def ctxt' true prop; |
|
18786 | 94 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
95 |
if x = x' then mx |
|
96 |
else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
18810 | 97 |
in |
18954 | 98 |
ctxt' |
18810 | 99 |
|> LocalTheory.def_finish prove ((x, mx), (a, rhs)) |
100 |
|>> pair (x, T) |
|
101 |
end; |
|
18786 | 102 |
|
18828 | 103 |
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
|
104 |
val def_frees = member (op =) (fold (Term.add_frees o fst) defs []); |
18954 | 105 |
val _ = LocalTheory.print_consts ctxt def_frees cs; |
106 |
in (defs, defs_ctxt) end; |
|
18786 | 107 |
|
18954 | 108 |
val definition = gen_defs read_specification; |
109 |
val definition_i = gen_defs cert_specification; |
|
18786 | 110 |
|
19080 | 111 |
|
112 |
(* abbreviation *) |
|
113 |
||
19544 | 114 |
fun gen_abbrevs prep mode args ctxt = |
19080 | 115 |
let |
116 |
fun abbrev (raw_var, raw_prop) ctxt' = |
|
117 |
let |
|
19372
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
118 |
val ((vars, [(_, [prop])]), _) = |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
119 |
prep (the_list raw_var) [(("", []), [raw_prop])] |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
120 |
(ctxt' |> ProofContext.expand_abbrevs false); |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
121 |
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def ctxt' prop)); |
19080 | 122 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
123 |
if x = x' then mx |
|
124 |
else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
125 |
in |
|
126 |
ctxt' |
|
19544 | 127 |
|> LocalTheory.abbrev mode ((x, mx), rhs) |
19080 | 128 |
|> pair (x, T) |
129 |
end; |
|
130 |
||
19544 | 131 |
val (cs, abbrs_ctxt) = ctxt |
132 |
|> ProofContext.set_syntax_mode mode |
|
133 |
|> fold_map abbrev args |
|
134 |
||> ProofContext.restore_syntax_mode ctxt; |
|
19080 | 135 |
val _ = LocalTheory.print_consts ctxt (K false) cs; |
136 |
in abbrs_ctxt end; |
|
137 |
||
138 |
val abbreviation = gen_abbrevs read_specification; |
|
139 |
val abbreviation_i = gen_abbrevs cert_specification; |
|
140 |
||
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
141 |
end; |