--- a/src/HOL/Nominal/Examples/Class2.thy Tue Jan 10 23:58:10 2012 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Tue Jan 10 23:59:37 2012 +0100
@@ -2123,7 +2123,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2149,7 +2149,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2182,7 +2182,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2208,7 +2208,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2242,7 +2242,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2277,7 +2277,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2319,7 +2319,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2345,7 +2345,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2378,7 +2378,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2404,7 +2404,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2438,7 +2438,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2473,7 +2473,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2515,7 +2515,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2541,7 +2541,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2574,7 +2574,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2600,7 +2600,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2636,7 +2636,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2696,7 +2696,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2763,7 +2763,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2798,7 +2798,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_eq)
+apply(auto simp add: perm_set_def)
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)
@@ -2902,7 +2902,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_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
apply(perm_simp)
apply(rule ballI)
@@ -3130,7 +3130,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_eq)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
apply(simp)
@@ -3185,7 +3185,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_eq)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
apply(simp)
--- a/src/HOL/Nominal/Examples/Support.thy Tue Jan 10 23:58:10 2012 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Tue Jan 10 23:59:37 2012 +0100
@@ -98,14 +98,14 @@
proof (cases "x\<in>S")
case True
have "x\<in>S" by fact
- hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
+ hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
then show "x\<in>(supp S)" by (simp add: supp_def)
next
case False
have "x\<notin>S" by fact
- hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
+ hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
then show "x\<in>(supp S)" by (simp add: supp_def)
@@ -129,7 +129,7 @@
shows "supp (UNIV::atom set) = ({}::atom set)"
proof -
have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
- by (auto simp add: perm_set_eq calc_atm)
+ by (auto simp add: perm_set_def calc_atm)
then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
qed