Stream: Beginner Questions

Topic: Starting a induction with in a larger proof

Yiming Xu (Dec 23 2024 at 09:50):

Relevant definitions:

definition gen_birel :: "'m set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ ('a ×  'a) set"
  where
"gen_birel Op R = {(w,u). ∃m ul. m ∈ Op ∧ R m (w # ul) ∧ u ∈ list.set ul}"

definition rset :: "'a set ⇒ ('a ⇒ 'b list ⇒ bool)  ⇒ 'b set"
  where
"rset τ R =  {v. ∃m vl. m ∈ τ ∧ R m vl ∧ v ∈ set vl}"

definition tree :: "'m set ⇒ (('m ⇒ 'a list ⇒ bool)) ⇒ 'a ⇒ bool" where
"tree τ R r ≡
 r ∈ rset τ R ∧
 (∀t. t ∈ rset τ R ⟶ (r,t) ∈ (gen_birel τ R)⇧*) ∧
 (∀t. t ∈ rset τ R ⟶ t ≠ r ⟶

  (∀m1 m2 w1 w2 wl1 wl2.
    R m1 (w1 # wl1) ∧ t ∈ set wl1 ⟶
    R m2 (w2 # wl2) ∧ t ∈ set wl2 ⟶
    m1 = m2 ∧ wl1 = wl2)) ∧
 (∀t. t ∈ rset τ R ⟶ (t,t) ∉ (gen_birel τ R)⇧+)"



inductive_set generated_set :: "'m set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ 'a set ⇒ 'a set"
  for Op :: "'m set" and R :: "'m ⇒ 'a list ⇒ bool" and X :: "'a set"
  where
   "x ∈ X ⟹ x ∈ generated_set Op R X"
 | "w ∈ generated_set Op R X ⟹ m ∈ Op ⟹
    R m (w # ul) ⟹ u ∈ list.set ul ⟹ u ∈ generated_set Op R X"

I have a goal:

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof -
  have "⋀x. x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R"
  proof (induction rule: generated_set.induct)

And the line (induction rule: generated_set.induct) reports error:

Failed to apply initial proof method⌂:
goal (1 subgoal):
 1. ⋀x. x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R

May I please ask for a correct way of doing it? I guess this is because I have only binded x, but the induction principle has four meta-quantifiers. But how can I turn this x into a meta variable?

Yiming Xu (Dec 23 2024 at 09:52):

I know I can do:
lemma tree_rset:
assumes "tree τ R r"
and xgs: "x ∈ generated_set Op R {r}"
shows " x ∈ rset τ R" using xgs
proof (induction rule: generated_set.induct)

But I do not want a separate lemma for this.

irvin (Dec 23 2024 at 12:15):

could this work?

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof (rule set_eqI)
  fix  x
  have 1:"x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R"
  proof (induction rule: generated_set.induct)
    case (1 x)
    then show ?case sorry
  next
    case (2 w m ul u)
    then show ?case sorry
  qed
  moreover have 2:"x ∈ rset τ R ⟹ x ∈ generated_set Op R {r}"
    sorry
  ultimately show "(x ∈ rset τ R) = (x ∈ generated_set Op R {r})"
    by blast
qed

irvin (Dec 23 2024 at 12:25):

Btw if you dont like repeating assms you can also open a context like this

context
  fixes τ R r
  assumes "tree τ R r"
begin

lemma 1:"x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R"
  sorry

end
thm 1 (*tree ?τ ?R ?r ⟹ ?x ∈ generated_set ?Op ?R {?r} ⟹ ?x ∈ rset ?τ ?R*)

Balazs Toth (Dec 23 2024 at 12:46):

Another possiblity of doing it:

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof-

  {
    fix x
    assume "x ∈ generated_set Op R {r}"
    then have "x ∈ rset τ R"
    proof (induction rule: generated_set.induct)
      case (1 x)
      then show ?case sorry
    next
      case (2 w m ul u)
      then show ?case sorry
    qed

  }

  then show ?thesis
    sorry
qed

Yiming Xu (Dec 23 2024 at 12:48):

irvin said:

could this work?

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof (rule set_eqI)
  fix  x
  have 1:"x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R"
  proof (induction rule: generated_set.induct)
    case (1 x)
    then show ?case sorry
  next
    case (2 w m ul u)
    then show ?case sorry
  qed
  moreover have 2:"x ∈ rset τ R ⟹ x ∈ generated_set Op R {r}"
    sorry
  ultimately show "(x ∈ rset τ R) = (x ∈ generated_set Op R {r})"
    by blast
qed

Yes that works! Thanks and the context trick would be useful as well!

Yiming Xu (Dec 23 2024 at 12:49):

Balazs Toth said:

Another possiblity of doing it:

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof-

  {
    fix x
    assume "x ∈ generated_set Op R {r}"
    then have "x ∈ rset τ R"
    proof (induction rule: generated_set.induct)
      case (1 x)
      then show ?case sorry
    next
      case (2 w m ul u)
      then show ?case sorry
    qed

  }

  then show ?thesis
    sorry
qed

Thanks! I see, that is one useful aspect for the "{}" syntax you told me before.

Mathias Fleury (Dec 23 2024 at 14:50):

Yiming Xu said:

have "x ∈ rset τ R"

I prefer the have-syntax

have "x ∈ rset τ R" if "x ∈ generated_set Op R {r}" for x
  using that

but this is personal preference

Yiming Xu (Dec 23 2024 at 14:57):

Mathias Fleury said:

Yiming Xu said:

have "x ∈ rset τ R"

I prefer the have-syntax

have "x ∈ rset τ R" if "x ∈ generated_set Op R {r}" for x
  using that

but this is personal preference

I see. It rephrases

have "⋀x. x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R"
  proof (induction rule: generated_set.induct)

I have not seen this syntax before. In particular I do not know there is something called "that"!

 lemma tree_rset:
  assumes t:"tree τ R r"
  shows "rset τ R = generated_set τ R {r}"
proof -
have "x ∈ rset τ R" if "x ∈ generated_set τ R {r}" for x
  using that
proof (induction rule: generated_set.induct)

also works. Thanks!

Balazs Toth (Dec 23 2024 at 20:33):

My personally preferred way is this one:

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof(intro set_eqI iffI)
  fix x
  assume "x ∈ generated_set Op R {r}"

  then show "x ∈ rset τ R"
  proof (induction rule: generated_set.induct)
    case (1 x)
    then show ?case sorry
  next
    case (2 w m ul u)
    then show ?case sorry
  qed
next
  fix x
  assume "x ∈ rset τ R"
  then show "x ∈ generated_set Op R {r}"
    sorry
qed

Yiming Xu (Dec 24 2024 at 16:54):

Balazs Toth said:

My personally preferred way is this one:

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof(intro set_eqI iffI)
  fix x
  assume "x ∈ generated_set Op R {r}"

  then show "x ∈ rset τ R"
  proof (induction rule: generated_set.induct)
    case (1 x)
    then show ?case sorry
  next
    case (2 w m ul u)
    then show ?case sorry
  qed
next
  fix x
  assume "x ∈ rset τ R"
  then show "x ∈ generated_set Op R {r}"
    sorry
qed

This looks very neat! Thanks!

Mathias Fleury (Dec 24 2024 at 16:57):

Yiming Xu said:

Mathias Fleury said:

Yiming Xu said:

have "x ∈ rset τ R"

I prefer the have-syntax

have "x ∈ rset τ R" if "x ∈ generated_set Op R {r}" for x
  using that

but this is personal preference

I see. It rephrases

have "⋀x. x ∈ generated_set Op R {r} ⟹ x ∈ rset τ R"
  proof (induction rule: generated_set.induct)

I have not seen this syntax before. In particular I do not know there is something called "that"!

 lemma tree_rset:
  assumes t:"tree τ R r"
  shows "rset τ R = generated_set τ R {r}"
proof -
have "x ∈ rset τ R" if "x ∈ generated_set τ R {r}" for x
  using that
proof (induction rule: generated_set.induct)

also works. Thanks!

you can also name the assumptions and just use this name instead. In Isabelle there there are two things called that: the assumptions of a haveand the property of an obtain.

Mathias Fleury (Dec 24 2024 at 16:58):

Balazs Toth said:

My personally preferred way is this one:

lemma tree_rset:
  assumes "tree τ R r"
  shows "rset τ R = generated_set Op R {r}"
proof(intro set_eqI iffI)
  fix x
  assume "x ∈ generated_set Op R {r}"

  then show "x ∈ rset τ R"
  proof (induction rule: generated_set.induct)
    case (1 x)
    then show ?case sorry
  next
    case (2 w m ul u)
    then show ?case sorry
  qed
next
  fix x
  assume "x ∈ rset τ R"
  then show "x ∈ generated_set Op R {r}"
    sorry
qed

for this proof, it look like the best approach (I would name the LHS and the RHS of the equality and use that name however)

Yiming Xu (Dec 25 2024 at 21:47):

I see. Thanks for all these elabouration!

Last updated: Feb 01 2025 at 20:19 UTC