diff -r 72cdd2af7eb4 -r c8b31085cb5b Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 10:20:48 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 10:24:39 2010 +0200
@@ -150,24 +150,6 @@
   apply cleaning
   done
 
-text {* raw section *}
-
-lemma map_rsp_aux:
-  assumes a: "a \<approx> b"
-  shows "map f a \<approx> map f b"
-  using a
-apply(induct a arbitrary: b)
-apply(auto)
-apply(metis rev_image_eqI)
-done
-
-lemma map_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-by (auto simp add: map_rsp_aux)
-
-
-text {* lifted section *}
-
 (* TBD *)
 
 text {* syntax for fset comprehensions (adapted from lists) *}
@@ -267,210 +249,4 @@
 (* BELOW CONSTRUCTION SITE *)
 
 
-lemma no_mem_nil: 
-  "(\<forall>a. a \<notin> set A) = (A = [])"
-by (induct A) (auto)
-
-lemma none_mem_nil: 
-  "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
-by simp
-
-lemma mem_cons: 
-  "a \<in> set A \<Longrightarrow> a # A \<approx> A"
-by auto
-
-lemma cons_left_comm:
-  "x # y # A \<approx> y # x # A"
-by (auto simp add: id_simps)
-
-lemma cons_left_idem:
-  "x # x # A \<approx> x # A"
-by (auto simp add: id_simps)
-
-lemma finite_set_raw_strong_cases:
-  "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
-  apply (induct X)
-  apply (simp)
-  apply (rule disjI2)
-  apply (erule disjE)
-  apply (rule_tac x="a" in exI)
-  apply (rule_tac x="[]" in exI)
-  apply (simp)
-  apply (erule exE)+
-  apply (case_tac "a = aa")
-  apply (rule_tac x="a" in exI)
-  apply (rule_tac x="Y" in exI)
-  apply (simp)
-  apply (rule_tac x="aa" in exI)
-  apply (rule_tac x="a # Y" in exI)
-  apply (auto)
-  done
-
-fun
-  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 \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"
-  by (induct A arbitrary: x a) (auto)
-
-lemma mem_delete_raw_ident:
-  "\<not>(a \<in> set (delete_raw A a))"
-by (induct A) (auto)
-
-lemma not_mem_delete_raw_ident:
-  "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
-by (induct A) (auto)
-
-lemma delete_raw_RSP:
-  "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
-apply(induct A arbitrary: B a)
-apply(auto)
-sorry
-
-lemma cons_delete_raw:
-  "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"
-sorry
-
-lemma mem_cons_delete_raw:
-    "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
-sorry
-
-lemma finite_set_raw_delete_raw_cases:
-    "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
-  by (induct X) (auto)
-
-
-
-
-
-lemma list2set_thm:
-  shows "set [] = {}"
-  and "set (h # t) = insert h (set t)"
-  by (auto)
-
-lemma list2set_RSP:
-  "A \<approx> B \<Longrightarrow> set A = set B"
-  by auto
-
-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)
-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 *)
-
-
-section {* Constants on the Quotient Type *} 
-
-
-quotient_definition
-  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
-  is "delete_raw"
-
-quotient_definition
-  finter ("_ \<inter>f _" [70, 71] 70)
-where
-  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is "inter_raw"
-
-quotient_definition
-  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
-  is "fold_raw"
-
-quotient_definition
-  "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
-  is "set"
-
-
-section {* Lifted Theorems *}
-
-thm list.cases (* ??? *)
-
-thm cons_left_comm
-lemma "finsert a (finsert b S) = finsert b (finsert a S)"
-by (lifting cons_left_comm)
-
-thm cons_left_idem
-lemma "finsert a (finsert a S) = finsert a S"
-by (lifting cons_left_idem)
-
-(* thm MEM:
-  MEM x [] = F
-  MEM x (h::t) = (x=h) \/ MEM x t *)
-thm none_mem_nil
-(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)
-
-thm mem_cons
-thm finite_set_raw_strong_cases
-(*thm card_raw.simps*)
-(*thm not_mem_card_raw*)
-(*thm card_raw_suc*)
-
-lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"
-(*by (lifting card_raw_suc)*)
-sorry
-
-(*thm card_raw_cons_gt_0
-thm mem_card_raw_gt_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 fempty; \<And>a x. P x \<Longrightarrow> P (finsert 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