# HG changeset patch # User Christian Urban # Date 1282489012 -28800 # Node ID 957f69b9b7df784a69c10fd1d81ed4a11ac0c7e5 # Parent d21cea8e0bcf16e757530f4cb2db65f16465c7f9 added something about Goal.prove_multi diff -r d21cea8e0bcf -r 957f69b9b7df ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Fri Aug 13 18:52:16 2010 +0800 +++ b/ProgTutorial/Essential.thy Sun Aug 22 22:56:52 2010 +0800 @@ -150,8 +150,8 @@ @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \) $ Free (\"x\", \), - Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} - + Const (\"HOL.Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} + where a coercion is inserted in the second component and @{ML_response [display,gray] "(@{term \"P x \ Q x\"}, @{prop \"P x \ Q x\"})" @@ -227,7 +227,7 @@ @{ML_response [display,gray] "@{typ \"bool\"}" - "Type (\"bool\", [])"} + "Type (\"HOL.bool\", [])"} When printing out a list-type @@ -244,7 +244,7 @@ @{ML_response [display,gray] "@{typ \"bool \ nat\"}" - "Type (\"fun\", [Type (\"bool\", []), Type (\"Nat.nat\", [])])"} + "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"} We can restore the usual behaviour of Isabelle's pretty printer with the code @@ -496,13 +496,13 @@ for this function is *} -ML{*fun is_all (Const ("All", _) $ _) = true +ML{*fun is_all (Const ("HOL.All", _) $ _) = true | is_all _ = false*} text {* because now -@{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "true"} + @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "true"} matches correctly (the first wildcard in the pattern matches any type and the second any term). @@ -721,9 +721,9 @@ \begin{isabelle}*} ML{*fun pretty_helper aux env = env |> Vartab.dest - |> map ((fn (s1, s2) => Pretty.block [s1, Pretty.str ";=", s2]) o aux) - |> Pretty.commas - |> Pretty.enum "" "[" "]" + |> map aux + |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) + |> Pretty.enum "," "[" "]" |> pwriteln fun pretty_tyenv ctxt tyenv = @@ -978,7 +978,7 @@ text {* Unification of abstractions is more thoroughly studied in the context of higher-order pattern unification and higher-order pattern matching. A - \emph{\index*{pattern}} is a well-formed beta-normal term in which the arguments to + \emph{\index*{pattern}} is a well-formed term in which the arguments to every schematic variable are distinct bounds. In particular this excludes terms where a schematic variable is an argument of another one and where a schematic @@ -1741,7 +1741,7 @@ Theorems can also be produced from terms by giving an explicit proof. One way to achieve this is by using the function @{ML_ind prove in Goal} in the structure @{ML_struct Goal}. For example below we use this function - to prove the term @{term "P \ P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?} + to prove the term @{term "P \ P"}. @{ML_response_fake [display,gray] "let @@ -1754,12 +1754,45 @@ This function takes first a context and second a list of strings. This list specifies which variables should be turned into schematic 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. As before this code will produce a theorem, but the theorem - is not yet stored in the theorem database. - + is proved (in this case only @{text "\"P\""}). 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. + + There is also the possibility of proving multiple goals at the same time + using the function @{ML_ind prove_multi in Goal}. For this let us define the + following three helper functions. +*} + +ML{*fun rep_goals i = replicate i @{prop "f x = f x"} +fun rep_tacs i = replicate i (rtac @{thm refl}) + +fun multi_test ctxt i = + Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i) + (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*} + +text {* + With them we can now produce three theorem instances of the + proposition. + + @{ML_response_fake [display, gray] + "multi_test @{context} 3" + "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"} + + However you should be careful with @{ML prove_multi in Goal} and very + large goals. If you increase the counter in the code above to @{text 3000}, + you will notice that takes approximately ten(!) times longer than + using @{ML map} and @{ML prove in Goal}. +*} + +ML{*let + fun test_prove ctxt thm = + Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1)) +in + map (test_prove @{context}) (rep_goals 3000) +end*} + +text {* While the LCF-approach of going through interfaces ensures soundness in Isabelle, there is the function @{ML_ind make_thm in Skip_Proof} in the structure @{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem. diff -r d21cea8e0bcf -r 957f69b9b7df ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Fri Aug 13 18:52:16 2010 +0800 +++ b/ProgTutorial/Package/Ind_Code.thy Sun Aug 22 22:56:52 2010 +0800 @@ -596,8 +596,10 @@ Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] in pps |> Pretty.chunks - |> pwriteln + |> Pretty.string_of + |> tracing end*} + text_raw{* \end{isabelle} \end{minipage} @@ -788,6 +790,7 @@ of the accessible part is such a rule. *} + lemma accpartI: shows "\R x. (\y. R y x \ accpart R y) \ accpart R x" apply(tactic {* expand_tac @{thms accpart_def} *}) diff -r d21cea8e0bcf -r 957f69b9b7df ProgTutorial/Recipes/CallML.thy --- a/ProgTutorial/Recipes/CallML.thy Fri Aug 13 18:52:16 2010 +0800 +++ b/ProgTutorial/Recipes/CallML.thy Sun Aug 22 22:56:52 2010 +0800 @@ -72,7 +72,7 @@ @{text 4} is not prime: *} -lemma "\ prime(4::nat)" +lemma "\ prime (4::nat)" apply(rule factor_non_prime) apply eval done diff -r d21cea8e0bcf -r 957f69b9b7df progtutorial.pdf Binary file progtutorial.pdf has changed