author  wenzelm 
Tue, 28 Oct 2014 11:42:51 +0100  
changeset 58800  bfed1c26caed 
parent 58660  8d4aebb9e327 
child 58842  22b87ab47d3b 
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 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

9 
"!!" "!" "%" "(" ")" "+" "," "" ":" "::" ";" "<" "<=" "=" "==" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

10 
"=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" 
52143  11 
"\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

12 
"attach" "begin" "binder" "constrains" "defines" "fixes" "for" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

13 
"identifier" "if" "imports" "in" "includes" "infix" "infixl" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

14 
"infixr" "is" "keywords" "notes" "obtains" "open" "output" 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51274
diff
changeset

15 
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "" 
52449
79e7fd57acc4
recover command tags from 4cf3f6153eb8  important for document preparation;
wenzelm
parents:
52439
diff
changeset

16 
and "theory" :: thy_begin % "theory" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

17 
and "header" :: diag 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

18 
and "chapter" :: thy_heading1 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

19 
and "section" :: thy_heading2 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

20 
and "subsection" :: thy_heading3 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

21 
and "subsubsection" :: thy_heading4 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

22 
and "text" "text_raw" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

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

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

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

26 
and "txt" "txt_raw" :: prf_decl % "proof" 
57506  27 
and "default_sort" :: thy_decl == "" 
28 
and "typedecl" "type_synonym" "nonterminal" "judgment" 

55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset

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

30 
"definition" "abbreviation" "type_notation" "no_type_notation" "notation" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

31 
"no_notation" "axiomatization" "theorems" "lemmas" "declare" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

32 
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset

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

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

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

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

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

39 
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

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

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

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

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

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

45 
and "print_bundles" :: diag 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

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

47 
and "sublocale" "interpretation" :: thy_goal 
c3e99efacb67
back to nonschematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset

48 
and "interpret" :: prf_goal % "proof" 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

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

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

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

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

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

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

55 
and "theorem" "lemma" "corollary" :: thy_goal 
51274
cfc83ad52571
discontinued pointless command category "thy_schematic_goal"  this is checked dynamically;
wenzelm
parents:
51270
diff
changeset

56 
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

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

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

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

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

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

62 
and "then" "from" "with" :: prf_chain % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

63 
and "note" "using" "unfolding" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

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

65 
and "obtain" :: prf_asm_goal % "proof" 
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52549
diff
changeset

66 
and "guess" :: prf_asm_goal_script % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

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

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

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

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

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

72 
and "qed" :: qed_block % "proof" 
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset

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

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

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

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

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

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

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

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

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

82 
and "Isabelle.command" :: control 
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

83 
and "help" "print_commands" "print_options" "print_context" 
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

84 
"print_theory" "print_syntax" "print_abbrevs" "print_defn_rules" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

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

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

87 
"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

88 
"print_antiquotations" "print_ML_antiquotations" "thy_deps" 
57415
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56864
diff
changeset

89 
"locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings" 
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56864
diff
changeset

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

91 
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

92 
and "use_thy" "remove_thy" "kill_thy" :: control 
52549  93 
and "display_drafts" "print_state" "pr" :: diag 
52438
7b5a5116f3af
back to keyword 'pr' :: diag as required for ProofGeneral command line  reject this TTY command in Isabelle/jEdit by other means;
wenzelm
parents:
52437
diff
changeset

94 
and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control 
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

95 
and "welcome" :: diag 
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

96 
and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

97 
and "end" :: thy_end % "theory" 
56797  98 
and "realizers" :: thy_decl == "" 
99 
and "realizability" :: thy_decl == "" 

100 
and "extract_type" "extract" :: thy_decl 

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

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

102 
and "named_theorems" :: thy_decl 
52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset

103 
and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset

104 
"ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset

105 
"ProofGeneral.inform_file_retracted" :: control 
48638  106 
begin 
15803  107 

56205  108 
ML_file "ML/ml_antiquotations.ML" 
55516  109 
ML_file "ML/ml_thms.ML" 
56864  110 
ML_file "Tools/print_operation.ML" 
48891  111 
ML_file "Isar/isar_syn.ML" 
55141  112 
ML_file "Isar/calculation.ML" 
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58201
diff
changeset

113 
ML_file "Tools/bibtex.ML" 
55030  114 
ML_file "Tools/rail.ML" 
53707  115 
ML_file "Tools/rule_insts.ML"; 
57934
5e500c0e7eca
tuned signature  prefer selfcontained userspace tool;
wenzelm
parents:
57886
diff
changeset

116 
ML_file "Tools/thm_deps.ML"; 
58201  117 
ML_file "Tools/class_deps.ML" 
48891  118 
ML_file "Tools/find_theorems.ML" 
119 
ML_file "Tools/find_consts.ML" 

52009  120 
ML_file "Tools/proof_general_pure.ML" 
54730  121 
ML_file "Tools/simplifier_trace.ML" 
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
57506
diff
changeset

122 
ML_file "Tools/named_theorems.ML" 
48891  123 

124 

58611  125 
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

126 

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

127 
attribute_setup tagged = 
58611  128 
\<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

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

130 

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

131 
attribute_setup untagged = 
58611  132 
\<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

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

134 

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

135 
attribute_setup kind = 
58611  136 
\<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

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

138 

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

139 
attribute_setup THEN = 
58611  140 
\<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1)  Attrib.thm 
141 
>> (fn (i, B) => Thm.rule_attribute (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

142 
"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

143 

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

144 
attribute_setup OF = 
58611  145 
\<open>Attrib.thms >> (fn Bs => Thm.rule_attribute (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

146 
"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

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 rename_abs = 
58611  149 
\<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => 
150 
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

151 
"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

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 unfolded = 
58611  154 
\<open>Attrib.thms >> (fn ths => 
155 
Thm.rule_attribute (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

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

157 

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

158 
attribute_setup folded = 
58611  159 
\<open>Attrib.thms >> (fn ths => 
160 
Thm.rule_attribute (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

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

162 

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

163 
attribute_setup consumes = 
58611  164 
\<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

165 
"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

166 

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

167 
attribute_setup constraints = 
58611  168 
\<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

169 
"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

170 

58611  171 
attribute_setup case_names = 
172 
\<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

173 
Scan.optional (@{keyword "["}  Scan.repeat1 (Args.maybe Args.name)  @{keyword "]"}) [])) 
58611  174 
>> (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

175 
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

176 
(map #1 cs) 
58611  177 
(map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close> 
178 
"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

179 

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

180 
attribute_setup case_conclusion = 
58611  181 
\<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

182 
"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

183 

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

184 
attribute_setup params = 
58611  185 
\<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

186 
"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

187 

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

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

191 
"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

192 

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

193 
attribute_setup elim_format = 
58611  194 
\<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

195 
"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

196 

58611  197 
attribute_setup no_vars = 
198 
\<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

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

200 
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

201 
val ((_, [th']), _) = Variable.import true [th] ctxt; 
58611  202 
in th' end))\<close> 
203 
"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

204 

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

205 
attribute_setup eta_long = 
58611  206 
\<open>Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))\<close> 
55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

207 
"put theorem into eta long beta normal form" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

208 

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

209 
attribute_setup atomize = 
58611  210 
\<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

211 
"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

212 

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

213 
attribute_setup rulify = 
58611  214 
\<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

215 
"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

216 

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

217 
attribute_setup rotated = 
58611  218 
\<open>Scan.lift (Scan.optional Parse.int 1 
219 
>> (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

220 
"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

221 

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

222 
attribute_setup defn = 
58611  223 
\<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

224 
"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

225 

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

226 
attribute_setup abs_def = 
58611  227 
\<open>Scan.succeed (Thm.rule_attribute (fn context => 
228 
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

229 
"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

230 

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

231 

58611  232 
section \<open>Further content for the Pure theory\<close> 
20627  233 

58611  234 
subsection \<open>Metalevel connectives in assumptions\<close> 
15803  235 

236 
lemma meta_mp: 

58612  237 
assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P" 
15803  238 
shows "PROP Q" 
58612  239 
by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>]) 
15803  240 

23432  241 
lemmas meta_impE = meta_mp [elim_format] 
242 

15803  243 
lemma meta_spec: 
58612  244 
assumes "\<And>x. PROP P x" 
26958  245 
shows "PROP P x" 
58612  246 
by (rule \<open>\<And>x. PROP P x\<close>) 
15803  247 

248 
lemmas meta_allE = meta_spec [elim_format] 

249 

26570  250 
lemma swap_params: 
58612  251 
"(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" .. 
26570  252 

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

253 

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

255 

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

256 
lemma all_conjunction: 
58612  257 
"(\<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

258 
proof 
58612  259 
assume conj: "\<And>x. PROP A x &&& PROP B x" 
260 
show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)" 

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

262 
fix x 
26958  263 
from conj show "PROP A x" by (rule conjunctionD1) 
264 
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

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

266 
next 
58612  267 
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

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

269 
show "PROP A x &&& PROP B x" 
19121  270 
proof  
26958  271 
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) 
272 
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

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

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

275 

19121  276 
lemma imp_conjunction: 
58612  277 
"(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))" 
18836  278 
proof 
58612  279 
assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C" 
280 
show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)" 

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

282 
assume "PROP A" 
58611  283 
from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1) 
284 
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

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

286 
next 
58612  287 
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

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

289 
show "PROP B &&& PROP C" 
19121  290 
proof  
58611  291 
from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1]) 
292 
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

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

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

295 

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

296 
lemma conjunction_imp: 
58612  297 
"(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

298 
proof 
58612  299 
assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C" 
22933  300 
assume ab: "PROP A" "PROP B" 
301 
show "PROP C" 

302 
proof (rule r) 

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

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

305 
next 
58612  306 
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

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

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

309 
proof (rule r) 
19121  310 
from conj show "PROP A" by (rule conjunctionD1) 
311 
from conj show "PROP B" by (rule conjunctionD2) 

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

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

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

314 

48638  315 
end 
316 