684
|
1 |
theory FSet2
|
1128
|
2 |
imports "../Quotient" "../Quotient_List" List
|
684
|
3 |
begin
|
|
4 |
|
|
5 |
inductive
|
|
6 |
list_eq (infix "\<approx>" 50)
|
|
7 |
where
|
|
8 |
"a#b#xs \<approx> b#a#xs"
|
|
9 |
| "[] \<approx> []"
|
|
10 |
| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
|
|
11 |
| "a#a#xs \<approx> a#xs"
|
|
12 |
| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
|
|
13 |
| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
|
|
14 |
|
|
15 |
lemma list_eq_refl:
|
|
16 |
shows "xs \<approx> xs"
|
|
17 |
by (induct xs) (auto intro: list_eq.intros)
|
|
18 |
|
|
19 |
lemma equivp_list_eq:
|
|
20 |
shows "equivp list_eq"
|
|
21 |
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
|
|
22 |
by (auto intro: list_eq.intros list_eq_refl)
|
|
23 |
|
1144
|
24 |
quotient_type
|
787
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
'a fset = "'a list" / "list_eq"
|
684
|
26 |
by (rule equivp_list_eq)
|
|
27 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
quotient_definition
|
1144
|
29 |
fempty ("{||}")
|
|
30 |
where
|
|
31 |
"fempty :: 'a fset"
|
1139
|
32 |
is
|
684
|
33 |
"[]"
|
|
34 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
quotient_definition
|
705
|
36 |
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
|
1139
|
37 |
is
|
684
|
38 |
"(op #)"
|
|
39 |
|
|
40 |
lemma finsert_rsp[quot_respect]:
|
|
41 |
shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
|
|
42 |
by (auto intro: list_eq.intros)
|
|
43 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
quotient_definition
|
1144
|
45 |
funion ("_ \<union>f _" [65,66] 65)
|
|
46 |
where
|
|
47 |
"funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
|
1139
|
48 |
is
|
684
|
49 |
"(op @)"
|
|
50 |
|
|
51 |
lemma append_rsp_aux1:
|
|
52 |
assumes a : "l2 \<approx> r2 "
|
|
53 |
shows "(h @ l2) \<approx> (h @ r2)"
|
|
54 |
using a
|
|
55 |
apply(induct h)
|
|
56 |
apply(auto intro: list_eq.intros(5))
|
|
57 |
done
|
|
58 |
|
|
59 |
lemma append_rsp_aux2:
|
|
60 |
assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "
|
|
61 |
shows "(l1 @ l2) \<approx> (r1 @ r2)"
|
|
62 |
using a
|
|
63 |
apply(induct arbitrary: l2 r2)
|
|
64 |
apply(simp_all)
|
|
65 |
apply(blast intro: list_eq.intros append_rsp_aux1)+
|
|
66 |
done
|
|
67 |
|
|
68 |
lemma append_rsp[quot_respect]:
|
|
69 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
|
|
70 |
by (auto simp add: append_rsp_aux2)
|
|
71 |
|
|
72 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
quotient_definition
|
1144
|
74 |
fmem ("_ \<in>f _" [50, 51] 50)
|
|
75 |
where
|
|
76 |
"fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
|
1139
|
77 |
is
|
684
|
78 |
"(op mem)"
|
|
79 |
|
|
80 |
lemma memb_rsp_aux:
|
|
81 |
assumes a: "x \<approx> y"
|
|
82 |
shows "(z mem x) = (z mem y)"
|
|
83 |
using a by induct auto
|
|
84 |
|
|
85 |
lemma memb_rsp[quot_respect]:
|
|
86 |
shows "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
|
|
87 |
by (simp add: memb_rsp_aux)
|
|
88 |
|
1144
|
89 |
definition
|
684
|
90 |
fnot_mem :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
|
|
91 |
where
|
|
92 |
"x \<notin>f S \<equiv> \<not>(x \<in>f S)"
|
|
93 |
|
|
94 |
definition
|
|
95 |
"inter_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
|
96 |
where
|
|
97 |
"inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
|
|
98 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
quotient_definition
|
1144
|
100 |
finter ("_ \<inter>f _" [70, 71] 70)
|
|
101 |
where
|
|
102 |
"finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
|
1139
|
103 |
is
|
684
|
104 |
"inter_list"
|
|
105 |
|
|
106 |
no_syntax
|
|
107 |
"@Finset" :: "args => 'a fset" ("{|(_)|}")
|
|
108 |
syntax
|
|
109 |
"@Finfset" :: "args => 'a fset" ("{|(_)|}")
|
|
110 |
translations
|
|
111 |
"{|x, xs|}" == "CONST finsert x {|xs|}"
|
|
112 |
"{|x|}" == "CONST finsert x {||}"
|
|
113 |
|
|
114 |
|
|
115 |
subsection {* Empty sets *}
|
|
116 |
|
|
117 |
lemma test:
|
|
118 |
shows "\<not>(x # xs \<approx> [])"
|
|
119 |
sorry
|
|
120 |
|
|
121 |
lemma finsert_not_empty[simp]:
|
|
122 |
shows "finsert x S \<noteq> {||}"
|
|
123 |
by (lifting test)
|
|
124 |
|
|
125 |
|
|
126 |
|
|
127 |
|
|
128 |
end;
|