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