src/Pure/Pure.thy
author wenzelm
Fri May 17 20:53:28 2013 +0200 (2013-05-17)
changeset 52060 179236c82c2a
parent 52009 3b18ef9df768
child 52143 36ffe23b25f8
permissions -rw-r--r--
renamed 'print_configs' to 'print_options';
     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_options"
    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 ML_file "Tools/proof_general_pure.ML"
   102 
   103 
   104 section {* Further content for the Pure theory *}
   105 
   106 subsection {* Meta-level connectives in assumptions *}
   107 
   108 lemma meta_mp:
   109   assumes "PROP P ==> PROP Q" and "PROP P"
   110   shows "PROP Q"
   111     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
   112 
   113 lemmas meta_impE = meta_mp [elim_format]
   114 
   115 lemma meta_spec:
   116   assumes "!!x. PROP P x"
   117   shows "PROP P x"
   118     by (rule `!!x. PROP P x`)
   119 
   120 lemmas meta_allE = meta_spec [elim_format]
   121 
   122 lemma swap_params:
   123   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
   124 
   125 
   126 subsection {* Meta-level conjunction *}
   127 
   128 lemma all_conjunction:
   129   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
   130 proof
   131   assume conj: "!!x. PROP A x &&& PROP B x"
   132   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
   133   proof -
   134     fix x
   135     from conj show "PROP A x" by (rule conjunctionD1)
   136     from conj show "PROP B x" by (rule conjunctionD2)
   137   qed
   138 next
   139   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
   140   fix x
   141   show "PROP A x &&& PROP B x"
   142   proof -
   143     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   144     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   145   qed
   146 qed
   147 
   148 lemma imp_conjunction:
   149   "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
   150 proof
   151   assume conj: "PROP A ==> PROP B &&& PROP C"
   152   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   153   proof -
   154     assume "PROP A"
   155     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
   156     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   157   qed
   158 next
   159   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   160   assume "PROP A"
   161   show "PROP B &&& PROP C"
   162   proof -
   163     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
   164     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   165   qed
   166 qed
   167 
   168 lemma conjunction_imp:
   169   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   170 proof
   171   assume r: "PROP A &&& PROP B ==> PROP C"
   172   assume ab: "PROP A" "PROP B"
   173   show "PROP C"
   174   proof (rule r)
   175     from ab show "PROP A &&& PROP B" .
   176   qed
   177 next
   178   assume r: "PROP A ==> PROP B ==> PROP C"
   179   assume conj: "PROP A &&& PROP B"
   180   show "PROP C"
   181   proof (rule r)
   182     from conj show "PROP A" by (rule conjunctionD1)
   183     from conj show "PROP B" by (rule conjunctionD2)
   184   qed
   185 qed
   186 
   187 end
   188