diff -r 05f98e2ee48b -r 98e84b56543f Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Oct 15 15:56:16 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 15:58:48 2010 +0100
@@ -44,9 +44,9 @@
   "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
 
 definition
-  fcard_raw :: "'a list \<Rightarrow> nat"
+  card_list :: "'a list \<Rightarrow> nat"
 where
-  "fcard_raw xs = card (set xs)"
+  "card_list xs = card (set xs)"
 
 primrec
   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
@@ -212,9 +212,9 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
   by simp
 
-lemma fcard_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
-  by (simp add: fcard_raw_def)
+lemma card_list_rsp[quot_respect]:
+  shows "(op \<approx> ===> op =) card_list card_list"
+  by (simp add: card_list_def)
 
 
 
@@ -427,7 +427,7 @@
 
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat"
-  is fcard_raw
+  is card_list
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
@@ -622,29 +622,29 @@
 next
   {
     fix n
-    assume a: "fcard_raw l = n" and b: "l \<approx> r"
+    assume a: "card_list l = n" and b: "l \<approx> r"
     have "list_eq2 l r"
       using a b
     proof (induct n arbitrary: l r)
       case 0
-      have "fcard_raw l = 0" by fact
-      then have "\<forall>x. \<not> memb x l" unfolding fcard_raw_def memb_def by auto
+      have "card_list l = 0" by fact
+      then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto
       then have z: "l = []" unfolding memb_def by auto
       then have "r = []" using `l \<approx> r` by simp
       then show ?case using z list_eq2_refl by simp
     next
       case (Suc m)
       have b: "l \<approx> r" by fact
-      have d: "fcard_raw l = Suc m" by fact
+      have d: "card_list l = Suc m" by fact
       then have "\<exists>a. memb a l" 
-	apply(simp add: fcard_raw_def memb_def)
+	apply(simp add: card_list_def memb_def)
 	apply(drule card_eq_SucD)
 	apply(blast)
 	done
       then obtain a where e: "memb a l" by auto
       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
 	unfolding memb_def by auto
-      have f: "fcard_raw (removeAll a l) = m" using e d by (simp add: fcard_raw_def memb_def)
+      have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
       have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
@@ -909,15 +909,15 @@
 
 lemma fcard_set: 
   shows "fcard xs = card (fset xs)"
-  by (lifting fcard_raw_def)
+  by (lifting card_list_def)
 
 lemma fcard_finsert_if [simp]:
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
-  by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
+  by (descending) (auto simp add: card_list_def memb_def insert_absorb)
 
 lemma fcard_0[simp]:
   shows "fcard S = 0 \<longleftrightarrow> S = {||}"
-  by (descending) (simp add: fcard_raw_def)
+  by (descending) (simp add: card_list_def)
 
 lemma fcard_fempty[simp]:
   shows "fcard {||} = 0"
@@ -925,20 +925,20 @@
 
 lemma fcard_1:
   shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
-  by (descending) (auto simp add: fcard_raw_def card_Suc_eq)
+  by (descending) (auto simp add: card_list_def card_Suc_eq)
 
 lemma fcard_gt_0:
   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
-  by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
+  by (descending) (auto simp add: card_list_def card_gt_0_iff)
   
 lemma fcard_not_fin:
   shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
-  by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
+  by (descending) (auto simp add: memb_def card_list_def insert_absorb)
 
 lemma fcard_suc: 
   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
   apply(descending)
-  apply(auto simp add: fcard_raw_def memb_def)
+  apply(auto simp add: card_list_def memb_def)
   apply(drule card_eq_SucD)
   apply(auto)
   apply(rule_tac x="b" in exI)
@@ -948,19 +948,19 @@
 
 lemma fcard_delete:
   shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
-  by (descending) (simp add: fcard_raw_def memb_def)
+  by (descending) (simp add: card_list_def memb_def)
 
 lemma fcard_suc_memb: 
   shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
   apply(descending)
-  apply(simp add: fcard_raw_def memb_def)
+  apply(simp add: card_list_def memb_def)
   apply(drule card_eq_SucD)
   apply(auto)
   done
 
 lemma fin_fcard_not_0: 
   shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
-  by (descending) (auto simp add: fcard_raw_def memb_def)
+  by (descending) (auto simp add: card_list_def memb_def)
 
 lemma fcard_mono: 
   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"