--- a/src/HOL/Imperative_HOL/Array.thy Fri Nov 05 08:16:35 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Nov 05 09:07:14 2010 +0100
@@ -134,9 +134,13 @@
by (auto simp add: update_def set_set_swap list_update_swap)
lemma get_alloc:
- "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
+ "get (snd (alloc xs h)) (fst (alloc ys h)) = xs"
by (simp add: Let_def split_def alloc_def)
+lemma length_alloc:
+ "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs"
+ by (simp add: Array.length_def get_alloc)
+
lemma set:
"set (fst (alloc ls h))
new_ls (snd (alloc ls h))
--- a/src/HOL/Imperative_HOL/Overview.thy Fri Nov 05 08:16:35 2010 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy Fri Nov 05 09:07:14 2010 +0100
@@ -31,7 +31,7 @@
realisation has changed since, due to both extensions and
refinements. Therefore this overview wants to present the framework
\qt{as it is} by now. It focusses on the user-view, less on matters
- of constructions. For details study of the theory sources is
+ of construction. For details study of the theory sources is
encouraged.
*}
@@ -41,7 +41,8 @@
text {*
Heaps (@{type heap}) can be populated by values of class @{class
heap}; HOL's default types are already instantiated to class @{class
- heap}.
+ heap}. Class @{class heap} is a subclass of @{class countable}; see
+ theory @{text Countable} for ways to instantiate types as @{class countable}.
The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
following specification:
@@ -100,7 +101,7 @@
provides a simple relational calculus. Primitive rules are @{text
crelI} and @{text crelE}, rules appropriate for reasoning about
- imperative operation are available in the @{text crel_intros} and
+ imperative operations are available in the @{text crel_intros} and
@{text crel_elims} fact collections.
Often non-failure of imperative computations does not depend
--- a/src/HOL/Library/State_Monad.thy Fri Nov 05 08:16:35 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy Fri Nov 05 09:07:14 2010 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Combinator syntax for generic, open state monads (single threaded monads) *}
+header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
theory State_Monad
imports Main Monad_Syntax
@@ -11,19 +11,18 @@
subsection {* Motivation *}
text {*
- The logic HOL has no notion of constructor classes, so
- it is not possible to model monads the Haskell way
- in full genericity in Isabelle/HOL.
+ The logic HOL has no notion of constructor classes, so it is not
+ possible to model monads the Haskell way in full genericity in
+ Isabelle/HOL.
- However, this theory provides substantial support for
- a very common class of monads: \emph{state monads}
- (or \emph{single-threaded monads}, since a state
- is transformed single-threaded).
+ However, this theory provides substantial support for a very common
+ class of monads: \emph{state monads} (or \emph{single-threaded
+ monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
- makes a good motivating start. Here we just sketch briefly
- how those monads enter the game of Isabelle/HOL.
+ \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
+ a good motivating start. Here we just sketch briefly how those
+ monads enter the game of Isabelle/HOL.
*}
subsection {* State transformations and combinators *}
@@ -32,64 +31,66 @@
We classify functions operating on states into two categories:
\begin{description}
- \item[transformations]
- with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
+
+ \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
transforming a state.
- \item[``yielding'' transformations]
- with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
- ``yielding'' a side result while transforming a state.
- \item[queries]
- with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
- computing a result dependent on a state.
+
+ \item[``yielding'' transformations] with type signature @{text "\<sigma>
+ \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a
+ state.
+
+ \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
+ result dependent on a state.
+
\end{description}
- By convention we write @{text "\<sigma>"} for types representing states
- and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
- for types representing side results. Type changes due
- to transformations are not excluded in our scenario.
+ By convention we write @{text "\<sigma>"} for types representing states and
+ @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
+ representing side results. Type changes due to transformations are
+ not excluded in our scenario.
- We aim to assert that values of any state type @{text "\<sigma>"}
- are used in a single-threaded way: after application
- of a transformation on a value of type @{text "\<sigma>"}, the
- former value should not be used again. To achieve this,
- we use a set of monad combinators:
+ We aim to assert that values of any state type @{text "\<sigma>"} are used
+ in a single-threaded way: after application of a transformation on a
+ value of type @{text "\<sigma>"}, the former value should not be used
+ again. To achieve this, we use a set of monad combinators:
*}
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
-abbreviation (input)
- "return \<equiv> Pair"
-
text {*
- Given two transformations @{term f} and @{term g}, they
- may be directly composed using the @{term "op \<circ>>"} combinator,
- forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
+ Given two transformations @{term f} and @{term g}, they may be
+ directly composed using the @{term "op \<circ>>"} combinator, forming a
+ forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
After any yielding transformation, we bind the side result
- immediately using a lambda abstraction. This
- is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
- @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+ immediately using a lambda abstraction. This is the purpose of the
+ @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
+ = f s in g s')"}.
For queries, the existing @{term "Let"} is appropriate.
- Naturally, a computation may yield a side result by pairing
- it to the state from the left; we introduce the
- suggestive abbreviation @{term return} for this purpose.
+ Naturally, a computation may yield a side result by pairing it to
+ the state from the left; we introduce the suggestive abbreviation
+ @{term return} for this purpose.
- The most crucial distinction to Haskell is that we do
- not need to introduce distinguished type constructors
- for different kinds of state. This has two consequences:
+ The most crucial distinction to Haskell is that we do not need to
+ introduce distinguished type constructors for different kinds of
+ state. This has two consequences:
+
\begin{itemize}
- \item The monad model does not state anything about
- the kind of state; the model for the state is
- completely orthogonal and may be
- specified completely independently.
- \item There is no distinguished type constructor
- encapsulating away the state transformation, i.e.~transformations
- may be applied directly without using any lifting
- or providing and dropping units (``open monad'').
+
+ \item The monad model does not state anything about the kind of
+ state; the model for the state is completely orthogonal and may
+ be specified completely independently.
+
+ \item There is no distinguished type constructor encapsulating
+ away the state transformation, i.e.~transformations may be
+ applied directly without using any lifting or providing and
+ dropping units (``open monad'').
+
\item The type of states may change due to a transformation.
+
\end{itemize}
*}
@@ -97,8 +98,8 @@
subsection {* Monad laws *}
text {*
- The common monadic laws hold and may also be used
- as normalization rules for monadic expressions:
+ The common monadic laws hold and may also be used as normalization
+ rules for monadic expressions:
*}
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
@@ -145,7 +146,7 @@
"_sdo_block (_sdo_final e)" => "e"
text {*
- For an example, see HOL/Extraction/Higman.thy.
+ For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
*}
end
--- a/src/HOL/Proofs/Extraction/Higman.thy Fri Nov 05 08:16:35 2010 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy Fri Nov 05 09:07:14 2010 +0100
@@ -352,11 +352,11 @@
function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_aux k = exec {
i \<leftarrow> Random.range 10;
- (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
+ (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
else exec {
let l = (if i mod 2 = 0 then A else B);
ls \<leftarrow> mk_word_aux (Suc k);
- return (l # ls)
+ Pair (l # ls)
})}"
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
--- a/src/Pure/Isar/code.ML Fri Nov 05 08:16:35 2010 +0100
+++ b/src/Pure/Isar/code.ML Fri Nov 05 09:07:14 2010 +0100
@@ -124,11 +124,23 @@
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
-fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
+fun check_unoverload thy (c, ty) =
+ let
+ val c' = AxClass.unoverload_const thy (c, ty);
+ val ty_decl = Sign.the_const_type thy c';
+ in if Sign.typ_equiv thy
+ (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c'
+ else error ("Type\n" ^ string_of_typ thy ty
+ ^ "\nof constant " ^ quote c
+ ^ "\nis too specific compared to declared type\n"
+ ^ string_of_typ thy ty_decl)
+ end;
+
+fun check_const thy = check_unoverload thy o check_bare_const thy;
fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
-fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
+fun read_const thy = check_unoverload thy o read_bare_const thy;
(** data store **)
@@ -471,7 +483,7 @@
in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
else bad_thm ("Type\n" ^ string_of_typ thy ty
^ "\nof constant " ^ quote c
- ^ "\nis incompatible with declared type\n"
+ ^ "\nis too specific compared to declared type\n"
^ string_of_typ thy ty_decl)
end;
--- a/src/Tools/nbe.ML Fri Nov 05 08:16:35 2010 +0100
+++ b/src/Tools/nbe.ML Fri Nov 05 09:07:14 2010 +0100
@@ -64,7 +64,7 @@
val lhs_rhs = case try Logic.dest_equals eqn
of SOME lhs_rhs => lhs_rhs
| _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
- val c_c' = case try (pairself (Code.check_const thy)) lhs_rhs
+ val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
of SOME c_c' => c_c'
| _ => error ("Not an equation with two constants: "
^ Syntax.string_of_term_global thy eqn);