src/HOL/Nominal/Examples/Class.thy

 done
 
 lemma NOTRIGHT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma NOTRIGHT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma NOTLEFT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma NOTLEFT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ANDRIGHT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>c" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(rule_tac x="pi\<bullet>N" in exI)

 done
 
 lemma ANDRIGHT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>c" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(rule_tac x="pi\<bullet>N" in exI)

 done
 
 lemma ANDLEFT1_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ANDLEFT1_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ANDLEFT2_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ANDLEFT2_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ORLEFT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI)
 apply(rule_tac x="pi\<bullet>z" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(rule_tac x="pi\<bullet>N" in exI)

 done
 
 lemma ORLEFT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI)
 apply(rule_tac x="pi\<bullet>z" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(rule_tac x="pi\<bullet>N" in exI)

 done
 
 lemma ORRIGHT1_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ORRIGHT1_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ORRIGHT2_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma ORRIGHT2_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(rule conjI)

 done
 
 lemma IMPRIGHT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)

 done
 
 lemma IMPRIGHT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)

 done
 
 lemma IMPLEFT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI) 
 apply(rule_tac x="pi\<bullet>N" in exI)

 done
 
 lemma IMPLEFT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI) 
 apply(rule_tac x="pi\<bullet>N" in exI)

 
 lemma test2:
   shows "x\<in>(X\<inter>Y) = (x\<in>X \<and> x\<in>Y)"
 by blast
 
-lemma pt_Collect_eqvt:
-  fixes pi::"'x prm"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
-  shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-apply(auto simp add: perm_set_def  pt_rev_pi[OF pt, OF at])
-apply(rule_tac x="(rev pi)\<bullet>x" in exI)
-apply(simp add: pt_pi_rev[OF pt, OF at])
-done
-
 lemma big_inter_eqvt:
   fixes pi1::"name prm"
   and   X::"('a::pt_name) set set"
   and   pi2::"coname prm"
   and   Y::"('b::pt_coname) set set"
   shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
   and   "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
 apply(perm_simp)
 apply(rule ballI)
 apply(drule_tac x="pi1\<bullet>xa" in spec)
 apply(auto)

   and   pi2::"coname prm"
   and   g::"'b set \<Rightarrow> ('b::pt_coname) set"
   shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
   and   "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_def)
+apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
 apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
 apply(perm_simp)
 apply(rule Collect_cong)

 apply(rule subseteq_eqvt(1)[THEN iffD1])
 apply(simp add: perm_bool)
 apply(drule subseteq_eqvt(1)[THEN iffD2])
 apply(simp add: perm_bool)
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_def)
+apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
 apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
 apply(perm_simp)
 apply(rule Collect_cong)

 
 lemma BINDING_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)" 
   and   "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)" 
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(auto)[1]
 apply(drule_tac x="(rev pi)\<bullet>a" in spec)

 
 lemma BINDING_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)" 
   and   "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)" 
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
 apply(auto)[1]
 apply(drule_tac x="(rev pi)\<bullet>a" in spec)

 proof (nominal_induct B rule: ty.induct)
   case (PR X)
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       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)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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.induct)
   case (PR X)
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       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)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     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