author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18670  c3f445b92aff 
child 18771  63efe00371af 
permissions  rwrr 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Isar/specification.ML 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

4 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

5 
Theory specifications  with typeinference, but no internal 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

6 
polymorphism. 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

7 
*) 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

8 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

9 
signature SPECIFICATION = 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

10 
sig 
18640  11 
val pretty_consts: Proof.context > (string * typ) list > Pretty.T 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

12 
val read_specification: 
18640  13 
(string * string option * mixfix) list * 
14 
((string * Attrib.src list) * string list) list > Proof.context > 

15 
((string * typ * mixfix) list * 

18728  16 
((string * attribute list) * term list) list) * Proof.context 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

17 
val cert_specification: 
18640  18 
(string * typ option * mixfix) list * 
18728  19 
((string * attribute list) * term list) list > Proof.context > 
18640  20 
((string * typ * mixfix) list * 
18728  21 
((string * attribute list) * term list) list) * Proof.context 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

22 
val axiomatize: 
18640  23 
(string * string option * mixfix) list * 
24 
((bstring * Attrib.src list) * string list) list > theory > thm list list * theory 

18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

25 
val axiomatize_i: 
18640  26 
(string * typ option * mixfix) list * 
18728  27 
((bstring * attribute list) * term list) list > theory > 
18640  28 
thm list list * theory 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

29 
end; 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

30 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

31 
structure Specification: SPECIFICATION = 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

32 
struct 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

33 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

34 
(* pretty_consts *) 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

35 

18640  36 
fun pretty_const ctxt (c, T) = 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

37 
Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, 
18640  38 
Pretty.quote (ProofContext.pretty_typ ctxt T)]; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

39 

18640  40 
fun pretty_consts ctxt decls = 
41 
Pretty.big_list "constants" (map (pretty_const ctxt) decls); 

18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

42 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

43 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

44 
(* prepare specification *) 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

45 

18670  46 
fun prep_specification prep_vars prep_propp prep_att 
47 
(raw_vars, raw_specs) ctxt = 

18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

48 
let 
18670  49 
val thy = ProofContext.theory_of ctxt; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

50 

18670  51 
val (vars, vars_ctxt) = ctxt > prep_vars raw_vars; 
52 
val (xs, params_ctxt) = vars_ctxt > ProofContext.add_fixes_i vars; 

53 
val ((specs, vs), specs_ctxt) = 

18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

54 
prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs) 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

55 
> swap >> map (map fst) 
18670  56 
>> fold_map ProofContext.inferred_type xs; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

57 

18670  58 
val params = map2 (fn (x, T) => fn (_, _, mx) => (x, T, mx)) vs vars; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

59 
val names = map (fst o fst) raw_specs; 
18670  60 
val atts = map (map (prep_att thy) o snd o fst) raw_specs; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

61 
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

62 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

63 
fun read_specification x = 
18728  64 
prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.attribute x; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

65 
fun cert_specification x = 
18670  66 
prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

67 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

68 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

69 
(* axiomatize *) 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

70 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

71 
fun gen_axiomatize prep args thy = 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

72 
let 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

73 
val ((consts, specs), ctxt) = prep args (ProofContext.init thy); 
18640  74 
val subst = consts > map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T))); 
75 
val axioms = specs > map (fn ((name, att), ts) => 

18728  76 
((name, map (Term.subst_atomic subst) ts), att)); 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

77 
val (thms, thy') = 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

78 
thy 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

79 
> Theory.add_consts_i consts 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

80 
> PureThy.add_axiomss_i axioms 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

81 
> Theory.add_finals_i false (map snd subst); 
18640  82 
in Pretty.writeln (pretty_consts ctxt (map (dest_Free o fst) subst)); (thms, thy') end; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

83 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

84 
val axiomatize = gen_axiomatize read_specification; 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

85 
val axiomatize_i = gen_axiomatize cert_specification; 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

86 

fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

87 
end; 