--- a/CookBook/Package/Ind_Code.thy Thu Mar 12 15:43:22 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy Thu Mar 12 18:39:10 2009 +0000
@@ -24,7 +24,7 @@
been made. What is @{ML Thm.internalK}?
*}
-ML {*let
+ML{*let
val lthy = TheoryTarget.init NONE @{theory}
in
make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
@@ -70,6 +70,18 @@
the (fresh) arguments of the predicate.
*}
+ML{*let
+ val orules = [@{term "even 0"},
+ @{term "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
+ @{term "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
+ val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+in
+ warning
+ (Syntax.string_of_term @{context}
+ (defs_aux @{context} orules preds (@{term "even::nat\<Rightarrow>bool"}, [@{typ "nat"}])))
+end*}
+
+
text {*
The arguments of the main function for the definitions are
the intro rules; the predicates and their names, their syntax
@@ -94,7 +106,6 @@
The actual definitions are made in Line 7.
*}
-
subsection {* Induction Principles *}
ML{*fun inst_spec ct =
@@ -172,6 +183,7 @@
val cnewpreds = map (cterm_of thy) newpreds
val rules' = map (subst_free (preds ~~ newpreds)) rules
+
fun prove_induction ((pred, newpred), tys) =
let
val zs = replicate (length tys) "z"
@@ -184,18 +196,17 @@
in
Goal.prove lthy3 [] [prem] goal
(fn {prems, ...} => induction_tac defs prems cnewpreds)
- |> singleton (ProofContext.export lthy3 lthy1)
+ |> singleton (ProofContext.export lthy3 lthy1)
end
in
map prove_induction (preds ~~ newpreds ~~ tyss)
end*}
-(*
ML {*
let
- val rules = [@{term "even 0"},
- @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
- @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+ val rules = [@{prop "even (0::nat)"},
+ @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
val defs = [@{thm even_def}, @{thm odd_def}]
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
val tyss = [[@{typ "nat"}],[@{typ "nat"}]]
@@ -203,7 +214,6 @@
inductions rules defs preds tyss @{context}
end
*}
-*)
subsection {* Introduction Rules *}
@@ -242,6 +252,21 @@
REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
subproof1 rules preds i ctxt]*}
+lemma evenS:
+ shows "odd m \<Longrightarrow> even (Suc m)"
+apply(tactic {*
+let
+ val rules = [@{prop "even (0::nat)"},
+ @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+ val defs = [@{thm even_def}, @{thm odd_def}]
+ val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+in
+ introductions_tac defs rules preds 1 @{context}
+end *})
+done
+
+
ML{*fun introductions rules preds defs lthy =
let
fun prove_intro (i, goal) =
--- a/CookBook/Tactical.thy Thu Mar 12 15:43:22 2009 +0000
+++ b/CookBook/Tactical.thy Thu Mar 12 18:39:10 2009 +0000
@@ -165,7 +165,7 @@
text {*
which means @{ML no_tac} always fails. The second returns the given theorem wrapped
- up in a single member sequence; it is defined as
+ in a single member sequence; it is defined as
*}
ML{*fun all_tac thm = Seq.single thm*}
@@ -216,6 +216,7 @@
text_raw {*
\begin{figure}[p]
+ \begin{boxedminipage}{\textwidth}
\begin{isabelle}
*}
lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
@@ -284,10 +285,11 @@
done
text_raw {*
\end{isabelle}
+ \end{boxedminipage}
\caption{The figure shows a proof where each intermediate goal state is
printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
the goal state as represented internally (highlighted boxes). This
- illustrates that every goal state in Isabelle is represented by a theorem:
+ tactic shows that every goal state in Isabelle is represented by a theorem:
when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
@@ -326,10 +328,10 @@
section {* Simple Tactics *}
text {*
- Let us start with the tactic @{ML print_tac}, which is quite useful for low-level
- debugging of tactics. It just prints out a message and the current goal state
- (unlike @{ML my_print_tac}, it prints the goal state as the user would see it).
- For example, processing the proof
+ Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful
+ for low-level debugging of tactics. It just prints out a message and the current
+ goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
+ as the user would see it. For example, processing the proof
*}
lemma shows "False \<Longrightarrow> True"
@@ -386,9 +388,9 @@
text {*
Note the number in each tactic call. Also as mentioned in the previous section, most
- basic tactics take such a number as argument; it addresses the subgoal they are analysing.
- In the proof below, we first split up the conjunction in the second subgoal by
- focusing on this subgoal first.
+ basic tactics take such a number as argument: this argument addresses the subgoal
+ the tacics are analysing. In the proof below, we first split up the conjunction in
+ the second subgoal by focusing on this subgoal first.
*}
lemma shows "Foo" and "P \<and> Q"
@@ -421,7 +423,7 @@
(*<*)oops(*>*)
text {*
- Similarly versions taking a list of theorems exist for the tactics
+ Similarl versions taking a list of theorems exist for the tactics
@{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
@@ -521,7 +523,7 @@
*}
text_raw{*
-\begin{figure}
+\begin{figure}[t]
\begin{isabelle}
*}
ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
@@ -1117,7 +1119,7 @@
*}
text_raw {*
-\begin{figure}[tp]
+\begin{figure}[t]
\begin{isabelle}*}
ML{*fun print_ss ctxt ss =
let
@@ -1265,7 +1267,8 @@
text_raw {*
-\begin{figure}[tp]
+\begin{figure}[p]
+\begin{boxedminipage}{\textwidth}
\begin{isabelle} *}
types prm = "(nat \<times> nat) list"
consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80)
@@ -1302,7 +1305,8 @@
shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
by (induct pi\<^isub>2) (auto)
text_raw {*
-\end{isabelle}\medskip
+\end{isabelle}
+\end{boxedminipage}
\caption{A simple theory about permutations over @{typ nat}. The point is that the
lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
it would cause the simplifier to loop. It can still be used as a simplification
--- a/CookBook/document/root.tex Thu Mar 12 15:43:22 2009 +0000
+++ b/CookBook/document/root.tex Thu Mar 12 18:39:10 2009 +0000
@@ -12,6 +12,7 @@
\usepackage{lineno}
\usepackage{xcolor}
\usepackage{framed}
+\usepackage{boxedminipage}
\usepackage{mathpartir}
\usepackage{pdfsetup}
@@ -37,7 +38,7 @@
% sane default for proof documents
\parindent 0pt
\parskip 0.6ex
-\abovecaptionskip -3mm
+\abovecaptionskip 1mm
\belowcaptionskip 10mm
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hyphenation{Isabelle}
Binary file cookbook.pdf has changed