src/HOL/Inductive.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10434 6ea4735c3955
child 10727 2ccafccb81c0
permissions -rw-r--r--
hide many names from Datatype_Universe.
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$
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     4
*)
1187
bc94f00e47ba Includes Sum.thy as a parent for mutual recursion
lcp
parents: 923
diff changeset
     5
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 8482
diff changeset
     6
theory Inductive = Gfp + Sum_Type + NatDef
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     7
files
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
     8
  ("Tools/induct_method.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
     9
  ("Tools/inductive_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    10
  ("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    11
  ("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    12
  ("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    13
  ("Tools/datatype_abs_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    14
  ("Tools/datatype_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    15
  ("Tools/primrec_package.ML"):
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    16
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    17
constdefs
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    18
  forall :: "('a => bool) => bool"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    19
  "forall P == \<forall>x. P x"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    20
  implies :: "bool => bool => bool"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    21
  "implies A B == A --> B"
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    22
  equal :: "'a => 'a => bool"
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    23
  "equal x y == x = y"
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    24
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    25
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    26
  by (simp only: atomize_all forall_def)
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    27
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    28
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    29
  by (simp only: atomize_imp implies_def)
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    30
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    31
lemma equal_eq: "(x == y) == Trueprop (equal x y)"
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    32
  by (simp only: atomize_eq equal_def)
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    33
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    34
hide const forall implies equal
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    35
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    36
lemmas inductive_atomize = forall_eq implies_eq equal_eq
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    37
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    38
lemmas inductive_rulify2 = forall_def implies_def equal_def
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    39
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    40
use "Tools/induct_method.ML"
8303
5e7037409118 early setup of induct_method;
wenzelm
parents: 7710
diff changeset
    41
setup InductMethod.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    42
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    43
use "Tools/inductive_package.ML"
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    44
setup InductivePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    45
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    46
use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    47
use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    48
use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    49
use "Tools/datatype_abs_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    50
use "Tools/datatype_package.ML"
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    51
setup DatatypePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    52
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    53
use "Tools/primrec_package.ML"
8482
bbc805ebc904 Added setup for primrec theory data.
berghofe
parents: 8343
diff changeset
    54
setup PrimrecPackage.setup
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    55
10312
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    56
theorems basic_monos [mono] =
7710
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    57
   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
    58
   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
    59
   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
    60
   not_all not_ex
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents: 7700
diff changeset
    61
   Ball_def Bex_def
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    62
10312
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    63
(*belongs to theory Transitive_Closure*)
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    64
declare rtrancl_induct [induct set: rtrancl]
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    65
declare rtranclE [cases set: rtrancl]
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    66
declare trancl_induct [induct set: trancl]
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    67
declare tranclE [cases set: trancl]
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    68
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    69
end