src/HOL/Nominal/Examples/Class2.thy

 proof (nominal_induct B rule: ty.strong_induct)
   case (PR X)
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(perm_simp)
     done
   next
     case 2 show ?case
       apply -
       apply(simp only: NEGc_simps)
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(simp add: lfp_eqvt)
       apply(simp add: comp_def)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(perm_simp)
       done
   }
 next

   have ih2: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(NOT B)\<parallel>) = (\<parallel>(NOT B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2)
     done
   { case 1 show ?case by (rule g)

   have ih4: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(A AND B)\<parallel>) = (\<parallel>(A AND B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name 
                      ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
     done

   have ih4: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(A OR B)\<parallel>) = (\<parallel>(A OR B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name 
                      ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
     done

   have ih4: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(A IMP B)\<parallel>) = (\<parallel>(A IMP B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
     done
   { case 1 show ?case by (rule g)

 proof (nominal_induct B rule: ty.strong_induct)
   case (PR X)
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(perm_simp)
     done
   next
     case 2 show ?case
       apply -
       apply(simp only: NEGc_simps)
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(simp add: lfp_eqvt)
       apply(simp add: comp_def)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(perm_simp)
       done
   }
 next

   have ih2: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(NOT B)\<parallel>) = (\<parallel>(NOT B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
             NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
     apply(perm_simp add: ih1 ih2)
     done

   have ih4: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(A AND B)\<parallel>) = (\<parallel>(A AND B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname 
                      ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
     done

   have ih4: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(A OR B)\<parallel>) = (\<parallel>(A OR B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname 
                      ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
     done

   have ih4: "pi\<bullet>(\<parallel><B>\<parallel>) = (\<parallel><B>\<parallel>)" by fact
   have g: "pi\<bullet>(\<parallel>(A IMP B)\<parallel>) = (\<parallel>(A IMP B)\<parallel>)"
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname 
          IMPLEFT_eqvt_coname)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
     done