datatype t =
  TTrue
  | FFalse
  | Zero
  | Succ t
  | Pred t
  | IsZero t
  | IfElse t t t ("If _ Then _ Else _" [85,85,85] 80)

(* 3.2.5 *)
fun terms :: "nat ⇒ t set" where
"terms 0 = {}" |
"terms (Suc n) =
  {TTrue,FFalse,Zero}
  ∪ {Succ t | t. t ∈ terms n} ∪ {Pred t | t. t ∈ terms n} ∪ {IsZero t | t. t ∈ terms n}
  ∪ {IfElse t1 t2 t3 | t1 t2 t3. t2 ∈ terms n ∧ t2 ∈ terms n ∧ t3 ∈ terms n}"

lemma "terms n ⊆ terms (Suc n)"

proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  have "⋀t. t ∈ terms (Suc n) ⟹ t ∈ terms (Suc (Suc n))"
    sorry
  then show ?case
    by blast
qed

(* 3.2.5 *)
fun terms :: "nat ⇒ t set" where
"terms 0 = {}" |
"terms (Suc n) =
  {TTrue,FFalse,Zero}
  ∪ {Succ t | t. t ∈ terms n} ∪ {Pred t | t. t ∈ terms n} ∪ {IsZero t | t. t ∈ terms n}
  ∪ {IfElse t1 t2 t3 | t1 t2 t3. let termsn = terms n in t1 ∈ termsn ∧ t2 ∈ termsn ∧ t3 ∈ termsn}"

lemma succ: "Succ t ∈ terms (Suc n) ⟷ t ∈ terms n"
  by (induction n) auto

lemma pred: "Pred t ∈ terms (Suc n) ⟷ t ∈ terms n"
  by (induction n) auto

lemma iszero: "IsZero t ∈ terms (Suc n) ⟷ t ∈ terms n"
  by (induction n) auto

lemma ifelse: "IfElse t1 t2 t3 ∈ terms (Suc n) ⟷ t1 ∈ terms n ∧ t2 ∈ terms n ∧ t3 ∈ terms n"
  by (induction n) auto

lemma "terms n ⊆ terms (Suc n)"
proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  have "t ∈ terms (Suc n) ⟹ t ∈ terms (Suc (Suc n))" for t
  proof (induction t)
    case (Succ t)
    then show ?case
      using Suc.IH
      by (meson in_mono succ)
  next
    case (Pred t)
    then show ?case
      using Suc.IH
      by (meson in_mono pred)
  next
    case (IsZero t)
    then show ?case
      using Suc.IH
      by (meson in_mono iszero)
  next
    case (IfElse t1 t2 t3)
    then show ?case
      using Suc.IH
      by (meson in_mono ifelse)
  qed auto
  then show ?case
    by blast
qed