# HG changeset patch # User Christian Urban # Date 1319630384 -3600 # Node ID 25371f74c768fa127cd6d519e143a81e34c838a8 # Parent fea1b7ce5c4a9d974300e2b111571ec188a059e8 updated to post-2011-1 Isabelle diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/Advanced.thy Wed Oct 26 12:59:44 2011 +0100 @@ -127,8 +127,8 @@ section {* Contexts (TBD) *} -ML{*ProofContext.debug*} -ML{*ProofContext.verbose*} +ML{*Proof_Context.debug*} +ML{*Proof_Context.verbose*} section {* Local Theories (TBD) *} diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Appendix.thy --- a/ProgTutorial/Appendix.thy Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/Appendix.thy Wed Oct 26 12:59:44 2011 +0100 @@ -21,7 +21,7 @@ \begin{itemize} \item translations/print translations; - @{ML "ProofContext.print_syntax"} + @{ML "Proof_Context.print_syntax"} \item user space type systems (in the form that already exists) diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/Base.thy Wed Oct 26 12:59:44 2011 +0100 @@ -54,7 +54,7 @@ let val pre = implode ["\n", "local_setup ", "{", "*", "\n"] val post = implode ["\n", "*", "}", "\n"] - val _ = write_file (enclose pre post txt) (ProofContext.theory_of lthy) + val _ = write_file (enclose pre post txt) (Proof_Context.theory_of lthy) in lthy end diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/First_Steps.thy Wed Oct 26 12:59:44 2011 +0100 @@ -764,11 +764,11 @@ Another important antiquotation is @{text "@{context}"}. (What the difference between a theory and a context is will be described in Chapter \ref{chp:advanced}.) A context is for example needed in order to use the - function @{ML print_abbrevs in ProofContext} that list of all currently + function @{ML print_abbrevs in Proof_Context} that list of all currently defined abbreviations. @{ML_response_fake [display, gray] - "ProofContext.print_abbrevs @{context}" + "Proof_Context.print_abbrevs @{context}" "Code_Evaluation.valtermify \ \x. (x, \u. Code_Evaluation.termify x) INTER \ INFI Inter \ Inf @@ -857,7 +857,7 @@ val parser = Args.context -- Scan.lift Args.name_source fun term_pat (ctxt, str) = - str |> ProofContext.read_term_pattern ctxt + str |> Proof_Context.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomic in @@ -869,7 +869,7 @@ text {* The parser in Line 2 provides us with a context and a string; this string is transformed into a term using the function @{ML_ind read_term_pattern in - ProofContext} (Line 5); the next two lines transform the term into a string + Proof_Context} (Line 5); the next two lines transform the term into a string so that the ML-system can understand it. (All these functions will be explained in more detail in later sections.) An example for this antiquotation is: diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Wed Oct 26 12:59:44 2011 +0100 @@ -136,7 +136,7 @@ ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy = let - val thy = ProofContext.theory_of lthy + val thy = Proof_Context.theory_of lthy val orules = map (Object_Logic.atomize_term thy) rules val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) in @@ -148,7 +148,7 @@ meta-quanti\-fications. In Line 4, we transform these introduction rules into the object logic (since definitions cannot be stated with meta-connectives). To do this transformation we have to obtain the theory - behind the local theory using the function @{ML_ind theory_of in ProofContext} + behind the local theory using the function @{ML_ind theory_of in Proof_Context} (Line 3); with this theory we can use the function @{ML_ind atomize_term in Object_Logic} to make the transformation (Line 4). The call to @{ML defn_aux} in Line 5 produces all right-hand sides of the @@ -341,7 +341,7 @@ in Goal.prove lthy' [] [prem] goal (fn {prems, ...} => ind_tac defs prems cnewpreds) - |> singleton (ProofContext.export lthy' lthy) + |> singleton (Proof_Context.export lthy' lthy) end *} text {* @@ -405,7 +405,7 @@ val Ps = replicate (length preds) "P" val (newprednames, lthy') = Variable.variant_fixes Ps lthy - val thy = ProofContext.theory_of lthy' + val thy = Proof_Context.theory_of lthy' val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss val newpreds = map Free (newprednames ~~ tyss') @@ -415,7 +415,7 @@ in map (prove_ind lthy' defs srules cnewpreds) (preds ~~ newpreds ~~ arg_tyss) - |> ProofContext.export lthy' lthy + |> Proof_Context.export lthy' lthy end*} text {* diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Package/simple_inductive_package.ML --- a/ProgTutorial/Package/simple_inductive_package.ML Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/Package/simple_inductive_package.ML Wed Oct 26 12:59:44 2011 +0100 @@ -49,7 +49,7 @@ (* @chunk definitions *) fun definitions rules params preds prednames syns arg_typess lthy = let - val thy = ProofContext.theory_of lthy + val thy = Proof_Context.theory_of lthy val orules = map (Object_Logic.atomize_term thy) rules val defs = map (defs_aux lthy orules preds params) (preds ~~ arg_typess) @@ -78,7 +78,7 @@ val Ps = replicate (length preds) "P" val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 - val thy = ProofContext.theory_of lthy3 + val thy = Proof_Context.theory_of lthy3 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss val newpreds = map Free (newprednames ~~ Tss') @@ -97,7 +97,7 @@ in Goal.prove lthy4 [] [prem] goal (fn {prems, ...} => induction_tac defs prems cnewpreds) - |> singleton (ProofContext.export lthy4 lthy1) + |> singleton (Proof_Context.export lthy4 lthy1) end in map prove_induction (preds ~~ newpreds ~~ Tss) @@ -152,7 +152,7 @@ fun prove_intro (i, goal) = Goal.prove lthy2 [] [] goal (fn {context, ...} => introductions_tac defs rules preds i context) - |> singleton (ProofContext.export lthy2 lthy1) + |> singleton (Proof_Context.export lthy2 lthy1) in map_index prove_intro rules end diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/Tactical.thy Wed Oct 26 12:59:44 2011 +0100 @@ -13,6 +13,13 @@ chapter {* Tactical Reasoning\label{chp:tactical} *} text {* + \begin{flushright} + {\em ``The most effective debugging tool is still careful thought, coupled with + judiciously placed print statements.''} \\[1ex] + Brian Kernighan + \end{flushright} + + \medskip One of the main reason for descending to the ML-level of Isabelle is to be able to implement automatic proof procedures. Such proof procedures can considerably lessen the burden of manual reasoning. They are centred around @@ -1581,7 +1588,7 @@ \begin{figure}[p] \begin{boxedminipage}{\textwidth} \begin{isabelle} *} -types prm = "(nat \ nat) list" +type_synonym prm = "(nat \ nat) list" consts perm :: "prm \ 'a \ 'a" ("_ \ _" [80,80] 80) overloading @@ -2472,7 +2479,7 @@ val xs = strip_abs_vars (term_of rhs) val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt - val thy = ProofContext.theory_of ctxt' + val thy = Proof_Context.theory_of ctxt' val cxs = map (cterm_of thy o Free) xs val new_lhs = Drule.list_comb (lhs, cxs) @@ -2480,7 +2487,7 @@ | get_conv (_::xs) = Conv.fun_conv (get_conv xs) in get_conv xs new_lhs |> - singleton (ProofContext.export ctxt' ctxt) + singleton (Proof_Context.export ctxt' ctxt) end*} text {* diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Mon Oct 17 13:30:49 2011 +0100 +++ b/ProgTutorial/antiquote_setup.ML Wed Oct 26 12:59:44 2011 +0100 @@ -81,13 +81,13 @@ (* checks and expression agains a result pattern *) fun output_response {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_pat (lhs, pat)); - write_file_ml_blk lhs (ProofContext.theory_of ctxt); + write_file_ml_blk lhs (Proof_Context.theory_of ctxt); output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun output_response_fake {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_val [] NONE lhs); - write_file_ml_blk lhs (ProofContext.theory_of ctxt); + write_file_ml_blk lhs (Proof_Context.theory_of ctxt); output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) diff -r fea1b7ce5c4a -r 25371f74c768 progtutorial.pdf Binary file progtutorial.pdf has changed