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