author  wenzelm 
Mon, 02 Dec 2019 16:28:23 +0100  
changeset 71217  2dee5cd42fde 
parent 71214  5727bcc3c47c 
child 71674  48ff625687f5 
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 
59844
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

10 
val read_props: string list > (binding * string option * mixfix) list > Proof.context > 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

11 
term list * Proof.context 
63180  12 
val check_spec_open: (binding * typ option * mixfix) list > 
13 
(binding * typ option * mixfix) list > term list > term > Proof.context > 

63395  14 
((binding * typ option * mixfix) list * string list * (string > Position.T list) * term) * 
63180  15 
Proof.context 
16 
val read_spec_open: (binding * string option * mixfix) list > 

17 
(binding * string option * mixfix) list > string list > string > Proof.context > 

63395  18 
((binding * typ option * mixfix) list * string list * (string > Position.T list) * term) * 
63180  19 
Proof.context 
63182  20 
type multi_specs = 
21 
((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list 

22 
type multi_specs_cmd = 

23 
((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list 

63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63063
diff
changeset

24 
val check_multi_specs: (binding * typ option * mixfix) list > multi_specs > Proof.context > 
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

25 
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context 
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63063
diff
changeset

26 
val read_multi_specs: (binding * string option * mixfix) list > multi_specs_cmd > Proof.context > 
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

27 
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context 
63178  28 
val axiomatization: (binding * typ option * mixfix) list > 
29 
(binding * typ option * mixfix) list > term list > 

30 
(Attrib.binding * term) list > theory > (term list * thm list) * theory 

31 
val axiomatization_cmd: (binding * string option * mixfix) list > 

32 
(binding * string option * mixfix) list > string list > 

33 
(Attrib.binding * string) list > theory > (term list * thm list) * theory 

35894  34 
val axiom: Attrib.binding * term > theory > thm * theory 
63180  35 
val definition: (binding * typ option * mixfix) option > 
36 
(binding * typ option * mixfix) list > term list > Attrib.binding * term > 

37 
local_theory > (term * (string * thm)) * local_theory 

38 
val definition': (binding * typ option * mixfix) option > 

39 
(binding * typ option * mixfix) list > term list > Attrib.binding * term > 

40 
bool > local_theory > (term * (string * thm)) * local_theory 

41 
val definition_cmd: (binding * string option * mixfix) option > 

42 
(binding * string option * mixfix) list > string list > Attrib.binding * string > 

43 
bool > local_theory > (term * (string * thm)) * local_theory 

44 
val abbreviation: Syntax.mode > (binding * typ option * mixfix) option > 

45 
(binding * typ option * mixfix) list > term > bool > local_theory > local_theory 

46 
val abbreviation_cmd: Syntax.mode > (binding * string option * mixfix) option > 

47 
(binding * string option * mixfix) list > string > bool > local_theory > local_theory 

66248  48 
val alias: binding * string > local_theory > local_theory 
49 
val alias_cmd: binding * (xstring * Position.T) > local_theory > local_theory 

50 
val type_alias: binding * string > local_theory > local_theory 

51 
val type_alias_cmd: binding * (xstring * Position.T) > local_theory > local_theory 

35413  52 
val type_notation: bool > Syntax.mode > (typ * mixfix) list > local_theory > local_theory 
55639  53 
val type_notation_cmd: bool > Syntax.mode > (string * mixfix) list > 
54 
local_theory > local_theory 

24949  55 
val notation: bool > Syntax.mode > (term * mixfix) list > local_theory > local_theory 
56 
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

57 
val theorems: string > 
63267  58 
(Attrib.binding * Attrib.thms) list > 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

59 
(binding * typ option * mixfix) list > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

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

61 
val theorems_cmd: string > 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
56932
diff
changeset

62 
(Attrib.binding * (Facts.ref * Token.src list) list) list > 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

63 
(binding * string option * mixfix) list > 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
43329
diff
changeset

64 
bool > local_theory > (string * thm list) list * local_theory 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

65 
val theorem: bool > string > Method.text option > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

66 
(thm list list > local_theory > local_theory) > Attrib.binding > 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

67 
string list > Element.context_i list > Element.statement_i > 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

68 
bool > local_theory > Proof.state 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

69 
val theorem_cmd: bool > string > Method.text option > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

70 
(thm list list > local_theory > local_theory) > Attrib.binding > 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

71 
(xstring * Position.T) list > Element.context list > Element.statement > 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

72 
bool > local_theory > Proof.state 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

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

74 
(thm list list > local_theory > local_theory) > Attrib.binding > 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

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

76 
bool > local_theory > Proof.state 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

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

78 
(thm list list > local_theory > local_theory) > Attrib.binding > 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

79 
(xstring * Position.T) list > Element.context list > Element.statement > 
36317
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

80 
bool > local_theory > Proof.state 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

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

82 

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

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

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

85 

59844
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

86 
(* prepare propositions *) 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

87 

c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

88 
fun read_props raw_props raw_fixes ctxt = 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

89 
let 
60469  90 
val (_, ctxt1) = ctxt > Proof_Context.add_fixes_cmd raw_fixes; 
59844
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

91 
val props1 = map (Syntax.parse_prop ctxt1) raw_props; 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

92 
val (props2, ctxt2) = ctxt1 > fold_map Variable.fix_dummy_patterns props1; 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

93 
val props3 = Syntax.check_props ctxt2 props2; 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

94 
val ctxt3 = ctxt2 > fold Variable.declare_term props3; 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

95 
in (props3, ctxt3) end; 
c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

96 

c648efffea73
support for minimal specifications, with usual treatment of fixes and dummies;
wenzelm
parents:
58993
diff
changeset

97 

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

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

99 

63394  100 
fun get_positions ctxt x = 
101 
let 

102 
fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t 

103 
 get Cs (Free (y, T)) = 

104 
if x = y then 

105 
map_filter Term_Position.decode_positionT 

106 
(T :: map (Type.constraint_type ctxt) Cs) 

107 
else [] 

108 
 get _ (t $ u) = get [] t @ get [] u 

109 
 get _ (Abs (_, _, t)) = get [] t 

110 
 get _ _ = []; 

111 
in get [] end; 

112 

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

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

114 

63180  115 
fun prep_decls prep_var raw_vars ctxt = 
116 
let 

117 
val (vars, ctxt') = fold_map prep_var raw_vars ctxt; 

118 
val (xs, ctxt'') = ctxt' 

119 
> Context_Position.set_visible false 

120 
> Proof_Context.add_fixes vars 

121 
> Context_Position.restore_visible ctxt'; 

122 
val _ = 

123 
Context_Position.reports ctxt'' 

124 
(map (Binding.pos_of o #1) vars ~~ 

125 
map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs); 

126 
in ((vars, xs), ctxt'') end; 

127 

63182  128 
fun close_form ctxt ys prems concl = 
63396  129 
let 
130 
val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys)); 

131 

132 
val pos_props = Logic.strip_imp_concl concl :: Logic.strip_imp_prems concl @ prems; 

133 
fun get_pos x = maps (get_positions ctxt x) pos_props; 

134 
val _ = Context_Position.reports ctxt (maps (Syntax_Phases.reports_of_scope o get_pos) xs); 

63180  135 
in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end; 
136 

137 
fun dummy_frees ctxt xs tss = 

138 
let 

139 
val names = 

140 
Variable.names_of ((fold o fold) Variable.declare_term tss ctxt) 

141 
> fold Name.declare xs; 

142 
val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names; 

143 
in tss' end; 

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

144 

63180  145 
fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt = 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

146 
let 
63180  147 
val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt; 
148 
val (ys, params_ctxt) = vars_ctxt > fold_map prep_var raw_params > Proof_Context.add_fixes; 

149 

150 
val props = 

151 
map (parse_prop params_ctxt) (raw_concl :: raw_prems) 

152 
> singleton (dummy_frees params_ctxt (xs @ ys)); 

153 

154 
val concl :: prems = Syntax.check_props params_ctxt props; 

155 
val spec = Logic.list_implies (prems, concl); 

156 
val spec_ctxt = Variable.declare_term spec params_ctxt; 

157 

63395  158 
fun get_pos x = maps (get_positions spec_ctxt x) props; 
63180  159 
in ((vars, xs, get_pos, spec), spec_ctxt) end; 
160 

161 
fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt = 

162 
let 

163 
val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt; 

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

164 

63179  165 
val propss0 = 
63182  166 
raw_specss > map (fn ((_, raw_concl), raw_prems, raw_params) => 
167 
let val (ys, ctxt') = vars_ctxt > fold_map prep_var raw_params > Proof_Context.add_fixes 

168 
in (ys, map (pair ctxt') (raw_concl :: raw_prems)) end); 

63179  169 
val props = 
63182  170 
burrow (grouped 10 Par_List.map_independent (uncurry parse_prop)) (map #2 propss0) 
171 
> dummy_frees vars_ctxt xs 

172 
> map2 (fn (ys, _) => fn concl :: prems => close_form vars_ctxt ys prems concl) propss0; 

61947  173 

63180  174 
val specs = Syntax.check_props vars_ctxt props; 
175 
val specs_ctxt = vars_ctxt > fold Variable.declare_term specs; 

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

176 

60407  177 
val ps = specs_ctxt > fold_map Proof_Context.inferred_param xs > fst; 
178 
val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps; 

61947  179 
val name_atts: Attrib.binding list = 
63179  180 
map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (map #1 raw_specss); 
63180  181 
in ((params, name_atts ~~ specs), specs_ctxt) end; 
24724
0df74bb87a13
read/check_specification: proper type inference across multiple sections, result is in closed form;
wenzelm
parents:
24676
diff
changeset

182 

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

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

184 

63180  185 
val check_spec_open = prep_spec_open Proof_Context.cert_var (K I); 
186 
val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop; 

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

187 

63182  188 
type multi_specs = 
189 
((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list; 

190 
type multi_specs_cmd = 

191 
((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list; 

61947  192 

63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63063
diff
changeset

193 
fun check_multi_specs xs specs = 
63180  194 
prep_specs Proof_Context.cert_var (K I) (K I) xs specs; 
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63063
diff
changeset

195 

2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63063
diff
changeset

196 
fun read_multi_specs xs specs = 
63180  197 
prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs 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

198 

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

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

200 

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

201 

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

203 

63178  204 
fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy = 
18620
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

205 
let 
63178  206 
(*specification*) 
70734  207 
val ({vars, propss = [prems, concls], ...}, vars_ctxt) = 
63178  208 
Proof_Context.init_global thy 
209 
> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]); 

210 
val (decls, fixes) = chop (length raw_decls) vars; 

211 

212 
val frees = 

213 
rev ((fold o fold) (Variable.add_frees vars_ctxt) [prems, concls] []) 

214 
> map (fn (x, T) => (x, Free (x, T))); 

215 
val close = Logic.close_prop (map #2 fixes @ frees) prems; 

216 
val specs = 

217 
map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls; 

28114  218 

71213  219 
val spec_name = 
71214
5727bcc3c47c
proper spec_rule name via naming/binding/Morphism.binding;
wenzelm
parents:
71213
diff
changeset

220 
Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls); 
71213  221 

222 

28114  223 
(*consts*) 
63178  224 
val (consts, consts_thy) = thy 
225 
> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls; 

226 
val subst = Term.subst_atomic (map (#2 o #2) decls ~~ consts); 

28114  227 

228 
(*axioms*) 

63178  229 
val (axioms, axioms_thy) = 
230 
(specs, consts_thy) > fold_map (fn ((b, atts), prop) => 

231 
Thm.add_axiom_global (b, subst prop) #>> (fn (_, th) => ((b, atts), [([th], [])]))); 

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

232 

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

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

234 
val (facts, facts_lthy) = axioms_thy 
38388  235 
> Named_Target.theory_init 
71213  236 
> Spec_Rules.add spec_name Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms) 
33703
50b6c07c0dd4
axiomatization: declare Spec_Rules, direct result;
wenzelm
parents:
33671
diff
changeset

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

238 

63178  239 
in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end; 
18786  240 

63178  241 
val axiomatization = gen_axioms Proof_Context.cert_stmt (K I); 
242 
val axiomatization_cmd = gen_axioms Proof_Context.read_stmt Attrib.check_src; 

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

243 

63178  244 
fun axiom (b, ax) = axiomatization [] [] [] [(b, ax)] #>> (hd o snd); 
35894  245 

18786  246 

247 
(* definition *) 

248 

63180  249 
fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy = 
18786  250 
let 
63180  251 
val atts = map (prep_att lthy) raw_atts; 
252 

63394  253 
val ((vars, xs, get_pos, spec), _) = lthy 
63180  254 
> prep_spec (the_list raw_var) raw_params raw_prems raw_spec; 
63395  255 
val (((x, T), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = true} spec; 
56169
9b0dc5c704c9
reject internal names, notably from Term.free_dummy_patterns;
wenzelm
parents:
56026
diff
changeset

256 
val _ = Name.reject_internal (x, []); 
62770  257 
val (b, mx) = 
63180  258 
(case (vars, xs) of 
63395  259 
([], []) => (Binding.make (x, (case get_pos x of [] => Position.none  p :: _ => p)), NoSyn) 
63180  260 
 ([(b, _, mx)], [y]) => 
261 
if x = y then (b, mx) 

262 
else 

263 
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ 

264 
Position.here (Binding.pos_of b))); 

71179  265 
val const_name = Local_Theory.full_name lthy b; 
266 

63180  267 
val name = Thm.def_binding_optional b a; 
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

268 
val ((lhs, (_, raw_th)), lthy2) = lthy 
62770  269 
> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs)); 
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

270 

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

271 
val th = prove lthy2 raw_th; 
71217  272 
val lthy3 = lthy2 > Spec_Rules.add name Spec_Rules.equational [lhs] [th]; 
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset

273 

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

274 
val ([(def_name, [th'])], lthy4) = lthy3 
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

275 
> Local_Theory.notes [((name, atts), [([th], [])])]; 
18786  276 

66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

277 
val lthy5 = lthy4 
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

278 
> Code.declare_default_eqns [(th', true)]; 
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

279 

cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

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

281 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

282 
val _ = 
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

283 
Proof_Display.print_consts int (Position.thread_data ()) lthy5 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

284 
(member (op =) (Term.add_frees lhs' [])) [(x, T)]; 
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66248
diff
changeset

285 
in ((lhs, (def_name, th')), lthy5) end; 
18786  286 

63180  287 
val definition' = gen_def check_spec_open (K I); 
288 
fun definition xs ys As B = definition' xs ys As B false; 

289 
val definition_cmd = gen_def read_spec_open Attrib.check_src; 

18786  290 

19080  291 

292 
(* abbreviation *) 

293 

63180  294 
fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy = 
19080  295 
let 
63180  296 
val lthy1 = lthy > Proof_Context.set_syntax_mode mode; 
63394  297 
val ((vars, xs, get_pos, spec), _) = lthy 
63180  298 
> Proof_Context.set_mode Proof_Context.mode_abbrev 
299 
> prep_spec (the_list raw_var) raw_params [] raw_spec; 

63395  300 
val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 get_pos spec)); 
56169
9b0dc5c704c9
reject internal names, notably from Term.free_dummy_patterns;
wenzelm
parents:
56026
diff
changeset

301 
val _ = Name.reject_internal (x, []); 
62770  302 
val (b, mx) = 
63180  303 
(case (vars, xs) of 
63395  304 
([], []) => (Binding.make (x, (case get_pos x of [] => Position.none  p :: _ => p)), NoSyn) 
63180  305 
 ([(b, _, mx)], [y]) => 
306 
if x = y then (b, mx) 

307 
else 

308 
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ 

309 
Position.here (Binding.pos_of b))); 

55119
9ca72949ebac
observe local syntax mode (according to e3a39dae2004, which was lost in 0f3ad56548bc), e.g. relevant for "abbreviation (output)" with nonterminating syntax;
wenzelm
parents:
54883
diff
changeset

310 
val lthy2 = lthy1 
62770  311 
> Local_Theory.abbrev mode ((b, mx), rhs) > snd 
42360  312 
> 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

313 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

314 
val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)]; 
55119
9ca72949ebac
observe local syntax mode (according to e3a39dae2004, which was lost in 0f3ad56548bc), e.g. relevant for "abbreviation (output)" with nonterminating syntax;
wenzelm
parents:
54883
diff
changeset

315 
in lthy2 end; 
19080  316 

63180  317 
val abbreviation = gen_abbrev check_spec_open; 
318 
val abbreviation_cmd = gen_abbrev read_spec_open; 

19080  319 

19664  320 

66248  321 
(* alias *) 
322 

323 
fun gen_alias decl check (b, arg) lthy = 

324 
let 

325 
val (c, reports) = check {proper = true, strict = false} lthy arg; 

326 
val _ = Position.reports reports; 

327 
in decl b c lthy end; 

328 

329 
val alias = 

330 
gen_alias Local_Theory.const_alias (K (K (fn c => (c, [])))); 

331 
val alias_cmd = 

332 
gen_alias Local_Theory.const_alias 

333 
(fn flags => fn ctxt => fn (c, pos) => 

334 
apfst (#1 o dest_Const) (Proof_Context.check_const flags ctxt (c, [pos]))); 

335 

336 
val type_alias = 

337 
gen_alias Local_Theory.type_alias (K (K (fn c => (c, [])))); 

338 
val type_alias_cmd = 

339 
gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name); 

340 

341 

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

342 
(* notation *) 
19664  343 

35413  344 
local 
345 

346 
fun gen_type_notation prep_type add mode args lthy = 

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

348 

24949  349 
fun gen_notation prep_const add mode args lthy = 
33671  350 
lthy > Local_Theory.notation add mode (map (apfst (prep_const lthy)) args); 
19664  351 

35413  352 
in 
353 

354 
val type_notation = gen_type_notation (K I); 

55951
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55639
diff
changeset

355 
val type_notation_cmd = 
56002  356 
gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false}); 
35413  357 

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

358 
val notation = gen_notation (K I); 
56002  359 
val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false}); 
19664  360 

35413  361 
end; 
362 

20914  363 

21036  364 
(* fact statements *) 
20914  365 

45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

366 
local 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

367 

60469  368 
fun gen_theorems prep_fact prep_att add_fixes 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

369 
kind raw_facts raw_fixes int lthy = 
20914  370 
let 
371 
val facts = raw_facts > map (fn ((name, atts), bs) => 

55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55955
diff
changeset

372 
((name, map (prep_att lthy) atts), 
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55955
diff
changeset

373 
bs > map (fn (b, more_atts) => (prep_fact lthy b, map (prep_att lthy) more_atts)))); 
60469  374 
val (_, ctxt') = add_fixes raw_fixes lthy; 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

375 

1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

376 
val facts' = facts 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

377 
> Attrib.partial_evaluation ctxt' 
58028
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

378 
> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy); 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

379 
val (res, lthy') = lthy > Local_Theory.notes_kind kind facts'; 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

380 
val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res); 
20914  381 
in (res, lthy') end; 
382 

45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

383 
in 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

384 

60469  385 
val theorems = gen_theorems (K I) (K I) Proof_Context.add_fixes; 
386 
val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; 

45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

387 

1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

388 
end; 
20914  389 

21036  390 

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

391 
(* complex goal statements *) 
21036  392 

393 
local 

394 

60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

395 
fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

396 
let 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

397 
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt; 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

398 
val prems = Assumption.local_prems_of elems_ctxt ctxt; 
70308  399 
val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt; 
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

400 
in 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

401 
(case raw_stmt of 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

402 
Element.Shows _ => 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

403 
let val stmt' = Attrib.map_specs (map prep_att) stmt 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

404 
in (([], prems, stmt', NONE), stmt_ctxt) end 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

405 
 Element.Obtains raw_obtains => 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

406 
let 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

407 
val asms_ctxt = stmt_ctxt 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

408 
> fold (fn ((name, _), asm) => 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

409 
snd o Proof_Context.add_assms Assumption.assume_export 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

410 
[((name, [Context_Rules.intro_query NONE]), asm)]) stmt; 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

411 
val that = Assumption.local_prems_of asms_ctxt stmt_ctxt; 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

412 
val ([(_, that')], that_ctxt) = asms_ctxt 
63096
7910b1db2596
reenable fact index for 'obtains' assumption (amending 5c8e6a751adc);
wenzelm
parents:
63094
diff
changeset

413 
> Proof_Context.set_stmt true 
7910b1db2596
reenable fact index for 'obtains' assumption (amending 5c8e6a751adc);
wenzelm
parents:
63094
diff
changeset

414 
> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])] 
7910b1db2596
reenable fact index for 'obtains' assumption (amending 5c8e6a751adc);
wenzelm
parents:
63094
diff
changeset

415 
> Proof_Context.restore_stmt asms_ctxt; 
21036  416 

63352  417 
val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])]; 
63019  418 
in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end) 
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60469
diff
changeset

419 
end; 
21036  420 

56026
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

421 
fun gen_theorem schematic bundle_includes prep_att prep_stmt 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

422 
long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = 
21036  423 
let 
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47021
diff
changeset

424 
val _ = Local_Theory.assert lthy; 
21036  425 

55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55955
diff
changeset

426 
val elems = raw_elems > map (Element.map_ctxt_attrib (prep_att lthy)); 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

427 
val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy 
56026
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

428 
> bundle_includes raw_includes 
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55955
diff
changeset

429 
> prep_statement (prep_att lthy) prep_stmt elems raw_concl; 
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55955
diff
changeset

430 
val atts = more_atts @ map (prep_att lthy) raw_atts; 
21036  431 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

432 
val pos = Position.thread_data (); 
21036  433 
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

434 
let 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
51313
diff
changeset

435 
val results' = 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
51313
diff
changeset

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

437 
val (res, lthy') = 
63352  438 
if forall (Binding.is_empty_atts o fst) stmt then (map (pair "") results', lthy) 
45584
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45583
diff
changeset

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

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

441 
(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

442 
val lthy'' = 
63352  443 
if Binding.is_empty_atts (name, atts) then 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

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

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

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

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

448 
Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

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

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

451 
in after_qed results' lthy'' end; 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

452 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

453 
val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN; 
21036  454 
in 
455 
goal_ctxt 

63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

456 
> not (null prems) ? 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63069
diff
changeset

457 
(Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd) 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36317
diff
changeset

458 
> 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

459 
> (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

460 
> 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

461 
error "Illegal schematic goal statement") 
21036  462 
end; 
463 

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

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

465 

56026
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

466 
val theorem = 
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

467 
gen_theorem false Bundle.includes (K I) Expression.cert_statement; 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

468 
val theorem_cmd = 
56026
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

469 
gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement; 
36317
506d732cb522
explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents:
36106
diff
changeset

470 

56026
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

471 
val schematic_theorem = 
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

472 
gen_theorem true Bundle.includes (K I) Expression.cert_statement; 
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset

473 
val schematic_theorem_cmd = 
56026
893fe12639bc
tuned signature  prefer Name_Space.get with its builtin error;
wenzelm
parents:
56002
diff
changeset

474 
gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement; 
21036  475 

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

476 
end; 
21036  477 

478 
end; 