# HG changeset patch # User Christian Urban # Date 1250757506 -7200 # Node ID 79202e2eab6a0b21c39fd9b1705c524621be2f00 # Parent 1ca2f41770ccbde4f6b4182746a798b03388348d polished diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Wed Aug 19 09:25:49 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Thu Aug 20 10:38:26 2009 +0200 @@ -239,13 +239,13 @@ A @{ML_type cterm} can be transformed into a string by the following function. *} -ML{*fun string_of_cterm ctxt t = - string_of_term ctxt (term_of t)*} +ML{*fun string_of_cterm ctxt ct = + string_of_term ctxt (term_of ct)*} text {* - In this example the function @{ML [index] term_of} extracts the @{ML_type term} from - a @{ML_type cterm}. More than one @{ML_type cterm}s can again be printed - with @{ML [index] commas}. + In this example the function @{ML [index] term_of} extracts the @{ML_type + term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be + printed with @{ML [index] commas}. *} ML{*fun string_of_cterms ctxt cts = @@ -261,16 +261,19 @@ text {* Theorems also include schematic variables, such as @{text "?P"}, - @{text "?Q"} and so on. + @{text "?Q"} and so on. They are needed in order to able to + instantiate theorems when they are applied. For example the theorem + @{thm [source] conjI} shown below can be used for any (typable) + instantiation of @{text "?P"} and @{text "?Q"} @{ML_response_fake [display, gray] "tracing (string_of_thm @{context} @{thm conjI})" "\?P; ?Q\ \ ?P \ ?Q"} - In order to improve the readability of theorems we convert these schematic - variables into free variables using the function @{ML [index] import in - Variable}. This is similar to statements like @{text "conjI[no_vars]"} - from Isabelle's user-level. + However, in order to improve the readability when printing theorems, we + convert these schematic variables into free variables using the function + @{ML [index] import in Variable}. This is similar to statements like @{text + "conjI[no_vars]"} from Isabelle's user-level. *} ML{*fun no_vars ctxt thm = @@ -300,10 +303,10 @@ commas (map (string_of_thm_no_vars ctxt) thms) *} text {* - When printing out several parcels of information that semantically - belong together, like a warning message consisting for example - of a term and a type, you should try to keep this information - together in a single string. So do not print out information as + Note, that when printing out several parcels of information that + semantically belong together, like a warning message consisting for example + of a term and a type, you should try to keep this information together in a + single string. So do not print out information as @{ML_response_fake [display,gray] "tracing \"First half,\"; @@ -520,8 +523,8 @@ ML{*fun (x, y) ||> f = (x, f y)*} text {* - These two functions can be used to avoid explicit @{text "lets"} for - intermediate values in functions that return pairs. Suppose for example you + These two functions can, for example, be used to avoid explicit @{text "lets"} for + intermediate values in functions that return pairs. As an example, suppose you want to separate a list of integers into two lists according to a treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be @@ -549,9 +552,9 @@ else separate i xs |>> cons x*} text {* - avoiding the explicit @{text "let"}. While in this example the gain is only - small, in more complicated situations the benefit of avoiding @{text "lets"} - can be substantial. + avoiding the explicit @{text "let"}. While in this example the gain in + conciseness is only small, in more complicated situations the benefit of + avoiding @{text "lets"} can be substantial. With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. This combinator is defined as @@ -617,7 +620,7 @@ text {* - When using combinators for writing function in waterfall fashion, it is + When using combinators for writing functions in waterfall fashion, it is sometimes necessary to do some ``plumbing'' in order to fit functions together. We have already seen such plumbing in the function @{ML apply_fresh_args}, where @{ML curry} is needed for making the function @{ML @@ -643,9 +646,9 @@ In this example we obtain two terms with appropriate typing. However, if you have only a single term, then @{ML check_terms in Syntax} needs to be adapted. This can be done with the ``plumbing'' function @{ML - singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax}, - which however is defined in terms of @{ML singleton} and @{ML check_terms in - Syntax}.} For example + singleton}.\footnote{There is already a function @{ML check_term in Syntax} + in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML + check_terms in Syntax}.} For example @{ML_response_fake [display, gray] "let diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Wed Aug 19 09:25:49 2009 +0200 +++ b/ProgTutorial/Solutions.thy Thu Aug 20 10:38:26 2009 +0200 @@ -74,6 +74,102 @@ "(\"foo bar\", \"foo (**test**) bar (**test**)\")"} *} +text {* \solution{ex:dyckhoff} *} + +text {* + The axiom rule can be implemented with the function @{ML atac}. The other + rules correspond to the theorems: + + \begin{center} + \begin{tabular}{cc} + \begin{tabular}{rl} + $\wedge_R$ & @{thm [source] conjI}\\ + $\vee_{R_1}$ & @{thm [source] disjI1}\\ + $\vee_{R_2}$ & @{thm [source] disjI2}\\ + $\longrightarrow_R$ & @{thm [source] impI}\\ + $=_R$ & @{thm [source] iffI}\\ + \end{tabular} + & + \begin{tabular}{rl} + $False$ & @{thm [source] FalseE}\\ + $\wedge_L$ & @{thm [source] conjE}\\ + $\vee_L$ & @{thm [source] disjE}\\ + $=_L$ & @{thm [source] iffE} + \end{tabular} + \end{tabular} + \end{center} + + For the other rules we need to prove the following lemmas. +*} + +lemma impE1: + shows "\A \ B; A; B \ R\ \ R" + by iprover + +lemma impE2: + shows "\(C \ D) \ B; C \ (D \B) \ R\ \ R" + by iprover + +lemma impE3: + shows "\(C \ D) \ B; \C \ B; D \ B\ \ R\ \ R" + by iprover + +lemma impE4: + shows "\(C \ D) \ B; D \ B \ C \ D; B \ R\ \ R" + by iprover + +lemma impE5: + shows "\(C = D) \ B; (C \ D) \ ((D \ C) \ B) \ R\ \ R" + by iprover + +text {* + Now the tactic which applies a single rule can be implemented + as follows. +*} + +ML %linenosgray{*val apply_tac = +let + val intros = [@{thm conjI}, @{thm disjI1}, @{thm disjI2}, + @{thm impI}, @{thm iffI}] + val elims = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE}, + @{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}] +in + atac + ORELSE' resolve_tac intros + ORELSE' eresolve_tac elims + ORELSE' (etac @{thm impE1} THEN' atac) +end*} + +text {* + In Line 11 we apply the rule @{thm [source] impE1} in concjunction + with @{ML atac} in order to reduce the number of possibilities that + need to be explored. You can use the tactic as follows. +*} + +lemma + shows "((((P \ Q) \ P) \ P) \ Q) \ Q" +apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *}) +done + +text {* + We can use the tactic to prove or disprove automatically the + de Bruijn formulae from Exercise \ref{ex:debruijn}. +*} + +ML{*fun de_bruijn_prove ctxt n = +let + val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) +in + Goal.prove ctxt ["P"] [] goal + (fn _ => (DEPTH_SOLVE o apply_tac) 1) +end*} + +text {* + You can use this function to prove de Bruijn formulae. +*} + +ML{*de_bruijn_prove @{context} 3 *} + text {* \solution{ex:addsimproc} *} ML{*fun dest_sum term = diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Wed Aug 19 09:25:49 2009 +0200 +++ b/ProgTutorial/Tactical.thy Thu Aug 20 10:38:26 2009 +0200 @@ -1065,9 +1065,61 @@ Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. \end{readmore} +*} +text {* \begin{exercise}\label{ex:dyckhoff} + Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent + calculus, called G4ip, in which no contraction rule is needed in order to be + complete. As a result the rules applied in any order give a simple decision + procedure for propositional intuitionistic logic. His rules are + + \begin{center} + \def\arraystretch{2.3} + \begin{tabular}{cc} + \infer[Ax]{A,\varGamma \Rightarrow A}{} & + \infer[False]{False,\varGamma \Rightarrow G}{}\\ + + \infer[\wedge_L]{A \wedge B, \varGamma \Rightarrow G}{A, B, \varGamma \Rightarrow G} & + \infer[\wedge_R] + {\varGamma \Rightarrow A\wedge B}{\varGamma \Rightarrow A & \varGamma \Rightarrow B}\\ + \infer[\vee_L] + {A\vee B, \varGamma \Rightarrow G}{A,\varGamma \Rightarrow G & B,\varGamma \Rightarrow G} & + \infer[\vee_{R_1}] + {\varGamma \Rightarrow A \vee B}{\varGamma \Rightarrow A} \hspace{3mm} + \infer[\vee_{R_2}] + {\varGamma \Rightarrow A \vee B}{\varGamma \Rightarrow B}\\ + + \infer[\longrightarrow_{L_1}] + {A\longrightarrow B, A, \varGamma \Rightarrow G}{B, A, \varGamma \Rightarrow G} & + \infer[\longrightarrow_R] + {\varGamma \Rightarrow A\longrightarrow B}{A,\varGamma \Rightarrow B}\\ + + \infer[\longrightarrow_{L_2}] + {(C \wedge D)\longrightarrow B, \varGamma \Rightarrow G} + {C\longrightarrow (D \longrightarrow B), \varGamma \Rightarrow G} & + + \infer[\longrightarrow_{L_3}] + {(C \vee D)\longrightarrow B, \varGamma \Rightarrow G} + {C\longrightarrow B, D\longrightarrow B, \varGamma \Rightarrow G}\\ + + \multicolumn{2}{c}{ + \infer[\longrightarrow_{L_4}] + {(C \longrightarrow D)\longrightarrow B, \varGamma \Rightarrow G} + {D\longrightarrow B, \varGamma \Rightarrow C \longrightarrow D & + B, \varGamma \Rightarrow G}}\\ + \end{tabular} + \end{center} + + Implement a tactic that explores all possibilites of applying these rules to + a propositional formula until a goal state is reached in which all subgoals + are discharged. Note that in Isabelle the left-rules need to be implemented + as elimination rules. You need to prove separate lemmas corresponding to + $\longrightarrow_{L_{1..4}}$. In order to explore all possibilities of applying + the rules, use the tactic combinator @{ML [index] DEPTH_SOLVE}, which searches + for a state in which all subgoals are solved. Add also rules for equality and + run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. \end{exercise} *} diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/document/root.bib --- a/ProgTutorial/document/root.bib Wed Aug 19 09:25:49 2009 +0200 +++ b/ProgTutorial/document/root.bib Thu Aug 20 10:38:26 2009 +0200 @@ -10,36 +10,6 @@ Computing Science, Middlesex University} } -@inproceedings{Krauss-IJCAR06, - author = {A.~Krauss}, - title = {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic}, - editor = {Ulrich Furbach and Natarajan Shankar}, - booktitle = {Automated Reasoning, Third International Joint - Conference, IJCAR 2006, Seattle, WA, USA, August - 17-20, 2006, Proceedings}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {4130}, - year = {2006}, - pages = {589-603} -} - -@INPROCEEDINGS{Melham:1992:PIR, - AUTHOR = {T.~F.~Melham}, - TITLE = {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in - {HOL}}, - BOOKTITLE = {Proceedings of the 1991 International Workshop on - the {HOL} Theorem Proving System and its - Applications, {D}avis, {C}alifornia, {A}ugust - 28--30, 1991}, - EDITOR = {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt - and Phillip J. Windley}, - PUBLISHER = {IEEE Computer Society Press}, - YEAR = {1992}, - PAGES = {350--357}, - ISBN = {0-8186-2460-4}, -} - @Book{isa-tutorial, author = {T.~Nipkow and L.~C.~Paulson and M.~Wenzel}, title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic}, @@ -54,73 +24,6 @@ edition = {2nd}, publisher = {Cambridge University Press}} -@InCollection{Paulson-ind-defs, - author = {L.~C.~Paulson}, - title = {A fixedpoint approach to (co)inductive and - (co)datatype definitions}, - booktitle = {Proof, Language, and Interaction: Essays in Honour - of Robin Milner}, - pages = {187--211}, - publisher = {MIT Press}, - year = 2000, - editor = {G. Plotkin and C. Stirling and M. Tofte} -} - -@inproceedings{Schirmer-LPAR04, - author = {N.~Schirmer}, - title = {{A} {V}erification {E}nvironment for {S}equential {I}mperative - Programs in {I}sabelle/{HOL}}, - booktitle = "Logic for Programming, Artificial Intelligence, and - Reasoning", - editor = "F. Baader and A. Voronkov", - year = 2005, - publisher = "Springer-Verlag", - series = "Lecture Notes in Artificial Intelligence", - volume = 3452, - pages = {398--414} -} - -@TechReport{Schwichtenberg-MLCF, - author = {H.~Schwichtenberg}, - title = {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals}, - institution = {Mathematisches Institut, - Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen}, - year = 2005, - month = {December}, - note = {Available online at - \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}} -} - -@inproceedings{Urban-Berghofer06, - author = {C.~Urban and S.~Berghofer}, - title = {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes - {I}mplemented in {I}sabelle/{HOL}}, - editor = {Ulrich Furbach and Natarajan Shankar}, - booktitle = {Automated Reasoning, Third International Joint - Conference, IJCAR 2006, Seattle, WA, USA, August - 17-20, 2006, Proceedings}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {4130}, - year = {2006}, - pages = {498-512} -} - -@inproceedings{Wadler-AFP95, - author = {P.~Wadler}, - title = {Monads for Functional Programming}, - pages = {24-52}, - editor = {Johan Jeuring and Erik Meijer}, - booktitle = {Advanced Functional Programming, First International - Spring School on Advanced Functional Programming - Techniques, B{\aa}stad, Sweden, May 24-30, 1995, - Tutorial Text}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {925}, - year = {1995} -} - @manual{isa-imp, author = {M.~Wenzel}, title = {The {Isabelle/Isar} Implementation}, @@ -145,3 +48,13 @@ pages = {465--483} } +@Article{ Dyckhoff92, + title = "{Contraction-Free Sequent Calculi for Intuitionistic Logic}", + author = "R. Dyckhoff", + journal = "The Journal of Symbolic Logic", + volume = "57", + number = "3", + pages = "795--807", + year = "1992", + publisher = "JSTOR" +} \ No newline at end of file diff -r 1ca2f41770cc -r 79202e2eab6a progtutorial.pdf Binary file progtutorial.pdf has changed