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