--- a/Nominal/Ex/Typing.thy	Mon Jan 03 16:21:12 2011 +0000
+++ b/Nominal/Ex/Typing.thy	Tue Jan 04 13:47:38 2011 +0000
@@ -40,15 +40,16 @@
 *}
 
 ML {* 
-fun mk_vc_compat (avoid, avoid_trm) prems concl_args params =
+fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = 
   let
-    fun aux arg = arg
+    val vc_goal = concl_args
+      |> HOLogic.mk_tuple
       |> mk_fresh_star avoid_trm 
       |> HOLogic.mk_Trueprop
       |> (curry Logic.list_implies) prems
       |> (curry list_all_free) params
   in 
-    if null avoid then [] else map aux concl_args
+    if null avoid then [] else [vc_goal]
   end
 *}
 
@@ -192,16 +193,38 @@
     end) ctxt
 *}
 
+
 ML {*
-fun binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trms ctxt = 
+fun fresh_thm ctxt fresh_thms p c prms avoid_trm =
+  let
+    val conj1 = 
+      mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c
+    val conj2 =
+      mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) prms))) (Bound 0)
+    val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2))
+      |> HOLogic.mk_Trueprop
+
+    val _ = tracing ("fresh goal: " ^ Syntax.string_of_term ctxt fresh_goal)
+  in 
+    Goal.prove ctxt [] [] fresh_goal
+      (K (HEADGOAL (rtac @{thm at_set_avoiding2})))
+  end
+*}
+
+ML {*
+fun binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt = 
   Subgoal.FOCUS (fn {context, params, ...} =>
     let
       val thy = ProofContext.theory_of context
-      val (prms, p, _) = split_last2 (map snd params)
-      val prm_tys = map (fastype_of o term_of) prms
+      val (prms, p, c) = split_last2 (map snd params)
+      val prm_trms = map term_of prms
+      val prm_tys = map fastype_of prm_trms
       val cperms = map (cterm_of thy o perm_const) prm_tys
       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 
       val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem
+      val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm      
+
+      val fthm = fresh_thm context fresh_thms (term_of p) (term_of c) (map term_of prms) avoid_trm'
     in
       Skip_Proof.cheat_tac thy
       (* EVERY1 [rtac prem'] *)  
@@ -209,10 +232,10 @@
 *}
 
 ML {*
-fun case_tac ctxt fresh_thms Ps avoid avoid_trm intr_cvars prem =
+fun case_tac ctxt fresh_thms Ps (avoid, avoid_trm) intr_cvars param_trms prem =
   let
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
-    val tac2 = binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trm ctxt
+    val tac2 = binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt
   in 
     EVERY' [ rtac @{thm allI}, rtac @{thm allI}, eqvt_stac ctxt,
              if null avoid then tac1 else tac2 ]
@@ -220,16 +243,16 @@
 *}
 
 ML {*
-fun tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars {prems, context} =
+fun prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms {prems, context} =
   let
-    val cases_tac = map4 (case_tac context fresh_thms Ps) avoids avoid_trms intr_cvars prems
+    val cases_tac = map4 (case_tac context fresh_thms Ps) (avoids ~~avoid_trms) intr_cvars param_trms prems
   in 
     EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]
   end
 *}
 
 ML {*
-val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (\<And>c. Q ==> P (0::perm) c)" by simp}
+val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}
 *}
 
 ML {*
@@ -248,7 +271,7 @@
     val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs
     val intr_vars = (map o map) fst intr_vars_tys
     val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms
-    val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys
+    val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys      
 
     val (intr_prems, intr_concls) = intrs
       |> map prop_of
@@ -291,7 +314,7 @@
     fun after_qed ctxt_outside fresh_thms ctxt = 
       let
         val thms = Goal.prove ctxt [] ind_prems' ind_concl' 
-          (tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars) 
+          (prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms) 
           |> singleton (ProofContext.export ctxt ctxt_outside)
           |> Datatype_Aux.split_conj_thm
           |> map (fn thm => thm RS normalise)
@@ -439,6 +462,7 @@
 
 nominal_inductive typing
   avoids t_Lam: "x"
+      (* | t_Var: "x" *)
   apply -
   apply(simp_all add: fresh_star_def ty_fresh lam.fresh)?
   done
@@ -506,6 +530,7 @@
       apply(simp only: permute_plus)
       apply(rule supp_perm_eq)
       apply(simp add: supp_Pair fresh_star_Un)
+      (* apply(perm_simp) *) 
       apply(simp (no_asm) only: eqvts)
       apply(rule a3)
       apply(simp only: eqvts permute_plus)
@@ -517,6 +542,7 @@
       apply(assumption)
       apply(perm_strict_simp)
       apply(simp only:)
+      thm at_set_avoiding2
       apply(rule at_set_avoiding2)
       apply(simp add: finite_supp)
       apply(simp add: finite_supp)