author  wenzelm 
Tue, 01 Mar 2016 19:42:59 +0100  
changeset 62490  39d01eaf5292 
parent 62312  5e5a881ebc12 
child 62848  e4140efe699e 
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 

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

4 
Final stage of bootstrapping Pure, based on implicit background theory. 
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 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

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" 
61671
20d4cd2ceab2
prefer "rewrites" and "defines" to note rewrite morphisms
haftmann
parents:
61670
diff
changeset

12 
"defines" "rewrites" "fixes" "for" "identifier" "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 
60957
574254152856
support for ML files with/without debugger information;
wenzelm
parents:
60749
diff
changeset

24 
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

25 
and "SML_import" "SML_export" :: thy_decl % "ML" 
51295  26 
and "ML" :: 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" 

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

57 
and "fix" "assume" "presume" "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 

56205  96 
ML_file "ML/ml_antiquotations.ML" 
55516  97 
ML_file "ML/ml_thms.ML" 
56864  98 
ML_file "Tools/print_operation.ML" 
48891  99 
ML_file "Isar/isar_syn.ML" 
55141  100 
ML_file "Isar/calculation.ML" 
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58201
diff
changeset

101 
ML_file "Tools/bibtex.ML" 
55030  102 
ML_file "Tools/rail.ML" 
58860  103 
ML_file "Tools/rule_insts.ML" 
104 
ML_file "Tools/thm_deps.ML" 

60093  105 
ML_file "Tools/thy_deps.ML" 
58201  106 
ML_file "Tools/class_deps.ML" 
48891  107 
ML_file "Tools/find_theorems.ML" 
108 
ML_file "Tools/find_consts.ML" 

54730  109 
ML_file "Tools/simplifier_trace.ML" 
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62312
diff
changeset

110 
ML_file_no_debug "Tools/debugger.ML" 
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
57506
diff
changeset

111 
ML_file "Tools/named_theorems.ML" 
61617  112 
ML_file "Tools/jedit.ML" 
48891  113 

114 

58611  115 
section \<open>Basic attributes\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

116 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

117 
attribute_setup tagged = 
58611  118 
\<open>Scan.lift (Args.name  Args.name) >> Thm.tag\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

119 
"tagged theorem" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

120 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

121 
attribute_setup untagged = 
58611  122 
\<open>Scan.lift Args.name >> Thm.untag\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

123 
"untagged theorem" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

124 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

125 
attribute_setup kind = 
58611  126 
\<open>Scan.lift Args.name >> Thm.kind\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

127 
"theorem kind" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

128 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

129 
attribute_setup THEN = 
58611  130 
\<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1)  Attrib.thm 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

131 
>> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

132 
"resolution with rule" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

133 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

134 
attribute_setup OF = 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

135 
\<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

136 
"rule resolved with facts" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

137 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

138 
attribute_setup rename_abs = 
58611  139 
\<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

140 
Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

141 
"rename bound variables in abstractions" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

142 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

143 
attribute_setup unfolded = 
58611  144 
\<open>Attrib.thms >> (fn ths => 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

145 
Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

146 
"unfolded definitions" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

147 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

148 
attribute_setup folded = 
58611  149 
\<open>Attrib.thms >> (fn ths => 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

150 
Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

151 
"folded definitions" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

152 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

153 
attribute_setup consumes = 
58611  154 
\<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

155 
"number of consumed facts" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

156 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

157 
attribute_setup constraints = 
58611  158 
\<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

159 
"number of equality constraints" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

160 

58611  161 
attribute_setup case_names = 
162 
\<open>Scan.lift (Scan.repeat1 (Args.name  

55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

163 
Scan.optional (@{keyword "["}  Scan.repeat1 (Args.maybe Args.name)  @{keyword "]"}) [])) 
58611  164 
>> (fn cs => 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

165 
Rule_Cases.cases_hyp_names 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

166 
(map #1 cs) 
58611  167 
(map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close> 
168 
"named rule cases" 

55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

169 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

170 
attribute_setup case_conclusion = 
58611  171 
\<open>Scan.lift (Args.name  Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

172 
"named conclusion of rule cases" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

173 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

174 
attribute_setup params = 
58611  175 
\<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

176 
"named rule parameters" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

177 

58611  178 
attribute_setup rule_format = 
179 
\<open>Scan.lift (Args.mode "no_asm") 

180 
>> (fn true => Object_Logic.rule_format_no_asm  false => Object_Logic.rule_format)\<close> 

181 
"result put into canonical rule format" 

55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

182 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

183 
attribute_setup elim_format = 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

184 
\<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

185 
"destruct rule turned into elimination rule format" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

186 

58611  187 
attribute_setup no_vars = 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

188 
\<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th => 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

189 
let 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

190 
val ctxt = Variable.set_body false (Context.proof_of context); 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

191 
val ((_, [th']), _) = Variable.import true [th] ctxt; 
58611  192 
in th' end))\<close> 
193 
"imported schematic variables" 

55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

194 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

195 
attribute_setup atomize = 
58611  196 
\<open>Scan.succeed Object_Logic.declare_atomize\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

197 
"declaration of atomize rule" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

198 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

199 
attribute_setup rulify = 
58611  200 
\<open>Scan.succeed Object_Logic.declare_rulify\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

201 
"declaration of rulify rule" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

202 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

203 
attribute_setup rotated = 
58611  204 
\<open>Scan.lift (Scan.optional Parse.int 1 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

205 
>> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

206 
"rotated theorem premises" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

207 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

208 
attribute_setup defn = 
58611  209 
\<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

210 
"declaration of definitional transformations" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

211 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

212 
attribute_setup abs_def = 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61671
diff
changeset

213 
\<open>Scan.succeed (Thm.rule_attribute [] (fn context => 
58611  214 
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

215 
"abstract over free variables of definitional theorem" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

216 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

217 

58611  218 
section \<open>Further content for the Pure theory\<close> 
20627  219 

58611  220 
subsection \<open>Metalevel connectives in assumptions\<close> 
15803  221 

222 
lemma meta_mp: 

58612  223 
assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P" 
15803  224 
shows "PROP Q" 
58612  225 
by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>]) 
15803  226 

23432  227 
lemmas meta_impE = meta_mp [elim_format] 
228 

15803  229 
lemma meta_spec: 
58612  230 
assumes "\<And>x. PROP P x" 
26958  231 
shows "PROP P x" 
58612  232 
by (rule \<open>\<And>x. PROP P x\<close>) 
15803  233 

234 
lemmas meta_allE = meta_spec [elim_format] 

235 

26570  236 
lemma swap_params: 
58612  237 
"(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" .. 
26570  238 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

239 

58611  240 
subsection \<open>Metalevel conjunction\<close> 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

241 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

242 
lemma all_conjunction: 
58612  243 
"(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

244 
proof 
58612  245 
assume conj: "\<And>x. PROP A x &&& PROP B x" 
246 
show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)" 

19121  247 
proof  
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

248 
fix x 
26958  249 
from conj show "PROP A x" by (rule conjunctionD1) 
250 
from conj show "PROP B x" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

251 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

252 
next 
58612  253 
assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

254 
fix x 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

255 
show "PROP A x &&& PROP B x" 
19121  256 
proof  
26958  257 
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) 
258 
show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

259 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

260 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

261 

19121  262 
lemma imp_conjunction: 
58612  263 
"(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))" 
18836  264 
proof 
58612  265 
assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C" 
266 
show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)" 

19121  267 
proof  
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

268 
assume "PROP A" 
58611  269 
from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1) 
270 
from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

271 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

272 
next 
58612  273 
assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

274 
assume "PROP A" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

275 
show "PROP B &&& PROP C" 
19121  276 
proof  
58611  277 
from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1]) 
278 
from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2]) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

279 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

280 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

281 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

282 
lemma conjunction_imp: 
58612  283 
"(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

284 
proof 
58612  285 
assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C" 
22933  286 
assume ab: "PROP A" "PROP B" 
287 
show "PROP C" 

288 
proof (rule r) 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

289 
from ab show "PROP A &&& PROP B" . 
22933  290 
qed 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

291 
next 
58612  292 
assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

293 
assume conj: "PROP A &&& PROP B" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

294 
show "PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

295 
proof (rule r) 
19121  296 
from conj show "PROP A" by (rule conjunctionD1) 
297 
from conj show "PROP B" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

298 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

299 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

300 

48638  301 
end 