## Stream: Beginner Questions

### Topic: ✔ Simple proof for inductive definition

#### Matthias Hetzenberger (Sep 14 2022 at 10:53):

I am trying to formalize well-formed first-order terms and am stuck at the following lemma, that says that every variable is a well-formed first-order term:

datatype 'b FOTerm =
is_Var: Var "string" |
is_Fun: Fun (symbol: 'b) (args: "'b FOTerm list")

inductive WF_FOTerm :: "('a ⇒ bool) ⇒ ('a ⇒ nat) ⇒ 'a FOTerm ⇒ bool"
for fun_symbol :: "'a ⇒ bool" and
fun_arity :: "'a ⇒ nat"
where var_wf: "is_Var t ⟹ WF_FOTerm fun_symbol fun_arity t"
| fun_wf: "is_Fun t ⟹
fun_symbol (symbol t) ⟹
list_all (WF_FOTerm fun_symbol fun_arity) (args t) ⟹
length (args t) = fun_arity (symbol t) ⟹
WF_FOTerm fun_symbol fun_arity t"

lemma "WF_FOterm fun_symbol fun_arity (Var var_name)"

Though I feel that this is really simple, also Sledgehammer has no clue how to prove this. Does anyone have a hint for me?

#### Simon Roßkopf (Sep 14 2022 at 10:56):

WF_FOtermshould be WF_FOTermin your lemma. Then you can prove it (for example by (rule var_wf) simp) or sledgehammer finds a proof

#### waynee95 (Sep 14 2022 at 10:57):

It seems there is a typo in the lemma.

lemma "WF_FOTerm fun_symbol fun_arity (Var var_name)"

#### Matthias Hetzenberger (Sep 14 2022 at 10:58):

Oh well, looks like I wasted an hour there for nothing. Thank you very much!

#### Lukas Stevens (Sep 14 2022 at 10:58):

Free variables are shown in blue btw. This means that something is wrong if a term is printed in blue that should not be a free variable.

#### Notification Bot (Sep 14 2022 at 10:58):

Matthias Hetzenberger has marked this topic as resolved.

#### Matthias Hetzenberger (Sep 14 2022 at 10:59):

Lukas Stevens said:

Free variables are shown in blue btw. So if a term, that should not be a free variable, is printed in blue something is wrong.

Thanks, I will keep this in mind from now on.

Last updated: Feb 27 2024 at 08:17 UTC