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