isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:d21cea8e0bcf
+:957f69b9b7df
 usually invisible @{text "Trueprop"}-coercions whenever necessary.
 Consider for example the pairs
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
-Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
 where a coercion is inserted in the second component and
 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>,
 Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 text {*
 Now the type bool is printed out in full detail.
 @{ML_response [display,gray]
 "@{typ \"bool\"}"
-"Type (\"bool\", [])"}
+"Type (\"HOL.bool\", [])"}
 When printing out a list-type
 @{ML_response [display,gray]
 "@{typ \"'a list\"}"
 theories @{text "HOL"} and @{text "Nat"}, respectively, they are
 still represented by their simple name.
 @{ML_response [display,gray]
 "@{typ \"bool \<Rightarrow> 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
 *}
 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
 an arbitrary, but fixed type @{typ "'a"}. A properly working alternative
 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 \"\<forall>x::nat. P x\"}" "true"}
 matches correctly (the first wildcard in the pattern matches any type and the
 second any term).
 However there is still a problem: consider the similar function that
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}*}
 ML{*fun pretty_helper aux env =
 env |> Vartab.dest
-|> map ((fn (s1, s2) => Pretty.block [s1, Pretty.str ";=", s2]) o aux)
+|> map aux
-|> Pretty.commas
+|> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
-|> Pretty.enum "" "[" "]"
+|> Pretty.enum "," "[" "]"
 |> pwriteln
 fun pretty_tyenv ctxt tyenv =
 let
 fun get_typs (v, (s, T)) = (TVar (v, s), T)
 *}
 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
 variable is applied twice with the same bound variable. The function
 @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 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 \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?}
+to prove the term @{term "P \<Longrightarrow> P"}.
 @{ML_response_fake [display,gray]
 "let
 val trm = @{term \"P \<Longrightarrow> P::bool\"}
 val tac = K (atac 1)
 end"
 "?P \<Longrightarrow> ?P"}
 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
+is proved (in this case only @{text "\"P\""}).  The fourth argument is the term to be
-corresponding proof given in form of a tactic (we explain tactics in
+proved. The fifth is a corresponding proof given in form of a tactic (we explain
-Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem
+tactics in Chapter~\ref{chp:tactical}). In the code above, the tactic proves the
-by assumption. As before this code will produce a theorem, but the theorem
+theorem by assumption.
-is not yet stored in the theorem database.
+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.
 Potentially making the system unsound.  This is sometimes useful for developing
 purposes, or when explicit proof construction should be omitted due to performace

changeset 448	957f69b9b7df
parent 446	4c32349b9875
child 449	f952f2679a11