Re: [isabelle] Failed to parse term



Hi Martin,

You need to understand the definitions in your theory file, the ’a list datatype definition and the definition of app by primrec. Both define an infix operator (see infixr ”#” and infixr ” at ”).

# is the cons operation for lists, that is, x # xs works if x is an element of some fixed type ’a and xs is of type ’a list.

@ is an append operation that joins two _lists_, i.e.  xs @ ys works when xs and ys are both of type ’a list for some fixed type ’a.

In the above ’a is called a type variable.

When I load your theory into Isabelle/JEdit,

primrec rotate1 :: "'a list => 'a list" where
"rotate1 [] = []" |
"rotate1 (x # xs) = xs # [x]"

Isabelle says that the second clause of the rotate1 definition has an error. You cannot write xs # [x] as the left operand should be of type ‘a but it is of type ‘a list.

Concerning your mmap definition

primrec mmap :: "'a => 'b => 'a list => 'a list" where
"mmap f [] = []" |
"mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)"

this is seriously broken, you exchange the left hand side of the second clause with the right hand side, for example. The correct version is

primrec mmap :: "('a => 'b) => 'a list => 'b list" where
"mmap f [] = []" |
"mmap f (x # xs) = (f x) # (mmap f xs)"

mmap’s first argument is not a scalar element of type ‘a but a function that maps from ‘a to ‘b. Since that, it produces a ‘b list from an ‘a list.

I suggest you to learn functional programming first, preferably  with Standard ML as that is close to the higher order logic notation that Isabelle uses.

And please do not send many messages to the list at once.

Best Wishes

- Gergely

From: M A [mailto:tesleft at hotmail.com]
Sent: Thursday, October 30, 2014 5:29 AM
To: Buday Gergely; isabelle-users at cl.cam.ac.uk
Subject: RE: [isabelle] Failed to parse term

Hi Buday,

concatentate
what is the difference between @ and #?

do not know why rotate_app can not be proved and mmap can not be used in value


theory Scratch
imports Datatype
begin
datatype 'a list  = Nil ("[]")
                  | Cons 'a "'a list" (infixr "#" 65)
(* This is the append function: *)
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
primrec rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
primrec itrev :: "'a list => 'a list => 'a list" where
"itrev [] ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"
primrec rotate1 :: "'a list => 'a list" where
"rotate1 [] = []" |
"rotate1 (x # xs) = xs # [x]"
primrec mmap :: "'a => 'b => 'a list => 'a list" where
"mmap f [] = []" |
"mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)"
value "mmap x+1 [1, 2]"
value "rev (True # False # [])"
lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induct_tac xs)
apply(auto)
done
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)
apply(auto)
done
lemma map_app [simp]: "map f xs @ map f ys = map f (xs @ ys)"
apply(induct_tac xs)
apply(auto)
done
lemma rotate_app [simp]: "rotate1 xs @ rotate1 xs == rotate1 (xs @ xs)"
apply(induct_tac xs)
apply(auto)
done
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
apply(auto)
done
theorem rev_rev [simp]: "rev (rev xs) = xs"
apply(induct_tac xs)
apply(auto)
done
lemma "rev xs @ unit x = rev (x # xs)"
apply(induct_tac xs)
apply(auto)
done
lemma "itrev xs [] = rev xs"
apply(induct_tac xs, simp_all)
done
lemma "itrev xs ys = rev xs @ ys"
apply(induct_tac xs,induct_tac ys, simp_all)
done
lemma itrev_app [simp]: "itrev(xs @ ys) = (itrev ys) @ (itrev xs)"
apply(induct_tac xs,induct_tac ys)
apply(auto)
done
theorem itrev_itrev [simp]: "itrev (itrev xs) = xs"
apply(induct_tac xs)
apply(auto)
done
end

Regards,

Martin


From: tesleft at hotmail.com<mailto:tesleft at hotmail.com>
To: gbuday at karolyrobert.hu<mailto:gbuday at karolyrobert.hu>; isabelle-users at cl.cam.ac.uk<mailto:isabelle-users at cl.cam.ac.uk>
Subject: RE: [isabelle] Failed to parse term
Date: Thu, 30 Oct 2014 12:10:13 +0800

Hi Buday,

i send this email again because it seems filter the word which is a haskell program written by NickSmallBone, and i do not receive my email from user forum of Isabelle

i misunderstand @ and # and i see both are concatenate, what are their difference?

beside mmap primrec can not be valued,

i search potential lemma and named it rotate_app

then i copy rotate primrec to window version of Isabelle, it said it can not parse
then i remember Main contains all then i delete rotate1 and prove rotate_app

lemma rotate_app [simp]: "rotate1 xs @ rotate1 xs == rotate1 (xs @ xs)"

but it can not be proved. is it all potential lemma from a program written by NickSmallBone that not all of them can be proved and only some of them can be proved?


theory Scratch
imports Datatype
begin
datatype 'a list  = Nil ("[]")
                  | Cons 'a "'a list" (infixr "#" 65)
(* This is the append function: *)
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
primrec rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
primrec itrev :: "'a list => 'a list => 'a list" where
"itrev [] ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"
primrec rotate1 :: "'a list => 'a list" where
"rotate1 [] = []" |
"rotate1 (x # xs) = xs # [x]"
primrec mmap :: "'a => 'b => 'a list => 'a list" where
"mmap f [] = []" |
"mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)"
value "mmap x+1 [1, 2]"
value "rev (True # False # [])"
lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induct_tac xs)
apply(auto)
done
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)
apply(auto)
done
lemma map_app [simp]: "map f xs @ map f ys = map f (xs @ ys)"
apply(induct_tac xs)
apply(auto)
done
lemma rotate_app [simp]: "rotate1 xs @ rotate1 xs == rotate1 (xs @ xs)"
apply(induct_tac xs)
apply(auto)
done
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
apply(auto)
done
theorem rev_rev [simp]: "rev (rev xs) = xs"
apply(induct_tac xs)
apply(auto)
done
lemma "rev xs @ unit x = rev (x # xs)"
apply(induct_tac xs)
apply(auto)
done
lemma "itrev xs [] = rev xs"
apply(induct_tac xs, simp_all)
done
lemma "itrev xs ys = rev xs @ ys"
apply(induct_tac xs,induct_tac ys, simp_all)
done
lemma itrev_app [simp]: "itrev(xs @ ys) = (itrev ys) @ (itrev xs)"
apply(induct_tac xs,induct_tac ys)
apply(auto)
done
theorem itrev_itrev [simp]: "itrev (itrev xs) = xs"
apply(induct_tac xs)
apply(auto)
done
end

Regards,

Martin


> From: gbuday at karolyrobert.hu<mailto:gbuday at karolyrobert.hu>
> To: tesleft at hotmail.com<mailto:tesleft at hotmail.com>; isabelle-users at cl.cam.ac.uk<mailto:isabelle-users at cl.cam.ac.uk>
> Date: Wed, 29 Oct 2014 13:28:46 +0100
> Subject: Re: [isabelle] Failed to parse term
>
> Hi Martin,
>
> what is your definition of @ ? Did you get it from the Tutorial? As I mentioned it would be better to provide us a working Isabelle theory containing
>
> theory Blabla
> imports main
>
> and all the necessary definitions so we could try it out.
>
> - Gergely
>
> -----Original Message-----
> From: cl-isabelle-users-bounces at lists.cam.ac.uk<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk> [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of M A
> Sent: Wednesday, October 29, 2014 12:42 PM
> To: isabelle-users at cl.cam.ac.uk<mailto:isabelle-users at cl.cam.ac.uk>
> Subject: [isabelle] Failed to parse term
>
>
> Hi
> i am a beginner, first time to write primrec from lemma, however got an error when parse.
>
> lemma map_app [simp]: "map f xs @ map f ys = map f (xs @ ys)"
> apply(induct_tac xs)
> apply(auto)
> done
>
> goal (2 subgoals): 1. map f [] @ map f ys = map f ([] @ ys) 2. ⋀a list. map f list @ map f ys = map f (list @ ys) ⟹ map f (a # list) @ map f ys = map f ((a # list) @ ys)
> prepare to edit
> primrev
> map f [] = []
> map f (a # list) @ map f ys = map f ((a # list) @ ys)
>
> final resultprimrec mmap :: "'a => 'a => 'a list => 'a list" where "mmap f [] = []" | "mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)"
> value "mmap x+1 [1, 2]"
>
> Inner syntax error⌂
> Failed to parse term
>
> Regards,
> Martin


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.