diff -r a6f3e1b08494 -r b6873d123f9b Attic/Quot/Examples/Pair.thy
--- a/Attic/Quot/Examples/Pair.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-theory Pair
-imports Quotient_Product "../../../Nominal/FSet"
-begin
-
-fun alpha :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool" (infix "\<approx>" 100)
-where
-  "(a, b) \<approx> (c, d) = (a = c \<and> b = d \<or> a = d \<and> b = c)"
-
-lemma alpha_refl:
-  shows "z \<approx> z"
-  by (case_tac z, auto)
-
-lemma alpha_equivp:
-  shows "equivp op \<approx>"
-  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
-  by auto
-
-quotient_type
-  'a pair_set = "'a \<times> 'a" / alpha
-  by (auto intro: alpha_equivp)
-
-quotient_definition
-  "Two :: 'a \<Rightarrow> 'a \<Rightarrow> 'a pair_set"
-is
-  "Pair :: 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a)"
-
-fun
-  memb_both_lists
-where
-  "memb_both_lists a (b, c) = (memb a b \<and> memb a c)"
-
-quotient_definition
-  "mem_fsets :: 'a \<Rightarrow> 'a fset pair_set \<Rightarrow> bool"
-is memb_both_lists
-
-lemma prod_hlp: "prod_fun abs_fset abs_fset (prod_fun rep_fset rep_fset x) = x"
-  by (cases x, auto simp add: Quotient_abs_rep[OF Quotient_fset])
-
-lemma prod_hlp2:
-  "prod_rel list_eq list_eq (prod_fun rep_fset rep_fset z) (prod_fun rep_fset rep_fset z)"
-  by (cases z, simp)
-
-lemma [quot_thm]:
-  shows  "Quotient ((op \<approx>) OOO (prod_rel list_eq list_eq))
-    (abs_pair_set \<circ> prod_fun abs_fset abs_fset)
-    (prod_fun rep_fset rep_fset \<circ> rep_pair_set)"
-  unfolding Quotient_def comp_def
-  apply (intro conjI allI)
-  apply (simp add: prod_hlp Quotient_abs_rep[OF Quotient_pair_set])
-  apply rule
-  apply (rule alpha_refl)
-  apply rule
-  apply (rule prod_hlp2)
-  apply (rule alpha_refl)
-  apply (intro iffI conjI)
-  sorry
-
-lemma [quot_respect]:
-  "(op = ===> op \<approx> OOO prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists"
-  apply (intro fun_relI)
-  apply clarify
-  apply (simp only: memb_both_lists.simps)
-  sorry
-
-lemma [quot_respect]:
-  "(list_eq ===> list_eq ===> op \<approx> OOO prod_rel list_eq list_eq) Pair Pair"
-  apply (intro fun_relI)
-  apply rule
-  apply (rule alpha_refl)
-  apply rule
-  prefer 2
-  apply (rule alpha_refl)
-  apply simp
-  done
-
-lemma [quot_preserve]:
-  "(rep_fset ---> rep_fset ---> abs_pair_set \<circ> prod_fun abs_fset abs_fset) Pair = Two"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] Two_def)
-
-lemma "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
-  by (lifting memb_both_lists.simps)
-
-(* Doing it in 2 steps *)
-
-quotient_definition
-  "mem_lists :: 'a \<Rightarrow> 'a list pair_set \<Rightarrow> bool"
-is memb_both_lists
-
-lemma [quot_respect]: "(op = ===> op \<approx> ===> op =) memb_both_lists memb_both_lists"
-  by auto
-
-lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) Pair Pair"
-  by auto
-
-lemma step1: "mem_lists a (Two b c) = (memb a b \<and> memb a c)"
-  by (lifting memb_both_lists.simps)
-
-lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
-  (* apply (lifting step1) ??? *)
-  oops
-
-(* Doing it in 2 steps the other way *)
-
-quotient_definition
-  "memb_both_fsets :: 'a \<Rightarrow> 'a fset \<times> 'a fset \<Rightarrow> bool"
-is memb_both_lists
-
-lemma [quot_respect]:
-  "(op = ===> prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists"
-  by (auto simp add: memb_def[symmetric])
-
-lemma bla: "memb_both_fsets a (b, c) = (a |\<in>| b \<and> a |\<in>| c)"
-  by (lifting memb_both_lists.simps)
-
-lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
-  (* ??? *)
-  oops
-
-end
-