author | wenzelm |
Tue, 22 Sep 2015 18:56:25 +0200 | |
changeset 61252 | c165f0472d57 |
parent 60957 | 574254152856 |
child 61337 | 4645502c3c64 |
permissions | -rw-r--r-- |
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 |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
9 |
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<equiv>" |
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" |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
12 |
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix" |
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" |
60623 | 14 |
"overloaded" "pervasive" "premises" "private" "qualified" "shows" |
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60448
diff
changeset
|
15 |
"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" |
|
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset
|
20 |
"consts" "syntax" "no_syntax" "translations" "no_translations" "defs" |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset
|
21 |
"definition" "abbreviation" "type_notation" "no_type_notation" "notation" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
22 |
"no_notation" "axiomatization" "theorems" "lemmas" "declare" |
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 non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset
|
38 |
and "sublocale" "interpretation" :: thy_goal |
c3e99efacb67
back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset
|
39 |
and "interpret" :: prf_goal % "proof" |
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 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
46 |
and "theorem" "lemma" "corollary" :: thy_goal |
51274
cfc83ad52571
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
wenzelm
parents:
51270
diff
changeset
|
47 |
and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: 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" |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
67 |
and "by" ".." "." "sorry" :: "qed" % "proof" |
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" |
60749 | 110 |
ML_file "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" |
48891 | 112 |
|
113 |
||
58611 | 114 |
section \<open>Basic attributes\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
115 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
116 |
attribute_setup tagged = |
58611 | 117 |
\<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
118 |
"tagged theorem" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
119 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
120 |
attribute_setup untagged = |
58611 | 121 |
\<open>Scan.lift Args.name >> Thm.untag\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
122 |
"untagged theorem" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
123 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
124 |
attribute_setup kind = |
58611 | 125 |
\<open>Scan.lift Args.name >> Thm.kind\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
126 |
"theorem kind" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
127 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
128 |
attribute_setup THEN = |
58611 | 129 |
\<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm |
130 |
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))\<close> |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
131 |
"resolution with rule" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
132 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
133 |
attribute_setup OF = |
58611 | 134 |
\<open>Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
135 |
"rule resolved with facts" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
136 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
137 |
attribute_setup rename_abs = |
58611 | 138 |
\<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => |
139 |
Thm.rule_attribute (K (Drule.rename_bvars' vs)))\<close> |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
140 |
"rename bound variables in abstractions" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
141 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
142 |
attribute_setup unfolded = |
58611 | 143 |
\<open>Attrib.thms >> (fn ths => |
144 |
Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close> |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
145 |
"unfolded definitions" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
146 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
147 |
attribute_setup folded = |
58611 | 148 |
\<open>Attrib.thms >> (fn ths => |
149 |
Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close> |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
150 |
"folded definitions" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
151 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
152 |
attribute_setup consumes = |
58611 | 153 |
\<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
154 |
"number of consumed facts" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
155 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
156 |
attribute_setup constraints = |
58611 | 157 |
\<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
158 |
"number of equality constraints" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
159 |
|
58611 | 160 |
attribute_setup case_names = |
161 |
\<open>Scan.lift (Scan.repeat1 (Args.name -- |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
162 |
Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) [])) |
58611 | 163 |
>> (fn cs => |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
164 |
Rule_Cases.cases_hyp_names |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
165 |
(map #1 cs) |
58611 | 166 |
(map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close> |
167 |
"named rule cases" |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
168 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
169 |
attribute_setup case_conclusion = |
58611 | 170 |
\<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
171 |
"named conclusion of rule cases" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
172 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
173 |
attribute_setup params = |
58611 | 174 |
\<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
175 |
"named rule parameters" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
176 |
|
58611 | 177 |
attribute_setup rule_format = |
178 |
\<open>Scan.lift (Args.mode "no_asm") |
|
179 |
>> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close> |
|
180 |
"result put into canonical rule format" |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
181 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
182 |
attribute_setup elim_format = |
58611 | 183 |
\<open>Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
184 |
"destruct rule turned into elimination rule format" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
185 |
|
58611 | 186 |
attribute_setup no_vars = |
187 |
\<open>Scan.succeed (Thm.rule_attribute (fn context => fn th => |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
188 |
let |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
189 |
val ctxt = Variable.set_body false (Context.proof_of context); |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
190 |
val ((_, [th']), _) = Variable.import true [th] ctxt; |
58611 | 191 |
in th' end))\<close> |
192 |
"imported schematic variables" |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
193 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
194 |
attribute_setup atomize = |
58611 | 195 |
\<open>Scan.succeed Object_Logic.declare_atomize\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
196 |
"declaration of atomize rule" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
197 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
198 |
attribute_setup rulify = |
58611 | 199 |
\<open>Scan.succeed Object_Logic.declare_rulify\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
200 |
"declaration of rulify rule" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
201 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
202 |
attribute_setup rotated = |
58611 | 203 |
\<open>Scan.lift (Scan.optional Parse.int 1 |
204 |
>> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))\<close> |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
205 |
"rotated theorem premises" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
206 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
207 |
attribute_setup defn = |
58611 | 208 |
\<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close> |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
209 |
"declaration of definitional transformations" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
210 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
211 |
attribute_setup abs_def = |
58611 | 212 |
\<open>Scan.succeed (Thm.rule_attribute (fn context => |
213 |
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close> |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
214 |
"abstract over free variables of definitional theorem" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
215 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
216 |
|
58611 | 217 |
section \<open>Further content for the Pure theory\<close> |
20627 | 218 |
|
58611 | 219 |
subsection \<open>Meta-level connectives in assumptions\<close> |
15803 | 220 |
|
221 |
lemma meta_mp: |
|
58612 | 222 |
assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P" |
15803 | 223 |
shows "PROP Q" |
58612 | 224 |
by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>]) |
15803 | 225 |
|
23432 | 226 |
lemmas meta_impE = meta_mp [elim_format] |
227 |
||
15803 | 228 |
lemma meta_spec: |
58612 | 229 |
assumes "\<And>x. PROP P x" |
26958 | 230 |
shows "PROP P x" |
58612 | 231 |
by (rule \<open>\<And>x. PROP P x\<close>) |
15803 | 232 |
|
233 |
lemmas meta_allE = meta_spec [elim_format] |
|
234 |
||
26570 | 235 |
lemma swap_params: |
58612 | 236 |
"(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" .. |
26570 | 237 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
238 |
|
58611 | 239 |
subsection \<open>Meta-level conjunction\<close> |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
240 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
241 |
lemma all_conjunction: |
58612 | 242 |
"(\<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
|
243 |
proof |
58612 | 244 |
assume conj: "\<And>x. PROP A x &&& PROP B x" |
245 |
show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)" |
|
19121 | 246 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
247 |
fix x |
26958 | 248 |
from conj show "PROP A x" by (rule conjunctionD1) |
249 |
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
|
250 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
251 |
next |
58612 | 252 |
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
|
253 |
fix x |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
254 |
show "PROP A x &&& PROP B x" |
19121 | 255 |
proof - |
26958 | 256 |
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
257 |
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
|
258 |
qed |
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 |
|
19121 | 261 |
lemma imp_conjunction: |
58612 | 262 |
"(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))" |
18836 | 263 |
proof |
58612 | 264 |
assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C" |
265 |
show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)" |
|
19121 | 266 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
267 |
assume "PROP A" |
58611 | 268 |
from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1) |
269 |
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
|
270 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
271 |
next |
58612 | 272 |
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
|
273 |
assume "PROP A" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
274 |
show "PROP B &&& PROP C" |
19121 | 275 |
proof - |
58611 | 276 |
from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1]) |
277 |
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
|
278 |
qed |
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 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
281 |
lemma conjunction_imp: |
58612 | 282 |
"(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
|
283 |
proof |
58612 | 284 |
assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C" |
22933 | 285 |
assume ab: "PROP A" "PROP B" |
286 |
show "PROP C" |
|
287 |
proof (rule r) |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
288 |
from ab show "PROP A &&& PROP B" . |
22933 | 289 |
qed |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
290 |
next |
58612 | 291 |
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
|
292 |
assume conj: "PROP A &&& PROP B" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
293 |
show "PROP C" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
294 |
proof (rule r) |
19121 | 295 |
from conj show "PROP A" by (rule conjunctionD1) |
296 |
from conj show "PROP B" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
297 |
qed |
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 |
|
48638 | 300 |
end |
301 |