src/HOL/Word/TdThs.thy
 author wenzelm Wed Sep 17 21:27:14 2008 +0200 (2008-09-17) changeset 28263 69eaa97e7e96 parent 27138 63fdfcf6c7a3 child 29234 60f7fb56f8cd permissions -rw-r--r--
moved global ML bindings to global place;
1 (*
2     ID:         \$Id\$
3     Author:     Jeremy Dawson and Gerwin Klein, NICTA
5   consequences of type definition theorems,
6   and of extended type definition theorems
7 *)
9 header {* Type Definition Theorems *}
11 theory TdThs
12 imports Main
13 begin
15 section "More lemmas about normal type definitions"
17 lemma
18   tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and
19   tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and
20   tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
21   by (auto simp: type_definition_def)
23 lemma td_nat_int:
24   "type_definition int nat (Collect (op <= 0))"
25   unfolding type_definition_def by auto
27 context type_definition
28 begin
30 lemmas Rep' [iff] = Rep [simplified]  (* if A is given as Collect .. *)
32 declare Rep_inverse [simp] Rep_inject [simp]
34 lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
35   by (simp add: Abs_inject)
37 lemma Abs_inverse':
38   "r : A ==> Abs r = a ==> Rep a = r"
39   by (safe elim!: Abs_inverse)
41 lemma Rep_comp_inverse:
42   "Rep o f = g ==> Abs o g = f"
43   using Rep_inverse by (auto intro: ext)
45 lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
46   by simp
48 lemma Rep_inverse': "Rep a = r ==> Abs r = a"
49   by (safe intro!: Rep_inverse)
51 lemma comp_Abs_inverse:
52   "f o Abs = g ==> g o Rep = f"
53   using Rep_inverse by (auto intro: ext)
55 lemma set_Rep:
56   "A = range Rep"
57 proof (rule set_ext)
58   fix x
59   show "(x \<in> A) = (x \<in> range Rep)"
60     by (auto dest: Abs_inverse [of x, symmetric])
61 qed
63 lemma set_Rep_Abs: "A = range (Rep o Abs)"
64 proof (rule set_ext)
65   fix x
66   show "(x \<in> A) = (x \<in> range (Rep o Abs))"
67     by (auto dest: Abs_inverse [of x, symmetric])
68 qed
70 lemma Abs_inj_on: "inj_on Abs A"
71   unfolding inj_on_def
72   by (auto dest: Abs_inject [THEN iffD1])
74 lemma image: "Abs ` A = UNIV"
75   by (auto intro!: image_eqI)
77 lemmas td_thm = type_definition_axioms
79 lemma fns1:
80   "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
81   by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)
83 lemmas fns1a = disjI1 [THEN fns1]
84 lemmas fns1b = disjI2 [THEN fns1]
86 lemma fns4:
87   "Rep o fa o Abs = fr ==>
88    Rep o fa = fr o Rep & fa o Abs = Abs o fr"
89   by (auto intro!: ext)
91 end
93 interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
94   by (rule td_nat_int)
96 declare
97   nat_int.Rep_cases [cases del]
98   nat_int.Abs_cases [cases del]
99   nat_int.Rep_induct [induct del]
100   nat_int.Abs_induct [induct del]
103 subsection "Extended form of type definition predicate"
105 lemma td_conds:
106   "norm o norm = norm ==> (fr o norm = norm o fr) =
107     (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
108   apply safe
109     apply (simp_all add: o_assoc [symmetric])
110    apply (simp_all add: o_assoc)
111   done
113 lemma fn_comm_power:
114   "fa o tr = tr o fr ==> fa ^ n o tr = tr o fr ^ n"
115   apply (rule ext)
116   apply (induct n)
117    apply (auto dest: fun_cong)
118   done
120 lemmas fn_comm_power' =
121   ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def, standard]
124 locale td_ext = type_definition +
125   fixes norm
126   assumes eq_norm: "\<And>x. Rep (Abs x) = norm x"
127 begin
129 lemma Abs_norm [simp]:
130   "Abs (norm x) = Abs x"
131   using eq_norm [of x] by (auto elim: Rep_inverse')
133 lemma td_th:
134   "g o Abs = f ==> f (Rep x) = g x"
135   by (drule comp_Abs_inverse [symmetric]) simp
137 lemma eq_norm': "Rep o Abs = norm"
138   by (auto simp: eq_norm intro!: ext)
140 lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
141   by (auto simp: eq_norm' intro: td_th)
143 lemmas td = td_thm
145 lemma set_iff_norm: "w : A <-> w = norm w"
146   by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
148 lemma inverse_norm:
149   "(Abs n = w) = (Rep w = norm n)"
150   apply (rule iffI)
151    apply (clarsimp simp add: eq_norm)
152   apply (simp add: eq_norm' [symmetric])
153   done
155 lemma norm_eq_iff:
156   "(norm x = norm y) = (Abs x = Abs y)"
157   by (simp add: eq_norm' [symmetric])
159 lemma norm_comps:
160   "Abs o norm = Abs"
161   "norm o Rep = Rep"
162   "norm o norm = norm"
163   by (auto simp: eq_norm' [symmetric] o_def)
165 lemmas norm_norm [simp] = norm_comps
167 lemma fns5:
168   "Rep o fa o Abs = fr ==>
169   fr o norm = fr & norm o fr = fr"
170   by (fold eq_norm') (auto intro!: ext)
172 (* following give conditions for converses to td_fns1
173   the condition (norm o fr o norm = fr o norm) says that
174   fr takes normalised arguments to normalised results,
175   (norm o fr o norm = norm o fr) says that fr
176   takes norm-equivalent arguments to norm-equivalent results,
177   (fr o norm = fr) says that fr
178   takes norm-equivalent arguments to the same result, and
179   (norm o fr = fr) says that fr takes any argument to a normalised result
180   *)
181 lemma fns2:
182   "Abs o fr o Rep = fa ==>
183    (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)"
184   apply (fold eq_norm')
185   apply safe
186    prefer 2
187    apply (simp add: o_assoc)
188   apply (rule ext)
189   apply (drule_tac x="Rep x" in fun_cong)
190   apply auto
191   done
193 lemma fns3:
194   "Abs o fr o Rep = fa ==>
195    (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)"
196   apply (fold eq_norm')
197   apply safe
198    prefer 2
199    apply (simp add: o_assoc [symmetric])
200   apply (rule ext)
201   apply (drule fun_cong)
202   apply simp
203   done
205 lemma fns:
206   "fr o norm = norm o fr ==>
207     (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)"
208   apply safe
209    apply (frule fns1b)
210    prefer 2
211    apply (frule fns1a)
212    apply (rule fns3 [THEN iffD1])
213      prefer 3
214      apply (rule fns2 [THEN iffD1])
215        apply (simp_all add: o_assoc [symmetric])
216    apply (simp_all add: o_assoc)
217   done
219 lemma range_norm:
220   "range (Rep o Abs) = A"
221   by (simp add: set_Rep_Abs)
223 end
225 lemmas td_ext_def' =
226   td_ext_def [unfolded type_definition_def td_ext_axioms_def]
228 end