# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1280234279 -7200
# Node ID fe25a3ffeb14729dfa966c35c00ef6aa0eacbc96
# Parent  841b7e34e70ac20d9f9145d7f69ecde44c33e817
cleaned up a bit Abs.thy

diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/Abs.thy	Tue Jul 27 14:37:59 2010 +0200
@@ -43,7 +43,8 @@
   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
 
-(* monos *)
+section {* Mono *}
+
 lemma [mono]: 
   shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
@@ -51,8 +52,9 @@
   by (case_tac [!] bs, case_tac [!] cs) 
      (auto simp add: le_fun_def le_bool_def alphas)
 
-(* equivariance *)
-lemma alpha_gen_eqvt[eqvt]:
+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)"
   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)" 
@@ -63,8 +65,10 @@
   unfolding Diff_eqvt[symmetric]
   by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
-(* equivalence *)
-lemma alpha_gen_refl:
+
+section {* Equivalence *}
+
+lemma alpha_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
   and   "(bs, x) \<approx>res R f 0 (bs, x)"
@@ -74,7 +78,7 @@
   unfolding fresh_star_def
   by (simp_all add: fresh_zero_perm)
 
-lemma alpha_gen_sym:
+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)"
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
@@ -83,13 +87,22 @@
   using a
   by (auto simp add:  fresh_minus_perm)
 
-lemma alpha_gen_sym_eqvt:
+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)"
+  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
+  unfolding alphas fresh_star_def
+  by (simp_all add: fresh_plus_perm)
+
+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)" 
   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_gen_sym)
+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)
@@ -100,23 +113,13 @@
 apply(assumption)
 done
 
-lemma alpha_gen_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)"
-  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
-  unfolding alphas fresh_star_def
-  by (simp_all add: fresh_plus_perm)
-
-
 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)" 
   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)"
-apply(rule alpha_gen_trans)
+apply(rule alpha_trans)
 defer
 apply(rule a)
 apply(rule b)
@@ -136,7 +139,7 @@
   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_gen_trans)
+apply(rule alpha_trans)
 defer
 apply(rule a)
 apply(rule b)
@@ -156,7 +159,7 @@
   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_gen_trans)
+apply(rule alpha_trans)
 defer
 apply(rule a)
 apply(rule b)
@@ -172,12 +175,6 @@
 
 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
-lemma test:
-  shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
-  and   "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
-  and   "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
-  by (simp_all add: alphas)
-
 
 section {* General Abstractions *}
 
@@ -206,6 +203,7 @@
 
 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
+
 lemma alphas_abs_refl:
   shows "(bs, x) \<approx>abs (bs, x)"
   and   "(bs, x) \<approx>abs_res (bs, x)"
@@ -284,7 +282,7 @@
   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 simp only:)
+  by (auto intro: alphas_abs_refl)
 
 lemma [quot_respect]:
   shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
@@ -305,8 +303,7 @@
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (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)
+  unfolding alphas_abs by (lifting alphas_abs)
 
 instantiation abs_gen :: (pt) pt
 begin
@@ -373,6 +370,7 @@
 
 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
 
+
 lemma abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -405,7 +403,7 @@
 lemma abs_supports:
   shows "((supp x) - as) supports (Abs as x)"
   and   "((supp x) - as) supports (Abs_res as x)"
-  and   "((supp x) - (set bs)) supports (Abs_lst bs x)"
+  and   "((supp x) - set bs) supports (Abs_lst bs x)"
   unfolding supports_def
   unfolding permute_abs
   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
@@ -525,6 +523,54 @@
   unfolding supp_abs
   by auto
 
+fun
+  prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+where
+  "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
+
+definition 
+  prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+where
+ "prod_alpha = prod_rel"
+
+
+lemma [quot_respect]:
+  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  by auto
+
+lemma [quot_preserve]:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma [mono]: 
+  shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+  unfolding prod_alpha_def
+  by auto
+
+lemma [eqvt]: 
+  shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  unfolding prod_alpha_def
+  unfolding prod_rel.simps
+  by (perm_simp) (rule refl)
+
+lemma [eqvt]: 
+  shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+  unfolding prod_fv.simps
+  by (perm_simp) (rule refl)
+
+
+
+
+
+
+
+
+
+
+
+
 section {* BELOW is stuff that may or may not be needed *}
 
 lemma supp_atom_image:
@@ -579,97 +625,6 @@
      R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
 by (simp add: alphas)
 
-lemma alpha_gen_simpler:
-  assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
-  and fin_fv: "finite (f x)"
-  and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
-  shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
-     (f x - bs) \<sharp>* pi \<and>
-     R (pi \<bullet> x) y \<and>
-     pi \<bullet> bs = cs"
-  apply rule
-  unfolding alpha_gen
-  apply clarify
-  apply (erule conjE)+
-  apply (simp)
-  apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
-  apply (rule sym)
-  apply simp
-  apply (rule supp_perm_eq)
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (rule fin_fv)
-  apply (assumption)
-  apply (simp add: eqvts fv_eqvt)
-  apply (subst fv_rsp)
-  apply assumption
-  apply (simp)
-  done
-
-lemma alpha_lst_simpler:
-  assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
-  and fin_fv: "finite (f x)"
-  and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
-  shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
-     (f x - set bs) \<sharp>* pi \<and>
-     R (pi \<bullet> x) y \<and>
-     pi \<bullet> bs = cs"
-  apply rule
-  unfolding alpha_lst
-  apply clarify
-  apply (erule conjE)+
-  apply (simp)
-  apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
-  apply (rule sym)
-  apply simp
-  apply (rule supp_perm_eq)
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (rule fin_fv)
-  apply (assumption)
-  apply (simp add: eqvts fv_eqvt)
-  apply (subst fv_rsp)
-  apply assumption
-  apply (simp)
-  done
-
-fun
-  prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
-where
-  "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
-
-definition 
-  prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
-where
- "prod_alpha = prod_rel"
-
-
-lemma [quot_respect]:
-  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
-  by auto
-
-lemma [quot_preserve]:
-  assumes q1: "Quotient R1 abs1 rep1"
-  and     q2: "Quotient R2 abs2 rep2"
-  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
-
-lemma [mono]: 
-  shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
-  unfolding prod_alpha_def
-  by auto
-
-lemma [eqvt]: 
-  shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
-  unfolding prod_alpha_def
-  unfolding prod_rel.simps
-  by (perm_simp) (rule refl)
-
-lemma [eqvt]: 
-  shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
-  unfolding prod_fv.simps
-  by (perm_simp) (rule refl)
-
 
 end
 
diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 27 14:37:59 2010 +0200
@@ -45,26 +45,7 @@
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
--- ""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc)
--- ""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
-apply(simp only: Un_insert_left Un_empty_right Un_empty_left)
--- ""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
---""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
-apply(simp (no_asm) only: simp_thms)
---""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
+apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
 done
 
 lemma [quot_respect]: 
diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Tue Jul 27 14:37:59 2010 +0200
@@ -350,7 +350,7 @@
 
   val bound_tac = 
     EVERY' [ rtac exi_zero, 
-             resolve_tac @{thms alpha_gen_refl}, 
+             resolve_tac @{thms alpha_refl}, 
              asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
 in
   REPEAT o FIRST' [rtac @{thm conjI}, 
@@ -407,7 +407,7 @@
 in
   EVERY' 
     [ etac exi_neg,
-      resolve_tac @{thms alpha_gen_sym_eqvt},
+      resolve_tac @{thms alpha_sym_eqvt},
       asm_full_simp_tac (HOL_ss addsimps prod_simps),
       Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
       trans_prem_tac pred_names ctxt ] 
diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jul 27 14:37:59 2010 +0200
@@ -213,8 +213,6 @@
 
 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
 let
-  val _ = tracing ("bclausesss\n" ^ cat_lines (map (cat_lines o map PolyML.makestring) bclausesss))
-
   val fv_names = prefix_dt_names descr sorts "fv_"
   val fv_arg_tys = all_dtyps descr sorts
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;