src/Pure/Pure.thy
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 56205 ceb8a93460b7
child 56618 874bdedb2313
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
     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 "SML_file" "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" "print_context"
    82     "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" "print_ML_antiquotations" "thy_deps"
    87     "locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts"
    88     "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
    89     "term" "typ" "print_codesetup" "unused_thms"
    90     :: 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" "realizability" "extract_type" "extract" :: thy_decl
   100   and "find_theorems" "find_consts" :: diag
   101   and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
   102     "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
   103     "ProofGeneral.inform_file_retracted" :: control
   104 begin
   105 
   106 ML_file "ML/ml_antiquotations.ML"
   107 ML_file "ML/ml_thms.ML"
   108 ML_file "Isar/isar_syn.ML"
   109 ML_file "Isar/calculation.ML"
   110 ML_file "Tools/rail.ML"
   111 ML_file "Tools/rule_insts.ML";
   112 ML_file "Tools/find_theorems.ML"
   113 ML_file "Tools/find_consts.ML"
   114 ML_file "Tools/proof_general_pure.ML"
   115 ML_file "Tools/simplifier_trace.ML"
   116 
   117 
   118 section {* Basic attributes *}
   119 
   120 attribute_setup tagged =
   121   "Scan.lift (Args.name -- Args.name) >> Thm.tag"
   122   "tagged theorem"
   123 
   124 attribute_setup untagged =
   125   "Scan.lift Args.name >> Thm.untag"
   126   "untagged theorem"
   127 
   128 attribute_setup kind =
   129   "Scan.lift Args.name >> Thm.kind"
   130   "theorem kind"
   131 
   132 attribute_setup THEN =
   133   "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
   134     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
   135   "resolution with rule"
   136 
   137 attribute_setup OF =
   138   "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
   139   "rule resolved with facts"
   140 
   141 attribute_setup rename_abs =
   142   "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   143     Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
   144   "rename bound variables in abstractions"
   145 
   146 attribute_setup unfolded =
   147   "Attrib.thms >> (fn ths =>
   148     Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
   149   "unfolded definitions"
   150 
   151 attribute_setup folded =
   152   "Attrib.thms >> (fn ths =>
   153     Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
   154   "folded definitions"
   155 
   156 attribute_setup consumes =
   157   "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
   158   "number of consumed facts"
   159 
   160 attribute_setup constraints =
   161   "Scan.lift Parse.nat >> Rule_Cases.constraints"
   162   "number of equality constraints"
   163 
   164 attribute_setup case_names = {*
   165   Scan.lift (Scan.repeat1 (Args.name --
   166     Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
   167   >> (fn cs =>
   168       Rule_Cases.cases_hyp_names
   169         (map #1 cs)
   170         (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
   171 *} "named rule cases"
   172 
   173 attribute_setup case_conclusion =
   174   "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
   175   "named conclusion of rule cases"
   176 
   177 attribute_setup params =
   178   "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
   179   "named rule parameters"
   180 
   181 attribute_setup rule_format = {*
   182   Scan.lift (Args.mode "no_asm")
   183     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
   184 *} "result put into canonical rule format"
   185 
   186 attribute_setup elim_format =
   187   "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
   188   "destruct rule turned into elimination rule format"
   189 
   190 attribute_setup no_vars = {*
   191   Scan.succeed (Thm.rule_attribute (fn context => fn th =>
   192     let
   193       val ctxt = Variable.set_body false (Context.proof_of context);
   194       val ((_, [th']), _) = Variable.import true [th] ctxt;
   195     in th' end))
   196 *} "imported schematic variables"
   197 
   198 attribute_setup eta_long =
   199   "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
   200   "put theorem into eta long beta normal form"
   201 
   202 attribute_setup atomize =
   203   "Scan.succeed Object_Logic.declare_atomize"
   204   "declaration of atomize rule"
   205 
   206 attribute_setup rulify =
   207   "Scan.succeed Object_Logic.declare_rulify"
   208   "declaration of rulify rule"
   209 
   210 attribute_setup rotated =
   211   "Scan.lift (Scan.optional Parse.int 1
   212     >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
   213   "rotated theorem premises"
   214 
   215 attribute_setup defn =
   216   "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
   217   "declaration of definitional transformations"
   218 
   219 attribute_setup abs_def =
   220   "Scan.succeed (Thm.rule_attribute (fn context =>
   221     Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
   222   "abstract over free variables of definitional theorem"
   223 
   224 
   225 section {* Further content for the Pure theory *}
   226 
   227 subsection {* Meta-level connectives in assumptions *}
   228 
   229 lemma meta_mp:
   230   assumes "PROP P ==> PROP Q" and "PROP P"
   231   shows "PROP Q"
   232     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
   233 
   234 lemmas meta_impE = meta_mp [elim_format]
   235 
   236 lemma meta_spec:
   237   assumes "!!x. PROP P x"
   238   shows "PROP P x"
   239     by (rule `!!x. PROP P x`)
   240 
   241 lemmas meta_allE = meta_spec [elim_format]
   242 
   243 lemma swap_params:
   244   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
   245 
   246 
   247 subsection {* Meta-level conjunction *}
   248 
   249 lemma all_conjunction:
   250   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
   251 proof
   252   assume conj: "!!x. PROP A x &&& PROP B x"
   253   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
   254   proof -
   255     fix x
   256     from conj show "PROP A x" by (rule conjunctionD1)
   257     from conj show "PROP B x" by (rule conjunctionD2)
   258   qed
   259 next
   260   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
   261   fix x
   262   show "PROP A x &&& PROP B x"
   263   proof -
   264     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   265     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   266   qed
   267 qed
   268 
   269 lemma imp_conjunction:
   270   "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
   271 proof
   272   assume conj: "PROP A ==> PROP B &&& PROP C"
   273   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   274   proof -
   275     assume "PROP A"
   276     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
   277     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   278   qed
   279 next
   280   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   281   assume "PROP A"
   282   show "PROP B &&& PROP C"
   283   proof -
   284     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
   285     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   286   qed
   287 qed
   288 
   289 lemma conjunction_imp:
   290   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   291 proof
   292   assume r: "PROP A &&& PROP B ==> PROP C"
   293   assume ab: "PROP A" "PROP B"
   294   show "PROP C"
   295   proof (rule r)
   296     from ab show "PROP A &&& PROP B" .
   297   qed
   298 next
   299   assume r: "PROP A ==> PROP B ==> PROP C"
   300   assume conj: "PROP A &&& PROP B"
   301   show "PROP C"
   302   proof (rule r)
   303     from conj show "PROP A" by (rule conjunctionD1)
   304     from conj show "PROP B" by (rule conjunctionD2)
   305   qed
   306 qed
   307 
   308 end
   309