Unable to figure out induct rule for mutually recursive predicates

Question

Can you suggest how to apply an induction rule to the following lemma?

datatype 'a expr =
  Literal "'a literal_expr"
| Var "string"
and 'a literal_expr =
  NullLiteral
| CollectionLiteral "'a collection_literal_part_expr list"
and 'a collection_literal_part_expr =
  CollectionItem "'a expr"

datatype 'a type = OclVoid | Set "'a type"

inductive typing and collection_parts_typing where
  "typing Γ (Literal NullLiteral) OclVoid"
| "collection_parts_typing Γ prts τ ⟹
   typing Γ (Literal (CollectionLiteral prts)) (Set τ)"
| "collection_parts_typing Γ [] OclVoid"
| "⟦typing Γ a τ; collection_parts_typing Γ xs σ⟧ ⟹
   collection_parts_typing Γ (CollectionItem a # xs) σ"

lemma
  "typing Γ1 expr τ1 ⟹ typing Γ1 expr σ1 ⟹ τ1 = σ1" and
  "collection_parts_typing Γ2 prts τ2 ⟹
   collection_parts_typing Γ2 prts σ2 ⟹ τ2 = σ2"
  apply (induct expr and prts)
  apply (induct rule: typing_collection_parts_typing.inducts)

The following questions contains a very simple examples:

• How to prove lemmas for mutually recursive types?
• How to fix "Illegal schematic variable(s)" in mutually recursive rule induction?

But my example is more complicated. And I can't understand what's wrong with my datatypes, predicates or lemmas. This exact theory can be reformulated without mutual recursion. But it's just a small fragment of my actual theory.

Answer 1

There exists a plausible solution that is similar to the one provided in the accepted answer to your previous question. Please note that I changed some of the names of some of the elements in your definitions and that I relied heavily on sledgehammer to bring the proof to a conclusion.

datatype 'a expr =
  Literal "'a literal_expr"
| Var "string"
and 'a literal_expr =
  NL
| CL "'a clpe list"
and 'a clpe = CI "'a expr"

datatype 'a type = OclVoid | Set "'a type"

inductive typing and cpt where
  "typing Γ (Literal NL) OclVoid"
| "cpt Γ prts τ ⟹ typing Γ (Literal (CL prts)) (Set τ)"
| "cpt Γ [] OclVoid"
| "⟦typing Γ a τ; cpt Γ xs σ⟧ ⟹ cpt Γ (CI a # xs) σ"

lemma
  fixes Γ1 Γ2 :: 'a
    and expr :: "'b expr"
    and prts :: "'b clpe list"
    and σ1 τ1 σ2 τ2 :: "'c type"
  shows 
    "typing Γ1 expr τ1 ⟹ typing Γ1 expr σ1 ⟹ τ1 = σ1" and
    "cpt Γ2 prts τ2 ⟹ cpt Γ2 prts σ2 ⟹ τ2 = σ2"
  apply(
      induction Γ1 expr τ1 and Γ2 prts τ2 
      arbitrary: σ1 and σ2 
      rule: typing_cpt.inducts
      )
  subgoal by (blast dest: typing.cases)
  subgoal 
    by (metis 
        expr.inject(1) 
        literal_expr.distinct(1) 
        literal_expr.inject 
        typing.cases)
  subgoal by (blast dest: cpt.cases)
  subgoal by (metis cpt.cases list.discI list.sel(3))
  done

---

Isabelle version: Isabelle2020