1 theory Pair |
|
2 imports Quotient_Product "../../../Nominal/FSet" |
|
3 begin |
|
4 |
|
5 fun alpha :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool" (infix "\<approx>" 100) |
|
6 where |
|
7 "(a, b) \<approx> (c, d) = (a = c \<and> b = d \<or> a = d \<and> b = c)" |
|
8 |
|
9 lemma alpha_refl: |
|
10 shows "z \<approx> z" |
|
11 by (case_tac z, auto) |
|
12 |
|
13 lemma alpha_equivp: |
|
14 shows "equivp op \<approx>" |
|
15 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
|
16 by auto |
|
17 |
|
18 quotient_type |
|
19 'a pair_set = "'a \<times> 'a" / alpha |
|
20 by (auto intro: alpha_equivp) |
|
21 |
|
22 quotient_definition |
|
23 "Two :: 'a \<Rightarrow> 'a \<Rightarrow> 'a pair_set" |
|
24 is |
|
25 "Pair :: 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a)" |
|
26 |
|
27 fun |
|
28 memb_both_lists |
|
29 where |
|
30 "memb_both_lists a (b, c) = (memb a b \<and> memb a c)" |
|
31 |
|
32 quotient_definition |
|
33 "mem_fsets :: 'a \<Rightarrow> 'a fset pair_set \<Rightarrow> bool" |
|
34 is memb_both_lists |
|
35 |
|
36 lemma prod_hlp: "prod_fun abs_fset abs_fset (prod_fun rep_fset rep_fset x) = x" |
|
37 by (cases x, auto simp add: Quotient_abs_rep[OF Quotient_fset]) |
|
38 |
|
39 lemma prod_hlp2: |
|
40 "prod_rel list_eq list_eq (prod_fun rep_fset rep_fset z) (prod_fun rep_fset rep_fset z)" |
|
41 by (cases z, simp) |
|
42 |
|
43 lemma [quot_thm]: |
|
44 shows "Quotient ((op \<approx>) OOO (prod_rel list_eq list_eq)) |
|
45 (abs_pair_set \<circ> prod_fun abs_fset abs_fset) |
|
46 (prod_fun rep_fset rep_fset \<circ> rep_pair_set)" |
|
47 unfolding Quotient_def comp_def |
|
48 apply (intro conjI allI) |
|
49 apply (simp add: prod_hlp Quotient_abs_rep[OF Quotient_pair_set]) |
|
50 apply rule |
|
51 apply (rule alpha_refl) |
|
52 apply rule |
|
53 apply (rule prod_hlp2) |
|
54 apply (rule alpha_refl) |
|
55 apply (intro iffI conjI) |
|
56 sorry |
|
57 |
|
58 lemma [quot_respect]: |
|
59 "(op = ===> op \<approx> OOO prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists" |
|
60 apply (intro fun_relI) |
|
61 apply clarify |
|
62 apply (simp only: memb_both_lists.simps) |
|
63 sorry |
|
64 |
|
65 lemma [quot_respect]: |
|
66 "(list_eq ===> list_eq ===> op \<approx> OOO prod_rel list_eq list_eq) Pair Pair" |
|
67 apply (intro fun_relI) |
|
68 apply rule |
|
69 apply (rule alpha_refl) |
|
70 apply rule |
|
71 prefer 2 |
|
72 apply (rule alpha_refl) |
|
73 apply simp |
|
74 done |
|
75 |
|
76 lemma [quot_preserve]: |
|
77 "(rep_fset ---> rep_fset ---> abs_pair_set \<circ> prod_fun abs_fset abs_fset) Pair = Two" |
|
78 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] Two_def) |
|
79 |
|
80 lemma "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)" |
|
81 by (lifting memb_both_lists.simps) |
|
82 |
|
83 (* Doing it in 2 steps *) |
|
84 |
|
85 quotient_definition |
|
86 "mem_lists :: 'a \<Rightarrow> 'a list pair_set \<Rightarrow> bool" |
|
87 is memb_both_lists |
|
88 |
|
89 lemma [quot_respect]: "(op = ===> op \<approx> ===> op =) memb_both_lists memb_both_lists" |
|
90 by auto |
|
91 |
|
92 lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) Pair Pair" |
|
93 by auto |
|
94 |
|
95 lemma step1: "mem_lists a (Two b c) = (memb a b \<and> memb a c)" |
|
96 by (lifting memb_both_lists.simps) |
|
97 |
|
98 lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)" |
|
99 (* apply (lifting step1) ??? *) |
|
100 oops |
|
101 |
|
102 (* Doing it in 2 steps the other way *) |
|
103 |
|
104 quotient_definition |
|
105 "memb_both_fsets :: 'a \<Rightarrow> 'a fset \<times> 'a fset \<Rightarrow> bool" |
|
106 is memb_both_lists |
|
107 |
|
108 lemma [quot_respect]: |
|
109 "(op = ===> prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists" |
|
110 by (auto simp add: memb_def[symmetric]) |
|
111 |
|
112 lemma bla: "memb_both_fsets a (b, c) = (a |\<in>| b \<and> a |\<in>| c)" |
|
113 by (lifting memb_both_lists.simps) |
|
114 |
|
115 lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)" |
|
116 (* ??? *) |
|
117 oops |
|
118 |
|
119 end |
|
120 |
|