author | wenzelm |
Mon, 24 Jun 2013 23:33:14 +0200 | |
changeset 53576 | 4cf3f6153eb8 |
parent 53575 | 7b5a5116f3af |
child 53586 | 79e7fd57acc4 |
permissions | -rw-r--r-- |
wenzelm@49944 | 1 |
(* Title: Pure/Pure.thy |
wenzelm@49944 | 2 |
Author: Makarius |
wenzelm@49944 | 3 |
|
wenzelm@49944 | 4 |
Final stage of bootstrapping Pure, based on implicit background theory. |
wenzelm@49944 | 5 |
*) |
wenzelm@49944 | 6 |
|
wenzelm@49653 | 7 |
theory Pure |
wenzelm@49656 | 8 |
keywords |
wenzelm@49656 | 9 |
"!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "==" |
wenzelm@49656 | 10 |
"=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" |
wenzelm@53280 | 11 |
"\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes" |
wenzelm@49656 | 12 |
"attach" "begin" "binder" "constrains" "defines" "fixes" "for" |
wenzelm@49656 | 13 |
"identifier" "if" "imports" "in" "includes" "infix" "infixl" |
wenzelm@49656 | 14 |
"infixr" "is" "keywords" "notes" "obtains" "open" "output" |
wenzelm@52430 | 15 |
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" |
wenzelm@53576 | 16 |
and "theory" :: thy_begin |
wenzelm@53576 | 17 |
and "ML_file" :: thy_load |
wenzelm@49656 | 18 |
and "header" :: diag |
wenzelm@49656 | 19 |
and "chapter" :: thy_heading1 |
wenzelm@49656 | 20 |
and "section" :: thy_heading2 |
wenzelm@49656 | 21 |
and "subsection" :: thy_heading3 |
wenzelm@49656 | 22 |
and "subsubsection" :: thy_heading4 |
wenzelm@49656 | 23 |
and "text" "text_raw" :: thy_decl |
wenzelm@49656 | 24 |
and "sect" :: prf_heading2 % "proof" |
wenzelm@49656 | 25 |
and "subsect" :: prf_heading3 % "proof" |
wenzelm@49656 | 26 |
and "subsubsect" :: prf_heading4 % "proof" |
wenzelm@49656 | 27 |
and "txt" "txt_raw" :: prf_decl % "proof" |
wenzelm@49656 | 28 |
and "classes" "classrel" "default_sort" "typedecl" "type_synonym" |
wenzelm@49656 | 29 |
"nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax" |
wenzelm@52450 | 30 |
"translations" "no_translations" "defs" "definition" |
wenzelm@49656 | 31 |
"abbreviation" "type_notation" "no_type_notation" "notation" |
wenzelm@49656 | 32 |
"no_notation" "axiomatization" "theorems" "lemmas" "declare" |
wenzelm@49656 | 33 |
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl |
wenzelm@52432 | 34 |
and "ML" :: thy_decl % "ML" |
wenzelm@49656 | 35 |
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) |
wenzelm@49656 | 36 |
and "ML_val" "ML_command" :: diag % "ML" |
wenzelm@49656 | 37 |
and "setup" "local_setup" "attribute_setup" "method_setup" |
wenzelm@49656 | 38 |
"declaration" "syntax_declaration" "simproc_setup" |
wenzelm@49656 | 39 |
"parse_ast_translation" "parse_translation" "print_translation" |
wenzelm@49656 | 40 |
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" |
wenzelm@49656 | 41 |
and "bundle" :: thy_decl |
wenzelm@49656 | 42 |
and "include" "including" :: prf_decl |
wenzelm@49656 | 43 |
and "print_bundles" :: diag |
wenzelm@49656 | 44 |
and "context" "locale" :: thy_decl |
wenzelm@52361 | 45 |
and "sublocale" "interpretation" :: thy_goal |
wenzelm@52361 | 46 |
and "interpret" :: prf_goal % "proof" |
wenzelm@49656 | 47 |
and "class" :: thy_decl |
wenzelm@49656 | 48 |
and "subclass" :: thy_goal |
wenzelm@49656 | 49 |
and "instantiation" :: thy_decl |
wenzelm@49656 | 50 |
and "instance" :: thy_goal |
wenzelm@49656 | 51 |
and "overloading" :: thy_decl |
wenzelm@49656 | 52 |
and "code_datatype" :: thy_decl |
wenzelm@49656 | 53 |
and "theorem" "lemma" "corollary" :: thy_goal |
wenzelm@52411 | 54 |
and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal |
wenzelm@49656 | 55 |
and "notepad" :: thy_decl |
wenzelm@51143 | 56 |
and "have" :: prf_goal % "proof" |
wenzelm@51143 | 57 |
and "hence" :: prf_goal % "proof" == "then have" |
wenzelm@51143 | 58 |
and "show" :: prf_asm_goal % "proof" |
wenzelm@51143 | 59 |
and "thus" :: prf_asm_goal % "proof" == "then show" |
wenzelm@49656 | 60 |
and "then" "from" "with" :: prf_chain % "proof" |
wenzelm@49656 | 61 |
and "note" "using" "unfolding" :: prf_decl % "proof" |
wenzelm@49656 | 62 |
and "fix" "assume" "presume" "def" :: prf_asm % "proof" |
wenzelm@49656 | 63 |
and "obtain" "guess" :: prf_asm_goal % "proof" |
wenzelm@49656 | 64 |
and "let" "write" :: prf_decl % "proof" |
wenzelm@49656 | 65 |
and "case" :: prf_asm % "proof" |
wenzelm@49656 | 66 |
and "{" :: prf_open % "proof" |
wenzelm@49656 | 67 |
and "}" :: prf_close % "proof" |
wenzelm@49656 | 68 |
and "next" :: prf_block % "proof" |
wenzelm@49656 | 69 |
and "qed" :: qed_block % "proof" |
wenzelm@49656 | 70 |
and "by" ".." "." "done" "sorry" :: "qed" % "proof" |
wenzelm@49656 | 71 |
and "oops" :: qed_global % "proof" |
wenzelm@51143 | 72 |
and "defer" "prefer" "apply" :: prf_script % "proof" |
wenzelm@51143 | 73 |
and "apply_end" :: prf_script % "proof" == "" |
wenzelm@49656 | 74 |
and "proof" :: prf_block % "proof" |
wenzelm@49656 | 75 |
and "also" "moreover" :: prf_decl % "proof" |
wenzelm@49656 | 76 |
and "finally" "ultimately" :: prf_chain % "proof" |
wenzelm@49656 | 77 |
and "back" :: prf_script % "proof" |
wenzelm@49656 | 78 |
and "Isabelle.command" :: control |
wenzelm@53197 | 79 |
and "help" "print_commands" "print_options" |
wenzelm@52722 | 80 |
"print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules" |
wenzelm@49656 | 81 |
"print_theorems" "print_locales" "print_classes" "print_locale" |
wenzelm@49656 | 82 |
"print_interps" "print_dependencies" "print_attributes" |
wenzelm@49656 | 83 |
"print_simpset" "print_rules" "print_trans_rules" "print_methods" |
wenzelm@50584 | 84 |
"print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" |
wenzelm@49656 | 85 |
"print_binds" "print_facts" "print_cases" "print_statement" "thm" |
wenzelm@49656 | 86 |
"prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" |
wenzelm@49656 | 87 |
:: diag |
wenzelm@49656 | 88 |
and "cd" :: control |
wenzelm@49656 | 89 |
and "pwd" :: diag |
wenzelm@49656 | 90 |
and "use_thy" "remove_thy" "kill_thy" :: control |
wenzelm@53575 | 91 |
and "display_drafts" "print_drafts" "print_state" "pr" :: diag |
wenzelm@53575 | 92 |
and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control |
wenzelm@49661 | 93 |
and "welcome" :: diag |
wenzelm@49661 | 94 |
and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control |
wenzelm@49656 | 95 |
and "end" :: thy_end % "theory" |
wenzelm@49661 | 96 |
and "realizers" "realizability" "extract_type" "extract" :: thy_decl |
wenzelm@49661 | 97 |
and "find_theorems" "find_consts" :: diag |
wenzelm@53574 | 98 |
and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo" |
wenzelm@53574 | 99 |
"ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed" |
wenzelm@53574 | 100 |
"ProofGeneral.inform_file_retracted" :: control |
wenzelm@49653 | 101 |
begin |
wenzelm@15803 | 102 |
|
wenzelm@49906 | 103 |
ML_file "Isar/isar_syn.ML" |
wenzelm@49906 | 104 |
ML_file "Tools/find_theorems.ML" |
wenzelm@49906 | 105 |
ML_file "Tools/find_consts.ML" |
wenzelm@53146 | 106 |
ML_file "Tools/proof_general_pure.ML" |
wenzelm@49906 | 107 |
|
wenzelm@49906 | 108 |
|
wenzelm@26435 | 109 |
section {* Further content for the Pure theory *} |
wenzelm@20627 | 110 |
|
wenzelm@18466 | 111 |
subsection {* Meta-level connectives in assumptions *} |
wenzelm@15803 | 112 |
|
wenzelm@15803 | 113 |
lemma meta_mp: |
wenzelm@18019 | 114 |
assumes "PROP P ==> PROP Q" and "PROP P" |
wenzelm@15803 | 115 |
shows "PROP Q" |
wenzelm@18019 | 116 |
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
wenzelm@15803 | 117 |
|
nipkow@23432 | 118 |
lemmas meta_impE = meta_mp [elim_format] |
nipkow@23432 | 119 |
|
wenzelm@15803 | 120 |
lemma meta_spec: |
wenzelm@26958 | 121 |
assumes "!!x. PROP P x" |
wenzelm@26958 | 122 |
shows "PROP P x" |
wenzelm@26958 | 123 |
by (rule `!!x. PROP P x`) |
wenzelm@15803 | 124 |
|
wenzelm@15803 | 125 |
lemmas meta_allE = meta_spec [elim_format] |
wenzelm@15803 | 126 |
|
wenzelm@26570 | 127 |
lemma swap_params: |
wenzelm@26958 | 128 |
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
wenzelm@26570 | 129 |
|
wenzelm@18466 | 130 |
|
wenzelm@18466 | 131 |
subsection {* Meta-level conjunction *} |
wenzelm@18466 | 132 |
|
wenzelm@18466 | 133 |
lemma all_conjunction: |
wenzelm@28856 | 134 |
"(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))" |
wenzelm@18466 | 135 |
proof |
wenzelm@28856 | 136 |
assume conj: "!!x. PROP A x &&& PROP B x" |
wenzelm@28856 | 137 |
show "(!!x. PROP A x) &&& (!!x. PROP B x)" |
wenzelm@19121 | 138 |
proof - |
wenzelm@18466 | 139 |
fix x |
wenzelm@26958 | 140 |
from conj show "PROP A x" by (rule conjunctionD1) |
wenzelm@26958 | 141 |
from conj show "PROP B x" by (rule conjunctionD2) |
wenzelm@18466 | 142 |
qed |
wenzelm@18466 | 143 |
next |
wenzelm@28856 | 144 |
assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)" |
wenzelm@18466 | 145 |
fix x |
wenzelm@28856 | 146 |
show "PROP A x &&& PROP B x" |
wenzelm@19121 | 147 |
proof - |
wenzelm@26958 | 148 |
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
wenzelm@26958 | 149 |
show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) |
wenzelm@18466 | 150 |
qed |
wenzelm@18466 | 151 |
qed |
wenzelm@18466 | 152 |
|
wenzelm@19121 | 153 |
lemma imp_conjunction: |
nipkow@51618 | 154 |
"(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))" |
wenzelm@18836 | 155 |
proof |
wenzelm@28856 | 156 |
assume conj: "PROP A ==> PROP B &&& PROP C" |
wenzelm@28856 | 157 |
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
wenzelm@19121 | 158 |
proof - |
wenzelm@18466 | 159 |
assume "PROP A" |
wenzelm@19121 | 160 |
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
wenzelm@19121 | 161 |
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) |
wenzelm@18466 | 162 |
qed |
wenzelm@18466 | 163 |
next |
wenzelm@28856 | 164 |
assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
wenzelm@18466 | 165 |
assume "PROP A" |
wenzelm@28856 | 166 |
show "PROP B &&& PROP C" |
wenzelm@19121 | 167 |
proof - |
wenzelm@19121 | 168 |
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
wenzelm@19121 | 169 |
from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2]) |
wenzelm@18466 | 170 |
qed |
wenzelm@18466 | 171 |
qed |
wenzelm@18466 | 172 |
|
wenzelm@18466 | 173 |
lemma conjunction_imp: |
wenzelm@28856 | 174 |
"(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" |
wenzelm@18466 | 175 |
proof |
wenzelm@28856 | 176 |
assume r: "PROP A &&& PROP B ==> PROP C" |
wenzelm@22933 | 177 |
assume ab: "PROP A" "PROP B" |
wenzelm@22933 | 178 |
show "PROP C" |
wenzelm@22933 | 179 |
proof (rule r) |
wenzelm@28856 | 180 |
from ab show "PROP A &&& PROP B" . |
wenzelm@22933 | 181 |
qed |
wenzelm@18466 | 182 |
next |
wenzelm@18466 | 183 |
assume r: "PROP A ==> PROP B ==> PROP C" |
wenzelm@28856 | 184 |
assume conj: "PROP A &&& PROP B" |
wenzelm@18466 | 185 |
show "PROP C" |
wenzelm@18466 | 186 |
proof (rule r) |
wenzelm@19121 | 187 |
from conj show "PROP A" by (rule conjunctionD1) |
wenzelm@19121 | 188 |
from conj show "PROP B" by (rule conjunctionD2) |
wenzelm@18466 | 189 |
qed |
wenzelm@18466 | 190 |
qed |
wenzelm@18466 | 191 |
|
wenzelm@49653 | 192 |
end |
wenzelm@49653 | 193 |