src/HOL/Inductive.thy
author wenzelm
Fri, 26 Oct 2001 23:58:21 +0200
changeset 11952 b10f1e8862f4
parent 11825 ef7d619e2c88
child 11990 c1daefc08eff
permissions -rw-r--r--
* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
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)
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
     5
*)
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
     6
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
     7
header {* Support for inductive sets and types *}
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/inductive_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    12
  ("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    13
  ("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    14
  ("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    15
  ("Tools/datatype_abs_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    16
  ("Tools/datatype_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    17
  ("Tools/primrec_package.ML"):
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    18
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    19
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    20
subsection {* Inductive sets *}
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    21
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    22
text {* Inversion of injective functions. *}
11436
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    23
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    24
constdefs
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    25
  myinv :: "('a => 'b) => ('b => 'a)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    26
  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    27
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    28
lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    29
proof -
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    30
  assume "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    31
  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    32
    by (simp only: inj_eq)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    33
  also have "... = x" by (rule the_eq_trivial)
11439
wenzelm
parents: 11436
diff changeset
    34
  finally show ?thesis by (unfold myinv_def)
11436
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    35
qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    36
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    37
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    38
proof (unfold myinv_def)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    39
  assume inj: "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    40
  assume "y \<in> range f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    41
  then obtain x where "y = f x" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    42
  hence x: "f x = y" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    43
  thus "f (THE x. f x = y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    44
  proof (rule theI)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    45
    fix x' assume "f x' = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    46
    with x have "f x' = f x" by simp
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    47
    with inj show "x' = x" by (rule injD)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    48
  qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    49
qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    50
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    51
hide const myinv
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    52
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    53
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    54
text {* Package setup. *}
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    55
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    56
use "Tools/inductive_package.ML"
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    57
setup InductivePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    58
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    59
theorems basic_monos [mono] =
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    60
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    61
  Collect_mono in_mono vimage_mono
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    62
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    63
  not_all not_ex
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    64
  Ball_def Bex_def
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    65
  inductive_rulify2
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    66
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    67
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    68
subsubsection {* Inductive datatypes and primitive recursion *}
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    69
11825
ef7d619e2c88 moved InductMethod.setup to theory HOL;
wenzelm
parents: 11688
diff changeset
    70
text {* Package setup. *}
ef7d619e2c88 moved InductMethod.setup to theory HOL;
wenzelm
parents: 11688
diff changeset
    71
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    72
use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    73
use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    74
use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    75
use "Tools/datatype_abs_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    76
use "Tools/datatype_package.ML"
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    77
setup DatatypePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    78
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    79
use "Tools/primrec_package.ML"
8482
bbc805ebc904 Added setup for primrec theory data.
berghofe
parents: 8343
diff changeset
    80
setup PrimrecPackage.setup
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
    81
6437
9bdfe07ba8e9 'HOL/inductive' theory data;
wenzelm
parents: 5105
diff changeset
    82
end