839 % |
839 % |
840 \isadelimproof |
840 \isadelimproof |
841 % |
841 % |
842 \endisadelimproof |
842 \endisadelimproof |
843 \isanewline |
843 \isanewline |
|
844 \isacommand{end}\isamarkupfalse% |
|
845 % |
|
846 \isamarkupsection{Structured Natural Deduction% |
|
847 } |
|
848 \isamarkuptrue% |
|
849 % |
|
850 \isamarkupsubsection{Rule statements% |
|
851 } |
|
852 \isamarkuptrue% |
|
853 % |
|
854 \begin{isamarkuptext}% |
|
855 Isabelle/Pure ``theorems'' are always natural deduction rules, |
|
856 which sometimes happen to consist of a conclusion only. |
|
857 |
|
858 The framework connectives \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} indicate the |
|
859 rule structure declaratively. For example:% |
|
860 \end{isamarkuptext}% |
|
861 \isamarkuptrue% |
|
862 \isacommand{thm}\isamarkupfalse% |
|
863 \ conjI\isanewline |
|
864 \isacommand{thm}\isamarkupfalse% |
|
865 \ impI\isanewline |
|
866 \isacommand{thm}\isamarkupfalse% |
|
867 \ nat{\isaliteral{2E}{\isachardot}}induct% |
|
868 \begin{isamarkuptext}% |
|
869 The object-logic is embedded into the Pure framework via an implicit |
|
870 derivability judgment \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequote}}}. |
|
871 |
|
872 Thus any HOL formulae appears atomic to the Pure framework, while |
|
873 the rule structure outlines the corresponding proof pattern. |
|
874 |
|
875 This can be made explicit as follows:% |
|
876 \end{isamarkuptext}% |
|
877 \isamarkuptrue% |
|
878 \isacommand{notepad}\isamarkupfalse% |
|
879 \isanewline |
|
880 \isakeyword{begin}\isanewline |
|
881 % |
|
882 \isadelimproof |
|
883 \ \ % |
|
884 \endisadelimproof |
|
885 % |
|
886 \isatagproof |
|
887 \isacommand{write}\isamarkupfalse% |
|
888 \ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}% |
|
889 \endisatagproof |
|
890 {\isafoldproof}% |
|
891 % |
|
892 \isadelimproof |
|
893 \isanewline |
|
894 % |
|
895 \endisadelimproof |
|
896 \isanewline |
|
897 \ \ \isacommand{thm}\isamarkupfalse% |
|
898 \ conjI\isanewline |
|
899 \ \ \isacommand{thm}\isamarkupfalse% |
|
900 \ impI\isanewline |
|
901 \ \ \isacommand{thm}\isamarkupfalse% |
|
902 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline |
|
903 \isacommand{end}\isamarkupfalse% |
|
904 % |
|
905 \begin{isamarkuptext}% |
|
906 Isar provides first-class notation for rule statements as follows.% |
|
907 \end{isamarkuptext}% |
|
908 \isamarkuptrue% |
|
909 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% |
|
910 \ conjI\isanewline |
|
911 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% |
|
912 \ impI\isanewline |
|
913 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% |
|
914 \ nat{\isaliteral{2E}{\isachardot}}induct% |
|
915 \isamarkupsubsubsection{Examples% |
|
916 } |
|
917 \isamarkuptrue% |
|
918 % |
|
919 \begin{isamarkuptext}% |
|
920 Introductions and eliminations of some standard connectives of |
|
921 the object-logic can be written as rule statements as follows. (The |
|
922 proof ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.blast}{\mbox{\isa{blast}}}'' serves as sanity check.)% |
|
923 \end{isamarkuptext}% |
|
924 \isamarkuptrue% |
|
925 \isacommand{lemma}\isamarkupfalse% |
|
926 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}% |
|
927 \isadelimproof |
|
928 \ % |
|
929 \endisadelimproof |
|
930 % |
|
931 \isatagproof |
|
932 \isacommand{by}\isamarkupfalse% |
|
933 \ blast% |
|
934 \endisatagproof |
|
935 {\isafoldproof}% |
|
936 % |
|
937 \isadelimproof |
|
938 % |
|
939 \endisadelimproof |
|
940 \isanewline |
|
941 \isacommand{lemma}\isamarkupfalse% |
|
942 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% |
|
943 \isadelimproof |
|
944 \ % |
|
945 \endisadelimproof |
|
946 % |
|
947 \isatagproof |
|
948 \isacommand{by}\isamarkupfalse% |
|
949 \ blast% |
|
950 \endisatagproof |
|
951 {\isafoldproof}% |
|
952 % |
|
953 \isadelimproof |
|
954 % |
|
955 \endisadelimproof |
|
956 \isanewline |
|
957 \isanewline |
|
958 \isacommand{lemma}\isamarkupfalse% |
|
959 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% |
|
960 \isadelimproof |
|
961 \ % |
|
962 \endisadelimproof |
|
963 % |
|
964 \isatagproof |
|
965 \isacommand{by}\isamarkupfalse% |
|
966 \ blast% |
|
967 \endisatagproof |
|
968 {\isafoldproof}% |
|
969 % |
|
970 \isadelimproof |
|
971 % |
|
972 \endisadelimproof |
|
973 \isanewline |
|
974 \isacommand{lemma}\isamarkupfalse% |
|
975 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% |
|
976 \isadelimproof |
|
977 \ % |
|
978 \endisadelimproof |
|
979 % |
|
980 \isatagproof |
|
981 \isacommand{by}\isamarkupfalse% |
|
982 \ blast% |
|
983 \endisatagproof |
|
984 {\isafoldproof}% |
|
985 % |
|
986 \isadelimproof |
|
987 % |
|
988 \endisadelimproof |
|
989 \isanewline |
|
990 \isanewline |
|
991 \isacommand{lemma}\isamarkupfalse% |
|
992 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% |
|
993 \isadelimproof |
|
994 \ % |
|
995 \endisadelimproof |
|
996 % |
|
997 \isatagproof |
|
998 \isacommand{by}\isamarkupfalse% |
|
999 \ blast% |
|
1000 \endisatagproof |
|
1001 {\isafoldproof}% |
|
1002 % |
|
1003 \isadelimproof |
|
1004 % |
|
1005 \endisadelimproof |
|
1006 \isanewline |
|
1007 \isacommand{lemma}\isamarkupfalse% |
|
1008 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1009 \isadelimproof |
|
1010 \ % |
|
1011 \endisadelimproof |
|
1012 % |
|
1013 \isatagproof |
|
1014 \isacommand{by}\isamarkupfalse% |
|
1015 \ blast% |
|
1016 \endisatagproof |
|
1017 {\isafoldproof}% |
|
1018 % |
|
1019 \isadelimproof |
|
1020 % |
|
1021 \endisadelimproof |
|
1022 \isanewline |
|
1023 \isacommand{lemma}\isamarkupfalse% |
|
1024 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1025 \isadelimproof |
|
1026 \ % |
|
1027 \endisadelimproof |
|
1028 % |
|
1029 \isatagproof |
|
1030 \isacommand{by}\isamarkupfalse% |
|
1031 \ blast% |
|
1032 \endisatagproof |
|
1033 {\isafoldproof}% |
|
1034 % |
|
1035 \isadelimproof |
|
1036 % |
|
1037 \endisadelimproof |
|
1038 \isanewline |
|
1039 \isanewline |
|
1040 \isacommand{lemma}\isamarkupfalse% |
|
1041 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1042 \isadelimproof |
|
1043 \ % |
|
1044 \endisadelimproof |
|
1045 % |
|
1046 \isatagproof |
|
1047 \isacommand{by}\isamarkupfalse% |
|
1048 \ blast% |
|
1049 \endisatagproof |
|
1050 {\isafoldproof}% |
|
1051 % |
|
1052 \isadelimproof |
|
1053 % |
|
1054 \endisadelimproof |
|
1055 \isanewline |
|
1056 \isacommand{lemma}\isamarkupfalse% |
|
1057 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1058 \isadelimproof |
|
1059 \ % |
|
1060 \endisadelimproof |
|
1061 % |
|
1062 \isatagproof |
|
1063 \isacommand{by}\isamarkupfalse% |
|
1064 \ blast% |
|
1065 \endisatagproof |
|
1066 {\isafoldproof}% |
|
1067 % |
|
1068 \isadelimproof |
|
1069 % |
|
1070 \endisadelimproof |
|
1071 \isanewline |
|
1072 \isanewline |
|
1073 \isacommand{lemma}\isamarkupfalse% |
|
1074 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1075 \isadelimproof |
|
1076 \ % |
|
1077 \endisadelimproof |
|
1078 % |
|
1079 \isatagproof |
|
1080 \isacommand{by}\isamarkupfalse% |
|
1081 \ blast% |
|
1082 \endisatagproof |
|
1083 {\isafoldproof}% |
|
1084 % |
|
1085 \isadelimproof |
|
1086 % |
|
1087 \endisadelimproof |
|
1088 \isanewline |
|
1089 \isacommand{lemma}\isamarkupfalse% |
|
1090 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1091 \isadelimproof |
|
1092 \ % |
|
1093 \endisadelimproof |
|
1094 % |
|
1095 \isatagproof |
|
1096 \isacommand{by}\isamarkupfalse% |
|
1097 \ blast% |
|
1098 \endisatagproof |
|
1099 {\isafoldproof}% |
|
1100 % |
|
1101 \isadelimproof |
|
1102 % |
|
1103 \endisadelimproof |
|
1104 \isanewline |
|
1105 \isanewline |
|
1106 \isacommand{lemma}\isamarkupfalse% |
|
1107 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1108 \isadelimproof |
|
1109 \ % |
|
1110 \endisadelimproof |
|
1111 % |
|
1112 \isatagproof |
|
1113 \isacommand{by}\isamarkupfalse% |
|
1114 \ blast% |
|
1115 \endisatagproof |
|
1116 {\isafoldproof}% |
|
1117 % |
|
1118 \isadelimproof |
|
1119 % |
|
1120 \endisadelimproof |
|
1121 \isanewline |
|
1122 \isacommand{lemma}\isamarkupfalse% |
|
1123 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1124 \isadelimproof |
|
1125 \ % |
|
1126 \endisadelimproof |
|
1127 % |
|
1128 \isatagproof |
|
1129 \isacommand{by}\isamarkupfalse% |
|
1130 \ blast% |
|
1131 \endisatagproof |
|
1132 {\isafoldproof}% |
|
1133 % |
|
1134 \isadelimproof |
|
1135 % |
|
1136 \endisadelimproof |
|
1137 \isanewline |
|
1138 \isanewline |
|
1139 \isacommand{lemma}\isamarkupfalse% |
|
1140 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1141 \isadelimproof |
|
1142 \ % |
|
1143 \endisadelimproof |
|
1144 % |
|
1145 \isatagproof |
|
1146 \isacommand{by}\isamarkupfalse% |
|
1147 \ blast% |
|
1148 \endisatagproof |
|
1149 {\isafoldproof}% |
|
1150 % |
|
1151 \isadelimproof |
|
1152 % |
|
1153 \endisadelimproof |
|
1154 \isanewline |
|
1155 \isacommand{lemma}\isamarkupfalse% |
|
1156 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1157 \isadelimproof |
|
1158 \ % |
|
1159 \endisadelimproof |
|
1160 % |
|
1161 \isatagproof |
|
1162 \isacommand{by}\isamarkupfalse% |
|
1163 \ blast% |
|
1164 \endisatagproof |
|
1165 {\isafoldproof}% |
|
1166 % |
|
1167 \isadelimproof |
|
1168 % |
|
1169 \endisadelimproof |
|
1170 \isanewline |
|
1171 \isacommand{lemma}\isamarkupfalse% |
|
1172 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1173 \isadelimproof |
|
1174 \ % |
|
1175 \endisadelimproof |
|
1176 % |
|
1177 \isatagproof |
|
1178 \isacommand{by}\isamarkupfalse% |
|
1179 \ blast% |
|
1180 \endisatagproof |
|
1181 {\isafoldproof}% |
|
1182 % |
|
1183 \isadelimproof |
|
1184 % |
|
1185 \endisadelimproof |
|
1186 % |
|
1187 \isamarkupsubsection{Isar context elements% |
|
1188 } |
|
1189 \isamarkuptrue% |
|
1190 % |
|
1191 \begin{isamarkuptext}% |
|
1192 We derive some results out of the blue, using Isar context |
|
1193 elements and some explicit blocks. This illustrates their meaning |
|
1194 wrt.\ Pure connectives, without goal states getting in the way.% |
|
1195 \end{isamarkuptext}% |
|
1196 \isamarkuptrue% |
|
1197 \isacommand{notepad}\isamarkupfalse% |
|
1198 \isanewline |
|
1199 \isakeyword{begin}\isanewline |
|
1200 % |
|
1201 \isadelimproof |
|
1202 \ \ % |
|
1203 \endisadelimproof |
|
1204 % |
|
1205 \isatagproof |
|
1206 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
|
1207 \isanewline |
|
1208 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1209 \ x\isanewline |
|
1210 \ \ \ \ \isacommand{have}\isamarkupfalse% |
|
1211 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1212 \isanewline |
|
1213 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
|
1214 \isanewline |
|
1215 \ \ \isacommand{have}\isamarkupfalse% |
|
1216 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1217 \ fact\isanewline |
|
1218 \isanewline |
|
1219 \isacommand{next}\isamarkupfalse% |
|
1220 \isanewline |
|
1221 \isanewline |
|
1222 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
|
1223 \isanewline |
|
1224 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1225 \ A\isanewline |
|
1226 \ \ \ \ \isacommand{have}\isamarkupfalse% |
|
1227 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1228 \isanewline |
|
1229 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
|
1230 \isanewline |
|
1231 \ \ \isacommand{have}\isamarkupfalse% |
|
1232 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1233 \ fact\isanewline |
|
1234 \isanewline |
|
1235 \isacommand{next}\isamarkupfalse% |
|
1236 \isanewline |
|
1237 \isanewline |
|
1238 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
|
1239 \isanewline |
|
1240 \ \ \ \ \isacommand{def}\isamarkupfalse% |
|
1241 \ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isanewline |
|
1242 \ \ \ \ \isacommand{have}\isamarkupfalse% |
|
1243 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1244 \isanewline |
|
1245 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
|
1246 \isanewline |
|
1247 \ \ \isacommand{have}\isamarkupfalse% |
|
1248 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1249 \ fact\isanewline |
|
1250 \isanewline |
|
1251 \isacommand{next}\isamarkupfalse% |
|
1252 \isanewline |
|
1253 \isanewline |
|
1254 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
|
1255 \isanewline |
|
1256 \ \ \ \ \isacommand{obtain}\isamarkupfalse% |
|
1257 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1258 \isanewline |
|
1259 \ \ \ \ \isacommand{have}\isamarkupfalse% |
|
1260 \ C\ \isacommand{sorry}\isamarkupfalse% |
|
1261 \isanewline |
|
1262 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
|
1263 \isanewline |
|
1264 \ \ \isacommand{have}\isamarkupfalse% |
|
1265 \ C\ \isacommand{by}\isamarkupfalse% |
|
1266 \ fact% |
|
1267 \endisatagproof |
|
1268 {\isafoldproof}% |
|
1269 % |
|
1270 \isadelimproof |
|
1271 \isanewline |
|
1272 % |
|
1273 \endisadelimproof |
|
1274 \isanewline |
|
1275 \isacommand{end}\isamarkupfalse% |
|
1276 % |
|
1277 \isamarkupsubsection{Pure rule composition% |
|
1278 } |
|
1279 \isamarkuptrue% |
|
1280 % |
|
1281 \begin{isamarkuptext}% |
|
1282 The Pure framework provides means for: |
|
1283 |
|
1284 \begin{itemize} |
|
1285 |
|
1286 \item backward-chaining of rules by \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} |
|
1287 |
|
1288 \item closing of branches by \hyperlink{inference.assumption}{\mbox{\isa{assumption}}} |
|
1289 |
|
1290 \end{itemize} |
|
1291 |
|
1292 Both principles involve higher-order unification of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms |
|
1293 modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-equivalence (cf.\ Huet and Miller).% |
|
1294 \end{isamarkuptext}% |
|
1295 \isamarkuptrue% |
|
1296 \isacommand{notepad}\isamarkupfalse% |
|
1297 \isanewline |
|
1298 \isakeyword{begin}\isanewline |
|
1299 % |
|
1300 \isadelimproof |
|
1301 \ \ % |
|
1302 \endisadelimproof |
|
1303 % |
|
1304 \isatagproof |
|
1305 \isacommand{assume}\isamarkupfalse% |
|
1306 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B% |
|
1307 \endisatagproof |
|
1308 {\isafoldproof}% |
|
1309 % |
|
1310 \isadelimproof |
|
1311 \isanewline |
|
1312 % |
|
1313 \endisadelimproof |
|
1314 \ \ \isacommand{thm}\isamarkupfalse% |
|
1315 \ conjI\isanewline |
|
1316 \ \ \isacommand{thm}\isamarkupfalse% |
|
1317 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ % |
|
1318 \isamarkupcmt{instantiation% |
|
1319 } |
|
1320 \isanewline |
|
1321 \ \ \isacommand{thm}\isamarkupfalse% |
|
1322 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{2C}{\isacharcomma}}\ OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ % |
|
1323 \isamarkupcmt{instantiation and composition% |
|
1324 } |
|
1325 \isanewline |
|
1326 \ \ \isacommand{thm}\isamarkupfalse% |
|
1327 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ % |
|
1328 \isamarkupcmt{composition via unification (trivial)% |
|
1329 } |
|
1330 \isanewline |
|
1331 \ \ \isacommand{thm}\isamarkupfalse% |
|
1332 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
|
1333 \isanewline |
|
1334 \ \ \isacommand{thm}\isamarkupfalse% |
|
1335 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
|
1336 \isacommand{end}\isamarkupfalse% |
|
1337 % |
|
1338 \begin{isamarkuptext}% |
|
1339 Note: Low-level rule composition is tedious and leads to |
|
1340 unreadable~/ unmaintainable expressions in the text.% |
|
1341 \end{isamarkuptext}% |
|
1342 \isamarkuptrue% |
|
1343 % |
|
1344 \isamarkupsubsection{Structured backward reasoning% |
|
1345 } |
|
1346 \isamarkuptrue% |
|
1347 % |
|
1348 \begin{isamarkuptext}% |
|
1349 Idea: Canonical proof decomposition via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ |
|
1350 \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, where the body produces a |
|
1351 natural deduction rule to refine some goal.% |
|
1352 \end{isamarkuptext}% |
|
1353 \isamarkuptrue% |
|
1354 \isacommand{notepad}\isamarkupfalse% |
|
1355 \isanewline |
|
1356 \isakeyword{begin}\isanewline |
|
1357 % |
|
1358 \isadelimproof |
|
1359 \ \ % |
|
1360 \endisadelimproof |
|
1361 % |
|
1362 \isatagproof |
|
1363 \isacommand{fix}\isamarkupfalse% |
|
1364 \ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1365 \isanewline |
|
1366 \ \ \isacommand{have}\isamarkupfalse% |
|
1367 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1368 \ \ \isacommand{proof}\isamarkupfalse% |
|
1369 \ {\isaliteral{2D}{\isacharminus}}\isanewline |
|
1370 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1371 \ x\isanewline |
|
1372 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1373 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1374 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1375 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1376 \isanewline |
|
1377 \ \ \isacommand{qed}\isamarkupfalse% |
|
1378 \isanewline |
|
1379 \isanewline |
|
1380 \ \ \isacommand{have}\isamarkupfalse% |
|
1381 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1382 \ \ \isacommand{proof}\isamarkupfalse% |
|
1383 \ {\isaliteral{2D}{\isacharminus}}\isanewline |
|
1384 \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
|
1385 \isanewline |
|
1386 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1387 \ x\isanewline |
|
1388 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1389 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1390 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1391 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1392 \isanewline |
|
1393 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
|
1394 \ % |
|
1395 \isamarkupcmt{implicit block structure made explicit% |
|
1396 } |
|
1397 \isanewline |
|
1398 \ \ \ \ \isacommand{note}\isamarkupfalse% |
|
1399 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1400 \ \ \ \ \ \ % |
|
1401 \isamarkupcmt{side exit for the resulting rule% |
|
1402 } |
|
1403 \isanewline |
|
1404 \ \ \isacommand{qed}\isamarkupfalse% |
|
1405 % |
|
1406 \endisatagproof |
|
1407 {\isafoldproof}% |
|
1408 % |
|
1409 \isadelimproof |
|
1410 \isanewline |
|
1411 % |
|
1412 \endisadelimproof |
|
1413 \isacommand{end}\isamarkupfalse% |
|
1414 % |
|
1415 \isamarkupsubsection{Structured rule application% |
|
1416 } |
|
1417 \isamarkuptrue% |
|
1418 % |
|
1419 \begin{isamarkuptext}% |
|
1420 Idea: Previous facts and new claims are composed with a rule from |
|
1421 the context (or background library).% |
|
1422 \end{isamarkuptext}% |
|
1423 \isamarkuptrue% |
|
1424 \isacommand{notepad}\isamarkupfalse% |
|
1425 \isanewline |
|
1426 \isakeyword{begin}\isanewline |
|
1427 % |
|
1428 \isadelimproof |
|
1429 \ \ % |
|
1430 \endisadelimproof |
|
1431 % |
|
1432 \isatagproof |
|
1433 \isacommand{assume}\isamarkupfalse% |
|
1434 \ r{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ % |
|
1435 \isamarkupcmt{simple rule (Horn clause)% |
|
1436 } |
|
1437 \isanewline |
|
1438 \isanewline |
|
1439 \ \ \isacommand{have}\isamarkupfalse% |
|
1440 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1441 \ \ % |
|
1442 \isamarkupcmt{prefix of facts via outer sub-proof% |
|
1443 } |
|
1444 \isanewline |
|
1445 \ \ \isacommand{then}\isamarkupfalse% |
|
1446 \ \isacommand{have}\isamarkupfalse% |
|
1447 \ C\isanewline |
|
1448 \ \ \isacommand{proof}\isamarkupfalse% |
|
1449 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1450 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1451 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1452 \ \ % |
|
1453 \isamarkupcmt{remaining rule premises via inner sub-proof% |
|
1454 } |
|
1455 \isanewline |
|
1456 \ \ \isacommand{qed}\isamarkupfalse% |
|
1457 \isanewline |
|
1458 \isanewline |
|
1459 \ \ \isacommand{have}\isamarkupfalse% |
|
1460 \ C\isanewline |
|
1461 \ \ \isacommand{proof}\isamarkupfalse% |
|
1462 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1463 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1464 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1465 \isanewline |
|
1466 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1467 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1468 \isanewline |
|
1469 \ \ \isacommand{qed}\isamarkupfalse% |
|
1470 \isanewline |
|
1471 \isanewline |
|
1472 \ \ \isacommand{have}\isamarkupfalse% |
|
1473 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% |
|
1474 \isanewline |
|
1475 \ \ \isacommand{then}\isamarkupfalse% |
|
1476 \ \isacommand{have}\isamarkupfalse% |
|
1477 \ C\isanewline |
|
1478 \ \ \isacommand{proof}\isamarkupfalse% |
|
1479 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1480 \ \ \isacommand{qed}\isamarkupfalse% |
|
1481 \isanewline |
|
1482 \isanewline |
|
1483 \ \ \isacommand{have}\isamarkupfalse% |
|
1484 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% |
|
1485 \isanewline |
|
1486 \ \ \isacommand{then}\isamarkupfalse% |
|
1487 \ \isacommand{have}\isamarkupfalse% |
|
1488 \ C\ \isacommand{by}\isamarkupfalse% |
|
1489 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1490 \isanewline |
|
1491 \isacommand{next}\isamarkupfalse% |
|
1492 \isanewline |
|
1493 \isanewline |
|
1494 \ \ \isacommand{assume}\isamarkupfalse% |
|
1495 \ r{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ % |
|
1496 \isamarkupcmt{nested rule% |
|
1497 } |
|
1498 \isanewline |
|
1499 \isanewline |
|
1500 \ \ \isacommand{have}\isamarkupfalse% |
|
1501 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1502 \isanewline |
|
1503 \ \ \isacommand{then}\isamarkupfalse% |
|
1504 \ \isacommand{have}\isamarkupfalse% |
|
1505 \ C\isanewline |
|
1506 \ \ \isacommand{proof}\isamarkupfalse% |
|
1507 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1508 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1509 \ x\isanewline |
|
1510 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1511 \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1512 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1513 \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1514 \isanewline |
|
1515 \ \ \isacommand{qed}\isamarkupfalse% |
|
1516 % |
|
1517 \begin{isamarkuptxt}% |
|
1518 The compound rule premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequote}}} is better |
|
1519 addressed via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} |
|
1520 in the nested proof body.% |
|
1521 \end{isamarkuptxt}% |
|
1522 \isamarkuptrue% |
|
1523 % |
|
1524 \endisatagproof |
|
1525 {\isafoldproof}% |
|
1526 % |
|
1527 \isadelimproof |
|
1528 % |
|
1529 \endisadelimproof |
|
1530 \isacommand{end}\isamarkupfalse% |
|
1531 % |
|
1532 \isamarkupsubsection{Example: predicate logic% |
|
1533 } |
|
1534 \isamarkuptrue% |
|
1535 % |
|
1536 \begin{isamarkuptext}% |
|
1537 Using the above principles, standard introduction and elimination proofs |
|
1538 of predicate logic connectives of HOL work as follows.% |
|
1539 \end{isamarkuptext}% |
|
1540 \isamarkuptrue% |
|
1541 \isacommand{notepad}\isamarkupfalse% |
|
1542 \isanewline |
|
1543 \isakeyword{begin}\isanewline |
|
1544 % |
|
1545 \isadelimproof |
|
1546 \ \ % |
|
1547 \endisadelimproof |
|
1548 % |
|
1549 \isatagproof |
|
1550 \isacommand{have}\isamarkupfalse% |
|
1551 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse% |
|
1552 \isanewline |
|
1553 \ \ \isacommand{then}\isamarkupfalse% |
|
1554 \ \isacommand{have}\isamarkupfalse% |
|
1555 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1556 \isanewline |
|
1557 \isanewline |
|
1558 \ \ \isacommand{have}\isamarkupfalse% |
|
1559 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1560 \isanewline |
|
1561 \ \ \isacommand{then}\isamarkupfalse% |
|
1562 \ \isacommand{have}\isamarkupfalse% |
|
1563 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1564 \isanewline |
|
1565 \isanewline |
|
1566 \ \ \isacommand{have}\isamarkupfalse% |
|
1567 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1568 \isanewline |
|
1569 \ \ \isacommand{then}\isamarkupfalse% |
|
1570 \ \isacommand{have}\isamarkupfalse% |
|
1571 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1572 \isanewline |
|
1573 \isanewline |
|
1574 \ \ \isacommand{have}\isamarkupfalse% |
|
1575 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1576 \isanewline |
|
1577 \ \ \isacommand{then}\isamarkupfalse% |
|
1578 \ \isacommand{have}\isamarkupfalse% |
|
1579 \ C\isanewline |
|
1580 \ \ \isacommand{proof}\isamarkupfalse% |
|
1581 \isanewline |
|
1582 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1583 \ A\isanewline |
|
1584 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1585 \ \isacommand{show}\isamarkupfalse% |
|
1586 \ C\ \isacommand{sorry}\isamarkupfalse% |
|
1587 \isanewline |
|
1588 \ \ \isacommand{next}\isamarkupfalse% |
|
1589 \isanewline |
|
1590 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1591 \ B\isanewline |
|
1592 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1593 \ \isacommand{show}\isamarkupfalse% |
|
1594 \ C\ \isacommand{sorry}\isamarkupfalse% |
|
1595 \isanewline |
|
1596 \ \ \isacommand{qed}\isamarkupfalse% |
|
1597 \isanewline |
|
1598 \isanewline |
|
1599 \ \ \isacommand{have}\isamarkupfalse% |
|
1600 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% |
|
1601 \isanewline |
|
1602 \ \ \isacommand{then}\isamarkupfalse% |
|
1603 \ \isacommand{have}\isamarkupfalse% |
|
1604 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1605 \isanewline |
|
1606 \isanewline |
|
1607 \ \ \isacommand{have}\isamarkupfalse% |
|
1608 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1609 \isanewline |
|
1610 \ \ \isacommand{then}\isamarkupfalse% |
|
1611 \ \isacommand{have}\isamarkupfalse% |
|
1612 \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1613 \isanewline |
|
1614 \isanewline |
|
1615 \ \ \isacommand{have}\isamarkupfalse% |
|
1616 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1617 \isanewline |
|
1618 \ \ \isacommand{then}\isamarkupfalse% |
|
1619 \ \isacommand{have}\isamarkupfalse% |
|
1620 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1621 \isanewline |
|
1622 \isanewline |
|
1623 \ \ \isacommand{have}\isamarkupfalse% |
|
1624 \ False\ \isacommand{sorry}\isamarkupfalse% |
|
1625 \isanewline |
|
1626 \ \ \isacommand{then}\isamarkupfalse% |
|
1627 \ \isacommand{have}\isamarkupfalse% |
|
1628 \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1629 \isanewline |
|
1630 \isanewline |
|
1631 \ \ \isacommand{have}\isamarkupfalse% |
|
1632 \ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1633 \isanewline |
|
1634 \isanewline |
|
1635 \ \ \isacommand{have}\isamarkupfalse% |
|
1636 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1637 \ \ \isacommand{proof}\isamarkupfalse% |
|
1638 \isanewline |
|
1639 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1640 \ A\isanewline |
|
1641 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1642 \ \isacommand{show}\isamarkupfalse% |
|
1643 \ False\ \isacommand{sorry}\isamarkupfalse% |
|
1644 \isanewline |
|
1645 \ \ \isacommand{qed}\isamarkupfalse% |
|
1646 \isanewline |
|
1647 \isanewline |
|
1648 \ \ \isacommand{have}\isamarkupfalse% |
|
1649 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse% |
|
1650 \isanewline |
|
1651 \ \ \isacommand{then}\isamarkupfalse% |
|
1652 \ \isacommand{have}\isamarkupfalse% |
|
1653 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1654 \isanewline |
|
1655 \isanewline |
|
1656 \ \ \isacommand{have}\isamarkupfalse% |
|
1657 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1658 \ \ \isacommand{proof}\isamarkupfalse% |
|
1659 \isanewline |
|
1660 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1661 \ x\isanewline |
|
1662 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1663 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1664 \isanewline |
|
1665 \ \ \isacommand{qed}\isamarkupfalse% |
|
1666 \isanewline |
|
1667 \isanewline |
|
1668 \ \ \isacommand{have}\isamarkupfalse% |
|
1669 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1670 \isanewline |
|
1671 \ \ \isacommand{then}\isamarkupfalse% |
|
1672 \ \isacommand{have}\isamarkupfalse% |
|
1673 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1674 \isanewline |
|
1675 \isanewline |
|
1676 \ \ \isacommand{have}\isamarkupfalse% |
|
1677 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1678 \ \ \isacommand{proof}\isamarkupfalse% |
|
1679 \isanewline |
|
1680 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1681 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1682 \isanewline |
|
1683 \ \ \isacommand{qed}\isamarkupfalse% |
|
1684 \isanewline |
|
1685 \isanewline |
|
1686 \ \ \isacommand{have}\isamarkupfalse% |
|
1687 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1688 \isanewline |
|
1689 \ \ \isacommand{then}\isamarkupfalse% |
|
1690 \ \isacommand{have}\isamarkupfalse% |
|
1691 \ C\isanewline |
|
1692 \ \ \isacommand{proof}\isamarkupfalse% |
|
1693 \isanewline |
|
1694 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1695 \ a\isanewline |
|
1696 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1697 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1698 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1699 \ C\ \isacommand{sorry}\isamarkupfalse% |
|
1700 \isanewline |
|
1701 \ \ \isacommand{qed}\isamarkupfalse% |
|
1702 % |
|
1703 \begin{isamarkuptxt}% |
|
1704 Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:% |
|
1705 \end{isamarkuptxt}% |
|
1706 \isamarkuptrue% |
|
1707 \ \ \isacommand{have}\isamarkupfalse% |
|
1708 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1709 \isanewline |
|
1710 \ \ \isacommand{then}\isamarkupfalse% |
|
1711 \ \isacommand{obtain}\isamarkupfalse% |
|
1712 \ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1713 % |
|
1714 \endisatagproof |
|
1715 {\isafoldproof}% |
|
1716 % |
|
1717 \isadelimproof |
|
1718 \isanewline |
|
1719 % |
|
1720 \endisadelimproof |
|
1721 \isacommand{end}\isamarkupfalse% |
|
1722 % |
|
1723 \begin{isamarkuptext}% |
|
1724 Further variations to illustrate Isar sub-proofs involving |
|
1725 \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:% |
|
1726 \end{isamarkuptext}% |
|
1727 \isamarkuptrue% |
|
1728 \isacommand{notepad}\isamarkupfalse% |
|
1729 \isanewline |
|
1730 \isakeyword{begin}\isanewline |
|
1731 % |
|
1732 \isadelimproof |
|
1733 \ \ % |
|
1734 \endisadelimproof |
|
1735 % |
|
1736 \isatagproof |
|
1737 \isacommand{have}\isamarkupfalse% |
|
1738 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1739 \ \ \isacommand{proof}\isamarkupfalse% |
|
1740 \ \ % |
|
1741 \isamarkupcmt{two strictly isolated subproofs% |
|
1742 } |
|
1743 \isanewline |
|
1744 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1745 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1746 \isanewline |
|
1747 \ \ \isacommand{next}\isamarkupfalse% |
|
1748 \isanewline |
|
1749 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1750 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1751 \isanewline |
|
1752 \ \ \isacommand{qed}\isamarkupfalse% |
|
1753 \isanewline |
|
1754 \isanewline |
|
1755 \ \ \isacommand{have}\isamarkupfalse% |
|
1756 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1757 \ \ \isacommand{proof}\isamarkupfalse% |
|
1758 \ \ % |
|
1759 \isamarkupcmt{one simultaneous sub-proof% |
|
1760 } |
|
1761 \isanewline |
|
1762 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1763 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% |
|
1764 \isanewline |
|
1765 \ \ \isacommand{qed}\isamarkupfalse% |
|
1766 \isanewline |
|
1767 \isanewline |
|
1768 \ \ \isacommand{have}\isamarkupfalse% |
|
1769 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1770 \ \ \isacommand{proof}\isamarkupfalse% |
|
1771 \ \ % |
|
1772 \isamarkupcmt{two subproofs in the same context% |
|
1773 } |
|
1774 \isanewline |
|
1775 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1776 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1777 \isanewline |
|
1778 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1779 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1780 \isanewline |
|
1781 \ \ \isacommand{qed}\isamarkupfalse% |
|
1782 \isanewline |
|
1783 \isanewline |
|
1784 \ \ \isacommand{have}\isamarkupfalse% |
|
1785 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1786 \ \ \isacommand{proof}\isamarkupfalse% |
|
1787 \ \ % |
|
1788 \isamarkupcmt{swapped order% |
|
1789 } |
|
1790 \isanewline |
|
1791 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1792 \ B\ \isacommand{sorry}\isamarkupfalse% |
|
1793 \isanewline |
|
1794 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1795 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1796 \isanewline |
|
1797 \ \ \isacommand{qed}\isamarkupfalse% |
|
1798 \isanewline |
|
1799 \isanewline |
|
1800 \ \ \isacommand{have}\isamarkupfalse% |
|
1801 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1802 \ \ \isacommand{proof}\isamarkupfalse% |
|
1803 \ \ % |
|
1804 \isamarkupcmt{sequential subproofs% |
|
1805 } |
|
1806 \isanewline |
|
1807 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1808 \ A\ \isacommand{sorry}\isamarkupfalse% |
|
1809 \isanewline |
|
1810 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1811 \ B\ \isacommand{using}\isamarkupfalse% |
|
1812 \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1813 \isanewline |
|
1814 \ \ \isacommand{qed}\isamarkupfalse% |
|
1815 % |
|
1816 \endisatagproof |
|
1817 {\isafoldproof}% |
|
1818 % |
|
1819 \isadelimproof |
|
1820 \isanewline |
|
1821 % |
|
1822 \endisadelimproof |
|
1823 \isacommand{end}\isamarkupfalse% |
|
1824 % |
|
1825 \isamarkupsubsubsection{Example: set-theoretic operators% |
|
1826 } |
|
1827 \isamarkuptrue% |
|
1828 % |
|
1829 \begin{isamarkuptext}% |
|
1830 There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.). Operators from |
|
1831 set-theory or lattice-theory for analogously. It is only a matter |
|
1832 of rule declarations in the library; rules can be also specified |
|
1833 explicitly.% |
|
1834 \end{isamarkuptext}% |
|
1835 \isamarkuptrue% |
|
1836 \isacommand{notepad}\isamarkupfalse% |
|
1837 \isanewline |
|
1838 \isakeyword{begin}\isanewline |
|
1839 % |
|
1840 \isadelimproof |
|
1841 \ \ % |
|
1842 \endisadelimproof |
|
1843 % |
|
1844 \isatagproof |
|
1845 \isacommand{have}\isamarkupfalse% |
|
1846 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1847 \isanewline |
|
1848 \ \ \isacommand{then}\isamarkupfalse% |
|
1849 \ \isacommand{have}\isamarkupfalse% |
|
1850 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1851 \isanewline |
|
1852 \isanewline |
|
1853 \ \ \isacommand{have}\isamarkupfalse% |
|
1854 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1855 \isanewline |
|
1856 \ \ \isacommand{then}\isamarkupfalse% |
|
1857 \ \isacommand{have}\isamarkupfalse% |
|
1858 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1859 \isanewline |
|
1860 \isanewline |
|
1861 \ \ \isacommand{have}\isamarkupfalse% |
|
1862 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1863 \isanewline |
|
1864 \ \ \isacommand{then}\isamarkupfalse% |
|
1865 \ \isacommand{have}\isamarkupfalse% |
|
1866 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1867 \isanewline |
|
1868 \isanewline |
|
1869 \ \ \isacommand{have}\isamarkupfalse% |
|
1870 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1871 \isanewline |
|
1872 \ \ \isacommand{then}\isamarkupfalse% |
|
1873 \ \isacommand{have}\isamarkupfalse% |
|
1874 \ C\isanewline |
|
1875 \ \ \isacommand{proof}\isamarkupfalse% |
|
1876 \isanewline |
|
1877 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1878 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1879 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1880 \ \isacommand{show}\isamarkupfalse% |
|
1881 \ C\ \isacommand{sorry}\isamarkupfalse% |
|
1882 \isanewline |
|
1883 \ \ \isacommand{next}\isamarkupfalse% |
|
1884 \isanewline |
|
1885 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1886 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1887 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1888 \ \isacommand{show}\isamarkupfalse% |
|
1889 \ C\ \isacommand{sorry}\isamarkupfalse% |
|
1890 \isanewline |
|
1891 \ \ \isacommand{qed}\isamarkupfalse% |
|
1892 \isanewline |
|
1893 \isanewline |
|
1894 \isacommand{next}\isamarkupfalse% |
|
1895 \isanewline |
|
1896 \ \ \isacommand{have}\isamarkupfalse% |
|
1897 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1898 \ \ \isacommand{proof}\isamarkupfalse% |
|
1899 \isanewline |
|
1900 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
1901 \ a\isanewline |
|
1902 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
1903 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1904 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1905 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1906 \isanewline |
|
1907 \ \ \isacommand{qed}\isamarkupfalse% |
|
1908 \isanewline |
|
1909 \isanewline |
|
1910 \ \ \isacommand{have}\isamarkupfalse% |
|
1911 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1912 \isanewline |
|
1913 \ \ \isacommand{then}\isamarkupfalse% |
|
1914 \ \isacommand{have}\isamarkupfalse% |
|
1915 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1916 \ \ \isacommand{proof}\isamarkupfalse% |
|
1917 \isanewline |
|
1918 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1919 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1920 \isanewline |
|
1921 \ \ \isacommand{qed}\isamarkupfalse% |
|
1922 \isanewline |
|
1923 \isanewline |
|
1924 \ \ \isacommand{have}\isamarkupfalse% |
|
1925 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1926 \isanewline |
|
1927 \ \ \isacommand{then}\isamarkupfalse% |
|
1928 \ \isacommand{have}\isamarkupfalse% |
|
1929 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1930 \isanewline |
|
1931 \isanewline |
|
1932 \ \ \isacommand{have}\isamarkupfalse% |
|
1933 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1934 \isanewline |
|
1935 \ \ \isacommand{then}\isamarkupfalse% |
|
1936 \ \isacommand{obtain}\isamarkupfalse% |
|
1937 \ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1938 % |
|
1939 \endisatagproof |
|
1940 {\isafoldproof}% |
|
1941 % |
|
1942 \isadelimproof |
|
1943 \isanewline |
|
1944 % |
|
1945 \endisadelimproof |
844 \isacommand{end}\isamarkupfalse% |
1946 \isacommand{end}\isamarkupfalse% |
845 \isanewline |
1947 \isanewline |
846 % |
1948 % |
847 \isadelimtheory |
1949 \isadelimtheory |
848 \isanewline |
1950 \isanewline |