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