src/HOL/Inductive.thy
author haftmann
Tue, 18 Sep 2007 07:36:38 +0200
changeset 24625 0398a5e802d3
parent 24349 0dd8782fb02d
child 24626 85eceef2edc7
permissions -rw-r--r--
separated code for inductive sequences from inductive_codegen.ML
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
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
     4
*)
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
     5
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
     6
header {* Support for inductive sets and types *}
1187
bc94f00e47ba Includes Sum.thy as a parent for mutual recursion
lcp
parents: 923
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
     8
theory Inductive 
23708
b5eb0b4dd17d clarified import
haftmann
parents: 23529
diff changeset
     9
imports FixedPoint Product_Type Sum_Type
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15140
diff changeset
    10
uses
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    11
  ("Tools/inductive_package.ML")
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
    12
  ("Tools/inductive_set_package.ML")
13705
934d6c1421f2 Added InductiveRealizer package.
berghofe
parents: 13469
diff changeset
    13
  ("Tools/inductive_realizer.ML")
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents: 24349
diff changeset
    14
  "Tools/dseq.ML"
12437
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
    15
  ("Tools/inductive_codegen.ML")
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    16
  ("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    17
  ("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    18
  ("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    19
  ("Tools/datatype_abs_proofs.ML")
13469
70d8dfef587d Added file Tools/datatype_realizer.ML
berghofe
parents: 12920
diff changeset
    20
  ("Tools/datatype_realizer.ML")
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 18456
diff changeset
    21
  ("Tools/datatype_hooks.ML")
22783
e5f947e0ade8 Added datatype_case.
berghofe
parents: 22218
diff changeset
    22
  ("Tools/datatype_case.ML")
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    23
  ("Tools/datatype_package.ML")
12437
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
    24
  ("Tools/datatype_codegen.ML")
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
    25
  ("Tools/primrec_package.ML")
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
    26
begin
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    27
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
    28
subsection {* Inductive predicates and sets *}
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    29
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    30
text {* Inversion of injective functions. *}
11436
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    31
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    32
constdefs
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    33
  myinv :: "('a => 'b) => ('b => 'a)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    34
  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    35
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    36
lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    37
proof -
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    38
  assume "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    39
  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    40
    by (simp only: inj_eq)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    41
  also have "... = x" by (rule the_eq_trivial)
11439
wenzelm
parents: 11436
diff changeset
    42
  finally show ?thesis by (unfold myinv_def)
11436
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    43
qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    44
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    45
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
    46
proof (unfold myinv_def)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    47
  assume inj: "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    48
  assume "y \<in> range f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    49
  then obtain x where "y = f x" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    50
  hence x: "f x = y" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    51
  thus "f (THE x. f x = y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    52
  proof (rule theI)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    53
    fix x' assume "f x' = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    54
    with x have "f x' = f x" by simp
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    55
    with inj show "x' = x" by (rule injD)
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    56
  qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    57
qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    58
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    59
hide const myinv
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    60
3f74b80d979f private "myinv" (uses "The" instead of "Eps");
wenzelm
parents: 11325
diff changeset
    61
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    62
text {* Package setup. *}
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
    63
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
    64
theorems basic_monos =
22218
30a8890d2967 dropped lemma duplicates in HOL.thy
haftmann
parents: 21018
diff changeset
    65
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    66
  Collect_mono in_mono vimage_mono
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    67
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    68
  not_all not_ex
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    69
  Ball_def Bex_def
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 17009
diff changeset
    70
  induct_rulify_fallback
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
    71
21018
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    72
use "Tools/inductive_package.ML"
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    73
setup InductivePackage.setup
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    74
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
    75
theorems [mono] =
22218
30a8890d2967 dropped lemma duplicates in HOL.thy
haftmann
parents: 21018
diff changeset
    76
  imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
21018
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    77
  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    78
  not_all not_ex
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    79
  Ball_def Bex_def
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    80
  induct_rulify_fallback
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
    81
20604
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    82
lemma False_meta_all:
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    83
  "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    84
proof
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    85
  fix P
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    86
  assume False
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    87
  then show P ..
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    88
next
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    89
  assume "\<And>P\<Colon>bool. P"
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 22886
diff changeset
    90
  then show False .
20604
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    91
qed
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    92
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    93
lemma not_eq_False:
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    94
  assumes not_eq: "x \<noteq> y"
22886
cdff6ef76009 moved recfun_codegen.ML to Code_Generator.thy
haftmann
parents: 22846
diff changeset
    95
  and eq: "x \<equiv> y"
20604
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    96
  shows False
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    97
  using not_eq eq by auto
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    98
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
    99
lemmas not_eq_quodlibet =
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
   100
  not_eq_False [simplified False_meta_all]
9dba9c7872c9 added auxiliary lemma for code generation 2
haftmann
parents: 19599
diff changeset
   101
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   102
12023
wenzelm
parents: 11990
diff changeset
   103
subsection {* Inductive datatypes and primitive recursion *}
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   104
11825
ef7d619e2c88 moved InductMethod.setup to theory HOL;
wenzelm
parents: 11688
diff changeset
   105
text {* Package setup. *}
ef7d619e2c88 moved InductMethod.setup to theory HOL;
wenzelm
parents: 11688
diff changeset
   106
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   107
use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   108
use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   109
use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   110
use "Tools/datatype_abs_proofs.ML"
22783
e5f947e0ade8 Added datatype_case.
berghofe
parents: 22218
diff changeset
   111
use "Tools/datatype_case.ML"
13469
70d8dfef587d Added file Tools/datatype_realizer.ML
berghofe
parents: 12920
diff changeset
   112
use "Tools/datatype_realizer.ML"
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 18456
diff changeset
   113
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 18456
diff changeset
   114
use "Tools/datatype_hooks.ML"
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 18456
diff changeset
   115
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   116
use "Tools/datatype_package.ML"
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
   117
setup DatatypePackage.setup
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   118
12437
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   119
use "Tools/datatype_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   120
setup DatatypeCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   121
13705
934d6c1421f2 Added InductiveRealizer package.
berghofe
parents: 13469
diff changeset
   122
use "Tools/inductive_realizer.ML"
934d6c1421f2 Added InductiveRealizer package.
berghofe
parents: 13469
diff changeset
   123
setup InductiveRealizer.setup
934d6c1421f2 Added InductiveRealizer package.
berghofe
parents: 13469
diff changeset
   124
12437
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   125
use "Tools/inductive_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   126
setup InductiveCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   127
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   128
use "Tools/primrec_package.ML"
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
   129
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
   130
use "Tools/inductive_set_package.ML"
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
   131
setup InductiveSetPackage.setup
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23708
diff changeset
   132
23526
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   133
text{* Lambda-abstractions with pattern matching: *}
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   134
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   135
syntax
23529
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   136
  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
23526
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   137
syntax (xsymbols)
23529
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   138
  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
23526
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   139
23529
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   140
parse_translation (advanced) {*
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   141
let
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   142
  fun fun_tr ctxt [cs] =
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   143
    let
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   144
      val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
24349
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 23734
diff changeset
   145
      val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 23734
diff changeset
   146
                 ctxt [x, cs]
23529
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   147
    in lambda x ft end
958f9d9cfb63 Fixed problem with patterns in lambdas
nipkow
parents: 23526
diff changeset
   148
in [("_lam_pats_syntax", fun_tr)] end
23526
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   149
*}
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   150
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   151
end