author  wenzelm 
Tue, 08 Feb 2000 20:14:09 +0100  
changeset 8210  ca3997312f47 
parent 8204  b2a4a3d86b73 
child 8213  a541e261c660 
permissions  rwrr 
5830  1 
(* Title: Pure/Isar/isar_thy.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

6371  5 
Pure/Isar derived theory operations. 
5830  6 
*) 
7 

8 
signature ISAR_THY = 

9 
sig 

7734  10 
val add_header: Comment.text > Toplevel.transition > Toplevel.transition 
6552  11 
val add_chapter: Comment.text > theory > theory 
12 
val add_section: Comment.text > theory > theory 

13 
val add_subsection: Comment.text > theory > theory 

14 
val add_subsubsection: Comment.text > theory > theory 

7172  15 
val add_text: Comment.text > theory > theory 
7862  16 
val add_text_raw: Comment.text > theory > theory 
7172  17 
val add_sect: Comment.text > ProofHistory.T > ProofHistory.T 
18 
val add_subsect: Comment.text > ProofHistory.T > ProofHistory.T 

19 
val add_subsubsect: Comment.text > ProofHistory.T > ProofHistory.T 

20 
val add_txt: Comment.text > ProofHistory.T > ProofHistory.T 

7862  21 
val add_txt_raw: Comment.text > ProofHistory.T > ProofHistory.T 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

22 
val add_classes: (bclass * xclass list) list * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

23 
val add_classes_i: (bclass * class list) list * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

24 
val add_classrel: (xclass * xclass) * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

25 
val add_classrel_i: (class * class) * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

26 
val add_defsort: xsort * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

27 
val add_defsort_i: sort * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

28 
val add_nonterminals: (bstring * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

29 
val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

30 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

31 
val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

32 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

33 
val add_arities: ((xstring * xsort list * xsort) * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

34 
val add_arities_i: ((string * sort list * sort) * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

35 
val add_typedecl: (bstring * string list * mixfix) * Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

36 
val add_consts: ((bstring * string * mixfix) * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

37 
val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

38 
val add_modesyntax: string * bool > ((bstring * string * mixfix) * Comment.text) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

39 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

40 
val add_modesyntax_i: string * bool > ((bstring * typ * mixfix) * Comment.text) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

41 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

42 
val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

43 
val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

44 
val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

45 
val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

46 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

47 
val add_defs: (((bstring * string) * Args.src list) * Comment.text) list > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

48 
val add_defs_i: (((bstring * term) * theory attribute list) * Comment.text) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

49 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

50 
val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

51 
> theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

52 
val add_constdefs_i: (((bstring * typ * mixfix) * Comment.text) * (term * Comment.text)) list 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

53 
> theory > theory 
6371  54 
val apply_theorems: (xstring * Args.src list) list > theory > theory * thm list 
55 
val apply_theorems_i: (thm * theory attribute list) list > theory > theory * thm list 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

56 
val have_theorems: ((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text 
6371  57 
> theory > theory 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

58 
val have_theorems_i: ((bstring * theory attribute list) * (thm * theory attribute list) list) 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

59 
* Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

60 
val have_lemmas: ((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text 
5915  61 
> theory > theory 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

62 
val have_lemmas_i: ((bstring * theory attribute list) * (thm * theory attribute list) list) 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

63 
* Comment.text > theory > theory 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

64 
val have_facts: ((string * Args.src list) * (string * Args.src list) list) * Comment.text 
5915  65 
> ProofHistory.T > ProofHistory.T 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

66 
val have_facts_i: ((string * Proof.context attribute list) * 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

67 
(thm * Proof.context attribute list) list) * Comment.text > ProofHistory.T > ProofHistory.T 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

68 
val from_facts: (string * Args.src list) list * Comment.text > ProofHistory.T > ProofHistory.T 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

69 
val from_facts_i: (thm * Proof.context attribute list) list * Comment.text 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

70 
> ProofHistory.T > ProofHistory.T 
6879  71 
val with_facts: (string * Args.src list) list * Comment.text > ProofHistory.T > ProofHistory.T 
72 
val with_facts_i: (thm * Proof.context attribute list) list * Comment.text 

73 
> ProofHistory.T > ProofHistory.T 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

74 
val chain: Comment.text > ProofHistory.T > ProofHistory.T 
6937  75 
val export_chain: Comment.text > ProofHistory.T > ProofHistory.T 
7417  76 
val fix: ((string list * string option) * Comment.text) list > ProofHistory.T > ProofHistory.T 
7666  77 
val fix_i: ((string list * typ option) * Comment.text) list > ProofHistory.T > ProofHistory.T 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

78 
val match_bind: ((string list * string) * Comment.text) list > ProofHistory.T > ProofHistory.T 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

79 
val match_bind_i: ((term list * term) * Comment.text) list > ProofHistory.T > ProofHistory.T 
6937  80 
val theorem: (bstring * Args.src list * (string * (string list * string list))) 
81 
* Comment.text > bool > theory > ProofHistory.T 

82 
val theorem_i: (bstring * theory attribute list * (term * (term list * term list))) 

83 
* Comment.text > bool > theory > ProofHistory.T 

84 
val lemma: (bstring * Args.src list * (string * (string list * string list))) 

85 
* Comment.text > bool > theory > ProofHistory.T 

86 
val lemma_i: (bstring * theory attribute list * (term * (term list * term list))) 

87 
* Comment.text > bool > theory > ProofHistory.T 

7271  88 
val assume: ((string * Args.src list * (string * (string list * string list)) list) 
89 
* Comment.text) list > ProofHistory.T > ProofHistory.T 

90 
val assume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list) 

91 
* Comment.text) list > ProofHistory.T > ProofHistory.T 

92 
val presume: ((string * Args.src list * (string * (string list * string list)) list) 

93 
* Comment.text) list > ProofHistory.T > ProofHistory.T 

94 
val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list) 

95 
* Comment.text) list > ProofHistory.T > ProofHistory.T 

6952  96 
val local_def: (string * Args.src list * ((string * string option) * (string * string list))) 
97 
* Comment.text > ProofHistory.T > ProofHistory.T 

7666  98 
val local_def_i: (string * Args.src list * ((string * typ option) * (term * term list))) 
6952  99 
* Comment.text > ProofHistory.T > ProofHistory.T 
6937  100 
val show: (string * Args.src list * (string * (string list * string list))) 
101 
* Comment.text > ProofHistory.T > ProofHistory.T 

102 
val show_i: (string * Proof.context attribute list * (term * (term list * term list))) 

103 
* Comment.text > ProofHistory.T > ProofHistory.T 

104 
val have: (string * Args.src list * (string * (string list * string list))) 

105 
* Comment.text > ProofHistory.T > ProofHistory.T 

106 
val have_i: (string * Proof.context attribute list * (term * (term list * term list))) 

107 
* Comment.text > ProofHistory.T > ProofHistory.T 

108 
val thus: (string * Args.src list * (string * (string list * string list))) 

109 
* Comment.text > ProofHistory.T > ProofHistory.T 

110 
val thus_i: (string * Proof.context attribute list * (term * (term list * term list))) 

111 
* Comment.text > ProofHistory.T > ProofHistory.T 

112 
val hence: (string * Args.src list * (string * (string list * string list))) 

113 
* Comment.text > ProofHistory.T > ProofHistory.T 

114 
val hence_i: (string * Proof.context attribute list * (term * (term list * term list))) 

115 
* Comment.text > ProofHistory.T > ProofHistory.T 

5830  116 
val begin_block: ProofHistory.T > ProofHistory.T 
117 
val next_block: ProofHistory.T > ProofHistory.T 

118 
val end_block: ProofHistory.T > ProofHistory.T 

8165  119 
val defer: int option > ProofHistory.T > ProofHistory.T 
120 
val prefer: int > ProofHistory.T > ProofHistory.T 

5830  121 
val tac: Method.text > ProofHistory.T > ProofHistory.T 
5882  122 
val then_tac: Method.text > ProofHistory.T > ProofHistory.T 
7002  123 
val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

124 
> ProofHistory.T > ProofHistory.T 
7002  125 
val qed: (Method.text * Comment.interest) option * Comment.text 
6937  126 
> Toplevel.transition > Toplevel.transition 
7002  127 
val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option) 
128 
* Comment.text > Toplevel.transition > Toplevel.transition 

129 
val immediate_proof: Comment.text > Toplevel.transition > Toplevel.transition 

130 
val default_proof: Comment.text > Toplevel.transition > Toplevel.transition 

131 
val skip_proof: Comment.text > Toplevel.transition > Toplevel.transition 

8210  132 
val forget_proof: Comment.text > Toplevel.transition > Toplevel.transition 
7012  133 
val get_thmss: (string * Args.src list) list > Proof.state > thm list 
6879  134 
val also: ((string * Args.src list) list * Comment.interest) option * Comment.text 
135 
> Toplevel.transition > Toplevel.transition 

136 
val also_i: (thm list * Comment.interest) option * Comment.text 

137 
> Toplevel.transition > Toplevel.transition 

138 
val finally: ((string * Args.src list) list * Comment.interest) option * Comment.text 

139 
> Toplevel.transition > Toplevel.transition 

140 
val finally_i: (thm list * Comment.interest) option * Comment.text 

141 
> Toplevel.transition > Toplevel.transition 

7614  142 
val use_mltext: string > bool > theory option > unit 
143 
val use_mltext_theory: string > bool > theory > theory 

5830  144 
val use_setup: string > theory > theory 
145 
val parse_ast_translation: string > theory > theory 

146 
val parse_translation: string > theory > theory 

147 
val print_translation: string > theory > theory 

148 
val typed_print_translation: string > theory > theory 

149 
val print_ast_translation: string > theory > theory 

150 
val token_translation: string > theory > theory 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

151 
val add_oracle: (bstring * string) * Comment.text > theory > theory 
6331  152 
val begin_theory: string > string list > (string * bool) list > theory 
153 
val end_theory: theory > theory 

7932  154 
val kill_theory: string > unit 
6246  155 
val theory: string * string list * (string * bool) list 
156 
> Toplevel.transition > Toplevel.transition 

7960  157 
val init_context: ('a > unit) > 'a > Toplevel.transition > Toplevel.transition 
6246  158 
val context: string > Toplevel.transition > Toplevel.transition 
5830  159 
end; 
160 

161 
structure IsarThy: ISAR_THY = 

162 
struct 

163 

164 

165 
(** derived theory and proof operations **) 

166 

8090  167 
(* markup commands *) 
5959  168 

7734  169 
fun add_header comment = 
170 
Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF); 

171 

8090  172 
fun add_text _ x = x; 
8079  173 
fun add_text_raw _ x = x; 
7633  174 

8090  175 
fun add_heading add present txt thy = 
7633  176 
(Context.setmp (Some thy) present (Comment.string_of txt); add txt thy); 
177 

8090  178 
val add_chapter = add_heading add_text Present.section; 
179 
val add_section = add_heading add_text Present.section; 

180 
val add_subsection = add_heading add_text Present.subsection; 

181 
val add_subsubsection = add_heading add_text Present.subsubsection; 

5959  182 

8090  183 
fun add_txt (_: Comment.text) = ProofHistory.apply I; 
184 
val add_txt_raw = add_txt; 

7332  185 
val add_sect = add_txt; 
186 
val add_subsect = add_txt; 

187 
val add_subsubsect = add_txt; 

7172  188 

5959  189 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

190 
(* signature and syntax *) 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

191 

b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

192 
val add_classes = Theory.add_classes o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

193 
val add_classes_i = Theory.add_classes_i o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

194 
val add_classrel = Theory.add_classrel o single o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

195 
val add_classrel_i = Theory.add_classrel_i o single o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

196 
val add_defsort = Theory.add_defsort o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

197 
val add_defsort_i = Theory.add_defsort_i o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

198 
val add_nonterminals = Theory.add_nonterminals o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

199 
val add_tyabbrs = Theory.add_tyabbrs o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

200 
val add_tyabbrs_i = Theory.add_tyabbrs_i o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

201 
val add_arities = Theory.add_arities o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

202 
val add_arities_i = Theory.add_arities_i o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

203 
val add_typedecl = PureThy.add_typedecls o single o Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

204 
val add_consts = Theory.add_consts o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

205 
val add_consts_i = Theory.add_consts_i o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

206 
fun add_modesyntax mode = Theory.add_modesyntax mode o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

207 
fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

208 
val add_trrules = Theory.add_trrules o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

209 
val add_trrules_i = Theory.add_trrules_i o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

210 

b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

211 

b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

212 

5830  213 
(* axioms and defs *) 
214 

5915  215 
fun add_axms f args thy = 
216 
f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; 

217 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

218 
val add_axioms = add_axms PureThy.add_axioms o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

219 
val add_axioms_i = PureThy.add_axioms_i o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

220 
val add_defs = add_axms PureThy.add_defs o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

221 
val add_defs_i = PureThy.add_defs_i o map Comment.ignore; 
6371  222 

223 

224 
(* constdefs *) 

225 

226 
fun gen_add_constdefs consts defs args thy = 

227 
thy 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

228 
> consts (map (Comment.ignore o fst) args) 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

229 
> defs (map (fn (((c, _, mx), _), (s, _)) => 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

230 
(((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args); 
6371  231 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

232 
fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

233 
fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args; 
5915  234 

235 

236 
(* theorems *) 

237 

238 
fun gen_have_thmss get attrib f ((name, more_srcs), th_srcs) x = 

239 
f name (map (attrib x) more_srcs) 

240 
(map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x; 

241 

7572  242 
fun global_have_thmss kind f (x as ((name, _), _)) thy = 
243 
let val (thy', thms) = gen_have_thmss PureThy.get_thms Attrib.global_attribute f x thy in 

244 
if kind <> "" then Context.setmp (Some thy') (Present.results kind name) thms else (); 

245 
(thy', thms) 

246 
end; 

5915  247 

6371  248 
fun local_have_thmss x = 
249 
gen_have_thmss (ProofContext.get_thms o Proof.context_of) 

250 
(Attrib.local_attribute o Proof.theory_of) x; 

251 

7012  252 
fun gen_have_thmss_i f ((name, more_atts), th_atts) = 
6371  253 
f name more_atts (map (apfst single) th_atts); 
254 

255 
fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]); 

5915  256 

257 

7572  258 
fun apply_theorems th_srcs = global_have_thmss "" PureThy.have_thmss (("", []), th_srcs); 
7476  259 
fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss (("", []), th_srcs); 
7572  260 
val have_theorems = #1 oo (global_have_thmss "theorems" PureThy.have_thmss o Comment.ignore); 
7476  261 
val have_theorems_i = #1 oo (gen_have_thmss_i PureThy.have_thmss o Comment.ignore); 
7572  262 
val have_lemmas = #1 oo (global_have_thmss "lemmas" have_lemss o Comment.ignore); 
7476  263 
val have_lemmas_i = #1 oo (gen_have_thmss_i have_lemss o Comment.ignore); 
6879  264 
val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore; 
7012  265 
val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore; 
6371  266 

5915  267 

6371  268 
(* forward chaining *) 
269 

6879  270 
fun gen_from_facts f = ProofHistory.apply o (Proof.chain oo curry f ("", [])); 
271 

272 
fun add_thmss name atts ths_atts state = 

273 
Proof.have_thmss (Proof.the_facts state) name atts ths_atts state; 

6371  274 

6879  275 
val from_facts = gen_from_facts (local_have_thmss (Proof.have_thmss [])) o Comment.ignore; 
7012  276 
val from_facts_i = gen_from_facts (gen_have_thmss_i (Proof.have_thmss [])) o Comment.ignore; 
6879  277 
val with_facts = gen_from_facts (local_have_thmss add_thmss) o Comment.ignore; 
7012  278 
val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore; 
6879  279 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

280 
fun chain comment_ignore = ProofHistory.apply Proof.chain; 
6937  281 
fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain; 
5830  282 

283 

284 
(* context *) 

285 

7417  286 
val fix = ProofHistory.apply o Proof.fix o map Comment.ignore; 
287 
val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore; 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

288 
val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore; 
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

289 
val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore; 
5830  290 

291 

292 
(* statements *) 

293 

7271  294 
local 
295 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

296 
fun global_statement f (name, src, s) int thy = 
6688  297 
ProofHistory.init (Toplevel.undo_limit int) 
298 
(f name (map (Attrib.global_attribute thy) src) s thy); 

5830  299 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

300 
fun global_statement_i f (name, atts, t) int thy = 
6688  301 
ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy); 
6501  302 

6904
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

303 
fun local_statement f g (name, src, s) = ProofHistory.apply (fn state => 
6501  304 
f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state)); 
6371  305 

6904
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

306 
fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g); 
5830  307 

8090  308 
fun multi_local_attribute state (name, src, s) = 
309 
(name, map (Attrib.local_attribute (Proof.theory_of state)) src, s); 

310 

7271  311 
fun multi_statement f args = ProofHistory.apply (fn state => 
7678  312 
f (map (multi_local_attribute state) args) state); 
7271  313 

314 
fun multi_statement_i f args = ProofHistory.apply (f args); 

315 

316 
in 

317 

6952  318 
val theorem = global_statement Proof.theorem o Comment.ignore; 
319 
val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore; 

320 
val lemma = global_statement Proof.lemma o Comment.ignore; 

321 
val lemma_i = global_statement_i Proof.lemma_i o Comment.ignore; 

7271  322 
val assume = multi_statement Proof.assume o map Comment.ignore; 
323 
val assume_i = multi_statement_i Proof.assume_i o map Comment.ignore; 

324 
val presume = multi_statement Proof.presume o map Comment.ignore; 

325 
val presume_i = multi_statement_i Proof.presume_i o map Comment.ignore; 

6952  326 
val local_def = local_statement LocalDefs.def I o Comment.ignore; 
327 
val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore; 

7176  328 
val show = local_statement (Proof.show Seq.single) I o Comment.ignore; 
329 
val show_i = local_statement_i (Proof.show_i Seq.single) I o Comment.ignore; 

330 
val have = local_statement (Proof.have Seq.single) I o Comment.ignore; 

331 
val have_i = local_statement_i (Proof.have_i Seq.single) I o Comment.ignore; 

332 
val thus = local_statement (Proof.show Seq.single) Proof.chain o Comment.ignore; 

333 
val thus_i = local_statement_i (Proof.show_i Seq.single) Proof.chain o Comment.ignore; 

334 
val hence = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore; 

335 
val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore; 

5830  336 

7271  337 
end; 
338 

5830  339 

340 
(* blocks *) 

341 

6904
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

342 
val begin_block = ProofHistory.apply Proof.begin_block; 
5830  343 
val next_block = ProofHistory.apply Proof.next_block; 
6937  344 
val end_block = ProofHistory.applys Proof.end_block; 
5830  345 

346 

8165  347 
(* shuffle state *) 
348 

8204  349 
fun shuffle meth i = Method.refine_no_facts (Method.Basic (K (meth i))) o Proof.assert_no_chain; 
350 

351 
fun defer i = ProofHistory.applys (shuffle Method.defer i); 

352 
fun prefer i = ProofHistory.applys (shuffle Method.prefer i); 

8165  353 

354 

5830  355 
(* backward steps *) 
356 

7506  357 
val tac = ProofHistory.applys o Method.refine_no_facts; 
358 
val then_tac = ProofHistory.applys o Method.refine; 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

359 

7002  360 
val proof = ProofHistory.applys o Method.proof o 
361 
apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore; 

6404  362 

363 

6732  364 
(* print result *) 
365 

7572  366 
local 
367 

6732  368 
fun pretty_result {kind, name, thm} = 
7590  369 
Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"), 
7572  370 
Pretty.fbrk, Proof.pretty_thm thm]; 
6986  371 

372 
fun pretty_rule thm = 

7353  373 
Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm]; 
6732  374 

7572  375 
in 
376 

6732  377 
val print_result = Pretty.writeln o pretty_result; 
378 

6986  379 
fun cond_print_result_rule int = 
380 
if int then (print_result, Pretty.writeln o pretty_rule) 

381 
else (K (), K ()); 

382 

383 
fun proof'' f = Toplevel.proof' (f o cond_print_result_rule); 

6732  384 

7572  385 
end; 
386 

6732  387 

6404  388 
(* local endings *) 
389 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

390 
val local_qed = 
6904
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

391 
proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest; 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

392 

6937  393 
fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y); 
394 

6688  395 
val local_terminal_proof = 
6937  396 
proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests; 
6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

397 

6904
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

398 
val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof); 
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

399 
val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof); 
4125d6b6d8f9
removed proof history nesting commands (not useful);
wenzelm
parents:
6890
diff
changeset

400 
val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof); 
6404  401 

402 

403 
(* global endings *) 

404 

405 
fun global_result finish = Toplevel.proof_to_theory (fn prf => 

406 
let 

407 
val state = ProofHistory.current prf; 

408 
val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF; 

7572  409 
val (thy, res as {kind, name, thm}) = finish state; 
410 
in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end); 

6404  411 

6952  412 
val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest; 
6937  413 
val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests; 
6404  414 
val global_immediate_proof = global_result Method.global_immediate_proof; 
415 
val global_default_proof = global_result Method.global_default_proof; 

6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6885
diff
changeset

416 
val global_skip_proof = global_result SkipProof.global_skip_proof; 
6404  417 

418 

419 
(* common endings *) 

420 

7002  421 
fun qed (meth, comment) = local_qed meth o global_qed meth; 
422 
fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths; 

423 
fun immediate_proof comment = local_immediate_proof o global_immediate_proof; 

424 
fun default_proof comment = local_default_proof o global_default_proof; 

425 
fun skip_proof comment = local_skip_proof o global_skip_proof; 

5830  426 

8210  427 
fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current); 
428 

5830  429 

6774  430 
(* calculational proof commands *) 
431 

6879  432 
local 
433 

7417  434 
fun cond_print_calc int thms = 
435 
if int then Pretty.writeln (Pretty.big_list "calculation:" (map Proof.pretty_thm thms)) 

6774  436 
else (); 
437 

438 
fun proof''' f = Toplevel.proof' (f o cond_print_calc); 

439 

6879  440 
fun gen_calc get f (args, _) prt state = 
441 
f (apsome (fn (srcs, _) => get srcs state) args) prt state; 

442 

443 
in 

444 

7012  445 
fun get_thmss srcs = Proof.the_facts o local_have_thmss (Proof.have_thmss []) (("", []), srcs); 
446 
fun get_thmss_i thms _ = thms; 

447 

6879  448 
fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x); 
449 
fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x); 

450 
fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x); 

451 
fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x); 

452 

453 
end; 

6774  454 

455 

5830  456 
(* use ML text *) 
457 

7851  458 
fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt; 
459 
fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) txt); 

5830  460 

7614  461 
fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false; 
5830  462 

463 
fun use_let name body txt = 

464 
use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); 

465 

466 
val use_setup = 

5915  467 
use_let "setup: (theory > theory) list" "Library.apply setup"; 
5830  468 

469 

470 
(* translation functions *) 

471 

472 
val parse_ast_translation = 

473 
use_let "parse_ast_translation: (string * (Syntax.ast list > Syntax.ast)) list" 

474 
"Theory.add_trfuns (parse_ast_translation, [], [], [])"; 

475 

476 
val parse_translation = 

477 
use_let "parse_translation: (string * (term list > term)) list" 

478 
"Theory.add_trfuns ([], parse_translation, [], [])"; 

479 

480 
val print_translation = 

481 
use_let "print_translation: (string * (term list > term)) list" 

482 
"Theory.add_trfuns ([], [], print_translation, [])"; 

483 

484 
val print_ast_translation = 

485 
use_let "print_ast_translation: (string * (Syntax.ast list > Syntax.ast)) list" 

486 
"Theory.add_trfuns ([], [], [], print_ast_translation)"; 

487 

488 
val typed_print_translation = 

489 
use_let "typed_print_translation: (string * (bool > typ > term list > term)) list" 

490 
"Theory.add_trfunsT typed_print_translation"; 

491 

492 
val token_translation = 

493 
use_let "token_translation: (string * string * (string > string * int)) list" 

494 
"Theory.add_tokentrfuns token_translation"; 

495 

496 

497 
(* add_oracle *) 

498 

6728
b51b25db7bc6
added formal comment arguments almost everywhere (still ignored);
wenzelm
parents:
6688
diff
changeset

499 
fun add_oracle ((name, txt), comment_ignore) = 
5830  500 
use_let 
501 
"oracle: bstring * (Sign.sg * Object.T > term)" 

502 
"Theory.add_oracle oracle" 

503 
("(" ^ quote name ^ ", " ^ txt ^ ")"); 

504 

505 

6688  506 
(* theory init and exit *) 
5830  507 

7242  508 
fun gen_begin_theory bg name parents files = 
6266  509 
let 
6331  510 
val paths = map (apfst Path.unpack) files; 
7242  511 
val thy = bg name parents paths; 
6650
808a3d9e2404
Present.begin_theory now needs an additional argument of type
berghofe
parents:
6552
diff
changeset

512 
in Present.begin_theory name parents paths thy end; 
5830  513 

7242  514 
val begin_theory = gen_begin_theory ThyInfo.begin_theory; 
515 
val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory; 

7909  516 

517 
fun end_theory thy = 

7932  518 
if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy 
7909  519 
else thy; 
520 

7932  521 
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; 
6688  522 

7103  523 

524 
fun bg_theory (name, parents, files) int = 

7242  525 
(if int then begin_update_theory else begin_theory) name parents files; 
7103  526 

6331  527 
fun en_theory thy = (end_theory thy; ()); 
528 

7932  529 
fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name); 
6246  530 

531 

532 
(* context switch *) 

533 

7960  534 
fun fetch_context f x = 
535 
(case Context.pass None f x of 

536 
((), None) => raise Toplevel.UNDEF 

537 
 ((), Some thy) => thy); 

538 

539 
fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); 

7953  540 

541 
val context = init_context (ThyInfo.quiet_update_thy true); 

6246  542 

5830  543 

544 
end; 