src/HOL/Inductive.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 13705 934d6c1421f2
child 15131 c69542757a4d
permissions -rw-r--r--
Merged in license change from Isabelle2004
     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 = Gfp + Sum_Type + Relation + Record
     9 files
    10   ("Tools/inductive_package.ML")
    11   ("Tools/inductive_realizer.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_realizer.ML")
    18   ("Tools/datatype_package.ML")
    19   ("Tools/datatype_codegen.ML")
    20   ("Tools/recfun_codegen.ML")
    21   ("Tools/primrec_package.ML"):
    22 
    23 
    24 subsection {* Inductive sets *}
    25 
    26 text {* Inversion of injective functions. *}
    27 
    28 constdefs
    29   myinv :: "('a => 'b) => ('b => 'a)"
    30   "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
    31 
    32 lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
    33 proof -
    34   assume "inj f"
    35   hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
    36     by (simp only: inj_eq)
    37   also have "... = x" by (rule the_eq_trivial)
    38   finally show ?thesis by (unfold myinv_def)
    39 qed
    40 
    41 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
    42 proof (unfold myinv_def)
    43   assume inj: "inj f"
    44   assume "y \<in> range f"
    45   then obtain x where "y = f x" ..
    46   hence x: "f x = y" ..
    47   thus "f (THE x. f x = y) = y"
    48   proof (rule theI)
    49     fix x' assume "f x' = y"
    50     with x have "f x' = f x" by simp
    51     with inj show "x' = x" by (rule injD)
    52   qed
    53 qed
    54 
    55 hide const myinv
    56 
    57 
    58 text {* Package setup. *}
    59 
    60 use "Tools/inductive_package.ML"
    61 setup InductivePackage.setup
    62 
    63 theorems basic_monos [mono] =
    64   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    65   Collect_mono in_mono vimage_mono
    66   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    67   not_all not_ex
    68   Ball_def Bex_def
    69   induct_rulify2
    70 
    71 
    72 subsection {* Inductive datatypes and primitive recursion *}
    73 
    74 text {* Package setup. *}
    75 
    76 use "Tools/recfun_codegen.ML"
    77 setup RecfunCodegen.setup
    78 
    79 use "Tools/datatype_aux.ML"
    80 use "Tools/datatype_prop.ML"
    81 use "Tools/datatype_rep_proofs.ML"
    82 use "Tools/datatype_abs_proofs.ML"
    83 use "Tools/datatype_realizer.ML"
    84 use "Tools/datatype_package.ML"
    85 setup DatatypePackage.setup
    86 
    87 use "Tools/datatype_codegen.ML"
    88 setup DatatypeCodegen.setup
    89 
    90 use "Tools/inductive_realizer.ML"
    91 setup InductiveRealizer.setup
    92 
    93 use "Tools/inductive_codegen.ML"
    94 setup InductiveCodegen.setup
    95 
    96 use "Tools/primrec_package.ML"
    97 
    98 end