# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265725710 -3600
# Node ID f64d826a3f55a3dc5ff497863a4688485392c7e6
# Parent  551eacf071d731700a0e6e8f90ec5487769c7deb# Parent  a69ec3f3f53507f3209db518215d8a90eb9f2d95
merge

diff -r 551eacf071d7 -r f64d826a3f55 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Tue Feb 09 15:28:15 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 09 15:28:30 2010 +0100
@@ -51,6 +51,30 @@
   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
   using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
 
+lemma alpha_gen_trans:
+  assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
+  and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
+  and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
+  shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
+  using a b c using supp_plus_perm
+  apply(simp add: alpha_gen fresh_star_def fresh_def)
+  apply(blast)
+  done
+
+lemma alpha_gen_eqvt:
+  assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
+  and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+  and     c: "p \<bullet> (f x) = f (p \<bullet> x)"
+  and     d: "p \<bullet> (f y) = f (p \<bullet> y)"
+  shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  using a b
+  apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
+  apply(simp add: permute_eqvt[symmetric])
+  apply(simp add: fresh_star_permute_iff)
+  apply(clarsimp)
+  done
+
+(* introduced for examples *)
 lemma alpha_gen_atom_sym:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
@@ -67,16 +91,6 @@
   apply assumption
   done
 
-lemma alpha_gen_trans:
-  assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
-  and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
-  and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
-  shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
-  using a b c using supp_plus_perm
-  apply(simp add: alpha_gen fresh_star_def fresh_def)
-  apply(blast)
-  done
-
 lemma alpha_gen_atom_trans:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
@@ -98,19 +112,6 @@
   apply(simp)
   done
 
-lemma alpha_gen_eqvt:
-  assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
-  and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
-  and     c: "p \<bullet> (f x) = f (p \<bullet> x)"
-  and     d: "p \<bullet> (f y) = f (p \<bullet> y)"
-  shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  using a b
-  apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
-  apply(simp add: permute_eqvt[symmetric])
-  apply(simp add: fresh_star_permute_iff)
-  apply(clarsimp)
-  done
-
 lemma alpha_gen_atom_eqvt:
   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
   and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
@@ -258,11 +259,8 @@
   shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"
   by (lifting supp_abs_fun.simps(1))
 
-lemma supp_Abs_fun_eqvt:
-  shows "(p \<bullet> supp_Abs_fun) = supp_Abs_fun"
-  apply(subst permute_fun_def)
-  apply(subst expand_fun_eq)
-  apply(rule allI)
+lemma supp_Abs_fun_eqvt [eqvt]:
+  shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"
   apply(induct_tac x rule: abs_induct)
   apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)
   done
@@ -270,7 +268,7 @@
 lemma supp_Abs_fun_fresh:
   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"
   apply(rule fresh_fun_eqvt_app)
-  apply(simp add: supp_Abs_fun_eqvt)
+  apply(simp add: eqvts_raw)
   apply(simp)
   done
 
@@ -325,14 +323,14 @@
 
 lemma Abs_fresh_iff:
   fixes x::"'a::fs"
-  shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
+  shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
   apply(simp add: fresh_def)
   apply(simp add: supp_Abs)
   apply(auto)
   done
 
 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 bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   by (lifting alpha_abs.simps(1))
 
 
@@ -346,11 +344,47 @@
 fun
   alpha1
 where
-  "alpha1 (a, x) (b, y) \<longleftrightarrow> ((a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y))"
+  "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
 
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
+thm swap_set_not_in
+
+lemma qq:
+  fixes S::"atom set"
+  assumes a: "supp p \<inter> S = {}"
+  shows "p \<bullet> S = S"
+using a
+apply(simp add: supp_perm permute_set_eq)
+apply(auto)
+apply(simp only: disjoint_iff_not_equal)
+apply(simp)
+apply (metis permute_atom_def_raw)
+apply(rule_tac x="(- p) \<bullet> x" in exI)
+apply(simp)
+apply(simp only: disjoint_iff_not_equal)
+apply(simp)
+apply(metis permute_minus_cancel)
+done
+
+lemma alpha_abs_swap:
+  assumes a1: "(supp x - bs) \<sharp>* p"
+  and     a2: "(supp x - bs) \<sharp>* p"
+  shows "(bs, x) \<approx>abs (p \<bullet> bs, p \<bullet> x)"
+  apply(simp)
+  apply(rule_tac x="p" in exI)
+  apply(simp add: alpha_gen)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(rule conjI)
+  apply(rule sym)
+  apply(rule qq)
+  using a1 a2
+  apply(auto)[1]
+  oops
+
+
+
 lemma
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
@@ -383,6 +417,60 @@
 apply(simp add: supp_swap)
 done
 
+thm supp_perm
+
+lemma perm_induct_test:
+  fixes P :: "perm => bool"
+  assumes zero: "P 0"
+  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+sorry
+
+
+lemma tt:
+  "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+apply(induct p rule: perm_induct_test)
+apply(simp)
+apply(rule swap_fresh_fresh)
+apply(case_tac "a \<in> supp x")
+apply(simp add: fresh_star_def)
+apply(drule_tac x="a" in bspec)
+apply(simp)
+apply(simp add: fresh_def)
+apply(simp add: supp_swap)
+apply(simp add: fresh_def)
+apply(case_tac "b \<in> supp x")
+apply(simp add: fresh_star_def)
+apply(drule_tac x="b" in bspec)
+apply(simp)
+apply(simp add: fresh_def)
+apply(simp add: supp_swap)
+apply(simp add: fresh_def)
+apply(simp)
+apply(drule meta_mp)
+apply(simp add: fresh_star_def fresh_def)
+apply(drule meta_mp)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp)
+done
+
+lemma yy:
+  assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
+  shows "S1 = S2"
+using assms
+apply (metis insert_Diff_single insert_absorb)
+done
+
+
+lemma
+  assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
+  shows "(a, x) \<approx>abs1 (b, y)"
+using a
+apply(case_tac "a = b")
+apply(simp)
+oops
+
 
 end
 
diff -r 551eacf071d7 -r f64d826a3f55 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Feb 09 15:28:15 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 15:28:30 2010 +0100
@@ -687,9 +687,9 @@
 
 
 
-(*** Wrapper for transforming an rthm into a qthm ***)
+(*** Wrapper for automatically transforming an rthm into a qthm ***)
 
-(* subst_tys takes a list of (rty,qty) substitution pairs
+(* subst_tys takes a list of (rty, qty) substitution pairs
    and replaces all occurences of rty in the given type
    by appropriate qty, with substitution *)
 fun subst_ty thy ty (rty, qty) r =
@@ -705,7 +705,7 @@
         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
       | x => x)
 
-(* subst_trms takes a list of (rtrm,qtrm) substitution pairs
+(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
    and if the  given term matches any of the raw terms it
    returns the appropriate qtrm instantiated. If none of
    them matched it returns NONE. *)
@@ -722,9 +722,9 @@
 fun get_ty_trm_substs ctxt =
 let
   val thy = ProofContext.theory_of ctxt
-  val quot_infos = Quotient_Info.quotdata_dest ctxt
+  val quot_infos  = Quotient_Info.quotdata_dest ctxt
+  val const_infos = Quotient_Info.qconsts_dest ctxt
   val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
-  val const_infos = Quotient_Info.qconsts_dest ctxt
   val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
   fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
   val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
@@ -734,14 +734,14 @@
 
 
 (*
-Finds subterms of a term that can be lifted and:
+Takes a term and
 
-* replaces subterms matching lifted constants by the lifted constants
+* replaces raw constants by the quotient constants
 
 * replaces equivalence relations by equalities
 
-* In constants, frees and schematic variables replaces
-  subtypes matching lifted types by those types
+* replaces raw types by the quotient types
+
 *)
 
 fun quotient_lift_all ctxt t =
@@ -770,7 +770,6 @@
 end
 
 
-
 end; (* structure *)