Proof on inductive sets

Question

I am trying to wrap my brain around proofs on inductive sets and I am failing miserably. This is what I have so far:

theory MyTheory

imports Main
begin

inductive_set S where
  emptyI: "{} ∈ S" | 
  insertI: "A ∈ S ⟹ insert a A ∈ S"

definition plus :: "'a set set ⇒ 'a set set ⇒ 'a set set" (infixl "❙+" 100) where 
  "a ❙+ b = a ∪ b"
definition zero :: "'a set set" ("❙0") where 
  "❙0 = {}"

locale myLocale = 
  fixes f :: "'a set set ⇒ 'a set set"
  assumes f_zero: "f ❙0 = ❙0"
      and f_plus: "f (a ∪ b) = f a ∪ f b"
      and a_fin: "⋀a::'a set set. finite a"
begin

lemma 
  assumes "a ∈ S" "a = ⋃{{x}| x. x ∈ a}" "finite a"
  shows "f a = ⋃{f {x}| x. x ∈ a}"
proof cases 
case emptyI
  show ?thesis sorry
next
case (insertI A a)
  show ?thesis sorry
qed
end

I don't understand how to use the S.cases or S.induct in the proof, as described in Mr. Ballarin's example in Inductive Definitions (Slide 22).

With proof cases (or proof induct), my example definitely doesn't work:

Proof outline with cases:
  case True
  then show ?thesis sorry
next
  case False
  then show ?thesis sorry
qed

What am I missing?

LE: Oooh... I figured it out (digging more around for Mr. Ballarin's Demos on that tutorial!) What I was missing was the "anchoring" of the induction to the assumption "a ∈ S". Fixed it and all is well in my world now.

lemma 
  assumes **a0:** "a ∈ S" "a = ⋃{{x}| x. x ∈ a}" "finite a"
  shows "f a = ⋃{f {x}| x. x ∈ a}"
  **using a0**
proof cases 
case emptyI
  show ?thesis sorry
next
case (insertI A a)
  show ?thesis sorry
qed