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