# HG changeset patch # User Christian Urban # Date 1288346437 -3600 # Node ID fc074e669f9f50e2d2779dbd808092c8358b2e89 # Parent 102dc5cc1aed2616dca5a9c4f9c518fb99309243 disabled foobar_prove; updated to new Isabelle diff -r 102dc5cc1aed -r fc074e669f9f ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sat Aug 28 13:37:25 2010 +0800 +++ b/ProgTutorial/Essential.thy Fri Oct 29 11:00:37 2010 +0100 @@ -38,7 +38,7 @@ @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" -"Const (\"op =\", \) $ +"Const (\"HOL.eq\", \) $ (Const (\"Groups.plus_class.plus\", \) $ \ $ \) $ \"} constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using @@ -1092,10 +1092,10 @@ also tries first to solve the problem by higher-order pattern unification. Only in case of failure full higher-order unification is called. This function has a built-in bound, which can be accessed and - manipulated as a configuration value: + manipulated as a configuration value. For example @{ML_response_fake [display,gray] - "Config.get_global @{theory} (Unify.search_bound_value)" + "Config.get_global @{theory} (Unify.search_bound)" "Int 60"} If this bound is reached during unification, Isabelle prints out the @@ -1538,7 +1538,7 @@ also a bit too restrictive in cases where a theorem name should refer to a dynamically expanding list of theorems (like a simpset). Therefore Isabelle also implements a mechanism where a theorem name can refer to a custom theorem - list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. + list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}. To see how it works let us assume we defined our own theorem list @{text MyThmList}. *} @@ -1560,11 +1560,11 @@ text {* We can now install the theorem list so that it is visible to the user and can be refered to by a theorem name. For this need to call - @{ML_ind add_thms_dynamic in PureThy} + @{ML_ind add_thms_dynamic in Global_Theory} *} setup %gray {* - PureThy.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) + Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) *} text {* diff -r 102dc5cc1aed -r fc074e669f9f ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Sat Aug 28 13:37:25 2010 +0800 +++ b/ProgTutorial/First_Steps.thy Fri Oct 29 11:00:37 2010 +0100 @@ -259,17 +259,17 @@ text {* You can also print out terms together with their typing information. - For this you need to set the reference @{ML_ind show_types in Syntax} - to @{ML true}. + For this you need to set the configuration value + @{ML_ind show_types in Syntax} to @{ML true}. *} -ML{*show_types := true*} +ML{*val show_types_ctxt = Config.put show_types true @{context}*} text {* - Now @{ML pretty_term} prints out + Now by using this context @{ML pretty_term} prints out @{ML_response_fake [display, gray] - "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})" + "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})" "(1::nat, x::'a)"} where @{text 1} and @{text x} are displayed with their inferred type. @@ -277,19 +277,18 @@ the reference @{ML_ind show_all_types in Syntax} to @{ML true}. In this case we obtain *} -(*<*)ML %linenos {*show_all_types := true*} -(*>*) + text {* @{ML_response_fake [display, gray] - "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})" + "pwriteln (pretty_term + (Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})" "(Pair::nat \ 'a \ nat \ 'a) (1::nat) (x::'a)"} where @{term Pair} is the term-constructor for products. - Other references that influence printing of terms are + Other configuration values that influence printing of terms are @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. *} -(*<*)ML %linenos {*show_types := false; show_all_types := false*} -(*>*) + text {* A @{ML_type cterm} can be printed with the following function. *} diff -r 102dc5cc1aed -r fc074e669f9f ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Sat Aug 28 13:37:25 2010 +0800 +++ b/ProgTutorial/Helper/Command/Command.thy Fri Oct 29 11:00:37 2010 +0100 @@ -40,8 +40,13 @@ *} ML {* -val r = Unsynchronized.ref (NONE:(unit -> term) option) +structure Result = Proof_Data( + type T = unit -> term + fun init thy () = error "Result") + +val result_cookie = (Result.get, Result.put, "Result.put") *} + ML{* let fun after_qed thm_name thms lthy = @@ -49,7 +54,7 @@ fun setup_proof (thm_name, (txt, pos)) lthy = let - val trm = ML_Context.evaluate lthy true ("r", r) txt + val trm = Code_Runtime.value lthy result_cookie ("", txt) in Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy end @@ -63,4 +68,5 @@ + end diff -r 102dc5cc1aed -r fc074e669f9f ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Sat Aug 28 13:37:25 2010 +0800 +++ b/ProgTutorial/Parsing.thy Fri Oct 29 11:00:37 2010 +0100 @@ -802,6 +802,7 @@ for inductive predicates of the form: *} + simple_inductive even and odd where @@ -809,7 +810,6 @@ | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" - text {* For this we are going to use the parser: *} @@ -1202,27 +1202,37 @@ *} -ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*} +ML {* +structure Result = Proof_Data( + type T = unit -> term + fun init thy () = error "Result") + +val result_cookie = (Result.get, Result.put, "Result.put") +*} + ML{*let fun after_qed thm_name thms lthy = Local_Theory.note (thm_name, (flat thms)) lthy |> snd fun setup_proof (thm_name, (txt, pos)) lthy = let - val trm = ML_Context.evaluate lthy true ("r", r) txt + val trm = Code_Runtime.value lthy result_cookie ("", txt) in Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy end val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source + in Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" Keyword.thy_goal (parser >> setup_proof) end*} +(* foobar_prove test: {* @{prop "True"} *} apply(rule TrueI) done +*) (* ML {* diff -r 102dc5cc1aed -r fc074e669f9f ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sat Aug 28 13:37:25 2010 +0800 +++ b/ProgTutorial/Tactical.thy Fri Oct 29 11:00:37 2010 +0100 @@ -39,6 +39,8 @@ apply(assumption) done + + text {* This proof translates to the following ML-code. @@ -79,34 +81,6 @@ Manual. \end{readmore} - Note that in the code above we use antiquotations for referencing the - theorems. We could also just have written @{ML "etac disjE 1"} because - many of the basic theorems have a corresponding ML-binding: - - @{ML_response_fake [gray,display] - "disjE" - "\?P \ ?Q; ?P \ ?R; ?Q \ ?R\ \ ?R"} - - In case where no ML-binding exists, theorems can also be looked up dynamically - using the function @{ML thm} and the (string) name of the theorem. For example: - - @{ML_response_fake [gray,display] - "thm \"disjE\"" - "\?P \ ?Q; ?P \ ?R; ?Q \ ?R\ \ ?R"} - - Both ways however are considered \emph{bad} style! The reason is that the binding - for @{ML disjE} can be re-assigned and thus one does not have - complete control over which theorem is actually applied. Similarly with the - lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name - in the theorem database, the string can stand for a dynamically updatable - theorem list. Also in this case we cannot be sure which theorem is applied. - These problems can be nicely prevented by using antiquotations - - @{ML_response_fake [gray,display] - "@{thm \"disjE\"}" - "\?P \ ?Q; ?P \ ?R; ?Q \ ?R\ \ ?R"} - - because then the theorems are fixed statically at compile-time. \index{tactic@ {\tt\slshape{}tactic}} \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}} @@ -664,39 +638,8 @@ apply(rule TrueI) done - text {* - There is one peculiarity about @{ML FOCUS in Subgoal} and @{ML SUBPROOF}. - If we apply @{text "rtac @{thm allI}"} in the proof below -*} - -lemma - shows "B \ \x. A x" -apply(tactic {* rtac @{thm allI} 1 *}) -txt{* it will produce the expected goal state - @{subgoals [display]} *} -(*<*)oops(*>*) - -text {* But if we apply the same tactic inside @{ML FOCUS in Subgoal} - we obtain -*} - -lemma - shows "B \ \x. A x" -apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *}) -txt{* it will produce the goal state - @{subgoals [display]} - - If we want to imitate the behaviour of the ``plain'' tactic, then we - can apply the tactic @{ML norm_hhf_tac in Goal}. This gives -*} -apply(tactic {* Goal.norm_hhf_tac 1 *}) -txt{*@{subgoals [display]}*} -(*<*)oops(*>*) - -text {* - This tactic transforms the goal state into a \emph{hereditary Harrop normal - form}. To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather + To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather convenient, but can impose a considerable run-time penalty in automatic proofs. If speed is of the essence, then maybe the two lower level combinators described next are more appropriate. diff -r 102dc5cc1aed -r fc074e669f9f progtutorial.pdf Binary file progtutorial.pdf has changed