# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1346168887 -3600
# Node ID 93e7c1d8cc5c9bfa11f4f643f5388a622e2e6105
# Parent  e42d281bf5ef9a99527771daae170f29747c8a87
tuned

diff -r e42d281bf5ef -r 93e7c1d8cc5c Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Tue Aug 28 16:47:26 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Aug 28 16:48:07 2012 +0100
@@ -12,30 +12,30 @@
   alpha_set 
 where
   alpha_set[simp del]:
-  "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+  "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow> 
      f x - bs = f y - cs \<and> 
-     (f x - bs) \<sharp>* pi \<and> 
-     R (pi \<bullet> x) y \<and>
-     pi \<bullet> bs = cs"
+     (f x - bs) \<sharp>* p \<and> 
+     R (p \<bullet> x) y \<and>
+     p \<bullet> bs = cs"
 
 fun
   alpha_res
 where
   alpha_res[simp del]:
-  "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+  "alpha_res (bs, x) R f p (cs, y) \<longleftrightarrow> 
      f x - bs = f y - cs \<and> 
-     (f x - bs) \<sharp>* pi \<and> 
-     R (pi \<bullet> x) y"
+     (f x - bs) \<sharp>* p \<and> 
+     R (p \<bullet> x) y"
 
 fun
   alpha_lst
 where
   alpha_lst[simp del]:
-  "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+  "alpha_lst (bs, x) R f p (cs, y) \<longleftrightarrow> 
      f x - set bs = f y - set cs \<and> 
-     (f x - set bs) \<sharp>* pi \<and> 
-     R (pi \<bullet> x) y \<and>
-     pi \<bullet> bs = cs"
+     (f x - set bs) \<sharp>* p \<and> 
+     R (p \<bullet> x) y \<and>
+     p \<bullet> bs = cs"
 
 lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
 
@@ -66,8 +66,7 @@
   unfolding Diff_eqvt[symmetric]
   unfolding eq_eqvt[symmetric]
   unfolding fresh_star_eqvt[symmetric]
-  by (auto simp add: permute_bool_def)
-
+  by (auto simp only: permute_bool_def)
 
 section {* Equivalence *}
 
@@ -88,7 +87,7 @@
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
   unfolding alphas fresh_star_def
   using a
-  by (auto simp add:  fresh_minus_perm)
+  by (auto simp add: fresh_minus_perm)
 
 lemma alpha_trans:
   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
@@ -108,12 +107,7 @@
 apply(auto intro!: alpha_sym)
 apply(drule_tac [!] a)
 apply(rule_tac [!] p="p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel b)
-apply(assumption)
-apply(perm_simp add: permute_minus_cancel b)
-apply(assumption)
-apply(perm_simp add: permute_minus_cancel b)
-apply(assumption)
+apply(simp_all add: b permute_self)
 done
 
 lemma alpha_set_trans_eqvt:
@@ -122,18 +116,13 @@
   and     d: "q \<bullet> R = R"
   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
   shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
-apply(rule alpha_trans)
-defer
-apply(rule a)
-apply(rule b)
+apply(rule alpha_trans(1)[OF _ a b])
 apply(drule c)
 apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel d)
-apply(assumption)
+apply(simp add: d permute_self)
 apply(rotate_tac -1)
 apply(drule_tac p="q" in permute_boolI)
-apply(perm_simp add: permute_minus_cancel d)
-apply(simp add: permute_eqvt[symmetric])
+apply(simp add: d permute_self permute_eqvt[symmetric])
 done
 
 lemma alpha_res_trans_eqvt:
@@ -142,18 +131,13 @@
   and     d: "q \<bullet> R = R"
   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
   shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
-apply(rule alpha_trans)
-defer
-apply(rule a)
-apply(rule b)
+apply(rule alpha_trans(2)[OF _ a b])
 apply(drule c)
 apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel d)
-apply(assumption)
+apply(simp add: d permute_self)
 apply(rotate_tac -1)
 apply(drule_tac p="q" in permute_boolI)
-apply(perm_simp add: permute_minus_cancel d)
-apply(simp add: permute_eqvt[symmetric])
+apply(simp add: d permute_self permute_eqvt[symmetric])
 done
 
 lemma alpha_lst_trans_eqvt:
@@ -162,18 +146,13 @@
   and     d: "q \<bullet> R = R"
   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
   shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
-apply(rule alpha_trans)
-defer
-apply(rule a)
-apply(rule b)
+apply(rule alpha_trans(3)[OF _ a b])
 apply(drule c)
 apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel d)
-apply(assumption)
+apply(simp add: d permute_self)
 apply(rotate_tac -1)
 apply(drule_tac p="q" in permute_boolI)
-apply(perm_simp add: permute_minus_cancel d)
-apply(simp add: permute_eqvt[symmetric])
+apply(simp add: d permute_self permute_eqvt[symmetric])
 done
 
 lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
@@ -457,17 +436,15 @@
 
 section {* Quotient types *}
 
-(* FIXME: The three could be defined together, but due to bugs
-   introduced by the lifting package it doesn't work anymore *)
 quotient_type
     'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
-  apply(rule_tac [!] equivpI)
+  apply(rule equivpI)
   unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_type
     'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
-  apply(rule_tac [!] equivpI)
+  apply(rule equivpI)
   unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
@@ -537,7 +514,7 @@
   apply (simp add: fresh_star_zero)
   using asm by blast
 
-lemma Abs_exhausts:
+lemma Abs_exhausts[cases type]:
   shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1"
   and   "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2"
   and   "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3"
@@ -545,7 +522,6 @@
               prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
-
 instantiation abs_set :: (pt) pt
 begin
 
@@ -562,7 +538,7 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: Abs_exhausts(1))
+  apply(case_tac [!] x)
   apply(simp_all)
   done
 
@@ -584,7 +560,7 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: Abs_exhausts(2))
+  apply(case_tac [!] x)
   apply(simp_all)
   done
 
@@ -606,7 +582,7 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: Abs_exhausts(3))
+  apply(case_tac [!] x)
   apply(simp_all)
   done
 
@@ -651,51 +627,37 @@
   by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
 
 function
-  supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
+  supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set" and
+  supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" and
+  supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
 where
   "supp_set ([as]set. x) = supp x - as"
-apply(case_tac x rule: Abs_exhausts(1))
+| "supp_res ([as]res. x) = supp x - as"
+| "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+apply(simp_all add: Abs_eq_iff alphas_abs alphas)
+apply(case_tac x)
+apply(case_tac a)
 apply(simp)
-apply(simp add: Abs_eq_iff alphas_abs alphas)
+apply(case_tac b)
+apply(case_tac a)
+apply(simp)
+apply(case_tac ba)
+apply(simp)
 done
 
-termination supp_set 
-  by lexicographic_order
-
-function
-  supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
-where
-  "supp_res ([as]res. x) = supp x - as"
-apply(case_tac x rule: Abs_exhausts(2))
-apply(simp)
-apply(simp add: Abs_eq_iff alphas_abs alphas)
-done
-
-termination supp_res 
-  by lexicographic_order
-
-function
-  supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
-where
-  "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-apply(case_tac x rule: Abs_exhausts(3))
-apply(simp)
-apply(simp add: Abs_eq_iff alphas_abs alphas)
-done
-
-termination supp_lst
+termination
   by lexicographic_order
 
 lemma supp_funs_eqvt[eqvt]:
   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
-  apply(case_tac x rule: Abs_exhausts(1))
-  apply(simp add: supp_eqvt Diff_eqvt)
-  apply(case_tac y rule: Abs_exhausts(2))
-  apply(simp add: supp_eqvt Diff_eqvt)
-  apply(case_tac z rule: Abs_exhausts(3))
-  apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
+  apply(case_tac x)
+  apply(simp)
+  apply(case_tac y)
+  apply(simp)
+  apply(case_tac z)
+  apply(simp)
   done
 
 lemma Abs_fresh_aux:
@@ -739,19 +701,19 @@
 
 instance abs_set :: (fs) fs
   apply(default)
-  apply(case_tac x rule: Abs_exhausts(1))
+  apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_res :: (fs) fs
   apply(default)
-  apply(case_tac x rule: Abs_exhausts(2))
+  apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_lst :: (fs) fs
   apply(default)
-  apply(case_tac x rule: Abs_exhausts(3))
+  apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
@@ -791,15 +753,14 @@
 
 section {* Abstractions of single atoms *}
 
+
 lemma Abs1_eq:
   fixes x y::"'a::fs"
   shows "[{atom a}]set. x = [{atom a}]set. y \<longleftrightarrow> x = y"
   and   "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
   and   "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
 unfolding Abs_eq_iff2 alphas
-apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)
-apply(blast)+
-done
+by (auto simp add: supp_perm_singleton fresh_star_def fresh_zero_perm)
 
 lemma Abs1_eq_iff_fresh:
   fixes x y::"'a::fs"
@@ -850,29 +811,25 @@
   shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
   and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-apply -
 apply(auto) 
 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(1))
-apply(auto simp add: fresh_Pair)[1]
-apply(assumption)
+apply(auto simp add: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(2))
-apply(auto simp add: fresh_Pair)[1]
-apply(assumption)
+apply(auto simp add: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(3))
-apply(auto simp add: fresh_Pair)[1]
-apply(assumption)
+apply(auto simp add: fresh_Pair)[2]
 done
 
 lemma Abs1_eq_iff:
@@ -886,24 +843,24 @@
     then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
-  { assume *: "a \<noteq> b" and **: "Abs_set {atom a} x = Abs_set {atom b} y"
-    have #: "atom a \<sharp> Abs_set {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_set {atom b} y)" by (simp)
-    also have "\<dots> = Abs_set {atom b} y"
+  { assume *: "a \<noteq> b" and **: "[{atom a}]set. x = [{atom b}]set. y"
+    have #: "atom a \<sharp> [{atom b}]set. y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "[{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp)
+    also have "\<dots> = [{atom b}]set. y"
       by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
-    also have "\<dots> = Abs_set {atom a} x" using ** by simp
+    also have "\<dots> = [{atom a}]set. x" using ** by simp
     finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
   }
   moreover 
   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
-    have "Abs_set {atom a} x = Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_set {atom b} y" by (simp add: permute_set_def assms)
-    also have "\<dots> = Abs_set {atom b} y"
+    have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+    also have "\<dots> = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp add: permute_set_def assms)
+    also have "\<dots> = [{atom b}]set. y"
       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
-    finally have "Abs_set {atom a} x = Abs_set {atom b} y" .
+    finally have "[{atom a}]set. x = [{atom b}]set. y" .
   }
   ultimately 
-  show "Abs_set {atom a} x = Abs_set {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
+  show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
     by blast
 next
   { assume "a = b"
@@ -1130,5 +1087,10 @@
   by (auto intro!: ext)
 
 
+
+
+
+
+
 end