src/HOL/Import/HOL4Compat.thy
 author haftmann Mon Mar 01 13:40:23 2010 +0100 (2010-03-01) changeset 35416 d8d7d1b785af parent 32960 69916a850301 child 37596 248db70c9bcf permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
 skalberg@14620 ` 1` ```(* Title: HOL/Import/HOL4Compat.thy ``` skalberg@14620 ` 2` ``` Author: Sebastian Skalberg (TU Muenchen) ``` skalberg@14620 ` 3` ```*) ``` skalberg@14620 ` 4` haftmann@30660 ` 5` ```theory HOL4Compat ``` haftmann@32479 ` 6` ```imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum ``` obua@19064 ` 7` ```begin ``` skalberg@14516 ` 8` haftmann@30660 ` 9` ```no_notation differentiable (infixl "differentiable" 60) ``` haftmann@30660 ` 10` ```no_notation sums (infixr "sums" 80) ``` haftmann@30660 ` 11` skalberg@14516 ` 12` ```lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))" ``` skalberg@14516 ` 13` ``` by auto ``` skalberg@14516 ` 14` skalberg@14516 ` 15` ```lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))" ``` skalberg@14516 ` 16` ``` by auto ``` skalberg@14516 ` 17` haftmann@35416 ` 18` ```definition LET :: "['a \ 'b,'a] \ 'b" where ``` skalberg@14516 ` 19` ``` "LET f s == f s" ``` skalberg@14516 ` 20` skalberg@14516 ` 21` ```lemma [hol4rew]: "LET f s = Let s f" ``` skalberg@14516 ` 22` ``` by (simp add: LET_def Let_def) ``` skalberg@14516 ` 23` skalberg@14516 ` 24` ```lemmas [hol4rew] = ONE_ONE_rew ``` skalberg@14516 ` 25` skalberg@14516 ` 26` ```lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)" ``` haftmann@30660 ` 27` ``` by simp ``` skalberg@14516 ` 28` skalberg@14516 ` 29` ```lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))" ``` skalberg@14516 ` 30` ``` by safe ``` skalberg@14516 ` 31` obua@17188 ` 32` ```(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1" ``` obua@17188 ` 33` ``` by simp*) ``` obua@17188 ` 34` skalberg@14516 ` 35` ```consts ``` skalberg@14516 ` 36` ``` ISL :: "'a + 'b => bool" ``` skalberg@14516 ` 37` ``` ISR :: "'a + 'b => bool" ``` skalberg@14516 ` 38` skalberg@14516 ` 39` ```primrec ISL_def: ``` skalberg@14516 ` 40` ``` "ISL (Inl x) = True" ``` skalberg@14516 ` 41` ``` "ISL (Inr x) = False" ``` skalberg@14516 ` 42` skalberg@14516 ` 43` ```primrec ISR_def: ``` skalberg@14516 ` 44` ``` "ISR (Inl x) = False" ``` skalberg@14516 ` 45` ``` "ISR (Inr x) = True" ``` skalberg@14516 ` 46` skalberg@14516 ` 47` ```lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))" ``` skalberg@14516 ` 48` ``` by simp ``` skalberg@14516 ` 49` skalberg@14516 ` 50` ```lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))" ``` skalberg@14516 ` 51` ``` by simp ``` skalberg@14516 ` 52` skalberg@14516 ` 53` ```consts ``` skalberg@14516 ` 54` ``` OUTL :: "'a + 'b => 'a" ``` skalberg@14516 ` 55` ``` OUTR :: "'a + 'b => 'b" ``` skalberg@14516 ` 56` skalberg@14516 ` 57` ```primrec OUTL_def: ``` skalberg@14516 ` 58` ``` "OUTL (Inl x) = x" ``` skalberg@14516 ` 59` skalberg@14516 ` 60` ```primrec OUTR_def: ``` skalberg@14516 ` 61` ``` "OUTR (Inr x) = x" ``` skalberg@14516 ` 62` skalberg@14516 ` 63` ```lemma OUTL: "OUTL (Inl x) = x" ``` skalberg@14516 ` 64` ``` by simp ``` skalberg@14516 ` 65` skalberg@14516 ` 66` ```lemma OUTR: "OUTR (Inr x) = x" ``` skalberg@14516 ` 67` ``` by simp ``` skalberg@14516 ` 68` skalberg@14516 ` 69` ```lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)" ``` skalberg@14516 ` 70` ``` by simp; ``` skalberg@14516 ` 71` skalberg@14516 ` 72` ```lemma one: "ALL v. v = ()" ``` skalberg@14516 ` 73` ``` by simp; ``` skalberg@14516 ` 74` skalberg@14516 ` 75` ```lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)" ``` skalberg@14516 ` 76` ``` by simp ``` skalberg@14516 ` 77` nipkow@30235 ` 78` ```lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)" ``` skalberg@14516 ` 79` ``` by simp ``` skalberg@14516 ` 80` skalberg@14516 ` 81` ```consts ``` skalberg@14516 ` 82` ``` IS_SOME :: "'a option => bool" ``` skalberg@14516 ` 83` ``` IS_NONE :: "'a option => bool" ``` skalberg@14516 ` 84` skalberg@14516 ` 85` ```primrec IS_SOME_def: ``` skalberg@14516 ` 86` ``` "IS_SOME (Some x) = True" ``` skalberg@14516 ` 87` ``` "IS_SOME None = False" ``` skalberg@14516 ` 88` skalberg@14516 ` 89` ```primrec IS_NONE_def: ``` skalberg@14516 ` 90` ``` "IS_NONE (Some x) = False" ``` skalberg@14516 ` 91` ``` "IS_NONE None = True" ``` skalberg@14516 ` 92` skalberg@14516 ` 93` ```lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)" ``` skalberg@14516 ` 94` ``` by simp ``` skalberg@14516 ` 95` skalberg@14516 ` 96` ```lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)" ``` skalberg@14516 ` 97` ``` by simp ``` skalberg@14516 ` 98` skalberg@14516 ` 99` ```consts ``` skalberg@14516 ` 100` ``` OPTION_JOIN :: "'a option option => 'a option" ``` skalberg@14516 ` 101` skalberg@14516 ` 102` ```primrec OPTION_JOIN_def: ``` skalberg@14516 ` 103` ``` "OPTION_JOIN None = None" ``` skalberg@14516 ` 104` ``` "OPTION_JOIN (Some x) = x" ``` skalberg@14516 ` 105` skalberg@14516 ` 106` ```lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)" ``` skalberg@14516 ` 107` ``` by simp; ``` skalberg@14516 ` 108` skalberg@14516 ` 109` ```lemma PAIR: "(fst x,snd x) = x" ``` skalberg@14516 ` 110` ``` by simp ``` skalberg@14516 ` 111` skalberg@14516 ` 112` ```lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))" ``` skalberg@14516 ` 113` ``` by (simp add: prod_fun_def split_def) ``` skalberg@14516 ` 114` skalberg@14516 ` 115` ```lemma pair_case_def: "split = split" ``` skalberg@14516 ` 116` ``` ..; ``` skalberg@14516 ` 117` skalberg@14516 ` 118` ```lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)" ``` skalberg@14516 ` 119` ``` by auto ``` skalberg@14516 ` 120` haftmann@35416 ` 121` ```definition nat_gt :: "nat => nat => bool" where ``` skalberg@14516 ` 122` ``` "nat_gt == %m n. n < m" ``` haftmann@35416 ` 123` haftmann@35416 ` 124` ```definition nat_ge :: "nat => nat => bool" where ``` skalberg@14516 ` 125` ``` "nat_ge == %m n. nat_gt m n | m = n" ``` skalberg@14516 ` 126` skalberg@14516 ` 127` ```lemma [hol4rew]: "nat_gt m n = (n < m)" ``` skalberg@14516 ` 128` ``` by (simp add: nat_gt_def) ``` skalberg@14516 ` 129` skalberg@14516 ` 130` ```lemma [hol4rew]: "nat_ge m n = (n <= m)" ``` skalberg@14516 ` 131` ``` by (auto simp add: nat_ge_def nat_gt_def) ``` skalberg@14516 ` 132` skalberg@14516 ` 133` ```lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)" ``` skalberg@14516 ` 134` ``` by simp ``` skalberg@14516 ` 135` skalberg@14516 ` 136` ```lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)" ``` skalberg@14516 ` 137` ``` by auto ``` skalberg@14516 ` 138` skalberg@14516 ` 139` ```lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)" ``` skalberg@14516 ` 140` ```proof safe ``` skalberg@14516 ` 141` ``` assume "m < n" ``` skalberg@14516 ` 142` ``` def P == "%n. n <= m" ``` skalberg@14516 ` 143` ``` have "(!n. P (Suc n) \ P n) & P m & ~P n" ``` skalberg@14516 ` 144` ``` proof (auto simp add: P_def) ``` skalberg@14516 ` 145` ``` assume "n <= m" ``` skalberg@14516 ` 146` ``` from prems ``` skalberg@14516 ` 147` ``` show False ``` skalberg@14516 ` 148` ``` by auto ``` skalberg@14516 ` 149` ``` qed ``` skalberg@14516 ` 150` ``` thus "? P. (!n. P (Suc n) \ P n) & P m & ~P n" ``` skalberg@14516 ` 151` ``` by auto ``` skalberg@14516 ` 152` ```next ``` skalberg@14516 ` 153` ``` fix P ``` skalberg@14516 ` 154` ``` assume alln: "!n. P (Suc n) \ P n" ``` skalberg@14516 ` 155` ``` assume pm: "P m" ``` skalberg@14516 ` 156` ``` assume npn: "~P n" ``` skalberg@14516 ` 157` ``` have "!k q. q + k = m \ P q" ``` skalberg@14516 ` 158` ``` proof ``` skalberg@14516 ` 159` ``` fix k ``` skalberg@14516 ` 160` ``` show "!q. q + k = m \ P q" ``` skalberg@14516 ` 161` ``` proof (induct k,simp_all) ``` wenzelm@23389 ` 162` ``` show "P m" by fact ``` skalberg@14516 ` 163` ``` next ``` skalberg@14516 ` 164` ``` fix k ``` skalberg@14516 ` 165` ``` assume ind: "!q. q + k = m \ P q" ``` skalberg@14516 ` 166` ``` show "!q. Suc (q + k) = m \ P q" ``` skalberg@14516 ` 167` ``` proof (rule+) ``` wenzelm@32960 ` 168` ``` fix q ``` wenzelm@32960 ` 169` ``` assume "Suc (q + k) = m" ``` wenzelm@32960 ` 170` ``` hence "(Suc q) + k = m" ``` wenzelm@32960 ` 171` ``` by simp ``` wenzelm@32960 ` 172` ``` with ind ``` wenzelm@32960 ` 173` ``` have psq: "P (Suc q)" ``` wenzelm@32960 ` 174` ``` by simp ``` wenzelm@32960 ` 175` ``` from alln ``` wenzelm@32960 ` 176` ``` have "P (Suc q) --> P q" ``` wenzelm@32960 ` 177` ``` .. ``` wenzelm@32960 ` 178` ``` with psq ``` wenzelm@32960 ` 179` ``` show "P q" ``` wenzelm@32960 ` 180` ``` by simp ``` skalberg@14516 ` 181` ``` qed ``` skalberg@14516 ` 182` ``` qed ``` skalberg@14516 ` 183` ``` qed ``` skalberg@14516 ` 184` ``` hence "!q. q + (m - n) = m \ P q" ``` skalberg@14516 ` 185` ``` .. ``` skalberg@14516 ` 186` ``` hence hehe: "n + (m - n) = m \ P n" ``` skalberg@14516 ` 187` ``` .. ``` skalberg@14516 ` 188` ``` show "m < n" ``` skalberg@14516 ` 189` ``` proof (rule classical) ``` skalberg@14516 ` 190` ``` assume "~(m 'a) => nat => 'a => 'a" where ``` haftmann@30971 ` 203` ``` "FUNPOW f n == f ^^ n" ``` skalberg@14516 ` 204` haftmann@30971 ` 205` ```lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) & ``` haftmann@30971 ` 206` ``` (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))" ``` haftmann@30952 ` 207` ``` by (simp add: funpow_swap1) ``` skalberg@14516 ` 208` haftmann@30971 ` 209` ```lemma [hol4rew]: "FUNPOW f n = f ^^ n" ``` skalberg@14516 ` 210` ``` by (simp add: FUNPOW_def) ``` skalberg@14516 ` 211` skalberg@14516 ` 212` ```lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))" ``` skalberg@14516 ` 213` ``` by simp ``` skalberg@14516 ` 214` skalberg@14516 ` 215` ```lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)" ``` skalberg@14516 ` 216` ``` by simp ``` skalberg@14516 ` 217` skalberg@14516 ` 218` ```lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))" ``` haftmann@30952 ` 219` ``` by (simp) arith ``` skalberg@14516 ` 220` skalberg@14516 ` 221` ```lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)" ``` skalberg@14516 ` 222` ``` by (simp add: max_def) ``` skalberg@14516 ` 223` skalberg@14516 ` 224` ```lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)" ``` skalberg@14516 ` 225` ``` by (simp add: min_def) ``` skalberg@14516 ` 226` skalberg@14516 ` 227` ```lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)" ``` skalberg@14516 ` 228` ``` by simp ``` skalberg@14516 ` 229` haftmann@35416 ` 230` ```definition ALT_ZERO :: nat where ``` skalberg@14516 ` 231` ``` "ALT_ZERO == 0" ``` haftmann@35416 ` 232` haftmann@35416 ` 233` ```definition NUMERAL_BIT1 :: "nat \ nat" where ``` skalberg@14516 ` 234` ``` "NUMERAL_BIT1 n == n + (n + Suc 0)" ``` haftmann@35416 ` 235` haftmann@35416 ` 236` ```definition NUMERAL_BIT2 :: "nat \ nat" where ``` skalberg@14516 ` 237` ``` "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))" ``` haftmann@35416 ` 238` haftmann@35416 ` 239` ```definition NUMERAL :: "nat \ nat" where ``` skalberg@14516 ` 240` ``` "NUMERAL x == x" ``` skalberg@14516 ` 241` skalberg@14516 ` 242` ```lemma [hol4rew]: "NUMERAL ALT_ZERO = 0" ``` skalberg@14516 ` 243` ``` by (simp add: ALT_ZERO_def NUMERAL_def) ``` skalberg@14516 ` 244` skalberg@14516 ` 245` ```lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1" ``` skalberg@14516 ` 246` ``` by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def) ``` skalberg@14516 ` 247` skalberg@14516 ` 248` ```lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2" ``` skalberg@14516 ` 249` ``` by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def) ``` skalberg@14516 ` 250` skalberg@14516 ` 251` ```lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)" ``` skalberg@14516 ` 252` ``` by auto ``` skalberg@14516 ` 253` skalberg@14516 ` 254` ```lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)" ``` skalberg@14516 ` 255` ``` by simp; ``` skalberg@14516 ` 256` skalberg@14516 ` 257` ```lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)" ``` skalberg@14516 ` 258` ``` by (auto simp add: dvd_def); ``` skalberg@14516 ` 259` skalberg@14516 ` 260` ```lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)" ``` skalberg@14516 ` 261` ``` by simp ``` skalberg@14516 ` 262` skalberg@14516 ` 263` ```consts ``` skalberg@14516 ` 264` ``` list_size :: "('a \ nat) \ 'a list \ nat" ``` skalberg@14516 ` 265` skalberg@14516 ` 266` ```primrec ``` skalberg@14516 ` 267` ``` "list_size f [] = 0" ``` skalberg@14516 ` 268` ``` "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)" ``` skalberg@14516 ` 269` skalberg@14516 ` 270` ```lemma list_size_def: "(!f. list_size f [] = 0) & ``` skalberg@14516 ` 271` ``` (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))" ``` skalberg@14516 ` 272` ``` by simp ``` skalberg@14516 ` 273` skalberg@14516 ` 274` ```lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \ v = v') & ``` skalberg@14516 ` 275` ``` (!a0 a1. (M' = a0#a1) \ (f a0 a1 = f' a0 a1)) --> ``` skalberg@14516 ` 276` ``` (list_case v f M = list_case v' f' M')" ``` skalberg@14516 ` 277` ```proof clarify ``` skalberg@14516 ` 278` ``` fix M M' v f ``` skalberg@14516 ` 279` ``` assume "M' = [] \ v = v'" ``` skalberg@14516 ` 280` ``` and "!a0 a1. M' = a0 # a1 \ f a0 a1 = f' a0 a1" ``` skalberg@14516 ` 281` ``` show "list_case v f M' = list_case v' f' M'" ``` skalberg@14516 ` 282` ``` proof (rule List.list.case_cong) ``` skalberg@14516 ` 283` ``` show "M' = M'" ``` skalberg@14516 ` 284` ``` .. ``` skalberg@14516 ` 285` ``` next ``` skalberg@14516 ` 286` ``` assume "M' = []" ``` skalberg@14516 ` 287` ``` with prems ``` skalberg@14516 ` 288` ``` show "v = v'" ``` skalberg@14516 ` 289` ``` by auto ``` skalberg@14516 ` 290` ``` next ``` skalberg@14516 ` 291` ``` fix a0 a1 ``` skalberg@14516 ` 292` ``` assume "M' = a0 # a1" ``` skalberg@14516 ` 293` ``` with prems ``` skalberg@14516 ` 294` ``` show "f a0 a1 = f' a0 a1" ``` skalberg@14516 ` 295` ``` by auto ``` skalberg@14516 ` 296` ``` qed ``` skalberg@14516 ` 297` ```qed ``` skalberg@14516 ` 298` skalberg@14516 ` 299` ```lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))" ``` skalberg@14516 ` 300` ```proof safe ``` skalberg@14516 ` 301` ``` fix f0 f1 ``` skalberg@14516 ` 302` ``` def fn == "list_rec f0 f1" ``` skalberg@14516 ` 303` ``` have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))" ``` skalberg@14516 ` 304` ``` by (simp add: fn_def) ``` skalberg@14516 ` 305` ``` thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))" ``` skalberg@14516 ` 306` ``` by auto ``` skalberg@14516 ` 307` ```qed ``` skalberg@14516 ` 308` skalberg@14516 ` 309` ```lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)" ``` skalberg@14516 ` 310` ```proof safe ``` skalberg@14516 ` 311` ``` def fn == "list_rec x (%h t r. f r h t)" ``` skalberg@14516 ` 312` ``` have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)" ``` skalberg@14516 ` 313` ``` by (simp add: fn_def) ``` skalberg@14516 ` 314` ``` thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)" ``` skalberg@14516 ` 315` ``` by auto ``` skalberg@14516 ` 316` ```next ``` skalberg@14516 ` 317` ``` fix fn1 fn2 ``` skalberg@14516 ` 318` ``` assume "ALL h t. fn1 (h # t) = f (fn1 t) h t" ``` skalberg@14516 ` 319` ``` assume "ALL h t. fn2 (h # t) = f (fn2 t) h t" ``` skalberg@14516 ` 320` ``` assume "fn2 [] = fn1 []" ``` skalberg@14516 ` 321` ``` show "fn1 = fn2" ``` skalberg@14516 ` 322` ``` proof ``` skalberg@14516 ` 323` ``` fix xs ``` skalberg@14516 ` 324` ``` show "fn1 xs = fn2 xs" ``` skalberg@14516 ` 325` ``` by (induct xs,simp_all add: prems) ``` skalberg@14516 ` 326` ``` qed ``` skalberg@14516 ` 327` ```qed ``` skalberg@14516 ` 328` skalberg@14516 ` 329` ```lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)" ``` skalberg@14516 ` 330` ``` by simp ``` skalberg@14516 ` 331` haftmann@35416 ` 332` ```definition sum :: "nat list \ nat" where ``` skalberg@14516 ` 333` ``` "sum l == foldr (op +) l 0" ``` skalberg@14516 ` 334` skalberg@14516 ` 335` ```lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)" ``` skalberg@14516 ` 336` ``` by (simp add: sum_def) ``` skalberg@14516 ` 337` skalberg@14516 ` 338` ```lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)" ``` skalberg@14516 ` 339` ``` by simp ``` skalberg@14516 ` 340` skalberg@14516 ` 341` ```lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))" ``` skalberg@14516 ` 342` ``` by simp ``` skalberg@14516 ` 343` skalberg@14516 ` 344` ```lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))" ``` skalberg@14516 ` 345` ``` by simp ``` skalberg@14516 ` 346` skalberg@14516 ` 347` ```lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)" ``` skalberg@14516 ` 348` ``` by simp ``` skalberg@14516 ` 349` skalberg@14516 ` 350` ```lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))" ``` skalberg@14516 ` 351` ``` by auto ``` skalberg@14516 ` 352` skalberg@14516 ` 353` ```lemma FILTER: "(!P. filter P [] = []) & (!P h t. ``` skalberg@14516 ` 354` ``` filter P (h#t) = (if P h then h#filter P t else filter P t))" ``` skalberg@14516 ` 355` ``` by simp ``` skalberg@14516 ` 356` skalberg@14516 ` 357` ```lemma REPLICATE: "(ALL x. replicate 0 x = []) & ``` skalberg@14516 ` 358` ``` (ALL n x. replicate (Suc n) x = x # replicate n x)" ``` skalberg@14516 ` 359` ``` by simp ``` skalberg@14516 ` 360` haftmann@35416 ` 361` ```definition FOLDR :: "[['a,'b]\'b,'b,'a list] \ 'b" where ``` skalberg@14516 ` 362` ``` "FOLDR f e l == foldr f l e" ``` skalberg@14516 ` 363` skalberg@14516 ` 364` ```lemma [hol4rew]: "FOLDR f e l = foldr f l e" ``` skalberg@14516 ` 365` ``` by (simp add: FOLDR_def) ``` skalberg@14516 ` 366` skalberg@14516 ` 367` ```lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))" ``` skalberg@14516 ` 368` ``` by simp ``` skalberg@14516 ` 369` skalberg@14516 ` 370` ```lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)" ``` skalberg@14516 ` 371` ``` by simp ``` skalberg@14516 ` 372` skalberg@14516 ` 373` ```lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))" ``` skalberg@14516 ` 374` ``` by simp ``` skalberg@14516 ` 375` skalberg@14516 ` 376` ```consts ``` skalberg@14516 ` 377` ``` list_exists :: "['a \ bool,'a list] \ bool" ``` skalberg@14516 ` 378` skalberg@14516 ` 379` ```primrec ``` skalberg@14516 ` 380` ``` list_exists_Nil: "list_exists P Nil = False" ``` skalberg@14516 ` 381` ``` list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)" ``` skalberg@14516 ` 382` skalberg@14516 ` 383` ```lemma list_exists_DEF: "(!P. list_exists P [] = False) & ``` skalberg@14516 ` 384` ``` (!P h t. list_exists P (h#t) = (P h | list_exists P t))" ``` skalberg@14516 ` 385` ``` by simp ``` skalberg@14516 ` 386` skalberg@14516 ` 387` ```consts ``` skalberg@14516 ` 388` ``` map2 :: "[['a,'b]\'c,'a list,'b list] \ 'c list" ``` skalberg@14516 ` 389` skalberg@14516 ` 390` ```primrec ``` skalberg@14516 ` 391` ``` map2_Nil: "map2 f [] l2 = []" ``` skalberg@14516 ` 392` ``` map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)" ``` skalberg@14516 ` 393` skalberg@14516 ` 394` ```lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)" ``` skalberg@14516 ` 395` ``` by simp ``` skalberg@14516 ` 396` skalberg@14516 ` 397` ```lemma list_INDUCT: "\ P [] ; !t. P t \ (!h. P (h#t)) \ \ !l. P l" ``` skalberg@14516 ` 398` ```proof ``` skalberg@14516 ` 399` ``` fix l ``` skalberg@14516 ` 400` ``` assume "P []" ``` skalberg@14516 ` 401` ``` assume allt: "!t. P t \ (!h. P (h # t))" ``` skalberg@14516 ` 402` ``` show "P l" ``` skalberg@14516 ` 403` ``` proof (induct l) ``` wenzelm@23389 ` 404` ``` show "P []" by fact ``` skalberg@14516 ` 405` ``` next ``` skalberg@14516 ` 406` ``` fix h t ``` skalberg@14516 ` 407` ``` assume "P t" ``` skalberg@14516 ` 408` ``` with allt ``` skalberg@14516 ` 409` ``` have "!h. P (h # t)" ``` skalberg@14516 ` 410` ``` by auto ``` skalberg@14516 ` 411` ``` thus "P (h # t)" ``` skalberg@14516 ` 412` ``` .. ``` skalberg@14516 ` 413` ``` qed ``` skalberg@14516 ` 414` ```qed ``` skalberg@14516 ` 415` skalberg@14516 ` 416` ```lemma list_CASES: "(l = []) | (? t h. l = h#t)" ``` skalberg@14516 ` 417` ``` by (induct l,auto) ``` skalberg@14516 ` 418` haftmann@35416 ` 419` ```definition ZIP :: "'a list * 'b list \ ('a * 'b) list" where ``` skalberg@14516 ` 420` ``` "ZIP == %(a,b). zip a b" ``` skalberg@14516 ` 421` skalberg@14516 ` 422` ```lemma ZIP: "(zip [] [] = []) & ``` skalberg@14516 ` 423` ``` (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)" ``` skalberg@14516 ` 424` ``` by simp ``` skalberg@14516 ` 425` skalberg@14516 ` 426` ```lemma [hol4rew]: "ZIP (a,b) = zip a b" ``` skalberg@14516 ` 427` ``` by (simp add: ZIP_def) ``` skalberg@14516 ` 428` skalberg@14516 ` 429` ```consts ``` skalberg@14516 ` 430` ``` unzip :: "('a * 'b) list \ 'a list * 'b list" ``` skalberg@14516 ` 431` skalberg@14516 ` 432` ```primrec ``` skalberg@14516 ` 433` ``` unzip_Nil: "unzip [] = ([],[])" ``` skalberg@14516 ` 434` ``` unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))" ``` skalberg@14516 ` 435` skalberg@14516 ` 436` ```lemma UNZIP: "(unzip [] = ([],[])) & ``` skalberg@14516 ` 437` ``` (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))" ``` skalberg@14516 ` 438` ``` by (simp add: Let_def) ``` skalberg@14516 ` 439` skalberg@14516 ` 440` ```lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])" ``` skalberg@14516 ` 441` ``` by simp; ``` skalberg@14516 ` 442` skalberg@14516 ` 443` ```lemma REAL_SUP_ALLPOS: "\ ALL x. P (x::real) \ 0 < x ; EX x. P x; EX z. ALL x. P x \ x < z \ \ EX s. ALL y. (EX x. P x & y < x) = (y < s)" ``` skalberg@14516 ` 444` ```proof safe ``` skalberg@14516 ` 445` ``` fix x z ``` skalberg@14516 ` 446` ``` assume allx: "ALL x. P x \ 0 < x" ``` skalberg@14516 ` 447` ``` assume px: "P x" ``` skalberg@14516 ` 448` ``` assume allx': "ALL x. P x \ x < z" ``` skalberg@14516 ` 449` ``` have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)" ``` skalberg@14516 ` 450` ``` proof (rule posreal_complete) ``` skalberg@14516 ` 451` ``` show "ALL x : Collect P. 0 < x" ``` skalberg@14516 ` 452` ``` proof safe ``` skalberg@14516 ` 453` ``` fix x ``` skalberg@14516 ` 454` ``` assume "P x" ``` skalberg@14516 ` 455` ``` from allx ``` skalberg@14516 ` 456` ``` have "P x \ 0 < x" ``` wenzelm@32960 ` 457` ``` .. ``` skalberg@14516 ` 458` ``` thus "0 < x" ``` wenzelm@32960 ` 459` ``` by (simp add: prems) ``` skalberg@14516 ` 460` ``` qed ``` skalberg@14516 ` 461` ``` next ``` skalberg@14516 ` 462` ``` from px ``` skalberg@14516 ` 463` ``` show "EX x. x : Collect P" ``` skalberg@14516 ` 464` ``` by auto ``` skalberg@14516 ` 465` ``` next ``` skalberg@14516 ` 466` ``` from allx' ``` skalberg@14516 ` 467` ``` show "EX y. ALL x : Collect P. x < y" ``` skalberg@14516 ` 468` ``` apply simp ``` skalberg@14516 ` 469` ``` .. ``` skalberg@14516 ` 470` ``` qed ``` skalberg@14516 ` 471` ``` thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)" ``` skalberg@14516 ` 472` ``` by simp ``` skalberg@14516 ` 473` ```qed ``` skalberg@14516 ` 474` skalberg@14516 ` 475` ```lemma REAL_10: "~((1::real) = 0)" ``` skalberg@14516 ` 476` ``` by simp ``` skalberg@14516 ` 477` skalberg@14516 ` 478` ```lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z" ``` skalberg@14516 ` 479` ``` by simp ``` skalberg@14516 ` 480` skalberg@14516 ` 481` ```lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z" ``` skalberg@14516 ` 482` ``` by simp ``` skalberg@14516 ` 483` skalberg@14516 ` 484` ```lemma REAL_ADD_LINV: "-x + x = (0::real)" ``` skalberg@14516 ` 485` ``` by simp ``` skalberg@14516 ` 486` skalberg@14516 ` 487` ```lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1" ``` skalberg@14516 ` 488` ``` by simp ``` skalberg@14516 ` 489` skalberg@14516 ` 490` ```lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x" ``` skalberg@14516 ` 491` ``` by auto; ``` skalberg@14516 ` 492` skalberg@14516 ` 493` ```lemma [hol4rew]: "real (0::nat) = 0" ``` skalberg@14516 ` 494` ``` by simp ``` skalberg@14516 ` 495` skalberg@14516 ` 496` ```lemma [hol4rew]: "real (1::nat) = 1" ``` skalberg@14516 ` 497` ``` by simp ``` skalberg@14516 ` 498` skalberg@14516 ` 499` ```lemma [hol4rew]: "real (2::nat) = 2" ``` skalberg@14516 ` 500` ``` by simp ``` skalberg@14516 ` 501` skalberg@14516 ` 502` ```lemma real_lte: "((x::real) <= y) = (~(y < x))" ``` skalberg@14516 ` 503` ``` by auto ``` skalberg@14516 ` 504` skalberg@14516 ` 505` ```lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)" ``` skalberg@14516 ` 506` ``` by (simp add: real_of_nat_Suc) ``` skalberg@14516 ` 507` skalberg@14516 ` 508` ```lemma abs: "abs (x::real) = (if 0 <= x then x else -x)" ``` paulson@15003 ` 509` ``` by (simp add: abs_if) ``` skalberg@14516 ` 510` skalberg@14516 ` 511` ```lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" ``` paulson@15003 ` 512` ``` by simp ``` skalberg@14516 ` 513` haftmann@35416 ` 514` ```definition real_gt :: "real => real => bool" where ``` skalberg@14516 ` 515` ``` "real_gt == %x y. y < x" ``` skalberg@14516 ` 516` skalberg@14516 ` 517` ```lemma [hol4rew]: "real_gt x y = (y < x)" ``` skalberg@14516 ` 518` ``` by (simp add: real_gt_def) ``` skalberg@14516 ` 519` skalberg@14516 ` 520` ```lemma real_gt: "ALL x (y::real). (y < x) = (y < x)" ``` skalberg@14516 ` 521` ``` by simp ``` skalberg@14516 ` 522` haftmann@35416 ` 523` ```definition real_ge :: "real => real => bool" where ``` skalberg@14516 ` 524` ``` "real_ge x y == y <= x" ``` skalberg@14516 ` 525` skalberg@14516 ` 526` ```lemma [hol4rew]: "real_ge x y = (y <= x)" ``` skalberg@14516 ` 527` ``` by (simp add: real_ge_def) ``` skalberg@14516 ` 528` skalberg@14516 ` 529` ```lemma real_ge: "ALL x y. (y <= x) = (y <= x)" ``` skalberg@14516 ` 530` ``` by simp ``` skalberg@14516 ` 531` skalberg@14516 ` 532` ```end ```