src/HOL/Inductive.thy
author wenzelm
Fri Jul 20 22:00:06 2001 +0200 (2001-07-20)
changeset 11436 3f74b80d979f
parent 11325 a5e0289dd56c
child 11439 9aaab1a160a5
permissions -rw-r--r--
private "myinv" (uses "The" instead of "Eps");
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@10727
     5
wenzelm@10727
     6
Setup packages for inductive sets and types etc.
wenzelm@7700
     7
*)
lcp@1187
     8
berghofe@11325
     9
theory Inductive = Gfp + Sum_Type + Relation
wenzelm@7700
    10
files
wenzelm@10402
    11
  ("Tools/induct_method.ML")
wenzelm@10402
    12
  ("Tools/inductive_package.ML")
wenzelm@10402
    13
  ("Tools/datatype_aux.ML")
wenzelm@10402
    14
  ("Tools/datatype_prop.ML")
wenzelm@10402
    15
  ("Tools/datatype_rep_proofs.ML")
wenzelm@10402
    16
  ("Tools/datatype_abs_proofs.ML")
wenzelm@10402
    17
  ("Tools/datatype_package.ML")
wenzelm@10402
    18
  ("Tools/primrec_package.ML"):
wenzelm@10402
    19
wenzelm@10727
    20
wenzelm@10727
    21
(* handling of proper rules *)
wenzelm@10727
    22
wenzelm@10402
    23
constdefs
wenzelm@10402
    24
  forall :: "('a => bool) => bool"
wenzelm@10402
    25
  "forall P == \<forall>x. P x"
wenzelm@10402
    26
  implies :: "bool => bool => bool"
wenzelm@10402
    27
  "implies A B == A --> B"
wenzelm@10434
    28
  equal :: "'a => 'a => bool"
wenzelm@10434
    29
  "equal x y == x = y"
wenzelm@10727
    30
  conj :: "bool => bool => bool"
wenzelm@10727
    31
  "conj A B == A & B"
wenzelm@10402
    32
wenzelm@10402
    33
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
wenzelm@10434
    34
  by (simp only: atomize_all forall_def)
wenzelm@6437
    35
wenzelm@10402
    36
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
wenzelm@10434
    37
  by (simp only: atomize_imp implies_def)
wenzelm@10434
    38
wenzelm@10434
    39
lemma equal_eq: "(x == y) == Trueprop (equal x y)"
wenzelm@10434
    40
  by (simp only: atomize_eq equal_def)
wenzelm@10402
    41
wenzelm@10727
    42
lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
wenzelm@10727
    43
  by (unfold forall_def conj_def) blast
wenzelm@10727
    44
wenzelm@10727
    45
lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
wenzelm@10727
    46
  by (unfold implies_def conj_def) blast
wenzelm@10727
    47
wenzelm@10727
    48
lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
wenzelm@10727
    49
  by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
wenzelm@10434
    50
wenzelm@10434
    51
lemmas inductive_atomize = forall_eq implies_eq equal_eq
wenzelm@10434
    52
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
wenzelm@10727
    53
lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
wenzelm@10727
    54
lemmas inductive_conj = forall_conj implies_conj conj_curry
wenzelm@10727
    55
wenzelm@10727
    56
hide const forall implies equal conj
wenzelm@10727
    57
wenzelm@10727
    58
wenzelm@11436
    59
(* inversion of injective functions *)
wenzelm@11436
    60
wenzelm@11436
    61
constdefs
wenzelm@11436
    62
  myinv :: "('a => 'b) => ('b => 'a)"
wenzelm@11436
    63
  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
wenzelm@11436
    64
wenzelm@11436
    65
lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
wenzelm@11436
    66
proof -
wenzelm@11436
    67
  assume "inj f"
wenzelm@11436
    68
  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
wenzelm@11436
    69
    by (simp only: inj_eq)
wenzelm@11436
    70
  also have "... = x" by (rule the_eq_trivial)
wenzelm@11436
    71
  finally (trans) show ?thesis by (unfold myinv_def)
wenzelm@11436
    72
qed
wenzelm@11436
    73
wenzelm@11436
    74
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
wenzelm@11436
    75
proof (unfold myinv_def)
wenzelm@11436
    76
  assume inj: "inj f"
wenzelm@11436
    77
  assume "y \<in> range f"
wenzelm@11436
    78
  then obtain x where "y = f x" ..
wenzelm@11436
    79
  hence x: "f x = y" ..
wenzelm@11436
    80
  thus "f (THE x. f x = y) = y"
wenzelm@11436
    81
  proof (rule theI)
wenzelm@11436
    82
    fix x' assume "f x' = y"
wenzelm@11436
    83
    with x have "f x' = f x" by simp
wenzelm@11436
    84
    with inj show "x' = x" by (rule injD)
wenzelm@11436
    85
  qed
wenzelm@11436
    86
qed
wenzelm@11436
    87
wenzelm@11436
    88
hide const myinv
wenzelm@11436
    89
wenzelm@11436
    90
wenzelm@10727
    91
(* setup packages *)
wenzelm@10402
    92
wenzelm@10402
    93
use "Tools/induct_method.ML"
wenzelm@8303
    94
setup InductMethod.setup
wenzelm@10402
    95
wenzelm@10402
    96
use "Tools/inductive_package.ML"
wenzelm@6437
    97
setup InductivePackage.setup
wenzelm@10402
    98
wenzelm@10402
    99
use "Tools/datatype_aux.ML"
wenzelm@10402
   100
use "Tools/datatype_prop.ML"
wenzelm@10402
   101
use "Tools/datatype_rep_proofs.ML"
wenzelm@10402
   102
use "Tools/datatype_abs_proofs.ML"
wenzelm@10402
   103
use "Tools/datatype_package.ML"
wenzelm@7700
   104
setup DatatypePackage.setup
wenzelm@10402
   105
wenzelm@10402
   106
use "Tools/primrec_package.ML"
berghofe@8482
   107
setup PrimrecPackage.setup
wenzelm@7700
   108
wenzelm@10312
   109
theorems basic_monos [mono] =
oheimb@11003
   110
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
wenzelm@10727
   111
  Collect_mono in_mono vimage_mono
wenzelm@10727
   112
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
wenzelm@10727
   113
  not_all not_ex
wenzelm@10727
   114
  Ball_def Bex_def
wenzelm@10727
   115
  inductive_rulify2
wenzelm@10727
   116
wenzelm@6437
   117
end