--- 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})"
"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?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
--- 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 "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ by iprover
+
+lemma impE2:
+ shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ by iprover
+
+lemma impE3:
+ shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ by iprover
+
+lemma impE4:
+ shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ by iprover
+
+lemma impE5:
+ shows "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> 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 \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> 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 =
--- 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}
*}
--- 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
Binary file progtutorial.pdf has changed