345 @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]} |
345 @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]} |
346 \hfill\numbered{relfun} |
346 \hfill\numbered{relfun} |
347 \end{isabelle} |
347 \end{isabelle} |
348 |
348 |
349 \noindent |
349 \noindent |
350 In the context of quotients, the following two notions from are \cite{Homeier05} |
350 In the context of quotients, the following two notions from \cite{Homeier05} |
351 needed later on. |
351 are needed later on. |
352 |
352 |
353 \begin{definition}[Respects]\label{def:respects} |
353 \begin{definition}[Respects]\label{def:respects} |
354 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}. |
354 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}. |
355 \end{definition} |
355 \end{definition} |
356 |
356 |
392 use of this part of Homeier's work including an extension |
392 use of this part of Homeier's work including an extension |
393 to deal with compositions of equivalence relations defined as follows: |
393 to deal with compositions of equivalence relations defined as follows: |
394 |
394 |
395 \begin{definition}[Composition of Relations] |
395 \begin{definition}[Composition of Relations] |
396 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate |
396 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate |
397 composition defined by @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
397 composition defined by |
|
398 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
398 holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and |
399 holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and |
399 @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}. |
400 @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}. |
400 \end{definition} |
401 \end{definition} |
401 |
402 |
402 \noindent |
403 \noindent |
408 quotient theorem for composing particular quotient relations. |
409 quotient theorem for composing particular quotient relations. |
409 For example, to lift theorems involving @{term flat} the quotient theorem for |
410 For example, to lift theorems involving @{term flat} the quotient theorem for |
410 composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} |
411 composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} |
411 with @{text R} being an equivalence relation, then |
412 with @{text R} being an equivalence relation, then |
412 |
413 |
413 @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"} |
414 @{text [display, indent=10] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map Abs) (map Rep \<circ> Rep_fset)"} |
414 |
415 |
415 \vspace{-.5mm} |
416 \vspace{-.5mm} |
416 *} |
417 *} |
417 |
418 |
418 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
419 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
836 occurrences of a raw type, but not others. |
837 occurrences of a raw type, but not others. |
837 |
838 |
838 The second and third proof step will always succeed if the appropriate |
839 The second and third proof step will always succeed if the appropriate |
839 respectfulness and preservation theorems are given. In contrast, the first |
840 respectfulness and preservation theorems are given. In contrast, the first |
840 proof step can fail: a theorem given by the user does not always |
841 proof step can fail: a theorem given by the user does not always |
841 imply a regularized version and a stronger one needs to be proved. This |
842 imply a regularized version and a stronger one needs to be proved. An example |
842 is outside of the scope where the quotient package can help. An example |
|
843 for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}. |
843 for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}. |
844 One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"}, |
844 One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"}, |
845 but the raw theorem only shows that particular element in the |
845 but this raw theorem only shows that particular element in the |
846 equivalence classes are not equal. A more general statement stipulating that |
846 equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a |
847 the equivalence classes are not equal is necessary, and then leads to the |
847 more general statement stipulating that the equivalence classes are not |
848 theorem @{text "0 \<noteq> 1"}. |
848 equal is necessary. This kind of failure is beyond the scope where the |
|
849 quotient package can help: the user has to provide a raw theorem that |
|
850 can be regularized automatically, or has to provide an explicit proof |
|
851 for the first proof step. |
849 |
852 |
850 In the following we will first define the statement of the |
853 In the following we will first define the statement of the |
851 regularized theorem based on @{text "raw_thm"} and |
854 regularized theorem based on @{text "raw_thm"} and |
852 @{text "quot_thm"}. Then we define the statement of the injected theorem, based |
855 @{text "quot_thm"}. Then we define the statement of the injected theorem, based |
853 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, |
856 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, |
921 \end{cases}$\\ |
924 \end{cases}$\\ |
922 \end{tabular} |
925 \end{tabular} |
923 \end{center} |
926 \end{center} |
924 |
927 |
925 \noindent |
928 \noindent |
926 where again the cases for existential quantifiers and unique existential |
929 In this definition we again omitted the cases for existential and unique existential |
927 quantifiers have been omitted. |
930 quantifiers. |
928 |
931 |
929 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
932 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
930 start with an implication. Isabelle provides \emph{mono} rules that can split up |
933 start with an implication. Isabelle provides \emph{mono} rules that can split up |
931 the implications into simpler implication subgoals. This succeeds for every |
934 the implications into simpler implicational subgoals. This succeeds for every |
932 monotone connective, except in places where the function @{text REG} inserted, |
935 monotone connective, except in places where the function @{text REG} inserted, |
933 for instance, a quantifier by a bounded quantifier. In this case we have |
936 for instance, a quantifier by a bounded quantifier. In this case we have |
934 rules of the form |
937 rules of the form |
935 |
938 |
936 @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"} |
939 @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"} |