src/Pure/Pure.thy
author wenzelm
Tue Mar 01 19:42:59 2016 +0100 (2016-03-01)
changeset 62490 39d01eaf5292
parent 62312 5e5a881ebc12
child 62848 e4140efe699e
permissions -rw-r--r--
ML debugger support in Pure (again, see 3565c9f407ec);
     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     "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
    10     "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    11     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    12     "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    13     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    14     "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
    15     "shows" "structure" "unchecked" "where" "when" "|"
    16   and "text" "txt" :: document_body
    17   and "text_raw" :: document_raw
    18   and "default_sort" :: thy_decl == ""
    19   and "typedecl" "type_synonym" "nonterminal" "judgment"
    20     "consts" "syntax" "no_syntax" "translations" "no_translations"
    21     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    22     "no_notation" "axiomatization" "lemmas" "declare"
    23     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    24   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    25   and "SML_import" "SML_export" :: thy_decl % "ML"
    26   and "ML" :: thy_decl % "ML"
    27   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    28   and "ML_val" "ML_command" :: diag % "ML"
    29   and "simproc_setup" :: thy_decl % "ML" == ""
    30   and "setup" "local_setup" "attribute_setup" "method_setup"
    31     "declaration" "syntax_declaration"
    32     "parse_ast_translation" "parse_translation" "print_translation"
    33     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
    34   and "bundle" :: thy_decl
    35   and "include" "including" :: prf_decl
    36   and "print_bundles" :: diag
    37   and "context" "locale" "experiment" :: thy_decl_block
    38   and "interpret" :: prf_goal % "proof"
    39   and "interpretation" "global_interpretation" "sublocale" :: thy_goal
    40   and "class" :: thy_decl_block
    41   and "subclass" :: thy_goal
    42   and "instantiation" :: thy_decl_block
    43   and "instance" :: thy_goal
    44   and "overloading" :: thy_decl_block
    45   and "code_datatype" :: thy_decl
    46   and "theorem" "lemma" "corollary" "proposition" :: thy_goal
    47   and "schematic_goal" :: thy_goal
    48   and "notepad" :: thy_decl_block
    49   and "have" :: prf_goal % "proof"
    50   and "hence" :: prf_goal % "proof" == "then have"
    51   and "show" :: prf_asm_goal % "proof"
    52   and "thus" :: prf_asm_goal % "proof" == "then show"
    53   and "then" "from" "with" :: prf_chain % "proof"
    54   and "note" :: prf_decl % "proof"
    55   and "supply" :: prf_script % "proof"
    56   and "using" "unfolding" :: prf_decl % "proof"
    57   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    58   and "consider" :: prf_goal % "proof"
    59   and "obtain" :: prf_asm_goal % "proof"
    60   and "guess" :: prf_script_asm_goal % "proof"
    61   and "let" "write" :: prf_decl % "proof"
    62   and "case" :: prf_asm % "proof"
    63   and "{" :: prf_open % "proof"
    64   and "}" :: prf_close % "proof"
    65   and "next" :: next_block % "proof"
    66   and "qed" :: qed_block % "proof"
    67   and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof"
    68   and "done" :: "qed_script" % "proof"
    69   and "oops" :: qed_global % "proof"
    70   and "defer" "prefer" "apply" :: prf_script % "proof"
    71   and "apply_end" :: prf_script % "proof" == ""
    72   and "subgoal" :: prf_script_goal % "proof"
    73   and "proof" :: prf_block % "proof"
    74   and "also" "moreover" :: prf_decl % "proof"
    75   and "finally" "ultimately" :: prf_chain % "proof"
    76   and "back" :: prf_script % "proof"
    77   and "help" "print_commands" "print_options" "print_context" "print_theory"
    78     "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
    79     "print_theorems" "print_locales" "print_classes" "print_locale"
    80     "print_interps" "print_dependencies" "print_attributes"
    81     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
    82     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
    83     "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
    84     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
    85     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
    86   and "display_drafts" "print_state" :: diag
    87   and "welcome" :: diag
    88   and "end" :: thy_end % "theory"
    89   and "realizers" :: thy_decl == ""
    90   and "realizability" :: thy_decl == ""
    91   and "extract_type" "extract" :: thy_decl
    92   and "find_theorems" "find_consts" :: diag
    93   and "named_theorems" :: thy_decl
    94 begin
    95 
    96 ML_file "ML/ml_antiquotations.ML"
    97 ML_file "ML/ml_thms.ML"
    98 ML_file "Tools/print_operation.ML"
    99 ML_file "Isar/isar_syn.ML"
   100 ML_file "Isar/calculation.ML"
   101 ML_file "Tools/bibtex.ML"
   102 ML_file "Tools/rail.ML"
   103 ML_file "Tools/rule_insts.ML"
   104 ML_file "Tools/thm_deps.ML"
   105 ML_file "Tools/thy_deps.ML"
   106 ML_file "Tools/class_deps.ML"
   107 ML_file "Tools/find_theorems.ML"
   108 ML_file "Tools/find_consts.ML"
   109 ML_file "Tools/simplifier_trace.ML"
   110 ML_file_no_debug "Tools/debugger.ML"
   111 ML_file "Tools/named_theorems.ML"
   112 ML_file "Tools/jedit.ML"
   113 
   114 
   115 section \<open>Basic attributes\<close>
   116 
   117 attribute_setup tagged =
   118   \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>
   119   "tagged theorem"
   120 
   121 attribute_setup untagged =
   122   \<open>Scan.lift Args.name >> Thm.untag\<close>
   123   "untagged theorem"
   124 
   125 attribute_setup kind =
   126   \<open>Scan.lift Args.name >> Thm.kind\<close>
   127   "theorem kind"
   128 
   129 attribute_setup THEN =
   130   \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
   131     >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
   132   "resolution with rule"
   133 
   134 attribute_setup OF =
   135   \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
   136   "rule resolved with facts"
   137 
   138 attribute_setup rename_abs =
   139   \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   140     Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
   141   "rename bound variables in abstractions"
   142 
   143 attribute_setup unfolded =
   144   \<open>Attrib.thms >> (fn ths =>
   145     Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
   146   "unfolded definitions"
   147 
   148 attribute_setup folded =
   149   \<open>Attrib.thms >> (fn ths =>
   150     Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
   151   "folded definitions"
   152 
   153 attribute_setup consumes =
   154   \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
   155   "number of consumed facts"
   156 
   157 attribute_setup constraints =
   158   \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close>
   159   "number of equality constraints"
   160 
   161 attribute_setup case_names =
   162   \<open>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))\<close>
   168   "named rule cases"
   169 
   170 attribute_setup case_conclusion =
   171   \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close>
   172   "named conclusion of rule cases"
   173 
   174 attribute_setup params =
   175   \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close>
   176   "named rule parameters"
   177 
   178 attribute_setup rule_format =
   179   \<open>Scan.lift (Args.mode "no_asm")
   180     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
   181   "result put into canonical rule format"
   182 
   183 attribute_setup elim_format =
   184   \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
   185   "destruct rule turned into elimination rule format"
   186 
   187 attribute_setup no_vars =
   188   \<open>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))\<close>
   193   "imported schematic variables"
   194 
   195 attribute_setup atomize =
   196   \<open>Scan.succeed Object_Logic.declare_atomize\<close>
   197   "declaration of atomize rule"
   198 
   199 attribute_setup rulify =
   200   \<open>Scan.succeed Object_Logic.declare_rulify\<close>
   201   "declaration of rulify rule"
   202 
   203 attribute_setup rotated =
   204   \<open>Scan.lift (Scan.optional Parse.int 1
   205     >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
   206   "rotated theorem premises"
   207 
   208 attribute_setup defn =
   209   \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
   210   "declaration of definitional transformations"
   211 
   212 attribute_setup abs_def =
   213   \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
   214     Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
   215   "abstract over free variables of definitional theorem"
   216 
   217 
   218 section \<open>Further content for the Pure theory\<close>
   219 
   220 subsection \<open>Meta-level connectives in assumptions\<close>
   221 
   222 lemma meta_mp:
   223   assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
   224   shows "PROP Q"
   225     by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
   226 
   227 lemmas meta_impE = meta_mp [elim_format]
   228 
   229 lemma meta_spec:
   230   assumes "\<And>x. PROP P x"
   231   shows "PROP P x"
   232     by (rule \<open>\<And>x. PROP P x\<close>)
   233 
   234 lemmas meta_allE = meta_spec [elim_format]
   235 
   236 lemma swap_params:
   237   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
   238 
   239 
   240 subsection \<open>Meta-level conjunction\<close>
   241 
   242 lemma all_conjunction:
   243   "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
   244 proof
   245   assume conj: "\<And>x. PROP A x &&& PROP B x"
   246   show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
   247   proof -
   248     fix x
   249     from conj show "PROP A x" by (rule conjunctionD1)
   250     from conj show "PROP B x" by (rule conjunctionD2)
   251   qed
   252 next
   253   assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
   254   fix x
   255   show "PROP A x &&& PROP B x"
   256   proof -
   257     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   258     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   259   qed
   260 qed
   261 
   262 lemma imp_conjunction:
   263   "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
   264 proof
   265   assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
   266   show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
   267   proof -
   268     assume "PROP A"
   269     from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
   270     from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
   271   qed
   272 next
   273   assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
   274   assume "PROP A"
   275   show "PROP B &&& PROP C"
   276   proof -
   277     from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
   278     from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
   279   qed
   280 qed
   281 
   282 lemma conjunction_imp:
   283   "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
   284 proof
   285   assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
   286   assume ab: "PROP A" "PROP B"
   287   show "PROP C"
   288   proof (rule r)
   289     from ab show "PROP A &&& PROP B" .
   290   qed
   291 next
   292   assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
   293   assume conj: "PROP A &&& PROP B"
   294   show "PROP C"
   295   proof (rule r)
   296     from conj show "PROP A" by (rule conjunctionD1)
   297     from conj show "PROP B" by (rule conjunctionD2)
   298   qed
   299 qed
   300 
   301 end