author | wenzelm |
Tue, 31 Jan 2006 18:19:36 +0100 | |
changeset 18880 | b8a1c3cdf739 |
parent 18828 | 26b80ed2259b |
child 18954 | ab48b6ac9327 |
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 -> |
12 |
((string * Attrib.src list) * string list) list -> Proof.context -> |
|
13 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
|
14 |
Proof.context |
|
15 |
val cert_specification: (string * typ option * mixfix) list -> |
|
16 |
((string * Attrib.src list) * term list) list -> Proof.context -> |
|
17 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
|
18 |
Proof.context |
|
19 |
val axiomatization: xstring option -> (string * string option * mixfix) list -> |
|
20 |
((bstring * Attrib.src list) * string list) list -> theory -> |
|
18810 | 21 |
(term list * (bstring * thm list) list) * (Proof.context * theory) |
18771 | 22 |
val axiomatization_i: string option -> (string * typ option * mixfix) list -> |
23 |
((bstring * Attrib.src list) * term list) list -> theory -> |
|
18810 | 24 |
(term list * (bstring * thm list) list) * (Proof.context * theory) |
18828 | 25 |
val axiomatization_loc: (string * typ option * mixfix) list -> |
26 |
((bstring * Attrib.src list) * term list) list -> Proof.context -> |
|
27 |
(term list * (bstring * thm list) list) * Proof.context |
|
18786 | 28 |
val definition: xstring option -> |
29 |
((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list -> |
|
18810 | 30 |
theory -> (term * (bstring * thm)) list * (Proof.context * theory) |
18786 | 31 |
val definition_i: string option -> |
32 |
((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list -> |
|
18810 | 33 |
theory -> (term * (bstring * thm)) list * (Proof.context * theory) |
18828 | 34 |
val definition_loc: |
35 |
((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list -> |
|
36 |
Proof.context -> (term * (bstring * thm)) list * Proof.context |
|
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 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
42 |
(* prepare specification *) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
43 |
|
18828 | 44 |
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
|
45 |
let |
18670 | 46 |
val thy = ProofContext.theory_of ctxt; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
47 |
|
18670 | 48 |
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; |
49 |
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
|
50 |
val ((specs, vs), specs_ctxt) = |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
51 |
prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
52 |
|> swap |>> map (map fst) |
18771 | 53 |
||>> fold_map ProofContext.inferred_param xs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
54 |
|
18771 | 55 |
val params = vs ~~ map #3 vars; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
56 |
val names = map (fst o fst) raw_specs; |
18670 | 57 |
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
|
58 |
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
59 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
60 |
fun read_specification x = |
18771 | 61 |
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
|
62 |
fun cert_specification x = |
18670 | 63 |
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
|
64 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
65 |
|
18771 | 66 |
(* axiomatization *) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
67 |
|
18828 | 68 |
fun gen_axioms prep init exit print raw_vars raw_specs context = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
69 |
let |
18828 | 70 |
val ctxt = init context; |
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)); |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
82 |
val _ = print ctxt spec_frees cs; |
18828 | 83 |
in ((consts, axioms), exit axioms_ctxt) end; |
18786 | 84 |
|
18828 | 85 |
fun axiomatization loc = |
86 |
gen_axioms read_specification (LocalTheory.init loc) LocalTheory.exit LocalTheory.print_consts; |
|
87 |
fun axiomatization_i loc = |
|
88 |
gen_axioms cert_specification (LocalTheory.init_i loc) LocalTheory.exit LocalTheory.print_consts; |
|
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
89 |
val axiomatization_loc = gen_axioms cert_specification I I (K (K (K ()))); |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
90 |
|
18786 | 91 |
|
92 |
(* definition *) |
|
93 |
||
18828 | 94 |
fun gen_defs prep init exit print args context = |
18786 | 95 |
let |
96 |
fun define (raw_var, (raw_a, raw_prop)) ctxt = |
|
97 |
let |
|
98 |
val (vars, [(a, [prop])]) = fst (prep (the_list raw_var) [(raw_a, [raw_prop])] ctxt); |
|
18828 | 99 |
val (((x, T), rhs), prove) = LocalDefs.derived_def ctxt prop; |
18786 | 100 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
101 |
if x = x' then mx |
|
102 |
else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
18810 | 103 |
in |
104 |
ctxt |
|
105 |
|> LocalTheory.def_finish prove ((x, mx), (a, rhs)) |
|
106 |
|>> pair (x, T) |
|
107 |
end; |
|
18786 | 108 |
|
18828 | 109 |
val ctxt = init context; |
110 |
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
|
111 |
val def_frees = member (op =) (fold (Term.add_frees o fst) defs []); |
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
112 |
val _ = print ctxt def_frees cs; |
18828 | 113 |
in (defs, exit defs_ctxt) end; |
18786 | 114 |
|
18828 | 115 |
fun definition loc = |
116 |
gen_defs read_specification (LocalTheory.init loc) LocalTheory.exit LocalTheory.print_consts; |
|
117 |
fun definition_i loc = |
|
118 |
gen_defs cert_specification (LocalTheory.init_i loc) LocalTheory.exit LocalTheory.print_consts; |
|
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
119 |
val definition_loc = gen_defs cert_specification I I (K (K (K ()))); |
18786 | 120 |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
121 |
end; |