author  wenzelm 
Sun, 20 Nov 2011 17:44:41 +0100  
changeset 45600  1bbbac9a0cb0 
parent 45584  41a768a431a6 
child 45601  d5178f19b671 
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 > 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

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

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

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

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

59 
(binding * string 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 
24986  61 
val theorem: string > Method.text option > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28080
diff
changeset

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

64 
bool > local_theory > Proof.state 
24986  65 
val theorem_cmd: 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 > 
28710  67 
Element.context list > Element.statement > 
24452
93b113c5ac33
 theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset

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

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

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

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

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

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

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

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

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

77 
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

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

79 

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

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

81 
struct 
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 
(* prepare specification *) 
fc8b5f275359
Theory specifications  with typeinference, but no internal polymorphism.
wenzelm
parents:
diff
changeset

84 

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

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

86 

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

87 
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

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

89 
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

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

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

92 
 dups => error ("Duplicate local variables " ^ commas_quote dups)); 
42482  93 
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

94 
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

95 
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

96 

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

97 
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

98 
 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

99 
 abs_body lev y (t as Free (x, T)) = 
39288  100 
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

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

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

103 
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

104 
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

105 
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

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

107 
let 
42482  108 
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

109 
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

110 
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

111 
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

112 

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

113 
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

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

116 

18670  117 
val (vars, vars_ctxt) = ctxt > prep_vars raw_vars; 
42360  118 
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

119 

42265  120 
val Asss = 
121 
(map o map) snd raw_specss 

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

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

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

126 
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

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

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

131 
else Asss') 

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

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

133 
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

134 

42360  135 
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

136 
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

137 
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

138 
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

139 

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

140 

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

142 
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

143 

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

145 
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

146 
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

147 

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

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

149 

42360  150 
fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x; 
151 
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

152 

42360  153 
fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x; 
154 
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

155 

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 
fun check_specification vars specs = 
42360  157 
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

158 

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

159 
fun read_specification vars specs = 
42360  160 
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

161 

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

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

163 

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

164 

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

166 

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

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

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

172 
(*consts*) 

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

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

176 
(*axioms*) 

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

177 
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

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

179 
(map (apfst (fn a => Binding.map_name (K a) b)) 
42494  180 
(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

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

182 

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

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

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

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

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

188 

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

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

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

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

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

193 

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

196 

18786  197 

198 
(* definition *) 

199 

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

200 
fun gen_def prep (raw_var, raw_spec) int lthy = 
18786  201 
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

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

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

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

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

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

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

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

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

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

217 

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

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

219 
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

220 

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

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

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

223 
[((name, Code.add_default_eqn_attrib :: atts), [([th], [])])]; 
18786  224 

33671  225 
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

226 

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

227 
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

228 
in ((lhs, (def_name, th')), lthy4) end; 
18786  229 

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

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

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

232 
val definition_cmd = gen_def read_free_spec; 
18786  233 

19080  234 

235 
(* abbreviation *) 

236 

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

237 
fun gen_abbrev prep mode (raw_var, raw_prop) int lthy = 
19080  238 
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

239 
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

240 
prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)] 
42360  241 
(lthy > Proof_Context.set_mode Proof_Context.mode_abbrev); 
35624  242 
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

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

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

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

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

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

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

252 
in (b, mx) end); 
21705  253 
val lthy' = lthy 
42360  254 
> Proof_Context.set_syntax_mode mode (* FIXME ?!? *) 
33671  255 
> Local_Theory.abbrev mode (var, rhs) > snd 
42360  256 
> 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

257 

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

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

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

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

262 
val abbreviation_cmd = gen_abbrev read_free_spec; 
19080  263 

19664  264 

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

265 
(* notation *) 
19664  266 

35413  267 
local 
268 

269 
fun gen_type_notation prep_type add mode args lthy = 

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

271 

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

35413  275 
in 
276 

277 
val type_notation = gen_type_notation (K I); 

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

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

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

35413  283 
end; 
284 

20914  285 

21036  286 
(* fact statements *) 
20914  287 

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

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

289 

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

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

291 
kind raw_facts raw_fixes int lthy = 
20914  292 
let 
42360  293 
val attrib = prep_att (Proof_Context.theory_of lthy); 
20914  294 
val facts = raw_facts > map (fn ((name, atts), bs) => 
295 
((name, map attrib atts), 

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

296 
bs > map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts)))); 
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

297 
val (_, ctxt') = lthy > prep_vars raw_fixes > Proof_Context.add_fixes; 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

298 

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

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

300 
> Attrib.partial_evaluation ctxt' 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

301 
> Element.facts_map (Element.transform_ctxt (Proof_Context.export_morphism ctxt' lthy)); 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

302 
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

303 
val _ = Proof_Display.print_results int lthy' ((kind, ""), res); 
20914  304 
in (res, lthy') end; 
305 

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

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

307 

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

308 
val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars; 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

309 
val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src Proof_Context.read_vars; 
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45584
diff
changeset

310 

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

311 
end; 
20914  312 

21036  313 

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

314 
(* complex goal statements *) 
21036  315 

316 
local 

317 

21236  318 
fun prep_statement prep_att prep_stmt elems concl ctxt = 
319 
(case concl of 

320 
Element.Shows shows => 

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

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

324 
val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp); 
45327  325 
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

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

328 
let 
28862  329 
val case_names = obtains > map_index (fn (i, (b, _)) => 
42494  330 
if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b); 
21236  331 
val constraints = obtains > map (fn (_, (vars, _)) => 
28710  332 
Element.Constrains 
42494  333 
(vars > map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T)  _ => NONE))); 
21036  334 

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

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

21236  340 
fun assume_case ((name, (vars, _)), asms) ctxt' = 
341 
let 

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

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

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

348 
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

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

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

352 
> Variable.auto_fixes asm 
42360  353 
> Proof_Context.add_assms_i Assumption.assume_export 
33369  354 
[((name, [Context_Rules.intro_query NONE]), [(asm, [])])] 
21236  355 
>> (fn [(_, [th])] => th) 
356 
end; 

357 

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

358 
val more_atts = map (Attrib.internal o K) 
33368  359 
[Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names]; 
30472  360 
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

361 
val stmt = [((Binding.empty, []), [(thesis, [])])]; 
21236  362 

363 
val (facts, goal_ctxt) = elems_ctxt 

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

366 
> (fn ths => 
42360  367 
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

368 
#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

369 
in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end); 
21036  370 

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

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

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

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

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

375 
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

376 
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

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

378 

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

379 
fun gen_theorem schematic prep_att prep_stmt 
28858  380 
kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy = 
21036  381 
let 
33671  382 
val _ = Local_Theory.affirm lthy; 
42360  383 
val thy = Proof_Context.theory_of lthy; 
21036  384 

21435  385 
val attrib = prep_att thy; 
28710  386 
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

387 
val ((more_atts, prems, stmt, facts), goal_ctxt) = 
28880  388 
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

389 
val atts = more_atts @ map attrib raw_atts; 
21036  390 

391 
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

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

393 
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

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

395 
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

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

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

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

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

400 
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

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

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

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

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

405 
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

406 
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

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

408 
in after_qed results' lthy'' end; 
21036  409 
in 
410 
goal_ctxt 

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

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

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

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

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

417 
> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt)))) 
21036  418 
end; 
419 

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

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

421 

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

422 
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

423 
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

424 
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

425 

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

426 
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

427 
val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement; 
21036  428 

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

429 
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

430 

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

431 
end; 
21036  432 

433 
end; 