--- a/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 12:25:52 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Mon Apr 26 10:01:13 2010 +0200
@@ -2,154 +2,6 @@
 imports "../../../Nominal/FSet"
 begin
 
-notation
-  list_eq (infix "\<approx>" 50)
-
-lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
-  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (lifting list.exhaust)
-
-(* PROBLEM: these lemmas needs to be restated, since  *)
-(* concat.simps(1) and concat.simps(2) contain the    *)
-(* type variables ?'a1.0 (which are turned into frees *)
-(* 'a_1                                               *)
-
-lemma concat1:
-  shows "concat [] \<approx> []"
-by (simp)
-
-lemma concat2:
-  shows "concat (x # xs) \<approx> x @ concat xs"
-by (simp)
-
-lemma concat_rsp:
-  "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y"
-  apply (induct x y arbitrary: x' y' rule: list_induct2')
-  apply simp
-  defer defer
-  apply (simp only: concat.simps)
-  sorry
-
-lemma [quot_respect]:
-  shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-  apply (simp only: fun_rel_def)
-  apply clarify
-  apply (rule concat_rsp)
-  apply assumption+
-  done
-
-lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
-  by (metis nil_rsp list_rel.simps(1) pred_compI)
-
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
-  apply (rule eq_reflection)
-  apply auto
-  done
-
-lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
-  unfolding list_eq.simps
-  apply(simp only: set_map set_in_eq)
-  done
-
-lemma quotient_compose_list_pre:
-  "(list_rel op \<approx> OOO op \<approx>) r s =
-  ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>
-  abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
-  apply rule
-  apply rule
-  apply rule
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply(rule)
-  apply rule
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
-  apply (metis Quotient_rel[OF Quotient_fset])
-  apply (auto simp only:)[1]
-  apply (subgoal_tac "map abs_fset r = map abs_fset b")
-  prefer 2
-  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  apply (subgoal_tac "map abs_fset s = map abs_fset ba")
-  prefer 2
-  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  apply (simp only: map_rel_cong)
-  apply rule
-  apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])
-  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  prefer 2
-  apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])
-  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (erule conjE)+
-  apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
-  prefer 2
-  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
-  apply (rule map_rel_cong)
-  apply (assumption)
-  done
-
-lemma quotient_compose_list[quot_thm]:
-  shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
-    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
-  unfolding Quotient_def comp_def
-  apply (rule)+
-  apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
-  apply (rule)
-  apply (rule)
-  apply (rule)
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (rule)
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply rule
-  apply (rule quotient_compose_list_pre)
-  done
-
-lemma fconcat_empty:
-  shows "fconcat {||} = {||}"
-  apply(lifting concat1)
-  apply(cleaning)
-  apply(simp add: comp_def bot_fset_def)
-  done
-
-lemma insert_rsp2[quot_respect]:
-  "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
-  apply auto
-  apply (simp add: set_in_eq)
-  apply (rule_tac b="x # b" in pred_compI)
-  apply auto
-  apply (rule_tac b="x # ba" in pred_compI)
-  apply auto
-  done
-
-lemma append_rsp[quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by (auto)
-
-lemma fconcat_insert:
-  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-  apply(lifting concat2)
-  apply(cleaning)
-  apply (simp add: finsert_def fconcat_def comp_def)
-  apply cleaning
-  done
-
 (* TBD *)
 
 text {* syntax for fset comprehensions (adapted from lists) *}