*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Failed to parse term after convert to primrec*From*: M A <tesleft at hotmail.com>*Date*: Wed, 29 Oct 2014 11:57:47 +0800*Importance*: Normal*In-reply-to*: <BAY167-W1086A25A3C2791880694439B69E0@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>

Hi in quickspec, i find a lemma and then get 2 subgoals, after rewrite subgoals as primrec and value to see how it works.it return failed to parse term, how to write it and parse successfully? 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 editprimrevmap 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

**Follow-Ups**:**[isabelle] how to use brackets in lemma***From:*M A

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

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

- Previous by Date: Re: [isabelle] how to import circus after extract circus file for unifying theories
- Next by Date: [isabelle] how to use brackets in lemma
- Previous by Thread: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Next by Thread: [isabelle] how to use brackets in lemma
- 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