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)"
  by (simp add: var_wf)

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: Dec 21 2024 at 12:33 UTC