# HG changeset patch
# User boehmes
# Date 1231342189 -3600
# Node ID 64c9540f2f8402ca869038b2e5e7557c193503b6
# Parent  5b9c6010897bfcfd1f4984f41caefcd08c55993e
Added four recipes.

diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/ROOT.ML
--- a/CookBook/ROOT.ML	Sat Jan 03 20:44:54 2009 +0000
+++ b/CookBook/ROOT.ML	Wed Jan 07 16:29:49 2009 +0100
@@ -16,6 +16,10 @@
 use_thy "Recipes/NamedThms";
 use_thy "Recipes/Transformation";
 use_thy "Recipes/Antiquotes";
+use_thy "Recipes/TimeLimit";
+use_thy "Recipes/Config";
+use_thy "Recipes/StoringData";
+use_thy "Recipes/ExternalSolver";
 
 use_thy "Solutions";
-use_thy "Readme";
\ No newline at end of file
+use_thy "Readme";
diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/Recipes/Config.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Config.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,57 @@
+theory Config
+imports Base
+begin
+
+section {* Configuration Options *} 
+
+
+text {*
+  {\bf Problem:} 
+  You would like to enhance your tool with options which can be changed later on
+  by the user.\smallskip
+
+  {\bf Solution:} This can be achieved using configuration values.\smallskip
+
+  *}
+
+ML {*
+val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false
+val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0
+val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string"
+*}
+
+setup "setup_bvalue o setup_ivalue o setup_svalue"
+
+declare [[bvalue = true, ivalue = 3]]
+
+text {*
+  Note that this works without introducing a new command to modify the 
+  configuration options. *}
+
+ML {*
+Config.get @{context} bvalue
+*}
+
+ML {*
+Config.get_thy @{theory} ivalue
+*}
+
+setup {* Config.put_thy svalue "foo" *}
+
+ML {* 
+Config.get @{context} svalue
+*}
+
+ML {*
+let val ctxt = Config.map ivalue (fn i => i + 1) @{context}
+in Config.get ctxt ivalue end
+*}
+
+
+text {*
+  Code: Pure/Isar/attrib.ML, Pure/config.ML
+
+  Note: Avoid to use references for this purpose!
+  *}
+
+end
\ No newline at end of file
diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/Recipes/ExternalSolver.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,112 @@
+theory ExternalSolver
+imports "../Base"
+begin
+
+section {* Using an External Solver *} 
+
+text {*
+  {\bf Problem:}
+  You want to use an external solver, say, because it is more efficient in
+  deciding particular formulas than any Isabelle tactic.
+  \smallskip
+
+  {\bf Solution:} The easiest way to do this is writing an oracle.
+  To yield results checked by Isabelle's kernel, one can reconstruct the
+  proofs.
+  \smallskip
+
+  \begin{readmore}
+  A short introduction to oracles can be found in [isar-ref: no suitable label
+  for section 3.11]. A simple example is given in 
+  @{ML_file "FOL/ex/IffOracle"}.
+  (TODO: add more references to the code)
+  \end{readmore}
+
+  The general layout will be as follows. Given a goal G, we transform it into
+  the syntactical respresentation of the external solver, and invoke the
+  solver. The solver's result is then used inside the oracle to either return
+  the proved goal or raise an exception meaning that the solver was unable to
+  prove the goal.
+
+  For communication with external programs, there are the primitives
+  @{ML_text system} and @{ML_text system_out}, the latter of which captures
+  the invoked program's output. For simplicity, here, we will use metis, an
+  external solver included in the Isabelle destribution. Since it is written
+  in ML, we can call it directly without the detour of invoking an external
+  program.
+
+  We will restrict ourselves to proving formulas of propositional logic, a
+  task metis is very good at.
+  *}
+
+
+ML {*
+fun trans t =
+  (case t of
+    @{term Trueprop} $ t => trans t
+  | @{term True} => Metis.Formula.True
+  | @{term False} => Metis.Formula.False
+  | @{term Not} $ t => Metis.Formula.Not (trans t)
+  | @{term "op &"} $ t1 $ t2 => Metis.Formula.And (trans t1, trans t2)
+  | @{term "op |"} $ t1 $ t2 => Metis.Formula.Or (trans t1, trans t2)
+  | @{term "op -->"} $ t1 $ t2 => Metis.Formula.Imp (trans t1, trans t2)
+  | @{term "op = :: bool => bool => bool"} $ t1 $ t2 => 
+      Metis.Formula.Iff (trans t1, trans t2)
+  | Free (n, @{typ bool}) => Metis.Formula.Atom (n, [])
+  | _ => error "inacceptable term")
+*}
+
+
+ML {*
+fun solve f =
+  let
+    open Metis
+    fun fromLiterals fms = LiteralSet.fromList (map Literal.fromFormula fms)
+    fun fromClause fm = fromLiterals (Formula.stripDisj fm)
+    fun fromCnf fm = map fromClause (Formula.stripConj fm)
+
+    val mk_cnfs = map fromCnf o Normalize.cnf o Formula.Not
+    fun refute cls =
+      let val res = Resolution.new Resolution.default (map Thm.axiom cls)
+      in
+        (case Resolution.loop res of
+          Resolution.Contradiction _ => true
+        | Resolution.Satisfiable _ => false)
+      end
+  in List.all refute (mk_cnfs f) end
+*}
+
+
+ML {*
+fun prop_dp (thy, t) = if solve (trans t) then Thm.cterm_of thy t 
+  else error "Proof failed."
+*}
+
+oracle prop_oracle = prop_dp
+
+ML {*
+fun prop_oracle_tac ctxt = 
+  SUBGOAL (fn (goal, i) => 
+    (case try prop_oracle (ProofContext.theory_of ctxt, goal) of
+      SOME thm => rtac thm i
+    | NONE => no_tac))
+*}
+
+method_setup prop_oracle = {*
+  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (prop_oracle_tac ctxt))
+*} "Oracle-based decision procedure for propositional logic"
+
+lemma "p \<or> \<not>p"
+  by prop_oracle
+
+lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p"
+  by prop_oracle
+
+lemma "\<forall>x::nat. x \<ge> 0"
+  sorry
+
+
+(* TODO: proof reconstruction *)
+
+
+end
\ No newline at end of file
diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/Recipes/StoringData.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/StoringData.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,47 @@
+theory StoringData
+imports "../Base"
+begin
+
+section {* Storing Data *} 
+
+
+text {*
+  {\bf Problem:} 
+  Your tool needs to keep complex data.\smallskip
+
+  {\bf Solution:} This can be achieved using a generic data slot.\smallskip
+
+  Every generic data slot may keep data of any kind which is stored in the
+  context.
+
+  *}
+
+ML {*
+local
+
+structure Data = GenericDataFun
+(
+  type T = int Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  fun merge _ = Symtab.merge (K true)
+)
+
+in
+
+val lookup = Symtab.lookup o Data.get
+
+fun update k v = Data.map (Symtab.update (k, v))
+
+end
+*}
+
+setup {* Context.theory_map (update "foo" 1) *}
+
+ML {* lookup (Context.Proof @{context}) "foo" *}
+
+text {*
+  alternatives: TheoryDataFun, ProofDataFun
+  Code: Pure/context.ML *}
+
+end
\ No newline at end of file
diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/Recipes/TimeLimit.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,41 @@
+theory TimeLimit
+imports Base
+begin
+
+section {* Restricting the Runtime of a Function *} 
+
+
+text {*
+  {\bf Problem:}
+  Your tool should run only a specified amount of seconds.\smallskip
+
+  {\bf Solution:} This can be achieved using time limits.\smallskip
+
+  Assume the following function should run only five seconds:
+
+  *}
+
+ML {*
+fun ackermann (0, n) = n + 1
+  | ackermann (m, 0) = ackermann (m - 1, 1)
+  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))
+*}
+
+ML {* ackermann (3, 12) *}
+
+(* takes more than 10 seconds *)
+
+text {*
+  The call can be encapsulated in a time limit of five seconds as follows:
+  *}
+
+ML {* 
+TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) 
+  handle TimeOut => ~1
+*}
+
+text {*
+  The function "TimeLimit.timeLimit" has type "???" and is defined in
+  TODO: refer to code *}
+
+end
\ No newline at end of file
diff -r 5b9c6010897b -r 64c9540f2f84 cookbook.pdf
Binary file cookbook.pdf has changed