src/HOL/Inductive.thy
author wenzelm
Thu Oct 04 15:43:17 2001 +0200 (2001-10-04)
changeset 11688 56833637db2a
parent 11439 9aaab1a160a5
child 11825 ef7d619e2c88
permissions -rw-r--r--
generic induct_method.ML;
tuned;
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 {* Proof by cases and induction *}
wenzelm@11688
    21
wenzelm@11688
    22
text {* Proper handling of non-atomic rule statements. *}
wenzelm@10727
    23
wenzelm@10402
    24
constdefs
wenzelm@10402
    25
  forall :: "('a => bool) => bool"
wenzelm@10402
    26
  "forall P == \<forall>x. P x"
wenzelm@10402
    27
  implies :: "bool => bool => bool"
wenzelm@10402
    28
  "implies A B == A --> B"
wenzelm@10434
    29
  equal :: "'a => 'a => bool"
wenzelm@10434
    30
  "equal x y == x = y"
wenzelm@10727
    31
  conj :: "bool => bool => bool"
wenzelm@10727
    32
  "conj A B == A & B"
wenzelm@10402
    33
wenzelm@10402
    34
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
wenzelm@10434
    35
  by (simp only: atomize_all forall_def)
wenzelm@6437
    36
wenzelm@10402
    37
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
wenzelm@10434
    38
  by (simp only: atomize_imp implies_def)
wenzelm@10434
    39
wenzelm@10434
    40
lemma equal_eq: "(x == y) == Trueprop (equal x y)"
wenzelm@10434
    41
  by (simp only: atomize_eq equal_def)
wenzelm@10402
    42
wenzelm@10727
    43
lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
wenzelm@10727
    44
  by (unfold forall_def conj_def) blast
wenzelm@10727
    45
wenzelm@10727
    46
lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
wenzelm@10727
    47
  by (unfold implies_def conj_def) blast
wenzelm@10727
    48
wenzelm@10727
    49
lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
wenzelm@10727
    50
  by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
wenzelm@10434
    51
wenzelm@10434
    52
lemmas inductive_atomize = forall_eq implies_eq equal_eq
wenzelm@10434
    53
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
wenzelm@10727
    54
lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
wenzelm@10727
    55
lemmas inductive_conj = forall_conj implies_conj conj_curry
wenzelm@10727
    56
wenzelm@10727
    57
hide const forall implies equal conj
wenzelm@10727
    58
wenzelm@10727
    59
wenzelm@11688
    60
text {* Method setup. *}
wenzelm@11688
    61
wenzelm@11688
    62
ML {*
wenzelm@11688
    63
  structure InductMethod = InductMethodFun
wenzelm@11688
    64
  (struct
wenzelm@11688
    65
    val dest_concls = HOLogic.dest_concls;
wenzelm@11688
    66
    val cases_default = thm "case_split";
wenzelm@11688
    67
    val conjI = thm "conjI";
wenzelm@11688
    68
    val atomize = thms "inductive_atomize";
wenzelm@11688
    69
    val rulify1 = thms "inductive_rulify1";
wenzelm@11688
    70
    val rulify2 = thms "inductive_rulify2";
wenzelm@11688
    71
  end);
wenzelm@11688
    72
*}
wenzelm@11688
    73
wenzelm@11688
    74
setup InductMethod.setup
wenzelm@11688
    75
wenzelm@11688
    76
wenzelm@11688
    77
subsection {* Inductive sets *}
wenzelm@11688
    78
wenzelm@11688
    79
text {* Inversion of injective functions. *}
wenzelm@11436
    80
wenzelm@11436
    81
constdefs
wenzelm@11436
    82
  myinv :: "('a => 'b) => ('b => 'a)"
wenzelm@11436
    83
  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
wenzelm@11436
    84
wenzelm@11436
    85
lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
wenzelm@11436
    86
proof -
wenzelm@11436
    87
  assume "inj f"
wenzelm@11436
    88
  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
wenzelm@11436
    89
    by (simp only: inj_eq)
wenzelm@11436
    90
  also have "... = x" by (rule the_eq_trivial)
wenzelm@11439
    91
  finally show ?thesis by (unfold myinv_def)
wenzelm@11436
    92
qed
wenzelm@11436
    93
wenzelm@11436
    94
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
wenzelm@11436
    95
proof (unfold myinv_def)
wenzelm@11436
    96
  assume inj: "inj f"
wenzelm@11436
    97
  assume "y \<in> range f"
wenzelm@11436
    98
  then obtain x where "y = f x" ..
wenzelm@11436
    99
  hence x: "f x = y" ..
wenzelm@11436
   100
  thus "f (THE x. f x = y) = y"
wenzelm@11436
   101
  proof (rule theI)
wenzelm@11436
   102
    fix x' assume "f x' = y"
wenzelm@11436
   103
    with x have "f x' = f x" by simp
wenzelm@11436
   104
    with inj show "x' = x" by (rule injD)
wenzelm@11436
   105
  qed
wenzelm@11436
   106
qed
wenzelm@11436
   107
wenzelm@11436
   108
hide const myinv
wenzelm@11436
   109
wenzelm@11436
   110
wenzelm@11688
   111
text {* Package setup. *}
wenzelm@10402
   112
wenzelm@10402
   113
use "Tools/inductive_package.ML"
wenzelm@6437
   114
setup InductivePackage.setup
wenzelm@10402
   115
wenzelm@11688
   116
theorems basic_monos [mono] =
wenzelm@11688
   117
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
wenzelm@11688
   118
  Collect_mono in_mono vimage_mono
wenzelm@11688
   119
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
wenzelm@11688
   120
  not_all not_ex
wenzelm@11688
   121
  Ball_def Bex_def
wenzelm@11688
   122
  inductive_rulify2
wenzelm@11688
   123
wenzelm@11688
   124
wenzelm@11688
   125
subsubsection {* Inductive datatypes and primitive recursion *}
wenzelm@11688
   126
wenzelm@10402
   127
use "Tools/datatype_aux.ML"
wenzelm@10402
   128
use "Tools/datatype_prop.ML"
wenzelm@10402
   129
use "Tools/datatype_rep_proofs.ML"
wenzelm@10402
   130
use "Tools/datatype_abs_proofs.ML"
wenzelm@10402
   131
use "Tools/datatype_package.ML"
wenzelm@7700
   132
setup DatatypePackage.setup
wenzelm@10402
   133
wenzelm@10402
   134
use "Tools/primrec_package.ML"
berghofe@8482
   135
setup PrimrecPackage.setup
wenzelm@7700
   136
wenzelm@6437
   137
end