[isabelle] "distinct" for Datatype

Dear Sirs/Madams,

I'd like to ask a question.
The contents are as follows:

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

type_synonym str = "char list"

datatype  Type = PInt | PDouble

datatype Gvar = GV Type str

fun gvar_changename :: "str \<Rightarrow> Gvar list \<Rightarrow> Gvar list" where
"gvar_changename xs gl = map (%x. case x of (GV x y) \<Rightarrow> (GV x (xs at y)) ) gl"

fun gvl2strl :: "Gvar list \<Rightarrow> str list" where
"gvl2strl gl = map (%x. case x of (GV a b) \<Rightarrow> b) gl"

lemma limitation_gl_test : "(distinct (gvl2strl gl)) & (\<forall>x \<in> set (gvl2strl gl). x \<noteq> []  )
  \<Longrightarrow> (distinct (gvl2strl (gvar_changename pr gl)  ))"
apply (simp only:gvl2strl.simps)
apply (simp add:distinct_map)
apply (simp add:inj_on_def)
apply auto

This lemma is not solved.
I want to make "distinct (str list)", but "distinct gl" originally appears in the premise part.
Your help would be appreciated.


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

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