Email Gateway (Aug 18 2022 at 11:33): Email Gateway (Aug 18 2022 at 11:33):From: Ruben Henner Zilibowitz <rzilibowitz@yahoo.com.au>
Just trying to learn isabelle and had trouble with the following:
primrec
"checksort (x#y#zs) = ((x <= y) \<and> (checksort (y#zs)))"
"checksort _ = True"
The error is: "illegal argument in pattern". If someone could explain
why this causes an error or how to repair it I'd appreciate that very
much.
Cheers,
Ruben
Email Gateway (Aug 18 2022 at 11:33):From: Stefan Berghofer <berghofe@in.tum.de>
Ruben Henner Zilibowitz wrote:
Patterns containing "_" are currently not supported by primrec. You
can repair your definition by replacing "_" by a variable, e.g. x.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 11:33):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,
Ruben Henner Zilibowitz wrote:
primrec only supports primitive recursion, i.e. pattern matching on
lists must emply only the patterns (x#xs) and []. In your
specification, you could get along by using explicit case distinction on
the right hand side:
consts checksort :: "'a::order list => bool"
primrec
"checksort (x#xs) <-> (case xs of y # _ => x <= y & checksort xs | _
=> True)"
"checksort [] = True"
Alternativly, consider the "function" command.
Hope this helps,
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 12:30):From: Ruben Henner Zilibowitz <rzilibowitz@yahoo.com.au>
Hi,
I'm still learning Isabelle. I'm trying to prove the lemma named
"my_lemma" at the bottom of this file but can't. If someone could give
me a hint that would be great.
Regards,
Ruben
(* Title: Stuff.thy
Author: Ruben Zilibowitz
2008
*)
header {* Stuff *}
theory Stuff imports Main begin
consts
factorial :: "nat \<Rightarrow> nat"
primrec
"factorial 0 = 1"
"factorial (Suc n) = (Suc n) * (factorial n)"
lemma positive_factorial [simp]: "factorial n \<ge> 1"
apply (induct_tac n)
apply auto
done
lemma [simp]: "factorial n \<le> factorial (n+1)"
apply (induct_tac n)
apply auto
done
lemma [simp]: "\<forall> n. n > (0::nat) \<Longrightarrow> n \<le>
factorial n"
apply (induct_tac n)
apply auto
done
lemma [simp]: "n = 0 \<Longrightarrow> n \<le> factorial n" by simp
lemma my_lemma [simp]: "n \<le> factorial n"
apply (case_tac n)
apply auto
done
end
Email Gateway (Aug 18 2022 at 12:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Ruben,
The issue is that you have first to do induction and then case
distinction on the induction variable. See attached theory, to which I
have added further comments.
Hope this helps
Florian
Fac.thy
florian_haftmann.vcf
signature.asc
Last updated: May 03 2024 at 01:09 UTC