src/HOL/Inductive.thy
author wenzelm
Mon May 07 00:49:59 2007 +0200 (2007-05-07)
changeset 22846 fb79144af9a3
parent 22783 e5f947e0ade8
child 22886 cdff6ef76009
permissions -rw-r--r--
simplified DataFun interfaces;
     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 Relation Record
    10 uses
    11   ("Tools/inductive_package.ML")
    12   ("Tools/old_inductive_package.ML")
    13   ("Tools/inductive_realizer.ML")
    14   ("Tools/inductive_codegen.ML")
    15   ("Tools/datatype_aux.ML")
    16   ("Tools/datatype_prop.ML")
    17   ("Tools/datatype_rep_proofs.ML")
    18   ("Tools/datatype_abs_proofs.ML")
    19   ("Tools/datatype_realizer.ML")
    20   ("Tools/datatype_hooks.ML")
    21   ("Tools/datatype_case.ML")
    22   ("Tools/datatype_package.ML")
    23   ("Tools/datatype_codegen.ML")
    24   ("Tools/recfun_codegen.ML")
    25   ("Tools/primrec_package.ML")
    26 begin
    27 
    28 subsection {* Inductive sets *}
    29 
    30 text {* Inversion of injective functions. *}
    31 
    32 constdefs
    33   myinv :: "('a => 'b) => ('b => 'a)"
    34   "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
    35 
    36 lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
    37 proof -
    38   assume "inj f"
    39   hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
    40     by (simp only: inj_eq)
    41   also have "... = x" by (rule the_eq_trivial)
    42   finally show ?thesis by (unfold myinv_def)
    43 qed
    44 
    45 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
    46 proof (unfold myinv_def)
    47   assume inj: "inj f"
    48   assume "y \<in> range f"
    49   then obtain x where "y = f x" ..
    50   hence x: "f x = y" ..
    51   thus "f (THE x. f x = y) = y"
    52   proof (rule theI)
    53     fix x' assume "f x' = y"
    54     with x have "f x' = f x" by simp
    55     with inj show "x' = x" by (rule injD)
    56   qed
    57 qed
    58 
    59 hide const myinv
    60 
    61 
    62 text {* Package setup. *}
    63 
    64 use "Tools/old_inductive_package.ML"
    65 setup OldInductivePackage.setup
    66 
    67 theorems basic_monos [mono] =
    68   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    69   Collect_mono in_mono vimage_mono
    70   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    71   not_all not_ex
    72   Ball_def Bex_def
    73   induct_rulify_fallback
    74 
    75 use "Tools/inductive_package.ML"
    76 setup InductivePackage.setup
    77 
    78 theorems [mono2] =
    79   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    80   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    81   not_all not_ex
    82   Ball_def Bex_def
    83   induct_rulify_fallback
    84 
    85 lemma False_meta_all:
    86   "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
    87 proof
    88   fix P
    89   assume False
    90   then show P ..
    91 next
    92   assume "\<And>P\<Colon>bool. P"
    93   then show "False" ..
    94 qed
    95 
    96 lemma not_eq_False:
    97   assumes not_eq: "x \<noteq> y"
    98   and eq: "x == y"
    99   shows False
   100   using not_eq eq by auto
   101 
   102 lemmas not_eq_quodlibet =
   103   not_eq_False [simplified False_meta_all]
   104 
   105 
   106 subsection {* Inductive datatypes and primitive recursion *}
   107 
   108 text {* Package setup. *}
   109 
   110 use "Tools/recfun_codegen.ML"
   111 setup RecfunCodegen.setup
   112 
   113 use "Tools/datatype_aux.ML"
   114 use "Tools/datatype_prop.ML"
   115 use "Tools/datatype_rep_proofs.ML"
   116 use "Tools/datatype_abs_proofs.ML"
   117 use "Tools/datatype_case.ML"
   118 use "Tools/datatype_realizer.ML"
   119 
   120 use "Tools/datatype_hooks.ML"
   121 
   122 use "Tools/datatype_package.ML"
   123 setup DatatypePackage.setup
   124 
   125 use "Tools/datatype_codegen.ML"
   126 setup DatatypeCodegen.setup
   127 
   128 use "Tools/inductive_realizer.ML"
   129 setup InductiveRealizer.setup
   130 
   131 use "Tools/inductive_codegen.ML"
   132 setup InductiveCodegen.setup
   133 
   134 use "Tools/primrec_package.ML"
   135 
   136 end