Email Gateway (Aug 18 2022 at 10:44): Email Gateway (Aug 18 2022 at 10:44):From: Lucas Cavalcante <thesupervisar@gmail.com>
1st.:
Is there some "For-Newbie Forum/Chat" about Isabelle? I think most of my
questions are about how to proceed more than how Isabelle works.
Forgive me for that.
2nd.:
Once I need to apply induction in a variable with 'bool' datatype I need to
'measure' this variable when using recdef. Is there a way how to make it by
using primrec, or i will need recdef?
If recdef is needed, i will need 'measure'. Thus I need the function to
define itself.
I was trying something like that:
consts f :: "bool => nat"
primrec
"f (~P) = 1 + f P"
"f (P->Q) = 1 + f P + f Q"
... (the other conectives, like &, | and <->)
"f P = 0"
But it says there is a constructor missing. (Then I began to use recdef)
3rd.:
Consider the following function:
consts sum1 :: '[nat,nat] => nat"
primrec
"sum1 m 0 = m"
"sum1 m (Suc n) = sum1 (Suc m) n"
Then I try to prove:
lemma 1: "sum 0 n = n"
by
apply (induct_tac n, auto)
resulting this:
!!n. sum1 0 n = n ==> sum1 (Suc 0) n = Suc n
but this remaing stage seems trivial by definition of sum1.
Is 'auto' instead other more specific methods a mistake?
Doesn't Isabelle allow the Complete Induction?
Thank You
Lucas
Email Gateway (Aug 18 2022 at 10:44):From: Tobias Nipkow <nipkow@in.tum.de>
It does not follow trivially - you have no defn or lemma which tells
you what "sum1 (Suc 0) n" is. You need to prove such lemmas first.
Tobias
Email Gateway (Aug 18 2022 at 10:44):From: Stefan Berghofer <berghofe@in.tum.de>
Lucas Cavalcante wrote:
It seems that you are confusing the datatype "bool" with the datatype of
boolean formulae. Note that for example the term "(~ True) --> False" of
type "bool" is equivalent to the term "True", but the above function would
map the former term to 2 and the latter to 0. Therefore, such a function
cannot exist. While the datatype "bool" just consists of the two constructors
"True" and "False", the datatype of boolean formulae could be defined as follows:
datatype form = TT | FF | Neg form | Impl form form | And form form | Or form form | ...
Note that the datatype package already provides a "size" function for this
datatype automatically.
Greetings,
Stefan
Last updated: May 03 2024 at 04:19 UTC