3 imports "Quotient" |
3 imports "Quotient" |
4 "LaTeXsugar" |
4 "LaTeXsugar" |
5 begin |
5 begin |
6 |
6 |
7 notation (latex output) |
7 notation (latex output) |
|
8 rel_conj ("_ OOO _" [53, 53] 52) |
|
9 and |
|
10 fun_map ("_ ---> _" [51, 51] 50) |
|
11 and |
8 fun_rel ("_ ===> _" [51, 51] 50) |
12 fun_rel ("_ ===> _" [51, 51] 50) |
9 |
13 |
|
14 ML {* |
|
15 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
|
16 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
|
17 let |
|
18 val concl = |
|
19 Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t) |
|
20 in |
|
21 case concl of (_ $ l $ r) => proj (l, r) |
|
22 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) |
|
23 end); |
|
24 *} |
|
25 setup {* |
|
26 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
|
27 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
|
28 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
|
29 *} |
10 (*>*) |
30 (*>*) |
11 |
31 |
12 section {* Introduction *} |
32 section {* Introduction *} |
13 |
33 |
14 text {* |
34 text {* |
24 in terms of existing ones; the other is the introduction of new types |
44 in terms of existing ones; the other is the introduction of new types |
25 by identifying non-empty subsets in existing types. It is well understood |
45 by identifying non-empty subsets in existing types. It is well understood |
26 to use both mechanism for dealing with quotient constructions in HOL (cite Larry). |
46 to use both mechanism for dealing with quotient constructions in HOL (cite Larry). |
27 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
47 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
28 the type @{typ "nat \<times> nat"} and the equivalence relation |
48 the type @{typ "nat \<times> nat"} and the equivalence relation |
|
49 |
|
50 % I would avoid substraction for natural numbers. |
29 |
51 |
30 @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"} |
52 @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"} |
31 |
53 |
32 \noindent |
54 \noindent |
33 Similarly one can construct the type of finite sets by quotienting lists |
55 Similarly one can construct the type of finite sets by quotienting lists |
82 composition. |
104 composition. |
83 |
105 |
84 \item We allow lifting only some occurrences of quotiented |
106 \item We allow lifting only some occurrences of quotiented |
85 types. Rsp/Prs extended. (used in nominal) |
107 types. Rsp/Prs extended. (used in nominal) |
86 |
108 |
87 \item We regularize more thanks to new lemmas. (inductions in |
|
88 nominal). |
|
89 |
|
90 \item The quotient package is very modular. Definitions can be added |
109 \item The quotient package is very modular. Definitions can be added |
91 separately, rsp and prs can be proved separately and theorems can |
110 separately, rsp and prs can be proved separately and theorems can |
92 be lifted on a need basis. (useful with type-classes). |
111 be lifted on a need basis. (useful with type-classes). |
93 |
112 |
94 \item Can be used both manually (attribute, separate tactics, |
113 \item Can be used both manually (attribute, separate tactics, |
95 rsp/prs databases) and programatically (automated definition of |
114 rsp/prs databases) and programatically (automated definition of |
96 lifted constants, the rsp proof obligations and theorem statement |
115 lifted constants, the rsp proof obligations and theorem statement |
97 translation according to given quotients). |
116 translation according to given quotients). |
99 \end{itemize} |
118 \end{itemize} |
100 *} |
119 *} |
101 |
120 |
102 section {* Quotient Type*} |
121 section {* Quotient Type*} |
103 |
122 |
104 text {* |
123 |
105 Defintion of quotient, |
124 |
106 |
125 text {* |
107 Equivalence, |
126 In this section we present the definitions of a quotient that follow |
108 |
127 those by Homeier, the proofs can be found there. |
109 Relation map and function map |
128 |
|
129 \begin{definition}[Quotient] |
|
130 A relation $R$ with an abstraction function $Abs$ |
|
131 and a representation function $Rep$ is a \emph{quotient} |
|
132 if and only if: |
|
133 |
|
134 \begin{enumerate} |
|
135 \item @{thm (rhs1) Quotient_def[of "R", no_vars]} |
|
136 \item @{thm (rhs2) Quotient_def[of "R", no_vars]} |
|
137 \item @{thm (rhs3) Quotient_def[of "R", no_vars]} |
|
138 \end{enumerate} |
|
139 |
|
140 \end{definition} |
|
141 |
|
142 \begin{definition}[Relation map and function map] |
|
143 @{thm fun_rel_def[no_vars]}\\ |
|
144 @{thm fun_map_def[no_vars]} |
|
145 \end{definition} |
|
146 |
|
147 The main theorems for building higher order quotients is: |
|
148 \begin{lemma}[Function Quotient] |
|
149 If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]} |
|
150 then @{thm (concl) fun_quotient[no_vars]} |
|
151 \end{lemma} |
|
152 |
110 *} |
153 *} |
111 |
154 |
112 section {* Constants *} |
155 section {* Constants *} |
113 |
156 |
114 text {* |
157 (* Describe what containers are? *) |
115 Rep and Abs, Rsp and Prs |
158 |
|
159 text {* |
|
160 \begin{definition}[Composition of Relations] |
|
161 @{abbrev "rel_conj R1 R2"} |
|
162 \end{definition} |
|
163 |
|
164 The first operation that we describe is the generation of |
|
165 aggregate Abs or Rep function for two given compound types. |
|
166 This operation will be used for the constant defnitions |
|
167 and for the translation of theorems statements. It relies on |
|
168 knowing map functions and relation functions for container types. |
|
169 It follows the following algorithm: |
|
170 |
|
171 \begin{itemize} |
|
172 \item For equal types or free type variables return identity. |
|
173 |
|
174 \item For function types recurse, change the Rep/Abs flag to |
|
175 the opposite one for the domain type and compose the |
|
176 results with @{term "fun_map"}. |
|
177 |
|
178 \item For equal type constructors use the appropriate map function |
|
179 applied to the results for the arguments. |
|
180 |
|
181 \item For unequal type constructors are unequal, we look in the |
|
182 quotients information for a raw type quotient type pair that |
|
183 matches the given types. We apply the environment to the arguments |
|
184 and recurse composing it with the aggregate map function. |
|
185 \end{itemize} |
|
186 |
|
187 |
|
188 |
|
189 Rsp and Prs |
116 *} |
190 *} |
117 |
191 |
118 section {* Lifting Theorems *} |
192 section {* Lifting Theorems *} |
119 |
193 |
120 text {* TBD *} |
194 text {* TBD *} |