Re: [isabelle] [Q]Question about Isabelle/hol

Thank you for an answer.

According to the indication,

"prefix_app xs y = map (%x. y @ x) xs"

lemma "(distinct xs) ==> (distinct (prefix_app xs y))"
unfolding prefix_app_def by (auto simp add: distinct_map inj_on_def)

by the above, I was able to solve a problem.

It is the question about applying "map" to "Datatype" definition this time.

  char = A | B | C | D | E | F

type_synonym str = "char list"

type_synonym FileName = str
datatype Gvar = GV Type str
type_synonym GvarList = "Gvar list"

type_synonym Prog = "(FileName * GvarList * Funcs * Main)"

fun gvar_changename :: "Prog =>GvarList => GvarList" where
"gvar_changebname pr1 xs = map (%(GV x y). (GV x (fst pr1)@y)) xs"

It is the expansion of having had you teach it, but this "fun" is displayed with "Syntax error".
Why will you be?
Please reply it if possible.

"Funcs" and "Main" define it at other places, but do not use it here.

Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646 at

On 07/22/2012 08:13 AM, Yuki Goto wrote:
> I am sorry for the delay in my response.
> I am grateful for all the help you game me while we were try to fix the issue.
> I ask you a question about proof of "'a list list" this time.
> I want to prove that there is not overlap even if I append it in each top on the list when "'a list list" does not have overlap.
> fun prefix_app :: "'a list list => 'a list => 'a list list" where
> "prefix_app [] y = []" |
> "prefix_app xs [] = xs" |
> "prefix_app (x#xs) y =  (y @ x) # (prefix_app xs y)"
> lemma "(distinct xs) ==> (distinct (prefix_app xs y))"
> apply (induct_tac y)
> It does not occur to a proof method of this lemma.
> If there is a solution, would you teach it?

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