diff -r f118240ab44a -r 9f12e53eb121 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Sun Oct 18 21:22:44 2009 +0200 +++ b/ProgTutorial/General.thy Mon Oct 19 02:02:21 2009 +0200 @@ -316,9 +316,14 @@ function that strips off the outermost quantifiers in a term. *} -ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) = - strip_alls t |>> cons (Free (n, T)) - | strip_alls t = ([], t) *} +ML{*fun strip_alls t = +let + fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T)) +in + case t of + Const ("All", _) $ Abs body => aux body + | _ => ([], t) +end*} text {* The function returns a pair consisting of the stripped off variables and @@ -343,10 +348,25 @@ end" "x = y"} - Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls} - returned. The reason is that the head of the list the function @{ML subst_bounds} - takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"} - and so on. + Note that in Line 4 we had to reverse the list of variables that @{ML + strip_alls} returned. The reason is that the head of the list the function + @{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next + element for @{ML "Bound 1"} and so on. + + Notice also that this function might introduce name clashes, since we + substitute just a variable with the name recorded in an abstraction. This + name is by no means unique. If clashes need to be avoided, then we should + use the function @{ML_ind dest_abs in Term}, which returns the body where + the lose de Bruijn index is replaced by a unique free variable. For example + + + @{ML_response_fake [display,gray] + "let + val app = Bound 0 $ Free (\"x\", @{typ nat}) +in + Term.dest_abs (\"x\", @{typ \"nat \ bool\"}, app) +end" + "(\"xa\", Free (\"xa\", \"nat \ bool\") $ Free (\"x\", \"nat\"))"} There are also many convenient functions that construct specific HOL-terms in the structure @{ML_struct HOLogic}. For @@ -936,7 +956,7 @@ The simplifier can be used to unfold definition in theorms. To show this we build the theorem @{term "True \ True"} (Line 1) and then - unfold the constant according to its definition (Line 2). + unfold the constant @{term "True"} according to its definition (Line 2). @{ML_response_fake [display,gray,linenos] "Thm.reflexive @{cterm \"True\"} @@ -946,9 +966,12 @@ "(\x. x) = (\x. x) \ (\x. x) = (\x. x)"} Often it is necessary to transform theorems to and from the object - logic. For example, the function @{ML_ind rulify in ObjectLogic} - replaces all @{text "\"} and @{text "\"} into the equivalents of the - meta logic. For example + logic, that is eplacing all @{text "\"} and @{text "\"} with @{text "\"} + and @{text "\"}, respectively. A reason for such transformations is + that definitions can only be stated using object logic connectives, while + theorems using the connectives from the meta logic are more convenient for + reasoning. The function @{ML_ind rulify in ObjectLogic} replaces all + object connectives by equivalents in the meta logic. For example @{ML_response_fake [display, gray] "ObjectLogic.rulify @{thm foo_test2}" @@ -975,8 +998,9 @@ @{thm [display] list.induct} 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}. + @{text "?list"} in the theorem. For this we can use the function + @{ML_ind forall_intr_vars in Drule}. This allows us to implement the + following function for atomizing a theorem. *} ML{*fun atomize_thm thm = @@ -988,15 +1012,16 @@ end*} text {* - For the theorem @{thm [source] list.induct}, this function produces: + This function produces for the theorem @{thm [source] list.induct} @{ML_response_fake [display, gray] "atomize_thm @{thm list.induct}" "\P list. P [] \ (\a list. P list \ P (a # list)) \ P list"} 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 below we prove the term @{term "P \ P"}. + One way to achive this is by using the function @{ML_ind prove in Goal} + in the structure @{ML_struct Goal}. For example below we prove the term + @{term "P \ P"}. @{ML_response_fake [display,gray] "let @@ -1007,35 +1032,37 @@ end" "?P \ ?P"} - 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 as last argument. We explain tactics in - Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem + This function takes first a context and second a list of strings. This list + specifies which variables should be turned into meta-variables once the term + is proved. The fourth argument is the term to be proved. The fifth is a + corresponding proof given in form of a tactic. We explain tactics in + Chapter~\ref{chp:tactical}. In the code above, the tactic proves 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 - be retrieved with the function @{ML_ind get_tags in Thm}. Assume the - following lemma. + Theorems also contain auxiliary data, such as the name of the theorem, its + kind, the names for cases and so on. This data is stored in a string-string + list and can be retrieved with the function @{ML_ind get_tags in + Thm}. Assume the following lemma. *} lemma foo_data: "P \ P \ P" by assumption text {* - The auxiliary data of this lemma is as follows. + So far the the auxiliary data of this lemma is: @{ML_response_fake [display,gray] "Thm.get_tags @{thm foo_data}" "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"} - When we store lemmas in the theorem database, we can explicitly extend the data - associated with this lemma by attaching case names. + When we store lemmas in the theorem database, we may want to explicitly extend + this data by attaching case names to the two premises of the lemma. This can + be achieved with the function @{ML_ind name in RuleCases}. *} local_setup %gray {* LocalTheory.note Thm.lemmaK ((@{binding "foo_data'"}, []), - [(RuleCases.name ["foo_case1", "foo_case2"] + [(RuleCases.name ["foo_case_one", "foo_case_two"] @{thm foo_data})]) #> snd *} text {* @@ -1044,69 +1071,101 @@ @{ML_response_fake [display,gray] "Thm.get_tags @{thm foo_data'}" "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), - (\"case_names\", \"foo_case1;foo_case2\")]"} + (\"case_names\", \"foo_case_one;foo_case_two\")]"} - You notice the difference when using the proof methods @{ML_text cases} - or @{ML_text induct}. In the proof below + You can notice the case names on the user level when using the proof + methods @{ML_text cases} and @{ML_text induct}. In the proof below *} lemma - "Q \ Q \ Q" + shows "Q \ Q \ Q" proof (cases rule: foo_data') -print_cases + (*<*)oops(*>*) +text_raw{* +\begin{tabular}{@ {}l} +\isacommand{print\_cases}\\ +@{text "> cases:"}\\ +@{text "> foo_case_one:"}\\ +@{text "> let \"?case\" = \"?P\""}\\ +@{text "> foo_case_two:"}\\ +@{text "> let \"?case\" = \"?P\""} +\end{tabular}*} 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 + we can proceed by analysing the cases @{text "foo_case1"} and + @{text "foo_case2"}. While if the theorem has no names, then + the cases have standard names @{text 1}, @{text 2} and so on. This can be seen in the proof below. *} lemma - "Q \ Q \ Q" + shows "Q \ Q \ Q" proof (cases rule: foo_data) -print_cases + (*<*)oops(*>*) +text_raw{* +\begin{tabular}{@ {}l} +\isacommand{print\_cases}\\ +@{text "> cases:"}\\ +@{text "> 1:"}\\ +@{text "> let \"?case\" = \"?P\""}\\ +@{text "> 2:"}\\ +@{text "> let \"?case\" = \"?P\""} +\end{tabular}*} + text {* - TBD below - - One great feature of Isabelle is its document preparation system where + 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) + This helps minimises cut-and-paste errors. However, sometimes the verbatim + quoting is not what is wanted. For such situations Isabelle allows the + installation of \emph{styles}. These are, roughly speaking, functions from + terms to terms. The input term stands for the theorem to be presented. + Let us assume we want to display theorems without leading quantifiers. + For this we can implement the following function that strips off + meta-quantifiers. *} -ML {* -fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) = - strip_assums_all ((a, T)::params, t) - | strip_assums_all (params, B) = (params, B) +ML {*fun strip_all (Const (@{const_name "All"}, _) $ Abs body) = + Term.dest_abs body |> snd |> strip_all + | strip_all (Const (@{const_name "Trueprop"}, _) $ t) = strip_all t + | strip_all t = t*} + +ML {* strip_all @{term "\x y z. P x y z"}*} -fun style_parm_premise i ctxt t = - let val prems = Logic.strip_imp_prems t in - if i <= length prems - then let val (params,t) = strip_assums_all([], nth prems (i - 1)) - in subst_bounds(map Free params, t) end - else error ("Not enough premises for prem" ^ string_of_int i ^ - " in propositon: " ^ string_of_term ctxt t) - end; +text {* + Now we can install this function as the theorem style named + @{text "strip_all"}. +*} + +setup %gray {* + Term_Style.setup "strip_all" (Scan.succeed (K strip_all)) +*} + +text {* + We can test the theorem style with the following theorem *} -ML {* -strip_assums_all ([], @{term "\x y. A x y"}) -*} +theorem style_test: + shows "\x y z. (x, x) = (y, z)" sorry + +text {* + Now printing out the theorem @{thm [source] style_test} normally + in a document produces + + @{thm [display] style_test} -(* -setup %gray {* - TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #> - TermStyle.add_style "no_all_prem2" (style_parm_premise 2) + as expected. But with the theorem style @{text "@{thm (strip_all) \}"} + we obtain + + @{thm [display] (strip_all) style_test} + + without the leading quantifiers. Such theorem styles allow one to + print out theorems in documents formatted in any way wanted. Next we + explain theorem attributes, which is another mechanism for treating + theorems. *} -*) -lemma - shows "A \ B" - and "C \ D" -oops section {* Theorem Attributes\label{sec:attributes} *}