Email Gateway (Aug 18 2022 at 10:50): Email Gateway (Aug 18 2022 at 10:50):From: Tim Newsham <newsham@lava.net>
1) Is there a datatype for characters in isabelle? I would like
to prove stuff about a real world grammar for a language of
characters.
2) This is really basic but giving me a headache. How can I make
an optional tuple? I tried "('a, 'a) option" but that didnt seem
to work properly.
3) Do any isabelle users hang out on some real-time chat network where
a beginner like me could pester them? For example irc.freenode.net
#isabelle would be nice. hint hint
I'm there, but I'm afraid I'm in no position to answer questions :)
thanks in advance.
Tim Newsham
http://www.thenewsh.com/~newsham/
Email Gateway (Aug 18 2022 at 10:50):From: Tobias Nipkow <nipkow@in.tum.de>
1) Is there a datatype for characters in isabelle? I would like
to prove stuff about a real world grammar for a language of
characters.
Yes, char, in List.
2) This is really basic but giving me a headache. How can I make
an optional tuple? I tried "('a, 'a) option" but that didnt seem
to work properly.
You are using Haskell syntax. Try "('a * 'a) option".
Tobias
Email Gateway (Aug 18 2022 at 10:50):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
On Mon, Sep 24, 2007 at 05:33:51PM -1000, Tim Newsham wrote:
1) Is there a datatype for characters in isabelle? I would like
to prove stuff about a real world grammar for a language of
characters.
Yes there is (it is called char). To use them you
have to include letters in double single quotes.
E.g., the character A would be written as ''A''2) This is really basic but giving me a headache. How can I make
an optional tuple? I tried "('a, 'a) option" but that didnt seem
to work properly.
The syntax would be
datatype 'a option = None | Some 'a
But this type is already predefined... so just use the construcotrs
None and Some (taking one argument).
3) Do any isabelle users hang out on some real-time chat network where
a beginner like me could pester them? For example irc.freenode.net
#isabelle would be nice. hint hint
I'm there, but I'm afraid I'm in no position to answer questions :)
I do not know about that.thanks in advance.
Tim Newsham
http://www.thenewsh.com/~newsham/cheers
christian
Email Gateway (Aug 18 2022 at 10:50):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
On Tuesday 25 September 2007 05:33, Tim Newsham wrote:
1) Is there a datatype for characters in isabelle? I would like
to prove stuff about a real world grammar for a language of
characters.Yes. I'm not sure how you enter a single character, but you have
"''A'' :: char list" for example, and also
"''ABC'' :: char list" (ie two single forward quotes before and after).
Defined in src/HOL/List.thy
2) This is really basic but giving me a headache. How can I make
an optional tuple? I tried "('a, 'a) option" but that didnt seem
to work properly.
Your "('a, 'a)" is Haskell-style for expressing a tuple type.
Isabelle-style (and ML style) is ('a * 'a)
Thus eg
"Some (1, a) :: (nat * 'a) option"
Note the lower cases in Some and None.
Defined in src/HOL/Datatype.thy
Jeremy
thanks in advance.
Tim Newsham
http://www.thenewsh.com/~newsham/
Email Gateway (Aug 18 2022 at 10:50):From: Paul Graunke <paul.graunke@galois.com>
On Sep 24, 2007, at 8:33 PM, Tim Newsham wrote:
1) Is there a datatype for characters in isabelle? I would like
to prove stuff about a real world grammar for a language of
characters.
I think it is called "char". At one point the fully qualified name
was "List.char".
2) This is really basic but giving me a headache. How can I make
an optional tuple? I tried "('a, 'a) option" but that didnt seem
to work properly.
Try "('a * 'a) option" or "('a \<times> 'a) option".
Regards,
Paul
Email Gateway (Aug 18 2022 at 10:51):From: Tim Newsham <newsham@lava.net>
Thanks for the many answers. I wasn't properly using (a * b) for
tuple types, and I overlooked the "char" definition in List.
I've made a bit more progress and am again stuck. I made
a definition for a character parser and a property for when
a parser accepts a string and I want to prove that the character
parser only accepts strings that are made up of that one
particular character (excuse the extra parens, I'm playing it
safe until I'm more comfortable with Isabelle):
lemma "(accepts (pcar ch) s) => (s = (ch # []))"
apply(case_tac s)
apply(simp add:pchar_def)
apply(simp add:pchar_def)
at this point I feel like I want to use split_if, but
apply(split split_if) fails. I'm not sure if my definition for
onlyCh is acceptable, but I was able to dispatch part of the
proof so perhaps it is. Is my problem due to any of my definitions
being unsuitable or is there a simple way to continue the current
proof? The last goal was:
!! a list .
[| case if a = ch then Some (list, a) else None of None => False
| Some (resid, result) => null resid;
s = a # list |]
==> a = ch /\ list = []
The full body of my thy file is:
------- gram.thy -----
theory Gram
imports Main
begin
(* monadic parser (a la parsec) for character strings *)
datatype 'a parser = Parser "char list \<Rightarrow> (char list * 'a)
option"
(*
An input string is fully consumed and accepted by a parser.
Only if it parses successfully and it consumes the full input.
*)
consts accepts :: "'a parser \<Rightarrow> char list \<Rightarrow> bool"
primrec "accepts (Parser p) cs = (case p cs of
None \<Rightarrow> False
| Some (resid, result) \<Rightarrow> null resid)"
(* a parser for an arbitrary character *)
consts onlyCh :: "char \<Rightarrow> char list \<Rightarrow> (char list *
char) option"
primrec "onlyCh ch [] = None"
"onlyCh ch (x # xs) = (if (x = ch) then (Some (xs, x))
else None)"
constdefs
pchar :: "char \<Rightarrow> char parser"
"pchar == %ch . (Parser (onlyCh ch))"
(* character parser only accepts the single character *)
lemma "(accepts (pchar ch) s) \<Longrightarrow> (s = (ch # []))"
apply(case_tac s)
apply(simp add:pchar_def)
apply(simp add:pchar_def)
apply(split split_if)
---- end gram.thy ----
Tim Newsham
http://www.thenewsh.com/~newsham/
Email Gateway (Aug 18 2022 at 10:51):From: Brian Huffman <brianh@cs.pdx.edu>
If-then-else and other case-combinators each have two separate split rules:
One is for use in the conclusion of a subgoal, and the other is for use with
the assumptions. For if-then-else, the two split rules are called "split_if"
and "split_if_asm".
Since your subgoal has an if-then-else in the assumptions, you should use:
apply (split split_if_asm)
The split rules for case expressions have a standard naming scheme based on
the name of the datatype: For type nat they are "nat.split"
and "nat.split_asm"; "nat.splits" refers to both. Rules for other datatypes
are similarly named.
Last updated: May 03 2024 at 01:09 UTC