--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/FSet3.thy	Fri Dec 11 15:49:15 2009 +0100
@@ -0,0 +1,279 @@
+theory FSet3
+imports "../QuotMain" List
+begin
+
+definition
+  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+  "list_eq x y = (\<forall>e. e mem x = e mem y)"
+
+lemma list_eq_reflp:
+  shows "xs \<approx> xs"
+  by (metis list_eq_def)
+
+lemma list_eq_equivp:
+  shows "equivp list_eq"
+  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+  apply (auto intro: list_eq_def)
+  apply (metis list_eq_def)
+  apply (metis list_eq_def)
+  sorry
+
+quotient fset = "'a list" / "list_eq"
+  by (rule list_eq_equivp)
+
+lemma not_nil_equiv_cons: "[] \<noteq> a # A" sorry
+
+(* The 2 lemmas below are different from the ones in QuotList *)
+lemma nil_rsp[quot_respect]:
+  shows "[] \<approx> []"
+by (rule list_eq_reflp)
+
+lemma cons_rsp[quot_respect]: (* Better then the one from QuotList *)
+  " (op = ===> op \<approx> ===> op \<approx>) op # op #"
+  sorry
+
+lemma mem_rsp[quot_respect]:
+  "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
+  sorry
+
+lemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"
+sorry
+
+lemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"
+sorry
+
+lemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"
+sorry
+
+lemma cons_left_comm: "x # y # A \<approx> y # x # A"
+sorry
+
+lemma cons_left_idem: "x # x # A \<approx> x # A"
+sorry
+
+lemma finite_set_raw_strong_cases:
+  "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
+  apply (induct X)
+  apply (simp)
+  sorry
+
+primrec
+  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
+where
+  "delete_raw [] x = []"
+| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
+
+lemma mem_delete_raw:
+  "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
+sorry
+
+lemma mem_delete_raw_ident:
+  "\<not>(MEM a (A delete_raw a))"
+sorry
+
+lemma not_mem_delete_raw_ident:
+  "\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"
+sorry
+
+lemma delete_raw_RSP:
+  "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
+sorry
+
+lemma cons_delete_raw:
+  "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"
+sorry
+
+lemma mem_cons_delete_raw:
+    "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
+sorry
+
+lemma finite_set_raw_delete_raw_cases1:
+    "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"
+sorry
+
+lemma finite_set_raw_delete_raw_cases:
+    "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
+sorry
+
+fun
+  card_raw :: "'a list \<Rightarrow> nat"
+where
+  card_raw_nil: "card_raw [] = 0"
+| card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))"
+
+lemma not_mem_card_raw:
+  fixes x :: "'a"
+  fixes xs :: "'a list"
+  shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"
+  sorry
+
+lemma card_raw_suc:
+  fixes xs :: "'a list"
+  fixes n :: "nat"
+  assumes c: "card_raw xs = Suc n"
+  shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
+  using c
+apply(induct xs)
+apply(metis mem_delete_raw)
+apply(metis mem_delete_raw)
+done
+
+lemma mem_card_raw_not_0:
+  "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
+sorry
+
+lemma card_raw_cons_gt_0:
+  "0 < card_raw (a # A)"
+sorry
+
+lemma card_raw_delete_raw:
+  "card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"
+sorry
+
+lemma card_raw_rsp_aux:
+  assumes e: "a \<approx> b"
+  shows "card_raw a = card_raw b"
+  using e sorry
+
+lemma card_raw_rsp[quot_respect]:
+  "(op \<approx> ===> op =) card_raw card_raw"
+  by (simp add: card_raw_rsp_aux)
+
+lemma card_raw_0:
+  "(card_raw A = 0) = (A = [])"
+sorry
+
+lemma list2set_thm:
+  shows "set [] = {}"
+  and "set (h # t) = insert h (set t)"
+sorry
+
+lemma list2set_RSP:
+  "A \<approx> B \<Longrightarrow> set A = set B"
+sorry
+
+definition
+  rsp_fold
+where
+  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
+
+primrec
+  fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+where
+  "fold_raw f z [] = z"
+| "fold_raw f z (a # A) =
+     (if (rsp_fold f) then
+       if a mem A then fold_raw f z A
+       else f a (fold_raw f z A)
+     else z)"
+
+lemma mem_lcommuting_fold_raw:
+  "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"
+sorry
+
+lemma fold_rsp[quot_respect]:
+  "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
+  apply (auto)
+  apply (case_tac "rsp_fold x")
+sorry
+
+lemma append_rsp[quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
+  sorry
+
+primrec
+  inter_raw
+where
+  "inter_raw [] B = []"
+| "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"
+
+lemma mem_inter_raw:
+  "x mem (inter_raw A B) = x mem A \<and> x mem B"
+sorry
+
+lemma inter_raw_RSP:
+  "A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"
+sorry
+
+
+(* LIFTING DEFS *)
+
+quotient_def
+  "Empty :: 'a fset" as "[]::'a list"
+
+quotient_def
+  "Insert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"
+
+quotient_def
+  "In :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" as "op mem"
+
+quotient_def
+  "Card :: 'a fset \<Rightarrow> nat" as "card_raw"
+
+quotient_def
+  "Delete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"
+
+quotient_def
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op @"
+
+quotient_def
+  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "inter_raw"
+
+quotient_def
+  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"
+
+quotient_def
+  "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"
+
+
+(* LIFTING THMS *)
+
+thm list.cases (* ??? *)
+
+thm cons_left_comm
+lemma "Insert a (Insert b x) = Insert b (Insert a x)"
+by (lifting cons_left_comm)
+
+thm cons_left_idem
+lemma "Insert a (Insert a x) = Insert a x"
+by (lifting cons_left_idem)
+
+(* thm MEM:
+  MEM x [] = F
+  MEM x (h::t) = (x=h) \/ MEM x t *)
+thm none_mem_nil
+thm mem_cons
+thm finite_set_raw_strong_cases
+thm card_raw.simps
+thm not_mem_card_raw
+thm card_raw_suc
+lemma "Card x = Suc n \<Longrightarrow> (\<exists>a b. \<not> In a b & x = Insert a b)"
+by (lifting card_raw_suc)
+
+thm card_raw_cons_gt_0
+thm mem_card_raw_not_0
+thm not_nil_equiv_cons
+thm delete_raw.simps
+thm mem_delete_raw
+thm card_raw_delete_raw
+thm cons_delete_raw
+thm mem_cons_delete_raw
+thm finite_set_raw_delete_raw_cases
+thm append.simps
+(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)
+thm inter_raw.simps
+thm mem_inter_raw
+thm fold_raw.simps
+thm list2set_thm
+thm list_eq_def
+thm list.induct
+lemma "\<lbrakk>P Empty; \<And>a x. P x \<Longrightarrow> P (Insert a x)\<rbrakk> \<Longrightarrow> P l"
+by (lifting list.induct)
+
+(* We also have map and some properties of it in FSet *)
+(* and the following which still lifts ok *)
+lemma "funion (funion x xa) xb = funion x (funion xa xb)"
+by (lifting append_assoc)
+
+end