*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] more beginner questions*From*: Tim Newsham <newsham at lava.net>*Date*: Tue, 25 Sep 2007 06:59:02 -1000 (HST)*In-reply-to*: <46F8BCC9.50204@informatik.tu-muenchen.de>*References*: <Pine.BSI.4.64.0709241731260.6561@malasada.lava.net> <46F8BCC9.50204@informatik.tu-muenchen.de>

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 *)

(* 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 *)

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/

**Follow-Ups**:**Re: [isabelle] more beginner questions***From:*Brian Huffman

**References**:**[isabelle] more beginner questions***From:*Tim Newsham

- Previous by Date: Re: [isabelle] more beginner questions
- Next by Date: Re: [isabelle] more beginner questions
- Previous by Thread: Re: [isabelle] more beginner questions
- Next by Thread: Re: [isabelle] more beginner questions
- Cl-isabelle-users September 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list