another try to improve code generation of set equality (cf. da32cf32c0c7)
authorbulwahn
Sun Feb 05 08:24:39 2012 +0100 (2012-02-05)
changeset 4641822bb415d7754
parent 46417 1a68fcb80b62
child 46419 e139d0e29ca1
another try to improve code generation of set equality (cf. da32cf32c0c7)
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sun Feb 05 08:24:38 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Feb 05 08:24:39 2012 +0100
     1.3 @@ -5677,9 +5677,12 @@
     1.4  text {* Further operations on sets *}
     1.5  
     1.6  (* Minimal refinement of equality on sets *)
     1.7 -lemma [code]:
     1.8 -  "HOL.equal (set []) (List.coset []) = False"
     1.9 -by (metis UNIV_coset UNIV_not_empty empty_set equal_eq)
    1.10 +declare subset_eq[code del]
    1.11 +lemma subset_code [code]:
    1.12 +  "set xs <= B \<longleftrightarrow> (ALL x : set xs. x : B)"
    1.13 +  "List.coset xs <= List.coset ys \<longleftrightarrow> set ys <= set xs"
    1.14 +  "List.coset [] <= set [] \<longleftrightarrow> False"
    1.15 +by auto
    1.16  
    1.17  lemma setsum_code [code]:
    1.18    "setsum f (set xs) = listsum (map f (remdups xs))"