author | wenzelm |
Wed, 26 Jul 2006 00:44:44 +0200 | |
changeset 20207 | 4c57e850e8d5 |
parent 19599 | a5c7eb37d14f |
child 20604 | 9dba9c7872c9 |
permissions | -rw-r--r-- |
7700 | 1 |
(* Title: HOL/Inductive.thy |
2 |
ID: $Id$ |
|
10402 | 3 |
Author: Markus Wenzel, TU Muenchen |
11688 | 4 |
*) |
10727 | 5 |
|
11688 | 6 |
header {* Support for inductive sets and types *} |
1187 | 7 |
|
15131 | 8 |
theory Inductive |
17009 | 9 |
imports FixedPoint Sum_Type Relation Record |
16417 | 10 |
uses |
10402 | 11 |
("Tools/inductive_package.ML") |
13705 | 12 |
("Tools/inductive_realizer.ML") |
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
13 |
("Tools/inductive_codegen.ML") |
10402 | 14 |
("Tools/datatype_aux.ML") |
15 |
("Tools/datatype_prop.ML") |
|
16 |
("Tools/datatype_rep_proofs.ML") |
|
17 |
("Tools/datatype_abs_proofs.ML") |
|
13469 | 18 |
("Tools/datatype_realizer.ML") |
19599 | 19 |
("Tools/datatype_hooks.ML") |
10402 | 20 |
("Tools/datatype_package.ML") |
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
21 |
("Tools/datatype_codegen.ML") |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
22 |
("Tools/recfun_codegen.ML") |
15131 | 23 |
("Tools/primrec_package.ML") |
24 |
begin |
|
10727 | 25 |
|
11688 | 26 |
subsection {* Inductive sets *} |
27 |
||
28 |
text {* Inversion of injective functions. *} |
|
11436 | 29 |
|
30 |
constdefs |
|
31 |
myinv :: "('a => 'b) => ('b => 'a)" |
|
32 |
"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y" |
|
33 |
||
34 |
lemma myinv_f_f: "inj f ==> myinv f (f x) = x" |
|
35 |
proof - |
|
36 |
assume "inj f" |
|
37 |
hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |
|
38 |
by (simp only: inj_eq) |
|
39 |
also have "... = x" by (rule the_eq_trivial) |
|
11439 | 40 |
finally show ?thesis by (unfold myinv_def) |
11436 | 41 |
qed |
42 |
||
43 |
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |
|
44 |
proof (unfold myinv_def) |
|
45 |
assume inj: "inj f" |
|
46 |
assume "y \<in> range f" |
|
47 |
then obtain x where "y = f x" .. |
|
48 |
hence x: "f x = y" .. |
|
49 |
thus "f (THE x. f x = y) = y" |
|
50 |
proof (rule theI) |
|
51 |
fix x' assume "f x' = y" |
|
52 |
with x have "f x' = f x" by simp |
|
53 |
with inj show "x' = x" by (rule injD) |
|
54 |
qed |
|
55 |
qed |
|
56 |
||
57 |
hide const myinv |
|
58 |
||
59 |
||
11688 | 60 |
text {* Package setup. *} |
10402 | 61 |
|
62 |
use "Tools/inductive_package.ML" |
|
6437 | 63 |
setup InductivePackage.setup |
10402 | 64 |
|
11688 | 65 |
theorems basic_monos [mono] = |
66 |
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 |
|
67 |
Collect_mono in_mono vimage_mono |
|
68 |
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
|
69 |
not_all not_ex |
|
70 |
Ball_def Bex_def |
|
18456 | 71 |
induct_rulify_fallback |
11688 | 72 |
|
73 |
||
12023 | 74 |
subsection {* Inductive datatypes and primitive recursion *} |
11688 | 75 |
|
11825 | 76 |
text {* Package setup. *} |
77 |
||
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
78 |
use "Tools/recfun_codegen.ML" |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
79 |
setup RecfunCodegen.setup |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
80 |
|
10402 | 81 |
use "Tools/datatype_aux.ML" |
82 |
use "Tools/datatype_prop.ML" |
|
83 |
use "Tools/datatype_rep_proofs.ML" |
|
84 |
use "Tools/datatype_abs_proofs.ML" |
|
13469 | 85 |
use "Tools/datatype_realizer.ML" |
19599 | 86 |
|
87 |
use "Tools/datatype_hooks.ML" |
|
88 |
setup DatatypeHooks.setup |
|
89 |
||
10402 | 90 |
use "Tools/datatype_package.ML" |
7700 | 91 |
setup DatatypePackage.setup |
10402 | 92 |
|
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
93 |
use "Tools/datatype_codegen.ML" |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
94 |
setup DatatypeCodegen.setup |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
95 |
|
13705 | 96 |
use "Tools/inductive_realizer.ML" |
97 |
setup InductiveRealizer.setup |
|
98 |
||
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
99 |
use "Tools/inductive_codegen.ML" |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
100 |
setup InductiveCodegen.setup |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
101 |
|
10402 | 102 |
use "Tools/primrec_package.ML" |
7700 | 103 |
|
6437 | 104 |
end |