
diff -r 619ecb57db38 -r 3342a2d13d95 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Fri Jan 14 14:22:25 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Sat Jan 15 20:24:16 2011 +0000
@@ -34,6 +34,17 @@
 apply(rule fin)
 done
 
+lemma fresh_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  and     fresh: "as \<sharp>* x"
+  shows "as \<sharp>* f x"
+using fresh
+unfolding fresh_star_def
+unfolding fresh_def
+using supp_eqvt_at[OF asm fin]
+by auto
+
 definition
  "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
 
@@ -151,9 +162,10 @@
 val case_split = @{thm HOL.case_split}
 val fundef_default_value = @{thm FunDef.fundef_default_value}
 val not_acc_down = @{thm not_accp_down}
+*}
 
 
-
+ML {*
 fun find_calls tree =
   let
     fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
@@ -192,13 +204,6 @@
 
 fun mk_compat_proof_obligations domT ranT fvar f glrs =
   let
-    (*
-    val _ = tracing ("domT: " ^ @{make_string} domT)
-    val _ = tracing ("ranT: " ^ @{make_string} ranT)
-    val _ = tracing ("fvar: " ^ @{make_string} fvar)
-    val _ = tracing ("f: " ^ @{make_string} f)
-    *)
- 
     fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
       let
         val shift = incr_boundvars (length qs')
@@ -210,17 +215,14 @@
           (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
             HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
         |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) 
-        |> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')
-        (*|> (curry Logic.mk_implies) @{term "Trueprop True"}*)  (* HERE *)
+        |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* HERE *) 
+        (*|> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')*) (* HERE *) 
         |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
         |> curry abstract_over fvar
         |> curry subst_bound f
       end
   in
     map mk_impl (unordered_pairs glrs)
-    (*|> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts)))
-    *)
   end
 *}
 
@@ -238,8 +240,10 @@
     |> mk_forall_rename ("x", x)
     |> mk_forall_rename ("P", Pbool)
   end
+*}
 
 (** making a context with it's own local bindings **)
+ML {*
 
 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   let
@@ -261,8 +265,9 @@
     ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
       cqs = cqs, ags = ags, case_hyp = case_hyp }
   end
+*}
 
-
+ML {*
 (* lowlevel term function. FIXME: remove *)
 fun abstract_over_list vs body =
   let
@@ -327,18 +332,33 @@
   end
 *}
 
+ML {*
+fun pp_thm thm =
+  let
+    val hyps = Thm.hyps_of thm
+    val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of thm)
+  in
+      (@{make_string} thm) ^ "\n    hyps: " ^ (commas (map (Syntax.string_of_term @{context}) hyps))
+      ^ "    tpairs: " ^   (commas (map (Syntax.string_of_term @{context}) tpairs))
+  end
+*}
+
 
 ML {*
-fun eqvt_at_elim thm =
+(*
+fun eqvt_at_elim thy (eqvts:thm list) thm =
   case (prop_of thm) of
     Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ => 
       let
-        val el_thm = Skip_Proof.make_thm @{theory} t
+        val el_thm = Skip_Proof.make_thm thy t
+        val _ = tracing ("NEED TO PROVE  " ^ @{make_string} el_thm)
+        val _ = tracing ("HAVE\n" ^ cat_lines (map @{make_string} eqvts))
       in
         Thm.elim_implies el_thm thm 
-        |> eqvt_at_elim
+        |> eqvt_at_elim thy eqvts 
       end
   | _ => thm
+*)
 *}
 
 ML {*
@@ -348,7 +368,7 @@
 
 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
 (* if j < i, then turn around *)
-fun get_compat_thm thy cts i j ctxi ctxj =
+fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
   let
     val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
@@ -357,13 +377,12 @@
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts
+      val _ = tracing ("XXXX compat clause if:\n" ^ @{make_string} compat)
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-      (*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*)
-      (*|> Thm.elim_implies @{thm TrueI}*) (* THERE *)
-      |> eqvt_at_elim 
-      (*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
+      |> fold Thm.elim_implies (rev eqvtsj) (* HERE *)
+      (*|> eqvt_at_elim thy eqvtsj *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
       |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
@@ -371,13 +390,12 @@
     else
     let
       val compat = lookup_compat_thm i j cts
+      (* val _ = tracing ("XXXX compat clause else:\n" ^ @{make_string} compat) *)
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      (*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*) 
-      (*|> Thm.elim_implies @{thm TrueI}*)
-      |> eqvt_at_elim 
-      (*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
+      |> fold Thm.elim_implies (rev eqvtsi) (* HERE *)
+      (* |> eqvt_at_elim thy eqvts *) 
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -391,7 +409,7 @@
 (* Generates the replacement lemma in fully quantified form. *)
 fun mk_replacement_lemma thy h ih_elim clause =
   let
-    val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
+    val ClauseInfo {cdata=ClauseContext {qs, cqs, ags, case_hyp, ...},
       RCs, tree, ...} = clause
     local open Conv in
       val ih_conv = arg1_conv o arg_conv o arg_conv
@@ -419,50 +437,104 @@
 *}
 
 ML {*
-fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
+fun mk_eqvt_lemma thy ih_eqvt clause =
+  let
+    val ClauseInfo {cdata=ClauseContext {cqs, case_hyp, ...}, RCs, ...} = clause
+
+    local open Conv in
+      val ih_conv = arg1_conv o arg_conv o arg_conv
+    end
+
+    val ih_eqvt_case =
+      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
+
+    fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
+        (llRI RS ih_eqvt_case)
+        |> fold_rev (Thm.implies_intr o cprop_of) CCas
+        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+  in
+    map prep_eqvt RCs
+    |> map (Thm.implies_intr (cprop_of case_hyp))
+    |> map (fold_rev Thm.forall_intr cqs)
+    |> map (Thm.close_derivation) 
+  end
+*}
+
+ML {*
+fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
   let
     val Globals {h, y, x, fvar, ...} = globals
-    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
+    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ...}, ...} = clausei
     val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
 
     val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
-      mk_clause_context x ctxti cdescj
+      mk_clause_context x ctxti cdescj 
 
     val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
-    val compat = get_compat_thm thy compat_store i j cctxi cctxj
 
     val Ghsj' = map 
       (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
 
+    val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+    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 case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
+
     val RLj_import = RLj
       |> fold Thm.forall_elim cqsj'
       |> fold Thm.elim_implies agsj'
       |> fold Thm.elim_implies Ghsj'
 
-    val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
-    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 eqvtsi = nth eqvts (i - 1)
+      |> map (fold Thm.forall_elim cqsi)
+      |> map (fold Thm.elim_implies [case_hyp])
+
+    val eqvtsj = nth eqvts (j - 1)
+      |> map (fold Thm.forall_elim cqsj')
+      |> map (fold Thm.elim_implies [case_hypj'])
+
+    val _ = tracing ("eqvtsi:\n" ^ cat_lines (map @{make_string} eqvtsi))
+    val _ = tracing ("eqvtsj:\n" ^ cat_lines (map @{make_string} eqvtsj))
+    val _ = tracing ("case_hypi:\n" ^ @{make_string} case_hyp)
+    val _ = tracing ("case_hypj:\n" ^ @{make_string} case_hypj')
+
+    val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj
+    
+    (* 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"
     |> Thm.implies_elim RLj_import
       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
+    |> ppp "B"
     |> (fn it => trans OF [it, compat])
       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+    |> ppp "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"
     |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
+    |> ppp "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"
     |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
+    |> ppp "G"
     |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
+    |> ppp "H"
     |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
+    |> ppp "I"
   end
 *}
 
-(* HERE *)
 
 ML {*
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas eqvt_lemmas clausei =
   let
     val Globals {x, y, ranT, fvar, ...} = globals
     val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
@@ -470,9 +542,10 @@
 
     val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
 
-    fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
-      |> fold_rev (Thm.implies_intr o cprop_of) CCas
-      |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+    fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 
+        (llRI RS ih_intro_case)
+        |> fold_rev (Thm.implies_intr o cprop_of) CCas
+        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
 
     val existence = fold (curry op COMP o prep_RC) RCs lGI
 
@@ -480,11 +553,7 @@
     val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
     val unique_clauses =
-      map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
-     
-    (*
-    val _ = tracing ("unique_clauses\n" ^ cat_lines (map @{make_string} unique_clauses))
-    *)
+      map2 (mk_uniqueness_clause thy globals compat_store eqvt_lemmas clausei) clauses rep_lemmas
 
     fun elim_implies_eta A AB =
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
@@ -521,8 +590,6 @@
   end
 *}
 
-ML Thm.forall_elim_vars
-ML Thm.implies_intr
 
 ML {* (ex1_implies_ex, ex1_implies_un) *}
 thm fundef_ex1_eqvt_at
@@ -546,43 +613,33 @@
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
 
-
-    val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm)
-    val _ = tracing ("ih_intro\n" ^ @{make_string} ih_intro)
-    val _ = tracing ("ih_elim\n" ^ @{make_string} ih_elim)
-    val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
+    (*
+    val _ = tracing ("ihyp_thm\n" ^ pp_thm ihyp_thm)
+    val _ = tracing ("ih_intro\n" ^ pp_thm ih_intro)
+    val _ = tracing ("ih_elim\n" ^ pp_thm ih_elim)
+    val _ = tracing ("ih_eqvt\n" ^ pp_thm ih_eqvt)
+    *)
 
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
 
-    val _ = tracing (cat_lines (map @{make_string} repLemmas))
+    val _ = trace_msg (K "Proving Equivariance lemmas...")
+    val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
 
     val _ = trace_msg (K "Proving cases for unique existence...")
     val (ex1s, values) =
       split_list (map (mk_uniqueness_case thy globals G f 
-        ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+        ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)
      
-    val _ = tracing ("ex1s\n" ^ cat_lines (map @{make_string} ex1s))
-    val _ = tracing ("values\n" ^ cat_lines (map @{make_string} values)) 
-
     val _ = trace_msg (K "Proving: Graph is a function")
     val graph_is_function = complete
-      |> tap (fn th => tracing ("A\n" ^ @{make_string} th))
       |> Thm.forall_elim_vars 0
-      |> tap (fn th => tracing ("B\n" ^ @{make_string} th))
       |> fold (curry op COMP) ex1s
-      |> tap (fn th => tracing ("C\n" ^ @{make_string} th))
       |> Thm.implies_intr (ihyp)
-      |> tap (fn th => tracing ("D\n" ^ @{make_string} th))
       |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
-      |> tap (fn th => tracing ("E\n" ^ @{make_string} th))
       |> Thm.forall_intr (cterm_of thy x)
-      |> tap (fn th => tracing ("F\n" ^ @{make_string} th))
       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
-      |> tap (fn th => tracing ("G\n" ^ @{make_string} th))
       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
-      |> tap (fn th => tracing ("H\n" ^ @{make_string} th))
-
 
     val goalstate =  Conjunction.intr graph_is_function complete
       |> Thm.close_derivation
@@ -1078,33 +1135,33 @@
       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
     (* 
-    val _ = tracing ("Graph - name: " ^ @{make_string} G)
-    val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms))
-    val _ = tracing ("Graph Equivariance " ^ @{make_string} G_eqvt)
+    val _ = tracing ("Graph - name: " ^ pp_thm G)
+    val _ = tracing ("Graph intros:\n" ^ cat_lines (map pp_thm GIntro_thms))
+    val _ = tracing ("Graph Equivariance " ^ pp_thm G_eqvt)
     *)
 
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
     (*
-    val _ = tracing ("f - name: " ^ @{make_string} f)
-    val _ = tracing ("f_defthm:\n" ^ @{make_string} f_defthm)
+    val _ = tracing ("f - name: " ^ pp_thm f)
+    val _ = tracing ("f_defthm:\n" ^ pp_thm f_defthm)
     *)
 
     val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
     val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
 
     (*
-    val _ = tracing ("recursive calls:\n" ^ cat_lines (map @{make_string} RCss))
+    val _ = tracing ("recursive calls:\n" ^ cat_lines (map pp_thm RCss))
     *)
 
     val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 
     (*
-    val _ = tracing ("Relation - name: " ^ @{make_string} R) 
-    val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss))
-    val _ = tracing ("Relation Equivariance " ^ @{make_string} R_eqvt)
+    val _ = tracing ("Relation - name: " ^ pp_thm R) 
+    val _ = tracing ("Relation intros:\n" ^ cat_lines (map pp_thm RIntro_thmss))
+    val _ = tracing ("Relation Equivariance " ^ pp_thm R_eqvt)
     *)    
 
     val (_, lthy) =
@@ -1129,19 +1186,16 @@
     val compat_store = store_compat_thms n compat
 
     (*
-    val _ = tracing ("globals:\n" ^ @{make_string} globals)
-    val _ = tracing ("complete:\n" ^ @{make_string} complete)
-    val _ = tracing ("compat:\n" ^ @{make_string} compat)
-    val _ = tracing ("compat_store:\n" ^ @{make_string} compat_store)
+    val _ = tracing ("globals:\n" ^ pp_thm globals)
+    val _ = tracing ("complete:\n" ^ pp_thm complete)
+    val _ = tracing ("compat:\n" ^ pp_thm compat)
+    val _ = tracing ("compat_store:\n" ^ pp_thm compat_store)
     *)
 
     val (goalstate, values) = PROFILE "prove_stuff"
       (prove_stuff lthy globals G f R xclauses complete compat
          compat_store G_elim G_eqvt) f_defthm
      
-    val _ = tracing ("goalstate prove_stuff thm:\n" ^ @{make_string} goalstate)
-    val _ = tracing ("values prove_stuff thms:\n" ^ cat_lines (map @{make_string} values))
-
     val mk_trsimps =
       mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
 
@@ -1585,16 +1639,11 @@
   let
     val ((goal_state, afterqed), lthy') =
       prepare_function is_external prep default_constraint fixspec eqns config lthy
-
-    val _ = tracing ("goal state:\n" ^ @{make_string} goal_state)
-    val _ = tracing ("concl of goal state:\n" ^ Syntax.string_of_term lthy' (concl_of goal_state))
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
- (*|> tap (fn x => tracing ("after thm:\n" ^ Pretty.string_of (Pretty.chunks (Proof.pretty_goals true x))))*)
     |> Proof.refine (Method.primitive_text (K goal_state)) 
     |> Seq.hd
- (*|> tap (fn x => tracing ("after ref:\n" ^ Pretty.string_of (Pretty.chunks (Proof.pretty_goals true x))))*)
   end
 *}
 
@@ -1683,6 +1732,76 @@
 apply(simp_all only: lam.distinct)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
+apply(subst (asm) Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(clarify)
+oops
+
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+by (induct xs) (auto)
+
+nominal_primrec 
+  frees_lst :: "lam \<Rightarrow> atom list"
+where
+  "frees_lst (Var x) = [atom x]"
+| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
+| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
+apply(rule_tac y="x" in lam.exhaust)
+apply(simp_all)[3]
+apply(simp_all only: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+oops
+
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
+where
+  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
+apply(simp_all add: lam.distinct)[5]
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(erule conjE)+
+apply(subst (asm) Abs_eq_iff3) 
+apply(erule exE)
+
+
+
+nominal_primrec
+  depth :: "lam \<Rightarrow> nat"
+where
+  "depth (Var x) = 1"
+| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
+| "depth (Lam x t) = (depth t) + 1"
+apply(rule_tac y="x" in lam.exhaust)
+apply(simp_all)[3]
+apply(simp_all only: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+(*
+apply(subst (asm) Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(clarify)
+*)
 apply(subgoal_tac "finite (supp (x, xa, t, ta, depth_sumC t, depth_sumC ta))")
 apply(erule_tac ?'a="name" in obtain_at_base)
 unfolding fresh_def[symmetric]
@@ -1719,6 +1838,31 @@
   unfolding permute_set_eq
   using a by (auto simp add: permute_flip_at)
 
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+by (induct xs) (auto)
+
+nominal_primrec 
+  frees_lst :: "lam \<Rightarrow> atom list"
+where
+  "frees_lst (Var x) = [atom x]"
+| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
+| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
+apply(rule_tac y="x" in lam.exhaust)
+apply(simp_all)[3]
+apply(simp_all only: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+oops
 
 nominal_primrec 
   frees :: "lam \<Rightarrow> name set"
@@ -1745,6 +1889,116 @@
 apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst)
 oops
 
+thm Abs_eq_iff[simplified alphas]
+
+lemma Abs_set_eq_iff2:
+  fixes x y::"'a::fs"
+  shows "[bs]set. x = [cs]set. y \<longleftrightarrow>
+    (\<exists>p. supp ([bs]set. x) = supp ([cs]set. y) \<and>
+         supp ([bs]set. x) \<sharp>* p \<and>
+         p \<bullet> x = y \<and> p \<bullet> bs = cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+by simp
+
+lemma Abs_set_eq_iff3:
+  fixes x y::"'a::fs"
+  assumes a: "finite bs" "finite cs"
+  shows "[bs]set. x = [cs]set. y \<longleftrightarrow>
+    (\<exists>p. supp ([bs]set. x) = supp ([cs]set. y) \<and>
+         supp ([bs]set. x) \<sharp>* p \<and>
+         p \<bullet> x = y \<and> p \<bullet> bs = cs \<and>
+         supp p \<subseteq> bs \<union> cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+apply(auto)
+using set_renaming_perm
+sorry
+
+lemma Abs_eq_iff2:
+  fixes x y::"'a::fs"
+  shows "[bs]lst. x = [cs]lst. y \<longleftrightarrow>
+    (\<exists>p. supp ([bs]lst. x) = supp ([cs]lst. y) \<and>
+         supp ([bs]lst. x) \<sharp>* p \<and>
+         p \<bullet> x = y \<and> p \<bullet> bs = cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+by simp
+
+lemma Abs_eq_iff3:
+  fixes x y::"'a::fs"
+  shows "[bs]lst. x = [cs]lst. y \<longleftrightarrow>
+    (\<exists>p. supp ([bs]lst. x) = supp ([cs]lst. y) \<and>
+         supp ([bs]lst. x) \<sharp>* p \<and>
+         p \<bullet> x = y \<and> p \<bullet> bs = cs \<and>
+         supp p \<subseteq> set bs \<union> set cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+apply(auto)
+using list_renaming_perm
+apply -
+apply(drule_tac x="bs" in meta_spec)
+apply(drule_tac x="p" in meta_spec)
+apply(erule exE)
+apply(rule_tac x="q" in exI)
+apply(simp add: set_eqvt)
+sorry
+
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
+where
+  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
+apply(simp_all add: lam.distinct)[5]
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(erule conjE)+
+apply(subst (asm) Abs_eq_iff3) 
+apply(erule exE)
+apply(erule conjE)+
+apply(clarify)
+apply(perm_simp)
+apply(simp)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(drule fresh_star_supp_conv)
+apply(simp add: Abs_fresh_star_iff)
+thm fresh_eqvt_at
+apply(rule_tac f="subst_sumC" in fresh_eqvt_at)
+apply(assumption)
+apply(simp add: finite_supp)
+prefer 2
+apply(simp)
+apply(simp add: eqvt_at_def)
+apply(perm_simp)
+apply(subgoal_tac "p \<bullet> ya = ya")
+apply(subgoal_tac "p \<bullet> sa = sa")
+apply(simp)
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+
+
+
 nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where




