# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260413230 -3600
# Node ID 0d9e8aa1bc7a28c4c41bd4ca5243f8ec25bded5b
# Parent  8aa67d037b3cd14c8e040156449baaf0e000b3d6
removed memb and used standard mem (member from List.thy)

diff -r 8aa67d037b3c -r 0d9e8aa1bc7a Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Thu Dec 10 03:25:42 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 03:47:10 2009 +0100
@@ -42,16 +42,10 @@
   "op @"
 
 fun
-  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
-where
-  m1: "(x memb []) = False"
-| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
-
-fun
   card1 :: "'a list \<Rightarrow> nat"
 where
   card1_nil: "(card1 []) = 0"
-| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
+| card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
 
 quotient_def
   CARD :: "CARD :: 'a fset \<Rightarrow> nat"
@@ -72,13 +66,13 @@
 lemma not_mem_card1:
   fixes x :: "'a"
   fixes xs :: "'a list"
-  shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))"
+  shows "(~(x mem xs)) = (card1 (x # xs) = Suc (card1 xs))"
   by auto
 
 lemma mem_cons:
   fixes x :: "'a"
   fixes xs :: "'a list"
-  assumes a : "x memb xs"
+  assumes a : "x mem xs"
   shows "x # xs \<approx> xs"
   using a by (induct xs) (auto intro: list_eq.intros )
 
@@ -86,7 +80,7 @@
   fixes xs :: "'a list"
   fixes n :: "nat"
   assumes c: "card1 xs = Suc n"
-  shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
+  shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)"
   using c
 apply(induct xs)
 apply (metis Suc_neq_Zero card1_0)
@@ -105,21 +99,21 @@
 | "fold1 f g z (a # A) =
      (if rsp_fold f
      then (
-       if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
+       if (a mem A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
      ) else z)"
 
 lemma fs1_strong_cases:
   fixes X :: "'a list"
-  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
   apply (induct X)
   apply (simp)
-  apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
+  apply (metis List.member.simps(1) QUOT_TYPE_I_fset.R_trans list_eq_refl mem_cons)
   done
 
 quotient_def
   IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 where
-  "membship"
+  "op mem"
 
 quotient_def
   FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
@@ -131,21 +125,21 @@
 where
   "map"
 
-lemma memb_rsp:
+lemma mem_rsp:
   fixes z
   assumes a: "x \<approx> y"
-  shows "(z memb x) = (z memb y)"
+  shows "(z mem x) = (z mem y)"
   using a by induct auto
 
 lemma ho_memb_rsp[quot_respect]:
-  "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
-  by (simp add: memb_rsp)
+  "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
+  by (simp add: mem_rsp)
 
 lemma card1_rsp:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
-  using e by induct (simp_all add:memb_rsp)
+  using e by induct (simp_all add: mem_rsp)
 
 lemma ho_card1_rsp[quot_respect]: 
   "(op \<approx> ===> op =) card1 card1"
@@ -207,20 +201,19 @@
   apply (simp_all)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
-  apply (auto simp add: memb_rsp rsp_fold_def)
+  apply (auto simp add: mem_rsp rsp_fold_def)
 done
 
 lemma list_equiv_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 by (auto intro: list_eq.intros)
 
-
 lemma "IN x EMPTY = False"
-apply(lifting m1)
+apply(lifting member.simps(1))
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
-by (lifting m2)
+by (lifting member.simps(2))
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
 apply (lifting list_eq.intros(4))