src/HOL/Inductive.thy
author wenzelm
Mon Nov 06 22:49:16 2000 +0100 (2000-11-06)
changeset 10402 5e82d6cafb5f
parent 10312 4c5a03649af7
child 10434 6ea4735c3955
permissions -rw-r--r--
inductive_atomize, inductive_rulify;
wenzelm@7700
     1
(*  Title:      HOL/Inductive.thy
wenzelm@7700
     2
    ID:         $Id$
wenzelm@10402
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@7700
     4
*)
lcp@1187
     5
nipkow@10212
     6
theory Inductive = Gfp + Sum_Type + NatDef
wenzelm@7700
     7
files
wenzelm@10402
     8
  ("Tools/induct_method.ML")
wenzelm@10402
     9
  ("Tools/inductive_package.ML")
wenzelm@10402
    10
  ("Tools/datatype_aux.ML")
wenzelm@10402
    11
  ("Tools/datatype_prop.ML")
wenzelm@10402
    12
  ("Tools/datatype_rep_proofs.ML")
wenzelm@10402
    13
  ("Tools/datatype_abs_proofs.ML")
wenzelm@10402
    14
  ("Tools/datatype_package.ML")
wenzelm@10402
    15
  ("Tools/primrec_package.ML"):
wenzelm@10402
    16
wenzelm@10402
    17
constdefs
wenzelm@10402
    18
  forall :: "('a => bool) => bool"
wenzelm@10402
    19
  "forall P == \<forall>x. P x"
wenzelm@10402
    20
  implies :: "bool => bool => bool"
wenzelm@10402
    21
  "implies A B == A --> B"
wenzelm@10402
    22
wenzelm@10402
    23
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
wenzelm@10402
    24
proof
wenzelm@10402
    25
  assume "!!x. P x"
wenzelm@10402
    26
  thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast
wenzelm@10402
    27
next
wenzelm@10402
    28
  fix x
wenzelm@10402
    29
  assume "forall (\<lambda>x. P x)"
wenzelm@10402
    30
  thus "P x" by (unfold forall_def) blast
wenzelm@10402
    31
qed
wenzelm@6437
    32
wenzelm@10402
    33
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
wenzelm@10402
    34
proof
wenzelm@10402
    35
  assume "A ==> B"
wenzelm@10402
    36
  thus "implies A B" by (unfold implies_def) blast
wenzelm@10402
    37
next
wenzelm@10402
    38
  assume "implies A B" and A
wenzelm@10402
    39
  thus B by (unfold implies_def) blast
wenzelm@10402
    40
qed
wenzelm@10402
    41
wenzelm@10402
    42
lemmas inductive_atomize = forall_eq implies_eq
wenzelm@10402
    43
lemmas inductive_rulify = inductive_atomize [symmetric, standard]
wenzelm@10402
    44
hide const forall implies
wenzelm@10402
    45
wenzelm@10402
    46
use "Tools/induct_method.ML"
wenzelm@8303
    47
setup InductMethod.setup
wenzelm@10402
    48
wenzelm@10402
    49
use "Tools/inductive_package.ML"
wenzelm@6437
    50
setup InductivePackage.setup
wenzelm@10402
    51
wenzelm@10402
    52
use "Tools/datatype_aux.ML"
wenzelm@10402
    53
use "Tools/datatype_prop.ML"
wenzelm@10402
    54
use "Tools/datatype_rep_proofs.ML"
wenzelm@10402
    55
use "Tools/datatype_abs_proofs.ML"
wenzelm@10402
    56
use "Tools/datatype_package.ML"
wenzelm@7700
    57
setup DatatypePackage.setup
wenzelm@10402
    58
wenzelm@10402
    59
use "Tools/primrec_package.ML"
berghofe@8482
    60
setup PrimrecPackage.setup
wenzelm@7700
    61
wenzelm@10312
    62
theorems basic_monos [mono] =
berghofe@7710
    63
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
berghofe@7710
    64
   Collect_mono in_mono vimage_mono
berghofe@7710
    65
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
berghofe@7710
    66
   not_all not_ex
berghofe@7710
    67
   Ball_def Bex_def
wenzelm@6437
    68
wenzelm@10312
    69
(*belongs to theory Transitive_Closure*)
wenzelm@10312
    70
declare rtrancl_induct [induct set: rtrancl]
wenzelm@10312
    71
declare rtranclE [cases set: rtrancl]
wenzelm@10312
    72
declare trancl_induct [induct set: trancl]
wenzelm@10312
    73
declare tranclE [cases set: trancl]
wenzelm@10312
    74
wenzelm@6437
    75
end