2085
|
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 |
|