src/HOL/Inductive.thy
author berghofe
Mon Dec 10 15:17:49 2001 +0100 (2001-12-10)
changeset 12437 6d4e02b6dd43
parent 12023 d982f98e0f0d
child 12920 32292d83367b
permissions -rw-r--r--
Moved code generator setup from Recdef to Inductive.
     1 (*  Title:      HOL/Inductive.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Support for inductive sets and types *}
     8 
     9 theory Inductive = Gfp + Sum_Type + Relation
    10 files
    11   ("Tools/inductive_package.ML")
    12   ("Tools/inductive_codegen.ML")
    13   ("Tools/datatype_aux.ML")
    14   ("Tools/datatype_prop.ML")
    15   ("Tools/datatype_rep_proofs.ML")
    16   ("Tools/datatype_abs_proofs.ML")
    17   ("Tools/datatype_package.ML")
    18   ("Tools/datatype_codegen.ML")
    19   ("Tools/recfun_codegen.ML")
    20   ("Tools/primrec_package.ML"):
    21 
    22 
    23 subsection {* Inductive 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 use "Tools/inductive_package.ML"
    60 setup InductivePackage.setup
    61 
    62 theorems basic_monos [mono] =
    63   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    64   Collect_mono in_mono vimage_mono
    65   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    66   not_all not_ex
    67   Ball_def Bex_def
    68   induct_rulify2
    69 
    70 
    71 subsection {* Inductive datatypes and primitive recursion *}
    72 
    73 text {* Package setup. *}
    74 
    75 use "Tools/recfun_codegen.ML"
    76 setup RecfunCodegen.setup
    77 
    78 use "Tools/datatype_aux.ML"
    79 use "Tools/datatype_prop.ML"
    80 use "Tools/datatype_rep_proofs.ML"
    81 use "Tools/datatype_abs_proofs.ML"
    82 use "Tools/datatype_package.ML"
    83 setup DatatypePackage.setup
    84 
    85 use "Tools/datatype_codegen.ML"
    86 setup DatatypeCodegen.setup
    87 
    88 use "Tools/inductive_codegen.ML"
    89 setup InductiveCodegen.setup
    90 
    91 use "Tools/primrec_package.ML"
    92 
    93 end