src/Pure/Pure.thy
author wenzelm
Sun Jan 26 14:01:19 2014 +0100 (2014-01-26)
changeset 55152 a56099a6447a
parent 55141 863b4f9f6bd7
child 55385 169e12bbf9a3
permissions -rw-r--r--
discontinued obsolete attribute "standard";
     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 "classes" "classrel" "default_sort" "typedecl" "type_synonym"
    29     "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
    30     "translations" "no_translations" "defs" "definition"
    31     "abbreviation" "type_notation" "no_type_notation" "notation"
    32     "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    33     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    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 "setup" "local_setup" "attribute_setup" "method_setup"
    38     "declaration" "syntax_declaration" "simproc_setup"
    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 "Isar/isar_syn.ML"
   106 ML_file "Isar/calculation.ML"
   107 ML_file "Tools/rail.ML"
   108 ML_file "Tools/rule_insts.ML";
   109 ML_file "Tools/find_theorems.ML"
   110 ML_file "Tools/find_consts.ML"
   111 ML_file "Tools/proof_general_pure.ML"
   112 ML_file "Tools/simplifier_trace.ML"
   113 
   114 
   115 section {* Basic attributes *}
   116 
   117 attribute_setup tagged =
   118   "Scan.lift (Args.name -- Args.name) >> Thm.tag"
   119   "tagged theorem"
   120 
   121 attribute_setup untagged =
   122   "Scan.lift Args.name >> Thm.untag"
   123   "untagged theorem"
   124 
   125 attribute_setup kind =
   126   "Scan.lift Args.name >> Thm.kind"
   127   "theorem kind"
   128 
   129 attribute_setup THEN =
   130   "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
   131     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
   132   "resolution with rule"
   133 
   134 attribute_setup OF =
   135   "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
   136   "rule resolved with facts"
   137 
   138 attribute_setup rename_abs =
   139   "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   140     Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
   141   "rename bound variables in abstractions"
   142 
   143 attribute_setup unfolded =
   144   "Attrib.thms >> (fn ths =>
   145     Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
   146   "unfolded definitions"
   147 
   148 attribute_setup folded =
   149   "Attrib.thms >> (fn ths =>
   150     Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
   151   "folded definitions"
   152 
   153 attribute_setup consumes =
   154   "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
   155   "number of consumed facts"
   156 
   157 attribute_setup constraints =
   158   "Scan.lift Parse.nat >> Rule_Cases.constraints"
   159   "number of equality constraints"
   160 
   161 attribute_setup case_names = {*
   162   Scan.lift (Scan.repeat1 (Args.name --
   163     Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
   164   >> (fn cs =>
   165       Rule_Cases.cases_hyp_names
   166         (map #1 cs)
   167         (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
   168 *} "named rule cases"
   169 
   170 attribute_setup case_conclusion =
   171   "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
   172   "named conclusion of rule cases"
   173 
   174 attribute_setup params =
   175   "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
   176   "named rule parameters"
   177 
   178 attribute_setup rule_format = {*
   179   Scan.lift (Args.mode "no_asm")
   180     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
   181 *} "result put into canonical rule format"
   182 
   183 attribute_setup elim_format =
   184   "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
   185   "destruct rule turned into elimination rule format"
   186 
   187 attribute_setup no_vars = {*
   188   Scan.succeed (Thm.rule_attribute (fn context => fn th =>
   189     let
   190       val ctxt = Variable.set_body false (Context.proof_of context);
   191       val ((_, [th']), _) = Variable.import true [th] ctxt;
   192     in th' end))
   193 *} "imported schematic variables"
   194 
   195 attribute_setup eta_long =
   196   "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
   197   "put theorem into eta long beta normal form"
   198 
   199 attribute_setup atomize =
   200   "Scan.succeed Object_Logic.declare_atomize"
   201   "declaration of atomize rule"
   202 
   203 attribute_setup rulify =
   204   "Scan.succeed Object_Logic.declare_rulify"
   205   "declaration of rulify rule"
   206 
   207 attribute_setup rotated =
   208   "Scan.lift (Scan.optional Parse.int 1
   209     >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
   210   "rotated theorem premises"
   211 
   212 attribute_setup defn =
   213   "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
   214   "declaration of definitional transformations"
   215 
   216 attribute_setup abs_def =
   217   "Scan.succeed (Thm.rule_attribute (fn context =>
   218     Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
   219   "abstract over free variables of definitional theorem"
   220 
   221 
   222 section {* Further content for the Pure theory *}
   223 
   224 subsection {* Meta-level connectives in assumptions *}
   225 
   226 lemma meta_mp:
   227   assumes "PROP P ==> PROP Q" and "PROP P"
   228   shows "PROP Q"
   229     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
   230 
   231 lemmas meta_impE = meta_mp [elim_format]
   232 
   233 lemma meta_spec:
   234   assumes "!!x. PROP P x"
   235   shows "PROP P x"
   236     by (rule `!!x. PROP P x`)
   237 
   238 lemmas meta_allE = meta_spec [elim_format]
   239 
   240 lemma swap_params:
   241   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
   242 
   243 
   244 subsection {* Meta-level conjunction *}
   245 
   246 lemma all_conjunction:
   247   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
   248 proof
   249   assume conj: "!!x. PROP A x &&& PROP B x"
   250   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
   251   proof -
   252     fix x
   253     from conj show "PROP A x" by (rule conjunctionD1)
   254     from conj show "PROP B x" by (rule conjunctionD2)
   255   qed
   256 next
   257   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
   258   fix x
   259   show "PROP A x &&& PROP B x"
   260   proof -
   261     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   262     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   263   qed
   264 qed
   265 
   266 lemma imp_conjunction:
   267   "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
   268 proof
   269   assume conj: "PROP A ==> PROP B &&& PROP C"
   270   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   271   proof -
   272     assume "PROP A"
   273     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
   274     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   275   qed
   276 next
   277   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   278   assume "PROP A"
   279   show "PROP B &&& PROP C"
   280   proof -
   281     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
   282     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   283   qed
   284 qed
   285 
   286 lemma conjunction_imp:
   287   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   288 proof
   289   assume r: "PROP A &&& PROP B ==> PROP C"
   290   assume ab: "PROP A" "PROP B"
   291   show "PROP C"
   292   proof (rule r)
   293     from ab show "PROP A &&& PROP B" .
   294   qed
   295 next
   296   assume r: "PROP A ==> PROP B ==> PROP C"
   297   assume conj: "PROP A &&& PROP B"
   298   show "PROP C"
   299   proof (rule r)
   300     from conj show "PROP A" by (rule conjunctionD1)
   301     from conj show "PROP B" by (rule conjunctionD2)
   302   qed
   303 qed
   304 
   305 end
   306