author  wenzelm 
Sat, 28 May 2016 21:38:58 +0200  
changeset 63178  b9e1d53124f5 
parent 63094  056ea294c256 
child 63180  ddfd021884b4 
permissions  rwrr 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

1 
(* Title: Pure/Pure.thy 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

2 
Author: Makarius 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

3 

62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62913
diff
changeset

4 
The Pure theory, with definitions of Isar commands and some lemmas. 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

5 
*) 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

6 

48638  7 
theory Pure 
62859  8 
keywords 
61579  9 
"!!" "!" "+" "" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset

10 
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>" 
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset

11 
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains" 
62913  12 
"defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix" 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset

13 
"infixl" "infixr" "is" "notes" "obtains" "open" "output" 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61338
diff
changeset

14 
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites" 
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61338
diff
changeset

15 
"shows" "structure" "unchecked" "where" "when" "" 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset

16 
and "text" "txt" :: document_body 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset

17 
and "text_raw" :: document_raw 
57506  18 
and "default_sort" :: thy_decl == "" 
19 
and "typedecl" "type_synonym" "nonterminal" "judgment" 

62169  20 
"consts" "syntax" "no_syntax" "translations" "no_translations" 
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset

21 
"definition" "abbreviation" "type_notation" "no_type_notation" "notation" 
61337  22 
"no_notation" "axiomatization" "lemmas" "declare" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

23 
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

24 
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" 
60957
574254152856
support for ML files with/without debugger information;
wenzelm
parents:
60749
diff
changeset

25 
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset

26 
and "SML_import" "SML_export" :: thy_decl % "ML" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

27 
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

28 
and "ML_val" "ML_command" :: diag % "ML" 
55762
27a45aec67a0
suppress completion of obscure keyword, avoid confusion with plain "simp";
wenzelm
parents:
55516
diff
changeset

29 
and "simproc_setup" :: thy_decl % "ML" == "" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

30 
and "setup" "local_setup" "attribute_setup" "method_setup" 
55762
27a45aec67a0
suppress completion of obscure keyword, avoid confusion with plain "simp";
wenzelm
parents:
55516
diff
changeset

31 
"declaration" "syntax_declaration" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

32 
"parse_ast_translation" "parse_translation" "print_translation" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

33 
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

34 
and "bundle" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

35 
and "include" "including" :: prf_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

36 
and "print_bundles" :: diag 
59901  37 
and "context" "locale" "experiment" :: thy_decl_block 
51224
c3e99efacb67
back to nonschematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset

38 
and "interpret" :: prf_goal % "proof" 
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61853
diff
changeset

39 
and "interpretation" "global_interpretation" "sublocale" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

40 
and "class" :: thy_decl_block 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

41 
and "subclass" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

42 
and "instantiation" :: thy_decl_block 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

43 
and "instance" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

44 
and "overloading" :: thy_decl_block 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

45 
and "code_datatype" :: thy_decl 
61338  46 
and "theorem" "lemma" "corollary" "proposition" :: thy_goal 
61337  47 
and "schematic_goal" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

48 
and "notepad" :: thy_decl_block 
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

49 
and "have" :: prf_goal % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

50 
and "hence" :: prf_goal % "proof" == "then have" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

51 
and "show" :: prf_asm_goal % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

52 
and "thus" :: prf_asm_goal % "proof" == "then show" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

53 
and "then" "from" "with" :: prf_chain % "proof" 
60371  54 
and "note" :: prf_decl % "proof" 
55 
and "supply" :: prf_script % "proof" 

56 
and "using" "unfolding" :: prf_decl % "proof" 

63039  57 
and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof" 
60448  58 
and "consider" :: prf_goal % "proof" 
53371
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52549
diff
changeset

59 
and "obtain" :: prf_asm_goal % "proof" 
60624  60 
and "guess" :: prf_script_asm_goal % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

61 
and "let" "write" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

62 
and "case" :: prf_asm % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

63 
and "{" :: prf_open % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

64 
and "}" :: prf_close % "proof" 
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60624
diff
changeset

65 
and "next" :: next_block % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

66 
and "qed" :: qed_block % "proof" 
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62169
diff
changeset

67 
and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof" 
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset

68 
and "done" :: "qed_script" % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

69 
and "oops" :: qed_global % "proof" 
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

70 
and "defer" "prefer" "apply" :: prf_script % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

71 
and "apply_end" :: prf_script % "proof" == "" 
60624  72 
and "subgoal" :: prf_script_goal % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

73 
and "proof" :: prf_block % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

74 
and "also" "moreover" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

75 
and "finally" "ultimately" :: prf_chain % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

76 
and "back" :: prf_script % "proof" 
61252  77 
and "help" "print_commands" "print_options" "print_context" "print_theory" 
78 
"print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" 

48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

79 
"print_theorems" "print_locales" "print_classes" "print_locale" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

80 
"print_interps" "print_dependencies" "print_attributes" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

81 
"print_simpset" "print_rules" "print_trans_rules" "print_methods" 
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

82 
"print_antiquotations" "print_ML_antiquotations" "thy_deps" 
58845  83 
"locale_deps" "class_deps" "thm_deps" "print_term_bindings" 
57415
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56864
diff
changeset

84 
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" 
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56864
diff
changeset

85 
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag 
58845  86 
and "display_drafts" "print_state" :: diag 
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

87 
and "welcome" :: diag 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

88 
and "end" :: thy_end % "theory" 
56797  89 
and "realizers" :: thy_decl == "" 
90 
and "realizability" :: thy_decl == "" 

91 
and "extract_type" "extract" :: thy_decl 

48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

92 
and "find_theorems" "find_consts" :: diag 
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
57506
diff
changeset

93 
and "named_theorems" :: thy_decl 
48638  94 
begin 
15803  95 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

96 
section \<open>Isar commands\<close> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

97 

62856  98 
subsection \<open>Embedded ML text\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

99 

62856  100 
ML \<open> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

101 
local 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

102 

62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

103 
val semi = Scan.option @{keyword ";"}; 
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

104 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

105 
val _ = 
62867  106 
Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

107 
(Resources.parse_files "ML_file"  semi >> ML_File.ML NONE); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

108 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

109 
val _ = 
62867  110 
Outer_Syntax.command @{command_keyword ML_file_debug} 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

111 
"read and evaluate Isabelle/ML file (with debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

112 
(Resources.parse_files "ML_file_debug"  semi >> ML_File.ML (SOME true)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

113 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

114 
val _ = 
62867  115 
Outer_Syntax.command @{command_keyword ML_file_no_debug} 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

116 
"read and evaluate Isabelle/ML file (no debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

117 
(Resources.parse_files "ML_file_no_debug"  semi >> ML_File.ML (SOME false)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

118 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

119 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

120 
Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

121 
(Resources.parse_files "SML_file"  semi >> ML_File.SML NONE); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

122 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

123 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

124 
Outer_Syntax.command @{command_keyword SML_file_debug} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

125 
"read and evaluate Standard ML file (with debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

126 
(Resources.parse_files "SML_file_debug"  semi >> ML_File.SML (SOME true)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

127 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

128 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

129 
Outer_Syntax.command @{command_keyword SML_file_no_debug} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

130 
"read and evaluate Standard ML file (no debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

131 
(Resources.parse_files "SML_file_no_debug"  semi >> ML_File.SML (SOME false)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

132 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

133 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

134 
Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

135 
(Parse.ML_source >> (fn source => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

136 
let 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

137 
val flags: ML_Compiler.flags = 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

138 
{SML = true, exchange = true, redirect = false, verbose = true, 
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

139 
debug = NONE, writeln = writeln, warning = warning}; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

140 
in 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

141 
Toplevel.theory 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

142 
(Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

143 
end)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

144 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

145 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

146 
Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

147 
(Parse.ML_source >> (fn source => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

148 
let 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

149 
val flags: ML_Compiler.flags = 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

150 
{SML = false, exchange = true, redirect = false, verbose = true, 
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

151 
debug = NONE, writeln = writeln, warning = warning}; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

152 
in 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

153 
Toplevel.generic_theory 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

154 
(ML_Context.exec (fn () => ML_Context.eval_source flags source) #> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

155 
Local_Theory.propagate_ml_env) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

156 
end)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

157 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

158 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

159 
Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

160 
(Parse.ML_source >> (fn source => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

161 
Toplevel.proof (Proof.map_context (Context.proof_map 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

162 
(ML_Context.exec (fn () => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

163 
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

164 
Proof.propagate_ml_env))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

165 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

166 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

167 
Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

168 
(Parse.ML_source >> Isar_Cmd.ml_diag true); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

169 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

170 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

171 
Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

172 
(Parse.ML_source >> Isar_Cmd.ml_diag false); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

173 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

174 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

175 
Outer_Syntax.command @{command_keyword setup} "ML setup for global theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

176 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

177 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

178 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

179 
Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

180 
(Parse.ML_source >> Isar_Cmd.local_setup); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

181 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

182 
val _ = 
62856  183 
Outer_Syntax.command @{command_keyword oracle} "declare oracle" 
184 
(Parse.range Parse.name  (@{keyword "="}  Parse.ML_source) >> 

185 
(fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); 

186 

187 
val _ = 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

188 
Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

189 
(Parse.position Parse.name  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

190 
Parse.!!! (@{keyword "="}  Parse.ML_source  Scan.optional Parse.text "") 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

191 
>> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

192 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

193 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

194 
Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

195 
(Parse.position Parse.name  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

196 
Parse.!!! (@{keyword "="}  Parse.ML_source  Scan.optional Parse.text "") 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

197 
>> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

198 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

199 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

200 
Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

201 
(Parse.opt_keyword "pervasive"  Parse.ML_source 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

202 
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

203 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

204 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

205 
Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

206 
(Parse.opt_keyword "pervasive"  Parse.ML_source 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

207 
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

208 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

209 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

210 
Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

211 
(Parse.position Parse.name  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

212 
(@{keyword "("}  Parse.enum1 "" Parse.term  @{keyword ")"}  @{keyword "="})  
62913  213 
Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

214 

62856  215 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

216 

62856  217 

218 
subsection \<open>Theory commands\<close> 

219 

220 
subsubsection \<open>Sorts and types\<close> 

221 

222 
ML \<open> 

223 
local 

224 

225 
val _ = 

226 
Outer_Syntax.local_theory @{command_keyword default_sort} 

227 
"declare default sort for explicit type variables" 

228 
(Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); 

229 

230 
val _ = 

231 
Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration" 

232 
(Parse.type_args  Parse.binding  Parse.opt_mixfix 

233 
>> (fn ((args, a), mx) => 

234 
Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); 

235 

236 
val _ = 

237 
Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation" 

238 
(Parse.type_args  Parse.binding  

239 
(@{keyword "="}  Parse.!!! (Parse.typ  Parse.opt_mixfix')) 

240 
>> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); 

241 

242 
in end\<close> 

243 

244 

245 
subsubsection \<open>Consts\<close> 

246 

247 
ML \<open> 

248 
local 

249 

250 
val _ = 

251 
Outer_Syntax.command @{command_keyword judgment} "declare objectlogic judgment" 

252 
(Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); 

253 

254 
val _ = 

255 
Outer_Syntax.command @{command_keyword consts} "declare constants" 

256 
(Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); 

257 

258 
in end\<close> 

259 

260 

261 
subsubsection \<open>Syntax and translations\<close> 

262 

263 
ML \<open> 

264 
local 

265 

266 
val _ = 

267 
Outer_Syntax.command @{command_keyword nonterminal} 

268 
"declare syntactic type constructors (grammar nonterminal symbols)" 

269 
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); 

270 

271 
val _ = 

272 
Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses" 

273 
(Parse.syntax_mode  Scan.repeat1 Parse.const_decl 

274 
>> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); 

275 

276 
val _ = 

277 
Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses" 

278 
(Parse.syntax_mode  Scan.repeat1 Parse.const_decl 

279 
>> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); 

280 

281 
val trans_pat = 

282 
Scan.optional 

62969  283 
(@{keyword "("}  Parse.!!! (Parse.inner_syntax Parse.name  @{keyword ")"})) "logic" 
62856  284 
 Parse.inner_syntax Parse.string; 
285 

286 
fun trans_arrow toks = 

287 
((@{keyword "\<rightharpoonup>"}  @{keyword "=>"}) >> K Syntax.Parse_Rule  

288 
(@{keyword "\<leftharpoondown>"}  @{keyword "<="}) >> K Syntax.Print_Rule  

289 
(@{keyword "\<rightleftharpoons>"}  @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks; 

290 

291 
val trans_line = 

292 
trans_pat  Parse.!!! (trans_arrow  trans_pat) 

293 
>> (fn (left, (arr, right)) => arr (left, right)); 

294 

295 
val _ = 

296 
Outer_Syntax.command @{command_keyword translations} "add syntax translation rules" 

297 
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); 

298 

299 
val _ = 

300 
Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules" 

301 
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); 

302 

303 
in end\<close> 

304 

305 

306 
subsubsection \<open>Translation functions\<close> 

307 

308 
ML \<open> 

309 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

310 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

311 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

312 
Outer_Syntax.command @{command_keyword parse_ast_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

313 
"install parse ast translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

314 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

315 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

316 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

317 
Outer_Syntax.command @{command_keyword parse_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

318 
"install parse translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

319 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

320 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

321 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

322 
Outer_Syntax.command @{command_keyword print_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

323 
"install print translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

324 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

325 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

326 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

327 
Outer_Syntax.command @{command_keyword typed_print_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

328 
"install typed print translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

329 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

330 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

331 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

332 
Outer_Syntax.command @{command_keyword print_ast_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

333 
"install print ast translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

334 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

335 

62856  336 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

337 

62856  338 

339 
subsubsection \<open>Specifications\<close> 

340 

341 
ML \<open> 

342 
local 

343 

344 
val _ = 

345 
Outer_Syntax.local_theory' @{command_keyword definition} "constant definition" 

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

346 
(Scan.option Parse_Spec.constdecl  Parse_Spec.spec 
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63059
diff
changeset

347 
>> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c)); 
62856  348 

349 
val _ = 

350 
Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation" 

351 
(Parse.syntax_mode  (Scan.option Parse_Spec.constdecl  Parse.prop) 

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

352 
>> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b)); 
62856  353 

63178  354 
val axiomatization = 
355 
Parse.and_list1 (Parse_Spec.thm_name ":"  Parse.prop)  

356 
Parse_Spec.if_assumes  Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); 

357 

62856  358 
val _ = 
359 
Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification" 

360 
(Scan.optional Parse.fixes []  

63178  361 
Scan.optional (Parse.where_  Parse.!!! axiomatization) ([], [], []) 
362 
>> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); 

62856  363 

364 
in end\<close> 

365 

366 

367 
subsubsection \<open>Notation\<close> 

368 

369 
ML \<open> 

370 
local 

371 

372 
val _ = 

373 
Outer_Syntax.local_theory @{command_keyword type_notation} 

374 
"add concrete syntax for type constructors" 

375 
(Parse.syntax_mode  Parse.and_list1 (Parse.type_const  Parse.mixfix) 

376 
>> (fn (mode, args) => Specification.type_notation_cmd true mode args)); 

377 

378 
val _ = 

379 
Outer_Syntax.local_theory @{command_keyword no_type_notation} 

380 
"delete concrete syntax for type constructors" 

381 
(Parse.syntax_mode  Parse.and_list1 (Parse.type_const  Parse.mixfix) 

382 
>> (fn (mode, args) => Specification.type_notation_cmd false mode args)); 

383 

384 
val _ = 

385 
Outer_Syntax.local_theory @{command_keyword notation} 

386 
"add concrete syntax for constants / fixed variables" 

387 
(Parse.syntax_mode  Parse.and_list1 (Parse.const  Parse.mixfix) 

388 
>> (fn (mode, args) => Specification.notation_cmd true mode args)); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

389 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

390 
val _ = 
62856  391 
Outer_Syntax.local_theory @{command_keyword no_notation} 
392 
"delete concrete syntax for constants / fixed variables" 

393 
(Parse.syntax_mode  Parse.and_list1 (Parse.const  Parse.mixfix) 

394 
>> (fn (mode, args) => Specification.notation_cmd false mode args)); 

395 

396 
in end\<close> 

397 

398 

399 
subsubsection \<open>Theorems\<close> 

400 

401 
ML \<open> 

402 
local 

403 

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

404 
val long_keyword = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

405 
Parse_Spec.includes >> K ""  
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

406 
Parse_Spec.long_statement_keyword; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

407 

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

408 
val long_statement = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

409 
Scan.optional (Parse_Spec.opt_thm_name ":"  Scan.ahead long_keyword) Attrib.empty_binding  
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

410 
Scan.optional Parse_Spec.includes []  Parse_Spec.long_statement 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

411 
>> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

412 

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

413 
val short_statement = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

414 
Parse_Spec.statement  Parse_Spec.if_statement  Parse.for_fixes 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

415 
>> (fn ((shows, assumes), fixes) => 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

416 
(false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes], 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

417 
Element.Shows shows)); 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

418 

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

419 
fun theorem spec schematic descr = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

420 
Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

421 
((long_statement  short_statement) >> (fn (long, binding, includes, elems, concl) => 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

422 
((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

423 
long Thm.theoremK NONE (K I) binding includes elems concl))); 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

424 

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

425 
val _ = theorem @{command_keyword theorem} false "theorem"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

426 
val _ = theorem @{command_keyword lemma} false "lemma"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

427 
val _ = theorem @{command_keyword corollary} false "corollary"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

428 
val _ = theorem @{command_keyword proposition} false "proposition"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

429 
val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

430 

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

431 
in end\<close> 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

432 

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

433 
ML \<open> 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

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

435 

62856  436 
val _ = 
437 
Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems" 

438 
(Parse_Spec.name_facts  Parse.for_fixes >> 

439 
(fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); 

440 

441 
val _ = 

442 
Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems" 

62969  443 
(Parse.and_list1 Parse.thms1  Parse.for_fixes 
62856  444 
>> (fn (facts, fixes) => 
445 
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes)); 

446 

447 
val _ = 

448 
Outer_Syntax.local_theory @{command_keyword named_theorems} 

449 
"declare named collection of theorems" 

450 
(Parse.and_list1 (Parse.binding  Scan.optional Parse.text "") >> 

451 
fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); 

452 

453 
in end\<close> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

454 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

455 

62856  456 
subsubsection \<open>Hide names\<close> 
457 

458 
ML \<open> 

459 
local 

460 

461 
fun hide_names command_keyword what hide parse prep = 

462 
Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") 

463 
((Parse.opt_keyword "open" >> not)  Scan.repeat1 parse >> (fn (fully, args) => 

464 
(Toplevel.theory (fn thy => 

465 
let val ctxt = Proof_Context.init_global thy 

466 
in fold (hide fully o prep ctxt) args thy end)))); 

467 

468 
val _ = 

469 
hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class 

470 
Proof_Context.read_class; 

471 

472 
val _ = 

473 
hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const 

474 
((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); 

475 

476 
val _ = 

477 
hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const 

478 
((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); 

479 

480 
val _ = 

481 
hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact 

62969  482 
(Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of); 
62856  483 

484 
in end\<close> 

485 

486 

487 
subsection \<open>Bundled declarations\<close> 

488 

489 
ML \<open> 

490 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

491 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

492 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

493 
Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations" 
62969  494 
((Parse.binding  @{keyword "="})  Parse.thms1  Parse.for_fixes 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

495 
>> (uncurry Bundle.bundle_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

496 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

497 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

498 
Outer_Syntax.command @{command_keyword include} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

499 
"include declarations from bundle in proof body" 
62969  500 
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

501 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

502 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

503 
Outer_Syntax.command @{command_keyword including} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

504 
"include declarations from bundle in goal refinement" 
62969  505 
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

506 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

507 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

508 
Outer_Syntax.command @{command_keyword print_bundles} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

509 
"print bundles of declarations" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

510 
(Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

511 

62856  512 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

513 

62856  514 

515 
subsection \<open>Local theory specifications\<close> 

516 

517 
subsubsection \<open>Specification context\<close> 

518 

519 
ML \<open> 

520 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

521 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

522 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

523 
Outer_Syntax.command @{command_keyword context} "begin local theory context" 
62969  524 
((Parse.position Parse.name >> (fn name => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

525 
Toplevel.begin_local_theory true (Named_Target.begin name))  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

526 
Scan.optional Parse_Spec.includes []  Scan.repeat Parse_Spec.context_element 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

527 
>> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

528 
 Parse.begin); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

529 

62856  530 
val _ = 
531 
Outer_Syntax.command @{command_keyword end} "end context" 

532 
(Scan.succeed 

533 
(Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o 

534 
Toplevel.end_proof (K Proof.end_notepad))); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

535 

62856  536 
in end\<close> 
537 

538 

539 
subsubsection \<open>Locales and interpretation\<close> 

540 

541 
ML \<open> 

542 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

543 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

544 
val locale_val = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

545 
Parse_Spec.locale_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

546 
Scan.optional (@{keyword "+"}  Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) []  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

547 
Scan.repeat1 Parse_Spec.context_element >> pair ([], []); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

548 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

549 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

550 
Outer_Syntax.command @{command_keyword locale} "define named specification context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

551 
(Parse.binding  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

552 
Scan.optional (@{keyword "="}  Parse.!!! locale_val) (([], []), [])  Parse.opt_begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

553 
>> (fn ((name, (expr, elems)), begin) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

554 
Toplevel.begin_local_theory begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

555 
(Expression.add_locale_cmd name Binding.empty expr elems #> snd))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

556 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

557 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

558 
Outer_Syntax.command @{command_keyword experiment} "open private specification context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

559 
(Scan.repeat Parse_Spec.context_element  Parse.begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

560 
>> (fn elems => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

561 
Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

562 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

563 
val interpretation_args = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

564 
Parse.!!! Parse_Spec.locale_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

565 
Scan.optional 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

566 
(@{keyword "rewrites"}  Parse.and_list1 (Parse_Spec.opt_thm_name ":"  Parse.prop)) []; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

567 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

568 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

569 
Outer_Syntax.command @{command_keyword interpret} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

570 
"prove interpretation of locale expression in proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

571 
(interpretation_args >> (fn (expr, equations) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

572 
Toplevel.proof (Interpretation.interpret_cmd expr equations))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

573 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

574 
val interpretation_args_with_defs = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

575 
Parse.!!! Parse_Spec.locale_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

576 
(Scan.optional (@{keyword "defines"}  Parse.and_list1 (Parse_Spec.opt_thm_name ":" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

577 
 ((Parse.binding  Parse.opt_mixfix')  @{keyword "="}  Parse.term))) []  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

578 
Scan.optional 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

579 
(@{keyword "rewrites"}  Parse.and_list1 (Parse_Spec.opt_thm_name ":"  Parse.prop)) []); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

580 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

581 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

582 
Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

583 
"prove interpretation of locale expression into global theory" 
62856  584 
(interpretation_args_with_defs >> (fn (expr, (defs, equations)) => 
585 
Interpretation.global_interpretation_cmd expr defs equations)); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

586 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

587 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

588 
Outer_Syntax.command @{command_keyword sublocale} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

589 
"prove sublocale relation between a locale and a locale expression" 
62969  590 
((Parse.position Parse.name  (@{keyword "\<subseteq>"}  @{keyword "<"})  
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

591 
interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

592 
Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

593 
 interpretation_args_with_defs >> (fn (expr, (defs, equations)) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

594 
Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

595 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

596 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

597 
Outer_Syntax.command @{command_keyword interpretation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

598 
"prove interpretation of locale expression in local theory or into global theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

599 
(interpretation_args >> (fn (expr, equations) => 
62856  600 
Toplevel.local_theory_to_proof NONE NONE 
601 
(Interpretation.isar_interpretation_cmd expr equations))); 

602 

603 
in end\<close> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

604 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

605 

62856  606 
subsubsection \<open>Type classes\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

607 

62856  608 
ML \<open> 
609 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

610 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

611 
val class_val = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

612 
Parse_Spec.class_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

613 
Scan.optional (@{keyword "+"}  Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) []  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

614 
Scan.repeat1 Parse_Spec.context_element >> pair []; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

615 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

616 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

617 
Outer_Syntax.command @{command_keyword class} "define type class" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

618 
(Parse.binding  Scan.optional (@{keyword "="}  class_val) ([], [])  Parse.opt_begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

619 
>> (fn ((name, (supclasses, elems)), begin) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

620 
Toplevel.begin_local_theory begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

621 
(Class_Declaration.class_cmd name supclasses elems #> snd))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

622 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

623 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

624 
Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

625 
(Parse.class >> Class_Declaration.subclass_cmd); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

626 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

627 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

628 
Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

629 
(Parse.multi_arity  Parse.begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

630 
>> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

631 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

632 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

633 
Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

634 
((Parse.class  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

635 
((@{keyword "\<subseteq>"}  @{keyword "<"})  Parse.!!! Parse.class) >> Class.classrel_cmd  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

636 
Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

637 
Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

638 

62856  639 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

640 

62856  641 

642 
subsubsection \<open>Arbitrary overloading\<close> 

643 

644 
ML \<open> 

645 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

646 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

647 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

648 
Outer_Syntax.command @{command_keyword overloading} "overloaded definitions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

649 
(Scan.repeat1 (Parse.name  (@{keyword "=="}  @{keyword "\<equiv>"})  Parse.term  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

650 
Scan.optional (@{keyword "("}  (@{keyword "unchecked"} >> K false)  @{keyword ")"}) true 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

651 
>> Scan.triple1)  Parse.begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

652 
>> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

653 

62856  654 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

655 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

656 

62856  657 
subsection \<open>Proof commands\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

658 

62856  659 
ML \<open> 
660 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

661 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

662 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

663 
Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

664 
(Parse.begin >> K Proof.begin_notepad); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

665 

62856  666 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

667 

62856  668 

669 
subsubsection \<open>Statements\<close> 

670 

671 
ML \<open> 

672 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

673 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

674 
val structured_statement = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

675 
Parse_Spec.statement  Parse_Spec.cond_statement  Parse.for_fixes 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

676 
>> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

677 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

678 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

679 
Outer_Syntax.command @{command_keyword have} "state local goal" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

680 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

681 
Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

682 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

683 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

684 
Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

685 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

686 
Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

687 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

688 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

689 
Outer_Syntax.command @{command_keyword hence} "oldstyle alias of \"then have\"" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

690 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

691 
Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

692 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

693 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

694 
Outer_Syntax.command @{command_keyword thus} "oldstyle alias of \"then show\"" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

695 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

696 
Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

697 

62856  698 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

699 

62856  700 

701 
subsubsection \<open>Local facts\<close> 

702 

703 
ML \<open> 

704 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

705 

62969  706 
val facts = Parse.and_list1 Parse.thms1; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

707 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

708 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

709 
Outer_Syntax.command @{command_keyword then} "forward chaining" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

710 
(Scan.succeed (Toplevel.proof Proof.chain)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

711 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

712 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

713 
Outer_Syntax.command @{command_keyword from} "forward chaining from given facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

714 
(facts >> (Toplevel.proof o Proof.from_thmss_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

715 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

716 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

717 
Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

718 
(facts >> (Toplevel.proof o Proof.with_thmss_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

719 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

720 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

721 
Outer_Syntax.command @{command_keyword note} "define facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

722 
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

723 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

724 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

725 
Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

726 
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

727 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

728 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

729 
Outer_Syntax.command @{command_keyword using} "augment goal facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

730 
(facts >> (Toplevel.proof o Proof.using_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

731 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

732 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

733 
Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

734 
(facts >> (Toplevel.proof o Proof.unfolding_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

735 

62856  736 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

737 

62856  738 

739 
subsubsection \<open>Proof context\<close> 

740 

741 
ML \<open> 

742 
local 

743 

744 
val structured_statement = 

745 
Parse_Spec.statement  Parse_Spec.if_statement'  Parse.for_fixes 

746 
>> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

747 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

748 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

749 
Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

750 
(Parse.fixes >> (Toplevel.proof o Proof.fix_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

751 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

752 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

753 
Outer_Syntax.command @{command_keyword assume} "assume propositions" 
62856  754 
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

755 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

756 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

757 
Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later" 
62856  758 
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

759 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

760 
val _ = 
63039  761 
Outer_Syntax.command @{command_keyword define} "local definition (nonpolymorphic)" 
762 
((Parse.fixes  Parse.where_)  Parse_Spec.statement  Parse.for_fixes 

763 
>> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); 

764 

765 
val _ = 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

766 
Outer_Syntax.command @{command_keyword def} "local definition (nonpolymorphic)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

767 
(Parse.and_list1 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

768 
(Parse_Spec.opt_thm_name ":"  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

769 
((Parse.binding  Parse.opt_mixfix)  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

770 
((@{keyword "\<equiv>"}  @{keyword "=="})  Parse.!!! Parse.termp))) 
63043  771 
>> (fn args => Toplevel.proof (fn state => 
772 
(legacy_feature "Old 'def' command  use 'define' instead"; Proof.def_cmd args state)))); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

773 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

774 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

775 
Outer_Syntax.command @{command_keyword consider} "state cases rule" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

776 
(Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

777 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

778 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

779 
Outer_Syntax.command @{command_keyword obtain} "generalized elimination" 
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

780 
(Parse.parbinding  Scan.optional (Parse.fixes  Parse.where_) []  structured_statement 
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

781 
>> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

782 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

783 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

784 
Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

785 
(Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

786 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

787 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

788 
Outer_Syntax.command @{command_keyword let} "bind text variables" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

789 
(Parse.and_list1 (Parse.and_list1 Parse.term  (@{keyword "="}  Parse.term)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

790 
>> (Toplevel.proof o Proof.let_bind_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

791 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

792 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

793 
Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables" 
62856  794 
(Parse.syntax_mode  Parse.and_list1 (Parse.const  Parse.mixfix) 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

795 
>> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

796 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

797 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

798 
Outer_Syntax.command @{command_keyword case} "invoke local context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

799 
(Parse_Spec.opt_thm_name ":"  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

800 
(@{keyword "("}  
62969  801 
Parse.!!! (Parse.position Parse.name  Scan.repeat (Parse.maybe Parse.binding) 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

802 
 @{keyword ")"})  
62969  803 
Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

804 

62856  805 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

806 

62856  807 

808 
subsubsection \<open>Proof structure\<close> 

809 

810 
ML \<open> 

811 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

812 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

813 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

814 
Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

815 
(Scan.succeed (Toplevel.proof Proof.begin_block)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

816 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

817 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

818 
Outer_Syntax.command @{command_keyword "}"} "end explicit proof block" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

819 
(Scan.succeed (Toplevel.proof Proof.end_block)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

820 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

821 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

822 
Outer_Syntax.command @{command_keyword next} "enter next proof block" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

823 
(Scan.succeed (Toplevel.proof Proof.next_block)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

824 

62856  825 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

826 

62856  827 

828 
subsubsection \<open>End proof\<close> 

829 

830 
ML \<open> 

831 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

832 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

833 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

834 
Outer_Syntax.command @{command_keyword qed} "conclude proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

835 
(Scan.option Method.parse >> (fn m => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

836 
(Option.map Method.report m; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

837 
Isar_Cmd.qed m))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

838 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

839 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

840 
Outer_Syntax.command @{command_keyword by} "terminal backward proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

841 
(Method.parse  Scan.option Method.parse >> (fn (m1, m2) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

842 
(Method.report m1; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

843 
Option.map Method.report m2; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

844 
Isar_Cmd.terminal_proof (m1, m2)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

845 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

846 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

847 
Outer_Syntax.command @{command_keyword ".."} "default proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

848 
(Scan.succeed Isar_Cmd.default_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

849 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

850 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

851 
Outer_Syntax.command @{command_keyword "."} "immediate proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

852 
(Scan.succeed Isar_Cmd.immediate_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

853 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

854 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

855 
Outer_Syntax.command @{command_keyword done} "done proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

856 
(Scan.succeed Isar_Cmd.done_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

857 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

858 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

859 
Outer_Syntax.command @{command_keyword sorry} "skip proof (quickanddirty mode only!)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

860 
(Scan.succeed Isar_Cmd.skip_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

861 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

862 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

863 
Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quickanddirty mode only!)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

864 
(Scan.succeed Isar_Cmd.skip_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

865 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

866 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

867 
Outer_Syntax.command @{command_keyword oops} "forget proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

868 
(Scan.succeed (Toplevel.forget_proof true)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

869 

62856  870 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

871 

62856  872 

873 
subsubsection \<open>Proof steps\<close> 

874 

875 
ML \<open> 

876 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

877 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

878 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

879 
Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

880 
(Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

881 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

882 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

883 
Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

884 
(Parse.nat >> (Toplevel.proof o Proof.prefer)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

885 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

886 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

887 
Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

888 
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

889 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

890 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

891 
Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

892 
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

893 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

894 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

895 
Outer_Syntax.command @{command_keyword proof} "backward proof step" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

896 
(Scan.option Method.parse >> (fn m => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

897 
(Option.map Method.report m; Toplevel.proofs (Proof.proof m)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

898 

62856  899 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

900 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

901 

62856  902 
subsubsection \<open>Subgoal focus\<close> 
903 

904 
ML \<open> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

905 
local 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

906 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

907 
val opt_fact_binding = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

908 
Scan.optional (Parse.binding  Parse.opt_attribs  Parse.attribs >> pair Binding.empty) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

909 
Attrib.empty_binding; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

910 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

911 
val for_params = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

912 
Scan.optional 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

913 
(@{keyword "for"}  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

914 
Parse.!!! ((Scan.option Parse.dots >> is_some)  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

915 
(Scan.repeat1 (Parse.position (Parse.maybe Parse.name))))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

916 
(false, []); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

917 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

918 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

919 
Outer_Syntax.command @{command_keyword subgoal} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

920 
"focus on first subgoal within backward refinement" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

921 
(opt_fact_binding  (Scan.option (@{keyword "premises"}  Parse.!!! opt_fact_binding))  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

922 
for_params >> (fn ((a, b), c) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

923 
Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

924 

62856  925 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

926 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

927 

62856  928 
subsubsection \<open>Calculation\<close> 
929 

930 
ML \<open> 

931 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

932 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

933 
val calculation_args = 
62969  934 
Scan.option (@{keyword "("}  Parse.!!! ((Parse.thms1  @{keyword ")"}))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

935 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

936 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

937 
Outer_Syntax.command @{command_keyword also} "combine calculation and current facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

938 
(calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

939 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

940 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

941 
Outer_Syntax.command @{command_keyword finally} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

942 
"combine calculation and current facts, exhibit result" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

943 
(calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

944 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

945 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

946 
Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

947 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

948 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

949 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

950 
Outer_Syntax.command @{command_keyword ultimately} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

951 
"augment calculation by current facts, exhibit result" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

952 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

953 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

954 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

955 
Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

956 
(Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

957 

62856  958 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

959 

62856  960 

961 
subsubsection \<open>Proof navigation\<close> 

962 

963 
ML \<open> 

964 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

965 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

966 
fun report_back () = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

967 
Output.report [Markup.markup Markup.bad "Explicit backtracking"]; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

968 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

969 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

970 
Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

971 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

972 
(Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

973 
Toplevel.skip_proof report_back)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

974 

62856  975 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

976 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

977 

62856  978 
subsection \<open>Diagnostic commands (for interactive mode only)\<close> 
979 

980 
ML \<open> 

981 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

982 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

983 
val opt_modes = 
62969  984 
Scan.optional (@{keyword "("}  Parse.!!! (Scan.repeat1 Parse.name  @{keyword ")"})) []; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

985 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

986 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

987 
Outer_Syntax.command @{command_keyword help} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

988 
"retrieve outer syntax commands according to name patterns" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

989 
(Scan.repeat Parse.name >> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

990 
(fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

991 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

992 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

993 
Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

994 
(Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

995 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

996 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

997 
Outer_Syntax.command @{command_keyword print_options} "print configuration options" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

998 
(Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

999 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1000 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1001 
Outer_Syntax.command @{command_keyword print_context} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1002 
"print context of local theory target" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1003 
(Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1004 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1005 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1006 
Outer_Syntax.command @{command_keyword print_theory} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1007 
"print logical theory contents" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1008 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1009 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1010 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1011 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1012 
Outer_Syntax.command @{command_keyword print_definitions} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1013 
"print dependencies of definitional theory content" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1014 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1015 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1016 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1017 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1018 
Outer_Syntax.command @{command_keyword print_syntax} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1019 
"print inner syntax of context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1020 
(Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1021 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1022 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1023 
Outer_Syntax.command @{command_keyword print_defn_rules} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1024 
"print definitional rewrite rules of context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1025 
(Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1026 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1027 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1028 
Outer_Syntax.command @{command_keyword print_abbrevs} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1029 
"print constant abbreviations of context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1030 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1031 
Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1032 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1033 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1034 
Outer_Syntax.command @{command_keyword print_theorems} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1035 
"print theorems of local theory or proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1036 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1037 
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1038 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1039 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1040 
Outer_Syntax.command @{command_keyword print_locales} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1041 
"print locales of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1042 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1043 
Toplevel.keep (Locale.print_locales b o Toplevel.theory_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1044 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1045 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1046 
Outer_Syntax.command @{command_keyword print_classes} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1047 
"print classes of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1048 
(Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1049 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1050 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1051 
Outer_Syntax.command @{command_keyword print_locale} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1052 
"print locale of this theory" 
62969  1053 
(Parse.opt_bang  Parse.position Parse.name >> (fn (b, name) => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1054 
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1055 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1056 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1057 
Outer_Syntax.command @{command_keyword print_interps} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1058 
"print interpretations of locale for this theory or proof context" 
62969  1059 
(Parse.position Parse.name >> (fn name => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1060 
Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1061 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1062 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1063 
Outer_Syntax.command @{command_keyword print_dependencies} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1064 
"print dependencies of locale expression" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1065 
(Parse.opt_bang  Parse_Spec.locale_expression >> (fn (b, expr) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1066 
Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1067 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1068 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1069 
Outer_Syntax.command @{command_keyword print_attributes} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1070 
"print attributes of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1071 
(Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1072 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1073 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1074 
Outer_Syntax.command @{command_keyword print_simpset} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1075 
"print context of Simplifier" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1076 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1077 
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1078 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1079 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1080 
Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1081 
(Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1082 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1083 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1084 
Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1085 
(Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1086 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1087 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1088 
Outer_Syntax.command @{command_keyword print_antiquotations} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1089 
"print document antiquotations" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1090 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1091 
Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1092 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1093 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1094 
Outer_Syntax.command @{command_keyword print_ML_antiquotations} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1095 
"print ML antiquotations" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1096 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1097 
Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1098 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1099 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1100 
Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1101 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1102 
(Toplevel.keep (Toplevel.theory_of #> (fn thy => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1103 
Locale.pretty_locale_deps thy 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1104 
> map (fn {name, parents, body} => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1105 
((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1106 
> Graph_Display.display_graph_old)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1107 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1108 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1109 
Outer_Syntax.command @{command_keyword print_term_bindings} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1110 
"print term bindings of proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1111 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1112 
(Toplevel.keep 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1113 
(Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1114 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1115 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1116 
Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1117 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1118 
Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1119 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1120 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1121 
Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1122 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1123 
(Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1124 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1125 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1126 
Outer_Syntax.command @{command_keyword print_statement} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1127 
"print theorems as long statements" 
62969  1128 
(opt_modes  Parse.thms1 >> Isar_Cmd.print_stmts); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1129 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1130 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1131 
Outer_Syntax.command @{command_keyword thm} "print theorems" 
62969  1132 
(opt_modes  Parse.thms1 >> Isar_Cmd.print_thms); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1133 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1134 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1135 
Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems" 
62969  1136 
(opt_modes  Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1137 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1138 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1139 
Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems" 
62969  1140 
(opt_modes  Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1141 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1142 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1143 
Outer_Syntax.command @{command_keyword prop} "read and print proposition" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1144 
(opt_modes  Parse.term >> Isar_Cmd.print_prop); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1145 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1146 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1147 
Outer_Syntax.command @{command_keyword term} "read and print term" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1148 
(opt_modes  Parse.term >> Isar_Cmd.print_term); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1149 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1150 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1151 
Outer_Syntax.command @{command_keyword typ} "read and print type" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1152 
(opt_modes  (Parse.typ  Scan.option (@{keyword "::"}  Parse.!!! Parse.sort)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1153 
>> Isar_Cmd.print_type); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1154 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1155 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1156 
Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1157 
(Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1158 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1159 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1160 
Outer_Syntax.command @{command_keyword print_state} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1161 
"print current proof state (if present)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1162 
(opt_modes >> (fn modes => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1163 
Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1164 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1165 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1166 
Outer_Syntax.command @{command_keyword welcome} "print welcome message" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1167 
(Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1168 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1169 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1170 
Outer_Syntax.command @{command_keyword display_drafts} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1171 
"display raw source files with symbols" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1172 
(Scan.repeat1 Parse.path >> (fn names => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1173 
Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names))))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1174 

62856  1175 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1176 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1177 

62856  1178 
subsection \<open>Dependencies\<close> 
1179 

1180 
ML \<open> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1181 
local 
62856  1182 

1183 
val theory_bounds = 

62969  1184 
Parse.position Parse.theory_name >> single  
1185 
(@{keyword "("}  Parse.enum "" (Parse.position Parse.theory_name)  @{keyword ")"}); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1186 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1187 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1188 
Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1189 
(Scan.option theory_bounds  Scan.option theory_bounds >> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1190 
(fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1191 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1192 

62856  1193 
val class_bounds = 
1194 
Parse.sort >> single  

1195 
(@{keyword "("}  Parse.enum "" Parse.sort  @{keyword ")"}); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1196 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1197 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1198 
Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1199 
(Scan.option class_bounds  Scan.option class_bounds >> (fn args => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1200 
Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1201 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1202 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1203 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1204 
Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies" 
62969  1205 
(Parse.thms1 >> (fn args => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1206 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1207 
Thm_Deps.thm_deps (Toplevel.theory_of st) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1208 
(Attrib.eval_thms (Toplevel.context_of st) args)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1209 

62856  1210 

1211 
val thy_names = 

62969  1212 
Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1213 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1214 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1215 
Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1216 
(Scan.option ((thy_names  Parse.minus)  Scan.option thy_names) >> (fn opt_range => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1217 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1218 
let 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1219 
val thy = Toplevel.theory_of st; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1220 
val ctxt = Toplevel.context_of st; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1221 
fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1222 
val check = Theory.check ctxt; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1223 
in 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1224 
Thm_Deps.unused_thms 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1225 
(case opt_range of 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1226 
NONE => (Theory.parents_of thy, [thy]) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1227 
 SOME (xs, NONE) => (map check xs, [thy]) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1228 
 SOME (xs, SOME ys) => (map check xs, map check ys)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1229 
> map pretty_thm > Pretty.writeln_chunks 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1230 
end))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1231 

62856  1232 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1233 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1234 

62856  1235 
subsubsection \<open>Find consts and theorems\<close> 
1236 

1237 
ML \<open> 

1238 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1239 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1240 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1241 
Outer_Syntax.command @{command_keyword find_consts} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1242 
"find constants by name / type patterns" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1243 
(Find_Consts.query_parser >> (fn spec => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1244 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1245 
Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1246 

62856  1247 
val options = 
1248 
Scan.optional 

1249 
(Parse.$$$ "("  

1250 
Parse.!!! (Scan.option Parse.nat  

1251 
Scan.optional (Parse.reserved "with_dups" >> K false) true  Parse.$$$ ")")) 

1252 
(NONE, true); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1253 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1254 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1255 
Outer_Syntax.command @{command_keyword find_theorems} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1256 
"find theorems meeting specified criteria" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1257 
(options  Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1258 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1259 
Pretty.writeln 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1260 
(Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1261 

62856  1262 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1263 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1264 

62856  1265 
subsection \<open>Code generation\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1266 

62856  1267 
ML \<open> 
1268 
local 

1269 

1270 
val _ = 

1271 
Outer_Syntax.command @{command_keyword code_datatype} 

1272 
"define set of code datatype constructors" 

1273 
(Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd)); 

1274 

1275 
in end\<close> 

1276 

1277 

1278 
subsection \<open>Extraction of programs from proofs\<close> 

1279 

1280 
ML \<open> 

1281 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1282 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1283 
val parse_vars = Scan.optional (Parse.$$$ "("  Parse.list1 Parse.name  Parse.$$$ ")") []; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1284 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1285 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1286 
Outer_Syntax.command @{command_keyword realizers} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1287 
"specify realizers for primitive axioms / theorems, together with correctness proof" 
62969  1288 
(Scan.repeat1 (Parse.name  parse_vars  Parse.$$$ ":"  Parse.string  Parse.string) >> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1289 
(fn xs => Toplevel.theory (fn thy => Extraction.add_realizers 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1290 
(map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1291 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1292 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1293 
Outer_Syntax.command @{command_keyword realizability} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1294 
"add equations characterizing realizability" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1295 
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1296 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1297 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1298 
Outer_Syntax.command @{command_keyword extract_type} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1299 
"add equations characterizing type of extracted program" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1300 
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1301 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1302 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1303 
Outer_Syntax.command @{command_keyword extract} "extract terms from proofs" 
62969  1304 
(Scan.repeat1 (Parse.name  parse_vars) >> (fn xs => Toplevel.theory (fn thy => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1305 
Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1306 

62856  1307 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1308 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1309 

62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62913
diff
changeset

1310 
section \<open>Auxiliary lemmas\<close> 
20627  1311 

58611  1312 
subsection \<open>Metalevel connectives in assumptions\<close> 
15803  1313 

1314 
lemma meta_mp: 

58612  1315 
assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P" 
15803  1316 
shows "PROP Q" 
58612  1317 
by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>]) 
15803  1318 

23432 