summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 05 Nov 2010 08:28:57 +0100 | |

changeset 40363 | a78a4d03ad7e |

parent 40357 | 82ebdd19c4a4 (current diff) |

parent 40362 | 82a066bff182 (diff) |

child 40367 | 6fb991dc074b |

merged

--- a/src/HOL/Imperative_HOL/Array.thy Thu Nov 04 18:01:55 2010 +0100 +++ b/src/HOL/Imperative_HOL/Array.thy Fri Nov 05 08:28:57 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 Thu Nov 04 18:01:55 2010 +0100 +++ b/src/HOL/Imperative_HOL/Overview.thy Fri Nov 05 08:28:57 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 Thu Nov 04 18:01:55 2010 +0100 +++ b/src/HOL/Library/State_Monad.thy Fri Nov 05 08:28:57 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 Thu Nov 04 18:01:55 2010 +0100 +++ b/src/HOL/Proofs/Extraction/Higman.thy Fri Nov 05 08:28:57 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 Thu Nov 04 18:01:55 2010 +0100 +++ b/src/Pure/Isar/code.ML Fri Nov 05 08:28:57 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 Thu Nov 04 18:01:55 2010 +0100 +++ b/src/Tools/nbe.ML Fri Nov 05 08:28:57 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);