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

It was a question of the other day, but was settled by oneself by using "case_tac".
I am sorry if I had you already reply it.
I will keep trying my best.

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

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


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