# HG changeset patch # User Christian Urban # Date 1255524979 -7200 # Node ID 9e374cd891e1bd8167fb220b68a852f80a531386 # Parent 2f2018927f2a13d2e35c5023c0bb85b13f4d3f5d updated to Isabelle changes diff -r 2f2018927f2a -r 9e374cd891e1 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Wed Oct 14 12:33:38 2009 +0200 +++ b/ProgTutorial/General.thy Wed Oct 14 14:56:19 2009 +0200 @@ -857,6 +857,8 @@ the theorem does not have any meta-variables that would be present if we proved this theorem on the user-level. We will see later on that usually we have to construct meta-variables in theorems explicitly. + + \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}} *} text {* @@ -963,11 +965,11 @@ a meta-equation between the given theorem and the theorem transformed into the object logic. The result is the theorem with object logic connectives. However, in order to completely transform a theorem - such as @{thm [source] list.induct} + such as @{thm [source] list.induct}, which is of the form @{thm [display] list.induct} - we have to first abstract over the variables @{text "?P"} and + we have to first abstract over the meta variables @{text "?P"} and @{text "?list"}. For this we can use the function @{ML_ind forall_intr_vars in Drule}. *} @@ -981,7 +983,7 @@ end*} text {* - For @{thm [source] list.induct} it produces: + For the theorem @{thm [source] list.induct}, this function produces: @{ML_response_fake [display, gray] "atomize_thm @{thm list.induct}" @@ -989,7 +991,7 @@ Theorems can also be produced from terms by giving an explicit proof. One way to achive this is by using the function @{ML_ind prove in Goal}. - For example + For example below we prove the term @{term "P \ P"}. @{ML_response_fake [display,gray] "let @@ -1002,8 +1004,9 @@ This function takes as second argument a list of strings. This list specifies which variables should be turned into meta-variables once the term is proved. - The proof is given in form of a tactic. We explain tactics in - Chapter~\ref{chp:tactical}. + The proof is given in form of a tactic as last argument. We explain tactics in + Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem + by assumption. Theorems also contain auxiliary data, such their names and kind, but also names for cases etc. This data is stored in a string-string list and can @@ -1020,7 +1023,8 @@ "Thm.get_tags @{thm foo_data}" "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"} - We can extend the data associated with this lemma by attaching case names. + When we store lemmas in the theorem database, we can explicitly extend the data + associated with this lemma by attaching case names. *} local_setup %gray {* @@ -1030,22 +1034,42 @@ @{thm foo_data})]) #> snd *} text {* - The date of the theorem @{thm [source] foo_data'} is as follows: + The data of the theorem @{thm [source] foo_data'} is then as follows: @{ML_response_fake [display,gray] "Thm.get_tags @{thm foo_data'}" "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), (\"case_names\", \"foo_case1;foo_case2\")]"} + + You notice the difference when using the proof methods @{ML_text cases} + or @{ML_text induct}. In the proof below *} lemma "Q \ Q \ Q" -proof (induct rule: foo_data') +proof (cases rule: foo_data') +print_cases +(*<*)oops(*>*) + +text {* + we can proceed by analysing the cases @{ML_text "foo_case1"} and + @{ML_text "foo_case2"}. While if the theorem has no names, then + the cases have standard names @{ML_text 1}, @{ML_text 2} and so + on. This can be seen in the proof below. +*} + +lemma + "Q \ Q \ Q" +proof (cases rule: foo_data) +print_cases (*<*)oops(*>*) text {* TBD below + One great feature of Isabelle is its document preparation system where + proved theorems can be quoted in the text directly from the formalisation. + (FIXME: example for how to add theorem styles) *} @@ -1068,11 +1092,12 @@ strip_assums_all ([], @{term "\x y. A x y"}) *} +(* setup %gray {* TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #> TermStyle.add_style "no_all_prem2" (style_parm_premise 2) *} - +*) lemma shows "A \ B" and "C \ D" @@ -1376,14 +1401,6 @@ section {* Local Theories (TBD) *} -section {* Storing Theorems\label{sec:storing} (TBD) *} - -text {* @{ML_ind add_thms_dynamic in PureThy} *} - -local_setup %gray {* - LocalTheory.note Thm.theoremK - ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *} - (* setup {* @@ -1738,5 +1755,15 @@ section {* Managing Name Spaces (TBD) *} +section {* Summary *} + +text {* + \begin{conventions} + \begin{itemize} + \item Start with a proper context and then pass it around + through all your functions. + \end{itemize} + \end{conventions} +*} end diff -r 2f2018927f2a -r 9e374cd891e1 ProgTutorial/Recipes/ExternalSolver.thy --- a/ProgTutorial/Recipes/ExternalSolver.thy Wed Oct 14 12:33:38 2009 +0200 +++ b/ProgTutorial/Recipes/ExternalSolver.thy Wed Oct 14 14:56:19 2009 +0200 @@ -27,12 +27,10 @@ properly. For example, the following expression takes only approximately one second: - @{ML_response [display,gray] + @{ML_response_fake [display,gray] "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\" handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"} -*} -text {* The function @{ML system_out} can also be used for more reasonable applications, e.g. coupling external solvers with Isabelle. In that case, one has to make sure that Isabelle can find the particular executable. diff -r 2f2018927f2a -r 9e374cd891e1 progtutorial.pdf Binary file progtutorial.pdf has changed