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