Consider the following property:
lemma "finite {t. (c,s) ⇒ t}"
Which refers to the following big step semantics:
inductive gbig_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP, s) ⇒ s"
| Assign: "(x ::= a, s) ⇒ s(x := aval a s)"
| Seq: "⟦(c1, s1) ⇒ s2; (c2, s2) ⇒ s3⟧ ⟹ (c1;;c2, s1) ⇒ s3"
| IfBlock: "⟦(b,c) ∈ set gcs; bval b s; (c,s) ⇒ s'⟧ ⟹ (IF gcs FI, s) ⇒ s'"
| DoTrue: "⟦(b,c) ∈ set gcs; bval b s1; (c,s1) ⇒ s2;(DO gcs OD,s2) ⇒ s3⟧
⟹ (DO gcs OD, s1) ⇒ s3"
| DoFalse: "⟦(∀ (b,c) ∈ set gcs. ¬ bval b s)⟧ ⟹ (DO gcs OD, s) ⇒ s"
To me it is obvious that the property holds by induction on the big step relation. However, I can not get it out of the set, so I cannot effectively induct on it.
How could I do this?
Finiteness is nothing that you could prove directly with the induction rule of an inductive predicate. The problem is that looking at an individual run (as does the induction rule) does not say anything about the branching behaviour, which must also be finite for the statement to hold.
I see two approaches to proving finiteness:
Model the derivation tree explicitly as a datatype in Isabelle/HOL and prove that it adequately represent the derivation trees behind inductive. Then prove that the tree has finitely many leaves (by induction on the tree). If you design the datatype such that the states in the leaves are a type parameter, then the corresponding set function generated by the datatype package is what you want to prove to be finite. (Note that you cannot prove finiteness by the induction rule of the set function, because that would again be just a single run.)
Look at the internal construction of the inductive definition. It is defined as the least fixpoint of a functional. You can get access to these internals by putting the inductive definition into a context in which [[inductive_internals]] is declared. Then you can prove that the functional preserves finiteness in a single step and then lift that through the induction.
The proof argument in both approaches is similar. The explicit datatype in #1 simply reifies the fixpoint argument of #2. So you can think of #1 as a deep embedding of #2. Of course, you can also re-derive the internal construction (in a more suitable format) just from the introduction and induction theorems and then follow approach #2.
I would try to do precisely this as your semantics is small. For a large real-world semantics, it might make sense to spend the effort to automate step #2 in ML.