src/HOL/Induct/QuoNestedDataType.thy

 theory QuoNestedDataType imports Main begin
 
 subsection{*Defining the Free Algebra*}
 
 text{*Messages with encryption and decryption as free constructors.*}
-datatype
+datatype_new
      freeExp = VAR  nat
              | PLUS  freeExp freeExp
              | FNCALL  nat "freeExp list"
+
+datatype_compat freeExp
 
 text{*The equivalence relation, which makes PLUS associative.*}
 
 text{*The first rule is the desired equation. The next three rules
 make the equations applicable to subterms. The last two rules are symmetry

 
 text{*Proving that it is an equivalence relation*}
 
 lemma exprel_refl: "X \<sim> X"
   and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
-  by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+
+  by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct)
+    (blast intro: exprel.intros listrel.intros)+
 
 theorem equiv_exprel: "equiv UNIV exprel"
 proof -
   have "refl exprel" by (simp add: refl_on_def exprel_refl)
   moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)

 done
 
 lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
 apply (cases Xs rule: eq_Abs_ExpList) 
 apply (simp add: FnCall)
-apply (induct_tac Us) 
+apply (induct_tac Us)
 apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
 done
 
 lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}" 
 by simp

   shows "P1 exp" and "P2 list"
 proof -
   obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp)
   obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList)
   have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)"
-  proof (induct U and Us)
+  proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct)
     case (VAR nat)
     with V show ?case by (simp add: Var_def) 
   next
     case (PLUS X Y)
     with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"]