src/Pure/Pure.thy
author wenzelm
Mon Jun 30 10:34:28 2014 +0200 (2014-06-30)
changeset 57442 2373b4c61111
parent 57415 e721124f1b1e
child 57506 f5dbec155914
permissions -rw-r--r--
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
     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 "use_thy" "remove_thy" "kill_thy" :: control
    92   and "display_drafts" "print_state" "pr" :: diag
    93   and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    94   and "welcome" :: diag
    95   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
    96   and "end" :: thy_end % "theory"
    97   and "realizers" :: thy_decl == ""
    98   and "realizability" :: thy_decl == ""
    99   and "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 "Tools/print_operation.ML"
   109 ML_file "Isar/isar_syn.ML"
   110 ML_file "Isar/calculation.ML"
   111 ML_file "Tools/rail.ML"
   112 ML_file "Tools/rule_insts.ML";
   113 ML_file "Tools/find_theorems.ML"
   114 ML_file "Tools/find_consts.ML"
   115 ML_file "Tools/proof_general_pure.ML"
   116 ML_file "Tools/simplifier_trace.ML"
   117 
   118 
   119 section {* Basic attributes *}
   120 
   121 attribute_setup tagged =
   122   "Scan.lift (Args.name -- Args.name) >> Thm.tag"
   123   "tagged theorem"
   124 
   125 attribute_setup untagged =
   126   "Scan.lift Args.name >> Thm.untag"
   127   "untagged theorem"
   128 
   129 attribute_setup kind =
   130   "Scan.lift Args.name >> Thm.kind"
   131   "theorem kind"
   132 
   133 attribute_setup THEN =
   134   "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
   135     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
   136   "resolution with rule"
   137 
   138 attribute_setup OF =
   139   "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
   140   "rule resolved with facts"
   141 
   142 attribute_setup rename_abs =
   143   "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   144     Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
   145   "rename bound variables in abstractions"
   146 
   147 attribute_setup unfolded =
   148   "Attrib.thms >> (fn ths =>
   149     Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
   150   "unfolded definitions"
   151 
   152 attribute_setup folded =
   153   "Attrib.thms >> (fn ths =>
   154     Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
   155   "folded definitions"
   156 
   157 attribute_setup consumes =
   158   "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
   159   "number of consumed facts"
   160 
   161 attribute_setup constraints =
   162   "Scan.lift Parse.nat >> Rule_Cases.constraints"
   163   "number of equality constraints"
   164 
   165 attribute_setup case_names = {*
   166   Scan.lift (Scan.repeat1 (Args.name --
   167     Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
   168   >> (fn cs =>
   169       Rule_Cases.cases_hyp_names
   170         (map #1 cs)
   171         (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
   172 *} "named rule cases"
   173 
   174 attribute_setup case_conclusion =
   175   "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
   176   "named conclusion of rule cases"
   177 
   178 attribute_setup params =
   179   "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
   180   "named rule parameters"
   181 
   182 attribute_setup rule_format = {*
   183   Scan.lift (Args.mode "no_asm")
   184     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
   185 *} "result put into canonical rule format"
   186 
   187 attribute_setup elim_format =
   188   "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
   189   "destruct rule turned into elimination rule format"
   190 
   191 attribute_setup no_vars = {*
   192   Scan.succeed (Thm.rule_attribute (fn context => fn th =>
   193     let
   194       val ctxt = Variable.set_body false (Context.proof_of context);
   195       val ((_, [th']), _) = Variable.import true [th] ctxt;
   196     in th' end))
   197 *} "imported schematic variables"
   198 
   199 attribute_setup eta_long =
   200   "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
   201   "put theorem into eta long beta normal form"
   202 
   203 attribute_setup atomize =
   204   "Scan.succeed Object_Logic.declare_atomize"
   205   "declaration of atomize rule"
   206 
   207 attribute_setup rulify =
   208   "Scan.succeed Object_Logic.declare_rulify"
   209   "declaration of rulify rule"
   210 
   211 attribute_setup rotated =
   212   "Scan.lift (Scan.optional Parse.int 1
   213     >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
   214   "rotated theorem premises"
   215 
   216 attribute_setup defn =
   217   "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
   218   "declaration of definitional transformations"
   219 
   220 attribute_setup abs_def =
   221   "Scan.succeed (Thm.rule_attribute (fn context =>
   222     Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
   223   "abstract over free variables of definitional theorem"
   224 
   225 
   226 section {* Further content for the Pure theory *}
   227 
   228 subsection {* Meta-level connectives in assumptions *}
   229 
   230 lemma meta_mp:
   231   assumes "PROP P ==> PROP Q" and "PROP P"
   232   shows "PROP Q"
   233     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
   234 
   235 lemmas meta_impE = meta_mp [elim_format]
   236 
   237 lemma meta_spec:
   238   assumes "!!x. PROP P x"
   239   shows "PROP P x"
   240     by (rule `!!x. PROP P x`)
   241 
   242 lemmas meta_allE = meta_spec [elim_format]
   243 
   244 lemma swap_params:
   245   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
   246 
   247 
   248 subsection {* Meta-level conjunction *}
   249 
   250 lemma all_conjunction:
   251   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
   252 proof
   253   assume conj: "!!x. PROP A x &&& PROP B x"
   254   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
   255   proof -
   256     fix x
   257     from conj show "PROP A x" by (rule conjunctionD1)
   258     from conj show "PROP B x" by (rule conjunctionD2)
   259   qed
   260 next
   261   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
   262   fix x
   263   show "PROP A x &&& PROP B x"
   264   proof -
   265     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   266     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   267   qed
   268 qed
   269 
   270 lemma imp_conjunction:
   271   "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
   272 proof
   273   assume conj: "PROP A ==> PROP B &&& PROP C"
   274   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   275   proof -
   276     assume "PROP A"
   277     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
   278     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   279   qed
   280 next
   281   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   282   assume "PROP A"
   283   show "PROP B &&& PROP C"
   284   proof -
   285     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
   286     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   287   qed
   288 qed
   289 
   290 lemma conjunction_imp:
   291   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   292 proof
   293   assume r: "PROP A &&& PROP B ==> PROP C"
   294   assume ab: "PROP A" "PROP B"
   295   show "PROP C"
   296   proof (rule r)
   297     from ab show "PROP A &&& PROP B" .
   298   qed
   299 next
   300   assume r: "PROP A ==> PROP B ==> PROP C"
   301   assume conj: "PROP A &&& PROP B"
   302   show "PROP C"
   303   proof (rule r)
   304     from conj show "PROP A" by (rule conjunctionD1)
   305     from conj show "PROP B" by (rule conjunctionD2)
   306   qed
   307 qed
   308 
   309 end
   310