Re: [isabelle-dev] HOLCF lists
On 07/17/2012 07:53 PM, Brian Huffman wrote:
2) I think at some point something like "set :: 'a list => 'a set" for HOLCF
lists would be useful...
What for? Is it meant to be an abstraction of some kind of executable
function, or is it only useful for writing logical specifications?
Only for specification. Thus, I'll use an inductive definition.
4) How to nicely integrate natural numbers? I don't really want to mix =>
and ->, e.g., the "list"-function "take" should have type "nat lift -> 'a
list -> 'a list" (or something similar), rather than "nat => 'a list -> 'a
list" I guess.
HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
nat and int, so you can write types like "nat -> 'a list" or
"nat\<^sub>\ -> 'a list". Decisions about which types to use
should probably follow Haskell: "Integer" should be modeled as
"int\<^sub>\" or "int lift", and for unboxed Haskell types
(e.g. Int#) you can use "int".
Sorry for asking stupid questions (since I am to lazy to look it up
myself): what's the difference between "'a lift" and "'a u" exactly? Is
either of them preferable to model "Haskell-Integers"? I tried to
instantiate "'a u" for my eq-class, but failed due to sort problems,
since I'm not that familiar with the type class hierarchy of HOLCF,
maybe you could save me some time ;).
class eq =
fixes eq :: "'a::pcpo → 'a → tr"
assumes equals_strict [simp]:
"eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
and eq_simps [dest]:
"eq⋅x⋅y = TT ⟹ x = y"
"eq⋅x⋅y = FF ⟹ x ≠ y"
Btw: any more thoughts on actually putting code into some publicly
available destination (bitbucket, sourceforge, ...)?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Locale interpretation introduces abbreviations rather than definitions
On Tue, 17 Jul 2012, Peter Lammich wrote: I have the problem that locale interpretation introduces abbreviations for locally defined constants, rather than definitions. Cross-posting on isabelle-users and isabelle-dev is bad. Since Florian has already answered on isabelle-users, the thread should be there exclusively (or a different one opened on isabelle-dev). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Locale interpretation introduces abbreviations rather than definitions
Hi all, I have the problem that locale interpretation introduces abbreviations for locally defined constants, rather than definitions. This does not work well with the code generator. Is there a way to make locale interpretation introduce real definitions, and, if not, how much effort would it be to implement such a feature? Example: locale l = fixes g::"'a => 'b" begin definition "foo x == (g x,x)" lemma lem: "snd (foo x) = x" unfolding foo_def by simp end interpretation i: l id . thm i.lem export_code i.foo *** Not a constant: l.foo id What I would like here is, that the interpretation command introduces a new constant i.foo, with the definition (or at least code equation) "i.foo x == (g x,x)", and that this constant is also used in the instantiated facts. For this, the code generator could then generate code. Currently, I am defining those constants by hand, after the interpretation, which causes lots of boilerplate in my real applications with more than a dozen of definitions. -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOLCF lists
On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
wrote:
> Dear all,
>
> I put together some functions on lists (that I use in some small proof) in
> Data_List.thy. While doing so and thinking about functions and proofs I
> would need in the future, I stumbled across the following points:
>
> 1) how to name HOLCF functions for which similar functions already exist in
> HOL. As you can see from my example thy-file, I tried to be as close to
> Haskell as possible and therefore hid existing HOL-names. My thinking was
> that when having a HOLCF type of lazy lists one would never want to use the
> HOL datatype list again. Maybe this was oversimplified. What do you think?
I think it is a good idea to use the Haskell names for the HOLCF list functions.
As for name-hiding, ideally this is something that users, not library
writers, should decide. Eventually I hope to see a feature like
"import qualified" for Isabelle. I wouldn't spend too much time
worrying about this for now.
> 2) I think at some point something like "set :: 'a list => 'a set" for HOLCF
> lists would be useful...
What for? Is it meant to be an abstraction of some kind of executable
function, or is it only useful for writing logical specifications?
> however, I did not manage to define it, since I was
> not able to prove continuity for the following specification
>
> "set $ Nil = {}" |
> "set $ (Cons$x$xs) = insert$x$(set$xs)"
>
> Maybe such a function is not a good idea at all in the HOLCF setting and we
> should find something different.
For "set" to have a continuous function type, you must be using a cpo
instance for 'a set, but which one?
If you want "set" to correspond to an executable type of thing, then
probably some kind of powerdomain would serve better as the result
type. But if you only want to use "set" for writing specifications,
then it probably shouldn't be defined as a continuous function; an
inductive definition would make more sense.
> 3) also if properties only hold for "defined" instances of lists (there are
> some differences in how defined they have to be... only xs not bottom, or
> additional no element of xs is bottom, ...), I am currently missing a
> convenient way of expressing this... (first I was thinking about "set" from
> above... but then again, if "set" is a continuous function also "set$xs" can
> be undefined... so maybe there is a nicer way?)
My suggestion: If a property is executable, then define it as a
continuous function; if it is not executable, then define it as an
ordinary HOL predicate.
> 4) How to nicely integrate natural numbers? I don't really want to mix =>
> and ->, e.g., the "list"-function "take" should have type "nat lift -> 'a
> list -> 'a list" (or something similar), rather than "nat => 'a list -> 'a
> list" I guess.
HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
nat and int, so you can write types like "nat -> 'a list" or
"nat\<^sub>\ -> 'a list". Decisions about which types to use
should probably follow Haskell: "Integer" should be modeled as
"int\<^sub>\" or "int lift", and for unboxed Haskell types
(e.g. Int#) you can use "int".
- Brian
>
> I am sure some of you have already considered the above points ;), so please
> let me know your conclusions.
>
> cheers
>
> chris
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOLCF lists
Dear all,
I put together some functions on lists (that I use in some small proof)
in Data_List.thy. While doing so and thinking about functions and proofs
I would need in the future, I stumbled across the following points:
1) how to name HOLCF functions for which similar functions already exist
in HOL. As you can see from my example thy-file, I tried to be as close
to Haskell as possible and therefore hid existing HOL-names. My thinking
was that when having a HOLCF type of lazy lists one would never want to
use the HOL datatype list again. Maybe this was oversimplified. What do
you think?
2) I think at some point something like "set :: 'a list => 'a set" for
HOLCF lists would be useful... however, I did not manage to define it,
since I was not able to prove continuity for the following specification
"set $ Nil = {}" |
"set $ (Cons$x$xs) = insert$x$(set$xs)"
Maybe such a function is not a good idea at all in the HOLCF setting and
we should find something different.
3) also if properties only hold for "defined" instances of lists (there
are some differences in how defined they have to be... only xs not
bottom, or additional no element of xs is bottom, ...), I am currently
missing a convenient way of expressing this... (first I was thinking
about "set" from above... but then again, if "set" is a continuous
function also "set$xs" can be undefined... so maybe there is a nicer way?)
4) How to nicely integrate natural numbers? I don't really want to mix
=> and ->, e.g., the "list"-function "take" should have type "nat lift
-> 'a list -> 'a list" (or something similar), rather than "nat => 'a
list -> 'a list" I guess.
I am sure some of you have already considered the above points ;), so
please let me know your conclusions.
cheers
chris
theory Type_Classes
imports HOLCF
begin
class eq =
fixes eq :: "'a::pcpo \ 'a \ tr"
assumes equals_strict [simp]:
"eq\x\\ = \" "eq\\\y =
\"
and eq_simps [dest]:
"eq\x\y = TT \ x = y"
"eq\x\y = FF \ x \ y"
instantiation lift :: (type) eq
begin
definition eq_lift where
"eq_lift \ \ x y.
(case x of Def x' \
(case y of Def y' \
Def (x' = y')
| \ \ \)
| \ \ \)"
lemma 1: "eq\(x::'a lift)\\ = \"
by (cases x) (simp add: eq_lift_def)+
lemma 2: "eq\\\(y::'a lift) = \"
by (cases y) (simp add: eq_lift_def)+
lemma 3: "eq\(x::'a lift)\y = TT \ x = y"
by (cases x) (cases y, simp_all add: eq_lift_def)+
lemma 4: "eq\(x::'a lift)\y = FF \ x \ y"
by (cases x) (cases y, simp_all add: eq_lift_def)+
instance
by (intro_classes) (fact 1 2 3 4)+
end
end
theory Data_List
imports Type_Classes
begin
subsection {* Setup *}
hide_type (open) list
hide_const (open) List.append List.Cons List.filter List.foldr List.map
List.Nil List.take
no_notation Map.map_add (infixl "++" 100)
domain 'a list =
Nil |
Cons (lazy head :: 'a) (lazy tail :: "'a list")
abbreviation null :: "'a list \ tr" where "null \ is_Nil"
subsection {* Definitions *}
fixrec map :: "('a \ 'b) \ 'a list \ 'b
list" where
"map\f\Nil = Nil" |
"map\f\(Cons\x\xs) =
Cons\(f\x)\(map\f\xs)"
fixrec filter :: "('a \ tr) \ 'a list \ 'a
list" where
"filter\P\Nil = Nil" |
"filter\P\(Cons\x\xs) =
If (P\x) then Cons\x\(filter\P\xs) else
filter\P\xs"
fixrec iterate :: "('a \ 'a) \ 'a \ 'a
list" where
"iterate\f\x =
Cons\x\(iterate\f\(f\x))"
fixrec foldr :: "('a \ 'b \ 'b) \ 'b
\ 'a list \ 'b" where
"foldr\f\d\Nil = d" |
"foldr\f\d\(Cons\x\xs) =
f\x\(foldr\f\d\xs)"
fixrec elem :: "'a::{domain, eq} \ 'a list \ tr" where
"elem\x\Nil = FF" |
"elem\x\(Cons\y\ys) = (eq\x\y orelse
elem\x\ys)"
fixrec append :: "'a list \ 'a list \ 'a list" where
"append\Nil\ys = ys" |
"append\(Cons\x\xs)\ys =
Cons\x\(append\xs\ys)"
fixrec all :: "('a \ tr) \ 'a list \ tr"
where
"all\P\Nil = TT" |
"all\P\(Cons\x\xs) = (P\x andalso
all\P\xs)"
abbreviation append_syn :: "'a list \ 'a list \ 'a
list" (infixr "++" 65) where
"xs ++ ys \ append\xs\ys"
lemma filter_strict [simp]:
"filter\P\\ = \"
by fixrec_simp
lemma map_strict [simp]:
"map\f\\ = \"
by fixrec_simp
lemma map_ID [simp]:
"map\ID\xs = xs"
by (induct xs) simp_all
lemma strict_foldr_strict2 [simp]:
"(\x. f\x\\ = \) \
foldr\f\\\xs = \"
by (induct xs, auto) fixrec_simp
lemma foldr_strict [simp]:
"foldr\f\d\\ = \"
"foldr\f\\\Nil = \"
"foldr\\\d\(Cons\x\xs) = \"
by fixrec_simp+
lemma elem_strict [simp]:
"elem\x\\ = \"
"elem\\\(Cons\y\ys) = \"
by fixrec_simp+
lemma append_strict1 [simp]:
"\ ++ ys = \"
by fixrec_simp
lemma append_Nil2 [simp]:
"xs ++ Nil = xs"
by (induct xs) simp_all
lemma append_assoc [simp]:
"(xs ++ ys) ++ zs = xs ++ ys ++ zs"
by (induct xs) simp_all
lemma filter_append [simp]:
"filter\P\(xs ++ ys) = filter\P\xs ++
filter\P\ys"
proof (induct xs)
case (Cons x xs) thus ?case by (cases "P\x") (auto simp: If_and_if)
qed simp_all
(*FIXME: move*)
lemma orelse_assoc [simp]:
"((x orelse y) orelse z) = (x orelse y orel
