equal
deleted
inserted
replaced
891 \end{center} |
891 \end{center} |
892 % |
892 % |
893 \noindent |
893 \noindent |
894 In the above definition we omitted the cases for existential quantifiers |
894 In the above definition we omitted the cases for existential quantifiers |
895 and unique existential quantifiers, as they are very similar to the cases |
895 and unique existential quantifiers, as they are very similar to the cases |
896 for the universal quantifier. For the third and fourth clause, note that |
896 for the universal quantifier. |
897 @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}. |
|
898 |
897 |
899 Next we define the function @{text INJ} which takes as argument |
898 Next we define the function @{text INJ} which takes as argument |
900 @{text "reg_thm"} and @{text "quot_thm"} (both as |
899 @{text "reg_thm"} and @{text "quot_thm"} (both as |
901 terms) and returns @{text "inj_thm"}: |
900 terms) and returns @{text "inj_thm"}: |
902 |
901 |
928 \end{tabular} |
927 \end{tabular} |
929 \end{center} |
928 \end{center} |
930 |
929 |
931 \noindent |
930 \noindent |
932 In this definition we again omitted the cases for existential and unique existential |
931 In this definition we again omitted the cases for existential and unique existential |
933 quantifiers. |
932 quantifiers. |
934 |
933 |
935 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
934 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
936 start with an implication. Isabelle provides \emph{mono} rules that can split up |
935 start with an implication. Isabelle provides \emph{mono} rules that can split up |
937 the implications into simpler implicational subgoals. This succeeds for every |
936 the implications into simpler implicational subgoals. This succeeds for every |
938 monotone connective, except in places where the function @{text REG} replaced, |
937 monotone connective, except in places where the function @{text REG} replaced, |
997 |
996 |
998 \noindent |
997 \noindent |
999 Next, relations over lifted types are folded to equalities. |
998 Next, relations over lifted types are folded to equalities. |
1000 For this the following theorem has been shown by Homeier~\cite{Homeier05}: |
999 For this the following theorem has been shown by Homeier~\cite{Homeier05}: |
1001 |
1000 |
1002 @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]} |
1001 @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]} |
1003 |
1002 |
1004 \noindent |
1003 \noindent |
1005 Finally, we rewrite with the preservation theorems. This will result |
1004 Finally, we rewrite with the preservation theorems. This will result |
1006 in two equal terms that can be solved by reflexivity. |
1005 in two equal terms that can be solved by reflexivity. |
1007 *} |
1006 *} |
|
1007 |
1008 |
1008 |
1009 section {* Examples \label{sec:examples} *} |
1009 section {* Examples \label{sec:examples} *} |
1010 |
1010 |
1011 (* Mention why equivalence *) |
1011 (* Mention why equivalence *) |
1012 |
1012 |