54   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the

    54   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the

    55   assumptions @{text As} (happens to be empty) with the variables

    55   assumptions @{text As} (happens to be empty) with the variables

    56   @{text xs} that will be generalised once the goal is proved (in our case

    56   @{text xs} that will be generalised once the goal is proved (in our case

    57   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;

    57   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;

    58   it can make use of the local assumptions (there are none in this example). 

    58   it can make use of the local assumptions (there are none in this example). 

    60   @{text erule}, @{text rule} and @{text assumption}, respectively. 

    60   @{text erule}, @{text rule} and @{text assumption}, respectively. 

    61   The operator @{ML THEN} strings the tactics together. 

    61   The operator @{ML THEN} strings the tactics together. 

    62 

    62 

    63   \begin{readmore}

    63   \begin{readmore}

    64   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}

    64   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}

    66   "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic

    66   "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic

    67   tactics and tactic combinators; see also Chapters 3 and 4 in the old

    67   tactics and tactic combinators; see also Chapters 3 and 4 in the old

    68   Isabelle Reference Manual.

    68   Isabelle Reference Manual.

    69   \end{readmore}

    69   \end{readmore}

    70 

    70 

    72   also have ML-bindings with the same name. Therefore, we could also just have

    72   also have ML-bindings with the same name. Therefore, we could also just have

    73   written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain

    73   written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain

    74   the theorem dynamically using the function @{ML thm}; for example 

    74   the theorem dynamically using the function @{ML thm}; for example 

    75   \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! 

    75   \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! 

    76   The reason

    76   The reason

   307   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are

   307   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are

   308   the subgoals. So after setting up the lemma, the goal state is always of the

   308   the subgoals. So after setting up the lemma, the goal state is always of the

   309   form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text

   309   form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text

   310   "(C)"}. Since the goal @{term C} can potentially be an implication, there is

   310   "(C)"}. Since the goal @{term C} can potentially be an implication, there is

   311   a ``protector'' wrapped around it (in from of an outermost constant @{text

   311   a ``protector'' wrapped around it (in from of an outermost constant @{text

   313   is invisible in the figure). This prevents that premises of @{text C} are

   313   is invisible in the figure). This prevents that premises of @{text C} are

   314   mis-interpreted as open subgoals. While tactics can operate on the subgoals

   314   mis-interpreted as open subgoals. While tactics can operate on the subgoals

   315   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion

   315   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion

   316   @{term C} intact, with the exception of possibly instantiating schematic

   316   @{term C} intact, with the exception of possibly instantiating schematic

   317   variables. If you use the predefined tactics, which we describe in the next

   317   variables. If you use the predefined tactics, which we describe in the next

   950       \end{minipage} *}

   950       \end{minipage} *}

   951 (*<*)oops(*>*)

   951 (*<*)oops(*>*)

   952 

   952 

   953 text {*

   953 text {*

   954   is completely analysed according to the theorems we chose to

   954   is completely analysed according to the theorems we chose to

   956 

   956 

   957   Recall that tactics produce a lazy sequence of successor goal states. These

   957   Recall that tactics produce a lazy sequence of successor goal states. These

   958   states can be explored using the command \isacommand{back}. For example

   958   states can be explored using the command \isacommand{back}. For example

   959 

   959 

   960 *}

   960 *}

  1013 

  1013 

  1014 section {* Rewriting and Simplifier Tactics *}

  1014 section {* Rewriting and Simplifier Tactics *}

  1015 

  1015 

  1016 text {*

  1016 text {*

  1017   @{ML rewrite_goals_tac}

  1017   @{ML rewrite_goals_tac}

  1018   @{ML ObjectLogic.full_atomize_tac}

  1019   @{ML ObjectLogic.full_atomize_tac}

  1019   @{ML ObjectLogic.rulify_tac}

  1021   @{ML ObjectLogic.rulify_tac}

  1020 *}

  1025 *}

  1021 

  1026 

  1022 

  1027 

  1023 section {* Structured Proofs *}

  1028 section {* Structured Proofs *}

  1024 

  1029