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"

     2.1 --- a/src/HOL/Library/RBT_Set.thy	Fri Sep 20 00:08:42 2013 +0200
     2.2 +++ b/src/HOL/Library/RBT_Set.thy	Fri Sep 20 10:09:16 2013 +0200
     2.3 @@ -628,20 +628,16 @@
     2.4    "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
     2.5  by auto
     2.6  
     2.7 -definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2"
     2.8 -
     2.9 -code_abort non_empty_trees
    2.10 -
    2.11  lemma subset_Coset_empty_Set_empty [code]:
    2.12    "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
    2.13      (rbt.Empty, rbt.Empty) => False |
    2.14 -    (_, _) => non_empty_trees t1 t2)"
    2.15 +    (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
    2.16  proof -
    2.17    have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
    2.18      by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
    2.19    have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
    2.20    show ?thesis  
    2.21 -    by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def)
    2.22 +    by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
    2.23  qed
    2.24  
    2.25  text {* A frequent case – avoid intermediate sets *}
    2.26 @@ -661,15 +657,11 @@
    2.27      by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
    2.28  qed
    2.29  
    2.30 -definition not_a_singleton_tree  where [code del]: "not_a_singleton_tree x y = x y"
    2.31 -
    2.32 -code_abort not_a_singleton_tree
    2.33 -
    2.34  lemma the_elem_set [code]:
    2.35    fixes t :: "('a :: linorder, unit) rbt"
    2.36    shows "the_elem (Set t) = (case impl_of t of 
    2.37      (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
    2.38 -    | _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))"
    2.39 +    | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
    2.40  proof -
    2.41    {
    2.42      fix x :: "'a :: linorder"
    2.43 @@ -681,7 +673,7 @@
    2.44        by (subst(asm) RBT_inverse[symmetric, OF *])
    2.45          (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
    2.46    }
    2.47 -  then show ?thesis unfolding not_a_singleton_tree_def
    2.48 +  then show ?thesis
    2.49      by(auto split: rbt.split unit.split color.split)
    2.50  qed
    2.51  
    2.52 @@ -729,17 +721,16 @@
    2.53    "wf (Set t) = acyclic (Set t)"
    2.54  by (simp add: wf_iff_acyclic_if_finite)
    2.55  
    2.56 -definition not_non_empty_tree  where [code del]: "not_non_empty_tree x y = x y"
    2.57 -
    2.58 -code_abort not_non_empty_tree
    2.59 -
    2.60  lemma Min_fin_set_fold [code]:
    2.61 -  "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)"
    2.62 +  "Min (Set t) = 
    2.63 +  (if is_empty t
    2.64 +   then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
    2.65 +   else r_min_opt t)"
    2.66  proof -
    2.67    have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
    2.68    with finite_fold1_fold1_keys [OF *, folded Min_def]
    2.69    show ?thesis
    2.70 -    by (simp add: not_non_empty_tree_def r_min_alt_def r_min_eq_r_min_opt [symmetric])  
    2.71 +    by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric])  
    2.72  qed
    2.73  
    2.74  lemma Inf_fin_set_fold [code]:
    2.75 @@ -771,12 +762,15 @@
    2.76  qed
    2.77  
    2.78  lemma Max_fin_set_fold [code]:
    2.79 -  "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)"
    2.80 +  "Max (Set t) = 
    2.81 +  (if is_empty t
    2.82 +   then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
    2.83 +   else r_max_opt t)"
    2.84  proof -
    2.85    have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
    2.86    with finite_fold1_fold1_keys [OF *, folded Max_def]
    2.87    show ?thesis
    2.88 -    by (simp add: not_non_empty_tree_def r_max_alt_def r_max_eq_r_max_opt [symmetric])  
    2.89 +    by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric])  
    2.90  qed
    2.91  
    2.92  lemma Sup_fin_set_fold [code]: