src/HOL/Nominal/Examples/CR.thy

 
 lemma forget: 
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
 using asm
-proof (nominal_induct L avoiding: x P rule: lam.induct)
+proof (nominal_induct L avoiding: x P rule: lam.strong_induct)
   case (Var z)
   have "x\<sharp>Var z" by fact
   thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm)
 next 
   case (App M1 M2)

 
 lemma forget_automatic: 
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
   using asm 
-by (nominal_induct L avoiding: x P rule: lam.induct)
+by (nominal_induct L avoiding: x P rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
   fixes z::"name"
   assumes asms: "z\<sharp>N" "z\<sharp>L"
   shows "z\<sharp>(N[y::=L])"
 using asms
-proof (nominal_induct N avoiding: z y L rule: lam.induct)
+proof (nominal_induct N avoiding: z y L rule: lam.strong_induct)
   case (Var u)
   have "z\<sharp>(Var u)" "z\<sharp>L" by fact+
   thus "z\<sharp>((Var u)[y::=L])" by simp
 next
   case (App N1 N2)

 lemma fresh_fact_automatic: 
   fixes z::"name"
   assumes asms: "z\<sharp>N" "z\<sharp>L"
   shows "z\<sharp>(N[y::=L])"
   using asms 
-by (nominal_induct N avoiding: z y L rule: lam.induct)
+by (nominal_induct N avoiding: z y L rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact': 
   fixes a::"name"
   assumes a: "a\<sharp>t2"
   shows "a\<sharp>t1[a::=t2]"
 using a 
-by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma substitution_lemma:  
   assumes a: "x\<noteq>y"
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-proof (nominal_induct M avoiding: x y N L rule: lam.induct)
+proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
   case (Var z) (* case 1: Variables*)
   have "x\<noteq>y" by fact
   have "x\<sharp>L" by fact
   show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
   proof -

 
 lemma substitution_lemma_automatic:  
   assumes asm: "x\<noteq>y" "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
   using asm 
-by (nominal_induct M avoiding: x y N L rule: lam.induct)
+by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
 section {* Beta Reduction *}
 
 inductive

 
 lemma subst_rename: 
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
-by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma one_abs: 
   assumes a: "Lam [a].t\<longrightarrow>\<^isub>1t'"
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"

 
 lemma one_subst_aux:
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-proof (nominal_induct M avoiding: x N N' rule: lam.induct)
+proof (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
   case (Var y) 
   thus "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y") auto
 next
   case (App P Q) (* application case - third line *)
   thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1  (App P Q)[x::=N']" using o2 by simp

 
 lemma one_subst_aux_automatic:
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-by (nominal_induct M avoiding: x N N' rule: lam.induct)
+by (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
    (auto simp add: fresh_prod fresh_atm)
 
 lemma one_subst: 
   assumes a: "M\<longrightarrow>\<^isub>1M'"
   and     b: "N\<longrightarrow>\<^isub>1N'"