# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283554094 -28800
# Node ID 4a6e78bd9de98462933b0464a4656b01a145c20a
# Parent  7b1470b559365effbf9bc0f1c8b99f1bcdf2080a
renamed alpha_gen -> alpha_set and Abs -> Abs_set etc

diff -r 7b1470b55936 -r 4a6e78bd9de9 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Sep 04 06:23:31 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 04 06:48:14 2010 +0800
@@ -8,10 +8,10 @@
 begin
 
 fun
-  alpha_gen 
+  alpha_set 
 where
-  alpha_gen[simp del]:
-  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+  alpha_set[simp del]:
+  "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow> 
      f x - bs = f y - cs \<and> 
      (f x - bs) \<sharp>* pi \<and> 
      R (pi \<bullet> x) y \<and>
@@ -36,17 +36,17 @@
      R (pi \<bullet> x) y \<and>
      pi \<bullet> bs = cs"
 
-lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
+lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
 
 notation
-  alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
+  alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and
   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
 
 section {* Mono *}
 
 lemma [mono]: 
-  shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
+  shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"
   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
   and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
   by (case_tac [!] bs, case_tac [!] cs) 
@@ -55,7 +55,7 @@
 section {* Equivariance *}
 
 lemma alpha_eqvt[eqvt]:
-  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
   unfolding alphas
@@ -70,7 +70,7 @@
 
 lemma alpha_refl:
   assumes a: "R x x"
-  shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+  shows "(bs, x) \<approx>set R f 0 (bs, x)"
   and   "(bs, x) \<approx>res R f 0 (bs, x)"
   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
   using a 
@@ -80,7 +80,7 @@
 
 lemma alpha_sym:
   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
-  shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+  shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   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
@@ -89,7 +89,7 @@
 
 lemma alpha_trans:
   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
-  shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+  shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)"
   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
   using a
@@ -99,7 +99,7 @@
 lemma alpha_sym_eqvt:
   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
   and     b: "p \<bullet> R = R"
-  shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" 
+  shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)" 
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" 
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 apply(auto intro!: alpha_sym)
@@ -113,12 +113,12 @@
 apply(assumption)
 done
 
-lemma alpha_gen_trans_eqvt:
-  assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
-  and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
+lemma alpha_set_trans_eqvt:
+  assumes b: "(cs, y) \<approx>set R f q (ds, z)"
+  and     a: "(bs, x) \<approx>set R f p (cs, y)" 
   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>gen R f (q + p) (ds, z)"
+  shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
 apply(rule alpha_trans)
 defer
 apply(rule a)
@@ -173,16 +173,16 @@
 apply(simp add: permute_eqvt[symmetric])
 done
 
-lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
 
 section {* General Abstractions *}
 
 fun
-  alpha_abs 
+  alpha_abs_set 
 where
   [simp del]:
-  "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+  "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
 
 fun
   alpha_abs_lst
@@ -197,15 +197,15 @@
   "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
 
 notation
-  alpha_abs (infix "\<approx>abs" 50) and
+  alpha_abs_set (infix "\<approx>abs'_set" 50) and
   alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
   alpha_abs_res (infix "\<approx>abs'_res" 50)
 
-lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
+lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
 
 
 lemma alphas_abs_refl:
-  shows "(bs, x) \<approx>abs (bs, x)"
+  shows "(bs, x) \<approx>abs_set (bs, x)"
   and   "(bs, x) \<approx>abs_res (bs, x)"
   and   "(cs, x) \<approx>abs_lst (cs, x)" 
   unfolding alphas_abs
@@ -215,7 +215,7 @@
      (simp_all add: fresh_zero_perm)
 
 lemma alphas_abs_sym:
-  shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
+  shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
   unfolding alphas_abs
@@ -225,7 +225,7 @@
      (auto simp add: fresh_minus_perm)
 
 lemma alphas_abs_trans:
-  shows "\<lbrakk>(bs, x) \<approx>abs (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (ds, z)"
+  shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
   and   "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
   and   "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
   unfolding alphas_abs
@@ -236,7 +236,7 @@
   by (simp_all add: fresh_plus_perm)
 
 lemma alphas_abs_eqvt:
-  shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (p \<bullet> cs, p \<bullet> y)"
+  shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_set (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
   unfolding alphas_abs
@@ -249,7 +249,7 @@
   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
 quotient_type 
-    'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
+    'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   apply(rule_tac [!] equivpI)
@@ -257,9 +257,9 @@
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition
-  Abs ("[_]set. _" [60, 60] 60)
+  Abs_set ("[_]set. _" [60, 60] 60)
 where
-  "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
+  "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
@@ -278,21 +278,21 @@
   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
 
 lemma [quot_respect]:
-  shows "(op= ===> op= ===> alpha_abs) Pair Pair"
+  shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
   unfolding fun_rel_def
   by (auto intro: alphas_abs_refl)
 
 lemma [quot_respect]:
-  shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
+  shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
   unfolding fun_rel_def
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma abs_exhausts:
-  shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
+  shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
   and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
   by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
@@ -300,22 +300,22 @@
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
 lemma abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (cs, y)"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
   unfolding alphas_abs by (lifting alphas_abs)
 
-instantiation abs_gen :: (pt) pt
+instantiation abs_set :: (pt) pt
 begin
 
 quotient_definition
-  "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
+  "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
 lemma permute_Abs[simp]:
   fixes x::"'a::pt"  
-  shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+  shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
@@ -374,7 +374,7 @@
 lemma abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
-  shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
   and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
   unfolding abs_eq_iff
   unfolding alphas_abs
@@ -401,7 +401,7 @@
      (auto simp add: supp_perm swap_atom)
 
 lemma abs_supports:
-  shows "((supp x) - as) supports (Abs as x)"
+  shows "((supp x) - as) supports (Abs_set as x)"
   and   "((supp x) - as) supports (Abs_res as x)"
   and   "((supp x) - set bs) supports (Abs_lst bs x)"
   unfolding supports_def
@@ -409,15 +409,15 @@
   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
 function
-  supp_gen  :: "('a::pt) abs_gen \<Rightarrow> atom set"
+  supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
 where
-  "supp_gen (Abs as x) = supp x - as"
+  "supp_set (Abs_set as x) = supp x - as"
 apply(case_tac x rule: abs_exhausts(1))
 apply(simp)
 apply(simp add: abs_eq_iff alphas_abs alphas)
 done
 
-termination supp_gen 
+termination supp_set 
   by (auto intro!: local.termination)
 
 function
@@ -445,7 +445,7 @@
   by (auto intro!: local.termination)
 
 lemma [eqvt]:
-  shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
+  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))
@@ -457,7 +457,7 @@
   done
 
 lemma aux_fresh:
-  shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
+  shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
   by (rule_tac [!] fresh_fun_eqvt_app)
@@ -465,7 +465,7 @@
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
-  shows "(supp x) - as \<subseteq> supp (Abs as x)"
+  shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
   unfolding supp_conv_fresh
@@ -474,7 +474,7 @@
 
 lemma supp_abs_subset2:
   assumes a: "finite (supp x)"
-  shows "supp (Abs as x) \<subseteq> (supp x) - as"
+  shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
   by (rule_tac [!] supp_is_subset)
@@ -482,7 +482,7 @@
 
 lemma abs_finite_supp:
   assumes a: "finite (supp x)"
-  shows "supp (Abs as x) = (supp x) - as"
+  shows "supp (Abs_set as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
   by (rule_tac [!] subset_antisym)
@@ -490,13 +490,13 @@
 
 lemma supp_abs:
   fixes x::"'a::fs"
-  shows "supp (Abs as x) = (supp x) - as"
+  shows "supp (Abs_set as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
   by (rule_tac [!] abs_finite_supp)
      (simp_all add: finite_supp)
 
-instance abs_gen :: (fs) fs
+instance abs_set :: (fs) fs
   apply(default)
   apply(case_tac x rule: abs_exhausts(1))
   apply(simp add: supp_abs finite_supp)
@@ -516,7 +516,7 @@
 
 lemma abs_fresh_iff:
   fixes x::"'a::fs"
-  shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+  shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
   and   "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
   and   "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
   unfolding fresh_def
@@ -524,7 +524,7 @@
   by auto
 
 lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
   by (lifting alphas_abs)
diff -r 7b1470b55936 -r 4a6e78bd9de9 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Sat Sep 04 06:23:31 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sat Sep 04 06:48:14 2010 +0800
@@ -88,7 +88,7 @@
   val (alpha_name, binder_ty) = 
     case bmode of
       Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
-    | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
+    | Set => (@{const_name "alpha_set"}, @{typ "atom set"})
     | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
   val ty = fastype_of args
   val pair_ty = HOLogic.mk_prodT (binder_ty, ty)