author | wenzelm |
Wed, 26 Sep 2007 19:17:55 +0200 | |
changeset 24720 | 4d2f2e375fa1 |
parent 24699 | c6674504103f |
child 24845 | abcd15369ffa |
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 |
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24626
diff
changeset
|
9 |
imports FixedPoint Sum_Type |
16417 | 10 |
uses |
10402 | 11 |
("Tools/inductive_package.ML") |
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
24349
diff
changeset
|
12 |
"Tools/dseq.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") |
|
22783 | 18 |
("Tools/datatype_case.ML") |
10402 | 19 |
("Tools/datatype_package.ML") |
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
20 |
("Tools/datatype_codegen.ML") |
15131 | 21 |
("Tools/primrec_package.ML") |
22 |
begin |
|
10727 | 23 |
|
23734 | 24 |
subsection {* Inductive predicates and sets *} |
11688 | 25 |
|
26 |
text {* Inversion of injective functions. *} |
|
11436 | 27 |
|
28 |
constdefs |
|
29 |
myinv :: "('a => 'b) => ('b => 'a)" |
|
30 |
"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y" |
|
31 |
||
32 |
lemma myinv_f_f: "inj f ==> myinv f (f x) = x" |
|
33 |
proof - |
|
34 |
assume "inj f" |
|
35 |
hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |
|
36 |
by (simp only: inj_eq) |
|
37 |
also have "... = x" by (rule the_eq_trivial) |
|
11439 | 38 |
finally show ?thesis by (unfold myinv_def) |
11436 | 39 |
qed |
40 |
||
41 |
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |
|
42 |
proof (unfold myinv_def) |
|
43 |
assume inj: "inj f" |
|
44 |
assume "y \<in> range f" |
|
45 |
then obtain x where "y = f x" .. |
|
46 |
hence x: "f x = y" .. |
|
47 |
thus "f (THE x. f x = y) = y" |
|
48 |
proof (rule theI) |
|
49 |
fix x' assume "f x' = y" |
|
50 |
with x have "f x' = f x" by simp |
|
51 |
with inj show "x' = x" by (rule injD) |
|
52 |
qed |
|
53 |
qed |
|
54 |
||
55 |
hide const myinv |
|
56 |
||
57 |
||
11688 | 58 |
text {* Package setup. *} |
10402 | 59 |
|
23734 | 60 |
theorems basic_monos = |
22218 | 61 |
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
11688 | 62 |
Collect_mono in_mono vimage_mono |
63 |
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
|
64 |
not_all not_ex |
|
65 |
Ball_def Bex_def |
|
18456 | 66 |
induct_rulify_fallback |
11688 | 67 |
|
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset
|
68 |
use "Tools/inductive_package.ML" |
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset
|
69 |
setup InductivePackage.setup |
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset
|
70 |
|
23734 | 71 |
theorems [mono] = |
22218 | 72 |
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
|
73 |
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
|
74 |
not_all not_ex |
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset
|
75 |
Ball_def Bex_def |
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset
|
76 |
induct_rulify_fallback |
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset
|
77 |
|
20604 | 78 |
lemma False_meta_all: |
79 |
"Trueprop False \<equiv> (\<And>P\<Colon>bool. P)" |
|
80 |
proof |
|
81 |
fix P |
|
82 |
assume False |
|
83 |
then show P .. |
|
84 |
next |
|
85 |
assume "\<And>P\<Colon>bool. P" |
|
23389 | 86 |
then show False . |
20604 | 87 |
qed |
88 |
||
89 |
lemma not_eq_False: |
|
90 |
assumes not_eq: "x \<noteq> y" |
|
22886 | 91 |
and eq: "x \<equiv> y" |
20604 | 92 |
shows False |
93 |
using not_eq eq by auto |
|
94 |
||
95 |
lemmas not_eq_quodlibet = |
|
96 |
not_eq_False [simplified False_meta_all] |
|
97 |
||
11688 | 98 |
|
12023 | 99 |
subsection {* Inductive datatypes and primitive recursion *} |
11688 | 100 |
|
11825 | 101 |
text {* Package setup. *} |
102 |
||
10402 | 103 |
use "Tools/datatype_aux.ML" |
104 |
use "Tools/datatype_prop.ML" |
|
105 |
use "Tools/datatype_rep_proofs.ML" |
|
106 |
use "Tools/datatype_abs_proofs.ML" |
|
22783 | 107 |
use "Tools/datatype_case.ML" |
10402 | 108 |
use "Tools/datatype_package.ML" |
7700 | 109 |
setup DatatypePackage.setup |
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24626
diff
changeset
|
110 |
use "Tools/primrec_package.ML" |
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
111 |
use "Tools/datatype_codegen.ML" |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
112 |
setup DatatypeCodegen.setup |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
113 |
|
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
114 |
use "Tools/inductive_codegen.ML" |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
115 |
setup InductiveCodegen.setup |
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset
|
116 |
|
23526 | 117 |
text{* Lambda-abstractions with pattern matching: *} |
118 |
||
119 |
syntax |
|
23529 | 120 |
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) |
23526 | 121 |
syntax (xsymbols) |
23529 | 122 |
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) |
23526 | 123 |
|
23529 | 124 |
parse_translation (advanced) {* |
125 |
let |
|
126 |
fun fun_tr ctxt [cs] = |
|
127 |
let |
|
128 |
val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT); |
|
24349 | 129 |
val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr |
130 |
ctxt [x, cs] |
|
23529 | 131 |
in lambda x ft end |
132 |
in [("_lam_pats_syntax", fun_tr)] end |
|
23526 | 133 |
*} |
134 |
||
135 |
end |