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