src/HOL/Inductive.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8482 bbc805ebc904
child 10212 33fe2d701ddd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     1
(*  Title:      HOL/Inductive.thy
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     2
    ID:         $Id$
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     3
*)
1187
bc94f00e47ba Includes Sum.thy as a parent for mutual recursion
lcp
parents: 923
diff changeset
     4
8343
fb604f0e5640 require NatDef;
wenzelm
parents: 8303
diff changeset
     5
theory Inductive = Gfp + Prod + Sum + NatDef
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     6
files
8303
5e7037409118 early setup of induct_method;
wenzelm
parents: 7710
diff changeset
     7
  "Tools/induct_method.ML"
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     8
  "Tools/inductive_package.ML"
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     9
  "Tools/datatype_aux.ML"
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    10
  "Tools/datatype_prop.ML"
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    11
  "Tools/datatype_rep_proofs.ML"
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    12
  "Tools/datatype_abs_proofs.ML"
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    13
  "Tools/datatype_package.ML"
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    14
  "Tools/primrec_package.ML":
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    15
8303
5e7037409118 early setup of induct_method;
wenzelm
parents: 7710
diff changeset
    16
setup InductMethod.setup
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    17
setup InductivePackage.setup
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    18
setup DatatypePackage.setup
8482
bbc805ebc904 Added setup for primrec theory data.
berghofe
parents: 8343
diff changeset
    19
setup PrimrecPackage.setup
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    20
7710
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    21
theorems [mono] =
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    22
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    23
   Collect_mono in_mono vimage_mono
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    24
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    25
   not_all not_ex
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    26
   Ball_def Bex_def
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    27
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    28
end