Stream: Beginner Questions

Topic: How to structure proofs with inductive sets with parameters?

James Hanson (Mar 29 2024 at 21:22):

I'm having difficulty figuring out how to structure a proof involving an inductive set or predicate with a parameter when there is more than one instance of the set or predicate involved. Here's a toy example of what I'm talking about:

inductive
  A :: "'b set => 'b list => bool"
  for
    B :: "'b set"
  where "A B []"
      | "[| b \<in> B; A B bs |] ==> A B (b#bs)"

lemma A_monotonic:
  assumes
    B_subset_C: "B \<subseteq> C"
  shows
    "A B x ==> A C x"
proof -
  oops

(Obviously this is not a good way to define this set, which would just be {bs. set bs \<subseteq> B} but this kind of definition seems to make sense in my actual project.)
How would you go about proving this?

James Hanson (Mar 31 2024 at 20:50):

I realized that I didn't correctly identify what my problem was, which actually had to do with matching types in the statement of a lemma about mutually inductive sets with implicit type parameters.

For the record, here is a proof for my toy example:

inductive
  A :: "'b set => 'b list => bool"
  for
    B :: "'b set"
    where "A B []"
    | "[| b \<in> B; A B bs |] ==> A B (b#bs)"

lemma A_monotonic:
  assumes
    B_subset_C: "B \<subseteq> C"
  shows
    "A B x ==> A C x"
proof (induct rule: A.induct)
  case 1
  then show ?case
    using A.intros(1) by auto
next
  case (2 b bs)
  then show ?case
    by (meson A.intros(2) assms in_mono)
qed

Last updated: May 19 2024 at 08:18 UTC