Re: [isabelle] more beginner questions
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 # ))"
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 -----
(* monadic parser (a la parsec) for character strings *)
datatype 'a parser = Parser "char list \<Rightarrow> (char list * 'a)
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 *
primrec "onlyCh ch  = None"
"onlyCh ch (x # xs) = (if (x = ch) then (Some (xs, x))
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 # ))"
---- end gram.thy ----
This archive was generated by a fusion of
Pipermail (Mailman edition) and