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