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