author | nipkow |
Fri, 21 Sep 2012 03:41:10 +0200 | |
changeset 49487 | 7e7ac4956117 |
parent 48929 | 05d4e5f660ae |
child 49569 | 7b6aaf446496 |
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>" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
11 |
"\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes" |
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" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
15 |
"overloaded" "pervasive" "shows" "structure" "unchecked" "uses" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
16 |
"where" "|" |
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" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
27 |
and "classes" "classrel" "default_sort" "typedecl" "type_synonym" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
28 |
"nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
29 |
"translations" "no_translations" "axioms" "defs" "definition" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
30 |
"abbreviation" "type_notation" "no_type_notation" "notation" |
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 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
33 |
and "use" "ML" :: thy_decl % "ML" |
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 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
44 |
and "sublocale" "interpretation" :: thy_schematic_goal |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
45 |
and "interpret" :: prf_goal % "proof" (* FIXME schematic? *) |
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 |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
53 |
and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
54 |
and "notepad" :: thy_decl |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
55 |
and "have" "hence" :: prf_goal % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
56 |
and "show" "thus" :: prf_asm_goal % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
57 |
and "then" "from" "with" :: prf_chain % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
58 |
and "note" "using" "unfolding" :: prf_decl % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
59 |
and "fix" "assume" "presume" "def" :: prf_asm % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
60 |
and "obtain" "guess" :: prf_asm_goal % "proof" |
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" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
65 |
and "next" :: prf_block % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
66 |
and "qed" :: qed_block % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
67 |
and "by" ".." "." "done" "sorry" :: "qed" % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
68 |
and "oops" :: qed_global % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
69 |
and "defer" "prefer" "apply" "apply_end" :: prf_script % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
70 |
and "proof" :: prf_block % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
71 |
and "also" "moreover" :: prf_decl % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
72 |
and "finally" "ultimately" :: prf_chain % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
73 |
and "back" :: prf_script % "proof" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
74 |
and "Isabelle.command" :: control |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
75 |
and "pretty_setmargin" "help" "print_commands" "print_configs" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
76 |
"print_context" "print_theory" "print_syntax" "print_abbrevs" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
77 |
"print_theorems" "print_locales" "print_classes" "print_locale" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
78 |
"print_interps" "print_dependencies" "print_attributes" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
79 |
"print_simpset" "print_rules" "print_trans_rules" "print_methods" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
80 |
"print_antiquotations" "thy_deps" "class_deps" "thm_deps" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
81 |
"print_binds" "print_facts" "print_cases" "print_statement" "thm" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
82 |
"prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
83 |
:: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
84 |
and "cd" :: control |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
85 |
and "pwd" :: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
86 |
and "use_thy" "remove_thy" "kill_thy" :: control |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
87 |
and "display_drafts" "print_drafts" "pr" :: diag |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
88 |
and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
89 |
and "welcome" :: diag |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
90 |
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
|
91 |
and "end" :: thy_end % "theory" |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
92 |
and "realizers" "realizability" "extract_type" "extract" :: thy_decl |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
93 |
and "find_theorems" "find_consts" :: diag |
48638 | 94 |
begin |
15803 | 95 |
|
48891 | 96 |
ML_file "Isar/isar_syn.ML" |
97 |
ML_file "Tools/find_theorems.ML" |
|
98 |
ML_file "Tools/find_consts.ML" |
|
99 |
||
100 |
||
26435 | 101 |
section {* Further content for the Pure theory *} |
20627 | 102 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
103 |
subsection {* Meta-level connectives in assumptions *} |
15803 | 104 |
|
105 |
lemma meta_mp: |
|
18019 | 106 |
assumes "PROP P ==> PROP Q" and "PROP P" |
15803 | 107 |
shows "PROP Q" |
18019 | 108 |
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
15803 | 109 |
|
23432 | 110 |
lemmas meta_impE = meta_mp [elim_format] |
111 |
||
15803 | 112 |
lemma meta_spec: |
26958 | 113 |
assumes "!!x. PROP P x" |
114 |
shows "PROP P x" |
|
115 |
by (rule `!!x. PROP P x`) |
|
15803 | 116 |
|
117 |
lemmas meta_allE = meta_spec [elim_format] |
|
118 |
||
26570 | 119 |
lemma swap_params: |
26958 | 120 |
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
26570 | 121 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
122 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
123 |
subsection {* Meta-level conjunction *} |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
124 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
125 |
lemma all_conjunction: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
126 |
"(!!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
|
127 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
128 |
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
|
129 |
show "(!!x. PROP A x) &&& (!!x. PROP B x)" |
19121 | 130 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
131 |
fix x |
26958 | 132 |
from conj show "PROP A x" by (rule conjunctionD1) |
133 |
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
|
134 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
135 |
next |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
136 |
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
|
137 |
fix x |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
138 |
show "PROP A x &&& PROP B x" |
19121 | 139 |
proof - |
26958 | 140 |
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
141 |
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
|
142 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
143 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
144 |
|
19121 | 145 |
lemma imp_conjunction: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
146 |
"(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
18836 | 147 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
148 |
assume conj: "PROP A ==> PROP B &&& PROP C" |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
149 |
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
19121 | 150 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
151 |
assume "PROP A" |
19121 | 152 |
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
153 |
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
|
154 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
155 |
next |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
156 |
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
|
157 |
assume "PROP A" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
158 |
show "PROP B &&& PROP C" |
19121 | 159 |
proof - |
160 |
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
|
161 |
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
|
162 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
163 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
164 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
165 |
lemma conjunction_imp: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
166 |
"(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
|
167 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
168 |
assume r: "PROP A &&& PROP B ==> PROP C" |
22933 | 169 |
assume ab: "PROP A" "PROP B" |
170 |
show "PROP C" |
|
171 |
proof (rule r) |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
172 |
from ab show "PROP A &&& PROP B" . |
22933 | 173 |
qed |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
174 |
next |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
175 |
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
|
176 |
assume conj: "PROP A &&& PROP B" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
177 |
show "PROP C" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
178 |
proof (rule r) |
19121 | 179 |
from conj show "PROP A" by (rule conjunctionD1) |
180 |
from conj show "PROP B" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
181 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
182 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
183 |
|
48638 | 184 |
end |
185 |