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