src/Pure/Pure.thy
author wenzelm
Sat Jan 25 18:18:03 2014 +0100 (2014-01-25)
changeset 55140 7eb0c04e4c40
parent 55030 9a9049d12e21
child 55141 863b4f9f6bd7
permissions -rw-r--r--
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
     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 "Tools/rail.ML"
   107 ML_file "Tools/rule_insts.ML";
   108 ML_file "Tools/find_theorems.ML"
   109 ML_file "Tools/find_consts.ML"
   110 ML_file "Tools/proof_general_pure.ML"
   111 ML_file "Tools/simplifier_trace.ML"
   112 
   113 
   114 section {* Basic attributes *}
   115 
   116 attribute_setup tagged =
   117   "Scan.lift (Args.name -- Args.name) >> Thm.tag"
   118   "tagged theorem"
   119 
   120 attribute_setup untagged =
   121   "Scan.lift Args.name >> Thm.untag"
   122   "untagged theorem"
   123 
   124 attribute_setup kind =
   125   "Scan.lift Args.name >> Thm.kind"
   126   "theorem kind"
   127 
   128 attribute_setup THEN =
   129   "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
   130     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
   131   "resolution with rule"
   132 
   133 attribute_setup OF =
   134   "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
   135   "rule resolved with facts"
   136 
   137 attribute_setup rename_abs =
   138   "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   139     Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
   140   "rename bound variables in abstractions"
   141 
   142 attribute_setup unfolded =
   143   "Attrib.thms >> (fn ths =>
   144     Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
   145   "unfolded definitions"
   146 
   147 attribute_setup folded =
   148   "Attrib.thms >> (fn ths =>
   149     Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
   150   "folded definitions"
   151 
   152 attribute_setup consumes =
   153   "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
   154   "number of consumed facts"
   155 
   156 attribute_setup constraints =
   157   "Scan.lift Parse.nat >> Rule_Cases.constraints"
   158   "number of equality constraints"
   159 
   160 attribute_setup case_names = {*
   161   Scan.lift (Scan.repeat1 (Args.name --
   162     Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
   163   >> (fn cs =>
   164       Rule_Cases.cases_hyp_names
   165         (map #1 cs)
   166         (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
   167 *} "named rule cases"
   168 
   169 attribute_setup case_conclusion =
   170   "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
   171   "named conclusion of rule cases"
   172 
   173 attribute_setup params =
   174   "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
   175   "named rule parameters"
   176 
   177 attribute_setup standard =
   178   "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
   179   "result put into standard form (legacy)"
   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