841 % |
841 % |
842 \endisadelimproof |
842 \endisadelimproof |
843 \isanewline |
843 \isanewline |
844 \isacommand{end}\isamarkupfalse% |
844 \isacommand{end}\isamarkupfalse% |
845 % |
845 % |
846 \isamarkupsection{Structured Natural Deduction% |
846 \isamarkupsection{Structured induction proofs% |
|
847 } |
|
848 \isamarkuptrue% |
|
849 % |
|
850 \isamarkupsubsection{Induction as Natural Deduction% |
|
851 } |
|
852 \isamarkuptrue% |
|
853 % |
|
854 \begin{isamarkuptext}% |
|
855 In principle, induction is just a special case of Natural |
|
856 Deduction (see also \secref{sec:natural-deduction-synopsis}). For |
|
857 example:% |
|
858 \end{isamarkuptext}% |
|
859 \isamarkuptrue% |
|
860 \isacommand{thm}\isamarkupfalse% |
|
861 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline |
|
862 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% |
|
863 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline |
|
864 \isanewline |
|
865 \isacommand{notepad}\isamarkupfalse% |
|
866 \isanewline |
|
867 \isakeyword{begin}\isanewline |
|
868 % |
|
869 \isadelimproof |
|
870 \ \ % |
|
871 \endisadelimproof |
|
872 % |
|
873 \isatagproof |
|
874 \isacommand{fix}\isamarkupfalse% |
|
875 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
876 \ \ \isacommand{have}\isamarkupfalse% |
|
877 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
878 \ \ \isacommand{proof}\isamarkupfalse% |
|
879 \ {\isaliteral{28}{\isacharparenleft}}rule\ nat{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\ \ % |
|
880 \isamarkupcmt{fragile rule application!% |
|
881 } |
|
882 \isanewline |
|
883 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
884 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
885 \isanewline |
|
886 \ \ \isacommand{next}\isamarkupfalse% |
|
887 \isanewline |
|
888 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
889 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
890 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
891 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
892 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
893 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
894 \isanewline |
|
895 \ \ \isacommand{qed}\isamarkupfalse% |
|
896 % |
|
897 \endisatagproof |
|
898 {\isafoldproof}% |
|
899 % |
|
900 \isadelimproof |
|
901 \isanewline |
|
902 % |
|
903 \endisadelimproof |
|
904 \isacommand{end}\isamarkupfalse% |
|
905 % |
|
906 \begin{isamarkuptext}% |
|
907 In practice, much more proof infrastructure is required. |
|
908 |
|
909 The proof method \hyperlink{method.induct}{\mbox{\isa{induct}}} provides: |
|
910 \begin{itemize} |
|
911 |
|
912 \item implicit rule selection and robust instantiation |
|
913 |
|
914 \item context elements via symbolic case names |
|
915 |
|
916 \item support for rule-structured induction statements, with local |
|
917 parameters, premises, etc. |
|
918 |
|
919 \end{itemize}% |
|
920 \end{isamarkuptext}% |
|
921 \isamarkuptrue% |
|
922 \isacommand{notepad}\isamarkupfalse% |
|
923 \isanewline |
|
924 \isakeyword{begin}\isanewline |
|
925 % |
|
926 \isadelimproof |
|
927 \ \ % |
|
928 \endisadelimproof |
|
929 % |
|
930 \isatagproof |
|
931 \isacommand{fix}\isamarkupfalse% |
|
932 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
933 \ \ \isacommand{have}\isamarkupfalse% |
|
934 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
935 \ \ \isacommand{proof}\isamarkupfalse% |
|
936 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
937 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
938 \ {\isadigit{0}}\isanewline |
|
939 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
940 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse% |
|
941 \isanewline |
|
942 \ \ \isacommand{next}\isamarkupfalse% |
|
943 \isanewline |
|
944 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
945 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
946 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
947 \ Suc{\isaliteral{2E}{\isachardot}}hyps\ \isacommand{show}\isamarkupfalse% |
|
948 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse% |
|
949 \isanewline |
|
950 \ \ \isacommand{qed}\isamarkupfalse% |
|
951 % |
|
952 \endisatagproof |
|
953 {\isafoldproof}% |
|
954 % |
|
955 \isadelimproof |
|
956 \isanewline |
|
957 % |
|
958 \endisadelimproof |
|
959 \isacommand{end}\isamarkupfalse% |
|
960 % |
|
961 \isamarkupsubsubsection{Example% |
|
962 } |
|
963 \isamarkuptrue% |
|
964 % |
|
965 \begin{isamarkuptext}% |
|
966 The subsequent example combines the following proof patterns: |
|
967 \begin{itemize} |
|
968 |
|
969 \item outermost induction (over the datatype structure of natural |
|
970 numbers), to decompose the proof problem in top-down manner |
|
971 |
|
972 \item calculational reasoning (\secref{sec:calculations-synopsis}) |
|
973 to compose the result in each case |
|
974 |
|
975 \item solving local claims within the calculation by simplification |
|
976 |
|
977 \end{itemize}% |
|
978 \end{isamarkuptext}% |
|
979 \isamarkuptrue% |
|
980 \isacommand{lemma}\isamarkupfalse% |
|
981 \isanewline |
|
982 \ \ \isakeyword{fixes}\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
983 \ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
984 % |
|
985 \isadelimproof |
|
986 % |
|
987 \endisadelimproof |
|
988 % |
|
989 \isatagproof |
|
990 \isacommand{proof}\isamarkupfalse% |
|
991 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
992 \ \ \isacommand{case}\isamarkupfalse% |
|
993 \ {\isadigit{0}}\isanewline |
|
994 \ \ \isacommand{have}\isamarkupfalse% |
|
995 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
996 \ simp\isanewline |
|
997 \ \ \isacommand{also}\isamarkupfalse% |
|
998 \ \isacommand{have}\isamarkupfalse% |
|
999 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1000 \ simp\isanewline |
|
1001 \ \ \isacommand{finally}\isamarkupfalse% |
|
1002 \ \isacommand{show}\isamarkupfalse% |
|
1003 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1004 \isanewline |
|
1005 \isacommand{next}\isamarkupfalse% |
|
1006 \isanewline |
|
1007 \ \ \isacommand{case}\isamarkupfalse% |
|
1008 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1009 \ \ \isacommand{have}\isamarkupfalse% |
|
1010 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1011 \ simp\isanewline |
|
1012 \ \ \isacommand{also}\isamarkupfalse% |
|
1013 \ \isacommand{have}\isamarkupfalse% |
|
1014 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1015 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{2E}{\isachardot}}hyps{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1016 \ \ \isacommand{also}\isamarkupfalse% |
|
1017 \ \isacommand{have}\isamarkupfalse% |
|
1018 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1019 \ simp\isanewline |
|
1020 \ \ \isacommand{also}\isamarkupfalse% |
|
1021 \ \isacommand{have}\isamarkupfalse% |
|
1022 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
1023 \ simp\isanewline |
|
1024 \ \ \isacommand{finally}\isamarkupfalse% |
|
1025 \ \isacommand{show}\isamarkupfalse% |
|
1026 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
1027 \isanewline |
|
1028 \isacommand{qed}\isamarkupfalse% |
|
1029 % |
|
1030 \endisatagproof |
|
1031 {\isafoldproof}% |
|
1032 % |
|
1033 \isadelimproof |
|
1034 % |
|
1035 \endisadelimproof |
|
1036 % |
|
1037 \begin{isamarkuptext}% |
|
1038 This demonstrates how induction proofs can be done without |
|
1039 having to consider the raw Natural Deduction structure.% |
|
1040 \end{isamarkuptext}% |
|
1041 \isamarkuptrue% |
|
1042 % |
|
1043 \isamarkupsubsection{Induction with local parameters and premises% |
|
1044 } |
|
1045 \isamarkuptrue% |
|
1046 % |
|
1047 \begin{isamarkuptext}% |
|
1048 Idea: Pure rule statements are passed through the induction |
|
1049 rule. This achieves convenient proof patterns, thanks to some |
|
1050 internal trickery in the \hyperlink{method.induct}{\mbox{\isa{induct}}} method. |
|
1051 |
|
1052 Important: Using compact HOL formulae with \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} is a |
|
1053 well-known anti-pattern! It would produce useless formal noise.% |
|
1054 \end{isamarkuptext}% |
|
1055 \isamarkuptrue% |
|
1056 \isacommand{notepad}\isamarkupfalse% |
|
1057 \isanewline |
|
1058 \isakeyword{begin}\isanewline |
|
1059 % |
|
1060 \isadelimproof |
|
1061 \ \ % |
|
1062 \endisadelimproof |
|
1063 % |
|
1064 \isatagproof |
|
1065 \isacommand{fix}\isamarkupfalse% |
|
1066 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
1067 \ \ \isacommand{fix}\isamarkupfalse% |
|
1068 \ P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1069 \ \ \isacommand{fix}\isamarkupfalse% |
|
1070 \ Q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1071 \isanewline |
|
1072 \ \ \isacommand{have}\isamarkupfalse% |
|
1073 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1074 \ \ \isacommand{proof}\isamarkupfalse% |
|
1075 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1076 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1077 \ {\isadigit{0}}\isanewline |
|
1078 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1079 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1080 \isanewline |
|
1081 \ \ \isacommand{next}\isamarkupfalse% |
|
1082 \isanewline |
|
1083 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1084 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1085 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
1086 \ {\isaliteral{60}{\isacharbackquoteopen}}P\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% |
|
1087 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1088 \isanewline |
|
1089 \ \ \isacommand{qed}\isamarkupfalse% |
|
1090 \isanewline |
|
1091 \isanewline |
|
1092 \ \ \isacommand{have}\isamarkupfalse% |
|
1093 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1094 \ \ \isacommand{proof}\isamarkupfalse% |
|
1095 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1096 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1097 \ {\isadigit{0}}\isanewline |
|
1098 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
1099 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% |
|
1100 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1101 \isanewline |
|
1102 \ \ \isacommand{next}\isamarkupfalse% |
|
1103 \isanewline |
|
1104 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1105 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1106 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
1107 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1108 \ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% |
|
1109 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1110 \isanewline |
|
1111 \ \ \isacommand{qed}\isamarkupfalse% |
|
1112 \isanewline |
|
1113 \isanewline |
|
1114 \ \ \isacommand{have}\isamarkupfalse% |
|
1115 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1116 \ \ \isacommand{proof}\isamarkupfalse% |
|
1117 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1118 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1119 \ {\isadigit{0}}\isanewline |
|
1120 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1121 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1122 \isanewline |
|
1123 \ \ \isacommand{next}\isamarkupfalse% |
|
1124 \isanewline |
|
1125 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1126 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1127 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
1128 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% |
|
1129 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1130 % |
|
1131 \begin{isamarkuptxt}% |
|
1132 Local quantification admits arbitrary instances:% |
|
1133 \end{isamarkuptxt}% |
|
1134 \isamarkuptrue% |
|
1135 \ \ \ \ \isacommand{note}\isamarkupfalse% |
|
1136 \ {\isaliteral{60}{\isacharbackquoteopen}}Q\ a\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}Q\ b\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1137 \ \ \isacommand{qed}\isamarkupfalse% |
|
1138 % |
|
1139 \endisatagproof |
|
1140 {\isafoldproof}% |
|
1141 % |
|
1142 \isadelimproof |
|
1143 \isanewline |
|
1144 % |
|
1145 \endisadelimproof |
|
1146 \isacommand{end}\isamarkupfalse% |
|
1147 % |
|
1148 \isamarkupsubsection{Implicit induction context% |
|
1149 } |
|
1150 \isamarkuptrue% |
|
1151 % |
|
1152 \begin{isamarkuptext}% |
|
1153 The \hyperlink{method.induct}{\mbox{\isa{induct}}} method can isolate local parameters and |
|
1154 premises directly from the given statement. This is convenient in |
|
1155 practical applications, but requires some understanding of what is |
|
1156 going on internally (as explained above).% |
|
1157 \end{isamarkuptext}% |
|
1158 \isamarkuptrue% |
|
1159 \isacommand{notepad}\isamarkupfalse% |
|
1160 \isanewline |
|
1161 \isakeyword{begin}\isanewline |
|
1162 % |
|
1163 \isadelimproof |
|
1164 \ \ % |
|
1165 \endisadelimproof |
|
1166 % |
|
1167 \isatagproof |
|
1168 \isacommand{fix}\isamarkupfalse% |
|
1169 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
1170 \ \ \isacommand{fix}\isamarkupfalse% |
|
1171 \ Q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1172 \isanewline |
|
1173 \ \ \isacommand{fix}\isamarkupfalse% |
|
1174 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
1175 \ \ \isacommand{assume}\isamarkupfalse% |
|
1176 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1177 \ \ \isacommand{then}\isamarkupfalse% |
|
1178 \ \isacommand{have}\isamarkupfalse% |
|
1179 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1180 \ \ \isacommand{proof}\isamarkupfalse% |
|
1181 \ {\isaliteral{28}{\isacharparenleft}}induct\ n\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1182 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1183 \ {\isadigit{0}}\isanewline |
|
1184 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
1185 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% |
|
1186 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1187 \isanewline |
|
1188 \ \ \isacommand{next}\isamarkupfalse% |
|
1189 \isanewline |
|
1190 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1191 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1192 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
1193 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \ % |
|
1194 \isamarkupcmt{arbitrary instances can be produced here% |
|
1195 } |
|
1196 \isanewline |
|
1197 \ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% |
|
1198 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1199 \isanewline |
|
1200 \ \ \isacommand{qed}\isamarkupfalse% |
|
1201 % |
|
1202 \endisatagproof |
|
1203 {\isafoldproof}% |
|
1204 % |
|
1205 \isadelimproof |
|
1206 \isanewline |
|
1207 % |
|
1208 \endisadelimproof |
|
1209 \isacommand{end}\isamarkupfalse% |
|
1210 % |
|
1211 \isamarkupsubsection{Advanced induction with term definitions% |
|
1212 } |
|
1213 \isamarkuptrue% |
|
1214 % |
|
1215 \begin{isamarkuptext}% |
|
1216 Induction over subexpressions of a certain shape are delicate |
|
1217 to formalize. The Isar \hyperlink{method.induct}{\mbox{\isa{induct}}} method provides |
|
1218 infrastructure for this. |
|
1219 |
|
1220 Idea: sub-expressions of the problem are turned into a defined |
|
1221 induction variable; often accompanied with fixing of auxiliary |
|
1222 parameters in the original expression.% |
|
1223 \end{isamarkuptext}% |
|
1224 \isamarkuptrue% |
|
1225 \isacommand{notepad}\isamarkupfalse% |
|
1226 \isanewline |
|
1227 \isakeyword{begin}\isanewline |
|
1228 % |
|
1229 \isadelimproof |
|
1230 \ \ % |
|
1231 \endisadelimproof |
|
1232 % |
|
1233 \isatagproof |
|
1234 \isacommand{fix}\isamarkupfalse% |
|
1235 \ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1236 \ \ \isacommand{fix}\isamarkupfalse% |
|
1237 \ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1238 \isanewline |
|
1239 \ \ \isacommand{assume}\isamarkupfalse% |
|
1240 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1241 \ \ \isacommand{then}\isamarkupfalse% |
|
1242 \ \isacommand{have}\isamarkupfalse% |
|
1243 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
1244 \ \ \isacommand{proof}\isamarkupfalse% |
|
1245 \ {\isaliteral{28}{\isacharparenleft}}induct\ {\isaliteral{22}{\isachardoublequoteopen}}a\ x{\isaliteral{22}{\isachardoublequoteclose}}\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1246 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1247 \ {\isadigit{0}}\isanewline |
|
1248 \ \ \ \ \isacommand{note}\isamarkupfalse% |
|
1249 \ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1250 \ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1251 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1252 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1253 \isanewline |
|
1254 \ \ \isacommand{next}\isamarkupfalse% |
|
1255 \isanewline |
|
1256 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1257 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1258 \ \ \ \ \isacommand{note}\isamarkupfalse% |
|
1259 \ hyp\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1260 \ \ \ \ \ \ \isakeyword{and}\ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1261 \ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}Suc\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline |
|
1262 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
1263 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% |
|
1264 \isanewline |
|
1265 \ \ \isacommand{qed}\isamarkupfalse% |
|
1266 % |
|
1267 \endisatagproof |
|
1268 {\isafoldproof}% |
|
1269 % |
|
1270 \isadelimproof |
|
1271 \isanewline |
|
1272 % |
|
1273 \endisadelimproof |
|
1274 \isacommand{end}\isamarkupfalse% |
|
1275 % |
|
1276 \isamarkupsection{Structured Natural Deduction \label{sec:natural-deduction-synopsis}% |
847 } |
1277 } |
848 \isamarkuptrue% |
1278 \isamarkuptrue% |
849 % |
1279 % |
850 \isamarkupsubsection{Rule statements% |
1280 \isamarkupsubsection{Rule statements% |
851 } |
1281 } |