Email Gateway (Aug 18 2022 at 20:16): Email Gateway (Aug 18 2022 at 20:16):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
Dear Sirs/Madams,
My name is Yuki Goto and I am a graduate school student in Kwansei Gakuin University in Japan.
The reason why I am writing this email to you is I'd like to ask some questions about Isabelle/hol.
datatype
char = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z |Dot
type_synonym str = "char list"
fun str_eq :: "str => str => bool" where
"str_eq [] _ = True" |
"str_eq _ [] = True" |
"str_eq (x#xs) (y#ys) = ( (x=y) & (str_eq xs ys))"
fun simp_hd_eq :: "str list => str => bool" where
"simp_hd_eq [] y = False" |
"simp_hd_eq (x#xs) y = (if (str_eq x y) then True else (simp_hd_eq xs y) )"
lemma simp_add_nq : "(simp_hd_eq xs y) = False & (simp_hd_eq ys y) = False ==> (simp_hd_eq (xs @ ys) y) = False"
This is the first question and I cannot prove this lemma.
Probably I think that I am self-evident, how can you prove it?
lemma simp_hd_eq_app[simp] : "(simp_hd_eq xs y) = True ==> (simp_hd_eq (xs @ ys) y) = True"
apply simp
When I was going to carry out "apply simp" in this "lemma", the second question is why "Proof General" freezes.
Can you shed any light on this?
In addition, I want to know whether Isabelle/hol is suitable for "String" and whether there is an example using "String".
I wish to thank you in advance for answering these questions,
Sincerely,
Yuki Goto
Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646@kwansei.ac.jp
Email Gateway (Aug 18 2022 at 20:16):From: Brian Huffman <huffman@in.tum.de>
On Thu, Jun 28, 2012 at 3:38 AM, 後藤 裕貴 <auf75646@kwansei.ac.jp> wrote:
datatype
char = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z |Dottype_synonym str = "char list"
fun simp_hd_eq :: "str list => str => bool" where
"simp_hd_eq [] y = False" |
"simp_hd_eq (x#xs) y = (if (str_eq x y) then True else (simp_hd_eq xs y) )"lemma simp_add_nq : "(simp_hd_eq xs y) = False & (simp_hd_eq ys y) = False ==> (simp_hd_eq (xs @ ys) y) = False"
This is the first question and I cannot prove this lemma.
Probably I think that I am self-evident, how can you prove it?
This lemma cannot be proved by simplification alone; it requires
induction: "apply (induct xs) apply auto" should do it.
lemma simp_hd_eq_app[simp] : "(simp_hd_eq xs y) = True ==> (simp_hd_eq (xs @ ys) y) = True"
apply simp
"apply (induct xs) apply auto" should work here too.
When I was going to carry out "apply simp" in this "lemma", the second question is why "Proof General" freezes.
Can you shed any light on this?
It doesn't freeze for me. You might try turning off "auto quickcheck"
or similar tools if they are enabled.
Hope this helps,
Email Gateway (Aug 18 2022 at 20:19):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
Dear Mr. Huffman,
Thank you very much for your help.
The cause of the "simp freeze" seemed to be "lemma" before it.
This later proof was proved by a method according to advice well
Causative "lemma" is the following thing.
lemma app_test_n[simp] :
"~ ( (simp_hd_eq xs y) = True | (simp_hd_eq ys y) = True )
==> ((simp_hd_eq xs y) = False) & ( (simp_hd_eq ys y) = False) "
apply simp
done
I think that "lemma" which caused it cannot be established.
In spite of it, the proof is completed.
Which point will it be if caused by a definition of "simp_hd_eq"?
It would be nice if you could reply.
Yuki Goto
Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646@kwansei.ac.jp
On Thu, Jun 28, 2012 at 3:38 AM, 後藤 裕貴 <auf75646@kwansei.ac.jp> wrote:
datatype
char = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z |Dottype_synonym str = "char list"
fun simp_hd_eq :: "str list => str => bool" where
"simp_hd_eq [] y = False" |
"simp_hd_eq (x#xs) y = (if (str_eq x y) then True else (simp_hd_eq xs y) )"lemma simp_add_nq : "(simp_hd_eq xs y) = False & (simp_hd_eq ys y) = False ==> (simp_hd_eq (xs @ ys) y) = False"
This is the first question and I cannot prove this lemma.
Probably I think that I am self-evident, how can you prove it?
This lemma cannot be proved by simplification alone; it requires
induction: "apply (induct xs) apply auto" should do it.
lemma simp_hd_eq_app[simp] : "(simp_hd_eq xs y) = True ==> (simp_hd_eq (xs @ ys) y) = True"
apply simp
"apply (induct xs) apply auto" should work here too.
When I was going to carry out "apply simp" in this "lemma", the second question is why "Proof General" freezes.
Can you shed any light on this?
It doesn't freeze for me. You might try turning off "auto quickcheck"
or similar tools if they are enabled.
Hope this helps,
Email Gateway (Aug 19 2022 at 07:49):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
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?
Yuki
Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646@kwansei.ac.jp
Email Gateway (Aug 19 2022 at 07:50):From: Lars Noschinski <noschinl@in.tum.de>
I would probably proceed by proving that
"prefix_app xs y = map (%z. y @ z) xs"
holds and that "%z. y @ z" is injective. Then the proposition follows
from List.distinct_map.
-- Lars
Email Gateway (Aug 19 2022 at 08:00):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
Thank you for an answer.
According to the indication,
definition
"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.
datatype
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@kwansei.ac.jp
Email Gateway (Aug 19 2022 at 08:00):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Goto-san,
On 07/28/2012 12:30 PM, 後藤 裕貴 wrote:
It is the question about applying "map" to "Datatype" definition this time.
datatype
char = A | B | C | D | E | Ftype_synonym str = "char list"
type_synonym FileName = str
datatype Gvar = GV Type str
Here Type is not defined. so I use
datatype Gvar = GV str
instead.
type_synonym GvarList = "Gvar list"
type_synonym Prog = "(FileName * GvarList * Funcs * Main)"
Here I just removed Funcs and Main, i.e.,
type_synonym Prog = "(FileName * GvarList)"
Now your function-definition still results in a syntax error.
fun gvar_changename :: "Prog =>GvarList => GvarList" where
"gvar_changebname pr1 xs = map (%(GV x y). (GV x (fst pr1)@y)) xs"
The point is that pattern matching does not work in general as part of
lambda abstractions (only for special cases, like pairs). So you have to
use a case-expression, e.g., as follows:
fun gvar_changename :: "Prog => GvarList => GvarList" where
"gvar_changename pr1 xs =
map (%x. case x of GV y => GV (fst pr1 @ y)) xs"
(Also note that the paranthesization in your original definition is not
right, it should be "GV x (fst pr1 @ y)"; and you have to use the same
name for your function at every occurrence, cf. "gvar_changename" vs.
"gvar_changebname".)
cheers
chris
Email Gateway (Aug 19 2022 at 08:02):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
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
datatype
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
Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646@kwansei.ac.jp
Email Gateway (Aug 19 2022 at 08:06):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
I think that the problem is that your lemma "app_test_n" has been
declared [simp]. This rule is looping the simplifier (causing it to do
busy-work with no progress). Note that Isabelle making no progress is
different to Proof General crashing. You can probably still interrupt
Isabelle and carry on.
When rules of the form "P ==> Q & R" are added with [simp], the
simplifier sees that as a recipe for showing Q or R by attempting to
show P. In your case, Q == R and P can be simplified back to Q, which
can then be attempted with the rule again, thus the loop. Care needs to
be taken when adding "conditional rewrite rules" of the form "P ==> Q"
to the simplifier.
In this case, what was the point? Why make this a [simp] rule when the
simplifier knows how to show this anyway?
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 08:27):From: 後藤 裕貴 <auf75646@kwansei.ac.jp>
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@kwansei.ac.jp
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
datatype
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
Last updated: May 06 2024 at 20:16 UTC