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