src/HOL/Import/HOL_Light_Maps.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63950 cdc1e59aa513
child 67399 eab6ce8368fa
permissions -rw-r--r--
executable domain membership checks
cezarykaliszyk@47258
     1
(*  Title:      HOL/Import/HOL_Light_Maps.thy
cezarykaliszyk@47258
     2
    Author:     Cezary Kaliszyk, University of Innsbruck
cezarykaliszyk@47258
     3
    Author:     Alexander Krauss, QAware GmbH
cezarykaliszyk@47258
     4
cezarykaliszyk@47258
     5
Based on earlier code by Steven Obua and Sebastian Skalberg
cezarykaliszyk@47258
     6
*)
cezarykaliszyk@47258
     7
wenzelm@63167
     8
section \<open>Type and constant mappings of HOL Light importer\<close>
cezarykaliszyk@47258
     9
cezarykaliszyk@47258
    10
theory HOL_Light_Maps
cezarykaliszyk@47258
    11
imports Import_Setup
cezarykaliszyk@47258
    12
begin
cezarykaliszyk@47258
    13
cezarykaliszyk@47258
    14
lemma [import_const T]:
cezarykaliszyk@47258
    15
  "True = ((\<lambda>p :: bool. p) = (\<lambda>p. p))"
cezarykaliszyk@47258
    16
  by simp
cezarykaliszyk@47258
    17
cezarykaliszyk@47258
    18
lemma [import_const "/\\"]:
wenzelm@61076
    19
  "(op \<and>) = (\<lambda>p q. (\<lambda>f. f p q :: bool) = (\<lambda>f. f True True))"
cezarykaliszyk@47258
    20
  by metis
cezarykaliszyk@47258
    21
cezarykaliszyk@47258
    22
lemma [import_const "==>"]:
wenzelm@61076
    23
  "(op \<longrightarrow>) = (\<lambda>(p::bool) q::bool. (p \<and> q) = p)"
cezarykaliszyk@47258
    24
  by auto
cezarykaliszyk@47258
    25
cezarykaliszyk@47258
    26
lemma [import_const "!"]:
wenzelm@61076
    27
  "All = (\<lambda>P::'A \<Rightarrow> bool. P = (\<lambda>x::'A. True))"
cezarykaliszyk@47258
    28
  by auto
cezarykaliszyk@47258
    29
cezarykaliszyk@47258
    30
lemma [import_const "?"]:
wenzelm@61076
    31
  "Ex = (\<lambda>P::'A \<Rightarrow> bool. All (\<lambda>q::bool. (All (\<lambda>x::'A::type. (P x) \<longrightarrow> q)) \<longrightarrow> q))"
cezarykaliszyk@47258
    32
  by auto
cezarykaliszyk@47258
    33
cezarykaliszyk@47258
    34
lemma [import_const "\\/"]:
cezarykaliszyk@47258
    35
  "(op \<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)"
cezarykaliszyk@47258
    36
  by auto
cezarykaliszyk@47258
    37
cezarykaliszyk@47258
    38
lemma [import_const F]:
cezarykaliszyk@47258
    39
  "False = (\<forall>p. p)"
cezarykaliszyk@47258
    40
  by auto
cezarykaliszyk@47258
    41
cezarykaliszyk@47258
    42
lemma [import_const "~"]:
cezarykaliszyk@47258
    43
  "Not = (\<lambda>p. p \<longrightarrow> False)"
cezarykaliszyk@47258
    44
  by simp
cezarykaliszyk@47258
    45
cezarykaliszyk@47258
    46
lemma [import_const "?!"]:
wenzelm@61076
    47
  "Ex1 = (\<lambda>P::'A \<Rightarrow> bool. Ex P \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y))"
cezarykaliszyk@47258
    48
  by auto
cezarykaliszyk@47258
    49
cezarykaliszyk@47258
    50
lemma [import_const "_FALSITY_"]: "False = False"
cezarykaliszyk@47258
    51
  by simp
cezarykaliszyk@47258
    52
wenzelm@61076
    53
lemma hl_ax1: "\<forall>t::'A \<Rightarrow> 'B. (\<lambda>x. t x) = t"
cezarykaliszyk@47258
    54
  by metis
cezarykaliszyk@47258
    55
wenzelm@61076
    56
lemma hl_ax2: "\<forall>P x::'A. P x \<longrightarrow> P (Eps P)"
cezarykaliszyk@47258
    57
  by (auto intro: someI)
cezarykaliszyk@47258
    58
cezarykaliszyk@47258
    59
lemma [import_const COND]:
cezarykaliszyk@47258
    60
  "If = (\<lambda>t (t1 :: 'A) t2. SOME x. (t = True \<longrightarrow> x = t1) \<and> (t = False \<longrightarrow> x = t2))"
cezarykaliszyk@47258
    61
  unfolding fun_eq_iff by auto
cezarykaliszyk@47258
    62
cezarykaliszyk@47258
    63
lemma [import_const o]:
wenzelm@61076
    64
  "(op \<circ>) = (\<lambda>(f::'B \<Rightarrow> 'C) g x::'A. f (g x))"
cezarykaliszyk@47258
    65
  unfolding fun_eq_iff by simp
cezarykaliszyk@47258
    66
wenzelm@61076
    67
lemma [import_const I]: "id = (\<lambda>x::'A. x)"
cezarykaliszyk@47258
    68
  by auto
cezarykaliszyk@47258
    69
cezarykaliszyk@47258
    70
lemma [import_type 1 one_ABS one_REP]:
cezarykaliszyk@47258
    71
  "type_definition Rep_unit Abs_unit (Collect (\<lambda>b. b))"
cezarykaliszyk@47258
    72
  by (metis (full_types) Collect_cong singleton_conv2 type_definition_unit)
cezarykaliszyk@47258
    73
wenzelm@61076
    74
lemma [import_const one]: "() = (SOME x::unit. True)"
cezarykaliszyk@47258
    75
  by auto
cezarykaliszyk@47258
    76
cezarykaliszyk@47258
    77
lemma [import_const mk_pair]:
wenzelm@61076
    78
  "Pair_Rep = (\<lambda>(x::'A) (y::'B) (a::'A) b::'B. a = x \<and> b = y)"
cezarykaliszyk@47258
    79
  by (simp add: Pair_Rep_def fun_eq_iff)
cezarykaliszyk@47258
    80
cezarykaliszyk@47258
    81
lemma [import_type prod ABS_prod REP_prod]:
wenzelm@61076
    82
  "type_definition Rep_prod Abs_prod (Collect (\<lambda>x::'A \<Rightarrow> 'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b))"
cezarykaliszyk@47258
    83
  using type_definition_prod[unfolded Product_Type.prod_def] by simp
cezarykaliszyk@47258
    84
wenzelm@61076
    85
lemma [import_const ","]: "Pair = (\<lambda>(x::'A) y::'B. Abs_prod (Pair_Rep x y))"
cezarykaliszyk@47258
    86
  by (metis Pair_def)
cezarykaliszyk@47258
    87
cezarykaliszyk@47258
    88
lemma [import_const FST]:
wenzelm@61076
    89
  "fst = (\<lambda>p::'A \<times> 'B. SOME x::'A. \<exists>y::'B. p = (x, y))"
cezarykaliszyk@47258
    90
  by auto
cezarykaliszyk@47258
    91
cezarykaliszyk@47258
    92
lemma [import_const SND]:
wenzelm@61076
    93
  "snd = (\<lambda>p::'A \<times> 'B. SOME y::'B. \<exists>x::'A. p = (x, y))"
cezarykaliszyk@47258
    94
  by auto
cezarykaliszyk@47258
    95
cezarykaliszyk@47364
    96
lemma CURRY_DEF[import_const CURRY]:
wenzelm@61076
    97
  "curry = (\<lambda>(f::'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
cezarykaliszyk@47364
    98
  using curry_def .
cezarykaliszyk@47258
    99
wenzelm@56266
   100
lemma [import_const ONE_ONE : inj]:
wenzelm@61076
   101
  "inj = (\<lambda>(f::'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
cezarykaliszyk@47258
   102
  by (auto simp add: fun_eq_iff inj_on_def)
cezarykaliszyk@47258
   103
wenzelm@56266
   104
lemma [import_const ONTO : surj]:
wenzelm@61076
   105
  "surj = (\<lambda>(f::'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)"
cezarykaliszyk@47258
   106
  by (auto simp add: fun_eq_iff)
cezarykaliszyk@47258
   107
wenzelm@61076
   108
lemma hl_ax3: "\<exists>f::ind \<Rightarrow> ind. inj f \<and> \<not> surj f"
cezarykaliszyk@47258
   109
  by (rule_tac x="Suc_Rep" in exI)
cezarykaliszyk@47258
   110
     (metis Suc_Rep_inject' injI Suc_Rep_not_Zero_Rep surjD)
cezarykaliszyk@47258
   111
wenzelm@56266
   112
import_type_map num : nat
wenzelm@56266
   113
import_const_map "_0" : zero_class.zero
wenzelm@56266
   114
import_const_map SUC : Suc
cezarykaliszyk@47258
   115
cezarykaliszyk@47258
   116
lemma NOT_SUC: "\<forall>n. Suc n \<noteq> 0"
cezarykaliszyk@47258
   117
  by simp
cezarykaliszyk@47258
   118
cezarykaliszyk@47258
   119
lemma SUC_INJ: "\<forall>m n. (Suc m = Suc n) = (m = n)"
cezarykaliszyk@47258
   120
  by simp
cezarykaliszyk@47258
   121
cezarykaliszyk@47258
   122
lemma num_INDUCTION:
cezarykaliszyk@47258
   123
  "\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)"
cezarykaliszyk@47258
   124
  by (auto intro: nat.induct)
cezarykaliszyk@47258
   125
cezarykaliszyk@47258
   126
lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)"
cezarykaliszyk@47258
   127
  by auto
cezarykaliszyk@47258
   128
cezarykaliszyk@47258
   129
definition [simp]: "bit0 n = 2 * n"
cezarykaliszyk@47258
   130
cezarykaliszyk@47258
   131
lemma [import_const BIT0]:
cezarykaliszyk@47258
   132
  "bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>n. fn (Suc n) = Suc (Suc (fn n))))"
cezarykaliszyk@47258
   133
  apply (auto intro!: some_equality[symmetric])
cezarykaliszyk@47258
   134
  apply (auto simp add: fun_eq_iff)
cezarykaliszyk@47258
   135
  apply (induct_tac x)
cezarykaliszyk@47258
   136
  apply auto
cezarykaliszyk@47258
   137
  done
cezarykaliszyk@47258
   138
cezarykaliszyk@47258
   139
definition [import_const BIT1, simp]:
cezarykaliszyk@47258
   140
  "bit1 = (\<lambda>x. Suc (bit0 x))"
cezarykaliszyk@47258
   141
cezarykaliszyk@47258
   142
definition [simp]: "pred n = n - 1"
cezarykaliszyk@47258
   143
wenzelm@56266
   144
lemma PRE[import_const PRE : pred]:
wenzelm@61076
   145
  "pred (id (0::nat)) = id (0::nat) \<and> (\<forall>n::nat. pred (Suc n) = n)"
cezarykaliszyk@47258
   146
  by simp
cezarykaliszyk@47258
   147
wenzelm@56266
   148
lemma ADD[import_const "+" : plus]:
cezarykaliszyk@47258
   149
  "(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))"
cezarykaliszyk@47258
   150
  by simp
cezarykaliszyk@47258
   151
wenzelm@56266
   152
lemma MULT[import_const "*" : times]:
cezarykaliszyk@47258
   153
  "(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)"
cezarykaliszyk@47258
   154
  by simp
cezarykaliszyk@47258
   155
wenzelm@56266
   156
lemma EXP[import_const EXP : power]:
cezarykaliszyk@47258
   157
  "(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
cezarykaliszyk@47258
   158
  by simp
cezarykaliszyk@47258
   159
wenzelm@56266
   160
lemma LE[import_const "<=" : less_eq]:
cezarykaliszyk@47258
   161
  "(\<forall>m :: nat. m \<le> (id 0) = (m = id 0)) \<and> (\<forall>m n. m \<le> (Suc n) = (m = Suc n \<or> m \<le> n))"
cezarykaliszyk@47258
   162
  by auto
cezarykaliszyk@47258
   163
wenzelm@56266
   164
lemma LT[import_const "<" : less]:
cezarykaliszyk@47258
   165
  "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
cezarykaliszyk@47258
   166
  by auto
cezarykaliszyk@47258
   167
wenzelm@56266
   168
lemma DEF_GE[import_const ">=" : greater_eq]:
cezarykaliszyk@47258
   169
  "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
cezarykaliszyk@47258
   170
  by simp
cezarykaliszyk@47258
   171
wenzelm@56266
   172
lemma DEF_GT[import_const ">" : greater]:
cezarykaliszyk@47258
   173
  "(op >) = (\<lambda>x y :: nat. y < x)"
cezarykaliszyk@47258
   174
  by simp
cezarykaliszyk@47258
   175
cezarykaliszyk@47258
   176
lemma DEF_MAX[import_const "MAX"]:
cezarykaliszyk@47258
   177
  "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
haftmann@54863
   178
  by (auto simp add: max.absorb_iff2 fun_eq_iff)
cezarykaliszyk@47258
   179
cezarykaliszyk@47258
   180
lemma DEF_MIN[import_const "MIN"]:
cezarykaliszyk@47258
   181
  "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
haftmann@54863
   182
  by (auto simp add: min.absorb_iff1 fun_eq_iff)
cezarykaliszyk@47258
   183
haftmann@58773
   184
definition even
haftmann@58773
   185
where
haftmann@58773
   186
  "even = Parity.even"
haftmann@58773
   187
  
wenzelm@56266
   188
lemma EVEN[import_const "EVEN" : even]:
wenzelm@61076
   189
  "even (id 0::nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
haftmann@58773
   190
  by (simp add: even_def)
cezarykaliszyk@47258
   191
wenzelm@56266
   192
lemma SUB[import_const "-" : minus]:
wenzelm@61076
   193
  "(\<forall>m::nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
cezarykaliszyk@47258
   194
  by simp
cezarykaliszyk@47258
   195
wenzelm@56266
   196
lemma FACT[import_const "FACT" : fact]:
cezarykaliszyk@47258
   197
  "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
cezarykaliszyk@47258
   198
  by simp
cezarykaliszyk@47258
   199
haftmann@63950
   200
import_const_map MOD : modulo
haftmann@60429
   201
import_const_map DIV : divide
cezarykaliszyk@47258
   202
cezarykaliszyk@47258
   203
lemma DIVISION_0:
wenzelm@61076
   204
  "\<forall>m n::nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"
cezarykaliszyk@47258
   205
  by simp
cezarykaliszyk@47258
   206
cezarykaliszyk@47364
   207
lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"]
wenzelm@56266
   208
import_const_map INL : Inl
wenzelm@56266
   209
import_const_map INR : Inr
cezarykaliszyk@47258
   210
cezarykaliszyk@47258
   211
lemma sum_INDUCT:
cezarykaliszyk@47364
   212
  "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
cezarykaliszyk@47258
   213
  by (auto intro: sum.induct)
cezarykaliszyk@47258
   214
cezarykaliszyk@47258
   215
lemma sum_RECURSION:
cezarykaliszyk@47364
   216
  "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
blanchet@55414
   217
  by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
cezarykaliszyk@47258
   218
wenzelm@56266
   219
lemma OUTL[import_const "OUTL" : projl]:
blanchet@55393
   220
  "Sum_Type.projl (Inl x) = x"
cezarykaliszyk@47258
   221
  by simp
cezarykaliszyk@47258
   222
wenzelm@56266
   223
lemma OUTR[import_const "OUTR" : projr]:
blanchet@55393
   224
  "Sum_Type.projr (Inr y) = y"
cezarykaliszyk@47258
   225
  by simp
cezarykaliszyk@47258
   226
wenzelm@56266
   227
import_type_map list : list
wenzelm@56266
   228
import_const_map NIL : Nil
wenzelm@56266
   229
import_const_map CONS : Cons
cezarykaliszyk@47258
   230
cezarykaliszyk@47258
   231
lemma list_INDUCT:
wenzelm@61076
   232
  "\<forall>P::'A list \<Rightarrow> bool. P [] \<and> (\<forall>a0 a1. P a1 \<longrightarrow> P (a0 # a1)) \<longrightarrow> (\<forall>x. P x)"
cezarykaliszyk@47258
   233
  using list.induct by auto
cezarykaliszyk@47258
   234
cezarykaliszyk@47258
   235
lemma list_RECURSION:
wenzelm@61076
   236
 "\<forall>nil' cons'. \<exists>fn::'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0::'A) a1::'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
blanchet@55413
   237
  by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
cezarykaliszyk@47258
   238
wenzelm@56266
   239
lemma HD[import_const HD : hd]:
wenzelm@61076
   240
  "hd ((h::'A) # t) = h"
cezarykaliszyk@47258
   241
  by simp
cezarykaliszyk@47258
   242
wenzelm@56266
   243
lemma TL[import_const TL : tl]:
wenzelm@61076
   244
  "tl ((h::'A) # t) = t"
cezarykaliszyk@47258
   245
  by simp
cezarykaliszyk@47258
   246
wenzelm@56266
   247
lemma APPEND[import_const APPEND : append]:
wenzelm@61076
   248
  "(\<forall>l::'A list. [] @ l = l) \<and> (\<forall>(h::'A) t l. (h # t) @ l = h # t @ l)"
cezarykaliszyk@47258
   249
  by simp
cezarykaliszyk@47258
   250
wenzelm@56266
   251
lemma REVERSE[import_const REVERSE : rev]:
wenzelm@61076
   252
  "rev [] = ([] :: 'A list) \<and> rev ((x::'A) # l) = rev l @ [x]"
cezarykaliszyk@47258
   253
  by simp
cezarykaliszyk@47258
   254
wenzelm@56266
   255
lemma LENGTH[import_const LENGTH : length]:
wenzelm@61076
   256
  "length ([] :: 'A list) = id 0 \<and> (\<forall>(h::'A) t. length (h # t) = Suc (length t))"
cezarykaliszyk@47258
   257
  by simp
cezarykaliszyk@47258
   258
wenzelm@56266
   259
lemma MAP[import_const MAP : map]:
wenzelm@61076
   260
  "(\<forall>f::'A \<Rightarrow> 'B. map f [] = []) \<and>
wenzelm@61076
   261
       (\<forall>(f::'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
cezarykaliszyk@47258
   262
  by simp
cezarykaliszyk@47258
   263
wenzelm@56266
   264
lemma LAST[import_const LAST : last]:
wenzelm@61076
   265
  "last ((h::'A) # t) = (if t = [] then h else last t)"
cezarykaliszyk@47258
   266
  by simp
cezarykaliszyk@47258
   267
wenzelm@56266
   268
lemma BUTLAST[import_const BUTLAST : butlast]:
cezarykaliszyk@47258
   269
    "butlast [] = ([] :: 't18337 list) \<and>
cezarykaliszyk@47258
   270
     butlast ((h :: 't18337) # t) = (if t = [] then [] else h # butlast t)"
cezarykaliszyk@47258
   271
  by simp
cezarykaliszyk@47258
   272
wenzelm@56266
   273
lemma REPLICATE[import_const REPLICATE : replicate]:
wenzelm@61076
   274
  "replicate (id (0::nat)) (x::'t18358) = [] \<and>
cezarykaliszyk@47258
   275
   replicate (Suc n) x = x # replicate n x"
cezarykaliszyk@47258
   276
  by simp
cezarykaliszyk@47258
   277
cezarykaliszyk@47258
   278
lemma NULL[import_const NULL : List.null]:
wenzelm@61076
   279
  "List.null ([]::'t18373 list) = True \<and> List.null ((h::'t18373) # t) = False"
cezarykaliszyk@47258
   280
  unfolding null_def by simp
cezarykaliszyk@47258
   281
wenzelm@56266
   282
lemma ALL[import_const ALL : list_all]:
wenzelm@61076
   283
  "list_all (P::'t18393 \<Rightarrow> bool) [] = True \<and>
cezarykaliszyk@47258
   284
  list_all P (h # t) = (P h \<and> list_all P t)"
cezarykaliszyk@47258
   285
  by simp
cezarykaliszyk@47258
   286
wenzelm@56266
   287
lemma EX[import_const EX : list_ex]:
wenzelm@61076
   288
  "list_ex (P::'t18414 \<Rightarrow> bool) [] = False \<and>
cezarykaliszyk@47258
   289
  list_ex P (h # t) = (P h \<or> list_ex P t)"
cezarykaliszyk@47258
   290
  by simp
cezarykaliszyk@47258
   291
wenzelm@56266
   292
lemma ITLIST[import_const ITLIST : foldr]:
wenzelm@61076
   293
  "foldr (f::'t18437 \<Rightarrow> 't18436 \<Rightarrow> 't18436) [] b = b \<and>
cezarykaliszyk@47258
   294
  foldr f (h # t) b = f h (foldr f t b)"
cezarykaliszyk@47258
   295
  by simp
cezarykaliszyk@47258
   296
wenzelm@56266
   297
lemma ALL2_DEF[import_const ALL2 : list_all2]:
wenzelm@61076
   298
  "list_all2 (P::'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2::'t18502 list) = (l2 = []) \<and>
wenzelm@61076
   299
  list_all2 P ((h1::'t18495) # (t1::'t18495 list)) l2 =
cezarykaliszyk@47258
   300
  (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
cezarykaliszyk@47258
   301
  by simp (induct_tac l2, simp_all)
cezarykaliszyk@47258
   302
wenzelm@56266
   303
lemma FILTER[import_const FILTER : filter]:
wenzelm@61076
   304
  "filter (P::'t18680 \<Rightarrow> bool) [] = [] \<and>
wenzelm@61076
   305
  filter P ((h::'t18680) # t) = (if P h then h # filter P t else filter P t)"
cezarykaliszyk@47258
   306
  by simp
cezarykaliszyk@47258
   307
wenzelm@56266
   308
lemma ZIP[import_const ZIP : zip]:
cezarykaliszyk@47258
   309
 "zip [] [] = ([] :: ('t18824 \<times> 't18825) list) \<and>
wenzelm@61076
   310
  zip ((h1::'t18849) # t1) ((h2::'t18850) # t2) = (h1, h2) # zip t1 t2"
cezarykaliszyk@47258
   311
  by simp
cezarykaliszyk@47258
   312
wenzelm@56266
   313
lemma WF[import_const WF : wfP]:
cezarykaliszyk@47364
   314
  "\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
cezarykaliszyk@47258
   315
proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
cezarykaliszyk@47258
   316
  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
cezarykaliszyk@47258
   317
  assume a: "xa \<in> Q"
cezarykaliszyk@47258
   318
  assume "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
cezarykaliszyk@47258
   319
  then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
cezarykaliszyk@47258
   320
  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
cezarykaliszyk@47258
   321
next
cezarykaliszyk@47258
   322
  fix x P and xa :: 'A and z
cezarykaliszyk@47258
   323
  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
cezarykaliszyk@47258
   324
  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
cezarykaliszyk@47258
   325
qed auto
cezarykaliszyk@47258
   326
cezarykaliszyk@47258
   327
end
cezarykaliszyk@47258
   328