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