src/HOL/Word/Misc_Typedef.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 59807 22bc39064290 child 61799 4cf66f21b764 permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
 kleing@24333 ` 1` ```(* ``` kleing@44939 ` 2` ``` Author: Jeremy Dawson and Gerwin Klein, NICTA ``` kleing@24333 ` 3` haftmann@53062 ` 4` ``` Consequences of type definition theorems, and of extended type definition. ``` kleing@24333 ` 5` ```*) ``` huffman@24350 ` 6` wenzelm@58874 ` 7` ```section {* Type Definition Theorems *} ``` huffman@24350 ` 8` haftmann@37655 ` 9` ```theory Misc_Typedef ``` haftmann@26560 ` 10` ```imports Main ``` haftmann@26560 ` 11` ```begin ``` kleing@24333 ` 12` kleing@25262 ` 13` ```section "More lemmas about normal type definitions" ``` kleing@25262 ` 14` kleing@24333 ` 15` ```lemma ``` kleing@24333 ` 16` ``` tdD1: "type_definition Rep Abs A \ \x. Rep x \ A" and ``` kleing@24333 ` 17` ``` tdD2: "type_definition Rep Abs A \ \x. Abs (Rep x) = x" and ``` kleing@24333 ` 18` ``` tdD3: "type_definition Rep Abs A \ \y. y \ A \ Rep (Abs y) = y" ``` kleing@24333 ` 19` ``` by (auto simp: type_definition_def) ``` kleing@24333 ` 20` kleing@24333 ` 21` ```lemma td_nat_int: ``` kleing@24333 ` 22` ``` "type_definition int nat (Collect (op <= 0))" ``` kleing@24333 ` 23` ``` unfolding type_definition_def by auto ``` kleing@24333 ` 24` kleing@24333 ` 25` ```context type_definition ``` kleing@24333 ` 26` ```begin ``` kleing@24333 ` 27` wenzelm@45538 ` 28` ```declare Rep [iff] Rep_inverse [simp] Rep_inject [simp] ``` kleing@24333 ` 29` kleing@24333 ` 30` ```lemma Abs_eqD: "Abs x = Abs y ==> x \ A ==> y \ A ==> x = y" ``` kleing@24333 ` 31` ``` by (simp add: Abs_inject) ``` kleing@24333 ` 32` ``` ``` kleing@24333 ` 33` ```lemma Abs_inverse': ``` kleing@24333 ` 34` ``` "r : A ==> Abs r = a ==> Rep a = r" ``` kleing@24333 ` 35` ``` by (safe elim!: Abs_inverse) ``` kleing@24333 ` 36` kleing@24333 ` 37` ```lemma Rep_comp_inverse: ``` kleing@24333 ` 38` ``` "Rep o f = g ==> Abs o g = f" ``` wenzelm@45538 ` 39` ``` using Rep_inverse by auto ``` kleing@24333 ` 40` kleing@24333 ` 41` ```lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y" ``` kleing@24333 ` 42` ``` by simp ``` kleing@24333 ` 43` kleing@24333 ` 44` ```lemma Rep_inverse': "Rep a = r ==> Abs r = a" ``` kleing@24333 ` 45` ``` by (safe intro!: Rep_inverse) ``` kleing@24333 ` 46` kleing@24333 ` 47` ```lemma comp_Abs_inverse: ``` kleing@24333 ` 48` ``` "f o Abs = g ==> g o Rep = f" ``` wenzelm@45538 ` 49` ``` using Rep_inverse by auto ``` kleing@24333 ` 50` kleing@24333 ` 51` ```lemma set_Rep: ``` kleing@24333 ` 52` ``` "A = range Rep" ``` nipkow@39302 ` 53` ```proof (rule set_eqI) ``` kleing@24333 ` 54` ``` fix x ``` kleing@24333 ` 55` ``` show "(x \ A) = (x \ range Rep)" ``` kleing@24333 ` 56` ``` by (auto dest: Abs_inverse [of x, symmetric]) ``` kleing@24333 ` 57` ```qed ``` kleing@24333 ` 58` kleing@24333 ` 59` ```lemma set_Rep_Abs: "A = range (Rep o Abs)" ``` nipkow@39302 ` 60` ```proof (rule set_eqI) ``` kleing@24333 ` 61` ``` fix x ``` kleing@24333 ` 62` ``` show "(x \ A) = (x \ range (Rep o Abs))" ``` kleing@24333 ` 63` ``` by (auto dest: Abs_inverse [of x, symmetric]) ``` kleing@24333 ` 64` ```qed ``` kleing@24333 ` 65` kleing@24333 ` 66` ```lemma Abs_inj_on: "inj_on Abs A" ``` kleing@24333 ` 67` ``` unfolding inj_on_def ``` kleing@24333 ` 68` ``` by (auto dest: Abs_inject [THEN iffD1]) ``` kleing@24333 ` 69` kleing@24333 ` 70` ```lemma image: "Abs ` A = UNIV" ``` kleing@24333 ` 71` ``` by (auto intro!: image_eqI) ``` kleing@24333 ` 72` kleing@24333 ` 73` ```lemmas td_thm = type_definition_axioms ``` kleing@24333 ` 74` kleing@24333 ` 75` ```lemma fns1: ``` kleing@24333 ` 76` ``` "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa" ``` kleing@24333 ` 77` ``` by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) ``` kleing@24333 ` 78` kleing@24333 ` 79` ```lemmas fns1a = disjI1 [THEN fns1] ``` kleing@24333 ` 80` ```lemmas fns1b = disjI2 [THEN fns1] ``` kleing@24333 ` 81` kleing@24333 ` 82` ```lemma fns4: ``` kleing@24333 ` 83` ``` "Rep o fa o Abs = fr ==> ``` kleing@24333 ` 84` ``` Rep o fa = fr o Rep & fa o Abs = Abs o fr" ``` wenzelm@45538 ` 85` ``` by auto ``` kleing@24333 ` 86` kleing@24333 ` 87` ```end ``` kleing@24333 ` 88` wenzelm@30729 ` 89` ```interpretation nat_int: type_definition int nat "Collect (op <= 0)" ``` kleing@24333 ` 90` ``` by (rule td_nat_int) ``` kleing@24333 ` 91` wenzelm@27138 ` 92` ```declare ``` wenzelm@27138 ` 93` ``` nat_int.Rep_cases [cases del] ``` wenzelm@27138 ` 94` ``` nat_int.Abs_cases [cases del] ``` wenzelm@27138 ` 95` ``` nat_int.Rep_induct [induct del] ``` wenzelm@27138 ` 96` ``` nat_int.Abs_induct [induct del] ``` kleing@24333 ` 97` kleing@24333 ` 98` huffman@24350 ` 99` ```subsection "Extended form of type definition predicate" ``` kleing@24333 ` 100` kleing@24333 ` 101` ```lemma td_conds: ``` kleing@24333 ` 102` ``` "norm o norm = norm ==> (fr o norm = norm o fr) = ``` kleing@24333 ` 103` ``` (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)" ``` kleing@24333 ` 104` ``` apply safe ``` haftmann@49739 ` 105` ``` apply (simp_all add: comp_assoc) ``` kleing@24333 ` 106` ``` apply (simp_all add: o_assoc) ``` kleing@24333 ` 107` ``` done ``` kleing@24333 ` 108` kleing@24333 ` 109` ```lemma fn_comm_power: ``` haftmann@30971 ` 110` ``` "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n" ``` kleing@24333 ` 111` ``` apply (rule ext) ``` kleing@24333 ` 112` ``` apply (induct n) ``` kleing@24333 ` 113` ``` apply (auto dest: fun_cong) ``` kleing@24333 ` 114` ``` done ``` kleing@24333 ` 115` kleing@24333 ` 116` ```lemmas fn_comm_power' = ``` wenzelm@45604 ` 117` ``` ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def] ``` kleing@24333 ` 118` kleing@24333 ` 119` kleing@24333 ` 120` ```locale td_ext = type_definition + ``` kleing@24333 ` 121` ``` fixes norm ``` kleing@24333 ` 122` ``` assumes eq_norm: "\x. Rep (Abs x) = norm x" ``` kleing@24333 ` 123` ```begin ``` kleing@24333 ` 124` kleing@24333 ` 125` ```lemma Abs_norm [simp]: ``` kleing@24333 ` 126` ``` "Abs (norm x) = Abs x" ``` kleing@24333 ` 127` ``` using eq_norm [of x] by (auto elim: Rep_inverse') ``` kleing@24333 ` 128` kleing@24333 ` 129` ```lemma td_th: ``` kleing@24333 ` 130` ``` "g o Abs = f ==> f (Rep x) = g x" ``` kleing@24333 ` 131` ``` by (drule comp_Abs_inverse [symmetric]) simp ``` kleing@24333 ` 132` kleing@24333 ` 133` ```lemma eq_norm': "Rep o Abs = norm" ``` wenzelm@45538 ` 134` ``` by (auto simp: eq_norm) ``` kleing@24333 ` 135` kleing@24333 ` 136` ```lemma norm_Rep [simp]: "norm (Rep x) = Rep x" ``` kleing@24333 ` 137` ``` by (auto simp: eq_norm' intro: td_th) ``` kleing@24333 ` 138` kleing@24333 ` 139` ```lemmas td = td_thm ``` kleing@24333 ` 140` kleing@24333 ` 141` ```lemma set_iff_norm: "w : A <-> w = norm w" ``` kleing@24333 ` 142` ``` by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) ``` kleing@24333 ` 143` kleing@24333 ` 144` ```lemma inverse_norm: ``` kleing@24333 ` 145` ``` "(Abs n = w) = (Rep w = norm n)" ``` kleing@24333 ` 146` ``` apply (rule iffI) ``` kleing@24333 ` 147` ``` apply (clarsimp simp add: eq_norm) ``` kleing@24333 ` 148` ``` apply (simp add: eq_norm' [symmetric]) ``` kleing@24333 ` 149` ``` done ``` kleing@24333 ` 150` kleing@24333 ` 151` ```lemma norm_eq_iff: ``` kleing@24333 ` 152` ``` "(norm x = norm y) = (Abs x = Abs y)" ``` kleing@24333 ` 153` ``` by (simp add: eq_norm' [symmetric]) ``` kleing@24333 ` 154` kleing@24333 ` 155` ```lemma norm_comps: ``` kleing@24333 ` 156` ``` "Abs o norm = Abs" ``` kleing@24333 ` 157` ``` "norm o Rep = Rep" ``` kleing@24333 ` 158` ``` "norm o norm = norm" ``` kleing@24333 ` 159` ``` by (auto simp: eq_norm' [symmetric] o_def) ``` kleing@24333 ` 160` kleing@24333 ` 161` ```lemmas norm_norm [simp] = norm_comps ``` kleing@24333 ` 162` kleing@24333 ` 163` ```lemma fns5: ``` kleing@24333 ` 164` ``` "Rep o fa o Abs = fr ==> ``` kleing@24333 ` 165` ``` fr o norm = fr & norm o fr = fr" ``` wenzelm@45538 ` 166` ``` by (fold eq_norm') auto ``` kleing@24333 ` 167` kleing@24333 ` 168` ```(* following give conditions for converses to td_fns1 ``` kleing@24333 ` 169` ``` the condition (norm o fr o norm = fr o norm) says that ``` kleing@24333 ` 170` ``` fr takes normalised arguments to normalised results, ``` kleing@24333 ` 171` ``` (norm o fr o norm = norm o fr) says that fr ``` kleing@24333 ` 172` ``` takes norm-equivalent arguments to norm-equivalent results, ``` kleing@24333 ` 173` ``` (fr o norm = fr) says that fr ``` kleing@24333 ` 174` ``` takes norm-equivalent arguments to the same result, and ``` kleing@24333 ` 175` ``` (norm o fr = fr) says that fr takes any argument to a normalised result ``` kleing@24333 ` 176` ``` *) ``` kleing@24333 ` 177` ```lemma fns2: ``` kleing@24333 ` 178` ``` "Abs o fr o Rep = fa ==> ``` kleing@24333 ` 179` ``` (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)" ``` kleing@24333 ` 180` ``` apply (fold eq_norm') ``` kleing@24333 ` 181` ``` apply safe ``` kleing@24333 ` 182` ``` prefer 2 ``` kleing@24333 ` 183` ``` apply (simp add: o_assoc) ``` kleing@24333 ` 184` ``` apply (rule ext) ``` kleing@24333 ` 185` ``` apply (drule_tac x="Rep x" in fun_cong) ``` kleing@24333 ` 186` ``` apply auto ``` kleing@24333 ` 187` ``` done ``` kleing@24333 ` 188` kleing@24333 ` 189` ```lemma fns3: ``` kleing@24333 ` 190` ``` "Abs o fr o Rep = fa ==> ``` kleing@24333 ` 191` ``` (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)" ``` kleing@24333 ` 192` ``` apply (fold eq_norm') ``` kleing@24333 ` 193` ``` apply safe ``` kleing@24333 ` 194` ``` prefer 2 ``` haftmann@49739 ` 195` ``` apply (simp add: comp_assoc) ``` kleing@24333 ` 196` ``` apply (rule ext) ``` wenzelm@59807 ` 197` ``` apply (drule_tac f="a o b" for a b in fun_cong) ``` kleing@24333 ` 198` ``` apply simp ``` kleing@24333 ` 199` ``` done ``` kleing@24333 ` 200` kleing@24333 ` 201` ```lemma fns: ``` kleing@24333 ` 202` ``` "fr o norm = norm o fr ==> ``` kleing@24333 ` 203` ``` (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)" ``` kleing@24333 ` 204` ``` apply safe ``` kleing@24333 ` 205` ``` apply (frule fns1b) ``` kleing@24333 ` 206` ``` prefer 2 ``` kleing@24333 ` 207` ``` apply (frule fns1a) ``` kleing@24333 ` 208` ``` apply (rule fns3 [THEN iffD1]) ``` kleing@24333 ` 209` ``` prefer 3 ``` kleing@24333 ` 210` ``` apply (rule fns2 [THEN iffD1]) ``` haftmann@49739 ` 211` ``` apply (simp_all add: comp_assoc) ``` kleing@24333 ` 212` ``` apply (simp_all add: o_assoc) ``` kleing@24333 ` 213` ``` done ``` kleing@24333 ` 214` kleing@24333 ` 215` ```lemma range_norm: ``` kleing@24333 ` 216` ``` "range (Rep o Abs) = A" ``` kleing@24333 ` 217` ``` by (simp add: set_Rep_Abs) ``` kleing@24333 ` 218` kleing@24333 ` 219` ```end ``` kleing@24333 ` 220` kleing@24333 ` 221` ```lemmas td_ext_def' = ``` kleing@24333 ` 222` ``` td_ext_def [unfolded type_definition_def td_ext_axioms_def] ``` kleing@24333 ` 223` kleing@24333 ` 224` ```end ``` kleing@24333 ` 225`