src/HOL/Inductive.thy
author haftmann
Tue Sep 19 15:22:35 2006 +0200 (2006-09-19)
changeset 20604 9dba9c7872c9
parent 19599 a5c7eb37d14f
child 21018 e6b8d6784792
permissions -rw-r--r--
added auxiliary lemma for code generation 2
wenzelm@7700
     1
(*  Title:      HOL/Inductive.thy
wenzelm@7700
     2
    ID:         $Id$
wenzelm@10402
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@11688
     4
*)
wenzelm@10727
     5
wenzelm@11688
     6
header {* Support for inductive sets and types *}
lcp@1187
     7
nipkow@15131
     8
theory Inductive 
avigad@17009
     9
imports FixedPoint Sum_Type Relation Record
haftmann@16417
    10
uses
wenzelm@10402
    11
  ("Tools/inductive_package.ML")
berghofe@13705
    12
  ("Tools/inductive_realizer.ML")
berghofe@12437
    13
  ("Tools/inductive_codegen.ML")
wenzelm@10402
    14
  ("Tools/datatype_aux.ML")
wenzelm@10402
    15
  ("Tools/datatype_prop.ML")
wenzelm@10402
    16
  ("Tools/datatype_rep_proofs.ML")
wenzelm@10402
    17
  ("Tools/datatype_abs_proofs.ML")
berghofe@13469
    18
  ("Tools/datatype_realizer.ML")
haftmann@19599
    19
  ("Tools/datatype_hooks.ML")
wenzelm@10402
    20
  ("Tools/datatype_package.ML")
berghofe@12437
    21
  ("Tools/datatype_codegen.ML")
berghofe@12437
    22
  ("Tools/recfun_codegen.ML")
nipkow@15131
    23
  ("Tools/primrec_package.ML")
nipkow@15131
    24
begin
wenzelm@10727
    25
wenzelm@11688
    26
subsection {* Inductive sets *}
wenzelm@11688
    27
wenzelm@11688
    28
text {* Inversion of injective functions. *}
wenzelm@11436
    29
wenzelm@11436
    30
constdefs
wenzelm@11436
    31
  myinv :: "('a => 'b) => ('b => 'a)"
wenzelm@11436
    32
  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
wenzelm@11436
    33
wenzelm@11436
    34
lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
wenzelm@11436
    35
proof -
wenzelm@11436
    36
  assume "inj f"
wenzelm@11436
    37
  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
wenzelm@11436
    38
    by (simp only: inj_eq)
wenzelm@11436
    39
  also have "... = x" by (rule the_eq_trivial)
wenzelm@11439
    40
  finally show ?thesis by (unfold myinv_def)
wenzelm@11436
    41
qed
wenzelm@11436
    42
wenzelm@11436
    43
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
wenzelm@11436
    44
proof (unfold myinv_def)
wenzelm@11436
    45
  assume inj: "inj f"
wenzelm@11436
    46
  assume "y \<in> range f"
wenzelm@11436
    47
  then obtain x where "y = f x" ..
wenzelm@11436
    48
  hence x: "f x = y" ..
wenzelm@11436
    49
  thus "f (THE x. f x = y) = y"
wenzelm@11436
    50
  proof (rule theI)
wenzelm@11436
    51
    fix x' assume "f x' = y"
wenzelm@11436
    52
    with x have "f x' = f x" by simp
wenzelm@11436
    53
    with inj show "x' = x" by (rule injD)
wenzelm@11436
    54
  qed
wenzelm@11436
    55
qed
wenzelm@11436
    56
wenzelm@11436
    57
hide const myinv
wenzelm@11436
    58
wenzelm@11436
    59
wenzelm@11688
    60
text {* Package setup. *}
wenzelm@10402
    61
wenzelm@10402
    62
use "Tools/inductive_package.ML"
wenzelm@6437
    63
setup InductivePackage.setup
wenzelm@10402
    64
wenzelm@11688
    65
theorems basic_monos [mono] =
wenzelm@11688
    66
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
wenzelm@11688
    67
  Collect_mono in_mono vimage_mono
wenzelm@11688
    68
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
wenzelm@11688
    69
  not_all not_ex
wenzelm@11688
    70
  Ball_def Bex_def
wenzelm@18456
    71
  induct_rulify_fallback
wenzelm@11688
    72
haftmann@20604
    73
lemma False_meta_all:
haftmann@20604
    74
  "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
haftmann@20604
    75
proof
haftmann@20604
    76
  fix P
haftmann@20604
    77
  assume False
haftmann@20604
    78
  then show P ..
haftmann@20604
    79
next
haftmann@20604
    80
  assume "\<And>P\<Colon>bool. P"
haftmann@20604
    81
  then show "False" ..
haftmann@20604
    82
qed
haftmann@20604
    83
haftmann@20604
    84
lemma not_eq_False:
haftmann@20604
    85
  assumes not_eq: "x \<noteq> y"
haftmann@20604
    86
  and eq: "x == y"
haftmann@20604
    87
  shows False
haftmann@20604
    88
  using not_eq eq by auto
haftmann@20604
    89
haftmann@20604
    90
lemmas not_eq_quodlibet =
haftmann@20604
    91
  not_eq_False [simplified False_meta_all]
haftmann@20604
    92
wenzelm@11688
    93
wenzelm@12023
    94
subsection {* Inductive datatypes and primitive recursion *}
wenzelm@11688
    95
wenzelm@11825
    96
text {* Package setup. *}
wenzelm@11825
    97
berghofe@12437
    98
use "Tools/recfun_codegen.ML"
berghofe@12437
    99
setup RecfunCodegen.setup
berghofe@12437
   100
wenzelm@10402
   101
use "Tools/datatype_aux.ML"
wenzelm@10402
   102
use "Tools/datatype_prop.ML"
wenzelm@10402
   103
use "Tools/datatype_rep_proofs.ML"
wenzelm@10402
   104
use "Tools/datatype_abs_proofs.ML"
berghofe@13469
   105
use "Tools/datatype_realizer.ML"
haftmann@19599
   106
haftmann@19599
   107
use "Tools/datatype_hooks.ML"
haftmann@19599
   108
setup DatatypeHooks.setup
haftmann@19599
   109
wenzelm@10402
   110
use "Tools/datatype_package.ML"
wenzelm@7700
   111
setup DatatypePackage.setup
wenzelm@10402
   112
berghofe@12437
   113
use "Tools/datatype_codegen.ML"
berghofe@12437
   114
setup DatatypeCodegen.setup
berghofe@12437
   115
berghofe@13705
   116
use "Tools/inductive_realizer.ML"
berghofe@13705
   117
setup InductiveRealizer.setup
berghofe@13705
   118
berghofe@12437
   119
use "Tools/inductive_codegen.ML"
berghofe@12437
   120
setup InductiveCodegen.setup
berghofe@12437
   121
wenzelm@10402
   122
use "Tools/primrec_package.ML"
wenzelm@7700
   123
wenzelm@6437
   124
end