
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Wed May 07 10:57:19 2008 +0200
@@ -10317,7 +10317,7 @@
 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)
@@ -10343,7 +10343,7 @@
 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)
@@ -10377,7 +10377,7 @@
 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)
@@ -10403,7 +10403,7 @@
 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)
@@ -10438,7 +10438,7 @@
 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)
@@ -10473,7 +10473,7 @@
 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)
@@ -10516,7 +10516,7 @@
 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)
@@ -10542,7 +10542,7 @@
 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)
@@ -10576,7 +10576,7 @@
 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)
@@ -10602,7 +10602,7 @@
 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)
@@ -10637,7 +10637,7 @@
 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)
@@ -10672,7 +10672,7 @@
 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)
@@ -10715,7 +10715,7 @@
 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)
@@ -10741,7 +10741,7 @@
 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)
@@ -10775,7 +10775,7 @@
 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)
@@ -10801,7 +10801,7 @@
 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)
@@ -10838,7 +10838,7 @@
 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)
@@ -10898,7 +10898,7 @@
 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)
@@ -10966,7 +10966,7 @@
 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) 
@@ -11001,7 +11001,7 @@
 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) 
@@ -11098,16 +11098,6 @@
   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"
@@ -11115,7 +11105,7 @@
   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)
@@ -11150,7 +11140,7 @@
   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)}")
@@ -11162,7 +11152,7 @@
 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)}")
@@ -11345,7 +11335,7 @@
   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)
@@ -11400,7 +11390,7 @@
   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)
@@ -11460,7 +11450,7 @@
   { 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
@@ -11471,7 +11461,7 @@
       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
@@ -11484,7 +11474,7 @@
     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)
@@ -11504,7 +11494,7 @@
     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)
@@ -11526,7 +11516,7 @@
     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)
@@ -11548,7 +11538,7 @@
     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)
@@ -11570,7 +11560,7 @@
   { 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
@@ -11581,7 +11571,7 @@
       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
@@ -11594,7 +11584,7 @@
     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)
@@ -11616,7 +11606,7 @@
     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)
@@ -11638,7 +11628,7 @@
     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)
@@ -11660,7 +11650,7 @@
     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)




