src/HOL/Inductive.thy
author haftmann
Tue Sep 25 12:16:08 2007 +0200 (2007-09-25)
changeset 24699 c6674504103f
parent 24626 85eceef2edc7
child 24720 4d2f2e375fa1
permissions -rw-r--r--
datatype interpretators for size and datatype_realizer
     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/inductive_set_package.ML")
    13   ("Tools/inductive_realizer.ML")*)
    14   "Tools/dseq.ML"
    15   ("Tools/inductive_codegen.ML")
    16   ("Tools/datatype_aux.ML")
    17   ("Tools/datatype_prop.ML")
    18   ("Tools/datatype_rep_proofs.ML")
    19   ("Tools/datatype_abs_proofs.ML")
    20   ("Tools/datatype_case.ML")
    21   ("Tools/datatype_package.ML")
    22   ("Tools/datatype_codegen.ML")
    23   ("Tools/primrec_package.ML")
    24 begin
    25 
    26 subsection {* Inductive predicates and sets *}
    27 
    28 text {* Inversion of injective functions. *}
    29 
    30 constdefs
    31   myinv :: "('a => 'b) => ('b => 'a)"
    32   "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
    33 
    34 lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
    35 proof -
    36   assume "inj f"
    37   hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
    38     by (simp only: inj_eq)
    39   also have "... = x" by (rule the_eq_trivial)
    40   finally show ?thesis by (unfold myinv_def)
    41 qed
    42 
    43 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
    44 proof (unfold myinv_def)
    45   assume inj: "inj f"
    46   assume "y \<in> range f"
    47   then obtain x where "y = f x" ..
    48   hence x: "f x = y" ..
    49   thus "f (THE x. f x = y) = y"
    50   proof (rule theI)
    51     fix x' assume "f x' = y"
    52     with x have "f x' = f x" by simp
    53     with inj show "x' = x" by (rule injD)
    54   qed
    55 qed
    56 
    57 hide const myinv
    58 
    59 
    60 text {* Package setup. *}
    61 
    62 theorems basic_monos =
    63   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    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_rulify_fallback
    69 
    70 use "Tools/inductive_package.ML"
    71 setup InductivePackage.setup
    72 
    73 theorems [mono] =
    74   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    75   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    76   not_all not_ex
    77   Ball_def Bex_def
    78   induct_rulify_fallback
    79 
    80 lemma False_meta_all:
    81   "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
    82 proof
    83   fix P
    84   assume False
    85   then show P ..
    86 next
    87   assume "\<And>P\<Colon>bool. P"
    88   then show False .
    89 qed
    90 
    91 lemma not_eq_False:
    92   assumes not_eq: "x \<noteq> y"
    93   and eq: "x \<equiv> y"
    94   shows False
    95   using not_eq eq by auto
    96 
    97 lemmas not_eq_quodlibet =
    98   not_eq_False [simplified False_meta_all]
    99 
   100 
   101 subsection {* Inductive datatypes and primitive recursion *}
   102 
   103 text {* Package setup. *}
   104 
   105 use "Tools/datatype_aux.ML"
   106 use "Tools/datatype_prop.ML"
   107 use "Tools/datatype_rep_proofs.ML"
   108 use "Tools/datatype_abs_proofs.ML"
   109 use "Tools/datatype_case.ML"
   110 use "Tools/datatype_package.ML"
   111 setup DatatypePackage.setup
   112 use "Tools/primrec_package.ML"
   113 use "Tools/datatype_codegen.ML"
   114 setup DatatypeCodegen.setup
   115 
   116 use "Tools/inductive_codegen.ML"
   117 setup InductiveCodegen.setup
   118 
   119 text{* Lambda-abstractions with pattern matching: *}
   120 
   121 syntax
   122   "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
   123 syntax (xsymbols)
   124   "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
   125 
   126 parse_translation (advanced) {*
   127 let
   128   fun fun_tr ctxt [cs] =
   129     let
   130       val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
   131       val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
   132                  ctxt [x, cs]
   133     in lambda x ft end
   134 in [("_lam_pats_syntax", fun_tr)] end
   135 *}
   136 
   137 end