nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:fec38b7ceeb3
+:01d08af79f01
 will present a formal definition of our aggregate abstraction and
 representation functions (this definition was omitted in \cite{Homeier05}).
 They generate definitions, like the one above for @{text "\<Union>"},
 according to the type of the raw constant and the type
 of the quotient constant. This means we also have to extend the notions
-of \emph{respectfulness} and \emph{preservation} from Homeier
+of \emph{aggregate relation}, \emph{respectfulness} and \emph{preservation}
-\cite{Homeier05}.
+from Homeier \cite{Homeier05}.
 We will also address the criticism by Paulson \cite{Paulson06} cited at the
 beginning of this section about having to collect theorems that are lifted from the raw
 level to the quotient level. Our quotient package is the first one that is modular so that it
 allows to lift single theorems separately. This has the advantage for the
 and applies @{term "map rep_fset"} composed with @{term rep_fset} to
 its input, obtaining a list of lists, passes the result to @{term concat}
 obtaining a list and applies @{term abs_fset} obtaining the composed
 finite set.
-{\it we can compactify the term by noticing that map id\ldots id = id}
+For every type map function we require the property that @{term "map id = id"}.
+With this we can compactify the term, removing the identity mappings,
+obtaining a definition that is the same as the one privided by Homeier
+in the cases where the internal type does not change.
 {\it we should be able to prove}
 \begin{lemma}
 If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
 With the above definitions of @{text "REG"} and @{text "INJ"} we can show
 how the proof is performed. The first step is always the application of
 of the following lemma:
-@{term "[|A; A --> B; B = C; C = D|] ==> D"}
+@{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}
 With @{text A} instantiated to the original raw theorem,
 @{text B} instantiated to @{text "REG(A)"},
 @{text C} instantiated to @{text "INJ(REG(A))"},
 and @{text D} instantiated to the statement of the lifted theorem.
 the versions for the universal quantifier. For the existential quantifier
 and abstraction they are analogous with some symmetry.
 First, bounded universal quantifiers can be removed on the right:
-@{thm [display] ball_reg_right[no_vars]}
+@{thm [display, indent=10] ball_reg_right[no_vars]}
 They can be removed anywhere if the relation is an equivalence relation:
-@{thm [display] ball_reg_eqv[no_vars]}
+@{thm [display, indent=10] ball_reg_eqv[no_vars]}
 And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
-\[
-@{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}
+@{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
-\]
+The last theorem is new in comparison with Homeier's package, there the
-The last theorem is new in comparison with Homeier's package; it allows separating
+injection procedure would be used to prove goals with such shape, and there
-regularization from injection.
+the equivalence assumption would be useful. We use it directly also for
+composed relations where the range type is a type for which we know an
+equivalence theorem. This allows separating regularization from injection.
 *}
 (*
-@{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}
+@{thm bex_reg_eqv_range[no_vars]}
 @{thm [display] bex_reg_left[no_vars]}
 @{thm [display] bex1_bexeq_reg[no_vars]}
 @{thm [display] bex_reg_eqv[no_vars]}
 @{thm [display] babs_reg_eqv[no_vars]}
 @{thm [display] babs_simp[no_vars]}

changeset 2231	01d08af79f01
parent 2230	fec38b7ceeb3
child 2232	f49b5dfabd59