src/Pure/Pure.thy
author wenzelm
Mon Apr 04 17:02:34 2016 +0200 (2016-04-04)
changeset 62848 e4140efe699e
parent 62490 39d01eaf5292
child 62849 caaa2fc4040d
permissions -rw-r--r--
clarified bootstrap -- more uniform use of ML files;
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@61579
     9
    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
wenzelm@58928
    10
    "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
wenzelm@58928
    11
    "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
haftmann@61671
    12
    "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
wenzelm@58928
    13
    "infixl" "infixr" "is" "notes" "obtains" "open" "output"
ballarin@61566
    14
    "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
ballarin@61566
    15
    "shows" "structure" "unchecked" "where" "when" "|"
wenzelm@58999
    16
  and "text" "txt" :: document_body
wenzelm@58999
    17
  and "text_raw" :: document_raw
wenzelm@57506
    18
  and "default_sort" :: thy_decl == ""
wenzelm@57506
    19
  and "typedecl" "type_synonym" "nonterminal" "judgment"
wenzelm@62169
    20
    "consts" "syntax" "no_syntax" "translations" "no_translations"
wenzelm@55385
    21
    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
wenzelm@61337
    22
    "no_notation" "axiomatization" "lemmas" "declare"
wenzelm@48641
    23
    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
wenzelm@60957
    24
  and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
wenzelm@56618
    25
  and "SML_import" "SML_export" :: thy_decl % "ML"
wenzelm@51295
    26
  and "ML" :: thy_decl % "ML"
wenzelm@48641
    27
  and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
wenzelm@48641
    28
  and "ML_val" "ML_command" :: diag % "ML"
wenzelm@55762
    29
  and "simproc_setup" :: thy_decl % "ML" == ""
wenzelm@48641
    30
  and "setup" "local_setup" "attribute_setup" "method_setup"
wenzelm@55762
    31
    "declaration" "syntax_declaration"
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@59901
    37
  and "context" "locale" "experiment" :: thy_decl_block
wenzelm@51224
    38
  and "interpret" :: prf_goal % "proof"
haftmann@61890
    39
  and "interpretation" "global_interpretation" "sublocale" :: thy_goal
wenzelm@58800
    40
  and "class" :: thy_decl_block
wenzelm@48641
    41
  and "subclass" :: thy_goal
wenzelm@58800
    42
  and "instantiation" :: thy_decl_block
wenzelm@48641
    43
  and "instance" :: thy_goal
wenzelm@58800
    44
  and "overloading" :: thy_decl_block
wenzelm@48641
    45
  and "code_datatype" :: thy_decl
wenzelm@61338
    46
  and "theorem" "lemma" "corollary" "proposition" :: thy_goal
wenzelm@61337
    47
  and "schematic_goal" :: thy_goal
wenzelm@58800
    48
  and "notepad" :: thy_decl_block
wenzelm@50128
    49
  and "have" :: prf_goal % "proof"
wenzelm@50128
    50
  and "hence" :: prf_goal % "proof" == "then have"
wenzelm@50128
    51
  and "show" :: prf_asm_goal % "proof"
wenzelm@50128
    52
  and "thus" :: prf_asm_goal % "proof" == "then show"
wenzelm@48641
    53
  and "then" "from" "with" :: prf_chain % "proof"
wenzelm@60371
    54
  and "note" :: prf_decl % "proof"
wenzelm@60371
    55
  and "supply" :: prf_script % "proof"
wenzelm@60371
    56
  and "using" "unfolding" :: prf_decl % "proof"
wenzelm@48641
    57
  and "fix" "assume" "presume" "def" :: prf_asm % "proof"
wenzelm@60448
    58
  and "consider" :: prf_goal % "proof"
wenzelm@53371
    59
  and "obtain" :: prf_asm_goal % "proof"
wenzelm@60624
    60
  and "guess" :: prf_script_asm_goal % "proof"
wenzelm@48641
    61
  and "let" "write" :: prf_decl % "proof"
wenzelm@48641
    62
  and "case" :: prf_asm % "proof"
wenzelm@48641
    63
  and "{" :: prf_open % "proof"
wenzelm@48641
    64
  and "}" :: prf_close % "proof"
wenzelm@60694
    65
  and "next" :: next_block % "proof"
wenzelm@48641
    66
  and "qed" :: qed_block % "proof"
wenzelm@62312
    67
  and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof"
wenzelm@53571
    68
  and "done" :: "qed_script" % "proof"
wenzelm@48641
    69
  and "oops" :: qed_global % "proof"
wenzelm@50128
    70
  and "defer" "prefer" "apply" :: prf_script % "proof"
wenzelm@50128
    71
  and "apply_end" :: prf_script % "proof" == ""
wenzelm@60624
    72
  and "subgoal" :: prf_script_goal % "proof"
wenzelm@48641
    73
  and "proof" :: prf_block % "proof"
wenzelm@48641
    74
  and "also" "moreover" :: prf_decl % "proof"
wenzelm@48641
    75
  and "finally" "ultimately" :: prf_chain % "proof"
wenzelm@48641
    76
  and "back" :: prf_script % "proof"
wenzelm@61252
    77
  and "help" "print_commands" "print_options" "print_context" "print_theory"
wenzelm@61252
    78
    "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
wenzelm@48641
    79
    "print_theorems" "print_locales" "print_classes" "print_locale"
wenzelm@48641
    80
    "print_interps" "print_dependencies" "print_attributes"
wenzelm@48641
    81
    "print_simpset" "print_rules" "print_trans_rules" "print_methods"
wenzelm@56069
    82
    "print_antiquotations" "print_ML_antiquotations" "thy_deps"
wenzelm@58845
    83
    "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
wenzelm@57415
    84
    "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
wenzelm@57415
    85
    "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
wenzelm@58845
    86
  and "display_drafts" "print_state" :: diag
wenzelm@48646
    87
  and "welcome" :: diag
wenzelm@48641
    88
  and "end" :: thy_end % "theory"
wenzelm@56797
    89
  and "realizers" :: thy_decl == ""
wenzelm@56797
    90
  and "realizability" :: thy_decl == ""
wenzelm@56797
    91
  and "extract_type" "extract" :: thy_decl
wenzelm@48646
    92
  and "find_theorems" "find_consts" :: diag
wenzelm@57886
    93
  and "named_theorems" :: thy_decl
wenzelm@48638
    94
begin
wenzelm@15803
    95
wenzelm@48891
    96
ML_file "Isar/isar_syn.ML"
wenzelm@48891
    97
wenzelm@48891
    98
wenzelm@58611
    99
section \<open>Basic attributes\<close>
wenzelm@55140
   100
wenzelm@55140
   101
attribute_setup tagged =
wenzelm@58611
   102
  \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>
wenzelm@55140
   103
  "tagged theorem"
wenzelm@55140
   104
wenzelm@55140
   105
attribute_setup untagged =
wenzelm@58611
   106
  \<open>Scan.lift Args.name >> Thm.untag\<close>
wenzelm@55140
   107
  "untagged theorem"
wenzelm@55140
   108
wenzelm@55140
   109
attribute_setup kind =
wenzelm@58611
   110
  \<open>Scan.lift Args.name >> Thm.kind\<close>
wenzelm@55140
   111
  "theorem kind"
wenzelm@55140
   112
wenzelm@55140
   113
attribute_setup THEN =
wenzelm@58611
   114
  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
wenzelm@61853
   115
    >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
wenzelm@55140
   116
  "resolution with rule"
wenzelm@55140
   117
wenzelm@55140
   118
attribute_setup OF =
wenzelm@61853
   119
  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
wenzelm@55140
   120
  "rule resolved with facts"
wenzelm@55140
   121
wenzelm@55140
   122
attribute_setup rename_abs =
wenzelm@58611
   123
  \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
wenzelm@61853
   124
    Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
wenzelm@55140
   125
  "rename bound variables in abstractions"
wenzelm@55140
   126
wenzelm@55140
   127
attribute_setup unfolded =
wenzelm@58611
   128
  \<open>Attrib.thms >> (fn ths =>
wenzelm@61853
   129
    Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
wenzelm@55140
   130
  "unfolded definitions"
wenzelm@55140
   131
wenzelm@55140
   132
attribute_setup folded =
wenzelm@58611
   133
  \<open>Attrib.thms >> (fn ths =>
wenzelm@61853
   134
    Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
wenzelm@55140
   135
  "folded definitions"
wenzelm@55140
   136
wenzelm@55140
   137
attribute_setup consumes =
wenzelm@58611
   138
  \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
wenzelm@55140
   139
  "number of consumed facts"
wenzelm@55140
   140
wenzelm@55140
   141
attribute_setup constraints =
wenzelm@58611
   142
  \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close>
wenzelm@55140
   143
  "number of equality constraints"
wenzelm@55140
   144
wenzelm@58611
   145
attribute_setup case_names =
wenzelm@58611
   146
  \<open>Scan.lift (Scan.repeat1 (Args.name --
wenzelm@55140
   147
    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
wenzelm@58611
   148
    >> (fn cs =>
wenzelm@55140
   149
      Rule_Cases.cases_hyp_names
wenzelm@55140
   150
        (map #1 cs)
wenzelm@58611
   151
        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close>
wenzelm@58611
   152
  "named rule cases"
wenzelm@55140
   153
wenzelm@55140
   154
attribute_setup case_conclusion =
wenzelm@58611
   155
  \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close>
wenzelm@55140
   156
  "named conclusion of rule cases"
wenzelm@55140
   157
wenzelm@55140
   158
attribute_setup params =
wenzelm@58611
   159
  \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close>
wenzelm@55140
   160
  "named rule parameters"
wenzelm@55140
   161
wenzelm@58611
   162
attribute_setup rule_format =
wenzelm@58611
   163
  \<open>Scan.lift (Args.mode "no_asm")
wenzelm@58611
   164
    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
wenzelm@58611
   165
  "result put into canonical rule format"
wenzelm@55140
   166
wenzelm@55140
   167
attribute_setup elim_format =
wenzelm@61853
   168
  \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
wenzelm@55140
   169
  "destruct rule turned into elimination rule format"
wenzelm@55140
   170
wenzelm@58611
   171
attribute_setup no_vars =
wenzelm@61853
   172
  \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
wenzelm@55140
   173
    let
wenzelm@55140
   174
      val ctxt = Variable.set_body false (Context.proof_of context);
wenzelm@55140
   175
      val ((_, [th']), _) = Variable.import true [th] ctxt;
wenzelm@58611
   176
    in th' end))\<close>
wenzelm@58611
   177
  "imported schematic variables"
wenzelm@55140
   178
wenzelm@55140
   179
attribute_setup atomize =
wenzelm@58611
   180
  \<open>Scan.succeed Object_Logic.declare_atomize\<close>
wenzelm@55140
   181
  "declaration of atomize rule"
wenzelm@55140
   182
wenzelm@55140
   183
attribute_setup rulify =
wenzelm@58611
   184
  \<open>Scan.succeed Object_Logic.declare_rulify\<close>
wenzelm@55140
   185
  "declaration of rulify rule"
wenzelm@55140
   186
wenzelm@55140
   187
attribute_setup rotated =
wenzelm@58611
   188
  \<open>Scan.lift (Scan.optional Parse.int 1
wenzelm@61853
   189
    >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
wenzelm@55140
   190
  "rotated theorem premises"
wenzelm@55140
   191
wenzelm@55140
   192
attribute_setup defn =
wenzelm@58611
   193
  \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
wenzelm@55140
   194
  "declaration of definitional transformations"
wenzelm@55140
   195
wenzelm@55140
   196
attribute_setup abs_def =
wenzelm@61853
   197
  \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
wenzelm@58611
   198
    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
wenzelm@55140
   199
  "abstract over free variables of definitional theorem"
wenzelm@55140
   200
wenzelm@55140
   201
wenzelm@58611
   202
section \<open>Further content for the Pure theory\<close>
wenzelm@20627
   203
wenzelm@58611
   204
subsection \<open>Meta-level connectives in assumptions\<close>
wenzelm@15803
   205
wenzelm@15803
   206
lemma meta_mp:
wenzelm@58612
   207
  assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
wenzelm@15803
   208
  shows "PROP Q"
wenzelm@58612
   209
    by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
wenzelm@15803
   210
nipkow@23432
   211
lemmas meta_impE = meta_mp [elim_format]
nipkow@23432
   212
wenzelm@15803
   213
lemma meta_spec:
wenzelm@58612
   214
  assumes "\<And>x. PROP P x"
wenzelm@26958
   215
  shows "PROP P x"
wenzelm@58612
   216
    by (rule \<open>\<And>x. PROP P x\<close>)
wenzelm@15803
   217
wenzelm@15803
   218
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
   219
wenzelm@26570
   220
lemma swap_params:
wenzelm@58612
   221
  "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
wenzelm@26570
   222
wenzelm@18466
   223
wenzelm@58611
   224
subsection \<open>Meta-level conjunction\<close>
wenzelm@18466
   225
wenzelm@18466
   226
lemma all_conjunction:
wenzelm@58612
   227
  "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
wenzelm@18466
   228
proof
wenzelm@58612
   229
  assume conj: "\<And>x. PROP A x &&& PROP B x"
wenzelm@58612
   230
  show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
wenzelm@19121
   231
  proof -
wenzelm@18466
   232
    fix x
wenzelm@26958
   233
    from conj show "PROP A x" by (rule conjunctionD1)
wenzelm@26958
   234
    from conj show "PROP B x" by (rule conjunctionD2)
wenzelm@18466
   235
  qed
wenzelm@18466
   236
next
wenzelm@58612
   237
  assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
wenzelm@18466
   238
  fix x
wenzelm@28856
   239
  show "PROP A x &&& PROP B x"
wenzelm@19121
   240
  proof -
wenzelm@26958
   241
    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
wenzelm@26958
   242
    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
wenzelm@18466
   243
  qed
wenzelm@18466
   244
qed
wenzelm@18466
   245
wenzelm@19121
   246
lemma imp_conjunction:
wenzelm@58612
   247
  "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
wenzelm@18836
   248
proof
wenzelm@58612
   249
  assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
wenzelm@58612
   250
  show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
wenzelm@19121
   251
  proof -
wenzelm@18466
   252
    assume "PROP A"
wenzelm@58611
   253
    from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
wenzelm@58611
   254
    from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
wenzelm@18466
   255
  qed
wenzelm@18466
   256
next
wenzelm@58612
   257
  assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
wenzelm@18466
   258
  assume "PROP A"
wenzelm@28856
   259
  show "PROP B &&& PROP C"
wenzelm@19121
   260
  proof -
wenzelm@58611
   261
    from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
wenzelm@58611
   262
    from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
wenzelm@18466
   263
  qed
wenzelm@18466
   264
qed
wenzelm@18466
   265
wenzelm@18466
   266
lemma conjunction_imp:
wenzelm@58612
   267
  "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
wenzelm@18466
   268
proof
wenzelm@58612
   269
  assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
wenzelm@22933
   270
  assume ab: "PROP A" "PROP B"
wenzelm@22933
   271
  show "PROP C"
wenzelm@22933
   272
  proof (rule r)
wenzelm@28856
   273
    from ab show "PROP A &&& PROP B" .
wenzelm@22933
   274
  qed
wenzelm@18466
   275
next
wenzelm@58612
   276
  assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
wenzelm@28856
   277
  assume conj: "PROP A &&& PROP B"
wenzelm@18466
   278
  show "PROP C"
wenzelm@18466
   279
  proof (rule r)
wenzelm@19121
   280
    from conj show "PROP A" by (rule conjunctionD1)
wenzelm@19121
   281
    from conj show "PROP B" by (rule conjunctionD2)
wenzelm@18466
   282
  qed
wenzelm@18466
   283
qed
wenzelm@18466
   284
wenzelm@48638
   285
end