# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273485880 -7200
# Node ID 78ffb5b00e4fd42d25694a18e441c22f0e93eff9
# Parent  b1d64b7ce2b787458aa717ddf7a42da9421b332d
Membership in a pair of lists.

diff -r b1d64b7ce2b7 -r 78ffb5b00e4f Attic/Quot/Examples/Pair.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/Examples/Pair.thy	Mon May 10 12:04:40 2010 +0200
@@ -0,0 +1,120 @@
+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
+