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