src/HOL/Import/HOL4Compat.thy
author obua
Wed Feb 15 23:57:06 2006 +0100 (2006-02-15)
changeset 19064 bf19cc5a7899
parent 17188 a26a4fc323ed
child 20269 c40070317ab8
permissions -rw-r--r--
fixed bugs, added caching
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)
skalberg@14516
   160
      show "P m" .
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)))"
skalberg@14516
   224
  apply simp
skalberg@14516
   225
  apply arith
skalberg@14516
   226
  done
skalberg@14516
   227
skalberg@14516
   228
lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
skalberg@14516
   229
  by (simp add: max_def)
skalberg@14516
   230
skalberg@14516
   231
lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)"
skalberg@14516
   232
  by (simp add: min_def)
skalberg@14516
   233
skalberg@14516
   234
lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
skalberg@14516
   235
  by simp
skalberg@14516
   236
skalberg@14516
   237
constdefs
skalberg@14516
   238
  ALT_ZERO :: nat
skalberg@14516
   239
  "ALT_ZERO == 0"
skalberg@14516
   240
  NUMERAL_BIT1 :: "nat \<Rightarrow> nat"
skalberg@14516
   241
  "NUMERAL_BIT1 n == n + (n + Suc 0)"
skalberg@14516
   242
  NUMERAL_BIT2 :: "nat \<Rightarrow> nat"
skalberg@14516
   243
  "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
skalberg@14516
   244
  NUMERAL :: "nat \<Rightarrow> nat"
skalberg@14516
   245
  "NUMERAL x == x"
skalberg@14516
   246
skalberg@14516
   247
lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
skalberg@14516
   248
  by (simp add: ALT_ZERO_def NUMERAL_def)
skalberg@14516
   249
skalberg@14516
   250
lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1"
skalberg@14516
   251
  by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def)
skalberg@14516
   252
skalberg@14516
   253
lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2"
skalberg@14516
   254
  by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def)
skalberg@14516
   255
skalberg@14516
   256
lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)"
skalberg@14516
   257
  by auto
skalberg@14516
   258
skalberg@14516
   259
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
   260
  by simp;
skalberg@14516
   261
skalberg@14516
   262
lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
skalberg@14516
   263
  by (auto simp add: dvd_def);
skalberg@14516
   264
skalberg@14516
   265
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
   266
  by simp
skalberg@14516
   267
skalberg@14516
   268
consts
skalberg@14516
   269
  list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
skalberg@14516
   270
skalberg@14516
   271
primrec
skalberg@14516
   272
  "list_size f [] = 0"
skalberg@14516
   273
  "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
skalberg@14516
   274
skalberg@14516
   275
lemma list_size_def: "(!f. list_size f [] = 0) &
skalberg@14516
   276
         (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
skalberg@14516
   277
  by simp
skalberg@14516
   278
skalberg@14516
   279
lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow>  v = v') &
skalberg@14516
   280
           (!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) -->
skalberg@14516
   281
           (list_case v f M = list_case v' f' M')"
skalberg@14516
   282
proof clarify
skalberg@14516
   283
  fix M M' v f
skalberg@14516
   284
  assume "M' = [] \<longrightarrow> v = v'"
skalberg@14516
   285
    and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
skalberg@14516
   286
  show "list_case v f M' = list_case v' f' M'"
skalberg@14516
   287
  proof (rule List.list.case_cong)
skalberg@14516
   288
    show "M' = M'"
skalberg@14516
   289
      ..
skalberg@14516
   290
  next
skalberg@14516
   291
    assume "M' = []"
skalberg@14516
   292
    with prems
skalberg@14516
   293
    show "v = v'"
skalberg@14516
   294
      by auto
skalberg@14516
   295
  next
skalberg@14516
   296
    fix a0 a1
skalberg@14516
   297
    assume "M' = a0 # a1"
skalberg@14516
   298
    with prems
skalberg@14516
   299
    show "f a0 a1 = f' a0 a1"
skalberg@14516
   300
      by auto
skalberg@14516
   301
  qed
skalberg@14516
   302
qed
skalberg@14516
   303
skalberg@14516
   304
lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))"
skalberg@14516
   305
proof safe
skalberg@14516
   306
  fix f0 f1
skalberg@14516
   307
  def fn == "list_rec f0 f1"
skalberg@14516
   308
  have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
skalberg@14516
   309
    by (simp add: fn_def)
skalberg@14516
   310
  thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
skalberg@14516
   311
    by auto
skalberg@14516
   312
qed
skalberg@14516
   313
skalberg@14516
   314
lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)"
skalberg@14516
   315
proof safe
skalberg@14516
   316
  def fn == "list_rec x (%h t r. f r h t)"
skalberg@14516
   317
  have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
skalberg@14516
   318
    by (simp add: fn_def)
skalberg@14516
   319
  thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
skalberg@14516
   320
    by auto
skalberg@14516
   321
next
skalberg@14516
   322
  fix fn1 fn2
skalberg@14516
   323
  assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
skalberg@14516
   324
  assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
skalberg@14516
   325
  assume "fn2 [] = fn1 []"
skalberg@14516
   326
  show "fn1 = fn2"
skalberg@14516
   327
  proof
skalberg@14516
   328
    fix xs
skalberg@14516
   329
    show "fn1 xs = fn2 xs"
skalberg@14516
   330
      by (induct xs,simp_all add: prems) 
skalberg@14516
   331
  qed
skalberg@14516
   332
qed
skalberg@14516
   333
skalberg@14516
   334
lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
skalberg@14516
   335
  by simp
skalberg@14516
   336
skalberg@14516
   337
constdefs
skalberg@14516
   338
  sum :: "nat list \<Rightarrow> nat"
skalberg@14516
   339
  "sum l == foldr (op +) l 0"
skalberg@14516
   340
skalberg@14516
   341
lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
skalberg@14516
   342
  by (simp add: sum_def)
skalberg@14516
   343
skalberg@14516
   344
lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)"
skalberg@14516
   345
  by simp
skalberg@14516
   346
skalberg@14516
   347
lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))"
skalberg@14516
   348
  by simp
skalberg@14516
   349
skalberg@14516
   350
lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))"
skalberg@14516
   351
  by simp
skalberg@14516
   352
skalberg@14516
   353
lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
skalberg@14516
   354
  by simp
skalberg@14516
   355
skalberg@14516
   356
lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
skalberg@14516
   357
  by auto
skalberg@14516
   358
skalberg@14516
   359
lemma FILTER: "(!P. filter P [] = []) & (!P h t.
skalberg@14516
   360
           filter P (h#t) = (if P h then h#filter P t else filter P t))"
skalberg@14516
   361
  by simp
skalberg@14516
   362
skalberg@14516
   363
lemma REPLICATE: "(ALL x. replicate 0 x = []) &
skalberg@14516
   364
  (ALL n x. replicate (Suc n) x = x # replicate n x)"
skalberg@14516
   365
  by simp
skalberg@14516
   366
skalberg@14516
   367
constdefs
skalberg@14516
   368
  FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b"
skalberg@14516
   369
  "FOLDR f e l == foldr f l e"
skalberg@14516
   370
skalberg@14516
   371
lemma [hol4rew]: "FOLDR f e l = foldr f l e"
skalberg@14516
   372
  by (simp add: FOLDR_def)
skalberg@14516
   373
skalberg@14516
   374
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
   375
  by simp
skalberg@14516
   376
skalberg@14516
   377
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
   378
  by simp
skalberg@14516
   379
skalberg@14516
   380
lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
skalberg@14516
   381
  by simp
skalberg@14516
   382
skalberg@14516
   383
consts
skalberg@14516
   384
  list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
skalberg@14516
   385
skalberg@14516
   386
primrec
skalberg@14516
   387
  list_exists_Nil: "list_exists P Nil = False"
skalberg@14516
   388
  list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
skalberg@14516
   389
skalberg@14516
   390
lemma list_exists_DEF: "(!P. list_exists P [] = False) &
skalberg@14516
   391
         (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
skalberg@14516
   392
  by simp
skalberg@14516
   393
skalberg@14516
   394
consts
skalberg@14516
   395
  map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
skalberg@14516
   396
skalberg@14516
   397
primrec
skalberg@14516
   398
  map2_Nil: "map2 f [] l2 = []"
skalberg@14516
   399
  map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
skalberg@14516
   400
skalberg@14516
   401
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
   402
  by simp
skalberg@14516
   403
skalberg@14516
   404
lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l"
skalberg@14516
   405
proof
skalberg@14516
   406
  fix l
skalberg@14516
   407
  assume "P []"
skalberg@14516
   408
  assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
skalberg@14516
   409
  show "P l"
skalberg@14516
   410
  proof (induct l)
skalberg@14516
   411
    show "P []" .
skalberg@14516
   412
  next
skalberg@14516
   413
    fix h t
skalberg@14516
   414
    assume "P t"
skalberg@14516
   415
    with allt
skalberg@14516
   416
    have "!h. P (h # t)"
skalberg@14516
   417
      by auto
skalberg@14516
   418
    thus "P (h # t)"
skalberg@14516
   419
      ..
skalberg@14516
   420
  qed
skalberg@14516
   421
qed
skalberg@14516
   422
skalberg@14516
   423
lemma list_CASES: "(l = []) | (? t h. l = h#t)"
skalberg@14516
   424
  by (induct l,auto)
skalberg@14516
   425
skalberg@14516
   426
constdefs
skalberg@14516
   427
  ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list"
skalberg@14516
   428
  "ZIP == %(a,b). zip a b"
skalberg@14516
   429
skalberg@14516
   430
lemma ZIP: "(zip [] [] = []) &
skalberg@14516
   431
  (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)"
skalberg@14516
   432
  by simp
skalberg@14516
   433
skalberg@14516
   434
lemma [hol4rew]: "ZIP (a,b) = zip a b"
skalberg@14516
   435
  by (simp add: ZIP_def)
skalberg@14516
   436
skalberg@14516
   437
consts
skalberg@14516
   438
  unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
skalberg@14516
   439
skalberg@14516
   440
primrec
skalberg@14516
   441
  unzip_Nil: "unzip [] = ([],[])"
skalberg@14516
   442
  unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
skalberg@14516
   443
skalberg@14516
   444
lemma UNZIP: "(unzip [] = ([],[])) &
skalberg@14516
   445
         (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
skalberg@14516
   446
  by (simp add: Let_def)
skalberg@14516
   447
skalberg@14516
   448
lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
skalberg@14516
   449
  by simp;
skalberg@14516
   450
skalberg@14516
   451
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
   452
proof safe
skalberg@14516
   453
  fix x z
skalberg@14516
   454
  assume allx: "ALL x. P x \<longrightarrow> 0 < x"
skalberg@14516
   455
  assume px: "P x"
skalberg@14516
   456
  assume allx': "ALL x. P x \<longrightarrow> x < z"
skalberg@14516
   457
  have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
skalberg@14516
   458
  proof (rule posreal_complete)
skalberg@14516
   459
    show "ALL x : Collect P. 0 < x"
skalberg@14516
   460
    proof safe
skalberg@14516
   461
      fix x
skalberg@14516
   462
      assume "P x"
skalberg@14516
   463
      from allx
skalberg@14516
   464
      have "P x \<longrightarrow> 0 < x"
skalberg@14516
   465
	..
skalberg@14516
   466
      thus "0 < x"
skalberg@14516
   467
	by (simp add: prems)
skalberg@14516
   468
    qed
skalberg@14516
   469
  next
skalberg@14516
   470
    from px
skalberg@14516
   471
    show "EX x. x : Collect P"
skalberg@14516
   472
      by auto
skalberg@14516
   473
  next
skalberg@14516
   474
    from allx'
skalberg@14516
   475
    show "EX y. ALL x : Collect P. x < y"
skalberg@14516
   476
      apply simp
skalberg@14516
   477
      ..
skalberg@14516
   478
  qed
skalberg@14516
   479
  thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)"
skalberg@14516
   480
    by simp
skalberg@14516
   481
qed
skalberg@14516
   482
skalberg@14516
   483
lemma REAL_10: "~((1::real) = 0)"
skalberg@14516
   484
  by simp
skalberg@14516
   485
skalberg@14516
   486
lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
skalberg@14516
   487
  by simp
skalberg@14516
   488
skalberg@14516
   489
lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
skalberg@14516
   490
  by simp
skalberg@14516
   491
skalberg@14516
   492
lemma REAL_ADD_LINV:  "-x + x = (0::real)"
skalberg@14516
   493
  by simp
skalberg@14516
   494
skalberg@14516
   495
lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1"
skalberg@14516
   496
  by simp
skalberg@14516
   497
skalberg@14516
   498
lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
skalberg@14516
   499
  by auto;
skalberg@14516
   500
skalberg@14516
   501
lemma [hol4rew]: "real (0::nat) = 0"
skalberg@14516
   502
  by simp
skalberg@14516
   503
skalberg@14516
   504
lemma [hol4rew]: "real (1::nat) = 1"
skalberg@14516
   505
  by simp
skalberg@14516
   506
skalberg@14516
   507
lemma [hol4rew]: "real (2::nat) = 2"
skalberg@14516
   508
  by simp
skalberg@14516
   509
skalberg@14516
   510
lemma real_lte: "((x::real) <= y) = (~(y < x))"
skalberg@14516
   511
  by auto
skalberg@14516
   512
skalberg@14516
   513
lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)"
skalberg@14516
   514
  by (simp add: real_of_nat_Suc)
skalberg@14516
   515
skalberg@14516
   516
lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
paulson@15003
   517
  by (simp add: abs_if)
skalberg@14516
   518
skalberg@14516
   519
lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
paulson@15003
   520
  by simp
skalberg@14516
   521
skalberg@14516
   522
constdefs
skalberg@14516
   523
  real_gt :: "real => real => bool" 
skalberg@14516
   524
  "real_gt == %x y. y < x"
skalberg@14516
   525
skalberg@14516
   526
lemma [hol4rew]: "real_gt x y = (y < x)"
skalberg@14516
   527
  by (simp add: real_gt_def)
skalberg@14516
   528
skalberg@14516
   529
lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
skalberg@14516
   530
  by simp
skalberg@14516
   531
skalberg@14516
   532
constdefs
skalberg@14516
   533
  real_ge :: "real => real => bool"
skalberg@14516
   534
  "real_ge x y == y <= x"
skalberg@14516
   535
skalberg@14516
   536
lemma [hol4rew]: "real_ge x y = (y <= x)"
skalberg@14516
   537
  by (simp add: real_ge_def)
skalberg@14516
   538
skalberg@14516
   539
lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
skalberg@14516
   540
  by simp
skalberg@14516
   541
skalberg@14516
   542
end