# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277827439 -3600
# Node ID 2116425cebc86ac80d37f114c1a95f38b18b6fed
# Parent  ff1137a9c0561b8375a98a4f5aed741b09970ee0
cleaned by using descending instead of lifting

diff -r ff1137a9c056 -r 2116425cebc8 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Jun 29 11:38:51 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Jun 29 17:03:59 2010 +0100
@@ -379,50 +379,6 @@
 
 text {* Distributive lattice with bot *}
 
-lemma sub_list_not_eq:
-  "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
-  by (auto simp add: sub_list_def)
-
-lemma sub_list_refl:
-  "sub_list x x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_trans:
-  "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"
-  by (simp add: sub_list_def)
-
-lemma sub_list_empty:
-  "sub_list [] x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_left:
-  "sub_list x (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_right:
-  "sub_list y (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_inter_left:
-  shows "sub_list (finter_raw x y) x"
-  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
-
-lemma sub_list_inter_right:
-  shows "sub_list (finter_raw x y) y"
-  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
-
-lemma sub_list_list_eq:
-  "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
-  unfolding sub_list_def list_eq.simps by blast
-
-lemma sub_list_append:
-  "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
-  unfolding sub_list_def by auto
-
-lemma sub_list_inter:
-  "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
-  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
-
 lemma append_inter_distrib:
   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
   apply (induct x)
@@ -431,7 +387,7 @@
   apply (auto simp add: memb_def)
   done
 
-instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
+instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
 
 quotient_definition
@@ -482,42 +438,50 @@
   "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
 
 quotient_definition
-  "minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
-  "fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+  "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
 instance
 proof
   fix x y z :: "'a fset"
-  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
-    unfolding less_fset by (lifting sub_list_not_eq)
-  show "x |\<subseteq>| x" by (lifting sub_list_refl)
-  show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
-  show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
-  show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
-  show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
-  show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
-  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
+    unfolding less_fset 
+    by (descending) (auto simp add: sub_list_def)
+  show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
+  show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
+  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+  show "x |\<inter>| y |\<subseteq>| x" 
+    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+  show "x |\<inter>| y |\<subseteq>| y" 
+    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
+    by (descending) (rule append_inter_distrib)
 next
   fix x y z :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "y |\<subseteq>| z"
-  show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
+  show "x |\<subseteq>| z" using a b 
+    by (descending) (simp add: sub_list_def)
 next
   fix x y :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "y |\<subseteq>| x"
-  show "x = y" using a b by (lifting sub_list_list_eq)
+  show "x = y" using a b 
+    by (descending) (unfold sub_list_def list_eq.simps, blast)
 next
   fix x y z :: "'a fset"
   assume a: "y |\<subseteq>| x"
   assume b: "z |\<subseteq>| x"
-  show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
+  show "y |\<union>| z |\<subseteq>| x" using a b 
+    by (descending) (simp add: sub_list_def)
 next
   fix x y z :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "x |\<subseteq>| z"
-  show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
+  show "x |\<subseteq>| y |\<inter>| z" using a b 
+    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 qed
 
 end
@@ -750,14 +714,6 @@
   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
-lemma cons_left_comm:
-  "x # y # xs \<approx> y # x # xs"
-  by auto
-
-lemma cons_left_idem:
-  "x # x # xs \<approx> x # xs"
-  by auto
-
 lemma fset_raw_strong_cases:
   obtains "xs = []"
     | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
@@ -809,10 +765,6 @@
   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
-lemma finter_raw_empty:
-  "finter_raw l [] = []"
-  by (induct l) (simp_all add: not_memb_nil)
-
 lemma set_cong:
   shows "(x \<approx> y) = (set x = set y)"
   by auto
@@ -903,7 +855,7 @@
 text {* Set *}
 
 lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
-  by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+  unfolding sub_list_def by auto
 
 lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
   by (auto simp add: sub_list_set)
@@ -939,20 +891,20 @@
 text {* Lifted theorems *}
 
 lemma not_fin_fnil: "x |\<notin>| {||}"
-  by (lifting not_memb_nil)
+  by (descending) (simp add: memb_def)
 
 lemma fin_finsert_iff[simp]:
-  "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
-  by (lifting memb_cons_iff)
+  "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
+  by (descending) (simp add: memb_def)
 
 lemma
   shows finsertI1: "x |\<in>| finsert x S"
   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
-  by (lifting memb_consI1, lifting memb_consI2)
+  by (lifting memb_consI1 memb_consI2)
 
 lemma finsert_absorb[simp]:
   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
-  by (lifting memb_absorb)
+  by (descending) (auto simp add: memb_def)
 
 lemma fempty_not_finsert[simp]:
   "{||} \<noteq> finsert x S"
@@ -961,21 +913,23 @@
 
 lemma finsert_left_comm:
   "finsert x (finsert y S) = finsert y (finsert x S)"
-  by (lifting cons_left_comm)
+  by (descending) (auto)
 
 lemma finsert_left_idem:
   "finsert x (finsert x S) = finsert x S"
-  by (lifting cons_left_idem)
+  by (descending) (auto)
 
 lemma fsingleton_eq[simp]:
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
-  by (lifting singleton_list_eq)
+  by (descending) (auto)
+
 
 text {* fset_to_set *}
 
-lemma fset_to_set_simps[simp]:
-  "fset_to_set {||} = ({} :: 'a set)"
-  "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
+lemma fset_to_set_simps [simp]:
+  fixes h::"'a"
+  shows "fset_to_set {||} = ({} :: 'a set)"
+  and "fset_to_set (finsert h t) = insert h (fset_to_set t)"
   by (lifting set.simps)
 
 lemma in_fset_to_set:
@@ -983,28 +937,29 @@
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
-  "(\<forall>x. x |\<notin>| S) = (S = {||})"
+  "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
   by (lifting none_memb_nil)
 
 lemma fset_cong:
-  "(S = T) = (fset_to_set S = fset_to_set T)"
+  "S = T \<longleftrightarrow> fset_to_set S = fset_to_set T"
   by (lifting set_cong)
 
 text {* fcard *}
 
 lemma fcard_fempty [simp]:
   shows "fcard {||} = 0"
-  by (lifting fcard_raw_nil)
+  by (descending) (simp)
 
 lemma fcard_finsert_if [simp]:
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
-  by (lifting fcard_raw_cons)
+  by (descending) (simp)
 
-lemma fcard_0: "(fcard S = 0) = (S = {||})"
+lemma fcard_0: 
+  "fcard S = 0 \<longleftrightarrow> S = {||}"
   by (lifting fcard_raw_0)
 
 lemma fcard_1:
-  shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
+  shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
   by (lifting fcard_raw_1)
 
 lemma fcard_gt_0:
@@ -1039,11 +994,11 @@
   by (lifting append.simps(2))
 
 lemma singleton_union_left:
-  "{|a|} |\<union>| S = finsert a S"
+  shows "{|a|} |\<union>| S = finsert a S"
   by simp
 
 lemma singleton_union_right:
-  "S |\<union>| {|a|} = finsert a S"
+  shows "S |\<union>| {|a|} = finsert a S"
   by (subst sup.commute) simp
 
 section {* Induction and Cases rules for finite sets *}
@@ -1105,8 +1060,9 @@
 text {* fmap *}
 
 lemma fmap_simps[simp]:
-  "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
-  "fmap f (finsert x S) = finsert (f x) (fmap f S)"
+  fixes f::"'a \<Rightarrow> 'b"
+  shows "fmap f {||} = {||}"
+  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
   by (lifting map.simps)
 
 lemma fmap_set_image:
@@ -1114,51 +1070,62 @@
   by (induct S) simp_all
 
 lemma inj_fmap_eq_iff:
-  "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
+  "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
   by (lifting inj_map_eq_iff)
 
-lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
+lemma fmap_funion: 
+  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
   by (lifting map_append)
 
 lemma fin_funion:
-  "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
+  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   by (lifting memb_append)
 
 text {* to_set *}
 
-lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+lemma fin_set: 
+  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset_to_set xs"
   by (lifting memb_set)
 
-lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+lemma fnotin_set: 
+  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset_to_set xs"
   by (simp add: fin_set)
 
-lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+lemma fcard_set: 
+  shows "fcard xs = card (fset_to_set xs)"
   by (lifting fcard_raw_set)
 
-lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+lemma fsubseteq_set: 
+  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset_to_set xs \<subseteq> fset_to_set ys"
   by (lifting sub_list_set)
 
-lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+lemma fsubset_set: 
+  shows "xs |\<subset>| ys \<longleftrightarrow> fset_to_set xs \<subset> fset_to_set ys"
   unfolding less_fset by (lifting sub_list_neq_set)
 
-lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+lemma ffilter_set: 
+  shows "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
   by (lifting filter_set)
 
-lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+lemma fdelete_set: 
+  shows "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
   by (lifting delete_raw_set)
 
-lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+lemma finter_set: 
+  shows "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
   by (lifting inter_raw_set)
 
-lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+lemma funion_set: 
+  shows "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
   by (lifting set_append)
 
-lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+lemma fminus_set: 
+  shows "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
   by (lifting fminus_raw_set)
 
 lemmas fset_to_set_trans =
   fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
-  inter_set union_set ffilter_set fset_to_set_simps
+  finter_set funion_set ffilter_set fset_to_set_simps
   fset_cong fdelete_set fmap_set_image fminus_set
 
 
@@ -1193,13 +1160,16 @@
   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
   by (lifting fset_raw_delete_raw_cases)
 
-text {* inter *}
+text {* finite intersection *}
 
-lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
-  by (lifting finter_raw.simps(1))
+lemma finter_empty_l: 
+  shows "{||} |\<inter>| S = {||}"
+  by simp
 
-lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
-  by (lifting finter_raw_empty)
+
+lemma finter_empty_r: 
+  shows "S |\<inter>| {||} = {||}"
+  by simp
 
 lemma finter_finsert:
   "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
@@ -1210,30 +1180,36 @@
   by (lifting memb_finter_raw)
 
 lemma fsubset_finsert:
-  "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
+  shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
   by (lifting sub_list_cons)
 
-lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+lemma 
+  shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
   by (lifting sub_list_def[simplified memb_def[symmetric]])
 
-lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+lemma fsubset_fin: 
+  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
 by (rule meta_eq_to_obj_eq)
    (lifting sub_list_def[simplified memb_def[symmetric]])
 
-lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+lemma fminus_fin: 
+  shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
   by (lifting fminus_raw_memb)
 
-lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+lemma fminus_red: 
+  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
   by (lifting fminus_raw_red)
 
-lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+lemma fminus_red_fin [simp]: 
+  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
   by (simp add: fminus_red)
 
-lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+lemma fminus_red_fnotin[simp]: 
+  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
   by (simp add: fminus_red)
 
 lemma expand_fset_eq:
-  "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
+  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])
 
 (* We cannot write it as "assumes .. shows" since Isabelle changes
@@ -1261,7 +1237,7 @@
   using assms
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
-text {* concat *}
+section {* fconcat *}
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
@@ -1271,19 +1247,24 @@
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
   by (lifting concat.simps(2))
 
-lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+lemma 
+  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
   by (lifting concat_append)
 
-text {* ffilter *}
+
+section {* ffilter *}
 
-lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
-by (lifting sub_list_filter)
+lemma subseteq_filter: 
+  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+  by (lifting sub_list_filter)
 
-lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
-by (lifting list_eq_filter)
+lemma eq_ffilter: 
+  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+  by (lifting list_eq_filter)
 
-lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
-unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+lemma subset_ffilter: 
+  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+  unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
 
 section {* lemmas transferred from Finite_Set theory *}
 
@@ -1291,67 +1272,82 @@
 lemma finite_fset: "finite (fset_to_set S)"
   by (induct S) auto
 
-lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+lemma fset_choice: 
+  shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
   unfolding fset_to_set_trans
   by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
 
-lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+lemma fsubseteq_fnil: 
+  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
   unfolding fset_to_set_trans
   by (rule subset_empty)
 
-lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+lemma not_fsubset_fnil: 
+  shows "\<not> xs |\<subset>| {||}"
   unfolding fset_to_set_trans
   by (rule not_psubset_empty)
 
-lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+lemma fcard_mono: 
+  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
   unfolding fset_to_set_trans
   by (rule card_mono[OF finite_fset])
 
-lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+lemma fcard_fseteq: 
+  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
   unfolding fset_to_set_trans
   by (rule card_seteq[OF finite_fset])
 
-lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+lemma psubset_fcard_mono: 
+  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
   unfolding fset_to_set_trans
   by (rule psubset_card_mono[OF finite_fset])
 
-lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+lemma fcard_funion_finter: 
+  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
   unfolding fset_to_set_trans
   by (rule card_Un_Int[OF finite_fset finite_fset])
 
-lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+lemma fcard_funion_disjoint: 
+  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
   unfolding fset_to_set_trans
   by (rule card_Un_disjoint[OF finite_fset finite_fset])
 
-lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+lemma fcard_delete1_less: 
+  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
   unfolding fset_to_set_trans
   by (rule card_Diff1_less[OF finite_fset])
 
-lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+lemma fcard_delete2_less: 
+  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
   unfolding fset_to_set_trans
   by (rule card_Diff2_less[OF finite_fset])
 
-lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+lemma fcard_delete1_le: 
+  shows "fcard (fdelete xs x) \<le> fcard xs"
   unfolding fset_to_set_trans
   by (rule card_Diff1_le[OF finite_fset])
 
-lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+lemma fcard_psubset: 
+  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
   unfolding fset_to_set_trans
   by (rule card_psubset[OF finite_fset])
 
-lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+lemma fcard_fmap_le: 
+  shows "fcard (fmap f xs) \<le> fcard xs"
   unfolding fset_to_set_trans
   by (rule card_image_le[OF finite_fset])
 
-lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+lemma fin_fminus_fnotin: 
+  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
   unfolding fset_to_set_trans
   by blast
 
-lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+lemma fin_fnotin_fminus: 
+  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
   unfolding fset_to_set_trans
   by blast
 
-lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+lemma fin_mdef: "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
   unfolding fset_to_set_trans
   by blast
 
@@ -1370,7 +1366,7 @@
 lemma fcard_fminus_subset_finter:
   "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
   unfolding fset_to_set_trans
-  by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
+  by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset)
 
 
 ML {*