author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 67408 | 4a4c14b24800 |
child 71942 | d2654b30f7bd |
permissions | -rw-r--r-- |
65363 | 1 |
(* |
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
39302
diff
changeset
|
2 |
Author: Jeremy Dawson and Gerwin Klein, NICTA |
24333 | 3 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
49739
diff
changeset
|
4 |
Consequences of type definition theorems, and of extended type definition. |
24333 | 5 |
*) |
24350 | 6 |
|
61799 | 7 |
section \<open>Type Definition Theorems\<close> |
24350 | 8 |
|
37655 | 9 |
theory Misc_Typedef |
67120 | 10 |
imports Main |
26560 | 11 |
begin |
24333 | 12 |
|
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24350
diff
changeset
|
13 |
section "More lemmas about normal type definitions" |
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24350
diff
changeset
|
14 |
|
67120 | 15 |
lemma tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" |
16 |
and tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" |
|
17 |
and tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y" |
|
24333 | 18 |
by (auto simp: type_definition_def) |
19 |
||
67399 | 20 |
lemma td_nat_int: "type_definition int nat (Collect ((\<le>) 0))" |
24333 | 21 |
unfolding type_definition_def by auto |
22 |
||
23 |
context type_definition |
|
24 |
begin |
|
25 |
||
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
26 |
declare Rep [iff] Rep_inverse [simp] Rep_inject [simp] |
24333 | 27 |
|
67120 | 28 |
lemma Abs_eqD: "Abs x = Abs y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y" |
24333 | 29 |
by (simp add: Abs_inject) |
65363 | 30 |
|
67120 | 31 |
lemma Abs_inverse': "r \<in> A \<Longrightarrow> Abs r = a \<Longrightarrow> Rep a = r" |
24333 | 32 |
by (safe elim!: Abs_inverse) |
33 |
||
67120 | 34 |
lemma Rep_comp_inverse: "Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
35 |
using Rep_inverse by auto |
24333 | 36 |
|
67120 | 37 |
lemma Rep_eqD [elim!]: "Rep x = Rep y \<Longrightarrow> x = y" |
24333 | 38 |
by simp |
39 |
||
67120 | 40 |
lemma Rep_inverse': "Rep a = r \<Longrightarrow> Abs r = a" |
24333 | 41 |
by (safe intro!: Rep_inverse) |
42 |
||
67120 | 43 |
lemma comp_Abs_inverse: "f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
44 |
using Rep_inverse by auto |
24333 | 45 |
|
67120 | 46 |
lemma set_Rep: "A = range Rep" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
37655
diff
changeset
|
47 |
proof (rule set_eqI) |
67120 | 48 |
show "x \<in> A \<longleftrightarrow> x \<in> range Rep" for x |
24333 | 49 |
by (auto dest: Abs_inverse [of x, symmetric]) |
65363 | 50 |
qed |
24333 | 51 |
|
65363 | 52 |
lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
37655
diff
changeset
|
53 |
proof (rule set_eqI) |
67120 | 54 |
show "x \<in> A \<longleftrightarrow> x \<in> range (Rep \<circ> Abs)" for x |
24333 | 55 |
by (auto dest: Abs_inverse [of x, symmetric]) |
65363 | 56 |
qed |
24333 | 57 |
|
58 |
lemma Abs_inj_on: "inj_on Abs A" |
|
65363 | 59 |
unfolding inj_on_def |
24333 | 60 |
by (auto dest: Abs_inject [THEN iffD1]) |
61 |
||
62 |
lemma image: "Abs ` A = UNIV" |
|
63 |
by (auto intro!: image_eqI) |
|
64 |
||
65 |
lemmas td_thm = type_definition_axioms |
|
66 |
||
67120 | 67 |
lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" |
24333 | 68 |
by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) |
69 |
||
70 |
lemmas fns1a = disjI1 [THEN fns1] |
|
71 |
lemmas fns1b = disjI2 [THEN fns1] |
|
72 |
||
67120 | 73 |
lemma fns4: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
74 |
by auto |
24333 | 75 |
|
76 |
end |
|
77 |
||
67399 | 78 |
interpretation nat_int: type_definition int nat "Collect ((\<le>) 0)" |
24333 | 79 |
by (rule td_nat_int) |
80 |
||
27138
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
81 |
declare |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
82 |
nat_int.Rep_cases [cases del] |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
83 |
nat_int.Abs_cases [cases del] |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
84 |
nat_int.Rep_induct [induct del] |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
85 |
nat_int.Abs_induct [induct del] |
24333 | 86 |
|
87 |
||
24350 | 88 |
subsection "Extended form of type definition predicate" |
24333 | 89 |
|
90 |
lemma td_conds: |
|
67120 | 91 |
"norm \<circ> norm = norm \<Longrightarrow> |
92 |
fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<and> norm \<circ> fr \<circ> norm = norm \<circ> fr" |
|
24333 | 93 |
apply safe |
49739 | 94 |
apply (simp_all add: comp_assoc) |
24333 | 95 |
apply (simp_all add: o_assoc) |
96 |
done |
|
97 |
||
67120 | 98 |
lemma fn_comm_power: "fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n" |
65363 | 99 |
apply (rule ext) |
24333 | 100 |
apply (induct n) |
101 |
apply (auto dest: fun_cong) |
|
102 |
done |
|
103 |
||
104 |
lemmas fn_comm_power' = |
|
45604 | 105 |
ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def] |
24333 | 106 |
|
107 |
||
108 |
locale td_ext = type_definition + |
|
109 |
fixes norm |
|
110 |
assumes eq_norm: "\<And>x. Rep (Abs x) = norm x" |
|
111 |
begin |
|
112 |
||
67120 | 113 |
lemma Abs_norm [simp]: "Abs (norm x) = Abs x" |
24333 | 114 |
using eq_norm [of x] by (auto elim: Rep_inverse') |
115 |
||
67120 | 116 |
lemma td_th: "g \<circ> Abs = f \<Longrightarrow> f (Rep x) = g x" |
24333 | 117 |
by (drule comp_Abs_inverse [symmetric]) simp |
118 |
||
65363 | 119 |
lemma eq_norm': "Rep \<circ> Abs = norm" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
120 |
by (auto simp: eq_norm) |
24333 | 121 |
|
122 |
lemma norm_Rep [simp]: "norm (Rep x) = Rep x" |
|
123 |
by (auto simp: eq_norm' intro: td_th) |
|
124 |
||
125 |
lemmas td = td_thm |
|
126 |
||
67613 | 127 |
lemma set_iff_norm: "w \<in> A \<longleftrightarrow> w = norm w" |
24333 | 128 |
by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
129 |
||
67120 | 130 |
lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" |
24333 | 131 |
apply (rule iffI) |
132 |
apply (clarsimp simp add: eq_norm) |
|
133 |
apply (simp add: eq_norm' [symmetric]) |
|
134 |
done |
|
135 |
||
67120 | 136 |
lemma norm_eq_iff: "norm x = norm y \<longleftrightarrow> Abs x = Abs y" |
24333 | 137 |
by (simp add: eq_norm' [symmetric]) |
138 |
||
65363 | 139 |
lemma norm_comps: |
140 |
"Abs \<circ> norm = Abs" |
|
141 |
"norm \<circ> Rep = Rep" |
|
142 |
"norm \<circ> norm = norm" |
|
24333 | 143 |
by (auto simp: eq_norm' [symmetric] o_def) |
144 |
||
145 |
lemmas norm_norm [simp] = norm_comps |
|
146 |
||
67120 | 147 |
lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
148 |
by (fold eq_norm') auto |
24333 | 149 |
|
67408 | 150 |
text \<open> |
151 |
following give conditions for converses to \<open>td_fns1\<close> |
|
152 |
\<^item> the condition \<open>norm \<circ> fr \<circ> norm = fr \<circ> norm\<close> says that |
|
153 |
\<open>fr\<close> takes normalised arguments to normalised results |
|
154 |
\<^item> \<open>norm \<circ> fr \<circ> norm = norm \<circ> fr\<close> says that \<open>fr\<close> |
|
155 |
takes norm-equivalent arguments to norm-equivalent results |
|
156 |
\<^item> \<open>fr \<circ> norm = fr\<close> says that \<open>fr\<close> |
|
157 |
takes norm-equivalent arguments to the same result |
|
158 |
\<^item> \<open>norm \<circ> fr = fr\<close> says that \<open>fr\<close> takes any argument to a normalised result |
|
159 |
\<close> |
|
67120 | 160 |
lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
24333 | 161 |
apply (fold eq_norm') |
162 |
apply safe |
|
163 |
prefer 2 |
|
164 |
apply (simp add: o_assoc) |
|
165 |
apply (rule ext) |
|
166 |
apply (drule_tac x="Rep x" in fun_cong) |
|
167 |
apply auto |
|
168 |
done |
|
169 |
||
67120 | 170 |
lemma fns3: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> fa \<circ> Abs = Abs \<circ> fr" |
24333 | 171 |
apply (fold eq_norm') |
172 |
apply safe |
|
173 |
prefer 2 |
|
49739 | 174 |
apply (simp add: comp_assoc) |
24333 | 175 |
apply (rule ext) |
65363 | 176 |
apply (drule_tac f="a \<circ> b" for a b in fun_cong) |
24333 | 177 |
apply simp |
178 |
done |
|
179 |
||
67120 | 180 |
lemma fns: "fr \<circ> norm = norm \<circ> fr \<Longrightarrow> fa \<circ> Abs = Abs \<circ> fr \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
24333 | 181 |
apply safe |
182 |
apply (frule fns1b) |
|
65363 | 183 |
prefer 2 |
184 |
apply (frule fns1a) |
|
24333 | 185 |
apply (rule fns3 [THEN iffD1]) |
186 |
prefer 3 |
|
187 |
apply (rule fns2 [THEN iffD1]) |
|
49739 | 188 |
apply (simp_all add: comp_assoc) |
24333 | 189 |
apply (simp_all add: o_assoc) |
190 |
done |
|
191 |
||
67120 | 192 |
lemma range_norm: "range (Rep \<circ> Abs) = A" |
24333 | 193 |
by (simp add: set_Rep_Abs) |
194 |
||
195 |
end |
|
196 |
||
197 |
lemmas td_ext_def' = |
|
198 |
td_ext_def [unfolded type_definition_def td_ext_axioms_def] |
|
199 |
||
200 |
end |
|
201 |