src/Pure/Pure.thy
author haftmann
Sun Sep 07 17:51:28 2014 +0200 (2014-09-07)
changeset 58201 5bf56c758e02
parent 57934 5e500c0e7eca
child 58544 340f130b3d38
permissions -rw-r--r--
separated class_deps command into separate file
wenzelm@48929
     1
(*  Title:      Pure/Pure.thy
wenzelm@48929
     2
    Author:     Makarius
wenzelm@48929
     3
wenzelm@48929
     4
Final stage of bootstrapping Pure, based on implicit background theory.
wenzelm@48929
     5
*)
wenzelm@48929
     6
wenzelm@48638
     7
theory Pure
wenzelm@48641
     8
  keywords
wenzelm@48641
     9
    "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
wenzelm@48641
    10
    "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
wenzelm@52143
    11
    "\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes"
wenzelm@48641
    12
    "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
wenzelm@48641
    13
    "identifier" "if" "imports" "in" "includes" "infix" "infixl"
wenzelm@48641
    14
    "infixr" "is" "keywords" "notes" "obtains" "open" "output"
wenzelm@51293
    15
    "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
wenzelm@52449
    16
  and "theory" :: thy_begin % "theory"
wenzelm@48641
    17
  and "header" :: diag
wenzelm@48641
    18
  and "chapter" :: thy_heading1
wenzelm@48641
    19
  and "section" :: thy_heading2
wenzelm@48641
    20
  and "subsection" :: thy_heading3
wenzelm@48641
    21
  and "subsubsection" :: thy_heading4
wenzelm@48641
    22
  and "text" "text_raw" :: thy_decl
wenzelm@48641
    23
  and "sect" :: prf_heading2 % "proof"
wenzelm@48641
    24
  and "subsect" :: prf_heading3 % "proof"
wenzelm@48641
    25
  and "subsubsect" :: prf_heading4 % "proof"
wenzelm@48641
    26
  and "txt" "txt_raw" :: prf_decl % "proof"
wenzelm@57506
    27
  and "default_sort" :: thy_decl == ""
wenzelm@57506
    28
  and "typedecl" "type_synonym" "nonterminal" "judgment"
wenzelm@55385
    29
    "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
wenzelm@55385
    30
    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
wenzelm@48641
    31
    "no_notation" "axiomatization" "theorems" "lemmas" "declare"
wenzelm@48641
    32
    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
wenzelm@56618
    33
  and "SML_file" "ML_file" :: thy_load % "ML"
wenzelm@56618
    34
  and "SML_import" "SML_export" :: thy_decl % "ML"
wenzelm@51295
    35
  and "ML" :: thy_decl % "ML"
wenzelm@48641
    36
  and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
wenzelm@48641
    37
  and "ML_val" "ML_command" :: diag % "ML"
wenzelm@55762
    38
  and "simproc_setup" :: thy_decl % "ML" == ""
wenzelm@48641
    39
  and "setup" "local_setup" "attribute_setup" "method_setup"
wenzelm@55762
    40
    "declaration" "syntax_declaration"
wenzelm@48641
    41
    "parse_ast_translation" "parse_translation" "print_translation"
wenzelm@48641
    42
    "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
wenzelm@48641
    43
  and "bundle" :: thy_decl
wenzelm@48641
    44
  and "include" "including" :: prf_decl
wenzelm@48641
    45
  and "print_bundles" :: diag
wenzelm@48641
    46
  and "context" "locale" :: thy_decl
wenzelm@51224
    47
  and "sublocale" "interpretation" :: thy_goal
wenzelm@51224
    48
  and "interpret" :: prf_goal % "proof"
wenzelm@48641
    49
  and "class" :: thy_decl
wenzelm@48641
    50
  and "subclass" :: thy_goal
wenzelm@48641
    51
  and "instantiation" :: thy_decl
wenzelm@48641
    52
  and "instance" :: thy_goal
wenzelm@48641
    53
  and "overloading" :: thy_decl
wenzelm@48641
    54
  and "code_datatype" :: thy_decl
wenzelm@48641
    55
  and "theorem" "lemma" "corollary" :: thy_goal
wenzelm@51274
    56
  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
wenzelm@48641
    57
  and "notepad" :: thy_decl
wenzelm@50128
    58
  and "have" :: prf_goal % "proof"
wenzelm@50128
    59
  and "hence" :: prf_goal % "proof" == "then have"
wenzelm@50128
    60
  and "show" :: prf_asm_goal % "proof"
wenzelm@50128
    61
  and "thus" :: prf_asm_goal % "proof" == "then show"
wenzelm@48641
    62
  and "then" "from" "with" :: prf_chain % "proof"
wenzelm@48641
    63
  and "note" "using" "unfolding" :: prf_decl % "proof"
wenzelm@48641
    64
  and "fix" "assume" "presume" "def" :: prf_asm % "proof"
wenzelm@53371
    65
  and "obtain" :: prf_asm_goal % "proof"
wenzelm@53371
    66
  and "guess" :: prf_asm_goal_script % "proof"
wenzelm@48641
    67
  and "let" "write" :: prf_decl % "proof"
wenzelm@48641
    68
  and "case" :: prf_asm % "proof"
wenzelm@48641
    69
  and "{" :: prf_open % "proof"
wenzelm@48641
    70
  and "}" :: prf_close % "proof"
wenzelm@48641
    71
  and "next" :: prf_block % "proof"
wenzelm@48641
    72
  and "qed" :: qed_block % "proof"
wenzelm@53571
    73
  and "by" ".." "." "sorry" :: "qed" % "proof"
wenzelm@53571
    74
  and "done" :: "qed_script" % "proof"
wenzelm@48641
    75
  and "oops" :: qed_global % "proof"
wenzelm@50128
    76
  and "defer" "prefer" "apply" :: prf_script % "proof"
wenzelm@50128
    77
  and "apply_end" :: prf_script % "proof" == ""
wenzelm@48641
    78
  and "proof" :: prf_block % "proof"
wenzelm@48641
    79
  and "also" "moreover" :: prf_decl % "proof"
wenzelm@48641
    80
  and "finally" "ultimately" :: prf_chain % "proof"
wenzelm@48641
    81
  and "back" :: prf_script % "proof"
wenzelm@48641
    82
  and "Isabelle.command" :: control
wenzelm@56069
    83
  and "help" "print_commands" "print_options" "print_context"
wenzelm@56069
    84
    "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
wenzelm@48641
    85
    "print_theorems" "print_locales" "print_classes" "print_locale"
wenzelm@48641
    86
    "print_interps" "print_dependencies" "print_attributes"
wenzelm@48641
    87
    "print_simpset" "print_rules" "print_trans_rules" "print_methods"
wenzelm@56069
    88
    "print_antiquotations" "print_ML_antiquotations" "thy_deps"
wenzelm@57415
    89
    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
wenzelm@57415
    90
    "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
wenzelm@57415
    91
    "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
wenzelm@48641
    92
  and "use_thy" "remove_thy" "kill_thy" :: control
wenzelm@52549
    93
  and "display_drafts" "print_state" "pr" :: diag
wenzelm@52438
    94
  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
wenzelm@48646
    95
  and "welcome" :: diag
wenzelm@48646
    96
  and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
wenzelm@48641
    97
  and "end" :: thy_end % "theory"
wenzelm@56797
    98
  and "realizers" :: thy_decl == ""
wenzelm@56797
    99
  and "realizability" :: thy_decl == ""
wenzelm@56797
   100
  and "extract_type" "extract" :: thy_decl
wenzelm@48646
   101
  and "find_theorems" "find_consts" :: diag
wenzelm@57886
   102
  and "named_theorems" :: thy_decl
wenzelm@52437
   103
  and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
wenzelm@52437
   104
    "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
wenzelm@52437
   105
    "ProofGeneral.inform_file_retracted" :: control
wenzelm@48638
   106
begin
wenzelm@15803
   107
wenzelm@56205
   108
ML_file "ML/ml_antiquotations.ML"
wenzelm@55516
   109
ML_file "ML/ml_thms.ML"
wenzelm@56864
   110
ML_file "Tools/print_operation.ML"
wenzelm@48891
   111
ML_file "Isar/isar_syn.ML"
wenzelm@55141
   112
ML_file "Isar/calculation.ML"
wenzelm@55030
   113
ML_file "Tools/rail.ML"
wenzelm@53707
   114
ML_file "Tools/rule_insts.ML";
wenzelm@57934
   115
ML_file "Tools/thm_deps.ML";
haftmann@58201
   116
ML_file "Tools/class_deps.ML"
wenzelm@48891
   117
ML_file "Tools/find_theorems.ML"
wenzelm@48891
   118
ML_file "Tools/find_consts.ML"
wenzelm@52009
   119
ML_file "Tools/proof_general_pure.ML"
wenzelm@54730
   120
ML_file "Tools/simplifier_trace.ML"
wenzelm@57886
   121
ML_file "Tools/named_theorems.ML"
wenzelm@48891
   122
wenzelm@48891
   123
wenzelm@55140
   124
section {* Basic attributes *}
wenzelm@55140
   125
wenzelm@55140
   126
attribute_setup tagged =
wenzelm@55140
   127
  "Scan.lift (Args.name -- Args.name) >> Thm.tag"
wenzelm@55140
   128
  "tagged theorem"
wenzelm@55140
   129
wenzelm@55140
   130
attribute_setup untagged =
wenzelm@55140
   131
  "Scan.lift Args.name >> Thm.untag"
wenzelm@55140
   132
  "untagged theorem"
wenzelm@55140
   133
wenzelm@55140
   134
attribute_setup kind =
wenzelm@55140
   135
  "Scan.lift Args.name >> Thm.kind"
wenzelm@55140
   136
  "theorem kind"
wenzelm@55140
   137
wenzelm@55140
   138
attribute_setup THEN =
wenzelm@55140
   139
  "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
wenzelm@55140
   140
    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
wenzelm@55140
   141
  "resolution with rule"
wenzelm@55140
   142
wenzelm@55140
   143
attribute_setup OF =
wenzelm@55140
   144
  "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
wenzelm@55140
   145
  "rule resolved with facts"
wenzelm@55140
   146
wenzelm@55140
   147
attribute_setup rename_abs =
wenzelm@55140
   148
  "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
wenzelm@55140
   149
    Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
wenzelm@55140
   150
  "rename bound variables in abstractions"
wenzelm@55140
   151
wenzelm@55140
   152
attribute_setup unfolded =
wenzelm@55140
   153
  "Attrib.thms >> (fn ths =>
wenzelm@55140
   154
    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
wenzelm@55140
   155
  "unfolded definitions"
wenzelm@55140
   156
wenzelm@55140
   157
attribute_setup folded =
wenzelm@55140
   158
  "Attrib.thms >> (fn ths =>
wenzelm@55140
   159
    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
wenzelm@55140
   160
  "folded definitions"
wenzelm@55140
   161
wenzelm@55140
   162
attribute_setup consumes =
wenzelm@55140
   163
  "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
wenzelm@55140
   164
  "number of consumed facts"
wenzelm@55140
   165
wenzelm@55140
   166
attribute_setup constraints =
wenzelm@55140
   167
  "Scan.lift Parse.nat >> Rule_Cases.constraints"
wenzelm@55140
   168
  "number of equality constraints"
wenzelm@55140
   169
wenzelm@55140
   170
attribute_setup case_names = {*
wenzelm@55140
   171
  Scan.lift (Scan.repeat1 (Args.name --
wenzelm@55140
   172
    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
wenzelm@55140
   173
  >> (fn cs =>
wenzelm@55140
   174
      Rule_Cases.cases_hyp_names
wenzelm@55140
   175
        (map #1 cs)
wenzelm@55140
   176
        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
wenzelm@55140
   177
*} "named rule cases"
wenzelm@55140
   178
wenzelm@55140
   179
attribute_setup case_conclusion =
wenzelm@55140
   180
  "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
wenzelm@55140
   181
  "named conclusion of rule cases"
wenzelm@55140
   182
wenzelm@55140
   183
attribute_setup params =
wenzelm@55140
   184
  "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
wenzelm@55140
   185
  "named rule parameters"
wenzelm@55140
   186
wenzelm@55140
   187
attribute_setup rule_format = {*
wenzelm@55140
   188
  Scan.lift (Args.mode "no_asm")
wenzelm@55140
   189
    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
wenzelm@55140
   190
*} "result put into canonical rule format"
wenzelm@55140
   191
wenzelm@55140
   192
attribute_setup elim_format =
wenzelm@55140
   193
  "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
wenzelm@55140
   194
  "destruct rule turned into elimination rule format"
wenzelm@55140
   195
wenzelm@55140
   196
attribute_setup no_vars = {*
wenzelm@55140
   197
  Scan.succeed (Thm.rule_attribute (fn context => fn th =>
wenzelm@55140
   198
    let
wenzelm@55140
   199
      val ctxt = Variable.set_body false (Context.proof_of context);
wenzelm@55140
   200
      val ((_, [th']), _) = Variable.import true [th] ctxt;
wenzelm@55140
   201
    in th' end))
wenzelm@55140
   202
*} "imported schematic variables"
wenzelm@55140
   203
wenzelm@55140
   204
attribute_setup eta_long =
wenzelm@55140
   205
  "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
wenzelm@55140
   206
  "put theorem into eta long beta normal form"
wenzelm@55140
   207
wenzelm@55140
   208
attribute_setup atomize =
wenzelm@55140
   209
  "Scan.succeed Object_Logic.declare_atomize"
wenzelm@55140
   210
  "declaration of atomize rule"
wenzelm@55140
   211
wenzelm@55140
   212
attribute_setup rulify =
wenzelm@55140
   213
  "Scan.succeed Object_Logic.declare_rulify"
wenzelm@55140
   214
  "declaration of rulify rule"
wenzelm@55140
   215
wenzelm@55140
   216
attribute_setup rotated =
wenzelm@55140
   217
  "Scan.lift (Scan.optional Parse.int 1
wenzelm@55140
   218
    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
wenzelm@55140
   219
  "rotated theorem premises"
wenzelm@55140
   220
wenzelm@55140
   221
attribute_setup defn =
wenzelm@55140
   222
  "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
wenzelm@55140
   223
  "declaration of definitional transformations"
wenzelm@55140
   224
wenzelm@55140
   225
attribute_setup abs_def =
wenzelm@55140
   226
  "Scan.succeed (Thm.rule_attribute (fn context =>
wenzelm@55140
   227
    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
wenzelm@55140
   228
  "abstract over free variables of definitional theorem"
wenzelm@55140
   229
wenzelm@55140
   230
wenzelm@26435
   231
section {* Further content for the Pure theory *}
wenzelm@20627
   232
wenzelm@18466
   233
subsection {* Meta-level connectives in assumptions *}
wenzelm@15803
   234
wenzelm@15803
   235
lemma meta_mp:
wenzelm@18019
   236
  assumes "PROP P ==> PROP Q" and "PROP P"
wenzelm@15803
   237
  shows "PROP Q"
wenzelm@18019
   238
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
wenzelm@15803
   239
nipkow@23432
   240
lemmas meta_impE = meta_mp [elim_format]
nipkow@23432
   241
wenzelm@15803
   242
lemma meta_spec:
wenzelm@26958
   243
  assumes "!!x. PROP P x"
wenzelm@26958
   244
  shows "PROP P x"
wenzelm@26958
   245
    by (rule `!!x. PROP P x`)
wenzelm@15803
   246
wenzelm@15803
   247
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
   248
wenzelm@26570
   249
lemma swap_params:
wenzelm@26958
   250
  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
wenzelm@26570
   251
wenzelm@18466
   252
wenzelm@18466
   253
subsection {* Meta-level conjunction *}
wenzelm@18466
   254
wenzelm@18466
   255
lemma all_conjunction:
wenzelm@28856
   256
  "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
wenzelm@18466
   257
proof
wenzelm@28856
   258
  assume conj: "!!x. PROP A x &&& PROP B x"
wenzelm@28856
   259
  show "(!!x. PROP A x) &&& (!!x. PROP B x)"
wenzelm@19121
   260
  proof -
wenzelm@18466
   261
    fix x
wenzelm@26958
   262
    from conj show "PROP A x" by (rule conjunctionD1)
wenzelm@26958
   263
    from conj show "PROP B x" by (rule conjunctionD2)
wenzelm@18466
   264
  qed
wenzelm@18466
   265
next
wenzelm@28856
   266
  assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
wenzelm@18466
   267
  fix x
wenzelm@28856
   268
  show "PROP A x &&& PROP B x"
wenzelm@19121
   269
  proof -
wenzelm@26958
   270
    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
wenzelm@26958
   271
    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
wenzelm@18466
   272
  qed
wenzelm@18466
   273
qed
wenzelm@18466
   274
wenzelm@19121
   275
lemma imp_conjunction:
nipkow@50603
   276
  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
wenzelm@18836
   277
proof
wenzelm@28856
   278
  assume conj: "PROP A ==> PROP B &&& PROP C"
wenzelm@28856
   279
  show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
wenzelm@19121
   280
  proof -
wenzelm@18466
   281
    assume "PROP A"
wenzelm@19121
   282
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
wenzelm@19121
   283
    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
wenzelm@18466
   284
  qed
wenzelm@18466
   285
next
wenzelm@28856
   286
  assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
wenzelm@18466
   287
  assume "PROP A"
wenzelm@28856
   288
  show "PROP B &&& PROP C"
wenzelm@19121
   289
  proof -
wenzelm@19121
   290
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
wenzelm@19121
   291
    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
wenzelm@18466
   292
  qed
wenzelm@18466
   293
qed
wenzelm@18466
   294
wenzelm@18466
   295
lemma conjunction_imp:
wenzelm@28856
   296
  "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
wenzelm@18466
   297
proof
wenzelm@28856
   298
  assume r: "PROP A &&& PROP B ==> PROP C"
wenzelm@22933
   299
  assume ab: "PROP A" "PROP B"
wenzelm@22933
   300
  show "PROP C"
wenzelm@22933
   301
  proof (rule r)
wenzelm@28856
   302
    from ab show "PROP A &&& PROP B" .
wenzelm@22933
   303
  qed
wenzelm@18466
   304
next
wenzelm@18466
   305
  assume r: "PROP A ==> PROP B ==> PROP C"
wenzelm@28856
   306
  assume conj: "PROP A &&& PROP B"
wenzelm@18466
   307
  show "PROP C"
wenzelm@18466
   308
  proof (rule r)
wenzelm@19121
   309
    from conj show "PROP A" by (rule conjunctionD1)
wenzelm@19121
   310
    from conj show "PROP B" by (rule conjunctionD2)
wenzelm@18466
   311
  qed
wenzelm@18466
   312
qed
wenzelm@18466
   313
wenzelm@48638
   314
end
wenzelm@48638
   315