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?

`WF_FOterm`

should be `WF_FOTerm`

in your lemma. Then you can prove it (for example ```
by (rule var_wf) simp
```

) or sledgehammer finds a proof

It seems there is a typo in the lemma.

```
lemma "WF_FOTerm fun_symbol fun_arity (Var var_name)"
by (simp add: var_wf)
```

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

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.

Matthias Hetzenberger has marked this topic as resolved.

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: Oct 12 2024 at 20:18 UTC