author | wenzelm |
Sun, 16 Feb 2014 17:25:03 +0100 | |
changeset 55516 | d0157612ebe5 |
parent 55385 | 169e12bbf9a3 |
child 55762 | 27a45aec67a0 |
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 |
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" |
79e7fd57acc4
recover command tags from 4cf3f6153eb8 -- important for document preparation;
wenzelm
parents:
52439
diff
changeset
|
17 |
and "ML_file" :: thy_load % "ML" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
18 |
and "header" :: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
19 |
and "chapter" :: thy_heading1 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
20 |
and "section" :: thy_heading2 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
21 |
and "subsection" :: thy_heading3 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
22 |
and "subsubsection" :: thy_heading4 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
23 |
and "text" "text_raw" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
24 |
and "sect" :: prf_heading2 % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
25 |
and "subsect" :: prf_heading3 % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
26 |
and "subsubsect" :: prf_heading4 % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
27 |
and "txt" "txt_raw" :: prf_decl % "proof" |
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset
|
28 |
and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment" |
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 |
51295 | 33 |
and "ML" :: thy_decl % "ML" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
34 |
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
35 |
and "ML_val" "ML_command" :: diag % "ML" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
36 |
and "setup" "local_setup" "attribute_setup" "method_setup" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
37 |
"declaration" "syntax_declaration" "simproc_setup" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
38 |
"parse_ast_translation" "parse_translation" "print_translation" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
39 |
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
40 |
and "bundle" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
41 |
and "include" "including" :: prf_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
42 |
and "print_bundles" :: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
43 |
and "context" "locale" :: thy_decl |
51224
c3e99efacb67
back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset
|
44 |
and "sublocale" "interpretation" :: thy_goal |
c3e99efacb67
back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset
|
45 |
and "interpret" :: prf_goal % "proof" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
46 |
and "class" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
47 |
and "subclass" :: thy_goal |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
48 |
and "instantiation" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
49 |
and "instance" :: thy_goal |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
50 |
and "overloading" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
51 |
and "code_datatype" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
52 |
and "theorem" "lemma" "corollary" :: thy_goal |
51274
cfc83ad52571
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
wenzelm
parents:
51270
diff
changeset
|
53 |
and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
54 |
and "notepad" :: thy_decl |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset
|
55 |
and "have" :: prf_goal % "proof" |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset
|
56 |
and "hence" :: prf_goal % "proof" == "then have" |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset
|
57 |
and "show" :: prf_asm_goal % "proof" |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset
|
58 |
and "thus" :: prf_asm_goal % "proof" == "then show" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
59 |
and "then" "from" "with" :: prf_chain % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
60 |
and "note" "using" "unfolding" :: prf_decl % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
61 |
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
|
62 |
and "obtain" :: prf_asm_goal % "proof" |
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52549
diff
changeset
|
63 |
and "guess" :: prf_asm_goal_script % "proof" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
64 |
and "let" "write" :: prf_decl % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
65 |
and "case" :: prf_asm % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
66 |
and "{" :: prf_open % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
67 |
and "}" :: prf_close % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
68 |
and "next" :: prf_block % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
69 |
and "qed" :: qed_block % "proof" |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
70 |
and "by" ".." "." "sorry" :: "qed" % "proof" |
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
71 |
and "done" :: "qed_script" % "proof" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
72 |
and "oops" :: qed_global % "proof" |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset
|
73 |
and "defer" "prefer" "apply" :: prf_script % "proof" |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset
|
74 |
and "apply_end" :: prf_script % "proof" == "" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
75 |
and "proof" :: prf_block % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
76 |
and "also" "moreover" :: prf_decl % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
77 |
and "finally" "ultimately" :: prf_chain % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
78 |
and "back" :: prf_script % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
79 |
and "Isabelle.command" :: control |
52060 | 80 |
and "help" "print_commands" "print_options" |
51585 | 81 |
"print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
82 |
"print_theorems" "print_locales" "print_classes" "print_locale" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
83 |
"print_interps" "print_dependencies" "print_attributes" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
84 |
"print_simpset" "print_rules" "print_trans_rules" "print_methods" |
49569
7b6aaf446496
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
wenzelm
parents:
48929
diff
changeset
|
85 |
"print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
86 |
"print_binds" "print_facts" "print_cases" "print_statement" "thm" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
87 |
"prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
88 |
:: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
89 |
and "cd" :: control |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
90 |
and "pwd" :: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
91 |
and "use_thy" "remove_thy" "kill_thy" :: control |
52549 | 92 |
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
|
93 |
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
|
94 |
and "welcome" :: diag |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
95 |
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
|
96 |
and "end" :: thy_end % "theory" |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
97 |
and "realizers" "realizability" "extract_type" "extract" :: thy_decl |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
98 |
and "find_theorems" "find_consts" :: diag |
52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset
|
99 |
and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset
|
100 |
"ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset
|
101 |
"ProofGeneral.inform_file_retracted" :: control |
48638 | 102 |
begin |
15803 | 103 |
|
55516 | 104 |
ML_file "ML/ml_thms.ML" |
48891 | 105 |
ML_file "Isar/isar_syn.ML" |
55141 | 106 |
ML_file "Isar/calculation.ML" |
55030 | 107 |
ML_file "Tools/rail.ML" |
53707 | 108 |
ML_file "Tools/rule_insts.ML"; |
48891 | 109 |
ML_file "Tools/find_theorems.ML" |
110 |
ML_file "Tools/find_consts.ML" |
|
52009 | 111 |
ML_file "Tools/proof_general_pure.ML" |
54730 | 112 |
ML_file "Tools/simplifier_trace.ML" |
48891 | 113 |
|
114 |
||
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 |
section {* Basic attributes *} |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
116 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
117 |
attribute_setup tagged = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
118 |
"Scan.lift (Args.name -- Args.name) >> Thm.tag" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
119 |
"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
|
120 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
121 |
attribute_setup untagged = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
122 |
"Scan.lift Args.name >> Thm.untag" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
123 |
"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
|
124 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
125 |
attribute_setup kind = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
126 |
"Scan.lift Args.name >> Thm.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 |
"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
|
128 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
129 |
attribute_setup THEN = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
130 |
"Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
131 |
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
133 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
134 |
attribute_setup OF = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
135 |
"Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
137 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
138 |
attribute_setup rename_abs = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
139 |
"Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
140 |
Thm.rule_attribute (K (Drule.rename_bvars' vs)))" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
142 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
143 |
attribute_setup unfolded = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
144 |
"Attrib.thms >> (fn ths => |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
145 |
Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
146 |
"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
|
147 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
148 |
attribute_setup folded = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
149 |
"Attrib.thms >> (fn ths => |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
150 |
Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
151 |
"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
|
152 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
153 |
attribute_setup consumes = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
154 |
"Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
156 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
157 |
attribute_setup constraints = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
158 |
"Scan.lift Parse.nat >> Rule_Cases.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 |
"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
|
160 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
161 |
attribute_setup case_names = {* |
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.lift (Scan.repeat1 (Args.name -- |
7eb0c04e4c40
define basic attributes in user-space 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 "]"}) [])) |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
164 |
>> (fn cs => |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
166 |
(map #1 cs) |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
167 |
(map (map (the_default Rule_Cases.case_hypsN) o #2) cs)) |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
168 |
*} "named 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
|
169 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
170 |
attribute_setup case_conclusion = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
171 |
"Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
173 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
174 |
attribute_setup params = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
175 |
"Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
177 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
178 |
attribute_setup 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
|
179 |
Scan.lift (Args.mode "no_asm") |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
180 |
>> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.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
|
181 |
*} "result put into canonical 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
|
182 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
183 |
attribute_setup elim_format = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
184 |
"Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))" |
7eb0c04e4c40
define basic attributes in user-space 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 user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
186 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
187 |
attribute_setup no_vars = {* |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
188 |
Scan.succeed (Thm.rule_attribute (fn context => fn th => |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
189 |
let |
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 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
|
191 |
val ((_, [th']), _) = Variable.import true [th] ctxt; |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
192 |
in th' end)) |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
193 |
*} "imported schematic variables" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
194 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
195 |
attribute_setup eta_long = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
196 |
"Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
197 |
"put theorem into eta long beta normal form" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
198 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
199 |
attribute_setup atomize = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
200 |
"Scan.succeed Object_Logic.declare_atomize" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
201 |
"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
|
202 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
203 |
attribute_setup rulify = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
204 |
"Scan.succeed Object_Logic.declare_rulify" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
205 |
"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
|
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 rotated = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
208 |
"Scan.lift (Scan.optional Parse.int 1 |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
209 |
>> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
210 |
"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
|
211 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
212 |
attribute_setup defn = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
213 |
"Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
214 |
"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
|
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 |
attribute_setup abs_def = |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
217 |
"Scan.succeed (Thm.rule_attribute (fn context => |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
218 |
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))" |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
219 |
"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
|
220 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset
|
221 |
|
26435 | 222 |
section {* Further content for the Pure theory *} |
20627 | 223 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
224 |
subsection {* Meta-level connectives in assumptions *} |
15803 | 225 |
|
226 |
lemma meta_mp: |
|
18019 | 227 |
assumes "PROP P ==> PROP Q" and "PROP P" |
15803 | 228 |
shows "PROP Q" |
18019 | 229 |
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
15803 | 230 |
|
23432 | 231 |
lemmas meta_impE = meta_mp [elim_format] |
232 |
||
15803 | 233 |
lemma meta_spec: |
26958 | 234 |
assumes "!!x. PROP P x" |
235 |
shows "PROP P x" |
|
236 |
by (rule `!!x. PROP P x`) |
|
15803 | 237 |
|
238 |
lemmas meta_allE = meta_spec [elim_format] |
|
239 |
||
26570 | 240 |
lemma swap_params: |
26958 | 241 |
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
26570 | 242 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
243 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
244 |
subsection {* Meta-level conjunction *} |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
245 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
246 |
lemma all_conjunction: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
247 |
"(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
248 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
249 |
assume conj: "!!x. PROP A x &&& PROP B x" |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
250 |
show "(!!x. PROP A x) &&& (!!x. PROP B x)" |
19121 | 251 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
252 |
fix x |
26958 | 253 |
from conj show "PROP A x" by (rule conjunctionD1) |
254 |
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
|
255 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
256 |
next |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
257 |
assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
258 |
fix x |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
259 |
show "PROP A x &&& PROP B x" |
19121 | 260 |
proof - |
26958 | 261 |
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
262 |
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
|
263 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
264 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
265 |
|
19121 | 266 |
lemma imp_conjunction: |
50603 | 267 |
"(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))" |
18836 | 268 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
269 |
assume conj: "PROP A ==> PROP B &&& PROP C" |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
270 |
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
19121 | 271 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
272 |
assume "PROP A" |
19121 | 273 |
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
274 |
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
275 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
276 |
next |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
277 |
assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
278 |
assume "PROP A" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
279 |
show "PROP B &&& PROP C" |
19121 | 280 |
proof - |
281 |
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
|
282 |
from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2]) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
283 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
284 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
285 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
286 |
lemma conjunction_imp: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
287 |
"(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
288 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
289 |
assume r: "PROP A &&& PROP B ==> PROP C" |
22933 | 290 |
assume ab: "PROP A" "PROP B" |
291 |
show "PROP C" |
|
292 |
proof (rule r) |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
293 |
from ab show "PROP A &&& PROP B" . |
22933 | 294 |
qed |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
295 |
next |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
296 |
assume r: "PROP A ==> PROP B ==> PROP C" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
297 |
assume conj: "PROP A &&& PROP B" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
298 |
show "PROP C" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
299 |
proof (rule r) |
19121 | 300 |
from conj show "PROP A" by (rule conjunctionD1) |
301 |
from conj show "PROP B" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
302 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
303 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
304 |
|
48638 | 305 |
end |
306 |