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_FOTermin 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: Dec 07 2023 at 20:16 UTC