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