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 \<Rightarrow> 'b,'a] \<Rightarrow> '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) \<longrightarrow> 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) \<longrightarrow> 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) \<longrightarrow> 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 \<longrightarrow> P q"
skalberg@14516
   158
  proof
skalberg@14516
   159
    fix k
skalberg@14516
   160
    show "!q. q + k = m \<longrightarrow> 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 \<longrightarrow> P q"
skalberg@14516
   166
      show "!q. Suc (q + k) = m \<longrightarrow> 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 \<longrightarrow> P q"
skalberg@14516
   185
    ..
skalberg@14516
   186
  hence hehe: "n + (m - n) = m \<longrightarrow> P n"
skalberg@14516
   187
    ..
skalberg@14516
   188
  show "m < n"
skalberg@14516
   189
  proof (rule classical)
skalberg@14516
   190
    assume "~(m<n)"
skalberg@14516
   191
    hence "n <= m"
skalberg@14516
   192
      by simp
skalberg@14516
   193
    with hehe
skalberg@14516
   194
    have "P n"
skalberg@14516
   195
      by simp
skalberg@14516
   196
    with npn
skalberg@14516
   197
    show "m < n"
skalberg@14516
   198
      ..
skalberg@14516
   199
  qed
skalberg@14516
   200
qed;
skalberg@14516
   201
haftmann@35416
   202
definition FUNPOW :: "('a => '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 \<Rightarrow> nat" where 
skalberg@14516
   234
  "NUMERAL_BIT1 n == n + (n + Suc 0)"
haftmann@35416
   235
haftmann@35416
   236
definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where 
skalberg@14516
   237
  "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
haftmann@35416
   238
haftmann@35416
   239
definition NUMERAL :: "nat \<Rightarrow> 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 \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 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' = [] \<longrightarrow>  v = v') &
skalberg@14516
   275
           (!a0 a1. (M' = a0#a1) \<longrightarrow> (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' = [] \<longrightarrow> v = v'"
skalberg@14516
   280
    and "!a0 a1. M' = a0 # a1 \<longrightarrow> 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 \<Rightarrow> 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]\<Rightarrow>'b,'b,'a list] \<Rightarrow> '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 \<Rightarrow> bool,'a list] \<Rightarrow> 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]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> '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: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !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 \<longrightarrow> (!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 \<Rightarrow> ('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 \<Rightarrow> '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: "\<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
   444
proof safe
skalberg@14516
   445
  fix x z
skalberg@14516
   446
  assume allx: "ALL x. P x \<longrightarrow> 0 < x"
skalberg@14516
   447
  assume px: "P x"
skalberg@14516
   448
  assume allx': "ALL x. P x \<longrightarrow> 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 \<longrightarrow> 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