src/HOL/Inductive.thy
author berghofe
Tue, 22 May 2001 15:10:06 +0200
changeset 11325 a5e0289dd56c
parent 11003 ee0838d89deb
child 11436 3f74b80d979f
permissions -rw-r--r--
Inductive definitions are now introduced earlier in the theory hierarchy.
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
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
     5
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
     6
Setup packages for inductive sets and types etc.
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     7
*)
1187
bc94f00e47ba Includes Sum.thy as a parent for mutual recursion
lcp
parents: 923
diff changeset
     8
11325
a5e0289dd56c Inductive definitions are now introduced earlier in the theory hierarchy.
berghofe
parents: 11003
diff changeset
     9
theory Inductive = Gfp + Sum_Type + Relation
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    10
files
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    11
  ("Tools/induct_method.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    12
  ("Tools/inductive_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    13
  ("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    14
  ("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    15
  ("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    16
  ("Tools/datatype_abs_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    17
  ("Tools/datatype_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    18
  ("Tools/primrec_package.ML"):
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    19
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    20
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    21
(* handling of proper rules *)
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    22
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    23
constdefs
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    24
  forall :: "('a => bool) => bool"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    25
  "forall P == \<forall>x. P x"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    26
  implies :: "bool => bool => bool"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    27
  "implies A B == A --> B"
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    28
  equal :: "'a => 'a => bool"
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    29
  "equal x y == x = y"
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    30
  conj :: "bool => bool => bool"
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    31
  "conj A B == A & B"
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    32
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    33
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    34
  by (simp only: atomize_all forall_def)
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    35
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    36
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    37
  by (simp only: atomize_imp implies_def)
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    38
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    39
lemma equal_eq: "(x == y) == Trueprop (equal x y)"
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    40
  by (simp only: atomize_eq equal_def)
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    41
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    42
lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    43
  by (unfold forall_def conj_def) blast
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    44
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    45
lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    46
  by (unfold implies_def conj_def) blast
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    47
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    48
lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    49
  by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
10434
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    50
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    51
lemmas inductive_atomize = forall_eq implies_eq equal_eq
6ea4735c3955 simplified atomize;
wenzelm
parents: 10402
diff changeset
    52
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    53
lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    54
lemmas inductive_conj = forall_conj implies_conj conj_curry
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    55
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    56
hide const forall implies equal conj
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    57
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    58
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    59
(* setup packages *)
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    60
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    61
use "Tools/induct_method.ML"
8303
5e7037409118 early setup of induct_method;
wenzelm
parents: 7710
diff changeset
    62
setup InductMethod.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    63
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    64
use "Tools/inductive_package.ML"
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    65
setup InductivePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    66
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    67
use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    68
use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    69
use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    70
use "Tools/datatype_abs_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    71
use "Tools/datatype_package.ML"
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    72
setup DatatypePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    73
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    74
use "Tools/primrec_package.ML"
8482
bbc805ebc904 Added setup for primrec theory data.
berghofe
parents: 8343
diff changeset
    75
setup PrimrecPackage.setup
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    76
10312
4c5a03649af7 declare trancl rules;
wenzelm
parents: 10212
diff changeset
    77
theorems basic_monos [mono] =
11003
ee0838d89deb added if_def2
oheimb
parents: 10727
diff changeset
    78
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    79
  Collect_mono in_mono vimage_mono
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    80
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    81
  not_all not_ex
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    82
  Ball_def Bex_def
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    83
  inductive_rulify2
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    84
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    85
end