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