src/HOL/Library/Cardinality.thy
changeset 53745 788730ab7da4
parent 53191 14ab2f821e1d
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Cardinality.thy	Fri Sep 20 00:08:42 2013 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Sep 20 10:09:16 2013 +0200
     1.3 @@ -499,23 +499,18 @@
     1.4    Constrain the element type with sort @{class card_UNIV} to change this.
     1.5  *}
     1.6  
     1.7 -definition card_coset_requires_card_UNIV :: "'a list \<Rightarrow> nat"
     1.8 -where [code del, simp]: "card_coset_requires_card_UNIV xs = card (List.coset xs)"
     1.9 -
    1.10 -code_abort card_coset_requires_card_UNIV
    1.11 -
    1.12  lemma card_coset_error [code]:
    1.13 -  "card (List.coset xs) = card_coset_requires_card_UNIV xs"
    1.14 +  "card (List.coset xs) = 
    1.15 +   Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
    1.16 +     (\<lambda>_. card (List.coset xs))"
    1.17  by(simp)
    1.18  
    1.19 -definition coset_subseteq_set_requires_card_UNIV :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.20 -where [code del, simp]: "coset_subseteq_set_requires_card_UNIV xs ys \<longleftrightarrow> List.coset xs \<subseteq> set ys"
    1.21 -
    1.22 -code_abort coset_subseteq_set_requires_card_UNIV
    1.23 -
    1.24  lemma coset_subseteq_set_code [code]:
    1.25    "List.coset xs \<subseteq> set ys \<longleftrightarrow> 
    1.26 -  (if xs = [] \<and> ys = [] then False else coset_subseteq_set_requires_card_UNIV xs ys)"
    1.27 +  (if xs = [] \<and> ys = [] then False 
    1.28 +   else Code.abort
    1.29 +     (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
    1.30 +     (\<lambda>_. List.coset xs \<subseteq> set ys))"
    1.31  by simp
    1.32  
    1.33  notepad begin -- "test code setup"