author  wenzelm 
Sat, 19 Nov 2011 13:02:50 +0100  
changeset 45584  41a768a431a6 
parent 45583  93499f36d59a 
child 45600  1bbbac9a0cb0 
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 
Author: Makarius 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

3 

21036  4 
Derived local theory specifications  with typeinference and 
18810  5 
toplevel polymorphism. 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

6 
*) 
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 
signature SPECIFICATION = 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

9 
sig 
30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

10 
val check_spec: 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

11 
(binding * typ option * mixfix) list > (Attrib.binding * term) list > Proof.context > 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

12 
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

13 
val read_spec: 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

14 
(binding * string option * mixfix) list > (Attrib.binding * string) list > Proof.context > 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

15 
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

16 
val check_free_spec: 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

17 
(binding * typ option * mixfix) list > (Attrib.binding * term) list > Proof.context > 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

18 
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

19 
val read_free_spec: 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

20 
(binding * string option * mixfix) list > (Attrib.binding * string) list > Proof.context > 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

21 
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context 
29581  22 
val check_specification: (binding * typ option * mixfix) list > 
30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

23 
(Attrib.binding * term list) list > Proof.context > 
29581  24 
(((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context 
25 
val read_specification: (binding * string option * mixfix) list > 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

26 
(Attrib.binding * string list) list > Proof.context > 
29581  27 
(((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context 
28 
val axiomatization: (binding * typ option * mixfix) list > 

28114  29 
(Attrib.binding * term list) list > theory > 
33703
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

30 
(term list * thm list list) * theory 
29581  31 
val axiomatization_cmd: (binding * string option * mixfix) list > 
28114  32 
(Attrib.binding * string list) list > theory > 
33703
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

33 
(term list * thm list list) * theory 
35894  34 
val axiom: Attrib.binding * term > theory > thm * theory 
35 
val axiom_cmd: Attrib.binding * string > theory > thm * theory 

18954  36 
val definition: 
29581  37 
(binding * typ option * mixfix) option * (Attrib.binding * term) > 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

38 
local_theory > (term * (string * thm)) * local_theory 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

39 
val definition': 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

40 
(binding * typ option * mixfix) option * (Attrib.binding * term) > 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

41 
bool > local_theory > (term * (string * thm)) * local_theory 
24927
48e08f37ce92
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24848
diff
changeset

42 
val definition_cmd: 
29581  43 
(binding * string option * mixfix) option * (Attrib.binding * string) > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

44 
bool > local_theory > (term * (string * thm)) * local_theory 
29581  45 
val abbreviation: Syntax.mode > (binding * typ option * mixfix) option * term > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

46 
bool > local_theory > local_theory 
29581  47 
val abbreviation_cmd: Syntax.mode > (binding * string option * mixfix) option * string > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

48 
bool > local_theory > local_theory 
35413  49 
val type_notation: bool > Syntax.mode > (typ * mixfix) list > local_theory > local_theory 
50 
val type_notation_cmd: bool > Syntax.mode > (string * mixfix) list > local_theory > local_theory 

24949  51 
val notation: bool > Syntax.mode > (term * mixfix) list > local_theory > local_theory 
52 
val notation_cmd: bool > Syntax.mode > (string * mixfix) list > local_theory > local_theory 

28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

53 
val theorems: string > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

54 
(Attrib.binding * (thm list * Attrib.src list) list) list > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

55 
bool > local_theory > (string * thm list) list * local_theory 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25371
diff
changeset

56 
val theorems_cmd: string > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

57 
(Attrib.binding * (Facts.ref * Attrib.src list) list) list > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

58 
bool > local_theory > (string * thm list) list * local_theory 
24986  59 
val theorem: string > Method.text option > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

60 
(thm list list > local_theory > local_theory) > Attrib.binding > 
28710  61 
Element.context_i list > Element.statement_i > 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

62 
bool > local_theory > Proof.state 
24986  63 
val theorem_cmd: string > Method.text option > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

64 
(thm list list > local_theory > local_theory) > Attrib.binding > 
28710  65 
Element.context list > Element.statement > 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

66 
bool > local_theory > Proof.state 
36317
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

67 
val schematic_theorem: string > Method.text option > 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

68 
(thm list list > local_theory > local_theory) > Attrib.binding > 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

69 
Element.context_i list > Element.statement_i > 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

70 
bool > local_theory > Proof.state 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

71 
val schematic_theorem_cmd: string > Method.text option > 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

72 
(thm list list > local_theory > local_theory) > Attrib.binding > 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

73 
Element.context list > Element.statement > 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

74 
bool > local_theory > Proof.state 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

75 
val add_theorem_hook: (bool > Proof.state > Proof.state) > Context.generic > Context.generic 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

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

77 

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

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

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

80 

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

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

82 

24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

83 
local 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

84 

0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

85 
fun close_forms ctxt i xs As = 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

86 
let 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

87 
val commons = map #1 xs; 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

88 
val _ = 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

89 
(case duplicates (op =) commons of [] => () 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

90 
 dups => error ("Duplicate local variables " ^ commas_quote dups)); 
42482  91 
val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons)); 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42494
diff
changeset

92 
val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees)); 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

93 
val uniform_typing = the o AList.lookup (op =) (frees ~~ types); 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

94 

0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

95 
fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b) 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

96 
 abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

97 
 abs_body lev y (t as Free (x, T)) = 
39288  98 
if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev)) 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

99 
else t 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

100 
 abs_body _ _ a = a; 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

101 
fun close (y, U) B = 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

102 
let val B' = abs_body 0 y (Term.incr_boundvars 1 B) 
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
41472
diff
changeset

103 
in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end; 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

104 
fun close_form A = 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

105 
let 
42482  106 
val occ_frees = rev (Variable.add_free_names ctxt A []); 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

107 
val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees); 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

108 
in fold_rev close bounds A end; 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

109 
in map close_form As end; 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

110 

30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

111 
fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt = 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

112 
let 
42360  113 
val thy = Proof_Context.theory_of ctxt; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

114 

18670  115 
val (vars, vars_ctxt) = ctxt > prep_vars raw_vars; 
42360  116 
val (xs, params_ctxt) = vars_ctxt > Proof_Context.add_fixes vars; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

117 

42265  118 
val Asss = 
119 
(map o map) snd raw_specss 

120 
> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt)); 

24734  121 
val names = Variable.names_of (params_ctxt > (fold o fold o fold) Variable.declare_term Asss) 
122 
> fold Name.declare xs; 

123 
val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names); 

124 
val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1; 

24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

125 
val specs = 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

126 
(if do_close then 
24734  127 
#1 (fold_map 
128 
(fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss' idx) 

129 
else Asss') 

24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

130 
> flat > burrow (Syntax.check_props params_ctxt); 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

131 
val specs_ctxt = params_ctxt > (fold o fold) Variable.declare_term specs; 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

132 

42360  133 
val Ts = specs_ctxt > fold_map Proof_Context.inferred_param xs > fst; 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

134 
val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts; 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

135 
val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss); 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

136 
in ((params, name_atts ~~ specs), specs_ctxt) end; 
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

137 

30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

138 

6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

139 
fun single_spec (a, prop) = [(a, [prop])]; 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

140 
fun the_spec (a, [prop]) = (a, prop); 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

141 

6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

142 
fun prep_spec prep_vars parse_prop prep_att do_close vars specs = 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

143 
prepare prep_vars parse_prop prep_att do_close 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

144 
vars (map single_spec specs) #>> apsnd (map the_spec); 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

145 

24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

146 
in 
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21359
diff
changeset

147 

42360  148 
fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x; 
149 
fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true x; 

30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

150 

42360  151 
fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x; 
152 
fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src false x; 

30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

153 

6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

154 
fun check_specification vars specs = 
42360  155 
prepare Proof_Context.cert_vars (K I) (K I) true vars [specs]; 
30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

156 

6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

157 
fun read_specification vars specs = 
42360  158 
prepare Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs]; 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

159 

0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

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

161 

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

162 

28114  163 
(* axiomatization  within global theory *) 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

164 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

165 
fun gen_axioms prep raw_vars raw_specs thy = 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

166 
let 
42360  167 
val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy); 
42494  168 
val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars; 
28114  169 

170 
(*consts*) 

33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
32856
diff
changeset

171 
val (consts, consts_thy) = thy > fold_map Theory.specify_const vars; 
28114  172 
val subst = Term.subst_atomic (map Free xs ~~ consts); 
173 

174 
(*axioms*) 

30470
9ae8f9d78cd3
axiomatization: more precise treatment of binding;
wenzelm
parents:
30434
diff
changeset

175 
val (axioms, axioms_thy) = (specs, consts_thy) > fold_map (fn ((b, atts), props) => 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

176 
fold_map Thm.add_axiom_global 
30470
9ae8f9d78cd3
axiomatization: more precise treatment of binding;
wenzelm
parents:
30434
diff
changeset

177 
(map (apfst (fn a => Binding.map_name (K a) b)) 
42494  178 
(Global_Theory.name_multi (Variable.check_name b) (map subst props))) 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35894
diff
changeset

179 
#>> (fn ths => ((b, atts), [(map #2 ths, [])]))); 
30470
9ae8f9d78cd3
axiomatization: more precise treatment of binding;
wenzelm
parents:
30434
diff
changeset

180 

9ae8f9d78cd3
axiomatization: more precise treatment of binding;
wenzelm
parents:
30434
diff
changeset

181 
(*facts*) 
33703
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

182 
val (facts, facts_lthy) = axioms_thy 
38388  183 
> Named_Target.theory_init 
33703
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

184 
> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms) 
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

185 
> Local_Theory.notes axioms; 
30470
9ae8f9d78cd3
axiomatization: more precise treatment of binding;
wenzelm
parents:
30434
diff
changeset

186 

33703
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

187 
in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end; 
18786  188 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

189 
val axiomatization = gen_axioms check_specification; 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

190 
val axiomatization_cmd = gen_axioms read_specification; 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

191 

35894  192 
fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd); 
193 
fun axiom_cmd (b, ax) = axiomatization_cmd [] [(b, [ax])] #>> (hd o hd o snd); 

194 

18786  195 

196 
(* definition *) 

197 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

198 
fun gen_def prep (raw_var, raw_spec) int lthy = 
18786  199 
let 
30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

200 
val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy); 
35624  201 
val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop; 
30434  202 
val var as (b, _) = 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

203 
(case vars of 
28965  204 
[] => (Binding.name x, NoSyn) 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

205 
 [((b, _), mx)] => 
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

206 
let 
42494  207 
val y = Variable.check_name b; 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

208 
val _ = x = y orelse 
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

209 
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ 
28941  210 
Position.str_of (Binding.pos_of b)); 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

211 
in (b, mx) end); 
30434  212 
val name = Thm.def_binding_optional b raw_name; 
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

213 
val ((lhs, (_, raw_th)), lthy2) = lthy 
33765
47b5db097646
Specification.definition: Thm.definitionK marks exactly the highlevel enduser result;
wenzelm
parents:
33756
diff
changeset

214 
> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs)); 
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

215 

4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

216 
val th = prove lthy2 raw_th; 
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

217 
val lthy3 = lthy2 > Spec_Rules.add Spec_Rules.Equational ([lhs], [th]); 
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

218 

33670
02b7738aef6a
eliminated slightly odd kind argument of LocalTheory.note(s);
wenzelm
parents:
33644
diff
changeset

219 
val ([(def_name, [th'])], lthy4) = lthy3 
42440
5e7a7343ab11
discontinuend obsolete Thm.definitionK, which was hardly ever welldefined;
wenzelm
parents:
42375
diff
changeset

220 
> Local_Theory.notes_kind "" 
33756
47b7c9e0bf6e
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
bulwahn
parents:
33703
diff
changeset

221 
[((name, Code.add_default_eqn_attrib :: atts), [([th], [])])]; 
18786  222 

33671  223 
val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs; 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

224 

a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

225 
val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)]; 
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

226 
in ((lhs, (def_name, th')), lthy4) end; 
18786  227 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

228 
val definition' = gen_def check_free_spec; 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

229 
fun definition spec = definition' spec false; 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

230 
val definition_cmd = gen_def read_free_spec; 
18786  231 

19080  232 

233 
(* abbreviation *) 

234 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

235 
fun gen_abbrev prep mode (raw_var, raw_prop) int lthy = 
19080  236 
let 
30482
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

237 
val ((vars, [(_, prop)]), _) = 
6e3c92de4a7d
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
wenzelm
parents:
30472
diff
changeset

238 
prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)] 
42360  239 
(lthy > Proof_Context.set_mode Proof_Context.mode_abbrev); 
35624  240 
val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop)); 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

241 
val var = 
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

242 
(case vars of 
28965  243 
[] => (Binding.name x, NoSyn) 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

244 
 [((b, _), mx)] => 
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

245 
let 
42494  246 
val y = Variable.check_name b; 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

247 
val _ = x = y orelse 
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

248 
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ 
28941  249 
Position.str_of (Binding.pos_of b)); 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

250 
in (b, mx) end); 
21705  251 
val lthy' = lthy 
42360  252 
> Proof_Context.set_syntax_mode mode (* FIXME ?!? *) 
33671  253 
> Local_Theory.abbrev mode (var, rhs) > snd 
42360  254 
> Proof_Context.restore_syntax_mode lthy; 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

255 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

256 
val _ = Proof_Display.print_consts int lthy' (K false) [(x, T)]; 
21532  257 
in lthy' end; 
19080  258 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

259 
val abbreviation = gen_abbrev check_free_spec; 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

260 
val abbreviation_cmd = gen_abbrev read_free_spec; 
19080  261 

19664  262 

21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset

263 
(* notation *) 
19664  264 

35413  265 
local 
266 

267 
fun gen_type_notation prep_type add mode args lthy = 

268 
lthy > Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args); 

269 

24949  270 
fun gen_notation prep_const add mode args lthy = 
33671  271 
lthy > Local_Theory.notation add mode (map (apfst (prep_const lthy)) args); 
19664  272 

35413  273 
in 
274 

275 
val type_notation = gen_type_notation (K I); 

42360  276 
val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false); 
35413  277 

24927
48e08f37ce92
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24848
diff
changeset

278 
val notation = gen_notation (K I); 
42360  279 
val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT); 
19664  280 

35413  281 
end; 
282 

20914  283 

21036  284 
(* fact statements *) 
20914  285 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

286 
fun gen_theorems prep_fact prep_att kind raw_facts int lthy = 
20914  287 
let 
42360  288 
val attrib = prep_att (Proof_Context.theory_of lthy); 
20914  289 
val facts = raw_facts > map (fn ((name, atts), bs) => 
290 
((name, map attrib atts), 

26345
f70620a4cf81
renamed former get_thms(_silent) to get_fact(_silent);
wenzelm
parents:
26336
diff
changeset

291 
bs > map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts)))); 
33671  292 
val (res, lthy') = lthy > Local_Theory.notes_kind kind facts; 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

293 
val _ = Proof_Display.print_results int lthy' ((kind, ""), res); 
20914  294 
in (res, lthy') end; 
295 

24927
48e08f37ce92
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24848
diff
changeset

296 
val theorems = gen_theorems (K I) (K I); 
42360  297 
val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src; 
20914  298 

21036  299 

21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset

300 
(* complex goal statements *) 
21036  301 

302 
local 

303 

21236  304 
fun prep_statement prep_att prep_stmt elems concl ctxt = 
305 
(case concl of 

306 
Element.Shows shows => 

21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset

307 
let 
28880  308 
val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt; 
30472  309 
val prems = Assumption.local_prems_of elems_ctxt ctxt; 
45390
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45327
diff
changeset

310 
val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp); 
45327  311 
val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt; 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

312 
in (([], prems, stmt, NONE), goal_ctxt) end 
21236  313 
 Element.Obtains obtains => 
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset

314 
let 
28862  315 
val case_names = obtains > map_index (fn (i, (b, _)) => 
42494  316 
if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b); 
21236  317 
val constraints = obtains > map (fn (_, (vars, _)) => 
28710  318 
Element.Constrains 
42494  319 
(vars > map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T)  _ => NONE))); 
21036  320 

21236  321 
val raw_propp = obtains > map (fn (_, (_, props)) => map (rpair []) props); 
28880  322 
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt; 
21236  323 

42360  324 
val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN; 
21036  325 

21236  326 
fun assume_case ((name, (vars, _)), asms) ctxt' = 
327 
let 

28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

328 
val bs = map fst vars; 
42494  329 
val xs = map Variable.check_name bs; 
21236  330 
val props = map fst asms; 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

331 
val (Ts, _) = ctxt' 
21236  332 
> fold Variable.declare_term props 
42360  333 
> fold_map Proof_Context.inferred_param xs; 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

334 
val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis)); 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

335 
val _ = ctxt' > Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs); 
21236  336 
in 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

337 
ctxt' 
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

338 
> Variable.auto_fixes asm 
42360  339 
> Proof_Context.add_assms_i Assumption.assume_export 
33369  340 
[((name, [Context_Rules.intro_query NONE]), [(asm, [])])] 
21236  341 
>> (fn [(_, [th])] => th) 
342 
end; 

343 

45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

344 
val more_atts = map (Attrib.internal o K) 
33368  345 
[Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names]; 
30472  346 
val prems = Assumption.local_prems_of elems_ctxt ctxt; 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

347 
val stmt = [((Binding.empty, []), [(thesis, [])])]; 
21236  348 

349 
val (facts, goal_ctxt) = elems_ctxt 

42360  350 
> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]) 
21236  351 
> fold_map assume_case (obtains ~~ propp) 
33644
5266a72e0889
eliminated slightly odd (unused) "axiom" and "assumption"  collapsed to unspecific "";
wenzelm
parents:
33519
diff
changeset

352 
> (fn ths => 
42360  353 
Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #> 
33644
5266a72e0889
eliminated slightly odd (unused) "axiom" and "assumption"  collapsed to unspecific "";
wenzelm
parents:
33519
diff
changeset

354 
#2 #> pair ths); 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

355 
in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end); 
21036  356 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37145
diff
changeset

357 
structure Theorem_Hook = Generic_Data 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

358 
( 
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

359 
type T = ((bool > Proof.state > Proof.state) * stamp) list; 
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

360 
val empty = []; 
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

361 
val extend = I; 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
39557
diff
changeset

362 
fun merge data : T = Library.merge (eq_snd op =) data; 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

363 
); 
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

364 

36317
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

365 
fun gen_theorem schematic prep_att prep_stmt 
28858  366 
kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy = 
21036  367 
let 
33671  368 
val _ = Local_Theory.affirm lthy; 
42360  369 
val thy = Proof_Context.theory_of lthy; 
21036  370 

21435  371 
val attrib = prep_att thy; 
28710  372 
val elems = raw_elems > map (Element.map_ctxt_attrib attrib); 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

373 
val ((more_atts, prems, stmt, facts), goal_ctxt) = 
28880  374 
prep_statement attrib prep_stmt elems raw_concl lthy; 
45583
93499f36d59a
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
wenzelm
parents:
45390
diff
changeset

375 
val atts = more_atts @ map attrib raw_atts; 
21036  376 

377 
fun after_qed' results goal_ctxt' = 

45584
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

378 
let 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

379 
val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results; 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

380 
val (res, lthy') = 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

381 
if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy) 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

382 
else 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

383 
Local_Theory.notes_kind kind 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

384 
(map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

385 
val lthy'' = 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

386 
if Attrib.is_empty_binding (name, atts) then 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

387 
(Proof_Display.print_results int lthy' ((kind, ""), res); lthy') 
28080
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

388 
else 
4723eb2456ce
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27858
diff
changeset

389 
let 
45584
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

390 
val ([(res_name, _)], lthy'') = 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

391 
Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

392 
val _ = Proof_Display.print_results int lthy' ((kind, res_name), res); 
45584
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

393 
in lthy'' end; 
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

394 
in after_qed results' lthy'' end; 
21036  395 
in 
396 
goal_ctxt 

42360  397 
> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])] 
21450  398 
> snd 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36317
diff
changeset

399 
> Proof.theorem before_qed after_qed' (map snd stmt) 
32856
92d9555ac790
clarified Proof.refine_insert  always "refine" to apply standard method treatment (of conjunctions);
wenzelm
parents:
32786
diff
changeset

400 
> (case facts of NONE => I  SOME ths => Proof.refine_insert ths) 
36317
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

401 
> tap (fn state => not schematic andalso Proof.schematic_goal state andalso 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

402 
error "Illegal schematic goal statement") 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37145
diff
changeset

403 
> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt)))) 
21036  404 
end; 
405 

21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset

406 
in 
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset

407 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

408 
val theorem' = gen_theorem false (K I) Expression.cert_statement; 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

409 
fun theorem a b c d e f = theorem' a b c d e f; 
36317
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

410 
val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement; 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

411 

506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

412 
val schematic_theorem = gen_theorem true (K I) Expression.cert_statement; 
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

413 
val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement; 
21036  414 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37145
diff
changeset

415 
fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ())); 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

416 

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

417 
end; 
21036  418 

419 
end; 