--- a/ProgTutorial/FirstSteps.thy Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Sat Mar 21 12:35:03 2009 +0100
@@ -119,6 +119,22 @@
"Exception- ERROR \"foo\" raised
At command \"ML\"."}
+ (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
+*}
+
+(*
+ML {*
+fun dodgy_fun () = (raise (ERROR "bar"); 1)
+*}
+
+ML {* set Toplevel.debug *}
+
+ML {* fun f1 () = dodgy_fun () *}
+
+ML {* f1 () *}
+*)
+
+text {*
Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
@@ -197,10 +213,6 @@
fun str_of_thms_raw ctxt thms =
commas (map (str_of_thm_raw ctxt) thms)*}
-text {*
-(FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug})
-*}
-
section {* Combinators\label{sec:combinators} *}
text {*
@@ -477,6 +489,26 @@
Again, this way or referencing simpsets makes you independent from additions
of lemmas to the simpset by the user that potentially cause loops.
+ On the ML-level of Isabelle, you often have to work with qualified names;
+ these are strings with some additional information, such positional information
+ and qualifiers. Such bindings can be generated with the antiquotation
+ @{text "@{bindin \<dots>}"}.
+
+ @{ML_response [display,gray]
+ "@{binding \"name\"}"
+ "name"}
+
+ An example where a binding is needed is the function @{ML define in LocalTheory}.
+ Below this function defines the constant @{term "TrueConj"} as the conjunction
+ @{term "True \<and> True"}.
+*}
+
+local_setup %gray {*
+ snd o LocalTheory.define Thm.internalK
+ ((@{binding "TrueConj"}, NoSyn),
+ (Attrib.empty_binding, @{term "True \<and> True"})) *}
+
+text {*
While antiquotations have many applications, they were originally introduced in order
to avoid explicit bindings for theorems such as:
*}
@@ -494,10 +526,6 @@
kinds of logical elements from th ML-level.
*}
-text {*
- (FIXME: say something about @{text "@{binding \<dots>}"}
-*}
-
section {* Terms and Types *}
text {*
@@ -616,14 +644,27 @@
"Const \<dots> $
Abs (\"x\", \<dots>,
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
- (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
+ (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
- (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda},
+ There are a number of handy functions that are frequently used for
+ constructing terms. One is the function @{ML list_comb} which a term
+ and a list of terms as argument, and produces as output the term
+ list applied to the term. For example
+
+@{ML_response_fake [display,gray]
+"list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
+"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
+
+ (FIXME: handy functions for constructing terms: @{ML lambda},
@{ML subst_free})
*}
+ML {* lambda @{term "x::nat"} @{term "P x"}*}
+
text {*
+ As can be seen this function does not take the typing annotation into account.
+
\begin{readmore}
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
@{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
--- a/ProgTutorial/Intro.thy Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Intro.thy Sat Mar 21 12:35:03 2009 +0100
@@ -151,7 +151,7 @@
{\Large\bf
This document is still in the process of being written! All of the
- text is still under constructions. Sections and
+ text is still under construction. Sections and
chapters that are under \underline{heavy} construction are marked
with TBD.}
--- a/ProgTutorial/Package/Ind_Code.thy Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Sat Mar 21 12:35:03 2009 +0100
@@ -2,9 +2,24 @@
imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
begin
+datatype trm =
+ Var "string"
+| App "trm" "trm"
+| Lam "string" "trm"
+
+simple_inductive
+ fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)
+where
+ "a\<noteq>b \<Longrightarrow> a\<sharp>Var b"
+| "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+| "a\<sharp>Lam a t"
+| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"
+
+
section {* Code *}
text {*
+
@{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
@{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
@@ -533,13 +548,13 @@
ML {* Logic.strip_assums_hyp *}
ML {*
-fun chop_print_tac ctxt thm =
+fun chop_print_tac m n ctxt thm =
let
val [trm] = prems_of thm
val params = map fst (Logic.strip_params trm)
val prems = Logic.strip_assums_hyp trm
- val (prems1, prems2) = chop (length prems - 3) prems;
- val (params1, params2) = chop (length params - 2) params;
+ val (prems1, prems2) = chop (length prems - m) prems;
+ val (params1, params2) = chop (length params - n) params;
val _ = warning (Syntax.string_of_term ctxt trm)
val _ = warning (commas params)
val _ = warning (commas (map (Syntax.string_of_term ctxt) prems))
@@ -551,15 +566,58 @@
end
*}
+ML {* METAHYPS *}
+
+ML {*
+fun chop_print_tac2 ctxt prems =
+let
+ val _ = warning (commas (map (str_of_thm ctxt) prems))
+in
+ all_tac
+end
+*}
lemma intro1:
shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
apply(tactic {* ObjectLogic.rulify_tac 1 *})
apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
-apply(tactic {* chop_print_tac @{context} *})
+apply(tactic {* chop_print_tac 3 2 @{context} *})
oops
+ML {*
+fun SUBPROOF_test tac ctxt =
+ SUBPROOF (fn {params, prems, context,...} =>
+ let
+ val thy = ProofContext.theory_of context
+ in
+ tac (params, prems, context)
+ THEN Method.insert_tac prems 1
+ THEN print_tac "SUBPROOF Test"
+ THEN SkipProof.cheat_tac thy
+ end) ctxt 1
+*}
+
+
+
+
+lemma fresh_App:
+ shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+apply(tactic {* ObjectLogic.rulify_tac 1 *})
+apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
+apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
+oops
+(*
+apply(tactic {* SUBPROOF_test
+ (fn (params, prems, ctxt) =>
+ let
+ val (prems1, prems2) = chop (length prems - 4) prems;
+ val (params1, params2) = chop (length params - 1) params;
+ in
+ rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 2))) 1
+ end) @{context} *})
+*)
+
ML{*fun subproof2 prem params2 prems2 =
SUBPROOF (fn {prems, ...} =>
let
@@ -717,6 +775,7 @@
the rules
\item say that the induction principle is weaker (weaker than
what the standard inductive package generates)
+ \item say that no conformity test is done
\end{itemize}
*}
--- a/ProgTutorial/Parsing.thy Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Parsing.thy Sat Mar 21 12:35:03 2009 +0100
@@ -976,7 +976,7 @@
text {*
Methods are a central concept in Isabelle. They are the ones you use for example
in \isacommand{apply}. To print out all currently known methods you can use the
- Isabelle command.
+ Isabelle command:
*}
print_methods
--- a/ProgTutorial/Solutions.thy Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Solutions.thy Sat Mar 21 12:35:03 2009 +0100
@@ -146,12 +146,8 @@
simplified. We have to be careful to set up the goal so that
other parts of the simplifier do not interfere. For this we construct an
unprovable goal which, after simplification, we are going to ``prove'' with
- the help of the lemma:
-*}
+ the help of ``\isacommand{sorry}'', that is the method @{ML SkipProof.cheat_tac}
-lemma cheat: "A" sorry
-
-text {*
For constructing test cases, we first define a function that returns a
complete binary tree whose leaves are numbers and the nodes are
additions.
@@ -187,11 +183,11 @@
Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
respectively. The idea is to first apply the conversion (respectively simproc) and
- then prove the remaining goal using the @{thm [source] cheat}-lemma.
+ then prove the remaining goal using @{ML "cheat_tac" in SkipProof}.
*}
ML{*local
- fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])
+ fun mk_tac tac = timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})])
in
val c_tac = mk_tac (add_tac @{context})
val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
--- a/ProgTutorial/Tactical.thy Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Tactical.thy Sat Mar 21 12:35:03 2009 +0100
@@ -347,6 +347,20 @@
(*<*)oops(*>*)
text {*
+ A simple tactic making theorem proving particularly simple is
+ @{ML SkipProof.cheat_tac}. This tactic corresponds to
+ the Isabelle command \isacommand{sorry} and is sometimes useful
+ during the development of tactics.
+*}
+
+lemma shows "False" and "something_else_obviously_false"
+apply(tactic {* SkipProof.cheat_tac @{theory} *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
Another simple tactic is the function @{ML atac}, which, as shown in the previous
section, corresponds to the assumption command.
*}
Binary file progtutorial.pdf has changed