src/HOL/Nominal/Examples/CR.thy

 by (nominal_induct M avoiding: x y N L rule: lam.induct)
    (auto simp add: fresh_fact forget)
 
 section {* Beta Reduction *}
 
-inductive2
+inductive
   "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
 where
     b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
   | b2[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
   | b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"

 equivariance Beta
 
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
-inductive2
+inductive
   "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
 where
     bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
   | bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
 

 using a2 a1
 by (induct) (auto)
 
 section {* One-Reduction *}
 
-inductive2
+inductive
   One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
 where
     o1[intro!]:      "M\<longrightarrow>\<^isub>1M"
   | o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)"
   | o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"

 equivariance One
 
 nominal_inductive One
   by (simp_all add: abs_fresh fresh_fact')
 
-inductive2
+inductive
   "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
 where
     os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M"
   | os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3"
 

   and      a :: "name"
   assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
   using a
   apply -
-  apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
+  apply(ind_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
   apply(auto simp add: lam.inject alpha)
   apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   apply(rule conjI)
   apply(perm_simp)
   apply(simp add: fresh_left calc_atm)

   assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
   shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
          (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   using a
   apply -
-  apply(ind_cases2 "App t1 t2 \<longrightarrow>\<^isub>1 t'")
+  apply(ind_cases "App t1 t2 \<longrightarrow>\<^isub>1 t'")
   apply(auto simp add: lam.distinct lam.inject)
   done
 
 lemma one_red: 
   assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M"
   shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
          (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   using a
   apply -
-  apply(ind_cases2 "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
+  apply(ind_cases "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
   apply(simp_all add: lam.inject)
   apply(force)
   apply(erule conjE)
   apply(drule sym[of "Lam [a].t1"])
   apply(simp)