--- a/Nominal/Ex/LamTest.thy	Sat Jan 15 20:24:16 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Sat Jan 15 21:16:15 2011 +0000
@@ -345,7 +345,6 @@
 
 
 ML {*
-(*
 fun eqvt_at_elim thy (eqvts:thm list) thm =
   case (prop_of thm) of
     Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ => 
@@ -358,7 +357,6 @@
         |> eqvt_at_elim thy eqvts 
       end
   | _ => thm
-*)
 *}
 
 ML {*
@@ -394,8 +392,8 @@
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      |> fold Thm.elim_implies (rev eqvtsi) (* HERE *)
-      (* |> eqvt_at_elim thy eqvts *) 
+      |> fold Thm.elim_implies (rev eqvtsi)  (* HERE *)
+      (* |> eqvt_at_elim thy eqvtsi *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -439,7 +437,7 @@
 ML {*
 fun mk_eqvt_lemma thy ih_eqvt clause =
   let
-    val ClauseInfo {cdata=ClauseContext {cqs, case_hyp, ...}, RCs, ...} = clause
+    val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
 
     local open Conv in
       val ih_conv = arg1_conv o arg_conv o arg_conv
@@ -454,6 +452,7 @@
         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
   in
     map prep_eqvt RCs
+    |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
     |> map (Thm.implies_intr (cprop_of case_hyp))
     |> map (fold_rev Thm.forall_intr cqs)
     |> map (Thm.close_derivation) 
@@ -463,8 +462,10 @@
 ML {*
 fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
   let
+    val _ = tracing "START"
+
     val Globals {h, y, x, fvar, ...} = globals
-    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ...}, ...} = clausei
+    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ags = agsi, ...}, ...} = clausei
     val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
 
     val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
@@ -479,6 +480,8 @@
     val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 
 
+    val _ = tracing "POINT B"
+
     val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
 
     val RLj_import = RLj
@@ -486,13 +489,22 @@
       |> fold Thm.elim_implies agsj'
       |> fold Thm.elim_implies Ghsj'
 
+    val _ = tracing "POINT C"
+ 
     val eqvtsi = nth eqvts (i - 1)
       |> map (fold Thm.forall_elim cqsi)
       |> map (fold Thm.elim_implies [case_hyp])
+      |> map (fold Thm.elim_implies agsi)
+
+    val _ = tracing "POINT D"
 
     val eqvtsj = nth eqvts (j - 1)
+      |> tap (fn thms => tracing ("O1:\n" ^ cat_lines (map @{make_string} thms)))
       |> map (fold Thm.forall_elim cqsj')
+      |> tap (fn thms => tracing ("O2:\n" ^ cat_lines (map @{make_string} thms)))
       |> map (fold Thm.elim_implies [case_hypj'])
+      |> tap (fn thms => tracing ("O3:\n" ^ cat_lines (map @{make_string} thms)))
+      |> map (fold Thm.elim_implies agsj')
 
     val _ = tracing ("eqvtsi:\n" ^ cat_lines (map @{make_string} eqvtsi))
     val _ = tracing ("eqvtsj:\n" ^ cat_lines (map @{make_string} eqvtsj))
@@ -501,34 +513,34 @@
 
     val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj
     
-    (* val _ = tracing ("compats:\n" ^ pp_thm compat)  *)
+    val _ = tracing ("compats:\n" ^ pp_thm compat) 
     
 
     fun pppp str = tap (fn thm => tracing (str ^ ": " ^ pp_thm thm))
     fun ppp str = I
   in
     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
-    |> ppp "A"
+    |> pppp "A"
     |> Thm.implies_elim RLj_import
       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
-    |> ppp "B"
+    |> pppp "B"
     |> (fn it => trans OF [it, compat])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
-    |> ppp "C"
+    |> pppp "C"
     |> (fn it => trans OF [y_eq_rhsj'h, it])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
-    |> ppp "D"
+    |> pppp "D"
     |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
-    |> ppp "E"
+    |> pppp "E"
     |> fold_rev (Thm.implies_intr o cprop_of) agsj'
       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
-    |> ppp "F"
+    |> pppp "F"
     |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
-    |> ppp "G"
+    |> pppp "G"
     |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
-    |> ppp "H"
+    |> pppp "H"
     |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
-    |> ppp "I"
+    |> pppp "I"
   end
 *}
 
@@ -555,6 +567,8 @@
     val unique_clauses =
       map2 (mk_uniqueness_clause thy globals compat_store eqvt_lemmas clausei) clauses rep_lemmas
 
+    val _ = tracing ("DONE unique clauses") 
+
     fun elim_implies_eta A AB =
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
 
@@ -1780,8 +1794,7 @@
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(erule conjE)+
-apply(subst (asm) Abs_eq_iff3) 
-apply(erule exE)
+oops