src/HOL/Inductive.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24845 abcd15369ffa
child 24915 fc90277c0dd7
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/Inductive.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Support for inductive sets and types *}
     7 
     8 theory Inductive 
     9 imports FixedPoint Sum_Type
    10 uses
    11   ("Tools/inductive_package.ML")
    12   "Tools/dseq.ML"
    13   ("Tools/inductive_codegen.ML")
    14   ("Tools/datatype_aux.ML")
    15   ("Tools/datatype_prop.ML")
    16   ("Tools/datatype_rep_proofs.ML")
    17   ("Tools/datatype_abs_proofs.ML")
    18   ("Tools/datatype_case.ML")
    19   ("Tools/datatype_package.ML")
    20   ("Tools/primrec_package.ML")
    21 begin
    22 
    23 subsection {* Inductive predicates and sets *}
    24 
    25 text {* Inversion of injective functions. *}
    26 
    27 constdefs
    28   myinv :: "('a => 'b) => ('b => 'a)"
    29   "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
    30 
    31 lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
    32 proof -
    33   assume "inj f"
    34   hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
    35     by (simp only: inj_eq)
    36   also have "... = x" by (rule the_eq_trivial)
    37   finally show ?thesis by (unfold myinv_def)
    38 qed
    39 
    40 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
    41 proof (unfold myinv_def)
    42   assume inj: "inj f"
    43   assume "y \<in> range f"
    44   then obtain x where "y = f x" ..
    45   hence x: "f x = y" ..
    46   thus "f (THE x. f x = y) = y"
    47   proof (rule theI)
    48     fix x' assume "f x' = y"
    49     with x have "f x' = f x" by simp
    50     with inj show "x' = x" by (rule injD)
    51   qed
    52 qed
    53 
    54 hide const myinv
    55 
    56 
    57 text {* Package setup. *}
    58 
    59 theorems basic_monos =
    60   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    61   Collect_mono in_mono vimage_mono
    62   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    63   not_all not_ex
    64   Ball_def Bex_def
    65   induct_rulify_fallback
    66 
    67 use "Tools/inductive_package.ML"
    68 setup InductivePackage.setup
    69 
    70 theorems [mono] =
    71   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    72   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    73   not_all not_ex
    74   Ball_def Bex_def
    75   induct_rulify_fallback
    76 
    77 lemma False_meta_all:
    78   "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
    79 proof
    80   fix P
    81   assume False
    82   then show P ..
    83 next
    84   assume "\<And>P\<Colon>bool. P"
    85   then show False .
    86 qed
    87 
    88 lemma not_eq_False:
    89   assumes not_eq: "x \<noteq> y"
    90   and eq: "x \<equiv> y"
    91   shows False
    92   using not_eq eq by auto
    93 
    94 lemmas not_eq_quodlibet =
    95   not_eq_False [simplified False_meta_all]
    96 
    97 
    98 subsection {* Inductive datatypes and primitive recursion *}
    99 
   100 text {* Package setup. *}
   101 
   102 use "Tools/datatype_aux.ML"
   103 use "Tools/datatype_prop.ML"
   104 use "Tools/datatype_rep_proofs.ML"
   105 use "Tools/datatype_abs_proofs.ML"
   106 use "Tools/datatype_case.ML"
   107 use "Tools/datatype_package.ML"
   108 setup DatatypePackage.setup
   109 use "Tools/primrec_package.ML"
   110 
   111 use "Tools/inductive_codegen.ML"
   112 setup InductiveCodegen.setup
   113 
   114 text{* Lambda-abstractions with pattern matching: *}
   115 
   116 syntax
   117   "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
   118 syntax (xsymbols)
   119   "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
   120 
   121 parse_translation (advanced) {*
   122 let
   123   fun fun_tr ctxt [cs] =
   124     let
   125       val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
   126       val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
   127                  ctxt [x, cs]
   128     in lambda x ft end
   129 in [("_lam_pats_syntax", fun_tr)] end
   130 *}
   131 
   132 end