src/Pure/Pure.thy
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50128 599c935aac82
child 50603 3e3c2af5e8a5
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     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" :: prf_goal % "proof"
    56   and "hence" :: prf_goal % "proof" == "then have"
    57   and "show" :: prf_asm_goal % "proof"
    58   and "thus" :: prf_asm_goal % "proof" == "then show"
    59   and "then" "from" "with" :: prf_chain % "proof"
    60   and "note" "using" "unfolding" :: prf_decl % "proof"
    61   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    62   and "obtain" "guess" :: prf_asm_goal % "proof"
    63   and "let" "write" :: prf_decl % "proof"
    64   and "case" :: prf_asm % "proof"
    65   and "{" :: prf_open % "proof"
    66   and "}" :: prf_close % "proof"
    67   and "next" :: prf_block % "proof"
    68   and "qed" :: qed_block % "proof"
    69   and "by" ".." "." "done" "sorry" :: "qed" % "proof"
    70   and "oops" :: qed_global % "proof"
    71   and "defer" "prefer" "apply" :: prf_script % "proof"
    72   and "apply_end" :: prf_script % "proof" == ""
    73   and "proof" :: prf_block % "proof"
    74   and "also" "moreover" :: prf_decl % "proof"
    75   and "finally" "ultimately" :: prf_chain % "proof"
    76   and "back" :: prf_script % "proof"
    77   and "Isabelle.command" :: control
    78   and "pretty_setmargin" "help" "print_commands" "print_configs"
    79     "print_context" "print_theory" "print_syntax" "print_abbrevs"
    80     "print_theorems" "print_locales" "print_classes" "print_locale"
    81     "print_interps" "print_dependencies" "print_attributes"
    82     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
    83     "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
    84     "print_binds" "print_facts" "print_cases" "print_statement" "thm"
    85     "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
    86     :: diag
    87   and "cd" :: control
    88   and "pwd" :: diag
    89   and "use_thy" "remove_thy" "kill_thy" :: control
    90   and "display_drafts" "print_drafts" "pr" :: diag
    91   and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    92   and "welcome" :: diag
    93   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
    94   and "end" :: thy_end % "theory"
    95   and "realizers" "realizability" "extract_type" "extract" :: thy_decl
    96   and "find_theorems" "find_consts" :: diag
    97 begin
    98 
    99 ML_file "Isar/isar_syn.ML"
   100 ML_file "Tools/find_theorems.ML"
   101 ML_file "Tools/find_consts.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