# HG changeset patch # User Christian Urban # Date 1236883150 0 # Node ID d820cb5873ea996052027c50252d7adc92fbf51f # Parent ec47352e99c289db0b78a2a34b8e63b8d3304140 used latex package boxedminipage diff -r ec47352e99c2 -r d820cb5873ea CookBook/Package/Ind_Code.thy --- 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 "\n::nat. odd n \ even (Suc n)"}, + @{term "\n::nat. even n \ odd (Suc n)"}] + val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] +in + warning + (Syntax.string_of_term @{context} + (defs_aux @{context} orules preds (@{term "even::nat\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 "\n::nat. odd n \ even (Suc n)"}, - @{term "\n::nat. even n \ odd (Suc n)"}] + val rules = [@{prop "even (0::nat)"}, + @{prop "\n::nat. odd n \ even (Suc n)"}, + @{prop "\n::nat. even n \ odd (Suc n)"}] val defs = [@{thm even_def}, @{thm odd_def}] val preds = [@{term "even::nat\bool"}, @{term "odd::nat\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 \ even (Suc m)" +apply(tactic {* +let + val rules = [@{prop "even (0::nat)"}, + @{prop "\n::nat. odd n \ even (Suc n)"}, + @{prop "\n::nat. even n \ odd (Suc n)"}] + val defs = [@{thm even_def}, @{thm odd_def}] + val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] +in + introductions_tac defs rules preds 1 @{context} +end *}) +done + + ML{*fun introductions rules preds defs lthy = let fun prove_intro (i, goal) = diff -r ec47352e99c2 -r d820cb5873ea CookBook/Tactical.thy --- 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 "\A; B\ \ A \ 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 "\A; B\ \ A \ B"}} the theorem is @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"}; when you finish the proof the theorem is @{text "\A; B\ \ A \ 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 \ 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 \ 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 \ nat) list" consts perm :: "prm \ 'a \ 'a" ("_ \ _" [80,80] 80) @@ -1302,7 +1305,8 @@ shows "pi\<^isub>1\(pi\<^isub>2\c) = (pi\<^isub>1\pi\<^isub>2)\(pi\<^isub>1\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 diff -r ec47352e99c2 -r d820cb5873ea CookBook/document/root.tex --- 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} diff -r ec47352e99c2 -r d820cb5873ea cookbook.pdf Binary file cookbook.pdf has changed