# HG changeset patch # User haftmann # Date 1288942137 -3600 # Node ID a78a4d03ad7ea0259e92808e6830bff47a9f1168 # Parent 82ebdd19c4a44e80e48149cbd0c505c41c734e17# Parent 82a066bff182054e27e986244632667e3dbcd0bd merged diff -r 82ebdd19c4a4 -r a78a4d03ad7e src/HOL/Imperative_HOL/Array.thy --- 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)) diff -r 82ebdd19c4a4 -r a78a4d03ad7e src/HOL/Imperative_HOL/Overview.thy --- 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 diff -r 82ebdd19c4a4 -r a78a4d03ad7e src/HOL/Library/State_Monad.thy --- 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 "\ \ \'"}, + + \item[transformations] with type signature @{text "\ \ \'"}, transforming a state. - \item[``yielding'' transformations] - with type signature @{text "\ \ \ \ \'"}, - ``yielding'' a side result while transforming a state. - \item[queries] - with type signature @{text "\ \ \"}, - computing a result dependent on a state. + + \item[``yielding'' transformations] with type signature @{text "\ + \ \ \ \'"}, ``yielding'' a side result while transforming a + state. + + \item[queries] with type signature @{text "\ \ \"}, computing a + result dependent on a state. + \end{description} - By convention we write @{text "\"} for types representing states - and @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} - for types representing side results. Type changes due - to transformations are not excluded in our scenario. + By convention we write @{text "\"} for types representing states and + @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} 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 "\"} - are used in a single-threaded way: after application - of a transformation on a value of type @{text "\"}, 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 "\"} are used + in a single-threaded way: after application of a transformation on a + value of type @{text "\"}, the former value should not be used + again. To achieve this, we use a set of monad combinators: *} notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) -abbreviation (input) - "return \ Pair" - text {* - Given two transformations @{term f} and @{term g}, they - may be directly composed using the @{term "op \>"} combinator, - forming a forward composition: @{prop "(f \> g) s = f (g s)"}. + Given two transformations @{term f} and @{term g}, they may be + directly composed using the @{term "op \>"} combinator, forming a + forward composition: @{prop "(f \> 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 \\"} combinator: - @{prop "(f \\ (\x. g)) s = (let (x, s') = f s in g s')"}. + immediately using a lambda abstraction. This is the purpose of the + @{term "op \\"} combinator: @{prop "(f \\ (\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 diff -r 82ebdd19c4a4 -r a78a4d03ad7e src/HOL/Proofs/Extraction/Higman.thy --- 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 \ Random.seed \ letter list \ Random.seed" where "mk_word_aux k = exec { i \ Random.range 10; - (if i > 7 \ k > 2 \ k > 1000 then return [] + (if i > 7 \ k > 2 \ k > 1000 then Pair [] else exec { let l = (if i mod 2 = 0 then A else B); ls \ mk_word_aux (Suc k); - return (l # ls) + Pair (l # ls) })}" by pat_completeness auto termination by (relation "measure ((op -) 1001)") auto diff -r 82ebdd19c4a4 -r a78a4d03ad7e src/Pure/Isar/code.ML --- 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; diff -r 82ebdd19c4a4 -r a78a4d03ad7e src/Tools/nbe.ML --- 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);