author  wenzelm 
Wed, 27 Oct 1999 17:25:53 +0200  
changeset 7953  955fde69fa7b 
parent 7932  92df50fb89ca 
child 7960  d5c91c131070 
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 

119 
val tac: Method.text > ProofHistory.T > ProofHistory.T 

5882  120 
val then_tac: Method.text > ProofHistory.T > ProofHistory.T 
7002  121 
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

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

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

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

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

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

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

135 
> Toplevel.transition > Toplevel.transition 

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

137 
> Toplevel.transition > Toplevel.transition 

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

139 
> Toplevel.transition > Toplevel.transition 

7678  140 
val obtain: ((string list * string option) * Comment.text) list 
141 
* ((string * Args.src list * (string * (string list * string list)) list) 

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

143 
val obtain_i: ((string list * typ option) * Comment.text) list 

144 
* ((string * Proof.context attribute list * (term * (term list * term list)) list) 

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

7614  146 
val use_mltext: string > bool > theory option > unit 
147 
val use_mltext_theory: string > bool > theory > theory 

5830  148 
val use_setup: string > theory > theory 
149 
val parse_ast_translation: string > theory > theory 

150 
val parse_translation: string > theory > theory 

151 
val print_translation: string > theory > theory 

152 
val typed_print_translation: string > theory > theory 

153 
val print_ast_translation: string > theory > theory 

154 
val token_translation: string > theory > theory 

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

155 
val add_oracle: (bstring * string) * Comment.text > theory > theory 
6331  156 
val begin_theory: string > string list > (string * bool) list > theory 
157 
val end_theory: theory > theory 

7932  158 
val kill_theory: string > unit 
6246  159 
val theory: string * string list * (string * bool) list 
160 
> Toplevel.transition > Toplevel.transition 

7953  161 
val init_context: (string > unit) > string > Toplevel.transition > Toplevel.transition 
6246  162 
val context: string > Toplevel.transition > Toplevel.transition 
5830  163 
end; 
164 

165 
structure IsarThy: ISAR_THY = 

166 
struct 

167 

168 

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

170 

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

171 
(* formal comments *) 
5959  172 

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

175 

7332  176 
fun add_text comment thy = thy:theory; 
7862  177 
val add_text_raw = add_text; 
5959  178 
val add_chapter = add_text; 
7633  179 

180 
fun gen_add_section add present txt thy = 

181 
(Context.setmp (Some thy) present (Comment.string_of txt); add txt thy); 

182 

183 
val add_section = gen_add_section add_text Present.section; 

184 
val add_subsection = gen_add_section add_text Present.subsection; 

185 
val add_subsubsection = gen_add_section add_text Present.subsubsection; 

5959  186 

7172  187 
fun add_txt comment = ProofHistory.apply Proof.assert_forward; 
7862  188 
val add_txt_raw = add_txt; 
7332  189 
val add_sect = add_txt; 
190 
val add_subsect = add_txt; 

191 
val add_subsubsect = add_txt; 

7172  192 

5959  193 

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

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

195 

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

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

197 
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

198 
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

199 
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

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

201 
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

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

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

204 
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

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

206 
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

207 
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

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

209 
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

210 
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

211 
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

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

213 
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

214 

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

215 

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

216 

5830  217 
(* axioms and defs *) 
218 

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

221 

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

222 
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

223 
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

224 
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

225 
val add_defs_i = PureThy.add_defs_i o map Comment.ignore; 
6371  226 

227 

228 
(* constdefs *) 

229 

230 
fun gen_add_constdefs consts defs args thy = 

231 
thy 

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

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

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

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

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

236 
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

237 
fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args; 
5915  238 

239 

240 
(* theorems *) 

241 

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

243 
f name (map (attrib x) more_srcs) 

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

245 

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

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

249 
(thy', thms) 

250 
end; 

5915  251 

6371  252 
fun local_have_thmss x = 
253 
gen_have_thmss (ProofContext.get_thms o Proof.context_of) 

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

255 

7012  256 
fun gen_have_thmss_i f ((name, more_atts), th_atts) = 
6371  257 
f name more_atts (map (apfst single) th_atts); 
258 

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

5915  260 

261 

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

5915  271 

6371  272 
(* forward chaining *) 
273 

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

276 
fun add_thmss name atts ths_atts state = 

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

6371  278 

6879  279 
val from_facts = gen_from_facts (local_have_thmss (Proof.have_thmss [])) o Comment.ignore; 
7012  280 
val from_facts_i = gen_from_facts (gen_have_thmss_i (Proof.have_thmss [])) o Comment.ignore; 
6879  281 
val with_facts = gen_from_facts (local_have_thmss add_thmss) o Comment.ignore; 
7012  282 
val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore; 
6879  283 

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

284 
fun chain comment_ignore = ProofHistory.apply Proof.chain; 
6937  285 
fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain; 
5830  286 

287 

288 
(* context *) 

289 

7417  290 
val fix = ProofHistory.apply o Proof.fix o map Comment.ignore; 
291 
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

292 
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

293 
val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore; 
5830  294 

295 

296 
(* statements *) 

297 

7678  298 
fun multi_local_attribute state (name, src, s) = 
299 
(name, map (Attrib.local_attribute (Proof.theory_of state)) src, s); 

300 

7271  301 
local 
302 

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

303 
fun global_statement f (name, src, s) int thy = 
6688  304 
ProofHistory.init (Toplevel.undo_limit int) 
305 
(f name (map (Attrib.global_attribute thy) src) s thy); 

5830  306 

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

307 
fun global_statement_i f (name, atts, t) int thy = 
6688  308 
ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy); 
6501  309 

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

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

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

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

7271  315 
fun multi_statement f args = ProofHistory.apply (fn state => 
7678  316 
f (map (multi_local_attribute state) args) state); 
7271  317 

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

319 

320 
in 

321 

6952  322 
val theorem = global_statement Proof.theorem o Comment.ignore; 
323 
val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore; 

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

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

7271  326 
val assume = multi_statement Proof.assume o map Comment.ignore; 
327 
val assume_i = multi_statement_i Proof.assume_i o map Comment.ignore; 

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

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

6952  330 
val local_def = local_statement LocalDefs.def I o Comment.ignore; 
331 
val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore; 

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

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

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

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

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

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

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

5830  340 

7271  341 
end; 
342 

5830  343 

344 
(* blocks *) 

345 

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

346 
val begin_block = ProofHistory.apply Proof.begin_block; 
5830  347 
val next_block = ProofHistory.apply Proof.next_block; 
6937  348 
val end_block = ProofHistory.applys Proof.end_block; 
5830  349 

350 

351 
(* backward steps *) 

352 

7506  353 
val tac = ProofHistory.applys o Method.refine_no_facts; 
354 
val then_tac = ProofHistory.applys o Method.refine; 

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

355 

7002  356 
val proof = ProofHistory.applys o Method.proof o 
357 
apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore; 

6404  358 

359 

6732  360 
(* print result *) 
361 

7572  362 
local 
363 

6732  364 
fun pretty_result {kind, name, thm} = 
7590  365 
Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"), 
7572  366 
Pretty.fbrk, Proof.pretty_thm thm]; 
6986  367 

368 
fun pretty_rule thm = 

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

7572  371 
in 
372 

6732  373 
val print_result = Pretty.writeln o pretty_result; 
374 

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

377 
else (K (), K ()); 

378 

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

6732  380 

7572  381 
end; 
382 

6732  383 

6404  384 
(* local endings *) 
385 

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

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

387 
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

388 

6937  389 
fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y); 
390 

6688  391 
val local_terminal_proof = 
6937  392 
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

393 

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

394 
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

395 
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

396 
val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof); 
6404  397 

398 

399 
(* global endings *) 

400 

401 
val kill_proof = Proof.theory_of o ProofHistory.current; 

402 

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

404 
let 

405 
val state = ProofHistory.current prf; 

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

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

6404  409 

6952  410 
val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest; 
6937  411 
val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests; 
6404  412 
val global_immediate_proof = global_result Method.global_immediate_proof; 
413 
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

414 
val global_skip_proof = global_result SkipProof.global_skip_proof; 
6404  415 

416 

417 
(* common endings *) 

418 

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

421 
fun immediate_proof comment = local_immediate_proof o global_immediate_proof; 

422 
fun default_proof comment = local_default_proof o global_default_proof; 

423 
fun skip_proof comment = local_skip_proof o global_skip_proof; 

5830  424 

425 

6774  426 
(* calculational proof commands *) 
427 

6879  428 
local 
429 

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

6774  432 
else (); 
433 

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

435 

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

438 

439 
in 

440 

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

443 

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

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

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

448 

449 
end; 

6774  450 

451 

7678  452 
(* obtain *) 
453 

454 
fun obtain (xs, asms) = ProofHistory.applys (fn state => 

455 
Obtain.obtain (map Comment.ignore xs) 

456 
(map (multi_local_attribute state o Comment.ignore) asms) state); 

457 

458 
fun obtain_i (xs, asms) = ProofHistory.applys 

459 
(Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms)); 

460 

461 

5830  462 
(* use ML text *) 
463 

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

5830  466 

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

469 
fun use_let name body txt = 

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

471 

472 
val use_setup = 

5915  473 
use_let "setup: (theory > theory) list" "Library.apply setup"; 
5830  474 

475 

476 
(* translation functions *) 

477 

478 
val parse_ast_translation = 

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

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

481 

482 
val parse_translation = 

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

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

485 

486 
val print_translation = 

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

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

489 

490 
val print_ast_translation = 

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

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

493 

494 
val typed_print_translation = 

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

496 
"Theory.add_trfunsT typed_print_translation"; 

497 

498 
val token_translation = 

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

500 
"Theory.add_tokentrfuns token_translation"; 

501 

502 

503 
(* add_oracle *) 

504 

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

505 
fun add_oracle ((name, txt), comment_ignore) = 
5830  506 
use_let 
507 
"oracle: bstring * (Sign.sg * Object.T > term)" 

508 
"Theory.add_oracle oracle" 

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

510 

511 

6688  512 
(* theory init and exit *) 
5830  513 

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

518 
in Present.begin_theory name parents paths thy end; 
5830  519 

7242  520 
val begin_theory = gen_begin_theory ThyInfo.begin_theory; 
521 
val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory; 

7909  522 

523 
fun end_theory thy = 

7932  524 
if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy 
7909  525 
else thy; 
526 

7932  527 
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; 
6688  528 

7103  529 

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

7242  531 
(if int then begin_update_theory else begin_theory) name parents files; 
7103  532 

6331  533 
fun en_theory thy = (end_theory thy; ()); 
534 

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

537 

538 
(* context switch *) 

539 

7953  540 
fun init_context (f: string > unit) name = 
541 
Toplevel.init_theory (fn _ => (the (#2 (Context.pass None f name)))) (K ()) (K ()); 

542 

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

6246  544 

5830  545 

546 
end; 