Stream: Beginner Questions

Topic: Using keyword using

Gergely Buday (Mar 22 2023 at 10:33):

At Chained_Facts.thy there is a simple apply script

lemma
  "∃x::nat. x > 0"
  using zero_less_one
  apply (rule exI)
  done

demonstrating the chaining of the fact zero_less_one

I tried to transform this into a structured Isar proof but I could not prove my first goal in the forward proof:

lemma
  "∃x::nat. x > 0"
proof -
  have "(0::nat) < 1"
    using zero_less_one

How could I prove this with an elementary rule? by (rule ...)

waynee95 (Mar 22 2023 at 10:55):

You can do it like this

lemma "∃x::nat. x > 0"
proof -
  have "(0::nat) < 1"
    using zero_less_one .
  then show ?thesis by (rule exI)
qed

The . here means "immediate proof".

Alternatively, this works too

lemma "∃x::nat. x > 0"
proof -
  have "(0::nat) < 1"
    by (rule zero_less_one)
  then show ?thesis by (rule exI)
qed

Andrei Koltsov (Mar 25 2023 at 22:28):

I can not use datatype tree.
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
Then I try:
value "Node(Tip, 1, Tip)" or value "Node([], 1, [])" or something else like this. Evry time I have error masage. Hope
somebody can help me.

Zixuan Fan (Mar 26 2023 at 08:18):

You do not need a tuple for a datatype constructor, try

value "Node Tip (1::nat) Tip"
(*Still have to tell Isabelle the type of 1*)

If you want to use a tuple for the constructor, it may look like this

datatype 'a tree = Tip | Node "'a tree * 'a * 'a tree"

Wolfgang Jeltsch (Mar 26 2023 at 13:50):

Yes, data constructors in Isabelle/HOL use Currying.

Zakaria El mezamzi (Mar 29 2023 at 06:29):

El ladrón debió entrar por la puerta y uno de los sirvientes está implicado

Last updated: Dec 21 2024 at 16:20 UTC