HOL/Import: Fix errors with _mk_list
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Sat Jul 16 00:01:17 2011 +0200 (2011-07-16)
changeset 4384316f2fd9103bd
parent 43842 f035d867fb41
child 43844 33e20b7d7e72
child 43852 7411fbf0a325
HOL/Import: Fix errors with _mk_list
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOLLight/HOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/HOLLightList.thy
     1.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Jul 15 16:51:01 2011 +0200
     1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Jul 16 00:01:17 2011 +0200
     1.3 @@ -30,15 +30,18 @@
     1.4  
     1.5    (* list_of_set uses Isabelle lists with HOLLight CARD *)
     1.6    DEF_list_of_set LIST_OF_SET_PROPERTIES SET_OF_LIST_OF_SET LENGTH_LIST_OF_SET
     1.7 -  MEM_LIST_OF_SET FINITE_SET_OF_LIST
     1.8 +  MEM_LIST_OF_SET HAS_SIZE_SET_OF_LIST FINITE_SET_OF_LIST
     1.9    (* UNIV *)
    1.10 -  DIMINDEX_FINITE_SUM  DIMINDEX_HAS_SIZE_FINITE_SUM
    1.11 -  FSTCART_PASTECART SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
    1.12 +  DIMINDEX_FINITE_SUM  DIMINDEX_HAS_SIZE_FINITE_SUM FSTCART_PASTECART
    1.13 +  SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
    1.14    (* Reals *)
    1.15    (* TYDEF_real DEF_real_of_num DEF_real_neg DEF_real_add DEF_real_mul DEF_real_le
    1.16    DEF_real_inv REAL_HREAL_LEMMA1 REAL_HREAL_LEMMA2 *)
    1.17    (* Integers *)
    1.18    (* TYDEF_int DEF_int_divides DEF_int_coprime*)
    1.19 +  (* HOLLight CARD and CASEWISE with Isabelle lists *)
    1.20 +  CARD_SET_OF_LIST_LE CASEWISE CASEWISE_CASES RECURSION_CASEWISE CASEWISE_WORKS
    1.21 +  WF_REC_CASES RECURSION_CASEWISE_PAIRWISE
    1.22  
    1.23  ;type_maps
    1.24    bool > HOL.bool
     2.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Fri Jul 15 16:51:01 2011 +0200
     2.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Sat Jul 16 00:01:17 2011 +0200
     2.3 @@ -3857,9 +3857,6 @@
     2.4  lemma EQ_UNIV: "(ALL x::'A. x : (s::'A => bool)) = (s = UNIV)"
     2.5    by (import hollight EQ_UNIV)
     2.6  
     2.7 -lemma UNIV_SUBSET: "(UNIV <= (x::'A => bool)) = (x = UNIV)"
     2.8 -  by (import hollight UNIV_SUBSET)
     2.9 -
    2.10  lemma SING_SUBSET: "({xa::'q_44493} <= (x::'q_44493 => bool)) = (xa : x)"
    2.11    by (import hollight SING_SUBSET)
    2.12  
    2.13 @@ -5205,25 +5202,25 @@
    2.14    by (import hollight FINITE_SUPPORT)
    2.15  
    2.16  lemma SUPPORT_CLAUSES: "(ALL x::'q_60297 => 'q_60530.
    2.17 -    support (u_4372::'q_60530 => 'q_60530 => 'q_60530) x {} = {}) &
    2.18 +    support (u_4371::'q_60530 => 'q_60530 => 'q_60530) x {} = {}) &
    2.19  (ALL (x::'q_60345 => 'q_60530) (xa::'q_60345) xb::'q_60345 => bool.
    2.20 -    support u_4372 x (insert xa xb) =
    2.21 -    (if x xa = neutral u_4372 then support u_4372 x xb
    2.22 -     else insert xa (support u_4372 x xb))) &
    2.23 +    support u_4371 x (insert xa xb) =
    2.24 +    (if x xa = neutral u_4371 then support u_4371 x xb
    2.25 +     else insert xa (support u_4371 x xb))) &
    2.26  (ALL (x::'q_60378 => 'q_60530) (xa::'q_60378) xb::'q_60378 => bool.
    2.27 -    support u_4372 x (xb - {xa}) = support u_4372 x xb - {xa}) &
    2.28 +    support u_4371 x (xb - {xa}) = support u_4371 x xb - {xa}) &
    2.29  (ALL (x::'q_60416 => 'q_60530) (xa::'q_60416 => bool) xb::'q_60416 => bool.
    2.30 -    support u_4372 x (xa Un xb) =
    2.31 -    support u_4372 x xa Un support u_4372 x xb) &
    2.32 +    support u_4371 x (xa Un xb) =
    2.33 +    support u_4371 x xa Un support u_4371 x xb) &
    2.34  (ALL (x::'q_60454 => 'q_60530) (xa::'q_60454 => bool) xb::'q_60454 => bool.
    2.35 -    support u_4372 x (xa Int xb) =
    2.36 -    support u_4372 x xa Int support u_4372 x xb) &
    2.37 +    support u_4371 x (xa Int xb) =
    2.38 +    support u_4371 x xa Int support u_4371 x xb) &
    2.39  (ALL (x::'q_60492 => 'q_60530) (xa::'q_60492 => bool) xb::'q_60492 => bool.
    2.40 -    support u_4372 x (xa - xb) =
    2.41 -    support u_4372 x xa - support u_4372 x xb) &
    2.42 +    support u_4371 x (xa - xb) =
    2.43 +    support u_4371 x xa - support u_4371 x xb) &
    2.44  (ALL (x::'q_60529 => 'q_60520) (xa::'q_60520 => 'q_60530)
    2.45      xb::'q_60529 => bool.
    2.46 -    support u_4372 xa (x ` xb) = x ` support u_4372 (xa o x) xb)"
    2.47 +    support u_4371 xa (x ` xb) = x ` support u_4371 (xa o x) xb)"
    2.48    by (import hollight SUPPORT_CLAUSES)
    2.49  
    2.50  lemma SUPPORT_DELTA: "support (x::'q_60556 => 'q_60556 => 'q_60556)
    2.51 @@ -5253,13 +5250,13 @@
    2.52   else neutral x)"
    2.53    by (import hollight ITERATE_EXPAND_CASES)
    2.54  
    2.55 -lemma ITERATE_CLAUSES_GEN: "monoidal (u_4372::'B => 'B => 'B)
    2.56 -==> (ALL f::'A => 'B. iterate u_4372 {} f = neutral u_4372) &
    2.57 +lemma ITERATE_CLAUSES_GEN: "monoidal (u_4371::'B => 'B => 'B)
    2.58 +==> (ALL f::'A => 'B. iterate u_4371 {} f = neutral u_4371) &
    2.59      (ALL (f::'A => 'B) (x::'A) s::'A => bool.
    2.60 -        monoidal u_4372 & finite (support u_4372 f s) -->
    2.61 -        iterate u_4372 (insert x s) f =
    2.62 -        (if x : s then iterate u_4372 s f
    2.63 -         else u_4372 (f x) (iterate u_4372 s f)))"
    2.64 +        monoidal u_4371 & finite (support u_4371 f s) -->
    2.65 +        iterate u_4371 (insert x s) f =
    2.66 +        (if x : s then iterate u_4371 s f
    2.67 +         else u_4371 (f x) (iterate u_4371 s f)))"
    2.68    by (import hollight ITERATE_CLAUSES_GEN)
    2.69  
    2.70  lemma ITERATE_CLAUSES: "monoidal (x::'q_60857 => 'q_60857 => 'q_60857)
    2.71 @@ -5270,11 +5267,11 @@
    2.72          (if xa : s then iterate x s f else x (f xa) (iterate x s f)))"
    2.73    by (import hollight ITERATE_CLAUSES)
    2.74  
    2.75 -lemma ITERATE_UNION: "[| monoidal (u_4372::'q_60945 => 'q_60945 => 'q_60945);
    2.76 +lemma ITERATE_UNION: "[| monoidal (u_4371::'q_60945 => 'q_60945 => 'q_60945);
    2.77     finite (s::'q_60930 => bool) &
    2.78     finite (x::'q_60930 => bool) & s Int x = {} |]
    2.79 -==> iterate u_4372 (s Un x) (f::'q_60930 => 'q_60945) =
    2.80 -    u_4372 (iterate u_4372 s f) (iterate u_4372 x f)"
    2.81 +==> iterate u_4371 (s Un x) (f::'q_60930 => 'q_60945) =
    2.82 +    u_4371 (iterate u_4371 s f) (iterate u_4371 x f)"
    2.83    by (import hollight ITERATE_UNION)
    2.84  
    2.85  lemma ITERATE_UNION_GEN: "[| monoidal (x::'B => 'B => 'B);
    2.86 @@ -5296,33 +5293,33 @@
    2.87  ==> x (iterate x (xb - xc) xa) (iterate x xc xa) = iterate x xb xa"
    2.88    by (import hollight ITERATE_DIFF_GEN)
    2.89  
    2.90 -lemma ITERATE_INCL_EXCL: "[| monoidal (u_4372::'q_61316 => 'q_61316 => 'q_61316);
    2.91 +lemma ITERATE_INCL_EXCL: "[| monoidal (u_4371::'q_61316 => 'q_61316 => 'q_61316);
    2.92     finite (s::'q_61298 => bool) & finite (t::'q_61298 => bool) |]
    2.93 -==> u_4372 (iterate u_4372 s (f::'q_61298 => 'q_61316))
    2.94 -     (iterate u_4372 t f) =
    2.95 -    u_4372 (iterate u_4372 (s Un t) f) (iterate u_4372 (s Int t) f)"
    2.96 +==> u_4371 (iterate u_4371 s (f::'q_61298 => 'q_61316))
    2.97 +     (iterate u_4371 t f) =
    2.98 +    u_4371 (iterate u_4371 (s Un t) f) (iterate u_4371 (s Int t) f)"
    2.99    by (import hollight ITERATE_INCL_EXCL)
   2.100  
   2.101 -lemma ITERATE_CLOSED: "[| monoidal (u_4372::'B => 'B => 'B);
   2.102 -   (P::'B => bool) (neutral u_4372) &
   2.103 -   (ALL (x::'B) y::'B. P x & P y --> P (u_4372 x y));
   2.104 +lemma ITERATE_CLOSED: "[| monoidal (u_4371::'B => 'B => 'B);
   2.105 +   (P::'B => bool) (neutral u_4371) &
   2.106 +   (ALL (x::'B) y::'B. P x & P y --> P (u_4371 x y));
   2.107     !!x::'A.
   2.108 -      x : (s::'A => bool) & (f::'A => 'B) x ~= neutral u_4372 ==> P (f x) |]
   2.109 -==> P (iterate u_4372 s f)"
   2.110 +      x : (s::'A => bool) & (f::'A => 'B) x ~= neutral u_4371 ==> P (f x) |]
   2.111 +==> P (iterate u_4371 s f)"
   2.112    by (import hollight ITERATE_CLOSED)
   2.113  
   2.114 -lemma ITERATE_RELATED: "[| monoidal (u_4372::'B => 'B => 'B);
   2.115 -   (R::'B => 'B => bool) (neutral u_4372) (neutral u_4372) &
   2.116 +lemma ITERATE_RELATED: "[| monoidal (u_4371::'B => 'B => 'B);
   2.117 +   (R::'B => 'B => bool) (neutral u_4371) (neutral u_4371) &
   2.118     (ALL (x1::'B) (y1::'B) (x2::'B) y2::'B.
   2.119 -       R x1 x2 & R y1 y2 --> R (u_4372 x1 y1) (u_4372 x2 y2));
   2.120 +       R x1 x2 & R y1 y2 --> R (u_4371 x1 y1) (u_4371 x2 y2));
   2.121     finite (x::'A => bool) &
   2.122     (ALL xa::'A. xa : x --> R ((f::'A => 'B) xa) ((g::'A => 'B) xa)) |]
   2.123 -==> R (iterate u_4372 x f) (iterate u_4372 x g)"
   2.124 +==> R (iterate u_4371 x f) (iterate u_4371 x g)"
   2.125    by (import hollight ITERATE_RELATED)
   2.126  
   2.127 -lemma ITERATE_EQ_NEUTRAL: "[| monoidal (u_4372::'B => 'B => 'B);
   2.128 -   !!x::'A. x : (s::'A => bool) ==> (f::'A => 'B) x = neutral u_4372 |]
   2.129 -==> iterate u_4372 s f = neutral u_4372"
   2.130 +lemma ITERATE_EQ_NEUTRAL: "[| monoidal (u_4371::'B => 'B => 'B);
   2.131 +   !!x::'A. x : (s::'A => bool) ==> (f::'A => 'B) x = neutral u_4371 |]
   2.132 +==> iterate u_4371 s f = neutral u_4371"
   2.133    by (import hollight ITERATE_EQ_NEUTRAL)
   2.134  
   2.135  lemma ITERATE_SING: "monoidal (x::'B => 'B => 'B) ==> iterate x {xa::'A} (f::'A => 'B) = f xa"
   2.136 @@ -5332,110 +5329,110 @@
   2.137  ==> u ((f::'A => 'B) a) (iterate u (s - {a}) f) = iterate u s f"
   2.138    by (import hollight ITERATE_DELETE)
   2.139  
   2.140 -lemma ITERATE_DELTA: "monoidal (u_4372::'q_61672 => 'q_61672 => 'q_61672)
   2.141 -==> iterate u_4372 (xb::'q_61691 => bool)
   2.142 +lemma ITERATE_DELTA: "monoidal (u_4371::'q_61672 => 'q_61672 => 'q_61672)
   2.143 +==> iterate u_4371 (xb::'q_61691 => bool)
   2.144       (%xb::'q_61691.
   2.145           if xb = (xa::'q_61691) then (x::'q_61691 => 'q_61672) xb
   2.146 -         else neutral u_4372) =
   2.147 -    (if xa : xb then x xa else neutral u_4372)"
   2.148 +         else neutral u_4371) =
   2.149 +    (if xa : xb then x xa else neutral u_4371)"
   2.150    by (import hollight ITERATE_DELTA)
   2.151  
   2.152 -lemma ITERATE_IMAGE: "[| monoidal (u_4372::'C => 'C => 'C);
   2.153 +lemma ITERATE_IMAGE: "[| monoidal (u_4371::'C => 'C => 'C);
   2.154     !!(x::'A) y::'A.
   2.155        x : (s::'A => bool) & y : s & (f::'A => 'B) x = f y ==> x = y |]
   2.156 -==> iterate u_4372 (f ` s) (g::'B => 'C) = iterate u_4372 s (g o f)"
   2.157 +==> iterate u_4371 (f ` s) (g::'B => 'C) = iterate u_4371 s (g o f)"
   2.158    by (import hollight ITERATE_IMAGE)
   2.159  
   2.160 -lemma ITERATE_BIJECTION: "[| monoidal (u_4372::'B => 'B => 'B);
   2.161 +lemma ITERATE_BIJECTION: "[| monoidal (u_4371::'B => 'B => 'B);
   2.162     (ALL x::'A. x : (s::'A => bool) --> (p::'A => 'A) x : s) &
   2.163     (ALL y::'A. y : s --> (EX! x::'A. x : s & p x = y)) |]
   2.164 -==> iterate u_4372 s (f::'A => 'B) = iterate u_4372 s (f o p)"
   2.165 +==> iterate u_4371 s (f::'A => 'B) = iterate u_4371 s (f o p)"
   2.166    by (import hollight ITERATE_BIJECTION)
   2.167  
   2.168 -lemma ITERATE_ITERATE_PRODUCT: "[| monoidal (u_4372::'C => 'C => 'C);
   2.169 +lemma ITERATE_ITERATE_PRODUCT: "[| monoidal (u_4371::'C => 'C => 'C);
   2.170     finite (x::'A => bool) &
   2.171     (ALL i::'A. i : x --> finite ((xa::'A => 'B => bool) i)) |]
   2.172 -==> iterate u_4372 x
   2.173 -     (%i::'A. iterate u_4372 (xa i) ((xb::'A => 'B => 'C) i)) =
   2.174 -    iterate u_4372
   2.175 +==> iterate u_4371 x
   2.176 +     (%i::'A. iterate u_4371 (xa i) ((xb::'A => 'B => 'C) i)) =
   2.177 +    iterate u_4371
   2.178       {u::'A * 'B. EX (i::'A) j::'B. (i : x & j : xa i) & u = (i, j)}
   2.179       (SOME f::'A * 'B => 'C. ALL (i::'A) j::'B. f (i, j) = xb i j)"
   2.180    by (import hollight ITERATE_ITERATE_PRODUCT)
   2.181  
   2.182 -lemma ITERATE_EQ: "[| monoidal (u_4372::'B => 'B => 'B);
   2.183 +lemma ITERATE_EQ: "[| monoidal (u_4371::'B => 'B => 'B);
   2.184     !!x::'A. x : (s::'A => bool) ==> (f::'A => 'B) x = (g::'A => 'B) x |]
   2.185 -==> iterate u_4372 s f = iterate u_4372 s g"
   2.186 +==> iterate u_4371 s f = iterate u_4371 s g"
   2.187    by (import hollight ITERATE_EQ)
   2.188  
   2.189 -lemma ITERATE_EQ_GENERAL: "[| monoidal (u_4372::'C => 'C => 'C);
   2.190 +lemma ITERATE_EQ_GENERAL: "[| monoidal (u_4371::'C => 'C => 'C);
   2.191     (ALL y::'B.
   2.192         y : (t::'B => bool) -->
   2.193         (EX! x::'A. x : (s::'A => bool) & (h::'A => 'B) x = y)) &
   2.194     (ALL x::'A. x : s --> h x : t & (g::'B => 'C) (h x) = (f::'A => 'C) x) |]
   2.195 -==> iterate u_4372 s f = iterate u_4372 t g"
   2.196 +==> iterate u_4371 s f = iterate u_4371 t g"
   2.197    by (import hollight ITERATE_EQ_GENERAL)
   2.198  
   2.199 -lemma ITERATE_EQ_GENERAL_INVERSES: "[| monoidal (u_4372::'C => 'C => 'C);
   2.200 +lemma ITERATE_EQ_GENERAL_INVERSES: "[| monoidal (u_4371::'C => 'C => 'C);
   2.201     (ALL y::'B.
   2.202         y : (t::'B => bool) -->
   2.203         (k::'B => 'A) y : (s::'A => bool) & (h::'A => 'B) (k y) = y) &
   2.204     (ALL x::'A.
   2.205         x : s -->
   2.206         h x : t & k (h x) = x & (g::'B => 'C) (h x) = (f::'A => 'C) x) |]
   2.207 -==> iterate u_4372 s f = iterate u_4372 t g"
   2.208 +==> iterate u_4371 s f = iterate u_4371 t g"
   2.209    by (import hollight ITERATE_EQ_GENERAL_INVERSES)
   2.210  
   2.211 -lemma ITERATE_INJECTION: "[| monoidal (u_4372::'B => 'B => 'B);
   2.212 +lemma ITERATE_INJECTION: "[| monoidal (u_4371::'B => 'B => 'B);
   2.213     finite (s::'A => bool) &
   2.214     (ALL x::'A. x : s --> (p::'A => 'A) x : s) &
   2.215     (ALL (x::'A) y::'A. x : s & y : s & p x = p y --> x = y) |]
   2.216 -==> iterate u_4372 s ((f::'A => 'B) o p) = iterate u_4372 s f"
   2.217 +==> iterate u_4371 s ((f::'A => 'B) o p) = iterate u_4371 s f"
   2.218    by (import hollight ITERATE_INJECTION)
   2.219  
   2.220 -lemma ITERATE_UNION_NONZERO: "[| monoidal (u_4372::'B => 'B => 'B);
   2.221 +lemma ITERATE_UNION_NONZERO: "[| monoidal (u_4371::'B => 'B => 'B);
   2.222     finite (s::'A => bool) &
   2.223     finite (t::'A => bool) &
   2.224 -   (ALL x::'A. x : s Int t --> (f::'A => 'B) x = neutral u_4372) |]
   2.225 -==> iterate u_4372 (s Un t) f =
   2.226 -    u_4372 (iterate u_4372 s f) (iterate u_4372 t f)"
   2.227 +   (ALL x::'A. x : s Int t --> (f::'A => 'B) x = neutral u_4371) |]
   2.228 +==> iterate u_4371 (s Un t) f =
   2.229 +    u_4371 (iterate u_4371 s f) (iterate u_4371 t f)"
   2.230    by (import hollight ITERATE_UNION_NONZERO)
   2.231  
   2.232 -lemma ITERATE_OP: "[| monoidal (u_4372::'q_62649 => 'q_62649 => 'q_62649);
   2.233 +lemma ITERATE_OP: "[| monoidal (u_4371::'q_62649 => 'q_62649 => 'q_62649);
   2.234     finite (s::'q_62648 => bool) |]
   2.235 -==> iterate u_4372 s
   2.236 +==> iterate u_4371 s
   2.237       (%x::'q_62648.
   2.238 -         u_4372 ((f::'q_62648 => 'q_62649) x)
   2.239 +         u_4371 ((f::'q_62648 => 'q_62649) x)
   2.240            ((g::'q_62648 => 'q_62649) x)) =
   2.241 -    u_4372 (iterate u_4372 s f) (iterate u_4372 s g)"
   2.242 +    u_4371 (iterate u_4371 s f) (iterate u_4371 s g)"
   2.243    by (import hollight ITERATE_OP)
   2.244  
   2.245 -lemma ITERATE_SUPERSET: "[| monoidal (u_4372::'B => 'B => 'B);
   2.246 +lemma ITERATE_SUPERSET: "[| monoidal (u_4371::'B => 'B => 'B);
   2.247     (u::'A => bool) <= (v::'A => bool) &
   2.248 -   (ALL x::'A. x : v & x ~: u --> (f::'A => 'B) x = neutral u_4372) |]
   2.249 -==> iterate u_4372 v f = iterate u_4372 u f"
   2.250 +   (ALL x::'A. x : v & x ~: u --> (f::'A => 'B) x = neutral u_4371) |]
   2.251 +==> iterate u_4371 v f = iterate u_4371 u f"
   2.252    by (import hollight ITERATE_SUPERSET)
   2.253  
   2.254 -lemma ITERATE_IMAGE_NONZERO: "[| monoidal (u_4372::'C => 'C => 'C);
   2.255 +lemma ITERATE_IMAGE_NONZERO: "[| monoidal (u_4371::'C => 'C => 'C);
   2.256     finite (x::'A => bool) &
   2.257     (ALL (xa::'A) y::'A.
   2.258         xa : x & y : x & xa ~= y & (f::'A => 'B) xa = f y -->
   2.259 -       (g::'B => 'C) (f xa) = neutral u_4372) |]
   2.260 -==> iterate u_4372 (f ` x) g = iterate u_4372 x (g o f)"
   2.261 +       (g::'B => 'C) (f xa) = neutral u_4371) |]
   2.262 +==> iterate u_4371 (f ` x) g = iterate u_4371 x (g o f)"
   2.263    by (import hollight ITERATE_IMAGE_NONZERO)
   2.264  
   2.265 -lemma ITERATE_CASES: "[| monoidal (u_4372::'B => 'B => 'B); finite (s::'A => bool) |]
   2.266 -==> iterate u_4372 s
   2.267 +lemma ITERATE_CASES: "[| monoidal (u_4371::'B => 'B => 'B); finite (s::'A => bool) |]
   2.268 +==> iterate u_4371 s
   2.269       (%x::'A.
   2.270           if (P::'A => bool) x then (f::'A => 'B) x else (g::'A => 'B) x) =
   2.271 -    u_4372 (iterate u_4372 {u::'A. EX x::'A. (x : s & P x) & u = x} f)
   2.272 -     (iterate u_4372 {u::'A. EX x::'A. (x : s & ~ P x) & u = x} g)"
   2.273 +    u_4371 (iterate u_4371 {u::'A. EX x::'A. (x : s & P x) & u = x} f)
   2.274 +     (iterate u_4371 {u::'A. EX x::'A. (x : s & ~ P x) & u = x} g)"
   2.275    by (import hollight ITERATE_CASES)
   2.276  
   2.277 -lemma ITERATE_OP_GEN: "[| monoidal (u_4372::'B => 'B => 'B);
   2.278 -   finite (support u_4372 (f::'A => 'B) (s::'A => bool)) &
   2.279 -   finite (support u_4372 (g::'A => 'B) s) |]
   2.280 -==> iterate u_4372 s (%x::'A. u_4372 (f x) (g x)) =
   2.281 -    u_4372 (iterate u_4372 s f) (iterate u_4372 s g)"
   2.282 +lemma ITERATE_OP_GEN: "[| monoidal (u_4371::'B => 'B => 'B);
   2.283 +   finite (support u_4371 (f::'A => 'B) (s::'A => bool)) &
   2.284 +   finite (support u_4371 (g::'A => 'B) s) |]
   2.285 +==> iterate u_4371 s (%x::'A. u_4371 (f x) (g x)) =
   2.286 +    u_4371 (iterate u_4371 s f) (iterate u_4371 s g)"
   2.287    by (import hollight ITERATE_OP_GEN)
   2.288  
   2.289  lemma ITERATE_CLAUSES_NUMSEG: "monoidal (x::'q_63246 => 'q_63246 => 'q_63246)
   2.290 @@ -5448,11 +5445,11 @@
   2.291           else iterate x {xa..xb} f))"
   2.292    by (import hollight ITERATE_CLAUSES_NUMSEG)
   2.293  
   2.294 -lemma ITERATE_PAIR: "monoidal (u_4372::'q_63421 => 'q_63421 => 'q_63421)
   2.295 -==> iterate u_4372 {(2::nat) * (m::nat)..(2::nat) * (n::nat) + (1::nat)}
   2.296 +lemma ITERATE_PAIR: "monoidal (u_4371::'q_63421 => 'q_63421 => 'q_63421)
   2.297 +==> iterate u_4371 {(2::nat) * (m::nat)..(2::nat) * (n::nat) + (1::nat)}
   2.298       (f::nat => 'q_63421) =
   2.299 -    iterate u_4372 {m..n}
   2.300 -     (%i::nat. u_4372 (f ((2::nat) * i)) (f ((2::nat) * i + (1::nat))))"
   2.301 +    iterate u_4371 {m..n}
   2.302 +     (%i::nat. u_4371 (f ((2::nat) * i)) (f ((2::nat) * i + (1::nat))))"
   2.303    by (import hollight ITERATE_PAIR)
   2.304  
   2.305  definition
     3.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Fri Jul 15 16:51:01 2011 +0200
     3.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Sat Jul 16 00:01:17 2011 +0200
     3.3 @@ -572,7 +572,7 @@
     3.4    "WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
     3.5    "UNWIND_THM2" > "HOL.simp_thms_39"
     3.6    "UNWIND_THM1" > "HOL.simp_thms_40"
     3.7 -  "UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
     3.8 +  "UNIV_SUBSET" > "Orderings.top_class.top_unique"
     3.9    "UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
    3.10    "UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
    3.11    "UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
    3.12 @@ -791,7 +791,7 @@
    3.13    "SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
    3.14    "SUBSET_INSERT" > "Set.subset_insert"
    3.15    "SUBSET_IMAGE" > "Set.subset_image_iff"
    3.16 -  "SUBSET_EMPTY" > "Set.subset_empty"
    3.17 +  "SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
    3.18    "SUBSET_DIFF" > "Set.Diff_subset"
    3.19    "SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
    3.20    "SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
    3.21 @@ -1547,6 +1547,7 @@
    3.22    "IN_UNION" > "Complete_Lattice.mem_simps_3"
    3.23    "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
    3.24    "IN_SING" > "Set.singleton_iff"
    3.25 +  "IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
    3.26    "IN_REST" > "HOLLight.hollight.IN_REST"
    3.27    "IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
    3.28    "IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
    3.29 @@ -2278,6 +2279,7 @@
    3.30    "$_def" > "HOLLight.hollight.$_def"
    3.31  
    3.32  ignore_thms
    3.33 +  "WF_REC_CASES"
    3.34    "TYDEF_sum"
    3.35    "TYDEF_prod"
    3.36    "TYDEF_option"
    3.37 @@ -2287,12 +2289,15 @@
    3.38    "SNDCART_PASTECART"
    3.39    "SET_OF_LIST_OF_SET"
    3.40    "REP_ABS_PAIR"
    3.41 +  "RECURSION_CASEWISE_PAIRWISE"
    3.42 +  "RECURSION_CASEWISE"
    3.43    "PASTECART_FST_SND"
    3.44    "PASTECART_EQ"
    3.45    "MEM_LIST_OF_SET"
    3.46    "MEM_ASSOC"
    3.47    "LIST_OF_SET_PROPERTIES"
    3.48    "LENGTH_LIST_OF_SET"
    3.49 +  "HAS_SIZE_SET_OF_LIST"
    3.50    "FSTCART_PASTECART"
    3.51    "FORALL_PASTECART"
    3.52    "FINITE_SET_OF_LIST"
    3.53 @@ -2321,6 +2326,10 @@
    3.54    "DEF_CONS"
    3.55    "DEF_ASSOC"
    3.56    "DEF_,"
    3.57 +  "CASEWISE_WORKS"
    3.58 +  "CASEWISE_CASES"
    3.59 +  "CASEWISE"
    3.60 +  "CARD_SET_OF_LIST_LE"
    3.61    "ALL_MAP"
    3.62  
    3.63  end
     4.1 --- a/src/HOL/Import/HOLLightList.thy	Fri Jul 15 16:51:01 2011 +0200
     4.2 +++ b/src/HOL/Import/HOLLightList.thy	Sat Jul 16 00:01:17 2011 +0200
     4.3 @@ -8,6 +8,10 @@
     4.4  imports List
     4.5  begin
     4.6  
     4.7 +lemma FINITE_SET_OF_LIST:
     4.8 +  "finite (set l)"
     4.9 +  by simp
    4.10 +
    4.11  lemma AND_ALL2:
    4.12    "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m"
    4.13    by (induct l m rule: list_induct2') auto
    4.14 @@ -298,8 +302,8 @@
    4.15    done
    4.16  
    4.17  lemma IN_SET_OF_LIST:
    4.18 -  "ALL x l. (x\<in>set l) = list_mem x l"
    4.19 -  by (simp add: member_def)
    4.20 +  "(x : set l) = (x : set l)"
    4.21 +  by simp
    4.22  
    4.23  lemma DEF_BUTLAST:
    4.24    "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"