# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271263640 -7200
# Node ID 2a61e91019a35585b7d7bf380394a7ff7e665928
# Parent  fcc660ece04048bd3381981d80e02602715e6560# Parent  b435ee87d9c8728504af2c6ad863aeb161c95656
merged

diff -r b435ee87d9c8 -r 2a61e91019a3 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 16:11:04 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 18:47:20 2010 +0200
@@ -39,6 +39,28 @@
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
 struct
 
+fun get_ps trm =
+  case trm of 
+     Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm])
+   | Const (@{const_name permute}, _) $ p $ _ => [p]
+   | t $ u => get_ps t @ get_ps u
+   | Abs (_, _, t) => get_ps t 
+   | _ => []
+
+fun put_p p trm =
+  case trm of 
+     Bound _ => trm
+   | Const _ => trm
+   | t $ u => put_p p t $ put_p p u
+   | Abs (x, ty, t) => Abs (x, ty, put_p p t)
+   | _ => mk_perm p trm
+
+(* tests whether the lists of ps all agree, and that there is at least one p *)
+fun is_bad_list [] = true
+  | is_bad_list [_] = false
+  | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
+
+
 structure EqvtData = Generic_Data
 ( type T = thm Item_Net.T;
   val empty = Thm.full_rules;
@@ -62,45 +84,48 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)
+    Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
   | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
-fun eq_transform_tac thm = REPEAT o FIRST' 
-  [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),
-   rtac (thm RS @{thm trans}),
-   rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
+fun eq_transform_tac thm = 
+let
+  val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
+in
+  REPEAT o FIRST' 
+    [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),
+     rtac (thm RS @{thm trans}),
+     rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
+end
 
 (* transform equations into the "p o c = c"-form *)
 fun transform_eq ctxt thm = 
 let
-  val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
-  val (p, t) = dest_perm lhs
-  val (c, args) = strip_comb t
-  val (c', args') = strip_comb rhs
-  val eargs = map Envir.eta_contract args 
-  val eargs' = map Envir.eta_contract args'
-  val p_str = fst (fst (dest_Var p))
-  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
+  val ((p, t), rhs) = apfst dest_perm 
+    (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))
+    handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c...  = c..."
+  val ps = get_ps rhs handle TERM _ => []  
+  val (c, c') = (head_of t, head_of rhs)
 in
   if c <> c' 
     then error "Eqvt lemma is not of the right form (constants do not agree)"
-  else if eargs' <> map (mk_perm p) eargs 
+  else if is_bad_list (p::ps)  
+    then error "Eqvt lemma is not of the right form (permutations do not agree)" 
+  else if not (rhs aconv (put_p p t))
     then error "Eqvt lemma is not of the right form (arguments do not agree)"
-  else if args = [] 
+  else if is_Const t 
     then thm
-  else Goal.prove ctxt [p_str] [] goal
-    (fn _ => eq_transform_tac thm 1)
+  else 
+    let 
+      val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
+      val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
+    in
+      Goal.prove ctxt [] [] goal' (fn _ => eq_transform_tac thm 1)
+      |> singleton (ProofContext.export ctxt' ctxt)
+    end
 end
 
-
-(* tests whether the lists of pis all agree, and that there is at least one p *)
-fun is_bad_list [] = true
-  | is_bad_list [_] = false
-  | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
-
-
 fun imp_transform_tac thy p p' thm = 
 let
   val cp = Thm.cterm_of thy p
@@ -116,20 +141,19 @@
 let
   val thy = ProofContext.theory_of ctxt
   val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
-  val (c, prem_args) = strip_comb prem
-  val (c', concl_args) = strip_comb concl
-  val ps = map (fst o dest_perm) concl_args handle TERM _ => []  
+  val (c, c') = (head_of prem, head_of concl)
+  val ps = get_ps concl handle TERM _ => []  
   val p = try hd ps
 in
   if c <> c' 
     then error "Eqvt lemma is not of the right form (constants do not agree)"
   else if is_bad_list ps  
     then error "Eqvt lemma is not of the right form (permutations do not agree)" 
-  else if concl_args <> map (mk_perm (the p)) prem_args 
+  else if not (concl aconv (put_p (the p) prem)) 
     then error "Eqvt lemma is not of the right form (arguments do not agree)"
   else 
     let
-      val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem    
+      val prem' = mk_perm (the p) prem    
       val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))
       val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
     in
diff -r b435ee87d9c8 -r 2a61e91019a3 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 14 16:11:04 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 14 18:47:20 2010 +0200
@@ -762,8 +762,7 @@
   by (simp_all add: fresh_plus_perm)
 
 
-(* PROBLEM: this should be the real eqvt lemma for the alphas *)
-lemma alpha_gen_real_eqvt:
+lemma alpha_gen_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)" 
@@ -774,23 +773,6 @@
   unfolding Diff_eqvt[symmetric]
   by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
-
-lemma alpha_gen_eqvt:
-  assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
-  and     b: "p \<bullet> (f x) = f (p \<bullet> x)"
-  and     c: "p \<bullet> (f y) = f (p \<bullet> y)"
-  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R 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 R 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 R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
-  unfolding alphas
-  unfolding set_eqvt[symmetric]
-  unfolding b[symmetric] c[symmetric]
-  unfolding Diff_eqvt[symmetric]
-  unfolding permute_eqvt[symmetric]
-  using a
-  by (auto simp add: fresh_star_permute_iff)
-
-
 lemma alpha_gen_simpler:
   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
   and fin_fv: "finite (f x)"