849 |
851 |
850 |
852 |
851 subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close> |
853 subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close> |
852 |
854 |
853 text \<open> |
855 text \<open> |
854 The Isar provides separate commands to accommodate tactic-style |
|
855 proof scripts within the same system. While being outside the |
|
856 orthodox Isar proof language, these might come in handy for |
|
857 interactive exploration and debugging, or even actual tactical proof |
|
858 within new-style theories (to benefit from document preparation, for |
|
859 example). See also \secref{sec:tactics} for actual tactics, that |
|
860 have been encapsulated as proof methods. Proper proof methods may |
|
861 be used in scripts, too. |
|
862 |
|
863 \begin{matharray}{rcl} |
856 \begin{matharray}{rcl} |
864 @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\ |
857 @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\ |
865 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\ |
858 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\ |
866 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\ |
859 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\ |
867 @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\ |
860 @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\ |
868 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\ |
861 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\ |
869 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\ |
862 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\ |
870 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\ |
863 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\ |
871 \end{matharray} |
864 \end{matharray} |
|
865 |
|
866 The Isar language provides separate commands to accommodate tactic-style |
|
867 proof scripts within the same system. While being outside the |
|
868 orthodox Isar proof language, these might come in handy for |
|
869 interactive exploration and debugging, or even actual tactical proof |
|
870 within new-style theories (to benefit from document preparation, for |
|
871 example). See also \secref{sec:tactics} for actual tactics, that |
|
872 have been encapsulated as proof methods. Proper proof methods may |
|
873 be used in scripts, too. |
872 |
874 |
873 @{rail \<open> |
875 @{rail \<open> |
874 @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and') |
876 @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and') |
875 ; |
877 ; |
876 ( @@{command apply} | @@{command apply_end} ) @{syntax method} |
878 ( @@{command apply} | @@{command apply_end} ) @{syntax method} |
975 SIMPLE_METHOD' (fn i: int => no_tac))\<close> |
977 SIMPLE_METHOD' (fn i: int => no_tac))\<close> |
976 "my third method (with theorem arguments and context)" |
978 "my third method (with theorem arguments and context)" |
977 (*<*)end(*>*) |
979 (*<*)end(*>*) |
978 |
980 |
979 |
981 |
980 section \<open>Generalized elimination \label{sec:obtain}\<close> |
982 section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close> |
981 |
983 |
982 text \<open> |
984 text \<open> |
983 \begin{matharray}{rcl} |
985 \begin{matharray}{rcl} |
|
986 @{command_def "consider"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
984 @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
987 @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
985 @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
988 @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
986 \end{matharray} |
989 \end{matharray} |
987 |
990 |
988 Generalized elimination means that additional elements with certain |
991 Generalized elimination means that hypothetical parameters and premises |
989 properties may be introduced in the current context, by virtue of a |
992 may be introduced in the current context, potentially with a split into |
990 locally proven ``soundness statement''. Technically speaking, the |
993 cases. This works by virtue of a locally proven rule that establishes the |
991 @{command "obtain"} language element is like a declaration of |
994 soundness of this temporary context extension. As representative examples, |
992 @{command "fix"} and @{command "assume"} (see also see |
995 one may think of standard rules from Isabelle/HOL like this: |
993 \secref{sec:proof-context}), together with a soundness proof of its |
996 |
994 additional claim. According to the nature of existential reasoning, |
997 \medskip |
995 assumptions get eliminated from any result exported from the context |
998 \begin{tabular}{ll} |
996 later, provided that the corresponding parameters do \emph{not} |
999 @{text "\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\ |
997 occur in the conclusion. |
1000 @{text "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\ |
|
1001 @{text "A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\ |
|
1002 \end{tabular} |
|
1003 \medskip |
|
1004 |
|
1005 In general, these particular rules and connectives need to get involved at |
|
1006 all: this concept works directly in Isabelle/Pure via Isar commands |
|
1007 defined below. In particular, the logic of elimination and case splitting |
|
1008 is delegated to an Isar proof, which often involves automated tools. |
998 |
1009 |
999 @{rail \<open> |
1010 @{rail \<open> |
|
1011 @@{command consider} @{syntax obtain_clauses} |
|
1012 ; |
1000 @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') |
1013 @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') |
1001 @'where' (@{syntax props} + @'and') |
1014 @'where' (@{syntax props} + @'and') |
1002 ; |
1015 ; |
1003 @@{command guess} (@{syntax vars} + @'and') |
1016 @@{command guess} (@{syntax "fixes"} + @'and') |
1004 \<close>} |
1017 \<close>} |
1005 |
1018 |
1006 The derived Isar command @{command "obtain"} is defined as follows |
1019 \begin{description} |
1007 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional) |
1020 |
1008 facts indicated for forward chaining). |
1021 \item @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x |
|
1022 | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} states a rule for case |
|
1023 splitting into separate subgoals, such that each case involves new |
|
1024 parameters and premises. After the proof is finished, the resulting rule |
|
1025 may be used directly with the @{method cases} proof method |
|
1026 (\secref{sec:cases-induct}), in order to perform actual case-splitting of |
|
1027 the proof text via @{command case} and @{command next} as usual. |
|
1028 |
|
1029 Optional names in round parentheses refer to case names: in the proof of |
|
1030 the rule this is a fact name, in the resulting rule it is used as |
|
1031 annotation with the @{attribute_ref case_names} attribute. |
|
1032 |
|
1033 \medskip Formally, the command @{command consider} is defined as derived |
|
1034 Isar language element as follows: |
|
1035 |
1009 \begin{matharray}{l} |
1036 \begin{matharray}{l} |
1010 @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex] |
1037 @{command "consider"}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>"} \\[1ex] |
1011 \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\ |
1038 \quad @{command "have"}~@{text "[case_names a b \<dots>]: thesis"} \\ |
1012 \quad @{command "proof"}~@{method succeed} \\ |
1039 \qquad @{text "\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\ |
1013 \qquad @{command "fix"}~@{text thesis} \\ |
1040 \qquad @{text "\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis"} \\ |
1014 \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\ |
1041 \qquad @{text "\<AND> \<dots>"} \\ |
1015 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\ |
1042 \qquad @{text "\<FOR> thesis"} \\ |
1016 \quad\qquad @{command "apply"}~@{text -} \\ |
1043 \qquad @{command "apply"}~@{text "(insert a b \<dots>)"} \\ |
1017 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\ |
1044 \end{matharray} |
1018 \quad @{command "qed"} \\ |
1045 |
1019 \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\ |
1046 See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal |
1020 \end{matharray} |
1047 statements, as well as @{command print_statement} to print existing rules |
1021 |
1048 in a similar format. |
1022 Typically, the soundness proof is relatively straight-forward, often |
1049 |
1023 just by canonical automated tools such as ``@{command "by"}~@{text |
1050 \item @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"} |
1024 simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the |
1051 states a generalized elimination rule with exactly one case. After the |
1025 ``@{text that}'' reduction above is declared as simplification and |
1052 proof is finished, it is activated for the subsequent proof text: the |
1026 introduction rule. |
1053 context is augmented via @{command fix}~@{text "\<^vec>x"} @{command |
1027 |
1054 assume}~@{text "\<^vec>A \<^vec>x"}, with special provisions to export |
1028 In a sense, @{command "obtain"} represents at the level of Isar |
1055 later results by discharging these assumptions again. |
1029 proofs what would be meta-logical existential quantifiers and |
1056 |
1030 conjunctions. This concept has a broad range of useful |
1057 Note that according to the parameter scopes within the elimination rule, |
1031 applications, ranging from plain elimination (or introduction) of |
1058 results \emph{must not} refer to hypothetical parameters; otherwise the |
1032 object-level existential and conjunctions, to elimination over |
1059 export will fail! This restriction conforms to the usual manner of |
1033 results of symbolic evaluation of recursive definitions, for |
1060 existential reasoning in Natural Deduction. |
1034 example. Also note that @{command "obtain"} without parameters acts |
1061 |
1035 much like @{command "have"}, where the result is treated as a |
1062 \medskip Formally, the command @{command obtain} is defined as derived |
1036 genuine assumption. |
1063 Isar language element as follows, using an instrumented variant of |
1037 |
1064 @{command assume}: |
1038 An alternative name to be used instead of ``@{text that}'' above may |
1065 |
1039 be given in parentheses. |
1066 \begin{matharray}{l} |
1040 |
1067 @{command "obtain"}~@{text "\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>"} \\[1ex] |
1041 \medskip The improper variant @{command "guess"} is similar to |
1068 \quad @{command "have"}~@{text "thesis"} \\ |
1042 @{command "obtain"}, but derives the obtained statement from the |
1069 \qquad @{text "\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\ |
1043 course of reasoning! The proof starts with a fixed goal @{text |
1070 \qquad @{text "\<FOR> thesis"} \\ |
1044 thesis}. The subsequent proof may refine this to anything of the |
1071 \qquad @{command "apply"}~@{text "(insert that)"} \\ |
1045 form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> |
1072 \qquad @{text "\<langle>proof\<rangle>"} \\ |
1046 \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The |
1073 \quad @{command "fix"}~@{text "\<^vec>x"}~@{command "assume"}@{text "\<^sup>* a: \<^vec>A \<^vec>x"} \\ |
1047 final goal state is then used as reduction rule for the obtain |
1074 \end{matharray} |
1048 scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>, |
1075 |
1049 x\<^sub>m"} are marked as internal by default, which prevents the |
1076 \item @{command guess} is similar to @{command obtain}, but it derives the |
1050 proof context from being polluted by ad-hoc variables. The variable |
1077 obtained context elements from the course of tactical reasoning in the |
1051 names and type constraints given as arguments for @{command "guess"} |
1078 proof. Thus it can considerably obscure the proof: it is classified as |
1052 specify a prefix of obtained parameters explicitly in the text. |
1079 \emph{improper}. |
1053 |
1080 |
1054 It is important to note that the facts introduced by @{command |
1081 A proof with @{command guess} starts with a fixed goal @{text thesis}. The |
1055 "obtain"} and @{command "guess"} may not be polymorphic: any |
1082 subsequent refinement steps may turn this to anything of the form @{text |
1056 type-variables occurring here are fixed in the present context! |
1083 "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"}, but without splitting into new |
|
1084 subgoals. The final goal state is then used as reduction rule for the |
|
1085 obtain pattern described above. Obtained parameters @{text "\<^vec>x"} are |
|
1086 marked as internal by default, and thus inaccessible in the proof text. |
|
1087 The variable names and type constraints given as arguments for @{command |
|
1088 "guess"} specify a prefix of accessible parameters. |
|
1089 |
|
1090 \end{description} |
|
1091 |
|
1092 In the proof of @{command consider} and @{command obtain} the local |
|
1093 premises are always bound to the fact name ``@{text that}'', according to |
|
1094 structured Isar statements involving @{keyword_ref "if"} |
|
1095 (\secref{sec:goals}). |
|
1096 |
|
1097 Facts that are established by @{command "obtain"} and @{command "guess"} |
|
1098 may not be polymorphic: any type-variables occurring here are fixed in the |
|
1099 present context. This is a natural consequence of the role of @{command |
|
1100 fix} and @{command assume} in these constructs. |
1057 \<close> |
1101 \<close> |
1058 |
1102 |
1059 |
1103 |
1060 section \<open>Calculational reasoning \label{sec:calculation}\<close> |
1104 section \<open>Calculational reasoning \label{sec:calculation}\<close> |
1061 |
1105 |