src/HOL/Inductive.thy
author wenzelm
Wed Oct 31 01:21:01 2001 +0100 (2001-10-31)
changeset 11990 c1daefc08eff
parent 11825 ef7d619e2c88
child 12023 d982f98e0f0d
permissions -rw-r--r--
use induct_rulify2;
wenzelm@7700
     1
(*  Title:      HOL/Inductive.thy
wenzelm@7700
     2
    ID:         $Id$
wenzelm@10402
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10727
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@11688
     5
*)
wenzelm@10727
     6
wenzelm@11688
     7
header {* Support for inductive sets and types *}
lcp@1187
     8
berghofe@11325
     9
theory Inductive = Gfp + Sum_Type + Relation
wenzelm@7700
    10
files
wenzelm@10402
    11
  ("Tools/inductive_package.ML")
wenzelm@10402
    12
  ("Tools/datatype_aux.ML")
wenzelm@10402
    13
  ("Tools/datatype_prop.ML")
wenzelm@10402
    14
  ("Tools/datatype_rep_proofs.ML")
wenzelm@10402
    15
  ("Tools/datatype_abs_proofs.ML")
wenzelm@10402
    16
  ("Tools/datatype_package.ML")
wenzelm@10402
    17
  ("Tools/primrec_package.ML"):
wenzelm@10402
    18
wenzelm@10727
    19
wenzelm@11688
    20
subsection {* Inductive sets *}
wenzelm@11688
    21
wenzelm@11688
    22
text {* Inversion of injective functions. *}
wenzelm@11436
    23
wenzelm@11436
    24
constdefs
wenzelm@11436
    25
  myinv :: "('a => 'b) => ('b => 'a)"
wenzelm@11436
    26
  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
wenzelm@11436
    27
wenzelm@11436
    28
lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
wenzelm@11436
    29
proof -
wenzelm@11436
    30
  assume "inj f"
wenzelm@11436
    31
  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
wenzelm@11436
    32
    by (simp only: inj_eq)
wenzelm@11436
    33
  also have "... = x" by (rule the_eq_trivial)
wenzelm@11439
    34
  finally show ?thesis by (unfold myinv_def)
wenzelm@11436
    35
qed
wenzelm@11436
    36
wenzelm@11436
    37
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
wenzelm@11436
    38
proof (unfold myinv_def)
wenzelm@11436
    39
  assume inj: "inj f"
wenzelm@11436
    40
  assume "y \<in> range f"
wenzelm@11436
    41
  then obtain x where "y = f x" ..
wenzelm@11436
    42
  hence x: "f x = y" ..
wenzelm@11436
    43
  thus "f (THE x. f x = y) = y"
wenzelm@11436
    44
  proof (rule theI)
wenzelm@11436
    45
    fix x' assume "f x' = y"
wenzelm@11436
    46
    with x have "f x' = f x" by simp
wenzelm@11436
    47
    with inj show "x' = x" by (rule injD)
wenzelm@11436
    48
  qed
wenzelm@11436
    49
qed
wenzelm@11436
    50
wenzelm@11436
    51
hide const myinv
wenzelm@11436
    52
wenzelm@11436
    53
wenzelm@11688
    54
text {* Package setup. *}
wenzelm@10402
    55
wenzelm@10402
    56
use "Tools/inductive_package.ML"
wenzelm@6437
    57
setup InductivePackage.setup
wenzelm@10402
    58
wenzelm@11688
    59
theorems basic_monos [mono] =
wenzelm@11688
    60
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
wenzelm@11688
    61
  Collect_mono in_mono vimage_mono
wenzelm@11688
    62
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
wenzelm@11688
    63
  not_all not_ex
wenzelm@11688
    64
  Ball_def Bex_def
wenzelm@11990
    65
  induct_rulify2
wenzelm@11688
    66
wenzelm@11688
    67
wenzelm@11688
    68
subsubsection {* Inductive datatypes and primitive recursion *}
wenzelm@11688
    69
wenzelm@11825
    70
text {* Package setup. *}
wenzelm@11825
    71
wenzelm@10402
    72
use "Tools/datatype_aux.ML"
wenzelm@10402
    73
use "Tools/datatype_prop.ML"
wenzelm@10402
    74
use "Tools/datatype_rep_proofs.ML"
wenzelm@10402
    75
use "Tools/datatype_abs_proofs.ML"
wenzelm@10402
    76
use "Tools/datatype_package.ML"
wenzelm@7700
    77
setup DatatypePackage.setup
wenzelm@10402
    78
wenzelm@10402
    79
use "Tools/primrec_package.ML"
berghofe@8482
    80
setup PrimrecPackage.setup
wenzelm@7700
    81
wenzelm@6437
    82
end