Email Gateway (Aug 19 2022 at 08:37): Email Gateway (Aug 19 2022 at 08:37):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
Dear Sirs/Madams,
I'd like to ask a question.
The contents are as follows:
datatype
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@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.
Sincerely,
Goto
Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646@kwansei.ac.jp
Last updated: Apr 25 2024 at 20:15 UTC