# HG changeset patch # User Thomas Sewell # Date 1254111361 -36000 # Node ID fb32a99a7689cada260d5b0272c6bedc64f91aa7 # Parent a4ae77549ed191ca270faa3fd86672cf42a6968b Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form. diff -r a4ae77549ed1 -r fb32a99a7689 src/HOL/Record.thy --- a/src/HOL/Record.thy Mon Sep 28 11:13:11 2009 +1000 +++ b/src/HOL/Record.thy Mon Sep 28 14:16:01 2009 +1000 @@ -70,13 +70,13 @@ text {* Records are isomorphic to compound tuple types. To implement efficient records, we make this isomorphism explicit. Consider the record -access/update simplification "alpha (beta_update f rec) = alpha rec" for +access/update simplification @{text "alpha (beta_update f rec) = alpha rec"} for distinct fields alpha and beta of some record rec with n fields. There -are n^2 such theorems, which prohibits storage of all of them for +are @{text "n ^ 2"} such theorems, which prohibits storage of all of them for large n. The rules can be proved on the fly by case decomposition and simplification in O(n) time. By creating O(n) isomorphic-tuple types while defining the record, however, we can prove the access/update -simplification in O(log(n)^2) time. +simplification in @{text "O(log(n)^2)"} time. The O(n) cost of case decomposition is not because O(n) steps are taken, but rather because the resulting rule must contain O(n) new variables and @@ -85,34 +85,35 @@ Record types are defined as isomorphic to tuple types. For instance, a record type with fields 'a, 'b, 'c and 'd might be introduced as -isomorphic to 'a \ ('b \ ('c \ 'd)). If we balance the tuple tree to -('a \ 'b) \ ('c \ 'd) then accessors can be defined by converting to +isomorphic to @{text "'a \ ('b \ ('c \ 'd))"}. If we balance the tuple tree to +@{text "('a \ 'b) \ ('c \ 'd)"} then accessors can be defined by converting to the underlying type then using O(log(n)) fst or snd operations. -Updators can be defined similarly, if we introduce a fst_update and -snd_update function. Furthermore, we can prove the access/update +Updators can be defined similarly, if we introduce a @{text "fst_update"} and +@{text "snd_update"} function. Furthermore, we can prove the access/update theorem in O(log(n)) steps by using simple rewrites on fst, snd, -fst_update and snd_update. +@{text "fst_update"} and @{text "snd_update"}. The catch is that, although O(log(n)) steps were taken, the underlying type we converted to is a tuple tree of size O(n). Processing this term type wastes performance. We avoid this for large n by taking each subtree of size K and defining a new type isomorphic to that tuple subtree. A record can now be defined as isomorphic to a tuple tree -of these O(n/K) new types, or, if n > K*K, we can repeat the process, +of these O(n/K) new types, or, if @{text "n > K*K"}, we can repeat the process, until the record can be defined in terms of a tuple tree of complexity less than the constant K. If we prove the access/update theorem on this type with the analagous -steps to the tuple tree, we consume O(log(n)^2) time as the intermediate +steps to the tuple tree, we consume @{text "O(log(n)^2)"} time as the intermediate terms are O(log(n)) in size and the types needed have size bounded by K. To enable this analagous traversal, we define the functions seen below: -istuple_fst, istuple_snd, istuple_fst_update and istuple_snd_update. -These functions generalise tuple operations by taking a parameter that -encapsulates a tuple isomorphism. The rewrites needed on these functions -now need an additional assumption which is that the isomorphism works. +@{text "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"} +and @{text "istuple_snd_update"}. These functions generalise tuple +operations by taking a parameter that encapsulates a tuple isomorphism. +The rewrites needed on these functions now need an additional assumption +which is that the isomorphism works. These rewrites are typically used in a structured way. They are here -presented as the introduction rule isomorphic_tuple.intros rather than +presented as the introduction rule @{text "isomorphic_tuple.intros"} rather than as a rewrite rule set. The introduction form is an optimisation, as net matching can be performed at one term location for each step rather than the simplifier searching the term for possible pattern matches. The rule