src/Pure/Pure.thy
author wenzelm
Fri Jun 27 16:04:56 2014 +0200 (2014-06-27)
changeset 57415 e721124f1b1e
parent 56864 0446c7ac2e32
child 57442 2373b4c61111
permissions -rw-r--r--
command 'print_term_bindings' supersedes 'print_binds';
     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" "typedecl" "type_synonym" "nonterminal" "judgment"
    28     "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
    29     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    30     "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    31     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    32   and "SML_file" "ML_file" :: thy_load % "ML"
    33   and "SML_import" "SML_export" :: thy_decl % "ML"
    34   and "ML" :: thy_decl % "ML"
    35   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    36   and "ML_val" "ML_command" :: diag % "ML"
    37   and "simproc_setup" :: thy_decl % "ML" == ""
    38   and "setup" "local_setup" "attribute_setup" "method_setup"
    39     "declaration" "syntax_declaration"
    40     "parse_ast_translation" "parse_translation" "print_translation"
    41     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
    42   and "bundle" :: thy_decl
    43   and "include" "including" :: prf_decl
    44   and "print_bundles" :: diag
    45   and "context" "locale" :: thy_decl
    46   and "sublocale" "interpretation" :: thy_goal
    47   and "interpret" :: prf_goal % "proof"
    48   and "class" :: thy_decl
    49   and "subclass" :: thy_goal
    50   and "instantiation" :: thy_decl
    51   and "instance" :: thy_goal
    52   and "overloading" :: thy_decl
    53   and "code_datatype" :: thy_decl
    54   and "theorem" "lemma" "corollary" :: thy_goal
    55   and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
    56   and "notepad" :: thy_decl
    57   and "have" :: prf_goal % "proof"
    58   and "hence" :: prf_goal % "proof" == "then have"
    59   and "show" :: prf_asm_goal % "proof"
    60   and "thus" :: prf_asm_goal % "proof" == "then show"
    61   and "then" "from" "with" :: prf_chain % "proof"
    62   and "note" "using" "unfolding" :: prf_decl % "proof"
    63   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    64   and "obtain" :: prf_asm_goal % "proof"
    65   and "guess" :: prf_asm_goal_script % "proof"
    66   and "let" "write" :: prf_decl % "proof"
    67   and "case" :: prf_asm % "proof"
    68   and "{" :: prf_open % "proof"
    69   and "}" :: prf_close % "proof"
    70   and "next" :: prf_block % "proof"
    71   and "qed" :: qed_block % "proof"
    72   and "by" ".." "." "sorry" :: "qed" % "proof"
    73   and "done" :: "qed_script" % "proof"
    74   and "oops" :: qed_global % "proof"
    75   and "defer" "prefer" "apply" :: prf_script % "proof"
    76   and "apply_end" :: prf_script % "proof" == ""
    77   and "proof" :: prf_block % "proof"
    78   and "also" "moreover" :: prf_decl % "proof"
    79   and "finally" "ultimately" :: prf_chain % "proof"
    80   and "back" :: prf_script % "proof"
    81   and "Isabelle.command" :: control
    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_binds" "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 "cd" :: control
    92   and "pwd" :: diag
    93   and "use_thy" "remove_thy" "kill_thy" :: control
    94   and "display_drafts" "print_state" "pr" :: diag
    95   and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    96   and "welcome" :: diag
    97   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
    98   and "end" :: thy_end % "theory"
    99   and "realizers" :: thy_decl == ""
   100   and "realizability" :: thy_decl == ""
   101   and "extract_type" "extract" :: thy_decl
   102   and "find_theorems" "find_consts" :: diag
   103   and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
   104     "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
   105     "ProofGeneral.inform_file_retracted" :: control
   106 begin
   107 
   108 ML_file "ML/ml_antiquotations.ML"
   109 ML_file "ML/ml_thms.ML"
   110 ML_file "Tools/print_operation.ML"
   111 ML_file "Isar/isar_syn.ML"
   112 ML_file "Isar/calculation.ML"
   113 ML_file "Tools/rail.ML"
   114 ML_file "Tools/rule_insts.ML";
   115 ML_file "Tools/find_theorems.ML"
   116 ML_file "Tools/find_consts.ML"
   117 ML_file "Tools/proof_general_pure.ML"
   118 ML_file "Tools/simplifier_trace.ML"
   119 
   120 
   121 section {* Basic attributes *}
   122 
   123 attribute_setup tagged =
   124   "Scan.lift (Args.name -- Args.name) >> Thm.tag"
   125   "tagged theorem"
   126 
   127 attribute_setup untagged =
   128   "Scan.lift Args.name >> Thm.untag"
   129   "untagged theorem"
   130 
   131 attribute_setup kind =
   132   "Scan.lift Args.name >> Thm.kind"
   133   "theorem kind"
   134 
   135 attribute_setup THEN =
   136   "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
   137     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
   138   "resolution with rule"
   139 
   140 attribute_setup OF =
   141   "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
   142   "rule resolved with facts"
   143 
   144 attribute_setup rename_abs =
   145   "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   146     Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
   147   "rename bound variables in abstractions"
   148 
   149 attribute_setup unfolded =
   150   "Attrib.thms >> (fn ths =>
   151     Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
   152   "unfolded definitions"
   153 
   154 attribute_setup folded =
   155   "Attrib.thms >> (fn ths =>
   156     Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
   157   "folded definitions"
   158 
   159 attribute_setup consumes =
   160   "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
   161   "number of consumed facts"
   162 
   163 attribute_setup constraints =
   164   "Scan.lift Parse.nat >> Rule_Cases.constraints"
   165   "number of equality constraints"
   166 
   167 attribute_setup case_names = {*
   168   Scan.lift (Scan.repeat1 (Args.name --
   169     Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
   170   >> (fn cs =>
   171       Rule_Cases.cases_hyp_names
   172         (map #1 cs)
   173         (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
   174 *} "named rule cases"
   175 
   176 attribute_setup case_conclusion =
   177   "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
   178   "named conclusion of rule cases"
   179 
   180 attribute_setup params =
   181   "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
   182   "named rule parameters"
   183 
   184 attribute_setup rule_format = {*
   185   Scan.lift (Args.mode "no_asm")
   186     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
   187 *} "result put into canonical rule format"
   188 
   189 attribute_setup elim_format =
   190   "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
   191   "destruct rule turned into elimination rule format"
   192 
   193 attribute_setup no_vars = {*
   194   Scan.succeed (Thm.rule_attribute (fn context => fn th =>
   195     let
   196       val ctxt = Variable.set_body false (Context.proof_of context);
   197       val ((_, [th']), _) = Variable.import true [th] ctxt;
   198     in th' end))
   199 *} "imported schematic variables"
   200 
   201 attribute_setup eta_long =
   202   "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
   203   "put theorem into eta long beta normal form"
   204 
   205 attribute_setup atomize =
   206   "Scan.succeed Object_Logic.declare_atomize"
   207   "declaration of atomize rule"
   208 
   209 attribute_setup rulify =
   210   "Scan.succeed Object_Logic.declare_rulify"
   211   "declaration of rulify rule"
   212 
   213 attribute_setup rotated =
   214   "Scan.lift (Scan.optional Parse.int 1
   215     >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
   216   "rotated theorem premises"
   217 
   218 attribute_setup defn =
   219   "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
   220   "declaration of definitional transformations"
   221 
   222 attribute_setup abs_def =
   223   "Scan.succeed (Thm.rule_attribute (fn context =>
   224     Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
   225   "abstract over free variables of definitional theorem"
   226 
   227 
   228 section {* Further content for the Pure theory *}
   229 
   230 subsection {* Meta-level connectives in assumptions *}
   231 
   232 lemma meta_mp:
   233   assumes "PROP P ==> PROP Q" and "PROP P"
   234   shows "PROP Q"
   235     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
   236 
   237 lemmas meta_impE = meta_mp [elim_format]
   238 
   239 lemma meta_spec:
   240   assumes "!!x. PROP P x"
   241   shows "PROP P x"
   242     by (rule `!!x. PROP P x`)
   243 
   244 lemmas meta_allE = meta_spec [elim_format]
   245 
   246 lemma swap_params:
   247   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
   248 
   249 
   250 subsection {* Meta-level conjunction *}
   251 
   252 lemma all_conjunction:
   253   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
   254 proof
   255   assume conj: "!!x. PROP A x &&& PROP B x"
   256   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
   257   proof -
   258     fix x
   259     from conj show "PROP A x" by (rule conjunctionD1)
   260     from conj show "PROP B x" by (rule conjunctionD2)
   261   qed
   262 next
   263   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
   264   fix x
   265   show "PROP A x &&& PROP B x"
   266   proof -
   267     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   268     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   269   qed
   270 qed
   271 
   272 lemma imp_conjunction:
   273   "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
   274 proof
   275   assume conj: "PROP A ==> PROP B &&& PROP C"
   276   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   277   proof -
   278     assume "PROP A"
   279     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
   280     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   281   qed
   282 next
   283   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   284   assume "PROP A"
   285   show "PROP B &&& PROP C"
   286   proof -
   287     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
   288     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   289   qed
   290 qed
   291 
   292 lemma conjunction_imp:
   293   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   294 proof
   295   assume r: "PROP A &&& PROP B ==> PROP C"
   296   assume ab: "PROP A" "PROP B"
   297   show "PROP C"
   298   proof (rule r)
   299     from ab show "PROP A &&& PROP B" .
   300   qed
   301 next
   302   assume r: "PROP A ==> PROP B ==> PROP C"
   303   assume conj: "PROP A &&& PROP B"
   304   show "PROP C"
   305   proof (rule r)
   306     from conj show "PROP A" by (rule conjunctionD1)
   307     from conj show "PROP B" by (rule conjunctionD2)
   308   qed
   309 qed
   310 
   311 end
   312