src/HOL/Library/Extended.thy
 author nipkow Wed Mar 06 12:17:52 2013 +0100 (2013-03-06) changeset 51357 ac4c1cf1b001 parent 51338 054d1653950f child 51358 0c376ef98559 permissions -rw-r--r--
extended numerals
 nipkow@51338 ` 1` ```(* Author: Tobias Nipkow, TU München ``` nipkow@51338 ` 2` nipkow@51338 ` 3` ```A theory of types extended with a greatest and a least element. ``` nipkow@51338 ` 4` ```Oriented towards numeric types, hence "\" and "-\". ``` nipkow@51338 ` 5` ```*) ``` nipkow@51338 ` 6` nipkow@51338 ` 7` ```theory Extended ``` nipkow@51338 ` 8` ```imports Main ``` nipkow@51338 ` 9` ```begin ``` nipkow@51338 ` 10` nipkow@51338 ` 11` ```datatype 'a extended = Fin 'a | Pinf ("\") | Minf ("-\") ``` nipkow@51338 ` 12` nipkow@51338 ` 13` ```lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust] ``` nipkow@51338 ` 14` ```lemmas extended_cases3 = extended.exhaust[case_product extended_cases2] ``` nipkow@51338 ` 15` nipkow@51357 ` 16` nipkow@51338 ` 17` ```instantiation extended :: (order)order ``` nipkow@51338 ` 18` ```begin ``` nipkow@51338 ` 19` nipkow@51338 ` 20` ```fun less_eq_extended :: "'a extended \ 'a extended \ bool" where ``` nipkow@51338 ` 21` ```"Fin x \ Fin y = (x \ y)" | ``` nipkow@51338 ` 22` ```"_ \ Pinf = True" | ``` nipkow@51338 ` 23` ```"Minf \ _ = True" | ``` nipkow@51338 ` 24` ```"(_::'a extended) \ _ = False" ``` nipkow@51338 ` 25` nipkow@51338 ` 26` ```lemma less_eq_extended_cases: ``` nipkow@51338 ` 27` ``` "x \ y = (case x of Fin x \ (case y of Fin y \ x \ y | Pinf \ True | Minf \ False) ``` nipkow@51338 ` 28` ``` | Pinf \ y=Pinf | Minf \ True)" ``` nipkow@51338 ` 29` ```by(induct x y rule: less_eq_extended.induct)(auto split: extended.split) ``` nipkow@51338 ` 30` nipkow@51338 ` 31` ```definition less_extended :: "'a extended \ 'a extended \ bool" where ``` nipkow@51338 ` 32` ```"((x::'a extended) < y) = (x \ y & \ x \ y)" ``` nipkow@51338 ` 33` nipkow@51338 ` 34` ```instance ``` nipkow@51338 ` 35` ```proof ``` nipkow@51338 ` 36` ``` case goal1 show ?case by(rule less_extended_def) ``` nipkow@51338 ` 37` ```next ``` nipkow@51338 ` 38` ``` case goal2 show ?case by(cases x) auto ``` nipkow@51338 ` 39` ```next ``` nipkow@51338 ` 40` ``` case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits) ``` nipkow@51338 ` 41` ```next ``` nipkow@51338 ` 42` ``` case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits) ``` nipkow@51338 ` 43` ```qed ``` nipkow@51338 ` 44` nipkow@51338 ` 45` ```end ``` nipkow@51338 ` 46` nipkow@51338 ` 47` ```instance extended :: (linorder)linorder ``` nipkow@51338 ` 48` ```proof ``` nipkow@51338 ` 49` ``` case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits) ``` nipkow@51338 ` 50` ```qed ``` nipkow@51338 ` 51` nipkow@51338 ` 52` ```lemma Minf_le[simp]: "Minf \ y" ``` nipkow@51338 ` 53` ```by(cases y) auto ``` nipkow@51338 ` 54` ```lemma le_Pinf[simp]: "x \ Pinf" ``` nipkow@51338 ` 55` ```by(cases x) auto ``` nipkow@51338 ` 56` ```lemma le_Minf[simp]: "x \ Minf \ x = Minf" ``` nipkow@51338 ` 57` ```by(cases x) auto ``` nipkow@51338 ` 58` ```lemma Pinf_le[simp]: "Pinf \ x \ x = Pinf" ``` nipkow@51338 ` 59` ```by(cases x) auto ``` nipkow@51338 ` 60` nipkow@51338 ` 61` ```lemma less_extended_simps[simp]: ``` nipkow@51338 ` 62` ``` "Fin x < Fin y = (x < y)" ``` nipkow@51338 ` 63` ``` "Fin x < Pinf = True" ``` nipkow@51338 ` 64` ``` "Fin x < Minf = False" ``` nipkow@51338 ` 65` ``` "Pinf < h = False" ``` nipkow@51338 ` 66` ``` "Minf < Fin x = True" ``` nipkow@51338 ` 67` ``` "Minf < Pinf = True" ``` nipkow@51338 ` 68` ``` "l < Minf = False" ``` nipkow@51338 ` 69` ```by (auto simp add: less_extended_def) ``` nipkow@51338 ` 70` nipkow@51338 ` 71` ```lemma min_extended_simps[simp]: ``` nipkow@51338 ` 72` ``` "min (Fin x) (Fin y) = Fin(min x y)" ``` nipkow@51338 ` 73` ``` "min xx Pinf = xx" ``` nipkow@51338 ` 74` ``` "min xx Minf = Minf" ``` nipkow@51338 ` 75` ``` "min Pinf yy = yy" ``` nipkow@51338 ` 76` ``` "min Minf yy = Minf" ``` nipkow@51338 ` 77` ```by (auto simp add: min_def) ``` nipkow@51338 ` 78` nipkow@51338 ` 79` ```lemma max_extended_simps[simp]: ``` nipkow@51338 ` 80` ``` "max (Fin x) (Fin y) = Fin(max x y)" ``` nipkow@51338 ` 81` ``` "max xx Pinf = Pinf" ``` nipkow@51338 ` 82` ``` "max xx Minf = xx" ``` nipkow@51338 ` 83` ``` "max Pinf yy = Pinf" ``` nipkow@51338 ` 84` ``` "max Minf yy = yy" ``` nipkow@51338 ` 85` ```by (auto simp add: max_def) ``` nipkow@51338 ` 86` nipkow@51338 ` 87` nipkow@51357 ` 88` ```instantiation extended :: (zero)zero ``` nipkow@51357 ` 89` ```begin ``` nipkow@51357 ` 90` ```definition "0 = Fin(0::'a)" ``` nipkow@51357 ` 91` ```instance .. ``` nipkow@51357 ` 92` ```end ``` nipkow@51357 ` 93` nipkow@51357 ` 94` ```instantiation extended :: (one)one ``` nipkow@51357 ` 95` ```begin ``` nipkow@51357 ` 96` ```definition "1 = Fin(1::'a)" ``` nipkow@51357 ` 97` ```instance .. ``` nipkow@51357 ` 98` ```end ``` nipkow@51357 ` 99` nipkow@51338 ` 100` ```instantiation extended :: (plus)plus ``` nipkow@51338 ` 101` ```begin ``` nipkow@51338 ` 102` nipkow@51338 ` 103` ```text {* The following definition of of addition is totalized ``` nipkow@51338 ` 104` ```to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *} ``` nipkow@51338 ` 105` nipkow@51338 ` 106` ```fun plus_extended where ``` nipkow@51338 ` 107` ```"Fin x + Fin y = Fin(x+y)" | ``` nipkow@51338 ` 108` ```"Fin x + Pinf = Pinf" | ``` nipkow@51338 ` 109` ```"Pinf + Fin x = Pinf" | ``` nipkow@51338 ` 110` ```"Pinf + Pinf = Pinf" | ``` nipkow@51338 ` 111` ```"Minf + Fin y = Minf" | ``` nipkow@51338 ` 112` ```"Fin x + Minf = Minf" | ``` nipkow@51338 ` 113` ```"Minf + Minf = Minf" | ``` nipkow@51338 ` 114` ```"Minf + Pinf = Pinf" | ``` nipkow@51338 ` 115` ```"Pinf + Minf = Pinf" ``` nipkow@51338 ` 116` nipkow@51338 ` 117` ```instance .. ``` nipkow@51338 ` 118` nipkow@51338 ` 119` ```end ``` nipkow@51338 ` 120` nipkow@51338 ` 121` nipkow@51338 ` 122` ```instance extended :: (ab_semigroup_add)ab_semigroup_add ``` nipkow@51338 ` 123` ```proof ``` nipkow@51338 ` 124` ``` fix a b c :: "'a extended" ``` nipkow@51338 ` 125` ``` show "a + b = b + a" ``` nipkow@51338 ` 126` ``` by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps) ``` nipkow@51338 ` 127` ``` show "a + b + c = a + (b + c)" ``` nipkow@51338 ` 128` ``` by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps) ``` nipkow@51338 ` 129` ```qed ``` nipkow@51338 ` 130` nipkow@51338 ` 131` ```instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add ``` nipkow@51338 ` 132` ```proof ``` nipkow@51338 ` 133` ``` fix a b c :: "'a extended" ``` nipkow@51338 ` 134` ``` assume "a \ b" then show "c + a \ c + b" ``` nipkow@51338 ` 135` ``` by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono) ``` nipkow@51338 ` 136` ```qed ``` nipkow@51338 ` 137` nipkow@51357 ` 138` ```instance extended :: (comm_monoid_add)comm_monoid_add ``` nipkow@51338 ` 139` ```proof ``` nipkow@51338 ` 140` ``` fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto ``` nipkow@51338 ` 141` ```qed ``` nipkow@51338 ` 142` nipkow@51338 ` 143` ```instantiation extended :: (uminus)uminus ``` nipkow@51338 ` 144` ```begin ``` nipkow@51338 ` 145` nipkow@51338 ` 146` ```fun uminus_extended where ``` nipkow@51338 ` 147` ```"- (Fin x) = Fin (- x)" | ``` nipkow@51338 ` 148` ```"- Pinf = Minf" | ``` nipkow@51338 ` 149` ```"- Minf = Pinf" ``` nipkow@51338 ` 150` nipkow@51338 ` 151` ```instance .. ``` nipkow@51338 ` 152` nipkow@51338 ` 153` ```end ``` nipkow@51338 ` 154` nipkow@51338 ` 155` nipkow@51338 ` 156` ```instantiation extended :: (ab_group_add)minus ``` nipkow@51338 ` 157` ```begin ``` nipkow@51338 ` 158` ```definition "x - y = x + -(y::'a extended)" ``` nipkow@51338 ` 159` ```instance .. ``` nipkow@51338 ` 160` ```end ``` nipkow@51338 ` 161` nipkow@51338 ` 162` ```lemma minus_extended_simps[simp]: ``` nipkow@51338 ` 163` ``` "Fin x - Fin y = Fin(x - y)" ``` nipkow@51338 ` 164` ``` "Fin x - Pinf = Minf" ``` nipkow@51338 ` 165` ``` "Fin x - Minf = Pinf" ``` nipkow@51338 ` 166` ``` "Pinf - Fin y = Pinf" ``` nipkow@51338 ` 167` ``` "Pinf - Minf = Pinf" ``` nipkow@51338 ` 168` ``` "Minf - Fin y = Minf" ``` nipkow@51338 ` 169` ``` "Minf - Pinf = Minf" ``` nipkow@51338 ` 170` ``` "Minf - Minf = Pinf" ``` nipkow@51338 ` 171` ``` "Pinf - Pinf = Pinf" ``` nipkow@51338 ` 172` ```by (simp_all add: minus_extended_def) ``` nipkow@51338 ` 173` nipkow@51357 ` 174` nipkow@51357 ` 175` ```text{* Numerals: *} ``` nipkow@51357 ` 176` nipkow@51357 ` 177` ```instance extended :: ("{ab_semigroup_add,one}")numeral .. ``` nipkow@51357 ` 178` nipkow@51357 ` 179` ```lemma Fin_numeral: "Fin(numeral w) = numeral w" ``` nipkow@51357 ` 180` ``` apply (induct w rule: num_induct) ``` nipkow@51357 ` 181` ``` apply (simp only: numeral_One one_extended_def) ``` nipkow@51357 ` 182` ``` apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric]) ``` nipkow@51357 ` 183` ``` done ``` nipkow@51357 ` 184` nipkow@51357 ` 185` nipkow@51338 ` 186` ```instantiation extended :: (lattice)bounded_lattice ``` nipkow@51338 ` 187` ```begin ``` nipkow@51338 ` 188` nipkow@51338 ` 189` ```definition "bot = Minf" ``` nipkow@51338 ` 190` ```definition "top = Pinf" ``` nipkow@51338 ` 191` nipkow@51338 ` 192` ```fun inf_extended :: "'a extended \ 'a extended \ 'a extended" where ``` nipkow@51338 ` 193` ```"inf_extended (Fin i) (Fin j) = Fin (inf i j)" | ``` nipkow@51338 ` 194` ```"inf_extended a Minf = Minf" | ``` nipkow@51338 ` 195` ```"inf_extended Minf a = Minf" | ``` nipkow@51338 ` 196` ```"inf_extended Pinf a = a" | ``` nipkow@51338 ` 197` ```"inf_extended a Pinf = a" ``` nipkow@51338 ` 198` nipkow@51338 ` 199` ```fun sup_extended :: "'a extended \ 'a extended \ 'a extended" where ``` nipkow@51338 ` 200` ```"sup_extended (Fin i) (Fin j) = Fin (sup i j)" | ``` nipkow@51338 ` 201` ```"sup_extended a Pinf = Pinf" | ``` nipkow@51338 ` 202` ```"sup_extended Pinf a = Pinf" | ``` nipkow@51338 ` 203` ```"sup_extended Minf a = a" | ``` nipkow@51338 ` 204` ```"sup_extended a Minf = a" ``` nipkow@51338 ` 205` nipkow@51338 ` 206` ```instance ``` nipkow@51338 ` 207` ```proof ``` nipkow@51338 ` 208` ``` fix x y z ::"'a extended" ``` nipkow@51338 ` 209` ``` show "inf x y \ x" "inf x y \ y" "\x \ y; x \ z\ \ x \ inf y z" ``` nipkow@51338 ` 210` ``` "x \ sup x y" "y \ sup x y" "\y \ x; z \ x\ \ sup y z \ x" "bot \ x" "x \ top" ``` nipkow@51338 ` 211` ``` apply (atomize (full)) ``` nipkow@51338 ` 212` ``` apply (cases rule: extended_cases3[of x y z]) ``` nipkow@51338 ` 213` ``` apply (auto simp: bot_extended_def top_extended_def) ``` nipkow@51338 ` 214` ``` done ``` nipkow@51338 ` 215` ```qed ``` nipkow@51338 ` 216` ```end ``` nipkow@51338 ` 217` nipkow@51338 ` 218` ```end ``` nipkow@51338 ` 219`