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

Thank you for an answer.

According to the indication,

fun gvar_changename :: "Prog => GvarList => GvarList" where
"gvar_changename pr1 xs = map (%x. case x of GV a b => GV a (fst pr1 @ b)) xs"

by the above, I was able to describe a definition without a problem.

However, in proof, a problem happened.

lemma pre_lim_gl:
"(distinct (Prog_GvarList pr2)) ==> (distinct (gvar_changename pr2 (Prog_GvarList pr2)))"
thm gvar_changename.simps
unfolding gvar_changename.simps
apply (simp add:distinct_map)
apply (simp add:inj_on_def)

"case" emerged in subgoal, and proof did not advance.
I think that I asked you a question many times that I am sorry, but please instruct it.


datatype  Type = PInt | PDouble

  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)"

"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

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