*To*: M A <tesleft at hotmail.com>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Failed to parse term*From*: Buday Gergely <gbuday at karolyrobert.hu>*Date*: Thu, 30 Oct 2014 10:40:34 +0100*Accept-language*: en-US, hu-HU*Acceptlanguage*: en-US, hu-HU*In-reply-to*: <BAY167-W1167A4BFFFB85AE4900BE42B69D0@phx.gbl>*References*: <BAY167-W3024082D992B681F64185DB69E0@phx.gbl>, , , , <BAY167-W27953B618A80B2575F3851B69E0@phx.gbl>, , , , , , , , <16FFFE45-32C8-44B9-8908-A9471D2F4C7D@uibk.ac.at>, , , , <BAY167-W1074477050F04D10DA461BBB69E0@phx.gbl>, , , , <alpine.LNX.2.00.1410272003580.59545@lxbroy10.informatik.tu-muenchen.de>, , <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl>, , <BAY167-W107C4A117B19EE941F4B91DB69C0@phx.gbl>, <BAY167-W10078F5DD087F07D31EA9C1B69C0@phx.gbl>, <C32D3449D568C445AB18C60817FABFE1012FCCA7415B@ingrid.foiskola.krf>, <BAY167-W1286F82424792323A0CEB12B69D0@phx.gbl>, <BAY167-W896B3BA4F8B0884A1DD23FB69D0@phx.gbl>, <BAY167-W890E49D218E525094D14DFB69D0@phx.gbl> <BAY167-W1167A4BFFFB85AE4900BE42B69D0@phx.gbl>*Thread-index*: Ac/z+hmVtRBI7cTUTo2XBOaNNtOt8gAKK88Q*Thread-topic*: [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

**References**:**[isabelle] is it possible to find the function from lemmas and which command can do?***From:*M A

**[isabelle] how to type logical and and logical or operators in Isabelle***From:*M A

**[isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*Makarius

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**[isabelle] Failed to parse term after convert to primrec***From:*M A

**[isabelle] Failed to parse term***From:*M A

**Re: [isabelle] Failed to parse term***From:*Buday Gergely

- Previous by Date: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- Next by Date: Re: [isabelle] Semantics of code adaptations
- Previous by Thread: Re: [isabelle] Failed to parse term
- Next by Thread: Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle
- Cl-isabelle-users October 2014 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